From 2cc44220182be48947bbccdcd0645f46d81d1ef6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 30 May 2026 15:12:56 -0700 Subject: [PATCH] use expr based access to enodes to allow for storing first-class lambas --- src/ast/ast.h | 4 +- src/ast/euf/ho_matcher.cpp | 4 +- src/ast/normal_forms/pull_quant.cpp | 2 +- src/smt/arith_eq_adapter.cpp | 6 +-- src/smt/arith_eq_adapter.h | 1 + src/smt/dyn_ack.cpp | 59 +++++++++++++-------------- src/smt/dyn_ack.h | 28 ++++++------- src/smt/qi_queue.cpp | 2 +- src/smt/smt_almost_cg_table.cpp | 2 +- src/smt/smt_conflict_resolution.cpp | 14 +++---- src/smt/smt_context.cpp | 16 ++++---- src/smt/smt_context.h | 2 +- src/smt/smt_context_pp.cpp | 4 +- src/smt/smt_enode.cpp | 2 +- src/smt/smt_enode.h | 14 ++++++- src/smt/smt_model_checker.cpp | 4 +- src/smt/smt_model_finder.cpp | 14 +++---- src/smt/smt_model_generator.cpp | 4 +- src/smt/smt_theory.h | 4 +- src/smt/theory_arith.h | 6 +-- src/smt/theory_arith_aux.h | 10 ++--- src/smt/theory_arith_core.h | 23 ++++++----- src/smt/theory_arith_int.h | 8 ++-- src/smt/theory_arith_nl.h | 2 +- src/smt/theory_arith_pp.h | 2 +- src/smt/theory_array.cpp | 16 ++++---- src/smt/theory_array.h | 2 +- src/smt/theory_array_base.cpp | 26 +++++------- src/smt/theory_array_base.h | 26 ++++++------ src/smt/theory_array_full.cpp | 40 ++++++++++-------- src/smt/theory_array_full.h | 3 +- src/smt/theory_bv.cpp | 51 ++++++++++++----------- src/smt/theory_bv.h | 12 +++--- src/smt/theory_datatype.cpp | 32 +++++++-------- src/smt/theory_datatype.h | 14 +++---- src/smt/theory_dense_diff_logic_def.h | 8 ++-- src/smt/theory_diff_logic.h | 2 +- src/smt/theory_diff_logic_def.h | 8 ++-- src/smt/theory_dl.cpp | 6 +-- src/smt/theory_finite_set.cpp | 5 ++- src/smt/theory_finite_set.h | 2 +- src/smt/theory_fpa.cpp | 10 ++--- src/smt/theory_fpa.h | 2 +- src/smt/theory_intblast.cpp | 2 +- src/smt/theory_lra.cpp | 35 ++++++++-------- src/smt/theory_lra.h | 2 +- src/smt/theory_pb.cpp | 2 +- src/smt/theory_recfun.cpp | 2 +- src/smt/theory_recfun.h | 6 +-- src/smt/theory_seq.cpp | 9 ++-- src/smt/theory_seq.h | 4 +- src/smt/theory_special_relations.cpp | 4 +- src/smt/theory_utvpi.h | 4 +- src/smt/theory_utvpi_def.h | 8 ++-- 54 files changed, 301 insertions(+), 279 deletions(-) diff --git a/src/ast/ast.h b/src/ast/ast.h index d8b271478..daed492c1 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -1644,10 +1644,10 @@ public: bool contains(ast * a) const { return m_ast_table.contains(a); } - bool is_lambda_def(quantifier* q) const { return q->get_qid() == m_lambda_def; } + bool is_lambda_q(quantifier* q) const { return q->get_qid() == m_lambda_def; } void add_lambda_def(func_decl* f, quantifier* q); quantifier* is_lambda_def(func_decl* f); - quantifier* is_lambda_def(app* e) { return is_lambda_def(e->get_decl()); } + quantifier* is_lambda_def(expr* e) { return is_app(e) ? is_lambda_def(to_app(e)->get_decl()) : nullptr; } obj_map const& lambda_defs() const { return m_lambda_defs; } symbol const& lambda_def_qid() const { return m_lambda_def; } diff --git a/src/ast/euf/ho_matcher.cpp b/src/ast/euf/ho_matcher.cpp index 5b90c4d47..acfe800f2 100644 --- a/src/ast/euf/ho_matcher.cpp +++ b/src/ast/euf/ho_matcher.cpp @@ -684,7 +684,7 @@ namespace euf { } auto is_ho = any_of(subterms::all(expr_ref(p, m)), [&](expr* t) { return m_unitary.is_flex(0, t) || - (is_app(t) && m.is_lambda_def(to_app(t)->get_decl())) || + m.is_lambda_def(t) || is_lambda(t); }); if (!is_ho) @@ -702,7 +702,7 @@ namespace euf { todo.pop_back(); continue; } - if (m_unitary.is_flex(0, t) || (is_app(t) && m.is_lambda_def(to_app(t)->get_decl())) || is_lambda(t)) { + if (m_unitary.is_flex(0, t) || m.is_lambda_def(t) || is_lambda(t)) { if (!contains_pat2abs) m_pat2abs.insert_if_not_there(p, svector>()).push_back({ nb, t }); auto v = m.mk_var(nb++, t->get_sort()); diff --git a/src/ast/normal_forms/pull_quant.cpp b/src/ast/normal_forms/pull_quant.cpp index a37580b86..8f69d8995 100644 --- a/src/ast/normal_forms/pull_quant.cpp +++ b/src/ast/normal_forms/pull_quant.cpp @@ -188,7 +188,7 @@ struct pull_quant::imp { var_names.data(), nested_q->get_expr(), std::min(q->get_weight(), nested_q->get_weight()), - m.is_lambda_def(q) ? symbol("pulled-lambda") : q->get_qid()); + m.is_lambda_q(q) ? symbol("pulled-lambda") : q->get_qid()); } void pull_quant1(quantifier * q, expr * new_expr, expr_ref & result) { diff --git a/src/smt/arith_eq_adapter.cpp b/src/smt/arith_eq_adapter.cpp index 56729af17..2bbe7a4e1 100644 --- a/src/smt/arith_eq_adapter.cpp +++ b/src/smt/arith_eq_adapter.cpp @@ -87,8 +87,8 @@ namespace smt { tout << mk_ismt2_pp(n1->get_expr(), m) << "\n" << mk_ismt2_pp(n2->get_expr(), m) << "\n";); if (n1->get_owner_id() > n2->get_owner_id()) std::swap(n1, n2); - app * t1 = n1->get_expr(); - app * t2 = n2->get_expr(); + expr * t1 = n1->get_expr(); + expr * t2 = n2->get_expr(); if (m.are_distinct(t1, t2)) { expr_ref eq(m.mk_eq(t1, t2), m); ctx.internalize(eq, true); @@ -233,7 +233,7 @@ namespace smt { void arith_eq_adapter::new_eq_eh(theory_var v1, theory_var v2) { TRACE(arith_eq_adapter, tout << "v" << v1 << " = v" << v2 << " #" << get_enode(v1)->get_owner_id() << " = #" << get_enode(v2)->get_owner_id() << "\n";); - TRACE(arith_eq_adapter_bug, tout << mk_bounded_pp(get_enode(v1)->get_expr(), get_manager()) << "\n" << mk_bounded_pp(get_enode(v2)->get_expr(), get_manager()) << "\n";); + TRACE(arith_eq_adapter_bug, tout << mk_bounded_pp(get_expr(v1), get_manager()) << "\n" << mk_bounded_pp(get_expr(v2), get_manager()) << "\n";); mk_axioms(get_enode(v1), get_enode(v2)); } diff --git a/src/smt/arith_eq_adapter.h b/src/smt/arith_eq_adapter.h index 22dfcacb0..7b1c06876 100644 --- a/src/smt/arith_eq_adapter.h +++ b/src/smt/arith_eq_adapter.h @@ -70,6 +70,7 @@ namespace smt { context & get_context() const { return m_owner.get_context(); } ast_manager & get_manager() const { return m_owner.get_manager(); } enode * get_enode(theory_var v) const { return m_owner.get_enode(v); } + expr * get_expr(theory_var v) const { return m_owner.get_expr(v); } public: arith_eq_adapter(theory & owner, arith_util & u):m_owner(owner), m_util(u) {} diff --git a/src/smt/dyn_ack.cpp b/src/smt/dyn_ack.cpp index a2a96e8a4..691bd7fc0 100644 --- a/src/smt/dyn_ack.cpp +++ b/src/smt/dyn_ack.cpp @@ -101,14 +101,14 @@ namespace smt { }; class dyn_ack_eq_justification : public justification { - app * m_app1; - app * m_app2; - app * m_r; + expr * m_app1; + expr * m_app2; + expr * m_r; app * m_eq1; app * m_eq2; app * m_eq3; public: - dyn_ack_eq_justification(app * n1, app * n2, app* r, app* eq1, app* eq2, app* eq3): + dyn_ack_eq_justification(expr * n1, expr * n2, expr* r, app* eq1, app* eq2, app* eq3): justification(false), // dyn_ack_cc_justifications are not stored in regions. m_app1(n1), m_app2(n2), @@ -167,7 +167,7 @@ namespace smt { dyn_ack_manager::~dyn_ack_manager() { reset_app_pairs(); - reset_app_triples(); + reset_expr_triples(); } void dyn_ack_manager::reset_app_pairs() { @@ -189,7 +189,7 @@ namespace smt { m_num_propagations_since_last_gc = 0; m_triple.m_app2num_occs.reset(); - reset_app_triples(); + reset_expr_triples(); m_triple.m_to_instantiate.reset(); m_triple.m_qhead = 0; } @@ -230,7 +230,7 @@ namespace smt { } } - void dyn_ack_manager::eq_eh(app * n1, app * n2, app* r) { + void dyn_ack_manager::eq_eh(expr * n1, expr * n2, expr* r) { if (n1 == n2 || r == n1 || r == n2 || m.is_bool(n1)) { return; } @@ -238,7 +238,7 @@ namespace smt { std::swap(n1,n2); TRACE(dyn_ack, tout << mk_pp(n1, m) << " = " << mk_pp(n2, m) << " = " << mk_pp(r, m) << "\n";); - app_triple tr(n1, n2, r); + expr_triple tr(n1, n2, r); if (m_triple.m_instantiated.contains(tr)) { return; } @@ -361,7 +361,7 @@ namespace smt { SASSERT(!m_app_pair2num_occs.contains(a1, a2)); return; } - app_triple tr(0,0,0); + expr_triple tr(0,0,0); if (m_triple.m_clause2apps.find(cls, tr)) { [[maybe_unused]] auto [a1, a2, a3] = tr; SASSERT(a1 && a2 && a3); @@ -451,9 +451,8 @@ namespace smt { m_triple.m_clause2apps.reset(); } - void dyn_ack_manager::reset_app_triples() { - for (app_triple& p : m_triple.m_apps) { - auto [a1, a2, a3] = p; + void dyn_ack_manager::reset_expr_triples() { + for (auto &[a1,a2,a3] : m_triple.m_apps) { m.dec_ref(a1); m.dec_ref(a2); m.dec_ref(a3); @@ -461,7 +460,7 @@ namespace smt { m_triple.m_apps.reset(); } - void dyn_ack_manager::instantiate(app * n1, app * n2, app* r) { + void dyn_ack_manager::instantiate(expr * n1, expr * n2, expr* r) { context& ctx = m_context; SASSERT(m_params.m_dack != dyn_ack_strategy::DACK_DISABLED); SASSERT(n1 != n2 && n1 != r && n2 != r); @@ -471,7 +470,7 @@ namespace smt { << mk_pp(n2, m) << "\n" << mk_pp(r, m) << "\n"; ); - app_triple tr(n1, n2, r); + expr_triple tr(n1, n2, r); SASSERT(m_triple.m_app2num_occs.contains(n1, n2, r)); m_triple.m_app2num_occs.erase(n1, n2, r); // pair n1,n2 is still in m_triple.m_apps @@ -504,22 +503,22 @@ namespace smt { } - struct app_triple_lt { - typedef triple app_triple; - typedef obj_triple_map app_triple2num_occs; - app_triple2num_occs & m_app_triple2num_occs; + struct expr_triple_lt { + typedef triple expr_triple; + typedef obj_triple_map expr_triple2num_occs; + expr_triple2num_occs & m_expr_triple2num_occs; - app_triple_lt(app_triple2num_occs & m): - m_app_triple2num_occs(m) { + expr_triple_lt(expr_triple2num_occs & m): + m_expr_triple2num_occs(m) { } - bool operator()(app_triple const & p1, app_triple const & p2) const { + bool operator()(expr_triple const & p1, expr_triple const & p2) const { auto [a1_1, a1_2, a1_3] = p1; auto [a2_1, a2_2, a2_3] = p2; unsigned n1 = 0; unsigned n2 = 0; - m_app_triple2num_occs.find(a1_1, a1_2, a1_3, n1); - m_app_triple2num_occs.find(a2_1, a2_2, a2_3, n2); + m_expr_triple2num_occs.find(a1_1, a1_2, a1_3, n1); + m_expr_triple2num_occs.find(a2_1, a2_2, a2_3, n2); SASSERT(n1 > 0); SASSERT(n2 > 0); return n1 > n2; @@ -530,11 +529,11 @@ namespace smt { TRACE(dyn_ack, tout << "dyn_ack GC\n";); m_triple.m_to_instantiate.reset(); m_triple.m_qhead = 0; - svector::iterator it = m_triple.m_apps.begin(); - svector::iterator end = m_triple.m_apps.end(); - svector::iterator it2 = it; + svector::iterator it = m_triple.m_apps.begin(); + svector::iterator end = m_triple.m_apps.end(); + svector::iterator it2 = it; for (; it != end; ++it) { - app_triple & p = *it; + expr_triple & p = *it; auto [a1, a2, a3] = p; if (m_triple.m_instantiated.contains(p)) { TRACE(dyn_ack, tout << "1) erasing:\n" << mk_pp(a1, m) << "\n" << mk_pp(a2, m) << "\n";); @@ -548,7 +547,7 @@ namespace smt { m_triple.m_app2num_occs.find(a1, a2, a3, num_occs); // The following invariant is not true. a1 and // a2 may have been instantiated, and removed from - // m_app_triple2num_occs, but not from m_app_triples. + // m_triple.m_app2num_occs, but not from m_triple.m_apps. // // SASSERT(num_occs > 0); num_occs = static_cast(num_occs * m_params.m_dack_gc_inv_decay); @@ -568,8 +567,8 @@ namespace smt { m_triple.m_to_instantiate.push_back(p); } m_triple.m_apps.set_end(it2); - app_triple_lt f(m_triple.m_app2num_occs); - // app_triple_lt is not a total order + expr_triple_lt f(m_triple.m_app2num_occs); + // expr_triple_lt is not a total order std::stable_sort(m_triple.m_to_instantiate.begin(), m_triple.m_to_instantiate.end(), f); } diff --git a/src/smt/dyn_ack.h b/src/smt/dyn_ack.h index 00c220c43..e04f78fd3 100644 --- a/src/smt/dyn_ack.h +++ b/src/smt/dyn_ack.h @@ -36,11 +36,11 @@ namespace smt { typedef obj_pair_hashtable app_pair_set; typedef obj_map clause2app_pair; - typedef triple app_triple; - typedef obj_triple_map app_triple2num_occs; - typedef svector app_triple_vector; - typedef obj_triple_hashtable app_triple_set; - typedef obj_map clause2app_triple; + typedef triple expr_triple; + typedef obj_triple_map expr_triple2num_occs; + typedef svector expr_triple_vector; + typedef obj_triple_hashtable expr_triple_set; + typedef obj_map clause2expr_triple; context & m_context; ast_manager & m; @@ -55,14 +55,14 @@ namespace smt { clause2app_pair m_clause2app_pair; struct _triple { - app_triple2num_occs m_app2num_occs; - app_triple_vector m_apps; - app_triple_vector m_to_instantiate; + expr_triple2num_occs m_app2num_occs; + expr_triple_vector m_apps; + expr_triple_vector m_to_instantiate; unsigned m_qhead; unsigned m_num_instances; unsigned m_num_propagations_since_last_gc; - app_triple_set m_instantiated; - clause2app_triple m_clause2apps; + expr_triple_set m_instantiated; + clause2expr_triple m_clause2apps; }; _triple m_triple; @@ -76,9 +76,9 @@ namespace smt { literal mk_eq(expr * n1, expr * n2); void cg_eh(app * n1, app * n2); - void eq_eh(app * n1, app * n2, app* r); - void instantiate(app * n1, app * n2, app* r); - void reset_app_triples(); + void eq_eh(expr * n1, expr * n2, expr* r); + void instantiate(expr * n1, expr * n2, expr* r); + void reset_expr_triples(); void gc_triples(); public: @@ -112,7 +112,7 @@ namespace smt { /** \brief This method is invoked when equalities are used during conflict resolution. */ - void used_eq_eh(app * n1, app * n2, app* r) { + void used_eq_eh(expr * n1, expr * n2, expr* r) { if (m_params.m_dack_eq) eq_eh(n1, n2, r); } diff --git a/src/smt/qi_queue.cpp b/src/smt/qi_queue.cpp index d4875d77f..a982a03b8 100644 --- a/src/smt/qi_queue.cpp +++ b/src/smt/qi_queue.cpp @@ -140,7 +140,7 @@ namespace smt { tout << "new instance of " << q->get_qid() << ", weight " << q->get_weight() << ", generation: " << generation << ", scope_level: " << m_context.get_scope_level() << ", cost: " << cost << "\n"; for (unsigned i = 0; i < f->get_num_args(); ++i) { - tout << "#" << f->get_arg(i)->get_expr_id() << " d:" << f->get_arg(i)->get_expr()->get_depth() << " "; + tout << "#" << f->get_arg(i)->get_expr_id() << " d:" << get_depth(f->get_arg(i)->get_expr()) << " "; } tout << "\n";); TRACE(new_entries_bug, tout << "[qi:insert]\n";); diff --git a/src/smt/smt_almost_cg_table.cpp b/src/smt/smt_almost_cg_table.cpp index dbbd6b888..f50f34dd6 100644 --- a/src/smt/smt_almost_cg_table.cpp +++ b/src/smt/smt_almost_cg_table.cpp @@ -77,7 +77,7 @@ namespace smt { } bool almost_cg_table::cg_eq::operator()(enode * n1, enode * n2) const { - if (n1->get_expr()->get_decl() != n2->get_expr()->get_decl()) + if (n1->get_decl() != n2->get_decl() || !n1->is_app()) return false; unsigned num_args = n1->get_num_args(); if (num_args != n2->get_num_args()) diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp index c8e378936..bf7c62a32 100644 --- a/src/smt/smt_conflict_resolution.cpp +++ b/src/smt/smt_conflict_resolution.cpp @@ -126,7 +126,7 @@ namespace smt { break; case eq_justification::CONGRUENCE: { CTRACE(dyn_ack_target, !lhs->is_eq(), tout << "dyn_ack_target2: " << lhs->get_owner_id() << " " << rhs->get_owner_id() << "\n";); - m_dyn_ack_manager.used_cg_eh(lhs->get_expr(), rhs->get_expr()); + m_dyn_ack_manager.used_cg_eh(lhs->get_app(), rhs->get_app()); unsigned num_args = lhs->get_num_args(); SASSERT(num_args == rhs->get_num_args()); if (js.used_commutativity()) { @@ -787,8 +787,8 @@ namespace smt { SASSERT(m.has_fact(pr)); expr* f1 = nullptr, *f2 = nullptr; app * fact = to_app(m.get_fact(pr)); - app * n1_owner = n1->get_expr(); - app * n2_owner = n2->get_expr(); + expr * n1_owner = n1->get_expr(); + expr * n2_owner = n2->get_expr(); bool is_eq = m.is_eq(fact, f1, f2); if (is_eq && is_quantifier(f1)) { f1 = m_ctx.get_enode(f1)->get_expr(); @@ -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_expr()->get_decl() == n2->get_expr()->get_decl()); + SASSERT(n1->get_app()->get_decl() == n2->get_app()->get_decl()); if (js.used_commutativity()) { bool visited = true; SASSERT(num_args == 2); @@ -878,8 +878,8 @@ namespace smt { } if (!visited) return nullptr; - app * e1 = n1->get_expr(); - app * e2 = n2->get_expr(); + app * e1 = n1->get_app(); + app * e2 = n2->get_app(); app * e2_prime = m.mk_app(e2->get_decl(), e2->get_arg(1), e2->get_arg(0)); proof * pr1 = nullptr; if (!prs.empty()) { @@ -910,7 +910,7 @@ namespace smt { } if (!visited) return nullptr; - proof * pr = m.mk_congruence(n1->get_expr(), n2->get_expr(), prs.size(), prs.data()); + proof * pr = m.mk_congruence(n1->get_app(), n2->get_app(), prs.size(), prs.data()); m_new_proofs.push_back(pr); return pr; } diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 7b0a8d5ee..f4dce7f8b 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -216,7 +216,7 @@ namespace smt { } ast_translation tr(src_ctx.m, m, false); for (unsigned i = 0; i < src_ctx.m_user_propagator->get_num_vars(); ++i) { - app* e = src_ctx.m_user_propagator->get_expr(i); + auto e = src_ctx.m_user_propagator->get_expr(i); m_user_propagator->add_expr(tr(e), true); } } @@ -653,7 +653,7 @@ namespace smt { lbool val = get_assignment(v); if (val != l_true) { if (val == l_false && js.get_kind() == eq_justification::CONGRUENCE) - m_dyn_ack_manager.cg_conflict_eh(n1->get_expr(), n2->get_expr()); + m_dyn_ack_manager.cg_conflict_eh(n1->get_app(), n2->get_app()); assign(literal(v), mk_justification(eq_propagation_justification(lhs, rhs))); } // It is not necessary to reinsert the equality to the congruence table @@ -919,7 +919,7 @@ namespace smt { lbool val2 = get_assignment(v2); if (val2 != val) { if (val2 != l_undef && congruent(source, target) && source->get_num_args() > 0) - m_dyn_ack_manager.cg_conflict_eh(source->get_expr(), target->get_expr()); + m_dyn_ack_manager.cg_conflict_eh(source->get_app(), target->get_app()); assign(literal(v2, sign), mk_justification(mp_iff_justification(source, target))); } target = target->get_next(); @@ -1137,7 +1137,7 @@ namespace smt { m.inc_ref(eq); _this->m_is_diseq_tmp = enode::mk_dummy(m, m_app2enode, eq); } - else if (m_is_diseq_tmp->get_expr()->get_arg(0)->get_sort() != n1->get_sort()) { + else if (m_is_diseq_tmp->get_arg(0)->get_sort() != n1->get_sort()) { m.dec_ref(m_is_diseq_tmp->get_expr()); app * eq = m.mk_eq(n1->get_expr(), n2->get_expr()); m.inc_ref(eq); @@ -1284,14 +1284,14 @@ namespace smt { enode * r = m_cg_table.find(tmp); #ifdef Z3DEBUG if (r != nullptr) { - SASSERT(r->get_expr()->get_decl() == f); + SASSERT(r->get_decl() == f); SASSERT(r->get_num_args() == num_args); if (r->is_commutative()) { // TODO } else { for (unsigned i = 0; i < num_args; ++i) { - expr * arg = r->get_expr()->get_arg(i); + expr * arg = r->get_arg(i)->get_expr(); SASSERT(e_internalized(arg)); enode * _arg = get_enode(arg); CTRACE(eq_to_bug, args[i]->get_root() != _arg->get_root(), @@ -4672,7 +4672,7 @@ namespace smt { theory_id th_id = l->get_id(); for (enode * parent : enode::parents(n)) { - app* p = parent->get_expr(); + auto p = parent->get_app(); family_id fid = p->get_family_id(); if (fid != th_id && fid != m.get_basic_family_id()) { if (is_beta_redex(parent, n)) @@ -4721,7 +4721,7 @@ namespace smt { } bool context::is_beta_redex(enode* p, enode* n) const { - family_id th_id = p->get_expr()->get_family_id(); + family_id th_id = p->get_family_id(); theory * th = get_theory(th_id); return th && th->is_beta_redex(p, n); } diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 6b84e8d6a..52e6c5b26 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1154,7 +1154,7 @@ namespace smt { void push_eq(enode * lhs, enode * rhs, eq_justification const & js) { if (lhs->get_root() != rhs->get_root()) { - SASSERT(lhs->get_expr()->get_sort() == rhs->get_expr()->get_sort()); + SASSERT(lhs->get_sort() == rhs->get_sort()); m_eq_propagation_queue.push_back(new_eq(lhs, rhs, js)); } } diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index 30c7adf8d..8041099e5 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -545,14 +545,14 @@ namespace smt { out << std::left << n->get_owner_id() << " #"; out.width(5); out << n->get_root()->get_owner_id() << " := " << std::right; - unsigned num = n->get_expr()->get_num_args(); + unsigned num = n->get_num_args(); if (num > 0) out << "("; out << n->get_decl()->get_name(); if (!n->get_decl()->private_parameters()) display_parameters(out, n->get_decl()->get_num_parameters(), n->get_decl()->get_parameters()); for (unsigned i = 0; i < num; ++i) { - expr * arg = n->get_expr()->get_arg(i); + expr * arg = n->get_arg(i)->get_expr(); if (e_internalized(arg)) { enode * n = get_enode(arg)->get_root(); out << " #" << n->get_owner_id(); diff --git a/src/smt/smt_enode.cpp b/src/smt/smt_enode.cpp index b1965c2f3..2f7073afd 100644 --- a/src/smt/smt_enode.cpp +++ b/src/smt/smt_enode.cpp @@ -280,7 +280,7 @@ namespace smt { bool congruent(enode * n1, enode * n2, bool & comm) { comm = false; - if (n1->get_expr()->get_decl() != n2->get_expr()->get_decl()) + if (!n1->is_app() || n1->get_decl() != n2->get_decl()) return false; unsigned num_args = n1->get_num_args(); if (num_args != n2->get_num_args()) diff --git a/src/smt/smt_enode.h b/src/smt/smt_enode.h index ab3dcd141..c3122185c 100644 --- a/src/smt/smt_enode.h +++ b/src/smt/smt_enode.h @@ -166,7 +166,15 @@ namespace smt { void del_eh(ast_manager & m, bool update_children_parent = true); - app * get_expr() const { return m_owner; } + app * get_app() const { return m_owner; } + + expr *get_expr() const { + return m_owner; + } + + bool is_app() const { + return ::is_app(m_owner); + } unsigned get_owner_id() const { return m_owner->get_id(); } unsigned get_expr_id() const { return m_owner->get_id(); } @@ -176,6 +184,10 @@ namespace smt { sort* get_sort() const { return m_owner->get_sort(); } + family_id get_family_id() const { + return m_owner->get_family_id(); + } + unsigned hash() const { return m_owner->hash(); } diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index 93988497d..d09348209 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -459,7 +459,7 @@ namespace smt { tout << "model:\n"; model_pp(tout, *m_curr_model);); for (quantifier* q : *m_qm) - if (m.is_lambda_def(q)) { + if (m.is_lambda_q(q)) { md->add_lambda_defs(); break; } @@ -519,7 +519,7 @@ namespace smt { if (!(m_qm->mbqi_enabled(q) && m_context->is_relevant(q) && m_context->get_assignment(q) == l_true && - (!m_context->get_fparams().m_ematching || !m.is_lambda_def(q)))) { + (!m_context->get_fparams().m_ematching || !m.is_lambda_q(q)))) { if (!m_qm->mbqi_enabled(q)) ++num_failures; continue; diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index b10178f20..7506e85af 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -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_expr()->get_decl() == auf_arr->get_decl()) { + if (ctx->is_relevant(p) && p->get_decl() == auf_arr->get_decl()) { arrays.push_back(p); } } @@ -1449,7 +1449,7 @@ namespace smt { }); node* n1 = s.get_uvar(q, m_var_j); for (enode* n : arrays) { - app* ground_array = n->get_expr(); + auto ground_array = n->get_app(); 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 arrays; get_auf_arrays(get_array(), ctx, arrays); for (enode* curr : arrays) { - app* ground_array = curr->get_expr(); + auto ground_array = curr->get_app(); 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); @@ -1471,8 +1471,8 @@ namespace smt { enode_vector::iterator end2 = curr->end_parents(); for (; it2 != end2; ++it2) { enode* p = *it2; - if (ctx->is_relevant(p) && p->get_expr()->get_decl() == m_select->get_decl()) { - SASSERT(m_arg_i < p->get_expr()->get_num_args()); + if (ctx->is_relevant(p) && p->get_decl() == m_select->get_decl()) { + SASSERT(m_arg_i < p->get_num_args()); enode* e_arg = p->get_arg(m_arg_i); A_f_i->insert(e_arg->get_expr(), e_arg->get_generation()); } @@ -1690,7 +1690,7 @@ namespace smt { typedef ptr_vector::const_iterator macro_iterator; static quantifier_ref mk_flat(ast_manager& m, quantifier* q) { - if (has_quantifiers(q->get_expr()) && !m.is_lambda_def(q)) { + if (has_quantifiers(q->get_expr()) && !m.is_lambda_q(q)) { proof_ref pr(m); expr_ref new_q(m); pull_quant pull(m); @@ -2279,7 +2279,7 @@ namespace smt { void operator()(quantifier_info* d) { m_info = d; quantifier* q = d->get_flat_q(); - if (m.is_lambda_def(q)) return; + if (m.is_lambda_q(q)) return; expr* e = q->get_expr(); reset_cache(); if (!m.inc()) return; diff --git a/src/smt/smt_model_generator.cpp b/src/smt/smt_model_generator.cpp index e49701a33..23973c2bb 100644 --- a/src/smt/smt_model_generator.cpp +++ b/src/smt/smt_model_generator.cpp @@ -105,7 +105,7 @@ namespace smt { proc = alloc(expr_wrapper_proc, m.mk_false()); } else if (m.is_model_value(r->get_expr())) - proc = alloc(expr_wrapper_proc, r->get_expr()); + proc = alloc(expr_wrapper_proc, r->get_app()); else { family_id fid = s->get_family_id(); theory * th = m_context->get_theory(fid); @@ -384,7 +384,7 @@ namespace smt { // send model for (enode * n : m_context->enodes()) { if (is_uninterp_const(n->get_expr()) && m_context->is_relevant(n)) { - func_decl * d = n->get_expr()->get_decl(); + func_decl * d = n->get_decl(); TRACE(mg_top_sort, tout << d->get_name() << " " << (m_hidden_ufs.contains(d)?"hidden":"visible") << "\n";); if (m_hidden_ufs.contains(d)) continue; expr * val = get_value(n); diff --git a/src/smt/smt_theory.h b/src/smt/smt_theory.h index abd8ae798..99da9a0b6 100644 --- a/src/smt/smt_theory.h +++ b/src/smt/smt_theory.h @@ -259,7 +259,7 @@ namespace smt { \brief This method is invoked when the theory application n is marked as relevant. */ - virtual void relevant_eh(app * n) { + virtual void relevant_eh(expr * n) { } /** @@ -435,7 +435,7 @@ namespace smt { return m_var2enode[v]; } - app * get_expr(theory_var v) const { + expr * get_expr(theory_var v) const { return get_enode(v)->get_expr(); } diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index 13e7a0986..c5dc9df66 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -524,7 +524,7 @@ namespace smt { bool has_var(expr * v) const { return get_context().e_internalized(v) && get_context().get_enode(v)->get_th_var(get_id()) != null_theory_var; } theory_var expr2var(expr * v) const { SASSERT(get_context().e_internalized(v)); return get_context().get_enode(v)->get_th_var(get_id()); } - expr * var2expr(theory_var v) const { return get_enode(v)->get_expr(); } + expr * var2expr(theory_var v) const { return get_expr(v); } bool reflection_enabled() const; bool reflect(app * n) const; unsigned lazy_pivoting_lvl() const { return m_params.m_arith_lazy_pivoting_lvl; } @@ -656,7 +656,7 @@ namespace smt { void push_scope_eh() override; void pop_scope_eh(unsigned num_scopes) override; - void relevant_eh(app * n) override; + void relevant_eh(expr * n) override; void restart_eh() override; void init_search_eh() override; @@ -966,7 +966,7 @@ namespace smt { \brief A monomial is 'pure' if does not have a numeric coefficient. */ bool is_pure_monomial(expr * m) const; - bool is_pure_monomial(theory_var v) const { return is_pure_monomial(get_enode(v)->get_expr()); } + bool is_pure_monomial(theory_var v) const { return is_pure_monomial(get_expr(v)); } void mark_var(theory_var v, svector & vars, var_set & already_found); void mark_dependents(theory_var v, svector & vars, var_set & already_found, row_set & already_visited_rows); void get_non_linear_cluster(svector & vars); diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index d4818cec8..0849639d5 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -1086,7 +1086,7 @@ namespace smt { expr_ref theory_arith::mk_gt(theory_var v) { ast_manager& m = get_manager(); inf_numeral const& val = get_value(v); - expr* obj = get_enode(v)->get_expr(); + expr* obj = get_expr(v); expr_ref e(m); rational r = val.get_rational(); if (m_util.is_int(obj->get_sort())) { @@ -1124,7 +1124,7 @@ namespace smt { expr_ref theory_arith::mk_ge(generic_model_converter& fm, theory_var v, inf_numeral const& val) { ast_manager& m = get_manager(); std::ostringstream strm; - strm << val << " <= " << mk_pp(get_enode(v)->get_expr(), get_manager()); + strm << val << " <= " << mk_pp(get_expr(v), get_manager()); app* b = m.mk_const(symbol(strm.str()), m.mk_bool_sort()); expr_ref result(b, m); TRACE(opt, tout << result << "\n";); @@ -1799,7 +1799,7 @@ namespace smt { */ template typename theory_arith::max_min_t theory_arith::max_min(theory_var v, bool max, bool maintain_integrality, bool& has_shared) { - expr* e = get_enode(v)->get_expr(); + expr* e = get_expr(v); (void)e; SASSERT(!maintain_integrality || valid_assignment()); SASSERT(satisfy_bounds()); @@ -2179,8 +2179,8 @@ 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_expr(); - if (o->get_family_id() == get_id()) { + app * o = parent->get_app(); + if (parent->get_family_id() == get_id()) { switch (o->get_decl_kind()) { case OP_DIV: case OP_IDIV: diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 498fa03f4..6ba5eef74 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -1381,18 +1381,19 @@ namespace smt { } template - void theory_arith::relevant_eh(app * n) { + void theory_arith::relevant_eh(expr * n) { TRACE(arith_relevant_eh, tout << "relevant_eh: " << mk_pp(n, m) << "\n";); - if (m_util.is_mod(n)) - mk_idiv_mod_axioms(n->get_arg(0), n->get_arg(1)); - else if (m_util.is_rem(n)) - mk_rem_axiom(n->get_arg(0), n->get_arg(1)); - else if (m_util.is_div(n)) - mk_div_axiom(n->get_arg(0), n->get_arg(1)); + expr* x = nullptr, *y = nullptr; + if (m_util.is_mod(n, x, y)) + mk_idiv_mod_axioms(x, y); + else if (m_util.is_rem(n, x, y)) + mk_rem_axiom(x, y); + else if (m_util.is_div(n, x, y)) + mk_div_axiom(x, y); else if (m_util.is_to_int(n)) - mk_to_int_axiom(n); + mk_to_int_axiom(to_app(n)); else if (m_util.is_is_int(n)) - mk_is_int_axiom(n); + mk_is_int_axiom(to_app(n)); } template @@ -1451,8 +1452,8 @@ namespace smt { template void theory_arith::new_diseq_eh(theory_var v1, theory_var v2) { - TRACE(arith_new_diseq_eh, tout << mk_bounded_pp(get_enode(v1)->get_expr(), m) << "\n" << - mk_bounded_pp(get_enode(v2)->get_expr(), m) << "\n";); + TRACE(arith_new_diseq_eh, tout << mk_bounded_pp(get_expr(v1), m) << "\n" << + mk_bounded_pp(get_expr(v2), m) << "\n";); m_stats.m_assert_diseq++; m_arith_eq_adapter.new_diseq_eh(v1, v2); } diff --git a/src/smt/theory_arith_int.h b/src/smt/theory_arith_int.h index 8c70ac66f..fe02fe884 100644 --- a/src/smt/theory_arith_int.h +++ b/src/smt/theory_arith_int.h @@ -215,7 +215,7 @@ namespace smt { tout << "k = " << k << ", _k = "<< _k << std::endl; ); expr_ref bound(m); - expr* e = get_enode(v)->get_expr(); + expr* e = get_expr(v); bound = m_util.mk_ge(e, m_util.mk_numeral(_k, m_util.is_int(e))); context & ctx = get_context(); { @@ -413,7 +413,7 @@ namespace smt { for (; it != end; ++it) { if (!it->is_dead() && it->m_var != b && is_free(it->m_var)) { theory_var v = it->m_var; - expr* e = get_enode(v)->get_expr(); + expr* e = get_expr(v); bool _is_int = m_util.is_int(e); expr_ref bound(m_util.mk_ge(e, m_util.mk_numeral(rational::zero(), _is_int)), get_manager()); context & ctx = get_context(); @@ -629,9 +629,9 @@ namespace smt { } rational _k = k.to_rational(); if (is_lower) - bound = m_util.mk_ge(get_enode(v)->get_expr(), m_util.mk_numeral(_k, is_int(v))); + bound = m_util.mk_ge(get_expr(v), m_util.mk_numeral(_k, is_int(v))); else - bound = m_util.mk_le(get_enode(v)->get_expr(), m_util.mk_numeral(_k, is_int(v))); + bound = m_util.mk_le(get_expr(v), m_util.mk_numeral(_k, is_int(v))); } else { if (num_ints > 0) { diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index 1fd80c365..749ac8251 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -653,7 +653,7 @@ theory_var theory_arith::find_nl_var_for_branching() { bool computed_epsilon = false; bool r = check_monomial_assignment(v, computed_epsilon); if (!r) { - expr * m = get_enode(v)->get_expr(); + expr * m = get_expr(v); SASSERT(is_pure_monomial(m)); for (expr * arg : *to_app(m)) { theory_var curr = ctx.get_enode(arg)->get_th_var(get_id()); diff --git a/src/smt/theory_arith_pp.h b/src/smt/theory_arith_pp.h index 7448f6db8..81ed03762 100644 --- a/src/smt/theory_arith_pp.h +++ b/src/smt/theory_arith_pp.h @@ -484,7 +484,7 @@ namespace smt { pp.set_benchmark_name("lemma"); int n = get_num_vars(); for (theory_var v = 0; v < n; ++v) { - expr * n = get_enode(v)->get_expr(); + expr * n = get_expr(v); if (is_fixed(v)) { inf_numeral k_inf = lower_bound(v); rational k = k_inf.get_rational().to_rational(); diff --git a/src/smt/theory_array.cpp b/src/smt/theory_array.cpp index 5c9ac3a80..8e3827188 100644 --- a/src/smt/theory_array.cpp +++ b/src/smt/theory_array.cpp @@ -42,7 +42,7 @@ namespace smt { // v1 is the new root TRACE(array, tout << "merging v" << v1 << " v" << v2 << "\n"; display_var(tout, v1); - tout << mk_pp(get_enode(v1)->get_expr(), m) << " <- " << mk_pp(get_enode(v2)->get_expr(), m) << "\n";); + tout << mk_pp(get_expr(v1), m) << " <- " << mk_pp(get_expr(v2), m) << "\n";); SASSERT(v1 == find(v1)); var_data * d1 = m_var_data[v1]; var_data * d2 = m_var_data[v2]; @@ -88,7 +88,7 @@ namespace smt { v = find(v); var_data * d = m_var_data[v]; d->m_parent_selects.push_back(s); - TRACE(array, tout << v << " " << mk_pp(s->get_expr(), m) << " " << mk_pp(get_enode(v)->get_expr(), m) << "\n";); + TRACE(array, tout << v << " " << mk_pp(s->get_expr(), m) << " " << mk_pp(get_expr(v), m) << "\n";); m_trail_stack.push(push_back_trail(d->m_parent_selects)); for (enode* n : d->m_stores) instantiate_axiom2a(s, n); @@ -299,8 +299,8 @@ namespace smt { void theory_array::new_eq_eh(theory_var v1, theory_var v2) { m_find.merge(v1, v2); enode* n1 = get_enode(v1), *n2 = get_enode(v2); - if (n1->get_expr()->get_decl()->is_lambda() || - n2->get_expr()->get_decl()->is_lambda()) { + if (n1->get_decl()->is_lambda() || + n2->get_decl()->is_lambda()) { assert_congruent(n1, n2); } } @@ -310,8 +310,8 @@ namespace smt { v2 = find(v2); var_data * d1 = m_var_data[v1]; TRACE(ext, tout << "extensionality: " << d1->m_is_array << "\n" - << mk_bounded_pp(get_enode(v1)->get_expr(), m, 5) << "\n" - << mk_bounded_pp(get_enode(v2)->get_expr(), m, 5) << "\n";); + << mk_bounded_pp(get_expr(v1), m, 5) << "\n" + << mk_bounded_pp(get_expr(v2), m, 5) << "\n";); if (d1->m_is_array) { SASSERT(m_var_data[v2]->m_is_array); @@ -319,7 +319,7 @@ namespace smt { } } - void theory_array::relevant_eh(app * n) { + void theory_array::relevant_eh(expr * n) { if (laziness() == 0) return; if (m.is_ite(n)) { @@ -328,7 +328,7 @@ namespace smt { if (!is_store(n) && !is_select(n)) return; if (!ctx.e_internalized(n)) ctx.internalize(n, false); - enode * arg = ctx.get_enode(n->get_arg(0)); + enode * arg = ctx.get_enode(to_app(n)->get_arg(0)); theory_var v_arg = arg->get_th_var(get_id()); SASSERT(v_arg != null_theory_var); diff --git a/src/smt/theory_array.h b/src/smt/theory_array.h index 899f3cd64..d6ce0f4b9 100644 --- a/src/smt/theory_array.h +++ b/src/smt/theory_array.h @@ -59,7 +59,7 @@ namespace smt { void apply_sort_cnstr(enode * n, sort * s) override; void new_eq_eh(theory_var v1, theory_var v2) override; void new_diseq_eh(theory_var v1, theory_var v2) override; - void relevant_eh(app * n) override; + void relevant_eh(expr * n) override; void push_scope_eh() override; void pop_scope_eh(unsigned num_scopes) override; final_check_status final_check_eh(unsigned) override; diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp index 979c55de6..b4966c2a7 100644 --- a/src/smt/theory_array_base.cpp +++ b/src/smt/theory_array_base.cpp @@ -108,7 +108,7 @@ namespace smt { } void theory_array_base::assert_store_axiom1_core(enode * e) { - app * n = e->get_expr(); + app * n = e->get_app(); SASSERT(is_store(n)); ptr_buffer sel_args; unsigned num_args = n->get_num_args(); @@ -235,10 +235,6 @@ namespace smt { return false; } - - - - func_decl_ref_vector * theory_array_base::register_sort(sort * s_array) { unsigned dimension = get_dimension(s_array); func_decl_ref_vector * ext_skolems = nullptr; @@ -333,8 +329,8 @@ namespace smt { void theory_array_base::assert_extensionality_core(enode * n1, enode * n2) { - app * e1 = n1->get_expr(); - app * e2 = n2->get_expr(); + expr * e1 = n1->get_expr(); + expr * e2 = n2->get_expr(); func_decl_ref_vector * funcs = nullptr; sort * s = e1->get_sort(); @@ -371,8 +367,8 @@ namespace smt { \brief assert n1 = n2 => forall vars . (n1 vars) = (n2 vars) */ void theory_array_base::assert_congruent_core(enode * n1, enode * n2) { - app * e1 = n1->get_expr(); - app * e2 = n2->get_expr(); + expr * e1 = n1->get_expr(); + expr * e2 = n2->get_expr(); sort* s = e1->get_sort(); unsigned dimension = get_array_arity(s); literal n1_eq_n2 = mk_eq(e1, e2, true); @@ -403,13 +399,13 @@ namespace smt { assert_axiom(~n1_eq_n2, fa_eq); } - expr_ref theory_array_base::instantiate_lambda(app* e) { - quantifier * q = m.is_lambda_def(e->get_decl()); + expr_ref theory_array_base::instantiate_lambda(expr* e) { + quantifier * q = m.is_lambda_def(e); expr_ref f(e, m); if (q) { // the variables in q are maybe not consecutive. var_subst sub(m, false); - f = sub(q, e->get_num_args(), e->get_args()); + f = sub(q, to_app(e)->get_num_args(), to_app(e)->get_args()); } return f; } @@ -561,13 +557,13 @@ namespace smt { TRACE(array_bug, tout << "mk_interface_eqs: processing: v" << *it1 << "\n";); theory_var v1 = *it1; enode * n1 = get_enode(v1); - sort * s1 = n1->get_expr()->get_sort(); + sort * s1 = n1->get_sort(); sbuffer::iterator it2 = it1; ++it2; for (; it2 != end1; ++it2) { theory_var v2 = *it2; enode * n2 = get_enode(v2); - sort * s2 = n2->get_expr()->get_sort(); + sort * s2 = n2->get_sort(); if (s1 == s2 && !ctx.is_diseq(n1, n2)) { app * eq = mk_eq_atom(n1->get_expr(), n2->get_expr()); if (!ctx.b_internalized(eq) || !ctx.is_relevant(eq)) { @@ -974,7 +970,7 @@ namespace smt { model_value_proc * theory_array_base::mk_value(enode * n, model_generator & mg) { theory_var v = n->get_th_var(get_id()); SASSERT(v != null_theory_var); - sort * s = n->get_expr()->get_sort(); + sort * s = n->get_sort(); enode * else_val_n = get_default(v); array_value_proc * result = nullptr; diff --git a/src/smt/theory_array_base.h b/src/smt/theory_array_base.h index 87a84cfa3..f9bf35e13 100644 --- a/src/smt/theory_array_base.h +++ b/src/smt/theory_array_base.h @@ -33,19 +33,19 @@ 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_expr()); } - void found_unsupported_op(theory_var v) { found_unsupported_op(get_enode(v)->get_expr()); } + 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()); } - bool is_store(app const* n) const { return n->is_app_of(get_id(), OP_STORE); } - bool is_map(app const* n) const { return n->is_app_of(get_id(), OP_ARRAY_MAP); } - bool is_select(app const* n) const { return n->is_app_of(get_id(), OP_SELECT); } - bool is_default(app const* n) const { return n->is_app_of(get_id(), OP_ARRAY_DEFAULT); } - bool is_const(app const* n) const { return n->is_app_of(get_id(), OP_CONST_ARRAY); } - bool is_array_ext(app const * n) const { return n->is_app_of(get_id(), OP_ARRAY_EXT); } - bool is_as_array(app const * n) const { return n->is_app_of(get_id(), OP_AS_ARRAY); } - bool is_choice(app const* n) const { return n->is_app_of(get_id(), OP_CHOICE); } + 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); } + bool is_select(expr const* n) const { return is_app(n) && to_app(n)->is_app_of(get_id(), OP_SELECT); } + bool is_default(expr const* n) const { return is_app(n) && to_app(n)->is_app_of(get_id(), OP_ARRAY_DEFAULT); } + bool is_const(expr const* n) const { return is_app(n) && to_app(n)->is_app_of(get_id(), OP_CONST_ARRAY); } + bool is_array_ext(expr const * n) const { return is_app(n) && to_app(n)->is_app_of(get_id(), OP_ARRAY_EXT); } + bool is_as_array(expr const * n) const { return is_app(n) && to_app(n)->is_app_of(get_id(), OP_AS_ARRAY); } + bool is_choice(expr const* n) const { return is_app(n) && to_app(n)->is_app_of(get_id(), OP_CHOICE); } bool is_array_sort(sort const* s) const { return s->is_sort_of(get_id(), ARRAY_SORT); } - bool is_array_sort(app const* n) const { return is_array_sort(n->get_sort()); } + bool is_array_sort(expr const* n) const { return is_array_sort(n->get_sort()); } bool is_store(enode const * n) const { return is_store(n->get_expr()); } bool is_map(enode const* n) const { return is_map(n->get_expr()); } @@ -54,7 +54,7 @@ namespace smt { bool is_as_array(enode const * n) const { return is_as_array(n->get_expr()); } bool is_choice(enode const* n) const { return is_choice(n->get_expr()); } bool is_default(enode const* n) const { return is_default(n->get_expr()); } - bool is_array_sort(enode const* n) const { return is_array_sort(n->get_expr()); } + bool is_array_sort(enode const* n) const { return is_array_sort(n->get_sort()); } bool is_select_arg(enode* r); app * mk_select(unsigned num_args, expr * const * args); @@ -82,7 +82,7 @@ namespace smt { void assert_extensionality_core(enode * a1, enode * a2); bool assert_extensionality(enode * a1, enode * a2); - expr_ref instantiate_lambda(app* e); + expr_ref instantiate_lambda(expr* e); void assert_congruent_core(enode * a1, enode * a2); void assert_congruent(enode * a1, enode * a2); diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp index 736e447d3..28f4f17d8 100644 --- a/src/smt/theory_array_full.cpp +++ b/src/smt/theory_array_full.cpp @@ -248,7 +248,7 @@ namespace smt { instantiate_default_as_array_axiom(n); d->m_as_arrays.push_back(n); } - else if (m.is_lambda_def(n->get_decl())) { + else if (m.is_lambda_def(n->get_expr())) { instantiate_default_lambda_def_axiom(n); d->m_lambdas.push_back(n); m_lambdas.push_back(n); @@ -406,22 +406,23 @@ namespace smt { } } - void theory_array_full::relevant_eh(app* n) { + void theory_array_full::relevant_eh(expr* n) { TRACE(array, tout << mk_pp(n, m) << "\n";); theory_array::relevant_eh(n); - if (!is_default(n) && !is_select(n) && !is_map(n) && !is_const(n) && !is_as_array(n) && !is_choice(n)){ + if (!is_default(n) && !is_select(n) && !is_map(n) && + !is_const(n) && !is_as_array(n) && !is_choice(n) && !is_lambda(n)){ return; } ctx.ensure_internalized(n); enode* node = ctx.get_enode(n); if (is_select(n)) { - enode * arg = ctx.get_enode(n->get_arg(0)); + enode * arg = ctx.get_enode(to_app(n)->get_arg(0)); theory_var v = arg->get_th_var(get_id()); SASSERT(v != null_theory_var); add_parent_select(find(v), node); } else if (is_default(n)) { - enode * arg = ctx.get_enode(n->get_arg(0)); + enode * arg = ctx.get_enode(to_app(n)->get_arg(0)); theory_var v = arg->get_th_var(get_id()); SASSERT(v != null_theory_var); set_prop_upward(v); @@ -434,7 +435,7 @@ namespace smt { add_parent_default(find(v)); } else if (is_map(n)) { - for (expr * e : *n) { + for (expr * e : *to_app(n)) { enode* arg = ctx.get_enode(e); theory_var v_arg = find(arg->get_th_var(get_id())); add_parent_map(v_arg, node); @@ -448,6 +449,9 @@ namespace smt { else if (is_choice(n)) { instantiate_choice_axiom(node); } + else if (is_lambda(n)) { + NOT_IMPLEMENTED_YET(); + } } bool theory_array_full::should_research(expr_ref_vector & unsat_core) { @@ -462,8 +466,8 @@ namespace smt { // select(map[f](a, ... d), i) = f(select(a,i),...,select(d,i)) // bool theory_array_full::instantiate_select_map_axiom(enode* sl, enode* mp) { - app* map = mp->get_expr(); - app* select = sl->get_expr(); + app* map = mp->get_app(); + app* select = sl->get_app(); SASSERT(is_map(map)); SASSERT(is_select(select)); SASSERT(map->get_num_args() > 0); @@ -529,7 +533,7 @@ namespace smt { bool theory_array_full::instantiate_default_map_axiom(enode* mp) { SASSERT(is_map(mp)); - app* map = mp->get_expr(); + app* map = mp->get_app(); if (!ctx.add_fingerprint(this, m_default_map_fingerprint, 1, &mp)) { return false; } @@ -581,7 +585,7 @@ namespace smt { m_stats.m_num_default_lambda_axiom++; expr* e = arr->get_expr(); expr_ref def(mk_default(e), m); - quantifier* lam = m.is_lambda_def(arr->get_decl()); + quantifier* lam = m.is_lambda_def(e); TRACE(array, tout << mk_pp(lam, m) << "\n" << mk_pp(e, m) << "\n"); expr_ref_vector args(m); var_subst subst(m, false); @@ -607,7 +611,7 @@ namespace smt { return false; ++m_stats.m_num_choice_axiom; SASSERT(is_choice(ch)); - app* choice_term = ch->get_expr(); + app* choice_term = ch->get_app(); expr* pred = choice_term->get_arg(0); sort* pred_sort = pred->get_sort(); SASSERT(is_array_sort(pred_sort)); @@ -645,10 +649,10 @@ namespace smt { ptr_buffer sel_args; sel_args.push_back(cnst->get_expr()); for (unsigned short i = 1; i < num_args; ++i) { - sel_args.push_back(select->get_expr()->get_arg(i)); + sel_args.push_back(select->get_app()->get_arg(i)); } expr * sel = mk_select(sel_args.size(), sel_args.data()); - expr * val = cnst->get_expr()->get_arg(0); + expr * val = cnst->get_app()->get_arg(0); TRACE(array, tout << "new select-const axiom...\n"; tout << "const: " << mk_bounded_pp(cnst->get_expr(), m) << "\n"; tout << "select: " << mk_bounded_pp(select->get_expr(), m) << "\n"; @@ -667,7 +671,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_expr())); + SASSERT(is_as_array(arr->get_app())); SASSERT(is_select(select)); SASSERT(arr->get_num_args() == 0); unsigned num_args = select->get_num_args(); @@ -677,12 +681,12 @@ namespace smt { m_stats.m_num_select_as_array_axiom++; ptr_buffer sel_args; - sel_args.push_back(arr->get_expr()); + sel_args.push_back(arr->get_app()); for (unsigned short i = 1; i < num_args; ++i) { - sel_args.push_back(select->get_expr()->get_arg(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_expr()); + func_decl * f = array_util(m).get_as_array_func_decl(arr->get_app()); 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"; @@ -701,7 +705,7 @@ namespace smt { bool theory_array_full::instantiate_default_store_axiom(enode* store) { SASSERT(is_store(store)); SASSERT(store->get_num_args() >= 3); - app* store_app = store->get_expr(); + app* store_app = store->get_app(); if (!ctx.add_fingerprint(this, m_default_store_fingerprint, store->get_num_args(), store->get_args())) { return false; } diff --git a/src/smt/theory_array_full.h b/src/smt/theory_array_full.h index 699730358..97e9d06a6 100644 --- a/src/smt/theory_array_full.h +++ b/src/smt/theory_array_full.h @@ -60,7 +60,7 @@ namespace smt { bool internalize_atom(app * atom, bool gate_ctx) override; void pop_scope_eh(unsigned num_scopes) override; theory_var mk_var(enode * n) override; - void relevant_eh(app * n) override; + void relevant_eh(expr * n) override; bool should_research(expr_ref_vector & unsat_core) override; void add_theory_assumptions(expr_ref_vector & assumptions) override; @@ -81,6 +81,7 @@ namespace smt { bool instantiate_default_map_axiom(enode* map); bool instantiate_default_as_array_axiom(enode* arr); bool instantiate_default_lambda_def_axiom(enode* arr); + bool instantiate_select_lambda_axiom(enode *lambda); bool instantiate_choice_axiom(enode* ch); bool instantiate_parent_stores_default(theory_var v); diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index 92d10a81a..145650b63 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -38,7 +38,7 @@ namespace smt { return r; } - app * theory_bv::mk_bit2bool(app * bv, unsigned idx) { + app * theory_bv::mk_bit2bool(expr * bv, unsigned idx) { parameter p(idx); expr * args[1] = {bv}; return get_manager().mk_app(get_id(), OP_BIT2BOOL, 1, &p, 1, args); @@ -46,7 +46,7 @@ namespace smt { void theory_bv::mk_bits(theory_var v) { enode * n = get_enode(v); - app * owner = n->get_expr(); + expr * owner = n->get_expr(); unsigned bv_size = get_bv_size(n); bool is_relevant = ctx.is_relevant(n); literal_vector & bits = m_bits[v]; @@ -180,7 +180,7 @@ namespace smt { return n->get_arg(idx); } else { - app * arg = to_app(n->get_expr()->get_arg(idx)); + app * arg = to_app(n->get_app()->get_arg(idx)); SASSERT(ctx.e_internalized(arg)); return ctx.get_enode(arg); } @@ -236,8 +236,8 @@ namespace smt { TRACE(bv_diseq_axiom, tout << "found new diseq axiom\n"; display_var(tout, v1); display_var(tout, v2);); // found new disequality m_stats.m_num_diseq_static++; - app * e1 = get_expr(v1); - app * e2 = get_expr(v2); + expr * e1 = get_expr(v1); + expr * e2 = get_expr(v2); expr_ref eq(m.mk_eq(e1, e2), m); literal l = ~mk_literal(eq); std::function logfn = [&]() { @@ -438,8 +438,8 @@ namespace smt { return; } ++m_stats.m_num_eq_dynamic; - app* o1 = get_enode(v1)->get_expr(); - app* o2 = get_enode(v2)->get_expr(); + expr* o1 = get_expr(v1); + expr* o2 = get_expr(v2); literal oeq = mk_eq(o1, o2, true); ctx.mark_as_relevant(oeq); @@ -475,7 +475,7 @@ namespace smt { VERIFY(get_fixed_value(v, val)); enode* n = get_enode(v); if (ctx.watches_fixed(n)) { - expr_ref num(m_util.mk_numeral(val, n->get_expr()->get_sort()), m); + expr_ref num(m_util.mk_numeral(val, n->get_sort()), m); literal_vector& lits = m_tmp_literals; lits.reset(); for (literal b : m_bits[v]) { @@ -1124,15 +1124,18 @@ namespace smt { // Determine whether bit-vector expression should be approximated // based on the number of bits used by the arguments. // - bool theory_bv::approximate_term(app* n) { + bool theory_bv::approximate_term(expr *e) { if (params().m_bv_blast_max_size == INT_MAX) { return false; } + if (!is_app(e)) + return false; + app *n = to_app(e); unsigned num_args = n->get_num_args(); for (unsigned i = 0; i <= num_args; ++i) { - expr* arg = (i == num_args)?n:n->get_arg(i); - sort* s = arg->get_sort(); - if (m_util.is_bv_sort(s) && m_util.get_bv_size(arg) > params().m_bv_blast_max_size) { + expr *arg = (i == num_args) ? n : n->get_arg(i); + sort *s = arg->get_sort(); + if (m_util.is_bv_sort(s) && m_util.get_bv_size(arg) > params().m_bv_blast_max_size) { if (!m_approximates_large_bvs) { TRACE(bv, tout << "found large size bit-vector:\n" << mk_pp(n, m) << "\n";); ctx.push_trail(value_trail(m_approximates_large_bvs)); @@ -1148,13 +1151,13 @@ 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_expr()); + relevant_eh(n->get_app()); } } } void theory_bv::new_eq_eh(theory_var v1, theory_var v2) { - TRACE(bv_eq, tout << "new_eq: " << mk_pp(get_enode(v1)->get_expr(), m) << " = " << mk_pp(get_enode(v2)->get_expr(), m) << "\n";); + TRACE(bv_eq, tout << "new_eq: " << mk_pp(get_expr(v1), m) << " = " << mk_pp(get_expr(v2), m) << "\n";); TRACE(bv, tout << "new_eq_eh v" << v1 << " = v" << v2 << " @ " << ctx.get_scope_level() << " relevant1: " << ctx.is_relevant(get_enode(v1)) << " relevant2: " << ctx.is_relevant(get_enode(v2)) << "\n";); @@ -1218,7 +1221,7 @@ namespace smt { literal_vector & lits = m_tmp_literals; lits.reset(); - literal eq = mk_eq(get_enode(v1)->get_expr(), get_enode(v2)->get_expr(), true); + literal eq = mk_eq(get_expr(v1), get_expr(v2), true); lits.push_back(eq); it1 = bits1.begin(); it2 = bits2.begin(); @@ -1232,7 +1235,7 @@ namespace smt { lits.push_back(arg); } TRACE(bv, - tout << mk_pp(get_enode(v1)->get_expr(), m) << " = " << mk_pp(get_enode(v2)->get_expr(), m) << " " + tout << mk_pp(get_expr(v1), m) << " = " << mk_pp(get_expr(v2), m) << " " << ctx.get_scope_level() << "\n"; ctx.display_literals_smt2(tout, lits);); @@ -1385,7 +1388,7 @@ namespace smt { } } - void theory_bv::relevant_eh(app * n) { + void theory_bv::relevant_eh(expr * n) { TRACE(arith, tout << "relevant: #" << n->get_id() << " " << ctx.e_internalized(n) << ": " << mk_bounded_pp(n, m) << "\n";); TRACE(bv, tout << "relevant: #" << n->get_id() << " " << ctx.e_internalized(n) << ": " << mk_pp(n, m) << "\n";); if (m.is_bool(n)) { @@ -1403,18 +1406,18 @@ namespace smt { } } else if (params().m_bv_enable_int2bv2int && m_util.is_ubv2int(n)) { - ctx.mark_as_relevant(n->get_arg(0)); - assert_bv2int_axiom(n); + ctx.mark_as_relevant(to_app(n)->get_arg(0)); + assert_bv2int_axiom(to_app(n)); } else if (params().m_bv_enable_int2bv2int && m_util.is_int2bv(n)) { - ctx.mark_as_relevant(n->get_arg(0)); - assert_int2bv_axiom(n); + ctx.mark_as_relevant(to_app(n)->get_arg(0)); + assert_int2bv_axiom(to_app(n)); } #if ENABLE_QUOT_REM_ENCODING else if (m_util.is_bv_udivi(n)) { - ctx.mark_as_relevant(n->get_arg(0)); - ctx.mark_as_relevant(n->get_arg(1)); - assert_udiv_quot_rem_axiom(n); + ctx.mark_as_relevant(to_app(n)->get_arg(0)); + ctx.mark_as_relevant(to_app(n)->get_arg(1)); + assert_udiv_quot_rem_axiom(to_app(n)); } #endif else if (ctx.e_internalized(n)) { diff --git a/src/smt/theory_bv.h b/src/smt/theory_bv.h index 476912117..9bcd331b7 100644 --- a/src/smt/theory_bv.h +++ b/src/smt/theory_bv.h @@ -142,15 +142,15 @@ 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_expr()); } + unsigned get_bv_size(enode const * n) const { return m_util.get_bv_size(n->get_app()); } 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_expr()); } + bool is_bv(enode const* n) const { return is_bv(n->get_app()); } bool is_bv(theory_var v) const { return is_bv(get_enode(v)); } region & get_region() { return m_trail_stack.get_region(); } - bool is_numeral(theory_var v) const { return m_util.is_numeral(get_enode(v)->get_expr()); } - app * mk_bit2bool(app * bv, unsigned idx); + bool is_numeral(theory_var v) const { return m_util.is_numeral(get_expr(v)); } + app * mk_bit2bool(expr * bv, unsigned idx); void mk_bits(theory_var v); friend class mk_atom_trail; void mk_bit2bool(app * n); @@ -217,7 +217,7 @@ namespace smt { void internalize_smul_no_overflow(app *n); void internalize_smul_no_underflow(app *n); - bool approximate_term(app* n); + bool approximate_term(expr* e); template void internalize_le(app * atom); @@ -240,7 +240,7 @@ namespace smt { void new_diseq_eh(theory_var v1, theory_var v2) override; virtual void expand_diseq(theory_var v1, theory_var v2); void assign_eh(bool_var v, bool is_true) override; - void relevant_eh(app * n) override; + void relevant_eh(expr * n) override; void push_scope_eh() override; void pop_scope_eh(unsigned num_scopes) override; final_check_status final_check_eh(unsigned) override; diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index e8149c183..6b3428998 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -138,7 +138,7 @@ namespace smt { where acc_i are the accessors of constructor c. */ void theory_datatype::assert_is_constructor_axiom(enode * n, func_decl * c, literal antecedent) { - app* e = n->get_expr(); + app* e = n->get_app(); TRACE(datatype_bug, tout << "creating axiom (= n (c (acc_1 n) ... (acc_m n))) for\n" << mk_pp(c, m) << " " << mk_pp(e, m) << "\n";); m_stats.m_assert_cnstr++; @@ -175,12 +175,12 @@ namespace smt { vector> 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_expr()); + bindings.push_back(n->get_arg(i)->get_app()); } 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_expr()), m); + app_ref acc_app(m.mk_app(acc, n->get_app()), m); enode * arg = n->get_arg(i); std::function fn = [&]() { @@ -223,7 +223,7 @@ namespace smt { void theory_datatype::assert_update_field_axioms(enode * n) { m_stats.m_assert_update_field++; SASSERT(is_update_field(n)); - app* own = n->get_expr(); + app* own = n->get_app(); expr* arg1 = own->get_arg(0); func_decl * upd = n->get_decl(); func_decl * acc = to_func_decl(upd->get_parameter(0).get_ast()); @@ -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_expr(), n->get_expr()), m); + app_ref reflex(m.mk_app(sub_decl, n->get_app(), n->get_app()), 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_expr()), m); + app_ref def(m_autil.mk_default(arg->get_app()), m); if (!ctx.e_internalized(def)) { ctx.internalize(def, false); } @@ -542,7 +542,7 @@ namespace smt { ptr_vector candidates = list_subterms(arg2); for (enode *s : candidates) { - bool is_leaf = !m_util.is_constructor(s->get_expr()); + bool is_leaf = !m_util.is_constructor(s->get_app()); // 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_expr(), s->get_expr())); + auto tmp = m.mk_not(m.mk_app(sub_decl, arg1->get_app(), s->get_app())); lits.push_back(mk_literal(tmp)); found_possible = true; } @@ -617,7 +617,7 @@ namespace smt { ptr_vector candidates = list_subterms(arg2); for (enode *s : candidates) { - bool is_leaf = !m_util.is_constructor(s->get_expr()); + bool is_leaf = !m_util.is_constructor(s->get_app()); 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_expr(), s->get_expr()); + auto sub_app = m.mk_app(sub_decl, arg1->get_app(), s->get_app()); 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_expr())) { + if (f.th.m_util.is_constructor(iter->get_app())) { ctor = iter; break; } @@ -706,7 +706,7 @@ namespace smt { return result; } - void theory_datatype::relevant_eh(app * n) { + void theory_datatype::relevant_eh(expr * n) { force_push(); TRACE(datatype, tout << "relevant_eh: " << mk_pp(n, m) << "\n";); SASSERT(ctx.relevancy()); @@ -967,7 +967,7 @@ namespace smt { }; for (enode* sib : *n) { - if (m_sutil.str.is_concat_of_units(sib->get_expr())) { + if (m_sutil.str.is_concat_of_units(sib->get_app())) { add_todo(sib); sibling = sib; break; @@ -994,7 +994,7 @@ namespace smt { theory_array* th = dynamic_cast(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_expr()), m); + app_ref def(m_autil.mk_default(n->get_app()), m); m_args.push_back(ctx.get_enode(def)); return m_args; } @@ -1328,7 +1328,7 @@ namespace smt { if (!r) { ptr_vector 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_expr()); + auto rec_app = m.mk_app(rec, n->get_app()); 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_expr()), m); + app_ref r_app(m.mk_app(r, n->get_app()), 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); diff --git a/src/smt/theory_datatype.h b/src/smt/theory_datatype.h index 88c3be3a0..be6b3d61a 100644 --- a/src/smt/theory_datatype.h +++ b/src/smt/theory_datatype.h @@ -68,17 +68,17 @@ namespace smt { datatype_factory * m_factory; stats m_stats; - bool is_constructor(app * f) const { return m_util.is_constructor(f); } - bool is_recognizer(app * f) const { return m_util.is_recognizer(f); } - bool is_subterm_predicate(app * f) const { return m_util.is_subterm_predicate(f); } - bool is_accessor(app * f) const { return m_util.is_accessor(f); } - bool is_update_field(app * f) const { return m_util.is_update_field(f); } + bool is_constructor(expr * f) const { return m_util.is_constructor(f); } + bool is_recognizer(expr * f) const { return m_util.is_recognizer(f); } + bool is_subterm_predicate(expr * f) const { return m_util.is_subterm_predicate(f); } + bool is_accessor(expr * f) const { return m_util.is_accessor(f); } + bool is_update_field(expr * f) const { return m_util.is_update_field(f); } bool is_constructor(enode * n) const { return is_constructor(n->get_expr()); } bool is_recognizer(enode * n) const { return is_recognizer(n->get_expr()); } bool is_subterm_predicate(enode * n) const { return is_subterm_predicate(n->get_expr()); } bool is_accessor(enode * n) const { return is_accessor(n->get_expr()); } - bool is_update_field(enode * n) const { return m_util.is_update_field(n->get_expr()); } + bool is_update_field(enode * n) const { return is_update_field(n->get_expr()); } void assert_eq_axiom(enode * lhs, expr * rhs, literal antecedent); void assert_is_constructor_axiom(enode * n, func_decl * c, literal antecedent); @@ -148,7 +148,7 @@ namespace smt { bool use_diseqs() const override; void new_diseq_eh(theory_var v1, theory_var v2) override; void assign_eh(bool_var v, bool is_true) override; - void relevant_eh(app * n) override; + void relevant_eh(expr * n) override; void push_scope_eh() override; void pop_scope_eh(unsigned num_scopes) override; final_check_status final_check_eh(unsigned) override; diff --git a/src/smt/theory_dense_diff_logic_def.h b/src/smt/theory_dense_diff_logic_def.h index 83c65d810..243629db7 100644 --- a/src/smt/theory_dense_diff_logic_def.h +++ b/src/smt/theory_dense_diff_logic_def.h @@ -721,7 +721,7 @@ namespace smt { TRACE(ddl_model, tout << "ddl model\n"; for (theory_var v = 0; v < num_vars; ++v) { - tout << "#" << mk_pp(get_enode(v)->get_expr(), m) << " = " << m_assignment[v] << "\n"; + tout << "#" << mk_pp(get_expr(v), m) << " = " << m_assignment[v] << "\n"; }); } @@ -799,11 +799,11 @@ namespace smt { enode * n = get_enode(v); if (m_autil.is_zero(n->get_expr()) && !m_assignment[v].is_zero()) { numeral val = m_assignment[v]; - sort * s = n->get_expr()->get_sort(); + sort * s = n->get_sort(); // adjust the value of all variables that have the same sort. for (int v2 = 0; v2 < num_vars; ++v2) { enode * n2 = get_enode(v2); - if (n2->get_expr()->get_sort() == s) { + if (n2->get_sort() == s) { m_assignment[v2] -= val; } } @@ -813,7 +813,7 @@ namespace smt { TRACE(ddl_model, tout << "ddl model\n"; for (theory_var v = 0; v < num_vars; ++v) { - tout << "#" << mk_pp(get_enode(v)->get_expr(), m) << " = " << m_assignment[v] << "\n"; + tout << "#" << mk_pp(get_expr(v), m) << " = " << m_assignment[v] << "\n"; }); } diff --git a/src/smt/theory_diff_logic.h b/src/smt/theory_diff_logic.h index 720cdb9bb..ac73ca820 100644 --- a/src/smt/theory_diff_logic.h +++ b/src/smt/theory_diff_logic.h @@ -263,7 +263,7 @@ namespace smt { m_arith_eq_adapter.restart_eh(); } - void relevant_eh(app* e) override {} + void relevant_eh(expr* e) override {} void init_search_eh() override { m_arith_eq_adapter.init_search_eh(); diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h index 7b7519d55..2a0246499 100644 --- a/src/smt/theory_diff_logic_def.h +++ b/src/smt/theory_diff_logic_def.h @@ -384,7 +384,7 @@ final_check_status theory_diff_logic::final_check_eh(unsigned level) { } for (enode* n : ctx.enodes()) { - family_id fid = n->get_expr()->get_family_id(); + family_id fid = n->get_family_id(); if (fid != get_family_id() && fid != m.get_basic_family_id() && !is_uninterp_const(n->get_expr())) { @@ -974,7 +974,7 @@ theory_var theory_diff_logic::expand(bool pos, theory_var v, rational & k) enode* e = get_enode(v); rational r; for (;;) { - app* n = e->get_expr(); + 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)); @@ -1024,8 +1024,8 @@ void theory_diff_logic::new_eq_or_diseq(bool is_eq, theory_var v1, theory_v app_ref eq(m), s2(m), t2(m); - app* s1 = get_enode(s)->get_expr(); - app* t1 = get_enode(t)->get_expr(); + expr* s1 = get_expr(s); + expr* t1 = get_expr(t); s2 = m_util.mk_sub(t1, s1); t2 = m_util.mk_numeral(k, s2->get_sort()); // t1 - s1 = k diff --git a/src/smt/theory_dl.cpp b/src/smt/theory_dl.cpp index ee8c94d9a..f18c8b375 100644 --- a/src/smt/theory_dl.cpp +++ b/src/smt/theory_dl.cpp @@ -166,20 +166,20 @@ namespace smt { } void apply_sort_cnstr(enode * n, sort * s) override { - app* term = n->get_expr(); + auto term = n->get_app(); if (u().is_finite_sort(term)) { mk_rep(term); } } - void relevant_eh(app * n) override { + void relevant_eh(expr * n) override { if (u().is_finite_sort(n)) { sort* s = n->get_sort(); func_decl* r, *v; get_rep(s, r, v); - if (n->get_decl() != v) { + if (is_app(n) && to_app(n)->get_decl() != v) { expr* rep = m().mk_app(r, n); uint64_t vl; if (u().is_numeral_ext(n, vl)) { diff --git a/src/smt/theory_finite_set.cpp b/src/smt/theory_finite_set.cpp index 7ca1d4216..6f07961bf 100644 --- a/src/smt/theory_finite_set.cpp +++ b/src/smt/theory_finite_set.cpp @@ -239,8 +239,9 @@ namespace smt { return true; } - void theory_finite_set::relevant_eh(app* t) { - add_immediate_axioms(t); + void theory_finite_set::relevant_eh(expr* t) { + if (is_app(t)) + add_immediate_axioms(to_app(t)); } void theory_finite_set::apply_sort_cnstr(enode* n, sort* s) { diff --git a/src/smt/theory_finite_set.h b/src/smt/theory_finite_set.h index 472249960..eb7e08fec 100644 --- a/src/smt/theory_finite_set.h +++ b/src/smt/theory_finite_set.h @@ -155,7 +155,7 @@ namespace smt { bool can_propagate() override; void propagate() override; void assign_eh(bool_var v, bool is_true) override; - void relevant_eh(app *n) override; + void relevant_eh(expr *n) override; theory * mk_fresh(context * new_ctx) override; char const * get_name() const override { return "finite_set"; } diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 962e44d27..107456455 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -298,9 +298,9 @@ namespace smt { SASSERT(s->get_family_id() == get_family_id()); SASSERT(m_fpa_util.is_float(s) || m_fpa_util.is_rm(s)); SASSERT(m_fpa_util.is_float(n->get_expr()) || m_fpa_util.is_rm(n->get_expr())); - SASSERT(n->get_expr()->get_decl()->get_range() == s); + SASSERT(n->get_decl()->get_range() == s); - app * owner = n->get_expr(); + expr * owner = n->get_expr(); if (!is_attached_to_var(n)) { attach_new_th_var(n); @@ -437,7 +437,7 @@ namespace smt { assert_cnstr(cnstr); } - void theory_fpa::relevant_eh(app * n) { + void theory_fpa::relevant_eh(expr * n) { TRACE(t_fpa, tout << "relevant_eh for: " << mk_ismt2_pp(n, m) << "\n";); mpf_manager & mpfm = m_fpa_util.fm(); @@ -477,7 +477,7 @@ namespace smt { // get-fp), mk_uf creates a separate BV UF that is not // linked to bvwrap. Assert wrap(n) == concat(conv_components) // to close the constraint gap (same pattern as numerals above). - if (n->get_family_id() != get_family_id()) { + if (!is_app(n) || to_app(n)->get_family_id() != get_family_id()) { expr_ref conv_e = convert(n); if (m_fpa_util.is_fp(conv_e) && to_app(conv_e)->get_num_args() == 3) { app_ref conv_a(m); @@ -491,7 +491,7 @@ namespace smt { } } } - else if (n->get_family_id() == get_family_id()) { + else if (is_app(n) && to_app(n)->get_family_id() == get_family_id()) { // These are the conversion functions fp.to_* */ SASSERT(!m_fpa_util.is_float(n) && !m_fpa_util.is_rm(n)); } diff --git a/src/smt/theory_fpa.h b/src/smt/theory_fpa.h index badce4e2a..14797f62a 100644 --- a/src/smt/theory_fpa.h +++ b/src/smt/theory_fpa.h @@ -104,7 +104,7 @@ namespace smt { model_value_proc * mk_value(enode * n, model_generator & mg) override; void assign_eh(bool_var v, bool is_true) override; - void relevant_eh(app * n) override; + void relevant_eh(expr * n) override; void init_model(model_generator & m) override; void finalize_model(model_generator & mg) override; diff --git a/src/smt/theory_intblast.cpp b/src/smt/theory_intblast.cpp index 1a17784b9..2d2c69951 100644 --- a/src/smt/theory_intblast.cpp +++ b/src/smt/theory_intblast.cpp @@ -153,7 +153,7 @@ namespace smt { void theory_intblast::apply_sort_cnstr(enode* n, sort* s) { SASSERT(bv.is_bv_sort(s)); if (!is_attached_to_var(n)) { - m_translator.internalize_bv(n->get_expr()); + m_translator.internalize_bv(n->get_app()); auto v = mk_var(n); ctx.attach_th_var(n, this, v); } diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index b4016dca8..faf367396 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -228,7 +228,7 @@ class theory_lra::imp { bool is_real(enode* n) const { return a.is_real(n->get_expr()); } enode* get_enode(theory_var v) const { return th.get_enode(v); } enode* get_enode(expr* e) const { return ctx().get_enode(e); } - expr* get_owner(theory_var v) const { return get_enode(v)->get_expr(); } + expr* get_expr(theory_var v) const { return get_enode(v)->get_expr(); } enode_pp pp(enode* n) const { return enode_pp(n, ctx()); } enode_pp pp(theory_var v) const { return pp(get_enode(v)); } mk_bounded_pp bpp(expr* e) { return mk_bounded_pp(e, m); } @@ -1118,7 +1118,7 @@ public: m_nla->simplify(); } - void relevant_eh(app* n) { + void relevant_eh(expr* n) { expr* n1, *n2; if (a.is_mod(n, n1, n2)) mk_idiv_mod_axioms(n1, n2); @@ -1127,11 +1127,11 @@ public: else if (a.is_div(n, n1, n2)) mk_div_axiom(n1, n2); else if (a.is_to_int(n)) - mk_to_int_axiom(n); + mk_to_int_axiom(to_app(n)); else if (a.is_is_int(n)) - mk_is_int_axiom(n); + mk_is_int_axiom(to_app(n)); else if (m.is_ite(n)) - mk_ite_axiom(n); + mk_ite_axiom(to_app(n)); else if (a.is_power(n, n1, n2)) mk_power_axiom(n, n1, n2); } @@ -1252,9 +1252,9 @@ public: /// abs(r) > r >= 0 void assert_idiv_mod_axioms(theory_var u, theory_var v, theory_var w, rational const& r) { app_ref term(m); - term = a.mk_mul(a.mk_numeral(r, true), get_enode(w)->get_expr()); - term = a.mk_add(get_enode(v)->get_expr(), term); - term = a.mk_sub(get_enode(u)->get_expr(), term); + term = a.mk_mul(a.mk_numeral(r, true), get_expr(w)); + term = a.mk_add(get_expr(v), term); + term = a.mk_sub(get_expr(u), term); theory_var z = internalize_def(term); lpvar zi = register_theory_var_in_lar_solver(z); lpvar vi = register_theory_var_in_lar_solver(v); @@ -1837,7 +1837,7 @@ public: rational lc = denominator(k); for (auto const& kv : coeffs) { theory_var w = kv.m_key; - expr* o = get_enode(w)->get_expr(); + expr* o = get_expr(w); is_int = a.is_int(o); if (!is_int) break; lc = lcm(lc, denominator(kv.m_value)); @@ -2512,7 +2512,7 @@ public: lpvar vi = be.m_j; if (lp().column_has_term(vi)) return; - expr_ref w(get_enode(v)->get_expr(), m); + expr_ref w(get_expr(v), m); if (a.is_add(w) || a.is_numeral(w) || m.is_ite(w)) return; literal bound = null_literal; @@ -3417,7 +3417,7 @@ public: theory_var v = lp().local_to_external(vi); rational val; TRACE(arith, tout << lp().get_variable_name(vi) << " " << v << "\n";); - if (v != null_theory_var && a.is_numeral(get_owner(v), val) && bound == val) { + if (v != null_theory_var && a.is_numeral(get_expr(v), val) && bound == val) { dep = nullptr; return bound == val; } @@ -4131,7 +4131,7 @@ public: // Overload: create blocker from a saved impq value (used when x has been restored) expr_ref mk_gt(theory_var v, lp::impq const& val) { - expr* obj = get_enode(v)->get_expr(); + expr* obj = get_expr(v); rational r = val.x; expr_ref e(m); if (a.is_int(obj->get_sort())) { @@ -4189,7 +4189,7 @@ public: app_ref coeffs2app(u_map const& coeffs, rational const& offset, bool is_int) { expr_ref_vector args(m); for (auto const& [w, coeff] : coeffs) { - expr* o = get_enode(w)->get_expr(); + expr* o = get_expr(w); if (coeff.is_zero()) { // continue } @@ -4236,13 +4236,14 @@ public: app_ref mk_obj(theory_var v) { auto t = get_lpvar(v); - bool is_int = a.is_int(get_enode(v)->get_expr()); + auto e = th.get_expr(v); + bool is_int = a.is_int(e); if (lp().column_has_term(t)) { return mk_term(lp().get_term(t), is_int); } else { // theory_var w = lp().external_to_local(vi); - return app_ref(get_enode(v)->get_expr(), m); + return app_ref(to_app(e), m); } } @@ -4250,7 +4251,7 @@ public: rational r = val.get_rational(); bool is_strict = val.get_infinitesimal().is_pos(); app_ref b(m); - bool is_int = a.is_int(get_enode(v)->get_expr()); + bool is_int = a.is_int(get_expr(v)); TRACE(arith, display(tout << "v" << v << "\n");); if (is_strict) { b = a.mk_le(mk_obj(v), a.mk_numeral(r, is_int)); @@ -4456,7 +4457,7 @@ void theory_lra::pop_scope_eh(unsigned num_scopes) { void theory_lra::restart_eh() { m_imp->restart_eh(); } -void theory_lra::relevant_eh(app* e) { +void theory_lra::relevant_eh(expr* e) { m_imp->relevant_eh(e); } void theory_lra::init_search_eh() { diff --git a/src/smt/theory_lra.h b/src/smt/theory_lra.h index fb1a16b15..172cdaa4d 100644 --- a/src/smt/theory_lra.h +++ b/src/smt/theory_lra.h @@ -59,7 +59,7 @@ namespace smt { void restart_eh() override; - void relevant_eh(app* e) override; + void relevant_eh(expr* e) override; void init_search_eh() override; diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index 862440e43..adedc4fae 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -2367,7 +2367,7 @@ namespace smt { } model_value_proc * theory_pb::mk_value(enode * n, model_generator & mg) { - app* a = n->get_expr(); + 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))); diff --git a/src/smt/theory_recfun.cpp b/src/smt/theory_recfun.cpp index d2dffaf98..ada0f0198 100644 --- a/src/smt/theory_recfun.cpp +++ b/src/smt/theory_recfun.cpp @@ -99,7 +99,7 @@ namespace smt { * then case-expand `n`. If it's a macro we can also immediately * body-expand it. */ - void theory_recfun::relevant_eh(app * n) { + void theory_recfun::relevant_eh(expr * n) { SASSERT(ctx.relevancy()); // TRACEFN("relevant_eh: (defined) " << u().is_defined(n) << " " << mk_pp(n, m)); if (u().is_defined(n) && u().has_defs()) diff --git a/src/smt/theory_recfun.h b/src/smt/theory_recfun.h index 25e77a469..16746f27e 100644 --- a/src/smt/theory_recfun.h +++ b/src/smt/theory_recfun.h @@ -61,8 +61,8 @@ namespace smt { bool is_disabled_guard(expr* guard) { return m_disabled_guards.contains(guard); } recfun::util & u() const { return m_util; } - bool is_defined(app * f) const { return u().is_defined(f); } - bool is_case_pred(app * f) const { return u().is_case_pred(f); } + bool is_defined(expr * f) const { return u().is_defined(f); } + bool is_case_pred(expr * f) const { return u().is_case_pred(f); } bool is_defined(enode * e) const { return is_defined(e->get_expr()); } bool is_case_pred(enode * e) const { return is_case_pred(e->get_expr()); } @@ -90,7 +90,7 @@ namespace smt { bool internalize_atom(app * atom, bool gate_ctx) override; bool internalize_term(app * term) override; void reset_eh() override; - void relevant_eh(app * n) override; + void relevant_eh(expr * n) override; char const * get_name() const override; final_check_status final_check_eh(unsigned) override; void assign_eh(bool_var v, bool is_true) override; diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 4224a06a4..5357814d3 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -2103,7 +2103,7 @@ app* theory_seq::get_ite_value(expr* e) { } model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) { - app* e = n->get_expr(); + expr* e = n->get_expr(); TRACE(seq, tout << mk_pp(e, m) << "\n";); // Shortcut for well-founded values to avoid some quadratic overhead @@ -2163,7 +2163,7 @@ model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) { } -app* theory_seq::mk_value(app* e) { +app* theory_seq::mk_value(expr* e) { expr_ref result(m); e = get_ite_value(e); result = m_rep.find(e); @@ -3286,7 +3286,10 @@ void theory_seq::pop_scope_eh(unsigned num_scopes) { void theory_seq::restart_eh() { } -void theory_seq::relevant_eh(app* n) { +void theory_seq::relevant_eh(expr* _n) { + if (!is_app(_n)) + return; + app *n = to_app(_n); if (m_util.str.is_index(n) || m_util.str.is_replace(n) || m_util.str.is_extract(n) || diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 800fe5600..ee2ae002a 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -392,7 +392,7 @@ namespace smt { void push_scope_eh() override; void pop_scope_eh(unsigned num_scopes) override; void restart_eh() override; - void relevant_eh(app* n) override; + void relevant_eh(expr* n) override; bool should_research(expr_ref_vector &) override; void add_theory_assumptions(expr_ref_vector & assumptions) override; theory* mk_fresh(context* new_ctx) override { return alloc(theory_seq, *new_ctx); } @@ -629,7 +629,7 @@ namespace smt { void init() override; // model building - app* mk_value(app* a); + app* mk_value(expr* a); trail_stack& get_trail_stack() { return m_trail_stack; } void merge_eh(theory_var, theory_var, theory_var v1, theory_var v2) {} diff --git a/src/smt/theory_special_relations.cpp b/src/smt/theory_special_relations.cpp index aec069a02..4547264fb 100644 --- a/src/smt/theory_special_relations.cpp +++ b/src/smt/theory_special_relations.cpp @@ -174,8 +174,8 @@ namespace smt { } void theory_special_relations::new_eq_eh(theory_var v1, theory_var v2) { - app* t1 = get_expr(v1); - app* t2 = get_expr(v2); + expr* t1 = get_expr(v1); + expr* t2 = get_expr(v2); literal eq = mk_eq(t1, t2, false); for (auto const& kv : m_relations) { relation& r = *kv.m_value; diff --git a/src/smt/theory_utvpi.h b/src/smt/theory_utvpi.h index a917910e9..e94df49eb 100644 --- a/src/smt/theory_utvpi.h +++ b/src/smt/theory_utvpi.h @@ -239,7 +239,7 @@ namespace smt { m_arith_eq_adapter.restart_eh(); } - void relevant_eh(app* e) override {} + void relevant_eh(expr* e) override {} void init_search_eh() override { m_arith_eq_adapter.init_search_eh(); @@ -323,7 +323,7 @@ namespace smt { void new_eq_or_diseq(bool is_eq, th_var v1, th_var v2, justification& eq_just); - bool is_int(theory_var v) const { return a.is_int(get_enode(v)->get_expr()); } + bool is_int(theory_var v) const { return a.is_int(get_expr(v)); } th_var get_zero(sort* s) { return a.is_int(s) ? m_izero : m_rzero; } diff --git a/src/smt/theory_utvpi_def.h b/src/smt/theory_utvpi_def.h index 9086f13aa..9d011299d 100644 --- a/src/smt/theory_utvpi_def.h +++ b/src/smt/theory_utvpi_def.h @@ -170,8 +170,8 @@ namespace smt { // app_ref eq(m), s2(m), t2(m); - app* s1 = get_enode(s)->get_expr(); - app* t1 = get_enode(t)->get_expr(); + expr* s1 = get_expr(s); + expr* t1 = get_expr(t); s2 = a.mk_sub(t1, s1); t2 = a.mk_numeral(k, s2->get_sort()); eq = m.mk_eq(s2.get(), t2.get()); @@ -588,7 +588,7 @@ namespace smt { expr* x, *y; rational r; for (;;) { - app* n = e->get_expr(); + auto n = e->get_expr(); if (a.is_add(n, x, y)) { if (a.is_numeral(x, r)) { e = ctx.get_enode(y); @@ -906,7 +906,7 @@ namespace smt { num = num/rational(2); SASSERT(!is_int || num.is_int()); TRACE(utvpi, - expr* n = get_enode(v)->get_expr(); + expr* n = get_expr(v); tout << mk_pp(n, m) << " |-> (" << val1 << " - " << val2 << ")/2 = " << num << "\n";); return num;