1 /*++ 2 Copyright (c) 2006 Microsoft Corporation 3 4 Module Name: 5 6 smt_consequences.cpp 7 8 Abstract: 9 10 Tuned consequence finding for smt_context. 11 12 Author: 13 14 nbjorner 2016-07-28. 15 16 Revision History: 17 18 --*/ 19 #include "util/max_cliques.h" 20 #include "util/stopwatch.h" 21 #include "ast/ast_util.h" 22 #include "ast/ast_pp.h" 23 #include "ast/datatype_decl_plugin.h" 24 #include "model/model_pp.h" 25 #include "smt/smt_context.h" 26 27 namespace smt { 28 antecedent2fml(index_set const & vars)29 expr_ref context::antecedent2fml(index_set const& vars) { 30 expr_ref_vector premises(m); 31 for (unsigned v : vars) { 32 expr* e; 33 if (m_assumption2orig.find(v, e)) { 34 premises.push_back(get_assignment(v) != l_false ? e : m.mk_not(e)); 35 } 36 } 37 return mk_and(premises); 38 } 39 40 // 41 // The literal lit is assigned at the search level, so it follows from the assumptions. 42 // We retrieve the set of assumptions it depends on in the set 's'. 43 // The map m_antecedents contains the association from these literals to the assumptions they depend on. 44 // We then examine the contents of the literal lit and augment the set of consequences in one of the following cases: 45 // - e is a propositional atom and it is one of the variables that is to be fixed. 46 // - e is an equality between a variable and value that is to be fixed. 47 // - e is a data-type recognizer of a variable that is to be fixed. 48 // extract_fixed_consequences(literal lit,index_set const & assumptions,expr_ref_vector & conseq)49 void context::extract_fixed_consequences(literal lit, index_set const& assumptions, expr_ref_vector& conseq) { 50 datatype_util dt(m); 51 expr* e1, *e2, *arg; 52 expr_ref fml(m); 53 if (lit == true_literal) return; 54 expr* e = bool_var2expr(lit.var()); 55 TRACE("context", tout << mk_pp(e, m) << "\n";); 56 index_set s; 57 if (assumptions.contains(lit.var())) { 58 s.insert(lit.var()); 59 } 60 else { 61 justify(lit, s); 62 } 63 m_antecedents.insert(lit.var(), s); 64 bool found = false; 65 if (m_var2val.contains(e)) { 66 found = true; 67 m_var2val.erase(e); 68 e = m_var2orig.find(e); 69 fml = lit.sign() ? m.mk_not(e) : e; 70 } 71 else if (!lit.sign() && m.is_eq(e, e1, e2)) { 72 if (m_var2val.contains(e2) && m.is_value(e1)) { 73 found = true; 74 m_var2val.erase(e2); 75 e2 = m_var2orig.find(e2); 76 std::swap(e1, e2); 77 fml = m.mk_eq(e1, e2); 78 } 79 else if (m_var2val.contains(e1) && m.is_value(e2)) { 80 found = true; 81 m_var2val.erase(e1); 82 e1 = m_var2orig.find(e1); 83 fml = m.mk_eq(e1, e2); 84 } 85 } 86 else if (!lit.sign() && dt.is_recognizer(e, arg)) { 87 if (m_var2val.contains(arg)) { 88 found = true; 89 fml = m.mk_eq(arg, m.mk_const(dt.get_recognizer_constructor(to_app(e)->get_decl()))); 90 m_var2val.erase(arg); 91 } 92 } 93 if (found) { 94 fml = m.mk_implies(antecedent2fml(s), fml); 95 conseq.push_back(fml); 96 } 97 } 98 justify(literal lit,index_set & s)99 void context::justify(literal lit, index_set& s) { 100 (void)m; 101 auto add_antecedent = [&](literal l) { 102 CTRACE("context", !m_antecedents.contains(l.var()), 103 tout << "untracked literal: " << l << " " 104 << mk_pp(bool_var2expr(l.var()), m) << "\n";); 105 if (m_antecedents.contains(l.var())) { 106 s |= m_antecedents[l.var()]; 107 } 108 }; 109 b_justification js = get_justification(lit.var()); 110 switch (js.get_kind()) { 111 case b_justification::CLAUSE: { 112 clause * cls = js.get_clause(); 113 if (!cls) break; 114 for (literal lit2 : *cls) { 115 if (lit2.var() != lit.var()) { 116 add_antecedent(lit2); 117 } 118 } 119 break; 120 } 121 case b_justification::BIN_CLAUSE: { 122 add_antecedent(js.get_literal()); 123 break; 124 } 125 case b_justification::AXIOM: { 126 break; 127 } 128 case b_justification::JUSTIFICATION: { 129 literal_vector literals; 130 m_conflict_resolution->justification2literals(js.get_justification(), literals); 131 for (unsigned j = 0; j < literals.size(); ++j) { 132 add_antecedent(literals[j]); 133 } 134 break; 135 } 136 } 137 } 138 extract_fixed_consequences(unsigned & start,index_set const & assumptions,expr_ref_vector & conseq)139 void context::extract_fixed_consequences(unsigned& start, index_set const& assumptions, expr_ref_vector& conseq) { 140 pop_to_search_lvl(); 141 SASSERT(!inconsistent()); 142 literal_vector const& lits = assigned_literals(); 143 unsigned sz = lits.size(); 144 for (unsigned i = start; i < sz; ++i) { 145 extract_fixed_consequences(lits[i], assumptions, conseq); 146 } 147 start = sz; 148 SASSERT(!inconsistent()); 149 } 150 151 152 // 153 // The assignment stack is assumed consistent. 154 // For each Boolean variable, we check if there is a literal assigned to the 155 // opposite value of the reference model, and for non-Boolean variables we 156 // check if the current state forces the variable to be distinct from the reference value. 157 // 158 // For yet to be determined Boolean variables we furthermore force the phase to be opposite 159 // to the reference value in the attempt to let the sat engine emerge with a model that 160 // rules out as many non-fixed variables as possible. 161 // 162 delete_unfixed(expr_ref_vector & unfixed)163 unsigned context::delete_unfixed(expr_ref_vector& unfixed) { 164 ptr_vector<expr> to_delete; 165 for (auto const& kv : m_var2val) { 166 expr* k = kv.m_key; 167 expr* v = kv.m_value; 168 if (m.is_bool(k)) { 169 literal lit = get_literal(k); 170 TRACE("context", 171 tout << "checking " << mk_pp(k, m) << " " 172 << mk_pp(v, m) << " " << get_assignment(lit) << "\n"; 173 display(tout); 174 ); 175 switch (get_assignment(lit)) { 176 case l_true: 177 if (m.is_false(v)) { 178 to_delete.push_back(k); 179 } 180 else { 181 force_phase(lit.var(), false); 182 } 183 break; 184 case l_false: 185 if (m.is_true(v)) { 186 to_delete.push_back(k); 187 } 188 else { 189 force_phase(lit.var(), true); 190 } 191 break; 192 default: 193 to_delete.push_back(k); 194 break; 195 } 196 } 197 else if (e_internalized(k) && m.are_distinct(v, get_enode(k)->get_root()->get_owner())) { 198 to_delete.push_back(k); 199 } 200 else if (get_assignment(mk_diseq(k, v)) == l_true) { 201 to_delete.push_back(k); 202 } 203 } 204 for (expr* e : to_delete) { 205 m_var2val.remove(e); 206 unfixed.push_back(e); 207 } 208 return to_delete.size(); 209 } 210 211 // 212 // Extract equalities that are congruent at the search level. 213 // Add a clause to short-circuit the congruence justifications for 214 // next rounds. 215 // extract_fixed_eqs(expr_ref_vector & conseq)216 unsigned context::extract_fixed_eqs(expr_ref_vector& conseq) { 217 TRACE("context", tout << "extract fixed consequences\n";); 218 auto are_equal = [&](expr* k, expr* v) { 219 return e_internalized(k) && 220 e_internalized(v) && 221 get_enode(k)->get_root() == get_enode(v)->get_root(); 222 }; 223 ptr_vector<expr> to_delete; 224 expr_ref fml(m), eq(m); 225 for (auto const& kv : m_var2val) { 226 expr* k = kv.m_key; 227 expr* v = kv.m_value; 228 if (!m.is_bool(k) && are_equal(k, v)) { 229 literal_vector literals; 230 m_conflict_resolution->eq2literals(get_enode(v), get_enode(k), literals); 231 index_set s; 232 for (literal lit : literals) { 233 SASSERT(get_assign_level(lit) <= get_search_level()); 234 s |= m_antecedents.find(lit.var()); 235 } 236 237 fml = m.mk_eq(m_var2orig.find(k), v); 238 fml = m.mk_implies(antecedent2fml(s), fml); 239 conseq.push_back(fml); 240 to_delete.push_back(k); 241 242 for (literal& lit : literals) 243 lit.neg(); 244 245 literal lit = mk_diseq(k, v); 246 literals.push_back(lit); 247 mk_clause(literals.size(), literals.c_ptr(), nullptr); 248 TRACE("context", display_literals_verbose(tout, literals.size(), literals.c_ptr());); 249 } 250 } 251 for (expr* e : to_delete) { 252 m_var2val.remove(e); 253 } 254 return to_delete.size(); 255 } 256 mk_diseq(expr * e,expr * val)257 literal context::mk_diseq(expr* e, expr* val) { 258 if (m.is_bool(e) && b_internalized(e)) { 259 return literal(get_bool_var(e), m.is_true(val)); 260 } 261 else if (m.is_bool(e)) { 262 internalize_formula(e, false); 263 return literal(get_bool_var(e), !m.is_true(val)); 264 } 265 else { 266 expr_ref eq(mk_eq_atom(e, val), m); 267 internalize_formula(eq, false); 268 return literal(get_bool_var(eq), true); 269 } 270 } 271 get_consequences(expr_ref_vector const & assumptions0,expr_ref_vector const & vars0,expr_ref_vector & conseq,expr_ref_vector & unfixed)272 lbool context::get_consequences(expr_ref_vector const& assumptions0, 273 expr_ref_vector const& vars0, 274 expr_ref_vector& conseq, 275 expr_ref_vector& unfixed) { 276 277 m_antecedents.reset(); 278 m_antecedents.insert(true_literal.var(), index_set()); 279 pop_to_base_lvl(); 280 expr_ref_vector vars(m), assumptions(m); 281 index_set _assumptions; 282 m_var2val.reset(); 283 m_var2orig.reset(); 284 m_assumption2orig.reset(); 285 bool pushed = false; 286 struct scoped_level { 287 context& c; 288 bool& pushed; 289 unsigned lvl; 290 scoped_level(context& c, bool& pushed): 291 c(c), pushed(pushed), lvl(c.get_scope_level()) {} 292 ~scoped_level() { 293 if (c.get_scope_level() > lvl + pushed) 294 c.pop_scope(c.get_scope_level() - lvl - pushed); 295 if (pushed) 296 c.pop(1); 297 } 298 }; 299 scoped_level _lvl(*this, pushed); 300 301 for (expr* v : vars0) { 302 if (is_uninterp_const(v)) { 303 vars.push_back(v); 304 m_var2orig.insert(v, v); 305 } 306 else { 307 if (!pushed) pushed = true, push(); 308 expr_ref c(m.mk_fresh_const("v", m.get_sort(v)), m); 309 expr_ref eq(m.mk_eq(c, v), m); 310 assert_expr(eq); 311 vars.push_back(c); 312 m_var2orig.insert(c, v); 313 } 314 } 315 for (expr* a : assumptions0) { 316 if (is_uninterp_const(a)) { 317 assumptions.push_back(a); 318 } 319 else { 320 if (!pushed) pushed = true, push(); 321 expr_ref c(m.mk_fresh_const("a", m.get_sort(a)), m); 322 expr_ref eq(m.mk_eq(c, a), m); 323 assert_expr(eq); 324 assumptions.push_back(c); 325 } 326 expr* e = assumptions.back(); 327 if (!e_internalized(e)) internalize(e, false); 328 literal lit = get_literal(e); 329 _assumptions.insert(lit.var()); 330 m_assumption2orig.insert(lit.var(), a); 331 } 332 333 lbool is_sat = check(assumptions.size(), assumptions.c_ptr()); 334 335 if (is_sat != l_true) { 336 TRACE("context", tout << is_sat << "\n";); 337 return is_sat; 338 } 339 if (m_qmanager->has_quantifiers()) { 340 IF_VERBOSE(1, verbose_stream() << "(get-consequences :unsupported-quantifiers)\n";); 341 return l_undef; 342 } 343 344 TRACE("context", display(tout);); 345 346 model_ref mdl; 347 get_model(mdl); 348 expr_ref_vector trail(m); 349 model_evaluator eval(*mdl.get()); 350 expr_ref val(m); 351 TRACE("context", model_pp(tout, *mdl);); 352 for (expr* v : vars) { 353 eval(v, val); 354 if (m.is_value(val)) { 355 trail.push_back(val); 356 m_var2val.insert(v, val); 357 } 358 else { 359 unfixed.push_back(v); 360 } 361 } 362 unsigned num_units = 0; 363 extract_fixed_consequences(num_units, _assumptions, conseq); 364 app_ref eq(m); 365 TRACE("context", 366 tout << "vars: " << vars.size() << "\n"; 367 tout << "lits: " << num_units << "\n";); 368 pop_to_base_lvl(); 369 m_case_split_queue->init_search_eh(); 370 unsigned num_iterations = 0; 371 unsigned num_fixed_eqs = 0; 372 unsigned chunk_size = 100; 373 374 init_assumptions(assumptions); 375 num_units = 0; 376 377 while (!m_var2val.empty()) { 378 unsigned num_vars = 0; 379 for (auto const& kv : m_var2val) { 380 if (num_vars >= chunk_size) 381 break; 382 if (get_cancel_flag()) { 383 return l_undef; 384 } 385 expr* e = kv.m_key; 386 expr* val = kv.m_value; 387 literal lit = mk_diseq(e, val); 388 mark_as_relevant(lit); 389 if (get_assignment(lit) != l_undef) { 390 continue; 391 } 392 ++num_vars; 393 push_scope(); 394 assign(lit, b_justification::mk_axiom(), true); 395 while (can_propagate()) { 396 if (propagate()) 397 break; 398 if (resolve_conflict()) 399 continue; 400 if (inconsistent()) { 401 SASSERT(inconsistent()); 402 IF_VERBOSE(1, verbose_stream() << "(get-consequences base-inconsistent " << get_scope_level() << ")\n"); 403 return l_undef; 404 } 405 } 406 } 407 SASSERT(!inconsistent()); 408 ++num_iterations; 409 410 lbool is_sat = l_undef; 411 while (true) { 412 is_sat = bounded_search(); 413 if (is_sat != l_true && m_last_search_failure != OK) { 414 return is_sat; 415 } 416 if (is_sat == l_undef) { 417 IF_VERBOSE(1, verbose_stream() << "(get-consequences inc-limits)\n";); 418 inc_limits(); 419 continue; 420 } 421 break; 422 } 423 if (is_sat == l_false) { 424 SASSERT(inconsistent()); 425 m_conflict = null_b_justification; 426 m_not_l = null_literal; 427 } 428 if (is_sat == l_true) { 429 TRACE("context", display(tout);); 430 delete_unfixed(unfixed); 431 } 432 extract_fixed_consequences(num_units, _assumptions, conseq); 433 num_fixed_eqs += extract_fixed_eqs(conseq); 434 IF_VERBOSE(1, display_consequence_progress(verbose_stream(), num_iterations, m_var2val.size(), conseq.size(), 435 unfixed.size(), num_fixed_eqs);); 436 TRACE("context", display_consequence_progress(tout, num_iterations, m_var2val.size(), conseq.size(), 437 unfixed.size(), num_fixed_eqs);); 438 } 439 440 end_search(); 441 DEBUG_CODE(validate_consequences(assumptions, vars, conseq, unfixed);); 442 return l_true; 443 } 444 445 display_consequence_progress(std::ostream & out,unsigned it,unsigned nv,unsigned fixed,unsigned unfixed,unsigned eq)446 void context::display_consequence_progress(std::ostream& out, unsigned it, unsigned nv, unsigned fixed, unsigned unfixed, unsigned eq) { 447 out << "(get-consequences" 448 << " iterations: " << it 449 << " variables: " << nv 450 << " fixed: " << fixed 451 << " unfixed: " << unfixed 452 << " fixed-eqs: " << eq 453 << ")\n"; 454 } 455 extract_cores(expr_ref_vector const & asms,vector<expr_ref_vector> & cores,unsigned & min_core_size)456 void context::extract_cores(expr_ref_vector const& asms, vector<expr_ref_vector>& cores, unsigned& min_core_size) { 457 index_set _asms, _nasms; 458 u_map<expr*> var2expr; 459 for (unsigned i = 0; i < asms.size(); ++i) { 460 literal lit = get_literal(asms[i]); 461 _asms.insert(lit.index()); 462 _nasms.insert((~lit).index()); 463 var2expr.insert(lit.var(), asms[i]); 464 } 465 466 m_antecedents.reset(); 467 for (literal lit : assigned_literals()) { 468 index_set s; 469 if (_asms.contains(lit.index())) { 470 s.insert(lit.var()); 471 } 472 else { 473 justify(lit, s); 474 } 475 m_antecedents.insert(lit.var(), s); 476 if (_nasms.contains(lit.index())) { 477 expr_ref_vector core(m); 478 for (auto v : s) 479 core.push_back(var2expr[v]); 480 core.push_back(var2expr[lit.var()]); 481 cores.push_back(core); 482 min_core_size = std::min(min_core_size, core.size()); 483 } 484 } 485 } 486 preferred_sat(literal_vector & lits)487 void context::preferred_sat(literal_vector& lits) { 488 bool retry = true; 489 while (retry) { 490 retry = false; 491 for (unsigned i = 0; i < lits.size(); ++i) { 492 literal lit = lits[i]; 493 if (lit == null_literal || get_assignment(lit) != l_undef) { 494 continue; 495 } 496 push_scope(); 497 assign(lit, b_justification::mk_axiom(), true); 498 while (!propagate()) { 499 lits[i] = null_literal; 500 retry = true; 501 if (!resolve_conflict() || inconsistent()) { 502 SASSERT(inconsistent()); 503 return; 504 } 505 } 506 } 507 } 508 } 509 display_partial_assignment(std::ostream & out,expr_ref_vector const & asms,unsigned min_core_size)510 void context::display_partial_assignment(std::ostream& out, expr_ref_vector const& asms, unsigned min_core_size) { 511 unsigned num_true = 0, num_false = 0, num_undef = 0; 512 for (unsigned i = 0; i < asms.size(); ++i) { 513 literal lit = get_literal(asms[i]); 514 if (get_assignment(lit) == l_false) { 515 ++num_false; 516 } 517 if (get_assignment(lit) == l_true) { 518 ++num_true; 519 } 520 if (get_assignment(lit) == l_undef) { 521 ++num_undef; 522 } 523 } 524 out << "(smt.preferred-sat true: " << num_true << " false: " << num_false << " undef: " << num_undef << " min core: " << min_core_size << ")\n"; 525 } 526 preferred_sat(expr_ref_vector const & asms,vector<expr_ref_vector> & cores)527 lbool context::preferred_sat(expr_ref_vector const& asms, vector<expr_ref_vector>& cores) { 528 pop_to_base_lvl(); 529 cores.reset(); 530 setup_context(false); 531 internalize_assertions(); 532 if (m_asserted_formulas.inconsistent() || inconsistent()) { 533 return l_false; 534 } 535 reset_model(); 536 init_search(); 537 flet<bool> l(m_searching, true); 538 unsigned level = m_scope_lvl; 539 unsigned min_core_size = UINT_MAX; 540 lbool is_sat = l_true; 541 unsigned num_restarts = 0; 542 543 while (true) { 544 if (!m.inc()) { 545 is_sat = l_undef; 546 break; 547 } 548 literal_vector lits; 549 for (unsigned i = 0; i < asms.size(); ++i) { 550 lits.push_back(get_literal(asms[i])); 551 } 552 preferred_sat(lits); 553 if (inconsistent()) { 554 SASSERT(m_scope_lvl == level); 555 is_sat = l_false; 556 break; 557 } 558 extract_cores(asms, cores, min_core_size); 559 IF_VERBOSE(1, display_partial_assignment(verbose_stream(), asms, min_core_size);); 560 561 if (min_core_size <= 10) { 562 is_sat = l_undef; 563 break; 564 } 565 566 is_sat = bounded_search(); 567 if (!restart(is_sat, level)) { 568 break; 569 } 570 ++num_restarts; 571 if (num_restarts >= min_core_size) { 572 is_sat = l_undef; 573 while (num_restarts <= 10*min_core_size) { 574 is_sat = bounded_search(); 575 if (!restart(is_sat, level)) { 576 break; 577 } 578 ++num_restarts; 579 } 580 break; 581 } 582 } 583 end_search(); 584 585 return check_finalize(is_sat); 586 } 587 588 struct neg_literal { negatesmt::neg_literal589 unsigned negate(unsigned i) { 590 return (~to_literal(i)).index(); 591 } 592 }; 593 find_mutexes(expr_ref_vector const & vars,vector<expr_ref_vector> & mutexes)594 lbool context::find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) { 595 unsigned_vector ps; 596 max_cliques<neg_literal> mc; 597 expr_ref lit(m); 598 for (expr* n : vars) { 599 bool neg = m.is_not(n, n); 600 if (b_internalized(n)) { 601 ps.push_back(literal(get_bool_var(n), neg).index()); 602 } 603 } 604 for (unsigned i = 0; i < m_watches.size(); ++i) { 605 watch_list & w = m_watches[i]; 606 for (literal const* it = w.begin_literals(), *end = w.end_literals(); it != end; ++it) { 607 unsigned idx1 = (~to_literal(i)).index(); 608 unsigned idx2 = it->index(); 609 if (idx1 < idx2) { 610 mc.add_edge(idx1, idx2); 611 } 612 } 613 } 614 vector<unsigned_vector> _mutexes; 615 mc.cliques(ps, _mutexes); 616 for (auto const& mux : _mutexes) { 617 expr_ref_vector lits(m); 618 for (unsigned idx : mux) { 619 literal2expr(to_literal(idx), lit); 620 lits.push_back(lit); 621 } 622 mutexes.push_back(lits); 623 } 624 return l_true; 625 } 626 627 // 628 // Validate, in a slow pass, that the current consequences are correctly 629 // extracted. 630 // validate_consequences(expr_ref_vector const & assumptions,expr_ref_vector const & vars,expr_ref_vector const & conseq,expr_ref_vector const & unfixed)631 void context::validate_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, 632 expr_ref_vector const& conseq, expr_ref_vector const& unfixed) { 633 m_fparams.m_threads = 1; 634 expr_ref tmp(m); 635 SASSERT(!inconsistent()); 636 for (expr* c : conseq) { 637 push(); 638 for (expr* a : assumptions) { 639 assert_expr(a); 640 } 641 TRACE("context", tout << "checking fixed: " << mk_pp(c, m) << "\n";); 642 tmp = m.mk_not(c); 643 assert_expr(tmp); 644 VERIFY(check() != l_true); 645 pop(1); 646 } 647 model_ref mdl; 648 for (expr* uf : unfixed) { 649 push(); 650 for (expr* a : assumptions) 651 assert_expr(a); 652 TRACE("context", tout << "checking unfixed: " << mk_pp(uf, m) << "\n";); 653 lbool is_sat = check(); 654 SASSERT(is_sat != l_false); 655 if (is_sat == l_true) { 656 get_model(mdl); 657 tmp = (*mdl)(uf); 658 if (m.is_value(tmp)) { 659 tmp = m.mk_not(m.mk_eq(uf, tmp)); 660 assert_expr(tmp); 661 is_sat = check(); 662 SASSERT(is_sat != l_false); 663 } 664 } 665 pop(1); 666 } 667 } 668 669 } 670