```1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 ``` ```--- This library provides a Boolean Constraint Solver based on BDDs. --- --- @author Sebastian Fischer --- @version May 2006 --- @category general module CLPB ( Boolean, true, false, neg, (.&&), (.||), (./=), (.==), (.<=), (.>=), (.<), (.>), count, exists, satisfied, check, bound, simplify, evaluate ) where infixr 3 .&& infixr 2 .|| infix 1 ./=, .== data Boolean = B Int -- abstract deriving (Eq,Show) --- The always satisfied constraint true :: Boolean true = B 1 --- The never satisfied constraint false :: Boolean false = B 0 --- Result is true iff argument is false. neg :: Boolean -> Boolean neg (B x) = B (prim_neg \$! x) prim_neg :: Int -> Int prim_neg external --- Result is true iff both arguments are true. (.&&) :: Boolean -> Boolean -> Boolean (B x) .&& (B y) = B ((prim_and \$!y) \$! x) prim_and :: Int -> Int -> Int prim_and external --- Result is true iff at least one argument is true. (.||) :: Boolean -> Boolean -> Boolean (B x) .|| (B y) = B ((prim_or \$!y) \$! x) prim_or :: Int -> Int -> Int prim_or external --- Result is true iff exactly one argument is true. (./=) :: Boolean -> Boolean -> Boolean (B x) ./= (B y) = B ((prim_xor \$!y) \$! x) prim_xor :: Int -> Int -> Int prim_xor external --- Result is true iff both arguments are equal. (.==) :: Boolean -> Boolean -> Boolean x .== y = neg x ./= y --- Result is true iff the first argument implies the second. (.<=) :: Boolean -> Boolean -> Boolean x .<= y = neg x .|| y --- Result is true iff the second argument implies the first. (.>=) :: Boolean -> Boolean -> Boolean x .>= y = y .<= x --- Result is true iff the first argument is false and the second is true. (.<) :: Boolean -> Boolean -> Boolean x .< y = neg x .&& y --- Result is true iff the first argument is true and the second is false. (.>) :: Boolean -> Boolean -> Boolean x .> y = y .< x --- Result is true iff the count of valid constraints in the first list --- is an element of the second list. count :: [Boolean] -> [Int] -> Boolean count bs ns = B ((card \$!! map ensureNotFree (ensureSpine ns)) \$!! map int (ensureSpine bs)) card :: [Int] -> [Int] -> Int card external --- Result is true, if the first argument is a variable which can be --- instantiated such that the second argument is true. exists :: Boolean -> Boolean -> Boolean exists (B v) (B b) = B ((prim_exists \$!! v) \$!! b) prim_exists :: Int -> Int -> Int prim_exists external --- Checks the consistency of the constraint with regard to the accumulated --- constraints, and, if the check succeeds, tells the constraint. satisfied :: Boolean -> Bool satisfied (B b) = sat \$!! b sat :: Int -> Bool sat external --- Asks whether the argument (or its negation) is now entailed by the --- accumulated constraints. Fails if it is not. check :: Boolean -> Bool check (B b) = (prim_check \$!! b) == 1 prim_check :: Int -> Int prim_check external --- Instantiates given variables with regard to the accumulated constraints. bound :: [Boolean] -> Bool bound bs = labeling \$!! map int (ensureSpine bs) labeling :: [Int] -> Bool labeling external --- Simplifies the argument with regard to the accumulated constraints. simplify :: Boolean -> Boolean simplify b | satisfied (a .== b) = a where a free --- Evaluates the argument with regard to the accumulated constraints. evaluate :: Boolean -> Bool evaluate x | bound [y] = int y == 1 where y = simplify x -- private int :: Boolean -> Int int (B x) = x ```