mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-22 16:40:29 +00:00
Code Activity

rejection of invalid split atoms happens DURING selection of split atoms, not as a post-processing step, just like smt_parallel does. this requires changing the shape of the cube function so I've moved this to a second function, cube_vsids, for now and restored the original cube/lookahead functions to master branch. this should hopefully give a perf bump due to eliminating needless postprocessing

Browse source
This commit is contained in:
Ilana Shapiro 2026-06-21 12:37:47 -07:00
parent ac12384d00
commit 85fa14774a
4 changed files with 101 additions and 113 deletions
Download patch file Download diff file Expand all files Collapse all files

75
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -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<expr> 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<solver::scored_literal>& candidates, unsigned max_num) override {
if (!is_internalized()) {
lbool r = internalize_formulas();

73
src/smt/smt_solver.cpp
View file

@ -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 <algorithm>
@ -444,45 +443,8 @@ namespace {
void solve_for(vector<solver::solution>& 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<expr> 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<expr> 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;

64
src/solver/parallel_tactical2.cpp
View file

@ -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<expr> 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<expr> 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())

2
src/solver/solver.h
View file

@ -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.
*/