• Erwan Jahier's avatar
    lurette 0.122 Mon, 17 Feb 2003 14:50:50 +0100 by jahier · 78f40b65
    Erwan Jahier authored
    Parent-Version:      0.121
    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.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).
       One of the main change is that now, draw_in_bdd returns 2 stores.
       One is Range based, the other one is polyhedron-based.
       Add the function switch_to_polyhedron_representation which
       handle delayed constraint if necessary. It is meant to be called
       at bdd leaves.
       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.
       Implement get_vars that retreive the variables occuring in a contraint
       or an expression.
    Project-Description: Lurette
luc_exe.ml 12 KB