diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 95664a4fe..525a2bbbe 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -500,38 +500,8 @@ public: vars.push_back(kv.m_value); } sat::literal_vector lits; - expr_ref_vector fmls(m); - parallel_params pp(m_params); - if (!pp.cube_lookahead()) { - sat::bool_var_vector candidates; - sat::bool_var result = sat::null_bool_var; - double score = 0.0; - unsigned n = 0; - unsigned search_lvl = m_solver.search_lvl(); - for (sat::bool_var v : vars) { - if (was_eliminated(v)) - continue; - if (get_assignment(v) != l_undef && m_solver.lvl(v) <= search_lvl) - continue; - candidates.push_back(v); - double new_score = get_activity(v); - if (new_score > score || result == sat::null_bool_var || (new_score == score && m_solver.rand()(++n) == 0)) { - score = new_score; - result = v; - } - } - vs.reset(); - for (sat::bool_var v : candidates) { - expr* e = bool_var2expr(v); - if (e) - vs.push_back(e); - } - expr* e = result == sat::null_bool_var ? nullptr : bool_var2expr(result); - if (e) - fmls.push_back(e); - return fmls; - } lbool result = m_solver.cube(vars, lits, backtrack_level); + expr_ref_vector fmls(m); expr_ref_vector lit2expr(m); lit2expr.resize(m_solver.num_vars() * 2); m_map.mk_inv(lit2expr); @@ -561,6 +531,49 @@ public: return fmls; } + expr_ref cube_vsids(expr_ref_vector const& invalid_split_atoms) override { + if (!is_internalized()) { + lbool r = internalize_formulas(); + if (r != l_true) + return expr_ref(m); + } + convert_internalized(); + if (m_solver.inconsistent()) + return expr_ref(m); + + obj_hashtable invalid_split_atoms_set; + for (expr* e : invalid_split_atoms) { + expr* atom = e; + m.is_not(e, atom); + invalid_split_atoms_set.insert(atom); + } + + expr_ref result(m); + double score = 0.0; + unsigned n = 0; + unsigned search_lvl = m_solver.search_lvl(); + for (auto& kv : m_map) { + sat::bool_var v = kv.m_value; + if (was_eliminated(v)) + continue; + if (get_assignment(v) != l_undef && m_solver.lvl(v) <= search_lvl) + continue; + expr* e = kv.m_key; + if (!e) + continue; + expr* atom = e; + m.is_not(e, atom); + if (invalid_split_atoms_set.contains(atom)) + continue; + double new_score = get_activity(v); + if (new_score > score || !result || (new_score == score && m_solver.rand()(++n) == 0)) { + score = new_score; + result = e; + } + } + return result; + } + void get_backbone_candidates(vector& candidates, unsigned max_num) override { if (!is_internalized()) { lbool r = internalize_formulas(); diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index fb9edfdcb..393fff202 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -27,7 +27,6 @@ Notes: #include "params/smt_params.h" #include "params/smt_params_helper.hpp" #include "solver/solver_na2as.h" -#include "solver/parallel_params.hpp" #include "solver/mus.h" #include @@ -444,45 +443,8 @@ namespace { void solve_for(vector& s) override { m_context.solve_for(s); } - expr_ref_vector cube(expr_ref_vector& vars, unsigned backtrack_level) override { + expr_ref_vector cube(expr_ref_vector& vars, unsigned cutoff) override { ast_manager& m = get_manager(); - parallel_params pp(get_params()); - if (!pp.cube_lookahead()) { - auto& ctx = m_context.get_context(); - obj_hashtable selected_vars; - for (expr* v : vars) - selected_vars.insert(v); - expr_ref_vector candidates(m); - expr_ref result(m); - double score = 0.0; - unsigned n = 0; - - ctx.pop_to_search_level(); - for (unsigned v = 0; v < ctx.get_num_bool_vars(); ++v) { - if (ctx.get_assignment(v) != l_undef) - continue; - expr* e = ctx.bool_var2expr(v); - if (!e) - continue; - if (!selected_vars.empty() && !selected_vars.contains(e)) - continue; - candidates.push_back(e); - double new_score = ctx.get_activity(v); - if (new_score > score || !result || (new_score == score && m_rand(++n) == 0)) { - score = new_score; - result = e; - } - } - - vars.reset(); - vars.append(candidates); - - expr_ref_vector lits(m); - if (result) - lits.push_back(result); - return lits; - } - if (!m_cuber) { m_cuber = alloc(cuber, *this); // force propagation @@ -504,6 +466,39 @@ namespace { return lits; } + expr_ref cube_vsids(expr_ref_vector const& invalid_split_atoms) override { + ast_manager& m = get_manager(); + auto& ctx = m_context.get_context(); + obj_hashtable invalid_split_atoms_set; + for (expr* e : invalid_split_atoms) { + expr* atom = e; + m.is_not(e, atom); + invalid_split_atoms_set.insert(atom); + } + expr_ref result(m); + double score = 0.0; + unsigned n = 0; + + ctx.pop_to_search_level(); + for (unsigned v = 0; v < ctx.get_num_bool_vars(); ++v) { + if (ctx.get_assignment(v) != l_undef) + continue; + expr* e = ctx.bool_var2expr(v); + if (!e) + continue; + expr* atom = e; + m.is_not(e, atom); + if (invalid_split_atoms_set.contains(atom)) + continue; + double new_score = ctx.get_activity(v); + if (new_score > score || !result || (new_score == score && m_rand(++n) == 0)) { + score = new_score; + result = e; + } + } + return result; + } + struct collect_fds_proc { ast_manager & m; func_decl_set & m_fds; diff --git a/src/solver/parallel_tactical2.cpp b/src/solver/parallel_tactical2.cpp index dafcfa759..1694a5461 100644 --- a/src/solver/parallel_tactical2.cpp +++ b/src/solver/parallel_tactical2.cpp @@ -1097,50 +1097,28 @@ class parallel_solver { if (cube.size() >= m_config.m_max_cube_depth) return result; - expr_ref_vector vars(m); - obj_hashtable rejected_atoms; - try { - while (true) { - expr_ref_vector cands = s->cube(vars, 1); - bool rejected = false; - for (expr* lit : cands) { - if (!lit) - continue; - if (m.is_true(lit) || m.is_false(lit)) - continue; - if (b.path_contains_atom(m_l2g, lease, lit)) { - expr* atom = lit; - m.is_not(lit, atom); - rejected_atoms.insert(atom); - rejected = true; - continue; - } - if (m_config.m_global_backbones && b.is_global_backbone_or_negation(m_l2g, lit)) { - expr* atom = lit; - m.is_not(lit, atom); - rejected_atoms.insert(atom); - rejected = true; - continue; - } - result = lit; - return result; - } - - if (!rejected || vars.empty()) - return result; - - expr_ref_vector next_vars(m); - for (expr* v : vars) { - expr* atom = v; - m.is_not(v, atom); - if (!rejected_atoms.contains(atom)) - next_vars.push_back(v); - } - if (next_vars.empty() || next_vars.size() == vars.size()) - return result; - vars.reset(); - vars.append(next_vars); + obj_hashtable invalid_split_atoms_set; + expr_ref_vector invalid_split_atoms(m); + auto mark_invalid_split_atom = [&](expr* lit) { + expr* atom = lit; + m.is_not(lit, atom); + if (!invalid_split_atoms_set.contains(atom)) { + invalid_split_atoms_set.insert(atom); + invalid_split_atoms.push_back(atom); } + }; + for (expr* lit : cube) { // don't split on atoms already in the cube + mark_invalid_split_atom(lit); + } + if (m_config.m_global_backbones) { // don't split on global backbones or their negations + expr_ref_vector global_backbones = b.get_global_backbones_snapshot(m_g2l); + for (expr* lit : global_backbones) { + mark_invalid_split_atom(lit); + } + } + + try { + return s->cube_vsids(invalid_split_atoms); } catch (...) { if (!m.limit().is_canceled()) diff --git a/src/solver/solver.h b/src/solver/solver.h index df0d11711..556b8b27c 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -257,6 +257,8 @@ public: virtual expr_ref_vector cube(expr_ref_vector& vars, unsigned backtrack_level=0) = 0; + virtual expr_ref cube_vsids(expr_ref_vector const&) { return expr_ref(m); } + /** \brief retrieve congruence closure root. */