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

prepare for enodes over lambdas

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-06-01 13:00:35 -07:00
parent 705569df24
commit d025b34606
17 changed files with 65 additions and 62 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/smt_conflict_resolution.cpp
View file

@ -855,7 +855,7 @@ namespace smt {
case eq_justification::CONGRUENCE:
num_args = n1->get_num_args();
SASSERT(num_args == n2->get_num_args());
SASSERT(n1->get_app()->get_decl() == n2->get_app()->get_decl());
SASSERT(n1->get_decl() == n2->get_decl());
if (js.used_commutativity()) {
bool visited = true;
SASSERT(num_args == 2);

4
src/smt/smt_context.cpp
View file

@ -4672,8 +4672,8 @@ namespace smt {
theory_id th_id = l->get_id();
for (enode * parent : enode::parents(n)) {
auto p = parent->get_app();
family_id fid = p->get_family_id();
auto p = parent->get_expr();
family_id fid = parent->get_family_id();
if (fid != th_id && fid != m.get_basic_family_id()) {
if (is_beta_redex(parent, n))
continue;

2
src/smt/smt_context.h
View file

@ -1025,7 +1025,7 @@ namespace smt {
bool_var mk_bool_var(expr * n);
enode * mk_enode(app * n, bool suppress_args, bool merge_tf, bool cgc_enabled);
enode * mk_enode(expr * n, bool suppress_args, bool merge_tf, bool cgc_enabled);
void attach_th_var(enode * n, theory * th, theory_var v);

12
src/smt/smt_enode.h
View file

@ -59,7 +59,7 @@ namespace smt {
equality propagation, and the theory central bus of equalities.
*/
class enode {
app * m_owner; //!< The application that 'owns' this enode.
expr * m_owner; //!< The application that 'owns' this enode.
enode * m_root; //!< Representative of the equivalence class
enode * m_next; //!< Next element in the equivalence class.
enode * m_cg;
@ -166,7 +166,7 @@ namespace smt {
void del_eh(ast_manager & m, bool update_children_parent = true);
app * get_app() const { return m_owner; }
app * get_app() const { SASSERT(is_app()); return to_app(m_owner); }
expr *get_expr() const {
return m_owner;
@ -179,13 +179,13 @@ namespace smt {
unsigned get_owner_id() const { return m_owner->get_id(); }
unsigned get_expr_id() const { return m_owner->get_id(); }
func_decl * get_decl() const { return m_owner->get_decl(); }
unsigned get_decl_id() const { return m_owner->get_decl()->get_small_id(); }
func_decl * get_decl() const { return is_app() ? to_app(m_owner)->get_decl() : nullptr; }
unsigned get_decl_id() const { return is_app() ? to_app(m_owner)->get_decl()->get_small_id() : 43; }
sort* get_sort() const { return m_owner->get_sort(); }
family_id get_family_id() const {
return m_owner->get_family_id();
return is_app() ? to_app(m_owner)->get_family_id() : basic_family_id;
}
unsigned hash() const {
@ -225,7 +225,7 @@ namespace smt {
}
unsigned get_num_args() const {
return m_suppress_args ? 0 : m_owner->get_num_args();
return m_suppress_args || !is_app() ? 0 : to_app(m_owner)->get_num_args();
}
enode * get_arg(unsigned idx) const {

8
src/smt/smt_internalizer.cpp
View file

@ -996,7 +996,7 @@ namespace smt {
\remark If suppress_args is true, then the enode is viewed as a constant
in the egraph.
*/
enode * context::mk_enode(app * n, bool suppress_args, bool merge_tf, bool cgc_enabled) {
enode * context::mk_enode(expr * n, bool suppress_args, bool merge_tf, bool cgc_enabled) {
TRACE(mk_enode_detail, tout << mk_pp(n, m) << "\nsuppress_args: " << suppress_args << ", merge_tf: " <<
merge_tf << ", cgc_enabled: " << cgc_enabled << "\n";);
SASSERT(!e_internalized(n));
@ -1008,7 +1008,7 @@ namespace smt {
CTRACE(cached_generation, generation != m_generation,
tout << "cached_generation: #" << n->get_id() << " " << generation << " " << m_generation << "\n";);
}
enode *e = enode::mk(m, get_region(), m_app2enode, n, generation, suppress_args, merge_tf, m_scope_lvl,
enode *e = enode::mk(m, get_region(), m_app2enode, to_app(n), generation, suppress_args, merge_tf, m_scope_lvl,
cgc_enabled, true);
TRACE(mk_enode_detail, tout << "e.get_num_args() = " << e->get_num_args() << "\n";);
if (m.is_unique_value(n))
@ -1042,7 +1042,7 @@ namespace smt {
}
}
if (!e->is_eq()) {
unsigned decl_id = n->get_decl()->get_small_id();
unsigned decl_id = e->get_decl_id();
if (decl_id >= m_decl2enodes.size())
m_decl2enodes.resize(decl_id+1);
m_decl2enodes[decl_id].push_back(e);
@ -1086,7 +1086,7 @@ namespace smt {
m_cg_table.erase(e);
}
if (e->get_num_args() > 0 && !e->is_eq()) {
unsigned decl_id = to_app(n)->get_decl()->get_small_id();
unsigned decl_id = e->get_decl_id();
SASSERT(decl_id < m_decl2enodes.size());
SASSERT(m_decl2enodes[decl_id].back() == e);
m_decl2enodes[decl_id].pop_back();

16
src/smt/smt_model_finder.cpp
View file

@ -1378,7 +1378,7 @@ namespace smt {
Store in arrays, all enodes that match the pattern
*/
void get_auf_arrays(app* auf_arr, context* ctx, ptr_buffer<enode>& arrays) {
void get_auf_arrays(expr* auf_arr, context* ctx, ptr_buffer<enode>& arrays) {
if (is_ground(auf_arr)) {
if (ctx->e_internalized(auf_arr)) {
enode* e = ctx->get_enode(auf_arr);
@ -1387,8 +1387,8 @@ namespace smt {
}
}
}
else {
app* nested_array = to_app(auf_arr->get_arg(0));
else if (is_app(auf_arr)) {
app* nested_array = to_app(to_app(auf_arr)->get_arg(0));
ptr_buffer<enode> nested_arrays;
get_auf_arrays(nested_array, ctx, nested_arrays);
for (enode* curr : nested_arrays) {
@ -1396,7 +1396,7 @@ namespace smt {
enode_vector::iterator end2 = curr->end_parents();
for (; it2 != end2; ++it2) {
enode* p = *it2;
if (ctx->is_relevant(p) && p->get_decl() == auf_arr->get_decl()) {
if (ctx->is_relevant(p) && p->get_decl() == to_app(auf_arr)->get_decl()) {
arrays.push_back(p);
}
}
@ -1411,9 +1411,9 @@ namespace smt {
unsigned m_arg_i;
unsigned m_var_j;
app* get_array() const { return to_app(m_select->get_arg(0)); }
expr* get_array() const { return m_select->get_arg(0); }
func_decl* get_array_func_decl(app* ground_array, auf_solver& s) {
func_decl* get_array_func_decl(expr* ground_array, auf_solver& s) {
TRACE(model_evaluator, tout << expr_ref(ground_array, m) << "\n";);
expr* ground_array_interp = s.eval(ground_array, false);
if (ground_array_interp && m_array.is_as_array(ground_array_interp))
@ -1449,7 +1449,7 @@ namespace smt {
});
node* n1 = s.get_uvar(q, m_var_j);
for (enode* n : arrays) {
auto ground_array = n->get_app();
auto ground_array = n->get_expr();
func_decl* f = get_array_func_decl(ground_array, s);
if (f) {
SASSERT(m_arg_i >= 1);
@ -1463,7 +1463,7 @@ namespace smt {
ptr_buffer<enode> arrays;
get_auf_arrays(get_array(), ctx, arrays);
for (enode* curr : arrays) {
auto ground_array = curr->get_app();
auto ground_array = curr->get_expr();
func_decl* f = get_array_func_decl(ground_array, s);
if (f) {
node* A_f_i = s.get_A_f_i(f, m_arg_i - 1);

2
src/smt/smt_theory.cpp
View file

@ -204,7 +204,7 @@ namespace smt {
log_axiom_instantiation(mk_or(fmls));
}
void theory::log_axiom_instantiation(app * r, unsigned axiom_id, unsigned num_bindings, app * const * bindings, unsigned pattern_id, const vector<std::tuple<enode *, enode *>> & used_enodes) {
void theory::log_axiom_instantiation(app * r, unsigned axiom_id, unsigned num_bindings, expr * const * bindings, unsigned pattern_id, const vector<std::tuple<enode *, enode *>> & used_enodes) {
ast_manager & m = get_manager();
SASSERT(r->get_ref_count() > 0);
std::ostream& out = m.trace_stream();

4
src/smt/smt_theory.h
View file

@ -482,11 +482,11 @@ namespace smt {
protected:
void log_axiom_instantiation(app * r, unsigned axiom_id = UINT_MAX, unsigned num_bindings = 0,
app * const * bindings = nullptr, unsigned pattern_id = UINT_MAX,
expr * const * bindings = nullptr, unsigned pattern_id = UINT_MAX,
const vector<std::tuple<enode *, enode *>> & used_enodes = vector<std::tuple<enode *, enode*>>());
void log_axiom_instantiation(expr * r, unsigned axiom_id = UINT_MAX, unsigned num_bindings = 0,
app * const * bindings = nullptr, unsigned pattern_id = UINT_MAX,
expr * const * bindings = nullptr, unsigned pattern_id = UINT_MAX,
const vector<std::tuple<enode *, enode *>> & used_enodes = vector<std::tuple<enode *, enode*>>()) {
log_axiom_instantiation(to_app(r), axiom_id, num_bindings, bindings, pattern_id, used_enodes);
}

2
src/smt/theory_arith_aux.h
View file

@ -2179,7 +2179,7 @@ namespace smt {
TRACE(shared, tout << ctx.get_scope_level() << " " << v << " " << r->get_num_parents() << "\n";);
for (; it != end; ++it) {
enode * parent = *it;
app * o = parent->get_app();
app* o = parent->get_app();
if (parent->get_family_id() == get_id()) {
switch (o->get_decl_kind()) {
case OP_DIV:

4
src/smt/theory_array_base.h
View file

@ -33,8 +33,8 @@ namespace smt {
void add_weak_var(theory_var v);
virtual void set_prop_upward(theory_var v) {}
void found_unsupported_op(expr * n);
void found_unsupported_op(enode* n) { found_unsupported_op(n->get_app()); }
void found_unsupported_op(theory_var v) { found_unsupported_op(get_enode(v)->get_app()); }
void found_unsupported_op(enode* n) { found_unsupported_op(n->get_expr()); }
void found_unsupported_op(theory_var v) { found_unsupported_op(get_expr(v)); }
bool is_store(expr const* n) const { return is_app(n) && to_app(n)->is_app_of(get_id(), OP_STORE); }
bool is_map(expr const* n) const { return is_app(n) && to_app(n)->is_app_of(get_id(), OP_ARRAY_MAP); }

6
src/smt/theory_array_full.cpp
View file

@ -667,7 +667,7 @@ namespace smt {
// select(as-array f, i_1, ..., i_n) = (f i_1 ... i_n)
//
bool theory_array_full::instantiate_select_as_array_axiom(enode* select, enode* arr) {
SASSERT(is_as_array(arr->get_app()));
SASSERT(is_as_array(arr->get_expr()));
SASSERT(is_select(select));
SASSERT(arr->get_num_args() == 0);
unsigned num_args = select->get_num_args();
@ -677,12 +677,12 @@ namespace smt {
m_stats.m_num_select_as_array_axiom++;
ptr_buffer<expr> sel_args;
sel_args.push_back(arr->get_app());
sel_args.push_back(arr->get_expr());
for (unsigned short i = 1; i < num_args; ++i) {
sel_args.push_back(select->get_app()->get_arg(i));
}
expr * sel = mk_select(sel_args.size(), sel_args.data());
func_decl * f = array_util(m).get_as_array_func_decl(arr->get_app());
func_decl * f = array_util(m).get_as_array_func_decl(arr->get_expr());
expr_ref val(m.mk_app(f, sel_args.size()-1, sel_args.data()+1), m);
TRACE(array, tout << "new select-as-array axiom...\n";
tout << "as-array: " << mk_bounded_pp(arr->get_expr(), m) << "\n";

8
src/smt/theory_bv.cpp
View file

@ -179,11 +179,15 @@ namespace smt {
if (params().m_bv_reflect) {
return n->get_arg(idx);
}
else {
else if (n->is_app()) {
app * arg = to_app(n->get_app()->get_arg(idx));
SASSERT(ctx.e_internalized(arg));
return ctx.get_enode(arg);
}
else {
UNREACHABLE();
return nullptr;
}
}
inline theory_var theory_bv::get_arg_var(enode * n, unsigned idx) {
@ -1151,7 +1155,7 @@ namespace smt {
if (!is_attached_to_var(n) && !approximate_term(n->get_expr())) {
mk_bits(mk_var(n));
if (ctx.is_relevant(n)) {
relevant_eh(n->get_app());
relevant_eh(n->get_expr());
}
}
}

6
src/smt/theory_bv.h
View file

@ -142,10 +142,10 @@ namespace smt {
theory_var next(theory_var v) const { return m_find.next(v); }
bool is_root(theory_var v) const { return m_find.is_root(v); }
unsigned get_bv_size(app const * n) const { return m_util.get_bv_size(n); }
unsigned get_bv_size(enode const * n) const { return m_util.get_bv_size(n->get_app()); }
unsigned get_bv_size(enode const * n) const { return m_util.get_bv_size(n->get_expr()); }
unsigned get_bv_size(theory_var v) const { return get_bv_size(get_enode(v)); }
bool is_bv(app const* n) const { return m_util.is_bv_sort(n->get_sort()); }
bool is_bv(enode const* n) const { return is_bv(n->get_app()); }
bool is_bv(expr const* n) const { return m_util.is_bv_sort(n->get_sort()); }
bool is_bv(enode const* n) const { return is_bv(n->get_expr()); }
bool is_bv(theory_var v) const { return is_bv(get_enode(v)); }
region & get_region() { return m_trail_stack.get_region(); }

28
src/smt/theory_datatype.cpp
View file

@ -171,16 +171,16 @@ namespace smt {
func_decl * d = n->get_decl();
ptr_vector<func_decl> const & accessors = *m_util.get_constructor_accessors(d);
SASSERT(n->get_num_args() == accessors.size());
app_ref_vector bindings(m);
expr_ref_vector bindings(m);
vector<std::tuple<enode *, enode *>> used_enodes;
used_enodes.push_back(std::make_tuple(nullptr, n));
for (unsigned i = 0; i < n->get_num_args(); ++i) {
bindings.push_back(n->get_arg(i)->get_app());
bindings.push_back(n->get_arg(i)->get_expr());
}
unsigned base_id = m.has_trace_stream() && accessors.size() > 0 ? m_util.plugin().get_axiom_base_id(d->get_name()) : 0;
unsigned i = 0;
for (func_decl * acc : accessors) {
app_ref acc_app(m.mk_app(acc, n->get_app()), m);
app_ref acc_app(m.mk_app(acc, n->get_expr()), m);
enode * arg = n->get_arg(i);
std::function<void(void)> fn = [&]() {
@ -267,7 +267,7 @@ namespace smt {
func_decl * sub_decl = m_util.get_datatype_subterm(s);
if (sub_decl) {
TRACE(datatype, tout << "asserting reflexivity for #" << n->get_owner_id() << " " << mk_pp(n->get_expr(), m) << "\n";);
app_ref reflex(m.mk_app(sub_decl, n->get_app(), n->get_app()), m);
app_ref reflex(m.mk_app(sub_decl, n->get_expr(), n->get_expr()), m);
ctx.internalize(reflex, false);
literal l(ctx.get_bool_var(reflex));
ctx.mark_as_relevant(l);
@ -356,7 +356,7 @@ namespace smt {
sort * s = arg->get_sort();
sort *e_sort = nullptr;
if (m_autil.is_array(s) && m_util.is_datatype(get_array_range(s))) {
app_ref def(m_autil.mk_default(arg->get_app()), m);
app_ref def(m_autil.mk_default(arg->get_expr()), m);
if (!ctx.e_internalized(def)) {
ctx.internalize(def, false);
}
@ -542,7 +542,7 @@ namespace smt {
ptr_vector<enode> candidates = list_subterms(arg2);
for (enode *s : candidates) {
bool is_leaf = !m_util.is_constructor(s->get_app());
bool is_leaf = !m_util.is_constructor(s->get_expr());
// Case 1: Equality check (arg1 == s)
// Valid if sorts are compatible.
@ -570,7 +570,7 @@ namespace smt {
if (sub_decl) {
TRACE(datatype, tout << "adding recursive case: " << mk_pp(arg1->get_expr(), m) << " ⊑ "
<< mk_pp(s->get_expr(), m) << "\n";);
auto tmp = m.mk_not(m.mk_app(sub_decl, arg1->get_app(), s->get_app()));
auto tmp = m.mk_not(m.mk_app(sub_decl, arg1->get_expr(), s->get_expr()));
lits.push_back(mk_literal(tmp));
found_possible = true;
}
@ -617,7 +617,7 @@ namespace smt {
ptr_vector<enode> candidates = list_subterms(arg2);
for (enode *s : candidates) {
bool is_leaf = !m_util.is_constructor(s->get_app());
bool is_leaf = !m_util.is_constructor(s->get_expr());
if (s->get_sort() == arg1->get_sort()) {
TRACE(datatype,
@ -638,7 +638,7 @@ namespace smt {
if (sub_decl) {
TRACE(datatype, tout << "asserting NOT " << mk_pp(arg1->get_expr(), m) << " subterm "
<< mk_pp(s->get_expr(), m) << "\n";);
auto sub_app = m.mk_app(sub_decl, arg1->get_app(), s->get_app());
auto sub_app = m.mk_app(sub_decl, arg1->get_expr(), s->get_expr());
literal sub_lit = mk_literal(sub_app);
literal lits[2] = {antecedent, ~sub_lit};
ctx.mk_th_axiom(get_id(), 2, lits);
@ -678,7 +678,7 @@ namespace smt {
enode *ctor = nullptr;
enode *iter = root;
do {
if (f.th.m_util.is_constructor(iter->get_app())) {
if (f.th.m_util.is_constructor(iter->get_expr())) {
ctor = iter;
break;
}
@ -967,7 +967,7 @@ namespace smt {
};
for (enode* sib : *n) {
if (m_sutil.str.is_concat_of_units(sib->get_app())) {
if (m_sutil.str.is_concat_of_units(sib->get_expr())) {
add_todo(sib);
sibling = sib;
break;
@ -994,7 +994,7 @@ namespace smt {
theory_array* th = dynamic_cast<theory_array*>(ctx.get_theory(m_autil.get_family_id()));
for (enode* p : th->parent_selects(n))
m_args.push_back(p);
app_ref def(m_autil.mk_default(n->get_app()), m);
app_ref def(m_autil.mk_default(n->get_expr()), m);
m_args.push_back(ctx.get_enode(def));
return m_args;
}
@ -1328,7 +1328,7 @@ namespace smt {
if (!r) {
ptr_vector<func_decl> const & constructors = *m_util.get_datatype_constructors(dt);
func_decl * rec = m_util.get_constructor_is(constructors[unassigned_idx]);
auto rec_app = m.mk_app(rec, n->get_app());
auto rec_app = m.mk_app(rec, n->get_expr());
consequent = mk_literal(rec_app);
}
else {
@ -1405,7 +1405,7 @@ namespace smt {
}
}
SASSERT(r != nullptr);
app_ref r_app(m.mk_app(r, n->get_app()), m);
app_ref r_app(m.mk_app(r, n->get_expr()), m);
TRACE(datatype, tout << "creating split: " << mk_pp(r_app, m) << "\n";);
ctx.internalize(r_app, false);
bool_var bv = ctx.get_bool_var(r_app);

7
src/smt/theory_diff_logic_def.h
View file

@ -974,10 +974,9 @@ theory_var theory_diff_logic<Ext>::expand(bool pos, theory_var v, rational & k)
enode* e = get_enode(v);
rational r;
for (;;) {
app* n = e->get_app();
if (m_util.is_add(n) && n->get_num_args() == 2) {
app* x = to_app(n->get_arg(0));
app* y = to_app(n->get_arg(1));
expr *x = nullptr, *y = nullptr;
expr* n = e->get_expr();
if (m_util.is_add(n, x, y)) {
if (m_util.is_numeral(x, r)) {
e = ctx.get_enode(y);
}

11
src/smt/theory_dl.cpp
View file

@ -166,7 +166,7 @@ namespace smt {
}
void apply_sort_cnstr(enode * n, sort * s) override {
auto term = n->get_app();
auto term = n->get_expr();
if (u().is_finite_sort(term)) {
mk_rep(term);
}
@ -214,11 +214,12 @@ namespace smt {
}
}
bool mk_rep(app* n) {
unsigned num_args = n->get_num_args();
bool mk_rep(expr* n) {
enode * e = nullptr;
for (unsigned i = 0; i < num_args; ++i) {
ctx.internalize(n->get_arg(i), false);
if (is_app(n)) {
for (auto arg : *to_app(n))
ctx.internalize(arg, false);
}
if (ctx.e_internalized(n)) {
e = ctx.get_enode(n);

5
src/smt/theory_pb.cpp
View file

@ -2369,9 +2369,8 @@ namespace smt {
model_value_proc * theory_pb::mk_value(enode * n, model_generator & mg) {
auto a = n->get_app();
pb_model_value_proc* p = alloc(pb_model_value_proc, a);
for (unsigned i = 0; i < a->get_num_args(); ++i) {
p->add(ctx.get_enode(a->get_arg(i)));
}
for (auto arg : *a)
p->add(ctx.get_enode(arg));
return p;
}