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