1 /*++ 2 Copyright (c) 2012 Microsoft Corporation 3 4 Module Name: 5 6 nlsat_solver.cpp 7 8 Abstract: 9 10 Nonlinear arithmetic satisfiability procedure. The procedure is 11 complete for nonlinear real arithmetic, but it also has limited 12 support for integers. 13 14 Author: 15 16 Leonardo de Moura (leonardo) 2012-01-02. 17 18 Revision History: 19 20 --*/ 21 #include "util/z3_exception.h" 22 #include "util/chashtable.h" 23 #include "util/id_gen.h" 24 #include "util/map.h" 25 #include "util/dependency.h" 26 #include "util/permutation.h" 27 #include "math/polynomial/algebraic_numbers.h" 28 #include "math/polynomial/polynomial_cache.h" 29 #include "nlsat/nlsat_solver.h" 30 #include "nlsat/nlsat_clause.h" 31 #include "nlsat/nlsat_assignment.h" 32 #include "nlsat/nlsat_justification.h" 33 #include "nlsat/nlsat_evaluator.h" 34 #include "nlsat/nlsat_explain.h" 35 #include "nlsat/nlsat_params.hpp" 36 37 #define NLSAT_EXTRA_VERBOSE 38 39 #ifdef NLSAT_EXTRA_VERBOSE 40 #define NLSAT_VERBOSE(CODE) IF_VERBOSE(10, CODE) 41 #else 42 #define NLSAT_VERBOSE(CODE) ((void)0) 43 #endif 44 45 namespace nlsat { 46 47 typedef chashtable<ineq_atom*, ineq_atom::hash_proc, ineq_atom::eq_proc> ineq_atom_table; 48 typedef chashtable<root_atom*, root_atom::hash_proc, root_atom::eq_proc> root_atom_table; 49 50 // for apply_permutation procedure swap(clause * & c1,clause * & c2)51 void swap(clause * & c1, clause * & c2) { 52 std::swap(c1, c2); 53 } 54 55 struct solver::ctx { 56 params_ref m_params; 57 reslimit& m_rlimit; 58 small_object_allocator m_allocator; 59 unsynch_mpq_manager m_qm; 60 pmanager m_pm; 61 anum_manager m_am; 62 bool m_incremental; ctxnlsat::solver::ctx63 ctx(reslimit& rlim, params_ref const & p, bool incremental): 64 m_params(p), 65 m_rlimit(rlim), 66 m_allocator("nlsat"), 67 m_pm(rlim, m_qm, &m_allocator), 68 m_am(rlim, m_qm, p, &m_allocator), 69 m_incremental(incremental) 70 {} 71 }; 72 73 struct solver::imp { 74 struct dconfig { 75 typedef imp value_manager; 76 typedef small_object_allocator allocator; 77 typedef void * value; 78 static const bool ref_count = false; 79 }; 80 typedef dependency_manager<dconfig> assumption_manager; 81 typedef assumption_manager::dependency * _assumption_set; 82 typedef obj_ref<assumption_manager::dependency, assumption_manager> assumption_set_ref; 83 84 85 typedef polynomial::cache cache; 86 typedef ptr_vector<interval_set> interval_set_vector; 87 88 ctx& m_ctx; 89 solver& m_solver; 90 reslimit& m_rlimit; 91 small_object_allocator& m_allocator; 92 bool m_incremental; 93 unsynch_mpq_manager& m_qm; 94 pmanager& m_pm; 95 cache m_cache; 96 anum_manager& m_am; 97 mutable assumption_manager m_asm; 98 assignment m_assignment; // partial interpretation 99 evaluator m_evaluator; 100 interval_set_manager & m_ism; 101 ineq_atom_table m_ineq_atoms; 102 root_atom_table m_root_atoms; 103 svector<bool_var> m_patch_var; 104 polynomial_ref_vector m_patch_num, m_patch_denom; 105 106 id_gen m_cid_gen; 107 clause_vector m_clauses; // set of clauses 108 clause_vector m_learned; // set of learned clauses 109 clause_vector m_valids; 110 111 unsigned m_num_bool_vars; 112 atom_vector m_atoms; // bool_var -> atom 113 svector<lbool> m_bvalues; // boolean assignment 114 unsigned_vector m_levels; // bool_var -> level 115 svector<justification> m_justifications; 116 vector<clause_vector> m_bwatches; // bool_var (that are not attached to atoms) -> clauses where it is maximal 117 bool_vector m_dead; // mark dead boolean variables 118 id_gen m_bid_gen; 119 120 bool_vector m_is_int; // m_is_int[x] is true if variable is integer 121 vector<clause_vector> m_watches; // var -> clauses where variable is maximal 122 interval_set_vector m_infeasible; // var -> to a set of interval where the variable cannot be assigned to. 123 atom_vector m_var2eq; // var -> to asserted equality 124 var_vector m_perm; // var -> var permutation of the variables 125 var_vector m_inv_perm; 126 // m_perm: internal -> external 127 // m_inv_perm: external -> internal 128 struct perm_display_var_proc : public display_var_proc { 129 var_vector & m_perm; 130 display_var_proc m_default_display_var; 131 display_var_proc const * m_proc; // display external var ids perm_display_var_procnlsat::solver::imp::perm_display_var_proc132 perm_display_var_proc(var_vector & perm): 133 m_perm(perm), 134 m_proc(nullptr) { 135 } operator ()nlsat::solver::imp::perm_display_var_proc136 std::ostream& operator()(std::ostream & out, var x) const override { 137 if (m_proc == nullptr) 138 m_default_display_var(out, x); 139 else 140 (*m_proc)(out, m_perm[x]); 141 return out; 142 } 143 }; 144 perm_display_var_proc m_display_var; 145 146 display_assumption_proc const* m_display_assumption; 147 struct display_literal_assumption : public display_assumption_proc { 148 imp& i; 149 literal_vector const& lits; display_literal_assumptionnlsat::solver::imp::display_literal_assumption150 display_literal_assumption(imp& i, literal_vector const& lits): i(i), lits(lits) {} operator ()nlsat::solver::imp::display_literal_assumption151 std::ostream& operator()(std::ostream& out, assumption a) const override { 152 if (lits.begin() <= a && a < lits.end()) { 153 out << *((literal const*)a); 154 } 155 else if (i.m_display_assumption) { 156 (*i.m_display_assumption)(out, a); 157 } 158 return out; 159 } 160 161 }; 162 struct scoped_display_assumptions { 163 imp& i; 164 display_assumption_proc const* m_save; scoped_display_assumptionsnlsat::solver::imp::scoped_display_assumptions165 scoped_display_assumptions(imp& i, display_assumption_proc const& p): i(i), m_save(i.m_display_assumption) { 166 i.m_display_assumption = &p; 167 } ~scoped_display_assumptionsnlsat::solver::imp::scoped_display_assumptions168 ~scoped_display_assumptions() { 169 i.m_display_assumption = m_save; 170 } 171 }; 172 173 explain m_explain; 174 175 bool_var m_bk; // current Boolean variable we are processing 176 var m_xk; // current arith variable we are processing 177 178 unsigned m_scope_lvl; 179 180 struct bvar_assignment {}; 181 struct stage {}; 182 struct trail { 183 enum kind { BVAR_ASSIGNMENT, INFEASIBLE_UPDT, NEW_LEVEL, NEW_STAGE, UPDT_EQ }; 184 kind m_kind; 185 union { 186 bool_var m_b; 187 interval_set * m_old_set; 188 atom * m_old_eq; 189 }; trailnlsat::solver::imp::trail190 trail(bool_var b, bvar_assignment):m_kind(BVAR_ASSIGNMENT), m_b(b) {} trailnlsat::solver::imp::trail191 trail(interval_set * old_set):m_kind(INFEASIBLE_UPDT), m_old_set(old_set) {} trailnlsat::solver::imp::trail192 trail(bool s, stage):m_kind(s ? NEW_STAGE : NEW_LEVEL) {} trailnlsat::solver::imp::trail193 trail(atom * a):m_kind(UPDT_EQ), m_old_eq(a) {} 194 }; 195 svector<trail> m_trail; 196 197 anum m_zero; 198 199 // configuration 200 unsigned long long m_max_memory; 201 unsigned m_lazy; // how lazy the solver is: 0 - satisfy all learned clauses, 1 - process only unit and empty learned clauses, 2 - use only conflict clauses for resolving conflicts 202 bool m_simplify_cores; 203 bool m_reorder; 204 bool m_randomize; 205 bool m_random_order; 206 unsigned m_random_seed; 207 bool m_inline_vars; 208 bool m_log_lemmas; 209 bool m_check_lemmas; 210 unsigned m_max_conflicts; 211 unsigned m_lemma_count; 212 213 // statistics 214 unsigned m_conflicts; 215 unsigned m_propagations; 216 unsigned m_decisions; 217 unsigned m_stages; 218 unsigned m_irrational_assignments; // number of irrational witnesses 219 impnlsat::solver::imp220 imp(solver& s, ctx& c): 221 m_ctx(c), 222 m_solver(s), 223 m_rlimit(c.m_rlimit), 224 m_allocator(c.m_allocator), 225 m_incremental(c.m_incremental), 226 m_qm(c.m_qm), 227 m_pm(c.m_pm), 228 m_cache(m_pm), 229 m_am(c.m_am), 230 m_asm(*this, m_allocator), 231 m_assignment(m_am), 232 m_evaluator(s, m_assignment, m_pm, m_allocator), 233 m_ism(m_evaluator.ism()), 234 m_patch_num(m_pm), 235 m_patch_denom(m_pm), 236 m_num_bool_vars(0), 237 m_display_var(m_perm), 238 m_display_assumption(nullptr), 239 m_explain(s, m_assignment, m_cache, m_atoms, m_var2eq, m_evaluator), 240 m_scope_lvl(0), 241 m_lemma(s), 242 m_lazy_clause(s), 243 m_lemma_assumptions(m_asm) { 244 updt_params(c.m_params); 245 reset_statistics(); 246 mk_true_bvar(); 247 m_lemma_count = 0; 248 } 249 ~impnlsat::solver::imp250 ~imp() { 251 clear(); 252 } 253 mk_true_bvarnlsat::solver::imp254 void mk_true_bvar() { 255 bool_var b = mk_bool_var(); 256 SASSERT(b == true_bool_var); 257 literal true_lit(b, false); 258 mk_clause(1, &true_lit, false, nullptr); 259 } 260 updt_paramsnlsat::solver::imp261 void updt_params(params_ref const & _p) { 262 nlsat_params p(_p); 263 m_max_memory = p.max_memory(); 264 m_lazy = p.lazy(); 265 m_simplify_cores = p.simplify_conflicts(); 266 bool min_cores = p.minimize_conflicts(); 267 m_reorder = p.reorder(); 268 m_randomize = p.randomize(); 269 m_max_conflicts = p.max_conflicts(); 270 m_random_order = p.shuffle_vars(); 271 m_random_seed = p.seed(); 272 m_inline_vars = p.inline_vars(); 273 m_log_lemmas = p.log_lemmas(); 274 m_check_lemmas = p.check_lemmas(); 275 m_ism.set_seed(m_random_seed); 276 m_explain.set_simplify_cores(m_simplify_cores); 277 m_explain.set_minimize_cores(min_cores); 278 m_explain.set_factor(p.factor()); 279 m_am.updt_params(p.p); 280 } 281 resetnlsat::solver::imp282 void reset() { 283 m_explain.reset(); 284 m_lemma.reset(); 285 m_lazy_clause.reset(); 286 undo_until_size(0); 287 del_clauses(); 288 del_unref_atoms(); 289 m_cache.reset(); 290 m_assignment.reset(); 291 } 292 clearnlsat::solver::imp293 void clear() { 294 m_explain.reset(); 295 m_lemma.reset(); 296 m_lazy_clause.reset(); 297 undo_until_size(0); 298 del_clauses(); 299 del_unref_atoms(); 300 } 301 checkpointnlsat::solver::imp302 void checkpoint() { 303 if (!m_rlimit.inc()) throw solver_exception(m_rlimit.get_cancel_msg()); 304 if (memory::get_allocation_size() > m_max_memory) throw solver_exception(Z3_MAX_MEMORY_MSG); 305 } 306 307 // ----------------------- 308 // 309 // Basic 310 // 311 // ----------------------- 312 num_bool_varsnlsat::solver::imp313 unsigned num_bool_vars() const { 314 return m_num_bool_vars; 315 } 316 num_varsnlsat::solver::imp317 unsigned num_vars() const { 318 return m_is_int.size(); 319 } 320 is_intnlsat::solver::imp321 bool is_int(var x) const { 322 return m_is_int[x]; 323 } 324 inc_refnlsat::solver::imp325 void inc_ref(assumption) {} 326 dec_refnlsat::solver::imp327 void dec_ref(assumption) {} 328 inc_refnlsat::solver::imp329 void inc_ref(_assumption_set a) { 330 if (a != nullptr) m_asm.inc_ref(a); 331 } 332 dec_refnlsat::solver::imp333 void dec_ref(_assumption_set a) { 334 if (a != nullptr) m_asm.dec_ref(a); 335 } 336 inc_refnlsat::solver::imp337 void inc_ref(bool_var b) { 338 if (b == null_bool_var) 339 return; 340 atom * a = m_atoms[b]; 341 if (a == nullptr) 342 return; 343 TRACE("ref", display(tout << "inc: " << b << " " << a->ref_count() << " ", *a) << "\n";); 344 a->inc_ref(); 345 } 346 inc_refnlsat::solver::imp347 void inc_ref(literal l) { 348 inc_ref(l.var()); 349 } 350 dec_refnlsat::solver::imp351 void dec_ref(bool_var b) { 352 if (b == null_bool_var) 353 return; 354 atom * a = m_atoms[b]; 355 if (a == nullptr) 356 return; 357 SASSERT(a->ref_count() > 0); 358 a->dec_ref(); 359 TRACE("ref", display(tout << "dec: " << b << " " << a->ref_count() << " ", *a) << "\n";); 360 if (a->ref_count() == 0) 361 del(a); 362 } 363 dec_refnlsat::solver::imp364 void dec_ref(literal l) { 365 dec_ref(l.var()); 366 } 367 is_arith_atomnlsat::solver::imp368 bool is_arith_atom(bool_var b) const { return m_atoms[b] != nullptr; } 369 is_arith_literalnlsat::solver::imp370 bool is_arith_literal(literal l) const { return is_arith_atom(l.var()); } 371 max_varnlsat::solver::imp372 var max_var(poly const * p) const { 373 return m_pm.max_var(p); 374 } 375 max_varnlsat::solver::imp376 var max_var(bool_var b) const { 377 if (!is_arith_atom(b)) 378 return null_var; 379 else 380 return m_atoms[b]->max_var(); 381 } 382 max_varnlsat::solver::imp383 var max_var(literal l) const { 384 return max_var(l.var()); 385 } 386 387 /** 388 \brief Return the maximum variable occurring in cls. 389 */ max_varnlsat::solver::imp390 var max_var(unsigned sz, literal const * cls) const { 391 var x = null_var; 392 for (unsigned i = 0; i < sz; i++) { 393 literal l = cls[i]; 394 if (is_arith_literal(l)) { 395 var y = max_var(l); 396 if (x == null_var || y > x) 397 x = y; 398 } 399 } 400 return x; 401 } 402 max_varnlsat::solver::imp403 var max_var(clause const & cls) const { 404 return max_var(cls.size(), cls.c_ptr()); 405 } 406 407 /** 408 \brief Return the maximum Boolean variable occurring in cls. 409 */ max_bvarnlsat::solver::imp410 bool_var max_bvar(clause const & cls) const { 411 bool_var b = null_bool_var; 412 for (literal l : cls) { 413 if (b == null_bool_var || l.var() > b) 414 b = l.var(); 415 } 416 return b; 417 } 418 419 /** 420 \brief Return the degree of the maximal variable of the given atom 421 */ degreenlsat::solver::imp422 unsigned degree(atom const * a) const { 423 if (a->is_ineq_atom()) { 424 unsigned max = 0; 425 unsigned sz = to_ineq_atom(a)->size(); 426 var x = a->max_var(); 427 for (unsigned i = 0; i < sz; i++) { 428 unsigned d = m_pm.degree(to_ineq_atom(a)->p(i), x); 429 if (d > max) 430 max = d; 431 } 432 return max; 433 } 434 else { 435 return m_pm.degree(to_root_atom(a)->p(), a->max_var()); 436 } 437 } 438 439 /** 440 \brief Return the degree of the maximal variable in c 441 */ degreenlsat::solver::imp442 unsigned degree(clause const & c) const { 443 var x = max_var(c); 444 if (x == null_var) 445 return 0; 446 unsigned max = 0; 447 for (literal l : c) { 448 atom const * a = m_atoms[l.var()]; 449 if (a == nullptr) 450 continue; 451 unsigned d = degree(a); 452 if (d > max) 453 max = d; 454 } 455 return max; 456 } 457 458 // ----------------------- 459 // 460 // Variable, Atoms, Clauses & Assumption creation 461 // 462 // ----------------------- 463 mk_bool_var_corenlsat::solver::imp464 bool_var mk_bool_var_core() { 465 bool_var b = m_bid_gen.mk(); 466 m_num_bool_vars++; 467 m_atoms .setx(b, nullptr, nullptr); 468 m_bvalues .setx(b, l_undef, l_undef); 469 m_levels .setx(b, UINT_MAX, UINT_MAX); 470 m_justifications.setx(b, null_justification, null_justification); 471 m_bwatches .setx(b, clause_vector(), clause_vector()); 472 m_dead .setx(b, false, true); 473 return b; 474 } 475 mk_bool_varnlsat::solver::imp476 bool_var mk_bool_var() { 477 return mk_bool_var_core(); 478 } 479 mk_varnlsat::solver::imp480 var mk_var(bool is_int) { 481 var x = m_pm.mk_var(); 482 register_var(x, is_int); 483 return x; 484 } register_varnlsat::solver::imp485 void register_var(var x, bool is_int) { 486 SASSERT(x == num_vars()); 487 m_is_int. push_back(is_int); 488 m_watches. push_back(clause_vector()); 489 m_infeasible.push_back(0); 490 m_var2eq. push_back(nullptr); 491 m_perm. push_back(x); 492 m_inv_perm. push_back(x); 493 SASSERT(m_is_int.size() == m_watches.size()); 494 SASSERT(m_is_int.size() == m_infeasible.size()); 495 SASSERT(m_is_int.size() == m_var2eq.size()); 496 SASSERT(m_is_int.size() == m_perm.size()); 497 SASSERT(m_is_int.size() == m_inv_perm.size()); 498 } 499 500 bool_vector m_found_vars; varsnlsat::solver::imp501 void vars(literal l, var_vector& vs) { 502 vs.reset(); 503 atom * a = m_atoms[l.var()]; 504 if (a == nullptr) { 505 506 } 507 else if (a->is_ineq_atom()) { 508 unsigned sz = to_ineq_atom(a)->size(); 509 var_vector new_vs; 510 for (unsigned j = 0; j < sz; j++) { 511 m_found_vars.reset(); 512 m_pm.vars(to_ineq_atom(a)->p(j), new_vs); 513 for (unsigned i = 0; i < new_vs.size(); ++i) { 514 if (!m_found_vars.get(new_vs[i], false)) { 515 m_found_vars.setx(new_vs[i], true, false); 516 vs.push_back(new_vs[i]); 517 } 518 } 519 } 520 } 521 else { 522 m_pm.vars(to_root_atom(a)->p(), vs); 523 //vs.erase(max_var(to_root_atom(a)->p())); 524 vs.push_back(to_root_atom(a)->x()); 525 } 526 } 527 deallocatenlsat::solver::imp528 void deallocate(ineq_atom * a) { 529 unsigned obj_sz = ineq_atom::get_obj_size(a->size()); 530 a->~ineq_atom(); 531 m_allocator.deallocate(obj_sz, a); 532 } 533 deallocatenlsat::solver::imp534 void deallocate(root_atom * a) { 535 a->~root_atom(); 536 m_allocator.deallocate(sizeof(root_atom), a); 537 } 538 delnlsat::solver::imp539 void del(bool_var b) { 540 SASSERT(m_bwatches[b].empty()); 541 //SASSERT(m_bvalues[b] == l_undef); 542 m_num_bool_vars--; 543 m_dead[b] = true; 544 m_atoms[b] = nullptr; 545 m_bvalues[b] = l_undef; 546 m_bid_gen.recycle(b); 547 } 548 delnlsat::solver::imp549 void del(ineq_atom * a) { 550 CTRACE("nlsat_solver", a->ref_count() > 0, display(tout, *a) << "\n";); 551 // this triggers in too many benign cases: 552 // SASSERT(a->ref_count() == 0); 553 m_ineq_atoms.erase(a); 554 del(a->bvar()); 555 unsigned sz = a->size(); 556 for (unsigned i = 0; i < sz; i++) 557 m_pm.dec_ref(a->p(i)); 558 deallocate(a); 559 } 560 delnlsat::solver::imp561 void del(root_atom * a) { 562 SASSERT(a->ref_count() == 0); 563 m_root_atoms.erase(a); 564 del(a->bvar()); 565 m_pm.dec_ref(a->p()); 566 deallocate(a); 567 } 568 delnlsat::solver::imp569 void del(atom * a) { 570 if (a == nullptr) 571 return; 572 TRACE("nlsat_verbose", display(tout << "del: b" << a->m_bool_var << " " << a->ref_count() << " ", *a) << "\n";); 573 if (a->is_ineq_atom()) 574 del(to_ineq_atom(a)); 575 else 576 del(to_root_atom(a)); 577 } 578 579 // Delete atoms with ref_count == 0 del_unref_atomsnlsat::solver::imp580 void del_unref_atoms() { 581 for (auto* a : m_atoms) { 582 del(a); 583 } 584 } 585 586 mk_ineq_atomnlsat::solver::imp587 ineq_atom* mk_ineq_atom(atom::kind k, unsigned sz, poly * const * ps, bool const * is_even, bool& is_new) { 588 SASSERT(sz >= 1); 589 SASSERT(k == atom::LT || k == atom::GT || k == atom::EQ); 590 int sign = 1; 591 polynomial_ref p(m_pm); 592 ptr_buffer<poly> uniq_ps; 593 var max = null_var; 594 for (unsigned i = 0; i < sz; i++) { 595 p = m_pm.flip_sign_if_lm_neg(ps[i]); 596 if (p.get() != ps[i] && !is_even[i]) { 597 sign = -sign; 598 } 599 var curr_max = max_var(p.get()); 600 if (curr_max > max || max == null_var) 601 max = curr_max; 602 uniq_ps.push_back(m_cache.mk_unique(p)); 603 TRACE("nlsat_table_bug", tout << "p: " << p << ", uniq: " << uniq_ps.back() << "\n";); 604 } 605 void * mem = m_allocator.allocate(ineq_atom::get_obj_size(sz)); 606 if (sign < 0) 607 k = atom::flip(k); 608 ineq_atom * tmp_atom = new (mem) ineq_atom(k, sz, uniq_ps.c_ptr(), is_even, max); 609 ineq_atom * atom = m_ineq_atoms.insert_if_not_there(tmp_atom); 610 CTRACE("nlsat_table_bug", tmp_atom != atom, ineq_atom::hash_proc h; 611 tout << "mk_ineq_atom hash: " << h(tmp_atom) << "\n"; display(tout, *tmp_atom, m_display_var) << "\n";); 612 CTRACE("nlsat_table_bug", atom->max_var() != max, display(tout << "nonmax: ", *atom, m_display_var) << "\n";); 613 SASSERT(atom->max_var() == max); 614 is_new = (atom == tmp_atom); 615 if (is_new) { 616 for (unsigned i = 0; i < sz; i++) { 617 m_pm.inc_ref(atom->p(i)); 618 } 619 } 620 else { 621 deallocate(tmp_atom); 622 } 623 return atom; 624 } 625 mk_ineq_atomnlsat::solver::imp626 bool_var mk_ineq_atom(atom::kind k, unsigned sz, poly * const * ps, bool const * is_even) { 627 bool is_new = false; 628 ineq_atom* atom = mk_ineq_atom(k, sz, ps, is_even, is_new); 629 if (!is_new) { 630 return atom->bvar(); 631 } 632 else { 633 bool_var b = mk_bool_var_core(); 634 m_atoms[b] = atom; 635 atom->m_bool_var = b; 636 TRACE("nlsat_verbose", display(tout << "create: b" << atom->m_bool_var << " ", *atom) << "\n";); 637 return b; 638 } 639 } 640 mk_ineq_literalnlsat::solver::imp641 literal mk_ineq_literal(atom::kind k, unsigned sz, poly * const * ps, bool const * is_even) { 642 SASSERT(k == atom::LT || k == atom::GT || k == atom::EQ); 643 bool is_const = true; 644 polynomial::manager::scoped_numeral cnst(m_pm.m()); 645 m_pm.m().set(cnst, 1); 646 for (unsigned i = 0; i < sz; ++i) { 647 if (m_pm.is_const(ps[i])) { 648 if (m_pm.is_zero(ps[i])) { 649 m_pm.m().set(cnst, 0); 650 is_const = true; 651 break; 652 } 653 auto const& c = m_pm.coeff(ps[i], 0); 654 m_pm.m().mul(cnst, c, cnst); 655 if (is_even[i] && m_pm.m().is_neg(c)) { 656 m_pm.m().neg(cnst); 657 } 658 } 659 else { 660 is_const = false; 661 } 662 } 663 if (is_const) { 664 if (m_pm.m().is_pos(cnst) && k == atom::GT) return true_literal; 665 if (m_pm.m().is_neg(cnst) && k == atom::LT) return true_literal; 666 if (m_pm.m().is_zero(cnst) && k == atom::EQ) return true_literal; 667 return false_literal; 668 } 669 return literal(mk_ineq_atom(k, sz, ps, is_even), false); 670 } 671 mk_root_atomnlsat::solver::imp672 bool_var mk_root_atom(atom::kind k, var x, unsigned i, poly * p) { 673 polynomial_ref p1(m_pm), uniq_p(m_pm); 674 p1 = m_pm.flip_sign_if_lm_neg(p); // flipping the sign of the polynomial will not change its roots. 675 uniq_p = m_cache.mk_unique(p1); 676 TRACE("nlsat_solver", tout << x << " " << p1 << " " << uniq_p << "\n";); 677 SASSERT(i > 0); 678 SASSERT(x >= max_var(p)); 679 SASSERT(k == atom::ROOT_LT || k == atom::ROOT_GT || k == atom::ROOT_EQ || k == atom::ROOT_LE || k == atom::ROOT_GE); 680 681 void * mem = m_allocator.allocate(sizeof(root_atom)); 682 root_atom * new_atom = new (mem) root_atom(k, x, i, uniq_p); 683 root_atom * old_atom = m_root_atoms.insert_if_not_there(new_atom); 684 SASSERT(old_atom->max_var() == x); 685 if (old_atom != new_atom) { 686 deallocate(new_atom); 687 return old_atom->bvar(); 688 } 689 bool_var b = mk_bool_var_core(); 690 m_atoms[b] = new_atom; 691 new_atom->m_bool_var = b; 692 m_pm.inc_ref(new_atom->p()); 693 return b; 694 } 695 attach_clausenlsat::solver::imp696 void attach_clause(clause & cls) { 697 var x = max_var(cls); 698 if (x != null_var) { 699 m_watches[x].push_back(&cls); 700 } 701 else { 702 bool_var b = max_bvar(cls); 703 m_bwatches[b].push_back(&cls); 704 } 705 } 706 deattach_clausenlsat::solver::imp707 void deattach_clause(clause & cls) { 708 var x = max_var(cls); 709 if (x != null_var) { 710 m_watches[x].erase(&cls); 711 } 712 else { 713 bool_var b = max_bvar(cls); 714 m_bwatches[b].erase(&cls); 715 } 716 } 717 deallocatenlsat::solver::imp718 void deallocate(clause * cls) { 719 size_t obj_sz = clause::get_obj_size(cls->size()); 720 cls->~clause(); 721 m_allocator.deallocate(obj_sz, cls); 722 } 723 del_clausenlsat::solver::imp724 void del_clause(clause * cls) { 725 deattach_clause(*cls); 726 m_cid_gen.recycle(cls->id()); 727 unsigned sz = cls->size(); 728 for (unsigned i = 0; i < sz; i++) 729 dec_ref((*cls)[i]); 730 _assumption_set a = static_cast<_assumption_set>(cls->assumptions()); 731 dec_ref(a); 732 deallocate(cls); 733 } 734 del_clausenlsat::solver::imp735 void del_clause(clause * cls, clause_vector& clauses) { 736 clauses.erase(cls); 737 del_clause(cls); 738 } 739 del_clausesnlsat::solver::imp740 void del_clauses(ptr_vector<clause> & cs) { 741 for (clause* cp : cs) 742 del_clause(cp); 743 cs.reset(); 744 } 745 del_clausesnlsat::solver::imp746 void del_clauses() { 747 del_clauses(m_clauses); 748 del_clauses(m_learned); 749 del_clauses(m_valids); 750 } 751 752 // We use a simple heuristic to sort literals 753 // - bool literals < arith literals 754 // - sort literals based on max_var 755 // - sort literal with the same max_var using degree 756 // break ties using the fact that ineqs are usually cheaper to process than eqs. 757 struct lit_lt { 758 imp & m; lit_ltnlsat::solver::imp::lit_lt759 lit_lt(imp & _m):m(_m) {} 760 operator ()nlsat::solver::imp::lit_lt761 bool operator()(literal l1, literal l2) const { 762 atom * a1 = m.m_atoms[l1.var()]; 763 atom * a2 = m.m_atoms[l2.var()]; 764 if (a1 == nullptr && a2 == nullptr) 765 return l1.index() < l2.index(); 766 if (a1 == nullptr) 767 return true; 768 if (a2 == nullptr) 769 return false; 770 var x1 = a1->max_var(); 771 var x2 = a2->max_var(); 772 if (x1 < x2) 773 return true; 774 if (x1 > x2) 775 return false; 776 SASSERT(x1 == x2); 777 unsigned d1 = m.degree(a1); 778 unsigned d2 = m.degree(a2); 779 if (d1 < d2) 780 return true; 781 if (d1 > d2) 782 return false; 783 if (!a1->is_eq() && a2->is_eq()) 784 return true; 785 if (a1->is_eq() && !a2->is_eq()) 786 return false; 787 return l1.index() < l2.index(); 788 } 789 }; 790 791 class scoped_bool_vars { 792 imp& s; 793 svector<bool_var> vec; 794 public: scoped_bool_vars(imp & s)795 scoped_bool_vars(imp& s):s(s) {} ~scoped_bool_vars()796 ~scoped_bool_vars() { 797 for (bool_var v : vec) { 798 s.dec_ref(v); 799 } 800 } push_back(bool_var v)801 void push_back(bool_var v) { 802 s.inc_ref(v); 803 vec.push_back(v); 804 } begin() const805 bool_var const* begin() const { return vec.begin(); } end() const806 bool_var const* end() const { return vec.end(); } operator [](bool_var v) const807 bool_var operator[](bool_var v) const { return vec[v]; } 808 }; 809 check_lemmanlsat::solver::imp810 void check_lemma(unsigned n, literal const* cls, bool is_valid, assumption_set a) { 811 TRACE("nlsat", display(tout << "check lemma: ", n, cls) << "\n"; 812 display(tout);); 813 IF_VERBOSE(0, display(verbose_stream() << "check lemma: ", n, cls) << "\n"); 814 for (clause* c : m_learned) IF_VERBOSE(1, display(verbose_stream() << "lemma: ", *c) << "\n"); 815 816 solver solver2(m_ctx); 817 imp& checker = *(solver2.m_imp); 818 checker.m_check_lemmas = false; 819 checker.m_log_lemmas = false; 820 checker.m_inline_vars = false; 821 822 // need to translate Boolean variables and literals 823 scoped_bool_vars tr(checker); 824 for (var x = 0; x < m_is_int.size(); ++x) { 825 checker.register_var(x, m_is_int[x]); 826 } 827 bool_var bv = 0; 828 tr.push_back(bv); 829 for (bool_var b = 1; b < m_atoms.size(); ++b) { 830 atom* a = m_atoms[b]; 831 if (a == nullptr) { 832 bv = checker.mk_bool_var(); 833 } 834 else if (a->is_ineq_atom()) { 835 ineq_atom& ia = *to_ineq_atom(a); 836 unsigned sz = ia.size(); 837 ptr_vector<poly> ps; 838 bool_vector is_even; 839 for (unsigned i = 0; i < sz; ++i) { 840 ps.push_back(ia.p(i)); 841 is_even.push_back(ia.is_even(i)); 842 } 843 bv = checker.mk_ineq_atom(ia.get_kind(), sz, ps.c_ptr(), is_even.c_ptr()); 844 } 845 else if (a->is_root_atom()) { 846 root_atom& r = *to_root_atom(a); 847 if (r.x() >= max_var(r.p())) { 848 // permutation may be reverted after check completes, 849 // but then root atoms are not used in lemmas. 850 bv = checker.mk_root_atom(r.get_kind(), r.x(), r.i(), r.p()); 851 } 852 } 853 else { 854 UNREACHABLE(); 855 } 856 tr.push_back(bv); 857 } 858 if (!is_valid) { 859 for (clause* c : m_clauses) { 860 if (!a && c->assumptions()) { 861 continue; 862 } 863 literal_vector lits; 864 for (literal lit : *c) { 865 lits.push_back(literal(tr[lit.var()], lit.sign())); 866 } 867 checker.mk_clause(lits.size(), lits.c_ptr(), nullptr); 868 } 869 } 870 for (unsigned i = 0; i < n; ++i) { 871 literal lit = cls[i]; 872 literal nlit(tr[lit.var()], !lit.sign()); 873 checker.mk_clause(1, &nlit, nullptr); 874 } 875 IF_VERBOSE(0, verbose_stream() << "check\n";); 876 lbool r = checker.check(); 877 if (r == l_true) { 878 for (bool_var b : tr) { 879 literal lit(b, false); 880 IF_VERBOSE(0, checker.display(verbose_stream(), lit) << " := " << checker.value(lit) << "\n"); 881 TRACE("nlsat", checker.display(tout, lit) << " := " << checker.value(lit) << "\n";); 882 } 883 for (clause* c : m_learned) { 884 bool found = false; 885 for (literal lit: *c) { 886 literal tlit(tr[lit.var()], lit.sign()); 887 found |= checker.value(tlit) == l_true; 888 } 889 if (!found) { 890 IF_VERBOSE(0, display(verbose_stream() << "violdated clause: ", *c) << "\n"); 891 TRACE("nlsat", display(tout << "violdated clause: ", *c) << "\n";); 892 } 893 } 894 for (clause* c : m_valids) { 895 bool found = false; 896 for (literal lit: *c) { 897 literal tlit(tr[lit.var()], lit.sign()); 898 found |= checker.value(tlit) == l_true; 899 } 900 if (!found) { 901 IF_VERBOSE(0, display(verbose_stream() << "violdated tautology clause: ", *c) << "\n"); 902 TRACE("nlsat", display(tout << "violdated tautology clause: ", *c) << "\n";); 903 } 904 } 905 UNREACHABLE(); 906 } 907 } 908 log_lemmanlsat::solver::imp909 void log_lemma(std::ostream& out, clause const& cls) { 910 display_smt2(out); 911 out << "(assert (not "; 912 display_smt2(out, cls) << "))\n"; 913 display(out << "(echo \"#" << m_lemma_count << " ", cls) << "\")\n"; 914 out << "(check-sat)\n(reset)\n"; 915 } 916 mk_clause_corenlsat::solver::imp917 clause * mk_clause_core(unsigned num_lits, literal const * lits, bool learned, _assumption_set a) { 918 SASSERT(num_lits > 0); 919 unsigned cid = m_cid_gen.mk(); 920 void * mem = m_allocator.allocate(clause::get_obj_size(num_lits)); 921 clause * cls = new (mem) clause(cid, num_lits, lits, learned, a); 922 for (unsigned i = 0; i < num_lits; i++) 923 inc_ref(lits[i]); 924 inc_ref(a); 925 return cls; 926 } 927 mk_clausenlsat::solver::imp928 clause * mk_clause(unsigned num_lits, literal const * lits, bool learned, _assumption_set a) { 929 SASSERT(num_lits > 0); 930 clause * cls = mk_clause_core(num_lits, lits, learned, a); 931 ++m_lemma_count; 932 TRACE("nlsat_sort", display(tout << "mk_clause:\n", *cls) << "\n";); 933 std::sort(cls->begin(), cls->end(), lit_lt(*this)); 934 TRACE("nlsat_sort", display(tout << "#" << m_lemma_count << " after sort:\n", *cls) << "\n";); 935 if (learned && m_log_lemmas) { 936 log_lemma(verbose_stream(), *cls); 937 } 938 if (learned && m_check_lemmas) { 939 check_lemma(cls->size(), cls->c_ptr(), false, cls->assumptions()); 940 } 941 if (learned) 942 m_learned.push_back(cls); 943 else 944 m_clauses.push_back(cls); 945 attach_clause(*cls); 946 return cls; 947 } 948 mk_clausenlsat::solver::imp949 void mk_clause(unsigned num_lits, literal const * lits, assumption a) { 950 _assumption_set as = nullptr; 951 if (a != nullptr) 952 as = m_asm.mk_leaf(a); 953 if (num_lits == 0) { 954 num_lits = 1; 955 lits = &false_literal; 956 } 957 mk_clause(num_lits, lits, false, as); 958 } 959 960 // ----------------------- 961 // 962 // Search 963 // 964 // ----------------------- 965 save_assign_trailnlsat::solver::imp966 void save_assign_trail(bool_var b) { 967 m_trail.push_back(trail(b, bvar_assignment())); 968 } 969 save_set_updt_trailnlsat::solver::imp970 void save_set_updt_trail(interval_set * old_set) { 971 m_trail.push_back(trail(old_set)); 972 } 973 save_updt_eq_trailnlsat::solver::imp974 void save_updt_eq_trail(atom * old_eq) { 975 m_trail.push_back(trail(old_eq)); 976 } 977 save_new_stage_trailnlsat::solver::imp978 void save_new_stage_trail() { 979 m_trail.push_back(trail(true, stage())); 980 } 981 save_new_level_trailnlsat::solver::imp982 void save_new_level_trail() { 983 m_trail.push_back(trail(false, stage())); 984 } 985 undo_bvar_assignmentnlsat::solver::imp986 void undo_bvar_assignment(bool_var b) { 987 m_bvalues[b] = l_undef; 988 m_levels[b] = UINT_MAX; 989 del_jst(m_allocator, m_justifications[b]); 990 m_justifications[b] = null_justification; 991 if (m_atoms[b] == nullptr && b < m_bk) 992 m_bk = b; 993 } 994 undo_set_updtnlsat::solver::imp995 void undo_set_updt(interval_set * old_set) { 996 if (m_xk == null_var) return; 997 var x = m_xk; 998 if (x < m_infeasible.size()) { 999 m_ism.dec_ref(m_infeasible[x]); 1000 m_infeasible[x] = old_set; 1001 } 1002 } 1003 undo_new_stagenlsat::solver::imp1004 void undo_new_stage() { 1005 if (m_xk == 0) { 1006 m_xk = null_var; 1007 } 1008 else if (m_xk != null_var) { 1009 m_xk--; 1010 m_assignment.reset(m_xk); 1011 } 1012 } 1013 undo_new_levelnlsat::solver::imp1014 void undo_new_level() { 1015 SASSERT(m_scope_lvl > 0); 1016 m_scope_lvl--; 1017 m_evaluator.pop(1); 1018 } 1019 undo_updt_eqnlsat::solver::imp1020 void undo_updt_eq(atom * a) { 1021 if (m_var2eq.size() > m_xk) 1022 m_var2eq[m_xk] = a; 1023 } 1024 1025 template<typename Predicate> undo_untilnlsat::solver::imp1026 void undo_until(Predicate const & pred) { 1027 while (pred() && !m_trail.empty()) { 1028 trail & t = m_trail.back(); 1029 switch (t.m_kind) { 1030 case trail::BVAR_ASSIGNMENT: 1031 undo_bvar_assignment(t.m_b); 1032 break; 1033 case trail::INFEASIBLE_UPDT: 1034 undo_set_updt(t.m_old_set); 1035 break; 1036 case trail::NEW_STAGE: 1037 undo_new_stage(); 1038 break; 1039 case trail::NEW_LEVEL: 1040 undo_new_level(); 1041 break; 1042 case trail::UPDT_EQ: 1043 undo_updt_eq(t.m_old_eq); 1044 break; 1045 default: 1046 break; 1047 } 1048 m_trail.pop_back(); 1049 } 1050 } 1051 1052 struct size_pred { 1053 svector<trail> & m_trail; 1054 unsigned m_old_size; size_prednlsat::solver::imp::size_pred1055 size_pred(svector<trail> & trail, unsigned old_size):m_trail(trail), m_old_size(old_size) {} operator ()nlsat::solver::imp::size_pred1056 bool operator()() const { return m_trail.size() > m_old_size; } 1057 }; 1058 1059 // Keep undoing until trail has the given size undo_until_sizenlsat::solver::imp1060 void undo_until_size(unsigned old_size) { 1061 SASSERT(m_trail.size() >= old_size); 1062 undo_until(size_pred(m_trail, old_size)); 1063 } 1064 1065 struct stage_pred { 1066 var const & m_xk; 1067 var m_target; stage_prednlsat::solver::imp::stage_pred1068 stage_pred(var const & xk, var target):m_xk(xk), m_target(target) {} operator ()nlsat::solver::imp::stage_pred1069 bool operator()() const { return m_xk != m_target; } 1070 }; 1071 1072 // Keep undoing until stage is new_xk undo_until_stagenlsat::solver::imp1073 void undo_until_stage(var new_xk) { 1074 undo_until(stage_pred(m_xk, new_xk)); 1075 } 1076 1077 struct level_pred { 1078 unsigned const & m_scope_lvl; 1079 unsigned m_new_lvl; level_prednlsat::solver::imp::level_pred1080 level_pred(unsigned const & scope_lvl, unsigned new_lvl):m_scope_lvl(scope_lvl), m_new_lvl(new_lvl) {} operator ()nlsat::solver::imp::level_pred1081 bool operator()() const { return m_scope_lvl > m_new_lvl; } 1082 }; 1083 1084 // Keep undoing until level is new_lvl undo_until_levelnlsat::solver::imp1085 void undo_until_level(unsigned new_lvl) { 1086 undo_until(level_pred(m_scope_lvl, new_lvl)); 1087 } 1088 1089 struct unassigned_pred { 1090 bool_var m_b; 1091 svector<lbool> const & m_bvalues; unassigned_prednlsat::solver::imp::unassigned_pred1092 unassigned_pred(svector<lbool> const & bvalues, bool_var b): 1093 m_b(b), 1094 m_bvalues(bvalues) {} operator ()nlsat::solver::imp::unassigned_pred1095 bool operator()() const { return m_bvalues[m_b] != l_undef; } 1096 }; 1097 1098 // Keep undoing until b is unassigned undo_until_unassignednlsat::solver::imp1099 void undo_until_unassigned(bool_var b) { 1100 undo_until(unassigned_pred(m_bvalues, b)); 1101 SASSERT(m_bvalues[b] == l_undef); 1102 } 1103 1104 struct true_pred { operator ()nlsat::solver::imp::true_pred1105 bool operator()() const { return true; } 1106 }; 1107 undo_until_emptynlsat::solver::imp1108 void undo_until_empty() { 1109 undo_until(true_pred()); 1110 } 1111 1112 /** 1113 \brief Create a new scope level 1114 */ new_levelnlsat::solver::imp1115 void new_level() { 1116 m_evaluator.push(); 1117 m_scope_lvl++; 1118 save_new_level_trail(); 1119 } 1120 1121 /** 1122 \brief Return the value of the given literal that was assigned by the search 1123 engine. 1124 */ assigned_valuenlsat::solver::imp1125 lbool assigned_value(literal l) const { 1126 bool_var b = l.var(); 1127 if (l.sign()) 1128 return ~m_bvalues[b]; 1129 else 1130 return m_bvalues[b]; 1131 } 1132 1133 /** 1134 \brief Assign literal using the given justification 1135 */ assignnlsat::solver::imp1136 void assign(literal l, justification j) { 1137 TRACE("nlsat", 1138 display(tout << "assigning literal: ", l); 1139 display(tout << " <- ", j);); 1140 1141 SASSERT(assigned_value(l) == l_undef); 1142 SASSERT(j != null_justification); 1143 SASSERT(!j.is_null()); 1144 if (j.is_decision()) 1145 m_decisions++; 1146 else 1147 m_propagations++; 1148 bool_var b = l.var(); 1149 m_bvalues[b] = to_lbool(!l.sign()); 1150 m_levels[b] = m_scope_lvl; 1151 m_justifications[b] = j; 1152 save_assign_trail(b); 1153 updt_eq(b, j); 1154 TRACE("nlsat_assign", tout << "b" << b << " -> " << m_bvalues[b] << "\n";); 1155 } 1156 1157 /** 1158 \brief Create a "case-split" 1159 */ decidenlsat::solver::imp1160 void decide(literal l) { 1161 new_level(); 1162 assign(l, decided_justification); 1163 } 1164 1165 /** 1166 \brief Return the value of a literal as defined in Dejan and Leo's paper. 1167 */ valuenlsat::solver::imp1168 lbool value(literal l) { 1169 lbool val = assigned_value(l); 1170 if (val != l_undef) { 1171 TRACE("nlsat_verbose", display(tout << " assigned value " << val << " for ", l) << "\n";); 1172 return val; 1173 } 1174 bool_var b = l.var(); 1175 atom * a = m_atoms[b]; 1176 if (a == nullptr) { 1177 TRACE("nlsat_verbose", display(tout << " no atom for ", l) << "\n";); 1178 return l_undef; 1179 } 1180 var max = a->max_var(); 1181 if (!m_assignment.is_assigned(max)) { 1182 TRACE("nlsat_verbose", display(tout << " maximal variable not assigned ", l) << "\n";); 1183 return l_undef; 1184 } 1185 val = to_lbool(m_evaluator.eval(a, l.sign())); 1186 TRACE("nlsat_verbose", display(tout << " evaluated value " << val << " for ", l) << "\n";); 1187 TRACE("value_bug", tout << "value of: "; display(tout, l); tout << " := " << val << "\n"; 1188 tout << "xk: " << m_xk << ", a->max_var(): " << a->max_var() << "\n"; 1189 display_assignment(tout);); 1190 return val; 1191 } 1192 1193 /** 1194 \brief Return true if the given clause is already satisfied in the current partial interpretation. 1195 */ is_satisfiednlsat::solver::imp1196 bool is_satisfied(clause const & cls) const { 1197 for (literal l : cls) { 1198 if (const_cast<imp*>(this)->value(l) == l_true) { 1199 TRACE("value_bug:", tout << l << " := true\n";); 1200 return true; 1201 } 1202 } 1203 return false; 1204 } 1205 1206 /** 1207 \brief Return true if the given clause is false in the current partial interpretation. 1208 */ is_inconsistentnlsat::solver::imp1209 bool is_inconsistent(unsigned sz, literal const * cls) { 1210 for (unsigned i = 0; i < sz; i++) { 1211 if (value(cls[i]) != l_false) { 1212 TRACE("is_inconsistent", tout << "literal is not false:\n"; display(tout, cls[i]); tout << "\n";); 1213 return false; 1214 } 1215 } 1216 return true; 1217 } 1218 1219 /** 1220 \brief Process a clauses that contains only Boolean literals. 1221 */ process_boolean_clausenlsat::solver::imp1222 bool process_boolean_clause(clause const & cls) { 1223 SASSERT(m_xk == null_var); 1224 unsigned num_undef = 0; 1225 unsigned first_undef = UINT_MAX; 1226 unsigned sz = cls.size(); 1227 for (unsigned i = 0; i < sz; i++) { 1228 literal l = cls[i]; 1229 SASSERT(m_atoms[l.var()] == nullptr); 1230 SASSERT(value(l) != l_true); 1231 if (value(l) == l_false) 1232 continue; 1233 SASSERT(value(l) == l_undef); 1234 num_undef++; 1235 if (first_undef == UINT_MAX) 1236 first_undef = i; 1237 } 1238 if (num_undef == 0) 1239 return false; 1240 SASSERT(first_undef != UINT_MAX); 1241 if (num_undef == 1) 1242 assign(cls[first_undef], mk_clause_jst(&cls)); // unit clause 1243 else 1244 decide(cls[first_undef]); 1245 return true; 1246 } 1247 1248 /** 1249 \brief assign l to true, because l + (justification of) s is infeasible in RCF in the current interpretation. 1250 */ 1251 literal_vector core; 1252 ptr_vector<clause> clauses; R_propagatenlsat::solver::imp1253 void R_propagate(literal l, interval_set const * s, bool include_l = true) { 1254 m_ism.get_justifications(s, core, clauses); 1255 if (include_l) 1256 core.push_back(~l); 1257 assign(l, mk_lazy_jst(m_allocator, core.size(), core.c_ptr(), clauses.size(), clauses.c_ptr())); 1258 SASSERT(value(l) == l_true); 1259 } 1260 1261 /** 1262 \brief m_infeasible[m_xk] <- m_infeasible[m_xk] Union s 1263 */ updt_infeasiblenlsat::solver::imp1264 void updt_infeasible(interval_set const * s) { 1265 SASSERT(m_xk != null_var); 1266 interval_set * xk_set = m_infeasible[m_xk]; 1267 save_set_updt_trail(xk_set); 1268 interval_set_ref new_set(m_ism); 1269 TRACE("nlsat_inf_set", tout << "updating infeasible set\n"; m_ism.display(tout, xk_set) << "\n"; m_ism.display(tout, s) << "\n";); 1270 new_set = m_ism.mk_union(s, xk_set); 1271 TRACE("nlsat_inf_set", tout << "new infeasible set:\n"; m_ism.display(tout, new_set) << "\n";); 1272 SASSERT(!m_ism.is_full(new_set)); 1273 m_ism.inc_ref(new_set); 1274 m_infeasible[m_xk] = new_set; 1275 } 1276 1277 /** 1278 \brief Update m_var2eq mapping. 1279 */ updt_eqnlsat::solver::imp1280 void updt_eq(bool_var b, justification j) { 1281 if (!m_simplify_cores) 1282 return; 1283 if (m_bvalues[b] != l_true) 1284 return; 1285 atom * a = m_atoms[b]; 1286 if (a == nullptr || a->get_kind() != atom::EQ || to_ineq_atom(a)->size() > 1 || to_ineq_atom(a)->is_even(0)) 1287 return; 1288 switch (j.get_kind()) { 1289 case justification::CLAUSE: 1290 if (j.get_clause()->assumptions() != nullptr) return; 1291 break; 1292 case justification::LAZY: 1293 if (j.get_lazy()->num_clauses() > 0) return; 1294 if (j.get_lazy()->num_lits() > 0) return; 1295 break; 1296 default: 1297 break; 1298 } 1299 var x = m_xk; 1300 SASSERT(a->max_var() == x); 1301 SASSERT(x != null_var); 1302 if (m_var2eq[x] != 0 && degree(m_var2eq[x]) <= degree(a)) 1303 return; // we only update m_var2eq if the new equality has smaller degree 1304 TRACE("nlsat_simplify_core", tout << "Saving equality for "; m_display_var(tout, x) << " (x" << x << ") "; 1305 tout << "scope-lvl: " << scope_lvl() << "\n"; display(tout, literal(b, false)) << "\n"; 1306 display(tout, j); 1307 ); 1308 save_updt_eq_trail(m_var2eq[x]); 1309 m_var2eq[x] = a; 1310 } 1311 1312 /** 1313 \brief Process a clause that contains nonlinear arithmetic literals 1314 1315 If satisfy_learned is true, then learned clauses are satisfied even if m_lazy > 0 1316 */ process_arith_clausenlsat::solver::imp1317 bool process_arith_clause(clause const & cls, bool satisfy_learned) { 1318 if (!satisfy_learned && m_lazy >= 2 && cls.is_learned()) { 1319 TRACE("nlsat", tout << "skip learned\n";); 1320 return true; // ignore lemmas in super lazy mode 1321 } 1322 SASSERT(m_xk == max_var(cls)); 1323 unsigned num_undef = 0; // number of undefined literals 1324 unsigned first_undef = UINT_MAX; // position of the first undefined literal 1325 interval_set_ref first_undef_set(m_ism); // infeasible region of the first undefined literal 1326 interval_set * xk_set = m_infeasible[m_xk]; // current set of infeasible interval for current variable 1327 SASSERT(!m_ism.is_full(xk_set)); 1328 for (unsigned idx = 0; idx < cls.size(); ++idx) { 1329 literal l = cls[idx]; 1330 checkpoint(); 1331 if (value(l) == l_false) 1332 continue; 1333 if (value(l) == l_true) 1334 return true; // could happen if clause is a tautology 1335 CTRACE("nlsat", max_var(l) != m_xk || value(l) != l_undef, display(tout); 1336 tout << "xk: " << m_xk << ", max_var(l): " << max_var(l) << ", l: "; display(tout, l) << "\n"; 1337 display(tout, cls) << "\n";); 1338 SASSERT(value(l) == l_undef); 1339 SASSERT(max_var(l) == m_xk); 1340 bool_var b = l.var(); 1341 atom * a = m_atoms[b]; 1342 SASSERT(a != nullptr); 1343 interval_set_ref curr_set(m_ism); 1344 curr_set = m_evaluator.infeasible_intervals(a, l.sign(), &cls); 1345 TRACE("nlsat_inf_set", tout << "infeasible set for literal: "; display(tout, l); tout << "\n"; m_ism.display(tout, curr_set); tout << "\n"; 1346 display(tout, cls) << "\n";); 1347 if (m_ism.is_empty(curr_set)) { 1348 TRACE("nlsat_inf_set", tout << "infeasible set is empty, found literal\n";); 1349 R_propagate(l, nullptr); 1350 SASSERT(is_satisfied(cls)); 1351 return true; 1352 } 1353 if (m_ism.is_full(curr_set)) { 1354 TRACE("nlsat_inf_set", tout << "infeasible set is R, skip literal\n";); 1355 R_propagate(~l, nullptr); 1356 continue; 1357 } 1358 if (m_ism.subset(curr_set, xk_set)) { 1359 TRACE("nlsat_inf_set", tout << "infeasible set is a subset of current set, found literal\n";); 1360 R_propagate(l, xk_set); 1361 return true; 1362 } 1363 interval_set_ref tmp(m_ism); 1364 tmp = m_ism.mk_union(curr_set, xk_set); 1365 if (m_ism.is_full(tmp)) { 1366 TRACE("nlsat_inf_set", tout << "infeasible set + current set = R, skip literal\n"; 1367 display(tout, cls) << "\n";); 1368 R_propagate(~l, tmp, false); 1369 continue; 1370 } 1371 num_undef++; 1372 if (first_undef == UINT_MAX) { 1373 first_undef = idx; 1374 first_undef_set = curr_set; 1375 } 1376 } 1377 TRACE("nlsat_inf_set", tout << "num_undef: " << num_undef << "\n";); 1378 if (num_undef == 0) 1379 return false; 1380 SASSERT(first_undef != UINT_MAX); 1381 if (num_undef == 1) { 1382 // unit clause 1383 assign(cls[first_undef], mk_clause_jst(&cls)); 1384 updt_infeasible(first_undef_set); 1385 } 1386 else if ( satisfy_learned || 1387 !cls.is_learned() /* must always satisfy input clauses */ || 1388 m_lazy == 0 /* if not in lazy mode, we also satiffy lemmas */) { 1389 decide(cls[first_undef]); 1390 updt_infeasible(first_undef_set); 1391 } 1392 else { 1393 TRACE("nlsat_lazy", tout << "skipping clause, satisfy_learned: " << satisfy_learned << ", cls.is_learned(): " << cls.is_learned() 1394 << ", lazy: " << m_lazy << "\n";); 1395 } 1396 return true; 1397 } 1398 1399 /** 1400 \brief Try to satisfy the given clause. Return true if succeeded. 1401 1402 If satisfy_learned is true, then (arithmetic) learned clauses are satisfied even if m_lazy > 0 1403 */ process_clausenlsat::solver::imp1404 bool process_clause(clause const & cls, bool satisfy_learned) { 1405 if (is_satisfied(cls)) 1406 return true; 1407 if (m_xk == null_var) 1408 return process_boolean_clause(cls); 1409 else 1410 return process_arith_clause(cls, satisfy_learned); 1411 } 1412 1413 /** 1414 \brief Try to satisfy the given "set" of clauses. 1415 Return 0, if the set was satisfied, or the violating clause otherwise 1416 */ process_clausesnlsat::solver::imp1417 clause * process_clauses(clause_vector const & cs) { 1418 for (clause* c : cs) { 1419 if (!process_clause(*c, false)) 1420 return c; 1421 } 1422 return nullptr; // succeeded 1423 } 1424 1425 /** 1426 \brief Make sure m_bk is the first unassigned pure Boolean variable. 1427 Set m_bk == null_bool_var if there is no unassigned pure Boolean variable. 1428 */ peek_next_bool_varnlsat::solver::imp1429 void peek_next_bool_var() { 1430 while (m_bk < m_atoms.size()) { 1431 if (!m_dead[m_bk] && m_atoms[m_bk] == nullptr && m_bvalues[m_bk] == l_undef) { 1432 return; 1433 } 1434 m_bk++; 1435 } 1436 m_bk = null_bool_var; 1437 } 1438 1439 /** 1440 \brief Create a new stage. See Dejan and Leo's paper. 1441 */ new_stagenlsat::solver::imp1442 void new_stage() { 1443 m_stages++; 1444 save_new_stage_trail(); 1445 if (m_xk == null_var) 1446 m_xk = 0; 1447 else 1448 m_xk++; 1449 } 1450 1451 /** 1452 \brief Assign m_xk 1453 */ select_witnessnlsat::solver::imp1454 void select_witness() { 1455 scoped_anum w(m_am); 1456 SASSERT(!m_ism.is_full(m_infeasible[m_xk])); 1457 m_ism.peek_in_complement(m_infeasible[m_xk], m_is_int[m_xk], w, m_randomize); 1458 TRACE("nlsat", 1459 tout << "infeasible intervals: "; m_ism.display(tout, m_infeasible[m_xk]); tout << "\n"; 1460 tout << "assigning "; m_display_var(tout, m_xk) << "(x" << m_xk << ") -> " << w << "\n";); 1461 TRACE("nlsat_root", tout << "value as root object: "; m_am.display_root(tout, w); tout << "\n";); 1462 if (!m_am.is_rational(w)) 1463 m_irrational_assignments++; 1464 m_assignment.set_core(m_xk, w); 1465 } 1466 1467 1468 is_satisfiednlsat::solver::imp1469 bool is_satisfied() { 1470 if (m_bk == null_bool_var && m_xk >= num_vars()) { 1471 TRACE("nlsat", tout << "found model\n"; display_assignment(tout);); 1472 fix_patch(); 1473 SASSERT(check_satisfied(m_clauses)); 1474 return true; // all variables were assigned, and all clauses were satisfied. 1475 } 1476 else { 1477 return false; 1478 } 1479 } 1480 1481 1482 /** 1483 \brief main procedure 1484 */ searchnlsat::solver::imp1485 lbool search() { 1486 TRACE("nlsat", tout << "starting search...\n"; display(tout); tout << "\nvar order:\n"; display_vars(tout);); 1487 TRACE("nlsat_proof", tout << "ASSERTED\n"; display(tout);); 1488 TRACE("nlsat_proof_sk", tout << "ASSERTED\n"; display_abst(tout);); 1489 TRACE("nlsat_mathematica", display_mathematica(tout);); 1490 TRACE("nlsat", display_smt2(tout);); 1491 m_bk = 0; 1492 m_xk = null_var; 1493 m_conflicts = 0; 1494 1495 while (true) { 1496 CASSERT("nlsat", check_satisfied()); 1497 if (m_xk == null_var) { 1498 peek_next_bool_var(); 1499 if (m_bk == null_bool_var) 1500 new_stage(); // move to arith vars 1501 } 1502 else { 1503 new_stage(); // peek next arith var 1504 } 1505 TRACE("nlsat_bug", tout << "xk: x" << m_xk << " bk: b" << m_bk << "\n";); 1506 if (is_satisfied()) { 1507 return l_true; 1508 } 1509 while (true) { 1510 TRACE("nlsat_verbose", tout << "processing variable "; 1511 if (m_xk != null_var) { 1512 m_display_var(tout, m_xk); tout << " " << m_watches[m_xk].size(); 1513 } 1514 else { 1515 tout << m_bwatches[m_bk].size() << " boolean b" << m_bk; 1516 } 1517 tout << "\n";); 1518 checkpoint(); 1519 clause * conflict_clause; 1520 if (m_xk == null_var) 1521 conflict_clause = process_clauses(m_bwatches[m_bk]); 1522 else 1523 conflict_clause = process_clauses(m_watches[m_xk]); 1524 if (conflict_clause == nullptr) 1525 break; 1526 if (!resolve(*conflict_clause)) 1527 return l_false; 1528 if (m_conflicts >= m_max_conflicts) 1529 return l_undef; 1530 } 1531 1532 if (m_xk == null_var) { 1533 if (m_bvalues[m_bk] == l_undef) { 1534 decide(literal(m_bk, true)); 1535 m_bk++; 1536 } 1537 } 1538 else { 1539 select_witness(); 1540 } 1541 } 1542 } 1543 1544 search_checknlsat::solver::imp1545 lbool search_check() { 1546 lbool r = l_undef; 1547 while (true) { 1548 r = search(); 1549 if (r != l_true) break; 1550 vector<std::pair<var, rational>> bounds; 1551 1552 for (var x = 0; x < num_vars(); x++) { 1553 if (m_is_int[x] && m_assignment.is_assigned(x) && !m_am.is_int(m_assignment.value(x))) { 1554 scoped_anum v(m_am), vlo(m_am); 1555 v = m_assignment.value(x); 1556 rational lo; 1557 m_am.int_lt(v, vlo); 1558 if (!m_am.is_int(vlo)) 1559 continue; 1560 m_am.to_rational(vlo, lo); 1561 // derive tight bounds. 1562 while (true) { 1563 lo++; 1564 if (!m_am.gt(v, lo.to_mpq())) { lo--; break; } 1565 } 1566 bounds.push_back(std::make_pair(x, lo)); 1567 } 1568 } 1569 if (bounds.empty()) break; 1570 1571 init_search(); 1572 for (auto const& b : bounds) { 1573 var x = b.first; 1574 rational lo = b.second; 1575 rational hi = lo + 1; // rational::one(); 1576 bool is_even = false; 1577 polynomial_ref p(m_pm); 1578 rational one(1); 1579 m_lemma.reset(); 1580 p = m_pm.mk_linear(1, &one, &x, -lo); 1581 poly* p1 = p.get(); 1582 m_lemma.push_back(~mk_ineq_literal(atom::GT, 1, &p1, &is_even)); 1583 p = m_pm.mk_linear(1, &one, &x, -hi); 1584 poly* p2 = p.get(); 1585 m_lemma.push_back(~mk_ineq_literal(atom::LT, 1, &p2, &is_even)); 1586 1587 // perform branch and bound 1588 clause * cls = mk_clause(m_lemma.size(), m_lemma.c_ptr(), false, nullptr); 1589 if (cls) { 1590 TRACE("nlsat", display(tout << "conflict " << lo << " " << hi, *cls); tout << "\n";); 1591 } 1592 } 1593 } 1594 return r; 1595 } 1596 checknlsat::solver::imp1597 lbool check() { 1598 TRACE("nlsat_smt2", display_smt2(tout);); 1599 TRACE("nlsat_fd", tout << "is_full_dimensional: " << is_full_dimensional() << "\n";); 1600 init_search(); 1601 m_explain.set_full_dimensional(is_full_dimensional()); 1602 bool reordered = false; 1603 1604 if (!m_incremental && m_inline_vars) { 1605 if (!simplify()) 1606 return l_false; 1607 } 1608 1609 if (!can_reorder()) { 1610 1611 } 1612 else if (m_random_order) { 1613 shuffle_vars(); 1614 reordered = true; 1615 } 1616 else if (m_reorder) { 1617 heuristic_reorder(); 1618 reordered = true; 1619 } 1620 sort_watched_clauses(); 1621 lbool r = search_check(); 1622 CTRACE("nlsat_model", r == l_true, tout << "model before restore order\n"; display_assignment(tout);); 1623 if (reordered) { 1624 restore_order(); 1625 } 1626 CTRACE("nlsat_model", r == l_true, tout << "model\n"; display_assignment(tout);); 1627 CTRACE("nlsat", r == l_false, display(tout);); 1628 SASSERT(r != l_true || check_satisfied(m_clauses)); 1629 return r; 1630 } 1631 init_searchnlsat::solver::imp1632 void init_search() { 1633 undo_until_empty(); 1634 while (m_scope_lvl > 0) { 1635 undo_new_level(); 1636 } 1637 m_xk = null_var; 1638 for (unsigned i = 0; i < m_bvalues.size(); ++i) { 1639 m_bvalues[i] = l_undef; 1640 } 1641 m_assignment.reset(); 1642 } 1643 checknlsat::solver::imp1644 lbool check(literal_vector& assumptions) { 1645 literal_vector result; 1646 unsigned sz = assumptions.size(); 1647 literal const* ptr = assumptions.c_ptr(); 1648 for (unsigned i = 0; i < sz; ++i) { 1649 mk_clause(1, ptr+i, (assumption)(ptr+i)); 1650 } 1651 display_literal_assumption dla(*this, assumptions); 1652 scoped_display_assumptions _scoped_display(*this, dla); 1653 lbool r = check(); 1654 1655 if (r == l_false) { 1656 // collect used literals from m_lemma_assumptions 1657 vector<assumption, false> deps; 1658 get_core(deps); 1659 for (unsigned i = 0; i < deps.size(); ++i) { 1660 literal const* lp = (literal const*)(deps[i]); 1661 if (ptr <= lp && lp < ptr + sz) { 1662 result.push_back(*lp); 1663 } 1664 } 1665 } 1666 collect(assumptions, m_clauses); 1667 collect(assumptions, m_learned); 1668 del_clauses(m_valids); 1669 if (m_check_lemmas) { 1670 for (clause* c : m_learned) { 1671 check_lemma(c->size(), c->c_ptr(), false, nullptr); 1672 } 1673 } 1674 1675 #if 0 1676 for (clause* c : m_learned) { 1677 IF_VERBOSE(0, display(verbose_stream() << "KEEP: ", c->size(), c->c_ptr()) << "\n"); 1678 } 1679 #endif 1680 assumptions.reset(); 1681 assumptions.append(result); 1682 return r; 1683 } 1684 get_corenlsat::solver::imp1685 void get_core(vector<assumption, false>& deps) { 1686 m_asm.linearize(m_lemma_assumptions.get(), deps); 1687 } 1688 collectnlsat::solver::imp1689 void collect(literal_vector const& assumptions, clause_vector& clauses) { 1690 unsigned j = 0; 1691 for (clause * c : clauses) { 1692 if (collect(assumptions, *c)) { 1693 del_clause(c); 1694 } 1695 else { 1696 clauses[j++] = c; 1697 } 1698 } 1699 clauses.shrink(j); 1700 } 1701 collectnlsat::solver::imp1702 bool collect(literal_vector const& assumptions, clause const& c) { 1703 unsigned sz = assumptions.size(); 1704 literal const* ptr = assumptions.c_ptr(); 1705 _assumption_set asms = static_cast<_assumption_set>(c.assumptions()); 1706 if (asms == nullptr) { 1707 return false; 1708 } 1709 vector<assumption, false> deps; 1710 m_asm.linearize(asms, deps); 1711 for (auto dep : deps) { 1712 if (ptr <= dep && dep < ptr + sz) { 1713 return true; 1714 } 1715 } 1716 return false; 1717 } 1718 1719 // ----------------------- 1720 // 1721 // Conflict Resolution 1722 // 1723 // ----------------------- 1724 svector<char> m_marks; // bool_var -> bool temp mark used during conflict resolution 1725 unsigned m_num_marks; 1726 scoped_literal_vector m_lemma; 1727 scoped_literal_vector m_lazy_clause; 1728 assumption_set_ref m_lemma_assumptions; // assumption tracking 1729 1730 // Conflict resolution invariant: a marked literal is in m_lemma or on the trail stack. 1731 check_marksnlsat::solver::imp1732 bool check_marks() { 1733 for (unsigned m : m_marks) { 1734 (void)m; 1735 SASSERT(m == 0); 1736 } 1737 return true; 1738 } 1739 scope_lvlnlsat::solver::imp1740 unsigned scope_lvl() const { return m_scope_lvl; } 1741 is_markednlsat::solver::imp1742 bool is_marked(bool_var b) const { return m_marks.get(b, 0) == 1; } 1743 marknlsat::solver::imp1744 void mark(bool_var b) { m_marks.setx(b, 1, 0); } 1745 reset_marknlsat::solver::imp1746 void reset_mark(bool_var b) { m_marks[b] = 0; } 1747 reset_marksnlsat::solver::imp1748 void reset_marks() { 1749 for (auto const& l : m_lemma) { 1750 reset_mark(l.var()); 1751 } 1752 } 1753 process_antecedentnlsat::solver::imp1754 void process_antecedent(literal antecedent) { 1755 checkpoint(); 1756 bool_var b = antecedent.var(); 1757 TRACE("nlsat_resolve", display(tout << "resolving antecedent: ", antecedent) << "\n";); 1758 if (assigned_value(antecedent) == l_undef) { 1759 checkpoint(); 1760 // antecedent must be false in the current arith interpretation 1761 SASSERT(value(antecedent) == l_false || m_rlimit.is_canceled()); 1762 if (!is_marked(b)) { 1763 SASSERT(is_arith_atom(b) && max_var(b) < m_xk); // must be in a previous stage 1764 TRACE("nlsat_resolve", tout << "literal is unassigned, but it is false in arithmetic interpretation, adding it to lemma\n";); 1765 mark(b); 1766 m_lemma.push_back(antecedent); 1767 } 1768 return; 1769 } 1770 1771 unsigned b_lvl = m_levels[b]; 1772 TRACE("nlsat_resolve", tout << "b_lvl: " << b_lvl << ", is_marked(b): " << is_marked(b) << ", m_num_marks: " << m_num_marks << "\n";); 1773 if (!is_marked(b)) { 1774 mark(b); 1775 if (b_lvl == scope_lvl() /* same level */ && max_var(b) == m_xk /* same stage */) { 1776 TRACE("nlsat_resolve", tout << "literal is in the same level and stage, increasing marks\n";); 1777 m_num_marks++; 1778 } 1779 else { 1780 TRACE("nlsat_resolve", tout << "previous level or stage, adding literal to lemma\n"; 1781 tout << "max_var(b): " << max_var(b) << ", m_xk: " << m_xk << ", lvl: " << b_lvl << ", scope_lvl: " << scope_lvl() << "\n";); 1782 m_lemma.push_back(antecedent); 1783 } 1784 } 1785 } 1786 resolve_clausenlsat::solver::imp1787 void resolve_clause(bool_var b, unsigned sz, literal const * c) { 1788 TRACE("nlsat_proof", tout << "resolving "; if (b != null_bool_var) display_atom(tout, b) << "\n"; display(tout, sz, c); tout << "\n";); 1789 TRACE("nlsat_proof_sk", tout << "resolving "; if (b != null_bool_var) tout << "b" << b; tout << "\n"; display_abst(tout, sz, c); tout << "\n";); 1790 1791 for (unsigned i = 0; i < sz; i++) { 1792 if (c[i].var() != b) 1793 process_antecedent(c[i]); 1794 } 1795 } 1796 resolve_clausenlsat::solver::imp1797 void resolve_clause(bool_var b, clause const & c) { 1798 TRACE("nlsat_resolve", tout << "resolving clause for b: " << b << "\n";); 1799 resolve_clause(b, c.size(), c.c_ptr()); 1800 m_lemma_assumptions = m_asm.mk_join(static_cast<_assumption_set>(c.assumptions()), m_lemma_assumptions); 1801 } 1802 resolve_lazy_justificationnlsat::solver::imp1803 void resolve_lazy_justification(bool_var b, lazy_justification const & jst) { 1804 TRACE("nlsat_resolve", tout << "resolving lazy_justification for b" << b << "\n";); 1805 unsigned sz = jst.num_lits(); 1806 1807 // Dump lemma as Mathematica formula that must be true, 1808 // if the current interpretation (really) makes the core in jst infeasible. 1809 TRACE("nlsat_mathematica", 1810 tout << "assignment lemma\n"; 1811 literal_vector core; 1812 for (unsigned i = 0; i < sz; i++) { 1813 core.push_back(~jst.lit(i)); 1814 } 1815 display_mathematica_lemma(tout, core.size(), core.c_ptr(), true);); 1816 1817 m_lazy_clause.reset(); 1818 m_explain(jst.num_lits(), jst.lits(), m_lazy_clause); 1819 for (unsigned i = 0; i < sz; i++) 1820 m_lazy_clause.push_back(~jst.lit(i)); 1821 1822 // lazy clause is a valid clause 1823 TRACE("nlsat_mathematica", display_mathematica_lemma(tout, m_lazy_clause.size(), m_lazy_clause.c_ptr());); 1824 TRACE("nlsat_proof_sk", tout << "theory lemma\n"; display_abst(tout, m_lazy_clause.size(), m_lazy_clause.c_ptr()); tout << "\n";); 1825 TRACE("nlsat_resolve", 1826 tout << "m_xk: " << m_xk << ", "; m_display_var(tout, m_xk) << "\n"; 1827 tout << "new valid clause:\n"; 1828 display(tout, m_lazy_clause.size(), m_lazy_clause.c_ptr()) << "\n";); 1829 1830 if (m_check_lemmas) { 1831 m_valids.push_back(mk_clause_core(m_lazy_clause.size(), m_lazy_clause.c_ptr(), false, nullptr)); 1832 } 1833 1834 DEBUG_CODE({ 1835 unsigned sz = m_lazy_clause.size(); 1836 for (unsigned i = 0; i < sz; i++) { 1837 literal l = m_lazy_clause[i]; 1838 if (l.var() != b) { 1839 SASSERT(value(l) == l_false || m_rlimit.is_canceled()); 1840 } 1841 else { 1842 SASSERT(value(l) == l_true || m_rlimit.is_canceled()); 1843 SASSERT(!l.sign() || m_bvalues[b] == l_false); 1844 SASSERT(l.sign() || m_bvalues[b] == l_true); 1845 } 1846 } 1847 }); 1848 checkpoint(); 1849 resolve_clause(b, m_lazy_clause.size(), m_lazy_clause.c_ptr()); 1850 1851 for (unsigned i = 0; i < jst.num_clauses(); ++i) { 1852 clause const& c = jst.clause(i); 1853 TRACE("nlsat", display(tout << "adding clause assumptions ", c) << "\n";); 1854 m_lemma_assumptions = m_asm.mk_join(static_cast<_assumption_set>(c.assumptions()), m_lemma_assumptions); 1855 } 1856 } 1857 1858 /** 1859 \brief Return true if all literals in ls are from previous stages. 1860 */ only_literals_from_previous_stagesnlsat::solver::imp1861 bool only_literals_from_previous_stages(unsigned num, literal const * ls) const { 1862 for (unsigned i = 0; i < num; i++) { 1863 if (max_var(ls[i]) == m_xk) 1864 return false; 1865 } 1866 return true; 1867 } 1868 1869 /** 1870 \brief Return the maximum scope level in ls. 1871 1872 \pre This method assumes value(ls[i]) is l_false for i in [0, num) 1873 */ max_scope_lvlnlsat::solver::imp1874 unsigned max_scope_lvl(unsigned num, literal const * ls) { 1875 unsigned max = 0; 1876 for (unsigned i = 0; i < num; i++) { 1877 literal l = ls[i]; 1878 bool_var b = l.var(); 1879 SASSERT(value(ls[i]) == l_false); 1880 if (assigned_value(l) == l_false) { 1881 unsigned lvl = m_levels[b]; 1882 if (lvl > max) 1883 max = lvl; 1884 } 1885 else { 1886 // l must be a literal from a previous stage that is false in the current interpretation 1887 SASSERT(assigned_value(l) == l_undef); 1888 SASSERT(max_var(b) != null_var); 1889 SASSERT(m_xk != null_var); 1890 SASSERT(max_var(b) < m_xk); 1891 } 1892 } 1893 return max; 1894 } 1895 1896 /** 1897 \brief Remove literals of the given lvl (that are in the current stage) from lemma. 1898 1899 \pre This method assumes value(ls[i]) is l_false for i in [0, num) 1900 */ remove_literals_from_lvlnlsat::solver::imp1901 void remove_literals_from_lvl(scoped_literal_vector & lemma, unsigned lvl) { 1902 TRACE("nlsat_resolve", tout << "removing literals from lvl: " << lvl << " and stage " << m_xk << "\n";); 1903 unsigned sz = lemma.size(); 1904 unsigned j = 0; 1905 for (unsigned i = 0; i < sz; i++) { 1906 literal l = lemma[i]; 1907 bool_var b = l.var(); 1908 SASSERT(is_marked(b)); 1909 SASSERT(value(lemma[i]) == l_false); 1910 if (assigned_value(l) == l_false && m_levels[b] == lvl && max_var(b) == m_xk) { 1911 m_num_marks++; 1912 continue; 1913 } 1914 lemma.set(j, l); 1915 j++; 1916 } 1917 lemma.shrink(j); 1918 } 1919 1920 /** 1921 \brief Return true if it is a Boolean lemma. 1922 */ is_bool_lemmanlsat::solver::imp1923 bool is_bool_lemma(unsigned sz, literal const * ls) const { 1924 for (unsigned i = 0; i < sz; i++) { 1925 if (m_atoms[ls[i].var()] != nullptr) 1926 return false; 1927 } 1928 return true; 1929 } 1930 1931 1932 /** 1933 Return the maximal decision level in lemma for literals in the first sz-1 positions that 1934 are at the same stage. If all these literals are from previous stages, 1935 we just backtrack the current level. 1936 */ find_new_level_arith_lemmanlsat::solver::imp1937 unsigned find_new_level_arith_lemma(unsigned sz, literal const * lemma) { 1938 SASSERT(!is_bool_lemma(sz, lemma)); 1939 unsigned new_lvl = 0; 1940 bool found_lvl = false; 1941 for (unsigned i = 0; i < sz - 1; i++) { 1942 literal l = lemma[i]; 1943 if (max_var(l) == m_xk) { 1944 bool_var b = l.var(); 1945 if (!found_lvl) { 1946 found_lvl = true; 1947 new_lvl = m_levels[b]; 1948 } 1949 else { 1950 if (m_levels[b] > new_lvl) 1951 new_lvl = m_levels[b]; 1952 } 1953 } 1954 } 1955 SASSERT(!found_lvl || new_lvl < scope_lvl()); 1956 if (!found_lvl) { 1957 TRACE("nlsat_resolve", tout << "fail to find new lvl, using previous one\n";); 1958 new_lvl = scope_lvl() - 1; 1959 } 1960 return new_lvl; 1961 } 1962 1963 struct scoped_reset_marks { 1964 imp& i; scoped_reset_marksnlsat::solver::imp::scoped_reset_marks1965 scoped_reset_marks(imp& i):i(i) {} ~scoped_reset_marksnlsat::solver::imp::scoped_reset_marks1966 ~scoped_reset_marks() { if (i.m_num_marks > 0) { i.m_num_marks = 0; for (char& m : i.m_marks) m = 0; } } 1967 }; 1968 1969 1970 /** 1971 \brief Return true if the conflict was solved. 1972 */ resolvenlsat::solver::imp1973 bool resolve(clause const & conflict) { 1974 clause const * conflict_clause = &conflict; 1975 m_lemma_assumptions = nullptr; 1976 start: 1977 SASSERT(check_marks()); 1978 TRACE("nlsat_proof", tout << "STARTING RESOLUTION\n";); 1979 TRACE("nlsat_proof_sk", tout << "STARTING RESOLUTION\n";); 1980 m_conflicts++; 1981 TRACE("nlsat", tout << "resolve, conflicting clause:\n"; display(tout, *conflict_clause) << "\n"; 1982 tout << "xk: "; if (m_xk != null_var) m_display_var(tout, m_xk); else tout << "<null>"; tout << "\n"; 1983 tout << "scope_lvl: " << scope_lvl() << "\n"; 1984 tout << "current assignment\n"; display_assignment(tout);); 1985 1986 m_num_marks = 0; 1987 m_lemma.reset(); 1988 m_lemma_assumptions = nullptr; 1989 scoped_reset_marks _sr(*this); 1990 resolve_clause(null_bool_var, *conflict_clause); 1991 1992 unsigned top = m_trail.size(); 1993 bool found_decision; 1994 while (true) { 1995 found_decision = false; 1996 while (m_num_marks > 0) { 1997 checkpoint(); 1998 SASSERT(top > 0); 1999 trail & t = m_trail[top-1]; 2000 SASSERT(t.m_kind != trail::NEW_STAGE); // we only mark literals that are in the same stage 2001 if (t.m_kind == trail::BVAR_ASSIGNMENT) { 2002 bool_var b = t.m_b; 2003 if (is_marked(b)) { 2004 TRACE("nlsat_resolve", tout << "found marked: b" << b << "\n"; display_atom(tout, b) << "\n";); 2005 m_num_marks--; 2006 reset_mark(b); 2007 justification jst = m_justifications[b]; 2008 switch (jst.get_kind()) { 2009 case justification::CLAUSE: 2010 resolve_clause(b, *(jst.get_clause())); 2011 break; 2012 case justification::LAZY: 2013 resolve_lazy_justification(b, *(jst.get_lazy())); 2014 break; 2015 case justification::DECISION: 2016 SASSERT(m_num_marks == 0); 2017 found_decision = true; 2018 TRACE("nlsat_resolve", tout << "found decision\n";); 2019 m_lemma.push_back(literal(b, m_bvalues[b] == l_true)); 2020 break; 2021 default: 2022 UNREACHABLE(); 2023 break; 2024 } 2025 } 2026 } 2027 top--; 2028 } 2029 2030 // m_lemma is an implicating clause after backtracking current scope level. 2031 if (found_decision) 2032 break; 2033 2034 // If lemma only contains literals from previous stages, then we can stop. 2035 // We make progress by returning to a previous stage with additional information (new lemma) 2036 // that forces us to select a new partial interpretation 2037 if (only_literals_from_previous_stages(m_lemma.size(), m_lemma.c_ptr())) 2038 break; 2039 2040 // Conflict does not depend on the current decision, and it is still in the current stage. 2041 // We should find 2042 // - the maximal scope level in the lemma 2043 // - remove literal assigned in the scope level from m_lemma 2044 // - backtrack to this level 2045 // - and continue conflict resolution from there 2046 // - we must bump m_num_marks for literals removed from m_lemma 2047 unsigned max_lvl = max_scope_lvl(m_lemma.size(), m_lemma.c_ptr()); 2048 TRACE("nlsat_resolve", tout << "conflict does not depend on current decision, backtracking to level: " << max_lvl << "\n";); 2049 SASSERT(max_lvl < scope_lvl()); 2050 remove_literals_from_lvl(m_lemma, max_lvl); 2051 undo_until_level(max_lvl); 2052 top = m_trail.size(); 2053 TRACE("nlsat_resolve", tout << "scope_lvl: " << scope_lvl() << " num marks: " << m_num_marks << "\n";); 2054 SASSERT(scope_lvl() == max_lvl); 2055 } 2056 2057 TRACE("nlsat_proof", tout << "New lemma\n"; display(tout, m_lemma); tout << "\n=========================\n";); 2058 TRACE("nlsat_proof_sk", tout << "New lemma\n"; display_abst(tout, m_lemma); tout << "\n=========================\n";); 2059 2060 if (m_lemma.empty()) { 2061 TRACE("nlsat", tout << "empty clause generated\n";); 2062 return false; // problem is unsat, empty clause was generated 2063 } 2064 2065 reset_marks(); // remove marks from the literals in m_lemmas. 2066 TRACE("nlsat", tout << "new lemma:\n"; display(tout, m_lemma.size(), m_lemma.c_ptr()); tout << "\n"; 2067 tout << "found_decision: " << found_decision << "\n";); 2068 2069 if (false && m_check_lemmas) { 2070 check_lemma(m_lemma.size(), m_lemma.c_ptr(), false, m_lemma_assumptions.get()); 2071 } 2072 2073 // There are two possibilities: 2074 // 1) m_lemma contains only literals from previous stages, and they 2075 // are false in the current interpretation. We make progress 2076 // by returning to a previous stage with additional information (new clause) 2077 // that forces us to select a new partial interpretation 2078 // >>> Return to some previous stage (we may also backjump many decisions and stages). 2079 // 2080 // 2) m_lemma contains at most one literal from the current level (the last literal). 2081 // Moreover, this literal was a decision, but the new lemma forces it to 2082 // be assigned to a different value. 2083 // >>> In this case, we remain in the same stage but, we add a new asserted literal 2084 // in a previous scope level. We may backjump many decisions. 2085 // 2086 unsigned sz = m_lemma.size(); 2087 clause * new_cls = nullptr; 2088 if (!found_decision) { 2089 // Case 1) 2090 // We just have to find the maximal variable in m_lemma, and return to that stage 2091 // Remark: the lemma may contain only boolean literals, in this case new_max_var == null_var; 2092 var new_max_var = max_var(sz, m_lemma.c_ptr()); 2093 TRACE("nlsat_resolve", tout << "backtracking to stage: " << new_max_var << ", curr: " << m_xk << "\n";); 2094 undo_until_stage(new_max_var); 2095 SASSERT(m_xk == new_max_var); 2096 new_cls = mk_clause(sz, m_lemma.c_ptr(), true, m_lemma_assumptions.get()); 2097 TRACE("nlsat", tout << "new_level: " << scope_lvl() << "\nnew_stage: " << new_max_var << "\n"; 2098 if (new_max_var != null_var) m_display_var(tout, new_max_var) << "\n";); 2099 } 2100 else { 2101 SASSERT(scope_lvl() >= 1); 2102 // Case 2) 2103 if (is_bool_lemma(m_lemma.size(), m_lemma.c_ptr())) { 2104 // boolean lemma, we just backtrack until the last literal is unassigned. 2105 bool_var max_bool_var = m_lemma[m_lemma.size()-1].var(); 2106 undo_until_unassigned(max_bool_var); 2107 } 2108 else { 2109 // We must find the maximal decision level in literals in the first sz-1 positions that 2110 // are at the same stage. If all these literals are from previous stages, 2111 // we just backtrack the current level. 2112 unsigned new_lvl = find_new_level_arith_lemma(m_lemma.size(), m_lemma.c_ptr()); 2113 TRACE("nlsat", tout << "backtracking to new level: " << new_lvl << ", curr: " << m_scope_lvl << "\n";); 2114 undo_until_level(new_lvl); 2115 } 2116 2117 if (lemma_is_clause(*conflict_clause)) { 2118 TRACE("nlsat", tout << "found decision literal in conflict clause\n";); 2119 VERIFY(process_clause(*conflict_clause, true)); 2120 return true; 2121 } 2122 new_cls = mk_clause(sz, m_lemma.c_ptr(), true, m_lemma_assumptions.get()); 2123 2124 } 2125 NLSAT_VERBOSE(display(verbose_stream(), *new_cls) << "\n";); 2126 if (!process_clause(*new_cls, true)) { 2127 TRACE("nlsat", tout << "new clause triggered another conflict, restarting conflict resolution...\n"; 2128 display(tout, *new_cls) << "\n"; 2129 ); 2130 // we are still in conflict 2131 conflict_clause = new_cls; 2132 goto start; 2133 } 2134 TRACE("nlsat_resolve_done", display_assignment(tout);); 2135 return true; 2136 } 2137 lemma_is_clausenlsat::solver::imp2138 bool lemma_is_clause(clause const& cls) const { 2139 bool same = (m_lemma.size() == cls.size()); 2140 for (unsigned i = 0; same && i < m_lemma.size(); ++i) { 2141 same = m_lemma[i] == cls[i]; 2142 } 2143 return same; 2144 } 2145 2146 2147 // ----------------------- 2148 // 2149 // Debugging 2150 // 2151 // ----------------------- 2152 check_watchesnlsat::solver::imp2153 bool check_watches() const { 2154 DEBUG_CODE( 2155 for (var x = 0; x < num_vars(); x++) { 2156 clause_vector const & cs = m_watches[x]; 2157 unsigned sz = cs.size(); 2158 for (unsigned i = 0; i < sz; i++) { 2159 SASSERT(max_var(*(cs[i])) == x); 2160 } 2161 }); 2162 return true; 2163 } 2164 check_bwatchesnlsat::solver::imp2165 bool check_bwatches() const { 2166 DEBUG_CODE( 2167 for (bool_var b = 0; b < m_bwatches.size(); b++) { 2168 clause_vector const & cs = m_bwatches[b]; 2169 unsigned sz = cs.size(); 2170 for (unsigned i = 0; i < sz; i++) { 2171 clause const & c = *(cs[i]); 2172 SASSERT(max_var(c) == null_var); 2173 SASSERT(max_bvar(c) == b); 2174 } 2175 }); 2176 return true; 2177 } 2178 check_invariantnlsat::solver::imp2179 bool check_invariant() const { 2180 SASSERT(check_watches()); 2181 SASSERT(check_bwatches()); 2182 return true; 2183 } 2184 check_satisfiednlsat::solver::imp2185 bool check_satisfied(clause_vector const & cs) const { 2186 unsigned sz = cs.size(); 2187 for (unsigned i = 0; i < sz; i++) { 2188 clause const & c = *(cs[i]); 2189 if (!is_satisfied(c)) { 2190 TRACE("nlsat", tout << "not satisfied\n"; display(tout, c); tout << "\n";); 2191 return false; 2192 } 2193 } 2194 return true; 2195 } 2196 check_satisfiednlsat::solver::imp2197 bool check_satisfied() const { 2198 TRACE("nlsat", tout << "bk: b" << m_bk << ", xk: x" << m_xk << "\n"; if (m_xk != null_var) { m_display_var(tout, m_xk); tout << "\n"; }); 2199 unsigned num = m_atoms.size(); 2200 if (m_bk != null_bool_var) 2201 num = m_bk; 2202 for (bool_var b = 0; b < num; b++) { 2203 if (!check_satisfied(m_bwatches[b])) { 2204 UNREACHABLE(); 2205 return false; 2206 } 2207 } 2208 if (m_xk != null_var) { 2209 for (var x = 0; x < m_xk; x++) { 2210 if (!check_satisfied(m_watches[x])) { 2211 UNREACHABLE(); 2212 return false; 2213 } 2214 } 2215 } 2216 return true; 2217 } 2218 2219 // ----------------------- 2220 // 2221 // Statistics 2222 // 2223 // ----------------------- 2224 collect_statisticsnlsat::solver::imp2225 void collect_statistics(statistics & st) { 2226 st.update("nlsat conflicts", m_conflicts); 2227 st.update("nlsat propagations", m_propagations); 2228 st.update("nlsat decisions", m_decisions); 2229 st.update("nlsat stages", m_stages); 2230 st.update("nlsat irrational assignments", m_irrational_assignments); 2231 } 2232 reset_statisticsnlsat::solver::imp2233 void reset_statistics() { 2234 m_conflicts = 0; 2235 m_propagations = 0; 2236 m_decisions = 0; 2237 m_stages = 0; 2238 m_irrational_assignments = 0; 2239 } 2240 2241 // ----------------------- 2242 // 2243 // Variable reordering 2244 // 2245 // ----------------------- 2246 2247 struct var_info_collector { 2248 pmanager & pm; 2249 atom_vector const & m_atoms; 2250 unsigned_vector m_max_degree; 2251 unsigned_vector m_num_occs; 2252 var_info_collectornlsat::solver::imp::var_info_collector2253 var_info_collector(pmanager & _pm, atom_vector const & atoms, unsigned num_vars): 2254 pm(_pm), 2255 m_atoms(atoms) { 2256 m_max_degree.resize(num_vars, 0); 2257 m_num_occs.resize(num_vars, 0); 2258 } 2259 2260 var_vector m_vars; collectnlsat::solver::imp::var_info_collector2261 void collect(poly * p) { 2262 m_vars.reset(); 2263 pm.vars(p, m_vars); 2264 unsigned sz = m_vars.size(); 2265 for (unsigned i = 0; i < sz; i++) { 2266 var x = m_vars[i]; 2267 unsigned k = pm.degree(p, x); 2268 m_num_occs[x]++; 2269 if (k > m_max_degree[x]) 2270 m_max_degree[x] = k; 2271 } 2272 } 2273 collectnlsat::solver::imp::var_info_collector2274 void collect(literal l) { 2275 bool_var b = l.var(); 2276 atom * a = m_atoms[b]; 2277 if (a == nullptr) 2278 return; 2279 if (a->is_ineq_atom()) { 2280 unsigned sz = to_ineq_atom(a)->size(); 2281 for (unsigned i = 0; i < sz; i++) { 2282 collect(to_ineq_atom(a)->p(i)); 2283 } 2284 } 2285 else { 2286 collect(to_root_atom(a)->p()); 2287 } 2288 } 2289 collectnlsat::solver::imp::var_info_collector2290 void collect(clause const & c) { 2291 unsigned sz = c.size(); 2292 for (unsigned i = 0; i < sz; i++) 2293 collect(c[i]); 2294 } 2295 collectnlsat::solver::imp::var_info_collector2296 void collect(clause_vector const & cs) { 2297 unsigned sz = cs.size(); 2298 for (unsigned i = 0; i < sz; i++) 2299 collect(*(cs[i])); 2300 } 2301 displaynlsat::solver::imp::var_info_collector2302 std::ostream& display(std::ostream & out, display_var_proc const & proc) { 2303 unsigned sz = m_num_occs.size(); 2304 for (unsigned i = 0; i < sz; i++) { 2305 proc(out, i); out << " -> " << m_max_degree[i] << " : " << m_num_occs[i] << "\n"; 2306 } 2307 return out; 2308 } 2309 }; 2310 2311 struct reorder_lt { 2312 var_info_collector const & m_info; reorder_ltnlsat::solver::imp::reorder_lt2313 reorder_lt(var_info_collector const & info):m_info(info) {} operator ()nlsat::solver::imp::reorder_lt2314 bool operator()(var x, var y) const { 2315 // high degree first 2316 if (m_info.m_max_degree[x] < m_info.m_max_degree[y]) 2317 return false; 2318 if (m_info.m_max_degree[x] > m_info.m_max_degree[y]) 2319 return true; 2320 // more constrained first 2321 if (m_info.m_num_occs[x] < m_info.m_num_occs[y]) 2322 return false; 2323 if (m_info.m_num_occs[x] > m_info.m_num_occs[y]) 2324 return true; 2325 return x < y; 2326 } 2327 }; 2328 2329 // Order variables by degree and number of occurrences heuristic_reordernlsat::solver::imp2330 void heuristic_reorder() { 2331 unsigned num = num_vars(); 2332 var_info_collector collector(m_pm, m_atoms, num); 2333 collector.collect(m_clauses); 2334 collector.collect(m_learned); 2335 TRACE("nlsat_reorder", collector.display(tout, m_display_var);); 2336 var_vector new_order; 2337 for (var x = 0; x < num; x++) { 2338 new_order.push_back(x); 2339 } 2340 std::sort(new_order.begin(), new_order.end(), reorder_lt(collector)); 2341 TRACE("nlsat_reorder", 2342 tout << "new order: "; for (unsigned i = 0; i < num; i++) tout << new_order[i] << " "; tout << "\n";); 2343 var_vector perm; 2344 perm.resize(num, 0); 2345 for (var x = 0; x < num; x++) { 2346 perm[new_order[x]] = x; 2347 } 2348 reorder(perm.size(), perm.c_ptr()); 2349 SASSERT(check_invariant()); 2350 } 2351 shuffle_varsnlsat::solver::imp2352 void shuffle_vars() { 2353 var_vector p; 2354 unsigned num = num_vars(); 2355 for (var x = 0; x < num; x++) { 2356 p.push_back(x); 2357 } 2358 random_gen r(++m_random_seed); 2359 shuffle(p.size(), p.c_ptr(), r); 2360 reorder(p.size(), p.c_ptr()); 2361 } 2362 can_reordernlsat::solver::imp2363 bool can_reorder() const { 2364 for (clause* c : m_learned) { 2365 if (has_root_atom(*c)) return false; 2366 } 2367 for (clause* c : m_clauses) { 2368 if (has_root_atom(*c)) return false; 2369 } 2370 return m_patch_var.empty(); 2371 } 2372 2373 /** 2374 \brief Reorder variables using the giving permutation. 2375 p maps internal variables to their new positions 2376 */ reordernlsat::solver::imp2377 void reorder(unsigned sz, var const * p) { 2378 remove_learned_roots(); 2379 SASSERT(can_reorder()); 2380 TRACE("nlsat_reorder", tout << "solver before variable reorder\n"; display(tout); 2381 display_vars(tout); 2382 tout << "\npermutation:\n"; 2383 for (unsigned i = 0; i < sz; i++) tout << p[i] << " "; tout << "\n"; 2384 ); 2385 SASSERT(num_vars() == sz); 2386 TRACE("nlsat_bool_assignment_bug", tout << "before reset watches\n"; display_bool_assignment(tout);); 2387 reset_watches(); 2388 assignment new_assignment(m_am); 2389 for (var x = 0; x < num_vars(); x++) { 2390 if (m_assignment.is_assigned(x)) 2391 new_assignment.set(p[x], m_assignment.value(x)); 2392 } 2393 var_vector new_inv_perm; 2394 new_inv_perm.resize(sz); 2395 // the undo_until_size(0) statement erases the Boolean assignment. 2396 // undo_until_size(0) 2397 undo_until_stage(null_var); 2398 m_cache.reset(); 2399 DEBUG_CODE({ 2400 for (var x = 0; x < num_vars(); x++) { 2401 SASSERT(m_watches[x].empty()); 2402 } 2403 }); 2404 // update m_perm mapping 2405 for (unsigned ext_x = 0; ext_x < sz; ext_x++) { 2406 // p: internal -> new pos 2407 // m_perm: internal -> external 2408 // m_inv_perm: external -> internal 2409 new_inv_perm[ext_x] = p[m_inv_perm[ext_x]]; 2410 m_perm.set(new_inv_perm[ext_x], ext_x); 2411 } 2412 bool_vector is_int; 2413 is_int.swap(m_is_int); 2414 for (var x = 0; x < sz; x++) { 2415 m_is_int.setx(p[x], is_int[x], false); 2416 SASSERT(m_infeasible[x] == 0); 2417 } 2418 m_inv_perm.swap(new_inv_perm); 2419 DEBUG_CODE({ 2420 for (var x = 0; x < num_vars(); x++) { 2421 SASSERT(x == m_inv_perm[m_perm[x]]); 2422 SASSERT(m_watches[x].empty()); 2423 } 2424 }); 2425 m_pm.rename(sz, p); 2426 TRACE("nlsat_bool_assignment_bug", tout << "before reinit cache\n"; display_bool_assignment(tout);); 2427 reinit_cache(); 2428 m_assignment.swap(new_assignment); 2429 reattach_arith_clauses(m_clauses); 2430 reattach_arith_clauses(m_learned); 2431 TRACE("nlsat_reorder", tout << "solver after variable reorder\n"; display(tout); display_vars(tout);); 2432 } 2433 2434 2435 /** 2436 \brief Restore variable order. 2437 */ restore_ordernlsat::solver::imp2438 void restore_order() { 2439 // m_perm: internal -> external 2440 // m_inv_perm: external -> internal 2441 var_vector p; 2442 p.append(m_perm); 2443 reorder(p.size(), p.c_ptr()); 2444 DEBUG_CODE({ 2445 for (var x = 0; x < num_vars(); x++) { 2446 SASSERT(m_perm[x] == x); 2447 SASSERT(m_inv_perm[x] == x); 2448 } 2449 }); 2450 } 2451 2452 /** 2453 \brief After variable reordering some lemmas containing root atoms may be ill-formed. 2454 */ remove_learned_rootsnlsat::solver::imp2455 void remove_learned_roots() { 2456 unsigned j = 0; 2457 for (clause* c : m_learned) { 2458 if (has_root_atom(*c)) { 2459 del_clause(c); 2460 } 2461 else { 2462 m_learned[j++] = c; 2463 } 2464 } 2465 m_learned.shrink(j); 2466 } 2467 2468 /** 2469 \brief Return true if the clause contains an ill formed root atom 2470 */ has_root_atomnlsat::solver::imp2471 bool has_root_atom(clause const & c) const { 2472 for (literal lit : c) { 2473 bool_var b = lit.var(); 2474 atom * a = m_atoms[b]; 2475 if (a && a->is_root_atom()) 2476 return true; 2477 } 2478 return false; 2479 } 2480 2481 /** 2482 \brief reinsert all polynomials in the unique cache 2483 */ reinit_cachenlsat::solver::imp2484 void reinit_cache() { 2485 reinit_cache(m_clauses); 2486 reinit_cache(m_learned); 2487 for (atom* a : m_atoms) 2488 reinit_cache(a); 2489 } reinit_cachenlsat::solver::imp2490 void reinit_cache(clause_vector const & cs) { 2491 for (clause* c : cs) 2492 reinit_cache(*c); 2493 } reinit_cachenlsat::solver::imp2494 void reinit_cache(clause const & c) { 2495 for (literal l : c) 2496 reinit_cache(l); 2497 } reinit_cachenlsat::solver::imp2498 void reinit_cache(literal l) { 2499 bool_var b = l.var(); 2500 reinit_cache(m_atoms[b]); 2501 } reinit_cachenlsat::solver::imp2502 void reinit_cache(atom* a) { 2503 if (a == nullptr) { 2504 2505 } 2506 else if (a->is_ineq_atom()) { 2507 var max = 0; 2508 unsigned sz = to_ineq_atom(a)->size(); 2509 for (unsigned i = 0; i < sz; i++) { 2510 poly * p = to_ineq_atom(a)->p(i); 2511 VERIFY(m_cache.mk_unique(p) == p); 2512 var x = m_pm.max_var(p); 2513 if (x > max) 2514 max = x; 2515 } 2516 a->m_max_var = max; 2517 } 2518 else { 2519 poly * p = to_root_atom(a)->p(); 2520 VERIFY(m_cache.mk_unique(p) == p); 2521 a->m_max_var = m_pm.max_var(p); 2522 } 2523 } 2524 reset_watchesnlsat::solver::imp2525 void reset_watches() { 2526 unsigned num = num_vars(); 2527 for (var x = 0; x < num; x++) { 2528 m_watches[x].reset(); 2529 } 2530 } 2531 reattach_arith_clausesnlsat::solver::imp2532 void reattach_arith_clauses(clause_vector const & cs) { 2533 for (clause* cp : cs) { 2534 var x = max_var(*cp); 2535 if (x != null_var) 2536 m_watches[x].push_back(cp); 2537 } 2538 } 2539 2540 // ----------------------- 2541 // 2542 // Solver initialization 2543 // 2544 // ----------------------- 2545 2546 struct degree_lt { 2547 unsigned_vector & m_degrees; degree_ltnlsat::solver::imp::degree_lt2548 degree_lt(unsigned_vector & ds):m_degrees(ds) {} operator ()nlsat::solver::imp::degree_lt2549 bool operator()(unsigned i1, unsigned i2) const { 2550 if (m_degrees[i1] < m_degrees[i2]) 2551 return true; 2552 if (m_degrees[i1] > m_degrees[i2]) 2553 return false; 2554 return i1 < i2; 2555 } 2556 }; 2557 2558 unsigned_vector m_cs_degrees; 2559 unsigned_vector m_cs_p; sort_clauses_by_degreenlsat::solver::imp2560 void sort_clauses_by_degree(unsigned sz, clause ** cs) { 2561 if (sz <= 1) 2562 return; 2563 TRACE("nlsat_reorder_clauses", tout << "before:\n"; for (unsigned i = 0; i < sz; i++) { display(tout, *(cs[i])); tout << "\n"; }); 2564 m_cs_degrees.reset(); 2565 m_cs_p.reset(); 2566 for (unsigned i = 0; i < sz; i++) { 2567 m_cs_p.push_back(i); 2568 m_cs_degrees.push_back(degree(*(cs[i]))); 2569 } 2570 std::sort(m_cs_p.begin(), m_cs_p.end(), degree_lt(m_cs_degrees)); 2571 TRACE("nlsat_reorder_clauses", tout << "permutation: "; ::display(tout, m_cs_p.begin(), m_cs_p.end()); tout << "\n";); 2572 apply_permutation(sz, cs, m_cs_p.c_ptr()); 2573 TRACE("nlsat_reorder_clauses", tout << "after:\n"; for (unsigned i = 0; i < sz; i++) { display(tout, *(cs[i])); tout << "\n"; }); 2574 } 2575 sort_watched_clausesnlsat::solver::imp2576 void sort_watched_clauses() { 2577 unsigned num = num_vars(); 2578 for (unsigned i = 0; i < num; i++) { 2579 clause_vector & ws = m_watches[i]; 2580 sort_clauses_by_degree(ws.size(), ws.c_ptr()); 2581 } 2582 } 2583 2584 // ----------------------- 2585 // 2586 // Full dimensional 2587 // 2588 // A problem is in the full dimensional fragment if it does 2589 // not contain equalities or non-strict inequalities. 2590 // 2591 // ----------------------- 2592 is_full_dimensionalnlsat::solver::imp2593 bool is_full_dimensional(literal l) const { 2594 atom * a = m_atoms[l.var()]; 2595 if (a == nullptr) 2596 return true; 2597 switch (a->get_kind()) { 2598 case atom::EQ: return l.sign(); 2599 case atom::LT: return !l.sign(); 2600 case atom::GT: return !l.sign(); 2601 case atom::ROOT_EQ: return l.sign(); 2602 case atom::ROOT_LT: return !l.sign(); 2603 case atom::ROOT_GT: return !l.sign(); 2604 case atom::ROOT_LE: return l.sign(); 2605 case atom::ROOT_GE: return l.sign(); 2606 default: 2607 UNREACHABLE(); 2608 return false; 2609 } 2610 } 2611 is_full_dimensionalnlsat::solver::imp2612 bool is_full_dimensional(clause const & c) const { 2613 for (literal l : c) { 2614 if (!is_full_dimensional(l)) 2615 return false; 2616 } 2617 return true; 2618 } 2619 is_full_dimensionalnlsat::solver::imp2620 bool is_full_dimensional(clause_vector const & cs) const { 2621 for (clause* c : cs) { 2622 if (!is_full_dimensional(*c)) 2623 return false; 2624 } 2625 return true; 2626 } 2627 is_full_dimensionalnlsat::solver::imp2628 bool is_full_dimensional() const { 2629 return is_full_dimensional(m_clauses); 2630 } 2631 2632 2633 // ----------------------- 2634 // 2635 // Simplification 2636 // 2637 // ----------------------- 2638 2639 // solve simple equalities 2640 // TBD WU-Reit decomposition? 2641 2642 /** 2643 \brief isolate variables in unit equalities. 2644 Assume a clause is c == v*p + q 2645 and the context implies p > 0 2646 2647 replace v by -q/p 2648 remove clause c, 2649 The for other occurrences of v, 2650 replace v*r + v*v*r' > 0 by 2651 by p*p*v*r + p*p*v*v*r' > 0 2652 by p*q*r + q*q*r' > 0 2653 2654 The method ignores lemmas and assumes constraints don't use roots. 2655 */ 2656 simplifynlsat::solver::imp2657 bool simplify() { 2658 polynomial_ref p(m_pm), q(m_pm); 2659 var v; 2660 init_var_signs(); 2661 SASSERT(m_learned.empty()); 2662 bool change = true; 2663 while (change) { 2664 change = false; 2665 for (clause* c : m_clauses) { 2666 if (solve_var(*c, v, p, q)) { 2667 q = -q; 2668 TRACE("nlsat", tout << "p: " << p << "\nq: " << q << "\n x" << v << "\n";); 2669 m_patch_var.push_back(v); 2670 m_patch_num.push_back(q); 2671 m_patch_denom.push_back(p); 2672 del_clause(c, m_clauses); 2673 if (!substitute_var(v, p, q)) 2674 return false; 2675 TRACE("nlsat", display(tout << "simplified\n");); 2676 change = true; 2677 break; 2678 } 2679 } 2680 } 2681 return true; 2682 } 2683 fix_patchnlsat::solver::imp2684 void fix_patch() { 2685 for (unsigned i = m_patch_var.size(); i-- > 0; ) { 2686 var v = m_patch_var[i]; 2687 poly* q = m_patch_num.get(i); 2688 poly* p = m_patch_denom.get(i); 2689 scoped_anum pv(m_am), qv(m_am), val(m_am); 2690 m_pm.eval(p, m_assignment, pv); 2691 m_pm.eval(q, m_assignment, qv); 2692 SASSERT(!m_am.is_zero(pv)); 2693 val = qv / pv; 2694 TRACE("nlsat", 2695 m_display_var(tout << "patch v" << v << " ", v) << "\n"; 2696 if (m_assignment.is_assigned(v)) m_am.display(tout << "previous value: ", m_assignment.value(v)); tout << "\n"; 2697 m_am.display(tout << "updated value: ", val); tout << "\n"; 2698 ); 2699 m_assignment.set_core(v, val); 2700 } 2701 } 2702 substitute_varnlsat::solver::imp2703 bool substitute_var(var x, poly* p, poly* q) { 2704 bool is_sat = true; 2705 polynomial_ref pr(m_pm); 2706 polynomial_ref_vector ps(m_pm); 2707 2708 u_map<literal> b2l; 2709 scoped_literal_vector lits(m_solver); 2710 bool_vector even; 2711 unsigned num_atoms = m_atoms.size(); 2712 for (unsigned j = 0; j < num_atoms; ++j) { 2713 atom* a = m_atoms[j]; 2714 if (a && a->is_ineq_atom()) { 2715 ineq_atom const& a1 = *to_ineq_atom(a); 2716 unsigned sz = a1.size(); 2717 ps.reset(); 2718 even.reset(); 2719 bool change = false; 2720 auto k = a1.get_kind(); 2721 for (unsigned i = 0; i < sz; ++i) { 2722 poly * po = a1.p(i); 2723 m_pm.substitute(po, x, q, p, pr); 2724 change |= pr != po; 2725 TRACE("nlsat", tout << pr << "\n";); 2726 if (m_pm.is_zero(pr)) { 2727 ps.reset(); 2728 even.reset(); 2729 ps.push_back(pr); 2730 even.push_back(false); 2731 break; 2732 } 2733 if (m_pm.is_const(pr)) { 2734 if (!a1.is_even(i) && m_pm.m().is_neg(m_pm.coeff(pr, 0))) { 2735 k = atom::flip(k); 2736 } 2737 continue; 2738 } 2739 ps.push_back(pr); 2740 even.push_back(a1.is_even(i)); 2741 } 2742 if (!change) continue; 2743 literal l = mk_ineq_literal(k, ps.size(), ps.c_ptr(), even.c_ptr()); 2744 lits.push_back(l); 2745 if (a1.m_bool_var != l.var()) { 2746 b2l.insert(a1.m_bool_var, l); 2747 } 2748 } 2749 } 2750 is_sat = update_clauses(b2l); 2751 return is_sat; 2752 } 2753 2754 update_clausesnlsat::solver::imp2755 bool update_clauses(u_map<literal> const& b2l) { 2756 bool is_sat = true; 2757 literal_vector lits; 2758 clause_vector to_delete; 2759 unsigned n = m_clauses.size(); 2760 for (unsigned i = 0; i < n; ++i) { 2761 clause* c = m_clauses[i]; 2762 lits.reset(); 2763 bool changed = false; 2764 bool is_tautology = false; 2765 for (literal l : *c) { 2766 literal lit = null_literal; 2767 if (b2l.find(l.var(), lit)) { 2768 lit = l.sign() ? ~lit : lit; 2769 if (lit == true_literal) { 2770 is_tautology = true; 2771 } 2772 else if (lit != false_literal) { 2773 lits.push_back(lit); 2774 } 2775 changed = true; 2776 } 2777 else { 2778 lits.push_back(l); 2779 } 2780 } 2781 if (changed) { 2782 to_delete.push_back(c); 2783 if (is_tautology) { 2784 continue; 2785 } 2786 if (lits.empty()) { 2787 is_sat = false; 2788 } 2789 else { 2790 mk_clause(lits.size(), lits.c_ptr(), c->is_learned(), static_cast<_assumption_set>(c->assumptions())); 2791 } 2792 } 2793 } 2794 for (clause* c : to_delete) { 2795 del_clause(c, m_clauses); 2796 } 2797 return is_sat; 2798 } 2799 is_unit_ineqnlsat::solver::imp2800 bool is_unit_ineq(clause const& c) const { 2801 return 2802 c.size() == 1 && 2803 m_atoms[c[0].var()] && 2804 m_atoms[c[0].var()]->is_ineq_atom(); 2805 } 2806 is_unit_eqnlsat::solver::imp2807 bool is_unit_eq(clause const& c) const { 2808 return 2809 is_unit_ineq(c) && 2810 !c[0].sign() && 2811 m_atoms[c[0].var()]->is_eq(); 2812 } 2813 2814 /** 2815 \brief determine whether the clause is a comparison v > k or v < k', where k >= 0 or k' <= 0. 2816 */ is_cmp0nlsat::solver::imp2817 lbool is_cmp0(clause const& c, var& v) { 2818 if (!is_unit_ineq(c)) return l_undef; 2819 literal lit = c[0]; 2820 ineq_atom const& a = *to_ineq_atom(m_atoms[lit.var()]); 2821 bool sign = lit.sign(); 2822 poly * p0; 2823 if (!is_single_poly(a, p0)) return l_undef; 2824 if (m_pm.is_var(p0, v)) { 2825 if (!sign && a.get_kind() == atom::GT) { 2826 return l_true; 2827 } 2828 if (!sign && a.get_kind() == atom::LT) { 2829 return l_false; 2830 } 2831 return l_undef; 2832 } 2833 polynomial::scoped_numeral n(m_pm.m()); 2834 if (m_pm.is_var_num(p0, v, n)) { 2835 // x - k > 0 2836 if (!sign && a.get_kind() == atom::GT && m_pm.m().is_nonneg(n)) { 2837 return l_true; 2838 } 2839 // x + k < 0 2840 if (!sign && a.get_kind() == atom::LT && m_pm.m().is_nonpos(n)) { 2841 return l_false; 2842 } 2843 // !(x + k > 0) 2844 if (sign && a.get_kind() == atom::GT && m_pm.m().is_pos(n)) { 2845 return l_false; 2846 } 2847 // !(x - k < 0) 2848 if (sign && a.get_kind() == atom::LT && m_pm.m().is_neg(n)) { 2849 return l_true; 2850 } 2851 } 2852 return l_undef; 2853 } 2854 is_single_polynlsat::solver::imp2855 bool is_single_poly(ineq_atom const& a, poly*& p) { 2856 unsigned sz = a.size(); 2857 return sz == 1 && a.is_odd(0) && (p = a.p(0), true); 2858 } 2859 2860 svector<lbool> m_var_signs; 2861 init_var_signsnlsat::solver::imp2862 void init_var_signs() { 2863 m_var_signs.reset(); 2864 for (clause* cp : m_clauses) { 2865 clause& c = *cp; 2866 var x = 0; 2867 lbool cmp = is_cmp0(c, x); 2868 switch (cmp) { 2869 case l_true: 2870 m_var_signs.setx(x, l_true, l_undef); 2871 break; 2872 case l_false: 2873 m_var_signs.setx(x, l_false, l_undef); 2874 break; 2875 default: 2876 break; 2877 } 2878 } 2879 } 2880 2881 /** 2882 \brief returns true then c is an equality that is equivalent to v*p + q, 2883 and p > 0, v does not occur in p, q. 2884 */ solve_varnlsat::solver::imp2885 bool solve_var(clause& c, var& v, polynomial_ref& p, polynomial_ref& q) { 2886 poly* p0; 2887 if (!is_unit_eq(c)) return false; 2888 ineq_atom & a = *to_ineq_atom(m_atoms[c[0].var()]); 2889 if (!is_single_poly(a, p0)) return false; 2890 var mx = max_var(p0); 2891 if (mx >= m_is_int.size()) return false; 2892 for (var x = 0; x <= mx; ++x) { 2893 if (m_is_int[x]) continue; 2894 if (1 == m_pm.degree(p0, x)) { 2895 p = m_pm.coeff(p0, x, 1, q); 2896 if (!m_pm.is_const(p)) 2897 break; 2898 switch (m_pm.sign(p, m_var_signs)) { 2899 case l_true: 2900 v = x; 2901 return true; 2902 case l_false: 2903 v = x; 2904 p = -p; 2905 q = -q; 2906 return true; 2907 default: 2908 break; 2909 } 2910 } 2911 } 2912 return false; 2913 } 2914 2915 // ----------------------- 2916 // 2917 // Pretty printing 2918 // 2919 // ----------------------- 2920 display_num_assignmentnlsat::solver::imp2921 std::ostream& display_num_assignment(std::ostream & out, display_var_proc const & proc) const { 2922 for (var x = 0; x < num_vars(); x++) { 2923 if (m_assignment.is_assigned(x)) { 2924 proc(out, x); 2925 out << " -> "; 2926 m_am.display_decimal(out, m_assignment.value(x)); 2927 out << "\n"; 2928 } 2929 } 2930 return out; 2931 } 2932 display_bool_assignmentnlsat::solver::imp2933 std::ostream& display_bool_assignment(std::ostream & out) const { 2934 unsigned sz = m_atoms.size(); 2935 for (bool_var b = 0; b < sz; b++) { 2936 if (m_atoms[b] == nullptr && m_bvalues[b] != l_undef) { 2937 out << "b" << b << " -> " << (m_bvalues[b] == l_true ? "true" : "false") << "\n"; 2938 } 2939 else if (m_atoms[b] != nullptr && m_bvalues[b] != l_undef) { 2940 display(out << "b" << b << " ", *m_atoms[b]) << " -> " << (m_bvalues[b] == l_true ? "true" : "false") << "\n"; 2941 } 2942 } 2943 TRACE("nlsat_bool_assignment", 2944 for (bool_var b = 0; b < sz; b++) { 2945 out << "b" << b << " -> " << m_bvalues[b] << " "; 2946 if (m_atoms[b]) display(out, *m_atoms[b]); 2947 out << "\n"; 2948 }); 2949 return out; 2950 } 2951 display_mathematica_assignmentnlsat::solver::imp2952 bool display_mathematica_assignment(std::ostream & out) const { 2953 bool first = true; 2954 for (var x = 0; x < num_vars(); x++) { 2955 if (m_assignment.is_assigned(x)) { 2956 if (first) 2957 first = false; 2958 else 2959 out << " && "; 2960 out << "x" << x << " == "; 2961 m_am.display_mathematica(out, m_assignment.value(x)); 2962 } 2963 } 2964 return !first; 2965 } 2966 display_num_assignmentnlsat::solver::imp2967 std::ostream& display_num_assignment(std::ostream & out) const { 2968 return display_num_assignment(out, m_display_var); 2969 } 2970 display_assignmentnlsat::solver::imp2971 std::ostream& display_assignment(std::ostream& out) const { 2972 display_bool_assignment(out); 2973 display_num_assignment(out); 2974 return out; 2975 } 2976 displaynlsat::solver::imp2977 std::ostream& display(std::ostream& out, justification j) const { 2978 switch (j.get_kind()) { 2979 case justification::CLAUSE: 2980 display(out, *j.get_clause()) << "\n"; 2981 break; 2982 case justification::LAZY: { 2983 lazy_justification const& lz = *j.get_lazy(); 2984 display_not(out, lz.num_lits(), lz.lits()) << "\n"; 2985 for (unsigned i = 0; i < lz.num_clauses(); ++i) { 2986 display(out, lz.clause(i)) << "\n"; 2987 } 2988 break; 2989 } 2990 default: 2991 out << j.get_kind() << "\n"; 2992 break; 2993 } 2994 return out; 2995 } 2996 displaynlsat::solver::imp2997 std::ostream& display(std::ostream & out, ineq_atom const & a, display_var_proc const & proc, bool use_star = false) const { 2998 unsigned sz = a.size(); 2999 for (unsigned i = 0; i < sz; i++) { 3000 if (use_star && i > 0) 3001 out << "*"; 3002 bool is_even = a.is_even(i); 3003 if (is_even || sz > 1) 3004 out << "("; 3005 m_pm.display(out, a.p(i), proc, use_star); 3006 if (is_even || sz > 1) 3007 out << ")"; 3008 if (is_even) 3009 out << "^2"; 3010 } 3011 switch (a.get_kind()) { 3012 case atom::LT: out << " < 0"; break; 3013 case atom::GT: out << " > 0"; break; 3014 case atom::EQ: out << " = 0"; break; 3015 default: UNREACHABLE(); break; 3016 } 3017 return out; 3018 } 3019 display_mathematicanlsat::solver::imp3020 std::ostream& display_mathematica(std::ostream & out, ineq_atom const & a) const { 3021 unsigned sz = a.size(); 3022 for (unsigned i = 0; i < sz; i++) { 3023 if (i > 0) 3024 out << "*"; 3025 bool is_even = a.is_even(i); 3026 if (sz > 1) 3027 out << "("; 3028 if (is_even) 3029 out << "("; 3030 m_pm.display(out, a.p(i), display_var_proc(), true); 3031 if (is_even) 3032 out << "^2)"; 3033 if (sz > 1) 3034 out << ")"; 3035 } 3036 switch (a.get_kind()) { 3037 case atom::LT: out << " < 0"; break; 3038 case atom::GT: out << " > 0"; break; 3039 case atom::EQ: out << " == 0"; break; 3040 default: UNREACHABLE(); break; 3041 } 3042 return out; 3043 } 3044 display_smt2nlsat::solver::imp3045 std::ostream& display_smt2(std::ostream & out, ineq_atom const & a, display_var_proc const & proc) const { 3046 switch (a.get_kind()) { 3047 case atom::LT: out << "(< "; break; 3048 case atom::GT: out << "(> "; break; 3049 case atom::EQ: out << "(= "; break; 3050 default: UNREACHABLE(); break; 3051 } 3052 unsigned sz = a.size(); 3053 if (sz > 1) 3054 out << "(* "; 3055 for (unsigned i = 0; i < sz; i++) { 3056 if (i > 0) out << " "; 3057 if (a.is_even(i)) { 3058 out << "(* "; 3059 m_pm.display_smt2(out, a.p(i), proc); 3060 out << " "; 3061 m_pm.display_smt2(out, a.p(i), proc); 3062 out << ")"; 3063 } 3064 else { 3065 m_pm.display_smt2(out, a.p(i), proc); 3066 } 3067 } 3068 if (sz > 1) 3069 out << ")"; 3070 out << " 0)"; 3071 return out; 3072 } 3073 display_smt2nlsat::solver::imp3074 std::ostream& display_smt2(std::ostream & out, root_atom const & a, display_var_proc const & proc) const { 3075 return display(out, a, proc); 3076 } 3077 displaynlsat::solver::imp3078 std::ostream& display(std::ostream & out, root_atom const & a, display_var_proc const & proc) const { 3079 proc(out, a.x()); 3080 switch (a.get_kind()) { 3081 case atom::ROOT_LT: out << " < "; break; 3082 case atom::ROOT_GT: out << " > "; break; 3083 case atom::ROOT_LE: out << " <= "; break; 3084 case atom::ROOT_GE: out << " >= "; break; 3085 case atom::ROOT_EQ: out << " = "; break; 3086 default: UNREACHABLE(); break; 3087 } 3088 out << "root[" << a.i() << "]("; 3089 m_pm.display(out, a.p(), proc); 3090 out << ")"; 3091 return out; 3092 } 3093 3094 struct mathematica_var_proc : public display_var_proc { 3095 var m_x; 3096 public: mathematica_var_procnlsat::solver::imp::mathematica_var_proc3097 mathematica_var_proc(var x):m_x(x) {} operator ()nlsat::solver::imp::mathematica_var_proc3098 std::ostream& operator()(std::ostream & out, var x) const override { 3099 if (m_x == x) 3100 return out << "#1"; 3101 else 3102 return out << "x" << x; 3103 } 3104 }; 3105 display_mathematicanlsat::solver::imp3106 std::ostream& display_mathematica(std::ostream & out, root_atom const & a) const { 3107 out << "x" << a.x(); 3108 switch (a.get_kind()) { 3109 case atom::ROOT_LT: out << " < "; break; 3110 case atom::ROOT_GT: out << " > "; break; 3111 case atom::ROOT_LE: out << " <= "; break; 3112 case atom::ROOT_GE: out << " >= "; break; 3113 case atom::ROOT_EQ: out << " == "; break; 3114 default: UNREACHABLE(); break; 3115 } 3116 out << "Root["; 3117 m_pm.display(out, a.p(), mathematica_var_proc(a.x()), true); 3118 out << " &, " << a.i() << "]"; 3119 return out; 3120 } 3121 display_smt2nlsat::solver::imp3122 std::ostream& display_smt2(std::ostream & out, root_atom const & a) const { 3123 NOT_IMPLEMENTED_YET(); 3124 return out; 3125 } 3126 displaynlsat::solver::imp3127 std::ostream& display(std::ostream & out, atom const & a, display_var_proc const & proc) const { 3128 if (a.is_ineq_atom()) 3129 return display(out, static_cast<ineq_atom const &>(a), proc); 3130 else 3131 return display(out, static_cast<root_atom const &>(a), proc); 3132 } 3133 displaynlsat::solver::imp3134 std::ostream& display(std::ostream & out, atom const & a) const { 3135 return display(out, a, m_display_var); 3136 } 3137 display_mathematicanlsat::solver::imp3138 std::ostream& display_mathematica(std::ostream & out, atom const & a) const { 3139 if (a.is_ineq_atom()) 3140 return display_mathematica(out, static_cast<ineq_atom const &>(a)); 3141 else 3142 return display_mathematica(out, static_cast<root_atom const &>(a)); 3143 } 3144 display_smt2nlsat::solver::imp3145 std::ostream& display_smt2(std::ostream & out, atom const & a, display_var_proc const & proc) const { 3146 if (a.is_ineq_atom()) 3147 return display_smt2(out, static_cast<ineq_atom const &>(a), proc); 3148 else 3149 return display_smt2(out, static_cast<root_atom const &>(a), proc); 3150 } 3151 display_atomnlsat::solver::imp3152 std::ostream& display_atom(std::ostream & out, bool_var b, display_var_proc const & proc) const { 3153 if (b == 0) 3154 out << "true"; 3155 else if (m_atoms[b] == 0) 3156 out << "b" << b; 3157 else 3158 display(out, *(m_atoms[b]), proc); 3159 return out; 3160 } 3161 display_atomnlsat::solver::imp3162 std::ostream& display_atom(std::ostream & out, bool_var b) const { 3163 return display_atom(out, b, m_display_var); 3164 } 3165 display_mathematica_atomnlsat::solver::imp3166 std::ostream& display_mathematica_atom(std::ostream & out, bool_var b) const { 3167 if (b == 0) 3168 out << "(0 < 1)"; 3169 else if (m_atoms[b] == 0) 3170 out << "b" << b; 3171 else 3172 display_mathematica(out, *(m_atoms[b])); 3173 return out; 3174 } 3175 display_smt2_atomnlsat::solver::imp3176 std::ostream& display_smt2_atom(std::ostream & out, bool_var b, display_var_proc const & proc) const { 3177 if (b == 0) 3178 out << "true"; 3179 else if (m_atoms[b] == 0) 3180 out << "b" << b; 3181 else 3182 display_smt2(out, *(m_atoms[b]), proc); 3183 return out; 3184 } 3185 displaynlsat::solver::imp3186 std::ostream& display(std::ostream & out, literal l, display_var_proc const & proc) const { 3187 if (l.sign()) { 3188 bool_var b = l.var(); 3189 out << "!"; 3190 if (m_atoms[b] != 0) 3191 out << "("; 3192 display_atom(out, b, proc); 3193 if (m_atoms[b] != 0) 3194 out << ")"; 3195 } 3196 else { 3197 display_atom(out, l.var(), proc); 3198 } 3199 return out; 3200 } 3201 displaynlsat::solver::imp3202 std::ostream& display(std::ostream & out, literal l) const { 3203 return display(out, l, m_display_var); 3204 } 3205 display_smt2nlsat::solver::imp3206 std::ostream& display_smt2(std::ostream & out, literal l) const { 3207 return display_smt2(out, l, m_display_var); 3208 } 3209 display_mathematicanlsat::solver::imp3210 std::ostream& display_mathematica(std::ostream & out, literal l) const { 3211 if (l.sign()) { 3212 bool_var b = l.var(); 3213 out << "!"; 3214 if (m_atoms[b] != 0) 3215 out << "("; 3216 display_mathematica_atom(out, b); 3217 if (m_atoms[b] != 0) 3218 out << ")"; 3219 } 3220 else { 3221 display_mathematica_atom(out, l.var()); 3222 } 3223 return out; 3224 } 3225 display_smt2nlsat::solver::imp3226 std::ostream& display_smt2(std::ostream & out, literal l, display_var_proc const & proc) const { 3227 if (l.sign()) { 3228 bool_var b = l.var(); 3229 out << "(not "; 3230 display_smt2_atom(out, b, proc); 3231 out << ")"; 3232 } 3233 else { 3234 display_smt2_atom(out, l.var(), proc); 3235 } 3236 return out; 3237 } 3238 display_assumptionsnlsat::solver::imp3239 std::ostream& display_assumptions(std::ostream & out, _assumption_set s) const { 3240 vector<assumption, false> deps; 3241 m_asm.linearize(s, deps); 3242 bool first = true; 3243 for (auto dep : deps) { 3244 if (first) first = false; else out << " "; 3245 if (m_display_assumption) (*m_display_assumption)(out, dep); 3246 } 3247 return out; 3248 } 3249 displaynlsat::solver::imp3250 std::ostream& display(std::ostream & out, unsigned num, literal const * ls, display_var_proc const & proc) const { 3251 for (unsigned i = 0; i < num; i++) { 3252 if (i > 0) 3253 out << " or "; 3254 display(out, ls[i], proc); 3255 } 3256 return out; 3257 } 3258 displaynlsat::solver::imp3259 std::ostream& display(std::ostream & out, unsigned num, literal const * ls) const { 3260 return display(out, num, ls, m_display_var); 3261 } 3262 display_notnlsat::solver::imp3263 std::ostream& display_not(std::ostream & out, unsigned num, literal const * ls, display_var_proc const & proc) const { 3264 for (unsigned i = 0; i < num; i++) { 3265 if (i > 0) 3266 out << " or "; 3267 display(out, ~ls[i], proc); 3268 } 3269 return out; 3270 } 3271 display_notnlsat::solver::imp3272 std::ostream& display_not(std::ostream & out, unsigned num, literal const * ls) const { 3273 return display_not(out, num, ls, m_display_var); 3274 } 3275 displaynlsat::solver::imp3276 std::ostream& display(std::ostream & out, scoped_literal_vector const & cs) { 3277 return display(out, cs.size(), cs.c_ptr(), m_display_var); 3278 } 3279 displaynlsat::solver::imp3280 std::ostream& display(std::ostream & out, clause const & c, display_var_proc const & proc) const { 3281 if (c.assumptions() != nullptr) { 3282 display_assumptions(out, static_cast<_assumption_set>(c.assumptions())); 3283 out << " |- "; 3284 } 3285 return display(out, c.size(), c.c_ptr(), proc); 3286 } 3287 displaynlsat::solver::imp3288 std::ostream& display(std::ostream & out, clause const & c) const { 3289 return display(out, c, m_display_var); 3290 } 3291 display_smt2nlsat::solver::imp3292 std::ostream& display_smt2(std::ostream & out, unsigned num, literal const * ls, display_var_proc const & proc) const { 3293 if (num == 0) { 3294 out << "false"; 3295 } 3296 else if (num == 1) { 3297 display_smt2(out, ls[0], proc); 3298 } 3299 else { 3300 out << "(or"; 3301 for (unsigned i = 0; i < num; i++) { 3302 out << " "; 3303 display_smt2(out, ls[i], proc); 3304 } 3305 out << ")"; 3306 } 3307 return out; 3308 } 3309 display_smt2nlsat::solver::imp3310 std::ostream& display_smt2(std::ostream & out, clause const & c, display_var_proc const & proc = display_var_proc()) const { 3311 return display_smt2(out, c.size(), c.c_ptr(), proc); 3312 } 3313 display_abstnlsat::solver::imp3314 std::ostream& display_abst(std::ostream & out, literal l) const { 3315 if (l.sign()) { 3316 bool_var b = l.var(); 3317 out << "!"; 3318 if (b == true_bool_var) 3319 out << "true"; 3320 else 3321 out << "b" << b; 3322 } 3323 else { 3324 out << "b" << l.var(); 3325 } 3326 return out; 3327 } 3328 display_abstnlsat::solver::imp3329 std::ostream& display_abst(std::ostream & out, unsigned num, literal const * ls) const { 3330 for (unsigned i = 0; i < num; i++) { 3331 if (i > 0) 3332 out << " or "; 3333 display_abst(out, ls[i]); 3334 } 3335 return out; 3336 } 3337 display_abstnlsat::solver::imp3338 std::ostream& display_abst(std::ostream & out, scoped_literal_vector const & cs) const { 3339 return display_abst(out, cs.size(), cs.c_ptr()); 3340 } 3341 display_abstnlsat::solver::imp3342 std::ostream& display_abst(std::ostream & out, clause const & c) const { 3343 return display_abst(out, c.size(), c.c_ptr()); 3344 } 3345 display_mathematicanlsat::solver::imp3346 std::ostream& display_mathematica(std::ostream & out, clause const & c) const { 3347 out << "("; 3348 unsigned sz = c.size(); 3349 for (unsigned i = 0; i < sz; i++) { 3350 if (i > 0) 3351 out << " || "; 3352 display_mathematica(out, c[i]); 3353 } 3354 out << ")"; 3355 return out; 3356 } 3357 3358 // Debugging support: 3359 // Display generated lemma in Mathematica format. 3360 // Mathematica must reduce lemma to True (modulo resource constraints). display_mathematica_lemmanlsat::solver::imp3361 std::ostream& display_mathematica_lemma(std::ostream & out, unsigned num, literal const * ls, bool include_assignment = false) const { 3362 out << "Resolve[ForAll[{"; 3363 // var definition 3364 for (unsigned i = 0; i < num_vars(); i++) { 3365 if (i > 0) 3366 out << ", "; 3367 out << "x" << i; 3368 } 3369 out << "}, "; 3370 if (include_assignment) { 3371 out << "!("; 3372 if (!display_mathematica_assignment(out)) 3373 out << "0 < 1"; // nothing was printed 3374 out << ") || "; 3375 } 3376 for (unsigned i = 0; i < num; i++) { 3377 if (i > 0) 3378 out << " || "; 3379 display_mathematica(out, ls[i]); 3380 } 3381 out << "], Reals]\n"; // end of exists 3382 return out; 3383 } 3384 displaynlsat::solver::imp3385 std::ostream& display(std::ostream & out, clause_vector const & cs, display_var_proc const & proc) const { 3386 for (clause* c : cs) { 3387 display(out, *c, proc) << "\n"; 3388 } 3389 return out; 3390 } 3391 displaynlsat::solver::imp3392 std::ostream& display(std::ostream & out, clause_vector const & cs) const { 3393 return display(out, cs, m_display_var); 3394 } 3395 display_mathematicanlsat::solver::imp3396 std::ostream& display_mathematica(std::ostream & out, clause_vector const & cs) const { 3397 unsigned sz = cs.size(); 3398 for (unsigned i = 0; i < sz; i++) { 3399 if (i > 0) out << ",\n"; 3400 display_mathematica(out << " ", *(cs[i])); 3401 } 3402 return out; 3403 } 3404 display_abstnlsat::solver::imp3405 std::ostream& display_abst(std::ostream & out, clause_vector const & cs) const { 3406 for (clause* c : cs) { 3407 display_abst(out, *c) << "\n"; 3408 } 3409 return out; 3410 } 3411 displaynlsat::solver::imp3412 std::ostream& display(std::ostream & out, display_var_proc const & proc) const { 3413 display(out, m_clauses, proc); 3414 if (!m_learned.empty()) { 3415 display(out << "Lemmas:\n", m_learned, proc); 3416 } 3417 return out; 3418 } 3419 display_mathematicanlsat::solver::imp3420 std::ostream& display_mathematica(std::ostream & out) const { 3421 return display_mathematica(out << "{\n", m_clauses) << "}\n"; 3422 } 3423 display_abstnlsat::solver::imp3424 std::ostream& display_abst(std::ostream & out) const { 3425 display_abst(out, m_clauses); 3426 if (!m_learned.empty()) { 3427 display_abst(out << "Lemmas:\n", m_learned); 3428 } 3429 return out; 3430 } 3431 displaynlsat::solver::imp3432 std::ostream& display(std::ostream & out) const { 3433 display(out, m_display_var); 3434 display_assignment(out << "assignment:\n"); 3435 return out << "---\n"; 3436 } 3437 display_varsnlsat::solver::imp3438 std::ostream& display_vars(std::ostream & out) const { 3439 for (unsigned i = 0; i < num_vars(); i++) { 3440 out << i << " -> "; m_display_var(out, i); out << "\n"; 3441 } 3442 return out; 3443 } 3444 display_smt2_arith_declsnlsat::solver::imp3445 std::ostream& display_smt2_arith_decls(std::ostream & out) const { 3446 unsigned sz = m_is_int.size(); 3447 for (unsigned i = 0; i < sz; i++) { 3448 if (m_is_int[i]) 3449 out << "(declare-fun x" << i << " () Int)\n"; 3450 else 3451 out << "(declare-fun x" << i << " () Real)\n"; 3452 } 3453 return out; 3454 } 3455 display_smt2_bool_declsnlsat::solver::imp3456 std::ostream& display_smt2_bool_decls(std::ostream & out) const { 3457 unsigned sz = m_atoms.size(); 3458 for (unsigned i = 0; i < sz; i++) { 3459 if (m_atoms[i] == nullptr) 3460 out << "(declare-fun b" << i << " () Bool)\n"; 3461 } 3462 return out; 3463 } 3464 display_smt2nlsat::solver::imp3465 std::ostream& display_smt2(std::ostream & out) const { 3466 display_smt2_bool_decls(out); 3467 display_smt2_arith_decls(out); 3468 out << "(assert (and true\n"; 3469 for (clause* c : m_clauses) { 3470 display_smt2(out, *c) << "\n"; 3471 } 3472 out << "))\n" << std::endl; 3473 return out; 3474 } 3475 }; 3476 solver(reslimit & rlim,params_ref const & p,bool incremental)3477 solver::solver(reslimit& rlim, params_ref const & p, bool incremental) { 3478 m_ctx = alloc(ctx, rlim, p, incremental); 3479 m_imp = alloc(imp, *this, *m_ctx); 3480 } 3481 solver(ctx & ctx)3482 solver::solver(ctx& ctx) { 3483 m_ctx = nullptr; 3484 m_imp = alloc(imp, *this, ctx); 3485 } 3486 ~solver()3487 solver::~solver() { 3488 dealloc(m_imp); 3489 dealloc(m_ctx); 3490 } 3491 check()3492 lbool solver::check() { 3493 return m_imp->check(); 3494 } 3495 check(literal_vector & assumptions)3496 lbool solver::check(literal_vector& assumptions) { 3497 return m_imp->check(assumptions); 3498 } 3499 get_core(vector<assumption,false> & assumptions)3500 void solver::get_core(vector<assumption, false>& assumptions) { 3501 return m_imp->get_core(assumptions); 3502 } 3503 reset()3504 void solver::reset() { 3505 m_imp->reset(); 3506 } 3507 3508 updt_params(params_ref const & p)3509 void solver::updt_params(params_ref const & p) { 3510 m_imp->updt_params(p); 3511 } 3512 3513 collect_param_descrs(param_descrs & d)3514 void solver::collect_param_descrs(param_descrs & d) { 3515 algebraic_numbers::manager::collect_param_descrs(d); 3516 nlsat_params::collect_param_descrs(d); 3517 } 3518 qm()3519 unsynch_mpq_manager & solver::qm() { 3520 return m_imp->m_qm; 3521 } 3522 am()3523 anum_manager & solver::am() { 3524 return m_imp->m_am; 3525 } 3526 pm()3527 pmanager & solver::pm() { 3528 return m_imp->m_pm; 3529 } 3530 set_display_var(display_var_proc const & proc)3531 void solver::set_display_var(display_var_proc const & proc) { 3532 m_imp->m_display_var.m_proc = &proc; 3533 } 3534 set_display_assumption(display_assumption_proc const & proc)3535 void solver::set_display_assumption(display_assumption_proc const& proc) { 3536 m_imp->m_display_assumption = &proc; 3537 } 3538 3539 num_vars() const3540 unsigned solver::num_vars() const { 3541 return m_imp->num_vars(); 3542 } 3543 is_int(var x) const3544 bool solver::is_int(var x) const { 3545 return m_imp->is_int(x); 3546 } 3547 mk_bool_var()3548 bool_var solver::mk_bool_var() { 3549 return m_imp->mk_bool_var(); 3550 } 3551 mk_true()3552 literal solver::mk_true() { 3553 return literal(0, false); 3554 } 3555 bool_var2atom(bool_var b)3556 atom * solver::bool_var2atom(bool_var b) { 3557 return m_imp->m_atoms[b]; 3558 } 3559 vars(literal l,var_vector & vs)3560 void solver::vars(literal l, var_vector& vs) { 3561 m_imp->vars(l, vs); 3562 } 3563 get_atoms()3564 atom_vector const& solver::get_atoms() { 3565 return m_imp->m_atoms; 3566 } 3567 get_var2eq()3568 atom_vector const& solver::get_var2eq() { 3569 return m_imp->m_var2eq; 3570 } 3571 get_evaluator()3572 evaluator& solver::get_evaluator() { 3573 return m_imp->m_evaluator; 3574 } 3575 get_explain()3576 explain& solver::get_explain() { 3577 return m_imp->m_explain; 3578 } 3579 reorder(unsigned sz,var const * p)3580 void solver::reorder(unsigned sz, var const* p) { 3581 m_imp->reorder(sz, p); 3582 } 3583 restore_order()3584 void solver::restore_order() { 3585 m_imp->restore_order(); 3586 } 3587 set_rvalues(assignment const & as)3588 void solver::set_rvalues(assignment const& as) { 3589 m_imp->m_assignment.copy(as); 3590 } 3591 get_rvalues(assignment & as)3592 void solver::get_rvalues(assignment& as) { 3593 as.copy(m_imp->m_assignment); 3594 } 3595 get_bvalues(svector<bool_var> const & bvars,svector<lbool> & vs)3596 void solver::get_bvalues(svector<bool_var> const& bvars, svector<lbool>& vs) { 3597 vs.reset(); 3598 for (bool_var b : bvars) { 3599 vs.reserve(b + 1, l_undef); 3600 if (!m_imp->m_atoms[b]) { 3601 vs[b] = m_imp->m_bvalues[b]; 3602 } 3603 } 3604 TRACE("nlsat", display(tout);); 3605 } 3606 set_bvalues(svector<lbool> const & vs)3607 void solver::set_bvalues(svector<lbool> const& vs) { 3608 TRACE("nlsat", display(tout);); 3609 for (bool_var b = 0; b < vs.size(); ++b) { 3610 if (vs[b] != l_undef) { 3611 m_imp->m_bvalues[b] = vs[b]; 3612 SASSERT(!m_imp->m_atoms[b]); 3613 } 3614 } 3615 #if 0 3616 m_imp->m_bvalues.reset(); 3617 m_imp->m_bvalues.append(vs); 3618 m_imp->m_bvalues.resize(m_imp->m_atoms.size(), l_undef); 3619 for (unsigned i = 0; i < m_imp->m_atoms.size(); ++i) { 3620 atom* a = m_imp->m_atoms[i]; 3621 SASSERT(!a); 3622 if (a) { 3623 m_imp->m_bvalues[i] = to_lbool(m_imp->m_evaluator.eval(a, false)); 3624 } 3625 } 3626 #endif 3627 TRACE("nlsat", display(tout);); 3628 } 3629 mk_var(bool is_int)3630 var solver::mk_var(bool is_int) { 3631 return m_imp->mk_var(is_int); 3632 } 3633 mk_ineq_atom(atom::kind k,unsigned sz,poly * const * ps,bool const * is_even)3634 bool_var solver::mk_ineq_atom(atom::kind k, unsigned sz, poly * const * ps, bool const * is_even) { 3635 return m_imp->mk_ineq_atom(k, sz, ps, is_even); 3636 } 3637 mk_ineq_literal(atom::kind k,unsigned sz,poly * const * ps,bool const * is_even)3638 literal solver::mk_ineq_literal(atom::kind k, unsigned sz, poly * const * ps, bool const * is_even) { 3639 return m_imp->mk_ineq_literal(k, sz, ps, is_even); 3640 } 3641 mk_root_atom(atom::kind k,var x,unsigned i,poly * p)3642 bool_var solver::mk_root_atom(atom::kind k, var x, unsigned i, poly * p) { 3643 return m_imp->mk_root_atom(k, x, i, p); 3644 } 3645 inc_ref(bool_var b)3646 void solver::inc_ref(bool_var b) { 3647 m_imp->inc_ref(b); 3648 } 3649 dec_ref(bool_var b)3650 void solver::dec_ref(bool_var b) { 3651 m_imp->dec_ref(b); 3652 } 3653 mk_clause(unsigned num_lits,literal * lits,assumption a)3654 void solver::mk_clause(unsigned num_lits, literal * lits, assumption a) { 3655 return m_imp->mk_clause(num_lits, lits, a); 3656 } 3657 display(std::ostream & out) const3658 std::ostream& solver::display(std::ostream & out) const { 3659 return m_imp->display(out); 3660 } 3661 display(std::ostream & out,literal l) const3662 std::ostream& solver::display(std::ostream & out, literal l) const { 3663 return m_imp->display(out, l); 3664 } 3665 display(std::ostream & out,unsigned n,literal const * ls) const3666 std::ostream& solver::display(std::ostream & out, unsigned n, literal const* ls) const { 3667 for (unsigned i = 0; i < n; ++i) { 3668 display(out, ls[i]); 3669 out << "; "; 3670 } 3671 return out; 3672 } 3673 display(std::ostream & out,literal_vector const & ls) const3674 std::ostream& solver::display(std::ostream & out, literal_vector const& ls) const { 3675 return display(out, ls.size(), ls.c_ptr()); 3676 } 3677 display_smt2(std::ostream & out,literal l) const3678 std::ostream& solver::display_smt2(std::ostream & out, literal l) const { 3679 return m_imp->display_smt2(out, l); 3680 } 3681 display_smt2(std::ostream & out,unsigned n,literal const * ls) const3682 std::ostream& solver::display_smt2(std::ostream & out, unsigned n, literal const* ls) const { 3683 for (unsigned i = 0; i < n; ++i) { 3684 display_smt2(out, ls[i]); 3685 out << " "; 3686 } 3687 return out; 3688 } 3689 display_smt2(std::ostream & out,literal_vector const & ls) const3690 std::ostream& solver::display_smt2(std::ostream & out, literal_vector const& ls) const { 3691 return display_smt2(out, ls.size(), ls.c_ptr()); 3692 } 3693 display(std::ostream & out,var x) const3694 std::ostream& solver::display(std::ostream & out, var x) const { 3695 return m_imp->m_display_var(out, x); 3696 } 3697 display(std::ostream & out,atom const & a) const3698 std::ostream& solver::display(std::ostream & out, atom const& a) const { 3699 return m_imp->display(out, a, m_imp->m_display_var); 3700 } 3701 display_proc() const3702 display_var_proc const & solver::display_proc() const { 3703 return m_imp->m_display_var; 3704 } 3705 value(var x) const3706 anum const & solver::value(var x) const { 3707 if (m_imp->m_assignment.is_assigned(x)) 3708 return m_imp->m_assignment.value(x); 3709 return m_imp->m_zero; 3710 } 3711 bvalue(bool_var b) const3712 lbool solver::bvalue(bool_var b) const { 3713 return m_imp->m_bvalues[b]; 3714 } 3715 value(literal l) const3716 lbool solver::value(literal l) const { 3717 return m_imp->value(l); 3718 } 3719 is_interpreted(bool_var b) const3720 bool solver::is_interpreted(bool_var b) const { 3721 return m_imp->m_atoms[b] != 0; 3722 } 3723 reset_statistics()3724 void solver::reset_statistics() { 3725 return m_imp->reset_statistics(); 3726 } 3727 collect_statistics(statistics & st)3728 void solver::collect_statistics(statistics & st) { 3729 return m_imp->collect_statistics(st); 3730 } 3731 3732 3733 }; 3734