From a8d069ba460d2d839986ceceec1bf6fa7051af7e Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Tue, 2 May 2017 13:06:08 -0400 Subject: [PATCH] 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); } }