Skip to content
  • Erwan Jahier's avatar
    lurette 0.94 Fri, 27 Sep 2002 13:20:05 +0200 by jahier · f8219704
    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