Module CLPB

This library provides a Boolean Constraint Solver based on BDDs.

Author: Sebastian Fischer

Version: May 2006

Summary of exported operations:

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.

Exported datatypes:


Boolean

Constructors:


Exported operations:

true :: Boolean   

The always satisfied constraint

Further infos:
  • solution complete, i.e., able to compute all solutions

false :: Boolean   

The never satisfied constraint

Further infos:
  • solution complete, i.e., able to compute all solutions

neg :: Boolean -> Boolean   

Result is true iff argument is false.

(.&&) :: Boolean -> Boolean -> Boolean   

Result is true iff both arguments are true.

Further infos:
  • defined as right-associative infix operator with precedence 3

(.||) :: Boolean -> Boolean -> Boolean   

Result is true iff at least one argument is true.

Further infos:
  • defined as right-associative infix operator with precedence 2

(./=) :: Boolean -> Boolean -> Boolean   

Result is true iff exactly one argument is true.

Further infos:
  • defined as non-associative infix operator with precedence 1

(.==) :: Boolean -> Boolean -> Boolean   

Result is true iff both arguments are equal.

Further infos:
  • defined as non-associative infix operator with precedence 1

(.<=) :: 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. Fails if it is not.

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.