-
Notifications
You must be signed in to change notification settings - Fork 1
/
combining.ml
356 lines (271 loc) · 14 KB
/
combining.ml
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
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
(* ========================================================================= *)
(* Nelson-Oppen combined decision procedure. *)
(* *)
(* Copyright (c) 2003-2007, John Harrison. (See "LICENSE.txt" for details.) *)
(* ========================================================================= *)
(* ------------------------------------------------------------------------- *)
(* Real language with decision procedure. *)
(* ------------------------------------------------------------------------- *)
let real_lang =
let fn = ["-",1; "+",2; "-",2; "*",2; "^",2]
and pr = ["<=",2; "<",2; ">=",2; ">",2] in
(fun (s,n) -> n = 0 & is_numeral(Fn(s,[])) or mem (s,n) fn),
(fun sn -> mem sn pr),
(fun fm -> real_qelim(generalize fm) = True);;
(* ------------------------------------------------------------------------- *)
(* Integer language with decision procedure. *)
(* ------------------------------------------------------------------------- *)
let int_lang =
let fn = ["-",1; "+",2; "-",2; "*",2]
and pr = ["<=",2; "<",2; ">=",2; ">",2] in
(fun (s,n) -> n = 0 & is_numeral(Fn(s,[])) or mem (s,n) fn),
(fun sn -> mem sn pr),
(fun fm -> integer_qelim(generalize fm) = True);;
(* ------------------------------------------------------------------------- *)
(* Add any uninterpreted functions to a list of languages. *)
(* ------------------------------------------------------------------------- *)
let add_default langs =
langs @ [(fun sn -> not (exists (fun (f,p,d) -> f sn) langs)),
(fun sn -> sn = ("=",2)),ccvalid];;
(* ------------------------------------------------------------------------- *)
(* Choose a language for homogenization of an atom. *)
(* ------------------------------------------------------------------------- *)
let chooselang langs fm =
match fm with
Atom(R("=",[Fn(f,args);_])) | Atom(R("=",[_;Fn(f,args)])) ->
find (fun (fn,pr,dp) -> fn(f,length args)) langs
| Atom(R(p,args)) ->
find (fun (fn,pr,dp) -> pr(p,length args)) langs;;
(* ------------------------------------------------------------------------- *)
(* General listification for CPS-style function. *)
(* ------------------------------------------------------------------------- *)
let rec listify f l cont =
match l with
[] -> cont []
| h::t -> f h (fun h' -> listify f t (fun t' -> cont(h'::t')));;
(* ------------------------------------------------------------------------- *)
(* Homogenize a term. *)
(* ------------------------------------------------------------------------- *)
let rec homot (fn,pr,dp) tm cont n defs =
match tm with
Var x -> cont tm n defs
| Fn(f,args) ->
if fn(f,length args) then
listify (homot (fn,pr,dp)) args (fun a -> cont (Fn(f,a))) n defs
else cont (Var("v_"^(string_of_num n))) (n +/ Int 1)
(mk_eq (Var("v_"^(string_of_num n))) tm :: defs);;
(* ------------------------------------------------------------------------- *)
(* Homogenize a literal. *)
(* ------------------------------------------------------------------------- *)
let rec homol langs fm cont n defs =
match fm with
Not(f) -> homol langs f (fun p -> cont(Not(p))) n defs
| Atom(R(p,args)) ->
let lang = chooselang langs fm in
listify (homot lang) args (fun a -> cont (Atom(R(p,a)))) n defs
| _ -> failwith "homol: not a literal";;
(* ------------------------------------------------------------------------- *)
(* Fully homogenize a list of literals. *)
(* ------------------------------------------------------------------------- *)
let rec homo langs fms cont =
listify (homol langs) fms
(fun dun n defs ->
if defs = [] then cont dun n defs
else homo langs defs (fun res -> cont (dun@res)) n []);;
(* ------------------------------------------------------------------------- *)
(* Overall homogenization. *)
(* ------------------------------------------------------------------------- *)
let homogenize langs fms =
let fvs = unions(map fv fms) in
let n = Int 1 +/ itlist (max_varindex "v_") fvs (Int 0) in
homo langs fms (fun res n defs -> res) n [];;
(* ------------------------------------------------------------------------- *)
(* Whether a formula belongs to a language. *)
(* ------------------------------------------------------------------------- *)
let belongs (fn,pr,dp) fm =
forall fn (functions fm) &
forall pr (subtract (predicates fm) ["=",2]);;
(* ------------------------------------------------------------------------- *)
(* Partition formulas among a list of languages. *)
(* ------------------------------------------------------------------------- *)
let rec langpartition langs fms =
match langs with
[] -> if fms = [] then [] else failwith "langpartition"
| l::ls -> let fms1,fms2 = partition (belongs l) fms in
fms1::langpartition ls fms2;;
(* ------------------------------------------------------------------------- *)
(* Running example if we magically knew the interpolant. *)
(* ------------------------------------------------------------------------- *)
START_INTERACTIVE;;
(integer_qelim ** generalize)
<<(u + 1 = v /\ v_1 + 1 = u - 1 /\ v_2 - 1 = v + 1 /\ v_3 = v - 1)
==> u = v_3 /\ ~(v_1 = v_2)>>;;
ccvalid
<<(v_2 = f(v_3) /\ v_1 = f(u)) ==> ~(u = v_3 /\ ~(v_1 = v_2))>>;;
END_INTERACTIVE;;
(* ------------------------------------------------------------------------- *)
(* Turn an arrangement (partition) of variables into corresponding formula. *)
(* ------------------------------------------------------------------------- *)
let rec arreq l =
match l with
v1::v2::rest -> mk_eq (Var v1) (Var v2) :: (arreq (v2::rest))
| _ -> [];;
let arrangement part =
itlist (union ** arreq) part
(map (fun (v,w) -> Not(mk_eq (Var v) (Var w)))
(distinctpairs (map hd part)));;
(* ------------------------------------------------------------------------- *)
(* Attempt to substitute with trivial equations. *)
(* ------------------------------------------------------------------------- *)
let dest_def fm =
match fm with
Atom(R("=",[Var x;t])) when not(mem x (fvt t)) -> x,t
| Atom(R("=",[t; Var x])) when not(mem x (fvt t)) -> x,t
| _ -> failwith "dest_def";;
let rec redeqs eqs =
try let eq = find (can dest_def) eqs in
let x,t = dest_def eq in
redeqs (map (subst (x |=> t)) (subtract eqs [eq]))
with Failure _ -> eqs;;
(* ------------------------------------------------------------------------- *)
(* Naive Nelson-Oppen variant trying all arrangements. *)
(* ------------------------------------------------------------------------- *)
let trydps ldseps fms =
exists (fun ((_,_,dp),fms0) -> dp(Not(list_conj(redeqs(fms0 @ fms)))))
ldseps;;
let allpartitions =
let allinsertions x l acc =
itlist (fun p acc -> ((x::p)::(subtract l [p])) :: acc) l
(([x]::l)::acc) in
fun l -> itlist (fun h y -> itlist (allinsertions h) y []) l [[]];;
let nelop_refute vars ldseps =
forall (trydps ldseps ** arrangement) (allpartitions vars);;
let nelop1 langs fms0 =
let fms = homogenize langs fms0 in
let seps = langpartition langs fms in
let fvlist = map (unions ** map fv) seps in
let vars = filter (fun x -> length (filter (mem x) fvlist) >= 2)
(unions fvlist) in
nelop_refute vars (zip langs seps);;
let nelop langs fm = forall (nelop1 langs) (simpdnf(simplify(Not fm)));;
(* ------------------------------------------------------------------------- *)
(* Check that our example works. *)
(* ------------------------------------------------------------------------- *)
START_INTERACTIVE;;
nelop (add_default [int_lang])
<<f(v - 1) - 1 = v + 1 /\ f(u) + 1 = u - 1 /\ u + 1 = v ==> false>>;;
(* ------------------------------------------------------------------------- *)
(* Bell numbers show the size of our case analysis. *)
(* ------------------------------------------------------------------------- *)
let bell n = length(allpartitions (1--n)) in map bell (1--10);;
END_INTERACTIVE;;
(* ------------------------------------------------------------------------- *)
(* Find the smallest subset satisfying a predicate. *)
(* ------------------------------------------------------------------------- *)
let rec findasubset p m l =
if m = 0 then p [] else
match l with
[] -> failwith "findasubset"
| h::t -> try findasubset (fun s -> p(h::s)) (m - 1) t
with Failure _ -> findasubset p m t;;
let findsubset p l =
tryfind (fun n ->
findasubset (fun x -> if p x then x else failwith "") n l)
(0--length l);;
(* ------------------------------------------------------------------------- *)
(* The "true" Nelson-Oppen method. *)
(* ------------------------------------------------------------------------- *)
let rec nelop_refute eqs ldseps =
try let dj = findsubset (trydps ldseps ** map negate) eqs in
forall (fun eq ->
nelop_refute (subtract eqs [eq])
(map (fun (dps,es) -> (dps,eq::es)) ldseps)) dj
with Failure _ -> false;;
let nelop1 langs fms0 =
let fms = homogenize langs fms0 in
let seps = langpartition langs fms in
let fvlist = map (unions ** map fv) seps in
let vars = filter (fun x -> length (filter (mem x) fvlist) >= 2)
(unions fvlist) in
let eqs = map (fun (a,b) -> mk_eq (Var a) (Var b))
(distinctpairs vars) in
nelop_refute eqs (zip langs seps);;
let nelop langs fm = forall (nelop1 langs) (simpdnf(simplify(Not fm)));;
(* ------------------------------------------------------------------------- *)
(* Some additional examples (from ICS paper and Shostak's "A practical..." *)
(* ------------------------------------------------------------------------- *)
START_INTERACTIVE;;
nelop (add_default [int_lang])
<<y <= x /\ y >= x + z /\ z >= 0 ==> f(f(x) - f(y)) = f(z)>>;;
nelop (add_default [int_lang])
<<x = y /\ y >= z /\ z >= x ==> f(z) = f(x)>>;;
nelop (add_default [int_lang])
<<a <= b /\ b <= f(a) /\ f(a) <= 1
==> a + b <= 1 \/ b + f(b) <= 1 \/ f(f(b)) <= f(a)>>;;
(* ------------------------------------------------------------------------- *)
(* Confirmation of non-convexity. *)
(* ------------------------------------------------------------------------- *)
map (real_qelim ** generalize)
[<<x * y = 0 /\ z = 0 ==> x = z \/ y = z>>;
<<x * y = 0 /\ z = 0 ==> x = z>>;
<<x * y = 0 /\ z = 0 ==> y = z>>];;
map (integer_qelim ** generalize)
[<<0 <= x /\ x < 2 /\ y = 0 /\ z = 1 ==> x = y \/ x = z>>;
<<0 <= x /\ x < 2 /\ y = 0 /\ z = 1 ==> x = y>>;
<<0 <= x /\ x < 2 /\ y = 0 /\ z = 1 ==> x = z>>];;
(* ------------------------------------------------------------------------- *)
(* Failures of original Shostak procedure. *)
(* ------------------------------------------------------------------------- *)
nelop (add_default [int_lang])
<<f(v - 1) - 1 = v + 1 /\ f(u) + 1 = u - 1 /\ u + 1 = v ==> false>>;;
(*** And this one is where the original procedure loops ***)
nelop (add_default [int_lang])
<<f(v) = v /\ f(u) = u - 1 /\ u = v ==> false>>;;
(* ------------------------------------------------------------------------- *)
(* Additional examples not in the text. *)
(* ------------------------------------------------------------------------- *)
(*** This is on p. 8 of Shostak's "Deciding combinations" paper ***)
time (nelop (add_default [int_lang]))
<<z = f(x - y) /\ x = z + y /\ ~(-(y) = -(x - f(f(z)))) ==> false>>;;
(*** This (ICS theories-1) fails without array operations ***)
time (nelop (add_default [int_lang]))
<<a + 2 = b ==> f(read(update(A,a,3),b-2)) = f(b - a + 1)>>;;
(*** can-001 from ICS examples site, with if-then-elses expanded manually ***)
time (nelop (add_default [int_lang]))
<<(x = y /\ z = 1 ==> f(f((x+z))) = f(f((1+y))))>>;;
(*** RJB example; lists plus uninterpreted functions ***)
time (nelop (add_default [int_lang]))
<<hd(x) = hd(y) /\ tl(x) = tl(y) /\ ~(x = nil) /\ ~(y = nil)
==> f(x) = f(y)>>;;
(*** Another one from the ICS paper ***)
time (nelop (add_default [int_lang]))
<<~(f(f(x) - f(y)) = f(z)) /\ y <= x /\ y >= x + z /\ z >= 0 ==> false>>;;
(*** Shostak's "A Practical Decision Procedure..." paper
*** No longer works since I didn't do predicates in congruence closure
time (nelop (add_default [int_lang]))
<<x < f(y) + 1 /\ f(y) <= x ==> (P(x,y) <=> P(f(y),y))>>;;
***)
(*** Shostak's "Practical..." paper again, using extra clauses for MAX ***)
time (nelop (add_default [int_lang]))
<<(x >= y ==> MAX(x,y) = x) /\ (y >= x ==> MAX(x,y) = y)
==> x = y + 2 ==> MAX(x,y) = x>>;;
(*** Shostak's "Practical..." paper again ***)
time (nelop (add_default [int_lang]))
<<x <= g(x) /\ x >= g(x) ==> x = g(g(g(g(x))))>>;;
(*** Easy example I invented ***)
time (nelop (add_default [real_lang]))
<<x^2 = 1 ==> (f(x) = f(-(x))) ==> (f(x) = f(1))>>;;
(*** Taken from Clark Barrett's CVC page ***)
time (nelop (add_default [int_lang]))
<<2 * f(x + y) = 3 * y /\ 2 * x = y ==> f(f(x + y)) = 3 * x>>;;
(*** My former running example in the text; seems too slow.
*** Anyway this also needs extra predicates in CC
time (nelop (add_default [real_lang]))
<<x^2 = y^2 /\ x < y /\ z^2 = z /\ x < x * z /\ P(f(1 + z))
==> P(f(x + y) - f(0))>>;;
***)
(*** An example where the "naive" procedure is slow but feasible ***)
nelop (add_default [int_lang])
<<4 * x = 2 * x + 2 * y /\ x = f(2 * x - y) /\
f(2 * y - x) = 3 /\ f(x) = 4 ==> false>>;;
END_INTERACTIVE;;