-
Erwan Jahier authored
Parent-Version: 0.121 Version-Log: When delayed constraints are remaining at bdd leaves, we were printing a message saying that one shoud use a polyhedron solver based instead. Now, I really call such a polyhedron solver in order to solve those constraints. This means that I use to different solvers to handle interval and polyhedron of dimension > 1. It also means that the satisfiability of constraints over polyhedra is only checked at bdd leaves, which, in some circumstances, migth be inefficient. The point is that, if we chose to check the formula satisfiability during the bdd traversal, we take the risk that a very polyhedron is created whereas it was not necessary (because of forthcoming equalities). And creating polyhedron with big (>15) dimension simply runs forever, which is really bad. nb : drawing in poyhedron not yet plugged. source/polyhedron.ml: source/polyhedron.mli: (new files) misc functions over polyhedra. The rational for creating that file is that rnumsolver is already much too big (and should be splitted some more btw). source/solver.ml: One of the main change is that now, draw_in_bdd returns 2 stores. One is Range based, the other one is polyhedron-based. source/rnumsolver.mli: source/rnumsolver.ml: Add the function switch_to_polyhedron_representation which handle delayed constraint if necessary. It is meant to be called at bdd leaves. source/solver.ml: source/rnumsolver.ml: Also do not use split_store anymore but add_constraint. This allows a much more elegant and efficient implementation of draw_in_bdd and draw_in_bdd_eq (Now the store is buid when and only when a new branch should be tried because of backtracking). It is also more efficient. source/constraint.mli source/constraint.ml source/ne.mli source/ne.ml Implement get_vars that retreive the variables occuring in a contraint or an expression. Project-Description: Lurette
78f40b65