mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
This commit is contained in:
parent
9c91698201
commit
3021da87cf
|
@ -581,6 +581,17 @@ namespace arith {
|
|||
value = ~value;
|
||||
if (!found_bad && value == get_phase(n->bool_var()))
|
||||
continue;
|
||||
|
||||
TRACE("arith",
|
||||
ptr_vector<expr> nodes;
|
||||
nodes.push_back(n->get_expr());
|
||||
for (unsigned i = 0; i < nodes.size(); ++i) {
|
||||
expr* r = nodes[i];
|
||||
if (is_app(r))
|
||||
for (expr* arg : *to_app(r))
|
||||
nodes.push_back(arg);
|
||||
tout << r->get_id() << ": " << mk_bounded_pp(r, m, 1) << " := " << mdl(r) << "\n";
|
||||
});
|
||||
TRACE("arith",
|
||||
tout << eval << " " << value << " " << ctx.bpp(n) << "\n";
|
||||
tout << mdl << "\n";
|
||||
|
|
|
@ -85,7 +85,7 @@ namespace euf {
|
|||
if (auto* s = expr2solver(e))
|
||||
s->internalize(e, m_is_redundant);
|
||||
else
|
||||
attach_node(m_egraph.mk(e, m_generation, 0, nullptr));
|
||||
attach_node(mk_enode(e, 0, nullptr));
|
||||
return true;
|
||||
}
|
||||
|
||||
|
@ -100,7 +100,7 @@ namespace euf {
|
|||
if (auto* s = expr2solver(e))
|
||||
s->internalize(e, m_is_redundant);
|
||||
else
|
||||
attach_node(m_egraph.mk(e, m_generation, num, m_args.data()));
|
||||
attach_node(mk_enode(e, num, m_args.data()));
|
||||
return true;
|
||||
}
|
||||
|
||||
|
@ -159,7 +159,7 @@ namespace euf {
|
|||
m_var_trail.push_back(v);
|
||||
enode* n = m_egraph.find(e);
|
||||
if (!n) {
|
||||
n = m_egraph.mk(e, m_generation, 0, nullptr);
|
||||
n = mk_enode(e, 0, nullptr);
|
||||
}
|
||||
SASSERT(n->bool_var() == sat::null_bool_var || n->bool_var() == v);
|
||||
m_egraph.set_bool_var(n, v);
|
||||
|
@ -263,7 +263,7 @@ namespace euf {
|
|||
for (unsigned i = 0; i < sz; ++i) {
|
||||
expr_ref fapp(m.mk_app(f, e->get_arg(i)), m);
|
||||
expr_ref fresh(m.mk_fresh_const("dist-value", u), m);
|
||||
enode* n = m_egraph.mk(fresh, m_generation, 0, nullptr);
|
||||
enode* n = mk_enode(fresh, 0, nullptr);
|
||||
n->mark_interpreted();
|
||||
expr_ref eq = mk_eq(fapp, fresh);
|
||||
sat::literal lit = mk_literal(eq);
|
||||
|
@ -429,4 +429,26 @@ namespace euf {
|
|||
return n;
|
||||
}
|
||||
|
||||
euf::enode* solver::mk_enode(expr* e, unsigned n, enode* const* args) {
|
||||
euf::enode* r = m_egraph.mk(e, m_generation, n, args);
|
||||
for (unsigned i = 0; i < n; ++i)
|
||||
ensure_merged_tf(args[i]);
|
||||
return r;
|
||||
}
|
||||
|
||||
void solver::ensure_merged_tf(euf::enode* n) {
|
||||
switch (n->value()) {
|
||||
case l_undef:
|
||||
break;
|
||||
case l_true:
|
||||
if (n->get_root() != mk_true())
|
||||
m_egraph.merge(n, mk_true(), to_ptr(sat::literal(n->bool_var())));
|
||||
break;
|
||||
case l_false:
|
||||
if (n->get_root() != mk_false())
|
||||
m_egraph.merge(n, mk_false(), to_ptr(~sat::literal(n->bool_var())));
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
}
|
||||
|
|
|
@ -127,6 +127,7 @@ namespace euf {
|
|||
void add_not_distinct_axiom(app* e, euf::enode* const* args);
|
||||
void axiomatize_basic(enode* n);
|
||||
bool internalize_root(app* e, bool sign, ptr_vector<enode> const& args);
|
||||
void ensure_merged_tf(euf::enode* n);
|
||||
euf::enode* mk_true();
|
||||
euf::enode* mk_false();
|
||||
|
||||
|
@ -349,7 +350,7 @@ 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* e_internalize(expr* e);
|
||||
euf::enode* mk_enode(expr* e, unsigned n, enode* const* args) { return m_egraph.mk(e, m_generation, n, args); }
|
||||
euf::enode* mk_enode(expr* e, unsigned n, enode* const* 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 (e && lit.sign()) ? expr_ref(m.mk_not(e), m) : expr_ref(e, m); }
|
||||
unsigned generation() const { return m_generation; }
|
||||
|
|
Loading…
Reference in a new issue