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..7f2b75830 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 { @@ -3520,6 +3523,7 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) { 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; @@ -3537,8 +3541,12 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) { 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; @@ -3548,8 +3556,12 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) { 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; } @@ -3558,7 +3570,7 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) { 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/smt/params/smt_params.h b/src/smt/params/smt_params.h index 295e141cc..4b7c924e4 100644 --- a/src/smt/params/smt_params.h +++ b/src/smt/params/smt_params.h @@ -67,7 +67,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, diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index f99c2df16..6c2ff4962 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'), @@ -61,8 +61,9 @@ 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.'), + ('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'), - ('string_solver', SYMBOL, 'auto', 'solver for string/sequence theories. options are: \'z3str3\' (specialized string solver), \'seq\' (sequence solver), \'auto\' (use static features to choose best solver)'), ('str.strong_arrangements', BOOL, True, 'assert equivalences instead of implications when generating string arrangement axioms'), ('str.aggressive_length_testing', BOOL, False, 'prioritize testing concrete length values over generating more options'), ('str.aggressive_value_testing', BOOL, False, 'prioritize testing concrete string constant values over generating more options'), @@ -72,7 +73,6 @@ def_module_params(module_name='smt', ('str.string_constant_cache', BOOL, True, 'cache all generated string constants generated from anywhere in theory_str'), ('str.use_binary_search', BOOL, False, 'use a binary search heuristic for finding concrete length values for free variables in theory_str (set to False to use linear search)'), ('str.binary_search_start', UINT, 64, 'initial upper bound for theory_str binary search'), - ('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.'), ('str.finite_overlap_models', BOOL, False, 'attempt a finite model search for overlapping variables instead of completely giving up on the arrangement'), ('str.overlap_priority', DOUBLE, -0.1, 'theory-aware priority for overlapping variable cases; use smt.theory_aware_branching=true'), 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); } } diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index f6837307a..9c70f5999 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -838,6 +838,7 @@ 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, diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 4d02218bf..a4f2ee646 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -824,19 +824,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(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(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'"); } } @@ -855,6 +859,10 @@ namespace smt { m_context.register_plugin(alloc(theory_str, m_manager, m_params)); } + 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()); @@ -864,7 +872,7 @@ namespace smt { setup_bv(); setup_datatypes(); setup_dl(); - setup_seq(st); + setup_seq_str(st); setup_card(); setup_fpa(); } @@ -879,7 +887,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(); diff --git a/src/test/cnf_backbones.cpp b/src/test/cnf_backbones.cpp index b95977a46..14fc594b6 100644 --- a/src/test/cnf_backbones.cpp +++ b/src/test/cnf_backbones.cpp @@ -246,13 +246,15 @@ 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) { + // 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); }