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
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
------------------------------------------------------------------------------
--- Library for finite domain constraint solving.
--- <p>
--- The general structure of a specification of an FD problem is as follows:
--- 
--- <code>domain_constraint & fd_constraint & labeling</code>
--- 
--- where:
--- 
--- <code>domain_constraint</code>
--- specifies the possible range of the FD variables (see constraint <code>domain</code>)
--- 
--- <code>fd_constraint</code>
--- specifies the constraint to be satisfied by a valid solution
--- (see constraints #+, #-, allDifferent, etc below)
--- 
--- <code>labeling</code>
--- is a labeling function to search for a concrete solution.
---
--- Note: This library is based on the corresponding library of Sicstus-Prolog
--- but does not implement the complete functionality of the
--- Sicstus-Prolog library.
--- However, using the PAKCS interface for external functions, it is relatively
--- easy to provide the complete functionality.
---
--- @author Michael Hanus
--- @version June 2012
--- @category general
------------------------------------------------------------------------------

module CLPFD(domain, (+#), (-#), (*#), (=#), (/=#), (<#), (<=#), (>#), (>=#),
             Constraint, (#=#), (#/=#), (#<#), (#<=#), (#>#), (#>=#),
             neg, (#/\#), (#\/#), (#=>#), (#<=>#), solve,
             sum, scalarProduct, allDifferent, all_different, count,
             indomain, labeling, LabelingOption(..)) where

-- The operator declarations are similar to the standard arithmetic
-- and relational operators.

infixl 7 *#
infixl 6 +#, -#
infix  4 =#, /=#, <#, <=#, >#, >=#
infix  4 #=#, #/=#, #<#, #<=#, #>#, #>=#
infixr 3 #/\#
infixr 2 #\/#
infixr 1 #=>#, #<=>#


--- Constraint to specify the domain of all finite domain variables.
--- @param xs - list of finite domain variables
--- @param min - minimum value for all variables in xs
--- @param max - maximum value for all variables in xs

domain :: [Int] -> Int -> Int -> Bool
domain vs l u = ((prim_domain $!! (ensureSpine vs)) $# l) $# u

prim_domain :: [Int] -> Int -> Int -> Bool
prim_domain external

--- Addition of FD variables.
(+#)   :: Int -> Int -> Int
x +# y = (prim_FD_plus $! y) $! x

prim_FD_plus :: Int -> Int -> Int
prim_FD_plus external

--- Subtraction of FD variables.
(-#)   :: Int -> Int -> Int
x -# y = (prim_FD_minus $! y) $! x

prim_FD_minus :: Int -> Int -> Int
prim_FD_minus external

--- Multiplication of FD variables.
(*#)   :: Int -> Int -> Int
x *# y = (prim_FD_times $! y) $! x

prim_FD_times :: Int -> Int -> Int
prim_FD_times external

--- Equality of FD variables.
(=#)   :: Int -> Int -> Bool
x =# y = (prim_FD_equal $! y) $! x

prim_FD_equal :: Int -> Int -> Bool
prim_FD_equal external

--- Disequality of FD variables.
(/=#)  :: Int -> Int -> Bool
x /=# y = (prim_FD_notequal $! y) $! x

prim_FD_notequal :: Int -> Int -> Bool
prim_FD_notequal external

--- "Less than" constraint on FD variables.
(<#)   :: Int -> Int -> Bool
x <# y = (prim_FD_le $! y) $! x

prim_FD_le :: Int -> Int -> Bool
prim_FD_le external

--- "Less than or equal" constraint on FD variables.
(<=#)  :: Int -> Int -> Bool
x <=# y = (prim_FD_leq $! y) $! x

prim_FD_leq :: Int -> Int -> Bool
prim_FD_leq external

--- "Greater than" constraint on FD variables.
(>#)   :: Int -> Int -> Bool
x ># y = (prim_FD_ge $! y) $! x

prim_FD_ge :: Int -> Int -> Bool
prim_FD_ge external

--- "Greater than or equal" constraint on FD variables.
(>=#)  :: Int -> Int -> Bool
x >=# y = (prim_FD_geq $! y) $! x

prim_FD_geq :: Int -> Int -> Bool
prim_FD_geq external

---------------------------------------------------------------------------
-- Reifyable constraints.

--- A datatype to represent reifyable constraints.
data Constraint = FDEqual Int Int
                | FDNotEqual Int Int
                | FDGreater Int Int
                | FDGreaterOrEqual Int Int
                | FDLess Int Int
                | FDLessOrEqual Int Int
                | FDNeg   Constraint
                | FDAnd   Constraint Constraint
                | FDOr    Constraint Constraint
                | FDImply Constraint Constraint
                | FDEquiv Constraint Constraint

--- Reifyable equality constraint on FD variables.
(#=#)  :: Int -> Int -> Constraint
x #=# y = FDEqual x y

--- Reifyable inequality constraint on FD variables.
(#/=#)  :: Int -> Int -> Constraint
x #/=# y = FDNotEqual x y

--- Reifyable "less than" constraint on FD variables.
(#<#)  :: Int -> Int -> Constraint
x #<# y = FDLess x y

--- Reifyable "less than or equal" constraint on FD variables.
(#<=#)  :: Int -> Int -> Constraint
x #<=# y = FDLessOrEqual x y

--- Reifyable "greater than" constraint on FD variables.
(#>#)  :: Int -> Int -> Constraint
x #># y = FDGreater x y

--- Reifyable "greater than or equal" constraint on FD variables.
(#>=#)  :: Int -> Int -> Constraint
x #>=# y = FDGreaterOrEqual x y

--- The resulting constraint is satisfied if both argument constraints
--- are satisfied.
neg :: Constraint -> Constraint
neg x = FDNeg x

--- The resulting constraint is satisfied if both argument constraints
--- are satisfied.
(#/\#)  :: Constraint -> Constraint -> Constraint
x #/\# y = FDAnd x y

--- The resulting constraint is satisfied if both argument constraints
--- are satisfied.
(#\/#)  :: Constraint -> Constraint -> Constraint
x #\/# y = FDOr x y

--- The resulting constraint is satisfied if the first argument constraint
--- do not hold or both argument constraints are satisfied.
(#=>#)  :: Constraint -> Constraint -> Constraint
x #=># y = FDImply x y

--- The resulting constraint is satisfied if both argument constraint
--- are either satisfied and do not hold.
(#<=>#)  :: Constraint -> Constraint -> Constraint
x #<=># y = FDEquiv x y

--- Solves a reified constraint.
solve :: Constraint -> Bool
solve c = prim_solve_reify $!! c

prim_solve_reify :: Constraint -> Bool
prim_solve_reify external

---------------------------------------------------------------------------
-- Complex constraints.

--- Relates the sum of FD variables with some integer of FD variable.
sum :: [Int] -> (Int -> Int -> Bool) -> Int -> Bool
sum vs rel v = seq (normalForm (ensureSpine vs))
                   (seq (ensureNotFree rel) (seq v (prim_sum vs rel v)))

prim_sum :: [Int] -> (Int -> Int -> Bool) -> Int -> Bool
prim_sum external

--- (scalarProduct cs vs relop v) is satisfied if ((cs*vs) relop v) is satisfied.
--- The first argument must be a list of integers. The other arguments are as
--- in <code>sum</code>.
scalarProduct :: [Int] -> [Int] -> (Int -> Int -> Bool) -> Int -> Bool
scalarProduct cs vs rel v =
  seq (groundNormalForm cs)
      (seq (normalForm (ensureSpine vs))
           (seq (ensureNotFree rel) (seq v (prim_scalarProduct cs vs rel v))))

prim_scalarProduct :: [Int] -> [Int] -> (Int -> Int -> Bool) -> Int -> Bool
prim_scalarProduct external


--- (count v vs relop c) is satisfied if (n relop c), where n is the number of
--- elements in the list of FD variables vs that are equal to v, is satisfied.
--- The first argument must be an integer. The other arguments are as
--- in <code>sum</code>.
count :: Int -> [Int] -> (Int -> Int -> Bool) -> Int -> Bool
count v vs rel c =
  seq (ensureNotFree v)
      (seq (normalForm (ensureSpine vs))
           (seq (ensureNotFree rel) (seq c (prim_count v vs rel c))))

prim_count :: Int -> [Int] -> (Int -> Int -> Bool) -> Int -> Bool
prim_count external


--- "All different" constraint on FD variables.
--- @param xs - list of FD variables
--- @return satisfied if the FD variables in the argument list xs
---         have pairwise different values.

allDifferent :: [Int] -> Bool
allDifferent vs = seq (normalForm (ensureSpine vs)) (prim_allDifferent vs)

--- For backward compatibility. Use <code>allDifferent</code>.
all_different :: [Int] -> Bool
all_different = allDifferent

prim_allDifferent :: [Int] -> Bool
prim_allDifferent external

--- Instantiate a single FD variable to its values in the specified domain.
indomain :: Int -> Bool
indomain x = seq x (prim_indomain x)

prim_indomain :: Int -> Bool
prim_indomain external


---------------------------------------------------------------------------
-- Labeling.

--- Instantiate FD variables to their values in the specified domain.
--- @param options - list of option to control the instantiation of FD variables
--- @param xs - list of FD variables that are non-deterministically
---             instantiated to their possible values.

labeling :: [LabelingOption] -> [Int] -> Bool
labeling options vs = seq (normalForm (map ensureNotFree (ensureSpine options)))
                          (seq (normalForm (ensureSpine vs))
                               (prim_labeling options vs))

prim_labeling :: [LabelingOption] -> [Int] -> Bool
prim_labeling external

--- This datatype contains all options to control the instantiated of FD variables
--- with the enumeration constraint <code>labeling</code>.
--- @cons LeftMost - The leftmost variable is selected for instantiation (default)
--- @cons FirstFail - The leftmost variable with the smallest domain is selected
---                   (also known as first-fail principle)
--- @cons FirstFailConstrained - The leftmost variable with the smallest domain
---                              and the most constraints on it is selected.
--- @cons Min - The leftmost variable with the smalled lower bound is selected.
--- @cons Max - The leftmost variable with the greatest upper bound is selected.
--- @cons Step - Make a binary choice between <code>x=#b</code> and
---              <code>x/=#b</code> for the selected variable
---              <code>x</code> where <code>b</code> is the lower or
---              upper bound of <code>x</code> (default).
--- @cons Enum - Make a multiple choice for the selected variable for all the values
---              in its domain.
--- @cons Bisect - Make a binary choice between <code>x&lt;=#m</code> and
---                <code>x&gt;#m</code> for the selected variable
---                <code>x</code> where <code>m</code> is the midpoint
---                of the domain <code>x</code>
---                (also known as domain splitting).
--- @cons Up - The domain is explored for instantiation in ascending order (default).
--- @cons Down - The domain is explored for instantiation in descending order.
--- @cons All - Enumerate all solutions by backtracking (default).
--- @cons Minimize v - Find a solution that minimizes the domain variable v
---                    (using a branch-and-bound algorithm).
--- @cons Maximize v - Find a solution that maximizes the domain variable v
---                    (using a branch-and-bound algorithm).
--- @cons Assumptions x - The variable x is unified with the number of choices
---                       made by the selected enumeration strategy when a solution
---                       is found.
--- @cons RandomVariable x - Select a random variable for instantiation
---                          where `x` is a seed value for the random numbers
---                          (only supported by SWI-Prolog).
--- @cons RandomValue x - Label variables with random integer values
---                       where `x` is a seed value for the random numbers
---                       (only supported by SWI-Prolog).

data LabelingOption = LeftMost
                    | FirstFail
                    | FirstFailConstrained
                    | Min
                    | Max
                    | Step
                    | Enum
                    | Bisect
                    | Up
                    | Down
                    | All
                    | Minimize Int
                    | Maximize Int
                    | Assumptions Int
                    | RandomVariable Int
                    | RandomValue Int


-- end of library CLPFD