Module Cube (.ml)

module Cube: sig .. end
Cubes and simplifications


Cubes and simplifications
type t = private {
   vars : Variable.t list; (*existential variables, all distinct*)
   litterals : Types.SAtom.t; (*conjunction of litterals as a set*)
   array : Types.ArrayAtom.t; (*conjunction of litterals as an array*)
}
the type of cubes, i.e. a conjunction of litterals existentially quanfified by distinct variables. The invariant that the array and the set correspond to the same conjunction is enforced.
val create : Variable.t list -> Types.SAtom.t -> t
create a cube given its existential variables and a conjunction
val normal_form : t -> t
puts a cube in normal form, so as to have the existential variables contiguous (#1, #2, #3, ...). Performs variable renaming if necessary.
val create_normal : Types.SAtom.t -> t
create a cube in normal form by finding the quantified variables
val subst : Variable.subst -> t -> t
apply a substitution on a cube
val dim : t -> int
returns the number of exitential distinct variables, i.e. the dimension of the cube
val size : t -> int
returns the number of atoms in the conjuction

Inconsistencies detection



The following five functions implements cheap checks for detecting inconsistencies
val inconsistent : ?use_sets:bool -> t -> bool
val inconsistent_2 : ?use_sets:bool -> t -> t -> bool
is the conjunction of c1 and c2 inconsistent knowing that c1 and c2 are consitent on their own.
val inconsistent_set : Types.SAtom.t -> bool
returns true if the conjunction inconsistent
val inconsistent_array : Types.ArrayAtom.t -> bool
same as Cube.inconsistent_set but for arrays
val inconsistent_2arrays : Types.ArrayAtom.t -> Types.ArrayAtom.t -> bool
same as Cube.inconsistent_2 but for arrays

Simplifications of cubes


val simplify_atoms_base : Types.SAtom.t -> Types.SAtom.t -> Types.SAtom.t
simplify_atoms_base b c simplifies c in the context of b. Raises Exit if it becomes inconsistent
val simplify_atoms : Types.SAtom.t -> Types.SAtom.t
simplify a conjunction. Raises Exit if it becomes inconsistent.
val simplify : t -> t
simplify a cube. Raises Exit if it becomes inconsistent.
val elim_ite_simplify_atoms : Types.SAtom.t -> Types.SAtom.t list
lifts if-then-else constructs and simplify a conjunction
val elim_ite_simplify : t -> t list
lifts if-then-else constructs and simplify a cube

Misc


val resolve_two : t -> t -> t option
val satom_globs : Types.SAtom.t -> Types.Term.Set.t
val print : Format.formatter -> t -> unit