mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
Move merge_tf handling to euf_internalize
literals true/false are not necessarily created when the merge flag is set. Also disable merge_tf for if-then-else expressions Perhaps even not insert children of if expressions into congruence table?
This commit is contained in:
parent
eceeb295fc
commit
15dc7b78a0
|
@ -36,10 +36,8 @@ namespace euf {
|
|||
}
|
||||
m_expr2enode.setx(f->get_id(), n, nullptr);
|
||||
push_node(n);
|
||||
for (unsigned i = 0; i < num_args; ++i) {
|
||||
set_cgc_enabled(args[i], true);
|
||||
set_merge_tf_enabled(args[i], true);
|
||||
}
|
||||
for (unsigned i = 0; i < num_args; ++i)
|
||||
set_cgc_enabled(args[i], true);
|
||||
return n;
|
||||
}
|
||||
|
||||
|
@ -271,12 +269,6 @@ namespace euf {
|
|||
if (enable_merge_tf != n->merge_tf()) {
|
||||
n->set_merge_tf(enable_merge_tf);
|
||||
m_updates.push_back(update_record(n, update_record::toggle_merge_tf()));
|
||||
if (enable_merge_tf && n->value() != l_undef && !m.is_value(n->get_root()->get_expr())) {
|
||||
expr* b = n->value() == l_true ? m.mk_true() : m.mk_false();
|
||||
enode* tf = find(b);
|
||||
if (tf)
|
||||
add_literal(n, tf);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
@ -474,6 +474,33 @@ namespace euf {
|
|||
enode* n = m_egraph.mk(e, m_generation, num, args);
|
||||
if (si.is_bool_op(e))
|
||||
m_egraph.set_cgc_enabled(n, false);
|
||||
|
||||
//
|
||||
// (if p th el) (non-Boolean case) produces clauses
|
||||
// (=> p (= (if p th el) th))
|
||||
// and (=> (not p) (= (if p th el) el))
|
||||
// The clauses establish equalities between the ite term and
|
||||
// the th or el sub-terms.
|
||||
//
|
||||
if (m.is_ite(e))
|
||||
num = 0;
|
||||
|
||||
//
|
||||
// To track congruences of Boolean children under non-Boolean
|
||||
// functions set the merge_tf flag to true.
|
||||
//
|
||||
for (unsigned i = 0; i < num; ++i) {
|
||||
if (!m.is_bool(args[i]->get_sort()))
|
||||
continue;
|
||||
bool was_enabled = args[i]->merge_tf();
|
||||
m_egraph.set_merge_tf_enabled(args[i], true);
|
||||
if (!was_enabled && n->value() != l_undef && !m.is_value(n->get_root()->get_expr())) {
|
||||
if (n->value() == l_true)
|
||||
m_egraph.merge(n, mk_true(), to_ptr(sat::literal(n->bool_var())));
|
||||
else
|
||||
m_egraph.merge(n, mk_false(), to_ptr(~sat::literal(n->bool_var())));
|
||||
}
|
||||
}
|
||||
return n;
|
||||
}
|
||||
|
||||
|
|
|
@ -146,7 +146,6 @@ namespace euf {
|
|||
|
||||
constraint* m_conflict = nullptr;
|
||||
constraint* m_eq = nullptr;
|
||||
constraint* m_lit = nullptr;
|
||||
|
||||
// proofs
|
||||
bool m_proof_initialized = false;
|
||||
|
@ -266,7 +265,6 @@ namespace euf {
|
|||
~solver() override {
|
||||
if (m_conflict) dealloc(sat::constraint_base::mem2base_ptr(m_conflict));
|
||||
if (m_eq) dealloc(sat::constraint_base::mem2base_ptr(m_eq));
|
||||
if (m_lit) dealloc(sat::constraint_base::mem2base_ptr(m_lit));
|
||||
m_trail.reset();
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue