mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-08-30 12:08:15 -07:00
parent 727ea43b16
commit 9f0b303263
1 changed files with 22 additions and 23 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

39
src/sat/smt/euf_solver.cpp
View file

@ -79,7 +79,7 @@ namespace euf {
} }
bool solver::propagate(literal l, ext_constraint_idx idx) { bool solver::propagate(literal l, ext_constraint_idx idx) {
force_push(); force_push();
auto* ext = sat::constraint_base::to_extension(idx); auto* ext = sat::constraint_base::to_extension(idx);
SASSERT(ext != this); SASSERT(ext != this);
return ext->propagate(l, idx); return ext->propagate(l, idx);
@ -128,10 +128,9 @@ namespace euf {
} }
void solver::asserted(literal l) { void solver::asserted(literal l) {
auto* ext = get_solver(l.var()); auto* ext = get_solver(l.var());
if (ext) { if (ext) {
force_push(); force_push();
ext->asserted(l); ext->asserted(l);
return; return;
} }
@ -139,7 +138,7 @@ namespace euf {
auto p = m_var2node.get(l.var(), enode_bool_pair(nullptr, false)); auto p = m_var2node.get(l.var(), enode_bool_pair(nullptr, false));
if (!p.first) if (!p.first)
return; return;
force_push(); force_push();
bool sign = p.second != l.sign(); bool sign = p.second != l.sign();
euf::enode* n = p.first; euf::enode* n = p.first;
expr* e = n->get_owner(); expr* e = n->get_owner();
@ -200,7 +199,7 @@ namespace euf {
} }
sat::check_result solver::check() { sat::check_result solver::check() {
force_push(); force_push();
bool give_up = false; bool give_up = false;
bool cont = false; bool cont = false;
for (auto* e : m_solvers) for (auto* e : m_solvers)
@ -220,17 +219,17 @@ namespace euf {
++m_num_scopes; ++m_num_scopes;
} }
void solver::force_push() { void solver::force_push() {
for (; m_num_scopes > 0; --m_num_scopes) { for (; m_num_scopes > 0; --m_num_scopes) {
scope s; scope s;
s.m_bool_var_lim = m_bool_var_trail.size(); s.m_bool_var_lim = m_bool_var_trail.size();
s.m_trail_lim = m_trail.size(); s.m_trail_lim = m_trail.size();
m_scopes.push_back(s); m_scopes.push_back(s);
for (auto* e : m_solvers) for (auto* e : m_solvers)
e->push(); e->push();
m_egraph.push(); m_egraph.push();
} }
} }
void solver::pop(unsigned n) { void solver::pop(unsigned n) {
if (n <= m_num_scopes) { if (n <= m_num_scopes) {
@ -242,13 +241,13 @@ namespace euf {
for (auto* e : m_solvers) for (auto* e : m_solvers)
e->pop(n); e->pop(n);
scope & s = m_scopes[m_scopes.size() - n]; scope & s = m_scopes[m_scopes.size() - n];
for (unsigned i = m_bool_var_trail.size(); i-- > s.m_bool_var_lim; ) for (unsigned i = m_bool_var_trail.size(); i-- > s.m_bool_var_lim; )
m_var2node[m_bool_var_trail[i]] = enode_bool_pair(nullptr, false); m_var2node[m_bool_var_trail[i]] = enode_bool_pair(nullptr, false);
m_bool_var_trail.shrink(s.m_bool_var_lim); m_bool_var_trail.shrink(s.m_bool_var_lim);
undo_trail_stack(*this, m_trail, s.m_trail_lim); undo_trail_stack(*this, m_trail, s.m_trail_lim);
m_scopes.shrink(m_scopes.size() - n); m_scopes.shrink(m_scopes.size() - n);
} }
@ -330,7 +329,7 @@ namespace euf {
} }
void solver::pop_reinit() { void solver::pop_reinit() {
force_push(); force_push();
for (auto* e : m_solvers) for (auto* e : m_solvers)
e->pop_reinit(); e->pop_reinit();
} }
@ -409,7 +408,7 @@ namespace euf {
} }
sat::literal solver::internalize(expr* e, bool sign, bool root) { sat::literal solver::internalize(expr* e, bool sign, bool root) {
force_push(); force_push();
auto* ext = get_solver(e); auto* ext = get_solver(e);
if (ext) if (ext)
return ext->internalize(e, sign, root); return ext->internalize(e, sign, root);