diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 8994b2b2a..9ab21ccc5 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -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 vals_map; - obj_map visited_roots; - flet f2(m_fparams.m_model, true); - flet f3(m_fparams.m_array_canonize_simplify, true); - model_ref m; - proof_ref pr(m_manager); - union_find_default_ctx df; - union_find 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 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. diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 825e5e81a..095bcff92 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -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();