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

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

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