From 6cd1f877b84a9d488d37035bff800e69e02221a7 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Tue, 2 May 2017 10:39:32 -0400 Subject: [PATCH 1/4] params for theory aware branching --- src/smt/params/smt_params.cpp | 1 + src/smt/params/smt_params.h | 3 +++ src/smt/params/smt_params_helper.pyg | 1 + 3 files changed, 5 insertions(+) diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp index 4b7920596..d4eb0b394 100644 --- a/src/smt/params/smt_params.cpp +++ b/src/smt/params/smt_params.cpp @@ -32,6 +32,7 @@ void smt_params::updt_local_params(params_ref const & _p) { m_restart_factor = p.restart_factor(); m_case_split_strategy = static_cast(p.case_split()); m_theory_case_split = p.theory_case_split(); + m_theory_aware_branching = p.theory_aware_branching(); m_delay_units = p.delay_units(); m_delay_units_threshold = p.delay_units_threshold(); m_preprocess = _p.get_bool("preprocess", true); // hidden parameter diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h index c03eaeaef..eacee95ab 100644 --- a/src/smt/params/smt_params.h +++ b/src/smt/params/smt_params.h @@ -110,6 +110,7 @@ struct smt_params : public preprocessor_params, unsigned m_rel_case_split_order; bool m_lookahead_diseq; bool m_theory_case_split; + bool m_theory_aware_branching; // ----------------------------------- // @@ -240,6 +241,8 @@ struct smt_params : public preprocessor_params, m_case_split_strategy(CS_ACTIVITY_DELAY_NEW), m_rel_case_split_order(0), m_lookahead_diseq(false), + m_theory_case_split(false), + m_theory_aware_branching(false), m_delay_units(false), m_delay_units_threshold(32), m_theory_resolve(false), diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index faa48400d..4c9bbc677 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -62,6 +62,7 @@ def_module_params(module_name='smt', ('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.'), + ('theory_aware_branching', BOOL, False, 'Allow the context to use extra information from theory solvers regarding literal branching prioritization.'), ('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 5b4792955dbc954a5d80ce1e5e9210ea82c33e2b Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Tue, 2 May 2017 10:43:40 -0400 Subject: [PATCH 2/4] theory-aware branching heuristic --- src/smt/smt_case_split_queue.cpp | 176 ++++++++++++++++++++++++++++--- src/smt/smt_case_split_queue.h | 3 + src/smt/smt_context.cpp | 4 + src/smt/smt_context.h | 10 +- 4 files changed, 176 insertions(+), 17 deletions(-) diff --git a/src/smt/smt_case_split_queue.cpp b/src/smt/smt_case_split_queue.cpp index 06004e3b8..35cdcb6fe 100644 --- a/src/smt/smt_case_split_queue.cpp +++ b/src/smt/smt_case_split_queue.cpp @@ -22,9 +22,13 @@ Revision History: #include"stopwatch.h" #include"for_each_expr.h" #include"ast_pp.h" +#include"map.h" +#include"hashtable.h" namespace smt { + typedef map > theory_var_priority_map; + struct bool_var_act_lt { svector const & m_activity; bool_var_act_lt(svector const & a):m_activity(a) {} @@ -35,6 +39,27 @@ namespace smt { typedef heap bool_var_act_queue; + struct theory_aware_act_lt { + svector const & m_activity; + theory_var_priority_map const & m_theory_var_priority; + theory_aware_act_lt(svector const & act, theory_var_priority_map const & a):m_activity(act),m_theory_var_priority(a) {} + bool operator()(bool_var v1, bool_var v2) const { + double p_v1, p_v2; + if (!m_theory_var_priority.find(v1, p_v1)) { + p_v1 = 0.0; + } + if (!m_theory_var_priority.find(v2, p_v2)) { + p_v2 = 0.0; + } + // add clause activity + p_v1 += m_activity[v1]; + p_v2 += m_activity[v2]; + return p_v1 > p_v2; + } + }; + + typedef heap theory_aware_act_queue; + /** \brief Case split queue based on activity and random splits. */ @@ -1086,32 +1111,151 @@ namespace smt { m_params.m_qi_eager_threshold += start_gen; } }; - + + class theory_aware_branching_queue : public case_split_queue { + protected: + context & m_context; + smt_params & m_params; + theory_var_priority_map m_theory_var_priority; + theory_aware_act_queue m_queue; + + int_hashtable > m_theory_vars; + map > m_theory_var_phase; + public: + theory_aware_branching_queue(context & ctx, smt_params & p): + m_context(ctx), + m_params(p), + m_theory_var_priority(), + m_queue(1024, theory_aware_act_lt(ctx.get_activity_vector(), m_theory_var_priority)) { + } + + virtual void activity_increased_eh(bool_var v) { + if (m_queue.contains(v)) + m_queue.decreased(v); + } + + virtual void mk_var_eh(bool_var v) { + m_queue.reserve(v+1); + m_queue.insert(v); + } + + virtual void del_var_eh(bool_var v) { + if (m_queue.contains(v)) + m_queue.erase(v); + } + + virtual void unassign_var_eh(bool_var v) { + if (!m_queue.contains(v)) + m_queue.insert(v); + } + + virtual void relevant_eh(expr * n) {} + + virtual void init_search_eh() {} + + virtual void end_search_eh() {} + + virtual void reset() { + m_queue.reset(); + } + + virtual void push_scope() {} + + virtual void pop_scope(unsigned num_scopes) {} + + virtual void next_case_split(bool_var & next, lbool & phase) { + phase = l_undef; + + if (m_context.get_random_value() < static_cast(m_params.m_random_var_freq * random_gen::max_value())) { + next = m_context.get_random_value() % m_context.get_num_b_internalized(); + TRACE("random_split", tout << "next: " << next << " get_assignment(next): " << m_context.get_assignment(next) << "\n";); + if (m_context.get_assignment(next) == l_undef) + return; + } + + while (!m_queue.empty()) { + next = m_queue.erase_min(); + if (m_context.get_assignment(next) == l_undef) + return; + } + + next = null_bool_var; + if (m_theory_vars.contains(next)) { + if (!m_theory_var_phase.find(next, phase)) { + phase = l_undef; + } + } + } + + virtual void add_theory_aware_branching_info(bool_var v, double priority, lbool phase) { + TRACE("theory_aware_branching", tout << "Add theory-aware branching information for l#" << v << ": priority=" << priority << std::endl;); + m_theory_vars.insert(v); + m_theory_var_phase.insert(v, phase); + m_theory_var_priority.insert(v, priority); + if (m_queue.contains(v)) { + if (priority > 0.0) { + m_queue.decreased(v); + } else { + m_queue.increased(v); + } + } + // m_theory_queue.reserve(v+1); + // m_theory_queue.insert(v); + } + + virtual void display(std::ostream & out) { + bool first = true; + bool_var_act_queue::const_iterator it = m_queue.begin(); + bool_var_act_queue::const_iterator end = m_queue.end(); + for (; it != end ; ++it) { + unsigned v = *it; + if (m_context.get_assignment(v) == l_undef) { + if (first) { + out << "remaining case-splits:\n"; + first = false; + } + out << "#" << m_context.bool_var2expr(v)->get_id() << " "; + } + } + if (!first) + out << "\n"; + + } + + virtual ~theory_aware_branching_queue() {}; + }; + case_split_queue * mk_case_split_queue(context & ctx, smt_params & p) { if (p.m_relevancy_lvl < 2 && (p.m_case_split_strategy == CS_RELEVANCY || p.m_case_split_strategy == CS_RELEVANCY_ACTIVITY || - p.m_case_split_strategy == CS_RELEVANCY_GOAL)) { + p.m_case_split_strategy == CS_RELEVANCY_GOAL)) { warning_msg("relevancy must be enabled to use option CASE_SPLIT=3, 4 or 5"); p.m_case_split_strategy = CS_ACTIVITY; } if (p.m_auto_config && (p.m_case_split_strategy == CS_RELEVANCY || p.m_case_split_strategy == CS_RELEVANCY_ACTIVITY || - p.m_case_split_strategy == CS_RELEVANCY_GOAL)) { + p.m_case_split_strategy == CS_RELEVANCY_GOAL)) { warning_msg("auto configuration (option AUTO_CONFIG) must be disabled to use option CASE_SPLIT=3, 4 or 5"); p.m_case_split_strategy = CS_ACTIVITY; } - switch (p.m_case_split_strategy) { - case CS_ACTIVITY_DELAY_NEW: - return alloc(dact_case_split_queue, ctx, p); - case CS_ACTIVITY_WITH_CACHE: - return alloc(cact_case_split_queue, ctx, p); - case CS_RELEVANCY: - return alloc(rel_case_split_queue, ctx, p); - case CS_RELEVANCY_ACTIVITY: - return alloc(rel_act_case_split_queue, ctx, p); - case CS_RELEVANCY_GOAL: - return alloc(rel_goal_case_split_queue, ctx, p); - default: - return alloc(act_case_split_queue, ctx, p); + + if (p.m_theory_aware_branching) { + // override + return alloc(theory_aware_branching_queue, ctx, p); + } else { + switch (p.m_case_split_strategy) { + case CS_ACTIVITY_DELAY_NEW: + return alloc(dact_case_split_queue, ctx, p); + case CS_ACTIVITY_WITH_CACHE: + return alloc(cact_case_split_queue, ctx, p); + case CS_RELEVANCY: + return alloc(rel_case_split_queue, ctx, p); + case CS_RELEVANCY_ACTIVITY: + return alloc(rel_act_case_split_queue, ctx, p); + case CS_RELEVANCY_GOAL: + return alloc(rel_goal_case_split_queue, ctx, p); + default: + return alloc(act_case_split_queue, ctx, p); + } } } diff --git a/src/smt/smt_case_split_queue.h b/src/smt/smt_case_split_queue.h index e6b217a22..9a3a93cc6 100644 --- a/src/smt/smt_case_split_queue.h +++ b/src/smt/smt_case_split_queue.h @@ -46,6 +46,9 @@ namespace smt { virtual void next_case_split(bool_var & next, lbool & phase) = 0; virtual void display(std::ostream & out) = 0; virtual ~case_split_queue() {} + + // theory-aware branching hint + virtual void add_theory_aware_branching_info(bool_var v, double priority, lbool phase) {} }; case_split_queue * mk_case_split_queue(context & ctx, smt_params & p); diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index abac9ef82..a6cef548f 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3022,6 +3022,10 @@ namespace smt { } } + void context::add_theory_aware_branching_info(bool_var v, double priority, lbool phase) { + m_case_split_queue->add_theory_aware_branching_info(v, priority, phase); + } + bool context::propagate_th_case_split(unsigned qhead) { if (m_all_th_case_split_literals.empty()) return true; diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index ca2429be8..9c70f5999 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -838,12 +838,20 @@ namespace smt { */ void mk_th_case_split(unsigned num_lits, literal * lits); + + /* + * Provide a hint to the branching heuristic about the priority of a "theory-aware literal". + * Literals marked in this way will always be branched on before unmarked literals, + * starting with the literal having the highest priority. + */ + void add_theory_aware_branching_info(bool_var v, double priority, lbool phase); + public: // helper function for trail void undo_th_case_split(literal l); - bool propagate_th_case_split(unsigned qhead); + bool propagate_th_case_split(unsigned qhead); bool_var mk_bool_var(expr * n); From a8d069ba460d2d839986ceceec1bf6fa7051af7e Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Tue, 2 May 2017 13:06:08 -0400 Subject: [PATCH 3/4] refactor: add asserts, use case split strategy param --- src/smt/params/smt_params.cpp | 1 - src/smt/params/smt_params.h | 5 ++-- src/smt/params/smt_params_helper.pyg | 3 +-- src/smt/smt_case_split_queue.cpp | 39 +++++++++++++--------------- 4 files changed, 21 insertions(+), 27 deletions(-) diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp index d4eb0b394..4b7920596 100644 --- a/src/smt/params/smt_params.cpp +++ b/src/smt/params/smt_params.cpp @@ -32,7 +32,6 @@ void smt_params::updt_local_params(params_ref const & _p) { m_restart_factor = p.restart_factor(); m_case_split_strategy = static_cast(p.case_split()); m_theory_case_split = p.theory_case_split(); - m_theory_aware_branching = p.theory_aware_branching(); m_delay_units = p.delay_units(); m_delay_units_threshold = p.delay_units_threshold(); m_preprocess = _p.get_bool("preprocess", true); // hidden parameter diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h index eacee95ab..07ae99242 100644 --- a/src/smt/params/smt_params.h +++ b/src/smt/params/smt_params.h @@ -66,7 +66,8 @@ enum case_split_strategy { CS_ACTIVITY_WITH_CACHE, // case split based on activity and cache the activity CS_RELEVANCY, // case split based on relevancy CS_RELEVANCY_ACTIVITY, // case split based on relevancy and activity - CS_RELEVANCY_GOAL // based on relevancy and the current goal + CS_RELEVANCY_GOAL, // based on relevancy and the current goal + CS_ACTIVITY_THEORY_AWARE_BRANCHING // activity-based case split, but theory solvers can manipulate activity }; struct smt_params : public preprocessor_params, @@ -110,7 +111,6 @@ struct smt_params : public preprocessor_params, unsigned m_rel_case_split_order; bool m_lookahead_diseq; bool m_theory_case_split; - bool m_theory_aware_branching; // ----------------------------------- // @@ -242,7 +242,6 @@ struct smt_params : public preprocessor_params, m_rel_case_split_order(0), m_lookahead_diseq(false), m_theory_case_split(false), - m_theory_aware_branching(false), m_delay_units(false), m_delay_units_threshold(32), m_theory_resolve(false), diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 4c9bbc677..450d2eff3 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -11,7 +11,7 @@ def_module_params(module_name='smt', ('phase_selection', UINT, 3, 'phase selection heuristic: 0 - always false, 1 - always true, 2 - phase caching, 3 - phase caching conservative, 4 - phase caching conservative 2, 5 - random, 6 - number of occurrences'), ('restart_strategy', UINT, 1, '0 - geometric, 1 - inner-outer-geometric, 2 - luby, 3 - fixed, 4 - arithmetic'), ('restart_factor', DOUBLE, 1.1, 'when using geometric (or inner-outer-geometric) progression of restarts, it specifies the constant used to multiply the currect restart threshold'), - ('case_split', UINT, 1, '0 - case split based on variable activity, 1 - similar to 0, but delay case splits created during the search, 2 - similar to 0, but cache the relevancy, 3 - case split based on relevancy (structural splitting), 4 - case split on relevancy and activity, 5 - case split on relevancy and current goal'), + ('case_split', UINT, 1, '0 - case split based on variable activity, 1 - similar to 0, but delay case splits created during the search, 2 - similar to 0, but cache the relevancy, 3 - case split based on relevancy (structural splitting), 4 - case split on relevancy and activity, 5 - case split on relevancy and current goal, 6 - activity-based case split with theory-aware branching activity'), ('delay_units', BOOL, False, 'if true then z3 will not restart when a unit clause is learned'), ('delay_units_threshold', UINT, 32, 'maximum number of learned unit clauses before restarting, ignored if delay_units is false'), ('pull_nested_quantifiers', BOOL, False, 'pull nested quantifiers'), @@ -62,7 +62,6 @@ def_module_params(module_name='smt', ('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.'), - ('theory_aware_branching', BOOL, False, 'Allow the context to use extra information from theory solvers regarding literal branching prioritization.'), ('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'), diff --git a/src/smt/smt_case_split_queue.cpp b/src/smt/smt_case_split_queue.cpp index 35cdcb6fe..129d77c85 100644 --- a/src/smt/smt_case_split_queue.cpp +++ b/src/smt/smt_case_split_queue.cpp @@ -1164,9 +1164,10 @@ namespace smt { virtual void pop_scope(unsigned num_scopes) {} virtual void next_case_split(bool_var & next, lbool & phase) { - phase = l_undef; - - if (m_context.get_random_value() < static_cast(m_params.m_random_var_freq * random_gen::max_value())) { + int threshold = static_cast(m_params.m_random_var_freq * random_gen::max_value()); + SASSERT(threshold >= 0); + if (m_context.get_random_value() < threshold) { + SASSERT(m_context.get_num_b_internalized() > 0); next = m_context.get_random_value() % m_context.get_num_b_internalized(); TRACE("random_split", tout << "next: " << next << " get_assignment(next): " << m_context.get_assignment(next) << "\n";); if (m_context.get_assignment(next) == l_undef) @@ -1237,25 +1238,21 @@ namespace smt { warning_msg("auto configuration (option AUTO_CONFIG) must be disabled to use option CASE_SPLIT=3, 4 or 5"); p.m_case_split_strategy = CS_ACTIVITY; } - - if (p.m_theory_aware_branching) { - // override + switch (p.m_case_split_strategy) { + case CS_ACTIVITY_DELAY_NEW: + return alloc(dact_case_split_queue, ctx, p); + case CS_ACTIVITY_WITH_CACHE: + return alloc(cact_case_split_queue, ctx, p); + case CS_RELEVANCY: + return alloc(rel_case_split_queue, ctx, p); + case CS_RELEVANCY_ACTIVITY: + return alloc(rel_act_case_split_queue, ctx, p); + case CS_RELEVANCY_GOAL: + return alloc(rel_goal_case_split_queue, ctx, p); + case CS_ACTIVITY_THEORY_AWARE_BRANCHING: return alloc(theory_aware_branching_queue, ctx, p); - } else { - switch (p.m_case_split_strategy) { - case CS_ACTIVITY_DELAY_NEW: - return alloc(dact_case_split_queue, ctx, p); - case CS_ACTIVITY_WITH_CACHE: - return alloc(cact_case_split_queue, ctx, p); - case CS_RELEVANCY: - return alloc(rel_case_split_queue, ctx, p); - case CS_RELEVANCY_ACTIVITY: - return alloc(rel_act_case_split_queue, ctx, p); - case CS_RELEVANCY_GOAL: - return alloc(rel_goal_case_split_queue, ctx, p); - default: - return alloc(act_case_split_queue, ctx, p); - } + default: + return alloc(act_case_split_queue, ctx, p); } } From 15cb2d7dbad86ce0411c902278ba8c57bb66474e Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Tue, 2 May 2017 14:08:48 -0400 Subject: [PATCH 4/4] cleanup --- src/smt/params/smt_params.h | 1 - 1 file changed, 1 deletion(-) diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h index 07ae99242..49487c4dd 100644 --- a/src/smt/params/smt_params.h +++ b/src/smt/params/smt_params.h @@ -241,7 +241,6 @@ struct smt_params : public preprocessor_params, m_case_split_strategy(CS_ACTIVITY_DELAY_NEW), m_rel_case_split_order(0), m_lookahead_diseq(false), - m_theory_case_split(false), m_delay_units(false), m_delay_units_threshold(32), m_theory_resolve(false),