1 /*++ 2 Copyright (c) 2010 Microsoft Corporation 3 4 Module Name: 5 6 qe.cpp 7 8 Abstract: 9 10 Quantifier elimination procedures 11 12 Author: 13 14 Nikolaj Bjorner (nbjorner) 2010-02-19 15 16 Revision History: 17 18 19 --*/ 20 21 #include "qe/qe.h" 22 #include "smt/smt_theory.h" 23 #include "ast/bv_decl_plugin.h" 24 #include "smt/smt_context.h" 25 #include "smt/theory_bv.h" 26 #include "ast/ast_ll_pp.h" 27 #include "ast/ast_pp.h" 28 #include "ast/ast_smt_pp.h" 29 #include "ast/expr_abstract.h" 30 #include "ast/rewriter/var_subst.h" 31 #include "ast/for_each_expr.h" 32 #include "ast/dl_decl_plugin.h" 33 #include "qe/nlarith_util.h" 34 #include "ast/rewriter/expr_replacer.h" 35 #include "ast/rewriter/factor_rewriter.h" 36 #include "ast/expr_functors.h" 37 #include "ast/rewriter/quant_hoist.h" 38 #include "ast/rewriter/bool_rewriter.h" 39 #include "ast/rewriter/th_rewriter.h" 40 #include "smt/smt_kernel.h" 41 #include "model/model_evaluator.h" 42 #include "ast/has_free_vars.h" 43 #include "ast/rewriter/rewriter_def.h" 44 #include "tactic/tactical.h" 45 #include "model/model_v2_pp.h" 46 #include "util/obj_hashtable.h" 47 48 49 namespace qe { 50 51 class conjunctions { 52 ast_manager& m; 53 ptr_vector<qe_solver_plugin> m_plugins; // family_id -> plugin 54 55 public: conjunctions(ast_manager & m)56 conjunctions(ast_manager& m) : m(m) {} 57 add_plugin(qe_solver_plugin * p)58 void add_plugin(qe_solver_plugin* p) { 59 family_id fid = p->get_family_id(); 60 if (static_cast<family_id>(m_plugins.size()) <= fid) { 61 m_plugins.resize(fid + 1); 62 } 63 m_plugins[fid] = p; 64 } 65 get_partition(expr * fml,unsigned num_vars,app * const * vars,expr_ref & fml_closed,expr_ref & fml_mixed,expr_ref & fml_open)66 void get_partition( 67 expr* fml, 68 unsigned num_vars, 69 app* const* vars, 70 expr_ref& fml_closed, // conjuncts that don't contain any variables from vars. 71 expr_ref& fml_mixed, // conjuncts that contain terms from vars and non-vars. 72 expr_ref& fml_open // conjuncts that contain vars (mixed or pure). 73 ) 74 { 75 expr_ref_vector conjs(m); 76 ast_mark visited; 77 ast_mark contains_var; 78 ast_mark contains_uf; 79 ptr_vector<expr> todo; 80 ptr_vector<expr> conjs_closed, conjs_mixed, conjs_open; 81 82 flatten_and(fml, conjs); 83 84 for (unsigned i = 0; i < conjs.size(); ++i) { 85 todo.push_back(conjs[i].get()); 86 } 87 while (!todo.empty()) { 88 expr* e = todo.back(); 89 if (visited.is_marked(e)) { 90 todo.pop_back(); 91 continue; 92 } 93 94 if (is_var(to_app(e), num_vars, vars)) { 95 contains_var.mark(e, true); 96 visited.mark(e, true); 97 todo.pop_back(); 98 continue; 99 } 100 101 if (!is_app(e)) { 102 visited.mark(e, true); 103 todo.pop_back(); 104 continue; 105 } 106 107 bool all_visited = true; 108 app* a = to_app(e); 109 if (is_uninterpreted(a)) { 110 contains_uf.mark(e, true); 111 } 112 for (unsigned i = 0; i < a->get_num_args(); ++i) { 113 expr* arg = a->get_arg(i); 114 if (!visited.is_marked(arg)) { 115 all_visited = false; 116 todo.push_back(arg); 117 } 118 else { 119 if (contains_var.is_marked(arg)) { 120 contains_var.mark(e, true); 121 } 122 if (contains_uf.is_marked(arg)) { 123 contains_uf.mark(e, true); 124 } 125 } 126 } 127 if (all_visited) { 128 todo.pop_back(); 129 visited.mark(e, true); 130 } 131 } 132 for (expr* e : conjs) { 133 bool cv = contains_var.is_marked(e); 134 bool cu = contains_uf.is_marked(e); 135 if (cv && cu) { 136 conjs_mixed.push_back(e); 137 conjs_open.push_back(e); 138 } 139 else if (cv) { 140 conjs_open.push_back(e); 141 } 142 else { 143 conjs_closed.push_back(e); 144 } 145 } 146 bool_rewriter rewriter(m); 147 rewriter.mk_and(conjs_closed.size(), conjs_closed.c_ptr(), fml_closed); 148 rewriter.mk_and(conjs_mixed.size(), conjs_mixed.c_ptr(), fml_mixed); 149 rewriter.mk_and(conjs_open.size(), conjs_open.c_ptr(), fml_open); 150 151 TRACE("qe", 152 tout << "closed\n" << mk_ismt2_pp(fml_closed, m) << "\n"; 153 tout << "open\n" << mk_ismt2_pp(fml_open, m) << "\n"; 154 tout << "mixed\n" << mk_ismt2_pp(fml_mixed, m) << "\n"; 155 ); 156 } 157 158 // 159 // Partition variables into buckets. 160 // The var_paritions buckets covering disjoint subsets of 161 // the conjuncts. The remaining variables in vars are non-partioned. 162 // partition_vars(unsigned num_vars,contains_app ** vars,unsigned num_args,expr * const * args,vector<unsigned_vector> & partition)163 bool partition_vars( 164 unsigned num_vars, 165 contains_app** vars, 166 unsigned num_args, 167 expr* const* args, 168 vector<unsigned_vector>& partition 169 ) 170 { 171 unsigned_vector contains_index; 172 unsigned_vector non_shared; 173 unsigned_vector non_shared_vars; 174 union_find_default_ctx df; 175 union_find<union_find_default_ctx> uf(df); 176 177 partition.reset(); 178 179 for (unsigned v = 0; v < num_vars; ++v) { 180 contains_app& contains_x = *vars[v]; 181 contains_index.reset(); 182 for (unsigned i = 0; i < num_args; ++i) { 183 if (contains_x(args[i])) { 184 contains_index.push_back(i); 185 TRACE("qe_verbose", tout << "var " << v << " in " << i << "\n";); 186 } 187 } 188 // 189 // x occurs in more than half of conjuncts. 190 // Mark it as shared. 191 // 192 if (2*contains_index.size() > num_args) { 193 if (partition.empty()) { 194 partition.push_back(unsigned_vector()); 195 } 196 partition.back().push_back(v); 197 TRACE("qe_verbose", tout << "majority " << v << "\n";); 198 continue; 199 } 200 // 201 // Create partition of variables that share conjuncts. 202 // 203 unsigned var_x = uf.mk_var(); 204 SASSERT(var_x == non_shared_vars.size()); 205 non_shared_vars.push_back(v); 206 for (unsigned i = 0; i < contains_index.size(); ++i) { 207 unsigned idx = contains_index[i]; 208 if (non_shared.size() <= idx) { 209 non_shared.resize(idx+1,UINT_MAX); 210 } 211 unsigned var_y = non_shared[idx]; 212 if (var_y != UINT_MAX) { 213 uf.merge(var_x, var_y); 214 } 215 else { 216 non_shared[idx] = var_x; 217 } 218 } 219 } 220 if (non_shared_vars.empty()) { 221 return false; 222 } 223 224 unsigned root0 = uf.find(0); 225 bool is_partitioned = false; 226 for (unsigned idx = 1; !is_partitioned && idx < non_shared_vars.size(); ++idx) { 227 is_partitioned = (uf.find(idx) != root0); 228 } 229 if (!is_partitioned) { 230 return false; 231 } 232 233 // 234 // variables are partitioned into more than one 235 // class. 236 // 237 238 unsigned_vector roots; 239 if (!partition.empty()) { 240 roots.push_back(UINT_MAX); 241 } 242 for (unsigned idx = 0; idx < non_shared_vars.size(); ++idx) { 243 unsigned x = non_shared_vars[idx]; 244 unsigned r = non_shared_vars[uf.find(idx)]; 245 TRACE("qe_verbose", tout << "x: " << x << " r: " << r << "\n";); 246 bool found = false; 247 for (unsigned i = 0; !found && i < roots.size(); ++i) { 248 if (roots[i] == r) { 249 found = true; 250 partition[i].push_back(x); 251 } 252 } 253 if (!found) { 254 roots.push_back(r); 255 partition.push_back(unsigned_vector()); 256 partition.back().push_back(x); 257 } 258 } 259 260 TRACE("qe_verbose", 261 for (unsigned i = 0; i < partition.size(); ++i) { 262 for (unsigned j = 0; j < partition[i].size(); ++j) { 263 tout << " " << mk_ismt2_pp(vars[partition[i][j]]->x(), m);; 264 } 265 tout << "\n"; 266 }); 267 268 SASSERT(partition.size() != 1); 269 SASSERT(!partition.empty() || roots.size() > 1); 270 271 return true; 272 } 273 274 private: 275 is_var(app * x,unsigned num_vars,app * const * vars)276 bool is_var(app* x, unsigned num_vars, app* const* vars) { 277 for (unsigned i = 0; i < num_vars; ++i) { 278 if (vars[i] == x) { 279 return true; 280 } 281 } 282 return false; 283 } 284 is_uninterpreted(app * a)285 bool is_uninterpreted(app* a) { 286 family_id fid = a->get_family_id(); 287 if (null_family_id == fid) { 288 return true; 289 } 290 if (static_cast<unsigned>(fid) >= m_plugins.size()) { 291 return true; 292 } 293 qe_solver_plugin* p = m_plugins[fid]; 294 if (!p) { 295 return true; 296 } 297 return p->is_uninterpreted(a); 298 } 299 300 }; 301 302 // --------------- 303 // conj_enum 304 conj_enum(ast_manager & m,expr * e)305 conj_enum::conj_enum(ast_manager& m, expr* e): m(m), m_conjs(m) { 306 flatten_and(e, m_conjs); 307 } 308 extract_equalities(expr_ref_vector & eqs)309 void conj_enum::extract_equalities(expr_ref_vector& eqs) { 310 arith_util arith(m); 311 obj_hashtable<expr> leqs; 312 expr_ref_vector trail(m); 313 expr_ref tmp1(m), tmp2(m); 314 expr *a0, *a1; 315 eqs.reset(); 316 conj_enum::iterator it = begin(); 317 for (; it != end(); ++it) { 318 expr* e = *it; 319 320 if (m.is_eq(e, a0, a1) && (arith.is_int(a0) || arith.is_real(a0))) { 321 tmp1 = arith.mk_sub(a0, a1); 322 eqs.push_back(tmp1); 323 } 324 else if (arith.is_le(e, a0, a1) || arith.is_ge(e, a1, a0)) { 325 tmp1 = arith.mk_sub(a0, a1); 326 tmp2 = arith.mk_sub(a1, a0); 327 328 if (leqs.contains(tmp2)) { 329 eqs.push_back(tmp1); 330 TRACE("qe", tout << "found: " << mk_ismt2_pp(tmp1, m) << "\n";); 331 } 332 else { 333 trail.push_back(tmp1); 334 leqs.insert(tmp1); 335 TRACE("qe_verbose", tout << "insert: " << mk_ismt2_pp(tmp1, m) << "\n";); 336 } 337 } 338 else { 339 // drop equality. 340 } 341 } 342 } 343 344 // ----------------- 345 // Lift ite from sub-formulas. 346 // 347 class lift_ite { 348 ast_manager& m; 349 i_expr_pred& m_is_relevant; 350 th_rewriter m_rewriter; 351 scoped_ptr<expr_replacer> m_replace; 352 public: lift_ite(ast_manager & m,i_expr_pred & is_relevant)353 lift_ite(ast_manager& m, i_expr_pred& is_relevant) : 354 m(m), m_is_relevant(is_relevant), m_rewriter(m), m_replace(mk_default_expr_replacer(m, false)) {} 355 operator ()(expr * fml,expr_ref & result)356 bool operator()(expr* fml, expr_ref& result) { 357 if (m.is_ite(fml)) { 358 result = fml; 359 return true; 360 } 361 app* ite; 362 if (find_ite(fml, ite)) { 363 expr* cond = nullptr, *th = nullptr, *el = nullptr; 364 VERIFY(m.is_ite(ite, cond, th, el)); 365 expr_ref tmp1(fml, m), tmp2(fml, m); 366 m_replace->apply_substitution(ite, th, tmp1); 367 m_replace->apply_substitution(ite, el, tmp2); 368 result = m.mk_ite(cond, tmp1, tmp2); 369 m_rewriter(result); 370 return result != fml; 371 } 372 else { 373 return false; 374 } 375 } 376 377 private: 378 find_ite(expr * e,app * & ite)379 bool find_ite(expr* e, app*& ite) { 380 ptr_vector<expr> todo; 381 ast_mark visited; 382 todo.push_back(e); 383 while(!todo.empty()) { 384 e = todo.back(); 385 todo.pop_back(); 386 if (visited.is_marked(e)) { 387 continue; 388 } 389 visited.mark(e, true); 390 if (!m_is_relevant(e)) { 391 continue; 392 } 393 if (m.is_ite(e)) { 394 ite = to_app(e); 395 return true; 396 } 397 if (is_app(e)) { 398 app* a = to_app(e); 399 unsigned num_args = a->get_num_args(); 400 for (unsigned i = 0; i < num_args; ++i) { 401 todo.push_back(a->get_arg(i)); 402 } 403 } 404 } 405 return false; 406 } 407 }; 408 409 // convert formula to NNF. 410 class nnf { 411 ast_manager& m; 412 i_expr_pred& m_is_relevant; 413 lift_ite m_lift_ite; 414 obj_map<expr, expr*> m_pos, m_neg; // memoize positive/negative sub-formulas 415 expr_ref_vector m_trail; // trail for generated terms 416 expr_ref_vector m_args; 417 ptr_vector<expr> m_todo; // stack of formulas to visit 418 bool_vector m_pols; // stack of polarities 419 bool_rewriter m_rewriter; 420 421 public: nnf(ast_manager & m,i_expr_pred & is_relevant)422 nnf(ast_manager& m, i_expr_pred& is_relevant): 423 m(m), 424 m_is_relevant(is_relevant), 425 m_lift_ite(m, is_relevant), 426 m_trail(m), 427 m_args(m), 428 m_rewriter(m) {} 429 operator ()(expr_ref & fml)430 void operator()(expr_ref& fml) { 431 reset(); 432 get_nnf(fml, true); 433 } 434 reset()435 void reset() { 436 m_todo.reset(); 437 m_trail.reset(); 438 m_pols.reset(); 439 m_pos.reset(); 440 m_neg.reset(); 441 } 442 443 private: 444 contains(expr * e,bool p)445 bool contains(expr* e, bool p) { 446 return p?m_pos.contains(e):m_neg.contains(e); 447 } 448 lookup(expr * e,bool p)449 expr* lookup(expr* e, bool p) { 450 expr* r = nullptr; 451 if (p && m_pos.find(e, r)) { 452 return r; 453 } 454 if (!p && m_neg.find(e, r)) { 455 return r; 456 } 457 m_todo.push_back(e); 458 m_pols.push_back(p); 459 return nullptr; 460 } 461 insert(expr * e,bool p,expr * r)462 void insert(expr* e, bool p, expr* r) { 463 if (p) { 464 m_pos.insert(e, r); 465 } 466 else { 467 m_neg.insert(e, r); 468 } 469 TRACE("nnf", 470 tout << mk_ismt2_pp(e, m) << " " << p << "\n"; 471 tout << mk_ismt2_pp(r, m) << "\n";); 472 473 m_trail.push_back(r); 474 } 475 pop()476 void pop() { 477 m_todo.pop_back(); 478 m_pols.pop_back(); 479 } 480 nnf_iff(app * a,bool p)481 void nnf_iff(app* a, bool p) { 482 SASSERT(m.is_iff(a) || m.is_xor(a) || m.is_eq(a)); 483 expr* a0 = a->get_arg(0); 484 expr* a1 = a->get_arg(1); 485 486 expr* r1 = lookup(a0, true); 487 expr* r2 = lookup(a0, false); 488 expr* p1 = lookup(a1, true); 489 expr* p2 = lookup(a1, false); 490 if (r1 && r2 && p1 && p2) { 491 expr_ref tmp1(m), tmp2(m), tmp(m); 492 pop(); 493 if (p) { 494 m_rewriter.mk_and(r1, p1, tmp1); 495 m_rewriter.mk_and(r2, p2, tmp2); 496 m_rewriter.mk_or(tmp1, tmp2, tmp); 497 } 498 else { 499 m_rewriter.mk_or(r1, p1, tmp1); 500 m_rewriter.mk_or(r2, p2, tmp2); 501 m_rewriter.mk_and(tmp1, tmp2, tmp); 502 } 503 insert(a, p, tmp); 504 } 505 } 506 nnf_ite(app * a,bool p)507 void nnf_ite(app* a, bool p) { 508 SASSERT(m.is_ite(a)); 509 expr* r1 = lookup(a->get_arg(0), true); 510 expr* r2 = lookup(a->get_arg(0), false); 511 expr* th = lookup(a->get_arg(1), p); 512 expr* el = lookup(a->get_arg(2), p); 513 if (r1 && r2 && th && el) { 514 expr_ref tmp1(m), tmp2(m), tmp(m); 515 pop(); 516 m_rewriter.mk_and(r1, th, tmp1); 517 m_rewriter.mk_and(r2, el, tmp2); 518 m_rewriter.mk_or(tmp1, tmp2, tmp); 519 TRACE("nnf", 520 tout << mk_ismt2_pp(a, m) << "\n"; 521 tout << mk_ismt2_pp(tmp, m) << "\n";); 522 insert(a, p, tmp); 523 } 524 } 525 nnf_implies(app * a,bool p)526 void nnf_implies(app* a, bool p) { 527 SASSERT(m.is_implies(a)); 528 expr* r1 = lookup(a->get_arg(0), !p); 529 expr* r2 = lookup(a->get_arg(1), p); 530 if (r1 && r2) { 531 expr_ref tmp(m); 532 if (p) { 533 m_rewriter.mk_or(r1, r2, tmp); 534 } 535 else { 536 m_rewriter.mk_and(r1, r2, tmp); 537 } 538 insert(a, p, tmp); 539 } 540 } 541 nnf_not(app * a,bool p)542 void nnf_not(app* a, bool p) { 543 SASSERT(m.is_not(a)); 544 expr* arg = a->get_arg(0); 545 expr* e = lookup(arg, !p); 546 if (e) { 547 insert(a, p, e); 548 } 549 } 550 nnf_and_or(bool is_and,app * a,bool p)551 void nnf_and_or(bool is_and, app* a, bool p) { 552 m_args.reset(); 553 unsigned num_args = a->get_num_args(); 554 expr_ref tmp(m); 555 bool visited = true; 556 for (expr* arg : *a) { 557 expr* r = lookup(arg, p); 558 if (r) { 559 m_args.push_back(r); 560 } 561 else { 562 visited = false; 563 } 564 } 565 if (visited) { 566 pop(); 567 if (p == is_and) 568 tmp = mk_and(m_args); 569 else 570 tmp = mk_or(m_args); 571 insert(a, p, tmp); 572 } 573 } 574 get_nnf(expr_ref & fml,bool p0)575 bool get_nnf(expr_ref& fml, bool p0) { 576 TRACE("nnf", tout << mk_ismt2_pp(fml.get(), m) << "\n";); 577 bool p = p0; 578 unsigned sz = m_todo.size(); 579 expr_ref tmp(m); 580 581 expr* e = lookup(fml, p); 582 if (e) { 583 fml = e; 584 return true; 585 } 586 m_trail.push_back(fml); 587 588 while (sz < m_todo.size()) { 589 e = m_todo.back(); 590 p = m_pols.back(); 591 if (!m_is_relevant(e)) { 592 pop(); 593 insert(e, p, p?e:mk_not(m, e)); 594 continue; 595 } 596 if (!is_app(e)) { 597 return false; 598 } 599 if (contains(e, p)) { 600 pop(); 601 continue; 602 } 603 app* a = to_app(e); 604 if (m.is_and(e) || m.is_or(e)) { 605 nnf_and_or(m.is_and(a), a, p); 606 } 607 else if (m.is_not(a)) { 608 nnf_not(a, p); 609 } 610 else if (m.is_ite(a)) { 611 nnf_ite(a, p); 612 } 613 else if (m.is_iff(a)) { 614 nnf_iff(a, p); 615 } 616 else if (m.is_xor(a)) { 617 nnf_iff(a, !p); 618 } 619 else if (m.is_implies(a)) { 620 nnf_implies(a, p); 621 } 622 else if (m_lift_ite(e, tmp)) { 623 if (!get_nnf(tmp, p)) { 624 return false; 625 } 626 pop(); 627 insert(e, p, tmp); 628 } 629 else { 630 pop(); 631 insert(e, p, p?e:mk_not(m, e)); 632 } 633 634 } 635 fml = lookup(fml, p0); 636 SASSERT(fml.get()); 637 return true; 638 } 639 }; 640 641 // ---------------------------------- 642 // Normalize literals in NNF formula. 643 644 class nnf_normalize_literals { 645 ast_manager& m; 646 i_expr_pred& m_is_relevant; 647 i_nnf_atom& m_mk_atom; 648 obj_map<expr, expr*> m_cache; 649 ptr_vector<expr> m_todo; 650 expr_ref_vector m_trail; 651 ptr_vector<expr> m_args; 652 public: nnf_normalize_literals(ast_manager & m,i_expr_pred & is_relevant,i_nnf_atom & mk_atom)653 nnf_normalize_literals(ast_manager& m, i_expr_pred& is_relevant, i_nnf_atom& mk_atom): 654 m(m), m_is_relevant(is_relevant), m_mk_atom(mk_atom), m_trail(m) {} 655 operator ()(expr_ref & fml)656 void operator()(expr_ref& fml) { 657 SASSERT(m_todo.empty()); 658 m_todo.push_back(fml); 659 while (!m_todo.empty()) { 660 expr* e = m_todo.back(); 661 if (m_cache.contains(e)) { 662 m_todo.pop_back(); 663 } 664 else if (!is_app(e)) { 665 m_todo.pop_back(); 666 m_cache.insert(e, e); 667 } 668 else if (visit(to_app(e))) { 669 m_todo.pop_back(); 670 } 671 } 672 fml = m_cache.find(fml); 673 reset(); 674 } 675 reset()676 void reset() { 677 m_cache.reset(); 678 m_todo.reset(); 679 m_trail.reset(); 680 } 681 682 private: 683 visit(app * e)684 bool visit(app* e) { 685 bool all_visit = true; 686 expr* f = nullptr; 687 expr_ref tmp(m); 688 if (!m_is_relevant(e)) { 689 m_cache.insert(e, e); 690 } 691 else if (m.is_and(e) || m.is_or(e)) { 692 m_args.reset(); 693 for (expr* arg : *e) { 694 if (m_cache.find(arg, f)) { 695 m_args.push_back(f); 696 } 697 else { 698 all_visit = false; 699 m_todo.push_back(arg); 700 } 701 } 702 if (all_visit) { 703 m_cache.insert(e, m.mk_app(e->get_decl(), m_args.size(), m_args.c_ptr())); 704 } 705 } 706 else if (m.is_not(e, f)) { 707 SASSERT(!m.is_not(f) && !m.is_and(f) && !m.is_or(f)); 708 m_mk_atom(f, false, tmp); 709 m_cache.insert(e, tmp); 710 m_trail.push_back(tmp); 711 } 712 else { 713 m_mk_atom(e, true, tmp); 714 m_trail.push_back(tmp); 715 m_cache.insert(e, tmp); 716 } 717 return all_visit; 718 } 719 }; 720 721 // ---------------------------- 722 // def_vector 723 normalize()724 void def_vector::normalize() { 725 // apply nested definitions into place. 726 ast_manager& m = m_vars.get_manager(); 727 expr_substitution sub(m); 728 scoped_ptr<expr_replacer> rep = mk_expr_simp_replacer(m); 729 if (size() <= 1) { 730 return; 731 } 732 for (unsigned i = size(); i > 0; ) { 733 --i; 734 expr_ref e(m); 735 e = def(i); 736 rep->set_substitution(&sub); 737 (*rep)(e); 738 sub.insert(m.mk_const(var(i)), e); 739 def_ref(i) = e; 740 } 741 } 742 project(unsigned num_vars,app * const * vars)743 void def_vector::project(unsigned num_vars, app* const* vars) { 744 obj_hashtable<func_decl> fns; 745 for (unsigned i = 0; i < num_vars; ++i) { 746 fns.insert(vars[i]->get_decl()); 747 } 748 for (unsigned i = 0; i < size(); ++i) { 749 if (fns.contains(m_vars[i].get())) { 750 // 751 // retain only first occurrence of eliminated variable. 752 // later occurrences are just recycling the name. 753 // 754 fns.remove(m_vars[i].get()); 755 } 756 else { 757 for (unsigned j = i+1; j < size(); ++j) { 758 m_vars.set(j-1, m_vars.get(j)); 759 m_defs.set(j-1, m_defs.get(j)); 760 } 761 m_vars.pop_back(); 762 m_defs.pop_back(); 763 --i; 764 } 765 } 766 } 767 768 // ---------------------------- 769 // guarded_defs 770 display(std::ostream & out) const771 std::ostream& guarded_defs::display(std::ostream& out) const { 772 ast_manager& m = m_guards.get_manager(); 773 for (unsigned i = 0; i < size(); ++i) { 774 for (unsigned j = 0; j < defs(i).size(); ++j) { 775 out << defs(i).var(j)->get_name() << " := " << mk_pp(defs(i).def(j), m) << "\n"; 776 } 777 out << "if " << mk_pp(guard(i), m) << "\n"; 778 } 779 return out; 780 } 781 inv()782 bool guarded_defs::inv() { 783 return m_defs.size() == m_guards.size(); 784 } 785 add(expr * guard,def_vector const & defs)786 void guarded_defs::add(expr* guard, def_vector const& defs) { 787 SASSERT(inv()); 788 m_defs.push_back(defs); 789 m_guards.push_back(guard); 790 m_defs.back().normalize(); 791 SASSERT(inv()); 792 } 793 project(unsigned num_vars,app * const * vars)794 void guarded_defs::project(unsigned num_vars, app* const* vars) { 795 for (unsigned i = 0; i < size(); ++i) { 796 m_defs[i].project(num_vars, vars); 797 } 798 } 799 800 // ---------------------------- 801 // Obtain atoms in NNF formula. 802 803 class nnf_collect_atoms { 804 ast_manager& m; 805 i_expr_pred& m_is_relevant; 806 ptr_vector<expr> m_todo; 807 ast_mark m_visited; 808 public: nnf_collect_atoms(ast_manager & m,i_expr_pred & is_relevant)809 nnf_collect_atoms(ast_manager& m, i_expr_pred& is_relevant): 810 m(m), m_is_relevant(is_relevant) {} 811 operator ()(expr * fml,atom_set & pos,atom_set & neg)812 void operator()(expr* fml, atom_set& pos, atom_set& neg) { 813 m_todo.push_back(fml); 814 while (!m_todo.empty()) { 815 expr* e = m_todo.back(); 816 m_todo.pop_back(); 817 if (m_visited.is_marked(e)) 818 continue; 819 m_visited.mark(e, true); 820 if (!is_app(e) || !m_is_relevant(e)) 821 continue; 822 app* a = to_app(e); 823 if (m.is_and(a) || m.is_or(a)) { 824 for (expr* arg : *a) 825 m_todo.push_back(arg); 826 } 827 else if (m.is_not(a, e) && is_app(e)) { 828 neg.insert(to_app(e)); 829 } 830 else { 831 pos.insert(a); 832 } 833 } 834 SASSERT(m_todo.empty()); 835 m_visited.reset(); 836 } 837 }; 838 839 840 // -------------------------------- 841 // Bring formula to NNF, normalize atoms, collect literals. 842 843 class nnf_normalizer { 844 nnf m_nnf_core; 845 nnf_collect_atoms m_collect_atoms; 846 nnf_normalize_literals m_normalize_literals; 847 public: nnf_normalizer(ast_manager & m,i_expr_pred & is_relevant,i_nnf_atom & mk_atom)848 nnf_normalizer(ast_manager& m, i_expr_pred& is_relevant, i_nnf_atom& mk_atom): 849 m_nnf_core(m, is_relevant), 850 m_collect_atoms(m, is_relevant), 851 m_normalize_literals(m, is_relevant, mk_atom) 852 {} 853 operator ()(expr_ref & fml,atom_set & pos,atom_set & neg)854 void operator()(expr_ref& fml, atom_set& pos, atom_set& neg) { 855 expr_ref orig(fml); 856 m_nnf_core(fml); 857 m_normalize_literals(fml); 858 m_collect_atoms(fml, pos, neg); 859 TRACE("qe", 860 ast_manager& m = fml.get_manager(); 861 tout << mk_ismt2_pp(orig, m) << "\n-->\n" << mk_ismt2_pp(fml, m) << "\n";); 862 } 863 reset()864 void reset() { 865 m_nnf_core.reset(); 866 m_normalize_literals.reset(); 867 } 868 }; 869 get_nnf(expr_ref & fml,i_expr_pred & pred,i_nnf_atom & mk_atom,atom_set & pos,atom_set & neg)870 void get_nnf(expr_ref& fml, i_expr_pred& pred, i_nnf_atom& mk_atom, atom_set& pos, atom_set& neg) { 871 nnf_normalizer nnf(fml.get_manager(), pred, mk_atom); 872 nnf(fml, pos, neg); 873 } 874 875 // 876 // Theory plugin for quantifier elimination. 877 // 878 879 class quant_elim { 880 public: ~quant_elim()881 virtual ~quant_elim() {} 882 883 virtual lbool eliminate_exists( 884 unsigned num_vars, app* const* vars, 885 expr_ref& fml, app_ref_vector& free_vars, bool get_first, guarded_defs* defs) = 0; 886 887 virtual void set_assumption(expr* fml) = 0; 888 889 virtual void collect_statistics(statistics & st) const = 0; 890 891 virtual void eliminate(bool is_forall, unsigned num_vars, app* const* vars, expr_ref& fml) = 0; 892 893 updt_params(params_ref const & p)894 virtual void updt_params(params_ref const& p) {} 895 896 }; 897 898 class search_tree { 899 typedef map<rational, unsigned, rational::hash_proc, rational::eq_proc> branch_map; 900 ast_manager& m; 901 app_ref_vector m_vars; // free variables 902 app_ref m_var; // 0 or selected free variable 903 def_vector m_def; // substitution for the variable eliminated relative to the parent. 904 expr_ref m_fml; // formula whose variables are to be eliminated 905 app_ref m_assignment; // assignment that got us here. 906 search_tree* m_parent; // parent pointer 907 rational m_num_branches; // number of possible branches 908 ptr_vector<search_tree> m_children; // list of children 909 branch_map m_branch_index; // branch_id -> child search tree index 910 atom_set m_pos; 911 atom_set m_neg; 912 bool m_pure; // is the node pure (no variables deleted). 913 914 // The invariant captures that search tree nodes are either 915 // - unit branches (with only one descendant), or 916 // - unassigned variable and formula 917 // - assigned formula, but unassigned variable for branching 918 // - assigned variable and formula with 0 or more branches. 919 // 920 #define CHECK_COND(_cond_) if (!(_cond_)) { TRACE("qe", tout << "violated: " << #_cond_ << "\n";); return false; } invariant() const921 bool invariant() const { 922 CHECK_COND(assignment()); 923 CHECK_COND(m_children.empty() || fml()); 924 CHECK_COND(!is_root() || fml()); 925 CHECK_COND(!fml() || has_var() || m_num_branches.is_zero() || is_unit()); 926 for (auto const & kv : m_branch_index) { 927 CHECK_COND(kv.m_value < m_children.size()); 928 CHECK_COND(kv.m_key < get_num_branches()); 929 } 930 for (unsigned i = 0; i < m_children.size(); ++i) { 931 CHECK_COND(m_children[i]); 932 CHECK_COND(this == m_children[i]->m_parent); 933 CHECK_COND(m_children[i]->invariant()); 934 } 935 return true; 936 } 937 #undef CHECKC_COND 938 939 public: search_tree(search_tree * parent,ast_manager & m,app * assignment)940 search_tree(search_tree* parent, ast_manager& m, app* assignment): 941 m(m), 942 m_vars(m), 943 m_var(m), 944 m_def(m), 945 m_fml(m), 946 m_assignment(assignment, m), 947 m_parent(parent), 948 m_pure(true) 949 {} 950 ~search_tree()951 ~search_tree() { 952 reset(); 953 } 954 fml() const955 expr* fml() const { return m_fml; } 956 fml_ref()957 expr_ref& fml_ref() { return m_fml; } 958 def() const959 def_vector const& def() const { return m_def; } 960 assignment() const961 app* assignment() const { return m_assignment; } 962 var() const963 app* var() const { SASSERT(has_var()); return m_var; } 964 has_var() const965 bool has_var() const { return nullptr != m_var.get(); } 966 parent() const967 search_tree* parent() const { return m_parent; } 968 is_root() const969 bool is_root() const { return !parent(); } 970 get_num_branches() const971 rational const& get_num_branches() const { SASSERT(has_var()); return m_num_branches; } 972 973 // extract disjunctions get_leaves(expr_ref_vector & result)974 void get_leaves(expr_ref_vector& result) { 975 SASSERT(is_root()); 976 ptr_vector<search_tree> todo; 977 todo.push_back(this); 978 while (!todo.empty()) { 979 search_tree* st = todo.back(); 980 todo.pop_back(); 981 if (st->m_children.empty() && st->fml() && 982 st->m_vars.empty() && !st->has_var()) { 983 TRACE("qe", st->display(tout << "appending leaf\n");); 984 result.push_back(st->fml()); 985 } 986 for (auto * ch : st->m_children) 987 todo.push_back(ch); 988 } 989 } 990 get_leaves_rec(def_vector & defs,guarded_defs & gdefs)991 void get_leaves_rec(def_vector& defs, guarded_defs& gdefs) { 992 expr* f = this->fml(); 993 unsigned sz = defs.size(); 994 defs.append(def()); 995 if (m_children.empty() && f && !m.is_false(f) && 996 m_vars.empty() && !has_var()) { 997 gdefs.add(f, defs); 998 } 999 else { 1000 for (unsigned i = 0; i < m_children.size(); ++i) { 1001 m_children[i]->get_leaves_rec(defs, gdefs); 1002 } 1003 } 1004 defs.shrink(sz); 1005 } 1006 get_leaves(guarded_defs & gdefs)1007 void get_leaves(guarded_defs& gdefs) { 1008 def_vector defs(m); 1009 get_leaves_rec(defs, gdefs); 1010 } 1011 reset()1012 void reset() { 1013 TRACE("qe",tout << "resetting\n";); 1014 for (auto* ch : m_children) dealloc(ch); 1015 m_pos.reset(); 1016 m_neg.reset(); 1017 m_children.reset(); 1018 m_vars.reset(); 1019 m_branch_index.reset(); 1020 m_var = nullptr; 1021 m_def.reset(); 1022 m_num_branches = rational::zero(); 1023 m_pure = true; 1024 } 1025 init(expr * fml)1026 void init(expr* fml) { 1027 m_fml = fml; 1028 SASSERT(invariant()); 1029 } 1030 add_def(app * v,expr * def)1031 void add_def(app* v, expr* def) { 1032 if (v && def) { 1033 m_def.push_back(v->get_decl(), def); 1034 } 1035 } 1036 num_free_vars() const1037 unsigned num_free_vars() const { return m_vars.size(); } 1038 // app* const* free_vars() const { return m_vars.c_ptr(); } free_vars() const1039 app_ref_vector const& free_vars() const { return m_vars; } free_var(unsigned i) const1040 app* free_var(unsigned i) const { return m_vars[i]; } reset_free_vars()1041 void reset_free_vars() { TRACE("qe", tout << m_vars << "\n";); m_vars.reset(); } 1042 pos_atoms() const1043 atom_set const& pos_atoms() const { return m_pos; } neg_atoms() const1044 atom_set const& neg_atoms() const { return m_neg; } 1045 pos_atoms()1046 atom_set& pos_atoms() { return m_pos; } neg_atoms()1047 atom_set& neg_atoms() { return m_neg; } 1048 1049 // set the branch variable. set_var(app * x,rational const & num_branches)1050 void set_var(app* x, rational const& num_branches) { 1051 SASSERT(!m_var.get()); 1052 SASSERT(m_vars.contains(x)); 1053 m_var = x; 1054 m_vars.erase(x); 1055 m_num_branches = num_branches; 1056 SASSERT(invariant()); 1057 } 1058 1059 // include new variables. consume_vars(app_ref_vector & vars)1060 void consume_vars(app_ref_vector& vars) { 1061 while (!vars.empty()) { 1062 m_vars.push_back(vars.back()); 1063 vars.pop_back(); 1064 } 1065 } 1066 is_pure() const1067 bool is_pure() const { 1068 search_tree const* node = this; 1069 while (node) { 1070 if (!node->m_pure) return false; 1071 node = node->parent(); 1072 } 1073 return true; 1074 } 1075 is_unit() const1076 bool is_unit() const { 1077 return m_children.size() == 1 && 1078 m_branch_index.empty(); 1079 } 1080 has_branch(rational const & branch_id) const1081 bool has_branch(rational const& branch_id) const { return m_branch_index.contains(branch_id); } 1082 child(rational const & branch_id) const1083 search_tree* child(rational const& branch_id) const { 1084 unsigned idx = m_branch_index.find(branch_id); 1085 return m_children[idx]; 1086 } 1087 child() const1088 search_tree* child() const { 1089 SASSERT(is_unit()); 1090 return m_children[0]; 1091 } 1092 1093 // remove variable from branch. del_var(app * x)1094 void del_var(app* x) { 1095 SASSERT(m_children.empty()); 1096 SASSERT(m_vars.contains(x)); 1097 m_vars.erase(x); 1098 m_pure = false; 1099 } 1100 1101 // add branch with a given formula add_child(expr * fml)1102 search_tree* add_child(expr* fml) { 1103 SASSERT(m_branch_index.empty()); 1104 SASSERT(m_children.empty()); 1105 m_num_branches = rational(1); 1106 search_tree* st = alloc(search_tree, this, m, m.mk_true()); 1107 m_children.push_back(st); 1108 st->init(fml); 1109 st->m_vars.append(m_vars.size(), m_vars.c_ptr()); 1110 SASSERT(invariant()); 1111 TRACE("qe", display_node(tout); st->display_node(tout);); 1112 return st; 1113 } 1114 add_child(rational const & branch_id,app * assignment)1115 search_tree* add_child(rational const& branch_id, app* assignment) { 1116 SASSERT(!m_branch_index.contains(branch_id)); 1117 SASSERT(has_var()); 1118 SASSERT(branch_id.is_nonneg() && branch_id < m_num_branches); 1119 unsigned index = m_children.size(); 1120 search_tree* st = alloc(search_tree, this, m, assignment); 1121 m_children.push_back(st); 1122 m_branch_index.insert(branch_id, index); 1123 st->m_vars.append(m_vars.size(), m_vars.c_ptr()); 1124 SASSERT(invariant()); 1125 TRACE("qe", display_node(tout); st->display_node(tout);); 1126 return st; 1127 } 1128 display(std::ostream & out) const1129 void display(std::ostream& out) const { 1130 display(out, ""); 1131 } 1132 display_node(std::ostream & out,char const * indent="") const1133 void display_node(std::ostream& out, char const* indent = "") const { 1134 out << indent << "node " << std::hex << this << std::dec << "\n"; 1135 if (m_var) { 1136 out << indent << " var: " << m_var << "\n"; 1137 } 1138 for (app* v : m_vars) { 1139 out << indent << " free: " << mk_pp(v, m) << "\n"; 1140 } 1141 if (m_fml) { 1142 out << indent << " fml: " << m_fml << "\n"; 1143 } 1144 for (unsigned i = 0; i < m_def.size(); ++i) { 1145 out << indent << " def: " << m_def.var(i)->get_name() << " = " << mk_ismt2_pp(m_def.def(i), m) << "\n"; 1146 } 1147 out << indent << " branches: " << m_num_branches << "\n"; 1148 } 1149 display(std::ostream & out,char const * indent) const1150 void display(std::ostream& out, char const* indent) const { 1151 display_node(out, indent); 1152 std::string new_indent(indent); 1153 new_indent += " "; 1154 for (auto * ch : m_children) { 1155 ch->display(out, new_indent.c_str()); 1156 } 1157 } 1158 abstract_variable(app * x,expr * fml) const1159 expr_ref abstract_variable(app* x, expr* fml) const { 1160 expr_ref result(m); 1161 expr* y = x; 1162 expr_abstract(m, 0, 1, &y, fml, result); 1163 symbol X(x->get_decl()->get_name()); 1164 sort* s = m.get_sort(x); 1165 result = m.mk_exists(1, &s, &X, result); 1166 return result; 1167 } 1168 display_validate(std::ostream & out) const1169 void display_validate(std::ostream& out) const { 1170 if (m_children.empty()) { 1171 return; 1172 } 1173 expr_ref q(m); 1174 expr* x = m_var; 1175 if (x) { 1176 q = abstract_variable(m_var, m_fml); 1177 1178 expr_ref_vector fmls(m); 1179 expr_ref fml(m); 1180 for (unsigned i = 0; i < m_children.size(); ++i) { 1181 search_tree const& child = *m_children[i]; 1182 fml = child.fml(); 1183 if (fml) { 1184 // abstract free variables in children. 1185 ptr_vector<app> child_vars, new_vars; 1186 child_vars.append(child.m_vars.size(), child.m_vars.c_ptr()); 1187 if (child.m_var) { 1188 child_vars.push_back(child.m_var); 1189 } 1190 for (unsigned j = 0; j < child_vars.size(); ++j) { 1191 if (!m_vars.contains(child_vars[j]) && 1192 !new_vars.contains(child_vars[j])) { 1193 fml = abstract_variable(child_vars[j], fml); 1194 new_vars.push_back(child_vars[j]); 1195 } 1196 } 1197 fmls.push_back(fml); 1198 } 1199 } 1200 bool_rewriter(m).mk_or(fmls.size(), fmls.c_ptr(), fml); 1201 1202 fml = mk_not(m, m.mk_iff(q, fml)); 1203 ast_smt_pp pp(m); 1204 out << "; eliminate " << mk_pp(m_var, m) << "\n"; 1205 out << "(push 1)\n"; 1206 pp.display_smt2(out, fml); 1207 out << "(pop 1)\n\n"; 1208 #if 0 1209 DEBUG_CODE( 1210 smt_params params; 1211 params.m_simplify_bit2int = true; 1212 params.m_arith_enum_const_mod = true; 1213 params.m_bv_enable_int2bv2int = true; 1214 params.m_relevancy_lvl = 0; 1215 smt::kernel ctx(m, params); 1216 ctx.assert_expr(fml); 1217 lbool is_sat = ctx.check(); 1218 if (is_sat == l_true) { 1219 std::cout << "; Validation failed:\n"; 1220 std::cout << mk_pp(fml, m) << "\n"; 1221 } 1222 ); 1223 #endif 1224 1225 } 1226 for (unsigned i = 0; i < m_children.size(); ++i) { 1227 if (m_children[i]->fml()) { 1228 m_children[i]->display_validate(out); 1229 } 1230 } 1231 } 1232 }; 1233 1234 // ------------------------- 1235 // i_solver_context 1236 ~i_solver_context()1237 i_solver_context::~i_solver_context() { 1238 for (unsigned i = 0; i < m_plugins.size(); ++i) { 1239 dealloc(m_plugins[i]); 1240 } 1241 } 1242 operator ()(expr * e)1243 bool i_solver_context::is_relevant::operator()(expr* e) { 1244 for (unsigned i = 0; i < m_s.get_num_vars(); ++i) { 1245 if (m_s.contains(i)(e)) { 1246 return true; 1247 } 1248 } 1249 TRACE("qe_verbose", tout << "Not relevant: " << mk_ismt2_pp(e, m_s.get_manager()) << "\n";); 1250 return false; 1251 } 1252 is_var(expr * x,unsigned & idx) const1253 bool i_solver_context::is_var(expr* x, unsigned& idx) const { 1254 unsigned nv = get_num_vars(); 1255 for (unsigned i = 0; i < nv; ++i) { 1256 if (get_var(i) == x) { 1257 idx = i; 1258 return true; 1259 } 1260 } 1261 return false; 1262 } 1263 add_plugin(qe_solver_plugin * p)1264 void i_solver_context::add_plugin(qe_solver_plugin* p) { 1265 family_id fid = p->get_family_id(); 1266 SASSERT(fid != null_family_id); 1267 if (static_cast<int>(m_plugins.size()) <= fid) { 1268 m_plugins.resize(fid+1); 1269 } 1270 SASSERT(!m_plugins[fid]); 1271 m_plugins[fid] = p; 1272 } 1273 has_plugin(app * x)1274 bool i_solver_context::has_plugin(app* x) { 1275 ast_manager& m = get_manager(); 1276 family_id fid = m.get_sort(x)->get_family_id(); 1277 return 1278 0 <= fid && 1279 fid < static_cast<int>(m_plugins.size()) && 1280 m_plugins[fid] != 0; 1281 } 1282 plugin(app * x)1283 qe_solver_plugin& i_solver_context::plugin(app* x) { 1284 ast_manager& m = get_manager(); 1285 SASSERT(has_plugin(x)); 1286 return *(m_plugins[m.get_sort(x)->get_family_id()]); 1287 } 1288 mk_atom(expr * e,bool p,expr_ref & result)1289 void i_solver_context::mk_atom(expr* e, bool p, expr_ref& result) { 1290 ast_manager& m = get_manager(); 1291 TRACE("qe_verbose", tout << mk_ismt2_pp(e, m) << "\n";); 1292 for (unsigned i = 0; i < m_plugins.size(); ++i) { 1293 qe_solver_plugin* pl = m_plugins[i]; 1294 if (pl && pl->mk_atom(e, p, result)) { 1295 return; 1296 } 1297 } 1298 TRACE("qe_verbose", tout << "No plugin for " << mk_ismt2_pp(e, m) << "\n";); 1299 result = p?e:mk_not(m, e); 1300 } 1301 operator ()(expr * e,bool p,expr_ref & result)1302 void i_solver_context::mk_atom_fn::operator()(expr* e, bool p, expr_ref& result) { 1303 m_s.mk_atom(e, p, result); 1304 } 1305 collect_statistics(statistics & st) const1306 void i_solver_context::collect_statistics(statistics& st) const { 1307 // tbd 1308 } 1309 1310 typedef ref_vector_ptr_hash<expr, ast_manager> expr_ref_vector_hash; 1311 typedef ref_vector_ptr_eq<expr, ast_manager> expr_ref_vector_eq; 1312 typedef hashtable<expr_ref_vector*, expr_ref_vector_hash, expr_ref_vector_eq> clause_table; 1313 typedef value_trail<smt::context, unsigned> _value_trail; 1314 1315 1316 class quant_elim_plugin : public i_solver_context { 1317 1318 ast_manager& m; 1319 quant_elim& m_qe; 1320 th_rewriter m_rewriter; 1321 smt::kernel m_solver; 1322 bv_util m_bv; 1323 expr_ref_vector m_literals; 1324 1325 bool_rewriter m_bool_rewriter; 1326 conjunctions m_conjs; 1327 1328 // maintain queue for variables. 1329 1330 app_ref_vector m_free_vars; // non-quantified variables 1331 app_ref_vector m_trail; 1332 1333 expr_ref m_fml; 1334 expr_ref m_subfml; 1335 1336 obj_map<app, app*> m_var2branch; // var -> bv-var, identify explored branch. 1337 obj_map<app, contains_app*> m_var2contains; // var -> contains_app 1338 obj_map<app, ptr_vector<app> > m_children; // var -> list of dependent children 1339 search_tree m_root; 1340 search_tree* m_current; // current branch 1341 1342 vector<unsigned_vector> m_partition; // cached latest partition of variables. 1343 1344 app_ref_vector m_new_vars; // variables added by solvers 1345 bool m_get_first; // get first satisfying branch. 1346 guarded_defs* m_defs; 1347 nnf_normalizer m_nnf; // nnf conversion 1348 1349 1350 public: 1351 quant_elim_plugin(ast_manager & m,quant_elim & qe,smt_params & p)1352 quant_elim_plugin(ast_manager& m, quant_elim& qe, smt_params& p): 1353 m(m), 1354 m_qe(qe), 1355 m_rewriter(m), 1356 m_solver(m, p), 1357 m_bv(m), 1358 m_literals(m), 1359 m_bool_rewriter(m), 1360 m_conjs(m), 1361 m_free_vars(m), 1362 m_trail(m), 1363 m_fml(m), 1364 m_subfml(m), 1365 m_root(nullptr, m, m.mk_true()), 1366 m_current(nullptr), 1367 m_new_vars(m), 1368 m_get_first(false), 1369 m_defs(nullptr), 1370 m_nnf(m, get_is_relevant(), get_mk_atom()) 1371 { 1372 params_ref params; 1373 params.set_bool("gcd_rounding", true); 1374 m_rewriter.updt_params(params); 1375 } 1376 ~quant_elim_plugin()1377 ~quant_elim_plugin() override { 1378 reset(); 1379 } 1380 reset()1381 void reset() { 1382 m_free_vars.reset(); 1383 m_trail.reset(); 1384 for (auto & kv : m_var2contains) { 1385 dealloc(kv.m_value); 1386 } 1387 m_var2contains.reset(); 1388 m_var2branch.reset(); 1389 m_root.reset(); 1390 m_new_vars.reset(); 1391 m_fml = nullptr; 1392 m_defs = nullptr; 1393 m_nnf.reset(); 1394 } 1395 add_plugin(qe_solver_plugin * p)1396 void add_plugin(qe_solver_plugin* p) { 1397 i_solver_context::add_plugin(p); 1398 m_conjs.add_plugin(p); 1399 } 1400 check(unsigned num_vars,app * const * vars,expr * assumption,expr_ref & fml,bool get_first,app_ref_vector & free_vars,guarded_defs * defs)1401 void check(unsigned num_vars, app* const* vars, 1402 expr* assumption, expr_ref& fml, bool get_first, 1403 app_ref_vector& free_vars, guarded_defs* defs) { 1404 1405 reset(); 1406 m_solver.push(); 1407 m_get_first = get_first; 1408 m_defs = defs; 1409 for (unsigned i = 0; i < num_vars; ++i) { 1410 if (has_plugin(vars[i])) { 1411 add_var(vars[i]); 1412 } 1413 else { 1414 m_free_vars.push_back(vars[i]); 1415 } 1416 } 1417 m_root.consume_vars(m_new_vars); 1418 m_current = &m_root; 1419 1420 // set sub-formula 1421 m_fml = fml; 1422 normalize(m_fml, m_root.pos_atoms(), m_root.neg_atoms()); 1423 expr_ref f(m_fml); 1424 get_max_relevant(get_is_relevant(), f, m_subfml); 1425 if (f.get() != m_subfml.get()) { 1426 m_fml = f; 1427 f = m_subfml; 1428 m_solver.assert_expr(f); 1429 } 1430 m_root.init(f); 1431 TRACE("qe", 1432 for (unsigned i = 0; i < num_vars; ++i) tout << mk_ismt2_pp(vars[i], m) << "\n"; 1433 tout << mk_ismt2_pp(f, m) << "\n";); 1434 1435 m_solver.assert_expr(m_fml); 1436 if (assumption) m_solver.assert_expr(assumption); 1437 bool is_sat = false; 1438 lbool res = l_true; 1439 while (res == l_true) { 1440 res = m_solver.check(); 1441 if (res == l_true && has_uninterpreted(m, m_fml)) 1442 res = l_undef; 1443 if (res == l_true) { 1444 is_sat = true; 1445 final_check(); 1446 } 1447 else { 1448 break; 1449 } 1450 } 1451 if (res == l_undef) { 1452 free_vars.append(num_vars, vars); 1453 reset(); 1454 m_solver.pop(1); 1455 return; 1456 } 1457 1458 if (!is_sat) { 1459 fml = m.mk_false(); 1460 if (m_fml.get() != m_subfml.get()) { 1461 scoped_ptr<expr_replacer> rp = mk_default_expr_replacer(m, false); 1462 rp->apply_substitution(to_app(m_subfml.get()), fml, m_fml); 1463 fml = m_fml; 1464 } 1465 reset(); 1466 m_solver.pop(1); 1467 return; 1468 } 1469 1470 if (!get_first) { 1471 expr_ref_vector result(m); 1472 m_root.get_leaves(result); 1473 m_bool_rewriter.mk_or(result.size(), result.c_ptr(), fml); 1474 } 1475 1476 if (defs) { 1477 m_root.get_leaves(*defs); 1478 defs->project(num_vars, vars); 1479 } 1480 1481 TRACE("qe", 1482 tout << "result:" << mk_ismt2_pp(fml, m) << "\n"; 1483 tout << "input: " << mk_ismt2_pp(m_fml, m) << "\n"; 1484 tout << "subformula: " << mk_ismt2_pp(m_subfml, m) << "\n"; 1485 m_root.display(tout); 1486 m_root.display_validate(tout); 1487 tout << "free: " << m_free_vars << "\n";); 1488 1489 free_vars.append(m_free_vars); 1490 if (!m_free_vars.empty() || m_solver.inconsistent()) { 1491 1492 if (m_fml.get() != m_subfml.get()) { 1493 scoped_ptr<expr_replacer> rp = mk_default_expr_replacer(m, false); 1494 rp->apply_substitution(to_app(m_subfml.get()), fml, m_fml); 1495 fml = m_fml; 1496 } 1497 } 1498 reset(); 1499 m_solver.pop(1); 1500 f = nullptr; 1501 } 1502 collect_statistics(statistics & st)1503 void collect_statistics(statistics& st) { 1504 m_solver.collect_statistics(st); 1505 } 1506 1507 private: 1508 final_check()1509 void final_check() { 1510 model_ref model; 1511 m_solver.get_model(model); 1512 scoped_ptr<model_evaluator> model_eval = alloc(model_evaluator, *model); 1513 1514 while (true) { 1515 TRACE("qe", model_v2_pp(tout, *model);); 1516 while (can_propagate_assignment(*model_eval)) { 1517 propagate_assignment(*model_eval); 1518 } 1519 VERIFY(CHOOSE_VAR == update_current(*model_eval, true)); 1520 SASSERT(m_current->fml()); 1521 if (l_true != m_solver.check()) { 1522 return; 1523 } 1524 m_solver.get_model(model); 1525 model_eval = alloc(model_evaluator, *model); 1526 search_tree* st = m_current; 1527 update_current(*model_eval, false); 1528 if (st == m_current) { 1529 break; 1530 } 1531 } 1532 pop(*model_eval); 1533 } 1534 get_manager()1535 ast_manager& get_manager() override { return m; } 1536 pos_atoms() const1537 atom_set const& pos_atoms() const override { return m_current->pos_atoms(); } 1538 neg_atoms() const1539 atom_set const& neg_atoms() const override { return m_current->neg_atoms(); } 1540 get_num_vars() const1541 unsigned get_num_vars() const override { return m_current->num_free_vars(); } 1542 get_var(unsigned idx) const1543 app* get_var(unsigned idx) const override { return m_current->free_var(idx); } 1544 get_vars() const1545 app_ref_vector const& get_vars() const override { return m_current->free_vars(); } 1546 contains(unsigned idx)1547 contains_app& contains(unsigned idx) override { return contains(get_var(idx)); } 1548 1549 // 1550 // The variable at idx is eliminated (without branching). 1551 // elim_var(unsigned idx,expr * _fml,expr * def)1552 void elim_var(unsigned idx, expr* _fml, expr* def) override { 1553 app* x = get_var(idx); 1554 expr_ref fml(_fml, m); 1555 TRACE("qe", tout << mk_pp(x,m) << " " << mk_pp(def, m) << "\n";); 1556 m_current->set_var(x, rational(1)); 1557 m_current = m_current->add_child(fml); 1558 m_current->add_def(x, def); 1559 m_current->consume_vars(m_new_vars); 1560 normalize(*m_current); 1561 } 1562 add_var(app * x)1563 void add_var(app* x) override { 1564 m_new_vars.push_back(x); 1565 if (m_var2branch.contains(x)) { 1566 return; 1567 } 1568 contains_app* ca = alloc(contains_app, m, x); 1569 m_var2contains.insert(x, ca); 1570 app* bv = nullptr; 1571 if (m.is_bool(x) || m_bv.is_bv(x)) { 1572 bv = x; 1573 } 1574 else { 1575 bv = m.mk_fresh_const("b", m_bv.mk_sort(20)); 1576 m_trail.push_back(bv); 1577 } 1578 TRACE("qe", tout << "Add branch var: " << mk_ismt2_pp(x, m) << " " << mk_ismt2_pp(bv, m) << "\n";); 1579 m_var2branch.insert(x, bv); 1580 } 1581 add_constraint(bool use_current_val,expr * l1=nullptr,expr * l2=nullptr,expr * l3=nullptr)1582 void add_constraint(bool use_current_val, expr* l1 = nullptr, expr* l2 = nullptr, expr* l3 = nullptr) override { 1583 search_tree* node = m_current; 1584 expr_ref _l1(l1, m), _l2(l2, m), _l3(l3, m); 1585 if (!use_current_val) { 1586 node = m_current->parent(); 1587 } 1588 m_literals.reset(); 1589 while (node) { 1590 m_literals.push_back(mk_not(m, node->assignment())); 1591 node = node->parent(); 1592 } 1593 add_literal(l1); 1594 add_literal(l2); 1595 add_literal(l3); 1596 expr_ref fml(m); 1597 fml = m.mk_or(m_literals); 1598 TRACE("qe", tout << fml << "\n";); 1599 m_solver.assert_expr(fml); 1600 } 1601 blast_or(app * var,expr_ref & fml)1602 void blast_or(app* var, expr_ref& fml) override { 1603 m_qe.eliminate_exists(1, &var, fml, m_free_vars, false, nullptr); 1604 } 1605 eliminate_exists(unsigned num_vars,app * const * vars,expr_ref & fml,bool get_first,guarded_defs * defs)1606 lbool eliminate_exists(unsigned num_vars, app* const* vars, expr_ref& fml, bool get_first, guarded_defs* defs) { 1607 return m_qe.eliminate_exists(num_vars, vars, fml, m_free_vars, get_first, defs); 1608 } 1609 1610 private: 1611 add_literal(expr * l)1612 void add_literal(expr* l) { 1613 if (l != nullptr) { 1614 m_literals.push_back(l); 1615 } 1616 } 1617 get_max_relevant(i_expr_pred & is_relevant,expr_ref & fml,expr_ref & subfml)1618 void get_max_relevant(i_expr_pred& is_relevant, expr_ref& fml, expr_ref& subfml) { 1619 if (m.is_and(fml) || m.is_or(fml)) { 1620 app* a = to_app(fml); 1621 unsigned num_args = a->get_num_args(); 1622 ptr_buffer<expr> r_args; 1623 ptr_buffer<expr> i_args; 1624 for (unsigned i = 0; i < num_args; ++i) { 1625 expr* arg = a->get_arg(i); 1626 if (is_relevant(arg)) { 1627 r_args.push_back(arg); 1628 } 1629 else { 1630 i_args.push_back(arg); 1631 } 1632 } 1633 if (r_args.empty() || i_args.empty()) { 1634 subfml = fml; 1635 } 1636 else if (r_args.size() == 1) { 1637 expr_ref tmp(r_args[0], m); 1638 get_max_relevant(is_relevant, tmp, subfml); 1639 i_args.push_back(tmp); 1640 fml = m.mk_app(a->get_decl(), i_args.size(), i_args.c_ptr()); 1641 } 1642 else { 1643 subfml = m.mk_app(a->get_decl(), r_args.size(), r_args.c_ptr()); 1644 i_args.push_back(subfml); 1645 fml = m.mk_app(a->get_decl(), i_args.size(), i_args.c_ptr()); 1646 } 1647 } 1648 else { 1649 subfml = fml; 1650 } 1651 } 1652 get_branch_id(app * x)1653 app* get_branch_id(app* x) { 1654 return m_var2branch[x]; 1655 } 1656 extract_partition(ptr_vector<app> & vars)1657 bool extract_partition(ptr_vector<app>& vars) { 1658 if (m_partition.empty()) { 1659 return false; 1660 } 1661 1662 unsigned_vector& vec = m_partition.back();; 1663 for (unsigned i = 0; i < vec.size(); ++i) { 1664 vars.push_back(m_current->free_var(vec[i])); 1665 } 1666 m_partition.pop_back(); 1667 return true; 1668 } 1669 1670 enum update_status { CHOOSE_VAR, NEED_PROPAGATION }; 1671 update_current(model_evaluator & model_eval,bool apply)1672 update_status update_current(model_evaluator& model_eval, bool apply) { 1673 SASSERT(m_fml); 1674 m_current = &m_root; 1675 rational branch, nb; 1676 while (true) { 1677 SASSERT(m_current->fml()); 1678 if (m_current->is_unit()) { 1679 m_current = m_current->child(); 1680 continue; 1681 } 1682 if (!m_current->has_var()) { 1683 return CHOOSE_VAR; 1684 } 1685 1686 app* x = m_current->var(); 1687 app* b = get_branch_id(x); 1688 nb = m_current->get_num_branches(); 1689 expr_ref fml(m_current->fml(), m); 1690 if (!eval(model_eval, b, branch) || branch >= nb) { 1691 TRACE("qe", tout << "evaluation failed: setting branch to 0\n";); 1692 branch = rational::zero(); 1693 } 1694 SASSERT(!branch.is_neg()); 1695 if (!m_current->has_branch(branch)) { 1696 if (apply) { 1697 app_ref assignment(mk_eq_value(b, branch), m); 1698 m_current = m_current->add_child(branch, assignment); 1699 plugin(x).assign(contains(x), fml, branch); 1700 m_current->consume_vars(m_new_vars); 1701 } 1702 return NEED_PROPAGATION; 1703 } 1704 m_current = m_current->child(branch); 1705 if (m_current->fml() == nullptr) { 1706 SASSERT(!m_current->has_var()); 1707 if (apply) { 1708 expr_ref def(m); 1709 plugin(x).subst(contains(x), branch, fml, m_defs?&def:nullptr); 1710 SASSERT(!contains(x)(fml)); 1711 m_current->consume_vars(m_new_vars); 1712 m_current->init(fml); 1713 m_current->add_def(x, def); 1714 normalize(*m_current); 1715 } 1716 return CHOOSE_VAR; 1717 } 1718 } 1719 } 1720 pop(model_evaluator & model_eval)1721 void pop(model_evaluator& model_eval) { 1722 // 1723 // Eliminate trivial quantifiers by solving 1724 // variables that can be eliminated. 1725 // 1726 solve_vars(); 1727 expr* fml = m_current->fml(); 1728 // we are done splitting. 1729 if (m_current->num_free_vars() == 0) { 1730 block_assignment(); 1731 return; 1732 } 1733 1734 expr_ref fml_closed(m), fml_open(m), fml_mixed(m); 1735 unsigned num_vars = m_current->num_free_vars(); 1736 ptr_vector<contains_app> cont; 1737 ptr_vector<app> vars; 1738 for (unsigned i = 0; i < num_vars; ++i) { 1739 cont.push_back(&contains(i)); 1740 vars.push_back(m_current->free_var(i)); 1741 } 1742 m_conjs.get_partition(fml, num_vars, vars.c_ptr(), fml_closed, fml_mixed, fml_open); 1743 if (m.is_and(fml_open) && 1744 m_conjs.partition_vars( 1745 num_vars, cont.c_ptr(), 1746 to_app(fml_open)->get_num_args(), to_app(fml_open)->get_args(), 1747 m_partition)) { 1748 process_partition(); 1749 return; 1750 } 1751 1752 // 1753 // The closed portion of the formula 1754 // can be used as the quantifier-free portion, 1755 // unless the current state is unsatisfiable. 1756 // 1757 if (m.is_true(fml_mixed)) { 1758 SASSERT(l_false != m_solver.check()); 1759 m_current = m_current->add_child(fml_closed); 1760 for (unsigned i = 0; m_defs && i < m_current->num_free_vars(); ++i) { 1761 expr_ref val(m); 1762 app* x = m_current->free_var(i); 1763 model_eval(x, val); 1764 // hack: assign may add new variables to the branch. 1765 if (val == x) { 1766 model_ref model; 1767 lbool is_sat = m_solver.check(); 1768 if (is_sat == l_undef) return; 1769 m_solver.get_model(model); 1770 SASSERT(is_sat == l_true); 1771 model_evaluator model_eval2(*model); 1772 model_eval2.set_model_completion(true); 1773 model_eval2(x, val); 1774 } 1775 TRACE("qe", tout << mk_pp(x,m) << " " << mk_pp(val, m) << "\n";); 1776 m_current->add_def(x, val); 1777 } 1778 m_current->reset_free_vars(); 1779 block_assignment(); 1780 return; 1781 } 1782 // 1783 // one variable is to be processed. 1784 // 1785 constrain_assignment(); 1786 } 1787 normalize(search_tree & st)1788 void normalize(search_tree& st) { 1789 normalize(st.fml_ref(), st.pos_atoms(), st.neg_atoms()); 1790 } 1791 normalize(expr_ref & result,atom_set & pos,atom_set & neg)1792 void normalize(expr_ref& result, atom_set& pos, atom_set& neg) { 1793 m_rewriter(result); 1794 bool simplified = true; 1795 while (simplified) { 1796 simplified = false; 1797 for (unsigned i = 0; !simplified && i < m_plugins.size(); ++i) { 1798 qe_solver_plugin* pl = m_plugins[i]; 1799 simplified = pl && pl->simplify(result); 1800 } 1801 } 1802 TRACE("qe_verbose", tout << "simp: " << mk_ismt2_pp(result.get(), m) << "\n";); 1803 m_nnf(result, pos, neg); 1804 TRACE("qe", tout << "nnf: " << mk_ismt2_pp(result.get(), m) << "\n";); 1805 } 1806 1807 // 1808 // variable queuing. 1809 // 1810 1811 1812 // ------------------------------------------------ 1813 // propagate the assignments to branch 1814 // literals to implied constraints on the 1815 // variable. 1816 // 1817 get_propagate_value(model_evaluator & model_eval,search_tree * node,app * & b,rational & b_val)1818 bool get_propagate_value(model_evaluator& model_eval, search_tree* node, app*& b, rational& b_val) { 1819 return node->has_var() && eval(model_eval, get_branch_id(node->var()), b_val); 1820 } 1821 can_propagate_assignment(model_evaluator & model_eval)1822 bool can_propagate_assignment(model_evaluator& model_eval) { 1823 return m_fml && NEED_PROPAGATION == update_current(model_eval, false); 1824 } 1825 propagate_assignment(model_evaluator & model_eval)1826 void propagate_assignment(model_evaluator& model_eval) { 1827 if (m_fml) { 1828 update_current(model_eval, true); 1829 } 1830 } 1831 1832 // 1833 // evaluate the Boolean or bit-vector 'b' in 1834 // the current model 1835 // eval(model_evaluator & model_eval,app * b,rational & val)1836 bool eval(model_evaluator& model_eval, app* b, rational& val) { 1837 unsigned bv_size; 1838 expr_ref res(m); 1839 model_eval(b, res); 1840 SASSERT(m.is_bool(b) || m_bv.is_bv(b)); 1841 if (m.is_true(res)) { 1842 val = rational::one(); 1843 return true; 1844 } 1845 else if (m.is_false(res)) { 1846 val = rational::zero(); 1847 return true; 1848 } 1849 else if (m_bv.is_numeral(res, val, bv_size)) { 1850 return true; 1851 } 1852 else { 1853 return false; 1854 } 1855 } 1856 1857 // 1858 // create literal 'b = r' 1859 // mk_eq_value(app * b,rational const & vl)1860 app* mk_eq_value(app* b, rational const& vl) { 1861 if (m.is_bool(b)) { 1862 if (vl.is_zero()) return to_app(mk_not(m, b)); 1863 if (vl.is_one()) return b; 1864 UNREACHABLE(); 1865 } 1866 SASSERT(m_bv.is_bv(b)); 1867 app_ref value(m_bv.mk_numeral(vl, m_bv.get_bv_size(b)), m); 1868 return m.mk_eq(b, value); 1869 } 1870 1871 is_eq_value(app * e,app * & bv,rational & v)1872 bool is_eq_value(app* e, app*& bv, rational& v) { 1873 unsigned sz = 0; 1874 if (!m.is_eq(e)) return false; 1875 expr* e0 = e->get_arg(0), *e1 = e->get_arg(1); 1876 if (!m_bv.is_bv(e0)) return false; 1877 if (m_bv.is_numeral(e0, v, sz) && is_app(e1)) { 1878 bv = to_app(e1); 1879 return true; 1880 } 1881 if (m_bv.is_numeral(e1, v, sz) && is_app(e0)) { 1882 bv = to_app(e0); 1883 return true; 1884 } 1885 return false; 1886 } 1887 1888 1889 // 1890 // the current state is satisfiable. 1891 // all bound decisions have been made. 1892 // block_assignment()1893 void block_assignment() { 1894 TRACE("qe_verbose", m_solver.display(tout);); 1895 add_constraint(true); 1896 } 1897 1898 // 1899 // The variable v is to be assigned a value in a range. 1900 // constrain_assignment()1901 void constrain_assignment() { 1902 SASSERT(m_current->fml()); 1903 rational k; 1904 app* x; 1905 if (!find_min_weight(x, k)) { 1906 return; 1907 } 1908 1909 m_current->set_var(x, k); 1910 TRACE("qe", tout << mk_pp(x, m) << " := " << k << "\n";); 1911 if (m_bv.is_bv(x)) { 1912 return; 1913 } 1914 1915 app* b = get_branch_id(x); 1916 // 1917 // Create implication: 1918 // 1919 // assign_0 /\ ... /\ assign_{v-1} => b(v) <= k-1 1920 // where 1921 // - assign_i is the current assignment: i = b(i) 1922 // - k is the number of cases for v 1923 // 1924 1925 if (m.is_bool(b)) { 1926 SASSERT(k <= rational(2)); 1927 return; 1928 } 1929 1930 SASSERT(m_bv.is_bv(b)); 1931 SASSERT(k.is_pos()); 1932 app_ref max_val(m_bv.mk_numeral(k-rational::one(), m_bv.get_bv_size(b)), m); 1933 expr_ref ub(m_bv.mk_ule(b, max_val), m); 1934 add_constraint(true, ub); 1935 } 1936 1937 1938 1939 // 1940 // Process the partition stored in m_vars. 1941 // process_partition()1942 void process_partition() { 1943 expr_ref fml(m_current->fml(), m); 1944 ptr_vector<app> vars; 1945 bool closed = true; 1946 while (extract_partition(vars)) { 1947 lbool r = m_qe.eliminate_exists(vars.size(), vars.c_ptr(), fml, m_free_vars, m_get_first, m_defs); 1948 vars.reset(); 1949 closed = closed && (r != l_undef); 1950 } 1951 TRACE("qe", tout << fml << " free: " << m_current->free_vars() << "\n";); 1952 m_current->add_child(fml)->reset_free_vars(); 1953 block_assignment(); 1954 } 1955 1956 1957 // variable queueing. 1958 contains(app * x)1959 contains_app& contains(app* x) { 1960 return *m_var2contains[x]; 1961 } 1962 find_min_weight(app * & x,rational & num_branches)1963 bool find_min_weight(app*& x, rational& num_branches) { 1964 SASSERT(!m_current->has_var()); 1965 while (m_current->num_free_vars() > 0) { 1966 unsigned weight = UINT_MAX; 1967 unsigned nv = m_current->num_free_vars(); 1968 expr* fml = m_current->fml(); 1969 unsigned index = 0; 1970 for (unsigned i = 0; i < nv; ++i) { 1971 x = get_var(i); 1972 if (!has_plugin(x)) { 1973 break; 1974 } 1975 unsigned weight1 = plugin(get_var(i)).get_weight(contains(i), fml); 1976 if (weight1 < weight) { 1977 index = i; 1978 } 1979 } 1980 x = get_var(index); 1981 if (has_plugin(x) && 1982 plugin(x).get_num_branches(contains(x), fml, num_branches)) { 1983 return true; 1984 } 1985 TRACE("qe", tout << "setting variable " << mk_pp(x, m) << " free\n";); 1986 m_free_vars.push_back(x); 1987 m_current->del_var(x); 1988 } 1989 return false; 1990 } 1991 1992 // 1993 // Solve for variables in fml. 1994 // Add a unit branch when variables are solved. 1995 // solve_vars()1996 void solve_vars() { 1997 bool solved = true; 1998 while (solved) { 1999 expr_ref fml(m_current->fml(), m); 2000 TRACE("qe", tout << fml << "\n";); 2001 conj_enum conjs(m, fml); 2002 solved = false; 2003 for (unsigned i = 0; !solved && i < m_plugins.size(); ++i) { 2004 qe_solver_plugin* p = m_plugins[i]; 2005 solved = p && p->solve(conjs, fml); 2006 SASSERT(m_new_vars.empty()); 2007 } 2008 } 2009 } 2010 2011 }; 2012 2013 // ------------------------------------------------ 2014 // quant_elim 2015 2016 2017 class quant_elim_new : public quant_elim { 2018 ast_manager& m; 2019 smt_params& m_fparams; 2020 expr_ref m_assumption; 2021 bool m_produce_models; 2022 ptr_vector<quant_elim_plugin> m_plugins; 2023 bool m_eliminate_variables_as_block; 2024 2025 public: quant_elim_new(ast_manager & m,smt_params & p)2026 quant_elim_new(ast_manager& m, smt_params& p) : 2027 m(m), 2028 m_fparams(p), 2029 m_assumption(m), 2030 m_produce_models(m_fparams.m_model), 2031 m_eliminate_variables_as_block(true) 2032 { 2033 } 2034 ~quant_elim_new()2035 ~quant_elim_new() override { 2036 reset(); 2037 } 2038 reset()2039 void reset() { 2040 for (unsigned i = 0; i < m_plugins.size(); ++i) { 2041 dealloc(m_plugins[i]); 2042 } 2043 } 2044 checkpoint()2045 void checkpoint() { 2046 if (!m.inc()) 2047 throw tactic_exception(m.limit().get_cancel_msg()); 2048 } 2049 2050 collect_statistics(statistics & st) const2051 void collect_statistics(statistics & st) const override { 2052 for (unsigned i = 0; i < m_plugins.size(); ++i) { 2053 m_plugins[i]->collect_statistics(st); 2054 } 2055 } 2056 updt_params(params_ref const & p)2057 void updt_params(params_ref const& p) override { 2058 m_eliminate_variables_as_block = p.get_bool("eliminate_variables_as_block", m_eliminate_variables_as_block); 2059 } 2060 eliminate(bool is_forall,unsigned num_vars,app * const * vars,expr_ref & fml)2061 void eliminate(bool is_forall, unsigned num_vars, app* const* vars, expr_ref& fml) override { 2062 if (is_forall) { 2063 eliminate_forall_bind(num_vars, vars, fml); 2064 } 2065 else { 2066 eliminate_exists_bind(num_vars, vars, fml); 2067 } 2068 } 2069 bind_variables(unsigned num_vars,app * const * vars,expr_ref & fml)2070 virtual void bind_variables(unsigned num_vars, app* const* vars, expr_ref& fml) { 2071 if (num_vars > 0) { 2072 ptr_vector<sort> sorts; 2073 vector<symbol> names; 2074 app_ref_vector free_vars(m); 2075 for (unsigned i = 0; i < num_vars; ++i) { 2076 contains_app contains_x(m, vars[i]); 2077 if (contains_x(fml)) { 2078 sorts.push_back(m.get_sort(vars[i])); 2079 names.push_back(vars[i]->get_decl()->get_name()); 2080 free_vars.push_back(vars[i]); 2081 } 2082 } 2083 if (!free_vars.empty()) { 2084 expr_ref tmp = expr_abstract(free_vars, fml); 2085 fml = m.mk_exists(free_vars.size(), sorts.c_ptr(), names.c_ptr(), tmp, 1); 2086 } 2087 } 2088 } 2089 set_assumption(expr * fml)2090 void set_assumption(expr* fml) override { 2091 m_assumption = fml; 2092 } 2093 2094 eliminate_exists(unsigned num_vars,app * const * vars,expr_ref & fml,app_ref_vector & free_vars,bool get_first,guarded_defs * defs)2095 lbool eliminate_exists( 2096 unsigned num_vars, app* const* vars, expr_ref& fml, 2097 app_ref_vector& free_vars, bool get_first, guarded_defs* defs) override { 2098 if (get_first) { 2099 return eliminate_block(num_vars, vars, fml, free_vars, get_first, defs); 2100 } 2101 if (m_eliminate_variables_as_block) { 2102 return eliminate_block(num_vars, vars, fml, free_vars, get_first, defs); 2103 } 2104 for (unsigned i = 0; i < num_vars; ++i) { 2105 lbool r = eliminate_block(1, vars+i, fml, free_vars, get_first, defs); 2106 switch(r) { 2107 case l_false: 2108 return l_false; 2109 case l_undef: 2110 free_vars.append(num_vars-i-1,vars+1+i); 2111 return l_undef; 2112 default: 2113 break; 2114 } 2115 } 2116 return l_true; 2117 } 2118 2119 private: 2120 eliminate_block(unsigned num_vars,app * const * vars,expr_ref & fml,app_ref_vector & free_vars,bool get_first,guarded_defs * defs)2121 lbool eliminate_block( 2122 unsigned num_vars, app* const* vars, expr_ref& fml, 2123 app_ref_vector& free_vars, bool get_first, guarded_defs* defs) { 2124 2125 checkpoint(); 2126 2127 if (has_quantifiers(fml)) { 2128 free_vars.append(num_vars, vars); 2129 return l_undef; 2130 } 2131 2132 flet<bool> fl1(m_fparams.m_model, true); 2133 flet<bool> fl2(m_fparams.m_simplify_bit2int, true); 2134 flet<bool> fl3(m_fparams.m_arith_enum_const_mod, true); 2135 flet<bool> fl4(m_fparams.m_bv_enable_int2bv2int, true); 2136 flet<bool> fl5(m_fparams.m_array_canonize_simplify, true); 2137 flet<unsigned> fl6(m_fparams.m_relevancy_lvl, 0); 2138 TRACE("qe", 2139 for (unsigned i = 0; i < num_vars; ++i) { 2140 tout << mk_ismt2_pp(vars[i], m) << " "; 2141 } 2142 tout << "\n"; 2143 tout << mk_ismt2_pp(fml, m) << "\n"; 2144 ); 2145 2146 expr_ref fml0(fml, m); 2147 2148 scoped_ptr<quant_elim_plugin> th; 2149 pop_context(th); 2150 2151 th->check(num_vars, vars, m_assumption, fml, get_first, free_vars, defs); 2152 2153 push_context(th.detach()); 2154 TRACE("qe", 2155 for (unsigned i = 0; i < num_vars; ++i) { 2156 tout << mk_ismt2_pp(vars[i], m) << " "; 2157 } 2158 tout << "\n"; 2159 tout << "Input:\n" << mk_ismt2_pp(fml0, m) << "\n"; 2160 tout << "Result:\n" << mk_ismt2_pp(fml, m) << "\n";); 2161 2162 if (m.is_false(fml)) { 2163 return l_false; 2164 } 2165 if (free_vars.empty()) { 2166 return l_true; 2167 } 2168 return l_undef; 2169 } 2170 pop_context(scoped_ptr<quant_elim_plugin> & th)2171 void pop_context(scoped_ptr<quant_elim_plugin>& th) { 2172 if (m_plugins.empty()) { 2173 th = alloc(quant_elim_plugin, m, *this, m_fparams); 2174 th->add_plugin(mk_bool_plugin(*th)); 2175 th->add_plugin(mk_bv_plugin(*th)); 2176 th->add_plugin(mk_arith_plugin(*th, m_produce_models, m_fparams)); 2177 th->add_plugin(mk_array_plugin(*th)); 2178 th->add_plugin(mk_datatype_plugin(*th)); 2179 th->add_plugin(mk_dl_plugin(*th)); 2180 } 2181 else { 2182 th = m_plugins.back(); 2183 m_plugins.pop_back(); 2184 } 2185 } 2186 push_context(quant_elim_plugin * th)2187 void push_context(quant_elim_plugin* th) { 2188 m_plugins.push_back(th); 2189 th->reset(); 2190 } 2191 eliminate_exists_bind(unsigned num_vars,app * const * vars,expr_ref & fml)2192 void eliminate_exists_bind(unsigned num_vars, app* const* vars, expr_ref& fml) { 2193 checkpoint(); 2194 app_ref_vector free_vars(m); 2195 eliminate_exists(num_vars, vars, fml, free_vars, false, nullptr); 2196 bind_variables(free_vars.size(), free_vars.c_ptr(), fml); 2197 } 2198 eliminate_forall_bind(unsigned num_vars,app * const * vars,expr_ref & fml)2199 void eliminate_forall_bind(unsigned num_vars, app* const* vars, expr_ref& fml) { 2200 expr_ref tmp(m); 2201 bool_rewriter rw(m); 2202 rw.mk_not(fml, tmp); 2203 eliminate_exists_bind(num_vars, vars, tmp); 2204 rw.mk_not(tmp, fml); 2205 } 2206 2207 }; 2208 2209 // ------------------------------------------------ 2210 // expr_quant_elim 2211 expr_quant_elim(ast_manager & m,smt_params const & fp,params_ref const & p)2212 expr_quant_elim::expr_quant_elim(ast_manager& m, smt_params const& fp, params_ref const& p): 2213 m(m), 2214 m_fparams(fp), 2215 m_params(p), 2216 m_trail(m), 2217 m_qe(nullptr), 2218 m_assumption(m.mk_true()) 2219 { 2220 } 2221 ~expr_quant_elim()2222 expr_quant_elim::~expr_quant_elim() { 2223 dealloc(m_qe); 2224 } 2225 operator ()(expr * assumption,expr * fml,expr_ref & result)2226 void expr_quant_elim::operator()(expr* assumption, expr* fml, expr_ref& result) { 2227 TRACE("qe", 2228 if (assumption) tout << "elim assumption\n" << mk_ismt2_pp(assumption, m) << "\n"; 2229 tout << "elim input\n" << mk_ismt2_pp(fml, m) << "\n";); 2230 expr_ref_vector bound(m); 2231 result = fml; 2232 m_assumption = assumption; 2233 instantiate_expr(bound, result); 2234 elim(result); 2235 m_trail.reset(); 2236 m_visited.reset(); 2237 abstract_expr(bound.size(), bound.c_ptr(), result); 2238 TRACE("qe", tout << "elim result\n" << mk_ismt2_pp(result, m) << "\n";); 2239 } 2240 updt_params(params_ref const & p)2241 void expr_quant_elim::updt_params(params_ref const& p) { 2242 init_qe(); 2243 m_qe->updt_params(p); 2244 } 2245 collect_param_descrs(param_descrs & r)2246 void expr_quant_elim::collect_param_descrs(param_descrs& r) { 2247 r.insert("eliminate_variables_as_block", CPK_BOOL, 2248 "(default: true) eliminate variables as a block (true) or one at a time (false)"); 2249 } 2250 init_qe()2251 void expr_quant_elim::init_qe() { 2252 if (!m_qe) { 2253 m_qe = alloc(quant_elim_new, m, const_cast<smt_params&>(m_fparams)); 2254 } 2255 } 2256 2257 instantiate_expr(expr_ref_vector & bound,expr_ref & fml)2258 void expr_quant_elim::instantiate_expr(expr_ref_vector& bound, expr_ref& fml) { 2259 expr_free_vars fv; 2260 fv(fml); 2261 fv.set_default_sort(m.mk_bool_sort()); 2262 if (!fv.empty()) { 2263 expr_ref tmp(m); 2264 for (unsigned i = fv.size(); i > 0;) { 2265 --i; 2266 bound.push_back(m.mk_fresh_const("bound", fv[i])); 2267 } 2268 var_subst subst(m); 2269 fml = subst(fml, bound.size(), bound.c_ptr()); 2270 } 2271 } 2272 abstract_expr(unsigned sz,expr * const * bound,expr_ref & fml)2273 void expr_quant_elim::abstract_expr(unsigned sz, expr* const* bound, expr_ref& fml) { 2274 if (sz > 0) { 2275 fml = expr_abstract(m, 0, sz, bound, fml); 2276 } 2277 } 2278 extract_vars(quantifier * q,expr_ref & new_body,app_ref_vector & vars)2279 void extract_vars(quantifier* q, expr_ref& new_body, app_ref_vector& vars) { 2280 ast_manager& m = new_body.get_manager(); 2281 expr_ref tmp(m); 2282 unsigned nd = q->get_num_decls(); 2283 for (unsigned i = 0; i < nd; ++i) { 2284 vars.push_back(m.mk_fresh_const("x",q->get_decl_sort(i))); 2285 } 2286 expr* const* exprs = (expr* const*)(vars.c_ptr()); 2287 var_subst subst(m); 2288 tmp = subst(new_body, vars.size(), exprs); 2289 inv_var_shifter shift(m); 2290 shift(tmp, vars.size(), new_body); 2291 } 2292 elim(expr_ref & result)2293 void expr_quant_elim::elim(expr_ref& result) { 2294 expr_ref tmp(m); 2295 ptr_vector<expr> todo; 2296 2297 m_trail.push_back(result); 2298 todo.push_back(result); 2299 expr* e = nullptr, *r = nullptr; 2300 2301 while (!todo.empty()) { 2302 e = todo.back(); 2303 if (m_visited.contains(e)) { 2304 todo.pop_back(); 2305 continue; 2306 } 2307 2308 switch(e->get_kind()) { 2309 case AST_APP: { 2310 app* a = to_app(e); 2311 expr_ref_vector args(m); 2312 bool all_visited = true; 2313 for (expr* arg : *a) { 2314 if (m_visited.find(arg, r)) { 2315 args.push_back(r); 2316 } 2317 else { 2318 todo.push_back(arg); 2319 all_visited = false; 2320 } 2321 } 2322 if (all_visited) { 2323 r = m.mk_app(a->get_decl(), args.size(), args.c_ptr()); 2324 todo.pop_back(); 2325 m_trail.push_back(r); 2326 m_visited.insert(e, r); 2327 } 2328 break; 2329 } 2330 case AST_QUANTIFIER: { 2331 app_ref_vector vars(m); 2332 quantifier* q = to_quantifier(e); 2333 if (is_lambda(q)) { 2334 tmp = e; 2335 } 2336 else { 2337 bool is_fa = is_forall(q); 2338 tmp = q->get_expr(); 2339 extract_vars(q, tmp, vars); 2340 elim(tmp); 2341 init_qe(); 2342 m_qe->set_assumption(m_assumption); 2343 m_qe->eliminate(is_fa, vars.size(), vars.c_ptr(), tmp); 2344 } 2345 m_trail.push_back(tmp); 2346 m_visited.insert(e, tmp); 2347 todo.pop_back(); 2348 break; 2349 } 2350 default: 2351 UNREACHABLE(); 2352 break; 2353 } 2354 } 2355 2356 VERIFY (m_visited.find(result, e)); 2357 result = e; 2358 } 2359 collect_statistics(statistics & st) const2360 void expr_quant_elim::collect_statistics(statistics & st) const { 2361 if (m_qe) { 2362 m_qe->collect_statistics(st); 2363 } 2364 } 2365 first_elim(unsigned num_vars,app * const * vars,expr_ref & fml,def_vector & defs)2366 lbool expr_quant_elim::first_elim(unsigned num_vars, app* const* vars, expr_ref& fml, def_vector& defs) { 2367 app_ref_vector fvs(m); 2368 init_qe(); 2369 guarded_defs gdefs(m); 2370 lbool res = m_qe->eliminate_exists(num_vars, vars, fml, fvs, true, &gdefs); 2371 if (gdefs.size() > 0) { 2372 defs.reset(); 2373 defs.append(gdefs.defs(0)); 2374 fml = gdefs.guard(0); 2375 } 2376 return res; 2377 } 2378 solve_for_var(app * var,expr * fml,guarded_defs & defs)2379 bool expr_quant_elim::solve_for_var(app* var, expr* fml, guarded_defs& defs) { 2380 return solve_for_vars(1,&var, fml, defs); 2381 } 2382 solve_for_vars(unsigned num_vars,app * const * vars,expr * _fml,guarded_defs & defs)2383 bool expr_quant_elim::solve_for_vars(unsigned num_vars, app* const* vars, expr* _fml, guarded_defs& defs) { 2384 app_ref_vector fvs(m); 2385 expr_ref fml(_fml, m); 2386 TRACE("qe", tout << mk_pp(fml, m) << "\n";); 2387 init_qe(); 2388 lbool is_sat = m_qe->eliminate_exists(num_vars, vars, fml, fvs, false, &defs); 2389 return is_sat != l_undef; 2390 } 2391 2392 2393 2394 2395 2396 #if 0 2397 // ------------------------------------------------ 2398 // expr_quant_elim_star1 2399 2400 bool expr_quant_elim_star1::visit_quantifier(quantifier * q) { 2401 if (!is_target(q)) { 2402 return true; 2403 } 2404 bool visited = true; 2405 visit(q->get_expr(), visited); 2406 return visited; 2407 } 2408 2409 void expr_quant_elim_star1::reduce1_quantifier(quantifier * q) { 2410 if (!is_target(q)) { 2411 cache_result(q, q, 0); 2412 return; 2413 } 2414 2415 quantifier_ref new_q(m); 2416 expr * new_body = 0; 2417 proof * new_pr; 2418 get_cached(q->get_expr(), new_body, new_pr); 2419 new_q = m.update_quantifier(q, new_body); 2420 expr_ref r(m); 2421 m_quant_elim(m_assumption, new_q, r); 2422 if (q == r.get()) { 2423 cache_result(q, q, 0); 2424 return; 2425 } 2426 proof_ref pr(m); 2427 if (m.proofs_enabled()) { 2428 pr = m.mk_rewrite(q, r); // TODO: improve justification 2429 } 2430 cache_result(q, r, pr); 2431 } 2432 2433 expr_quant_elim_star1::expr_quant_elim_star1(ast_manager& m, smt_params const& p): 2434 simplifier(m), m_quant_elim(m, p), m_assumption(m.mk_true()) 2435 { 2436 } 2437 #endif 2438 2439 hoist_exists(expr_ref & fml,app_ref_vector & vars)2440 void hoist_exists(expr_ref& fml, app_ref_vector& vars) { 2441 quantifier_hoister hoister(fml.get_manager()); 2442 hoister.pull_exists(fml, vars, fml); 2443 } 2444 mk_exists(unsigned num_bound,app * const * vars,expr_ref & fml)2445 void mk_exists(unsigned num_bound, app* const* vars, expr_ref& fml) { 2446 ast_manager& m = fml.get_manager(); 2447 expr_ref tmp(m); 2448 expr_abstract(m, 0, num_bound, (expr*const*)vars, fml, tmp); 2449 ptr_vector<sort> sorts; 2450 svector<symbol> names; 2451 for (unsigned i = 0; i < num_bound; ++i) { 2452 sorts.push_back(vars[i]->get_decl()->get_range()); 2453 names.push_back(vars[i]->get_decl()->get_name()); 2454 } 2455 if (num_bound > 0) { 2456 tmp = m.mk_exists(num_bound, sorts.c_ptr(), names.c_ptr(), tmp, 1); 2457 } 2458 fml = tmp; 2459 } 2460 has_quantified_uninterpreted(ast_manager & m,expr * fml)2461 bool has_quantified_uninterpreted(ast_manager& m, expr* fml) { 2462 struct found {}; 2463 struct proc { 2464 ast_manager& m; 2465 proc(ast_manager& m):m(m) {} 2466 void operator()(quantifier* q) { 2467 if (has_uninterpreted(m, q->get_expr())) 2468 throw found(); 2469 } 2470 void operator()(expr*) {} 2471 }; 2472 2473 try { 2474 proc p(m); 2475 for_each_expr(p, fml); 2476 return false; 2477 } 2478 catch (found) { 2479 return true; 2480 } 2481 } 2482 2483 class simplify_solver_context : public i_solver_context { 2484 ast_manager& m; 2485 smt_params m_fparams; 2486 app_ref_vector* m_vars; 2487 expr_ref* m_fml; 2488 ptr_vector<contains_app> m_contains; 2489 atom_set m_pos; 2490 atom_set m_neg; 2491 public: simplify_solver_context(ast_manager & m)2492 simplify_solver_context(ast_manager& m): 2493 m(m), 2494 m_vars(nullptr), 2495 m_fml(nullptr) 2496 { 2497 add_plugin(mk_bool_plugin(*this)); 2498 add_plugin(mk_arith_plugin(*this, false, m_fparams)); 2499 } 2500 updt_params(params_ref const & p)2501 void updt_params(params_ref const& p) { 2502 m_fparams.updt_params(p); 2503 } 2504 ~simplify_solver_context()2505 ~simplify_solver_context() override { reset(); } 2506 2507 solve(expr_ref & fml,app_ref_vector & vars)2508 void solve(expr_ref& fml, app_ref_vector& vars) { 2509 init(fml, vars); 2510 bool solved = true; 2511 do { 2512 conj_enum conjs(m, fml); 2513 solved = false; 2514 for (unsigned i = 0; !solved && i < m_plugins.size(); ++i) { 2515 qe_solver_plugin* p = m_plugins[i]; 2516 solved = p && p->solve(conjs, fml); 2517 } 2518 TRACE("qe", 2519 tout << (solved?"solved":"not solved") << "\n"; 2520 if (solved) tout << mk_ismt2_pp(fml, m) << "\n"; 2521 tout << *m_vars << "\n"; 2522 tout << "contains: " << m_contains.size() << "\n"; 2523 ); 2524 } 2525 while (solved); 2526 } 2527 get_manager()2528 ast_manager& get_manager() override { return m; } 2529 pos_atoms() const2530 atom_set const& pos_atoms() const override { return m_pos; } neg_atoms() const2531 atom_set const& neg_atoms() const override { return m_neg; } 2532 2533 // Access current set of variables to solve get_num_vars() const2534 unsigned get_num_vars() const override { return m_vars->size(); } get_var(unsigned idx) const2535 app* get_var(unsigned idx) const override { return (*m_vars)[idx].get(); } get_vars() const2536 app_ref_vector const& get_vars() const override { return *m_vars; } is_var(expr * e,unsigned & idx) const2537 bool is_var(expr* e, unsigned& idx) const override { 2538 for (unsigned i = 0; i < m_vars->size(); ++i) { 2539 if ((*m_vars)[i].get() == e) { 2540 idx = i; 2541 return true; 2542 } 2543 } 2544 return false; 2545 } 2546 contains(unsigned idx)2547 contains_app& contains(unsigned idx) override { 2548 return *m_contains[idx]; 2549 } 2550 2551 // callback to replace variable at index 'idx' with definition 'def' and updated formula 'fml' elim_var(unsigned idx,expr * fml,expr * def)2552 void elim_var(unsigned idx, expr* fml, expr* def) override { 2553 TRACE("qe", tout << idx << ": " << mk_pp(m_vars->get(idx), m) << " " << mk_pp(fml, m) << " " << m_contains.size() << "\n";); 2554 *m_fml = fml; 2555 m_vars->set(idx, m_vars->get(m_vars->size()-1)); 2556 m_vars->pop_back(); 2557 dealloc(m_contains[idx]); 2558 m_contains[idx] = m_contains[m_contains.size()-1]; 2559 m_contains.pop_back(); 2560 } 2561 2562 // callback to add new variable to branch. add_var(app * x)2563 void add_var(app* x) override { 2564 TRACE("qe", tout << "add var: " << mk_pp(x, m) << "\n";); 2565 m_vars->push_back(x); 2566 m_contains.push_back(alloc(contains_app, m, x)); 2567 } 2568 2569 // callback to add constraints in branch. add_constraint(bool use_var,expr * l1=nullptr,expr * l2=nullptr,expr * l3=nullptr)2570 void add_constraint(bool use_var, expr* l1 = nullptr, expr* l2 = nullptr, expr* l3 = nullptr) override { 2571 UNREACHABLE(); 2572 } 2573 // eliminate finite domain variable 'var' from fml. blast_or(app * var,expr_ref & fml)2574 void blast_or(app* var, expr_ref& fml) override { 2575 UNREACHABLE(); 2576 } 2577 2578 private: reset()2579 void reset() { 2580 for (auto* c : m_contains) 2581 dealloc (c); 2582 m_contains.reset(); 2583 } 2584 init(expr_ref & fml,app_ref_vector & vars)2585 void init(expr_ref& fml, app_ref_vector& vars) { 2586 reset(); 2587 m_fml = &fml; 2588 m_vars = &vars; 2589 TRACE("qe", tout << "Vars: " << vars << "\n";); 2590 for (auto* v : vars) { 2591 m_contains.push_back(alloc(contains_app, m, v)); 2592 } 2593 } 2594 }; 2595 2596 class simplify_rewriter_cfg::impl { 2597 ast_manager& m; 2598 simplify_solver_context m_ctx; 2599 public: impl(ast_manager & m)2600 impl(ast_manager& m) : m(m), m_ctx(m) {} 2601 updt_params(params_ref const & p)2602 void updt_params(params_ref const& p) { 2603 m_ctx.updt_params(p); 2604 } 2605 collect_statistics(statistics & st) const2606 void collect_statistics(statistics & st) const { 2607 m_ctx.collect_statistics(st); 2608 } 2609 reduce_quantifier(quantifier * old_q,expr * new_body,expr * const * new_patterns,expr * const * new_no_patterns,expr_ref & result,proof_ref & result_pr)2610 bool reduce_quantifier( 2611 quantifier * old_q, 2612 expr * new_body, 2613 expr * const * new_patterns, 2614 expr * const * new_no_patterns, 2615 expr_ref & result, 2616 proof_ref & result_pr 2617 ) 2618 { 2619 2620 if (is_lambda(old_q)) { 2621 return false; 2622 } 2623 // bool is_forall = old_q->is_forall(); 2624 app_ref_vector vars(m); 2625 TRACE("qe", tout << "simplifying" << mk_pp(new_body, m) << "\n";); 2626 result = new_body; 2627 extract_vars(old_q, result, vars); 2628 TRACE("qe", tout << "variables extracted" << mk_pp(result, m) << "\n";); 2629 2630 if (is_forall(old_q)) { 2631 result = mk_not(m, result); 2632 } 2633 m_ctx.solve(result, vars); 2634 if (is_forall(old_q)) { 2635 expr* e = nullptr; 2636 result = m.is_not(result, e)?e:mk_not(m, result); 2637 } 2638 var_shifter shift(m); 2639 shift(result, vars.size(), result); 2640 result = expr_abstract(vars, result); 2641 TRACE("qe", tout << "abstracted" << mk_pp(result, m) << "\n";); 2642 ptr_vector<sort> sorts; 2643 svector<symbol> names; 2644 for (app* v : vars) { 2645 sorts.push_back(v->get_decl()->get_range()); 2646 names.push_back(v->get_decl()->get_name()); 2647 } 2648 if (!vars.empty()) { 2649 result = m.mk_quantifier(old_q->get_kind(), vars.size(), sorts.c_ptr(), names.c_ptr(), result, 1); 2650 } 2651 result_pr = nullptr; 2652 return true; 2653 } 2654 2655 }; 2656 simplify_rewriter_cfg(ast_manager & m)2657 simplify_rewriter_cfg::simplify_rewriter_cfg(ast_manager& m) { 2658 imp = alloc(simplify_rewriter_cfg::impl, m); 2659 } 2660 ~simplify_rewriter_cfg()2661 simplify_rewriter_cfg::~simplify_rewriter_cfg() { 2662 dealloc(imp); 2663 } 2664 reduce_quantifier(quantifier * old_q,expr * new_body,expr * const * new_patterns,expr * const * new_no_patterns,expr_ref & result,proof_ref & result_pr)2665 bool simplify_rewriter_cfg::reduce_quantifier( 2666 quantifier * old_q, 2667 expr * new_body, 2668 expr * const * new_patterns, 2669 expr * const * new_no_patterns, 2670 expr_ref & result, 2671 proof_ref & result_pr 2672 ) { 2673 return imp->reduce_quantifier(old_q, new_body, new_patterns, new_no_patterns, result, result_pr); 2674 } 2675 updt_params(params_ref const & p)2676 void simplify_rewriter_cfg::updt_params(params_ref const& p) { 2677 imp->updt_params(p); 2678 } 2679 collect_statistics(statistics & st) const2680 void simplify_rewriter_cfg::collect_statistics(statistics & st) const { 2681 imp->collect_statistics(st); 2682 } 2683 pre_visit(expr * e)2684 bool simplify_rewriter_cfg::pre_visit(expr* e) { 2685 if (!is_quantifier(e)) return true; 2686 quantifier * q = to_quantifier(e); 2687 return (q->get_num_patterns() == 0 && q->get_num_no_patterns() == 0); 2688 } 2689 simplify_exists(app_ref_vector & vars,expr_ref & fml)2690 void simplify_exists(app_ref_vector& vars, expr_ref& fml) { 2691 ast_manager& m = fml.get_manager(); 2692 simplify_solver_context ctx(m); 2693 ctx.solve(fml, vars); 2694 } 2695 } 2696 2697 2698 template class rewriter_tpl<qe::simplify_rewriter_cfg>; 2699 2700 2701