This library provides a Boolean Constraint Solver based on BDDs.
Author: Sebastian Fischer
Version: May 2006
true
:: Boolean
The always satisfied constraint 
false
:: Boolean
The never satisfied constraint 
neg
:: Boolean > Boolean
Result is true iff argument is false. 
(.&&)
:: Boolean > Boolean > Boolean
Result is true iff both arguments are true. 
(.)
:: Boolean > Boolean > Boolean
Result is true iff at least one argument is true. 
(./=)
:: Boolean > Boolean > Boolean
Result is true iff exactly one argument is true. 
(.==)
:: Boolean > Boolean > Boolean
Result is true iff both arguments are equal. 
(.<=)
:: Boolean > Boolean > Boolean
Result is true iff the first argument implies the second. 
(.>=)
:: Boolean > Boolean > Boolean
Result is true iff the second argument implies the first. 
(.<)
:: Boolean > Boolean > Boolean
Result is true iff the first argument is false and the second is true. 
(.>)
:: Boolean > Boolean > Boolean
Result is true iff the first argument is true and the second is false. 
count
:: [Boolean] > [Int] > Boolean
Result is true iff the count of valid constraints in the first list is an element of the second list. 
exists
:: Boolean > Boolean > Boolean
Result is true, if the first argument is a variable which can be instantiated such that the second argument is true. 
satisfied
:: Boolean > Bool
Checks the consistency of the constraint with regard to the accumulated constraints, and, if the check succeeds, tells the constraint. 
check
:: Boolean > Bool
Asks whether the argument (or its negation) is now entailed by the accumulated constraints. 
bound
:: [Boolean] > Bool
Instantiates given variables with regard to the accumulated constraints. 
simplify
:: Boolean > Boolean
Simplifies the argument with regard to the accumulated constraints. 
evaluate
:: Boolean > Bool
Evaluates the argument with regard to the accumulated constraints. 
Constructors:
The always satisfied constraint

The never satisfied constraint

Result is true iff both arguments are true.

Result is true iff at least one argument is true.

Result is true iff exactly one argument is true.

Result is true iff both arguments are equal.

Result is true iff the first argument is false and the second is true. 
Result is true iff the first argument is true and the second is false. 
Result is true iff the count of valid constraints in the first list is an element of the second list. 
Result is true, if the first argument is a variable which can be instantiated such that the second argument is true. 
Checks the consistency of the constraint with regard to the accumulated constraints, and, if the check succeeds, tells the constraint. 
Asks whether the argument (or its negation) is now entailed by the accumulated constraints. Fails if it is not. 