From 6cd1f877b84a9d488d37035bff800e69e02221a7 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Tue, 2 May 2017 10:39:32 -0400 Subject: [PATCH 01/11] 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 02/11] 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 03/11] 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 04/11] 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), From ed0b2be618121b407bc3384e21a446538408c4c8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 2 May 2017 14:10:07 -0700 Subject: [PATCH 05/11] fix bug in tracking levels of variables: levels are not cleared, only truth assignment Signed-off-by: Nikolaj Bjorner --- src/opt/wmax.cpp | 4 +-- src/sat/sat_solver.cpp | 77 ++++++++++++++++++++++-------------------- 2 files changed, 41 insertions(+), 40 deletions(-) diff --git a/src/opt/wmax.cpp b/src/opt/wmax.cpp index 9708bdc8f..58d319a63 100644 --- a/src/opt/wmax.cpp +++ b/src/opt/wmax.cpp @@ -61,13 +61,12 @@ namespace opt { return is_sat; } m_upper = m_lower; - bool was_sat = false; expr_ref_vector asms(m); vector cores; obj_map::iterator it = soft.begin(), end = soft.end(); for (; it != end; ++it) { - expr* c = assert_weighted(wth(), it->m_key, it->m_value); + assert_weighted(wth(), it->m_key, it->m_value); if (!is_true(it->m_key)) { m_upper += it->m_value; } @@ -97,7 +96,6 @@ namespace opt { expr_ref fml = wth().mk_block(); //DEBUG_CODE(verify_cores(cores);); s().assert_expr(fml); - was_sat = true; } else { //DEBUG_CODE(verify_cores(cores);); diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index dc5aa2964..b5bd46168 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -3141,42 +3141,42 @@ namespace sat { // // ----------------------- -static void prune_unfixed(sat::literal_vector& lambda, sat::model const& m) { - for (unsigned i = 0; i < lambda.size(); ++i) { - if ((m[lambda[i].var()] == l_false) != lambda[i].sign()) { - lambda[i] = lambda.back(); - lambda.pop_back(); + static void prune_unfixed(sat::literal_vector& lambda, sat::model const& m) { + for (unsigned i = 0; i < lambda.size(); ++i) { + if ((m[lambda[i].var()] == l_false) != lambda[i].sign()) { + lambda[i] = lambda.back(); + lambda.pop_back(); + --i; + } + } + } + + // Algorithm 7: Corebased Algorithm with Chunking + + static void back_remove(sat::literal_vector& lits, sat::literal l) { + for (unsigned i = lits.size(); i > 0; ) { --i; + if (lits[i] == l) { + lits[i] = lits.back(); + lits.pop_back(); + return; + } } + UNREACHABLE(); } -} - -// Algorithm 7: Corebased Algorithm with Chunking - -static void back_remove(sat::literal_vector& lits, sat::literal l) { - for (unsigned i = lits.size(); i > 0; ) { - --i; - if (lits[i] == l) { - lits[i] = lits.back(); - lits.pop_back(); - return; - } - } - std::cout << "UNREACHABLE\n"; -} static void brute_force_consequences(sat::solver& s, sat::literal_vector const& asms, sat::literal_vector const& gamma, vector& conseq) { - for (unsigned i = 0; i < gamma.size(); ++i) { - sat::literal nlit = ~gamma[i]; - sat::literal_vector asms1(asms); - asms1.push_back(nlit); - lbool r = s.check(asms1.size(), asms1.c_ptr()); - if (r == l_false) { - conseq.push_back(s.get_core()); + for (unsigned i = 0; i < gamma.size(); ++i) { + sat::literal nlit = ~gamma[i]; + sat::literal_vector asms1(asms); + asms1.push_back(nlit); + lbool r = s.check(asms1.size(), asms1.c_ptr()); + if (r == l_false) { + conseq.push_back(s.get_core()); + } } } -} - + static lbool core_chunking(sat::solver& s, model const& m, sat::bool_var_vector const& vars, sat::literal_vector const& asms, vector& conseq, unsigned K) { sat::literal_vector lambda; for (unsigned i = 0; i < vars.size(); i++) { @@ -3259,9 +3259,12 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) { } } - // is_sat = core_chunking(*this, mdl, vars, asms, conseq, 100); - - is_sat = get_consequences(asms, lits, conseq); + if (false && asms.empty()) { + is_sat = core_chunking(*this, mdl, vars, asms, conseq, 100); + } + else { + is_sat = get_consequences(asms, lits, conseq); + } set_model(mdl); return is_sat; } @@ -3390,8 +3393,7 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) { literal lit = *it; if (value(lit) != l_undef) { ++num_fixed; - if (lvl(lit) <= 1) { - SASSERT(value(lit) == l_true); + if (lvl(lit) <= 1 && value(lit) == l_true) { extract_fixed_consequences(lit, assumptions, unfixed_vars, conseq); } continue; @@ -3498,8 +3500,9 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) { literal_set::iterator it = unfixed_lits.begin(), end = unfixed_lits.end(); for (; it != end; ++it) { literal lit = *it; - if (lvl(lit) <= 1) { - SASSERT(value(lit) == l_true); + TRACE("sat", tout << "extract: " << lit << " " << value(lit) << " " << lvl(lit) << "\n";); + + if (lvl(lit) <= 1 && value(lit) == l_true) { extract_fixed_consequences(lit, assumptions, unfixed_vars, conseq); } } @@ -3508,8 +3511,8 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) { bool solver::check_domain(literal lit, literal lit2) { if (!m_antecedents.contains(lit2.var())) { SASSERT(value(lit2) == l_true); + SASSERT(m_todo_antecedents.empty() || m_todo_antecedents.back() != lit2); m_todo_antecedents.push_back(lit2); - TRACE("sat", tout << "todo: " << lit2 << " " << value(lit2) << "\n";); return false; } else { From 92755b0185e32a31d0ed1e2d700b9971f1523087 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Tue, 2 May 2017 17:16:35 -0400 Subject: [PATCH 06/11] smt_setup framework, all hooks to theory_str are redirected to theory_seq --- src/smt/params/smt_params.cpp | 1 + src/smt/params/smt_params.h | 10 +++++++- src/smt/params/smt_params_helper.pyg | 1 + src/smt/smt_setup.cpp | 38 ++++++++++++++++++++++++---- src/smt/smt_setup.h | 4 ++- src/solver/smt_logics.cpp | 6 ++++- src/solver/smt_logics.h | 1 + 7 files changed, 53 insertions(+), 8 deletions(-) diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp index 4b7920596..3d0b59c88 100644 --- a/src/smt/params/smt_params.cpp +++ b/src/smt/params/smt_params.cpp @@ -40,6 +40,7 @@ void smt_params::updt_local_params(params_ref const & _p) { m_max_conflicts = p.max_conflicts(); m_core_validate = p.core_validate(); m_logic = _p.get_sym("logic", m_logic); + m_string_solver = p.string_solver(); model_params mp(_p); m_model_compact = mp.compact(); if (_p.get_bool("arith.greatest_error_pivot", false)) diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h index c03eaeaef..b44e782fd 100644 --- a/src/smt/params/smt_params.h +++ b/src/smt/params/smt_params.h @@ -213,6 +213,13 @@ struct smt_params : public preprocessor_params, bool m_dump_goal_as_smt; bool m_auto_config; + // ----------------------------------- + // + // Solver selection + // + // ----------------------------------- + symbol m_string_solver; + smt_params(params_ref const & p = params_ref()): m_display_proof(false), m_display_dot_proof(false), @@ -281,7 +288,8 @@ struct smt_params : public preprocessor_params, m_at_labels_cex(false), m_check_at_labels(false), m_dump_goal_as_smt(false), - m_auto_config(true) { + m_auto_config(true), + m_string_solver(symbol("seq")){ updt_local_params(p); } diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index faa48400d..a06a37f2a 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.'), + ('string_solver', SYMBOL, 'seq', 'solver for string/sequence theories. options are: \'z3str3\' (specialized string solver), \'seq\' (sequence solver), \'auto\' (use static features to choose best solver)'), ('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_setup.cpp b/src/smt/smt_setup.cpp index ee92c4f61..84e3dee32 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -120,6 +120,8 @@ namespace smt { setup_QF_FP(); else if (m_logic == "QF_FPBV" || m_logic == "QF_BVFP") setup_QF_FPBV(); + else if (m_logic == "QF_S") + setup_QF_S(); else setup_unknown(); } @@ -161,6 +163,8 @@ namespace smt { setup_QF_BVRE(); else if (m_logic == "QF_AUFLIA") setup_QF_AUFLIA(st); + else if (m_logic == "QF_S") + setup_QF_S(); else if (m_logic == "AUFLIA") setup_AUFLIA(st); else if (m_logic == "AUFLIRA") @@ -201,7 +205,7 @@ namespace smt { void setup::setup_QF_BVRE() { setup_QF_BV(); setup_QF_LIA(); - setup_seq(); + m_context.register_plugin(alloc(theory_seq, m_manager)); } void setup::setup_QF_UF(static_features const & st) { @@ -700,6 +704,10 @@ namespace smt { m_context.register_plugin(alloc(smt::theory_fpa, m_manager)); } + void setup::setup_QF_S() { + m_context.register_plugin(alloc(smt::theory_seq, m_manager)); + } + bool is_arith(static_features const & st) { return st.m_num_arith_ineqs > 0 || st.m_num_arith_terms > 0 || st.m_num_arith_eqs > 0; } @@ -814,8 +822,21 @@ namespace smt { m_context.register_plugin(mk_theory_dl(m_manager)); } - void setup::setup_seq() { - m_context.register_plugin(alloc(theory_seq, m_manager)); + void setup::setup_seq(static_features const & st) { + // check params for what to do here when it's ambiguous + if (m_params.m_string_solver == "z3str3") { + setup_str(); + } else if (m_params.m_string_solver == "seq") { + m_context.register_plugin(alloc(smt::theory_seq, m_manager)); + } else if (m_params.m_string_solver == "auto") { + if (st.m_has_seq_non_str) { + m_context.register_plugin(alloc(smt::theory_seq, m_manager)); + } else { + setup_str(); + } + } else { + throw default_exception("invalid parameter for smt.string_solver, valid options are 'z3str3', 'seq', 'auto'"); + } } void setup::setup_card() { @@ -827,13 +848,20 @@ namespace smt { m_context.register_plugin(alloc(theory_fpa, m_manager)); } + void setup::setup_str() { + m_context.register_plugin(alloc(smt::theory_seq, m_manager)); + } + void setup::setup_unknown() { + static_features st(m_manager); + st.collect(m_context.get_num_asserted_formulas(), m_context.get_asserted_formulas()); + setup_arith(); setup_arrays(); setup_bv(); setup_datatypes(); setup_dl(); - setup_seq(); + setup_seq(st); setup_card(); setup_fpa(); } @@ -848,7 +876,7 @@ namespace smt { setup_datatypes(); setup_bv(); setup_dl(); - setup_seq(); + setup_seq(st); setup_card(); setup_fpa(); return; diff --git a/src/smt/smt_setup.h b/src/smt/smt_setup.h index 68cd5703c..d30c896e5 100644 --- a/src/smt/smt_setup.h +++ b/src/smt/smt_setup.h @@ -77,6 +77,7 @@ namespace smt { void setup_QF_AUFLIA(static_features const & st); void setup_QF_FP(); void setup_QF_FPBV(); + void setup_QF_S(); void setup_LRA(); void setup_AUFLIA(bool simple_array = true); void setup_AUFLIA(static_features const & st); @@ -93,11 +94,12 @@ namespace smt { void setup_bv(); void setup_arith(); void setup_dl(); - void setup_seq(); + void setup_seq(static_features const & st); void setup_card(); void setup_i_arith(); void setup_mi_arith(); void setup_fpa(); + void setup_str(); public: setup(context & c, smt_params & params); diff --git a/src/solver/smt_logics.cpp b/src/solver/smt_logics.cpp index 210a09f96..c4ead74df 100644 --- a/src/solver/smt_logics.cpp +++ b/src/solver/smt_logics.cpp @@ -24,7 +24,7 @@ Revision History: bool smt_logics::supported_logic(symbol const & s) { return logic_has_uf(s) || logic_is_all(s) || logic_has_fd(s) || logic_has_arith(s) || logic_has_bv(s) || - logic_has_array(s) || logic_has_seq(s) || + logic_has_array(s) || logic_has_seq(s) || logic_has_str(s) || logic_has_horn(s) || logic_has_fpa(s); } @@ -132,6 +132,10 @@ bool smt_logics::logic_has_seq(symbol const & s) { return s == "QF_BVRE" || s == "QF_S" || s == "ALL"; } +bool smt_logics::logic_has_str(symbol const & s) { + return s == "QF_S" || s == "ALL"; +} + bool smt_logics::logic_has_fpa(symbol const & s) { return s == "QF_FP" || s == "QF_FPBV" || s == "QF_BVFP" || s == "ALL"; } diff --git a/src/solver/smt_logics.h b/src/solver/smt_logics.h index 72c3b8764..702431cdd 100644 --- a/src/solver/smt_logics.h +++ b/src/solver/smt_logics.h @@ -30,6 +30,7 @@ public: static bool logic_has_bv(symbol const & s); static bool logic_has_array(symbol const & s); static bool logic_has_seq(symbol const & s); + static bool logic_has_str(symbol const & s); static bool logic_has_fpa(symbol const & s); static bool logic_has_horn(symbol const& s); static bool logic_has_pb(symbol const& s); From 21cda27f5e175cecdc8ed0bd25bb1bfc0d8c1d17 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 2 May 2017 15:57:31 -0700 Subject: [PATCH 07/11] fix quadratic behavior of extract_assumptions Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver.cpp | 19 ++++++++++++++----- src/test/cnf_backbones.cpp | 3 ++- 2 files changed, 16 insertions(+), 6 deletions(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index b5bd46168..7f2b75830 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -3523,6 +3523,7 @@ namespace sat { bool solver::extract_assumptions(literal lit, index_set& s) { justification js = m_justification[lit.var()]; TRACE("sat", tout << lit << " " << js << "\n";); + bool all_found = true; switch (js.get_kind()) { case justification::NONE: break; @@ -3540,8 +3541,12 @@ namespace sat { clause & c = *(m_cls_allocator.get_clause(js.get_clause_offset())); for (unsigned i = 0; i < c.size(); ++i) { if (c[i] != lit) { - if (!check_domain(lit, ~c[i])) return false; - s |= m_antecedents.find(c[i].var()); + if (check_domain(lit, ~c[i]) && all_found) { + s |= m_antecedents.find(c[i].var()); + } + else { + all_found = false; + } } } break; @@ -3551,8 +3556,12 @@ namespace sat { literal_vector::iterator it = m_ext_antecedents.begin(); literal_vector::iterator end = m_ext_antecedents.end(); for (; it != end; ++it) { - if (!check_domain(lit, *it)) return false; - s |= m_antecedents.find(it->var()); + if (check_domain(lit, *it) && all_found) { + s |= m_antecedents.find(it->var()); + } + else { + all_found = false; + } } break; } @@ -3561,7 +3570,7 @@ namespace sat { break; } TRACE("sat", display_index_set(tout << lit << ": " , s) << "\n";); - return true; + return all_found; } std::ostream& solver::display_index_set(std::ostream& out, index_set const& s) const { diff --git a/src/test/cnf_backbones.cpp b/src/test/cnf_backbones.cpp index b95977a46..eab91e557 100644 --- a/src/test/cnf_backbones.cpp +++ b/src/test/cnf_backbones.cpp @@ -246,13 +246,14 @@ static void cnf_backbones(bool use_chunk, char const* file_name) { vector conseq; sat::bool_var_vector vars; sat::literal_vector assumptions; + unsigned num_vars = solver.num_vars(); if (p.get_bool("dimacs.core", false)) { g_solver = &solver2; vector tracking_clauses; track_clauses(solver, solver2, assumptions, tracking_clauses); } - for (unsigned i = 1; i < g_solver->num_vars(); ++i) { + for (unsigned i = 1; i < num_vars; ++i) { vars.push_back(i); g_solver->set_external(i); } From 561a4331a83438a3483504e272722bd1f291ba32 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 2 May 2017 16:36:05 -0700 Subject: [PATCH 08/11] add back use of all variables for tracking Signed-off-by: Nikolaj Bjorner --- src/test/cnf_backbones.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/test/cnf_backbones.cpp b/src/test/cnf_backbones.cpp index eab91e557..07edabece 100644 --- a/src/test/cnf_backbones.cpp +++ b/src/test/cnf_backbones.cpp @@ -257,6 +257,7 @@ static void cnf_backbones(bool use_chunk, char const* file_name) { vars.push_back(i); g_solver->set_external(i); } + num_vars = g_solver->num_vars(); lbool r; if (use_chunk) { r = core_chunking(*g_solver, vars, assumptions, conseq, 100); From eeb79e1c3c9343f3dcf7a5ec09c2e503abdeec6a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 2 May 2017 19:30:54 -0700 Subject: [PATCH 09/11] update to retain original behavior Signed-off-by: Nikolaj Bjorner --- src/opt/opt_context.cpp | 2 +- src/test/cnf_backbones.cpp | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 1310727aa..d486dfd11 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -406,7 +406,7 @@ namespace opt { if (r == l_true && !get_lower_as_num(i).is_finite()) { return r; } - if (r == l_true && i + 1 < m_objectives.size()) { + if (r == l_true && i + 1 < m_objectives.size() && get_lower_as_num(i).is_finite()) { update_lower(); } } diff --git a/src/test/cnf_backbones.cpp b/src/test/cnf_backbones.cpp index 07edabece..14fc594b6 100644 --- a/src/test/cnf_backbones.cpp +++ b/src/test/cnf_backbones.cpp @@ -252,12 +252,12 @@ static void cnf_backbones(bool use_chunk, char const* file_name) { vector tracking_clauses; track_clauses(solver, solver2, assumptions, tracking_clauses); } - + // remove this line to limit variables to exclude assumptions + num_vars = g_solver->num_vars(); for (unsigned i = 1; i < num_vars; ++i) { vars.push_back(i); g_solver->set_external(i); } - num_vars = g_solver->num_vars(); lbool r; if (use_chunk) { r = core_chunking(*g_solver, vars, assumptions, conseq, 100); From cc7a176c8936162be94235a6277c93bf7d96fd2f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 2 May 2017 19:32:03 -0700 Subject: [PATCH 10/11] update to retain original behavior Signed-off-by: Nikolaj Bjorner --- src/opt/opt_context.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index d486dfd11..1310727aa 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -406,7 +406,7 @@ namespace opt { if (r == l_true && !get_lower_as_num(i).is_finite()) { return r; } - if (r == l_true && i + 1 < m_objectives.size() && get_lower_as_num(i).is_finite()) { + if (r == l_true && i + 1 < m_objectives.size()) { update_lower(); } } From 1177be63913b2813f667d7202f09fe31f4a9688e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 2 May 2017 20:52:39 -0700 Subject: [PATCH 11/11] add common utility to set up seq Signed-off-by: Nikolaj Bjorner --- src/smt/smt_setup.cpp | 30 +++++++++++++++++++----------- src/smt/smt_setup.h | 3 ++- 2 files changed, 21 insertions(+), 12 deletions(-) diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 84e3dee32..820159d18 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -205,7 +205,7 @@ namespace smt { void setup::setup_QF_BVRE() { setup_QF_BV(); setup_QF_LIA(); - m_context.register_plugin(alloc(theory_seq, m_manager)); + setup_seq(); } void setup::setup_QF_UF(static_features const & st) { @@ -705,7 +705,7 @@ namespace smt { } void setup::setup_QF_S() { - m_context.register_plugin(alloc(smt::theory_seq, m_manager)); + setup_seq(); } bool is_arith(static_features const & st) { @@ -822,19 +822,23 @@ namespace smt { m_context.register_plugin(mk_theory_dl(m_manager)); } - void setup::setup_seq(static_features const & st) { + void setup::setup_seq_str(static_features const & st) { // check params for what to do here when it's ambiguous if (m_params.m_string_solver == "z3str3") { setup_str(); - } else if (m_params.m_string_solver == "seq") { - m_context.register_plugin(alloc(smt::theory_seq, m_manager)); - } else if (m_params.m_string_solver == "auto") { + } + else if (m_params.m_string_solver == "seq") { + setup_seq(); + } + else if (m_params.m_string_solver == "auto") { if (st.m_has_seq_non_str) { - m_context.register_plugin(alloc(smt::theory_seq, m_manager)); - } else { + setup_seq(); + } + else { setup_str(); } - } else { + } + else { throw default_exception("invalid parameter for smt.string_solver, valid options are 'z3str3', 'seq', 'auto'"); } } @@ -852,6 +856,10 @@ namespace smt { m_context.register_plugin(alloc(smt::theory_seq, m_manager)); } + void setup::setup_seq() { + m_context.register_plugin(alloc(smt::theory_seq, m_manager)); + } + void setup::setup_unknown() { static_features st(m_manager); st.collect(m_context.get_num_asserted_formulas(), m_context.get_asserted_formulas()); @@ -861,7 +869,7 @@ namespace smt { setup_bv(); setup_datatypes(); setup_dl(); - setup_seq(st); + setup_seq_str(st); setup_card(); setup_fpa(); } @@ -876,7 +884,7 @@ namespace smt { setup_datatypes(); setup_bv(); setup_dl(); - setup_seq(st); + setup_seq_str(st); setup_card(); setup_fpa(); return; diff --git a/src/smt/smt_setup.h b/src/smt/smt_setup.h index d30c896e5..80d5d7d1b 100644 --- a/src/smt/smt_setup.h +++ b/src/smt/smt_setup.h @@ -94,7 +94,8 @@ namespace smt { void setup_bv(); void setup_arith(); void setup_dl(); - void setup_seq(static_features const & st); + void setup_seq_str(static_features const & st); + void setup_seq(); void setup_card(); void setup_i_arith(); void setup_mi_arith();