1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3
4 Module Name:
5
6 fm_tactic.cpp
7
8 Abstract:
9
10 Use Fourier-Motzkin to eliminate variables.
11 This strategy can handle conditional bounds
12 (i.e., clauses with at most one constraint).
13
14 The strategy mk_occf can be used to put the
15 formula in OCC form.
16
17 Author:
18
19 Leonardo de Moura (leonardo) 2012-02-04.
20
21 Revision History:
22
23 --*/
24 #include "tactic/arith/fm_tactic.h"
25 #include "tactic/tactical.h"
26 #include "ast/arith_decl_plugin.h"
27 #include "ast/for_each_expr.h"
28 #include "ast/ast_smt2_pp.h"
29 #include "ast/ast_pp.h"
30 #include "util/id_gen.h"
31 #include "model/model_evaluator.h"
32 #include "model/model_v2_pp.h"
33 #include "tactic/core/simplify_tactic.h"
34
35 class fm_tactic : public tactic {
36 typedef ptr_vector<app> clauses;
37 typedef unsigned var;
38 typedef int bvar;
39 typedef int literal;
40 typedef svector<var> var_vector;
41
42 struct fm_model_converter : public model_converter {
43 ast_manager & m;
44 ptr_vector<func_decl> m_xs;
45 vector<clauses> m_clauses;
46
47 enum r_kind {
48 NONE,
49 LOWER,
50 UPPER
51 };
52
is_falsefm_tactic::fm_model_converter53 bool is_false(model_ref & md, app * p) {
54 SASSERT(is_uninterp_const(p));
55 expr * val = md->get_const_interp(p->get_decl());
56 if (val == nullptr) {
57 // if it is don't care, then set to false
58 md->register_decl(p->get_decl(), m.mk_false());
59 return true;
60 }
61 return m.is_false(val);
62 }
63
processfm_tactic::fm_model_converter64 r_kind process(func_decl * x, expr * cls, arith_util & u, model& ev, rational & r) {
65 unsigned num_lits;
66 expr * const * lits;
67 if (m.is_or(cls)) {
68 num_lits = to_app(cls)->get_num_args();
69 lits = to_app(cls)->get_args();
70 }
71 else {
72 num_lits = 1;
73 lits = &cls;
74 }
75
76 bool is_lower = false;
77 bool found = false;
78 for (unsigned i = 0; i < num_lits; i++) {
79 expr * l = lits[i];
80 expr * atom;
81 if (is_uninterp_const(l) || (m.is_not(l, atom) && is_uninterp_const(atom))) {
82 if (ev.is_true(l))
83 return NONE; // clause was satisfied
84 }
85 else {
86 found = true;
87 bool neg = m.is_not(l, l);
88 SASSERT(u.is_le(l) || u.is_ge(l));
89 bool strict = neg;
90 rational a_val;
91 if (u.is_ge(l))
92 neg = !neg;
93 expr * lhs = to_app(l)->get_arg(0);
94 expr * rhs = to_app(l)->get_arg(1);
95 rational c;
96 if (!u.is_numeral(rhs, c))
97 return NONE;
98 if (neg)
99 c.neg();
100 unsigned num_mons;
101 expr * const * mons;
102 if (u.is_add(lhs)) {
103 num_mons = to_app(lhs)->get_num_args();
104 mons = to_app(lhs)->get_args();
105 }
106 else {
107 num_mons = 1;
108 mons = &lhs;
109 }
110 for (unsigned j = 0; j < num_mons; j++) {
111 expr * monomial = mons[j];
112 expr * ai;
113 expr * xi;
114 rational ai_val;
115 if (u.is_mul(monomial, ai, xi)) {
116 if (!u.is_numeral(ai, ai_val))
117 return NONE;
118 }
119 else {
120 xi = monomial;
121 ai_val = rational(1);
122 }
123 if (u.is_to_real(xi))
124 xi = to_app(xi)->get_arg(0);
125 if (!is_uninterp_const(xi))
126 return NONE;
127 if (x == to_app(xi)->get_decl()) {
128 a_val = ai_val;
129 if (neg)
130 a_val.neg();
131 }
132 else {
133 expr_ref val(m);
134 val = ev(monomial);
135 rational tmp;
136 if (!u.is_numeral(val, tmp))
137 return NONE;
138 if (neg)
139 tmp.neg();
140 c -= tmp;
141 }
142 }
143 if (u.is_int(x->get_range()) && strict) {
144 // a*x < c --> a*x <= c-1
145 SASSERT(c.is_int());
146 c--;
147 }
148 is_lower = a_val.is_neg();
149 c /= a_val;
150 if (u.is_int(x->get_range())) {
151 if (is_lower)
152 c = ceil(c);
153 else
154 c = floor(c);
155 }
156 r = c;
157 }
158 }
159 (void)found;
160 SASSERT(found);
161 return is_lower ? LOWER : UPPER;
162 }
163
164 public:
fm_model_converterfm_tactic::fm_model_converter165 fm_model_converter(ast_manager & _m):m(_m) {}
166
~fm_model_converterfm_tactic::fm_model_converter167 ~fm_model_converter() override {
168 m.dec_array_ref(m_xs.size(), m_xs.data());
169 for (auto& c : m_clauses)
170 m.dec_array_ref(c.size(), c.data());
171 }
172
insertfm_tactic::fm_model_converter173 void insert(func_decl * x, clauses & c) {
174 m.inc_ref(x);
175 m.inc_array_ref(c.size(), c.data());
176 m_xs.push_back(x);
177 m_clauses.push_back(clauses());
178 m_clauses.back().swap(c);
179 }
180
181
get_unitsfm_tactic::fm_model_converter182 void get_units(obj_map<expr, bool>& units) override { units.reset(); }
183
operator ()fm_tactic::fm_model_converter184 void operator()(model_ref & md) override {
185 TRACE("fm_mc", model_v2_pp(tout, *md); display(tout););
186 model::scoped_model_completion _sc(*md, true);
187 //model_evaluator ev(*(md.get()));
188 //ev.set_model_completion(true);
189 arith_util u(m);
190 unsigned i = m_xs.size();
191 while (i > 0) {
192 --i;
193 func_decl * x = m_xs[i];
194 rational lower;
195 rational upper;
196 rational val;
197 bool has_lower = false;
198 bool has_upper = false;
199 TRACE("fm_mc", tout << "processing " << x->get_name() << "\n";);
200 clauses::iterator it = m_clauses[i].begin();
201 clauses::iterator end = m_clauses[i].end();
202 for (; it != end; ++it) {
203 if (!m.inc())
204 throw tactic_exception(m.limit().get_cancel_msg());
205 switch (process(x, *it, u, *md, val)) {
206 case NONE:
207 TRACE("fm_mc", tout << "no bound for:\n" << mk_ismt2_pp(*it, m) << "\n";);
208 break;
209 case LOWER:
210 TRACE("fm_mc", tout << "lower bound: " << val << " for:\n" << mk_ismt2_pp(*it, m) << "\n";);
211 if (!has_lower || val > lower)
212 lower = val;
213 has_lower = true;
214 break;
215 case UPPER:
216 TRACE("fm_mc", tout << "upper bound: " << val << " for:\n" << mk_ismt2_pp(*it, m) << "\n";);
217 if (!has_upper || val < upper)
218 upper = val;
219 has_upper = true;
220 break;
221 }
222 }
223
224 expr * x_val;
225 if (u.is_int(x->get_range())) {
226 if (has_lower)
227 x_val = u.mk_numeral(lower, true);
228 else if (has_upper)
229 x_val = u.mk_numeral(upper, true);
230 else
231 x_val = u.mk_numeral(rational(0), true);
232 }
233 else {
234 if (has_lower && has_upper)
235 x_val = u.mk_numeral((upper + lower)/rational(2), false);
236 else if (has_lower)
237 x_val = u.mk_numeral(lower + rational(1), false);
238 else if (has_upper)
239 x_val = u.mk_numeral(upper - rational(1), false);
240 else
241 x_val = u.mk_numeral(rational(0), false);
242 }
243 TRACE("fm_mc", tout << x->get_name() << " --> " << mk_ismt2_pp(x_val, m) << "\n";);
244 md->register_decl(x, x_val);
245 }
246 TRACE("fm_mc", model_v2_pp(tout, *md););
247 }
248
249
displayfm_tactic::fm_model_converter250 void display(std::ostream & out) override {
251 out << "(fm-model-converter";
252 SASSERT(m_xs.size() == m_clauses.size());
253 unsigned sz = m_xs.size();
254 for (unsigned i = 0; i < sz; i++) {
255 out << "\n(" << m_xs[i]->get_name();
256 clauses const & cs = m_clauses[i];
257 for (auto& c : cs)
258 out << "\n " << mk_ismt2_pp(c, m, 2);
259 out << ")";
260 }
261 out << ")\n";
262 }
263
translatefm_tactic::fm_model_converter264 model_converter * translate(ast_translation & translator) override {
265 ast_manager & to_m = translator.to();
266 fm_model_converter * res = alloc(fm_model_converter, to_m);
267 unsigned sz = m_xs.size();
268 for (unsigned i = 0; i < sz; i++) {
269 func_decl * new_x = translator(m_xs[i]);
270 to_m.inc_ref(new_x);
271 res->m_xs.push_back(new_x);
272
273 clauses const & cs = m_clauses[i];
274 res->m_clauses.push_back(clauses());
275 clauses & new_cs = res->m_clauses.back();
276 for (auto& c : cs) {
277 app * new_c = translator(c);
278 to_m.inc_ref(new_c);
279 new_cs.push_back(new_c);
280 }
281 }
282 return res;
283 }
284 };
285
286 // Encode the constraint
287 // lits \/ ( as[0]*xs[0] + ... + as[num_vars-1]*xs[num_vars-1] <= c
288 // if strict is true, then <= is <.
289 struct constraint {
get_obj_sizefm_tactic::constraint290 static unsigned get_obj_size(unsigned num_lits, unsigned num_vars) {
291 return sizeof(constraint) + num_lits*sizeof(literal) + num_vars*(sizeof(var) + sizeof(rational));
292 }
293 unsigned m_id;
294 unsigned m_num_lits:29;
295 unsigned m_strict:1;
296 unsigned m_dead:1;
297 unsigned m_mark:1;
298 unsigned m_num_vars;
299 literal * m_lits;
300 var * m_xs;
301 rational * m_as;
302 rational m_c;
303 expr_dependency * m_dep;
~constraintfm_tactic::constraint304 ~constraint() {
305 rational * it = m_as;
306 rational * end = it + m_num_vars;
307 for (; it != end; ++it)
308 it->~rational();
309 }
310
hashfm_tactic::constraint311 unsigned hash() const { return hash_u(m_id); }
312 };
313
314 typedef ptr_vector<constraint> constraints;
315
316 class constraint_set {
317 unsigned_vector m_id2pos;
318 constraints m_set;
319 public:
320 typedef constraints::const_iterator iterator;
321
contains(constraint const & c) const322 bool contains(constraint const & c) const {
323 if (c.m_id >= m_id2pos.size())
324 return false;
325 return m_id2pos[c.m_id] != UINT_MAX;
326 }
327
empty() const328 bool empty() const { return m_set.empty(); }
size() const329 unsigned size() const { return m_set.size(); }
330
insert(constraint & c)331 void insert(constraint & c) {
332 unsigned id = c.m_id;
333 m_id2pos.reserve(id+1, UINT_MAX);
334 if (m_id2pos[id] != UINT_MAX)
335 return; // already in the set
336 unsigned pos = m_set.size();
337 m_id2pos[id] = pos;
338 m_set.push_back(&c);
339 }
340
erase(constraint & c)341 void erase(constraint & c) {
342 unsigned id = c.m_id;
343 if (id >= m_id2pos.size())
344 return;
345 unsigned pos = m_id2pos[id];
346 if (pos == UINT_MAX)
347 return;
348 m_id2pos[id] = UINT_MAX;
349 unsigned last_pos = m_set.size() - 1;
350 if (pos != last_pos) {
351 constraint * last_c = m_set[last_pos];
352 m_set[pos] = last_c;
353 m_id2pos[last_c->m_id] = pos;
354 }
355 m_set.pop_back();
356 }
357
erase()358 constraint & erase() {
359 SASSERT(!empty());
360 constraint & c = *m_set.back();
361 m_id2pos[c.m_id] = UINT_MAX;
362 m_set.pop_back();
363 return c;
364 }
365
reset()366 void reset() { m_id2pos.reset(); m_set.reset(); }
finalize()367 void finalize() { m_id2pos.finalize(); m_set.finalize(); }
368
begin() const369 iterator begin() const { return m_set.begin(); }
end() const370 iterator end() const { return m_set.end(); }
371 };
372
373 struct imp {
374 ast_manager & m;
375 small_object_allocator m_allocator;
376 arith_util m_util;
377 constraints m_constraints;
378 expr_ref_vector m_bvar2expr;
379 signed_char_vector m_bvar2sign;
380 obj_map<expr, bvar> m_expr2bvar;
381 char_vector m_is_int;
382 char_vector m_forbidden;
383 expr_ref_vector m_var2expr;
384 obj_map<expr, var> m_expr2var;
385 unsigned_vector m_var2pos;
386 vector<constraints> m_lowers;
387 vector<constraints> m_uppers;
388 obj_hashtable<func_decl> m_forbidden_set; // variables that cannot be eliminated because occur in non OCC ineq part
389 goal_ref m_new_goal;
390 ref<fm_model_converter> m_mc;
391 id_gen m_id_gen;
392 bool m_produce_models;
393 bool m_fm_real_only;
394 unsigned m_fm_limit;
395 unsigned m_fm_cutoff1;
396 unsigned m_fm_cutoff2;
397 unsigned m_fm_extra;
398 bool m_fm_occ;
399 unsigned long long m_max_memory;
400 unsigned m_counter;
401 bool m_inconsistent;
402 expr_dependency_ref m_inconsistent_core;
403 constraint_set m_sub_todo;
404
405 // ---------------------------
406 //
407 // OCC clause recognizer
408 //
409 // ---------------------------
410
is_literalfm_tactic::imp411 bool is_literal(expr * t) const {
412 expr * atom;
413 return is_uninterp_const(t) || (m.is_not(t, atom) && is_uninterp_const(atom));
414 }
415
is_constraintfm_tactic::imp416 bool is_constraint(expr * t) const {
417 return !is_literal(t);
418 }
419
is_varfm_tactic::imp420 bool is_var(expr * t, expr * & x) const {
421 if (is_uninterp_const(t)) {
422 x = t;
423 return true;
424 }
425 else if (m_util.is_to_real(t) && is_uninterp_const(to_app(t)->get_arg(0))) {
426 x = to_app(t)->get_arg(0);
427 return true;
428 }
429 return false;
430 }
431
is_varfm_tactic::imp432 bool is_var(expr * t) const {
433 expr * x;
434 return is_var(t, x);
435 }
436
is_linear_mon_corefm_tactic::imp437 bool is_linear_mon_core(expr * t, expr * & x) const {
438 expr * c;
439 if (m_util.is_mul(t, c, x) && m_util.is_numeral(c) && is_var(x, x))
440 return true;
441 return is_var(t, x);
442 }
443
is_linear_monfm_tactic::imp444 bool is_linear_mon(expr * t) const {
445 expr * x;
446 return is_linear_mon_core(t, x);
447 }
448
is_linear_polfm_tactic::imp449 bool is_linear_pol(expr * t) const {
450 unsigned num_mons;
451 expr * const * mons;
452 if (m_util.is_add(t)) {
453 num_mons = to_app(t)->get_num_args();
454 mons = to_app(t)->get_args();
455 }
456 else {
457 num_mons = 1;
458 mons = &t;
459 }
460
461 expr_fast_mark2 visited;
462 bool all_forbidden = true;
463 for (unsigned i = 0; i < num_mons; i++) {
464 expr * x;
465 if (!is_linear_mon_core(mons[i], x))
466 return false;
467 if (visited.is_marked(x))
468 return false; // duplicates are not supported... must simplify first
469 visited.mark(x);
470 if (!m_forbidden_set.contains(to_app(x)->get_decl()) && (!m_fm_real_only || !m_util.is_int(x)))
471 all_forbidden = false;
472 }
473 return !all_forbidden;
474 }
475
is_linear_ineqfm_tactic::imp476 bool is_linear_ineq(expr * t) const {
477 m.is_not(t, t);
478 expr * lhs, * rhs;
479 TRACE("is_occ_bug", tout << mk_pp(t, m) << "\n";);
480 if (m_util.is_le(t, lhs, rhs) || m_util.is_ge(t, lhs, rhs)) {
481 if (!m_util.is_numeral(rhs))
482 return false;
483 return is_linear_pol(lhs);
484 }
485 return false;
486 }
487
is_occfm_tactic::imp488 bool is_occ(expr * t) {
489 if (m_fm_occ && m.is_or(t)) {
490 unsigned num = to_app(t)->get_num_args();
491 bool found = false;
492 for (unsigned i = 0; i < num; i++) {
493 expr * l = to_app(t)->get_arg(i);
494 if (is_literal(l)) {
495 continue;
496 }
497 else if (is_linear_ineq(l)) {
498 if (found)
499 return false;
500 found = true;
501 }
502 else {
503 return false;
504 }
505 }
506 return found;
507 }
508 return is_linear_ineq(t);
509 }
510
511 // ---------------------------
512 //
513 // Memory mng
514 //
515 // ---------------------------
del_constraintfm_tactic::imp516 void del_constraint(constraint * c) {
517 m.dec_ref(c->m_dep);
518 m_sub_todo.erase(*c);
519 m_id_gen.recycle(c->m_id);
520 c->~constraint();
521 unsigned sz = constraint::get_obj_size(c->m_num_lits, c->m_num_vars);
522 m_allocator.deallocate(sz, c);
523 }
524
del_constraintsfm_tactic::imp525 void del_constraints(unsigned sz, constraint * const * cs) {
526 for (unsigned i = 0; i < sz; i++)
527 del_constraint(cs[i]);
528 }
529
reset_constraintsfm_tactic::imp530 void reset_constraints() {
531 del_constraints(m_constraints.size(), m_constraints.data());
532 m_constraints.reset();
533 }
534
mk_constraintfm_tactic::imp535 constraint * mk_constraint(unsigned num_lits, literal * lits, unsigned num_vars, var * xs, rational * as, rational & c, bool strict,
536 expr_dependency * dep) {
537 unsigned sz = constraint::get_obj_size(num_lits, num_vars);
538 char * mem = static_cast<char*>(m_allocator.allocate(sz));
539 char * mem_as = mem + sizeof(constraint);
540 char * mem_lits = mem_as + sizeof(rational)*num_vars;
541 char * mem_xs = mem_lits + sizeof(literal)*num_lits;
542 constraint * cnstr = new (mem) constraint();
543 cnstr->m_id = m_id_gen.mk();
544 cnstr->m_num_lits = num_lits;
545 cnstr->m_dead = false;
546 cnstr->m_mark = false;
547 cnstr->m_strict = strict;
548 cnstr->m_num_vars = num_vars;
549 cnstr->m_lits = reinterpret_cast<literal*>(mem_lits);
550 for (unsigned i = 0; i < num_lits; i++)
551 cnstr->m_lits[i] = lits[i];
552 cnstr->m_xs = reinterpret_cast<var*>(mem_xs);
553 cnstr->m_as = reinterpret_cast<rational*>(mem_as);
554 for (unsigned i = 0; i < num_vars; i++) {
555 TRACE("mk_constraint_bug", tout << "xs[" << i << "]: " << xs[i] << "\n";);
556 cnstr->m_xs[i] = xs[i];
557 new (cnstr->m_as + i) rational(as[i]);
558 }
559 cnstr->m_c = c;
560 DEBUG_CODE({
561 for (unsigned i = 0; i < num_vars; i++) {
562 SASSERT(cnstr->m_xs[i] == xs[i]);
563 SASSERT(cnstr->m_as[i] == as[i]);
564 }
565 });
566 cnstr->m_dep = dep;
567 m.inc_ref(dep);
568 return cnstr;
569 }
570
571 // ---------------------------
572 //
573 // Util
574 //
575 // ---------------------------
576
num_varsfm_tactic::imp577 unsigned num_vars() const { return m_is_int.size(); }
578
579 // multiply as and c, by the lcm of their denominators
mk_intfm_tactic::imp580 void mk_int(unsigned num, rational * as, rational & c) {
581 rational l = denominator(c);
582 for (unsigned i = 0; i < num; i++)
583 l = lcm(l, denominator(as[i]));
584 if (l.is_one())
585 return;
586 c *= l;
587 SASSERT(c.is_int());
588 for (unsigned i = 0; i < num; i++) {
589 as[i] *= l;
590 SASSERT(as[i].is_int());
591 }
592 }
593
normalize_coeffsfm_tactic::imp594 void normalize_coeffs(constraint & c) {
595 if (c.m_num_vars == 0)
596 return;
597 // compute gcd of all coefficients
598 rational g = c.m_c;
599 if (g.is_neg())
600 g.neg();
601 for (unsigned i = 0; i < c.m_num_vars; i++) {
602 if (g.is_one())
603 break;
604 if (c.m_as[i].is_pos())
605 g = gcd(c.m_as[i], g);
606 else
607 g = gcd(-c.m_as[i], g);
608 }
609 if (g.is_one())
610 return;
611 c.m_c /= g;
612 for (unsigned i = 0; i < c.m_num_vars; i++)
613 c.m_as[i] /= g;
614 }
615
displayfm_tactic::imp616 void display(std::ostream & out, constraint const & c) const {
617 for (unsigned i = 0; i < c.m_num_lits; i++) {
618 literal l = c.m_lits[i];
619 if (sign(l))
620 out << "~";
621 bvar p = lit2bvar(l);
622 out << mk_ismt2_pp(m_bvar2expr[p], m);
623 out << " ";
624 }
625 out << "(";
626 if (c.m_num_vars == 0)
627 out << "0";
628 for (unsigned i = 0; i < c.m_num_vars; i++) {
629 if (i > 0)
630 out << " + ";
631 if (!c.m_as[i].is_one())
632 out << c.m_as[i] << "*";
633 out << mk_ismt2_pp(m_var2expr.get(c.m_xs[i]), m);
634 }
635 if (c.m_strict)
636 out << " < ";
637 else
638 out << " <= ";
639 out << c.m_c;
640 out << ")";
641 }
642
643 /**
644 \brief Return true if c1 subsumes c2
645
646 c1 subsumes c2 If
647 1) All literals of c1 are literals of c2
648 2) polynomial of c1 == polynomial of c2
649 3) c1.m_c <= c2.m_c
650 */
subsumesfm_tactic::imp651 bool subsumes(constraint const & c1, constraint const & c2) {
652 if (&c1 == &c2)
653 return false;
654 // quick checks first
655 if (c1.m_num_lits > c2.m_num_lits)
656 return false;
657 if (c1.m_num_vars != c2.m_num_vars)
658 return false;
659 if (c1.m_c > c2.m_c)
660 return false;
661 if (!c1.m_strict && c2.m_strict && c1.m_c == c2.m_c)
662 return false;
663
664 m_counter += c1.m_num_lits + c2.m_num_lits;
665
666 for (unsigned i = 0; i < c1.m_num_vars; i++) {
667 m_var2pos[c1.m_xs[i]] = i;
668 }
669
670 bool failed = false;
671 for (unsigned i = 0; i < c2.m_num_vars; i++) {
672 unsigned pos1 = m_var2pos[c2.m_xs[i]];
673 if (pos1 == UINT_MAX || c1.m_as[pos1] != c2.m_as[i]) {
674 failed = true;
675 break;
676 }
677 }
678
679 for (unsigned i = 0; i < c1.m_num_vars; i++) {
680 m_var2pos[c1.m_xs[i]] = UINT_MAX;
681 }
682
683 if (failed)
684 return false;
685
686 for (unsigned i = 0; i < c2.m_num_lits; i++) {
687 literal l = c2.m_lits[i];
688 bvar b = lit2bvar(l);
689 SASSERT(m_bvar2sign[b] == 0);
690 m_bvar2sign[b] = sign(l) ? -1 : 1;
691 }
692
693 for (unsigned i = 0; i < c1.m_num_lits; i++) {
694 literal l = c1.m_lits[i];
695 bvar b = lit2bvar(l);
696 char s = sign(l) ? -1 : 1;
697 if (m_bvar2sign[b] != s) {
698 failed = true;
699 break;
700 }
701 }
702
703 for (unsigned i = 0; i < c2.m_num_lits; i++) {
704 literal l = c2.m_lits[i];
705 bvar b = lit2bvar(l);
706 m_bvar2sign[b] = 0;
707 }
708
709 if (failed)
710 return false;
711
712 return true;
713 }
714
backward_subsumptionfm_tactic::imp715 void backward_subsumption(constraint const & c) {
716 if (c.m_num_vars == 0)
717 return;
718 var best = UINT_MAX;
719 unsigned best_sz = UINT_MAX;
720 bool best_lower = false;
721 for (unsigned i = 0; i < c.m_num_vars; i++) {
722 var xi = c.m_xs[i];
723 if (is_forbidden(xi))
724 continue; // variable is not in the index
725 bool neg_a = c.m_as[i].is_neg();
726 constraints & cs = neg_a ? m_lowers[xi] : m_uppers[xi];
727 if (cs.size() < best_sz) {
728 best = xi;
729 best_sz = cs.size();
730 best_lower = neg_a;
731 }
732 }
733 if (best_sz == 0)
734 return;
735 if (best == UINT_MAX)
736 return; // none of the c variables are in the index.
737 constraints & cs = best_lower ? m_lowers[best] : m_uppers[best];
738 m_counter += cs.size();
739 constraints::iterator it = cs.begin();
740 constraints::iterator it2 = it;
741 constraints::iterator end = cs.end();
742 for (; it != end; ++it) {
743 constraint * c2 = *it;
744 if (c2->m_dead)
745 continue;
746 if (subsumes(c, *c2)) {
747 TRACE("fm_subsumption", display(tout, c); tout << "\nsubsumed:\n"; display(tout, *c2); tout << "\n";);
748 c2->m_dead = true;
749 continue;
750 }
751 *it2 = *it;
752 ++it2;
753 }
754 cs.set_end(it2);
755 }
756
subsumefm_tactic::imp757 void subsume() {
758 while (!m_sub_todo.empty()) {
759 constraint & c = m_sub_todo.erase();
760 if (c.m_dead)
761 continue;
762 backward_subsumption(c);
763 }
764 }
765
766 // ---------------------------
767 //
768 // Initialization
769 //
770 // ---------------------------
771
impfm_tactic::imp772 imp(ast_manager & _m, params_ref const & p):
773 m(_m),
774 m_allocator("fm-tactic"),
775 m_util(m),
776 m_bvar2expr(m),
777 m_var2expr(m),
778 m_inconsistent_core(m) {
779 updt_params(p);
780 }
781
~impfm_tactic::imp782 ~imp() {
783 reset_constraints();
784 }
785
updt_paramsfm_tactic::imp786 void updt_params(params_ref const & p) {
787 m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
788 m_fm_real_only = p.get_bool("fm_real_only", true);
789 m_fm_limit = p.get_uint("fm_limit", 5000000);
790 m_fm_cutoff1 = p.get_uint("fm_cutoff1", 8);
791 m_fm_cutoff2 = p.get_uint("fm_cutoff2", 256);
792 m_fm_extra = p.get_uint("fm_extra", 0);
793 m_fm_occ = p.get_bool("fm_occ", false);
794 }
795
796
797 struct forbidden_proc {
798 imp & m_owner;
forbidden_procfm_tactic::imp::forbidden_proc799 forbidden_proc(imp & o):m_owner(o) {}
operator ()fm_tactic::imp::forbidden_proc800 void operator()(::var * n) {}
operator ()fm_tactic::imp::forbidden_proc801 void operator()(app * n) {
802 if (is_uninterp_const(n) && n->get_sort()->get_family_id() == m_owner.m_util.get_family_id()) {
803 m_owner.m_forbidden_set.insert(n->get_decl());
804 }
805 }
operator ()fm_tactic::imp::forbidden_proc806 void operator()(quantifier * n) {}
807 };
808
init_forbidden_setfm_tactic::imp809 void init_forbidden_set(goal const & g) {
810 m_forbidden_set.reset();
811 expr_fast_mark1 visited;
812 forbidden_proc proc(*this);
813 unsigned sz = g.size();
814 for (unsigned i = 0; i < sz; i++) {
815 expr * f = g.form(i);
816 if (is_occ(f))
817 continue;
818 TRACE("is_occ_bug", tout << "not OCC:\n" << mk_ismt2_pp(f, m) << "\n";);
819 quick_for_each_expr(proc, visited, f);
820 }
821 }
822
initfm_tactic::imp823 void init(goal const & g) {
824 m_sub_todo.reset();
825 m_id_gen.reset();
826 reset_constraints();
827 m_bvar2expr.reset();
828 m_bvar2sign.reset();
829 m_bvar2expr.push_back(nullptr); // bvar 0 is not used
830 m_bvar2sign.push_back(0);
831 m_expr2var.reset();
832 m_is_int.reset();
833 m_var2pos.reset();
834 m_forbidden.reset();
835 m_var2expr.reset();
836 m_expr2var.reset();
837 m_lowers.reset();
838 m_uppers.reset();
839 m_new_goal = nullptr;
840 m_mc = nullptr;
841 m_counter = 0;
842 m_inconsistent = false;
843 m_inconsistent_core = nullptr;
844 init_forbidden_set(g);
845 }
846
847 // ---------------------------
848 //
849 // Internal data-structures
850 //
851 // ---------------------------
852
signfm_tactic::imp853 static bool sign(literal l) { return l < 0; }
lit2bvarfm_tactic::imp854 static bvar lit2bvar(literal l) { return l < 0 ? -l : l; }
855
is_intfm_tactic::imp856 bool is_int(var x) const {
857 return m_is_int[x] != 0;
858 }
859
is_forbiddenfm_tactic::imp860 bool is_forbidden(var x) const {
861 return m_forbidden[x] != 0;
862 }
863
all_intfm_tactic::imp864 bool all_int(constraint const & c) const {
865 for (unsigned i = 0; i < c.m_num_vars; i++) {
866 if (!is_int(c.m_xs[i]))
867 return false;
868 }
869 return true;
870 }
871
to_exprfm_tactic::imp872 app * to_expr(constraint const & c) {
873 expr * ineq;
874 if (c.m_num_vars == 0) {
875 // 0 < k (for k > 0) --> true
876 // 0 <= 0 -- > true
877 if (c.m_c.is_pos() || (!c.m_strict && c.m_c.is_zero()))
878 return m.mk_true();
879 ineq = nullptr;
880 }
881 else {
882 bool int_cnstr = all_int(c);
883 ptr_buffer<expr> ms;
884 for (unsigned i = 0; i < c.m_num_vars; i++) {
885 expr * x = m_var2expr.get(c.m_xs[i]);
886 if (!int_cnstr && is_int(c.m_xs[i]))
887 x = m_util.mk_to_real(x);
888 if (c.m_as[i].is_one())
889 ms.push_back(x);
890 else
891 ms.push_back(m_util.mk_mul(m_util.mk_numeral(c.m_as[i], int_cnstr), x));
892 }
893 expr * lhs;
894 if (c.m_num_vars == 1)
895 lhs = ms[0];
896 else
897 lhs = m_util.mk_add(ms.size(), ms.data());
898 expr * rhs = m_util.mk_numeral(c.m_c, int_cnstr);
899 if (c.m_strict) {
900 ineq = m.mk_not(m_util.mk_ge(lhs, rhs));
901 }
902 else {
903 ineq = m_util.mk_le(lhs, rhs);
904 }
905 }
906
907 if (c.m_num_lits == 0) {
908 if (ineq)
909 return to_app(ineq);
910 else
911 return m.mk_false();
912 }
913
914 ptr_buffer<expr> lits;
915 for (unsigned i = 0; i < c.m_num_lits; i++) {
916 literal l = c.m_lits[i];
917 if (sign(l))
918 lits.push_back(m.mk_not(m_bvar2expr.get(lit2bvar(l))));
919 else
920 lits.push_back(m_bvar2expr.get(lit2bvar(l)));
921 }
922 if (ineq)
923 lits.push_back(ineq);
924 if (lits.size() == 1)
925 return to_app(lits[0]);
926 else
927 return m.mk_or(lits.size(), lits.data());
928 }
929
mk_varfm_tactic::imp930 var mk_var(expr * t) {
931 SASSERT(is_uninterp_const(t));
932 SASSERT(m_util.is_int(t) || m_util.is_real(t));
933 var x = m_var2expr.size();
934 m_var2expr.push_back(t);
935 bool is_int = m_util.is_int(t);
936 m_is_int.push_back(is_int);
937 m_var2pos.push_back(UINT_MAX);
938 m_expr2var.insert(t, x);
939 m_lowers.push_back(constraints());
940 m_uppers.push_back(constraints());
941 bool forbidden = m_forbidden_set.contains(to_app(t)->get_decl()) || (m_fm_real_only && is_int);
942 m_forbidden.push_back(forbidden);
943 SASSERT(m_var2expr.size() == m_is_int.size());
944 SASSERT(m_lowers.size() == m_is_int.size());
945 SASSERT(m_uppers.size() == m_is_int.size());
946 SASSERT(m_forbidden.size() == m_is_int.size());
947 SASSERT(m_var2pos.size() == m_is_int.size());
948 return x;
949 }
950
mk_bvarfm_tactic::imp951 bvar mk_bvar(expr * t) {
952 SASSERT(is_uninterp_const(t));
953 SASSERT(m.is_bool(t));
954 bvar p = m_bvar2expr.size();
955 m_bvar2expr.push_back(t);
956 m_bvar2sign.push_back(0);
957 SASSERT(m_bvar2expr.size() == m_bvar2sign.size());
958 m_expr2bvar.insert(t, p);
959 SASSERT(p > 0);
960 return p;
961 }
962
to_varfm_tactic::imp963 var to_var(expr * t) {
964 var x;
965 if (!m_expr2var.find(t, x))
966 x = mk_var(t);
967 SASSERT(m_expr2var.contains(t));
968 SASSERT(m_var2expr.get(x) == t);
969 TRACE("to_var_bug", tout << mk_ismt2_pp(t, m) << " --> " << x << "\n";);
970 return x;
971 }
972
to_bvarfm_tactic::imp973 bvar to_bvar(expr * t) {
974 bvar p;
975 if (m_expr2bvar.find(t, p))
976 return p;
977 return mk_bvar(t);
978 }
979
to_literalfm_tactic::imp980 literal to_literal(expr * t) {
981 if (m.is_not(t, t))
982 return -to_bvar(t);
983 else
984 return to_bvar(t);
985 }
986
987
add_constraintfm_tactic::imp988 void add_constraint(expr * f, expr_dependency * dep) {
989 SASSERT(!m.is_or(f) || m_fm_occ);
990 sbuffer<literal> lits;
991 sbuffer<var> xs;
992 buffer<rational> as;
993 rational c;
994 bool strict = false;
995 unsigned num;
996 expr * const * args;
997 if (m.is_or(f)) {
998 num = to_app(f)->get_num_args();
999 args = to_app(f)->get_args();
1000 }
1001 else {
1002 num = 1;
1003 args = &f;
1004 }
1005
1006 #if Z3DEBUG
1007 bool found_ineq = false;
1008 #endif
1009 for (unsigned i = 0; i < num; i++) {
1010 expr * l = args[i];
1011 if (is_literal(l)) {
1012 lits.push_back(to_literal(l));
1013 }
1014 else {
1015 // found inequality
1016 SASSERT(!found_ineq);
1017 DEBUG_CODE(found_ineq = true;);
1018 bool neg = m.is_not(l, l);
1019 SASSERT(m_util.is_le(l) || m_util.is_ge(l));
1020 strict = neg;
1021 if (m_util.is_ge(l))
1022 neg = !neg;
1023 expr * lhs = to_app(l)->get_arg(0);
1024 expr * rhs = to_app(l)->get_arg(1);
1025 m_util.is_numeral(rhs, c);
1026 if (neg)
1027 c.neg();
1028 unsigned num_mons;
1029 expr * const * mons;
1030 if (m_util.is_add(lhs)) {
1031 num_mons = to_app(lhs)->get_num_args();
1032 mons = to_app(lhs)->get_args();
1033 }
1034 else {
1035 num_mons = 1;
1036 mons = &lhs;
1037 }
1038
1039 bool all_int = true;
1040 for (unsigned j = 0; j < num_mons; j++) {
1041 expr * monomial = mons[j];
1042 expr * a;
1043 rational a_val;
1044 expr * x;
1045 if (m_util.is_mul(monomial, a, x)) {
1046 VERIFY(m_util.is_numeral(a, a_val));
1047 }
1048 else {
1049 x = monomial;
1050 a_val = rational(1);
1051 }
1052 if (neg)
1053 a_val.neg();
1054 VERIFY(is_var(x, x));
1055 xs.push_back(to_var(x));
1056 as.push_back(a_val);
1057 if (!is_int(xs.back()))
1058 all_int = false;
1059 }
1060 mk_int(as.size(), as.data(), c);
1061 if (all_int && strict) {
1062 strict = false;
1063 c--;
1064 }
1065 }
1066 }
1067
1068 TRACE("to_var_bug", tout << "before mk_constraint: "; for (unsigned i = 0; i < xs.size(); i++) tout << " " << xs[i]; tout << "\n";);
1069
1070 constraint * new_c = mk_constraint(lits.size(),
1071 lits.data(),
1072 xs.size(),
1073 xs.data(),
1074 as.data(),
1075 c,
1076 strict,
1077 dep);
1078
1079 TRACE("to_var_bug", tout << "add_constraint: "; display(tout, *new_c); tout << "\n";);
1080 VERIFY(register_constraint(new_c));
1081 }
1082
is_falsefm_tactic::imp1083 bool is_false(constraint const & c) const {
1084 return c.m_num_lits == 0 && c.m_num_vars == 0 && (c.m_c.is_neg() || (c.m_strict && c.m_c.is_zero()));
1085 }
1086
register_constraintfm_tactic::imp1087 bool register_constraint(constraint * c) {
1088 normalize_coeffs(*c);
1089 if (is_false(*c)) {
1090 del_constraint(c);
1091 m_inconsistent = true;
1092 TRACE("add_constraint_bug", tout << "is false "; display(tout, *c); tout << "\n";);
1093 return false;
1094 }
1095
1096 bool r = false;
1097
1098 for (unsigned i = 0; i < c->m_num_vars; i++) {
1099 var x = c->m_xs[i];
1100 if (!is_forbidden(x)) {
1101 r = true;
1102 if (c->m_as[i].is_neg())
1103 m_lowers[x].push_back(c);
1104 else
1105 m_uppers[x].push_back(c);
1106 }
1107 }
1108
1109 if (r) {
1110 m_sub_todo.insert(*c);
1111 m_constraints.push_back(c);
1112 return true;
1113 }
1114 else {
1115 TRACE("add_constraint_bug", tout << "all variables are forbidden "; display(tout, *c); tout << "\n";);
1116 m_new_goal->assert_expr(to_expr(*c), nullptr, c->m_dep);
1117 del_constraint(c);
1118 return false;
1119 }
1120 }
1121
init_use_listfm_tactic::imp1122 void init_use_list(goal const & g) {
1123 unsigned sz = g.size();
1124 for (unsigned i = 0; i < sz; i++) {
1125 if (m_inconsistent)
1126 return;
1127 expr * f = g.form(i);
1128 if (is_occ(f))
1129 add_constraint(f, g.dep(i));
1130 else
1131 m_new_goal->assert_expr(f, nullptr, g.dep(i));
1132 }
1133 }
1134
get_costfm_tactic::imp1135 unsigned get_cost(var x) const {
1136 unsigned long long r = static_cast<unsigned long long>(m_lowers[x].size()) * static_cast<unsigned long long>(m_uppers[x].size());
1137 if (r > UINT_MAX)
1138 return UINT_MAX;
1139 return static_cast<unsigned>(r);
1140 }
1141
1142 typedef std::pair<var, unsigned> x_cost;
1143
1144 struct x_cost_lt {
1145 char_vector const m_is_int;
x_cost_ltfm_tactic::imp::x_cost_lt1146 x_cost_lt(char_vector & is_int):m_is_int(is_int) {}
operator ()fm_tactic::imp::x_cost_lt1147 bool operator()(x_cost const & p1, x_cost const & p2) const {
1148 // Integer variables with cost 0 can be eliminated even if they depend on real variables.
1149 // Cost 0 == no lower or no upper bound.
1150 if (p1.second == 0) {
1151 if (p2.second > 0) return true;
1152 return p1.first < p2.first;
1153 }
1154 if (p2.second == 0) return false;
1155 bool int1 = m_is_int[p1.first] != 0;
1156 bool int2 = m_is_int[p2.first] != 0;
1157 return (!int1 && int2) || (int1 == int2 && p1.second < p2.second);
1158 }
1159 };
1160
sort_candidatesfm_tactic::imp1161 void sort_candidates(var_vector & xs) {
1162 svector<x_cost> x_cost_vector;
1163 unsigned num = num_vars();
1164 for (var x = 0; x < num; x++) {
1165 if (!is_forbidden(x)) {
1166 x_cost_vector.push_back(x_cost(x, get_cost(x)));
1167 }
1168 }
1169 // x_cost_lt is not a total order on variables
1170 std::stable_sort(x_cost_vector.begin(), x_cost_vector.end(), x_cost_lt(m_is_int));
1171 TRACE("fm",
1172 svector<x_cost>::iterator it2 = x_cost_vector.begin();
1173 svector<x_cost>::iterator end2 = x_cost_vector.end();
1174 for (; it2 != end2; ++it2) {
1175 tout << "(" << mk_ismt2_pp(m_var2expr.get(it2->first), m) << " " << it2->second << ") ";
1176 }
1177 tout << "\n";);
1178 svector<x_cost>::iterator it2 = x_cost_vector.begin();
1179 svector<x_cost>::iterator end2 = x_cost_vector.end();
1180 for (; it2 != end2; ++it2) {
1181 xs.push_back(it2->first);
1182 }
1183 }
1184
cleanup_constraintsfm_tactic::imp1185 void cleanup_constraints(constraints & cs) {
1186 unsigned j = 0;
1187 unsigned sz = cs.size();
1188 for (unsigned i = 0; i < sz; i++) {
1189 constraint * c = cs[i];
1190 if (c->m_dead)
1191 continue;
1192 cs[j] = c;
1193 j++;
1194 }
1195 cs.shrink(j);
1196 }
1197
1198 // Set all_int = true if all variables in c are int.
1199 // Set unit_coeff = true if the coefficient of x in c is 1 or -1.
1200 // If all_int = false, then unit_coeff may not be set.
analyzefm_tactic::imp1201 void analyze(constraint const & c, var x, bool & all_int, bool & unit_coeff) const {
1202 all_int = true;
1203 unit_coeff = true;
1204 for (unsigned i = 0; i < c.m_num_vars; i++) {
1205 if (!is_int(c.m_xs[i])) {
1206 all_int = false;
1207 return;
1208 }
1209 if (c.m_xs[i] == x) {
1210 unit_coeff = (c.m_as[i].is_one() || c.m_as[i].is_minus_one());
1211 }
1212 }
1213 }
1214
analyzefm_tactic::imp1215 void analyze(constraints const & cs, var x, bool & all_int, bool & unit_coeff) const {
1216 all_int = true;
1217 unit_coeff = true;
1218 constraints::const_iterator it = cs.begin();
1219 constraints::const_iterator end = cs.end();
1220 for (; it != end; ++it) {
1221 bool curr_unit_coeff;
1222 analyze(*(*it), x, all_int, curr_unit_coeff);
1223 if (!all_int)
1224 return;
1225 if (!curr_unit_coeff)
1226 unit_coeff = false;
1227 }
1228 }
1229
1230 // An integer variable x may be eliminated, if
1231 // 1- All variables in the constraints it occur are integer.
1232 // 2- The coefficient of x in all lower bounds (or all upper bounds) is unit.
can_eliminatefm_tactic::imp1233 bool can_eliminate(var x) const {
1234 if (!is_int(x))
1235 return true;
1236 bool all_int;
1237 bool l_unit, u_unit;
1238 analyze(m_lowers[x], x, all_int, l_unit);
1239 if (!all_int)
1240 return false;
1241 analyze(m_uppers[x], x, all_int, u_unit);
1242 return all_int && (l_unit || u_unit);
1243 }
1244
copy_constraintsfm_tactic::imp1245 void copy_constraints(constraints const & s, clauses & t) {
1246 constraints::const_iterator it = s.begin();
1247 constraints::const_iterator end = s.end();
1248 for (; it != end; ++it) {
1249 app * c = to_expr(*(*it));
1250 t.push_back(c);
1251 }
1252 }
1253
1254 clauses tmp_clauses;
save_constraintsfm_tactic::imp1255 void save_constraints(var x) {
1256 if (m_produce_models) {
1257 tmp_clauses.reset();
1258 copy_constraints(m_lowers[x], tmp_clauses);
1259 copy_constraints(m_uppers[x], tmp_clauses);
1260 m_mc->insert(to_app(m_var2expr.get(x))->get_decl(), tmp_clauses);
1261 }
1262 }
1263
mark_constraints_deadfm_tactic::imp1264 void mark_constraints_dead(constraints const & cs) {
1265 constraints::const_iterator it = cs.begin();
1266 constraints::const_iterator end = cs.end();
1267 for (; it != end; ++it)
1268 (*it)->m_dead = true;
1269 }
1270
mark_constraints_deadfm_tactic::imp1271 void mark_constraints_dead(var x) {
1272 save_constraints(x);
1273 mark_constraints_dead(m_lowers[x]);
1274 mark_constraints_dead(m_uppers[x]);
1275 }
1276
get_coefffm_tactic::imp1277 void get_coeff(constraint const & c, var x, rational & a) {
1278 for (unsigned i = 0; i < c.m_num_vars; i++) {
1279 if (c.m_xs[i] == x) {
1280 a = c.m_as[i];
1281 return;
1282 }
1283 }
1284 UNREACHABLE();
1285 }
1286
1287 var_vector new_xs;
1288 vector<rational> new_as;
1289 svector<literal> new_lits;
1290
resolvefm_tactic::imp1291 constraint * resolve(constraint const & l, constraint const & u, var x) {
1292 m_counter += l.m_num_vars + u.m_num_vars + l.m_num_lits + u.m_num_lits;
1293 rational a, b;
1294 get_coeff(l, x, a);
1295 get_coeff(u, x, b);
1296 SASSERT(a.is_neg());
1297 SASSERT(b.is_pos());
1298 a.neg();
1299
1300 SASSERT(!is_int(x) || a.is_one() || b.is_one());
1301
1302 new_xs.reset();
1303 new_as.reset();
1304 rational new_c = l.m_c*b + u.m_c*a;
1305 bool new_strict = l.m_strict || u.m_strict;
1306
1307 for (unsigned i = 0; i < l.m_num_vars; i++) {
1308 var xi = l.m_xs[i];
1309 if (xi == x)
1310 continue;
1311 unsigned pos = new_xs.size();
1312 new_xs.push_back(xi);
1313 SASSERT(m_var2pos[xi] == UINT_MAX);
1314 m_var2pos[xi] = pos;
1315 new_as.push_back(l.m_as[i] * b);
1316 SASSERT(new_xs[m_var2pos[xi]] == xi);
1317 SASSERT(new_xs.size() == new_as.size());
1318 }
1319
1320 for (unsigned i = 0; i < u.m_num_vars; i++) {
1321 var xi = u.m_xs[i];
1322 if (xi == x)
1323 continue;
1324 unsigned pos = m_var2pos[xi];
1325 if (pos == UINT_MAX) {
1326 new_xs.push_back(xi);
1327 new_as.push_back(u.m_as[i] * a);
1328 }
1329 else {
1330 new_as[pos] += u.m_as[i] * a;
1331 }
1332 }
1333
1334 // remove zeros and check whether all variables are int
1335 bool all_int = true;
1336 unsigned sz = new_xs.size();
1337 unsigned j = 0;
1338 for (unsigned i = 0; i < sz; i++) {
1339 if (new_as[i].is_zero())
1340 continue;
1341 if (!is_int(new_xs[i]))
1342 all_int = false;
1343 if (i != j) {
1344 new_xs[j] = new_xs[i];
1345 new_as[j] = new_as[i];
1346 }
1347 j++;
1348 }
1349 new_xs.shrink(j);
1350 new_as.shrink(j);
1351
1352 if (all_int && new_strict) {
1353 new_strict = false;
1354 new_c --;
1355 }
1356
1357 // reset m_var2pos
1358 for (unsigned i = 0; i < l.m_num_vars; i++) {
1359 m_var2pos[l.m_xs[i]] = UINT_MAX;
1360 }
1361
1362 if (new_xs.empty() && (new_c.is_pos() || (!new_strict && new_c.is_zero()))) {
1363 // literal is true
1364 TRACE("fm", tout << "resolution " << x << " consequent literal is always true: \n";
1365 display(tout, l);
1366 tout << "\n";
1367 display(tout, u); tout << "\n";);
1368 return nullptr; // no constraint needs to be created.
1369 }
1370
1371 new_lits.reset();
1372 for (unsigned i = 0; i < l.m_num_lits; i++) {
1373 literal lit = l.m_lits[i];
1374 bvar p = lit2bvar(lit);
1375 m_bvar2sign[p] = sign(lit) ? -1 : 1;
1376 new_lits.push_back(lit);
1377 }
1378
1379 bool tautology = false;
1380 for (unsigned i = 0; i < u.m_num_lits && !tautology; i++) {
1381 literal lit = u.m_lits[i];
1382 bvar p = lit2bvar(lit);
1383 switch (m_bvar2sign[p]) {
1384 case 0:
1385 new_lits.push_back(lit);
1386 break;
1387 case -1:
1388 if (!sign(lit))
1389 tautology = true;
1390 break;
1391 case 1:
1392 if (sign(lit))
1393 tautology = true;
1394 break;
1395 default:
1396 UNREACHABLE();
1397 }
1398 }
1399
1400 // reset m_bvar2sign
1401 for (unsigned i = 0; i < l.m_num_lits; i++) {
1402 literal lit = l.m_lits[i];
1403 bvar p = lit2bvar(lit);
1404 m_bvar2sign[p] = 0;
1405 }
1406
1407 if (tautology) {
1408 TRACE("fm", tout << "resolution " << x << " tautology: \n";
1409 display(tout, l);
1410 tout << "\n";
1411 display(tout, u); tout << "\n";);
1412 return nullptr;
1413 }
1414
1415 expr_dependency * new_dep = m.mk_join(l.m_dep, u.m_dep);
1416
1417 if (new_lits.empty() && new_xs.empty() && (new_c.is_neg() || (new_strict && new_c.is_zero()))) {
1418 TRACE("fm", tout << "resolution " << x << " inconsistent: \n";
1419 display(tout, l);
1420 tout << "\n";
1421 display(tout, u); tout << "\n";);
1422 m_inconsistent = true;
1423 m_inconsistent_core = new_dep;
1424 return nullptr;
1425 }
1426
1427 constraint * new_cnstr = mk_constraint(new_lits.size(),
1428 new_lits.data(),
1429 new_xs.size(),
1430 new_xs.data(),
1431 new_as.data(),
1432 new_c,
1433 new_strict,
1434 new_dep);
1435
1436 TRACE("fm", tout << "resolution " << x << "\n";
1437 display(tout, l);
1438 tout << "\n";
1439 display(tout, u);
1440 tout << "\n---->\n";
1441 display(tout, *new_cnstr);
1442 tout << "\n";
1443 tout << "new_dep: " << new_dep << "\n";);
1444
1445 return new_cnstr;
1446 }
1447
1448 ptr_vector<constraint> new_constraints;
1449
try_eliminatefm_tactic::imp1450 bool try_eliminate(var x) {
1451 constraints & l = m_lowers[x];
1452 constraints & u = m_uppers[x];
1453 cleanup_constraints(l);
1454 cleanup_constraints(u);
1455
1456 if (l.empty() || u.empty()) {
1457 // easy case
1458 mark_constraints_dead(x);
1459 TRACE("fm", tout << "variables was eliminated (trivial case)\n";);
1460 return true;
1461 }
1462
1463 unsigned num_lowers = l.size();
1464 unsigned num_uppers = u.size();
1465
1466 if (num_lowers > m_fm_cutoff1 && num_uppers > m_fm_cutoff1)
1467 return false;
1468
1469 if (num_lowers * num_uppers > m_fm_cutoff2)
1470 return false;
1471
1472 if (!can_eliminate(x))
1473 return false;
1474
1475 m_counter += num_lowers * num_uppers;
1476
1477 TRACE("fm_bug", tout << "eliminating " << mk_ismt2_pp(m_var2expr.get(x), m) << "\nlowers:\n";
1478 display_constraints(tout, l); tout << "uppers:\n"; display_constraints(tout, u););
1479
1480 unsigned num_old_cnstrs = num_uppers + num_lowers;
1481 unsigned limit = num_old_cnstrs + m_fm_extra;
1482 unsigned num_new_cnstrs = 0;
1483 new_constraints.reset();
1484 for (unsigned i = 0; i < num_lowers; i++) {
1485 for (unsigned j = 0; j < num_uppers; j++) {
1486 if (m_inconsistent || num_new_cnstrs > limit) {
1487 TRACE("fm", tout << "too many new constraints: " << num_new_cnstrs << "\n";);
1488 del_constraints(new_constraints.size(), new_constraints.data());
1489 return false;
1490 }
1491 constraint const & l_c = *(l[i]);
1492 constraint const & u_c = *(u[j]);
1493 constraint * new_c = resolve(l_c, u_c, x);
1494 if (new_c != nullptr) {
1495 num_new_cnstrs++;
1496 new_constraints.push_back(new_c);
1497 }
1498 }
1499 }
1500
1501 mark_constraints_dead(x);
1502
1503 unsigned sz = new_constraints.size();
1504
1505 m_counter += sz;
1506
1507 for (unsigned i = 0; i < sz; i++) {
1508 constraint * c = new_constraints[i];
1509 backward_subsumption(*c);
1510 register_constraint(c);
1511 }
1512 TRACE("fm", tout << "variables was eliminated old: " << num_old_cnstrs << " new_constraints: " << sz << "\n";);
1513 return true;
1514 }
1515
copy_remainingfm_tactic::imp1516 void copy_remaining(vector<constraints> & v2cs) {
1517 vector<constraints>::iterator it = v2cs.begin();
1518 vector<constraints>::iterator end = v2cs.end();
1519 for (; it != end; ++it) {
1520 constraints & cs = *it;
1521 constraints::iterator it2 = cs.begin();
1522 constraints::iterator end2 = cs.end();
1523 for (; it2 != end2; ++it2) {
1524 constraint * c = *it2;
1525 if (!c->m_dead) {
1526 c->m_dead = true;
1527 expr * new_f = to_expr(*c);
1528 TRACE("fm_bug", tout << "asserting...\n" << mk_ismt2_pp(new_f, m) << "\nnew_dep: " << c->m_dep << "\n";);
1529 m_new_goal->assert_expr(new_f, nullptr, c->m_dep);
1530 }
1531 }
1532 }
1533 v2cs.finalize();
1534 }
1535
1536 // Copy remaining clauses to m_new_goal
copy_remainingfm_tactic::imp1537 void copy_remaining() {
1538 copy_remaining(m_uppers);
1539 copy_remaining(m_lowers);
1540 }
1541
checkpointfm_tactic::imp1542 void checkpoint() {
1543 if (!m.inc())
1544 throw tactic_exception(m.limit().get_cancel_msg());
1545 if (memory::get_allocation_size() > m_max_memory)
1546 throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
1547 }
1548
operator ()fm_tactic::imp1549 void operator()(goal_ref const & g,
1550 goal_ref_buffer & result) {
1551 tactic_report report("fm", *g);
1552 fail_if_proof_generation("fm", g);
1553 m_produce_models = g->models_enabled();
1554
1555 init(*g);
1556
1557 m_new_goal = alloc(goal, *g, true);
1558 SASSERT(m_new_goal->depth() == g->depth());
1559 SASSERT(m_new_goal->prec() == g->prec());
1560 m_new_goal->inc_depth();
1561
1562 init_use_list(*g);
1563
1564 if (m_inconsistent) {
1565 m_new_goal->reset();
1566 m_new_goal->assert_expr(m.mk_false(), nullptr, m_inconsistent_core);
1567 }
1568 else {
1569 TRACE("fm", display(tout););
1570
1571 subsume();
1572 var_vector candidates;
1573 sort_candidates(candidates);
1574
1575 unsigned eliminated = 0;
1576
1577 if (m_produce_models)
1578 m_mc = alloc(fm_model_converter, m);
1579
1580 unsigned num = candidates.size();
1581 for (unsigned i = 0; i < num; i++) {
1582 checkpoint();
1583 if (m_counter > m_fm_limit)
1584 break;
1585 m_counter++;
1586 if (try_eliminate(candidates[i]))
1587 eliminated++;
1588 if (m_inconsistent) {
1589 m_new_goal->reset();
1590 m_new_goal->assert_expr(m.mk_false(), nullptr, m_inconsistent_core);
1591 break;
1592 }
1593 }
1594 report_tactic_progress(":fm-eliminated", eliminated);
1595 report_tactic_progress(":fm-cost", m_counter);
1596 if (!m_inconsistent) {
1597 copy_remaining();
1598 m_new_goal->add(m_mc.get());
1599 }
1600 }
1601 reset_constraints();
1602 result.push_back(m_new_goal.get());
1603 TRACE("fm", m_new_goal->display(tout););
1604 }
1605
display_constraintsfm_tactic::imp1606 void display_constraints(std::ostream & out, constraints const & cs) const {
1607 constraints::const_iterator it = cs.begin();
1608 constraints::const_iterator end = cs.end();
1609 for (; it != end; ++it) {
1610 out << " ";
1611 display(out, *(*it));
1612 out << "\n";
1613 }
1614 }
1615
displayfm_tactic::imp1616 void display(std::ostream & out) const {
1617 unsigned num = num_vars();
1618 for (var x = 0; x < num; x++) {
1619 if (is_forbidden(x))
1620 continue;
1621 out << mk_ismt2_pp(m_var2expr.get(x), m) << "\n";
1622 display_constraints(out, m_lowers[x]);
1623 display_constraints(out, m_uppers[x]);
1624 }
1625 }
1626 };
1627
1628 imp * m_imp;
1629 params_ref m_params;
1630 public:
1631
fm_tactic(ast_manager & m,params_ref const & p)1632 fm_tactic(ast_manager & m, params_ref const & p):
1633 m_params(p) {
1634 m_imp = alloc(imp, m, p);
1635 }
1636
translate(ast_manager & m)1637 tactic * translate(ast_manager & m) override {
1638 return alloc(fm_tactic, m, m_params);
1639 }
1640
~fm_tactic()1641 ~fm_tactic() override {
1642 dealloc(m_imp);
1643 }
1644
updt_params(params_ref const & p)1645 void updt_params(params_ref const & p) override {
1646 m_params = p;
1647 m_imp->updt_params(p);
1648 }
1649
collect_param_descrs(param_descrs & r)1650 void collect_param_descrs(param_descrs & r) override {
1651 insert_produce_models(r);
1652 insert_max_memory(r);
1653 r.insert("fm_real_only", CPK_BOOL, "(default: true) consider only real variables for fourier-motzkin elimination.");
1654 r.insert("fm_occ", CPK_BOOL, "(default: false) consider inequalities occurring in clauses for FM.");
1655 r.insert("fm_limit", CPK_UINT, "(default: 5000000) maximum number of constraints, monomials, clauses visited during FM.");
1656 r.insert("fm_cutoff1", CPK_UINT, "(default: 8) first cutoff for FM based on maximum number of lower/upper occurrences.");
1657 r.insert("fm_cutoff2", CPK_UINT, "(default: 256) second cutoff for FM based on num_lower * num_upper occurrences.");
1658 r.insert("fm_extra", CPK_UINT, "(default: 0) max. increase on the number of inequalities for each FM variable elimination step.");
1659 }
1660
1661
cleanup()1662 void cleanup() override {
1663 imp * d = alloc(imp, m_imp->m, m_params);
1664 std::swap(d, m_imp);
1665 dealloc(d);
1666 }
1667
operator ()(goal_ref const & in,goal_ref_buffer & result)1668 void operator()(goal_ref const & in,
1669 goal_ref_buffer & result) override {
1670 (*m_imp)(in, result);
1671 }
1672 };
1673
mk_fm_tactic(ast_manager & m,params_ref const & p)1674 tactic * mk_fm_tactic(ast_manager & m, params_ref const & p) {
1675 params_ref s_p = p;
1676 s_p.set_bool("arith_lhs", true);
1677 s_p.set_bool("elim_and", true);
1678 s_p.set_bool("som", true);
1679 return and_then(using_params(mk_simplify_tactic(m, s_p), s_p),
1680 clean(alloc(fm_tactic, m, p)));
1681 }
1682