mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-19 07:06:28 +00:00
Code Activity

Merge branch 'solver_parallel' of https://github.com/z3prover/z3 into solver_parallel

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-06-11 15:54:04 -07:00
commit 6b91b5a1dd
1 changed files with 6 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -406,16 +406,14 @@ public:
}
unsigned get_assign_level(expr* e) const override {
expr* atom = e;
m.is_not(e, atom);
sat::bool_var bv = m_map.to_bool_var(atom);
m.is_not(e, e);
sat::bool_var bv = m_map.to_bool_var(e);
return bv == sat::null_bool_var ? UINT_MAX : m_solver.lvl(bv);
}
bool is_relevant(expr* e) const override {
expr* atom = e;
m.is_not(e, atom);
sat::bool_var bv = m_map.to_bool_var(atom);
m.is_not(e, e);
sat::bool_var bv = m_map.to_bool_var(e);
if (bv == sat::null_bool_var)
return true;
auto* ext = dynamic_cast<euf::solver*>(m_solver.get_extension());
@ -427,9 +425,8 @@ public:
}
unsigned get_bool_var(expr* e) const override {
expr* atom = e;
m.is_not(e, atom);
sat::bool_var bv = m_map.to_bool_var(atom);
m.is_not(e, e);
auto bv = m_map.to_bool_var(atom);
return bv == sat::null_bool_var ? UINT_MAX : bv;
}