mirror of
https://github.com/Z3Prover/z3
synced 2025-04-13 20:38:43 +00:00
removed dead code
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
9072d80995
commit
e2f3f9abd7
|
|
@ -2923,214 +2923,6 @@ namespace smt {
|
|||
});
|
||||
}
|
||||
|
||||
lbool context::get_implied_equalities(
|
||||
unsigned num_terms,
|
||||
expr* const* terms,
|
||||
unsigned* class_ids,
|
||||
unsigned num_assumptions,
|
||||
expr * const * assumptions ) {
|
||||
|
||||
if (!validate_assumptions(num_assumptions, assumptions))
|
||||
return l_undef;
|
||||
|
||||
simplifier& simp = get_simplifier();
|
||||
expr_ref_vector sterms(m_manager), vals(m_manager), eqs(m_manager);
|
||||
expr_ref vl(m_manager), eq(m_manager);
|
||||
obj_map<expr, unsigned_vector > vals_map;
|
||||
obj_map<expr, unsigned> visited_roots;
|
||||
flet<bool> f2(m_fparams.m_model, true);
|
||||
flet<bool> f3(m_fparams.m_array_canonize_simplify, true);
|
||||
model_ref m;
|
||||
proof_ref pr(m_manager);
|
||||
union_find_default_ctx df;
|
||||
union_find<union_find_default_ctx> uf(df);
|
||||
lbool r;
|
||||
m_last_search_failure = OK;
|
||||
|
||||
push();
|
||||
for (unsigned i = 0; i < num_terms; ++i) {
|
||||
expr_ref t(m_manager);
|
||||
SASSERT(terms[i]->get_ref_count() > 0);
|
||||
simp(terms[i], t, pr);
|
||||
sterms.push_back(t);
|
||||
if (!e_internalized(t)) {
|
||||
internalize(t, false);
|
||||
}
|
||||
uf.mk_var();
|
||||
}
|
||||
lbool result = check(num_assumptions, assumptions);
|
||||
|
||||
//
|
||||
// extract model in current satisfying state.
|
||||
// The model contains all implied equalities, and
|
||||
// possibly more depending on decisions.
|
||||
//
|
||||
|
||||
if (result == l_false) {
|
||||
pop(1);
|
||||
m_last_search_failure = OK;
|
||||
return result;
|
||||
}
|
||||
failure fail = m_last_search_failure;
|
||||
|
||||
get_model(m);
|
||||
for (unsigned i = 0; i < num_terms; ++i) {
|
||||
enode* e = get_enode(sterms[i].get());
|
||||
expr* owner_root = e->get_root()->get_owner();
|
||||
m->eval(owner_root, vl);
|
||||
vals.push_back(vl);
|
||||
}
|
||||
|
||||
//
|
||||
// pop to base level to undo decision literals.
|
||||
// The congruence closure contains only implied
|
||||
// equalities, but possibly not them all.
|
||||
// Force propagation by using push.
|
||||
//
|
||||
|
||||
pop_to_base_lvl();
|
||||
SASSERT(at_base_level());
|
||||
push();
|
||||
SASSERT(!inconsistent());
|
||||
TRACE("get_implied_equalities", display(tout););
|
||||
|
||||
//
|
||||
// if different enodes evaluate to the same value
|
||||
// in current model,
|
||||
// check if them being disequal is consistent.
|
||||
// otherwise, add equality.
|
||||
//
|
||||
for (unsigned i = 0; i < num_terms; ++i) {
|
||||
SASSERT(at_base_level());
|
||||
enode* e = get_enode(sterms[i].get());
|
||||
expr* owner_root = e->get_root()->get_owner();
|
||||
unsigned idx_j;
|
||||
vl = vals[i].get();
|
||||
TRACE("get_implied_equalities",
|
||||
tout << mk_ll_pp(sterms[i].get(), m_manager) << " |-> ";
|
||||
tout << mk_ll_pp(owner_root, m_manager) << "|-> ";
|
||||
tout << mk_ll_pp(vl, m_manager) << "\n";
|
||||
);
|
||||
if (visited_roots.find(owner_root, idx_j)) {
|
||||
uf.merge(i, idx_j);
|
||||
continue;
|
||||
}
|
||||
visited_roots.insert(owner_root, i);
|
||||
unsigned_vector same_values;
|
||||
if (!vals_map.find(vl, same_values)) {
|
||||
same_values.push_back(i);
|
||||
vals_map.insert(vl, same_values);
|
||||
continue;
|
||||
}
|
||||
bool found_eq = false;
|
||||
for (unsigned j = 0; !found_eq && j < same_values.size(); ++j) {
|
||||
idx_j = same_values[j];
|
||||
enode* other_node = get_enode(sterms[idx_j].get());
|
||||
expr* other_root = other_node->get_root()->get_owner();
|
||||
expr_ref neq(m_manager.mk_not(mk_eq_atom(owner_root, other_root)), m_manager);
|
||||
|
||||
push();
|
||||
assert_expr(neq);
|
||||
r = check(num_assumptions, assumptions);
|
||||
pop(1);
|
||||
|
||||
TRACE("get_implied_equalities", tout << mk_pp(neq, m_manager) << " |-> " << r << "\n";);
|
||||
|
||||
if (r == l_false) {
|
||||
uf.merge(i, idx_j);
|
||||
found_eq = true;
|
||||
}
|
||||
SASSERT(!inconsistent());
|
||||
}
|
||||
if (!found_eq) {
|
||||
same_values.push_back(i);
|
||||
vals_map.insert(vl, same_values);
|
||||
}
|
||||
}
|
||||
SASSERT(!inconsistent());
|
||||
for (unsigned i = 0; i < num_terms; ++i) {
|
||||
unsigned j = uf.find(i);
|
||||
enode* e = get_enode(sterms[j].get());
|
||||
class_ids[i] = e->get_root()->get_owner_id();
|
||||
}
|
||||
TRACE("get_implied_equalities",
|
||||
for (unsigned i = 0; i < num_terms; ++i) {
|
||||
tout << mk_pp(sterms[i].get(), m_manager) << " |-> #" << class_ids[i] << "\n";
|
||||
}
|
||||
display(tout););
|
||||
pop(2);
|
||||
TRACE("get_implied_equalities", display(tout); );
|
||||
|
||||
/*
|
||||
DEBUG_CODE(
|
||||
for (unsigned i = 0; result != l_undef && i < num_terms; ++i) {
|
||||
for (unsigned j = i+1; j < num_terms; ++j) {
|
||||
if (class_ids[i] != class_ids[j]) {
|
||||
expr* e1 = sterms[i].get();
|
||||
expr* e2 = sterms[j].get();
|
||||
if (m_manager.get_sort(e1) != m_manager.get_sort(e2)) {
|
||||
continue;
|
||||
}
|
||||
SASSERT(!inconsistent());
|
||||
expr_ref neq(m_manager.mk_not(mk_eq_atom(e1,e2)), m_manager);
|
||||
|
||||
push();
|
||||
assert_expr(neq);
|
||||
r = check(num_assumptions, assumptions);
|
||||
pop(1);
|
||||
|
||||
if (r == l_false) {
|
||||
enable_trace("array");
|
||||
enable_trace("arith");
|
||||
enable_trace("context");
|
||||
enable_trace("unsat_core_bug");
|
||||
enable_trace("after_search");
|
||||
enable_trace("display_unsat_core");
|
||||
SASSERT(!inconsistent());
|
||||
|
||||
{
|
||||
flet<bool> f3(m_fparams.m_smtlib_dump_assertions, true);
|
||||
unsigned sz = m_asserted_formulas.get_num_formulas();
|
||||
for (unsigned l = 0; l < sz; ++l) {
|
||||
expr * f = m_asserted_formulas.get_formula(l);
|
||||
save_assertion_for_pp(f);
|
||||
}
|
||||
save_assertion_for_pp(neq);
|
||||
display_assertions_as_smt_problem();
|
||||
}
|
||||
|
||||
push();
|
||||
assert_expr(neq);
|
||||
r = check(num_assumptions, assumptions);
|
||||
pop(1);
|
||||
pop_to_base_lvl();
|
||||
|
||||
push();
|
||||
IF_VERBOSE(0,
|
||||
display(verbose_stream());
|
||||
for (unsigned k = 0; k < num_terms; ++k) {
|
||||
verbose_stream() << "id: " << class_ids[k] << "\n"
|
||||
<< "term: " << mk_pp(sterms[k].get(), m_manager) << "\n"
|
||||
<< "val: " << mk_pp(vals[k].get(), m_manager) << "\n";
|
||||
}
|
||||
verbose_stream() << "\n";
|
||||
verbose_stream() << "term1: " << mk_pp(e1, m_manager) << "\n";
|
||||
verbose_stream() << "term2: " << mk_pp(e2, m_manager) << "\n";
|
||||
verbose_stream() << "val1: " << mk_pp(vals[i].get(), m_manager) << "\n";
|
||||
verbose_stream() << "val2: " << mk_pp(vals[j].get(), m_manager) << "\n";);
|
||||
SASSERT(r != l_false);
|
||||
exit(0);
|
||||
}
|
||||
SASSERT(r != l_false);
|
||||
}
|
||||
}
|
||||
}
|
||||
);
|
||||
*/
|
||||
m_last_search_failure = fail;
|
||||
return result;
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Make some checks before starting the search.
|
||||
Return true if succeeded.
|
||||
|
|
|
|||
|
|
@ -1359,10 +1359,6 @@ namespace smt {
|
|||
|
||||
lbool setup_and_check(bool reset_cancel = true);
|
||||
|
||||
lbool get_implied_equalities(
|
||||
unsigned num_terms, expr* const* terms, unsigned* class_ids,
|
||||
unsigned num_assumptions = 0, expr * const * assumptions = 0);
|
||||
|
||||
// return 'true' if assertions are inconsistent.
|
||||
bool reduce_assertions();
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue