From f655e1976eca91d1aaa06d1551367910e63ec03c Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Mon, 1 May 2017 10:18:38 -0400 Subject: [PATCH 1/5] add params for theory case split --- src/smt/params/smt_params.cpp | 3 ++- src/smt/params/smt_params.h | 1 + src/smt/params/smt_params_helper.pyg | 1 + 3 files changed, 4 insertions(+), 1 deletion(-) diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp index 8a9188e2b..4b7920596 100644 --- a/src/smt/params/smt_params.cpp +++ b/src/smt/params/smt_params.cpp @@ -31,6 +31,7 @@ void smt_params::updt_local_params(params_ref const & _p) { m_restart_strategy = static_cast(p.restart_strategy()); m_restart_factor = p.restart_factor(); m_case_split_strategy = static_cast(p.case_split()); + m_theory_case_split = p.theory_case_split(); m_delay_units = p.delay_units(); m_delay_units_threshold = p.delay_units_threshold(); m_preprocess = _p.get_bool("preprocess", true); // hidden parameter @@ -155,4 +156,4 @@ void smt_params::display(std::ostream & out) const { DISPLAY_PARAM(m_check_at_labels); DISPLAY_PARAM(m_dump_goal_as_smt); DISPLAY_PARAM(m_auto_config); -} \ No newline at end of file +} diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h index 366570365..c03eaeaef 100644 --- a/src/smt/params/smt_params.h +++ b/src/smt/params/smt_params.h @@ -109,6 +109,7 @@ struct smt_params : public preprocessor_params, case_split_strategy m_case_split_strategy; unsigned m_rel_case_split_order; bool m_lookahead_diseq; + bool m_theory_case_split; // ----------------------------------- // diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 6ac4aab04..faa48400d 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -61,6 +61,7 @@ def_module_params(module_name='smt', ('dack.gc', UINT, 2000, 'Dynamic ackermannization garbage collection frequency (per conflict)'), ('dack.gc_inv_decay', DOUBLE, 0.8, 'Dynamic ackermannization garbage collection decay'), ('dack.threshold', UINT, 10, ' number of times the congruence rule must be used before Leibniz\'s axiom is expanded'), + ('theory_case_split', BOOL, False, 'Allow the context to use heuristics involving theory case splits, which are a set of literals of which exactly one can be assigned True. If this option is false, the context will generate extra axioms to enforce this instead.'), ('core.validate', BOOL, False, 'validate unsat core produced by SMT context'), ('core.minimize', BOOL, False, 'minimize unsat core produced by SMT context'), ('core.extend_patterns', BOOL, False, 'extend unsat core with literals that trigger (potential) quantifier instances'), From 2f56d128b0531829d8354c52d1059e368747c33e Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Mon, 1 May 2017 10:34:43 -0400 Subject: [PATCH 2/5] add theory case split support to smt_context --- src/smt/smt_context.cpp | 123 ++++++++++++++++++++++++++++++++++++++++ src/smt/smt_context.h | 25 ++++++++ 2 files changed, 148 insertions(+) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 6a3c036ca..af1e94e62 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -62,6 +62,7 @@ namespace smt { m_is_diseq_tmp(0), m_units_to_reassert(m_manager), m_qhead(0), + m_th_case_split_qhead(0), m_simp_qhead(0), m_simp_counter(0), m_bvar_inc(1.0), @@ -339,6 +340,7 @@ namespace smt { bool context::bcp() { SASSERT(!inconsistent()); + m_th_case_split_qhead = m_qhead; while (m_qhead < m_assigned_literals.size()) { if (get_cancel_flag()) { return true; @@ -1768,6 +1770,8 @@ namespace smt { unsigned qhead = m_qhead; if (!bcp()) return false; + if (!propagate_th_case_split()) + return false; if (get_cancel_flag()) { m_qhead = qhead; return true; @@ -2960,6 +2964,125 @@ namespace smt { assert_expr_core(e, pr); } + class case_split_insert_trail : public trail { + literal l; + public: + case_split_insert_trail(literal l): + l(l) { + } + virtual void undo(context & ctx) { + ctx.undo_th_case_split(l); + } + }; + + void context::mk_th_case_split(unsigned num_lits, literal * lits) { + TRACE("theory_case_split", display_literals_verbose(tout << "theory case split: ", num_lits, lits); tout << std::endl;); + // If we don't use the theory case split heuristic, + // for each pair of literals (l1, l2) we add the clause (~l1 OR ~l2) + // to enforce the condition that more than one literal can't be + // assigned 'true' simultaneously. + if (!m_fparams.m_theory_case_split) { + for (unsigned i = 0; i < num_lits; ++i) { + for (unsigned j = i+1; j < num_lits; ++j) { + literal l1 = lits[i]; + literal l2 = lits[j]; + literal excl[2] = {~l1, ~l2}; + justification * j_excl = 0; + mk_clause(2, excl, j_excl); + } + } + } else { + literal_vector new_case_split; + for (unsigned i = 0; i < num_lits; ++i) { + literal l = lits[i]; + SASSERT(!m_all_th_case_split_literals.contains(l.index())); + m_all_th_case_split_literals.insert(l.index()); + push_trail(case_split_insert_trail(l)); + new_case_split.push_back(l); + } + m_th_case_split_sets.push_back(new_case_split); + push_trail(push_back_vector >(m_th_case_split_sets)); + for (unsigned i = 0; i < num_lits; ++i) { + literal l = lits[i]; + if (!m_literal2casesplitsets.contains(l.index())) { + m_literal2casesplitsets.insert(l.index(), vector()); + } + m_literal2casesplitsets[l.index()].push_back(new_case_split); + } + TRACE("theory_case_split", tout << "tracking case split literal set { "; + for (unsigned i = 0; i < num_lits; ++i) { + tout << lits[i].index() << " "; + } + tout << "}" << std::endl; + ); + } + } + + void context::undo_th_case_split(literal l) { + m_all_th_case_split_literals.remove(l.index()); + if (m_literal2casesplitsets.contains(l.index())) { + if (!m_literal2casesplitsets[l.index()].empty()) { + m_literal2casesplitsets[l.index()].pop_back(); + } + } + } + + bool context::propagate_th_case_split() { + if (m_all_th_case_split_literals.empty()) + return true; + + // iterate over all literals assigned since the last time this method was called, + // not counting any literals that get assigned by this method + // this relies on bcp() to give us its old m_qhead and therefore + // bcp() should always be called before this method + unsigned assigned_literal_idx = m_th_case_split_qhead; + unsigned assigned_literal_end = m_assigned_literals.size(); + while(assigned_literal_idx < assigned_literal_end) { + literal l = m_assigned_literals[assigned_literal_idx]; + TRACE("theory_case_split", tout << "check literal " << l.index() << std::endl; display_literal_verbose(tout, l); tout << std::endl;); + ++assigned_literal_idx; + // check if this literal participates in any theory case split + if (m_all_th_case_split_literals.contains(l.index())) { + TRACE("theory_case_split", tout << "assigned literal " << l.index() << " is a theory case split literal" << std::endl;); + // now find the sets of literals which contain l + vector case_split_sets = m_literal2casesplitsets.get(l.index(), vector()); + for (vector::const_iterator it = case_split_sets.begin(); it != case_split_sets.end(); ++it) { + literal_vector case_split_set = *it; + TRACE("theory_case_split", tout << "found case split set { "; + for(literal_vector::iterator set_it = case_split_set.begin(); set_it != case_split_set.end(); ++set_it) { + tout << set_it->index() << " "; + } + tout << "}" << std::endl;); + for(literal_vector::iterator set_it = case_split_set.begin(); set_it != case_split_set.end(); ++set_it) { + literal l2 = *set_it; + if (l2 != l) { + b_justification js(l); + switch (get_assignment(l2)) { + case l_false: + TRACE("theory_case_split", tout << "case split literal " << l2.index() << " is already assigned False" << std::endl;); + break; + case l_undef: + TRACE("theory_case_split", tout << "case split literal " << l2.index() << " is not assigned" << std::endl;); + assign(~l2, js); + break; + case l_true: + TRACE("theory_case_split", tout << "case split literal " << l2.index() << " is already assigned True" << std::endl;); + assign(~l2, js); + break; + } + if (inconsistent()) { + TRACE("theory_case_split", tout << "conflict detected!" << std::endl;); + return false; + } + } + } + } + } + } + // if we get here without detecting a conflict, we're fine + return true; + } + bool context::reduce_assertions() { if (!m_asserted_formulas.inconsistent()) { SASSERT(at_base_level()); diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index b3cfb4639..d9817236e 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -226,6 +226,16 @@ namespace smt { literal2assumption m_literal2assumption; // maps an expression associated with a literal to the original assumption expr_ref_vector m_unsat_core; + // ----------------------------------- + // + // Theory case split + // + // ----------------------------------- + uint_set m_all_th_case_split_literals; + vector m_th_case_split_sets; + u_map< vector > m_literal2casesplitsets; // returns the case split literal sets that a literal participates in + unsigned m_th_case_split_qhead; + // ----------------------------------- // // Accessors @@ -820,6 +830,21 @@ namespace smt { void mk_th_axiom(theory_id tid, literal l1, literal l2, literal l3, unsigned num_params = 0, parameter * params = 0); + /* + * Provide a hint to the core solver that the specified literals form a "theory case split". + * The core solver will enforce the condition that exactly one of these literals can be + * assigned 'true' at any time. + * We assume that the theory solver has already asserted the disjunction of these literals + * or some other axiom that means at least one of them must be assigned 'true'. + */ + void mk_th_case_split(unsigned num_lits, literal * lits); + + public: + + // helper function for trail + void undo_th_case_split(literal l); + + bool propagate_th_case_split(); bool_var mk_bool_var(expr * n); From 3bce61e0d432261ae173ac77659c773aa148940e Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Mon, 1 May 2017 10:43:33 -0400 Subject: [PATCH 3/5] fix warning --- src/smt/smt_context.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index af1e94e62..9a841ea26 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -62,7 +62,6 @@ namespace smt { m_is_diseq_tmp(0), m_units_to_reassert(m_manager), m_qhead(0), - m_th_case_split_qhead(0), m_simp_qhead(0), m_simp_counter(0), m_bvar_inc(1.0), @@ -75,6 +74,7 @@ namespace smt { m_unsat_proof(m), m_unknown("unknown"), m_unsat_core(m), + m_th_case_split_qhead(0), #ifdef Z3DEBUG m_trail_enabled(true), #endif From b86d472eaf5767cc2d870a08d0c22b70b2262f47 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Mon, 1 May 2017 18:22:49 -0400 Subject: [PATCH 4/5] simplify theory case split handling --- src/smt/smt_context.cpp | 15 ++------------- 1 file changed, 2 insertions(+), 13 deletions(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 9a841ea26..af45f0fcc 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3057,19 +3057,8 @@ namespace smt { literal l2 = *set_it; if (l2 != l) { b_justification js(l); - switch (get_assignment(l2)) { - case l_false: - TRACE("theory_case_split", tout << "case split literal " << l2.index() << " is already assigned False" << std::endl;); - break; - case l_undef: - TRACE("theory_case_split", tout << "case split literal " << l2.index() << " is not assigned" << std::endl;); - assign(~l2, js); - break; - case l_true: - TRACE("theory_case_split", tout << "case split literal " << l2.index() << " is already assigned True" << std::endl;); - assign(~l2, js); - break; - } + TRACE("theory_case_split", tout << "case split literal "; l2.display(tout, m_manager, m_bool_var2expr.c_ptr());); + assign(~l2, js); if (inconsistent()) { TRACE("theory_case_split", tout << "conflict detected!" << std::endl;); return false; From 16a5e944d78aae384f2acb17e1bd60c6499f965e Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Mon, 1 May 2017 18:25:54 -0400 Subject: [PATCH 5/5] use reference for case split sets --- src/smt/smt_context.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index af45f0fcc..602ff5160 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3045,7 +3045,7 @@ namespace smt { if (m_all_th_case_split_literals.contains(l.index())) { TRACE("theory_case_split", tout << "assigned literal " << l.index() << " is a theory case split literal" << std::endl;); // now find the sets of literals which contain l - vector case_split_sets = m_literal2casesplitsets.get(l.index(), vector()); + vector & case_split_sets = m_literal2casesplitsets.get(l.index(), vector()); for (vector::const_iterator it = case_split_sets.begin(); it != case_split_sets.end(); ++it) { literal_vector case_split_set = *it; TRACE("theory_case_split", tout << "found case split set { ";