1
2 /*++
3 Copyright (c) 2015 Microsoft Corporation
4
5 --*/
6
7 #include "ast/ast.h"
8 #include "smt/params/smt_params.h"
9 #include "qe/qe.h"
10 #include "ast/ast_pp.h"
11 #include "util/lbool.h"
12 #include <sstream>
13 #include "ast/reg_decl_plugins.h"
14
15
16 #if 0
17 static void test_qe(ast_manager& m, lbool expected_outcome, expr* fml, char const* option) {
18
19 // enable_trace("bit2int");
20 //enable_trace("gomory_cut");
21 enable_trace("final_check_arith");
22 enable_trace("arith_final_check");
23 //enable_trace("arith_branching");
24 enable_trace("theory_arith_int");
25 enable_trace("presburger");
26 enable_trace("quant_elim");
27 // enable_trace("arith_simplifier_plugin");
28 // enable_trace("non_linear");
29 // enable_trace("gomory_cut_detail");
30 // enable_trace("arith");
31 // enable_trace("bv");
32 // enable_trace("after_search");
33 // enable_trace("bv_bit_prop");
34
35 smt_params params;
36 // params.m_quant_elim = true;
37
38 std::cout << mk_pp(fml, m) << "\n";
39 qe::expr_quant_elim qe(m, params);
40 expr_ref result(m);
41 qe(m.mk_true(), fml, result);
42 std::cout << " -> " << mk_pp(result, m) << " " << expected_outcome << "\n";
43 if (expected_outcome == l_true && !m.is_true(result)) {
44 std::cout << "ERROR: expected true, instead got " << mk_pp(result, m) << "\n";
45 //exit(-1);
46 }
47 if (expected_outcome == l_false && !m.is_false(result)) {
48 std::cout << "ERROR: expected false, instead got " << mk_pp(result, m) << "\n";
49 //exit(-1);
50 }
51 }
52 #endif
53
test_formula(lbool expected_outcome,char const * fml)54 static void test_formula(lbool expected_outcome, char const* fml) {
55 ast_manager m;
56 reg_decl_plugins(m);
57 // No-op requires SMTLIB2
58
59 #if 0
60 scoped_ptr<smtlib::parser> parser = smtlib::parser::create(m);
61 parser->initialize_smtlib();
62
63 std::ostringstream buffer;
64 buffer << "(benchmark presburger :status unknown :logic AUFLIA :extrapreds ((p1) (p2) (p3)) "
65 << ":extrafuns ((a Int) (b Int))\n"
66 << ":extrapreds ((p) (q) (r))\n"
67 << ":datatypes ((list (nil) (cons (hd Int) (tl list))))\n"
68 << ":datatypes ((cell (cnil) (ccons (car cell) (cdr cell))))\n"
69 << ":extrasorts (U)\n"
70 << ":extrafuns ((f U U))\n"
71 << ":formula " << fml << ")";
72 parser->parse_string(buffer.str().c_str());
73 smtlib::benchmark* b = parser->get_benchmark();
74 smtlib::theory::expr_iterator it = b->begin_formulas();
75 smtlib::theory::expr_iterator end = b->end_formulas();
76 for (; it != end; ++it) {
77 test_qe(m, expected_outcome, *it, 0);
78 }
79 #endif
80 }
81
82
tst_quant_elim()83 void tst_quant_elim() {
84 disable_debug("heap");
85
86 test_formula(l_undef, "(exists ((p1 Bool) (q1 Bool) (r1 Bool))\
87 (and (or (not p1) (not q1) r1)\
88 (or (and (not p) (not q) (not p1) q1)\
89 (and (not p) q p1 (not q1))\
90 (and p (not q) p1 q1)\
91 (and p q p1 q1))\
92 (or (and (not r) (not r1))\
93 (and (= p p1) (= q q1) r r1)\
94 (and (not (and (= p p1) (= q q1))) (not (= r r1))))))");
95
96
97 test_formula(l_false,"(forall (x Int) (y Int) (or (= x 0) (< (* 5 y) (* 6 x)) (> (* 5 y) (* 6 x))))");
98
99 test_formula(l_false, "(forall (a Int) (b Int) (exists (x Int) (and (< a (* 20 x)) (< (* 20 x) b))))");
100
101 test_formula(l_undef, "(exists (u U) (= (f u) u))");
102
103 test_formula(l_true,
104 "(exists (l Int) (forall (x Int) (implies (>= x l) "
105 " (exists (u Int) (v Int) (and (>= u 0) (>= v 0) (= x (+ (* 3 u) (* 7 v))))))))");
106
107
108 test_formula(l_true, "(forall (x Int) (y Int) (implies (= (* 6 x) (* 5 y)) (exists (d Int) (= y (* 3 d)))))");
109
110 test_formula(l_undef, "(exists (x Int) (= (- a (mod x 4)) 0))");
111 // return;
112
113
114 // test_formula(l_true, "(exists (x Int) (y Int) (= 1 (+ (* 5 x) (* 3 y))))");
115
116
117 test_formula(l_undef, "(exists (a Bool) (b Bool) (or (and p1 a) (and p2 (not b))))");
118
119
120
121
122 test_formula(l_false,
123 "(forall (x Int) (q1 Int) (q2 Int) (r1 Int) (r2 Int) "
124 " (implies "
125 " (and (< x 4699) "
126 " (= (* 2622 x) (+ (* 65536 q1) r1)) "
127 " (<= 0 q1) "
128 " (<= 0 r1) "
129 " (< r1 65536) "
130 " (= x (+ (* 100 q2) r2)) "
131 " (<= 0 q2) "
132 " (<= 0 r2) "
133 " (< r2 100)) "
134 " (= q1 q2)))");
135
136
137
138 test_formula(l_undef,
139 "(forall (l list) (or (= l nil) (exists (x Int) (ll list) (= l (cons x ll)))))");
140
141
142
143
144
145
146 test_formula(l_false, "(exists (x Real) (forall (y Real) (>= x y)))");
147 test_formula(l_false, "(exists (x Real) (forall (y Real) (> x y)))");
148 test_formula(l_false, "(exists (x Real) (forall (y Real) (< x y)))");
149 test_formula(l_false, "(exists (x Real) (forall (y Real) (<= x y)))");
150
151 test_formula(l_true, "(exists (x Real) (exists (y Real) (< x y)))");
152 test_formula(l_true, "(exists (x Real) (exists (y Real) (<= x y)))");
153 test_formula(l_true, "(exists (x Real) (exists (y Real) (>= x y)))");
154 test_formula(l_true, "(exists (x Real) (exists (y Real) (> x y)))");
155
156 test_formula(l_true, "(forall (x Real) (exists (y Real) (< x y)))");
157 test_formula(l_true, "(forall (x Real) (exists (y Real) (<= x y)))");
158 test_formula(l_true, "(forall (x Real) (exists (y Real) (>= x y)))");
159 test_formula(l_true, "(forall (x Real) (exists (y Real) (> x y)))");
160
161 test_formula(l_false, "(forall (x Real) (forall (y Real) (< x y)))");
162 test_formula(l_false, "(forall (x Real) (forall (y Real) (<= x y)))");
163 test_formula(l_false, "(forall (x Real) (forall (y Real) (>= x y)))");
164 test_formula(l_false, "(forall (x Real) (forall (y Real) (> x y)))");
165
166
167
168
169
170 test_formula(l_true,
171 "(exists (l Int) (forall (x Int) (implies (>= x l) "
172 " (exists (u Int) (v Int) (and (>= u 0) (>= v 0) (= x (+ (* 3 u) (* 5 v))))))))");
173
174
175 test_formula(l_false, "(forall (d Int) (implies (>= d 0) (exists (x Int) (y Int) (and (>= x 0) (>= y 0) (= d (+ (* 3 x) (* 5 y)))))))");
176
177 test_formula(l_true, "(forall (y Int) (implies (exists (d Int) (= y (* 6 d))) (exists (d Int) (= y (* 2 d)))))");
178
179 test_formula(l_true, "(forall (y Int) (implies (exists (d Int) (= y (* 65 d))) (exists (d Int) (= y (* 5 d)))))");
180
181
182 test_formula(l_true,
183 "(exists (z Int) (forall (w Int) (exists (x Int) (y Int) "
184 " (or (and (< (+ (* 3 x) w) 2) (< 1 (- (+ (* 2 x) z) w))) "
185 " (and (< z (* 2 y)) (> z y))))))");
186
187
188 test_formula(l_true, "(exists (x Int) (y Int) (and (> x 0) (>= y 0) (= 1 (- (* 3 x) (* 5 y)))))");
189
190
191 test_formula(l_true,
192 "(exists (a Int) (b Int) "
193 " (and (not (= a 1)) (= a b) (or (= a (* 2 b)) (= (* 2 b) (+ 1 (* 3 a))))))");
194
195
196
197 test_formula(l_true,
198 "(forall (x Int) (iff (and (not (= 0 (mod x 2))) (= 0 (mod (- x 1) 3))) "
199 " (or (= 0 (mod (- x 1) 12)) (= 0 (mod (- x 7) 12)))))");
200
201
202
203
204
205
206 test_formula(l_false, "(exists (x Int) (and (< (* 3 x) 2) (< 1 (* 2 x))))");
207
208
209 test_formula(l_true, "(forall (x Int) (y Int) (or (= 0 (mod x 5)) (not (= (* 6 x) (* 5 y)))))");
210
211
212 test_formula(l_false, "(forall (x Int) (exists (y Int) (= x (* 2 y))))");
213 test_formula(l_false,
214 "(forall (x Int) "
215 " (implies (not (= 0 (mod x 2))) "
216 " (or (= 0 (mod (- x 1) 4)) "
217 " (= 0 (mod (- x 1) 8)) "
218 " (= 0 (mod (- x 3) 8)) "
219 " (= 0 (mod (- x 1) 6)) "
220 " (= 0 (mod (- x 1) 14)) "
221 " (= 0 (mod (- x 9) 14)) "
222 " (= 0 (mod (- x 11) 14)) "
223 " (= 0 (mod (- x 5) 24)) "
224 " (= 0 (mod (- x 11) 24))))) ");
225
226 test_formula(l_true,
227 "(forall (x Int) (iff (and (not (= 0 (mod x 2))) (= 0 (mod (- x 1) 3))) "
228 " (or (= 0 (mod (- x 1) 12)) (= 0 (mod (- x 7) 12)))))");
229
230
231
232
233 test_formula(l_false,
234 "(forall (d Int) (c Int) (b Int) "
235 " (and (= c 0) (= d (* b c)) (= d 0)))");
236
237
238
239
240 //return;
241
242 test_formula(l_undef, "(exists (k!12 Int) (k!11 Int) (and (= (ite (= k!11 0) 0 k!11) k!11) (not (= (ite (= k!12 (+ 1)) 1 0) 0))))");
243 //return;
244
245
246
247
248
249 test_formula(l_false,
250 "(forall (a Int) (b Int) (x Int) (y Int) (z Int) "
251 " (implies (and (= (+ a 2) b) (= x (+ 1 (- b a))) (= y (- b 2)) (= z 3)) false))");
252
253
254
255 test_formula(l_false,
256 "(exists (a Int) (b Int) "
257 " (and (> a 1) (> b 1) (= a b) (or (= a (* 2 b)) (= (* 2 b) (+ 1 (* 3 a))))))");
258
259
260
261 test_formula(l_true, "(forall (d Int) (implies true (exists (x Int) (y Int) (and true true (= d (+ (* 3 x) (* 5 y)))))))");
262
263 // This one takes forever without bit-vectors
264 test_formula(l_true, "(forall (d Int) (implies (>= d 8) (exists (x Int) (y Int) (and (>= x 0) (>= y 0) (= d (+ (* 3 x) (* 5 y)))))))");
265
266 test_formula(l_true, "(forall (d Int) (implies (>= d 0) (exists (x Int) (y Int) (and (>= x 0) (>= y 0) (= d (- (* 3 x) (* 5 y)))))))");
267
268
269 test_formula(l_false, "(exists (x Int) (y Int) (z Int) (= 1 (- (* 4 x) (* 6 y))))");
270
271 //return;
272
273
274
275 test_formula(l_true,
276 "(exists (l Int) (forall (x Int) (implies (>= x l) "
277 " (exists (u Int) (v Int) (and (>= u 0) (>= v 0) (= x (+ (* 3 u) (* 8 v))))))))");
278
279 test_formula(l_true,
280 "(exists (l Int) (forall (x Int) (implies (>= x l) "
281 " (exists (u Int) (v Int) (and (>= u 0) (>= v 0) (= x (+ (* 3 u) (* 8 v))))))))");
282
283 #if 0
284
285 // too slow.
286
287 test_formula(l_true,
288 "(exists (l Int) (forall (x Int) (implies (>= x l) "
289 " (exists (u Int) (v Int) (and (>= u 0) (>= v 0) (= x (+ (* 7 u) (* 8 v))))))))");
290
291
292 #endif
293
294 test_formula(l_true, "(forall (x Int) (exists (y Int) (and (<= (* 2 y) x) (< x (* 2 (+ y 1))))))");
295
296
297 test_formula(l_false, "(exists (x Int) (y Int) (and (> y 0) (> y (* 2 x)) (< y (+ x 2)) (= 0 (mod y 2))))");
298
299 test_formula(l_false, "(exists (x Int) (and (< (* 3 x) 3) (< 1 (* 2 x))))");
300
301
302 test_formula(l_true, "(exists (x Int) (and (< (* 3 x) 4) (< 1 (* 2 x))))");
303
304 test_formula(l_false, "(exists (x Int) (and (< (+ (* 3 x) 1) 10) (> (- (* 7 x) 6) 7) (= 0 (mod x 3))))");
305
306
307 test_formula(l_false, "(exists (x Int) (y Int) (and (< (- 1 (* 5 y)) x) (< (+ 1 y) (* 13 x)) (< (+ x 2) 0) (> y 0)))");
308
309 test_formula(l_false, "(exists (x Int) (y Int) (and (< (- 1 (* 5 y)) x) (< (+ 1 y) (* 13 x)) (< x -2)))");
310
311 test_formula(l_true, "(exists (w Int) (z Int) (y Int) (x Int) (and (< (- 1 (* 5 y)) (+ x (* 2 z))) (< (+ 1 y w (* -4 z)) (* 13 x)) (< x -2) (> z 0)))");
312
313
314
315 test_formula(l_true,
316 "(forall (w Int) "
317 " (exists (z Int) (y Int) (x Int) "
318 " (and (< (- 1 (* 5 y)) (+ x (* 2 z))) "
319 " (< (- (+ 1 y) (* 4 z)) (* 13 x)) "
320 " (< x -2) (> z 0) (< x 10)))) ");
321
322
323 test_formula(l_false,
324 "(forall (d Int) (c Int) (b Int) "
325 " (and (= c 0) (= d (* b c)) (= d 4)))");
326
327 test_formula(l_undef,
328 "(exists (d Int) (c Int) (b Int) "
329 " (and (= c 0) (= d (* b c)) (= d 0)))");
330
331 test_formula(l_undef,
332 "(exists (d Int) (c Int) (b Int) "
333 " (and (= c 0) (= d (* b c)) (= d 4)))");
334
335
336
337 // Tests from Harrison's HOL-light version of Cooper.
338
339 test_formula(l_true, "(forall (x Int) (y Int) (not (= (+ 1 (* 2 x)) (* 2 y))))");
340
341
342 test_formula(l_false, "(exists (x Int) (y Int) (= 1 (- (* 4 x) (* 6 y))))");
343
344
345
346 // "(forall (x Int) (implies (< b x) (<= a x)))"
347 // "(forall (x Int) (implies (< b x) (< a x)))"
348
349
350 test_formula(l_false, "(forall (d Int) (implies (>= d 0) (exists (x Int) (y Int) (and (>= x 0) (>= y 0) (= d (+ (* 3 x) (* 5 y)))))))");
351
352 test_formula(l_true, "(forall (d Int) (implies true (exists (x Int) (y Int) (and true true (= d (+ (* 3 x) (* 5 y)))))))");
353
354 // This one takes forever without bit-vectors
355 test_formula(l_true, "(forall (d Int) (implies (>= d 8) (exists (x Int) (y Int) (and (>= x 0) (>= y 0) (= d (+ (* 3 x) (* 5 y)))))))");
356
357 test_formula(l_true, "(forall (d Int) (implies (>= d 0) (exists (x Int) (y Int) (and (>= x 0) (>= y 0) (= d (- (* 3 x) (* 5 y)))))))");
358
359 test_formula(l_true, "(exists (x Int) (y Int) (and (> x 0) (>= y 0) (= 1 (- (* 3 x) (* 5 y)))))");
360
361 test_formula(l_false, "(exists (x Int) (y Int) (z Int) (= 1 (- (* 4 x) (* 6 y))))");
362
363 // "(forall (x Int) (implies (< b (* 3 x)) (a < (* 3 x))))"
364
365 test_formula(l_false, "(forall (x Int) (y Int) (implies (<= x y) (< (+ 1 (* 2 x)) (* 2 y))))");
366
367
368 test_formula(l_true, "(forall (x Int) (y Int) (z Int) (implies (= (+ 1 (* 2 x)) (* 2 y)) (> (+ x y z) 129)))");
369
370 // Formula examples from Cooper's paper.
371
372
373 test_formula(l_true, "(forall (a Int) (exists (b Int) (or (< a (+ (* 4 b) (* 3 a))) (and (not (< a b)) (> a (+ b 1))))))");
374
375 test_formula(l_false, "(exists (y Int) (forall (x Int) (and (> (+ x (* 5 y)) 1) (> (- (* 13 x) y) 1) (< (+ x 2) 0))))");
376
377 // Harrison's formulas:
378
379 test_formula(l_false, "(forall (x Int) (y Int) (implies (and (>= x 0) (>= y 0)) (or (< (- (* 12 x) (* 8 y)) 0) (> (- (* 12 x) (* 8 y)) 2))))");
380
381
382 // test_formula(l_true, "(exists (x Int) (y Int) (= 1 (+ (* 5 x) (* 3 y))))");
383
384
385 test_formula(l_false, "(exists (x Int) (y Int) (= 1 (+ (* 5 x) (* 10 y))))");
386
387 test_formula(l_true, "(exists (x Int) (y Int) (and (>= x 0) (>= y 0) (= 1 (- (* 5 x) (* 6 y)))))");
388
389 test_formula(l_true, "(exists (x Int) (y Int) (z Int) (w Int) (= 1 (+ (* 2 w) (* 3 x) (* 4 y) (* 5 z))))");
390
391 test_formula(l_true, "(exists (x Int) (y Int) (and (>= x 0) (>= y 0) (= 1 (- (* 5 x) (* 3 y)))))");
392
393 test_formula(l_true, "(exists (x Int) (y Int) (and (>= x 0) (>= y 0) (= 1 (- (* 3 x) (* 5 y)))))");
394
395 test_formula(l_false,"(exists (x Int) (y Int) (and (>= x 0) (>= y 0) (= 1 (- (* 6 x) (* 3 y)))))");
396
397 test_formula(l_true, "(forall (x Int) (y Int) (or (= 0 (mod x 5)) (= 0 (mod y 6)) (not (= (* 6 x) (* 5 y)))))");
398
399
400 test_formula(l_false,"(forall (x Int) (y Int) (or (not (= (* 6 x) (* 5 y)))))");
401
402
403
404 // Positive variant of the Bezout theorem (see the exercise). *)
405
406 test_formula(l_true, "(forall (z Int) (implies (> z 7) (exists (x Int) (y Int) (and (>= x 0) (>= y 0) (= (+ (* 3 x) (* 5 y)) z)))))");
407
408 test_formula(l_false,"(forall (z Int) (implies (> z 2) (exists (x Int) (y Int) (and (>= x 0) (>= y 0) (= (+ (* 3 x) (* 5 y)) z)))))");
409
410 test_formula(l_true,
411 "(forall (z Int) (implies (<= z 7) "
412 " (iff (exists (x Int) (y Int) (and (>= x 0) (>= y 0) (= z (+ (* 3 x) (* 5 y))))) "
413 " (not (exists (x Int) (y Int) (and (>= x 0) (>= y 0) (= (- 7 z) (+ (* 3 x) (* 5 y))))))))) ");
414
415 // Basic result about congruences.
416
417 test_formula(l_true,
418 "(forall (x Int) "
419 " (iff (and (not (exists (m Int) (= x (* 2 m)))) (exists (m Int) (= x (+ (* 3 m) 1)))) "
420 " (or (exists (m Int) (= x (+ (* 12 m) 1))) (exists (m Int) (= x (+ (* 12 m) 7))))))");
421
422
423
424
425
426 // Inspired by the Collatz conjecture.
427
428 test_formula(l_false,
429 "(forall (a Int) (b Int) (x Int) (y Int) (z Int) "
430 " (implies (and (= (+ a 2) b) (= x (+ 1 (- b a))) (= y (- b 2)) (= z 3)) false))");
431
432 test_formula(l_true,
433 "(exists (a Int) (b Int) "
434 " (and (not (= a 1)) (= a b) (or (= a (* 2 b)) (= (* 2 b) (+ 1 (* 3 a))))))");
435
436
437 test_formula(l_false,
438 "(exists (a Int) (b Int) "
439 " (and (> a 1) (> b 1) (= a b) (or (= a (* 2 b)) (= (* 2 b) (+ 1 (* 3 a))))))");
440
441 test_formula(l_false,
442 "(exists (a Int) (b Int) "
443 " (and (> a 1) (> b 1) "
444 " (or (= a (* 2 b)) (= (* 2 b) (+ 1 (* 3 a)))) "
445 " (or (= b (* 2 a)) (= (* 2 a) (+ 1 (* 3 b))))))");
446
447 #if 0
448 // Bob Constable's "stamp problem".
449
450 test_formula(l_true,
451 "(forall (x Int) (implies (>= x 8) "
452 " (exists (u Int) (v Int) (and (>= u 0) (>= v 0) (= x (+ (* 3 u) (* 5 v)))))))");
453
454 test_formula(l_true,
455 "(exists (l Int) (forall (x Int) (implies (>= x l) "
456 " (exists (u Int) (v Int) (and (>= u 0) (>= v 0) (= x (+ (* 3 u) (* 5 v))))))))");
457
458 test_formula(l_true,
459 "(exists (l Int) (forall (x Int) (implies (>= x l) "
460 " (exists (u Int) (v Int) (and (>= u 0) (>= v 0) (= x (+ (* 3 u) (* 7 v))))))))");
461
462 test_formula(l_true,
463 "(exists (l Int) (forall (x Int) (implies (>= x l) "
464 " (exists (u Int) (v Int) (and (>= u 0) (>= v 0) (= x (+ (* 3 u) (* 8 v))))))))");
465
466 test_formula(l_true,
467 "(exists (l Int) (forall (x Int) (implies (>= x l) "
468 " (exists (u Int) (v Int) (and (>= u 0) (>= v 0) (= x (+ (* 7 u) (* 8 v))))))))");
469 #endif
470
471 // Example from reciprocal mult: (2622 * x)>>16 = x/100 within a range.
472
473
474 test_formula(l_true,
475 "(forall (x Int) (y Int) "
476 " (iff (exists (d Int) (= (+ x y) (* 2 d))) "
477 " (iff (exists (d Int) (= x (* 2 d))) (exists (d Int) (= y (* 2 d))))))");
478
479 test_formula(l_true,
480 "(forall (n Int) "
481 " (implies (and (< 0 n) (< n 2400)) "
482 " (or (and (<= n 2) (<= 2 (* 2 n))) "
483 " (and (<= n 3) (<= 3 (* 2 n))) "
484 " (and (<= n 5) (<= 5 (* 2 n))) "
485 " (and (<= n 7) (<= 7 (* 2 n))) "
486 " (and (<= n 13) (<= 13 (* 2 n))) "
487 " (and (<= n 23) (<= 23 (* 2 n))) "
488 " (and (<= n 43) (<= 43 (* 2 n))) "
489 " (and (<= n 83) (<= 83 (* 2 n))) "
490 " (and (<= n 163) (<= 163 (* 2 n))) "
491 " (and (<= n 317) (<= 317 (* 2 n))) "
492 " (and (<= n 631) (<= 631 (* 2 n))) "
493 " (and (<= n 1259) (<= 1259 (* 2 n))) "
494 " (and (<= n 2503) (<= 2503 (* 2 n)))))) ");
495
496
497
498
499 memory::finalize();
500 #ifdef _WINDOWS
501 _CrtDumpMemoryLeaks();
502 #endif
503 exit(0);
504 }
505
506
507