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.data(), fml_closed); 148 rewriter.mk_and(conjs_mixed.size(), conjs_mixed.data(), fml_mixed); 149 rewriter.mk_and(conjs_open.size(), conjs_open.data(), 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 expr_ref tmp(m); 554 bool visited = true; 555 for (expr* arg : *a) { 556 expr* r = lookup(arg, p); 557 if (r) { 558 m_args.push_back(r); 559 } 560 else { 561 visited = false; 562 } 563 } 564 if (visited) { 565 pop(); 566 if (p == is_and) 567 tmp = mk_and(m_args); 568 else 569 tmp = mk_or(m_args); 570 insert(a, p, tmp); 571 } 572 } 573 get_nnf(expr_ref & fml,bool p0)574 bool get_nnf(expr_ref& fml, bool p0) { 575 TRACE("nnf", tout << mk_ismt2_pp(fml.get(), m) << "\n";); 576 bool p = p0; 577 unsigned sz = m_todo.size(); 578 expr_ref tmp(m); 579 580 expr* e = lookup(fml, p); 581 if (e) { 582 fml = e; 583 return true; 584 } 585 m_trail.push_back(fml); 586 587 while (sz < m_todo.size()) { 588 e = m_todo.back(); 589 p = m_pols.back(); 590 if (!m_is_relevant(e)) { 591 pop(); 592 insert(e, p, p?e:mk_not(m, e)); 593 continue; 594 } 595 if (!is_app(e)) { 596 return false; 597 } 598 if (contains(e, p)) { 599 pop(); 600 continue; 601 } 602 app* a = to_app(e); 603 if (m.is_and(e) || m.is_or(e)) { 604 nnf_and_or(m.is_and(a), a, p); 605 } 606 else if (m.is_not(a)) { 607 nnf_not(a, p); 608 } 609 else if (m.is_ite(a)) { 610 nnf_ite(a, p); 611 } 612 else if (m.is_iff(a)) { 613 nnf_iff(a, p); 614 } 615 else if (m.is_xor(a)) { 616 nnf_iff(a, !p); 617 } 618 else if (m.is_implies(a)) { 619 nnf_implies(a, p); 620 } 621 else if (m_lift_ite(e, tmp)) { 622 if (!get_nnf(tmp, p)) { 623 return false; 624 } 625 pop(); 626 insert(e, p, tmp); 627 } 628 else { 629 pop(); 630 insert(e, p, p?e:mk_not(m, e)); 631 } 632 633 } 634 fml = lookup(fml, p0); 635 SASSERT(fml.get()); 636 return true; 637 } 638 }; 639 640 // ---------------------------------- 641 // Normalize literals in NNF formula. 642 643 class nnf_normalize_literals { 644 ast_manager& m; 645 i_expr_pred& m_is_relevant; 646 i_nnf_atom& m_mk_atom; 647 obj_map<expr, expr*> m_cache; 648 ptr_vector<expr> m_todo; 649 expr_ref_vector m_trail; 650 ptr_vector<expr> m_args; 651 public: nnf_normalize_literals(ast_manager & m,i_expr_pred & is_relevant,i_nnf_atom & mk_atom)652 nnf_normalize_literals(ast_manager& m, i_expr_pred& is_relevant, i_nnf_atom& mk_atom): 653 m(m), m_is_relevant(is_relevant), m_mk_atom(mk_atom), m_trail(m) {} 654 operator ()(expr_ref & fml)655 void operator()(expr_ref& fml) { 656 SASSERT(m_todo.empty()); 657 m_todo.push_back(fml); 658 while (!m_todo.empty()) { 659 expr* e = m_todo.back(); 660 if (m_cache.contains(e)) { 661 m_todo.pop_back(); 662 } 663 else if (!is_app(e)) { 664 m_todo.pop_back(); 665 m_cache.insert(e, e); 666 } 667 else if (visit(to_app(e))) { 668 m_todo.pop_back(); 669 } 670 } 671 fml = m_cache.find(fml); 672 reset(); 673 } 674 reset()675 void reset() { 676 m_cache.reset(); 677 m_todo.reset(); 678 m_trail.reset(); 679 } 680 681 private: 682 visit(app * e)683 bool visit(app* e) { 684 bool all_visit = true; 685 expr* f = nullptr; 686 expr_ref tmp(m); 687 if (!m_is_relevant(e)) { 688 m_cache.insert(e, e); 689 } 690 else if (m.is_and(e) || m.is_or(e)) { 691 m_args.reset(); 692 for (expr* arg : *e) { 693 if (m_cache.find(arg, f)) { 694 m_args.push_back(f); 695 } 696 else { 697 all_visit = false; 698 m_todo.push_back(arg); 699 } 700 } 701 if (all_visit) { 702 m_cache.insert(e, m.mk_app(e->get_decl(), m_args.size(), m_args.data())); 703 } 704 } 705 else if (m.is_not(e, f)) { 706 SASSERT(!m.is_not(f) && !m.is_and(f) && !m.is_or(f)); 707 m_mk_atom(f, false, tmp); 708 m_cache.insert(e, tmp); 709 m_trail.push_back(tmp); 710 } 711 else { 712 m_mk_atom(e, true, tmp); 713 m_trail.push_back(tmp); 714 m_cache.insert(e, tmp); 715 } 716 return all_visit; 717 } 718 }; 719 720 // ---------------------------- 721 // def_vector 722 normalize()723 void def_vector::normalize() { 724 // apply nested definitions into place. 725 ast_manager& m = m_vars.get_manager(); 726 expr_substitution sub(m); 727 scoped_ptr<expr_replacer> rep = mk_expr_simp_replacer(m); 728 if (size() <= 1) { 729 return; 730 } 731 for (unsigned i = size(); i > 0; ) { 732 --i; 733 expr_ref e(m); 734 e = def(i); 735 rep->set_substitution(&sub); 736 (*rep)(e); 737 sub.insert(m.mk_const(var(i)), e); 738 def_ref(i) = e; 739 } 740 } 741 project(unsigned num_vars,app * const * vars)742 void def_vector::project(unsigned num_vars, app* const* vars) { 743 obj_hashtable<func_decl> fns; 744 for (unsigned i = 0; i < num_vars; ++i) { 745 fns.insert(vars[i]->get_decl()); 746 } 747 for (unsigned i = 0; i < size(); ++i) { 748 if (fns.contains(m_vars[i].get())) { 749 // 750 // retain only first occurrence of eliminated variable. 751 // later occurrences are just recycling the name. 752 // 753 fns.remove(m_vars[i].get()); 754 } 755 else { 756 for (unsigned j = i+1; j < size(); ++j) { 757 m_vars.set(j-1, m_vars.get(j)); 758 m_defs.set(j-1, m_defs.get(j)); 759 } 760 m_vars.pop_back(); 761 m_defs.pop_back(); 762 --i; 763 } 764 } 765 } 766 767 // ---------------------------- 768 // guarded_defs 769 display(std::ostream & out) const770 std::ostream& guarded_defs::display(std::ostream& out) const { 771 ast_manager& m = m_guards.get_manager(); 772 for (unsigned i = 0; i < size(); ++i) { 773 for (unsigned j = 0; j < defs(i).size(); ++j) { 774 out << defs(i).var(j)->get_name() << " := " << mk_pp(defs(i).def(j), m) << "\n"; 775 } 776 out << "if " << mk_pp(guard(i), m) << "\n"; 777 } 778 return out; 779 } 780 inv()781 bool guarded_defs::inv() { 782 return m_defs.size() == m_guards.size(); 783 } 784 add(expr * guard,def_vector const & defs)785 void guarded_defs::add(expr* guard, def_vector const& defs) { 786 SASSERT(inv()); 787 m_defs.push_back(defs); 788 m_guards.push_back(guard); 789 m_defs.back().normalize(); 790 SASSERT(inv()); 791 } 792 project(unsigned num_vars,app * const * vars)793 void guarded_defs::project(unsigned num_vars, app* const* vars) { 794 for (unsigned i = 0; i < size(); ++i) { 795 m_defs[i].project(num_vars, vars); 796 } 797 } 798 799 // ---------------------------- 800 // Obtain atoms in NNF formula. 801 802 class nnf_collect_atoms { 803 ast_manager& m; 804 i_expr_pred& m_is_relevant; 805 ptr_vector<expr> m_todo; 806 ast_mark m_visited; 807 public: nnf_collect_atoms(ast_manager & m,i_expr_pred & is_relevant)808 nnf_collect_atoms(ast_manager& m, i_expr_pred& is_relevant): 809 m(m), m_is_relevant(is_relevant) {} 810 operator ()(expr * fml,atom_set & pos,atom_set & neg)811 void operator()(expr* fml, atom_set& pos, atom_set& neg) { 812 m_todo.push_back(fml); 813 while (!m_todo.empty()) { 814 expr* e = m_todo.back(); 815 m_todo.pop_back(); 816 if (m_visited.is_marked(e)) 817 continue; 818 m_visited.mark(e, true); 819 if (!is_app(e) || !m_is_relevant(e)) 820 continue; 821 app* a = to_app(e); 822 if (m.is_and(a) || m.is_or(a)) { 823 for (expr* arg : *a) 824 m_todo.push_back(arg); 825 } 826 else if (m.is_not(a, e) && is_app(e)) { 827 neg.insert(to_app(e)); 828 } 829 else { 830 pos.insert(a); 831 } 832 } 833 SASSERT(m_todo.empty()); 834 m_visited.reset(); 835 } 836 }; 837 838 839 // -------------------------------- 840 // Bring formula to NNF, normalize atoms, collect literals. 841 842 class nnf_normalizer { 843 nnf m_nnf_core; 844 nnf_collect_atoms m_collect_atoms; 845 nnf_normalize_literals m_normalize_literals; 846 public: nnf_normalizer(ast_manager & m,i_expr_pred & is_relevant,i_nnf_atom & mk_atom)847 nnf_normalizer(ast_manager& m, i_expr_pred& is_relevant, i_nnf_atom& mk_atom): 848 m_nnf_core(m, is_relevant), 849 m_collect_atoms(m, is_relevant), 850 m_normalize_literals(m, is_relevant, mk_atom) 851 {} 852 operator ()(expr_ref & fml,atom_set & pos,atom_set & neg)853 void operator()(expr_ref& fml, atom_set& pos, atom_set& neg) { 854 expr_ref orig(fml); 855 m_nnf_core(fml); 856 m_normalize_literals(fml); 857 m_collect_atoms(fml, pos, neg); 858 TRACE("qe", 859 ast_manager& m = fml.get_manager(); 860 tout << mk_ismt2_pp(orig, m) << "\n-->\n" << mk_ismt2_pp(fml, m) << "\n";); 861 } 862 reset()863 void reset() { 864 m_nnf_core.reset(); 865 m_normalize_literals.reset(); 866 } 867 }; 868 get_nnf(expr_ref & fml,i_expr_pred & pred,i_nnf_atom & mk_atom,atom_set & pos,atom_set & neg)869 void get_nnf(expr_ref& fml, i_expr_pred& pred, i_nnf_atom& mk_atom, atom_set& pos, atom_set& neg) { 870 nnf_normalizer nnf(fml.get_manager(), pred, mk_atom); 871 nnf(fml, pos, neg); 872 } 873 874 // 875 // Theory plugin for quantifier elimination. 876 // 877 878 class quant_elim { 879 public: ~quant_elim()880 virtual ~quant_elim() {} 881 882 virtual lbool eliminate_exists( 883 unsigned num_vars, app* const* vars, 884 expr_ref& fml, app_ref_vector& free_vars, bool get_first, guarded_defs* defs) = 0; 885 886 virtual void set_assumption(expr* fml) = 0; 887 888 virtual void collect_statistics(statistics & st) const = 0; 889 890 virtual void eliminate(bool is_forall, unsigned num_vars, app* const* vars, expr_ref& fml) = 0; 891 892 updt_params(params_ref const & p)893 virtual void updt_params(params_ref const& p) {} 894 895 }; 896 897 class search_tree { 898 typedef map<rational, unsigned, rational::hash_proc, rational::eq_proc> branch_map; 899 ast_manager& m; 900 app_ref_vector m_vars; // free variables 901 app_ref m_var; // 0 or selected free variable 902 def_vector m_def; // substitution for the variable eliminated relative to the parent. 903 expr_ref m_fml; // formula whose variables are to be eliminated 904 app_ref m_assignment; // assignment that got us here. 905 search_tree* m_parent; // parent pointer 906 rational m_num_branches; // number of possible branches 907 ptr_vector<search_tree> m_children; // list of children 908 branch_map m_branch_index; // branch_id -> child search tree index 909 atom_set m_pos; 910 atom_set m_neg; 911 bool m_pure; // is the node pure (no variables deleted). 912 913 // The invariant captures that search tree nodes are either 914 // - unit branches (with only one descendant), or 915 // - unassigned variable and formula 916 // - assigned formula, but unassigned variable for branching 917 // - assigned variable and formula with 0 or more branches. 918 // 919 #define CHECK_COND(_cond_) if (!(_cond_)) { TRACE("qe", tout << "violated: " << #_cond_ << "\n";); return false; } invariant() const920 bool invariant() const { 921 CHECK_COND(assignment()); 922 CHECK_COND(m_children.empty() || fml()); 923 CHECK_COND(!is_root() || fml()); 924 CHECK_COND(!fml() || has_var() || m_num_branches.is_zero() || is_unit()); 925 for (auto const & kv : m_branch_index) { 926 CHECK_COND(kv.m_value < m_children.size()); 927 CHECK_COND(kv.m_key < get_num_branches()); 928 } 929 for (unsigned i = 0; i < m_children.size(); ++i) { 930 CHECK_COND(m_children[i]); 931 CHECK_COND(this == m_children[i]->m_parent); 932 CHECK_COND(m_children[i]->invariant()); 933 } 934 return true; 935 } 936 #undef CHECKC_COND 937 938 public: search_tree(search_tree * parent,ast_manager & m,app * assignment)939 search_tree(search_tree* parent, ast_manager& m, app* assignment): 940 m(m), 941 m_vars(m), 942 m_var(m), 943 m_def(m), 944 m_fml(m), 945 m_assignment(assignment, m), 946 m_parent(parent), 947 m_pure(true) 948 {} 949 ~search_tree()950 ~search_tree() { 951 reset(); 952 } 953 fml() const954 expr* fml() const { return m_fml; } 955 fml_ref()956 expr_ref& fml_ref() { return m_fml; } 957 def() const958 def_vector const& def() const { return m_def; } 959 assignment() const960 app* assignment() const { return m_assignment; } 961 var() const962 app* var() const { SASSERT(has_var()); return m_var; } 963 has_var() const964 bool has_var() const { return nullptr != m_var.get(); } 965 parent() const966 search_tree* parent() const { return m_parent; } 967 is_root() const968 bool is_root() const { return !parent(); } 969 get_num_branches() const970 rational const& get_num_branches() const { SASSERT(has_var()); return m_num_branches; } 971 972 // extract disjunctions get_leaves(expr_ref_vector & result)973 void get_leaves(expr_ref_vector& result) { 974 SASSERT(is_root()); 975 ptr_vector<search_tree> todo; 976 todo.push_back(this); 977 while (!todo.empty()) { 978 search_tree* st = todo.back(); 979 todo.pop_back(); 980 if (st->m_children.empty() && st->fml() && 981 st->m_vars.empty() && !st->has_var()) { 982 TRACE("qe", st->display(tout << "appending leaf\n");); 983 result.push_back(st->fml()); 984 } 985 for (auto * ch : st->m_children) 986 todo.push_back(ch); 987 } 988 } 989 get_leaves_rec(def_vector & defs,guarded_defs & gdefs)990 void get_leaves_rec(def_vector& defs, guarded_defs& gdefs) { 991 expr* f = this->fml(); 992 unsigned sz = defs.size(); 993 defs.append(def()); 994 if (m_children.empty() && f && !m.is_false(f) && 995 m_vars.empty() && !has_var()) { 996 gdefs.add(f, defs); 997 } 998 else { 999 for (unsigned i = 0; i < m_children.size(); ++i) { 1000 m_children[i]->get_leaves_rec(defs, gdefs); 1001 } 1002 } 1003 defs.shrink(sz); 1004 } 1005 get_leaves(guarded_defs & gdefs)1006 void get_leaves(guarded_defs& gdefs) { 1007 def_vector defs(m); 1008 get_leaves_rec(defs, gdefs); 1009 } 1010 reset()1011 void reset() { 1012 TRACE("qe",tout << "resetting\n";); 1013 for (auto* ch : m_children) dealloc(ch); 1014 m_pos.reset(); 1015 m_neg.reset(); 1016 m_children.reset(); 1017 m_vars.reset(); 1018 m_branch_index.reset(); 1019 m_var = nullptr; 1020 m_def.reset(); 1021 m_num_branches = rational::zero(); 1022 m_pure = true; 1023 } 1024 init(expr * fml)1025 void init(expr* fml) { 1026 m_fml = fml; 1027 SASSERT(invariant()); 1028 } 1029 add_def(app * v,expr * def)1030 void add_def(app* v, expr* def) { 1031 if (v && def) { 1032 m_def.push_back(v->get_decl(), def); 1033 } 1034 } 1035 num_free_vars() const1036 unsigned num_free_vars() const { return m_vars.size(); } 1037 // app* const* free_vars() const { return m_vars.c_ptr(); } free_vars() const1038 app_ref_vector const& free_vars() const { return m_vars; } free_var(unsigned i) const1039 app* free_var(unsigned i) const { return m_vars[i]; } reset_free_vars()1040 void reset_free_vars() { TRACE("qe", tout << m_vars << "\n";); m_vars.reset(); } 1041 pos_atoms() const1042 atom_set const& pos_atoms() const { return m_pos; } neg_atoms() const1043 atom_set const& neg_atoms() const { return m_neg; } 1044 pos_atoms()1045 atom_set& pos_atoms() { return m_pos; } neg_atoms()1046 atom_set& neg_atoms() { return m_neg; } 1047 1048 // set the branch variable. set_var(app * x,rational const & num_branches)1049 void set_var(app* x, rational const& num_branches) { 1050 SASSERT(!m_var.get()); 1051 SASSERT(m_vars.contains(x)); 1052 m_var = x; 1053 m_vars.erase(x); 1054 m_num_branches = num_branches; 1055 SASSERT(invariant()); 1056 } 1057 1058 // include new variables. consume_vars(app_ref_vector & vars)1059 void consume_vars(app_ref_vector& vars) { 1060 while (!vars.empty()) { 1061 m_vars.push_back(vars.back()); 1062 vars.pop_back(); 1063 } 1064 } 1065 is_pure() const1066 bool is_pure() const { 1067 search_tree const* node = this; 1068 while (node) { 1069 if (!node->m_pure) return false; 1070 node = node->parent(); 1071 } 1072 return true; 1073 } 1074 is_unit() const1075 bool is_unit() const { 1076 return m_children.size() == 1 && 1077 m_branch_index.empty(); 1078 } 1079 has_branch(rational const & branch_id) const1080 bool has_branch(rational const& branch_id) const { return m_branch_index.contains(branch_id); } 1081 child(rational const & branch_id) const1082 search_tree* child(rational const& branch_id) const { 1083 unsigned idx = m_branch_index.find(branch_id); 1084 return m_children[idx]; 1085 } 1086 child() const1087 search_tree* child() const { 1088 SASSERT(is_unit()); 1089 return m_children[0]; 1090 } 1091 1092 // remove variable from branch. del_var(app * x)1093 void del_var(app* x) { 1094 SASSERT(m_children.empty()); 1095 SASSERT(m_vars.contains(x)); 1096 m_vars.erase(x); 1097 m_pure = false; 1098 } 1099 1100 // add branch with a given formula add_child(expr * fml)1101 search_tree* add_child(expr* fml) { 1102 SASSERT(m_branch_index.empty()); 1103 SASSERT(m_children.empty()); 1104 m_num_branches = rational(1); 1105 search_tree* st = alloc(search_tree, this, m, m.mk_true()); 1106 m_children.push_back(st); 1107 st->init(fml); 1108 st->m_vars.append(m_vars.size(), m_vars.data()); 1109 SASSERT(invariant()); 1110 TRACE("qe", display_node(tout); st->display_node(tout);); 1111 return st; 1112 } 1113 add_child(rational const & branch_id,app * assignment)1114 search_tree* add_child(rational const& branch_id, app* assignment) { 1115 SASSERT(!m_branch_index.contains(branch_id)); 1116 SASSERT(has_var()); 1117 SASSERT(branch_id.is_nonneg() && branch_id < m_num_branches); 1118 unsigned index = m_children.size(); 1119 search_tree* st = alloc(search_tree, this, m, assignment); 1120 m_children.push_back(st); 1121 m_branch_index.insert(branch_id, index); 1122 st->m_vars.append(m_vars.size(), m_vars.data()); 1123 SASSERT(invariant()); 1124 TRACE("qe", display_node(tout); st->display_node(tout);); 1125 return st; 1126 } 1127 display(std::ostream & out) const1128 void display(std::ostream& out) const { 1129 display(out, ""); 1130 } 1131 display_node(std::ostream & out,char const * indent="") const1132 void display_node(std::ostream& out, char const* indent = "") const { 1133 out << indent << "node " << std::hex << this << std::dec << "\n"; 1134 if (m_var) { 1135 out << indent << " var: " << m_var << "\n"; 1136 } 1137 for (app* v : m_vars) { 1138 out << indent << " free: " << mk_pp(v, m) << "\n"; 1139 } 1140 if (m_fml) { 1141 out << indent << " fml: " << m_fml << "\n"; 1142 } 1143 for (unsigned i = 0; i < m_def.size(); ++i) { 1144 out << indent << " def: " << m_def.var(i)->get_name() << " = " << mk_ismt2_pp(m_def.def(i), m) << "\n"; 1145 } 1146 out << indent << " branches: " << m_num_branches << "\n"; 1147 } 1148 display(std::ostream & out,char const * indent) const1149 void display(std::ostream& out, char const* indent) const { 1150 display_node(out, indent); 1151 std::string new_indent(indent); 1152 new_indent += " "; 1153 for (auto * ch : m_children) { 1154 ch->display(out, new_indent.c_str()); 1155 } 1156 } 1157 abstract_variable(app * x,expr * fml) const1158 expr_ref abstract_variable(app* x, expr* fml) const { 1159 expr_ref result(m); 1160 expr* y = x; 1161 expr_abstract(m, 0, 1, &y, fml, result); 1162 symbol X(x->get_decl()->get_name()); 1163 sort* s = x->get_sort(); 1164 result = m.mk_exists(1, &s, &X, result); 1165 return result; 1166 } 1167 display_validate(std::ostream & out) const1168 void display_validate(std::ostream& out) const { 1169 if (m_children.empty()) { 1170 return; 1171 } 1172 expr_ref q(m); 1173 expr* x = m_var; 1174 if (x) { 1175 q = abstract_variable(m_var, m_fml); 1176 1177 expr_ref_vector fmls(m); 1178 expr_ref fml(m); 1179 for (unsigned i = 0; i < m_children.size(); ++i) { 1180 search_tree const& child = *m_children[i]; 1181 fml = child.fml(); 1182 if (fml) { 1183 // abstract free variables in children. 1184 ptr_vector<app> child_vars, new_vars; 1185 child_vars.append(child.m_vars.size(), child.m_vars.data()); 1186 if (child.m_var) { 1187 child_vars.push_back(child.m_var); 1188 } 1189 for (unsigned j = 0; j < child_vars.size(); ++j) { 1190 if (!m_vars.contains(child_vars[j]) && 1191 !new_vars.contains(child_vars[j])) { 1192 fml = abstract_variable(child_vars[j], fml); 1193 new_vars.push_back(child_vars[j]); 1194 } 1195 } 1196 fmls.push_back(fml); 1197 } 1198 } 1199 bool_rewriter(m).mk_or(fmls.size(), fmls.data(), fml); 1200 1201 fml = mk_not(m, m.mk_iff(q, fml)); 1202 ast_smt_pp pp(m); 1203 out << "; eliminate " << mk_pp(m_var, m) << "\n"; 1204 out << "(push 1)\n"; 1205 pp.display_smt2(out, fml); 1206 out << "(pop 1)\n\n"; 1207 #if 0 1208 DEBUG_CODE( 1209 smt_params params; 1210 params.m_simplify_bit2int = true; 1211 params.m_arith_enum_const_mod = true; 1212 params.m_bv_enable_int2bv2int = true; 1213 params.m_relevancy_lvl = 0; 1214 smt::kernel ctx(m, params); 1215 ctx.assert_expr(fml); 1216 lbool is_sat = ctx.check(); 1217 if (is_sat == l_true) { 1218 std::cout << "; Validation failed:\n"; 1219 std::cout << mk_pp(fml, m) << "\n"; 1220 } 1221 ); 1222 #endif 1223 1224 } 1225 for (unsigned i = 0; i < m_children.size(); ++i) { 1226 if (m_children[i]->fml()) { 1227 m_children[i]->display_validate(out); 1228 } 1229 } 1230 } 1231 }; 1232 1233 // ------------------------- 1234 // i_solver_context 1235 ~i_solver_context()1236 i_solver_context::~i_solver_context() { 1237 for (unsigned i = 0; i < m_plugins.size(); ++i) { 1238 dealloc(m_plugins[i]); 1239 } 1240 } 1241 operator ()(expr * e)1242 bool i_solver_context::is_relevant::operator()(expr* e) { 1243 for (unsigned i = 0; i < m_s.get_num_vars(); ++i) { 1244 if (m_s.contains(i)(e)) { 1245 return true; 1246 } 1247 } 1248 TRACE("qe_verbose", tout << "Not relevant: " << mk_ismt2_pp(e, m_s.get_manager()) << "\n";); 1249 return false; 1250 } 1251 is_var(expr * x,unsigned & idx) const1252 bool i_solver_context::is_var(expr* x, unsigned& idx) const { 1253 unsigned nv = get_num_vars(); 1254 for (unsigned i = 0; i < nv; ++i) { 1255 if (get_var(i) == x) { 1256 idx = i; 1257 return true; 1258 } 1259 } 1260 return false; 1261 } 1262 add_plugin(qe_solver_plugin * p)1263 void i_solver_context::add_plugin(qe_solver_plugin* p) { 1264 family_id fid = p->get_family_id(); 1265 SASSERT(fid != null_family_id); 1266 if (static_cast<int>(m_plugins.size()) <= fid) { 1267 m_plugins.resize(fid+1); 1268 } 1269 SASSERT(!m_plugins[fid]); 1270 m_plugins[fid] = p; 1271 } 1272 has_plugin(app * x)1273 bool i_solver_context::has_plugin(app* x) { 1274 family_id fid = x->get_sort()->get_family_id(); 1275 return 1276 0 <= fid && 1277 fid < static_cast<int>(m_plugins.size()) && 1278 m_plugins[fid] != 0; 1279 } 1280 plugin(app * x)1281 qe_solver_plugin& i_solver_context::plugin(app* x) { 1282 SASSERT(has_plugin(x)); 1283 return *(m_plugins[x->get_sort()->get_family_id()]); 1284 } 1285 mk_atom(expr * e,bool p,expr_ref & result)1286 void i_solver_context::mk_atom(expr* e, bool p, expr_ref& result) { 1287 ast_manager& m = get_manager(); 1288 TRACE("qe_verbose", tout << mk_ismt2_pp(e, m) << "\n";); 1289 for (unsigned i = 0; i < m_plugins.size(); ++i) { 1290 qe_solver_plugin* pl = m_plugins[i]; 1291 if (pl && pl->mk_atom(e, p, result)) { 1292 return; 1293 } 1294 } 1295 TRACE("qe_verbose", tout << "No plugin for " << mk_ismt2_pp(e, m) << "\n";); 1296 result = p?e:mk_not(m, e); 1297 } 1298 operator ()(expr * e,bool p,expr_ref & result)1299 void i_solver_context::mk_atom_fn::operator()(expr* e, bool p, expr_ref& result) { 1300 m_s.mk_atom(e, p, result); 1301 } 1302 collect_statistics(statistics & st) const1303 void i_solver_context::collect_statistics(statistics& st) const { 1304 // tbd 1305 } 1306 1307 typedef ref_vector_ptr_hash<expr, ast_manager> expr_ref_vector_hash; 1308 typedef ref_vector_ptr_eq<expr, ast_manager> expr_ref_vector_eq; 1309 typedef hashtable<expr_ref_vector*, expr_ref_vector_hash, expr_ref_vector_eq> clause_table; 1310 typedef value_trail<unsigned> _value_trail; 1311 1312 1313 class quant_elim_plugin : public i_solver_context { 1314 1315 ast_manager& m; 1316 quant_elim& m_qe; 1317 th_rewriter m_rewriter; 1318 smt::kernel m_solver; 1319 bv_util m_bv; 1320 expr_ref_vector m_literals; 1321 1322 bool_rewriter m_bool_rewriter; 1323 conjunctions m_conjs; 1324 1325 // maintain queue for variables. 1326 1327 app_ref_vector m_free_vars; // non-quantified variables 1328 app_ref_vector m_trail; 1329 1330 expr_ref m_fml; 1331 expr_ref m_subfml; 1332 1333 obj_map<app, app*> m_var2branch; // var -> bv-var, identify explored branch. 1334 obj_map<app, contains_app*> m_var2contains; // var -> contains_app 1335 obj_map<app, ptr_vector<app> > m_children; // var -> list of dependent children 1336 search_tree m_root; 1337 search_tree* m_current; // current branch 1338 1339 vector<unsigned_vector> m_partition; // cached latest partition of variables. 1340 1341 app_ref_vector m_new_vars; // variables added by solvers 1342 bool m_get_first; // get first satisfying branch. 1343 guarded_defs* m_defs; 1344 nnf_normalizer m_nnf; // nnf conversion 1345 1346 1347 public: 1348 quant_elim_plugin(ast_manager & m,quant_elim & qe,smt_params & p)1349 quant_elim_plugin(ast_manager& m, quant_elim& qe, smt_params& p): 1350 m(m), 1351 m_qe(qe), 1352 m_rewriter(m), 1353 m_solver(m, p), 1354 m_bv(m), 1355 m_literals(m), 1356 m_bool_rewriter(m), 1357 m_conjs(m), 1358 m_free_vars(m), 1359 m_trail(m), 1360 m_fml(m), 1361 m_subfml(m), 1362 m_root(nullptr, m, m.mk_true()), 1363 m_current(nullptr), 1364 m_new_vars(m), 1365 m_get_first(false), 1366 m_defs(nullptr), 1367 m_nnf(m, get_is_relevant(), get_mk_atom()) 1368 { 1369 params_ref params; 1370 params.set_bool("gcd_rounding", true); 1371 m_rewriter.updt_params(params); 1372 } 1373 ~quant_elim_plugin()1374 ~quant_elim_plugin() override { 1375 reset(); 1376 } 1377 reset()1378 void reset() { 1379 m_free_vars.reset(); 1380 m_trail.reset(); 1381 for (auto & kv : m_var2contains) { 1382 dealloc(kv.m_value); 1383 } 1384 m_var2contains.reset(); 1385 m_var2branch.reset(); 1386 m_root.reset(); 1387 m_new_vars.reset(); 1388 m_fml = nullptr; 1389 m_defs = nullptr; 1390 m_nnf.reset(); 1391 } 1392 add_plugin(qe_solver_plugin * p)1393 void add_plugin(qe_solver_plugin* p) { 1394 i_solver_context::add_plugin(p); 1395 m_conjs.add_plugin(p); 1396 } 1397 check(unsigned num_vars,app * const * vars,expr * assumption,expr_ref & fml,bool get_first,app_ref_vector & free_vars,guarded_defs * defs)1398 void check(unsigned num_vars, app* const* vars, 1399 expr* assumption, expr_ref& fml, bool get_first, 1400 app_ref_vector& free_vars, guarded_defs* defs) { 1401 1402 reset(); 1403 m_solver.push(); 1404 m_get_first = get_first; 1405 m_defs = defs; 1406 for (unsigned i = 0; i < num_vars; ++i) { 1407 if (has_plugin(vars[i])) { 1408 add_var(vars[i]); 1409 } 1410 else { 1411 m_free_vars.push_back(vars[i]); 1412 } 1413 } 1414 m_root.consume_vars(m_new_vars); 1415 m_current = &m_root; 1416 1417 // set sub-formula 1418 m_fml = fml; 1419 normalize(m_fml, m_root.pos_atoms(), m_root.neg_atoms()); 1420 expr_ref f(m_fml); 1421 get_max_relevant(get_is_relevant(), f, m_subfml); 1422 if (f.get() != m_subfml.get()) { 1423 m_fml = f; 1424 f = m_subfml; 1425 m_solver.assert_expr(f); 1426 } 1427 m_root.init(f); 1428 TRACE("qe", 1429 for (unsigned i = 0; i < num_vars; ++i) tout << mk_ismt2_pp(vars[i], m) << "\n"; 1430 tout << mk_ismt2_pp(f, m) << "\n";); 1431 1432 m_solver.assert_expr(m_fml); 1433 if (assumption) m_solver.assert_expr(assumption); 1434 bool is_sat = false; 1435 lbool res = l_true; 1436 while (res == l_true) { 1437 res = m_solver.check(); 1438 if (res == l_true && has_uninterpreted(m, m_fml)) 1439 res = l_undef; 1440 if (res == l_true) { 1441 is_sat = true; 1442 final_check(); 1443 } 1444 else { 1445 break; 1446 } 1447 } 1448 if (res == l_undef) { 1449 free_vars.append(num_vars, vars); 1450 reset(); 1451 m_solver.pop(1); 1452 return; 1453 } 1454 1455 if (!is_sat) { 1456 fml = m.mk_false(); 1457 if (m_fml.get() != m_subfml.get()) { 1458 scoped_ptr<expr_replacer> rp = mk_default_expr_replacer(m, false); 1459 rp->apply_substitution(to_app(m_subfml.get()), fml, m_fml); 1460 fml = m_fml; 1461 } 1462 reset(); 1463 m_solver.pop(1); 1464 return; 1465 } 1466 1467 if (!get_first) { 1468 expr_ref_vector result(m); 1469 m_root.get_leaves(result); 1470 m_bool_rewriter.mk_or(result.size(), result.data(), fml); 1471 } 1472 1473 if (defs) { 1474 m_root.get_leaves(*defs); 1475 defs->project(num_vars, vars); 1476 } 1477 1478 TRACE("qe", 1479 tout << "result:" << mk_ismt2_pp(fml, m) << "\n"; 1480 tout << "input: " << mk_ismt2_pp(m_fml, m) << "\n"; 1481 tout << "subformula: " << mk_ismt2_pp(m_subfml, m) << "\n"; 1482 m_root.display(tout); 1483 m_root.display_validate(tout); 1484 tout << "free: " << m_free_vars << "\n";); 1485 1486 free_vars.append(m_free_vars); 1487 if (!m_free_vars.empty() || m_solver.inconsistent()) { 1488 1489 if (m_fml.get() != m_subfml.get()) { 1490 scoped_ptr<expr_replacer> rp = mk_default_expr_replacer(m, false); 1491 rp->apply_substitution(to_app(m_subfml.get()), fml, m_fml); 1492 fml = m_fml; 1493 } 1494 } 1495 reset(); 1496 m_solver.pop(1); 1497 f = nullptr; 1498 } 1499 collect_statistics(statistics & st)1500 void collect_statistics(statistics& st) { 1501 m_solver.collect_statistics(st); 1502 } 1503 1504 private: 1505 final_check()1506 void final_check() { 1507 model_ref model; 1508 m_solver.get_model(model); 1509 scoped_ptr<model_evaluator> model_eval = alloc(model_evaluator, *model); 1510 1511 while (true) { 1512 TRACE("qe", model_v2_pp(tout, *model);); 1513 while (can_propagate_assignment(*model_eval)) { 1514 propagate_assignment(*model_eval); 1515 } 1516 VERIFY(CHOOSE_VAR == update_current(*model_eval, true)); 1517 SASSERT(m_current->fml()); 1518 if (l_true != m_solver.check()) { 1519 return; 1520 } 1521 m_solver.get_model(model); 1522 model_eval = alloc(model_evaluator, *model); 1523 search_tree* st = m_current; 1524 update_current(*model_eval, false); 1525 if (st == m_current) { 1526 break; 1527 } 1528 } 1529 pop(*model_eval); 1530 } 1531 get_manager()1532 ast_manager& get_manager() override { return m; } 1533 pos_atoms() const1534 atom_set const& pos_atoms() const override { return m_current->pos_atoms(); } 1535 neg_atoms() const1536 atom_set const& neg_atoms() const override { return m_current->neg_atoms(); } 1537 get_num_vars() const1538 unsigned get_num_vars() const override { return m_current->num_free_vars(); } 1539 get_var(unsigned idx) const1540 app* get_var(unsigned idx) const override { return m_current->free_var(idx); } 1541 get_vars() const1542 app_ref_vector const& get_vars() const override { return m_current->free_vars(); } 1543 contains(unsigned idx)1544 contains_app& contains(unsigned idx) override { return contains(get_var(idx)); } 1545 1546 // 1547 // The variable at idx is eliminated (without branching). 1548 // elim_var(unsigned idx,expr * _fml,expr * def)1549 void elim_var(unsigned idx, expr* _fml, expr* def) override { 1550 app* x = get_var(idx); 1551 expr_ref fml(_fml, m); 1552 TRACE("qe", tout << mk_pp(x,m) << " " << mk_pp(def, m) << "\n";); 1553 m_current->set_var(x, rational(1)); 1554 m_current = m_current->add_child(fml); 1555 m_current->add_def(x, def); 1556 m_current->consume_vars(m_new_vars); 1557 normalize(*m_current); 1558 } 1559 add_var(app * x)1560 void add_var(app* x) override { 1561 m_new_vars.push_back(x); 1562 if (m_var2branch.contains(x)) { 1563 return; 1564 } 1565 contains_app* ca = alloc(contains_app, m, x); 1566 m_var2contains.insert(x, ca); 1567 app* bv = nullptr; 1568 if (m.is_bool(x) || m_bv.is_bv(x)) { 1569 bv = x; 1570 } 1571 else { 1572 bv = m.mk_fresh_const("b", m_bv.mk_sort(20)); 1573 m_trail.push_back(bv); 1574 } 1575 TRACE("qe", tout << "Add branch var: " << mk_ismt2_pp(x, m) << " " << mk_ismt2_pp(bv, m) << "\n";); 1576 m_var2branch.insert(x, bv); 1577 } 1578 add_constraint(bool use_current_val,expr * l1=nullptr,expr * l2=nullptr,expr * l3=nullptr)1579 void add_constraint(bool use_current_val, expr* l1 = nullptr, expr* l2 = nullptr, expr* l3 = nullptr) override { 1580 search_tree* node = m_current; 1581 expr_ref _l1(l1, m), _l2(l2, m), _l3(l3, m); 1582 if (!use_current_val) { 1583 node = m_current->parent(); 1584 } 1585 m_literals.reset(); 1586 while (node) { 1587 m_literals.push_back(mk_not(m, node->assignment())); 1588 node = node->parent(); 1589 } 1590 add_literal(l1); 1591 add_literal(l2); 1592 add_literal(l3); 1593 expr_ref fml(m); 1594 fml = m.mk_or(m_literals); 1595 TRACE("qe", tout << fml << "\n";); 1596 m_solver.assert_expr(fml); 1597 } 1598 blast_or(app * var,expr_ref & fml)1599 void blast_or(app* var, expr_ref& fml) override { 1600 m_qe.eliminate_exists(1, &var, fml, m_free_vars, false, nullptr); 1601 } 1602 eliminate_exists(unsigned num_vars,app * const * vars,expr_ref & fml,bool get_first,guarded_defs * defs)1603 lbool eliminate_exists(unsigned num_vars, app* const* vars, expr_ref& fml, bool get_first, guarded_defs* defs) { 1604 return m_qe.eliminate_exists(num_vars, vars, fml, m_free_vars, get_first, defs); 1605 } 1606 1607 private: 1608 add_literal(expr * l)1609 void add_literal(expr* l) { 1610 if (l != nullptr) { 1611 m_literals.push_back(l); 1612 } 1613 } 1614 get_max_relevant(i_expr_pred & is_relevant,expr_ref & fml,expr_ref & subfml)1615 void get_max_relevant(i_expr_pred& is_relevant, expr_ref& fml, expr_ref& subfml) { 1616 if (m.is_and(fml) || m.is_or(fml)) { 1617 app* a = to_app(fml); 1618 unsigned num_args = a->get_num_args(); 1619 ptr_buffer<expr> r_args; 1620 ptr_buffer<expr> i_args; 1621 for (unsigned i = 0; i < num_args; ++i) { 1622 expr* arg = a->get_arg(i); 1623 if (is_relevant(arg)) { 1624 r_args.push_back(arg); 1625 } 1626 else { 1627 i_args.push_back(arg); 1628 } 1629 } 1630 if (r_args.empty() || i_args.empty()) { 1631 subfml = fml; 1632 } 1633 else if (r_args.size() == 1) { 1634 expr_ref tmp(r_args[0], m); 1635 get_max_relevant(is_relevant, tmp, subfml); 1636 i_args.push_back(tmp); 1637 fml = m.mk_app(a->get_decl(), i_args.size(), i_args.data()); 1638 } 1639 else { 1640 subfml = m.mk_app(a->get_decl(), r_args.size(), r_args.data()); 1641 i_args.push_back(subfml); 1642 fml = m.mk_app(a->get_decl(), i_args.size(), i_args.data()); 1643 } 1644 } 1645 else { 1646 subfml = fml; 1647 } 1648 } 1649 get_branch_id(app * x)1650 app* get_branch_id(app* x) { 1651 return m_var2branch[x]; 1652 } 1653 extract_partition(ptr_vector<app> & vars)1654 bool extract_partition(ptr_vector<app>& vars) { 1655 if (m_partition.empty()) { 1656 return false; 1657 } 1658 1659 unsigned_vector& vec = m_partition.back(); 1660 for (auto v : vec) 1661 vars.push_back(m_current->free_var(v)); 1662 m_partition.pop_back(); 1663 return true; 1664 } 1665 1666 enum update_status { CHOOSE_VAR, NEED_PROPAGATION }; 1667 update_current(model_evaluator & model_eval,bool apply)1668 update_status update_current(model_evaluator& model_eval, bool apply) { 1669 SASSERT(m_fml); 1670 m_current = &m_root; 1671 rational branch, nb; 1672 while (true) { 1673 SASSERT(m_current->fml()); 1674 if (m_current->is_unit()) { 1675 m_current = m_current->child(); 1676 continue; 1677 } 1678 if (!m_current->has_var()) { 1679 return CHOOSE_VAR; 1680 } 1681 1682 app* x = m_current->var(); 1683 app* b = get_branch_id(x); 1684 nb = m_current->get_num_branches(); 1685 expr_ref fml(m_current->fml(), m); 1686 if (!eval(model_eval, b, branch) || branch >= nb) { 1687 TRACE("qe", tout << "evaluation failed: setting branch to 0\n";); 1688 branch = rational::zero(); 1689 } 1690 SASSERT(!branch.is_neg()); 1691 if (!m_current->has_branch(branch)) { 1692 if (apply) { 1693 app_ref assignment(mk_eq_value(b, branch), m); 1694 m_current = m_current->add_child(branch, assignment); 1695 plugin(x).assign(contains(x), fml, branch); 1696 m_current->consume_vars(m_new_vars); 1697 } 1698 return NEED_PROPAGATION; 1699 } 1700 m_current = m_current->child(branch); 1701 if (m_current->fml() == nullptr) { 1702 SASSERT(!m_current->has_var()); 1703 if (apply) { 1704 expr_ref def(m); 1705 plugin(x).subst(contains(x), branch, fml, m_defs?&def:nullptr); 1706 SASSERT(!contains(x)(fml)); 1707 m_current->consume_vars(m_new_vars); 1708 m_current->init(fml); 1709 m_current->add_def(x, def); 1710 normalize(*m_current); 1711 } 1712 return CHOOSE_VAR; 1713 } 1714 } 1715 } 1716 pop(model_evaluator & model_eval)1717 void pop(model_evaluator& model_eval) { 1718 // 1719 // Eliminate trivial quantifiers by solving 1720 // variables that can be eliminated. 1721 // 1722 solve_vars(); 1723 expr* fml = m_current->fml(); 1724 // we are done splitting. 1725 if (m_current->num_free_vars() == 0) { 1726 block_assignment(); 1727 return; 1728 } 1729 1730 expr_ref fml_closed(m), fml_open(m), fml_mixed(m); 1731 unsigned num_vars = m_current->num_free_vars(); 1732 ptr_vector<contains_app> cont; 1733 ptr_vector<app> vars; 1734 for (unsigned i = 0; i < num_vars; ++i) { 1735 cont.push_back(&contains(i)); 1736 vars.push_back(m_current->free_var(i)); 1737 } 1738 m_conjs.get_partition(fml, num_vars, vars.data(), fml_closed, fml_mixed, fml_open); 1739 if (m.is_and(fml_open) && 1740 m_conjs.partition_vars( 1741 num_vars, cont.data(), 1742 to_app(fml_open)->get_num_args(), to_app(fml_open)->get_args(), 1743 m_partition)) { 1744 process_partition(); 1745 return; 1746 } 1747 1748 // 1749 // The closed portion of the formula 1750 // can be used as the quantifier-free portion, 1751 // unless the current state is unsatisfiable. 1752 // 1753 if (m.is_true(fml_mixed)) { 1754 SASSERT(l_false != m_solver.check()); 1755 m_current = m_current->add_child(fml_closed); 1756 for (unsigned i = 0; m_defs && i < m_current->num_free_vars(); ++i) { 1757 expr_ref val(m); 1758 app* x = m_current->free_var(i); 1759 model_eval(x, val); 1760 // hack: assign may add new variables to the branch. 1761 if (val == x) { 1762 model_ref model; 1763 lbool is_sat = m_solver.check(); 1764 if (is_sat == l_undef) return; 1765 m_solver.get_model(model); 1766 SASSERT(is_sat == l_true); 1767 model_evaluator model_eval2(*model); 1768 model_eval2.set_model_completion(true); 1769 model_eval2(x, val); 1770 } 1771 TRACE("qe", tout << mk_pp(x,m) << " " << mk_pp(val, m) << "\n";); 1772 m_current->add_def(x, val); 1773 } 1774 m_current->reset_free_vars(); 1775 block_assignment(); 1776 return; 1777 } 1778 // 1779 // one variable is to be processed. 1780 // 1781 constrain_assignment(); 1782 } 1783 normalize(search_tree & st)1784 void normalize(search_tree& st) { 1785 normalize(st.fml_ref(), st.pos_atoms(), st.neg_atoms()); 1786 } 1787 normalize(expr_ref & result,atom_set & pos,atom_set & neg)1788 void normalize(expr_ref& result, atom_set& pos, atom_set& neg) { 1789 m_rewriter(result); 1790 bool simplified = true; 1791 while (simplified) { 1792 simplified = false; 1793 for (unsigned i = 0; !simplified && i < m_plugins.size(); ++i) { 1794 qe_solver_plugin* pl = m_plugins[i]; 1795 simplified = pl && pl->simplify(result); 1796 } 1797 } 1798 TRACE("qe_verbose", tout << "simp: " << mk_ismt2_pp(result.get(), m) << "\n";); 1799 m_nnf(result, pos, neg); 1800 TRACE("qe", tout << "nnf: " << mk_ismt2_pp(result.get(), m) << "\n";); 1801 } 1802 1803 // 1804 // variable queuing. 1805 // 1806 1807 1808 // ------------------------------------------------ 1809 // propagate the assignments to branch 1810 // literals to implied constraints on the 1811 // variable. 1812 // 1813 get_propagate_value(model_evaluator & model_eval,search_tree * node,app * & b,rational & b_val)1814 bool get_propagate_value(model_evaluator& model_eval, search_tree* node, app*& b, rational& b_val) { 1815 return node->has_var() && eval(model_eval, get_branch_id(node->var()), b_val); 1816 } 1817 can_propagate_assignment(model_evaluator & model_eval)1818 bool can_propagate_assignment(model_evaluator& model_eval) { 1819 return m_fml && NEED_PROPAGATION == update_current(model_eval, false); 1820 } 1821 propagate_assignment(model_evaluator & model_eval)1822 void propagate_assignment(model_evaluator& model_eval) { 1823 if (m_fml) { 1824 update_current(model_eval, true); 1825 } 1826 } 1827 1828 // 1829 // evaluate the Boolean or bit-vector 'b' in 1830 // the current model 1831 // eval(model_evaluator & model_eval,app * b,rational & val)1832 bool eval(model_evaluator& model_eval, app* b, rational& val) { 1833 unsigned bv_size; 1834 expr_ref res(m); 1835 model_eval(b, res); 1836 SASSERT(m.is_bool(b) || m_bv.is_bv(b)); 1837 if (m.is_true(res)) { 1838 val = rational::one(); 1839 return true; 1840 } 1841 else if (m.is_false(res)) { 1842 val = rational::zero(); 1843 return true; 1844 } 1845 else if (m_bv.is_numeral(res, val, bv_size)) { 1846 return true; 1847 } 1848 else { 1849 return false; 1850 } 1851 } 1852 1853 // 1854 // create literal 'b = r' 1855 // mk_eq_value(app * b,rational const & vl)1856 app* mk_eq_value(app* b, rational const& vl) { 1857 if (m.is_bool(b)) { 1858 if (vl.is_zero()) return to_app(mk_not(m, b)); 1859 if (vl.is_one()) return b; 1860 UNREACHABLE(); 1861 } 1862 SASSERT(m_bv.is_bv(b)); 1863 app_ref value(m_bv.mk_numeral(vl, m_bv.get_bv_size(b)), m); 1864 return m.mk_eq(b, value); 1865 } 1866 1867 is_eq_value(app * e,app * & bv,rational & v)1868 bool is_eq_value(app* e, app*& bv, rational& v) { 1869 unsigned sz = 0; 1870 if (!m.is_eq(e)) return false; 1871 expr* e0 = e->get_arg(0), *e1 = e->get_arg(1); 1872 if (!m_bv.is_bv(e0)) return false; 1873 if (m_bv.is_numeral(e0, v, sz) && is_app(e1)) { 1874 bv = to_app(e1); 1875 return true; 1876 } 1877 if (m_bv.is_numeral(e1, v, sz) && is_app(e0)) { 1878 bv = to_app(e0); 1879 return true; 1880 } 1881 return false; 1882 } 1883 1884 1885 // 1886 // the current state is satisfiable. 1887 // all bound decisions have been made. 1888 // block_assignment()1889 void block_assignment() { 1890 TRACE("qe_verbose", m_solver.display(tout);); 1891 add_constraint(true); 1892 } 1893 1894 // 1895 // The variable v is to be assigned a value in a range. 1896 // constrain_assignment()1897 void constrain_assignment() { 1898 SASSERT(m_current->fml()); 1899 rational k; 1900 app* x; 1901 if (!find_min_weight(x, k)) { 1902 return; 1903 } 1904 1905 m_current->set_var(x, k); 1906 TRACE("qe", tout << mk_pp(x, m) << " := " << k << "\n";); 1907 if (m_bv.is_bv(x)) { 1908 return; 1909 } 1910 1911 app* b = get_branch_id(x); 1912 // 1913 // Create implication: 1914 // 1915 // assign_0 /\ ... /\ assign_{v-1} => b(v) <= k-1 1916 // where 1917 // - assign_i is the current assignment: i = b(i) 1918 // - k is the number of cases for v 1919 // 1920 1921 if (m.is_bool(b)) { 1922 SASSERT(k <= rational(2)); 1923 return; 1924 } 1925 1926 SASSERT(m_bv.is_bv(b)); 1927 SASSERT(k.is_pos()); 1928 app_ref max_val(m_bv.mk_numeral(k-rational::one(), m_bv.get_bv_size(b)), m); 1929 expr_ref ub(m_bv.mk_ule(b, max_val), m); 1930 add_constraint(true, ub); 1931 } 1932 1933 1934 1935 // 1936 // Process the partition stored in m_vars. 1937 // process_partition()1938 void process_partition() { 1939 expr_ref fml(m_current->fml(), m); 1940 ptr_vector<app> vars; 1941 bool closed = true; 1942 while (extract_partition(vars)) { 1943 lbool r = m_qe.eliminate_exists(vars.size(), vars.data(), fml, m_free_vars, m_get_first, m_defs); 1944 vars.reset(); 1945 closed = closed && (r != l_undef); 1946 } 1947 TRACE("qe", tout << fml << " free: " << m_current->free_vars() << "\n";); 1948 m_current->add_child(fml)->reset_free_vars(); 1949 block_assignment(); 1950 } 1951 1952 1953 // variable queueing. 1954 contains(app * x)1955 contains_app& contains(app* x) { 1956 return *m_var2contains[x]; 1957 } 1958 find_min_weight(app * & x,rational & num_branches)1959 bool find_min_weight(app*& x, rational& num_branches) { 1960 SASSERT(!m_current->has_var()); 1961 while (m_current->num_free_vars() > 0) { 1962 unsigned weight = UINT_MAX; 1963 unsigned nv = m_current->num_free_vars(); 1964 expr* fml = m_current->fml(); 1965 unsigned index = 0; 1966 for (unsigned i = 0; i < nv; ++i) { 1967 x = get_var(i); 1968 if (!has_plugin(x)) { 1969 break; 1970 } 1971 unsigned weight1 = plugin(get_var(i)).get_weight(contains(i), fml); 1972 if (weight1 < weight) { 1973 index = i; 1974 } 1975 } 1976 x = get_var(index); 1977 if (has_plugin(x) && 1978 plugin(x).get_num_branches(contains(x), fml, num_branches)) { 1979 return true; 1980 } 1981 TRACE("qe", tout << "setting variable " << mk_pp(x, m) << " free\n";); 1982 m_free_vars.push_back(x); 1983 m_current->del_var(x); 1984 } 1985 return false; 1986 } 1987 1988 // 1989 // Solve for variables in fml. 1990 // Add a unit branch when variables are solved. 1991 // solve_vars()1992 void solve_vars() { 1993 bool solved = true; 1994 while (solved) { 1995 expr_ref fml(m_current->fml(), m); 1996 TRACE("qe", tout << fml << "\n";); 1997 conj_enum conjs(m, fml); 1998 solved = false; 1999 for (unsigned i = 0; !solved && i < m_plugins.size(); ++i) { 2000 qe_solver_plugin* p = m_plugins[i]; 2001 solved = p && p->solve(conjs, fml); 2002 SASSERT(m_new_vars.empty()); 2003 } 2004 } 2005 } 2006 2007 }; 2008 2009 // ------------------------------------------------ 2010 // quant_elim 2011 2012 2013 class quant_elim_new : public quant_elim { 2014 ast_manager& m; 2015 smt_params& m_fparams; 2016 expr_ref m_assumption; 2017 bool m_produce_models; 2018 ptr_vector<quant_elim_plugin> m_plugins; 2019 bool m_eliminate_variables_as_block; 2020 2021 public: quant_elim_new(ast_manager & m,smt_params & p)2022 quant_elim_new(ast_manager& m, smt_params& p) : 2023 m(m), 2024 m_fparams(p), 2025 m_assumption(m), 2026 m_produce_models(m_fparams.m_model), 2027 m_eliminate_variables_as_block(true) 2028 { 2029 } 2030 ~quant_elim_new()2031 ~quant_elim_new() override { 2032 reset(); 2033 } 2034 reset()2035 void reset() { 2036 for (unsigned i = 0; i < m_plugins.size(); ++i) { 2037 dealloc(m_plugins[i]); 2038 } 2039 } 2040 checkpoint()2041 void checkpoint() { 2042 if (!m.inc()) 2043 throw tactic_exception(m.limit().get_cancel_msg()); 2044 } 2045 2046 collect_statistics(statistics & st) const2047 void collect_statistics(statistics & st) const override { 2048 for (unsigned i = 0; i < m_plugins.size(); ++i) { 2049 m_plugins[i]->collect_statistics(st); 2050 } 2051 } 2052 updt_params(params_ref const & p)2053 void updt_params(params_ref const& p) override { 2054 m_eliminate_variables_as_block = p.get_bool("eliminate_variables_as_block", m_eliminate_variables_as_block); 2055 } 2056 eliminate(bool is_forall,unsigned num_vars,app * const * vars,expr_ref & fml)2057 void eliminate(bool is_forall, unsigned num_vars, app* const* vars, expr_ref& fml) override { 2058 if (is_forall) { 2059 eliminate_forall_bind(num_vars, vars, fml); 2060 } 2061 else { 2062 eliminate_exists_bind(num_vars, vars, fml); 2063 } 2064 } 2065 bind_variables(unsigned num_vars,app * const * vars,expr_ref & fml)2066 virtual void bind_variables(unsigned num_vars, app* const* vars, expr_ref& fml) { 2067 if (num_vars > 0) { 2068 ptr_vector<sort> sorts; 2069 vector<symbol> names; 2070 app_ref_vector free_vars(m); 2071 for (unsigned i = 0; i < num_vars; ++i) { 2072 contains_app contains_x(m, vars[i]); 2073 if (contains_x(fml)) { 2074 sorts.push_back(vars[i]->get_sort()); 2075 names.push_back(vars[i]->get_decl()->get_name()); 2076 free_vars.push_back(vars[i]); 2077 } 2078 } 2079 if (!free_vars.empty()) { 2080 expr_ref tmp = expr_abstract(free_vars, fml); 2081 fml = m.mk_exists(free_vars.size(), sorts.data(), names.data(), tmp, 1); 2082 } 2083 } 2084 } 2085 set_assumption(expr * fml)2086 void set_assumption(expr* fml) override { 2087 m_assumption = fml; 2088 } 2089 2090 eliminate_exists(unsigned num_vars,app * const * vars,expr_ref & fml,app_ref_vector & free_vars,bool get_first,guarded_defs * defs)2091 lbool eliminate_exists( 2092 unsigned num_vars, app* const* vars, expr_ref& fml, 2093 app_ref_vector& free_vars, bool get_first, guarded_defs* defs) override { 2094 if (get_first) { 2095 return eliminate_block(num_vars, vars, fml, free_vars, get_first, defs); 2096 } 2097 if (m_eliminate_variables_as_block) { 2098 return eliminate_block(num_vars, vars, fml, free_vars, get_first, defs); 2099 } 2100 for (unsigned i = 0; i < num_vars; ++i) { 2101 lbool r = eliminate_block(1, vars+i, fml, free_vars, get_first, defs); 2102 switch(r) { 2103 case l_false: 2104 return l_false; 2105 case l_undef: 2106 free_vars.append(num_vars-i-1,vars+1+i); 2107 return l_undef; 2108 default: 2109 break; 2110 } 2111 } 2112 return l_true; 2113 } 2114 2115 private: 2116 eliminate_block(unsigned num_vars,app * const * vars,expr_ref & fml,app_ref_vector & free_vars,bool get_first,guarded_defs * defs)2117 lbool eliminate_block( 2118 unsigned num_vars, app* const* vars, expr_ref& fml, 2119 app_ref_vector& free_vars, bool get_first, guarded_defs* defs) { 2120 2121 checkpoint(); 2122 2123 if (has_quantifiers(fml)) { 2124 free_vars.append(num_vars, vars); 2125 return l_undef; 2126 } 2127 2128 flet<bool> fl1(m_fparams.m_model, true); 2129 flet<bool> fl2(m_fparams.m_simplify_bit2int, true); 2130 flet<bool> fl3(m_fparams.m_arith_enum_const_mod, true); 2131 flet<bool> fl4(m_fparams.m_bv_enable_int2bv2int, true); 2132 flet<bool> fl5(m_fparams.m_array_canonize_simplify, true); 2133 flet<unsigned> fl6(m_fparams.m_relevancy_lvl, 0); 2134 TRACE("qe", 2135 for (unsigned i = 0; i < num_vars; ++i) { 2136 tout << mk_ismt2_pp(vars[i], m) << " "; 2137 } 2138 tout << "\n"; 2139 tout << mk_ismt2_pp(fml, m) << "\n"; 2140 ); 2141 2142 expr_ref fml0(fml, m); 2143 2144 scoped_ptr<quant_elim_plugin> th; 2145 pop_context(th); 2146 2147 th->check(num_vars, vars, m_assumption, fml, get_first, free_vars, defs); 2148 2149 push_context(th.detach()); 2150 TRACE("qe", 2151 for (unsigned i = 0; i < num_vars; ++i) { 2152 tout << mk_ismt2_pp(vars[i], m) << " "; 2153 } 2154 tout << "\n"; 2155 tout << "Input:\n" << mk_ismt2_pp(fml0, m) << "\n"; 2156 tout << "Result:\n" << mk_ismt2_pp(fml, m) << "\n";); 2157 2158 if (m.is_false(fml)) { 2159 return l_false; 2160 } 2161 if (free_vars.empty()) { 2162 return l_true; 2163 } 2164 return l_undef; 2165 } 2166 pop_context(scoped_ptr<quant_elim_plugin> & th)2167 void pop_context(scoped_ptr<quant_elim_plugin>& th) { 2168 if (m_plugins.empty()) { 2169 th = alloc(quant_elim_plugin, m, *this, m_fparams); 2170 th->add_plugin(mk_bool_plugin(*th)); 2171 th->add_plugin(mk_bv_plugin(*th)); 2172 th->add_plugin(mk_arith_plugin(*th, m_produce_models, m_fparams)); 2173 th->add_plugin(mk_array_plugin(*th)); 2174 th->add_plugin(mk_datatype_plugin(*th)); 2175 th->add_plugin(mk_dl_plugin(*th)); 2176 } 2177 else { 2178 th = m_plugins.back(); 2179 m_plugins.pop_back(); 2180 } 2181 } 2182 push_context(quant_elim_plugin * th)2183 void push_context(quant_elim_plugin* th) { 2184 m_plugins.push_back(th); 2185 th->reset(); 2186 } 2187 eliminate_exists_bind(unsigned num_vars,app * const * vars,expr_ref & fml)2188 void eliminate_exists_bind(unsigned num_vars, app* const* vars, expr_ref& fml) { 2189 checkpoint(); 2190 app_ref_vector free_vars(m); 2191 eliminate_exists(num_vars, vars, fml, free_vars, false, nullptr); 2192 bind_variables(free_vars.size(), free_vars.data(), fml); 2193 } 2194 eliminate_forall_bind(unsigned num_vars,app * const * vars,expr_ref & fml)2195 void eliminate_forall_bind(unsigned num_vars, app* const* vars, expr_ref& fml) { 2196 expr_ref tmp(m); 2197 bool_rewriter rw(m); 2198 rw.mk_not(fml, tmp); 2199 eliminate_exists_bind(num_vars, vars, tmp); 2200 rw.mk_not(tmp, fml); 2201 } 2202 2203 }; 2204 2205 // ------------------------------------------------ 2206 // expr_quant_elim 2207 expr_quant_elim(ast_manager & m,smt_params const & fp,params_ref const & p)2208 expr_quant_elim::expr_quant_elim(ast_manager& m, smt_params const& fp, params_ref const& p): 2209 m(m), 2210 m_fparams(fp), 2211 m_params(p), 2212 m_trail(m), 2213 m_qe(nullptr), 2214 m_assumption(m.mk_true()) 2215 { 2216 } 2217 ~expr_quant_elim()2218 expr_quant_elim::~expr_quant_elim() { 2219 dealloc(m_qe); 2220 } 2221 operator ()(expr * assumption,expr * fml,expr_ref & result)2222 void expr_quant_elim::operator()(expr* assumption, expr* fml, expr_ref& result) { 2223 TRACE("qe", 2224 if (assumption) tout << "elim assumption\n" << mk_ismt2_pp(assumption, m) << "\n"; 2225 tout << "elim input\n" << mk_ismt2_pp(fml, m) << "\n";); 2226 expr_ref_vector bound(m); 2227 result = fml; 2228 m_assumption = assumption; 2229 instantiate_expr(bound, result); 2230 elim(result); 2231 m_trail.reset(); 2232 m_visited.reset(); 2233 abstract_expr(bound.size(), bound.data(), result); 2234 TRACE("qe", tout << "elim result\n" << mk_ismt2_pp(result, m) << "\n";); 2235 } 2236 updt_params(params_ref const & p)2237 void expr_quant_elim::updt_params(params_ref const& p) { 2238 init_qe(); 2239 m_qe->updt_params(p); 2240 } 2241 collect_param_descrs(param_descrs & r)2242 void expr_quant_elim::collect_param_descrs(param_descrs& r) { 2243 r.insert("eliminate_variables_as_block", CPK_BOOL, 2244 "(default: true) eliminate variables as a block (true) or one at a time (false)"); 2245 } 2246 init_qe()2247 void expr_quant_elim::init_qe() { 2248 if (!m_qe) { 2249 m_qe = alloc(quant_elim_new, m, const_cast<smt_params&>(m_fparams)); 2250 } 2251 } 2252 2253 instantiate_expr(expr_ref_vector & bound,expr_ref & fml)2254 void expr_quant_elim::instantiate_expr(expr_ref_vector& bound, expr_ref& fml) { 2255 expr_free_vars fv; 2256 fv(fml); 2257 fv.set_default_sort(m.mk_bool_sort()); 2258 if (!fv.empty()) { 2259 expr_ref tmp(m); 2260 for (unsigned i = fv.size(); i > 0;) { 2261 --i; 2262 bound.push_back(m.mk_fresh_const("bound", fv[i])); 2263 } 2264 var_subst subst(m); 2265 fml = subst(fml, bound.size(), bound.data()); 2266 } 2267 } 2268 abstract_expr(unsigned sz,expr * const * bound,expr_ref & fml)2269 void expr_quant_elim::abstract_expr(unsigned sz, expr* const* bound, expr_ref& fml) { 2270 if (sz > 0) { 2271 fml = expr_abstract(m, 0, sz, bound, fml); 2272 } 2273 } 2274 extract_vars(quantifier * q,expr_ref & new_body,app_ref_vector & vars)2275 void extract_vars(quantifier* q, expr_ref& new_body, app_ref_vector& vars) { 2276 ast_manager& m = new_body.get_manager(); 2277 expr_ref tmp(m); 2278 unsigned nd = q->get_num_decls(); 2279 for (unsigned i = 0; i < nd; ++i) { 2280 vars.push_back(m.mk_fresh_const("x",q->get_decl_sort(i))); 2281 } 2282 expr* const* exprs = (expr* const*)(vars.data()); 2283 var_subst subst(m); 2284 tmp = subst(new_body, vars.size(), exprs); 2285 inv_var_shifter shift(m); 2286 shift(tmp, vars.size(), new_body); 2287 } 2288 elim(expr_ref & result)2289 void expr_quant_elim::elim(expr_ref& result) { 2290 expr_ref tmp(m); 2291 ptr_vector<expr> todo; 2292 2293 m_trail.push_back(result); 2294 todo.push_back(result); 2295 expr* e = nullptr, *r = nullptr; 2296 2297 while (!todo.empty()) { 2298 e = todo.back(); 2299 if (m_visited.contains(e)) { 2300 todo.pop_back(); 2301 continue; 2302 } 2303 2304 switch(e->get_kind()) { 2305 case AST_APP: { 2306 app* a = to_app(e); 2307 expr_ref_vector args(m); 2308 bool all_visited = true; 2309 for (expr* arg : *a) { 2310 if (m_visited.find(arg, r)) { 2311 args.push_back(r); 2312 } 2313 else { 2314 todo.push_back(arg); 2315 all_visited = false; 2316 } 2317 } 2318 if (all_visited) { 2319 r = m.mk_app(a->get_decl(), args.size(), args.data()); 2320 todo.pop_back(); 2321 m_trail.push_back(r); 2322 m_visited.insert(e, r); 2323 } 2324 break; 2325 } 2326 case AST_QUANTIFIER: { 2327 app_ref_vector vars(m); 2328 quantifier* q = to_quantifier(e); 2329 if (is_lambda(q)) { 2330 tmp = e; 2331 } 2332 else { 2333 bool is_fa = is_forall(q); 2334 tmp = q->get_expr(); 2335 extract_vars(q, tmp, vars); 2336 elim(tmp); 2337 init_qe(); 2338 m_qe->set_assumption(m_assumption); 2339 m_qe->eliminate(is_fa, vars.size(), vars.data(), tmp); 2340 } 2341 m_trail.push_back(tmp); 2342 m_visited.insert(e, tmp); 2343 todo.pop_back(); 2344 break; 2345 } 2346 default: 2347 UNREACHABLE(); 2348 break; 2349 } 2350 } 2351 2352 VERIFY (m_visited.find(result, e)); 2353 result = e; 2354 } 2355 collect_statistics(statistics & st) const2356 void expr_quant_elim::collect_statistics(statistics & st) const { 2357 if (m_qe) { 2358 m_qe->collect_statistics(st); 2359 } 2360 } 2361 first_elim(unsigned num_vars,app * const * vars,expr_ref & fml,def_vector & defs)2362 lbool expr_quant_elim::first_elim(unsigned num_vars, app* const* vars, expr_ref& fml, def_vector& defs) { 2363 app_ref_vector fvs(m); 2364 init_qe(); 2365 guarded_defs gdefs(m); 2366 lbool res = m_qe->eliminate_exists(num_vars, vars, fml, fvs, true, &gdefs); 2367 if (gdefs.size() > 0) { 2368 defs.reset(); 2369 defs.append(gdefs.defs(0)); 2370 fml = gdefs.guard(0); 2371 } 2372 return res; 2373 } 2374 solve_for_var(app * var,expr * fml,guarded_defs & defs)2375 bool expr_quant_elim::solve_for_var(app* var, expr* fml, guarded_defs& defs) { 2376 return solve_for_vars(1,&var, fml, defs); 2377 } 2378 solve_for_vars(unsigned num_vars,app * const * vars,expr * _fml,guarded_defs & defs)2379 bool expr_quant_elim::solve_for_vars(unsigned num_vars, app* const* vars, expr* _fml, guarded_defs& defs) { 2380 app_ref_vector fvs(m); 2381 expr_ref fml(_fml, m); 2382 TRACE("qe", tout << mk_pp(fml, m) << "\n";); 2383 init_qe(); 2384 lbool is_sat = m_qe->eliminate_exists(num_vars, vars, fml, fvs, false, &defs); 2385 return is_sat != l_undef; 2386 } 2387 2388 2389 2390 2391 2392 #if 0 2393 // ------------------------------------------------ 2394 // expr_quant_elim_star1 2395 2396 bool expr_quant_elim_star1::visit_quantifier(quantifier * q) { 2397 if (!is_target(q)) { 2398 return true; 2399 } 2400 bool visited = true; 2401 visit(q->get_expr(), visited); 2402 return visited; 2403 } 2404 2405 void expr_quant_elim_star1::reduce1_quantifier(quantifier * q) { 2406 if (!is_target(q)) { 2407 cache_result(q, q, 0); 2408 return; 2409 } 2410 2411 quantifier_ref new_q(m); 2412 expr * new_body = 0; 2413 proof * new_pr; 2414 get_cached(q->get_expr(), new_body, new_pr); 2415 new_q = m.update_quantifier(q, new_body); 2416 expr_ref r(m); 2417 m_quant_elim(m_assumption, new_q, r); 2418 if (q == r.get()) { 2419 cache_result(q, q, 0); 2420 return; 2421 } 2422 proof_ref pr(m); 2423 if (m.proofs_enabled()) { 2424 pr = m.mk_rewrite(q, r); // TODO: improve justification 2425 } 2426 cache_result(q, r, pr); 2427 } 2428 2429 expr_quant_elim_star1::expr_quant_elim_star1(ast_manager& m, smt_params const& p): 2430 simplifier(m), m_quant_elim(m, p), m_assumption(m.mk_true()) 2431 { 2432 } 2433 #endif 2434 2435 hoist_exists(expr_ref & fml,app_ref_vector & vars)2436 void hoist_exists(expr_ref& fml, app_ref_vector& vars) { 2437 quantifier_hoister hoister(fml.get_manager()); 2438 hoister.pull_exists(fml, vars, fml); 2439 } 2440 mk_exists(unsigned num_bound,app * const * vars,expr_ref & fml)2441 void mk_exists(unsigned num_bound, app* const* vars, expr_ref& fml) { 2442 ast_manager& m = fml.get_manager(); 2443 expr_ref tmp(m); 2444 expr_abstract(m, 0, num_bound, (expr*const*)vars, fml, tmp); 2445 ptr_vector<sort> sorts; 2446 svector<symbol> names; 2447 for (unsigned i = 0; i < num_bound; ++i) { 2448 sorts.push_back(vars[i]->get_decl()->get_range()); 2449 names.push_back(vars[i]->get_decl()->get_name()); 2450 } 2451 if (num_bound > 0) { 2452 tmp = m.mk_exists(num_bound, sorts.data(), names.data(), tmp, 1); 2453 } 2454 fml = tmp; 2455 } 2456 has_quantified_uninterpreted(ast_manager & m,expr * fml)2457 bool has_quantified_uninterpreted(ast_manager& m, expr* fml) { 2458 struct found {}; 2459 struct proc { 2460 ast_manager& m; 2461 proc(ast_manager& m):m(m) {} 2462 void operator()(quantifier* q) { 2463 if (has_uninterpreted(m, q->get_expr())) 2464 throw found(); 2465 } 2466 void operator()(expr*) {} 2467 }; 2468 2469 try { 2470 proc p(m); 2471 for_each_expr(p, fml); 2472 return false; 2473 } 2474 catch (found) { 2475 return true; 2476 } 2477 } 2478 2479 class simplify_solver_context : public i_solver_context { 2480 ast_manager& m; 2481 smt_params m_fparams; 2482 app_ref_vector* m_vars; 2483 expr_ref* m_fml; 2484 ptr_vector<contains_app> m_contains; 2485 atom_set m_pos; 2486 atom_set m_neg; 2487 public: simplify_solver_context(ast_manager & m)2488 simplify_solver_context(ast_manager& m): 2489 m(m), 2490 m_vars(nullptr), 2491 m_fml(nullptr) 2492 { 2493 add_plugin(mk_bool_plugin(*this)); 2494 add_plugin(mk_arith_plugin(*this, false, m_fparams)); 2495 } 2496 updt_params(params_ref const & p)2497 void updt_params(params_ref const& p) { 2498 m_fparams.updt_params(p); 2499 } 2500 ~simplify_solver_context()2501 ~simplify_solver_context() override { reset(); } 2502 2503 solve(expr_ref & fml,app_ref_vector & vars)2504 void solve(expr_ref& fml, app_ref_vector& vars) { 2505 init(fml, vars); 2506 bool solved = true; 2507 do { 2508 conj_enum conjs(m, fml); 2509 solved = false; 2510 for (unsigned i = 0; !solved && i < m_plugins.size(); ++i) { 2511 qe_solver_plugin* p = m_plugins[i]; 2512 solved = p && p->solve(conjs, fml); 2513 } 2514 TRACE("qe", 2515 tout << (solved?"solved":"not solved") << "\n"; 2516 if (solved) tout << mk_ismt2_pp(fml, m) << "\n"; 2517 tout << *m_vars << "\n"; 2518 tout << "contains: " << m_contains.size() << "\n"; 2519 ); 2520 } 2521 while (solved); 2522 } 2523 get_manager()2524 ast_manager& get_manager() override { return m; } 2525 pos_atoms() const2526 atom_set const& pos_atoms() const override { return m_pos; } neg_atoms() const2527 atom_set const& neg_atoms() const override { return m_neg; } 2528 2529 // Access current set of variables to solve get_num_vars() const2530 unsigned get_num_vars() const override { return m_vars->size(); } get_var(unsigned idx) const2531 app* get_var(unsigned idx) const override { return (*m_vars)[idx].get(); } get_vars() const2532 app_ref_vector const& get_vars() const override { return *m_vars; } is_var(expr * e,unsigned & idx) const2533 bool is_var(expr* e, unsigned& idx) const override { 2534 for (unsigned i = 0; i < m_vars->size(); ++i) { 2535 if ((*m_vars)[i].get() == e) { 2536 idx = i; 2537 return true; 2538 } 2539 } 2540 return false; 2541 } 2542 contains(unsigned idx)2543 contains_app& contains(unsigned idx) override { 2544 return *m_contains[idx]; 2545 } 2546 2547 // callback to replace variable at index 'idx' with definition 'def' and updated formula 'fml' elim_var(unsigned idx,expr * fml,expr * def)2548 void elim_var(unsigned idx, expr* fml, expr* def) override { 2549 TRACE("qe", tout << idx << ": " << mk_pp(m_vars->get(idx), m) << " " << mk_pp(fml, m) << " " << m_contains.size() << "\n";); 2550 *m_fml = fml; 2551 m_vars->set(idx, m_vars->get(m_vars->size()-1)); 2552 m_vars->pop_back(); 2553 dealloc(m_contains[idx]); 2554 m_contains[idx] = m_contains[m_contains.size()-1]; 2555 m_contains.pop_back(); 2556 } 2557 2558 // callback to add new variable to branch. add_var(app * x)2559 void add_var(app* x) override { 2560 TRACE("qe", tout << "add var: " << mk_pp(x, m) << "\n";); 2561 m_vars->push_back(x); 2562 m_contains.push_back(alloc(contains_app, m, x)); 2563 } 2564 2565 // callback to add constraints in branch. add_constraint(bool use_var,expr * l1=nullptr,expr * l2=nullptr,expr * l3=nullptr)2566 void add_constraint(bool use_var, expr* l1 = nullptr, expr* l2 = nullptr, expr* l3 = nullptr) override { 2567 UNREACHABLE(); 2568 } 2569 // eliminate finite domain variable 'var' from fml. blast_or(app * var,expr_ref & fml)2570 void blast_or(app* var, expr_ref& fml) override { 2571 UNREACHABLE(); 2572 } 2573 2574 private: reset()2575 void reset() { 2576 for (auto* c : m_contains) 2577 dealloc (c); 2578 m_contains.reset(); 2579 } 2580 init(expr_ref & fml,app_ref_vector & vars)2581 void init(expr_ref& fml, app_ref_vector& vars) { 2582 reset(); 2583 m_fml = &fml; 2584 m_vars = &vars; 2585 TRACE("qe", tout << "Vars: " << vars << "\n";); 2586 for (auto* v : vars) { 2587 m_contains.push_back(alloc(contains_app, m, v)); 2588 } 2589 } 2590 }; 2591 2592 class simplify_rewriter_cfg::impl { 2593 ast_manager& m; 2594 simplify_solver_context m_ctx; 2595 public: impl(ast_manager & m)2596 impl(ast_manager& m) : m(m), m_ctx(m) {} 2597 updt_params(params_ref const & p)2598 void updt_params(params_ref const& p) { 2599 m_ctx.updt_params(p); 2600 } 2601 collect_statistics(statistics & st) const2602 void collect_statistics(statistics & st) const { 2603 m_ctx.collect_statistics(st); 2604 } 2605 reduce_quantifier(quantifier * old_q,expr * new_body,expr * const * new_patterns,expr * const * new_no_patterns,expr_ref & result,proof_ref & result_pr)2606 bool reduce_quantifier( 2607 quantifier * old_q, 2608 expr * new_body, 2609 expr * const * new_patterns, 2610 expr * const * new_no_patterns, 2611 expr_ref & result, 2612 proof_ref & result_pr 2613 ) 2614 { 2615 2616 if (is_lambda(old_q)) { 2617 return false; 2618 } 2619 // bool is_forall = old_q->is_forall(); 2620 app_ref_vector vars(m); 2621 TRACE("qe", tout << "simplifying" << mk_pp(new_body, m) << "\n";); 2622 result = new_body; 2623 extract_vars(old_q, result, vars); 2624 TRACE("qe", tout << "variables extracted" << mk_pp(result, m) << "\n";); 2625 2626 if (is_forall(old_q)) { 2627 result = mk_not(m, result); 2628 } 2629 m_ctx.solve(result, vars); 2630 if (is_forall(old_q)) { 2631 expr* e = nullptr; 2632 result = m.is_not(result, e)?e:mk_not(m, result); 2633 } 2634 var_shifter shift(m); 2635 shift(result, vars.size(), result); 2636 result = expr_abstract(vars, result); 2637 TRACE("qe", tout << "abstracted" << mk_pp(result, m) << "\n";); 2638 ptr_vector<sort> sorts; 2639 svector<symbol> names; 2640 for (app* v : vars) { 2641 sorts.push_back(v->get_decl()->get_range()); 2642 names.push_back(v->get_decl()->get_name()); 2643 } 2644 if (!vars.empty()) { 2645 result = m.mk_quantifier(old_q->get_kind(), vars.size(), sorts.data(), names.data(), result, 1); 2646 } 2647 result_pr = nullptr; 2648 return true; 2649 } 2650 2651 }; 2652 simplify_rewriter_cfg(ast_manager & m)2653 simplify_rewriter_cfg::simplify_rewriter_cfg(ast_manager& m) { 2654 imp = alloc(simplify_rewriter_cfg::impl, m); 2655 } 2656 ~simplify_rewriter_cfg()2657 simplify_rewriter_cfg::~simplify_rewriter_cfg() { 2658 dealloc(imp); 2659 } 2660 reduce_quantifier(quantifier * old_q,expr * new_body,expr * const * new_patterns,expr * const * new_no_patterns,expr_ref & result,proof_ref & result_pr)2661 bool simplify_rewriter_cfg::reduce_quantifier( 2662 quantifier * old_q, 2663 expr * new_body, 2664 expr * const * new_patterns, 2665 expr * const * new_no_patterns, 2666 expr_ref & result, 2667 proof_ref & result_pr 2668 ) { 2669 return imp->reduce_quantifier(old_q, new_body, new_patterns, new_no_patterns, result, result_pr); 2670 } 2671 updt_params(params_ref const & p)2672 void simplify_rewriter_cfg::updt_params(params_ref const& p) { 2673 imp->updt_params(p); 2674 } 2675 collect_statistics(statistics & st) const2676 void simplify_rewriter_cfg::collect_statistics(statistics & st) const { 2677 imp->collect_statistics(st); 2678 } 2679 pre_visit(expr * e)2680 bool simplify_rewriter_cfg::pre_visit(expr* e) { 2681 if (!is_quantifier(e)) return true; 2682 quantifier * q = to_quantifier(e); 2683 return (q->get_num_patterns() == 0 && q->get_num_no_patterns() == 0); 2684 } 2685 simplify_exists(app_ref_vector & vars,expr_ref & fml)2686 void simplify_exists(app_ref_vector& vars, expr_ref& fml) { 2687 ast_manager& m = fml.get_manager(); 2688 simplify_solver_context ctx(m); 2689 ctx.solve(fml, vars); 2690 } 2691 } 2692 2693 2694 template class rewriter_tpl<qe::simplify_rewriter_cfg>; 2695 2696 2697