# 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.

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.