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/arith_decl_plugin.h"
11 #include "ast/ast_pp.h"
12 #include "util/lbool.h"
13 #include <sstream>
14 #include "ast/rewriter/expr_replacer.h"
15 #include "smt/smt_kernel.h"
16 #include "ast/reg_decl_plugins.h"
17 #include "ast/expr_abstract.h"
18 #include "model/model_smt2_pp.h"
19 #include "parsers/smt2/smt2parser.h"
20 #include "ast/rewriter/var_subst.h"
21
validate_quant_solution(ast_manager & m,expr * fml,expr * guard,qe::def_vector const & defs)22 static void validate_quant_solution(ast_manager& m, expr* fml, expr* guard, qe::def_vector const& defs) {
23 // verify:
24 // new_fml => fml[t/x]
25 scoped_ptr<expr_replacer> rep = mk_expr_simp_replacer(m);
26 app_ref_vector xs(m);
27 expr_substitution sub(m);
28 for (unsigned i = 0; i < defs.size(); ++i) {
29 xs.push_back(m.mk_const(defs.var(i)));
30 sub.insert(xs.back(), defs.def(i));
31 }
32 rep->set_substitution(&sub);
33 expr_ref fml1(fml, m);
34 (*rep)(fml1);
35 expr_ref tmp(m);
36 tmp = m.mk_not(m.mk_implies(guard, fml1));
37 std::cout << "validating: " << mk_pp(tmp, m) << "\n";
38 smt_params fp;
39 smt::kernel solver(m, fp);
40 solver.assert_expr(tmp);
41 lbool res = solver.check();
42 //ENSURE(res == l_false);
43 if (res != l_false) {
44 std::cout << "Validation failed: " << res << "\n";
45 std::cout << mk_pp(tmp, m) << "\n";
46 model_ref model;
47 solver.get_model(model);
48 model_smt2_pp(std::cout, m, *model, 0);
49 fatal_error(0);
50 }
51 }
52
53
54 #if 0
55 static void validate_quant_solutions(app* x, expr* fml, expr_ref_vector& guards) {
56 return;
57 // quant_elim option got removed...
58 // verify:
59 // fml <=> guard_1 \/ guard_2 \/ ...
60 ast_manager& m = guards.get_manager();
61 expr_ref tmp(m), fml2(m);
62 tmp = m.mk_or(guards.size(), guards.c_ptr());
63 expr* _x = x;
64 std::cout << mk_pp(fml, m) << "\n";
65 expr_abstract(m, 0, 1, &_x, fml, fml2);
66 std::cout << mk_pp(fml2, m) << "\n";
67 symbol name(x->get_decl()->get_name());
68 sort* s = x->get_sort();
69 fml2 = m.mk_exists(1, &s, &name, fml2);
70 std::cout << mk_pp(fml2, m) << "\n";
71 tmp = m.mk_not(m.mk_iff(fml2, tmp));
72 std::cout << mk_pp(tmp, m) << "\n";
73 smt_params fp;
74 smt::kernel solver(m, fp);
75 solver.assert_expr(tmp);
76 lbool res = solver.check();
77 std::cout << "checked\n";
78 ENSURE(res == l_false);
79 if (res != l_false) {
80 std::cout << res << "\n";
81 fatal_error(0);
82 }
83 }
84 #endif
85
86
test_quant_solver(ast_manager & m,unsigned sz,app * const * xs,expr * fml,bool validate)87 static void test_quant_solver(ast_manager& m, unsigned sz, app*const* xs, expr* fml, bool validate) {
88 smt_params params;
89 qe::expr_quant_elim qe(m, params);
90 qe::guarded_defs defs(m);
91 bool success = qe.solve_for_vars(sz, xs, fml, defs);
92 std::cout << "------------------------\n";
93 std::cout << mk_pp(fml, m) << "\n";
94 if (success) {
95 defs.display(std::cout);
96
97 for (unsigned i = 0; validate && i < defs.size(); ++i) {
98 validate_quant_solution(m, fml, defs.guard(i), defs.defs(i));
99 }
100 }
101 else {
102 std::cout << "failed\n";
103 }
104 }
105
parse_fml(ast_manager & m,char const * str)106 static expr_ref parse_fml(ast_manager& m, char const* str) {
107 expr_ref result(m);
108 cmd_context ctx(false, &m);
109 ctx.set_ignore_check(true);
110 std::ostringstream buffer;
111 buffer << "(declare-const x Int)\n"
112 << "(declare-const y Int)\n"
113 << "(declare-const z Int)\n"
114 << "(declare-const a Int)\n"
115 << "(declare-const b Int)\n"
116 << "(declare-const P Bool)\n"
117 << "(declare-const Q Bool)\n"
118 << "(declare-const r1 Real)\n"
119 << "(declare-const r2 Real)\n"
120 << "(declare-datatypes () ((IList (nil) (cons (car Int) (cdr IList)))))\n"
121 << "(declare-const l1 IList)\n"
122 << "(declare-const l2 IList)\n"
123 << "(declare-datatypes () ((Cell (null) (cell (car Cell) (cdr Cell)))))\n"
124 << "(declare-const c1 Cell)\n"
125 << "(declare-const c2 Cell)\n"
126 << "(declare-const c3 Cell)\n"
127 << "(declare-datatypes () ((Tuple (tuple (first Int) (second Bool) (third Real)))))\n"
128 << "(declare-const t1 Tuple)\n"
129 << "(declare-const t2 Tuple)\n"
130 << "(declare-const t3 Tuple)\n"
131 << "(assert " << str << ")\n";
132 std::istringstream is(buffer.str());
133 VERIFY(parse_smt2_commands(ctx, is));
134 result = ctx.assertions().get(0);
135 return result;
136 }
137
138
parse_fml(char const * str,app_ref_vector & vars,expr_ref & fml)139 static void parse_fml(char const* str, app_ref_vector& vars, expr_ref& fml) {
140 ast_manager& m = fml.get_manager();
141 fml = parse_fml(m, str);
142 if (is_exists(fml)) {
143 quantifier* q = to_quantifier(fml);
144 for (unsigned i = 0; i < q->get_num_decls(); ++i) {
145 vars.push_back(m.mk_const(q->get_decl_name(i), q->get_decl_sort(i)));
146 }
147 fml = q->get_expr();
148 var_subst vs(m, true);
149 fml = vs(fml, vars.size(), (expr*const*)vars.data());
150 }
151 }
152
test_quant_solver(ast_manager & m,app * x,char const * str,bool validate=true)153 static void test_quant_solver(ast_manager& m, app* x, char const* str, bool validate = true) {
154 expr_ref fml = parse_fml(m, str);
155 test_quant_solver(m, 1, &x, fml, validate);
156 }
157
test_quant_solver(ast_manager & m,unsigned sz,app * const * xs,char const * str,bool validate=true)158 static void test_quant_solver(ast_manager& m, unsigned sz, app*const* xs, char const* str, bool validate = true) {
159 expr_ref fml = parse_fml(m, str);
160 test_quant_solver(m, sz, xs, fml, validate);
161 }
162
test_quant_solver(ast_manager & m,char const * str,bool validate=true)163 static void test_quant_solver(ast_manager& m, char const* str, bool validate = true) {
164 expr_ref fml(m);
165 app_ref_vector vars(m);
166 parse_fml(str, vars, fml);
167 test_quant_solver(m, vars.size(), vars.data(), fml, validate);
168 }
169
170
test_quant_solve1()171 static void test_quant_solve1() {
172 ast_manager m;
173 arith_util ar(m);
174 reg_decl_plugins(m);
175 sort* i = ar.mk_int();
176 app_ref xr(m.mk_const(symbol("x"),i), m);
177 app_ref yr(m.mk_const(symbol("y"),i), m);
178 app* x = xr.get();
179 app* y = yr.get();
180 app* xy[2] = { x, y };
181
182
183 test_quant_solver(m, x, "(and (<= (* 2 x) y) (>= x z) (= (mod x 2) 0))");
184 test_quant_solver(m, x, "(and (<= x y) (= (mod x 2) 0))");
185 test_quant_solver(m, x, "(and (<= (* 2 x) y) (= (mod x 2) 0))");
186 test_quant_solver(m, x, "(and (>= x y) (= (mod x 2) 0))");
187 test_quant_solver(m, x, "(and (>= (* 2 x) y) (= (mod x 2) 0))");
188 test_quant_solver(m, x, "(and (<= (* 2 x) y) (>= (* 3 x) z) (= (mod x 2) 0))");
189 test_quant_solver(m, x, "(>= (* 2 x) a)");
190 test_quant_solver(m, x, "(<= (* 2 x) a)");
191 test_quant_solver(m, x, "(< (* 2 x) a)");
192 test_quant_solver(m, x, "(= (* 2 x) a)");
193 test_quant_solver(m, x, "(< (* 2 x) a)");
194 test_quant_solver(m, x, "(> (* 2 x) a)");
195 test_quant_solver(m, x, "(and (<= a x) (<= (* 2 x) b))");
196 test_quant_solver(m, x, "(and (<= a x) (<= x b))");
197 test_quant_solver(m, x, "(and (<= (* 2 a) x) (<= x b))");
198 test_quant_solver(m, x, "(and (<= (* 2 a) x) (<= (* 2 x) b))");
199 test_quant_solver(m, x, "(and (<= a x) (<= (* 3 x) b))");
200 test_quant_solver(m, x, "(and (<= (* 3 a) x) (<= x b))");
201 test_quant_solver(m, x, "(and (<= (* 3 a) x) (<= (* 3 x) b))");
202 test_quant_solver(m, x, "(and (< a (* 3 x)) (< (* 3 x) b))");
203 test_quant_solver(m, x, "(< (* 3 x) a)");
204 test_quant_solver(m, x, "(= (* 3 x) a)");
205 test_quant_solver(m, x, "(< (* 3 x) a)");
206 test_quant_solver(m, x, "(> (* 3 x) a)");
207 test_quant_solver(m, x, "(<= (* 3 x) a)");
208 test_quant_solver(m, x, "(>= (* 3 x) a)");
209 test_quant_solver(m, x, "(<= (* 2 x) a)");
210 test_quant_solver(m, x, "(or (= (* 2 x) y) (= (+ (* 2 x) 1) y))");
211 test_quant_solver(m, x, "(= x a)");
212 test_quant_solver(m, x, "(< x a)");
213 test_quant_solver(m, x, "(> x a)");
214 test_quant_solver(m, x, "(and (> x a) (< x b))");
215 test_quant_solver(m, x, "(and (> x a) (< x b))");
216 test_quant_solver(m, x, "(<= x a)");
217 test_quant_solver(m, x, "(>= x a)");
218 test_quant_solver(m, x, "(and (<= (* 2 x) y) (= (mod x 2) 0))");
219 test_quant_solver(m, x, "(= (* 2 x) y)");
220 test_quant_solver(m, x, "(or (< x 0) (> x 1))");
221 test_quant_solver(m, x, "(or (< x y) (> x y))");
222 test_quant_solver(m, x, "(= x y)");
223 test_quant_solver(m, x, "(<= x y)");
224 test_quant_solver(m, x, "(>= x y)");
225 test_quant_solver(m, x, "(and (<= (+ x y) 0) (<= (+ x z) 0))");
226 test_quant_solver(m, x, "(and (<= (+ x y) 0) (<= (+ (* 2 x) z) 0))");
227 test_quant_solver(m, x, "(and (<= (+ (* 3 x) y) 0) (<= (+ (* 2 x) z) 0))");
228 test_quant_solver(m, x, "(and (>= x y) (>= x z))");
229 test_quant_solver(m, x, "(< x y)");
230 test_quant_solver(m, x, "(> x y)");
231 test_quant_solver(m, 2, xy, "(and (<= (- (* 2 y) b) (+ (* 3 x) a)) (<= (- (* 2 x) a) (+ (* 4 y) b)))");
232
233 test_quant_solver(m, "(exists ((c Cell)) (= c null))");
234 test_quant_solver(m, "(exists ((c Cell)) (= c (cell null c1)))");
235
236 test_quant_solver(m, "(exists ((c Cell)) (not (= c null)))", false);
237 test_quant_solver(m, "(exists ((c Cell)) (= (cell c c) c1))", false);
238 test_quant_solver(m, "(exists ((c Cell)) (= (cell c (cdr c1)) c1))", false);
239
240
241 test_quant_solver(m, "(exists ((t Tuple)) (= (tuple a P r1) t))");
242 test_quant_solver(m, "(exists ((t Tuple)) (= a (first t)))");
243 test_quant_solver(m, "(exists ((t Tuple)) (= P (second t)))");
244 test_quant_solver(m, "(exists ((t Tuple)) (= r2 (third t)))");
245 test_quant_solver(m, "(exists ((t Tuple)) (not (= a (first t))))");
246 test_quant_solver(m, "(exists ((t Tuple)) (not (= P (second t))))");
247 test_quant_solver(m, "(exists ((t Tuple)) (not (= r2 (third t))))");
248 }
249
250
tst_quant_solve()251 void tst_quant_solve() {
252 disable_debug("heap");
253
254 test_quant_solve1();
255
256 #if 0
257 memory::finalize();
258 #ifdef _WINDOWS
259 _CrtDumpMemoryLeaks();
260 #endif
261 exit(0);
262 #endif
263 }
264
265
266