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

signatrue update

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-06-11 15:59:08 -07:00
parent 6b91b5a1dd
commit 9485e96416
1 changed files with 6 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -424,25 +424,24 @@ public:
return m_solver.num_vars();
}
unsigned get_bool_var(expr* e) const override {
sat::bool_var get_bool_var(expr* e) const override {
m.is_not(e, e);
auto bv = m_map.to_bool_var(atom);
return bv == sat::null_bool_var ? UINT_MAX : bv;
return m_map.to_bool_var(e);
}
expr* bool_var2expr(unsigned v) const override {
expr* bool_var2expr(sat::bool_var v) const override {
return v < m_solver.num_vars() ? m_map.bool_var2expr(v) : nullptr;
}
lbool get_assignment(unsigned v) const override {
lbool get_assignment(sat::bool_var v) const override {
return v < m_solver.num_vars() ? m_solver.value(v) : l_undef;
}
double get_activity(unsigned v) const override {
double get_activity(sat::bool_var v) const override {
return v < m_solver.num_vars() ? static_cast<double>(m_solver.get_activity(v)) : 0.0;
}
bool was_eliminated(unsigned v) const override {
bool was_eliminated(sat::bool_var v) const override {
return v < m_solver.num_vars() && m_solver.was_eliminated(v);
}