From b73aa3642a54c68e020e7d32b1dfaef86d94a9eb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 27 May 2018 16:54:15 -0700 Subject: [PATCH] check with cube and clause Signed-off-by: Nikolaj Bjorner --- src/smt/smt_clause.h | 8 +- src/smt/smt_context.cpp | 223 +++++++++++++++++++++---------------- src/smt/smt_context.h | 16 ++- src/smt/smt_context_pp.cpp | 2 +- src/smt/smt_kernel.cpp | 9 ++ src/smt/smt_kernel.h | 2 + src/smt/smt_solver.cpp | 20 ++++ src/smt/theory_pb.cpp | 2 +- src/solver/solver.cpp | 21 ++++ src/solver/solver.h | 7 ++ 10 files changed, 202 insertions(+), 108 deletions(-) diff --git a/src/smt/smt_clause.h b/src/smt/smt_clause.h index 8e843c4cf..f0b352e05 100644 --- a/src/smt/smt_clause.h +++ b/src/smt/smt_clause.h @@ -192,13 +192,13 @@ namespace smt { return m_lits[idx]; } - literal * begin_literals() { return m_lits; } + literal * begin() { return m_lits; } - literal * end_literals() { return m_lits + m_num_literals; } + literal * end() { return m_lits + m_num_literals; } - literal const * begin_literals() const { return m_lits; } + literal const * begin() const { return m_lits; } - literal const * end_literals() const { return m_lits + m_num_literals; } + literal const * end() const { return m_lits + m_num_literals; } unsigned get_activity() const { SASSERT(is_lemma()); diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 14a19f824..1e2599802 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -61,6 +61,7 @@ namespace smt { m_dyn_ack_manager(*this, p), m_is_diseq_tmp(nullptr), m_units_to_reassert(m_manager), + m_clause(nullptr), m_qhead(0), m_simp_qhead(0), m_simp_counter(0), @@ -203,8 +204,8 @@ namespace smt { literal l1 = to_literal(l_idx); literal neg_l1 = ~l1; watch_list const & wl = *it; - literal const * it2 = wl.begin_literals(); - literal const * end2 = wl.end_literals(); + literal const * it2 = wl.begin(); + literal const * end2 = wl.end(); for (; it2 != end2; ++it2) { literal l2 = *it2; if (l1.index() < l2.index()) { @@ -385,8 +386,8 @@ namespace smt { it2++; } else { - literal * it3 = cls->begin_literals() + 2; - literal * end3 = cls->end_literals(); + literal * it3 = cls->begin() + 2; + literal * end3 = cls->end(); for(; it3 != end3; ++it3) { if (get_assignment(*it3) != l_false) { // swap literal *it3 with literal at position 0 @@ -1813,6 +1814,17 @@ namespace smt { more case splits to be performed. */ bool context::decide() { + + if (m_clause && at_search_level()) { + switch (decide_clause()) { + case l_true: // already satisfied + break; + case l_undef: // made a decision + return true; + case l_false: // inconsistent + break; + } + } bool_var var; lbool phase; m_case_split_queue->next_case_split(var, phase); @@ -2152,7 +2164,7 @@ namespace smt { \brief See cache_generation(unsigned new_scope_lvl) */ void context::cache_generation(clause const * cls, unsigned new_scope_lvl) { - cache_generation(cls->get_num_literals(), cls->begin_literals(), new_scope_lvl); + cache_generation(cls->get_num_literals(), cls->begin(), new_scope_lvl); } /** @@ -2907,6 +2919,8 @@ namespace smt { del_clauses(m_aux_clauses, 0); del_clauses(m_lemmas, 0); del_justifications(m_justifications, 0); + if (m_clause) del_clause(m_clause); + m_clause = nullptr; if (m_is_diseq_tmp) { m_is_diseq_tmp->del_eh(m_manager, false); m_manager.dec_ref(m_is_diseq_tmp->get_owner()); @@ -3087,6 +3101,7 @@ namespace smt { } TRACE("internalize_assertions", tout << "after internalize_assertions()...\n"; tout << "inconsistent: " << inconsistent() << "\n";); + TRACE("after_internalize_assertions", display(tout);); } bool is_valid_assumption(ast_manager & m, expr * assumption) { @@ -3109,10 +3124,10 @@ namespace smt { /** \brief Assumptions must be uninterpreted boolean constants (aka propositional variables). */ - bool context::validate_assumptions(unsigned num_assumptions, expr * const * assumptions) { - for (unsigned i = 0; i < num_assumptions; i++) { - SASSERT(assumptions[i]); - if (!is_valid_assumption(m_manager, assumptions[i])) { + bool context::validate_assumptions(expr_ref_vector const& asms) { + for (expr* a : asms) { + SASSERT(a); + if (!is_valid_assumption(m_manager, a)) { warning_msg("an assumption must be a propositional variable or the negation of one"); return false; } @@ -3120,11 +3135,55 @@ namespace smt { return true; } - void context::init_assumptions(unsigned num_assumptions, expr * const * assumptions) { + void context::init_clause(expr_ref_vector const& clause) { + if (m_clause) del_clause(m_clause); + m_clause_lits.reset(); + for (expr* lit : clause) { + internalize_formula(lit, true); + mark_as_relevant(lit); + m_clause_lits.push_back(get_literal(lit)); + } + m_clause = mk_clause(m_clause_lits.size(), m_clause_lits.c_ptr(), nullptr); + } + + lbool context::decide_clause() { + if (!m_clause) return l_true; + shuffle(m_clause_lits.size(), m_clause_lits.c_ptr(), m_random); + for (literal l : m_clause_lits) { + switch (get_assignment(l)) { + case l_false: + break; + case l_true: + return l_true; + default: + push_scope(); + assign(l, b_justification::mk_axiom(), true); + return l_undef; + } + } + for (unsigned i = m_assigned_literals.size(); i-- > 0; ) { + literal lit = m_assigned_literals[i]; + if (m_clause_lits.contains(~lit)) { + for (unsigned j = 0, sz = m_clause->get_num_literals(); j < sz; ++j) { + if (m_clause->get_literal(j) == ~lit) { + if (j > 0) m_clause->swap_lits(j, 0); + break; + } + } + b_justification js(m_clause); + set_conflict(js, ~lit); + return l_false; + } + } + UNREACHABLE(); + return l_false; + } + + void context::init_assumptions(expr_ref_vector const& asms) { reset_assumptions(); m_literal2assumption.reset(); m_unsat_core.reset(); - if (num_assumptions > 0) { + if (!asms.empty()) { // We must give a chance to the theories to propagate before we create a new scope... propagate(); // Internal backtracking scopes (created with push_scope()) must only be created when we are @@ -3134,8 +3193,7 @@ namespace smt { if (get_cancel_flag()) return; push_scope(); - for (unsigned i = 0; i < num_assumptions; i++) { - expr * curr_assumption = assumptions[i]; + for (expr * curr_assumption : asms) { if (m_manager.is_true(curr_assumption)) continue; SASSERT(is_valid_assumption(m_manager, curr_assumption)); proof * pr = m_manager.mk_asserted(curr_assumption); @@ -3155,8 +3213,9 @@ namespace smt { } } m_search_lvl = m_scope_lvl; - SASSERT(!(num_assumptions > 0) || m_search_lvl > m_base_lvl); - SASSERT(!(num_assumptions == 0) || m_search_lvl == m_base_lvl); + SASSERT(asms.empty() || m_search_lvl > m_base_lvl); + SASSERT(!asms.empty() || m_search_lvl == m_base_lvl); + TRACE("after_internalization", display(tout);); } void context::reset_assumptions() { @@ -3165,7 +3224,8 @@ namespace smt { m_assumptions.reset(); } - lbool context::mk_unsat_core() { + lbool context::mk_unsat_core(lbool r) { + if (r != l_false) return r; SASSERT(inconsistent()); if (!tracking_assumptions()) { SASSERT(m_assumptions.empty()); @@ -3217,6 +3277,12 @@ namespace smt { m_last_search_failure = MEMOUT; return false; } + + if (m_clause) del_clause(m_clause); + m_clause = nullptr; + m_unsat_core.reset(); + m_stats.m_num_checks++; + pop_to_base_lvl(); return true; } @@ -3240,8 +3306,7 @@ namespace smt { and before internalizing any formulas. */ lbool context::setup_and_check(bool reset_cancel) { - if (!check_preamble(reset_cancel)) - return l_undef; + if (!check_preamble(reset_cancel)) return l_undef; SASSERT(m_scope_lvl == 0); SASSERT(!m_setup.already_configured()); setup_context(m_fparams.m_auto_config); @@ -3254,20 +3319,8 @@ namespace smt { } internalize_assertions(); - lbool r = l_undef; TRACE("before_search", display(tout);); - if (m_asserted_formulas.inconsistent()) { - r = l_false; - } - else { - if (inconsistent()) { - VERIFY(!resolve_conflict()); // build the proof - r = l_false; - } - else { - r = search(); - } - } + lbool r = search(); r = check_finalize(r); return r; } @@ -3281,7 +3334,7 @@ namespace smt { } void context::setup_context(bool use_static_features) { - if (m_setup.already_configured()) + if (m_setup.already_configured() || inconsistent()) return; m_setup(get_config_mode(use_static_features)); setup_components(); @@ -3316,72 +3369,40 @@ namespace smt { } } - lbool context::check(unsigned ext_num_assumptions, expr * const * ext_assumptions, bool reset_cancel, bool already_did_theory_assumptions) { - m_stats.m_num_checks++; - TRACE("check_bug", tout << "STARTING check(num_assumptions, assumptions)\n"; - tout << "inconsistent: " << inconsistent() << ", m_unsat_core.empty(): " << m_unsat_core.empty() << "\n"; - m_asserted_formulas.display(tout); - tout << "-----------------------\n"; - display(tout);); - if (!m_unsat_core.empty()) - m_unsat_core.reset(); - if (!check_preamble(reset_cancel)) - return l_undef; - - TRACE("check_bug", tout << "inconsistent: " << inconsistent() << ", m_unsat_core.empty(): " << m_unsat_core.empty() << "\n";); - pop_to_base_lvl(); + lbool context::check(unsigned num_assumptions, expr * const * assumptions, bool reset_cancel, bool already_did_theory_assumptions) { + if (!check_preamble(reset_cancel)) return l_undef; TRACE("before_search", display(tout);); SASSERT(at_base_level()); - lbool r = l_undef; - if (inconsistent()) { - r = l_false; - } - else { - setup_context(false); - expr_ref_vector all_assumptions(m_manager, ext_num_assumptions, ext_assumptions); - if (!already_did_theory_assumptions) { - add_theory_assumptions(all_assumptions); - } - - unsigned num_assumptions = all_assumptions.size(); - expr * const * assumptions = all_assumptions.c_ptr(); - - if (!validate_assumptions(num_assumptions, assumptions)) - return l_undef; - TRACE("unsat_core_bug", tout << all_assumptions << "\n";); - - internalize_assertions(); - TRACE("after_internalize_assertions", display(tout);); - if (m_asserted_formulas.inconsistent()) { - r = l_false; - } - else { - init_assumptions(num_assumptions, assumptions); - TRACE("after_internalization", display(tout);); - if (inconsistent()) { - VERIFY(!resolve_conflict()); // build the proof - lbool result = mk_unsat_core(); - if (result == l_undef) { - r = l_undef; - } else { - r = l_false; - } - } - else { - r = search(); - if (r == l_false) { - lbool result = mk_unsat_core(); - if (result == l_undef) { - r = l_undef; - } - } - } - } - } + setup_context(false); + expr_ref_vector asms(m_manager, num_assumptions, assumptions); + if (!already_did_theory_assumptions) add_theory_assumptions(asms); + if (!validate_assumptions(asms)) return l_undef; + TRACE("unsat_core_bug", tout << asms << "\n";); + internalize_assertions(); + init_assumptions(asms); + lbool r = search(); + r = mk_unsat_core(r); r = check_finalize(r); return r; } + lbool context::check(expr_ref_vector const& cube, expr_ref_vector const& clause) { + if (!check_preamble(true)) return l_undef; + TRACE("before_search", display(tout);); + setup_context(false); + expr_ref_vector asms(cube); + add_theory_assumptions(asms); + if (!validate_assumptions(asms)) return l_undef; + if (!validate_assumptions(clause)) return l_undef; + internalize_assertions(); + init_assumptions(asms); + init_clause(clause); + lbool r = search(); + r = mk_unsat_core(r); + r = check_finalize(r); + return r; + } + void context::init_search() { for (theory* th : m_theory_set) { th->init_search_eh(); @@ -3450,6 +3471,12 @@ namespace smt { exit(1); } #endif + if (m_asserted_formulas.inconsistent()) + return l_false; + if (inconsistent()) { + VERIFY(!resolve_conflict()); + return l_false; + } timeit tt(get_verbosity_level() >= 100, "smt.stats"); scoped_mk_model smk(*this); SASSERT(at_search_level()); @@ -3473,24 +3500,19 @@ namespace smt { if (!restart(status, curr_lvl)) { break; - } + } } - TRACE("search_lite", tout << "status: " << status << "\n";); TRACE("guessed_literals", expr_ref_vector guessed_lits(m_manager); get_guessed_literals(guessed_lits); - unsigned sz = guessed_lits.size(); - for (unsigned i = 0; i < sz; i++) { - tout << mk_pp(guessed_lits.get(i), m_manager) << "\n"; - }); + tout << guessed_lits << "\n";); end_search(); return status; } bool context::restart(lbool& status, unsigned curr_lvl) { - if (m_last_search_failure != OK) { if (status != l_false) { // build candidate model before returning @@ -3643,6 +3665,8 @@ namespace smt { simplify_clauses(); if (!decide()) { + if (inconsistent()) + return l_false; final_check_status fcs = final_check(); TRACE("final_check_result", tout << "fcs: " << fcs << " last_search_failure: " << m_last_search_failure << "\n";); switch (fcs) { @@ -3700,6 +3724,7 @@ namespace smt { TRACE("final_check", tout << "final_check inconsistent: " << inconsistent() << "\n"; display(tout); display_normalized_enodes(tout);); CASSERT("relevancy", check_relevancy()); + if (m_fparams.m_model_on_final_check) { mk_proto_model(l_undef); model_pp(std::cout, *m_proto_model); diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 32379c353..3110ea3c1 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -168,6 +168,8 @@ namespace smt { expr_ref_vector m_units_to_reassert; svector m_units_to_reassert_sign; literal_vector m_assigned_literals; + clause* m_clause; + literal_vector m_clause_lits; unsigned m_qhead; unsigned m_simp_qhead; int m_simp_counter; //!< can become negative @@ -1104,15 +1106,21 @@ namespace smt { void assert_assumption(expr * a); - bool validate_assumptions(unsigned num_assumptions, expr * const * assumptions); + bool validate_assumptions(expr_ref_vector const& asms); - void init_assumptions(unsigned num_assumptions, expr * const * assumptions); + void init_assumptions(expr_ref_vector const& asms); + + void init_clause(expr_ref_vector const& clause); + + lbool decide_clause(); void reset_assumptions(); + void reset_clause(); + void add_theory_assumptions(expr_ref_vector & theory_assumptions); - lbool mk_unsat_core(); + lbool mk_unsat_core(lbool result); void validate_unsat_core(); @@ -1497,6 +1505,8 @@ namespace smt { lbool check(unsigned num_assumptions = 0, expr * const * assumptions = nullptr, bool reset_cancel = true, bool already_did_theory_assumptions = false); + lbool check(expr_ref_vector const& cube, expr_ref_vector const& clause); + lbool get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq, expr_ref_vector& unfixed); lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes); diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index a6b881d10..19247c1d9 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -583,7 +583,7 @@ namespace smt { case b_justification::CLAUSE: { clause * cls = j.get_clause(); out << "clause "; - if (cls) out << literal_vector(cls->get_num_literals(), cls->begin_literals()); + if (cls) out << literal_vector(cls->get_num_literals(), cls->begin()); break; } case b_justification::JUSTIFICATION: { diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp index a6413aef9..1438efaf6 100644 --- a/src/smt/smt_kernel.cpp +++ b/src/smt/smt_kernel.cpp @@ -115,6 +115,10 @@ namespace smt { return m_kernel.check(num_assumptions, assumptions); } + lbool check(expr_ref_vector const& cube, expr_ref_vector const& clause) { + return m_kernel.check(cube, clause); + } + lbool get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq, expr_ref_vector& unfixed) { return m_kernel.get_consequences(assumptions, vars, conseq, unfixed); } @@ -287,6 +291,11 @@ namespace smt { return r; } + lbool kernel::check(expr_ref_vector const& cube, expr_ref_vector const& clause) { + return m_imp->check(cube, clause); + } + + lbool kernel::get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq, expr_ref_vector& unfixed) { return m_imp->get_consequences(assumptions, vars, conseq, unfixed); } diff --git a/src/smt/smt_kernel.h b/src/smt/smt_kernel.h index 7b2f774ad..4174422f4 100644 --- a/src/smt/smt_kernel.h +++ b/src/smt/smt_kernel.h @@ -132,6 +132,8 @@ namespace smt { lbool check(app_ref_vector const& asms) { return check(asms.size(), (expr* const*)asms.c_ptr()); } + lbool check(expr_ref_vector const& cube, expr_ref_vector const& clause); + /** \brief extract consequences among variables. */ diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 8e5c2aaa2..77f3f32db 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -190,6 +190,26 @@ namespace smt { return m_context.check(num_assumptions, assumptions); } + lbool check_sat(expr_ref_vector const& cube, expr_ref_vector const& clause, model_ref* mdl, expr_ref_vector* core, proof_ref* pr) override { + lbool r = m_context.check(cube, clause); + switch (r) { + case l_false: + if (pr) *pr = get_proof(); + if (core) { + ptr_vector _core; + get_unsat_core(_core); + core->append(_core.size(), _core.c_ptr()); + } + break; + case l_true: + if (mdl) get_model(*mdl); + break; + default: + break; + } + return r; + } + struct scoped_minimize_core { smt_solver& s; expr_ref_vector m_assumptions; diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index d45590bff..953ecea2c 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -2251,7 +2251,7 @@ namespace smt { for (unsigned i = 2; i < num_lits; ++i) { process_antecedent(cls.get_literal(i), offset); } - TRACE("pb", tout << literal_vector(cls.get_num_literals(), cls.begin_literals()) << "\n";); + TRACE("pb", tout << literal_vector(cls.get_num_literals(), cls.begin()) << "\n";); break; } case b_justification::BIN_CLAUSE: diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp index 84b5eb588..d295427e4 100644 --- a/src/solver/solver.cpp +++ b/src/solver/solver.cpp @@ -202,6 +202,27 @@ void solver::assert_expr(expr* f, expr* t) { assert_expr_core2(fml, a); } +lbool solver::check_sat(expr_ref_vector const& cube, expr_ref_vector const& clause, model_ref* mdl, expr_ref_vector* core, proof_ref* pr) { + ast_manager& m = clause.get_manager(); + scoped_push _push(*this); + expr_ref disj = mk_or(clause); + assert_expr(disj); + lbool r = check_sat(cube); + switch (r) { + case l_false: + if (core) get_unsat_core(*core); + if (pr) *pr = get_proof(); + break; + case l_true: + if (mdl) get_model(*mdl); + break; + default: + break; + } + return r; +} + + void solver::collect_param_descrs(param_descrs & r) { r.insert("solver.enforce_model_conversion", CPK_BOOL, "(default: false) enforce model conversion when asserting formulas"); } diff --git a/src/solver/solver.h b/src/solver/solver.h index 4c0c361ff..59a61b3c7 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -146,6 +146,13 @@ public: lbool check_sat(app_ref_vector const& asms) { return check_sat(asms.size(), (expr* const*)asms.c_ptr()); } + /** + \brief Check satisfiability modulo a cube and a clause. + + The cube corresponds to auxiliary assumptions. The clause as an auxiliary disjunction that is also + assumed for the check. + */ + virtual lbool check_sat(expr_ref_vector const& cube, expr_ref_vector const& clause, model_ref* mdl = nullptr, expr_ref_vector* core = nullptr, proof_ref* pr = nullptr); /** \brief Set a progress callback procedure that is invoked by this solver during check_sat.