mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
This commit is contained in:
parent
a566c7307d
commit
5633af76cc
|
@ -277,7 +277,7 @@ namespace arith {
|
|||
if (is_app(n)) {
|
||||
internalize_args(to_app(n));
|
||||
for (expr* arg : *to_app(n))
|
||||
if (a.is_arith_expr(arg))
|
||||
if (a.is_arith_expr(arg) && !m.is_bool(arg))
|
||||
internalize_term(arg);
|
||||
}
|
||||
theory_var v = mk_evar(n);
|
||||
|
|
|
@ -158,8 +158,9 @@ namespace euf {
|
|||
m_bool_var2expr[v] = e;
|
||||
m_var_trail.push_back(v);
|
||||
enode* n = m_egraph.find(e);
|
||||
if (!n)
|
||||
n = m_egraph.mk(e, m_generation, 0, nullptr);
|
||||
if (!n) {
|
||||
n = m_egraph.mk(e, m_generation, 0, nullptr);
|
||||
}
|
||||
SASSERT(n->bool_var() == sat::null_bool_var || n->bool_var() == v);
|
||||
m_egraph.set_bool_var(n, v);
|
||||
if (m.is_eq(e) || m.is_or(e) || m.is_and(e) || m.is_not(e))
|
||||
|
@ -419,4 +420,13 @@ namespace euf {
|
|||
return g;
|
||||
}
|
||||
|
||||
euf::enode* solver::e_internalize(expr* e) {
|
||||
euf::enode* n = m_egraph.find(e);
|
||||
if (!n) {
|
||||
internalize(e, m_is_redundant);
|
||||
n = m_egraph.find(e);
|
||||
}
|
||||
return n;
|
||||
}
|
||||
|
||||
}
|
||||
|
|
|
@ -584,14 +584,16 @@ namespace euf {
|
|||
TRACE("euf", for (auto const& kv : replay.m) tout << kv.m_value << "\n";);
|
||||
for (auto const& [e, generation, v] : m_reinit) {
|
||||
scoped_generation _sg(*this, generation);
|
||||
TRACE("euf", tout << "replay: " << v << " " << mk_bounded_pp(e, m) << "\n";);
|
||||
TRACE("euf", tout << "replay: " << v << " " << e->get_id() << " " << mk_bounded_pp(e, m) << " " << si.is_bool_op(e) << "\n";);
|
||||
sat::literal lit;
|
||||
if (si.is_bool_op(e))
|
||||
lit = literal(replay.m[e], false);
|
||||
else
|
||||
lit = si.internalize(e, true);
|
||||
VERIFY(lit.var() == v);
|
||||
|
||||
VERIFY(lit.var() == v);
|
||||
if (is_app(e))
|
||||
for (expr* arg : *to_app(e))
|
||||
e_internalize(arg);
|
||||
attach_lit(lit, e);
|
||||
}
|
||||
|
||||
|
|
|
@ -348,6 +348,7 @@ namespace euf {
|
|||
void attach_node(euf::enode* n);
|
||||
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* e_internalize(expr* e);
|
||||
euf::enode* mk_enode(expr* e, unsigned n, enode* const* args) { return m_egraph.mk(e, m_generation, n, args); }
|
||||
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); }
|
||||
|
|
|
@ -218,12 +218,7 @@ namespace euf {
|
|||
}
|
||||
|
||||
euf::enode* th_euf_solver::e_internalize(expr* e) {
|
||||
euf::enode* n = expr2enode(e);
|
||||
if (!n) {
|
||||
ctx.internalize(e, m_is_redundant);
|
||||
n = expr2enode(e);
|
||||
}
|
||||
return n;
|
||||
return ctx.e_internalize(e);
|
||||
}
|
||||
|
||||
unsigned th_euf_solver::random() {
|
||||
|
|
Loading…
Reference in a new issue