diff --git a/src/smt/fingerprints.cpp b/src/smt/fingerprints.cpp index f59d1dc3f..4550d22b5 100644 --- a/src/smt/fingerprints.cpp +++ b/src/smt/fingerprints.cpp @@ -20,10 +20,9 @@ Revision History: namespace smt { - fingerprint::fingerprint(region & r, void * d, unsigned d_h, expr* def, unsigned n, enode * const * args): + fingerprint::fingerprint(region & r, void * d, unsigned d_h, unsigned n, enode * const * args): m_data(d), m_data_hash(d_h), - m_def(def), m_num_args(n), m_args(nullptr) { m_args = new (r) enode*[n]; @@ -62,7 +61,7 @@ namespace smt { } - fingerprint * fingerprint_set::insert(void * data, unsigned data_hash, unsigned num_args, enode * const * args, expr* def) { + fingerprint * fingerprint_set::insert(void * data, unsigned data_hash, unsigned num_args, enode * const * args) { struct arg_data { unsigned data_hash; @@ -93,9 +92,8 @@ namespace smt { return nullptr; } TRACE(fingerprint_bug, tout << "inserting @" << m_scopes.size() << " " << *d;); - fingerprint * f = new (m_region) fingerprint(m_region, data, data_hash, def, num_args, d->m_args); + fingerprint * f = new (m_region) fingerprint(m_region, data, data_hash, num_args, d->m_args); m_fingerprints.push_back(f); - m_defs.push_back(def); m_set.insert(f); return f; } @@ -114,7 +112,6 @@ namespace smt { void fingerprint_set::reset() { m_set.reset(); m_fingerprints.reset(); - m_defs.reset(); } void fingerprint_set::push_scope() { @@ -134,7 +131,6 @@ namespace smt { m_set.erase(m_fingerprints[i]); } m_fingerprints.shrink(old_size); - m_defs.shrink(old_size); m_scopes.shrink(new_lvl); TRACE(fingerprint_bug, tout << "pop @" << m_scopes.size() << "\n";); } diff --git a/src/smt/fingerprints.h b/src/smt/fingerprints.h index 6a0bc1ccd..dc1863041 100644 --- a/src/smt/fingerprints.h +++ b/src/smt/fingerprints.h @@ -27,16 +27,14 @@ namespace smt { protected: void* m_data = nullptr; unsigned m_data_hash = 0; - expr* m_def = nullptr; unsigned m_num_args = 0; enode** m_args = nullptr; friend class fingerprint_set; fingerprint() = default; public: - fingerprint(region & r, void * d, unsigned d_hash, expr* def, unsigned n, enode * const * args); + fingerprint(region & r, void * d, unsigned d_hash, unsigned n, enode * const * args); void * get_data() const { return m_data; } - expr * get_def() const { return m_def; } unsigned get_data_hash() const { return m_data_hash; } unsigned get_num_args() const { return m_num_args; } enode * const * get_args() const { return m_args; } @@ -59,7 +57,6 @@ namespace smt { region & m_region; set m_set; ptr_vector m_fingerprints; - expr_ref_vector m_defs; unsigned_vector m_scopes; ptr_vector m_tmp; fingerprint m_dummy; @@ -67,8 +64,8 @@ namespace smt { fingerprint * mk_dummy(void * data, unsigned data_hash, unsigned num_args, enode * const * args); public: - fingerprint_set(ast_manager& m, region & r): m_region(r), m_defs(m) {} - fingerprint * insert(void * data, unsigned data_hash, unsigned num_args, enode * const * args, expr* def); + fingerprint_set(ast_manager& m, region & r): m_region(r) {} + fingerprint * insert(void * data, unsigned data_hash, unsigned num_args, enode * const * args); unsigned size() const { return m_fingerprints.size(); } bool contains(void * data, unsigned data_hash, unsigned num_args, enode * const * args); void reset(); diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp index 97a7a899c..db2ddc4ca 100644 --- a/src/smt/mam.cpp +++ b/src/smt/mam.cpp @@ -3975,7 +3975,7 @@ namespace { #endif unsigned min_gen = 0, max_gen = 0; m_interpreter.get_min_max_top_generation(min_gen, max_gen); - m_context.add_instance(qa, pat, num_bindings, bindings, nullptr, max_generation, min_gen, max_gen, used_enodes); + m_context.add_instance(qa, pat, num_bindings, bindings, max_generation, min_gen, max_gen, used_enodes); } bool is_shared(enode * n) const override { diff --git a/src/smt/qi_queue.cpp b/src/smt/qi_queue.cpp index a982a03b8..905644354 100644 --- a/src/smt/qi_queue.cpp +++ b/src/smt/qi_queue.cpp @@ -331,9 +331,6 @@ namespace smt { unsigned gen = get_new_gen(q, generation, ent.m_cost); display_instance_profile(f, q, num_bindings, bindings, proof_id, gen); m_context.internalize_instance(lemma, pr1, gen); - if (f->get_def()) { - m_context.internalize(f->get_def(), true); - } TRACE_CODE({ static unsigned num_useless = 0; if (m.is_or(lemma)) { diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index a67810925..098240fc9 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -1775,9 +1775,11 @@ namespace smt { return m_fingerprints.contains(q, q->get_id(), num_bindings, bindings); } - bool context::add_instance(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, expr* def, unsigned max_generation, + bool context::add_instance(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, //expr* def, + unsigned max_generation, unsigned min_top_generation, unsigned max_top_generation, vector> & used_enodes) { - return m_qmanager->add_instance(q, pat, num_bindings, bindings, def, max_generation, min_top_generation, max_top_generation, used_enodes); + return m_qmanager->add_instance(q, pat, num_bindings, bindings, + max_generation, min_top_generation, max_top_generation, used_enodes); } void context::rescale_bool_var_activity() { diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index b6d030f1a..6a19ab5fd 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -619,8 +619,8 @@ namespace smt { return m_asserted_formulas.has_quantifiers(); } - fingerprint * add_fingerprint(void * data, unsigned data_hash, unsigned num_args, enode * const * args, expr* def = nullptr) { - return m_fingerprints.insert(data, data_hash, num_args, args, def); + fingerprint * add_fingerprint(void * data, unsigned data_hash, unsigned num_args, enode * const * args) { + return m_fingerprints.insert(data, data_hash, num_args, args); } theory_id get_var_theory(bool_var v) const { @@ -1102,8 +1102,8 @@ namespace smt { bool contains_instance(quantifier * q, unsigned num_bindings, enode * const * bindings); - bool add_instance(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, expr* def, unsigned max_generation, - unsigned min_top_generation, unsigned max_top_generation, vector> & used_enodes /*gives the equalities used for the pattern match, see mam.cpp for more info*/); + bool add_instance(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, + unsigned max_generation, unsigned min_top_generation, unsigned max_top_generation, vector> & used_enodes /*gives the equalities used for the pattern match, see mam.cpp for more info*/); void set_global_generation(unsigned generation) { m_generation = generation; } diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index d43ff6af1..0037bb3da 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -203,7 +203,7 @@ namespace smt { unsigned num_decls = q->get_num_decls(); // Remark: sks were created for the flat version of q. SASSERT(sks.size() >= num_decls); - expr_ref_vector bindings(m), defs(m); + expr_ref_vector bindings(m); expr_ref def(m); bindings.resize(num_decls); unsigned max_generation = 0; @@ -249,6 +249,7 @@ namespace smt { sk_value = get_type_compatible_term(sk_value); } func_decl * f = nullptr; + expr_ref sk_term(sk_value, m); if (autil.is_as_array(sk_value, f) && cex->get_func_interp(f) && cex->get_func_interp(f)->get_interp()) { expr_ref body(cex->get_func_interp(f)->get_interp(), m); if (contains_model_value(body)) @@ -260,27 +261,23 @@ namespace smt { defined_names dn(m); body = replace_value_from_ctx(body); body = m.mk_lambda(sorts.size(), sorts.data(), names.data(), body); - // sk_value = m.mk_fresh_const(0, m.get_sort(sk_value)); // get rid of as-array - body = dn.mk_definition(body, to_app(sk_value)); - defs.push_back(body); + sk_term = body; } - bindings.set(num_decls - i - 1, sk_value); + bindings.set(num_decls - i - 1, sk_term); } - TRACE(model_checker, tout << q->get_qid() << " found (use_inv: " << use_inv << ") new instance: " << bindings << "\ndefs:\n" << defs << "\n";); - if (!defs.empty()) def = mk_and(defs); + TRACE(model_checker, tout << q->get_qid() << " found (use_inv: " << use_inv << ") new instance: " << bindings << "\n"); max_generation = std::max(m_qm->get_generation(q), max_generation); - add_instance(q, bindings, max_generation, def.get()); + add_instance(q, bindings, max_generation); return true; } - void model_checker::add_instance(quantifier* q, expr_ref_vector const& bindings, unsigned max_generation, expr* def) { + void model_checker::add_instance(quantifier* q, expr_ref_vector const& bindings, unsigned max_generation) { SASSERT(q->get_num_decls() == bindings.size()); unsigned offset = m_pinned_exprs.size(); m_pinned_exprs.append(bindings); m_pinned_exprs.push_back(q); - m_pinned_exprs.push_back(def); - m_new_instances.push_back(instance(q, offset, def, max_generation)); + m_new_instances.push_back(instance(q, offset, max_generation)); } void model_checker::operator()(expr *n) { @@ -581,27 +578,11 @@ namespace smt { bindings.push_back(m_context->get_enode(b)); } - if (inst.m_def) { - unsigned n = 1; - expr* const* args = &inst.m_def; - if (m.is_and(inst.m_def)) { - n = to_app(inst.m_def)->get_num_args(); - args = to_app(inst.m_def)->get_args(); - } - for (unsigned i = 0; i < n; ++i) { - proof* pr = nullptr; - expr* arg = args[i]; - if (m.proofs_enabled()) - pr = m.mk_def_intro(arg); - m_context->internalize_assertion(arg, pr, gen); - } - } - TRACE(model_checker_bug_detail, tout << "instantiating... q:\n" << mk_pp(q, m) << "\n"; tout << "inconsistent: " << m_context->inconsistent() << "\n"; tout << "bindings:\n" << expr_ref_vector(m, num_decls, m_pinned_exprs.data() + offset) << "\n"; - tout << "def " << mk_pp(inst.m_def, m) << "\n";); - m_context->add_instance(q, nullptr, num_decls, bindings.data(), inst.m_def, gen, gen, gen, dummy); + ); + m_context->add_instance(q, nullptr, num_decls, bindings.data(), gen, gen, gen, dummy); TRACE(model_checker_bug_detail, tout << "after instantiating, inconsistent: " << m_context->inconsistent() << "\n";); } } diff --git a/src/smt/smt_model_checker.h b/src/smt/smt_model_checker.h index fec9e2df5..c816b3cc0 100644 --- a/src/smt/smt_model_checker.h +++ b/src/smt/smt_model_checker.h @@ -70,9 +70,8 @@ namespace smt { struct instance { quantifier * m_q; unsigned m_generation; - expr * m_def; unsigned m_bindings_offset; - instance(quantifier * q, unsigned offset, expr* def, unsigned gen):m_q(q), m_generation(gen), m_def(def), m_bindings_offset(offset) {} + instance(quantifier * q, unsigned offset, unsigned gen):m_q(q), m_generation(gen), m_bindings_offset(offset) {} }; svector m_new_instances; @@ -86,7 +85,7 @@ namespace smt { struct is_model_value {}; expr_mark m_visited; bool contains_model_value(expr * e); - void add_instance(quantifier * q, expr_ref_vector const & bindings, unsigned max_generation, expr * def); + void add_instance(quantifier * q, expr_ref_vector const & bindings, unsigned max_generation); bool is_safe_for_mbqi(quantifier * q) const; public: diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index 3bfa45785..19953be75 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -292,7 +292,6 @@ namespace smt { bool add_instance(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, - expr* def, unsigned max_generation, unsigned min_top_generation, unsigned max_top_generation, @@ -310,7 +309,7 @@ namespace smt { max_generation = std::max(max_generation, get_generation(q)); get_stat(q)->update_max_generation(max_generation); - fingerprint * f = m_context.add_fingerprint(q, q->get_id(), num_bindings, bindings, def); + fingerprint * f = m_context.add_fingerprint(q, q->get_id(), num_bindings, bindings); if (f) { if (is_trace_enabled(TraceTag::causality)) { log_causality(f,pat,used_enodes); @@ -484,17 +483,17 @@ namespace smt { bool quantifier_manager::add_instance(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, - expr* def, unsigned max_generation, unsigned min_top_generation, unsigned max_top_generation, vector> & used_enodes) { - return m_imp->add_instance(q, pat, num_bindings, bindings, def, max_generation, min_top_generation, max_top_generation, used_enodes); + return m_imp->add_instance(q, pat, num_bindings, bindings, max_generation, min_top_generation, max_top_generation, used_enodes); } - bool quantifier_manager::add_instance(quantifier * q, unsigned num_bindings, enode * const * bindings, expr* def, unsigned generation) { + bool quantifier_manager::add_instance(quantifier * q, unsigned num_bindings, enode * const * bindings, unsigned generation) { vector> tmp; - return add_instance(q, nullptr, num_bindings, bindings, def, generation, generation, generation, tmp); + return add_instance(q, nullptr, num_bindings, bindings, + generation, generation, generation, tmp); } void quantifier_manager::init_search_eh() { @@ -721,7 +720,7 @@ namespace smt { vector> used_enodes; m_context->add_instance(q, nullptr, new_bindings.size(), new_bindings.data(), - nullptr, max_gen, st.m_min_top_generation, st.m_max_top_generation, used_enodes); + max_gen, st.m_min_top_generation, st.m_max_top_generation, used_enodes); } bool try_ho_refine(quantifier* qa, app* pat, unsigned num_bindings, enode* const* bindings, diff --git a/src/smt/smt_quantifier.h b/src/smt/smt_quantifier.h index 4d8e6da5a..6d9a44822 100644 --- a/src/smt/smt_quantifier.h +++ b/src/smt/smt_quantifier.h @@ -60,12 +60,11 @@ namespace smt { bool add_instance(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, - expr* def, unsigned max_generation, unsigned min_top_generation, unsigned max_top_generation, vector> & used_enodes /*gives the equalities used for the pattern match, see mam.cpp for more info*/); - bool add_instance(quantifier * q, unsigned num_bindings, enode * const * bindings, expr* def, unsigned generation = 0); + bool add_instance(quantifier * q, unsigned num_bindings, enode * const * bindings, unsigned generation = 0); void init_search_eh(); void assign_eh(quantifier * q); diff --git a/src/smt/smt_quick_checker.cpp b/src/smt/smt_quick_checker.cpp index c1b3a7a37..f267cb481 100644 --- a/src/smt/smt_quick_checker.cpp +++ b/src/smt/smt_quick_checker.cpp @@ -236,7 +236,7 @@ namespace smt { TRACE(quick_checker_sizes, tout << "found new candidate\n"; for (unsigned i = 0; i < m_num_bindings; ++i) tout << "#" << m_bindings[i]->get_owner_id() << " "; tout << "\n";); unsigned max_generation = get_max_generation(m_num_bindings, m_bindings.data()); - if (m_context.add_instance(q, nullptr /* no pattern was used */, m_num_bindings, m_bindings.data(), nullptr, + if (m_context.add_instance(q, nullptr /* no pattern was used */, m_num_bindings, m_bindings.data(), max_generation, 0, // min_top_generation is only available for instances created by the MAM 0, // max_top_generation is only available for instances created by the MAM