-
Erwan Jahier authored
Parent-Version: 0.93 Version-Log: 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. Project-Description: Lurette
f8219704