1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3
4 Module Name:
5
6 qe_lite.cpp
7
8 Abstract:
9
10 Light weight partial quantifier-elimination procedure
11
12 Author:
13
14 Nikolaj Bjorner (nbjorner) 2012-10-17
15
16 Revision History:
17
18
19 --*/
20 #include "util/uint_set.h"
21 #include "ast/expr_abstract.h"
22 #include "ast/used_vars.h"
23 #include "ast/rewriter/rewriter_def.h"
24 #include "ast/ast_pp.h"
25 #include "ast/ast_ll_pp.h"
26 #include "ast/ast_smt2_pp.h"
27 #include "ast/is_variable_test.h"
28 #include "ast/rewriter/bool_rewriter.h"
29 #include "ast/rewriter/var_subst.h"
30 #include "ast/ast_util.h"
31 #include "ast/rewriter/th_rewriter.h"
32 #include "ast/for_each_expr.h"
33 #include "ast/rewriter/expr_safe_replace.h"
34 #include "ast/datatype_decl_plugin.h"
35 #include "tactic/tactical.h"
36 #include "qe/mbp/mbp_solve_plugin.h"
37 #include "qe/qe_lite.h"
38
39 namespace qel {
40
occurs_var(unsigned idx,expr * e)41 bool occurs_var(unsigned idx, expr* e) {
42 if (is_ground(e)) return false;
43 ptr_buffer<expr> todo;
44 todo.push_back(e);
45 ast_mark mark;
46 while (!todo.empty()) {
47 expr* e = todo.back();
48 todo.pop_back();
49 if (mark.is_marked(e)) continue;
50 mark.mark(e, true);
51 if (is_ground(e)) continue;
52 if (is_var(e)) {
53 if (to_var(e)->get_idx() == idx) return true;
54 }
55 else if (is_app(e)) {
56 todo.append(to_app(e)->get_num_args(), to_app(e)->get_args());
57 }
58 else if (is_quantifier(e)) {
59 quantifier* q = to_quantifier(e);
60 if (occurs_var(idx + q->get_num_decls(), q->get_expr())) return true;
61 }
62 }
63 return false;
64 }
65
66 class eq_der {
67 ast_manager & m;
68 arith_util a;
69 datatype_util dt;
70 bv_util bv;
71 is_variable_proc* m_is_variable;
72 beta_reducer m_subst;
73 expr_ref_vector m_subst_map;
74 expr_ref_vector m_new_exprs;
75 plugin_manager<mbp::solve_plugin> m_solvers;
76
77 ptr_vector<expr> m_map;
78 int_vector m_pos2var;
79 int_vector m_var2pos;
80 ptr_vector<var> m_inx2var;
81 unsigned_vector m_order;
82 expr_ref_buffer m_new_args;
83 th_rewriter m_rewriter;
84 params_ref m_params;
85
is_sub_extract(unsigned idx,expr * t)86 bool is_sub_extract(unsigned idx, expr* t) {
87 bool has_ground = false;
88 if (bv.is_concat(t)) {
89 unsigned lo, hi;
90 ptr_buffer<expr> args;
91 args.append(to_app(t)->get_num_args(), to_app(t)->get_args());
92 for (unsigned i = 0; i < args.size(); ++i) {
93 expr* arg = args[i];
94 if (is_ground(arg)) {
95 has_ground = true;
96 continue;
97 }
98 if (bv.is_extract(arg, lo, hi, arg)) {
99 if (is_var(arg) && to_var(arg)->get_idx() == idx)
100 continue;
101 }
102 if (bv.is_concat(arg)) {
103 args.append(to_app(arg)->get_num_args(), to_app(arg)->get_args());
104 continue;
105 }
106 return false;
107 }
108 return has_ground;
109 }
110 return false;
111 }
112
strict_occurs_var(unsigned idx,expr * t)113 bool strict_occurs_var(unsigned idx, expr* t) {
114 return occurs_var(idx, t) && !is_sub_extract(idx, t);
115 }
116
der_sort_vars(ptr_vector<var> & vars,ptr_vector<expr> & definitions,unsigned_vector & order)117 void der_sort_vars(ptr_vector<var> & vars, ptr_vector<expr> & definitions, unsigned_vector & order) {
118 order.reset();
119
120 // eliminate self loops, and definitions containing quantifiers.
121 bool found = false;
122 for (unsigned i = 0; i < definitions.size(); i++) {
123 var * v = vars[i];
124 expr * t = definitions[i];
125 if (t == nullptr || has_quantifiers(t) || strict_occurs_var(v->get_idx(), t))
126 definitions[i] = nullptr;
127 else
128 found = true; // found at least one candidate
129 }
130
131 if (!found)
132 return;
133
134 typedef std::pair<expr *, unsigned> frame;
135 svector<frame> todo;
136
137 expr_fast_mark1 visiting;
138 expr_fast_mark2 done;
139
140 unsigned vidx, num;
141
142 for (unsigned i = 0; i < definitions.size(); i++) {
143 if (definitions[i] == nullptr)
144 continue;
145 var * v = vars[i];
146 SASSERT(v->get_idx() == i);
147 SASSERT(todo.empty());
148 todo.push_back(frame(v, 0));
149 while (!todo.empty()) {
150 start:
151 frame & fr = todo.back();
152 expr * t = fr.first;
153 if (done.is_marked(t)) {
154 todo.pop_back();
155 continue;
156 }
157 switch (t->get_kind()) {
158 case AST_VAR:
159 vidx = to_var(t)->get_idx();
160 if (fr.second == 0) {
161 CTRACE("der_bug", vidx >= definitions.size(), tout << "vidx: " << vidx << "\n";);
162 // Remark: The size of definitions may be smaller than the number of variables occurring in the quantified formula.
163 if (definitions.get(vidx, nullptr) != nullptr) {
164 if (visiting.is_marked(t)) {
165 // cycle detected: remove t
166 visiting.reset_mark(t);
167 definitions[vidx] = nullptr;
168 }
169 else if (is_sub_extract(vidx, definitions[vidx])) {
170 order.push_back(vidx);
171 done.mark(definitions[vidx]);
172 }
173 else {
174 visiting.mark(t);
175 fr.second = 1;
176 todo.push_back(frame(definitions[vidx], 0));
177 goto start;
178 }
179 }
180 }
181 else {
182 SASSERT(fr.second == 1);
183 visiting.reset_mark(t);
184 if (!done.is_marked(t) && definitions.get(vidx, nullptr) != nullptr) {
185 order.push_back(vidx);
186 }
187 }
188 done.mark(t);
189 todo.pop_back();
190 break;
191 case AST_QUANTIFIER:
192 UNREACHABLE();
193 break;
194 case AST_APP:
195 num = to_app(t)->get_num_args();
196 while (fr.second < num) {
197 expr * arg = to_app(t)->get_arg(fr.second);
198 fr.second++;
199 if (done.is_marked(arg)) continue;
200 todo.push_back(frame(arg, 0));
201 goto start;
202 }
203 done.mark(t);
204 todo.pop_back();
205 break;
206 default:
207 UNREACHABLE();
208 break;
209 }
210 }
211 }
212 }
213
is_variable(expr * e) const214 bool is_variable(expr * e) const {
215 return (*m_is_variable)(e);
216 }
217
is_neg_var(ast_manager & m,expr * e,var * & v)218 bool is_neg_var(ast_manager & m, expr * e, var*& v) {
219 expr* e1;
220 if (m.is_not(e, e1) && is_variable(e1)) {
221 v = to_var(e1);
222 return true;
223 }
224 else {
225 return false;
226 }
227 }
228
229
230 /**
231 \brief Return true if e can be viewed as a variable disequality.
232 Store the variable id in v and the definition in t.
233 For example:
234
235 if e is (not (= (VAR 1) T)), then v assigned to 1, and t to T.
236 if e is (iff (VAR 2) T), then v is assigned to 2, and t to (not T).
237 (not T) is used because this formula is equivalent to (not (iff (VAR 2) (not T))),
238 and can be viewed as a disequality.
239 */
is_var_diseq(expr * e,ptr_vector<var> & vs,expr_ref_vector & ts)240 bool is_var_diseq(expr * e, ptr_vector<var>& vs, expr_ref_vector& ts) {
241 expr* e1;
242 if (m.is_not(e, e1)) {
243 return is_var_eq(e, vs, ts);
244 }
245 else if (is_var_eq(e, vs, ts) && vs.size() == 1 && m.is_bool(vs[0])) {
246 expr_ref tmp(m);
247 bool_rewriter(m).mk_not(ts[0].get(), tmp);
248 ts[0] = tmp;
249 return true;
250 }
251 else {
252 return false;
253 }
254 }
255
trivial_solve(expr * lhs,expr * rhs,expr * eq,ptr_vector<var> & vs,expr_ref_vector & ts)256 bool trivial_solve(expr* lhs, expr* rhs, expr* eq, ptr_vector<var>& vs, expr_ref_vector& ts) {
257 if (!is_variable(lhs)) {
258 std::swap(lhs, rhs);
259 }
260 if (!is_variable(lhs)) {
261 return false;
262 }
263 vs.push_back(to_var(lhs));
264 ts.push_back(rhs);
265 TRACE("qe_lite", tout << mk_pp(eq, m) << "\n";);
266 return true;
267 }
268
269
same_vars(ptr_vector<var> const & vs1,ptr_vector<var> const & vs2) const270 bool same_vars(ptr_vector<var> const& vs1, ptr_vector<var> const& vs2) const {
271 if (vs1.size() != vs2.size()) {
272 return false;
273 }
274 for (unsigned i = 0; i < vs1.size(); ++i) {
275 if (vs1[i] != vs2[i]) {
276 return false;
277 }
278 }
279 return true;
280 }
281
282 /**
283 \brief Return true if e can be viewed as a variable equality.
284 */
285
is_var_eq(expr * e,ptr_vector<var> & vs,expr_ref_vector & ts)286 bool is_var_eq(expr * e, ptr_vector<var>& vs, expr_ref_vector & ts) {
287 expr* lhs = nullptr, *rhs = nullptr;
288 TRACE("qe_lite", tout << mk_pp(e, m) << "\n";);
289
290 // (= VAR t), (iff VAR t), (iff (not VAR) t), (iff t (not VAR)) cases
291 if (m.is_eq(e, lhs, rhs) && trivial_solve(lhs, rhs, e, vs, ts)) {
292 return true;
293 }
294 family_id fid = e->get_sort()->get_family_id();
295 if (m.is_eq(e, lhs, rhs)) {
296 fid = lhs->get_sort()->get_family_id();
297 }
298 auto* p = m_solvers.get_plugin(fid);
299 if (p) {
300 expr_ref res = (*p)(e);
301 if (res != e && m.is_eq(res, lhs, rhs) && is_variable(lhs)) {
302 vs.push_back(to_var(lhs));
303 ts.push_back(rhs);
304 TRACE("qe_lite", tout << res << "\n";);
305 return true;
306 }
307 }
308 return false;
309 }
310
311
is_var_def(bool check_eq,expr * e,ptr_vector<var> & vs,expr_ref_vector & ts)312 bool is_var_def(bool check_eq, expr* e, ptr_vector<var>& vs, expr_ref_vector& ts) {
313 if (check_eq) {
314 return is_var_eq(e, vs, ts);
315 }
316 else {
317 return is_var_diseq(e, vs, ts);
318 }
319 }
320
get_elimination_order()321 void get_elimination_order() {
322 TRACE("top_sort",
323 tout << "DEFINITIONS: " << std::endl;
324 for(unsigned i = 0; i < m_map.size(); i++)
325 if(m_map[i]) tout << "VAR " << i << " = " << mk_pp(m_map[i], m) << std::endl;
326 );
327
328 der_sort_vars(m_inx2var, m_map, m_order);
329
330 TRACE("qe_lite",
331 tout << "Elimination m_order:" << std::endl;
332 tout << m_order << std::endl;
333 );
334 }
335
create_substitution(unsigned sz)336 void create_substitution(unsigned sz) {
337 m_subst_map.reset();
338 m_subst_map.resize(sz, nullptr);
339 m_subst.reset();
340 m_subst.set_inv_bindings(sz, m_subst_map.data());
341 for (unsigned idx : m_order) {
342 // do all the previous substitutions before inserting
343 expr* cur = m_map[idx];
344 expr_ref r(m);
345 if (is_ground(cur)) r = cur; else m_subst(cur, r);
346 unsigned inx = sz - idx - 1;
347 TRACE("qe_lite", tout << idx << " |-> " << r << "\n";);
348 CTRACE("top_sort", m_subst_map.get(inx) != nullptr,
349 tout << "inx is " << inx << "\n"
350 << "idx is " << idx << "\n"
351 << "sz is " << sz << "\n"
352 << "subst_map[inx]: " << mk_pp(m_subst_map.get(inx), m) << "\n";);
353 SASSERT(m_subst_map.get(inx) == nullptr);
354 m_subst.update_inv_binding_at(inx, r);
355 m_subst_map[inx] = std::move(r);
356 }
357 }
358
flatten_args(quantifier * q,unsigned & num_args,expr * const * & args)359 void flatten_args(quantifier* q, unsigned& num_args, expr*const*& args) {
360 expr * e = q->get_expr();
361 if ((is_forall(q) && m.is_or(e)) ||
362 (is_exists(q) && m.is_and(e))) {
363 num_args = to_app(e)->get_num_args();
364 args = to_app(e)->get_args();
365 }
366 }
367
apply_substitution(quantifier * q,expr_ref & r)368 void apply_substitution(quantifier * q, expr_ref & r) {
369
370 expr * e = q->get_expr();
371 unsigned num_args = 1;
372 expr* const* args = &e;
373 flatten_args(q, num_args, args);
374 bool_rewriter rw(m);
375
376 // get a new expression
377 m_new_args.reset();
378 for(unsigned i = 0; i < num_args; i++) {
379 int x = m_pos2var[i];
380 if (x == -1 || m_map[x] == 0) {
381 m_new_args.push_back(args[i]);
382 }
383 }
384 if (m_new_args.size() == num_args) {
385 r = q;
386 return;
387 }
388
389 expr_ref t(m);
390 switch (q->get_kind()) {
391 case forall_k:
392 rw.mk_or(m_new_args.size(), m_new_args.data(), t);
393 break;
394 case exists_k:
395 rw.mk_and(m_new_args.size(), m_new_args.data(), t);
396 break;
397 default:
398 t = e;
399 break;
400 }
401 expr_ref new_e = m_subst(t, m_subst_map.size(), m_subst_map.data());
402 TRACE("qe_lite", tout << new_e << "\n";);
403
404 // don't forget to update the quantifier patterns
405 expr_ref_buffer new_patterns(m);
406 expr_ref_buffer new_no_patterns(m);
407 for (unsigned j = 0; j < q->get_num_patterns(); j++) {
408 expr_ref new_pat = m_subst(q->get_pattern(j), m_subst_map.size(), m_subst_map.data());
409 new_patterns.push_back(new_pat);
410 }
411
412 for (unsigned j = 0; j < q->get_num_no_patterns(); j++) {
413 expr_ref new_nopat = m_subst(q->get_no_pattern(j), m_subst_map.size(), m_subst_map.data());
414 new_no_patterns.push_back(new_nopat);
415 }
416
417 r = m.update_quantifier(q, new_patterns.size(), new_patterns.data(),
418 new_no_patterns.size(), new_no_patterns.data(), new_e);
419 }
420
reduce_quantifier1(quantifier * q,expr_ref & r,proof_ref & pr)421 void reduce_quantifier1(quantifier * q, expr_ref & r, proof_ref & pr) {
422 expr * e = q->get_expr();
423 is_variable_test is_v(q->get_num_decls());
424 set_is_variable_proc(is_v);
425 unsigned num_args = 1;
426 expr* const* args = &e;
427 if (is_lambda(q)) {
428 r = q;
429 pr = nullptr;
430 return;
431 }
432 flatten_args(q, num_args, args);
433
434 unsigned def_count = 0;
435 unsigned largest_vinx = 0;
436
437 find_definitions(num_args, args, is_exists(q), def_count, largest_vinx);
438
439 if (def_count > 0) {
440 get_elimination_order();
441 SASSERT(m_order.size() <= def_count); // some might be missing because of cycles
442
443 if (!m_order.empty()) {
444 create_substitution(largest_vinx + 1);
445 apply_substitution(q, r);
446 }
447 else {
448 r = q;
449 }
450 }
451 else {
452 TRACE("der_bug", tout << "Did not find any diseq\n" << mk_pp(q, m) << "\n";);
453 r = q;
454 }
455
456 if (m.proofs_enabled()) {
457 pr = r == q ? nullptr : m.mk_der(q, r);
458 }
459 }
460
elim_unused_vars(expr_ref & r,proof_ref & pr)461 void elim_unused_vars(expr_ref& r, proof_ref &pr) {
462 if (is_quantifier(r)) {
463 quantifier * q = to_quantifier(r);
464
465 r = ::elim_unused_vars(m, q, m_params);
466 if (m.proofs_enabled()) {
467 proof * p1 = m.mk_elim_unused_vars(q, r);
468 pr = m.mk_transitivity(pr, p1);
469 }
470 }
471 }
472
find_definitions(unsigned num_args,expr * const * args,bool is_exists,unsigned & def_count,unsigned & largest_vinx)473 void find_definitions(unsigned num_args, expr* const* args, bool is_exists, unsigned& def_count, unsigned& largest_vinx) {
474 def_count = 0;
475 largest_vinx = 0;
476 m_map.reset();
477 m_pos2var.reset();
478 m_var2pos.reset();
479 m_inx2var.reset();
480 m_pos2var.reserve(num_args, -1);
481
482 // Find all definitions
483 for (unsigned i = 0; i < num_args; i++) {
484 checkpoint();
485 ptr_vector<var> vs;
486 expr_ref_vector ts(m);
487 expr_ref t(m);
488 if (is_var_def(is_exists, args[i], vs, ts)) {
489 for (unsigned j = 0; j < vs.size(); ++j) {
490 var* v = vs[j];
491 t = ts.get(j);
492 m_rewriter(t);
493 if (t != ts.get(j)) m_new_exprs.push_back(t);
494 unsigned idx = v->get_idx();
495 if (m_map.get(idx, nullptr) == nullptr) {
496 m_map.reserve(idx + 1, 0);
497 m_inx2var.reserve(idx + 1, 0);
498 m_map[idx] = t;
499 m_inx2var[idx] = v;
500 m_pos2var[i] = idx;
501 m_var2pos.reserve(idx + 1, -1);
502 m_var2pos[idx] = i;
503 def_count++;
504 largest_vinx = std::max(idx, largest_vinx);
505 m_new_exprs.push_back(std::move(t));
506 }
507 else if (!m.is_value(m_map[idx])) {
508 // check if the new definition is simpler
509 expr *old_def = m_map[idx];
510
511 // -- prefer values
512 if (m.is_value(t)) {
513 m_pos2var[m_var2pos[idx]] = -1;
514 m_pos2var[i] = idx;
515 m_var2pos[idx] = i;
516 m_map[idx] = t;
517 m_new_exprs.push_back(std::move(t));
518 }
519 // -- prefer ground
520 else if (is_app(t) && to_app(t)->is_ground() &&
521 (!is_app(old_def) ||
522 !to_app(old_def)->is_ground())) {
523 m_pos2var[m_var2pos[idx]] = -1;
524 m_pos2var[i] = idx;
525 m_var2pos[idx] = i;
526 m_map[idx] = t;
527 m_new_exprs.push_back(std::move(t));
528 }
529 // -- prefer constants
530 else if (is_uninterp_const(t)
531 /* && !is_uninterp_const(old_def) */){
532 m_pos2var[m_var2pos[idx]] = -1;
533 m_pos2var[i] = idx;
534 m_var2pos[idx] = i;
535 m_map[idx] = t;
536 m_new_exprs.push_back(std::move(t));
537 }
538 TRACE ("qe_def",
539 tout << "Replacing definition of VAR " << idx << " from "
540 << mk_pp(old_def, m) << " to " << mk_pp(t, m)
541 << " inferred from: " << mk_pp(args[i], m) << "\n";);
542 }
543 }
544 }
545 }
546 }
547
flatten_definitions(expr_ref_vector & conjs)548 void flatten_definitions(expr_ref_vector& conjs) {
549 TRACE("qe_lite",
550 expr_ref tmp(m);
551 tmp = m.mk_and(conjs.size(), conjs.data());
552 tout << mk_pp(tmp, m) << "\n";);
553 for (unsigned i = 0; i < conjs.size(); ++i) {
554 expr* c = conjs[i].get();
555 expr *l = nullptr, *r = nullptr;
556 if (m.is_false(c)) {
557 conjs[0] = c;
558 conjs.resize(1);
559 break;
560 }
561 if (is_ground(c)) {
562 continue;
563 }
564 if (!m.is_eq(c, l, r)) {
565 continue;
566 }
567 if (!is_app(l) || !is_app(r)) {
568 continue;
569 }
570 if (dt.is_constructor(to_app(l)->get_decl())) {
571 flatten_constructor(to_app(l), to_app(r), conjs);
572 conjs[i] = conjs.back();
573 conjs.pop_back();
574 --i;
575 continue;
576 }
577 if (dt.is_constructor(to_app(r)->get_decl())) {
578 flatten_constructor(to_app(r), to_app(l), conjs);
579 conjs[i] = conjs.back();
580 conjs.pop_back();
581 --i;
582 continue;
583 }
584 }
585 TRACE("qe_lite",
586 expr_ref tmp(m);
587 tmp = m.mk_and(conjs.size(), conjs.data());
588 tout << "after flatten\n" << mk_pp(tmp, m) << "\n";);
589 }
590
flatten_constructor(app * c,app * r,expr_ref_vector & conjs)591 void flatten_constructor(app* c, app* r, expr_ref_vector& conjs) {
592 SASSERT(dt.is_constructor(c));
593
594 func_decl* d = c->get_decl();
595
596 if (dt.is_constructor(r->get_decl())) {
597 app* b = to_app(r);
598 if (d == b->get_decl()) {
599 for (unsigned j = 0; j < c->get_num_args(); ++j) {
600 conjs.push_back(m.mk_eq(c->get_arg(j), b->get_arg(j)));
601 }
602 }
603 else {
604 conjs.push_back(m.mk_false());
605 }
606 }
607 else {
608 func_decl* rec = dt.get_constructor_is(d);
609 conjs.push_back(m.mk_app(rec, r));
610 ptr_vector<func_decl> const& acc = *dt.get_constructor_accessors(d);
611 for (unsigned i = 0; i < acc.size(); ++i) {
612 conjs.push_back(m.mk_eq(c->get_arg(i), m.mk_app(acc[i], r)));
613 }
614 }
615 }
616
is_unconstrained(var * x,expr * t,unsigned i,expr_ref_vector const & conjs)617 bool is_unconstrained(var* x, expr* t, unsigned i, expr_ref_vector const& conjs) {
618 sort* s = x->get_sort();
619 if (!m.is_fully_interp(s) || !s->get_num_elements().is_infinite()) return false;
620 bool occ = occurs_var(x->get_idx(), t);
621 for (unsigned j = 0; !occ && j < conjs.size(); ++j) {
622 occ = (i != j) && occurs_var(x->get_idx(), conjs[j]);
623 }
624 return !occ;
625 }
626
remove_unconstrained(expr_ref_vector & conjs)627 bool remove_unconstrained(expr_ref_vector& conjs) {
628 bool reduced = false, change = true;
629 expr *r = nullptr, *l = nullptr, *ne = nullptr;
630 while (change) {
631 change = false;
632 for (unsigned i = 0; i < conjs.size(); ++i) {
633 if (m.is_not(conjs[i].get(), ne) && m.is_eq(ne, l, r)) {
634 TRACE("qe_lite", tout << mk_pp(conjs[i].get(), m) << " " << is_variable(l) << " " << is_variable(r) << "\n";);
635 if (is_variable(l) && ::is_var(l) && is_unconstrained(::to_var(l), r, i, conjs)) {
636 conjs[i] = m.mk_true();
637 reduced = true;
638 change = true;
639 }
640 else if (is_variable(r) && ::is_var(r) && is_unconstrained(::to_var(r), l, i, conjs)) {
641 conjs[i] = m.mk_true();
642 reduced = true;
643 change = true;
644 }
645 }
646 }
647 }
648 return reduced;
649 }
650
reduce_var_set(expr_ref_vector & conjs)651 bool reduce_var_set(expr_ref_vector& conjs) {
652 unsigned def_count = 0;
653 unsigned largest_vinx = 0;
654 bool reduced = false;
655
656 flatten_definitions(conjs);
657
658 find_definitions(conjs.size(), conjs.data(), true, def_count, largest_vinx);
659
660 if (def_count > 0) {
661 get_elimination_order();
662 SASSERT(m_order.size() <= def_count); // some might be missing because of cycles
663
664 if (!m_order.empty()) {
665 expr_ref r(m), new_r(m);
666 r = m.mk_and(conjs.size(), conjs.data());
667 create_substitution(largest_vinx + 1);
668 new_r = m_subst(r, m_subst_map.size(), m_subst_map.data());
669 m_rewriter(new_r);
670 conjs.reset();
671 flatten_and(new_r, conjs);
672 reduced = true;
673 }
674 }
675
676 if (remove_unconstrained(conjs)) {
677 reduced = true;
678 }
679
680 return reduced;
681 }
682
checkpoint()683 void checkpoint() {
684 tactic::checkpoint(m);
685 }
686
687 public:
eq_der(ast_manager & m,params_ref const & p)688 eq_der(ast_manager & m, params_ref const & p):
689 m(m),
690 a(m),
691 dt(m),
692 bv(m),
693 m_is_variable(nullptr),
694 m_subst(m),
695 m_subst_map(m),
696 m_new_exprs(m),
697 m_new_args(m),
698 m_rewriter(m),
699 m_params(p) {
700 }
701
set_is_variable_proc(is_variable_proc & proc)702 void set_is_variable_proc(is_variable_proc& proc) {
703 m_is_variable = &proc;
704 m_solvers.reset();
705 m_solvers.register_plugin(mbp::mk_arith_solve_plugin(m, proc));
706 m_solvers.register_plugin(mbp::mk_basic_solve_plugin(m, proc));
707 m_solvers.register_plugin(mbp::mk_bv_solve_plugin(m, proc));
708 }
709
operator ()(quantifier * q,expr_ref & r,proof_ref & pr)710 void operator()(quantifier * q, expr_ref & r, proof_ref & pr) {
711 TRACE("qe_lite", tout << mk_pp(q, m) << "\n";);
712 pr = nullptr;
713 r = q;
714 reduce_quantifier(q, r, pr);
715 if (r != q) {
716 elim_unused_vars(r, pr);
717 }
718 }
719
reduce_quantifier(quantifier * q,expr_ref & r,proof_ref & pr)720 void reduce_quantifier(quantifier * q, expr_ref & r, proof_ref & pr) {
721 r = q;
722 // Keep applying reduce_quantifier1 until r doesn't change anymore
723 do {
724 checkpoint();
725 proof_ref curr_pr(m);
726 q = to_quantifier(r);
727 reduce_quantifier1(q, r, curr_pr);
728 if (m.proofs_enabled() && r != q) {
729 pr = m.mk_transitivity(pr, curr_pr);
730 }
731 }
732 while (q != r && is_quantifier(r));
733
734 m_new_exprs.reset();
735 }
736
operator ()(expr_ref_vector & r)737 void operator()(expr_ref_vector& r) {
738 while (reduce_var_set(r)) ;
739 m_new_exprs.reset();
740 }
741
get_manager() const742 ast_manager& get_manager() const { return m; }
743
744
745 };
746
747 // ------------------------------------------------------------
748 // basic destructive equality (and disequality) resolution for arrays.
749
750 class ar_der {
751 ast_manager& m;
752 array_util a;
753 is_variable_proc* m_is_variable;
754 ptr_vector<expr> m_todo;
755 expr_mark m_visited;
756
is_variable(expr * e) const757 bool is_variable(expr * e) const {
758 return (*m_is_variable)(e);
759 }
760
mark_all(expr * e)761 void mark_all(expr* e) {
762 for_each_expr(*this, m_visited, e);
763 }
764
mark_all(expr_ref_vector const & fmls,unsigned j)765 void mark_all(expr_ref_vector const& fmls, unsigned j) {
766 for (unsigned i = 0; i < fmls.size(); ++i) {
767 if (i != j) {
768 mark_all(fmls[i]);
769 }
770 }
771 }
772
773 /**
774 Ex A. A[x] = t & Phi[A] where x \not\in A, t. A \not\in t, x
775 =>
776 Ex A. Phi[store(A,x,t)]
777
778 (Not implemented)
779 Perhaps also:
780 Ex A. store(A,y,z)[x] = t & Phi[A] where x \not\in A, t, y, z, A \not\in y z, t
781 =>
782 Ex A, v . (x = y => z = t) & Phi[store(store(A,x,t),y,v)]
783
784 */
785
solve_select(expr_ref_vector & conjs,unsigned i,expr * e1,expr * e2)786 bool solve_select(expr_ref_vector& conjs, unsigned i, expr* e1, expr* e2) {
787 if (a.is_select(e1)) {
788 app* a1 = to_app(e1);
789 expr* A = a1->get_arg(0);
790 if (!is_variable(A)) {
791 return false;
792 }
793 m_visited.reset();
794 for (unsigned j = 1; j < a1->get_num_args(); ++j) {
795 mark_all(a1->get_arg(j));
796 }
797 mark_all(e2);
798 if (m_visited.is_marked(A)) {
799 return false;
800 }
801 ptr_vector<expr> args;
802 args.push_back(A);
803 args.append(a1->get_num_args()-1, a1->get_args()+1);
804 args.push_back(e2);
805 expr* B = a.mk_store(args.size(), args.data());
806 expr_safe_replace rep(m);
807 rep.insert(A, B);
808 expr_ref tmp(m);
809 TRACE("qe_lite",
810 tout << mk_pp(e1, m) << " = " << mk_pp(e2, m) << "\n";);
811 for (unsigned j = 0; j < conjs.size(); ++j) {
812 if (i == j) {
813 conjs[j] = m.mk_true();
814 }
815 else {
816 rep(conjs[j].get(), tmp);
817 conjs[j] = tmp;
818 }
819 }
820 return true;
821 }
822 return false;
823 }
824
solve_select(expr_ref_vector & conjs,unsigned i,expr * e)825 bool solve_select(expr_ref_vector& conjs, unsigned i, expr* e) {
826 expr* e1, *e2;
827 return
828 m.is_eq(e, e1, e2) &&
829 (solve_select(conjs, i, e1, e2) ||
830 solve_select(conjs, i, e2, e1));
831 }
832
833 /**
834 Ex x. A[x] != B[x] & Phi where x \not\in A, B, Phi
835 =>
836 A != B & Phi
837 */
solve_neq_select(expr_ref_vector & conjs,unsigned i,expr * e)838 bool solve_neq_select(expr_ref_vector& conjs, unsigned i, expr* e) {
839 expr* e1, *a1, *a2;
840 if (m.is_not(e, e1) && m.is_eq(e1, a1, a2)) {
841 if (a.is_select(a1) &&
842 a.is_select(a2) &&
843 to_app(a1)->get_num_args() == to_app(a2)->get_num_args()) {
844 expr* e1 = to_app(a1)->get_arg(0);
845 expr* e2 = to_app(a2)->get_arg(0);
846 m_visited.reset();
847 mark_all(conjs, i);
848 mark_all(e1);
849 mark_all(e2);
850 for (unsigned j = 1; j < to_app(a1)->get_num_args(); ++j) {
851 expr* x = to_app(a1)->get_arg(j);
852 expr* y = to_app(a2)->get_arg(j);
853 if (!is_variable(x)) {
854 return false;
855 }
856 if (x != y) {
857 return false;
858 }
859 if (m_visited.is_marked(x)) {
860 return false;
861 }
862 }
863 conjs[i] = m.mk_not(m.mk_eq(e1, e2));
864 return true;
865 }
866 }
867 return false;
868 }
869
checkpoint()870 void checkpoint() {
871 tactic::checkpoint(m);
872 }
873
874 public:
875
ar_der(ast_manager & m)876 ar_der(ast_manager& m): m(m), a(m), m_is_variable(nullptr) {}
877
operator ()(expr_ref_vector & fmls)878 void operator()(expr_ref_vector& fmls) {
879 for (unsigned i = 0; i < fmls.size(); ++i) {
880 checkpoint();
881 solve_select(fmls, i, fmls[i].get());
882 solve_neq_select(fmls, i, fmls[i].get());
883 }
884 }
885
operator ()(expr * e)886 void operator()(expr* e) {}
887
set_is_variable_proc(is_variable_proc & proc)888 void set_is_variable_proc(is_variable_proc& proc) { m_is_variable = &proc;}
889
890 };
891
892
893 // ------------------------------------------------------------
894 // fm_tactic adapted to eliminate designated de-Bruijn indices.
895
896 namespace fm {
897 typedef ptr_vector<app> clauses;
898 typedef unsigned var;
899 typedef int bvar;
900 typedef int literal;
901 typedef svector<var> var_vector;
902
903 // Encode the constraint
904 // lits \/ ( as[0]*xs[0] + ... + as[num_vars-1]*xs[num_vars-1] <= c
905 // if strict is true, then <= is <.
906 struct constraint {
get_obj_sizeqel::fm::constraint907 static unsigned get_obj_size(unsigned num_lits, unsigned num_vars) {
908 return sizeof(constraint) + num_lits*sizeof(literal) + num_vars*(sizeof(var) + sizeof(rational));
909 }
910 unsigned m_id;
911 unsigned m_num_lits:29;
912 unsigned m_strict:1;
913 unsigned m_dead:1;
914 unsigned m_mark:1;
915 unsigned m_num_vars;
916 literal * m_lits;
917 var * m_xs;
918 rational * m_as;
919 rational m_c;
920 expr_dependency * m_dep;
~constraintqel::fm::constraint921 ~constraint() {
922 rational * it = m_as;
923 rational * end = it + m_num_vars;
924 for (; it != end; ++it)
925 it->~rational();
926 }
927
hashqel::fm::constraint928 unsigned hash() const { return hash_u(m_id); }
929 };
930
931 typedef ptr_vector<constraint> constraints;
932
933 class constraint_set {
934 unsigned_vector m_id2pos;
935 constraints m_set;
936 public:
937 typedef constraints::const_iterator iterator;
938
contains(constraint const & c) const939 bool contains(constraint const & c) const {
940 if (c.m_id >= m_id2pos.size())
941 return false;
942 return m_id2pos[c.m_id] != UINT_MAX;
943 }
944
empty() const945 bool empty() const { return m_set.empty(); }
size() const946 unsigned size() const { return m_set.size(); }
947
insert(constraint & c)948 void insert(constraint & c) {
949 unsigned id = c.m_id;
950 m_id2pos.reserve(id+1, UINT_MAX);
951 if (m_id2pos[id] != UINT_MAX)
952 return; // already in the set
953 unsigned pos = m_set.size();
954 m_id2pos[id] = pos;
955 m_set.push_back(&c);
956 }
957
erase(constraint & c)958 void erase(constraint & c) {
959 unsigned id = c.m_id;
960 if (id >= m_id2pos.size())
961 return;
962 unsigned pos = m_id2pos[id];
963 if (pos == UINT_MAX)
964 return;
965 m_id2pos[id] = UINT_MAX;
966 unsigned last_pos = m_set.size() - 1;
967 if (pos != last_pos) {
968 constraint * last_c = m_set[last_pos];
969 m_set[pos] = last_c;
970 m_id2pos[last_c->m_id] = pos;
971 }
972 m_set.pop_back();
973 }
974
erase()975 constraint & erase() {
976 SASSERT(!empty());
977 constraint & c = *m_set.back();
978 m_id2pos[c.m_id] = UINT_MAX;
979 m_set.pop_back();
980 return c;
981 }
982
reset()983 void reset() { m_id2pos.reset(); m_set.reset(); }
finalize()984 void finalize() { m_id2pos.finalize(); m_set.finalize(); }
985
begin() const986 iterator begin() const { return m_set.begin(); }
end() const987 iterator end() const { return m_set.end(); }
988 };
989
990 class fm {
991 ast_manager & m;
992 is_variable_proc* m_is_variable;
993 small_object_allocator m_allocator;
994 arith_util m_util;
995 constraints m_constraints;
996 expr_ref_vector m_bvar2expr;
997 signed_char_vector m_bvar2sign;
998 obj_map<expr, bvar> m_expr2bvar;
999 char_vector m_is_int;
1000 char_vector m_forbidden;
1001 expr_ref_vector m_var2expr;
1002 obj_map<expr, var> m_expr2var;
1003 unsigned_vector m_var2pos;
1004 vector<constraints> m_lowers;
1005 vector<constraints> m_uppers;
1006 uint_set m_forbidden_set; // variables that cannot be eliminated because occur in non OCC ineq part
1007 expr_ref_vector m_new_fmls;
1008 id_gen m_id_gen;
1009 bool m_fm_real_only;
1010 unsigned m_fm_limit;
1011 unsigned m_fm_cutoff1;
1012 unsigned m_fm_cutoff2;
1013 unsigned m_fm_extra;
1014 bool m_fm_occ;
1015 unsigned m_counter;
1016 bool m_inconsistent;
1017 expr_dependency_ref m_inconsistent_core;
1018 constraint_set m_sub_todo;
1019
1020 // ---------------------------
1021 //
1022 // OCC clause recognizer
1023 //
1024 // ---------------------------
1025
is_literal(expr * t) const1026 bool is_literal(expr * t) const {
1027 expr * atom;
1028 return is_uninterp_const(t) || (m.is_not(t, atom) && is_uninterp_const(atom));
1029 }
1030
is_constraint(expr * t) const1031 bool is_constraint(expr * t) const {
1032 return !is_literal(t);
1033 }
1034
is_var(expr * t,expr * & x) const1035 bool is_var(expr * t, expr * & x) const {
1036
1037 if ((*m_is_variable)(t)) {
1038 x = t;
1039 return true;
1040 }
1041 else if (m_util.is_to_real(t) && (*m_is_variable)(to_app(t)->get_arg(0))) {
1042 x = to_app(t)->get_arg(0);
1043 return true;
1044 }
1045 return false;
1046 }
1047
is_var(expr * t) const1048 bool is_var(expr * t) const {
1049 expr * x;
1050 return is_var(t, x);
1051 }
1052
is_linear_mon_core(expr * t,expr * & x) const1053 bool is_linear_mon_core(expr * t, expr * & x) const {
1054 expr * c;
1055 if (m_util.is_mul(t, c, x) && m_util.is_numeral(c) && is_var(x, x))
1056 return true;
1057 return is_var(t, x);
1058 }
1059
is_linear_mon(expr * t) const1060 bool is_linear_mon(expr * t) const {
1061 expr * x;
1062 return is_linear_mon_core(t, x);
1063 }
1064
is_linear_pol(expr * t) const1065 bool is_linear_pol(expr * t) const {
1066 unsigned num_mons;
1067 expr * const * mons;
1068 if (m_util.is_add(t)) {
1069 num_mons = to_app(t)->get_num_args();
1070 mons = to_app(t)->get_args();
1071 }
1072 else {
1073 num_mons = 1;
1074 mons = &t;
1075 }
1076
1077 expr_fast_mark2 visited;
1078 bool all_forbidden = true;
1079 for (unsigned i = 0; i < num_mons; i++) {
1080 expr * x;
1081 if (!is_linear_mon_core(mons[i], x))
1082 return false;
1083 if (visited.is_marked(x))
1084 return false; // duplicates are not supported... must simplify first
1085 visited.mark(x);
1086 SASSERT(::is_var(x));
1087 if (!m_forbidden_set.contains(::to_var(x)->get_idx()) && (!m_fm_real_only || !m_util.is_int(x)))
1088 all_forbidden = false;
1089 }
1090 return !all_forbidden;
1091 }
1092
is_linear_ineq(expr * t) const1093 bool is_linear_ineq(expr * t) const {
1094 bool result = false;
1095 m.is_not(t, t);
1096 expr * lhs, * rhs;
1097 if (m_util.is_le(t, lhs, rhs) || m_util.is_ge(t, lhs, rhs)) {
1098 result = m_util.is_numeral(rhs) && is_linear_pol(lhs);
1099 }
1100 TRACE("qe_lite", tout << mk_pp(t, m) << " " << (result?"true":"false") << "\n";);
1101
1102 return result;
1103 }
1104
is_occ(expr * t)1105 bool is_occ(expr * t) {
1106 if (m_fm_occ && m.is_or(t)) {
1107 unsigned num = to_app(t)->get_num_args();
1108 bool found = false;
1109 for (unsigned i = 0; i < num; i++) {
1110 expr * l = to_app(t)->get_arg(i);
1111 if (is_literal(l)) {
1112 continue;
1113 }
1114 else if (is_linear_ineq(l)) {
1115 if (found)
1116 return false;
1117 found = true;
1118 }
1119 else {
1120 return false;
1121 }
1122 }
1123 return found;
1124 }
1125 return is_linear_ineq(t);
1126 }
1127
1128 // ---------------------------
1129 //
1130 // Memory mng
1131 //
1132 // ---------------------------
del_constraint(constraint * c)1133 void del_constraint(constraint * c) {
1134 m.dec_ref(c->m_dep);
1135 m_sub_todo.erase(*c);
1136 m_id_gen.recycle(c->m_id);
1137 c->~constraint();
1138 unsigned sz = constraint::get_obj_size(c->m_num_lits, c->m_num_vars);
1139 m_allocator.deallocate(sz, c);
1140 }
1141
del_constraints(unsigned sz,constraint * const * cs)1142 void del_constraints(unsigned sz, constraint * const * cs) {
1143 for (unsigned i = 0; i < sz; i++)
1144 del_constraint(cs[i]);
1145 }
1146
reset_constraints()1147 void reset_constraints() {
1148 del_constraints(m_constraints.size(), m_constraints.data());
1149 m_constraints.reset();
1150 }
1151
mk_constraint(unsigned num_lits,literal * lits,unsigned num_vars,var * xs,rational * as,rational & c,bool strict,expr_dependency * dep)1152 constraint * mk_constraint(unsigned num_lits, literal * lits, unsigned num_vars, var * xs, rational * as, rational & c, bool strict,
1153 expr_dependency * dep) {
1154 unsigned sz = constraint::get_obj_size(num_lits, num_vars);
1155 char * mem = static_cast<char*>(m_allocator.allocate(sz));
1156 char * mem_as = mem + sizeof(constraint);
1157 char * mem_lits = mem_as + sizeof(rational)*num_vars;
1158 char * mem_xs = mem_lits + sizeof(literal)*num_lits;
1159 constraint * cnstr = new (mem) constraint();
1160 cnstr->m_id = m_id_gen.mk();
1161 cnstr->m_num_lits = num_lits;
1162 cnstr->m_dead = false;
1163 cnstr->m_mark = false;
1164 cnstr->m_strict = strict;
1165 cnstr->m_num_vars = num_vars;
1166 cnstr->m_lits = reinterpret_cast<literal*>(mem_lits);
1167 for (unsigned i = 0; i < num_lits; i++)
1168 cnstr->m_lits[i] = lits[i];
1169 cnstr->m_xs = reinterpret_cast<var*>(mem_xs);
1170 cnstr->m_as = reinterpret_cast<rational*>(mem_as);
1171 for (unsigned i = 0; i < num_vars; i++) {
1172 TRACE("qe_lite", tout << "xs[" << i << "]: " << xs[i] << "\n";);
1173 cnstr->m_xs[i] = xs[i];
1174 new (cnstr->m_as + i) rational(as[i]);
1175 }
1176 cnstr->m_c = c;
1177 DEBUG_CODE({
1178 for (unsigned i = 0; i < num_vars; i++) {
1179 SASSERT(cnstr->m_xs[i] == xs[i]);
1180 SASSERT(cnstr->m_as[i] == as[i]);
1181 }
1182 });
1183 cnstr->m_dep = dep;
1184 m.inc_ref(dep);
1185 return cnstr;
1186 }
1187
1188 // ---------------------------
1189 //
1190 // Util
1191 //
1192 // ---------------------------
1193
num_vars() const1194 unsigned num_vars() const { return m_is_int.size(); }
1195
1196 // multiply as and c, by the lcm of their denominators
mk_int(unsigned num,rational * as,rational & c)1197 void mk_int(unsigned num, rational * as, rational & c) {
1198 rational l = denominator(c);
1199 for (unsigned i = 0; i < num; i++)
1200 l = lcm(l, denominator(as[i]));
1201 if (l.is_one())
1202 return;
1203 c *= l;
1204 SASSERT(c.is_int());
1205 for (unsigned i = 0; i < num; i++) {
1206 as[i] *= l;
1207 SASSERT(as[i].is_int());
1208 }
1209 }
1210
normalize_coeffs(constraint & c)1211 void normalize_coeffs(constraint & c) {
1212 if (c.m_num_vars == 0)
1213 return;
1214 // compute gcd of all coefficients
1215 rational g = c.m_c;
1216 if (g.is_neg())
1217 g.neg();
1218 for (unsigned i = 0; i < c.m_num_vars; i++) {
1219 if (g.is_one())
1220 break;
1221 if (c.m_as[i].is_pos())
1222 g = gcd(c.m_as[i], g);
1223 else
1224 g = gcd(-c.m_as[i], g);
1225 }
1226 if (g.is_one())
1227 return;
1228 c.m_c /= g;
1229 for (unsigned i = 0; i < c.m_num_vars; i++)
1230 c.m_as[i] /= g;
1231 }
1232
display(std::ostream & out,constraint const & c) const1233 void display(std::ostream & out, constraint const & c) const {
1234 for (unsigned i = 0; i < c.m_num_lits; i++) {
1235 literal l = c.m_lits[i];
1236 if (sign(l))
1237 out << "~";
1238 bvar p = lit2bvar(l);
1239 out << mk_ismt2_pp(m_bvar2expr[p], m);
1240 out << " ";
1241 }
1242 out << "(";
1243 if (c.m_num_vars == 0)
1244 out << "0";
1245 for (unsigned i = 0; i < c.m_num_vars; i++) {
1246 if (i > 0)
1247 out << " + ";
1248 if (!c.m_as[i].is_one())
1249 out << c.m_as[i] << "*";
1250 out << mk_ismt2_pp(m_var2expr.get(c.m_xs[i]), m);
1251 }
1252 if (c.m_strict)
1253 out << " < ";
1254 else
1255 out << " <= ";
1256 out << c.m_c;
1257 out << ")";
1258 }
1259
1260 /**
1261 \brief Return true if c1 subsumes c2
1262
1263 c1 subsumes c2 If
1264 1) All literals of c1 are literals of c2
1265 2) polynomial of c1 == polynomial of c2
1266 3) c1.m_c <= c2.m_c
1267 */
subsumes(constraint const & c1,constraint const & c2)1268 bool subsumes(constraint const & c1, constraint const & c2) {
1269 if (&c1 == &c2)
1270 return false;
1271 // quick checks first
1272 if (c1.m_num_lits > c2.m_num_lits)
1273 return false;
1274 if (c1.m_num_vars != c2.m_num_vars)
1275 return false;
1276 if (c1.m_c > c2.m_c)
1277 return false;
1278 if (!c1.m_strict && c2.m_strict && c1.m_c == c2.m_c)
1279 return false;
1280
1281 m_counter += c1.m_num_lits + c2.m_num_lits;
1282
1283 for (unsigned i = 0; i < c1.m_num_vars; i++) {
1284 m_var2pos[c1.m_xs[i]] = i;
1285 }
1286
1287 bool failed = false;
1288 for (unsigned i = 0; i < c2.m_num_vars; i++) {
1289 unsigned pos1 = m_var2pos[c2.m_xs[i]];
1290 if (pos1 == UINT_MAX || c1.m_as[pos1] != c2.m_as[i]) {
1291 failed = true;
1292 break;
1293 }
1294 }
1295
1296 for (unsigned i = 0; i < c1.m_num_vars; i++) {
1297 m_var2pos[c1.m_xs[i]] = UINT_MAX;
1298 }
1299
1300 if (failed)
1301 return false;
1302
1303 for (unsigned i = 0; i < c2.m_num_lits; i++) {
1304 literal l = c2.m_lits[i];
1305 bvar b = lit2bvar(l);
1306 SASSERT(m_bvar2sign[b] == 0);
1307 m_bvar2sign[b] = sign(l) ? -1 : 1;
1308 }
1309
1310 for (unsigned i = 0; i < c1.m_num_lits; i++) {
1311 literal l = c1.m_lits[i];
1312 bvar b = lit2bvar(l);
1313 char s = sign(l) ? -1 : 1;
1314 if (m_bvar2sign[b] != s) {
1315 failed = true;
1316 break;
1317 }
1318 }
1319
1320 for (unsigned i = 0; i < c2.m_num_lits; i++) {
1321 literal l = c2.m_lits[i];
1322 bvar b = lit2bvar(l);
1323 m_bvar2sign[b] = 0;
1324 }
1325
1326 if (failed)
1327 return false;
1328
1329 return true;
1330 }
1331
backward_subsumption(constraint const & c)1332 void backward_subsumption(constraint const & c) {
1333 if (c.m_num_vars == 0)
1334 return;
1335 var best = UINT_MAX;
1336 unsigned best_sz = UINT_MAX;
1337 bool best_lower = false;
1338 for (unsigned i = 0; i < c.m_num_vars; i++) {
1339 var xi = c.m_xs[i];
1340 if (is_forbidden(xi))
1341 continue; // variable is not in the index
1342 bool neg_a = c.m_as[i].is_neg();
1343 constraints & cs = neg_a ? m_lowers[xi] : m_uppers[xi];
1344 if (cs.size() < best_sz) {
1345 best = xi;
1346 best_sz = cs.size();
1347 best_lower = neg_a;
1348 }
1349 }
1350 if (best_sz == 0)
1351 return;
1352 if (best == UINT_MAX)
1353 return; // none of the c variables are in the index.
1354 constraints & cs = best_lower ? m_lowers[best] : m_uppers[best];
1355 m_counter += cs.size();
1356 constraints::iterator it = cs.begin();
1357 constraints::iterator it2 = it;
1358 constraints::iterator end = cs.end();
1359 for (; it != end; ++it) {
1360 constraint * c2 = *it;
1361 if (c2->m_dead)
1362 continue;
1363 if (subsumes(c, *c2)) {
1364 TRACE("qe_lite", display(tout, c); tout << "\nsubsumed:\n"; display(tout, *c2); tout << "\n";);
1365 c2->m_dead = true;
1366 continue;
1367 }
1368 *it2 = *it;
1369 ++it2;
1370 }
1371 cs.set_end(it2);
1372 }
1373
subsume()1374 void subsume() {
1375 while (!m_sub_todo.empty()) {
1376 constraint & c = m_sub_todo.erase();
1377 if (c.m_dead)
1378 continue;
1379 backward_subsumption(c);
1380 }
1381 }
1382
1383 public:
1384
1385 // ---------------------------
1386 //
1387 // Initialization
1388 //
1389 // ---------------------------
1390
fm(ast_manager & _m)1391 fm(ast_manager & _m):
1392 m(_m),
1393 m_is_variable(nullptr),
1394 m_allocator("fm-elim"),
1395 m_util(m),
1396 m_bvar2expr(m),
1397 m_var2expr(m),
1398 m_new_fmls(m),
1399 m_inconsistent_core(m) {
1400 updt_params();
1401 m_counter = 0;
1402 m_inconsistent = false;
1403 }
1404
~fm()1405 ~fm() {
1406 reset_constraints();
1407 }
1408
updt_params()1409 void updt_params() {
1410 m_fm_real_only = false;
1411 m_fm_limit = 5000000;
1412 m_fm_cutoff1 = 8;
1413 m_fm_cutoff2 = 256;
1414 m_fm_extra = 0;
1415 m_fm_occ = true;
1416 }
1417
1418 private:
1419
1420 struct forbidden_proc {
1421 fm & m_owner;
forbidden_procqel::fm::fm::forbidden_proc1422 forbidden_proc(fm & o):m_owner(o) {}
operator ()qel::fm::fm::forbidden_proc1423 void operator()(::var * n) {
1424 if (m_owner.is_var(n) && n->get_sort()->get_family_id() == m_owner.m_util.get_family_id()) {
1425 m_owner.m_forbidden_set.insert(n->get_idx());
1426 }
1427 }
operator ()qel::fm::fm::forbidden_proc1428 void operator()(app * n) { }
operator ()qel::fm::fm::forbidden_proc1429 void operator()(quantifier * n) {}
1430 };
1431
init_forbidden_set(expr_ref_vector const & g)1432 void init_forbidden_set(expr_ref_vector const & g) {
1433 m_forbidden_set.reset();
1434 expr_fast_mark1 visited;
1435 forbidden_proc proc(*this);
1436 unsigned sz = g.size();
1437 for (unsigned i = 0; i < sz; i++) {
1438 expr * f = g[i];
1439 if (is_occ(f)) {
1440 TRACE("qe_lite", tout << "OCC: " << mk_ismt2_pp(f, m) << "\n";);
1441 continue;
1442 }
1443 TRACE("qe_lite", tout << "not OCC:\n" << mk_ismt2_pp(f, m) << "\n";);
1444 quick_for_each_expr(proc, visited, f);
1445 }
1446 }
1447
init(expr_ref_vector const & g)1448 void init(expr_ref_vector const & g) {
1449 m_sub_todo.reset();
1450 m_id_gen.reset();
1451 reset_constraints();
1452 m_bvar2expr.reset();
1453 m_bvar2sign.reset();
1454 m_bvar2expr.push_back(nullptr); // bvar 0 is not used
1455 m_bvar2sign.push_back(0);
1456 m_expr2var.reset();
1457 m_is_int.reset();
1458 m_var2pos.reset();
1459 m_forbidden.reset();
1460 m_var2expr.reset();
1461 m_expr2var.reset();
1462 m_lowers.reset();
1463 m_uppers.reset();
1464 m_new_fmls.reset();
1465 m_counter = 0;
1466 m_inconsistent = false;
1467 m_inconsistent_core = nullptr;
1468 init_forbidden_set(g);
1469 }
1470
1471 // ---------------------------
1472 //
1473 // Internal data-structures
1474 //
1475 // ---------------------------
1476
sign(literal l)1477 static bool sign(literal l) { return l < 0; }
lit2bvar(literal l)1478 static bvar lit2bvar(literal l) { return l < 0 ? -l : l; }
1479
is_int(var x) const1480 bool is_int(var x) const {
1481 return m_is_int[x] != 0;
1482 }
1483
is_forbidden(var x) const1484 bool is_forbidden(var x) const {
1485 return m_forbidden[x] != 0;
1486 }
1487
all_int(constraint const & c) const1488 bool all_int(constraint const & c) const {
1489 for (unsigned i = 0; i < c.m_num_vars; i++) {
1490 if (!is_int(c.m_xs[i]))
1491 return false;
1492 }
1493 return true;
1494 }
1495
to_expr(constraint const & c)1496 app * to_expr(constraint const & c) {
1497 expr * ineq;
1498 if (c.m_num_vars == 0) {
1499 // 0 < k (for k > 0) --> true
1500 // 0 <= 0 -- > true
1501 if (c.m_c.is_pos() || (!c.m_strict && c.m_c.is_zero()))
1502 return m.mk_true();
1503 ineq = nullptr;
1504 }
1505 else {
1506 bool int_cnstr = all_int(c);
1507 ptr_buffer<expr> ms;
1508 for (unsigned i = 0; i < c.m_num_vars; i++) {
1509 expr * x = m_var2expr.get(c.m_xs[i]);
1510 if (!int_cnstr && is_int(c.m_xs[i]))
1511 x = m_util.mk_to_real(x);
1512 if (c.m_as[i].is_one())
1513 ms.push_back(x);
1514 else
1515 ms.push_back(m_util.mk_mul(m_util.mk_numeral(c.m_as[i], int_cnstr), x));
1516 }
1517 expr * lhs;
1518 if (c.m_num_vars == 1)
1519 lhs = ms[0];
1520 else
1521 lhs = m_util.mk_add(ms.size(), ms.data());
1522 expr * rhs = m_util.mk_numeral(c.m_c, int_cnstr);
1523 if (c.m_strict) {
1524 ineq = m.mk_not(m_util.mk_ge(lhs, rhs));
1525 }
1526 else {
1527 ineq = m_util.mk_le(lhs, rhs);
1528 }
1529 }
1530
1531 if (c.m_num_lits == 0) {
1532 if (ineq)
1533 return to_app(ineq);
1534 else
1535 return m.mk_false();
1536 }
1537
1538 ptr_buffer<expr> lits;
1539 for (unsigned i = 0; i < c.m_num_lits; i++) {
1540 literal l = c.m_lits[i];
1541 if (sign(l))
1542 lits.push_back(m.mk_not(m_bvar2expr.get(lit2bvar(l))));
1543 else
1544 lits.push_back(m_bvar2expr.get(lit2bvar(l)));
1545 }
1546 if (ineq)
1547 lits.push_back(ineq);
1548 if (lits.size() == 1)
1549 return to_app(lits[0]);
1550 else
1551 return m.mk_or(lits.size(), lits.data());
1552 }
1553
mk_var(expr * t)1554 var mk_var(expr * t) {
1555 SASSERT(::is_var(t));
1556 SASSERT(m_util.is_int(t) || m_util.is_real(t));
1557 var x = m_var2expr.size();
1558 m_var2expr.push_back(t);
1559 bool is_int = m_util.is_int(t);
1560 m_is_int.push_back(is_int);
1561 m_var2pos.push_back(UINT_MAX);
1562 m_expr2var.insert(t, x);
1563 m_lowers.push_back(constraints());
1564 m_uppers.push_back(constraints());
1565 bool forbidden = m_forbidden_set.contains(::to_var(t)->get_idx()) || (m_fm_real_only && is_int);
1566 m_forbidden.push_back(forbidden);
1567 SASSERT(m_var2expr.size() == m_is_int.size());
1568 SASSERT(m_lowers.size() == m_is_int.size());
1569 SASSERT(m_uppers.size() == m_is_int.size());
1570 SASSERT(m_forbidden.size() == m_is_int.size());
1571 SASSERT(m_var2pos.size() == m_is_int.size());
1572 TRACE("qe_lite", tout << mk_pp(t,m) << " |-> " << x << " forbidden: " << forbidden << "\n";);
1573 return x;
1574 }
1575
mk_bvar(expr * t)1576 bvar mk_bvar(expr * t) {
1577 SASSERT(is_uninterp_const(t));
1578 SASSERT(m.is_bool(t));
1579 bvar p = m_bvar2expr.size();
1580 m_bvar2expr.push_back(t);
1581 m_bvar2sign.push_back(0);
1582 SASSERT(m_bvar2expr.size() == m_bvar2sign.size());
1583 m_expr2bvar.insert(t, p);
1584 SASSERT(p > 0);
1585 return p;
1586 }
1587
to_var(expr * t)1588 var to_var(expr * t) {
1589 var x;
1590 if (!m_expr2var.find(t, x))
1591 x = mk_var(t);
1592 SASSERT(m_expr2var.contains(t));
1593 SASSERT(m_var2expr.get(x) == t);
1594 TRACE("qe_lite", tout << mk_ismt2_pp(t, m) << " --> " << x << "\n";);
1595 return x;
1596 }
1597
to_bvar(expr * t)1598 bvar to_bvar(expr * t) {
1599 bvar p;
1600 if (m_expr2bvar.find(t, p))
1601 return p;
1602 return mk_bvar(t);
1603 }
1604
to_literal(expr * t)1605 literal to_literal(expr * t) {
1606 if (m.is_not(t, t))
1607 return -to_bvar(t);
1608 else
1609 return to_bvar(t);
1610 }
1611
1612
add_constraint(expr * f,expr_dependency * dep)1613 void add_constraint(expr * f, expr_dependency * dep) {
1614 TRACE("qe_lite", tout << mk_pp(f, m) << "\n";);
1615 SASSERT(!m.is_or(f) || m_fm_occ);
1616 sbuffer<literal> lits;
1617 sbuffer<var> xs;
1618 buffer<rational> as;
1619 rational c;
1620 bool strict = false;
1621 unsigned num;
1622 expr * const * args;
1623 if (m.is_or(f)) {
1624 num = to_app(f)->get_num_args();
1625 args = to_app(f)->get_args();
1626 }
1627 else {
1628 num = 1;
1629 args = &f;
1630 }
1631
1632 #if Z3DEBUG
1633 bool found_ineq = false;
1634 #endif
1635 for (unsigned i = 0; i < num; i++) {
1636 expr * l = args[i];
1637 if (is_literal(l)) {
1638 lits.push_back(to_literal(l));
1639 }
1640 else {
1641 // found inequality
1642 SASSERT(!found_ineq);
1643 DEBUG_CODE(found_ineq = true;);
1644 bool neg = m.is_not(l, l);
1645 SASSERT(m_util.is_le(l) || m_util.is_ge(l));
1646 strict = neg;
1647 if (m_util.is_ge(l))
1648 neg = !neg;
1649 expr * lhs = to_app(l)->get_arg(0);
1650 expr * rhs = to_app(l)->get_arg(1);
1651 VERIFY (m_util.is_numeral(rhs, c));
1652 if (neg)
1653 c.neg();
1654 unsigned num_mons;
1655 expr * const * mons;
1656 if (m_util.is_add(lhs)) {
1657 num_mons = to_app(lhs)->get_num_args();
1658 mons = to_app(lhs)->get_args();
1659 }
1660 else {
1661 num_mons = 1;
1662 mons = &lhs;
1663 }
1664
1665 bool all_int = true;
1666 for (unsigned j = 0; j < num_mons; j++) {
1667 expr * monomial = mons[j];
1668 expr * a;
1669 rational a_val;
1670 expr * x = nullptr;
1671 if (m_util.is_mul(monomial, a, x)) {
1672 VERIFY(m_util.is_numeral(a, a_val));
1673 }
1674 else {
1675 x = monomial;
1676 a_val = rational(1);
1677 }
1678 if (neg)
1679 a_val.neg();
1680 VERIFY(is_var(x, x));
1681 xs.push_back(to_var(x));
1682 as.push_back(a_val);
1683 if (!is_int(xs.back()))
1684 all_int = false;
1685 }
1686 mk_int(as.size(), as.data(), c);
1687 if (all_int && strict) {
1688 strict = false;
1689 c--;
1690 }
1691 }
1692 }
1693
1694 TRACE("qe_lite", tout << "before mk_constraint: "; for (unsigned i = 0; i < xs.size(); i++) tout << " " << xs[i]; tout << "\n";);
1695
1696 constraint * new_c = mk_constraint(lits.size(),
1697 lits.data(),
1698 xs.size(),
1699 xs.data(),
1700 as.data(),
1701 c,
1702 strict,
1703 dep);
1704
1705 TRACE("qe_lite", tout << "add_constraint: "; display(tout, *new_c); tout << "\n";);
1706 VERIFY(register_constraint(new_c));
1707 }
1708
is_false(constraint const & c) const1709 bool is_false(constraint const & c) const {
1710 return c.m_num_lits == 0 && c.m_num_vars == 0 && (c.m_c.is_neg() || (c.m_strict && c.m_c.is_zero()));
1711 }
1712
register_constraint(constraint * c)1713 bool register_constraint(constraint * c) {
1714 normalize_coeffs(*c);
1715 if (is_false(*c)) {
1716 del_constraint(c);
1717 m_inconsistent = true;
1718 TRACE("qe_lite", tout << "is false "; display(tout, *c); tout << "\n";);
1719 return false;
1720 }
1721
1722 bool r = false;
1723
1724 for (unsigned i = 0; i < c->m_num_vars; i++) {
1725 var x = c->m_xs[i];
1726 if (!is_forbidden(x)) {
1727 r = true;
1728 if (c->m_as[i].is_neg())
1729 m_lowers[x].push_back(c);
1730 else
1731 m_uppers[x].push_back(c);
1732 }
1733 }
1734
1735 if (r) {
1736 m_sub_todo.insert(*c);
1737 m_constraints.push_back(c);
1738 return true;
1739 }
1740 else {
1741 TRACE("qe_lite", tout << "all variables are forbidden "; display(tout, *c); tout << "\n";);
1742 m_new_fmls.push_back(to_expr(*c));
1743 del_constraint(c);
1744 return false;
1745 }
1746 }
1747
init_use_list(expr_ref_vector const & g)1748 void init_use_list(expr_ref_vector const & g) {
1749 unsigned sz = g.size();
1750 for (unsigned i = 0; !m_inconsistent && i < sz; i++) {
1751 expr * f = g[i];
1752 if (is_occ(f))
1753 add_constraint(f, nullptr);
1754 else
1755 m_new_fmls.push_back(f);
1756 }
1757 }
1758
get_cost(var x) const1759 unsigned get_cost(var x) const {
1760 unsigned long long r = static_cast<unsigned long long>(m_lowers[x].size()) * static_cast<unsigned long long>(m_uppers[x].size());
1761 if (r > UINT_MAX)
1762 return UINT_MAX;
1763 return static_cast<unsigned>(r);
1764 }
1765
1766 typedef std::pair<var, unsigned> x_cost;
1767
1768 struct x_cost_lt {
1769 char_vector const m_is_int;
x_cost_ltqel::fm::fm::x_cost_lt1770 x_cost_lt(char_vector & is_int):m_is_int(is_int) {}
operator ()qel::fm::fm::x_cost_lt1771 bool operator()(x_cost const & p1, x_cost const & p2) const {
1772 // Integer variables with cost 0 can be eliminated even if they depend on real variables.
1773 // Cost 0 == no lower or no upper bound.
1774 if (p1.second == 0) {
1775 if (p2.second > 0) return true;
1776 return p1.first < p2.first;
1777 }
1778 if (p2.second == 0) return false;
1779 bool int1 = m_is_int[p1.first] != 0;
1780 bool int2 = m_is_int[p2.first] != 0;
1781 return (!int1 && int2) || (int1 == int2 && p1.second < p2.second);
1782 }
1783 };
1784
sort_candidates(var_vector & xs)1785 void sort_candidates(var_vector & xs) {
1786 svector<x_cost> x_cost_vector;
1787 unsigned num = num_vars();
1788 for (var x = 0; x < num; x++) {
1789 if (!is_forbidden(x)) {
1790 x_cost_vector.push_back(x_cost(x, get_cost(x)));
1791 }
1792 }
1793 // x_cost_lt is not a total order on variables
1794 std::stable_sort(x_cost_vector.begin(), x_cost_vector.end(), x_cost_lt(m_is_int));
1795 TRACE("qe_lite",
1796 for (auto const& kv : x_cost_vector) {
1797 tout << "(" << mk_ismt2_pp(m_var2expr.get(kv.first), m) << " " << kv.second << ") ";
1798 }
1799 tout << "\n";);
1800 for (auto const& kv : x_cost_vector) {
1801 xs.push_back(kv.first);
1802 }
1803 }
1804
cleanup_constraints(constraints & cs)1805 void cleanup_constraints(constraints & cs) {
1806 unsigned j = 0;
1807 unsigned sz = cs.size();
1808 for (unsigned i = 0; i < sz; i++) {
1809 constraint * c = cs[i];
1810 if (c->m_dead)
1811 continue;
1812 cs[j] = c;
1813 j++;
1814 }
1815 cs.shrink(j);
1816 }
1817
1818 // Set all_int = true if all variables in c are int.
1819 // Set unit_coeff = true if the coefficient of x in c is 1 or -1.
1820 // If all_int = false, then unit_coeff may not be set.
analyze(constraint const & c,var x,bool & all_int,bool & unit_coeff) const1821 void analyze(constraint const & c, var x, bool & all_int, bool & unit_coeff) const {
1822 all_int = true;
1823 unit_coeff = true;
1824 for (unsigned i = 0; i < c.m_num_vars; i++) {
1825 if (!is_int(c.m_xs[i])) {
1826 all_int = false;
1827 return;
1828 }
1829 if (c.m_xs[i] == x) {
1830 unit_coeff = (c.m_as[i].is_one() || c.m_as[i].is_minus_one());
1831 }
1832 }
1833 }
1834
analyze(constraints const & cs,var x,bool & all_int,bool & unit_coeff) const1835 void analyze(constraints const & cs, var x, bool & all_int, bool & unit_coeff) const {
1836 all_int = true;
1837 unit_coeff = true;
1838 for (constraint const* c : cs) {
1839 bool curr_unit_coeff;
1840 analyze(*c, x, all_int, curr_unit_coeff);
1841 if (!all_int)
1842 return;
1843 if (!curr_unit_coeff)
1844 unit_coeff = false;
1845 }
1846 }
1847
1848 // An integer variable x may be eliminated, if
1849 // 1- All variables in the constraints it occur are integer.
1850 // 2- The coefficient of x in all lower bounds (or all upper bounds) is unit.
can_eliminate(var x) const1851 bool can_eliminate(var x) const {
1852 if (!is_int(x))
1853 return true;
1854 bool all_int;
1855 bool l_unit, u_unit;
1856 analyze(m_lowers[x], x, all_int, l_unit);
1857 if (!all_int)
1858 return false;
1859 analyze(m_uppers[x], x, all_int, u_unit);
1860 return all_int && (l_unit || u_unit);
1861 }
1862
copy_constraints(constraints const & s,clauses & t)1863 void copy_constraints(constraints const & s, clauses & t) {
1864 for (constraint const* cns : s) {
1865 app * c = to_expr(*cns);
1866 t.push_back(c);
1867 }
1868 }
1869
1870 clauses tmp_clauses;
save_constraints(var x)1871 void save_constraints(var x) { }
1872
mark_constraints_dead(constraints const & cs)1873 void mark_constraints_dead(constraints const & cs) {
1874 for (constraint* c : cs)
1875 c->m_dead = true;
1876 }
1877
mark_constraints_dead(var x)1878 void mark_constraints_dead(var x) {
1879 save_constraints(x);
1880 mark_constraints_dead(m_lowers[x]);
1881 mark_constraints_dead(m_uppers[x]);
1882 }
1883
get_coeff(constraint const & c,var x,rational & a)1884 void get_coeff(constraint const & c, var x, rational & a) {
1885 for (unsigned i = 0; i < c.m_num_vars; i++) {
1886 if (c.m_xs[i] == x) {
1887 a = c.m_as[i];
1888 return;
1889 }
1890 }
1891 UNREACHABLE();
1892 }
1893
1894 var_vector new_xs;
1895 vector<rational> new_as;
1896 svector<literal> new_lits;
1897
resolve(constraint const & l,constraint const & u,var x)1898 constraint * resolve(constraint const & l, constraint const & u, var x) {
1899 m_counter += l.m_num_vars + u.m_num_vars + l.m_num_lits + u.m_num_lits;
1900 rational a, b;
1901 get_coeff(l, x, a);
1902 get_coeff(u, x, b);
1903 SASSERT(a.is_neg());
1904 SASSERT(b.is_pos());
1905 a.neg();
1906
1907 SASSERT(!is_int(x) || a.is_one() || b.is_one());
1908
1909 new_xs.reset();
1910 new_as.reset();
1911 rational new_c = l.m_c*b + u.m_c*a;
1912 bool new_strict = l.m_strict || u.m_strict;
1913
1914 for (unsigned i = 0; i < l.m_num_vars; i++) {
1915 var xi = l.m_xs[i];
1916 if (xi == x)
1917 continue;
1918 unsigned pos = new_xs.size();
1919 new_xs.push_back(xi);
1920 SASSERT(m_var2pos[xi] == UINT_MAX);
1921 m_var2pos[xi] = pos;
1922 new_as.push_back(l.m_as[i] * b);
1923 SASSERT(new_xs[m_var2pos[xi]] == xi);
1924 SASSERT(new_xs.size() == new_as.size());
1925 }
1926
1927 for (unsigned i = 0; i < u.m_num_vars; i++) {
1928 var xi = u.m_xs[i];
1929 if (xi == x)
1930 continue;
1931 unsigned pos = m_var2pos[xi];
1932 if (pos == UINT_MAX) {
1933 new_xs.push_back(xi);
1934 new_as.push_back(u.m_as[i] * a);
1935 }
1936 else {
1937 new_as[pos] += u.m_as[i] * a;
1938 }
1939 }
1940
1941 // remove zeros and check whether all variables are int
1942 bool all_int = true;
1943 unsigned sz = new_xs.size();
1944 unsigned j = 0;
1945 for (unsigned i = 0; i < sz; i++) {
1946 if (new_as[i].is_zero())
1947 continue;
1948 if (!is_int(new_xs[i]))
1949 all_int = false;
1950 if (i != j) {
1951 new_xs[j] = new_xs[i];
1952 new_as[j] = new_as[i];
1953 }
1954 j++;
1955 }
1956 new_xs.shrink(j);
1957 new_as.shrink(j);
1958
1959 if (all_int && new_strict) {
1960 new_strict = false;
1961 new_c --;
1962 }
1963
1964 // reset m_var2pos
1965 for (unsigned i = 0; i < l.m_num_vars; i++) {
1966 m_var2pos[l.m_xs[i]] = UINT_MAX;
1967 }
1968
1969 if (new_xs.empty() && (new_c.is_pos() || (!new_strict && new_c.is_zero()))) {
1970 // literal is true
1971 TRACE("qe_lite", tout << "resolution " << x << " consequent literal is always true: \n";
1972 display(tout, l);
1973 tout << "\n";
1974 display(tout, u); tout << "\n";);
1975 return nullptr; // no constraint needs to be created.
1976 }
1977
1978 new_lits.reset();
1979 for (unsigned i = 0; i < l.m_num_lits; i++) {
1980 literal lit = l.m_lits[i];
1981 bvar p = lit2bvar(lit);
1982 m_bvar2sign[p] = sign(lit) ? -1 : 1;
1983 new_lits.push_back(lit);
1984 }
1985
1986 bool tautology = false;
1987 for (unsigned i = 0; i < u.m_num_lits && !tautology; i++) {
1988 literal lit = u.m_lits[i];
1989 bvar p = lit2bvar(lit);
1990 switch (m_bvar2sign[p]) {
1991 case 0:
1992 new_lits.push_back(lit);
1993 break;
1994 case -1:
1995 if (!sign(lit))
1996 tautology = true;
1997 break;
1998 case 1:
1999 if (sign(lit))
2000 tautology = true;
2001 break;
2002 default:
2003 UNREACHABLE();
2004 }
2005 }
2006
2007 // reset m_bvar2sign
2008 for (unsigned i = 0; i < l.m_num_lits; i++) {
2009 literal lit = l.m_lits[i];
2010 bvar p = lit2bvar(lit);
2011 m_bvar2sign[p] = 0;
2012 }
2013
2014 if (tautology) {
2015 TRACE("qe_lite", tout << "resolution " << x << " tautology: \n";
2016 display(tout, l);
2017 tout << "\n";
2018 display(tout, u); tout << "\n";);
2019 return nullptr;
2020 }
2021
2022 expr_dependency * new_dep = m.mk_join(l.m_dep, u.m_dep);
2023
2024 if (new_lits.empty() && new_xs.empty() && (new_c.is_neg() || (new_strict && new_c.is_zero()))) {
2025 TRACE("qe_lite", tout << "resolution " << x << " inconsistent: \n";
2026 display(tout, l);
2027 tout << "\n";
2028 display(tout, u); tout << "\n";);
2029 m_inconsistent = true;
2030 m_inconsistent_core = new_dep;
2031 return nullptr;
2032 }
2033
2034 constraint * new_cnstr = mk_constraint(new_lits.size(),
2035 new_lits.data(),
2036 new_xs.size(),
2037 new_xs.data(),
2038 new_as.data(),
2039 new_c,
2040 new_strict,
2041 new_dep);
2042
2043 TRACE("qe_lite", tout << "resolution " << x << "\n";
2044 display(tout, l);
2045 tout << "\n";
2046 display(tout, u);
2047 tout << "\n---->\n";
2048 display(tout, *new_cnstr);
2049 tout << "\n";
2050 tout << "new_dep: " << new_dep << "\n";);
2051
2052 return new_cnstr;
2053 }
2054
2055 ptr_vector<constraint> new_constraints;
2056
try_eliminate(var x)2057 bool try_eliminate(var x) {
2058 constraints & l = m_lowers[x];
2059 constraints & u = m_uppers[x];
2060 cleanup_constraints(l);
2061 cleanup_constraints(u);
2062
2063 if (l.empty() || u.empty()) {
2064 // easy case
2065 mark_constraints_dead(x);
2066 TRACE("qe_lite", tout << "variable was eliminated (trivial case)\n";);
2067 return true;
2068 }
2069
2070 unsigned num_lowers = l.size();
2071 unsigned num_uppers = u.size();
2072
2073 if (num_lowers > m_fm_cutoff1 && num_uppers > m_fm_cutoff1)
2074 return false;
2075
2076 if (num_lowers * num_uppers > m_fm_cutoff2)
2077 return false;
2078
2079 if (!can_eliminate(x))
2080 return false;
2081
2082 m_counter += num_lowers * num_uppers;
2083
2084 TRACE("qe_lite", tout << "eliminating " << mk_ismt2_pp(m_var2expr.get(x), m) << "\nlowers:\n";
2085 display_constraints(tout, l); tout << "uppers:\n"; display_constraints(tout, u););
2086
2087 unsigned num_old_cnstrs = num_uppers + num_lowers;
2088 unsigned limit = num_old_cnstrs + m_fm_extra;
2089 unsigned num_new_cnstrs = 0;
2090 new_constraints.reset();
2091 for (unsigned i = 0; i < num_lowers; i++) {
2092 for (unsigned j = 0; j < num_uppers; j++) {
2093 if (m_inconsistent || num_new_cnstrs > limit) {
2094 TRACE("qe_lite", tout << "too many new constraints: " << num_new_cnstrs << "\n";);
2095 del_constraints(new_constraints.size(), new_constraints.data());
2096 return false;
2097 }
2098 constraint const & l_c = *(l[i]);
2099 constraint const & u_c = *(u[j]);
2100 constraint * new_c = resolve(l_c, u_c, x);
2101 if (new_c != nullptr) {
2102 num_new_cnstrs++;
2103 new_constraints.push_back(new_c);
2104 }
2105 }
2106 }
2107
2108 mark_constraints_dead(x);
2109
2110 unsigned sz = new_constraints.size();
2111
2112 m_counter += sz;
2113
2114 for (unsigned i = 0; i < sz; i++) {
2115 constraint * c = new_constraints[i];
2116 backward_subsumption(*c);
2117 register_constraint(c);
2118 }
2119 TRACE("qe_lite", tout << "variables was eliminated old: " << num_old_cnstrs << " new_constraints: " << sz << "\n";);
2120 return true;
2121 }
2122
copy_remaining(vector<constraints> & v2cs)2123 void copy_remaining(vector<constraints> & v2cs) {
2124 for (constraints& cs : v2cs) {
2125 for (constraint* c : cs) {
2126 if (!c->m_dead) {
2127 c->m_dead = true;
2128 expr * new_f = to_expr(*c);
2129 TRACE("qe_lite", tout << "asserting...\n" << mk_ismt2_pp(new_f, m) << "\nnew_dep: " << c->m_dep << "\n";);
2130 m_new_fmls.push_back(new_f);
2131 }
2132 }
2133 }
2134 v2cs.finalize();
2135 }
2136
2137 // Copy remaining clauses to m_new_fmls
copy_remaining()2138 void copy_remaining() {
2139 copy_remaining(m_uppers);
2140 copy_remaining(m_lowers);
2141 }
2142
checkpoint()2143 void checkpoint() {
2144 tactic::checkpoint(m);
2145 }
2146 public:
2147
set_is_variable_proc(is_variable_proc & proc)2148 void set_is_variable_proc(is_variable_proc& proc) { m_is_variable = &proc;}
2149
operator ()(expr_ref_vector & fmls)2150 void operator()(expr_ref_vector& fmls) {
2151 init(fmls);
2152 init_use_list(fmls);
2153 for (auto & f : fmls) {
2154 if (has_quantifiers(f)) return;
2155 }
2156 if (m_inconsistent) {
2157 m_new_fmls.reset();
2158 m_new_fmls.push_back(m.mk_false());
2159 }
2160 else {
2161 TRACE("qe_lite", display(tout););
2162
2163 subsume();
2164 var_vector candidates;
2165 sort_candidates(candidates);
2166 unsigned eliminated = 0;
2167
2168 unsigned num = candidates.size();
2169 for (unsigned i = 0; i < num; i++) {
2170 checkpoint();
2171 if (m_counter > m_fm_limit)
2172 break;
2173 m_counter++;
2174 if (try_eliminate(candidates[i]))
2175 eliminated++;
2176 if (m_inconsistent) {
2177 m_new_fmls.reset();
2178 m_new_fmls.push_back(m.mk_false());
2179 break;
2180 }
2181 }
2182 if (!m_inconsistent) {
2183 copy_remaining();
2184 }
2185 }
2186 reset_constraints();
2187 fmls.reset();
2188 fmls.append(m_new_fmls);
2189 }
2190
display_constraints(std::ostream & out,constraints const & cs) const2191 void display_constraints(std::ostream & out, constraints const & cs) const {
2192 for (constraint const* c : cs) {
2193 display(out << " ", *c);
2194 out << "\n";
2195 }
2196 }
2197
display(std::ostream & out) const2198 void display(std::ostream & out) const {
2199 unsigned num = num_vars();
2200 for (var x = 0; x < num; x++) {
2201 if (is_forbidden(x))
2202 continue;
2203 out << mk_ismt2_pp(m_var2expr.get(x), m) << "\n";
2204 display_constraints(out, m_lowers[x]);
2205 display_constraints(out, m_uppers[x]);
2206 }
2207 }
2208 };
2209
2210 } // namespace fm
2211 } // anonymous namespace
2212
2213 class qe_lite::impl {
2214 struct elim_cfg : public default_rewriter_cfg {
2215 impl& m_imp;
2216 ast_manager& m;
2217 public:
elim_cfgqe_lite::impl::elim_cfg2218 elim_cfg(impl& i): m_imp(i), m(i.m) {}
2219
reduce_quantifierqe_lite::impl::elim_cfg2220 bool reduce_quantifier(quantifier * q,
2221 expr * new_body,
2222 expr * const * new_patterns,
2223 expr * const * new_no_patterns,
2224 expr_ref & result,
2225 proof_ref & result_pr) {
2226 result = new_body;
2227 if (is_forall(q)) {
2228 result = m.mk_not(result);
2229 }
2230 uint_set indices;
2231 for (unsigned i = 0; i < q->get_num_decls(); ++i) {
2232 indices.insert(i);
2233 }
2234 if (q->get_kind() != lambda_k) {
2235 m_imp(indices, true, result);
2236 }
2237 if (is_forall(q)) {
2238 result = push_not(result);
2239 }
2240 expr_ref tmp(m);
2241 tmp = m.update_quantifier(
2242 q,
2243 q->get_num_patterns(), new_patterns,
2244 q->get_num_no_patterns(), new_no_patterns, result);
2245 m_imp.m_rewriter(tmp, result, result_pr);
2246 if (m.proofs_enabled()) {
2247 result_pr = m.mk_transitivity(m.mk_rewrite(q, tmp), result_pr);
2248 }
2249
2250 return true;
2251 }
2252 };
2253
2254 class elim_star : public rewriter_tpl<elim_cfg> {
2255 elim_cfg m_cfg;
2256 public:
elim_star(impl & i)2257 elim_star(impl& i):
2258 rewriter_tpl<elim_cfg>(i.m, i.m.proofs_enabled(), m_cfg),
2259 m_cfg(i)
2260 {}
2261 };
2262
2263 private:
2264 ast_manager& m;
2265 qel::eq_der m_der;
2266 qel::fm::fm m_fm;
2267 qel::ar_der m_array_der;
2268 elim_star m_elim_star;
2269 th_rewriter m_rewriter;
2270
2271 bool m_use_array_der;
has_unique_non_ground(expr_ref_vector const & fmls,unsigned & index)2272 bool has_unique_non_ground(expr_ref_vector const& fmls, unsigned& index) {
2273 index = fmls.size();
2274 if (index <= 1) {
2275 return false;
2276 }
2277 for (unsigned i = 0; i < fmls.size(); ++i) {
2278 if (!is_ground(fmls[i])) {
2279 if (index != fmls.size()) {
2280 return false;
2281 }
2282 index = i;
2283 }
2284 }
2285 return index < fmls.size();
2286 }
2287
2288 public:
impl(ast_manager & m,params_ref const & p,bool use_array_der)2289 impl(ast_manager & m, params_ref const & p, bool use_array_der):
2290 m(m),
2291 m_der(m, p),
2292 m_fm(m),
2293 m_array_der(m),
2294 m_elim_star(*this),
2295 m_rewriter(m),
2296 m_use_array_der(use_array_der) {}
2297
operator ()(app_ref_vector & vars,expr_ref & fml)2298 void operator()(app_ref_vector& vars, expr_ref& fml) {
2299 if (vars.empty()) {
2300 return;
2301 }
2302 expr_ref tmp(fml);
2303 quantifier_ref q(m);
2304 proof_ref pr(m);
2305 symbol qe_lite("QE");
2306 expr_abstract(m, 0, vars.size(), (expr*const*)vars.data(), fml, tmp);
2307 ptr_vector<sort> sorts;
2308 svector<symbol> names;
2309 for (unsigned i = 0; i < vars.size(); ++i) {
2310 sorts.push_back(vars[i]->get_sort());
2311 names.push_back(vars[i]->get_decl()->get_name());
2312 }
2313 q = m.mk_exists(vars.size(), sorts.data(), names.data(), tmp, 1, qe_lite);
2314 m_der.reduce_quantifier(q, tmp, pr);
2315 // assumes m_der just updates the quantifier and does not change things more.
2316 if (is_exists(tmp) && to_quantifier(tmp)->get_qid() == qe_lite) {
2317 used_vars used;
2318 tmp = to_quantifier(tmp)->get_expr();
2319 used(tmp);
2320 var_subst vs(m, true);
2321 fml = vs(tmp, vars.size(), (expr*const*)vars.data());
2322 // collect set of variables that were used.
2323 unsigned j = 0;
2324 for (unsigned i = 0; i < vars.size(); ++i) {
2325 if (used.contains(vars.size()-i-1)) {
2326 vars.set(j, vars.get(i));
2327 ++j;
2328 }
2329 }
2330 vars.resize(j);
2331 }
2332 else {
2333 fml = std::move(tmp);
2334 }
2335 }
2336
operator ()(expr_ref & fml,proof_ref & pr)2337 void operator()(expr_ref& fml, proof_ref& pr) {
2338 expr_ref tmp(m);
2339 m_elim_star(fml, tmp, pr);
2340 if (m.proofs_enabled()) {
2341 pr = m.mk_rewrite(fml, tmp);
2342 }
2343 fml = std::move(tmp);
2344 }
2345
operator ()(uint_set const & index_set,bool index_of_bound,expr_ref & fml)2346 void operator()(uint_set const& index_set, bool index_of_bound, expr_ref& fml) {
2347 expr_ref_vector disjs(m), conjs(m);
2348 flatten_or(fml, disjs);
2349 for (unsigned i = 0, e = disjs.size(); i != e; ++i) {
2350 conjs.reset();
2351 conjs.push_back(disjs[i].get());
2352 (*this)(index_set, index_of_bound, conjs);
2353 bool_rewriter(m).mk_and(conjs.size(), conjs.data(), fml);
2354 disjs[i] = std::move(fml);
2355 }
2356 bool_rewriter(m).mk_or(disjs.size(), disjs.data(), fml);
2357 }
2358
2359
operator ()(uint_set const & index_set,bool index_of_bound,expr_ref_vector & fmls)2360 void operator()(uint_set const& index_set, bool index_of_bound, expr_ref_vector& fmls) {
2361 flatten_and(fmls);
2362 unsigned index;
2363 if (has_unique_non_ground(fmls, index)) {
2364 expr_ref fml(m);
2365 fml = fmls[index].get();
2366 (*this)(index_set, index_of_bound, fml);
2367 fmls[index] = fml;
2368 return;
2369 }
2370 TRACE("qe_lite", tout << fmls << "\n";);
2371 is_variable_test is_var(index_set, index_of_bound);
2372 m_der.set_is_variable_proc(is_var);
2373 m_fm.set_is_variable_proc(is_var);
2374 m_array_der.set_is_variable_proc(is_var);
2375 m_der(fmls);
2376 m_fm(fmls);
2377 // AG: disalble m_array_der() since it interferes with other array handling
2378 if (m_use_array_der) m_array_der(fmls);
2379 TRACE("qe_lite", for (unsigned i = 0; i < fmls.size(); ++i) tout << mk_pp(fmls[i].get(), m) << "\n";);
2380 }
2381
2382 };
2383
qe_lite(ast_manager & m,params_ref const & p,bool use_array_der)2384 qe_lite::qe_lite(ast_manager & m, params_ref const & p, bool use_array_der) {
2385 m_impl = alloc(impl, m, p, use_array_der);
2386 }
2387
~qe_lite()2388 qe_lite::~qe_lite() {
2389 dealloc(m_impl);
2390 }
2391
operator ()(app_ref_vector & vars,expr_ref & fml)2392 void qe_lite::operator()(app_ref_vector& vars, expr_ref& fml) {
2393 (*m_impl)(vars, fml);
2394 }
2395
2396
operator ()(expr_ref & fml,proof_ref & pr)2397 void qe_lite::operator()(expr_ref& fml, proof_ref& pr) {
2398 (*m_impl)(fml, pr);
2399 }
2400
operator ()(uint_set const & index_set,bool index_of_bound,expr_ref & fml)2401 void qe_lite::operator()(uint_set const& index_set, bool index_of_bound, expr_ref& fml) {
2402 (*m_impl)(index_set, index_of_bound, fml);
2403 }
2404
operator ()(uint_set const & index_set,bool index_of_bound,expr_ref_vector & fmls)2405 void qe_lite::operator()(uint_set const& index_set, bool index_of_bound, expr_ref_vector& fmls) {
2406 (*m_impl)(index_set, index_of_bound, fmls);
2407 }
2408
2409 namespace {
2410 class qe_lite_tactic : public tactic {
2411 ast_manager& m;
2412 params_ref m_params;
2413 qe_lite m_qe;
2414
checkpoint()2415 void checkpoint() {
2416 tactic::checkpoint(m);
2417 }
2418
2419 #if 0
2420 void debug_diff(expr* a, expr* b) {
2421 ptr_vector<expr> as, bs;
2422 as.push_back(a);
2423 bs.push_back(b);
2424 expr* a1, *a2, *b1, *b2;
2425 while (!as.empty()) {
2426 a = as.back();
2427 b = bs.back();
2428 as.pop_back();
2429 bs.pop_back();
2430 if (a == b) {
2431 continue;
2432 }
2433 else if (is_forall(a) && is_forall(b)) {
2434 as.push_back(to_quantifier(a)->get_expr());
2435 bs.push_back(to_quantifier(b)->get_expr());
2436 }
2437 else if (m.is_and(a, a1, a2) && m.is_and(b, b1, b2)) {
2438 as.push_back(a1);
2439 as.push_back(a2);
2440 bs.push_back(b1);
2441 bs.push_back(b2);
2442 }
2443 else if (m.is_eq(a, a1, a2) && m.is_eq(b, b1, b2)) {
2444 as.push_back(a1);
2445 as.push_back(a2);
2446 bs.push_back(b1);
2447 bs.push_back(b2);
2448 }
2449 else {
2450 TRACE("qe", tout << mk_pp(a, m) << " != " << mk_pp(b, m) << "\n";);
2451 }
2452 }
2453 }
2454 #endif
2455
2456 public:
qe_lite_tactic(ast_manager & m,params_ref const & p)2457 qe_lite_tactic(ast_manager & m, params_ref const & p):
2458 m(m),
2459 m_params(p),
2460 m_qe(m, p, true) {}
2461
translate(ast_manager & m)2462 tactic * translate(ast_manager & m) override {
2463 return alloc(qe_lite_tactic, m, m_params);
2464 }
2465
updt_params(params_ref const & p)2466 void updt_params(params_ref const & p) override {
2467 m_params = p;
2468 // m_imp->updt_params(p);
2469 }
2470
collect_param_descrs(param_descrs & r)2471 void collect_param_descrs(param_descrs & r) override {
2472 // m_imp->collect_param_descrs(r);
2473 }
2474
operator ()(goal_ref const & g,goal_ref_buffer & result)2475 void operator()(goal_ref const & g,
2476 goal_ref_buffer & result) override {
2477 tactic_report report("qe-lite", *g);
2478 proof_ref new_pr(m);
2479 expr_ref new_f(m);
2480
2481 unsigned sz = g->size();
2482 for (unsigned i = 0; i < sz; i++) {
2483 checkpoint();
2484 if (g->inconsistent())
2485 break;
2486 expr * f = g->form(i);
2487 if (!has_quantifiers(f))
2488 continue;
2489 new_f = f;
2490 m_qe(new_f, new_pr);
2491 if (new_pr) {
2492 expr* fact = m.get_fact(new_pr);
2493 if (to_app(fact)->get_arg(0) != to_app(fact)->get_arg(1)) {
2494 new_pr = m.mk_modus_ponens(g->pr(i), new_pr);
2495 }
2496 else {
2497 new_pr = g->pr(i);
2498 }
2499 }
2500 if (f != new_f) {
2501 TRACE("qe", tout << mk_pp(f, m) << "\n" << new_f << "\n" << new_pr << "\n";);
2502 g->update(i, new_f, new_pr, g->dep(i));
2503 }
2504 }
2505 g->inc_depth();
2506 result.push_back(g.get());
2507 }
2508
collect_statistics(statistics & st) const2509 void collect_statistics(statistics & st) const override {
2510 // m_imp->collect_statistics(st);
2511 }
2512
reset_statistics()2513 void reset_statistics() override {
2514 // m_imp->reset_statistics();
2515 }
2516
cleanup()2517 void cleanup() override {
2518 m_qe.~qe_lite();
2519 new (&m_qe) qe_lite(m, m_params, true);
2520 }
2521 };
2522 }
2523
mk_qe_lite_tactic(ast_manager & m,params_ref const & p)2524 tactic * mk_qe_lite_tactic(ast_manager & m, params_ref const & p) {
2525 return alloc(qe_lite_tactic, m, p);
2526 }
2527