mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
fix sign bug in internalization of literals
This commit is contained in:
parent
0ef8ebe89f
commit
692bed7991
|
@ -166,30 +166,33 @@ namespace euf {
|
|||
}
|
||||
}
|
||||
|
||||
void ackerman::add_cc(expr* _a, expr* _b) {
|
||||
void ackerman::add_cc(expr* _a, expr* _b) {
|
||||
flet<bool> _is_redundant(s.m_is_redundant, true);
|
||||
app* a = to_app(_a);
|
||||
app* b = to_app(_b);
|
||||
TRACE("ack", tout << mk_pp(a, m) << " " << mk_pp(b, m) << "\n";);
|
||||
sat::literal_vector lits;
|
||||
unsigned sz = a->get_num_args();
|
||||
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
expr_ref eq(m.mk_eq(a->get_arg(i), b->get_arg(i)), m);
|
||||
lits.push_back(s.internalize(eq, true, false, true));
|
||||
lits.push_back(~s.mk_literal(eq));
|
||||
}
|
||||
expr_ref eq(m.mk_eq(a, b), m);
|
||||
lits.push_back(s.internalize(eq, false, false, true));
|
||||
lits.push_back(s.mk_literal(eq));
|
||||
s.s().mk_clause(lits, sat::status::th(true, m.get_basic_family_id()));
|
||||
}
|
||||
|
||||
void ackerman::add_eq(expr* a, expr* b, expr* c) {
|
||||
flet<bool> _is_redundant(s.m_is_redundant, true);
|
||||
sat::literal lits[3];
|
||||
expr_ref eq1(m.mk_eq(a, c), m);
|
||||
expr_ref eq2(m.mk_eq(b, c), m);
|
||||
expr_ref eq3(m.mk_eq(a, b), m);
|
||||
TRACE("ack", tout << mk_pp(a, m) << " " << mk_pp(b, m) << " " << mk_pp(c, m) << "\n";);
|
||||
lits[0] = s.internalize(eq1, true, false, true);
|
||||
lits[1] = s.internalize(eq2, true, false, true);
|
||||
lits[2] = s.internalize(eq3, false, false, true);
|
||||
lits[0] = ~s.mk_literal(eq1);
|
||||
lits[1] = ~s.mk_literal(eq2);
|
||||
lits[2] = s.mk_literal(eq3);
|
||||
s.s().mk_clause(3, lits, sat::status::th(true, m.get_basic_family_id()));
|
||||
}
|
||||
}
|
||||
|
|
|
@ -41,15 +41,19 @@ namespace euf {
|
|||
euf::enode* n = get_enode(e);
|
||||
if (n) {
|
||||
if (m.is_bool(e)) {
|
||||
VERIFY(!s().was_eliminated(n->bool_var()));
|
||||
SASSERT(!s().was_eliminated(n->bool_var()));
|
||||
SASSERT(n->bool_var() != UINT_MAX);
|
||||
return literal(n->bool_var(), sign);
|
||||
}
|
||||
TRACE("euf", tout << "non-bool\n";);
|
||||
return sat::null_literal;
|
||||
}
|
||||
if (si.is_bool_op(e))
|
||||
return attach_lit(si.internalize(e, redundant), e);
|
||||
if (si.is_bool_op(e)) {
|
||||
sat::literal lit = attach_lit(si.internalize(e, redundant), e);
|
||||
if (sign)
|
||||
lit.neg();
|
||||
return lit;
|
||||
}
|
||||
if (auto* ext = expr2solver(e))
|
||||
return ext->internalize(e, sign, root, redundant);
|
||||
if (!visit_rec(m, e, sign, root, redundant)) {
|
||||
|
@ -180,7 +184,7 @@ namespace euf {
|
|||
for (unsigned i = 0; i < sz; ++i) {
|
||||
for (unsigned j = i + 1; j < sz; ++j) {
|
||||
expr_ref eq = mk_eq(args[i]->get_expr(), args[j]->get_expr());
|
||||
sat::literal lit = internalize(eq, false, false, m_is_redundant);
|
||||
sat::literal lit = mk_literal(eq);
|
||||
lits.push_back(lit);
|
||||
}
|
||||
}
|
||||
|
@ -203,7 +207,7 @@ namespace euf {
|
|||
expr_ref fapp(m.mk_app(f, arg), m);
|
||||
expr_ref gapp(m.mk_app(g, fapp.get()), m);
|
||||
expr_ref eq = mk_eq(gapp, arg);
|
||||
sat::literal lit = internalize(eq, false, false, m_is_redundant);
|
||||
sat::literal lit = mk_literal(eq);
|
||||
s().add_clause(1, &lit, st);
|
||||
eqs.push_back(mk_eq(fapp, a));
|
||||
}
|
||||
|
@ -229,7 +233,7 @@ namespace euf {
|
|||
for (unsigned i = 0; i < sz; ++i) {
|
||||
for (unsigned j = i + 1; j < sz; ++j) {
|
||||
expr_ref eq = mk_eq(args[i]->get_expr(), args[j]->get_expr());
|
||||
sat::literal lit = internalize(eq, true, false, m_is_redundant);
|
||||
sat::literal lit = ~mk_literal(eq);
|
||||
s().add_clause(1, &lit, st);
|
||||
if (relevancy_enabled())
|
||||
add_root(1, &lit);
|
||||
|
@ -248,7 +252,7 @@ namespace euf {
|
|||
enode* n = m_egraph.mk(fresh, 0, nullptr);
|
||||
n->mark_interpreted();
|
||||
expr_ref eq = mk_eq(fapp, fresh);
|
||||
sat::literal lit = internalize(eq, false, false, m_is_redundant);
|
||||
sat::literal lit = mk_literal(eq);
|
||||
s().add_clause(1, &lit, st);
|
||||
if (relevancy_enabled())
|
||||
add_root(1, &lit);
|
||||
|
@ -263,7 +267,7 @@ namespace euf {
|
|||
if (!m.is_bool(e) && m.is_ite(e, c, th, el)) {
|
||||
app* a = to_app(e);
|
||||
expr_ref eq_th = mk_eq(a, th);
|
||||
sat::literal lit_th = internalize(eq_th, false, false, m_is_redundant);
|
||||
sat::literal lit_th = mk_literal(eq_th);
|
||||
if (th == el) {
|
||||
s().add_clause(1, &lit_th, st);
|
||||
}
|
||||
|
@ -273,7 +277,7 @@ namespace euf {
|
|||
|
||||
expr_ref eq_el = mk_eq(a, el);
|
||||
|
||||
sat::literal lit_el = internalize(eq_el, false, false, m_is_redundant);
|
||||
sat::literal lit_el = mk_literal(eq_el);
|
||||
literal lits1[2] = { literal(v, true), lit_th };
|
||||
literal lits2[2] = { literal(v, false), lit_el };
|
||||
s().add_clause(2, lits1, st);
|
||||
|
|
|
@ -309,7 +309,9 @@ namespace euf {
|
|||
expr_ref mk_eq(expr* e1, expr* e2);
|
||||
expr_ref mk_eq(euf::enode* n1, euf::enode* n2) { return mk_eq(n1->get_expr(), n2->get_expr()); }
|
||||
euf::enode* mk_enode(expr* e, unsigned n, enode* const* args) { return m_egraph.mk(e, n, args); }
|
||||
expr* bool_var2expr(sat::bool_var v) { return m_bool_var2expr.get(v, nullptr); }
|
||||
expr* bool_var2expr(sat::bool_var v) const { return m_bool_var2expr.get(v, nullptr); }
|
||||
expr_ref literal2expr(sat::literal lit) const { expr* e = bool_var2expr(lit.var()); return lit.sign() ? expr_ref(m.mk_not(e), m) : expr_ref(e, m); }
|
||||
|
||||
sat::literal attach_lit(sat::literal lit, expr* e);
|
||||
void unhandled_function(func_decl* f);
|
||||
th_rewriter& get_rewriter() { return m_rewriter; }
|
||||
|
|
|
@ -81,6 +81,10 @@ namespace euf {
|
|||
return ctx.bool_var2expr(v);
|
||||
}
|
||||
|
||||
expr_ref th_euf_solver::literal2expr(sat::literal lit) const {
|
||||
return ctx.literal2expr(lit);
|
||||
}
|
||||
|
||||
theory_var th_euf_solver::mk_var(enode * n) {
|
||||
force_push();
|
||||
SASSERT(!is_attached_to_var(n));
|
||||
|
|
|
@ -177,8 +177,8 @@ namespace euf {
|
|||
enode* var2enode(theory_var v) const { return m_var2enode[v]; }
|
||||
expr* var2expr(theory_var v) const { return var2enode(v)->get_expr(); }
|
||||
expr* bool_var2expr(sat::bool_var v) const;
|
||||
expr_ref literal2expr(sat::literal lit) const;
|
||||
enode* bool_var2enode(sat::bool_var v) const { expr* e = bool_var2expr(v); return e ? expr2enode(e) : nullptr; }
|
||||
expr_ref literal2expr(sat::literal lit) const { expr* e = bool_var2expr(lit.var()); return lit.sign() ? expr_ref(m.mk_not(e), m) : expr_ref(e, m); }
|
||||
sat::literal mk_literal(expr* e) const;
|
||||
theory_var get_th_var(enode* n) const { return n->get_th_var(get_id()); }
|
||||
theory_var get_th_var(expr* e) const;
|
||||
|
|
Loading…
Reference in a new issue