wax-lib.theo
Make.Constraint
wax-lib
wax-lib.conversion
wax-lib.utils
wax-lib.wasm
wax-lib.wax
type t = atomic_constraint list
val bool : 'kind Var.t -> bool -> t
bool v b creates a constraint asserting that boolean variable v has value b.
bool v b
v
b
val not : t -> t
not c negates the constraint c. Supports only single atomic constraints.
not c
c
Invalid_argument
if c is not a single atomic constraint.
val and_ : t -> t -> t
and_ c1 c2 combines two constraints with logical AND.
and_ c1 c2
val or_ : t -> t -> t
or_ c1 c2 combines two constraints with logical OR.
or_ c1 c2
always. Disjunctions cannot be represented as a simple list of atomic constraints. Use full BDDs for disjunctions.