package lutin

  1. Overview
  2. Docs

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 t = {
  1. var : vars_domain;
  2. substl : Ne.subst list;
  3. delay : Constraint.ineq list;
  4. untouched : Exp.var list;
}
and vars_domain =
  1. | Unsat of Constraint.t * t
  2. | Range of range_store
val create : Exp.var list -> t

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 -> t

add_constraint s c returns the store s with the numeric constraint c added.

val is_store_satisfiable : int -> t -> bool

Returns false iff one of the variable domain is empty.

type p = (Var.vnt list * Poly.t * (int -> string) * Constraint.ineq list) list

Convex Polyhedron.

type t' = {
  1. range : range_store;
  2. substl' : Ne.subst list;
  3. untouched' : Exp.var list;
}

contains basically the same info as t with a few fields removed

exception No_polyedral_solution

Raised by the 2 functions below

val switch_to_polyhedron_representation : int -> t -> t' * p

switch_to_polyhedron_representation store is called when all the constraints have been handled, and returns a range-based and a list of polyhedra (cf the algorithm above).

Raises No_polyedral_solution if that conversion fails

OCaml

Innovation. Community. Security.