From dc48008d4654e0d1c966519c18f0d48f1761770b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 2 Sep 2016 11:00:40 +0800 Subject: [PATCH] fixestoconsequences Signed-off-by: Nikolaj Bjorner --- src/smt/smt_consequences.cpp | 106 +++++++++++++++++++++++++++++++---- src/smt/smt_context.cpp | 9 ++- src/smt/smt_context.h | 2 +- 3 files changed, 103 insertions(+), 14 deletions(-) diff --git a/src/smt/smt_consequences.cpp b/src/smt/smt_consequences.cpp index 8aa83e407..9e026760c 100644 --- a/src/smt/smt_consequences.cpp +++ b/src/smt/smt_consequences.cpp @@ -19,6 +19,7 @@ Revision History: #include "smt_context.h" #include "ast_util.h" #include "datatype_decl_plugin.h" +#include "model_pp.h" namespace smt { @@ -32,6 +33,15 @@ namespace smt { return mk_and(premises); } + // + // The literal lit is assigned at the search level, so it follows from the assumptions. + // We retrieve the set of assumptions it depends on in the set 's'. + // The map m_antecedents contains the association from these literals to the assumptions they depend on. + // We then examine the contents of the literal lit and augment the set of consequences in one of the following cases: + // - e is a propositional atom and it is one of the variables that is to be fixed. + // - e is an equality between a variable and value that is to be fixed. + // - e is a data-type recognizer of a variable that is to be fixed. + // void context::extract_fixed_consequences(literal lit, obj_map& vars, uint_set const& assumptions, expr_ref_vector& conseq) { ast_manager& m = m_manager; datatype_util dt(m); @@ -48,6 +58,7 @@ namespace smt { switch (js.get_kind()) { case b_justification::CLAUSE: { clause * cls = js.get_clause(); + if (!cls) break; unsigned num_lits = cls->get_num_literals(); for (unsigned j = 0; j < num_lits; ++j) { literal lit2 = cls->get_literal(j); @@ -115,6 +126,18 @@ namespace smt { } SASSERT(!inconsistent()); } + + + // + // The assignment stack is assumed consistent. + // For each Boolean variable, we check if there is a literal assigned to the + // opposite value of the reference model, and for non-Boolean variables we + // check if the current state forces the variable to be distinct from the reference value. + // + // For yet to be determined Boolean variables we furthermore force the phase to be opposite + // to the reference value in the attempt to let the sat engine emerge with a model that + // rules out as many non-fixed variables as possible. + // unsigned context::delete_unfixed(obj_map& var2val, expr_ref_vector& unfixed) { ast_manager& m = m_manager; @@ -158,8 +181,12 @@ namespace smt { return to_delete.size(); } +#define are_equal(v, k) (e_internalized(k) && e_internalized(v) && get_enode(k)->get_root() == get_enode(v)->get_root()) + // // Extract equalities that are congruent at the search level. + // Add a clause to short-circuit the congruence justifications for + // next rounds. // unsigned context::extract_fixed_eqs(obj_map& var2val, expr_ref_vector& conseq) { TRACE("context", tout << "extract fixed consequences\n";); @@ -170,8 +197,7 @@ namespace smt { for (; it != end; ++it) { expr* k = it->m_key; expr* v = it->m_value; - if (!m.is_bool(k) && e_internalized(k) && e_internalized(v) && - get_enode(k)->get_root() == get_enode(v)->get_root()) { + if (!m.is_bool(k) && are_equal(k, v)) { literal_vector literals; m_conflict_resolution->eq2literals(get_enode(v), get_enode(k), literals); uint_set s; @@ -208,6 +234,7 @@ namespace smt { expr_ref_vector& unfixed) { m_antecedents.reset(); + pop_to_base_lvl(); lbool is_sat = check(assumptions.size(), assumptions.c_ptr()); if (is_sat != l_true) { return is_sat; @@ -223,6 +250,7 @@ namespace smt { expr_ref_vector trail(m); model_evaluator eval(*mdl.get()); expr_ref val(m); + TRACE("context", model_pp(tout, *mdl);); for (unsigned i = 0; i < vars.size(); ++i) { eval(vars[i], val); if (m.is_value(val)) { @@ -249,23 +277,39 @@ namespace smt { obj_map::iterator it = var2val.begin(); expr* e = it->m_key; expr* val = it->m_value; - push_scope(); TRACE("context", tout << "scope level: " << get_scope_level() << "\n";); SASSERT(!inconsistent()); + // + // The current variable is checked to be a backbone + // We add the negation of the reference assignment to the variable. + // If the variable is a Boolean, it means adding literal that has + // the opposite value of the current reference model. + // If the variable is a non-Boolean, it means adding a disequality. + // literal lit; if (m.is_bool(e)) { lit = literal(get_bool_var(e), m.is_true(val)); } else { - TRACE("context", tout << mk_pp(e, m) << " " << mk_pp(val, m) << "\n";); eq = mk_eq_atom(e, val); internalize_formula(eq, false); lit = literal(get_bool_var(eq), true); + TRACE("context", tout << mk_pp(e, m) << " " << mk_pp(val, m) << "\n"; + display_literal_verbose(tout, lit); tout << "\n"; + tout << "Equal: " << are_equal(e, val) << "\n";); } + mark_as_relevant(lit); + push_scope(); assign(lit, b_justification::mk_axiom(), true); flet l(m_searching, true); + + // + // We check if the current assignment stack can be extended to a + // satisfying assignment. bounded search may decide to restart, + // in which case it returns l_undef and clears search failure. + // while (true) { is_sat = bounded_search(); TRACE("context", tout << "search result: " << is_sat << "\n";); @@ -279,21 +323,41 @@ namespace smt { } break; } - if (is_sat == l_true && get_assignment(lit) == l_true) { + // + // If the state is satisfiable with the current variable assigned to + // a different value from the reference model, it is unfixed. + // + // If it is assigned above the search level we can't conclude anything + // about its value. + // extract_fixed_consequences pops the assignment stack to the search level + // so this sets up the state to retry finding fixed values. + // + // Otherwise, the variable is fixed. + // - it is either assigned at the search level to l_false, or + // - the state is l_false, which means that the variable is fixed by + // the background constraints (and does not depend on assumptions). + // + if (is_sat == l_true && get_assignment(lit) == l_true && is_relevant(lit)) { var2val.erase(e); unfixed.push_back(e); - TRACE("context", tout << mk_pp(e, m) << " is unfixed\n";); + SASSERT(!are_equal(e, val)); + TRACE("context", tout << mk_pp(e, m) << " is unfixed\n"; + display_literal_verbose(tout, lit); tout << "\n"; + tout << "relevant: " << is_relevant(lit) << "\n"; + display(tout);); } - else if (is_sat == l_true && get_assign_level(lit) > get_search_level()) { + else if (is_sat == l_true && (get_assign_level(lit) > get_search_level() || !is_relevant(lit))) { TRACE("context", tout << "Retry fixing: " << mk_pp(e, m) << "\n";); extract_fixed_consequences(num_units, var2val, _assumptions, conseq); ++num_reiterations; continue; } else { + // // The state can be labeled as inconsistent when the implied consequence does // not depend on assumptions, then the conflict level sits at the search level // which causes the conflict resolver to decide that the state is unsat. + // if (l_false == is_sat) { SASSERT(inconsistent()); m_conflict = null_b_justification; @@ -305,6 +369,11 @@ namespace smt { } ++num_iterations; + // + // Check the slow pass: it retrieves an updated model and checks if the + // values in the updated model differ from the values in the reference + // model. + // bool apply_slow_pass = model_threshold <= num_iterations || num_iterations <= 2; if (apply_slow_pass && is_sat == l_true) { num_unfixed += delete_unfixed(var2val, unfixed); @@ -312,11 +381,20 @@ namespace smt { model_threshold *= 3; model_threshold /= 2; } - // repeat until we either have a model with negated literal or - // the literal is implied at base. + // + // Walk the assignment stack at level 1 for learned consequences. + // The current literal should be assigned at the search level unless + // the state is is_sat == l_true and the assignment to lit is l_true. + // This condition is checked above. + // extract_fixed_consequences(num_units, var2val, _assumptions, conseq); num_units = assigned_literals().size(); + + // + // Fixed equalities can be extracted by walking all variables and checking + // if the congruence roots are equal at the search level. + // if (apply_slow_pass) { num_fixed_eqs += extract_fixed_eqs(var2val, conseq); IF_VERBOSE(1, verbose_stream() << "(get-consequences" @@ -338,6 +416,11 @@ namespace smt { } TRACE("context", tout << "finishing " << mk_pp(e, m) << "\n";); SASSERT(!inconsistent()); + + // + // This becomes unnecessary when the fixed consequence are + // completely extracted. + // if (var2val.contains(e)) { TRACE("context", tout << "Fixed value to " << mk_pp(e, m) << " was not processed\n";); expr_ref fml(m); @@ -348,7 +431,6 @@ namespace smt { fml = m.mk_implies(antecedent2fml(m_antecedents[lit.var()]), fml); conseq.push_back(fml); var2val.erase(e); - SASSERT(get_assignment(lit) == l_false); } } end_search(); @@ -356,6 +438,10 @@ namespace smt { return l_true; } + // + // Validate, in a slow pass, that the current consequences are correctly + // extracted. + // void context::validate_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector const& conseq, expr_ref_vector const& unfixed) { ast_manager& m = m_manager; diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index c692173e6..0b3147d6b 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -1094,7 +1094,7 @@ namespace smt { \brief This method is invoked when a new disequality is asserted. The disequality is propagated to the theories. */ - void context::add_diseq(enode * n1, enode * n2) { + bool context::add_diseq(enode * n1, enode * n2) { enode * r1 = n1->get_root(); enode * r2 = n2->get_root(); TRACE("add_diseq", tout << "assigning: #" << n1->get_owner_id() << " != #" << n2->get_owner_id() << "\n"; @@ -1111,7 +1111,7 @@ namespace smt { if (r1 == r2) { TRACE("add_diseq_inconsistent", tout << "add_diseq #" << n1->get_owner_id() << " #" << n2->get_owner_id() << " inconsistency, scope_lvl: " << m_scope_lvl << "\n";); - return; // context is inconsistent + return false; // context is inconsistent } // Propagate disequalities to theories @@ -1145,6 +1145,7 @@ namespace smt { l1 = l1->get_next(); } } + return true; } /** @@ -1400,7 +1401,9 @@ namespace smt { } else { TRACE("add_diseq", display_eq_detail(tout, bool_var2enode(v));); - add_diseq(get_enode(lhs), get_enode(rhs)); + if (!add_diseq(get_enode(lhs), get_enode(rhs)) && !inconsistent()) { + set_conflict(b_justification(mk_justification(eq_propagation_justification(get_enode(lhs), get_enode(rhs)))), ~l); + } } } else if (d.is_theory_atom()) { diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 69388e586..79b969118 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -942,7 +942,7 @@ namespace smt { push_eq(n1, n2, eq_justification::mk_cg(used_commutativity)); } - void add_diseq(enode * n1, enode * n2); + bool add_diseq(enode * n1, enode * n2); void assign_quantifier(quantifier * q);