 17 Mar, 2010 5 commits


Erwan Jahier authored
ParentVersion: 0.120 VersionLog: source/pnumsolver.ml: source/pnumsolver.mli: [new files] Implements a numeric solver based on Polka. (not plugged yet). source/rnumsolver.ml: Reimplement split_store so that it uses 2 calls of add_constraint instead of doing the work twice inside split_store (in order to avoid code duplication). Also, whenever delayed constraints becomes of dimension 1, when a add_constraint binds a value, add them to the store. Enhance error msgs whenever int and float are mixed in the same lucky expressions. source/rnumsolver.ml: source/ne.ml: rename Ne.resolve_triangular_system into get_subst_from_solved_system and move it into rnumsolver. The rational is that is was not really solving any triangular system: the system ougth to be already solved. source/parce_env.ml: Set the max_float to max_int, otherwise, the conversion into polka rational fails... ProjectDescription: Lurette

Erwan Jahier authored
ParentVersion: 0.98 VersionLog: source/solver.ml: source/rnumsolver.mli,.ml: source/constraint.ml,.mli: Split the Constraint.t type into t and ineq where inequalities are in ineq. The rational is that most operations on constaint.t are actually done on ineq. This change therefore avoid pattern like <<_ > assert false>> and let the type checher check that sort of things. ProjectDescription: Lurette

Erwan Jahier authored
ParentVersion: 0.96 VersionLog: Handling equalities smartlier. . ProjectDescription: Lurette

Erwan Jahier authored
ParentVersion: 0.95 VersionLog: source/ne.ml,mli: source/value.ml,mli: (new files) put everything that is related to normal expressions and values in thoses 2 new modules. source/ne.ml,mli: source/gne.ml,mli: Make the normal expressions and the guarded normal expression abstract. source/solver.ml: also fix a bug in the previous change (forgot to try make test ...) ProjectDescription: Lurette

Erwan Jahier authored
ParentVersion: 0.93 VersionLog: Prepare things for the next change (which will try to handle equalities smartly). source/solver.ml: source/rnumsolver.ml: atomic_formula do not need both < and > (ditto for <= and >=). Indeed, I just need to take the opposite, and everything is fine. One advantage is that there are less cases to handle. But the key advantage is that it make the representation of constraint normal, which is important at least when I will try to detect equalities. Also add a subst list and constraint list fields to the store that will ebe used in the forthcoming change. They will resp. be used for removeing a dimension when an equality is encountered and to delay constraint with more than one variable. source/constraint.ml,mli: (new files) Move there from formula.ml everything that is related to the internal representation of constraints. Also change the name of atomic_formula to linear_constraint, which is more informative. ProjectDescription: Lurette
