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

Update inc_sat_solver.cpp

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-06-11 15:40:11 -07:00 • committed by GitHub
parent 5aa06b6333
commit de028f33a2
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
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 { unsigned get_assign_level(expr* e) const override {
expr* atom = e; m.is_not(e, e);
m.is_not(e, atom); sat::bool_var bv = m_map.to_bool_var(e);
sat::bool_var bv = m_map.to_bool_var(atom);
return bv == sat::null_bool_var ? UINT_MAX : m_solver.lvl(bv); return bv == sat::null_bool_var ? UINT_MAX : m_solver.lvl(bv);
} }
bool is_relevant(expr* e) const override { bool is_relevant(expr* e) const override {
expr* atom = e; m.is_not(e, e);
m.is_not(e, atom); sat::bool_var bv = m_map.to_bool_var(e);
sat::bool_var bv = m_map.to_bool_var(atom);
if (bv == sat::null_bool_var) if (bv == sat::null_bool_var)
return true; return true;
auto* ext = dynamic_cast<euf::solver*>(m_solver.get_extension()); auto* ext = dynamic_cast<euf::solver*>(m_solver.get_extension());
@ -427,9 +425,8 @@ public:
} }
unsigned get_bool_var(expr* e) const override { unsigned get_bool_var(expr* e) const override {
expr* atom = e; m.is_not(e, e);
m.is_not(e, atom); auto bv = m_map.to_bool_var(atom);
sat::bool_var bv = m_map.to_bool_var(atom);
return bv == sat::null_bool_var ? UINT_MAX : bv; return bv == sat::null_bool_var ? UINT_MAX : bv;
} }