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