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