Skip to content
  • Erwan Jahier's avatar
    lurette 0.95 Mon, 30 Sep 2002 09:32:45 +0200 by jahier · 9f11061a
    Erwan Jahier authored
    Parent-Version:      0.94
    Version-Log:
    
    Continue to prepare things for the next change (which will try to
    handle equalities smartly).
    
    test/test*.res:
       fix the expected results as this change adds a random toss
       that disturbs the random values.
    
    source/solver.ml:
    source/rnumsolver.ml:
       Add code to handle the fact that the negation of a equality
       is the disjunction of two inegalities, which can not be added
       to store as it is. So we first try with >, and if it fails,
       we try with < (or the other way aroung, depending on a fair toss).
    
       Also split up the code in Solver.draw_in_bdd depending on the
       fact that the current constraint is a boolean, an eq, or an ineg.
    
    source/solver.ml:
       split toss_up_one_var into toss_up_one_var and toss_up_one_var_index,
       one performing the the toss from a var, the other one from a var index.
    
    Project-Description: Lurette
    9f11061a