mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-05 00:20:50 +00:00
Code Activity

remove side definitions

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-06-02 21:43:55 -07:00
parent 77f8b33794
commit a0a3047e36
11 changed files with 35 additions and 65 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/smt/fingerprints.cpp
View file

@ -20,10 +20,9 @@ Revision History:
namespace smt { 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(d),
m_data_hash(d_h), m_data_hash(d_h),
m_def(def),
m_num_args(n), m_num_args(n),
m_args(nullptr) { m_args(nullptr) {
m_args = new (r) enode*[n]; 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 { struct arg_data {
unsigned data_hash; unsigned data_hash;
@ -93,9 +92,8 @@ namespace smt {
return nullptr; return nullptr;
} }
TRACE(fingerprint_bug, tout << "inserting @" << m_scopes.size() << " " << *d;); 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_fingerprints.push_back(f);
m_defs.push_back(def);
m_set.insert(f); m_set.insert(f);
return f; return f;
} }
@ -114,7 +112,6 @@ namespace smt {
void fingerprint_set::reset() { void fingerprint_set::reset() {
m_set.reset(); m_set.reset();
m_fingerprints.reset(); m_fingerprints.reset();
m_defs.reset();
} }
void fingerprint_set::push_scope() { void fingerprint_set::push_scope() {
@ -134,7 +131,6 @@ namespace smt {
m_set.erase(m_fingerprints[i]); m_set.erase(m_fingerprints[i]);
} }
m_fingerprints.shrink(old_size); m_fingerprints.shrink(old_size);
m_defs.shrink(old_size);
m_scopes.shrink(new_lvl); m_scopes.shrink(new_lvl);
TRACE(fingerprint_bug, tout << "pop @" << m_scopes.size() << "\n";); TRACE(fingerprint_bug, tout << "pop @" << m_scopes.size() << "\n";);
} }

9
src/smt/fingerprints.h
View file

@ -27,16 +27,14 @@ namespace smt {
protected: protected:
void* m_data = nullptr; void* m_data = nullptr;
unsigned m_data_hash = 0; unsigned m_data_hash = 0;
expr* m_def = nullptr;
unsigned m_num_args = 0; unsigned m_num_args = 0;
enode** m_args = nullptr; enode** m_args = nullptr;
friend class fingerprint_set; friend class fingerprint_set;
fingerprint() = default; fingerprint() = default;
public: 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; } 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_data_hash() const { return m_data_hash; }
unsigned get_num_args() const { return m_num_args; } unsigned get_num_args() const { return m_num_args; }
enode * const * get_args() const { return m_args; } enode * const * get_args() const { return m_args; }
@ -59,7 +57,6 @@ namespace smt {
region & m_region; region & m_region;
set m_set; set m_set;
ptr_vector<fingerprint> m_fingerprints; ptr_vector<fingerprint> m_fingerprints;
expr_ref_vector m_defs;
unsigned_vector m_scopes; unsigned_vector m_scopes;
ptr_vector<enode> m_tmp; ptr_vector<enode> m_tmp;
fingerprint m_dummy; fingerprint m_dummy;
@ -67,8 +64,8 @@ namespace smt {
fingerprint * mk_dummy(void * data, unsigned data_hash, unsigned num_args, enode * const * args); fingerprint * mk_dummy(void * data, unsigned data_hash, unsigned num_args, enode * const * args);
public: public:
fingerprint_set(ast_manager& m, region & r): m_region(r), m_defs(m) {} fingerprint_set(ast_manager& m, region & r): m_region(r) {}
fingerprint * insert(void * data, unsigned data_hash, unsigned num_args, enode * const * args, expr* def); fingerprint * insert(void * data, unsigned data_hash, unsigned num_args, enode * const * args);
unsigned size() const { return m_fingerprints.size(); } unsigned size() const { return m_fingerprints.size(); }
bool contains(void * data, unsigned data_hash, unsigned num_args, enode * const * args); bool contains(void * data, unsigned data_hash, unsigned num_args, enode * const * args);
void reset(); void reset();

2
src/smt/mam.cpp
View file

@ -3975,7 +3975,7 @@ namespace {
#endif #endif
unsigned min_gen = 0, max_gen = 0; unsigned min_gen = 0, max_gen = 0;
m_interpreter.get_min_max_top_generation(min_gen, max_gen); 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 { bool is_shared(enode * n) const override {

3
src/smt/qi_queue.cpp
View file

@ -331,9 +331,6 @@ namespace smt {
unsigned gen = get_new_gen(q, generation, ent.m_cost); unsigned gen = get_new_gen(q, generation, ent.m_cost);
display_instance_profile(f, q, num_bindings, bindings, proof_id, gen); display_instance_profile(f, q, num_bindings, bindings, proof_id, gen);
m_context.internalize_instance(lemma, pr1, gen); m_context.internalize_instance(lemma, pr1, gen);
if (f->get_def()) {
m_context.internalize(f->get_def(), true);
}
TRACE_CODE({ TRACE_CODE({
static unsigned num_useless = 0; static unsigned num_useless = 0;
if (m.is_or(lemma)) { if (m.is_or(lemma)) {

6
src/smt/smt_context.cpp
View file

@ -1775,9 +1775,11 @@ namespace smt {
return m_fingerprints.contains(q, q->get_id(), num_bindings, bindings); 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<std::tuple<enode *, enode *>> & used_enodes) { unsigned min_top_generation, unsigned max_top_generation, vector<std::tuple<enode *, enode *>> & 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() { void context::rescale_bool_var_activity() {

8
src/smt/smt_context.h
View file

@ -619,8 +619,8 @@ namespace smt {
return m_asserted_formulas.has_quantifiers(); return m_asserted_formulas.has_quantifiers();
} }
fingerprint * add_fingerprint(void * data, unsigned data_hash, unsigned num_args, enode * const * args, expr* def = nullptr) { fingerprint * add_fingerprint(void * data, unsigned data_hash, unsigned num_args, enode * const * args) {
return m_fingerprints.insert(data, data_hash, num_args, args, def); return m_fingerprints.insert(data, data_hash, num_args, args);
} }
theory_id get_var_theory(bool_var v) const { 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 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, bool add_instance(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings,
unsigned min_top_generation, unsigned max_top_generation, vector<std::tuple<enode *, enode*>> & used_enodes /*gives the equalities used for the pattern match, see mam.cpp for more info*/); unsigned max_generation, unsigned min_top_generation, unsigned max_top_generation, vector<std::tuple<enode *, enode*>> & 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; } void set_global_generation(unsigned generation) { m_generation = generation; }

39
src/smt/smt_model_checker.cpp
View file

@ -203,7 +203,7 @@ namespace smt {
unsigned num_decls = q->get_num_decls(); unsigned num_decls = q->get_num_decls();
// Remark: sks were created for the flat version of q. // Remark: sks were created for the flat version of q.
SASSERT(sks.size() >= num_decls); SASSERT(sks.size() >= num_decls);
expr_ref_vector bindings(m), defs(m); expr_ref_vector bindings(m);
expr_ref def(m); expr_ref def(m);
bindings.resize(num_decls); bindings.resize(num_decls);
unsigned max_generation = 0; unsigned max_generation = 0;
@ -249,6 +249,7 @@ namespace smt {
sk_value = get_type_compatible_term(sk_value); sk_value = get_type_compatible_term(sk_value);
} }
func_decl * f = nullptr; 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()) { 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); expr_ref body(cex->get_func_interp(f)->get_interp(), m);
if (contains_model_value(body)) if (contains_model_value(body))
@ -260,27 +261,23 @@ namespace smt {
defined_names dn(m); defined_names dn(m);
body = replace_value_from_ctx(body); body = replace_value_from_ctx(body);
body = m.mk_lambda(sorts.size(), sorts.data(), names.data(), 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 sk_term = body;
body = dn.mk_definition(body, to_app(sk_value));
defs.push_back(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";); TRACE(model_checker, tout << q->get_qid() << " found (use_inv: " << use_inv << ") new instance: " << bindings << "\n");
if (!defs.empty()) def = mk_and(defs);
max_generation = std::max(m_qm->get_generation(q), max_generation); 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; 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()); SASSERT(q->get_num_decls() == bindings.size());
unsigned offset = m_pinned_exprs.size(); unsigned offset = m_pinned_exprs.size();
m_pinned_exprs.append(bindings); m_pinned_exprs.append(bindings);
m_pinned_exprs.push_back(q); m_pinned_exprs.push_back(q);
m_pinned_exprs.push_back(def); m_new_instances.push_back(instance(q, offset, max_generation));
m_new_instances.push_back(instance(q, offset, def, max_generation));
} }
void model_checker::operator()(expr *n) { void model_checker::operator()(expr *n) {
@ -581,27 +578,11 @@ namespace smt {
bindings.push_back(m_context->get_enode(b)); 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"; TRACE(model_checker_bug_detail, tout << "instantiating... q:\n" << mk_pp(q, m) << "\n";
tout << "inconsistent: " << m_context->inconsistent() << "\n"; tout << "inconsistent: " << m_context->inconsistent() << "\n";
tout << "bindings:\n" << expr_ref_vector(m, num_decls, m_pinned_exprs.data() + offset) << "\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";); TRACE(model_checker_bug_detail, tout << "after instantiating, inconsistent: " << m_context->inconsistent() << "\n";);
} }
} }

5
src/smt/smt_model_checker.h
View file

@ -70,9 +70,8 @@ namespace smt {
struct instance { struct instance {
quantifier * m_q; quantifier * m_q;
unsigned m_generation; unsigned m_generation;
expr * m_def;
unsigned m_bindings_offset; 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<instance> m_new_instances; svector<instance> m_new_instances;
@ -86,7 +85,7 @@ namespace smt {
struct is_model_value {}; struct is_model_value {};
expr_mark m_visited; expr_mark m_visited;
bool contains_model_value(expr * e); 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; bool is_safe_for_mbqi(quantifier * q) const;
public: public:

13
src/smt/smt_quantifier.cpp
View file

@ -292,7 +292,6 @@ namespace smt {
bool add_instance(quantifier * q, app * pat, bool add_instance(quantifier * q, app * pat,
unsigned num_bindings, unsigned num_bindings,
enode * const * bindings, enode * const * bindings,
expr* def,
unsigned max_generation, unsigned max_generation,
unsigned min_top_generation, unsigned min_top_generation,
unsigned max_top_generation, unsigned max_top_generation,
@ -310,7 +309,7 @@ namespace smt {
max_generation = std::max(max_generation, get_generation(q)); max_generation = std::max(max_generation, get_generation(q));
get_stat(q)->update_max_generation(max_generation); 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 (f) {
if (is_trace_enabled(TraceTag::causality)) { if (is_trace_enabled(TraceTag::causality)) {
log_causality(f,pat,used_enodes); log_causality(f,pat,used_enodes);
@ -484,17 +483,17 @@ namespace smt {
bool quantifier_manager::add_instance(quantifier * q, app * pat, bool quantifier_manager::add_instance(quantifier * q, app * pat,
unsigned num_bindings, unsigned num_bindings,
enode * const * bindings, enode * const * bindings,
expr* def,
unsigned max_generation, unsigned max_generation,
unsigned min_top_generation, unsigned min_top_generation,
unsigned max_top_generation, unsigned max_top_generation,
vector<std::tuple<enode *, enode *>> & used_enodes) { vector<std::tuple<enode *, enode *>> & 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<std::tuple<enode *, enode *>> tmp; vector<std::tuple<enode *, enode *>> 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() { void quantifier_manager::init_search_eh() {
@ -721,7 +720,7 @@ namespace smt {
vector<std::tuple<enode*, enode*>> used_enodes; vector<std::tuple<enode*, enode*>> used_enodes;
m_context->add_instance(q, nullptr, new_bindings.size(), new_bindings.data(), 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, bool try_ho_refine(quantifier* qa, app* pat, unsigned num_bindings, enode* const* bindings,

3
src/smt/smt_quantifier.h
View file

@ -60,12 +60,11 @@ namespace smt {
bool add_instance(quantifier * q, app * pat, bool add_instance(quantifier * q, app * pat,
unsigned num_bindings, unsigned num_bindings,
enode * const * bindings, enode * const * bindings,
expr* def,
unsigned max_generation, unsigned max_generation,
unsigned min_top_generation, unsigned min_top_generation,
unsigned max_top_generation, unsigned max_top_generation,
vector<std::tuple<enode *, enode *>> & used_enodes /*gives the equalities used for the pattern match, see mam.cpp for more info*/); vector<std::tuple<enode *, enode *>> & 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 init_search_eh();
void assign_eh(quantifier * q); void assign_eh(quantifier * q);

2
src/smt/smt_quick_checker.cpp
View file

@ -236,7 +236,7 @@ namespace smt {
TRACE(quick_checker_sizes, tout << "found new candidate\n"; 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";); 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()); 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, max_generation,
0, // min_top_generation is only available for instances created by the MAM 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 0, // max_top_generation is only available for instances created by the MAM