From 8f577d39437ec69182698a7b5ec0fad281fa70c0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 2 Feb 2021 13:57:01 -0800 Subject: [PATCH] remove ast_manager get_sort method entirely --- src/api/api_arith.cpp | 2 +- src/api/api_array.cpp | 26 ++++++++--------- src/api/api_ast.cpp | 10 +++---- src/api/api_context.cpp | 2 +- src/api/api_datatype.cpp | 2 +- src/ast/ast.cpp | 8 +++--- src/ast/ast.h | 1 - src/ast/euf/euf_egraph.cpp | 6 ++-- src/ast/fpa/bv2fpa_converter.cpp | 2 +- src/ast/rewriter/expr_safe_replace.cpp | 4 +-- src/ast/rewriter/func_decl_replace.cpp | 2 +- src/ast/rewriter/rewriter.cpp | 2 +- src/ast/rewriter/rewriter_def.h | 28 +++++++++---------- src/ast/rewriter/seq_rewriter.cpp | 12 ++++---- src/ast/rewriter/th_rewriter.cpp | 4 +-- src/cmd_context/cmd_context.cpp | 2 +- src/model/value_factory.cpp | 2 +- src/muz/base/bind_variables.cpp | 4 +-- src/muz/base/dl_rule.cpp | 2 +- src/muz/base/dl_rule.h | 2 +- src/muz/base/rule_properties.cpp | 2 +- src/muz/bmc/dl_bmc_engine.cpp | 12 ++++---- src/muz/ddnf/ddnf.cpp | 4 +-- src/muz/fp/datalog_parser.cpp | 6 ++-- src/muz/rel/dl_external_relation.cpp | 2 +- src/muz/rel/dl_external_relation.h | 2 +- src/muz/rel/dl_mk_explanations.cpp | 2 +- src/muz/rel/udoc_relation.h | 2 +- src/muz/spacer/spacer_antiunify.cpp | 4 +-- src/muz/spacer/spacer_legacy_mev.cpp | 2 +- src/muz/spacer/spacer_mev_array.cpp | 2 +- src/muz/spacer/spacer_proof_utils.cpp | 2 +- src/muz/spacer/spacer_qe_project.cpp | 26 ++++++++--------- src/muz/tab/tab_context.cpp | 8 +++--- src/muz/transforms/dl_mk_coalesce.cpp | 8 +++--- src/muz/transforms/dl_mk_elim_term_ite.cpp | 2 +- .../dl_mk_quantifier_abstraction.cpp | 4 +-- src/opt/opt_context.cpp | 2 +- src/qe/mbp/mbp_arrays.cpp | 6 ++-- src/sat/smt/array_axioms.cpp | 2 +- src/sat/smt/array_solver.cpp | 2 +- src/sat/smt/bv_internalize.cpp | 2 +- src/smt/seq_eq_solver.cpp | 20 ++++++------- src/smt/seq_ne_solver.cpp | 2 +- src/smt/seq_regex.cpp | 16 +++++------ src/smt/smt_context.cpp | 10 +++---- src/smt/smt_context.h | 2 +- src/smt/smt_context_inv.cpp | 2 +- src/smt/smt_implied_equalities.cpp | 4 +-- src/smt/smt_model_checker.cpp | 4 +-- src/smt/smt_model_generator.cpp | 10 +++---- src/smt/theory_arith_aux.h | 6 ++-- src/smt/theory_arith_core.h | 2 +- src/smt/theory_arith_eq.h | 2 +- src/smt/theory_array_bapa.cpp | 10 +++---- src/smt/theory_bv.cpp | 2 +- src/smt/theory_datatype.cpp | 4 +-- src/smt/theory_dense_diff_logic_def.h | 4 +-- src/smt/theory_diff_logic_def.h | 4 +-- src/smt/theory_dl.cpp | 6 ++-- src/smt/theory_fpa.cpp | 12 ++++---- src/smt/theory_lra.cpp | 10 +++---- src/smt/theory_seq.cpp | 10 +++---- src/smt/theory_seq.h | 6 ++-- src/smt/theory_str.cpp | 20 ++++++------- src/smt/theory_str_mc.cpp | 6 ++-- src/smt/theory_utvpi_def.h | 2 +- src/solver/solver.h | 2 ++ src/tactic/bv/bit_blaster_model_converter.cpp | 2 +- src/tactic/core/injectivity_tactic.cpp | 2 +- src/tactic/fd_solver/smtfd_solver.cpp | 4 +-- src/test/qe_arith.cpp | 4 +-- 72 files changed, 209 insertions(+), 208 deletions(-) diff --git a/src/api/api_arith.cpp b/src/api/api_arith.cpp index 87f6efeb7..57f96dd6d 100644 --- a/src/api/api_arith.cpp +++ b/src/api/api_arith.cpp @@ -71,7 +71,7 @@ extern "C" { LOG_Z3_mk_div(c, n1, n2); RESET_ERROR_CODE(); decl_kind k = OP_IDIV; - sort* ty = mk_c(c)->m().get_sort(to_expr(n1)); + sort* ty = to_expr(n1)->get_sort(); sort* real_ty = mk_c(c)->m().mk_sort(mk_c(c)->get_arith_fid(), REAL_SORT); if (ty == real_ty) { k = OP_DIV; diff --git a/src/api/api_array.cpp b/src/api/api_array.cpp index c87566316..016fcd336 100644 --- a/src/api/api_array.cpp +++ b/src/api/api_array.cpp @@ -57,8 +57,8 @@ extern "C" { CHECK_IS_EXPR(i, nullptr); expr * _a = to_expr(a); expr * _i = to_expr(i); - sort * a_ty = m.get_sort(_a); - sort * i_ty = m.get_sort(_i); + sort * a_ty = _a->get_sort(); + sort * i_ty = _i->get_sort(); if (a_ty->get_family_id() != mk_c(c)->get_array_fid()) { SET_ERROR_CODE(Z3_SORT_ERROR, nullptr); RETURN_Z3(nullptr); @@ -80,7 +80,7 @@ extern "C" { ast_manager & m = mk_c(c)->m(); CHECK_IS_EXPR(a, nullptr); expr * _a = to_expr(a); - sort * a_ty = m.get_sort(_a); + sort * a_ty = _a->get_sort(); if (a_ty->get_family_id() != mk_c(c)->get_array_fid()) { SET_ERROR_CODE(Z3_SORT_ERROR, nullptr); RETURN_Z3(nullptr); @@ -92,7 +92,7 @@ extern "C" { for (unsigned i = 0; i < n; ++i) { CHECK_IS_EXPR(idxs[i], nullptr); args.push_back(to_expr(idxs[i])); - domain.push_back(m.get_sort(to_expr(idxs[i]))); + domain.push_back(to_expr(idxs[i])->get_sort()); } func_decl * d = m.mk_func_decl(mk_c(c)->get_array_fid(), OP_SELECT, 2, a_ty->get_parameters(), domain.size(), domain.c_ptr()); app * r = m.mk_app(d, args.size(), args.c_ptr()); @@ -114,9 +114,9 @@ extern "C" { expr * _a = to_expr(a); expr * _i = to_expr(i); expr * _v = to_expr(v); - sort * a_ty = m.get_sort(_a); - sort * i_ty = m.get_sort(_i); - sort * v_ty = m.get_sort(_v); + sort * a_ty = _a->get_sort(); + sort * i_ty = _i->get_sort(); + sort * v_ty = _v->get_sort(); if (a_ty->get_family_id() != mk_c(c)->get_array_fid()) { SET_ERROR_CODE(Z3_SORT_ERROR, nullptr); RETURN_Z3(nullptr); @@ -138,8 +138,8 @@ extern "C" { ast_manager & m = mk_c(c)->m(); expr * _a = to_expr(a); expr * _v = to_expr(v); - sort * a_ty = m.get_sort(_a); - sort * v_ty = m.get_sort(_v); + sort * a_ty = _a->get_sort(); + sort * v_ty = _v->get_sort(); if (a_ty->get_family_id() != mk_c(c)->get_array_fid()) { SET_ERROR_CODE(Z3_SORT_ERROR, nullptr); RETURN_Z3(nullptr); @@ -150,7 +150,7 @@ extern "C" { domain.push_back(a_ty); for (unsigned i = 0; i < n; ++i) { args.push_back(to_expr(idxs[i])); - domain.push_back(m.get_sort(to_expr(idxs[i]))); + domain.push_back(to_expr(idxs[i])->get_sort()); } args.push_back(_v); domain.push_back(v_ty); @@ -177,7 +177,7 @@ extern "C" { ptr_vector domain; for (unsigned i = 0; i < n; ++i) { - domain.push_back(m.get_sort(_args[i])); + domain.push_back(_args[i]->get_sort()); } parameter param(_f); func_decl * d = m.mk_func_decl(mk_c(c)->get_array_fid(), OP_ARRAY_MAP, 1, ¶m, n, domain.c_ptr()); @@ -194,7 +194,7 @@ extern "C" { RESET_ERROR_CODE(); ast_manager & m = mk_c(c)->m(); expr * _v = to_expr(v); - sort * _range = m.get_sort(_v); + sort * _range = _v->get_sort(); sort * _domain = to_sort(domain); parameter params[2] = { parameter(_domain), parameter(_range) }; sort * a_ty = mk_c(c)->m().mk_sort(mk_c(c)->get_array_fid(), ARRAY_SORT, 2, params); @@ -226,7 +226,7 @@ extern "C" { RESET_ERROR_CODE(); ast_manager & m = mk_c(c)->m(); expr * _v = to_expr(v); - sort * _range = m.get_sort(_v); + sort * _range = _v->get_sort(); sort * _domain = to_sort(domain); parameter params[2] = { parameter(_domain), parameter(_range) }; sort * a_ty = mk_c(c)->m().mk_sort(mk_c(c)->get_array_fid(), ARRAY_SORT, 2, params); diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 5aef93218..15bf13911 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -142,8 +142,8 @@ extern "C" { var_ref_vector _vars(m); for (unsigned i = 0; i < n; ++i) { _args.push_back(to_expr(args[i])); - _vars.push_back(m.mk_var(n - i - 1, m.get_sort(_args.back()))); - if (m.get_sort(_args.back()) != d->get_domain(i)) { + _vars.push_back(m.mk_var(n - i - 1, _args.back()->get_sort())); + if (_args.back()->get_sort() != d->get_domain(i)) { SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return; } @@ -154,7 +154,7 @@ extern "C" { SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return; } - if (m.get_sort(abs_body) != d->get_range()) { + if (abs_body->get_sort() != d->get_range()) { SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return; } @@ -622,7 +622,7 @@ extern "C" { LOG_Z3_get_sort(c, a); RESET_ERROR_CODE(); CHECK_IS_EXPR(a, nullptr); - Z3_sort r = of_sort(mk_c(c)->m().get_sort(to_expr(a))); + Z3_sort r = of_sort(to_expr(a)->get_sort()); RETURN_Z3(r); Z3_CATCH_RETURN(nullptr); } @@ -847,7 +847,7 @@ extern "C" { expr * const * to = to_exprs(num_exprs, _to); expr * r = nullptr; for (unsigned i = 0; i < num_exprs; i++) { - if (m.get_sort(from[i]) != m.get_sort(to[i])) { + if (from[i]->get_sort() != to[i]->get_sort()) { SET_ERROR_CODE(Z3_SORT_ERROR, nullptr); RETURN_Z3(of_expr(nullptr)); } diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 23a583702..00f985deb 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -300,7 +300,7 @@ namespace api { if (a->get_num_args() > 1) buffer << "\n"; for (unsigned i = 0; i < a->get_num_args(); ++i) { buffer << mk_bounded_pp(a->get_arg(i), m(), 3) << " of sort "; - buffer << mk_pp(m().get_sort(a->get_arg(i)), m()) << "\n"; + buffer << mk_pp(a->get_arg(i)->get_sort(), m()) << "\n"; } auto str = buffer.str(); warning_msg("%s", str.c_str()); diff --git a/src/api/api_datatype.cpp b/src/api/api_datatype.cpp index 04d7793a0..c84c2b38f 100644 --- a/src/api/api_datatype.cpp +++ b/src/api/api_datatype.cpp @@ -578,7 +578,7 @@ extern "C" { expr* _t = to_expr(t); expr* _v = to_expr(v); expr* args[2] = { _t, _v }; - sort* domain[2] = { m.get_sort(_t), m.get_sort(_v) }; + sort* domain[2] = { _t->get_sort(), _v->get_sort() }; parameter param(_f); func_decl * d = m.mk_func_decl(mk_c(c)->get_dt_fid(), OP_DT_UPDATE_FIELD, 1, ¶m, 2, domain); app* r = m.mk_app(d, 2, args); diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index c9f0cc4c3..235e14f63 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -2405,7 +2405,7 @@ var * ast_manager::mk_var(unsigned idx, sort * s) { app * ast_manager::mk_label(bool pos, unsigned num_names, symbol const * names, expr * n) { SASSERT(num_names > 0); - SASSERT(get_sort(n) == m_bool_sort); + SASSERT(n->get_sort() == m_bool_sort); buffer p; p.push_back(parameter(static_cast(pos))); for (unsigned i = 0; i < num_names; i++) @@ -2798,7 +2798,7 @@ proof * ast_manager::mk_true_proof() { } proof * ast_manager::mk_asserted(expr * f) { - CTRACE("mk_asserted_bug", !is_bool(f), tout << mk_ismt2_pp(f, *this) << "\nsort: " << mk_ismt2_pp(get_sort(f), *this) << "\n";); + CTRACE("mk_asserted_bug", !is_bool(f), tout << mk_ismt2_pp(f, *this) << "\nsort: " << mk_ismt2_pp(f->get_sort(), *this) << "\n";); SASSERT(is_bool(f)); return mk_proof(m_basic_family_id, PR_ASSERTED, f); } @@ -2958,14 +2958,14 @@ proof * ast_manager::mk_monotonicity(func_decl * R, app * f1, app * f2, unsigned } proof * ast_manager::mk_congruence(app * f1, app * f2, unsigned num_proofs, proof * const * proofs) { - SASSERT(get_sort(f1) == get_sort(f2)); + SASSERT(f1->get_sort() == f2->get_sort()); sort * s = f1->get_sort(); sort * d[2] = { s, s }; return mk_monotonicity(mk_func_decl(m_basic_family_id, get_eq_op(f1), 0, nullptr, 2, d), f1, f2, num_proofs, proofs); } proof * ast_manager::mk_oeq_congruence(app * f1, app * f2, unsigned num_proofs, proof * const * proofs) { - SASSERT(get_sort(f1) == get_sort(f2)); + SASSERT(f1->get_sort() == f2->get_sort()); sort * s = f1->get_sort(); sort * d[2] = { s, s }; return mk_monotonicity(mk_func_decl(m_basic_family_id, OP_OEQ, 0, nullptr, 2, d), f1, f2, num_proofs, proofs); diff --git a/src/ast/ast.h b/src/ast/ast.h index 0de63fe6b..c109db598 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -1735,7 +1735,6 @@ protected: } public: - sort * get_sort(expr const * n) const { return n->get_sort(); } void check_sort(func_decl const * decl, unsigned num_args, expr * const * args) const; void check_sorts_core(ast const * n) const; bool check_sorts(ast const * n) const; diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp index 088f4d2a6..66bba1e03 100644 --- a/src/ast/euf/euf_egraph.cpp +++ b/src/ast/euf/euf_egraph.cpp @@ -376,7 +376,7 @@ namespace euf { if (!n1->merge_enabled() && !n2->merge_enabled()) return; - SASSERT(m.get_sort(n1->get_expr()) == m.get_sort(n2->get_expr())); + SASSERT(n1->get_expr()->get_sort() == n2->get_expr()->get_sort()); enode* r1 = n1->get_root(); enode* r2 = n2->get_root(); if (r1 == r2) @@ -787,8 +787,8 @@ namespace euf { enode* n2 = m_nodes[i]; enode* n2t = n1t ? old_expr2new_enode[n1->get_expr_id()] : nullptr; SASSERT(!n1t || n2t); - SASSERT(!n1t || src.m.get_sort(n1->get_expr()) == src.m.get_sort(n1t->get_expr())); - SASSERT(!n1t || m.get_sort(n2->get_expr()) == m.get_sort(n2t->get_expr())); + SASSERT(!n1t || n1->get_expr()->get_sort() == n1t->get_expr()->get_sort()); + SASSERT(!n1t || n2->get_expr()->get_sort() == n2t->get_expr()->get_sort()); if (n1t && n2->get_root() != n2t->get_root()) merge(n2, n2t, n1->m_justification.copy(copy_justification)); } diff --git a/src/ast/fpa/bv2fpa_converter.cpp b/src/ast/fpa/bv2fpa_converter.cpp index 90bd42374..719b769c8 100644 --- a/src/ast/fpa/bv2fpa_converter.cpp +++ b/src/ast/fpa/bv2fpa_converter.cpp @@ -224,7 +224,7 @@ expr_ref bv2fpa_converter::rebuild_floats(model_core * mc, sort * s, expr * e) { else if (is_var(e)) { result = e; } - SASSERT(!result || m.get_sort(result) == s); + SASSERT(!result || result->get_sort() == s); return result; } diff --git a/src/ast/rewriter/expr_safe_replace.cpp b/src/ast/rewriter/expr_safe_replace.cpp index d0273be6e..9578a1151 100644 --- a/src/ast/rewriter/expr_safe_replace.cpp +++ b/src/ast/rewriter/expr_safe_replace.cpp @@ -26,7 +26,7 @@ Revision History: void expr_safe_replace::insert(expr* src, expr* dst) { - SASSERT(m.get_sort(src) == m.get_sort(dst)); + SASSERT(src->get_sort() == dst->get_sort()); m_src.push_back(src); m_dst.push_back(dst); #if ALIVE_OPT @@ -111,7 +111,7 @@ void expr_safe_replace::operator()(expr* e, expr_ref& res) { #if !ALIVE_OPT m_refs.push_back(b); #endif - SASSERT(m.get_sort(a) == m.get_sort(b)); + SASSERT(a->get_sort() == b->get_sort()); } else { b = a; } diff --git a/src/ast/rewriter/func_decl_replace.cpp b/src/ast/rewriter/func_decl_replace.cpp index 266088f43..3fbdb2470 100644 --- a/src/ast/rewriter/func_decl_replace.cpp +++ b/src/ast/rewriter/func_decl_replace.cpp @@ -53,7 +53,7 @@ expr_ref func_decl_replace::operator()(expr* e) { if (arg_differs) { b = m.mk_app(c->get_decl(), m_args.size(), m_args.c_ptr()); m_refs.push_back(b); - SASSERT(m.get_sort(a) == m.get_sort(b)); + SASSERT(a->get_sort() == b->get_sort()); } else { b = a; } diff --git a/src/ast/rewriter/rewriter.cpp b/src/ast/rewriter/rewriter.cpp index c88b59bb3..4c9933998 100644 --- a/src/ast/rewriter/rewriter.cpp +++ b/src/ast/rewriter/rewriter.cpp @@ -65,7 +65,7 @@ void rewriter_core::cache_shifted_result(expr * k, unsigned offset, expr * v) { TRACE("rewriter_cache_result", tout << mk_ismt2_pp(k, m()) << "\n--->\n" << mk_ismt2_pp(v, m()) << "\n";); - SASSERT(m().get_sort(k) == m().get_sort(v)); + SASSERT(k->get_sort() == v->get_sort()); m_cache->insert(k, offset, v); #if 0 diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h index 808d83cb3..f1caeb21c 100644 --- a/src/ast/rewriter/rewriter_def.h +++ b/src/ast/rewriter/rewriter_def.h @@ -26,7 +26,7 @@ template void rewriter_tpl::process_var(var * v) { if (m_cfg.reduce_var(v, m_r, m_pr)) { result_stack().push_back(m_r); - SASSERT(v->get_sort() == m().get_sort(m_r)); + SASSERT(v->get_sort() == m_r->get_sort()); if (ProofGen) { result_pr_stack().push_back(m_pr); m_pr = nullptr; @@ -43,11 +43,11 @@ void rewriter_tpl::process_var(var * v) { unsigned index = 0; expr * r; if (idx < m_bindings.size() && (index = m_bindings.size() - idx - 1, r = m_bindings[index])) { - CTRACE("rewriter", v->get_sort() != m().get_sort(r), - tout << expr_ref(v, m()) << ":" << sort_ref(v->get_sort(), m()) << " != " << expr_ref(r, m()) << ":" << sort_ref(m().get_sort(r), m()); + CTRACE("rewriter", v->get_sort() != r->get_sort(), + tout << expr_ref(v, m()) << ":" << sort_ref(v->get_sort(), m()) << " != " << expr_ref(r, m()) << ":" << sort_ref(r->get_sort(), m()); tout << "index " << index << " bindings " << m_bindings.size() << "\n"; display_bindings(tout);); - SASSERT(v->get_sort() == m().get_sort(r)); + SASSERT(v->get_sort() == r->get_sort()); if (!is_ground(r) && m_shifts[index] != m_bindings.size()) { unsigned shift_amount = m_bindings.size() - m_shifts[index]; expr* c = get_cached(r, shift_amount); @@ -90,10 +90,10 @@ bool rewriter_tpl::process_const(app * t0) { if (m_pr) tout << mk_bounded_pp(m_pr, m()) << "\n"; ); CTRACE("reduce_app", - st != BR_FAILED && m().get_sort(m_r) != t->get_sort(), + st != BR_FAILED && m_r->get_sort() != t->get_sort(), tout << mk_pp(t->get_sort(), m()) << ": " << mk_pp(t, m()) << "\n"; - tout << m_r->get_id() << " " << mk_pp(m().get_sort(m_r), m()) << ": " << m_r << "\n";); - SASSERT(st != BR_DONE || m().get_sort(m_r) == t->get_sort()); + tout << m_r->get_id() << " " << mk_pp(m_r->get_sort(), m()) << ": " << m_r << "\n";); + SASSERT(st != BR_DONE || m_r->get_sort() == t->get_sort()); switch (st) { case BR_FAILED: if (!retried) { @@ -144,7 +144,7 @@ bool rewriter_tpl::visit(expr * t, unsigned max_depth) { proof * new_t_pr = nullptr; if (m_cfg.get_subst(t, new_t, new_t_pr)) { TRACE("rewriter_subst", tout << "subst\n" << mk_ismt2_pp(t, m()) << "\n---->\n" << mk_ismt2_pp(new_t, m()) << "\n";); - SASSERT(t->get_sort() == m().get_sort(new_t)); + SASSERT(t->get_sort() == new_t->get_sort()); result_stack().push_back(new_t); set_new_child_flag(t, new_t); SASSERT(rewrites_from(t, new_t_pr)); @@ -171,7 +171,7 @@ bool rewriter_tpl::visit(expr * t, unsigned max_depth) { #endif expr * r = get_cached(t); if (r) { - SASSERT(m().get_sort(r) == t->get_sort()); + SASSERT(r->get_sort() == t->get_sort()); result_stack().push_back(r); set_new_child_flag(t, r); if (ProofGen) { @@ -312,10 +312,10 @@ void rewriter_tpl::process_app(app * t, frame & fr) { ); SASSERT(st == BR_FAILED || rewrites_to(m_r, m_pr2)); SASSERT(st == BR_FAILED || rewrites_from(new_t, m_pr2)); - SASSERT(st != BR_DONE || m().get_sort(m_r) == t->get_sort()); + SASSERT(st != BR_DONE || m_r->get_sort() == t->get_sort()); if (st != BR_FAILED) { result_stack().shrink(fr.m_spos); - SASSERT(m().get_sort(m_r) == t->get_sort()); + SASSERT(m_r->get_sort() == t->get_sort()); result_stack().push_back(m_r); if (ProofGen) { result_pr_stack().shrink(fr.m_spos); @@ -393,7 +393,7 @@ void rewriter_tpl::process_app(app * t, frame & fr) { if (get_macro(f, def, def_pr)) { SASSERT(!f->is_associative() || !flat_assoc(f)); SASSERT(new_num_args == t->get_num_args()); - SASSERT(m().get_sort(def) == t->get_sort()); + SASSERT(def->get_sort() == t->get_sort()); if (is_ground(def) && !m_cfg.reduce_macro()) { m_r = def; if (ProofGen) { @@ -597,7 +597,7 @@ void rewriter_tpl::process_quantifier(quantifier * q, frame & fr) { } result_stack().shrink(fr.m_spos); result_stack().push_back(m_r.get()); - SASSERT(m().get_sort(q) == m().get_sort(m_r)); + SASSERT(q->get_sort() == m_r->get_sort()); SASSERT(num_decls <= m_bindings.size()); m_bindings.shrink(m_bindings.size() - num_decls); m_shifts.shrink(m_shifts.size() - num_decls); @@ -759,7 +759,7 @@ void rewriter_tpl::resume_core(expr_ref & result, proof_ref & result_pr) if (first_visit(fr) && fr.m_cache_result) { expr * r = get_cached(t); if (r) { - SASSERT(m().get_sort(r) == t->get_sort()); + SASSERT(r->get_sort() == t->get_sort()); result_stack().push_back(r); if (ProofGen) { proof * pr = get_cached_pr(t); diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 9d7187ab2..8a3222c7c 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -47,7 +47,7 @@ expr_ref sym_expr::accept(expr* e) { result = m.mk_not(result); break; case t_char: - SASSERT(e->get_sort() == m.get_sort(m_t)); + SASSERT(e->get_sort() == m_t->get_sort()); SASSERT(e->get_sort() == m_sort); result = m.mk_eq(e, m_t); break; @@ -736,7 +736,7 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con st = lift_ites_throttled(f, num_args, args, result); } CTRACE("seq_verbose", st != BR_FAILED, tout << expr_ref(m().mk_app(f, num_args, args), m()) << " -> " << result << "\n";); - SASSERT(st == BR_FAILED || m().get_sort(result) == f->get_range()); + SASSERT(st == BR_FAILED || result->get_sort() == f->get_range()); return st; } @@ -2907,7 +2907,7 @@ expr_ref seq_rewriter::mk_der_cond(expr* cond, expr* ele, sort* seq_sort) { << mk_pp(cond, m()) << ", " << mk_pp(ele, m()) << std::endl;); sort *ele_sort = nullptr; VERIFY(u().is_seq(seq_sort, ele_sort)); - SASSERT(ele_sort == m().get_sort(ele)); + SASSERT(ele_sort == ele->get_sort()); expr *c1 = nullptr, *c2 = nullptr, *ch1 = nullptr, *ch2 = nullptr; unsigned ch = 0; expr_ref result(m()), r1(m()), r2(m()); @@ -2959,7 +2959,7 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) { sort* seq_sort = nullptr, *ele_sort = nullptr; VERIFY(m_util.is_re(r, seq_sort)); VERIFY(m_util.is_seq(seq_sort, ele_sort)); - SASSERT(ele_sort == m().get_sort(ele)); + SASSERT(ele_sort == ele->get_sort()); expr* r1 = nullptr, *r2 = nullptr, *p = nullptr; auto mk_empty = [&]() { return expr_ref(re().mk_empty(r->get_sort()), m()); }; unsigned lo = 0, hi = 0; @@ -4214,7 +4214,7 @@ bool seq_rewriter::reduce_back(expr_ref_vector& ls, expr_ref_vector& rs, expr_re SASSERT(s.length() > 0); app_ref ch(str().mk_char(s, s.length()-1), m()); - SASSERT(m().get_sort(ch) == a->get_sort()); + SASSERT(ch->get_sort() == a->get_sort()); new_eqs.push_back(ch, a); ls.pop_back(); if (s.length() == 1) { @@ -4281,7 +4281,7 @@ bool seq_rewriter::reduce_front(expr_ref_vector& ls, expr_ref_vector& rs, expr_r else if (str().is_unit(l, a) && str().is_string(r, s)) { SASSERT(s.length() > 0); app* ch = str().mk_char(s, 0); - SASSERT(m().get_sort(ch) == a->get_sort()); + SASSERT(ch->get_sort() == a->get_sort()); new_eqs.push_back(ch, a); ++head1; if (s.length() == 1) { diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index 5a7f4bffc..77a648202 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -749,7 +749,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { p1 = m().mk_rewrite(old_q, q1); } } - SASSERT(m().get_sort(old_q) == m().get_sort(q1)); + SASSERT(old_q->get_sort() == q1->get_sort()); result = elim_unused_vars(m(), q1, params_ref()); @@ -762,7 +762,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { p2 = m().mk_elim_unused_vars(q1, result); result_pr = m().mk_transitivity(p1, p2); } - SASSERT(m().get_sort(old_q) == m().get_sort(result)); + SASSERT(old_q->get_sort() == result->get_sort()); return true; } diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index f55e3ad1d..e7d382953 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1067,7 +1067,7 @@ void cmd_context::mk_app(symbol const & s, unsigned num_args, expr * const * arg TRACE("macro_bug", tout << "well_sorted_check_enabled(): " << well_sorted_check_enabled() << "\n"; tout << "s: " << s << "\n"; tout << "body:\n" << mk_ismt2_pp(_t, m()) << "\n"; - tout << "args:\n"; for (unsigned i = 0; i < num_args; i++) tout << mk_ismt2_pp(args[i], m()) << "\n" << mk_pp(m().get_sort(args[i]), m()) << "\n";); + tout << "args:\n"; for (unsigned i = 0; i < num_args; i++) tout << mk_ismt2_pp(args[i], m()) << "\n" << mk_pp(args[i]->get_sort(), m()) << "\n";); var_subst subst(m()); scoped_rlimit no_limit(m().limit(), 0); result = subst(_t, coerced_args); diff --git a/src/model/value_factory.cpp b/src/model/value_factory.cpp index 52fb4f7c0..2b412f850 100644 --- a/src/model/value_factory.cpp +++ b/src/model/value_factory.cpp @@ -118,7 +118,7 @@ expr * user_sort_factory::get_fresh_value(sort * s) { } void user_sort_factory::register_value(expr * n) { - SASSERT(!is_finite(m_manager.get_sort(n))); + SASSERT(!is_finite(n->get_sort())); simple_factory::register_value(n); } diff --git a/src/muz/base/bind_variables.cpp b/src/muz/base/bind_variables.cpp index ee50cf503..7b406869d 100644 --- a/src/muz/base/bind_variables.cpp +++ b/src/muz/base/bind_variables.cpp @@ -79,9 +79,9 @@ expr_ref bind_variables::abstract(expr* term, cache_t& cache, unsigned scope) { var* v = w->get_data().m_value; if (!v) { // allocate a bound index. - v = m.mk_var(m_names.size(), m.get_sort(a)); + v = m.mk_var(m_names.size(), a->get_sort()); m_names.push_back(a->get_decl()->get_name()); - m_bound.push_back(m.get_sort(a)); + m_bound.push_back(a->get_sort()); w->get_data().m_value = v; m_pinned.push_back(v); } diff --git a/src/muz/base/dl_rule.cpp b/src/muz/base/dl_rule.cpp index 24604e808..6c49edc27 100644 --- a/src/muz/base/dl_rule.cpp +++ b/src/muz/base/dl_rule.cpp @@ -396,7 +396,7 @@ namespace datalog { m_args.push_back(e); } else { - var* v = m.mk_var(num_bound++, m.get_sort(b)); + var* v = m.mk_var(num_bound++, b->get_sort()); m_args.push_back(v); body.push_back(m.mk_eq(v, b)); } diff --git a/src/muz/base/dl_rule.h b/src/muz/base/dl_rule.h index 7d29b1362..1e19d05c2 100644 --- a/src/muz/base/dl_rule.h +++ b/src/muz/base/dl_rule.h @@ -62,7 +62,7 @@ namespace datalog { m_func = n->get_decl(); } else if (m_dt.is_accessor(n)) { - sort* s = m.get_sort(n->get_arg(0)); + sort* s = n->get_arg(0)->get_sort(); SASSERT(m_dt.is_datatype(s)); if (m_dt.get_datatype_constructors(s)->size() > 1) { m_found = true; diff --git a/src/muz/base/rule_properties.cpp b/src/muz/base/rule_properties.cpp index 0610fd95e..3e5a51196 100644 --- a/src/muz/base/rule_properties.cpp +++ b/src/muz/base/rule_properties.cpp @@ -216,7 +216,7 @@ void rule_properties::operator()(app* n) { m_uninterp_funs.insert(f, m_rule); } else if (m_dt.is_accessor(n)) { - sort* s = m.get_sort(n->get_arg(0)); + sort* s = n->get_arg(0)->get_sort(); SASSERT(m_dt.is_datatype(s)); if (m_dt.get_datatype_constructors(s)->size() > 1) { bool found = false; diff --git a/src/muz/bmc/dl_bmc_engine.cpp b/src/muz/bmc/dl_bmc_engine.cpp index aea8cad0b..dd828f756 100644 --- a/src/muz/bmc/dl_bmc_engine.cpp +++ b/src/muz/bmc/dl_bmc_engine.cpp @@ -293,7 +293,7 @@ namespace datalog { sub[j] = vl; } else { - sub[j] = m.mk_var(j, m.get_sort(sub[j].get())); + sub[j] = m.mk_var(j, sub[j]->get_sort()); } } svector > positions; @@ -811,7 +811,7 @@ namespace datalog { datatype_util dtu(m); ptr_vector sorts; func_decl* p = r.get_decl(); - ptr_vector const& succs = *dtu.get_datatype_constructors(m.get_sort(path)); + ptr_vector const& succs = *dtu.get_datatype_constructors(path->get_sort()); // populate substitution of bound variables. r.get_vars(m, sorts); sub.reset(); @@ -928,11 +928,11 @@ namespace datalog { ptr_vector q_sorts; vector names; for (unsigned i = 0; i < vars.size(); ++i) { - q_sorts.push_back(m.get_sort(vars[i].get())); + q_sorts.push_back(vars[i]->get_sort()); names.push_back(symbol(i+1)); } vars.push_back(path_var); - q_sorts.push_back(m.get_sort(path_var)); + q_sorts.push_back(path_var->get_sort()); names.push_back(symbol("path")); SASSERT(names.size() == q_sorts.size()); SASSERT(vars.size() == names.size()); @@ -1039,7 +1039,7 @@ namespace datalog { proof_ref get_proof(model_ref& md, app* trace, app* path) { datatype_util dtu(m); rule_manager& rm = b.m_ctx.get_rule_manager(); - sort* trace_sort = m.get_sort(trace); + sort* trace_sort = trace->get_sort(); func_decl* p = m_sort2pred.find(trace_sort); datalog::rule_vector const& rules = b.m_rules.get_predicate_rules(p); ptr_vector const& cnstrs = *dtu.get_datatype_constructors(trace_sort); @@ -1226,7 +1226,7 @@ namespace datalog { sub[j] = vl; } else { - sub[j] = m.mk_var(j, m.get_sort(sub[j].get())); + sub[j] = m.mk_var(j, sub[j]->get_sort()); } } svector > positions; diff --git a/src/muz/ddnf/ddnf.cpp b/src/muz/ddnf/ddnf.cpp index 2a83a65e6..4763fce7e 100644 --- a/src/muz/ddnf/ddnf.cpp +++ b/src/muz/ddnf/ddnf.cpp @@ -723,7 +723,7 @@ namespace datalog { func_decl* d = p->get_decl(); SASSERT(d->get_family_id() == null_family_id); for (unsigned i = 0; i < p->get_num_args(); ++i) { - domain.push_back(compile_sort(m.get_sort(p->get_arg(i)))); + domain.push_back(compile_sort(p->get_arg(i)->get_sort())); } func_decl_ref fn(m); fn = m.mk_func_decl(d->get_name(), domain.size(), domain.c_ptr(), m.mk_bool_sort()); @@ -850,7 +850,7 @@ namespace datalog { ddnf_nodes const& ns = m_ddnfs.lookup(num_bits, *t); ddnf_nodes::iterator it = ns.begin(), end = ns.end(); expr_ref_vector eqs(m); - sort* s = m.get_sort(w); + sort* s = w->get_sort(); for (; it != end; ++it) { eqs.push_back(m.mk_eq(w, bv.mk_numeral(rational((*it)->get_id()), s))); } diff --git a/src/muz/fp/datalog_parser.cpp b/src/muz/fp/datalog_parser.cpp index 66aa58602..8ffe59389 100644 --- a/src/muz/fp/datalog_parser.cpp +++ b/src/muz/fp/datalog_parser.cpp @@ -805,10 +805,10 @@ protected: return unexpected(tok3, "at least one argument should be a variable"); } if (v1) { - s = m.get_sort(v1); + s = v1->get_sort(); } else { - s = m.get_sort(v2); + s = v2->get_sort(); } if (!v1) { v1 = mk_const(td1, s); @@ -850,7 +850,7 @@ protected: unsigned arity = args.size(); ptr_vector domain; for (unsigned i = 0; i < arity; ++i) { - domain.push_back(m.get_sort(args[i].get())); + domain.push_back(args[i]->get_sort()); } f = m.mk_func_decl(s, domain.size(), domain.c_ptr(), m.mk_bool_sort()); diff --git a/src/muz/rel/dl_external_relation.cpp b/src/muz/rel/dl_external_relation.cpp index 88511530e..43d68759a 100644 --- a/src/muz/rel/dl_external_relation.cpp +++ b/src/muz/rel/dl_external_relation.cpp @@ -84,7 +84,7 @@ namespace datalog { ast_manager& m = m_rel.get_manager(); family_id fid = get_plugin().get_family_id(); expr* rel = m_rel.get(); - expr_ref res(m.mk_fresh_const("T", m.get_sort(rel)), m); + expr_ref res(m.mk_fresh_const("T", rel->get_sort()), m); expr* rel_out = res.get(); func_decl_ref fn(m.mk_func_decl(fid, OP_RA_CLONE,0,nullptr, 1, &rel), m); get_plugin().reduce_assign(fn, 1, &rel, 1, &rel_out); diff --git a/src/muz/rel/dl_external_relation.h b/src/muz/rel/dl_external_relation.h index 9d6c5c675..4b5689465 100644 --- a/src/muz/rel/dl_external_relation.h +++ b/src/muz/rel/dl_external_relation.h @@ -117,7 +117,7 @@ namespace datalog { unsigned size() const { return get_signature().size(); } - sort* get_sort() const { return m_rel.get_manager().get_sort(m_rel); } + sort* get_sort() const { return m_rel->get_sort(); } void mk_accessor(decl_kind k, func_decl_ref& fn, const relation_fact& f, bool destructive, expr_ref& res) const; diff --git a/src/muz/rel/dl_mk_explanations.cpp b/src/muz/rel/dl_mk_explanations.cpp index 76ed1c5bb..03c4d6fee 100644 --- a/src/muz/rel/dl_mk_explanations.cpp +++ b/src/muz/rel/dl_mk_explanations.cpp @@ -185,7 +185,7 @@ namespace datalog { void to_formula(expr_ref& fml) const override { ast_manager& m = fml.get_manager(); - fml = m.mk_eq(m.mk_var(0, m.get_sort(m_data[0])), m_data[0]); + fml = m.mk_eq(m.mk_var(0, m_data[0]->get_sort()), m_data[0]); } bool is_undefined(unsigned col_idx) const { diff --git a/src/muz/rel/udoc_relation.h b/src/muz/rel/udoc_relation.h index d16760e18..54c0c580a 100644 --- a/src/muz/rel/udoc_relation.h +++ b/src/muz/rel/udoc_relation.h @@ -105,7 +105,7 @@ namespace datalog { static udoc_relation const & get(relation_base const& r); void mk_union(doc_manager& dm, udoc& dst, udoc const& src, udoc* delta); bool is_numeral(expr* e, rational& r, unsigned& num_bits); - unsigned num_sort_bits(expr* e) const { return num_sort_bits(get_ast_manager().get_sort(e)); } + unsigned num_sort_bits(expr* e) const { return num_sort_bits(e->get_sort()); } unsigned num_sort_bits(sort* s) const; bool is_finite_sort(sort* s) const; unsigned num_signature_bits(relation_signature const& sig); diff --git a/src/muz/spacer/spacer_antiunify.cpp b/src/muz/spacer/spacer_antiunify.cpp index 867eef884..ce45818ba 100644 --- a/src/muz/spacer/spacer_antiunify.cpp +++ b/src/muz/spacer/spacer_antiunify.cpp @@ -91,7 +91,7 @@ struct var_abs_rewriter : public default_rewriter_cfg { bool get_subst(expr * s, expr * & t, proof * & t_pr) { if (m_util.is_numeral(s)) { - t = m.mk_var(m_var_index++, m.get_sort(s)); + t = m.mk_var(m_var_index++, s->get_sort()); m_substitution.insert(t, s); m_pinned.push_back(t); m_has_num.mark(s, true); @@ -396,7 +396,7 @@ struct mk_num_pat_rewriter : public default_rewriter_cfg { bool get_subst(expr * s, expr * & t, proof * & t_pr) { if (m_arith.is_numeral(s)) { - t = m.mk_var(m_subs.size(), m.get_sort(s)); + t = m.mk_var(m_subs.size(), s->get_sort()); m_pinned.push_back(t); m_subs.push_back(to_app(s)); diff --git a/src/muz/spacer/spacer_legacy_mev.cpp b/src/muz/spacer/spacer_legacy_mev.cpp index f524d764a..485663d2b 100644 --- a/src/muz/spacer/spacer_legacy_mev.cpp +++ b/src/muz/spacer/spacer_legacy_mev.cpp @@ -467,7 +467,7 @@ void model_evaluator::eval_array_eq(app* e, expr* arg1, expr* arg2) set_true(e); return; } - sort* s = m.get_sort(arg1); + sort* s = arg1->get_sort(); sort* r = get_array_range(s); // give up evaluating finite domain/range arrays if (!r->is_infinite() && !r->is_very_big() && !s->is_infinite() && !s->is_very_big()) { diff --git a/src/muz/spacer/spacer_mev_array.cpp b/src/muz/spacer/spacer_mev_array.cpp index 526743b5f..2f2c2b297 100644 --- a/src/muz/spacer/spacer_mev_array.cpp +++ b/src/muz/spacer/spacer_mev_array.cpp @@ -110,7 +110,7 @@ void model_evaluator_array_util::eval_array_eq(model& mdl, app* e, expr* arg1, e res = m.mk_true (); return; } - sort* s = m.get_sort(arg1); + sort* s = arg1->get_sort(); sort* r = get_array_range(s); // give up evaluating finite domain/range arrays if (!r->is_infinite() && !r->is_very_big() && !s->is_infinite() && !s->is_very_big()) { diff --git a/src/muz/spacer/spacer_proof_utils.cpp b/src/muz/spacer/spacer_proof_utils.cpp index 141d14719..46f715318 100644 --- a/src/muz/spacer/spacer_proof_utils.cpp +++ b/src/muz/spacer/spacer_proof_utils.cpp @@ -124,7 +124,7 @@ namespace spacer { return false; } SASSERT(lit->get_num_args() == 2); - sort* s = m.get_sort(lit->get_arg(0)); + sort* s = lit->get_arg(0)->get_sort(); bool is_int = m_arith.is_int(s); if (!is_int && m_arith.is_int_expr(lit->get_arg(0))) { is_int = true; diff --git a/src/muz/spacer/spacer_qe_project.cpp b/src/muz/spacer/spacer_qe_project.cpp index e528fdd56..615a5b3a7 100644 --- a/src/muz/spacer/spacer_qe_project.cpp +++ b/src/muz/spacer/spacer_qe_project.cpp @@ -101,7 +101,7 @@ peq::peq (app* p, ast_manager& m): VERIFY (is_partial_eq (p)); SASSERT (m_arr_u.is_array (m_lhs) && m_arr_u.is_array (m_rhs) && - ast_eq_proc() (m.get_sort (m_lhs), m.get_sort (m_rhs))); + ast_eq_proc() (m_lhs->get_sort (), m_rhs->get_sort ())); for (unsigned i = 2; i < p->get_num_args (); i++) { m_diff_indices.push_back (p->get_arg (i)); } @@ -120,12 +120,12 @@ peq::peq (expr* lhs, expr* rhs, unsigned num_indices, expr * const * diff_indice { SASSERT (m_arr_u.is_array (lhs) && m_arr_u.is_array (rhs) && - ast_eq_proc() (m.get_sort (lhs), m.get_sort (rhs))); + ast_eq_proc() (lhs->get_sort (), rhs->get_sort ())); ptr_vector sorts; - sorts.push_back (m.get_sort (m_lhs)); - sorts.push_back (m.get_sort (m_rhs)); + sorts.push_back (m_lhs->get_sort ()); + sorts.push_back (m_rhs->get_sort ()); for (unsigned i = 0; i < num_indices; i++) { - sorts.push_back (m.get_sort (diff_indices [i])); + sorts.push_back (diff_indices[i]->get_sort ()); m_diff_indices.push_back (diff_indices [i]); } m_decl = m.mk_func_decl (symbol (PARTIAL_EQ), sorts.size (), sorts.c_ptr (), m.mk_bool_sort ()); @@ -161,7 +161,7 @@ void peq::mk_eq (app_ref_vector& aux_consts, app_ref& result, bool stores_on_rhs std::swap (lhs, rhs); } // lhs = (...(store (store rhs i0 v0) i1 v1)...) - sort* val_sort = get_array_range (m.get_sort (lhs)); + sort* val_sort = get_array_range (lhs->get_sort ()); expr_ref_vector::iterator end = m_diff_indices.end (); for (expr_ref_vector::iterator it = m_diff_indices.begin (); it != end; it++) { @@ -241,7 +241,7 @@ namespace spacer_qe { res = is_linear(-mul, t1, c, ts); } else if (a.is_numeral(t, mul1)) { - ts.push_back(a.mk_numeral(mul*mul1, m.get_sort(t))); + ts.push_back(a.mk_numeral(mul*mul1, t->get_sort())); } else if ((*m_var)(t)) { IF_VERBOSE(2, verbose_stream() << "can't project:" << mk_pp(t, m) << "\n";); @@ -252,7 +252,7 @@ namespace spacer_qe { ts.push_back(t); } else { - ts.push_back(a.mk_mul(a.mk_numeral(mul, m.get_sort(t)), t)); + ts.push_back(a.mk_mul(a.mk_numeral(mul, t->get_sort()), t)); } return res; } @@ -411,7 +411,7 @@ namespace spacer_qe { expr_ref cx (m), cxt (m), z (m), result (m); cx = mk_mul (m_coeffs[i], eq_term); cxt = mk_add (cx, m_terms.get(i)); - z = a.mk_numeral(rational(0), m.get_sort(eq_term)); + z = a.mk_numeral(rational(0), eq_term->get_sort()); if (m_eq[i]) { // c*x + t = 0 result = a.mk_eq (cxt, z); @@ -842,7 +842,7 @@ namespace spacer_qe { bt = mk_mul(abs(bc), t); as = mk_mul(abs(ac), s); ts = mk_add(bt, as); - z = a.mk_numeral(rational(0), m.get_sort(t)); + z = a.mk_numeral(rational(0), t->get_sort()); expr_ref result1(m), result2(m); if (m_strict[i] || m_strict[j]) { result1 = a.mk_lt(ts, z); @@ -898,7 +898,7 @@ namespace spacer_qe { return a.mk_add(t1, t2); } expr* mk_mul(rational const& r, expr* t2) { - expr* t1 = a.mk_numeral(r, m.get_sort(t2)); + expr* t1 = a.mk_numeral(r, t2->get_sort()); return a.mk_mul(t1, t2); } @@ -1407,7 +1407,7 @@ namespace spacer_qe { // if a_new is select on m_v, introduce new constant if (m_arr_u.is_select (a) && (args.get (0) == m_v || m_has_stores_v.is_marked (args.get (0)))) { - sort* val_sort = get_array_range (m.get_sort (m_v)); + sort* val_sort = get_array_range (m_v->get_sort()); app_ref val_const (m.mk_fresh_const ("sel", val_sort), m); m_aux_vars.push_back (val_const); // extend M to include val_const @@ -2073,7 +2073,7 @@ namespace spacer_qe { if (sel_terms.empty ()) return; expr* v = sel_terms.get (0)->get_arg (0); // array variable - sort* v_sort = m.get_sort (v); + sort* v_sort = v->get_sort (); sort* val_sort = get_array_range (v_sort); sort* idx_sort = get_array_domain (v_sort, 0); (void) idx_sort; diff --git a/src/muz/tab/tab_context.cpp b/src/muz/tab/tab_context.cpp index 15325da43..c43589e17 100644 --- a/src/muz/tab/tab_context.cpp +++ b/src/muz/tab/tab_context.cpp @@ -1216,9 +1216,9 @@ namespace tb { func_decl_ref delta(m); sort_ref_vector dom(m); for (unsigned j = 0; j < 1; ++j) { - for (unsigned i = 0; i < zs.size(); ++i) { - dom.push_back(m.get_sort(zs[i].get())); - zszs.push_back(zs[i].get()); + for (expr* arg : zs) { + dom.push_back(arg->get_sort()); + zszs.push_back(arg); } } app_ref_vector preds(m); @@ -1282,7 +1282,7 @@ namespace tb { app* p = g.get_head(); unsigned num_vars = g.get_num_vars(); for (unsigned i = 0; i < p->get_num_args(); ++i) { - result.push_back(m.mk_var(num_vars+i, m.get_sort(p->get_arg(i)))); + result.push_back(m.mk_var(num_vars+i, p->get_arg(i)->get_sort())); } return result; } diff --git a/src/muz/transforms/dl_mk_coalesce.cpp b/src/muz/transforms/dl_mk_coalesce.cpp index 5e31de326..e1e7d34e2 100644 --- a/src/muz/transforms/dl_mk_coalesce.cpp +++ b/src/muz/transforms/dl_mk_coalesce.cpp @@ -48,10 +48,10 @@ namespace datalog { for (unsigned i = 0; i < sz; ++i) { expr* a = p1->get_arg(i); expr* b = p2->get_arg(i); - SASSERT(m.get_sort(a) == m.get_sort(b)); + SASSERT(a->get_sort() == b->get_sort()); m_sub1.push_back(a); m_sub2.push_back(b); - args.push_back(m.mk_var(m_idx++, m.get_sort(a))); + args.push_back(m.mk_var(m_idx++, a->get_sort())); } pred = m.mk_app(p1->get_decl(), args.size(), args.c_ptr()); } @@ -80,14 +80,14 @@ namespace datalog { } else { SASSERT(revsub[v].get()); - SASSERT(m.get_sort(revsub[v].get()) == s); + SASSERT(revsub[v]->get_sort() == s); conjs.push_back(m.mk_eq(revsub[v].get(), w)); } } } else { SASSERT(m.is_value(e)); - SASSERT(e->get_sort() == m.get_sort(w)); + SASSERT(e->get_sort() == w->get_sort()); conjs.push_back(m.mk_eq(e, w)); } } diff --git a/src/muz/transforms/dl_mk_elim_term_ite.cpp b/src/muz/transforms/dl_mk_elim_term_ite.cpp index 1005f7667..9d8d59d5f 100644 --- a/src/muz/transforms/dl_mk_elim_term_ite.cpp +++ b/src/muz/transforms/dl_mk_elim_term_ite.cpp @@ -95,7 +95,7 @@ namespace datalog { continue; if (!m_ground.get(i)) m_ground[i] = m.mk_fresh_const("c", fv[i]); - SASSERT(m.get_sort(m_ground.get(i)) == fv[i]); + SASSERT(m_ground[i]->get_sort() == fv[i]); } var_subst vsub(m, false); return vsub(e, m_ground); diff --git a/src/muz/transforms/dl_mk_quantifier_abstraction.cpp b/src/muz/transforms/dl_mk_quantifier_abstraction.cpp index bcd54d016..603035979 100644 --- a/src/muz/transforms/dl_mk_quantifier_abstraction.cpp +++ b/src/muz/transforms/dl_mk_quantifier_abstraction.cpp @@ -95,7 +95,7 @@ namespace datalog { // the original predicate. expr_safe_replace rep(m); for (unsigned i = 0; i < sub.size(); ++i) { - rep.insert(m.mk_var(i, m.get_sort(sub[i])), sub[i]); + rep.insert(m.mk_var(i, sub[i]->get_sort()), sub[i]); } rep(body); rep.reset(); @@ -130,7 +130,7 @@ namespace datalog { // 4. replace remaining constants by variables. unsigned j = 0; for (expr* f : _free) { - rep.insert(f, m.mk_var(j++, m.get_sort(f))); + rep.insert(f, m.mk_var(j++, f->get_sort())); } rep(body); diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index b9e0b26c1..fa38ee2a9 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -1187,7 +1187,7 @@ namespace opt { app* context::purify(generic_model_converter_ref& fm, expr* term) { std::ostringstream out; out << mk_pp(term, m); - app* q = m.mk_fresh_const(out.str(), m.get_sort(term)); + app* q = m.mk_fresh_const(out.str(), term->get_sort()); if (!fm) fm = alloc(generic_model_converter, m, "opt"); if (m_arith.is_int_real(term)) { m_hard_constraints.push_back(m_arith.mk_ge(q, term)); diff --git a/src/qe/mbp/mbp_arrays.cpp b/src/qe/mbp/mbp_arrays.cpp index 7f9c34fc3..3602b2d39 100644 --- a/src/qe/mbp/mbp_arrays.cpp +++ b/src/qe/mbp/mbp_arrays.cpp @@ -72,7 +72,7 @@ namespace { VERIFY (is_partial_eq (p)); SASSERT (m_arr_u.is_array (m_lhs) && m_arr_u.is_array (m_rhs) && - m.get_sort(m_lhs) == m.get_sort(m_rhs)); + m_lhs->get_sort() == m_rhs->get_sort()); unsigned arity = get_array_arity(m_lhs->get_sort()); for (unsigned i = 2; i < p->get_num_args (); i += arity) { SASSERT(arity + i <= p->get_num_args()); @@ -93,12 +93,12 @@ namespace { m_arr_u (m) { SASSERT (m_arr_u.is_array (lhs) && m_arr_u.is_array (rhs) && - m.get_sort(lhs) == m.get_sort(rhs)); + lhs->get_sort() == rhs->get_sort()); ptr_vector sorts; sorts.push_back (m_lhs->get_sort ()); sorts.push_back (m_rhs->get_sort ()); for (auto const& v : diff_indices) { - SASSERT(v.size() == get_array_arity(m.get_sort(m_lhs))); + SASSERT(v.size() == get_array_arity(m_lhs->get_sort())); for (expr* e : v) sorts.push_back (e->get_sort()); } diff --git a/src/sat/smt/array_axioms.cpp b/src/sat/smt/array_axioms.cpp index e3aea9f25..4f26af02e 100644 --- a/src/sat/smt/array_axioms.cpp +++ b/src/sat/smt/array_axioms.cpp @@ -385,7 +385,7 @@ namespace array { ++m_stats.m_num_select_lambda_axiom; SASSERT(is_lambda(lambda)); SASSERT(a.is_select(select)); - SASSERT(m.get_sort(lambda) == m.get_sort(select->get_arg(0))); + SASSERT(lambda->get_sort() == select->get_arg(0)->get_sort()); ptr_vector args(select->get_num_args(), select->get_args()); args[0] = lambda; expr_ref alpha(a.mk_select(args), m); diff --git a/src/sat/smt/array_solver.cpp b/src/sat/smt/array_solver.cpp index 02d7ce1dd..c90e14491 100644 --- a/src/sat/smt/array_solver.cpp +++ b/src/sat/smt/array_solver.cpp @@ -206,7 +206,7 @@ namespace array { void solver::add_parent_select(theory_var v_child, euf::enode* select) { SASSERT(a.is_select(select->get_expr())); - SASSERT(m.get_sort(select->get_arg(0)->get_expr()) == m.get_sort(var2expr(v_child))); + SASSERT(select->get_arg(0)->get_expr()->get_sort() == var2expr(v_child)->get_sort()); v_child = find(v_child); ctx.push_vec(get_var_data(v_child).m_parent_selects, select); diff --git a/src/sat/smt/bv_internalize.cpp b/src/sat/smt/bv_internalize.cpp index 4e5e95e13..4fe50959c 100644 --- a/src/sat/smt/bv_internalize.cpp +++ b/src/sat/smt/bv_internalize.cpp @@ -393,7 +393,7 @@ namespace bv { void solver::assert_bv2int_axiom(app* n) { expr* k = nullptr; VERIFY(bv.is_bv2int(n, k)); - SASSERT(bv.is_bv_sort(m.get_sort(k))); + SASSERT(bv.is_bv_sort(k->get_sort())); expr_ref_vector k_bits(m); euf::enode* k_enode = expr2enode(k); get_bits(k_enode, k_bits); diff --git a/src/smt/seq_eq_solver.cpp b/src/smt/seq_eq_solver.cpp index c8d3f73df..cd91b790c 100644 --- a/src/smt/seq_eq_solver.cpp +++ b/src/smt/seq_eq_solver.cpp @@ -114,10 +114,10 @@ bool theory_seq::solve_unit_eq(expr* l, expr* r, dependency* deps) { } bool theory_seq::solve_unit_eq(expr_ref_vector const& l, expr_ref_vector const& r, dependency* deps) { - if (l.size() == 1 && is_var(l[0]) && !occurs(l[0], r) && add_solution(l[0], mk_concat(r, m.get_sort(l[0])), deps)) { + if (l.size() == 1 && is_var(l[0]) && !occurs(l[0], r) && add_solution(l[0], mk_concat(r, l[0]->get_sort()), deps)) { return true; } - if (r.size() == 1 && is_var(r[0]) && !occurs(r[0], l) && add_solution(r[0], mk_concat(l, m.get_sort(r[0])), deps)) { + if (r.size() == 1 && is_var(r[0]) && !occurs(r[0], l) && add_solution(r[0], mk_concat(l, r[0]->get_sort()), deps)) { return true; } return false; @@ -410,7 +410,7 @@ bool theory_seq::len_based_split(eq const& e) { TRACE("seq", tout << "split based on length\n";); TRACE("seq", display_equation(tout, e);); - sort* srt = m.get_sort(ls[0]); + sort* srt = ls[0]->get_sort(); expr_ref x11 = expr_ref(ls[0], m); expr_ref x12 = mk_concat(ls.size()-1, ls.c_ptr()+1, srt); expr_ref y11 = expr_ref(rs[0], m); @@ -604,7 +604,7 @@ bool theory_seq::split_lengths(dependency* dep, else if (m_util.str.is_unit(Y)) { SASSERT(lenB == lenX); bs.push_back(Y); - expr_ref bY = mk_concat(bs, m.get_sort(Y)); + expr_ref bY = mk_concat(bs, Y->get_sort()); propagate_eq(dep, lits, X, bY, true); } else { @@ -1172,7 +1172,7 @@ bool theory_seq::find_branch_candidate(unsigned& start, dependency* dep, expr_re TRACE("seq", tout << mk_pp(l, m) << ": " << ctx.get_scope_level() << " - start:" << start << "\n";); expr_ref v0(m); - v0 = m_util.str.mk_empty(m.get_sort(l)); + v0 = m_util.str.mk_empty(l->get_sort()); if (can_be_equal(ls.size() - 1, ls.c_ptr() + 1, rs.size(), rs.c_ptr())) { if (assume_equality(l, v0)) { TRACE("seq", tout << mk_pp(l, m) << " " << v0 << "\n";); @@ -1467,7 +1467,7 @@ bool theory_seq::is_quat_eq(expr_ref_vector const& ls, expr_ref_vector const& rs if (ls.size() > 1 && is_var(ls[0]) && is_var(ls.back()) && rs.size() > 1 && is_var(rs[0]) && is_var(rs.back())) { unsigned l_start = 1; - sort* srt = m.get_sort(ls[0]); + sort* srt = ls[0]->get_sort(); for (; l_start < ls.size()-1; ++l_start) { if (m_util.str.is_unit(ls[l_start])) break; } @@ -1510,7 +1510,7 @@ bool theory_seq::is_quat_eq(expr_ref_vector const& ls, expr_ref_vector const& rs bool theory_seq::is_ternary_eq_rhs(expr_ref_vector const& ls, expr_ref_vector const& rs, expr_ref& x, expr_ref_vector& xs, expr_ref& y1, expr_ref_vector& ys, expr_ref& y2) { if (ls.size() > 1 && rs.size() > 1 && is_var(rs[0]) && is_var(rs.back())) { - sort* srt = m.get_sort(ls[0]); + sort* srt = ls[0]->get_sort(); unsigned l_start = ls.size()-1; for (; l_start > 0; --l_start) { if (!m_util.str.is_unit(ls[l_start])) break; @@ -1548,7 +1548,7 @@ bool theory_seq::is_ternary_eq_rhs(expr_ref_vector const& ls, expr_ref_vector co bool theory_seq::is_ternary_eq_lhs(expr_ref_vector const& ls, expr_ref_vector const& rs, expr_ref_vector& xs, expr_ref& x, expr_ref& y1, expr_ref_vector& ys, expr_ref& y2) { if (ls.size() > 1 && rs.size() > 1 && is_var(rs[0]) && is_var(rs.back())) { - sort* srt = m.get_sort(ls[0]); + sort* srt = ls[0]->get_sort(); unsigned l_start = 0; for (; l_start < ls.size()-1; ++l_start) { if (!m_util.str.is_unit(ls[l_start])) break; @@ -1600,7 +1600,7 @@ bool theory_seq::solve_nth_eq2(expr_ref_vector const& ls, expr_ref_vector const& expr_ref_vector ls1(m), rs1(m); expr_ref idx1(m_autil.mk_add(idx, m_autil.mk_int(1)), m); m_rewrite(idx1); - expr_ref rhs = mk_concat(rs.size(), rs.c_ptr(), m.get_sort(ls[0])); + expr_ref rhs = mk_concat(rs.size(), rs.c_ptr(), ls[0]->get_sort()); if (m_nth_eq2_cache.contains(std::make_pair(rhs, ls[0]))) return false; m_nth_eq2_cache.insert(std::make_pair(rhs, ls[0])); @@ -1641,7 +1641,7 @@ bool theory_seq::solve_nth_eq1(expr_ref_vector const& ls, expr_ref_vector const& } return false; } - add_solution(l, mk_concat(rs, m.get_sort(l)), dep); + add_solution(l, mk_concat(rs, l->get_sort()), dep); return true; } diff --git a/src/smt/seq_ne_solver.cpp b/src/smt/seq_ne_solver.cpp index dc44b52cf..bdfa90923 100644 --- a/src/smt/seq_ne_solver.cpp +++ b/src/smt/seq_ne_solver.cpp @@ -142,7 +142,7 @@ bool theory_seq::propagate_ne2eq(unsigned idx, expr_ref_vector const& es) { } ne const& n = m_nqs[idx]; expr_ref e(m), head(m), tail(m); - e = mk_concat(es, m.get_sort(es[0])); + e = mk_concat(es, es[0]->get_sort()); m_sk.decompose(e, head, tail); propagate_eq(n.dep(), n.lits(), e, mk_concat(head, tail), false); return true; diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index 3effad182..bf62acac1 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -55,7 +55,7 @@ namespace smt { expr* e = ctx.bool_var2expr(lit.var()); expr_ref id(a().mk_int(e->get_id()), m); VERIFY(str().is_in_re(e, s, r)); - sort* seq_sort = m.get_sort(s); + sort* seq_sort = s->get_sort(); vector patterns; auto mk_cont = [&](unsigned idx) { return sk().mk("seq.cont", id, a().mk_int(idx), seq_sort); @@ -158,7 +158,7 @@ namespace smt { } else { //add the literal back - expr_ref r_alias(m.mk_fresh_const(symbol(r->get_id()), m.get_sort(r), false), m); + expr_ref r_alias(m.mk_fresh_const(symbol(r->get_id()), r->get_sort(), false), m); expr_ref s_in_r_alias(re().mk_in_re(s, r_alias), m); literal s_in_r_alias_lit = th.mk_literal(s_in_r_alias); m_const_to_expr.insert(r_alias, r, nullptr); @@ -192,7 +192,7 @@ namespace smt { */ expr_ref seq_regex::get_overapprox_regex(expr* s) { expr_ref s_to_re(re().mk_to_re(s), m); - expr_ref dotstar(re().mk_full_seq(m.get_sort(s_to_re)), m); + expr_ref dotstar(re().mk_full_seq(s_to_re->get_sort()), m); if (m.is_value(s)) return s_to_re; @@ -209,7 +209,7 @@ namespace smt { last = e_approx; } if (!s_approx) - s_approx = re().mk_epsilon(m.get_sort(s)); + s_approx = re().mk_epsilon(s->get_sort()); return s_approx; } @@ -402,7 +402,7 @@ namespace smt { expr_ref seq_regex::symmetric_diff(expr* r1, expr* r2) { expr_ref r(m); if (r1 == r2) - r = re().mk_empty(m.get_sort(r1)); + r = re().mk_empty(r1->get_sort()); else if (re().is_empty(r1)) r = r2; else if (re().is_empty(r2)) @@ -458,7 +458,7 @@ namespace smt { STRACE("seq_regex", tout << "derivative(" << mk_pp(hd, m) << "): " << mk_pp(r, m) << std::endl;); // Use canonical variable for head - expr_ref hd_canon(m.mk_var(0, m.get_sort(hd)), m); + expr_ref hd_canon(m.mk_var(0, hd->get_sort()), m); expr_ref result(re().mk_derivative(hd_canon, r), m); rewrite(result); @@ -496,7 +496,7 @@ namespace smt { if (re().is_empty(r)) //trivially true return; - expr_ref emp(re().mk_empty(m.get_sort(r)), m); + expr_ref emp(re().mk_empty(r->get_sort()), m); expr_ref f(m.mk_fresh_const("re.char", seq_sort), m); expr_ref is_empty = sk().mk_is_empty(r, r, f); // is_empty : (re,re,seq) -> Bool is a Skolem function @@ -516,7 +516,7 @@ namespace smt { sort* seq_sort = nullptr; VERIFY(u().is_re(r1, seq_sort)); expr_ref r = symmetric_diff(r1, r2); - expr_ref emp(re().mk_empty(m.get_sort(r)), m); + expr_ref emp(re().mk_empty(r->get_sort()), m); expr_ref n(m.mk_fresh_const("re.char", seq_sort), m); expr_ref is_non_empty = sk().mk_is_non_empty(r, r, n); th.add_axiom(th.mk_eq(r1, r2, false), th.mk_literal(is_non_empty)); diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 0c23c4578..a362cc364 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -259,7 +259,7 @@ namespace smt { See comments in theory::mk_eq_atom */ app * context::mk_eq_atom(expr * lhs, expr * rhs) { - family_id fid = m.get_sort(lhs)->get_family_id(); + family_id fid = lhs->get_sort()->get_family_id(); theory * th = get_theory(fid); if (th) return th->mk_eq_atom(lhs, rhs); @@ -474,7 +474,7 @@ namespace smt { TRACE("add_eq", tout << "assigning: #" << n1->get_owner_id() << " = #" << n2->get_owner_id() << "\n";); TRACE("add_eq_detail", tout << "assigning\n" << enode_pp(n1, *this) << "\n" << enode_pp(n2, *this) << "\n"; tout << "kind: " << js.get_kind() << "\n";); - SASSERT(m.get_sort(n1->get_owner()) == m.get_sort(n2->get_owner())); + SASSERT(n1->get_owner()->get_sort() == n2->get_owner()->get_sort()); m_stats.m_num_add_eq++; enode * r1 = n1->get_root(); @@ -1115,14 +1115,14 @@ namespace smt { context. */ bool context::is_diseq(enode * n1, enode * n2) const { - SASSERT(m.get_sort(n1->get_owner()) == m.get_sort(n2->get_owner())); + SASSERT(n1->get_owner()->get_sort() == n2->get_owner()->get_sort()); context * _this = const_cast(this); if (!m_is_diseq_tmp) { app * eq = m.mk_eq(n1->get_owner(), n2->get_owner()); m.inc_ref(eq); _this->m_is_diseq_tmp = enode::mk_dummy(m, m_app2enode, eq); } - else if (m.get_sort(m_is_diseq_tmp->get_owner()->get_arg(0)) != m.get_sort(n1->get_owner())) { + else if (m_is_diseq_tmp->get_owner()->get_arg(0)->get_sort() != n1->get_owner()->get_sort()) { m.dec_ref(m_is_diseq_tmp->get_owner()); app * eq = m.mk_eq(n1->get_owner(), n2->get_owner()); m.inc_ref(eq); @@ -4388,7 +4388,7 @@ namespace smt { bool_var_data & d = get_bdata(v); d.set_eq_flag(); set_true_first_flag(v); - sort * s = m.get_sort(to_app(eq)->get_arg(0)); + sort * s = to_app(eq)->get_arg(0)->get_sort(); theory * th = m_theories.get_plugin(s->get_family_id()); if (th) th->internalize_eq_eh(to_app(eq), v); diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 2a13b29f3..cd1add643 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1078,7 +1078,7 @@ namespace smt { void push_eq(enode * lhs, enode * rhs, eq_justification const & js) { if (lhs->get_root() != rhs->get_root()) { - SASSERT(m.get_sort(lhs->get_owner()) == m.get_sort(rhs->get_owner())); + SASSERT(lhs->get_owner()->get_sort() == rhs->get_owner()->get_sort()); m_eq_propagation_queue.push_back(new_eq(lhs, rhs, js)); } } diff --git a/src/smt/smt_context_inv.cpp b/src/smt/smt_context_inv.cpp index 4c3d16bee..63a45d0d5 100644 --- a/src/smt/smt_context_inv.cpp +++ b/src/smt/smt_context_inv.cpp @@ -279,7 +279,7 @@ namespace smt { if (lhs == rhs) continue; TRACE("check_th_diseq_propagation", tout << "num. theory_vars: " << lhs->get_num_th_vars() << " " - << mk_pp(m.get_sort(lhs->get_owner()), m) << "\n";); + << mk_pp(lhs->get_owner()->get_sort(), m) << "\n";); theory_var_list * l = lhs->get_th_var_list(); while (l) { theory_id th_id = l->get_id(); diff --git a/src/smt/smt_implied_equalities.cpp b/src/smt/smt_implied_equalities.cpp index 8722e6701..f02639c90 100644 --- a/src/smt/smt_implied_equalities.cpp +++ b/src/smt/smt_implied_equalities.cpp @@ -92,7 +92,7 @@ namespace { if (j < i && non_values.contains(j)) continue; if (found_root_value && !non_values.contains(j)) continue; expr* s = terms[j].term; - SASSERT(m.get_sort(t) == m.get_sort(s)); + SASSERT(t->get_sort() == s->get_sort()); ++m_stats_calls; m_solver.push(); m_solver.assert_expr(m.mk_not(m.mk_eq(s, t))); @@ -118,7 +118,7 @@ namespace { expr* t = terms[i].term; for (unsigned j = 0; j < i; ++j) { expr* s = terms[j].term; - SASSERT(m.get_sort(t) == m.get_sort(s)); + SASSERT(t->get_sort() == s->get_sort()); ++m_stats_calls; m_stats_timer.start(); m_solver.push(); diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index cb3f07851..e82d0c791 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -94,11 +94,11 @@ namespace smt { } for (expr* f : m_fresh_exprs) { - if (m.get_sort(f) == m.get_sort(val)) { + if (f->get_sort() == val->get_sort()) { return f; } } - fresh_term = m.mk_fresh_const("sk", m.get_sort(val)); + fresh_term = m.mk_fresh_const("sk", val->get_sort()); } m_fresh_exprs.push_back(fresh_term); m_context->ensure_internalized(fresh_term); diff --git a/src/smt/smt_model_generator.cpp b/src/smt/smt_model_generator.cpp index 382f6d64f..b07ada6fa 100644 --- a/src/smt/smt_model_generator.cpp +++ b/src/smt/smt_model_generator.cpp @@ -94,7 +94,7 @@ namespace smt { for (enode * r : m_context->enodes()) { if (r == r->get_root() && (m_context->is_relevant(r) || m.is_value(r->get_expr()))) { roots.push_back(r); - sort * s = m.get_sort(r->get_owner()); + sort * s = r->get_owner()->get_sort(); model_value_proc * proc = nullptr; if (m.is_bool(s)) { CTRACE("model", m_context->get_assignment(r) == l_undef, @@ -117,7 +117,7 @@ namespace smt { } else { TRACE("model", tout << "creating fresh value for #" << r->get_owner_id() << "\n";); - proc = alloc(fresh_value_proc, mk_extra_fresh_value(m.get_sort(r->get_owner()))); + proc = alloc(fresh_value_proc, mk_extra_fresh_value(r->get_owner()->get_sort())); } } else { @@ -136,7 +136,7 @@ namespace smt { SASSERT(r == r->get_root()); expr * n = r->get_owner(); if (!m.is_model_value(n)) { - sort * s = m.get_sort(r->get_owner()); + sort * s = r->get_owner()->get_sort(); n = m_model->get_fresh_value(s); CTRACE("model", n == 0, tout << mk_pp(r->get_owner(), m) << "\nsort:\n" << mk_pp(s, m) << "\n"; @@ -183,12 +183,12 @@ namespace smt { return true; bool visited = true; for (enode * r : roots) { - if (m.get_sort(r->get_owner()) != s) + if (r->get_owner()->get_sort() != s) continue; SASSERT(r == r->get_root()); if (root2proc[r]->is_fresh()) continue; // r is associated with a fresh value... - TRACE("mg_top_sort", tout << "fresh!" << src.get_value()->get_idx() << " -> #" << r->get_owner_id() << " " << mk_pp(m.get_sort(r->get_owner()), m) << "\n";); + TRACE("mg_top_sort", tout << "fresh!" << src.get_value()->get_idx() << " -> #" << r->get_owner_id() << " " << mk_pp(r->get_owner()->get_sort(), m) << "\n";); visit_child(source(r), colors, todo, visited); TRACE("mg_top_sort", tout << "visited: " << visited << ", todo.size(): " << todo.size() << "\n";); } diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index 5367f6e1e..d25331a6d 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -1089,19 +1089,19 @@ namespace smt { expr* obj = get_enode(v)->get_owner(); expr_ref e(m); rational r = val.get_rational(); - if (m_util.is_int(m.get_sort(obj))) { + if (m_util.is_int(obj->get_sort())) { if (r.is_int()) { r += rational::one(); } else { r = ceil(r); } - e = m_util.mk_numeral(r, m.get_sort(obj)); + e = m_util.mk_numeral(r, obj->get_sort()); e = m_util.mk_ge(obj, e); } else { // obj is over the reals. - e = m_util.mk_numeral(r, m.get_sort(obj)); + e = m_util.mk_numeral(r, obj->get_sort()); if (val.get_infinitesimal().is_neg()) { e = m_util.mk_ge(obj, e); diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 5da77cd29..690e82786 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -1376,7 +1376,7 @@ namespace smt { else { if (n1->get_owner_id() > n2->get_owner_id()) std::swap(n1, n2); - sort * st = m.get_sort(n1->get_owner()); + sort * st = n1->get_owner()->get_sort(); app * minus_one = m_util.mk_numeral(rational::minus_one(), st); app * s = m_util.mk_add(n1->get_owner(), m_util.mk_mul(minus_one, n2->get_owner())); ctx.internalize(s, false); diff --git a/src/smt/theory_arith_eq.h b/src/smt/theory_arith_eq.h index 9e2da768e..fb909100c 100644 --- a/src/smt/theory_arith_eq.h +++ b/src/smt/theory_arith_eq.h @@ -322,7 +322,7 @@ namespace smt { if (is_equal(x, y)) return; // I doesn't make sense to propagate an equality (to the core) of variables of different sort. - if (m.get_sort(var2expr(x)) != m.get_sort(var2expr(y))) { + if (var2expr(x)->get_sort() != var2expr(y)->get_sort()) { TRACE("arith", tout << mk_pp(var2expr(x), m) << " = " << mk_pp(var2expr(y), m) << "\n";); return; } diff --git a/src/smt/theory_array_bapa.cpp b/src/smt/theory_array_bapa.cpp index 74722fa25..1a11c2fd6 100644 --- a/src/smt/theory_array_bapa.cpp +++ b/src/smt/theory_array_bapa.cpp @@ -229,7 +229,7 @@ namespace smt { SASSERT(i2.m_is_leaf); expr* s = sz1->get_arg(0); expr* t = sz2->get_arg(0); - if (m.get_sort(s) != m.get_sort(t)) { + if (s->get_sort() != t->get_sort()) { return true; } enode* r1 = get_root(s); @@ -369,7 +369,7 @@ namespace smt { // create skolem function that is injective on integers (ensures uniqueness). expr_ref mk_index_skolem(app* sz, expr* a, unsigned n) { func_decls fg; - sort* s = m.get_sort(a); + sort* s = a->get_sort(); if (!m_index_skolems.find(s, fg)) { sort* idx_sort = get_array_domain(s, 0); sort* dom1[2] = { s, m_arith.mk_int() }; @@ -500,7 +500,7 @@ namespace smt { expr* s = term->get_arg(0); expr* n = term->get_arg(1); mk_th_axiom(~lit, mk_literal(m_arith.mk_ge(n, m_arith.mk_int(0)))); - sort_size const& sz = m.get_sort(s)->get_num_elements(); + sort_size const& sz = s->get_sort()->get_num_elements(); if (sz.is_infinite()) { mk_th_axiom(~lit, mk_eq(th.mk_default(s), m.mk_false())); } @@ -585,7 +585,7 @@ namespace smt { bool is_size_limit(app* e, expr*& set, expr*& sz) { func_decl* d = nullptr; - if (e->get_num_args() > 0 && m_size_limit_sort2skolems.find(m.get_sort(e->get_arg(0)), d) && d == e->get_decl()) { + if (e->get_num_args() > 0 && m_size_limit_sort2skolems.find(e->get_arg(0)->get_sort(), d) && d == e->get_decl()) { set = e->get_arg(0); sz = e->get_arg(1); return true; @@ -599,7 +599,7 @@ namespace smt { app_ref mk_size_limit(expr* set, expr* sz) { func_decl* sk = nullptr; - sort* s = m.get_sort(set); + sort* s = set->get_sort(); if (!m_size_limit_sort2skolems.find(s, sk)) { sort* dom[3] = { s, m_arith.mk_int(), m_arith.mk_int() }; sk = m.mk_fresh_func_decl("value-limit", "", 3, dom, m.mk_bool_sort()); diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index d99bd441d..b66fe36b7 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -604,7 +604,7 @@ namespace smt { TRACE("bv2int_bug", tout << "bv2int:\n" << mk_pp(n, m) << "\n";); sort * int_sort = n->get_sort(); app * k = to_app(n->get_arg(0)); - SASSERT(m_util.is_bv_sort(m.get_sort(k))); + SASSERT(m_util.is_bv_sort(k->get_sort())); expr_ref_vector k_bits(m); enode * k_enode = mk_enode(k); get_bits(k_enode, k_bits); diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index 1c8907287..a7c8a26cc 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -596,7 +596,7 @@ namespace smt { } // explore `arg` (with parent) expr* earg = arg->get_owner(); - sort* s = m.get_sort(earg); + sort* s = earg->get_sort(); if (m_util.is_datatype(s)) { m_parent.insert(arg->get_root(), parent); oc_push_stack(arg); @@ -610,7 +610,7 @@ namespace smt { occurs_check_explain(parent, aarg); return true; } - if (m_util.is_datatype(m.get_sort(aarg->get_owner()))) { + if (m_util.is_datatype(aarg->get_owner()->get_sort())) { m_parent.insert(aarg->get_root(), parent); oc_push_stack(aarg); } diff --git a/src/smt/theory_dense_diff_logic_def.h b/src/smt/theory_dense_diff_logic_def.h index deab6171e..d41bab49f 100644 --- a/src/smt/theory_dense_diff_logic_def.h +++ b/src/smt/theory_dense_diff_logic_def.h @@ -808,7 +808,7 @@ namespace smt { // 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 (m.get_sort(n2->get_owner()) == s) { + if (n2->get_owner()->get_sort() == s) { m_assignment[v2] -= val; } } @@ -1106,7 +1106,7 @@ namespace smt { return f; } - e = m_autil.mk_numeral(val.get_rational(), m.get_sort(f)); + e = m_autil.mk_numeral(val.get_rational(), f->get_sort()); if (val.get_infinitesimal().is_neg()) { if (is_strict) { diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h index 62eaef9a1..544d69960 100644 --- a/src/smt/theory_diff_logic_def.h +++ b/src/smt/theory_diff_logic_def.h @@ -1036,7 +1036,7 @@ void theory_diff_logic::new_eq_or_diseq(bool is_eq, theory_var v1, theory_v app* s1 = get_enode(s)->get_owner(); app* t1 = get_enode(t)->get_owner(); s2 = m_util.mk_sub(t1, s1); - t2 = m_util.mk_numeral(k, m.get_sort(s2.get())); + t2 = m_util.mk_numeral(k, s2->get_sort()); // t1 - s1 = k eq = m.mk_eq(s2.get(), t2.get()); if (m.has_trace_stream()) { @@ -1370,7 +1370,7 @@ expr_ref theory_diff_logic::mk_ineq(theory_var v, inf_eps const& val, bool } inf_eps new_val = val; // - inf_rational(m_objective_consts[v]); - e = m_util.mk_numeral(new_val.get_rational(), m.get_sort(f)); + e = m_util.mk_numeral(new_val.get_rational(), f->get_sort()); if (new_val.get_infinitesimal().is_neg()) { if (is_strict) { diff --git a/src/smt/theory_dl.cpp b/src/smt/theory_dl.cpp index 0d4b89f35..6dd84f95d 100644 --- a/src/smt/theory_dl.cpp +++ b/src/smt/theory_dl.cpp @@ -80,7 +80,7 @@ namespace smt { smt::context& ctx = m_th.get_context(); app* result = nullptr; expr* n = m_node->get_owner(); - sort* s = m_th.m().get_sort(n); + sort* s = n->get_sort(); func_decl* r, *v; m_th.get_rep(s, r, v); app_ref rep_of(m_th.m()); @@ -175,7 +175,7 @@ namespace smt { void relevant_eh(app * n) override { if (u().is_finite_sort(n)) { - sort* s = m().get_sort(n); + sort* s = n->get_sort(); func_decl* r, *v; get_rep(s, r, v); @@ -247,7 +247,7 @@ namespace smt { } void mk_lt(app* x, app* y) { - sort* s = m().get_sort(x); + sort* s = x->get_sort(); func_decl* r, *v; get_rep(s, r, v); app_ref lt(m()), le(m()); diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 701161a5f..38d06f532 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -564,8 +564,8 @@ namespace smt { a0 = to_app(owner->get_arg(0)); a1 = to_app(owner->get_arg(1)); a2 = to_app(owner->get_arg(2)); - unsigned ebits = m_fpa_util.get_ebits(m.get_sort(owner)); - unsigned sbits = m_fpa_util.get_sbits(m.get_sort(owner)); + unsigned ebits = m_fpa_util.get_ebits(owner->get_sort()); + unsigned sbits = m_fpa_util.get_sbits(owner->get_sort()); fpa_value_proc * vp = alloc(fpa_value_proc, this, ebits, sbits); vp->add_dependency(ctx.get_enode(a0)); vp->add_dependency(ctx.get_enode(a1)); @@ -593,8 +593,8 @@ namespace smt { res = vp; } else if (m_fpa_util.is_float(owner)) { - unsigned ebits = m_fpa_util.get_ebits(m.get_sort(owner)); - unsigned sbits = m_fpa_util.get_sbits(m.get_sort(owner)); + unsigned ebits = m_fpa_util.get_ebits(owner->get_sort()); + unsigned sbits = m_fpa_util.get_sbits(owner->get_sort()); fpa_value_proc * vp = alloc(fpa_value_proc, this, ebits, sbits); enode * en = ctx.get_enode(wrapped); vp->add_dependency(en); @@ -603,8 +603,8 @@ namespace smt { } } else { - unsigned ebits = m_fpa_util.get_ebits(m.get_sort(owner)); - unsigned sbits = m_fpa_util.get_sbits(m.get_sort(owner)); + unsigned ebits = m_fpa_util.get_ebits(owner->get_sort()); + unsigned sbits = m_fpa_util.get_sbits(owner->get_sort()); return alloc(expr_wrapper_proc, m_fpa_util.mk_pzero(ebits, sbits)); } diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 36811fbbe..f160e5e8a 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2295,7 +2295,7 @@ public: return; expr* e1 = n1->get_owner(); expr* e2 = n2->get_owner(); - if (e1->get_sort() != m.get_sort(e2)) + if (e1->get_sort() != e2->get_sort()) return; if (m.is_ite(e1) || m.is_ite(e2)) return; @@ -3296,7 +3296,7 @@ public: TRACE("arith", tout << mk_pp(o, m) << " v" << v << " := " << r << "\n";); SASSERT("integer variables should have integer values: " && (!a.is_int(o) || r.is_int() || m.limit().is_canceled())); if (a.is_int(o) && !r.is_int()) r = floor(r); - return alloc(expr_wrapper_proc, m_factory->mk_value(r, m.get_sort(o))); + return alloc(expr_wrapper_proc, m_factory->mk_value(r, o->get_sort())); } } @@ -3507,18 +3507,18 @@ public: expr* obj = get_enode(v)->get_owner(); rational r = val.x; expr_ref e(m); - if (a.is_int(m.get_sort(obj))) { + if (a.is_int(obj->get_sort())) { if (r.is_int()) { r += rational::one(); } else { r = ceil(r); } - e = a.mk_numeral(r, m.get_sort(obj)); + e = a.mk_numeral(r, obj->get_sort()); e = a.mk_ge(obj, e); } else { - e = a.mk_numeral(r, m.get_sort(obj)); + e = a.mk_numeral(r, obj->get_sort()); if (val.y.is_neg()) { e = a.mk_ge(obj, e); } diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index d293aa45a..a13b0b440 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -566,7 +566,7 @@ bool theory_seq::check_extensionality() { for (theory_var v : seqs) { enode* n2 = get_enode(v); expr* o2 = n2->get_owner(); - if (m.get_sort(o1) != m.get_sort(o2)) { + if (o1->get_sort() != o2->get_sort()) { continue; } if (ctx.is_diseq(n1, n2) || m_exclude.contains(o1, o2)) { @@ -1773,7 +1773,7 @@ void theory_seq::init_model(expr_ref_vector const& es) { expr_ref s(m); if (!canonize(e, eqs, s)) s = e; if (is_var(s)) { - new_s = m_factory->get_fresh_value(m.get_sort(s)); + new_s = m_factory->get_fresh_value(s->get_sort()); m_rep.update(s, new_s, eqs); } } @@ -1993,7 +1993,7 @@ app* theory_seq::mk_value(app* e) { if (is_var(result)) { SASSERT(m_factory); expr_ref val(m); - val = m_factory->get_fresh_value(m.get_sort(result)); + val = m_factory->get_fresh_value(result->get_sort()); if (val) { result = val; } @@ -2013,7 +2013,7 @@ void theory_seq::validate_model(model& mdl) { for (auto const& eq : m_eqs) { expr_ref_vector ls = eq.ls(); expr_ref_vector rs = eq.rs(); - sort* srt = m.get_sort(ls.get(0)); + sort* srt = ls[0]->get_sort(); expr_ref l(m_util.str.mk_concat(ls, srt), m); expr_ref r(m_util.str.mk_concat(rs, srt), m); if (!mdl.are_equal(l, r)) { @@ -2719,7 +2719,7 @@ void theory_seq::ensure_nth(literal lit, expr* s, expr* idx) { s2 = tail; } elems.push_back(s2); - conc = mk_concat(elems, m.get_sort(s)); + conc = mk_concat(elems, s->get_sort()); propagate_eq(lit, s, conc, true); } diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 58b5bda1f..563efd230 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -477,11 +477,11 @@ namespace smt { bool reduce_length(unsigned i, unsigned j, bool front, expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* deps); expr_ref mk_empty(sort* s) { return expr_ref(m_util.str.mk_empty(s), m); } - expr_ref mk_concat(unsigned n, expr*const* es) { return expr_ref(m_util.str.mk_concat(n, es, m.get_sort(es[0])), m); } + expr_ref mk_concat(unsigned n, expr*const* es) { return expr_ref(m_util.str.mk_concat(n, es, es[0]->get_sort()), m); } expr_ref mk_concat(unsigned n, expr*const* es, sort* s) { return expr_ref(m_util.str.mk_concat(n, es, s), m); } expr_ref mk_concat(expr_ref_vector const& es, sort* s) { return mk_concat(es.size(), es.c_ptr(), s); } - expr_ref mk_concat(expr_ref_vector const& es) { SASSERT(!es.empty()); return expr_ref(m_util.str.mk_concat(es.size(), es.c_ptr(), m.get_sort(es[0])), m); } - expr_ref mk_concat(ptr_vector const& es) { SASSERT(!es.empty()); return mk_concat(es.size(), es.c_ptr(), m.get_sort(es[0])); } + expr_ref mk_concat(expr_ref_vector const& es) { SASSERT(!es.empty()); return expr_ref(m_util.str.mk_concat(es.size(), es.c_ptr(), es[0]->get_sort()), m); } + expr_ref mk_concat(ptr_vector const& es) { SASSERT(!es.empty()); return mk_concat(es.size(), es.c_ptr(), es[0]->get_sort()); } expr_ref mk_concat(expr* e1, expr* e2) { return expr_ref(m_util.str.mk_concat(e1, e2), m); } expr_ref mk_concat(expr* e1, expr* e2, expr* e3) { return expr_ref(m_util.str.mk_concat(e1, e2, e3), m); } bool solve_nqs(unsigned i); diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 19c7abb83..04b5c4608 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -979,7 +979,7 @@ namespace smt { TRACE("str", tout << "set up basic string axioms on " << mk_pp(str->get_owner(), m) << std::endl;); { - sort * a_sort = m.get_sort(str->get_owner()); + sort * a_sort = str->get_owner()->get_sort(); sort * str_sort = u.str.mk_string_sort(); if (a_sort != str_sort) { TRACE("str", tout << "WARNING: not setting up string axioms on non-string term " << mk_pp(str->get_owner(), m) << std::endl;); @@ -6545,8 +6545,8 @@ namespace smt { void theory_str::handle_equality(expr * lhs, expr * rhs) { ast_manager & m = get_manager(); // both terms must be of sort String - sort * lhs_sort = m.get_sort(lhs); - sort * rhs_sort = m.get_sort(rhs); + sort * lhs_sort = lhs->get_sort(); + sort * rhs_sort = rhs->get_sort(); sort * str_sort = u.str.mk_string_sort(); // Pick up new terms added during the search (e.g. recursive function expansion). @@ -6793,7 +6793,7 @@ namespace smt { // expression throughout the lifetime of theory_str m_trail.push_back(ex); - sort * ex_sort = m.get_sort(ex); + sort * ex_sort = ex->get_sort(); sort * str_sort = u.str.mk_string_sort(); sort * bool_sort = m.mk_bool_sort(); @@ -7123,7 +7123,7 @@ namespace smt { app * a = to_app(ex); if (a->get_num_args() == 0) { // we only care about string variables - sort * s = m.get_sort(ex); + sort * s = ex->get_sort(); sort * string_sort = u.str.mk_string_sort(); if (s != string_sort) { return; @@ -7339,7 +7339,7 @@ namespace smt { if (m.is_eq(argAst)) { TRACE("str", tout << "eq ast " << mk_pp(argAst, m) << " is between args of sort " - << m.get_sort(to_app(argAst)->get_arg(0))->get_name() + << to_app(argAst)->get_arg(0)->get_sort()->get_name() << std::endl;); classify_ast_by_type(argAst, varMap, concatMap, unrollMap); } @@ -8454,7 +8454,7 @@ namespace smt { for (std::set::iterator it = eqc_roots.begin(); it != eqc_roots.end(); ++it) { enode * e = *it; app * a = e->get_owner(); - if (!(m.get_sort(a) == u.str.mk_string_sort())) { + if (!(a->get_sort() == u.str.mk_string_sort())) { TRACE("str", tout << "EQC root " << mk_pp(a, m) << " not a string term; skipping" << std::endl;); } else { TRACE("str", tout << "EQC root " << mk_pp(a, m) << " is a string term. Checking this EQC" << std::endl;); @@ -8950,7 +8950,7 @@ namespace smt { model_value_proc * theory_str::mk_value(enode * n, model_generator & mg) { TRACE("str", tout << "mk_value for: " << mk_ismt2_pp(n->get_owner(), get_manager()) << - " (sort " << mk_ismt2_pp(get_manager().get_sort(n->get_owner()), get_manager()) << ")" << std::endl;); + " (sort " << mk_ismt2_pp(n->get_owner()->get_sort(), get_manager()) << ")" << std::endl;); ast_manager & m = get_manager(); app_ref owner(m); owner = n->get_owner(); @@ -9208,13 +9208,13 @@ namespace smt { ast_manager & m = get_manager(); // TRACE("str", tout << "ex " << mk_pp(ex, m) << " target " << target << " length " << length << " sublen " << mk_pp(sublen, m) << " extra " << mk_pp(extra, m) << std::endl;); - sort * ex_sort = m.get_sort(ex); + sort * ex_sort = ex->get_sort(); sort * str_sort = u.str.mk_string_sort(); if (ex_sort == str_sort) { if (is_app(ex)) { app * ap = to_app(ex); - if(u.str.is_concat(ap)){ + if(u.str.is_concat(ap)) { unsigned num_args = ap->get_num_args(); bool success = true; for (unsigned i = 0; i < num_args; i++) { diff --git a/src/smt/theory_str_mc.cpp b/src/smt/theory_str_mc.cpp index fc7941591..05060b5fe 100644 --- a/src/smt/theory_str_mc.cpp +++ b/src/smt/theory_str_mc.cpp @@ -958,14 +958,14 @@ namespace smt { } } // reduce string formulas only. ignore others - sort * fSort = m.get_sort(f); + sort * fSort = f->get_sort(); if (fSort == bool_sort && !is_quantifier(f)) { // extracted terms expr * subterm; expr * lhs; expr * rhs; if (m.is_eq(f, lhs, rhs)) { - sort * lhs_sort = m.get_sort(lhs); + sort * lhs_sort = lhs->get_sort(); if (lhs_sort == str_sort) { TRACE("str_fl", tout << "reduce string equality: " << mk_pp(lhs, m) << " == " << mk_pp(rhs, m) << std::endl;); expr_ref cex(m); @@ -1031,7 +1031,7 @@ namespace smt { }else if (m.is_not(f, subterm)) { // if subterm is a string formula such as an equality, reduce it as a disequality if (m.is_eq(subterm, lhs, rhs)) { - sort * lhs_sort = m.get_sort(lhs); + sort * lhs_sort = lhs->get_sort(); if (lhs_sort == str_sort) { TRACE("str_fl", tout << "reduce string disequality: " << mk_pp(lhs, m) << " != " << mk_pp(rhs, m) << std::endl;); expr_ref cex(m); diff --git a/src/smt/theory_utvpi_def.h b/src/smt/theory_utvpi_def.h index 27fe14da5..954ad4a51 100644 --- a/src/smt/theory_utvpi_def.h +++ b/src/smt/theory_utvpi_def.h @@ -173,7 +173,7 @@ namespace smt { app* s1 = get_enode(s)->get_owner(); app* t1 = get_enode(t)->get_owner(); s2 = a.mk_sub(t1, s1); - t2 = a.mk_numeral(k, m.get_sort(s2.get())); + t2 = a.mk_numeral(k, s2->get_sort()); eq = m.mk_eq(s2.get(), t2.get()); TRACE("utvpi", tout << v1 << " .. " << v2 << "\n" << eq << "\n";); diff --git a/src/solver/solver.h b/src/solver/solver.h index 0ab8be126..9db168281 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -111,6 +111,8 @@ public: for (expr* e : ts) assert_expr(e); } +// void set_phase(expr* e) = 0; + void assert_expr(ptr_vector const& ts) { for (expr* e : ts) assert_expr(e); } diff --git a/src/tactic/bv/bit_blaster_model_converter.cpp b/src/tactic/bv/bit_blaster_model_converter.cpp index be6ea8b7a..e49b7f003 100644 --- a/src/tactic/bv/bit_blaster_model_converter.cpp +++ b/src/tactic/bv/bit_blaster_model_converter.cpp @@ -65,7 +65,7 @@ struct bit_blaster_model_converter : public model_converter { for (unsigned j = 0; j < num_args; j++) { expr * bit = to_app(bs)->get_arg(j); SASSERT(!TO_BOOL || m().is_bool(bit)); - SASSERT(TO_BOOL || is_sort_of(m().get_sort(bit), m().get_family_id("bv"), BV_SORT)); + SASSERT(TO_BOOL || is_sort_of(bit->get_sort(), m().get_family_id("bv"), BV_SORT)); SASSERT(is_uninterp_const(bit)); bits.insert(to_app(bit)->get_decl()); } diff --git a/src/tactic/core/injectivity_tactic.cpp b/src/tactic/core/injectivity_tactic.cpp index 0268179b5..82e78d771 100644 --- a/src/tactic/core/injectivity_tactic.cpp +++ b/src/tactic/core/injectivity_tactic.cpp @@ -207,7 +207,7 @@ class injectivity_tactic : public tactic { if (!inj_map.contains(a->get_decl())) return BR_FAILED; - SASSERT(m().get_sort(a->get_arg(0)) == m().get_sort(b->get_arg(0))); + SASSERT(a->get_arg(0)->get_sort() == b->get_arg(0)->get_sort()); TRACE("injectivity", tout << "Rewriting (= " << mk_ismt2_pp(args[0], m()) << " " << mk_ismt2_pp(args[1], m()) << ")" << std::endl;); result = m().mk_eq(a->get_arg(0), b->get_arg(0)); diff --git a/src/tactic/fd_solver/smtfd_solver.cpp b/src/tactic/fd_solver/smtfd_solver.cpp index 3f59e1107..04a4a4da7 100644 --- a/src/tactic/fd_solver/smtfd_solver.cpp +++ b/src/tactic/fd_solver/smtfd_solver.cpp @@ -1736,7 +1736,7 @@ namespace smtfd { for (expr* a : subterms(terms)) { expr_ref val0 = (*m_model)(a); expr_ref val1 = (*m_model)(abs(a)); - if (is_ground(a) && val0 != val1 && m.get_sort(val0) == m.get_sort(val1)) { + if (is_ground(a) && val0 != val1 && val0->get_sort() == val1->get_sort()) { tout << mk_bounded_pp(a, m, 2) << " := " << val0 << " " << val1 << "\n"; } if (!is_forall(a) && !is_exists(a) && (!m_context.term_covered(a) || !m_context.sort_covered(a->get_sort()))) { @@ -1753,7 +1753,7 @@ namespace smtfd { for (expr* a : subterms(core)) { expr_ref val0 = (*m_model)(a); expr_ref val1 = (*m_model)(abs(a)); - if (is_ground(a) && val0 != val1 && m.get_sort(val0) == m.get_sort(val1)) { + if (is_ground(a) && val0 != val1 && val0->get_sort() == val1->get_sort()) { std::cout << mk_bounded_pp(a, m, 2) << " := " << val0 << " " << val1 << "\n"; found_bad = true; } diff --git a/src/test/qe_arith.cpp b/src/test/qe_arith.cpp index 28733764f..ae8c09518 100644 --- a/src/test/qe_arith.cpp +++ b/src/test/qe_arith.cpp @@ -66,7 +66,7 @@ static void test(app* var, expr_ref& fml) { params.m_model = true; symbol x_name(var->get_decl()->get_name()); - sort* x_sort = m.get_sort(var); + sort* x_sort = var->get_sort(); expr_ref pr(m); expr_ref_vector lits(m); @@ -259,7 +259,7 @@ static void test2(char const *ex) { for (unsigned i = 0; i < vars.size(); ++i) { bound.push_back(vars[i].get()); names.push_back(vars[i]->get_decl()->get_name()); - sorts.push_back(m.get_sort(vars[i].get())); + sorts.push_back(vars[i]->get_sort()); } expr_abstract(m, 0, bound.size(), bound.c_ptr(), fml, fml2); fml2 = m.mk_exists(bound.size(), sorts.c_ptr(), names.c_ptr(), fml2);