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