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