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
module Engine =
struct
type env = (Cp__DomI.t, Cp__DomB.t) Cp__Type.env
type interp = (Z.t, bool) Cp__Type.interp
type model = (Z.t, bool) Cp__Type.model
module Prob =
struct type t = Constraints__simple__Simple.t list
end
module Watcher =
struct
type t = {
wb: (Constraints__simple__Simple.t list) Cp__Impl0.Hb.Make.t;
wi: (Constraints__simple__Simple.t list) Cp__Impl0.Hi.Make.t;
}
let rec init (wb:
(Constraints__simple__Simple.t list) Cp__Impl0.Hb.Make.t)
(wi:
(Constraints__simple__Simple.t list) Cp__Impl0.Hi.Make.t)
(prob: Constraints__simple__Simple.t list) : unit =
match prob with
| [] -> ()
| c :: l ->
init wb wi l;
let si = (Cp__Impl0.Si.create ()) in
Constraints__simple__Simple.compute_vars_ti c si;
let iteri = (Cp__Impl0.Si.Iterator.create si) in
while not (Cp__Impl0.Si.Iterator.is_empty iteri) do
let vi = (Cp__Impl0.Si.Iterator.next iteri) in
(Cp__Impl0.Hi.Make.set wi vi (c :: (Cp__Impl0.Hi.Make.find wi vi)))
done;
let sb = (Cp__Impl0.Sb.create ()) in
Constraints__simple__Simple.compute_vars_tb c sb;
let iterb = (Cp__Impl0.Sb.Iterator.create sb) in
while not (Cp__Impl0.Sb.Iterator.is_empty iterb) do
let vb = (Cp__Impl0.Sb.Iterator.next iterb) in
(Cp__Impl0.Hb.Make.set wb vb (c :: (Cp__Impl0.Hb.Make.find wb vb)))
done
let create :
type xi8 xi9. ((xi8, xi9) Cp__Type.env) ->
(Constraints__simple__Simple.t list) -> t =
fun e prob -> let wi =
(Cp__Impl0.Hi.Make.create (Cp__Impl0.Hbi.Make.max_tags
(e.Cp__Type.domi)) ([] )) in
let wb =
(Cp__Impl0.Hb.Make.create (Cp__Impl0.Hbb.Make.max_tags
(e.Cp__Type.domb)) ([] )) in
init wb wi prob; { wb = wb; wi = wi }
end
let rec propagate_all' (e: (Cp__DomI.t, Cp__DomB.t) Cp__Type.env)
(p: Constraints__simple__Simple.t list) : unit =
match p with
| [] -> ()
| c :: q -> Constraints__simple__Simple.propagate e c; propagate_all' e q
let rec propagate_all (e: (Cp__DomI.t, Cp__DomB.t) Cp__Type.env)
(p: Constraints__simple__Simple.t list) : unit =
e.Cp__Type.dirty <- false;
propagate_all' e p;
if e.Cp__Type.dirty then propagate_all e p
let rec check_model_all (mo: (Z.t, bool) Cp__Type.model)
(p: Constraints__simple__Simple.t list) : bool =
match p with
| [] -> true
| c :: q ->
Constraints__simple__Simple.check_model mo c && check_model_all mo q
let compute_model (e: (Cp__DomI.t, Cp__DomB.t) Cp__Type.env)
(varb: Cp__Var0.tb list) (vari: Cp__Var0.ti list) :
(Z.t, bool) Cp__Type.model =
let modb =
(Cp__Impl0.Hb.Make.create (Cp__Impl0.Hbb.Make.max_tags (e.Cp__Type.domb))
(Cp__DomB.default_value ())) in
let rec auxb (varb1: Cp__Var0.tb list) : unit =
match varb1 with
| [] -> ()
| v :: varb2 ->
auxb varb2;
let o =
Cp__DomB.get_singleton (Cp__Impl0.Hbb.Make.find (e.Cp__Type.domb) v) in
(Cp__Impl0.Hb.Make.set modb v o) in
auxb varb;
let modi =
(Cp__Impl0.Hi.Make.create (Cp__Impl0.Hbi.Make.max_tags (e.Cp__Type.domi))
(Cp__DomI.default_value ())) in
let rec auxi (vari1: Cp__Var0.ti list) : unit =
match vari1 with
| [] -> ()
| v :: vari2 ->
auxi vari2;
let o =
Cp__DomI.get_singleton (Cp__Impl0.Hbi.Make.find (e.Cp__Type.domi) v) in
(Cp__Impl0.Hi.Make.set modi v o) in
auxi vari;
{ Cp__Type.modi = (Cp__Impl0.Hi.Make.copy_lock modi); Cp__Type.modb =
(Cp__Impl0.Hb.Make.copy_lock modb) }
let set_singleton_bool (e: (Cp__DomI.t, Cp__DomB.t) Cp__Type.env)
(v: Cp__Var0.tb) (vb: bool) : unit =
(Cp__Impl0.Hbb.Make.set (e.Cp__Type.domb) v (Cp__DomB.mk_singleton vb))
let set_singleton_int (e: (Cp__DomI.t, Cp__DomB.t) Cp__Type.env)
(v: Cp__Var0.ti) (vi: Z.t) : unit =
(Cp__Impl0.Hbi.Make.set (e.Cp__Type.domi) v (Cp__DomI.mk_singleton vi))
let rec search (e: (Cp__DomI.t, Cp__DomB.t) Cp__Type.env)
(p: Constraints__simple__Simple.t list)
(varb: Cp__Var0.tb list) (vari: Cp__Var0.ti list)
(todob: Cp__Var0.tb list) (todoi: Cp__Var0.ti list) :
(Z.t, bool) Cp__Type.model =
match todob with
| b :: todob1 ->
begin match Cp__DomB.is_singleton (Cp__Type.get_bool e b) with
| Cp__Type.Is_singleton -> search e p varb vari todob1 todoi
| Cp__Type.Iter l ->
(let tokeni =
(Cp__Impl0.Hbi.Make.create_backtrack_point (e.Cp__Type.domi)) in
let tokenb =
(Cp__Impl0.Hbb.Make.create_backtrack_point (e.Cp__Type.domb)) in
let rec iterb (l1: (bool) list) : (Z.t, bool) Cp__Type.model =
match l1 with
| [] -> raise Cp__Type.Unsat
| v :: l2 ->
begin
try
set_singleton_bool e b v;
propagate_all e p;
search e p varb vari todob1 todoi
with
| Cp__Type.Unsat ->
(Cp__Impl0.Hbi.Make.backtrack (e.Cp__Type.domi) tokeni);
(Cp__Impl0.Hbb.Make.backtrack (e.Cp__Type.domb) tokenb);
iterb l2
end in
iterb l)
end
| [] ->
begin match todoi with
| i :: todoi1 ->
begin match Cp__DomI.is_singleton (Cp__Type.get_int e i) with
| Cp__Type.Is_singleton -> search e p varb vari todob todoi1
| Cp__Type.Iter l ->
(let tokeni =
(Cp__Impl0.Hbi.Make.create_backtrack_point (e.Cp__Type.domi)) in
let tokenb =
(Cp__Impl0.Hbb.Make.create_backtrack_point (e.Cp__Type.domb)) in
let rec iteri (l1: (Z.t) list) : (Z.t, bool) Cp__Type.model =
match l1 with
| [] -> raise Cp__Type.Unsat
| v :: l2 ->
begin
try
set_singleton_int e i v;
propagate_all e p;
search e p varb vari todob todoi1
with
| Cp__Type.Unsat ->
(Cp__Impl0.Hbi.Make.backtrack (e.Cp__Type.domi) tokeni);
(Cp__Impl0.Hbb.Make.backtrack (e.Cp__Type.domb) tokenb);
iteri l2
end in
iteri l)
end
| [] ->
(let model = compute_model e varb vari in
if not (check_model_all model p) then raise Cp__Type.Unsat; model)
end
let compute_vars_ti (p: Constraints__simple__Simple.t list)
(si: Cp__Impl0.Si.t) : unit =
let rec compute_vars (p1: Constraints__simple__Simple.t list)
(si1: Cp__Impl0.Si.t) : unit =
match p1 with
| [] -> ()
| a :: p2 ->
Constraints__simple__Simple.compute_vars_ti a si1;
compute_vars p2 si1 in
compute_vars p si
let compute_vars_tb (p: Constraints__simple__Simple.t list)
(sb: Cp__Impl0.Sb.t) : unit =
let rec compute_vars1 (p1: Constraints__simple__Simple.t list)
(sb1: Cp__Impl0.Sb.t) : unit =
match p1 with
| [] -> ()
| a :: p2 ->
Constraints__simple__Simple.compute_vars_tb a sb1;
compute_vars1 p2 sb1 in
compute_vars1 p sb
let start (p: Constraints__simple__Simple.t list) (topb: Cp__DomB.t)
(topi: Cp__DomI.t) : (Z.t, bool) Cp__Type.model =
let si = (Cp__Impl0.Si.create ()) in
compute_vars_ti p si;
let vari = ref ([] ) in
let iteri1 = (Cp__Impl0.Si.Iterator.create si) in
while not (Cp__Impl0.Si.Iterator.is_empty iteri1) do
let o = let o1 = (Cp__Impl0.Si.Iterator.next iteri1) in o1 :: !vari in
vari := o
done;
let domi = (Cp__Impl0.Hbi.Make.create (Cp__Impl0.Si.max_tags si) topi) in
let sb = (Cp__Impl0.Sb.create ()) in
compute_vars_tb p sb;
let varb = ref ([] ) in
let iterb1 = (Cp__Impl0.Sb.Iterator.create sb) in
while not (Cp__Impl0.Sb.Iterator.is_empty iterb1) do
let o = let o1 = (Cp__Impl0.Sb.Iterator.next iterb1) in o1 :: !varb in
varb := o
done;
let domb = (Cp__Impl0.Hbb.Make.create (Cp__Impl0.Sb.max_tags sb) topb) in
let e =
{ Cp__Type.domi = domi; Cp__Type.domb = domb; Cp__Type.dirty = false;
Cp__Type.mi = [] ; Cp__Type.mb = [] } in
search e p !varb !vari !varb !vari
end
let start' (p: Constraints__simple__Simple.t list) (minint: Z.t)
(maxint: Z.t) : (Z.t, bool) Cp__Type.model =
let topbool = Cp__DomB.Top in
let topint = { Cp__DomI.min = minint; Cp__DomI.max = maxint } in
Engine.start p topbool topint