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

#5427

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-07-22 12:07:11 -07:00
parent 76427cd281
commit 2589f2bad4
3 changed files with 12 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -211,7 +211,7 @@ namespace euf {
for (sat::literal lit : r) for (sat::literal lit : r)
if (s().lvl(lit) > 0) r[j++] = lit; if (s().lvl(lit) > 0) r[j++] = lit;
r.shrink(j); r.shrink(j);
TRACE("euf", tout << "eplain " << l << " <- " << r << " " << probing << "\n";); TRACE("euf", tout << "explain " << l << " <- " << r << " " << probing << "\n";);
DEBUG_CODE(for (auto lit : r) SASSERT(s().value(lit) == l_true);); DEBUG_CODE(for (auto lit : r) SASSERT(s().value(lit) == l_true););
if (!probing) if (!probing)

2
src/sat/smt/q_clause.h
View file

@ -59,10 +59,12 @@ namespace q {
unsigned m_index; unsigned m_index;
vector<lit> m_lits; vector<lit> m_lits;
quantifier_ref m_q; quantifier_ref m_q;
unsigned m_watch = 0;
sat::literal m_literal = sat::null_literal; sat::literal m_literal = sat::null_literal;
q::quantifier_stat* m_stat = nullptr; q::quantifier_stat* m_stat = nullptr;
binding* m_bindings = nullptr; binding* m_bindings = nullptr;
clause(ast_manager& m, unsigned idx): m_index(idx), m_q(m) {} clause(ast_manager& m, unsigned idx): m_index(idx), m_q(m) {}
std::ostream& display(euf::solver& ctx, std::ostream& out) const; std::ostream& display(euf::solver& ctx, std::ostream& out) const;

20
src/sat/smt/q_eval.cpp
View file

@ -39,40 +39,37 @@ namespace q {
unsigned sz = c.m_lits.size(); unsigned sz = c.m_lits.size();
unsigned n = c.num_decls(); unsigned n = c.num_decls();
m_indirect_nodes.reset(); m_indirect_nodes.reset();
for (unsigned i = 0; i < sz; ++i) { for (unsigned j = 0; j < sz; ++j) {
unsigned i = (j + c.m_watch) % sz;
unsigned lim = m_indirect_nodes.size(); unsigned lim = m_indirect_nodes.size();
lit l = c[i]; lit l = c[i];
lbool cmp = compare(n, binding, l.lhs, l.rhs, evidence); lbool cmp = compare(n, binding, l.lhs, l.rhs, evidence);
std::cout << l.sign << ": " << l.lhs << " ~~ " << l.rhs << " " << cmp << "\n";
switch (cmp) { switch (cmp) {
case l_false: case l_false:
m_indirect_nodes.shrink(lim); m_indirect_nodes.shrink(lim);
if (!l.sign) if (!l.sign)
break; break;
if (i > 0) c.m_watch = i;
std::swap(c[0], c[i]);
return l_true; return l_true;
case l_true: case l_true:
m_indirect_nodes.shrink(lim); m_indirect_nodes.shrink(lim);
if (l.sign) if (l.sign)
break; break;
if (i > 0) c.m_watch = i;
std::swap(c[0], c[i]);
return l_true; return l_true;
case l_undef: case l_undef:
TRACE("q", tout << l.lhs << " ~~ " << l.rhs << " is undef\n";); TRACE("q", tout << l.lhs << " ~~ " << l.rhs << " is undef\n";);
if (idx == 0) { if (idx != UINT_MAX) {
idx = UINT_MAX; idx = UINT_MAX;
return l_undef; return l_undef;
} }
if (i > 0) idx = i;
std::swap(c[0], c[i]);
idx = 0;
break; break;
} }
} }
if (idx == UINT_MAX) if (idx == UINT_MAX)
return l_false; return l_false;
return l_undef; return l_undef;
} }
@ -97,8 +94,9 @@ namespace q {
tout << ctx.bpp(sn) << " " << ctx.bpp(tn) << "\n";); tout << ctx.bpp(sn) << " " << ctx.bpp(tn) << "\n";);
lbool c; lbool c;
if (sn && sn == tn) if (sn && sn == tn)
return l_true; return l_true;
if (sn && tn && ctx.get_egraph().are_diseq(sn, tn)) { if (sn && tn && ctx.get_egraph().are_diseq(sn, tn)) {
evidence.push_back(euf::enode_pair(sn, tn)); evidence.push_back(euf::enode_pair(sn, tn));
return l_false; return l_false;