package lutin
-
lutin
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
package lutin
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
Numeric constraint store.
The algorithm is (roughly) the following: constraints are added one by one to the store. Constraints that involve more than one variable are delayed; the other ones are handled by a range-based (interval) store. Each time an equality constraint is added, we substitute it in the list of delayed variables. Some of the delayed constraints can therefore turn out to be of dimension 1; they are thus awaken and added to the range-based store.
At the end of that process, namely, when all constraints have been added, the constraints in the delayed list are transformed into polyhedra. Independant polyhedra should be detected here as some polyhedron operations are exponential into their dimension. Moreover, it is easy to do.
type range_store = Polyhedron.range Util.StringMap.ttype t = {var : vars_domain;substl : Ne.subst list;delay : Constraint.ineq list;untouched : Exp.var list;
}Store.create varl returns an initial store (the universe) for the variable contained in varl.
val add_constraint : t -> Formula_to_bdd.t -> Constraint.t -> tadd_constraint s c returns the store s with the numeric constraint c added.
val is_store_satisfiable : int -> t -> boolReturns false iff one of the variable domain is empty.
type p = (Var.vnt list * Poly.t * (int -> string) * Constraint.ineq list) listConvex Polyhedron.
contains basically the same info as t with a few fields removed