-
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