From 3ae4c6e9de3a6475ca6801cae94243c84be0f8d1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 2 Feb 2021 04:45:54 -0800 Subject: [PATCH] refactor get_sort --- src/api/api_ast.cpp | 2 +- src/api/api_quant.cpp | 4 +- src/ast/arith_decl_plugin.cpp | 6 +- src/ast/ast.cpp | 34 +++--- src/ast/ast.h | 2 +- src/ast/ast_smt_pp.cpp | 10 +- src/ast/bv_decl_plugin.cpp | 6 +- src/ast/bv_decl_plugin.h | 2 +- src/ast/dl_decl_plugin.cpp | 4 +- src/ast/dl_decl_plugin.h | 2 +- src/ast/euf/euf_egraph.cpp | 2 +- src/ast/expr_abstract.cpp | 4 +- src/ast/fpa/bv2fpa_converter.cpp | 2 +- src/ast/fpa/fpa2bv_converter.cpp | 14 +-- src/ast/fpa/fpa2bv_rewriter.cpp | 2 +- src/ast/fpa_decl_plugin.h | 4 +- src/ast/macros/macro_util.cpp | 10 +- src/ast/normal_forms/defined_names.cpp | 2 +- src/ast/proofs/proof_checker.cpp | 4 +- src/ast/recfun_decl_plugin.cpp | 2 +- src/ast/rewriter/arith_rewriter.cpp | 10 +- src/ast/rewriter/array_rewriter.cpp | 8 +- src/ast/rewriter/expr_safe_replace.cpp | 2 +- src/ast/rewriter/factor_rewriter.cpp | 8 +- src/ast/rewriter/fpa_rewriter.cpp | 6 +- src/ast/rewriter/func_decl_replace.cpp | 2 +- src/ast/rewriter/inj_axiom.cpp | 2 +- src/ast/rewriter/mk_extract_proc.cpp | 2 +- src/ast/rewriter/mk_simplified_app.cpp | 2 +- src/ast/rewriter/poly_rewriter.h | 4 +- src/ast/rewriter/poly_rewriter_def.h | 12 +-- src/ast/rewriter/quant_hoist.cpp | 4 +- src/ast/rewriter/rewriter_def.h | 18 ++-- src/ast/rewriter/seq_rewriter.cpp | 102 +++++++++--------- src/ast/rewriter/seq_rewriter.h | 4 +- src/ast/rewriter/th_rewriter.cpp | 16 +-- src/ast/rewriter/value_sweep.cpp | 2 +- src/ast/static_features.cpp | 12 +-- src/ast/substitution/substitution_tree.cpp | 6 +- src/ast/well_sorted.cpp | 2 +- src/cmd_context/cmd_context.cpp | 10 +- src/model/datatype_factory.cpp | 2 +- src/model/func_interp.cpp | 8 +- src/model/model2expr.cpp | 2 +- src/model/model_evaluator.cpp | 6 +- src/model/model_implicant.cpp | 6 +- src/model/seq_factory.h | 2 +- src/model/struct_factory.cpp | 2 +- src/model/value_factory.h | 2 +- src/muz/base/bind_variables.cpp | 2 +- src/muz/base/dl_context.cpp | 6 +- src/muz/base/rule_properties.cpp | 4 +- src/muz/bmc/dl_bmc_engine.cpp | 4 +- src/muz/fp/datalog_parser.cpp | 4 +- src/muz/rel/dl_compiler.cpp | 2 +- src/muz/rel/dl_interval_relation.cpp | 2 +- src/muz/rel/dl_mk_simple_joins.cpp | 6 +- src/muz/rel/udoc_relation.cpp | 2 +- src/muz/spacer/spacer_legacy_mev.cpp | 4 +- src/muz/spacer/spacer_mev_array.cpp | 2 +- src/muz/spacer/spacer_qe_project.cpp | 6 +- src/muz/transforms/dl_mk_array_blast.cpp | 2 +- src/muz/transforms/dl_mk_bit_blast.cpp | 4 +- src/muz/transforms/dl_mk_coalesce.cpp | 4 +- src/muz/transforms/dl_mk_coi_filter.cpp | 2 +- .../dl_mk_quantifier_abstraction.cpp | 4 +- .../dl_mk_separate_negated_tails.cpp | 2 +- src/opt/opt_context.cpp | 2 +- src/parsers/smt2/smt2parser.cpp | 8 +- src/qe/mbp/mbp_arrays.cpp | 24 ++--- src/qe/mbp/mbp_datatypes.cpp | 4 +- src/qe/mbp/mbp_term_graph.cpp | 2 +- src/qe/qe.cpp | 6 +- src/qe/qe_datatype_plugin.cpp | 2 +- src/qe/qe_lite.cpp | 4 +- src/qe/qe_mbp.cpp | 2 +- src/qe/qsat.cpp | 2 +- src/sat/sat_solver/inc_sat_solver.cpp | 2 +- src/sat/smt/arith_solver.cpp | 2 +- src/sat/smt/array_axioms.cpp | 8 +- src/sat/smt/array_model.cpp | 2 +- src/sat/smt/bv_ackerman.cpp | 4 +- src/sat/smt/dt_solver.cpp | 12 +-- src/sat/smt/dt_solver.h | 2 +- src/sat/smt/euf_internalize.cpp | 14 +-- src/sat/smt/euf_model.cpp | 4 +- src/sat/smt/fpa_solver.cpp | 10 +- src/sat/smt/q_mbi.cpp | 8 +- src/sat/smt/q_solver.cpp | 2 +- src/shell/drat_frontend.cpp | 4 +- src/smt/proto_model/proto_model.cpp | 2 +- src/smt/seq_axioms.cpp | 6 +- src/smt/seq_eq_solver.cpp | 10 +- src/smt/seq_skolem.cpp | 4 +- src/smt/smt_arith_value.cpp | 6 +- src/smt/smt_consequences.cpp | 2 +- src/smt/smt_induction.cpp | 2 +- src/smt/smt_value_sort.cpp | 2 +- src/smt/tactic/ctx_solver_simplify_tactic.cpp | 2 +- src/smt/theory_array_base.cpp | 4 +- src/smt/theory_array_full.cpp | 2 +- src/smt/theory_bv.cpp | 4 +- src/smt/theory_char.cpp | 2 +- src/smt/theory_datatype.cpp | 4 +- src/smt/theory_dense_diff_logic_def.h | 2 +- src/smt/theory_fpa.cpp | 2 +- src/smt/theory_lra.cpp | 2 +- src/smt/theory_seq.cpp | 8 +- src/smt/theory_str.cpp | 4 +- src/solver/check_logic.cpp | 6 +- src/tactic/arith/bv2real_rewriter.cpp | 2 +- src/tactic/arith/fix_dl_var_tactic.cpp | 2 +- src/tactic/arith/fm_tactic.cpp | 2 +- src/tactic/arith/lia2pb_tactic.cpp | 2 +- src/tactic/arith/normalize_bounds_tactic.cpp | 2 +- src/tactic/arith/probe_arith.cpp | 6 +- src/tactic/bv/bv_size_reduction_tactic.cpp | 4 +- src/tactic/bv/bvarray2uf_rewriter.cpp | 6 +- src/tactic/core/elim_uncnstr_tactic.cpp | 22 ++-- src/tactic/core/reduce_invertible_tactic.cpp | 4 +- src/tactic/fd_solver/smtfd_solver.cpp | 6 +- src/tactic/generic_model_converter.cpp | 2 +- src/tactic/horn_subsume_model_converter.cpp | 2 +- src/tactic/model_converter.cpp | 2 +- src/tactic/probe.cpp | 2 +- src/tactic/sls/sls_evaluator.h | 2 +- src/test/egraph.cpp | 2 +- src/test/fuzzing/expr_rand.cpp | 2 +- src/test/quant_solve.cpp | 2 +- 129 files changed, 362 insertions(+), 362 deletions(-) diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 7d26e55ff..5aef93218 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -365,7 +365,7 @@ extern "C" { case AST_APP: { expr * e = to_expr(_a); // Real algebraic numbers are not considered Z3_NUMERAL_AST - if (is_numeral_sort(c, of_sort(mk_c(c)->m().get_sort(e))) && mk_c(c)->m().is_unique_value(e)) + if (is_numeral_sort(c, of_sort(e->get_sort())) && mk_c(c)->m().is_unique_value(e)) return Z3_NUMERAL_AST; return Z3_APP_AST; } diff --git a/src/api/api_quant.cpp b/src/api/api_quant.cpp index 1e764301b..77fd5db6c 100644 --- a/src/api/api_quant.cpp +++ b/src/api/api_quant.cpp @@ -185,7 +185,7 @@ extern "C" { app* a = to_app(vars[i]); _names.push_back(to_app(a)->get_decl()->get_name()); _args.push_back(a); - _vars.push_back(mk_c(c)->m().get_sort(a)); + _vars.push_back(a->get_sort()); } expr_ref result(mk_c(c)->m()); expr_abstract(mk_c(c)->m(), 0, num_decls, _args.c_ptr(), to_expr(body), result); @@ -232,7 +232,7 @@ extern "C" { } symbol s(to_app(a)->get_decl()->get_name()); names.push_back(of_symbol(s)); - types.push_back(of_sort(mk_c(c)->m().get_sort(a))); + types.push_back(of_sort(a->get_sort())); bound_asts.push_back(a); if (a->get_family_id() != null_family_id || a->get_num_args() != 0) { SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp index 2aca15420..854e05732 100644 --- a/src/ast/arith_decl_plugin.cpp +++ b/src/ast/arith_decl_plugin.cpp @@ -496,7 +496,7 @@ static bool has_real_arg(unsigned arity, sort * const * domain, sort * real_sort static bool has_real_arg(ast_manager * m, unsigned num_args, expr * const * args, sort * real_sort) { for (unsigned i = 0; i < num_args; i++) - if (m->get_sort(args[i]) == real_sort) + if (args[i]->get_sort() == real_sort) return true; return false; } @@ -543,7 +543,7 @@ func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters return nullptr; } if (k == OP_IDIVIDES) { - if (num_args != 1 || m_manager->get_sort(args[0]) != m_int_decl || num_parameters != 1 || !parameters[0].is_int()) { + if (num_args != 1 || args[0]->get_sort() != m_int_decl || num_parameters != 1 || !parameters[0].is_int()) { m_manager->raise_exception("invalid divides application. Expects integer parameter and one argument of sort integer"); } return m_manager->mk_func_decl(symbol("divisible"), 1, &m_int_decl, m_manager->mk_bool_sort(), @@ -553,7 +553,7 @@ func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters return mk_func_decl(fix_kind(k, num_args), has_real_arg(m_manager, num_args, args, m_real_decl)); } else { - bool is_real = num_args > 0 && m_manager->get_sort(args[0]) == m_real_decl; + bool is_real = num_args > 0 && args[0]->get_sort() == m_real_decl; return mk_func_decl(fix_kind(k, num_args), is_real); } } diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index fcdaac5a0..c9f0cc4c3 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -689,7 +689,7 @@ func_decl * decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, para unsigned num_args, expr * const * args, sort * range) { ptr_buffer sorts; for (unsigned i = 0; i < num_args; i++) { - sorts.push_back(m_manager->get_sort(args[i])); + sorts.push_back(args[i]->get_sort()); } return mk_func_decl(k, num_parameters, parameters, num_args, sorts.c_ptr(), range); } @@ -769,11 +769,11 @@ bool basic_decl_plugin::check_proof_args(basic_op_kind k, unsigned num_args, exp return false; else { for (unsigned i = 0; i < num_args - 1; i++) - if (m_manager->get_sort(args[i]) != m_proof_sort) + if (args[i]->get_sort() != m_proof_sort) return false; return - m_manager->get_sort(args[num_args - 1]) == m_bool_sort || - m_manager->get_sort(args[num_args - 1]) == m_proof_sort || + args[num_args - 1]->get_sort() == m_bool_sort || + args[num_args - 1]->get_sort() == m_proof_sort || is_lambda(args[num_args-1]); } } @@ -1098,11 +1098,11 @@ sort* basic_decl_plugin::join(unsigned n, sort* const* srts) { sort* basic_decl_plugin::join(unsigned n, expr* const* es) { SASSERT(n > 0); - sort* s = m_manager->get_sort(*es); + sort* s = es[0]->get_sort(); while (n > 1) { ++es; --n; - s = join(s, m_manager->get_sort(*es)); + s = join(s, (*es)->get_sort()); } return s; } @@ -1179,7 +1179,7 @@ func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters case OP_NOT: return m_not_decl; case OP_IMPLIES: return m_implies_decl; case OP_XOR: return m_xor_decl; - case OP_ITE: return num_args == 3 ? mk_ite_decl(join(m_manager->get_sort(args[1]), m_manager->get_sort(args[2]))): nullptr; + case OP_ITE: return num_args == 3 ? mk_ite_decl(join(args[1]->get_sort(), args[2]->get_sort())): nullptr; // eq and oeq must have at least two arguments, they can have more since they are chainable case OP_EQ: return num_args >= 2 ? mk_eq_decl_core("=", OP_EQ, join(num_args, args), m_eq_decls) : nullptr; case OP_OEQ: return num_args >= 2 ? mk_eq_decl_core("~", OP_OEQ, join(num_args, args), m_oeq_decls) : nullptr; @@ -1187,7 +1187,7 @@ func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters return decl_plugin::mk_func_decl(k, num_parameters, parameters, num_args, args, range); case PR_BIND: { ptr_buffer sorts; - for (unsigned i = 0; i < num_args; ++i) sorts.push_back(m_manager->get_sort(args[i])); + for (unsigned i = 0; i < num_args; ++i) sorts.push_back(args[i]->get_sort()); return mk_func_decl(k, num_parameters, parameters, num_args, sorts.c_ptr(), range); } default: @@ -1763,7 +1763,7 @@ void ast_manager::register_plugin(family_id id, decl_plugin * plugin) { } bool ast_manager::is_bool(expr const * n) const { - return get_sort(n) == m_bool_sort; + return n->get_sort() == m_bool_sort; } #ifdef Z3DEBUG @@ -2106,7 +2106,7 @@ void ast_manager::check_sort(func_decl const * decl, unsigned num_args, expr * c if (decl->is_associative()) { sort * expected = decl->get_domain(0); for (unsigned i = 0; i < num_args; i++) { - sort * given = get_sort(args[i]); + sort * given = args[i]->get_sort(); if (!compatible_sorts(expected, given)) { std::ostringstream buff; buff << "invalid function application for " << decl->get_name() << ", "; @@ -2122,7 +2122,7 @@ void ast_manager::check_sort(func_decl const * decl, unsigned num_args, expr * c } for (unsigned i = 0; i < num_args; i++) { sort * expected = decl->get_domain(i); - sort * given = get_sort(args[i]); + sort * given = args[i]->get_sort(); if (!compatible_sorts(expected, given)) { std::ostringstream buff; buff << "invalid function application for " << decl->get_name() << ", "; @@ -2186,7 +2186,7 @@ bool ast_manager::coercion_needed(func_decl * decl, unsigned num_args, expr * co sort * d = decl->get_domain(0); if (d->get_family_id() == m_arith_family_id) { for (unsigned i = 0; i < num_args; i++) { - if (d != get_sort(args[i])) + if (d != args[i]->get_sort()) return true; } } @@ -2199,7 +2199,7 @@ bool ast_manager::coercion_needed(func_decl * decl, unsigned num_args, expr * co } for (unsigned i = 0; i < num_args; i++) { sort * d = decl->get_domain(i); - if (d->get_family_id() == m_arith_family_id && d != get_sort(args[i])) + if (d->get_family_id() == m_arith_family_id && d != args[i]->get_sort()) return true; } } @@ -2207,7 +2207,7 @@ bool ast_manager::coercion_needed(func_decl * decl, unsigned num_args, expr * co } expr* ast_manager::coerce_to(expr* e, sort* s) { - sort* se = get_sort(e); + sort* se = e->get_sort(); if (s != se && s->get_family_id() == m_arith_family_id && se->get_family_id() == m_arith_family_id) { if (s->get_decl_kind() == REAL_SORT) { return mk_app(m_arith_family_id, OP_TO_REAL, e); @@ -2277,7 +2277,7 @@ app * ast_manager::mk_app_core(func_decl * decl, unsigned num_args, expr * const void ast_manager::check_args(func_decl* f, unsigned n, expr* const* es) { for (unsigned i = 0; i < n; i++) { - sort * actual_sort = get_sort(es[i]); + sort * actual_sort = es[i]->get_sort(); sort * expected_sort = f->is_associative() ? f->get_domain(0) : f->get_domain(i); if (expected_sort != actual_sort) { std::ostringstream buffer; @@ -2959,14 +2959,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)); - sort * s = get_sort(f1); + 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)); - sort * s = get_sort(f1); + 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 ab70f6694..0de63fe6b 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -2311,7 +2311,7 @@ public: bool has_fact(proof const * p) const { SASSERT(is_proof(p)); unsigned n = p->get_num_args(); - return n > 0 && get_sort(p->get_arg(n - 1)) != m_proof_sort; + return n > 0 && p->get_arg(n - 1)->get_sort() != m_proof_sort; } expr * get_fact(proof const * p) const { SASSERT(is_proof(p)); SASSERT(has_fact(p)); return p->get_arg(p->get_num_args() - 1); } diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp index 53e928597..dabf11d69 100644 --- a/src/ast/ast_smt_pp.cpp +++ b/src/ast/ast_smt_pp.cpp @@ -197,7 +197,7 @@ class smt_printer { } bool is_bool(expr* e) { - return is_bool(m_manager.get_sort(e)); + return is_bool(e->get_sort()); } bool is_proof(sort* s) { @@ -207,7 +207,7 @@ class smt_printer { } bool is_proof(expr* e) { - return is_proof(m_manager.get_sort(e)); + return is_proof(e->get_sort()); } void pp_id(expr* n) { @@ -450,11 +450,11 @@ class smt_printer { while (idx < args.size() && !args[idx]) idx++; if (idx >= args.size()) break; - sort * s = m_manager.get_sort(args[idx]); + sort * s = args[idx]->get_sort(); unsigned next = idx + 1; // check if there is only a single one - while (next < args.size() && (!args[next] || m_manager.get_sort(args[next]) != s)) + while (next < args.size() && (!args[next] || args[next]->get_sort() != s)) next++; if (next >= args.size()) { args[idx] = 0; @@ -465,7 +465,7 @@ class smt_printer { // otherwise print all of the relevant sort m_out << " (distinct"; for (unsigned i = idx; i < args.size(); ++i) { - if (args[i] && s == m_manager.get_sort(args[i])) { + if (args[i] && s == args[i]->get_sort()) { m_out << " "; pp_marked_expr(args[i]); args[i] = 0; diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index 672fa8b9c..369492b7f 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/src/ast/bv_decl_plugin.cpp @@ -350,7 +350,7 @@ inline bool bv_decl_plugin::get_bv_size(sort * s, int & result) { } inline bool bv_decl_plugin::get_bv_size(expr * t, int & result) { - return get_bv_size(m_manager->get_sort(t), result); + return get_bv_size(t->get_sort(), result); } bool bv_decl_plugin::get_concat_size(unsigned arity, sort * const * domain, int & result) { @@ -604,7 +604,7 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p if (r->get_info()->is_associative()) { sort * fs = r->get_domain(0); for (unsigned i = 0; i < num_args; ++i) { - if (m.get_sort(args[i]) != fs) { + if (args[i]->get_sort() != fs) { m_manager->raise_exception("declared sorts do not match supplied sorts"); return nullptr; } @@ -617,7 +617,7 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p } } for (unsigned i = 0; i < num_args; ++i) { - if (m.get_sort(args[i]) != r->get_domain(i)) { + if (args[i]->get_sort() != r->get_domain(i)) { std::ostringstream buffer; buffer << "Argument " << mk_pp(args[i], m) << " at position " << i << " does not match declaration " << mk_pp(r, m); m.raise_exception(buffer.str()); diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h index 98a34a376..62f7d246c 100644 --- a/src/ast/bv_decl_plugin.h +++ b/src/ast/bv_decl_plugin.h @@ -398,7 +398,7 @@ public: SASSERT(is_bv_sort(s)); return static_cast(s->get_parameter(0).get_int()); } - unsigned get_bv_size(expr const * n) const { return get_bv_size(m_manager.get_sort(n)); } + unsigned get_bv_size(expr const * n) const { return get_bv_size(n->get_sort()); } unsigned get_int2bv_size(parameter const& p); diff --git a/src/ast/dl_decl_plugin.cpp b/src/ast/dl_decl_plugin.cpp index 29a1e5d74..d133e78b6 100644 --- a/src/ast/dl_decl_plugin.cpp +++ b/src/ast/dl_decl_plugin.cpp @@ -297,7 +297,7 @@ namespace datalog { m_manager->raise_exception("illegal index"); return nullptr; } - if (sorts[idx] != m.get_sort(e)) { + if (sorts[idx] != e->get_sort()) { m_manager->raise_exception("sort mismatch in filter"); return nullptr; } @@ -766,7 +766,7 @@ namespace datalog { app* dl_decl_util::mk_rule(symbol const& name, unsigned num_args, expr* const* args) { ptr_buffer sorts; for (unsigned i = 0; i < num_args; ++i) { - sorts.push_back(m.get_sort(args[i])); + sorts.push_back(args[i]->get_sort()); } func_decl* f = m.mk_func_decl(name, num_args, sorts.c_ptr(), mk_rule_sort()); return m.mk_app(f, num_args, args); diff --git a/src/ast/dl_decl_plugin.h b/src/ast/dl_decl_plugin.h index bf1f88a77..39cdbf835 100644 --- a/src/ast/dl_decl_plugin.h +++ b/src/ast/dl_decl_plugin.h @@ -180,7 +180,7 @@ namespace datalog { } bool is_finite_sort(expr* e) const { - return is_finite_sort(m.get_sort(e)); + return is_finite_sort(e->get_sort()); } bool is_rule_sort(sort* s) const { diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp index eb393188c..088f4d2a6 100644 --- a/src/ast/euf/euf_egraph.cpp +++ b/src/ast/euf/euf_egraph.cpp @@ -560,7 +560,7 @@ namespace euf { return false; if (ra->interpreted() && rb->interpreted()) return true; - if (m.get_sort(ra->get_expr()) != m.get_sort(rb->get_expr())) + if (ra->get_expr()->get_sort() != rb->get_expr()->get_sort()) return true; expr_ref eq(m.mk_eq(a->get_expr(), b->get_expr()), m); m_tmp_eq->m_args[0] = a; diff --git a/src/ast/expr_abstract.cpp b/src/ast/expr_abstract.cpp index e9d7f9ada..801c570c2 100644 --- a/src/ast/expr_abstract.cpp +++ b/src/ast/expr_abstract.cpp @@ -34,7 +34,7 @@ void expr_abstractor::operator()(unsigned base, unsigned num_bound, expr* const* for (unsigned i = 0; i < num_bound; ++i) { b = bound[i]; - expr* v = m.mk_var(base + num_bound - i - 1, m.get_sort(b)); + expr* v = m.mk_var(base + num_bound - i - 1, b->get_sort()); m_pinned.push_back(v); m_map.insert(b, v); } @@ -122,7 +122,7 @@ expr_ref mk_quantifier(quantifier_kind k, ast_manager& m, unsigned num_bound, ap ptr_vector sorts; svector names; for (unsigned i = 0; i < num_bound; ++i) { - sorts.push_back(m.get_sort(bound[i])); + sorts.push_back(bound[i]->get_sort()); names.push_back(bound[i]->get_decl()->get_name()); } result = m.mk_quantifier(k, num_bound, sorts.c_ptr(), names.c_ptr(), result); diff --git a/src/ast/fpa/bv2fpa_converter.cpp b/src/ast/fpa/bv2fpa_converter.cpp index 3e05fedcc..90bd42374 100644 --- a/src/ast/fpa/bv2fpa_converter.cpp +++ b/src/ast/fpa/bv2fpa_converter.cpp @@ -217,7 +217,7 @@ expr_ref bv2fpa_converter::rebuild_floats(model_core * mc, sort * s, expr * e) { app * a = to_app(e); expr_ref_vector new_args(m); for (expr* arg : *a) { - new_args.push_back(rebuild_floats(mc, m.get_sort(arg), arg)); + new_args.push_back(rebuild_floats(mc, arg->get_sort(), arg)); } result = m.mk_app(a->get_decl(), new_args.size(), new_args.c_ptr()); } diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 39154cce9..d16daa22d 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -2475,8 +2475,8 @@ void fpa2bv_converter::mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr * } void fpa2bv_converter::mk_to_fp_float(sort * to_srt, expr * rm, expr * x, expr_ref & result) { - unsigned from_sbits = m_util.get_sbits(m.get_sort(x)); - unsigned from_ebits = m_util.get_ebits(m.get_sort(x)); + unsigned from_sbits = m_util.get_sbits(x->get_sort()); + unsigned from_ebits = m_util.get_ebits(x->get_sort()); unsigned to_sbits = m_util.get_sbits(to_srt); unsigned to_ebits = m_util.get_ebits(to_srt); @@ -2844,7 +2844,7 @@ void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * ar SASSERT(is_app_of(args[0], m_plugin->get_family_id(), OP_FPA_FP)); expr * x = args[0]; - sort * s = m.get_sort(x); + sort * s = x->get_sort(); unsigned ebits = m_util.get_ebits(s); unsigned sbits = m_util.get_sbits(s); @@ -3252,7 +3252,7 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args expr * rm = to_app(args[0])->get_arg(0); expr * x = args[1]; - sort * xs = m.get_sort(x); + sort * xs = x->get_sort(); sort * bv_srt = f->get_range(); expr_ref sgn(m), sig(m), exp(m), lz(m); @@ -3421,7 +3421,7 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg expr_ref fpa2bv_converter::nan_wrap(expr * n) { expr_ref n_bv(m), arg_is_nan(m), nan(m), nan_bv(m), res(m); mk_is_nan(n, arg_is_nan); - mk_nan(m.get_sort(n), nan); + mk_nan(n->get_sort(), nan); join_fp(nan, nan_bv); join_fp(n, n_bv); res = expr_ref(m.mk_ite(arg_is_nan, nan_bv, n_bv), m); @@ -3845,7 +3845,7 @@ void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) { } else { expr_ref new_e(m), new_e_eq_e(m); - new_e = m.mk_fresh_const(prefix, m.get_sort(e)); + new_e = m.mk_fresh_const(prefix, e->get_sort()); new_e_eq_e = m.mk_eq(new_e, e); m_extra_assertions.push_back(new_e_eq_e); e = new_e; @@ -4279,7 +4279,7 @@ app_ref fpa2bv_converter_wrapped::wrap(expr* e) { res = to_app(tmp); } else { - sort* es = m.get_sort(e); + sort* es = e->get_sort(); sort_ref bv_srt(m); if (is_rm(es)) diff --git a/src/ast/fpa/fpa2bv_rewriter.cpp b/src/ast/fpa/fpa2bv_rewriter.cpp index d4d61c5e1..24a2be2d1 100644 --- a/src/ast/fpa/fpa2bv_rewriter.cpp +++ b/src/ast/fpa/fpa2bv_rewriter.cpp @@ -73,7 +73,7 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co SASSERT(num == 2); TRACE("fpa2bv_rw", tout << "(= " << mk_ismt2_pp(args[0], m()) << " " << mk_ismt2_pp(args[1], m()) << ")" << std::endl;); - SASSERT(m().get_sort(args[0]) == m().get_sort(args[1])); + SASSERT(args[0]->get_sort() == args[1]->get_sort()); sort * ds = f->get_domain()[0]; if (m_conv.is_float(ds)) { m_conv.mk_eq(args[0], args[1], result); diff --git a/src/ast/fpa_decl_plugin.h b/src/ast/fpa_decl_plugin.h index ac6acb325..1cbe9fc4b 100644 --- a/src/ast/fpa_decl_plugin.h +++ b/src/ast/fpa_decl_plugin.h @@ -223,8 +223,8 @@ public: sort * mk_rm_sort() { return m().mk_sort(m_fid, ROUNDING_MODE_SORT); } bool is_float(sort * s) const { return is_sort_of(s, m_fid, FLOATING_POINT_SORT); } bool is_rm(sort * s) const { return is_sort_of(s, m_fid, ROUNDING_MODE_SORT); } - bool is_float(expr * e) const { return is_float(m_manager.get_sort(e)); } - bool is_rm(expr * e) const { return is_rm(m_manager.get_sort(e)); } + bool is_float(expr * e) const { return is_float(e->get_sort()); } + bool is_rm(expr * e) const { return is_rm(e->get_sort()); } bool is_fp(expr const * e) const { return is_app_of(e, m_fid, OP_FPA_FP); } unsigned get_ebits(sort * s) const; unsigned get_sbits(sort * s) const; diff --git a/src/ast/macros/macro_util.cpp b/src/ast/macros/macro_util.cpp index 07a547e18..6ab75453e 100644 --- a/src/ast/macros/macro_util.cpp +++ b/src/ast/macros/macro_util.cpp @@ -307,7 +307,7 @@ bool macro_util::is_pseudo_head(expr * n, unsigned num_decls, app_ref & head, ap return false; if (!is_ground(lhs) && !is_ground(rhs)) return false; - sort * s = m_manager.get_sort(lhs); + sort * s = lhs->get_sort(); if (m_manager.is_uninterp(s)) return false; sort_size sz = s->get_num_elements(); @@ -448,7 +448,7 @@ void macro_util::quasi_macro_head_to_macro_head(app * qhead, unsigned & num_decl continue; } } - var * new_var = m_manager.mk_var(next_var_idx, m_manager.get_sort(arg)); + var * new_var = m_manager.mk_var(next_var_idx, arg->get_sort()); next_var_idx++; expr * new_cond = m_manager.mk_eq(new_var, arg); new_args.push_back(new_var); @@ -609,7 +609,7 @@ void hint_to_macro_head(ast_manager & m, app * head, unsigned & num_decls, app_r continue; } } - var * new_var = m.mk_var(next_var_idx, m.get_sort(arg)); + var * new_var = m.mk_var(next_var_idx, arg->get_sort()); next_var_idx++; new_args.push_back(new_var); } @@ -820,7 +820,7 @@ void macro_util::collect_arith_macro_candidates(expr * lhs, expr * rhs, expr * a if (_is_arith_macro || _is_poly_hint) { collect_poly_args(lhs, arg, args); expr_ref rest(m_manager); - mk_add(args.size(), args.c_ptr(), m_manager.get_sort(arg), rest); + mk_add(args.size(), args.c_ptr(), arg->get_sort(), rest); expr_ref def(m_manager); mk_sub(rhs, rest, def); // If is_poly_hint, rhs may contain variables that do not occur in to_app(arg). @@ -841,7 +841,7 @@ void macro_util::collect_arith_macro_candidates(expr * lhs, expr * rhs, expr * a if (_is_arith_macro || _is_poly_hint) { collect_poly_args(lhs, arg, args); expr_ref rest(m_manager); - mk_add(args.size(), args.c_ptr(), m_manager.get_sort(arg), rest); + mk_add(args.size(), args.c_ptr(), arg->get_sort(), rest); expr_ref def(m_manager); mk_sub(rest, rhs, def); // If is_poly_hint, rhs may contain variables that do not occur in to_app(neg_arg). diff --git a/src/ast/normal_forms/defined_names.cpp b/src/ast/normal_forms/defined_names.cpp index 1a5ffb4da..3156e94fa 100644 --- a/src/ast/normal_forms/defined_names.cpp +++ b/src/ast/normal_forms/defined_names.cpp @@ -119,7 +119,7 @@ app * defined_names::impl::gen_name(expr * e, sort_ref_buffer & var_sorts, buffe var_names.push_back(symbol(i)); } - sort * range = m.get_sort(e); + sort * range = e->get_sort(); func_decl * new_skolem_decl = m.mk_fresh_func_decl(m_z3name, symbol::null, domain.size(), domain.c_ptr(), range); app * n = m.mk_app(new_skolem_decl, new_args.size(), new_args.c_ptr()); if (is_lambda(e)) { diff --git a/src/ast/proofs/proof_checker.cpp b/src/ast/proofs/proof_checker.cpp index 5cf981ee2..e89dfa27f 100644 --- a/src/ast/proofs/proof_checker.cpp +++ b/src/ast/proofs/proof_checker.cpp @@ -1278,7 +1278,7 @@ bool proof_checker::check_arith_literal(bool is_pos, app* lit0, rational const& 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 = a.is_int(s); if (!is_int && a.is_int_expr(lit->get_arg(0))) { is_int = true; @@ -1425,7 +1425,7 @@ bool proof_checker::check_arith_proof(proof* p) { return false; } - sort* s = m.get_sort(sum); + sort* s = sum->get_sort(); if (is_strict) { diff --git a/src/ast/recfun_decl_plugin.cpp b/src/ast/recfun_decl_plugin.cpp index 87a09afb0..e63b50700 100644 --- a/src/ast/recfun_decl_plugin.cpp +++ b/src/ast/recfun_decl_plugin.cpp @@ -501,7 +501,7 @@ namespace recfun { } symbol fresh_name(m().mk_fresh_id()); - auto pd = mk_def(fresh_name, n, domain.c_ptr(), m().get_sort(max_expr)); + auto pd = mk_def(fresh_name, n, domain.c_ptr(), max_expr->get_sort()); func_decl* f = pd.get_def()->get_decl(); expr_ref new_body(m().mk_app(f, n, args.c_ptr()), m()); set_definition(subst, pd, n, vars, max_expr); diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index eb55c8877..8741d7965 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -342,7 +342,7 @@ br_status arith_rewriter::is_separated(expr* arg1, expr* arg2, op_kind kind, exp } SASSERT(r1 == r2); - expr_ref zero(m_util.mk_numeral(rational(0), m().get_sort(arg1)), m()); + expr_ref zero(m_util.mk_numeral(rational(0), arg1->get_sort()), m()); if (r1.is_zero() && m_util.is_mul(arg1)) { expr_ref_buffer eqs(m()); @@ -931,7 +931,7 @@ br_status arith_rewriter::mk_div_core(expr * arg1, expr * arg2, expr_ref & resul if (m_util.is_irrational_algebraic_numeral(arg2) && m_util.is_numeral(arg1)) return mk_div_rat_irrat(arg1, arg2, result); } - set_curr_sort(m().get_sort(arg1)); + set_curr_sort(arg1->get_sort()); numeral v1, v2; bool is_int; if (m_util.is_numeral(arg2, v2, is_int)) { @@ -992,7 +992,7 @@ br_status arith_rewriter::mk_idivides(unsigned k, expr * arg, expr_ref & result) } br_status arith_rewriter::mk_idiv_core(expr * arg1, expr * arg2, expr_ref & result) { - set_curr_sort(m().get_sort(arg1)); + set_curr_sort(arg1->get_sort()); numeral v1, v2; bool is_int; if (m_util.is_numeral(arg1, v1, is_int) && m_util.is_numeral(arg2, v2, is_int) && !v2.is_zero()) { @@ -1142,7 +1142,7 @@ static rational symmod(rational const& a, rational const& b) { } br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & result) { - set_curr_sort(m().get_sort(arg1)); + set_curr_sort(arg1->get_sort()); numeral v1, v2; bool is_int; if (m_util.is_numeral(arg1, v1, is_int) && m_util.is_numeral(arg2, v2, is_int) && !v2.is_zero()) { @@ -1203,7 +1203,7 @@ br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & resul } br_status arith_rewriter::mk_rem_core(expr * arg1, expr * arg2, expr_ref & result) { - set_curr_sort(m().get_sort(arg1)); + set_curr_sort(arg1->get_sort()); numeral v1, v2; bool is_int; if (m_util.is_numeral(arg1, v1, is_int) && m_util.is_numeral(arg2, v2, is_int) && !v2.is_zero()) { diff --git a/src/ast/rewriter/array_rewriter.cpp b/src/ast/rewriter/array_rewriter.cpp index 15c7bcfc9..a85f8a430 100644 --- a/src/ast/rewriter/array_rewriter.cpp +++ b/src/ast/rewriter/array_rewriter.cpp @@ -267,7 +267,7 @@ br_status array_rewriter::mk_select_core(unsigned num_args, expr * const * args, } sort_ref array_rewriter::get_map_array_sort(func_decl* f, unsigned num_args, expr* const* args) { - sort* s0 = m().get_sort(args[0]); + sort* s0 = args[0]->get_sort(); unsigned sz = get_array_arity(s0); ptr_vector domain; for (unsigned i = 0; i < sz; ++i) domain.push_back(get_array_domain(s0, i)); @@ -533,7 +533,7 @@ br_status array_rewriter::mk_set_difference(expr * arg1, expr * arg2, expr_ref & br_status array_rewriter::mk_set_subset(expr * arg1, expr * arg2, expr_ref & result) { mk_set_difference(arg1, arg2, result); - result = m().mk_eq(result.get(), m_util.mk_empty_set(m().get_sort(arg1))); + result = m().mk_eq(result.get(), m_util.mk_empty_set(arg1->get_sort())); return BR_REWRITE3; } @@ -654,7 +654,7 @@ bool array_rewriter::is_expandable_store(expr* s) { } expr_ref array_rewriter::expand_store(expr* s) { - sort* srt = m().get_sort(s); + sort* srt = s->get_sort(); unsigned arity = get_array_arity(srt); ptr_vector stores; expr_ref result(m()), tmp(m()); @@ -784,7 +784,7 @@ br_status array_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) return false; }; if (m_util.is_const(lhs1, v) && m_util.is_const(rhs1, w) && - has_large_domain(m().get_sort(lhs), std::max(num_lhs, num_rhs))) { + has_large_domain(lhs->get_sort(), std::max(num_lhs, num_rhs))) { mk_eq(lhs, lhs, rhs, fmls); mk_eq(rhs, lhs, rhs, fmls); fmls.push_back(m().mk_eq(v, w)); diff --git a/src/ast/rewriter/expr_safe_replace.cpp b/src/ast/rewriter/expr_safe_replace.cpp index 362384d2c..b3bb06e91 100644 --- a/src/ast/rewriter/expr_safe_replace.cpp +++ b/src/ast/rewriter/expr_safe_replace.cpp @@ -99,7 +99,7 @@ void expr_safe_replace::operator()(expr* e, expr_ref& res) { if (d) { m_args.push_back(d); arg_differs |= arg != d; - SASSERT(m.get_sort(arg) == m.get_sort(d)); + SASSERT(arg->get_sort() == m.get_sort(d)); } else { m_todo.push_back(arg); diff --git a/src/ast/rewriter/factor_rewriter.cpp b/src/ast/rewriter/factor_rewriter.cpp index 2a1c7217d..fe93d6253 100644 --- a/src/ast/rewriter/factor_rewriter.cpp +++ b/src/ast/rewriter/factor_rewriter.cpp @@ -60,7 +60,7 @@ br_status factor_rewriter::mk_eq(expr * arg1, expr * arg2, expr_ref & result) { expr_ref_vector eqs(m()); for(; it != end; ++it) { expr* e = it->m_key; - eqs.push_back(m().mk_eq(e, a().mk_numeral(rational(0), m().get_sort(e)))); + eqs.push_back(m().mk_eq(e, a().mk_numeral(rational(0), e->get_sort()))); } result = m().mk_or(eqs.size(), eqs.c_ptr()); return BR_DONE; @@ -126,7 +126,7 @@ void factor_rewriter::mk_is_negative(expr_ref& result, expr_ref_vector& eqs) { SASSERT(it != end); expr_ref neg0(m()), neg(m()), pos0(m()), pos(m()), tmp(m()); expr* e = it->m_key; - expr_ref zero(a().mk_numeral(rational(0), m().get_sort(e)), m()); + expr_ref zero(a().mk_numeral(rational(0), e->get_sort()), m()); expr_ref_vector conjs(m()); pos0 = m().mk_true(); neg0 = m().mk_false(); @@ -257,7 +257,7 @@ bool factor_rewriter::extract_factors() { m_factors.append(m_muls[0].size(), m_muls[0].c_ptr()); if (!m_adds[0].second) { bool found_numeral = false; - sort* s = m().get_sort(m_muls[0][0]); + sort* s = m_muls[0][0]->get_sort(); rational v; for (unsigned i = 0; !found_numeral && i < m_factors.size(); ++i) { if (a().is_numeral(m_factors[i].get(), v)) { @@ -301,7 +301,7 @@ bool factor_rewriter::extract_factors() { } SASSERT(m_muls.size() == m_adds.size()); expr_ref_vector trail(m()); - sort* s = m().get_sort(m_factors[0].get()); + sort* s = m_factors[0]->get_sort(); for (unsigned i = 0; i < m_adds.size(); ++i) { switch(m_muls[i].size()) { case 0: diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index fbc1a8e58..c53df0c41 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -313,12 +313,12 @@ br_status fpa_rewriter::mk_neg(expr * arg1, expr_ref & result) { } if (m_util.is_pinf(arg1)) { // - +oo --> -oo - result = m_util.mk_ninf(m().get_sort(arg1)); + result = m_util.mk_ninf(arg1->get_sort()); return BR_DONE; } if (m_util.is_ninf(arg1)) { // - -oo -> +oo - result = m_util.mk_pinf(m().get_sort(arg1)); + result = m_util.mk_pinf(arg1->get_sort()); return BR_DONE; } if (m_util.is_neg(arg1)) { @@ -476,7 +476,7 @@ br_status fpa_rewriter::mk_float_eq(expr * arg1, expr * arg2, expr_ref & result) // Return (= arg NaN) app * fpa_rewriter::mk_eq_nan(expr * arg) { - return m().mk_eq(arg, m_util.mk_nan(m().get_sort(arg))); + return m().mk_eq(arg, m_util.mk_nan(arg->get_sort())); } // Return (not (= arg NaN)) diff --git a/src/ast/rewriter/func_decl_replace.cpp b/src/ast/rewriter/func_decl_replace.cpp index 97451cb58..fa034ff6b 100644 --- a/src/ast/rewriter/func_decl_replace.cpp +++ b/src/ast/rewriter/func_decl_replace.cpp @@ -43,7 +43,7 @@ expr_ref func_decl_replace::operator()(expr* e) { if (m_cache.find(arg, d)) { m_args.push_back(d); arg_differs |= arg != d; - SASSERT(m.get_sort(arg) == m.get_sort(d)); + SASSERT(arg->get_sort() == m.get_sort(d)); } else { m_todo.push_back(arg); diff --git a/src/ast/rewriter/inj_axiom.cpp b/src/ast/rewriter/inj_axiom.cpp index 5fa60ad93..d24315d88 100644 --- a/src/ast/rewriter/inj_axiom.cpp +++ b/src/ast/rewriter/inj_axiom.cpp @@ -112,7 +112,7 @@ bool simplify_inj_axiom(ast_manager & m, quantifier * q, expr_ref & result) { ptr_vector domain; inv_vars.push_back(f); for (unsigned i = 0; i < inv_vars.size(); ++i) { - domain.push_back(m.get_sort(inv_vars[i])); + domain.push_back(inv_vars[i]->get_sort()); } sort * d = decl->get_domain(idx); func_decl * inv_decl = m.mk_fresh_func_decl("inj", domain.size(), domain.c_ptr(), d); diff --git a/src/ast/rewriter/mk_extract_proc.cpp b/src/ast/rewriter/mk_extract_proc.cpp index e245f3a3d..be61047a4 100644 --- a/src/ast/rewriter/mk_extract_proc.cpp +++ b/src/ast/rewriter/mk_extract_proc.cpp @@ -33,7 +33,7 @@ mk_extract_proc::~mk_extract_proc() { app * mk_extract_proc::operator()(unsigned high, unsigned low, expr * arg) { ast_manager & m = m_util.get_manager(); - sort * s = m.get_sort(arg); + sort * s = arg->get_sort(); if (m_low == low && m_high == high && m_domain == s) return m.mk_app(m_f_cached, arg); // m_f_cached has a reference to m_domain, so, I don't need to inc_ref m_domain diff --git a/src/ast/rewriter/mk_simplified_app.cpp b/src/ast/rewriter/mk_simplified_app.cpp index 9bf460aa9..9511adc9d 100644 --- a/src/ast/rewriter/mk_simplified_app.cpp +++ b/src/ast/rewriter/mk_simplified_app.cpp @@ -53,7 +53,7 @@ struct mk_simplified_app::imp { if (k == OP_EQ) { // theory dispatch for = SASSERT(num == 2); - family_id s_fid = m.get_sort(args[0])->get_family_id(); + family_id s_fid = args[0]->get_sort()->get_family_id(); if (s_fid == m_a_rw.get_fid()) st = m_a_rw.mk_eq_core(args[0], args[1], result); else if (s_fid == m_bv_rw.get_fid()) diff --git a/src/ast/rewriter/poly_rewriter.h b/src/ast/rewriter/poly_rewriter.h index 5f263ce1d..c505103bb 100644 --- a/src/ast/rewriter/poly_rewriter.h +++ b/src/ast/rewriter/poly_rewriter.h @@ -133,7 +133,7 @@ public: result = args[0]; return BR_DONE; } - set_curr_sort(m().get_sort(args[0])); + set_curr_sort(args[0]->get_sort()); return m_flat ? mk_flat_mul_core(num_args, args, result) : mk_nflat_mul_core(num_args, args, result); @@ -144,7 +144,7 @@ public: result = args[0]; return BR_DONE; } - set_curr_sort(m().get_sort(args[0])); + set_curr_sort(args[0]->get_sort()); return m_flat ? mk_flat_add_core(num_args, args, result) : mk_nflat_add_core(num_args, args, result); diff --git a/src/ast/rewriter/poly_rewriter_def.h b/src/ast/rewriter/poly_rewriter_def.h index fd95bb85a..0f2c2fc79 100644 --- a/src/ast/rewriter/poly_rewriter_def.h +++ b/src/ast/rewriter/poly_rewriter_def.h @@ -85,7 +85,7 @@ expr * poly_rewriter::mk_mul_app(unsigned num_args, expr * const * args) return args[0]; default: if (use_power()) { - sort* s = m().get_sort(args[0]); + sort* s = args[0]->get_sort(); rational k_prev; expr * prev = get_power_body(args[0], k_prev); rational k; @@ -668,7 +668,7 @@ br_status poly_rewriter::mk_nflat_add_core(unsigned num_args, expr * con template br_status poly_rewriter::mk_uminus(expr * arg, expr_ref & result) { numeral a; - set_curr_sort(m().get_sort(arg)); + set_curr_sort(arg->get_sort()); if (is_numeral(arg, a)) { a.neg(); normalize(a); @@ -688,7 +688,7 @@ br_status poly_rewriter::mk_sub(unsigned num_args, expr * const * args, result = args[0]; return BR_DONE; } - set_curr_sort(m().get_sort(args[0])); + set_curr_sort(args[0]->get_sort()); expr_ref minus_one(mk_numeral(numeral(-1)), m()); expr_ref_buffer new_args(m()); new_args.push_back(args[0]); @@ -708,7 +708,7 @@ br_status poly_rewriter::mk_sub(unsigned num_args, expr * const * args, */ template br_status poly_rewriter::cancel_monomials(expr * lhs, expr * rhs, bool move, expr_ref & lhs_result, expr_ref & rhs_result) { - set_curr_sort(m().get_sort(lhs)); + set_curr_sort(lhs->get_sort()); mon_lt lt(*this); unsigned lhs_sz; expr * const * lhs_monomials = get_monomials(lhs, lhs_sz); @@ -921,7 +921,7 @@ bool poly_rewriter::hoist_multiplication(expr_ref& som) { continue; } if (mul_map.find(e, j) && valid[j] && j != k) { - m_curr_sort = m().get_sort(adds[k]); + m_curr_sort = adds[k]->get_sort(); adds[j] = merge_muls(adds[j], adds[k]); adds[k] = mk_numeral(rational(0)); valid[j] = false; @@ -964,7 +964,7 @@ expr* poly_rewriter::merge_muls(expr* x, expr* y) { ++k; } } - m_curr_sort = m().get_sort(x); + m_curr_sort = x->get_sort(); SASSERT(k > 0); SASSERT(m1.size() >= k); SASSERT(m2.size() >= k); diff --git a/src/ast/rewriter/quant_hoist.cpp b/src/ast/rewriter/quant_hoist.cpp index b5cf57927..127b18a45 100644 --- a/src/ast/rewriter/quant_hoist.cpp +++ b/src/ast/rewriter/quant_hoist.cpp @@ -113,9 +113,9 @@ public: bound_names.push_back(v->get_decl()->get_name()); } if (sorts) { - bound_sorts.push_back(m.get_sort(v)); + bound_sorts.push_back(v->get_sort()); } - rep.insert(v, m.mk_var(index++, m.get_sort(v))); + rep.insert(v, m.mk_var(index++, v->get_sort())); } if (names && !bound_names.empty()) { bound_names.reverse(); diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h index 8e3845a3e..808d83cb3 100644 --- a/src/ast/rewriter/rewriter_def.h +++ b/src/ast/rewriter/rewriter_def.h @@ -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) != m().get_sort(t), - tout << mk_pp(m().get_sort(t), m()) << ": " << mk_pp(t, m()) << "\n"; + st != BR_FAILED && m().get_sort(m_r) != 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) == m().get_sort(t)); + SASSERT(st != BR_DONE || m().get_sort(m_r) == 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(m().get_sort(t) == m().get_sort(new_t)); + SASSERT(t->get_sort() == m().get_sort(new_t)); 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) == m().get_sort(t)); + SASSERT(m().get_sort(r) == 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) == m().get_sort(t)); + SASSERT(st != BR_DONE || m().get_sort(m_r) == t->get_sort()); if (st != BR_FAILED) { result_stack().shrink(fr.m_spos); - SASSERT(m().get_sort(m_r) == m().get_sort(t)); + SASSERT(m().get_sort(m_r) == 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) == m().get_sort(t)); + SASSERT(m().get_sort(def) == t->get_sort()); if (is_ground(def) && !m_cfg.reduce_macro()) { m_r = def; if (ProofGen) { @@ -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) == m().get_sort(t)); + SASSERT(m().get_sort(r) == 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 e7bb70da6..9d7187ab2 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -47,8 +47,8 @@ expr_ref sym_expr::accept(expr* e) { result = m.mk_not(result); break; case t_char: - SASSERT(m.get_sort(e) == m.get_sort(m_t)); - SASSERT(m.get_sort(e) == m_sort); + SASSERT(e->get_sort() == m.get_sort(m_t)); + SASSERT(e->get_sort() == m_sort); result = m.mk_eq(e, m_t); break; case t_range: @@ -214,7 +214,7 @@ public: if (x->is_not() && x->get_arg()->is_range() && u.is_const_char(x->get_arg()->get_lo(), lo) && 0 < lo) { return l_true; } - if (!m_var || m.get_sort(m_var) != x->get_sort()) { + if (!m_var || m_var->get_sort() != x->get_sort()) { m_var = m.mk_fresh_const("x", x->get_sort()); } expr_ref fml = x->accept(m_var); @@ -345,7 +345,7 @@ eautomaton* re2automaton::re2aut(expr* e) { else if (u.re.is_full_seq(e)) { expr_ref tt(m.mk_true(), m); sort *seq_s = nullptr, *char_s = nullptr; - VERIFY (u.is_re(m.get_sort(e), seq_s)); + VERIFY (u.is_re(e->get_sort(), seq_s)); VERIFY (u.is_seq(seq_s, char_s)); sym_expr* _true = sym_expr::mk_pred(tt, char_s); return eautomaton::mk_loop(sm, _true); @@ -353,7 +353,7 @@ eautomaton* re2automaton::re2aut(expr* e) { else if (u.re.is_full_char(e)) { expr_ref tt(m.mk_true(), m); sort *seq_s = nullptr, *char_s = nullptr; - VERIFY (u.is_re(m.get_sort(e), seq_s)); + VERIFY (u.is_re(e->get_sort(), seq_s)); VERIFY (u.is_seq(seq_s, char_s)); sym_expr* _true = sym_expr::mk_pred(tt, char_s); a = alloc(eautomaton, sm, _true); @@ -887,7 +887,7 @@ br_status seq_rewriter::lift_ites_throttled(func_decl* f, unsigned n, expr* cons bool seq_rewriter::lift_ites_filter(func_decl* f, expr* ite) { // do not lift ites from sequences over regexes // for example DO NOT lift to_re(ite(c, s, t)) to ite(c, to_re(s), to_re(t)) - if (u().is_re(f->get_range()) && u().is_seq(m().get_sort(ite))) + if (u().is_re(f->get_range()) && u().is_seq(ite->get_sort())) return false; // The following check is intended to avoid lifting cases such as // substring(s,0,ite(c,e1,e2)) ==> ite(c, substring(s,0,e1), substring(s,0,e2)) @@ -967,7 +967,7 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu bool constantPos = m_autil.is_numeral(b, pos); bool constantLen = m_autil.is_numeral(c, len); bool lengthPos = str().is_length(b) || m_autil.is_add(b); - sort* a_sort = m().get_sort(a); + sort* a_sort = a->get_sort(); sign sg; if (sign_is_determined(c, sg) && sg == sign_neg) { @@ -1009,7 +1009,7 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu expr_ref_vector as(m()), bs(m()); str().get_concat_units(a, as); if (as.empty()) { - result = str().mk_empty(m().get_sort(a)); + result = str().mk_empty(a->get_sort()); return BR_DONE; } @@ -1039,7 +1039,7 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu } if (i == 0) return BR_FAILED; expr_ref t1(m()), t2(m()); - t1 = str().mk_concat(m_lhs.size() - i, m_lhs.c_ptr() + i, m().get_sort(a)); + t1 = str().mk_concat(m_lhs.size() - i, m_lhs.c_ptr() + i, a->get_sort()); t2 = m_autil.mk_int(pos); for (expr* rhs : lens) { t2 = m_autil.mk_add(t2, str().mk_length(rhs)); @@ -1080,10 +1080,10 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu std::function is_unit = [&](expr *e) { return str().is_unit(e); }; if (_pos == 0 && as.forall(is_unit)) { - result = str().mk_empty(m().get_sort(a)); + result = str().mk_empty(a->get_sort()); for (unsigned i = 1; i <= as.size(); ++i) { result = m().mk_ite(m_autil.mk_ge(c, m_autil.mk_int(i)), - str().mk_concat(i, as.c_ptr(), m().get_sort(a)), + str().mk_concat(i, as.c_ptr(), a->get_sort()), result); } return BR_REWRITE_FULL; @@ -1093,7 +1093,7 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu } // (extract (++ (unit x) (unit y)) 3 c) = empty if (offset == as.size()) { - result = str().mk_empty(m().get_sort(a)); + result = str().mk_empty(a->get_sort()); return BR_DONE; } SASSERT(offset != 0 || _pos == 0); @@ -1104,11 +1104,11 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu unsigned i = offset; for (; i < as.size() && str().is_unit(as.get(i)) && i - offset < _len; ++i); if (i - offset == _len) { - result = str().mk_concat(_len, as.c_ptr() + offset, m().get_sort(a)); + result = str().mk_concat(_len, as.c_ptr() + offset, a->get_sort()); return BR_DONE; } if (i == as.size()) { - result = str().mk_concat(as.size() - offset, as.c_ptr() + offset, m().get_sort(as.get(0))); + result = str().mk_concat(as.size() - offset, as.c_ptr() + offset, as[0]->get_sort()); return BR_DONE; } } @@ -1117,7 +1117,7 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu } expr_ref pos1(m()); pos1 = m_autil.mk_sub(b, m_autil.mk_int(offset)); - result = str().mk_concat(as.size() - offset, as.c_ptr() + offset, m().get_sort(as.get(0))); + result = str().mk_concat(as.size() - offset, as.c_ptr() + offset, as[0]->get_sort()); result = str().mk_substr(result, pos1, c); return BR_REWRITE3; } @@ -1246,7 +1246,7 @@ br_status seq_rewriter::mk_seq_contains(expr* a, expr* b, expr_ref& result) { } if (offs > 0 || sz < as.size()) { SASSERT(sz > offs); - result = str().mk_contains(str().mk_concat(sz-offs, as.c_ptr()+offs, m().get_sort(a)), b); + result = str().mk_contains(str().mk_concat(sz-offs, as.c_ptr()+offs, a->get_sort()), b); return BR_REWRITE2; } @@ -1285,7 +1285,7 @@ br_status seq_rewriter::mk_seq_at(expr* a, expr* b, expr_ref& result) { zstring c; rational r; expr_ref_vector lens(m()); - sort* sort_a = m().get_sort(a); + sort* sort_a = a->get_sort(); if (!get_lengths(b, lens, r)) { return BR_FAILED; } @@ -1309,7 +1309,7 @@ br_status seq_rewriter::mk_seq_at(expr* a, expr* b, expr_ref& result) { str().get_concat_units(a, m_lhs); if (m_lhs.empty()) { - result = str().mk_empty(m().get_sort(a)); + result = str().mk_empty(a->get_sort()); return BR_DONE; } @@ -1441,7 +1441,7 @@ br_status seq_rewriter::mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result rational r; bool isc1 = str().is_string(a, s1); bool isc2 = str().is_string(b, s2); - sort* sort_a = m().get_sort(a); + sort* sort_a = a->get_sort(); if (isc1 && isc2 && m_autil.is_numeral(c, r) && r.is_unsigned()) { int idx = s1.indexofu(s2, r.get_unsigned()); @@ -1534,7 +1534,7 @@ br_status seq_rewriter::mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result break; } if (is_zero && !as.empty() && str().is_unit(as.get(0))) { - expr_ref a1(str().mk_concat(as.size() - 1, as.c_ptr() + 1, m().get_sort(as.get(0))), m()); + expr_ref a1(str().mk_concat(as.size() - 1, as.c_ptr() + 1, as[0]->get_sort()), m()); expr_ref b1(str().mk_index(a1, b, c), m()); result = m().mk_ite(str().mk_prefix(b, a), zero(), m().mk_ite(m_autil.mk_ge(b1, zero()), m_autil.mk_add(one(), b1), minus_one())); @@ -1589,7 +1589,7 @@ seq_rewriter::length_comparison seq_rewriter::compare_lengths(unsigned sza, expr br_status seq_rewriter::mk_seq_replace(expr* a, expr* b, expr* c, expr_ref& result) { zstring s1, s2, s3; - sort* sort_a = m().get_sort(a); + sort* sort_a = a->get_sort(); if (str().is_string(a, s1) && str().is_string(b, s2) && str().is_string(c, s3)) { result = str().mk_string(s1.replace(s2, s3)); @@ -1701,7 +1701,7 @@ br_status seq_rewriter::mk_seq_replace_all(expr* a, expr* b, expr* c, expr_ref& return BR_DONE; } if (a == b) { - result = m().mk_ite(str().mk_is_empty(b), str().mk_empty(m().get_sort(a)), c); + result = m().mk_ite(str().mk_is_empty(b), str().mk_empty(a->get_sort()), c); return BR_REWRITE1; } zstring s1, s2; @@ -1721,7 +1721,7 @@ br_status seq_rewriter::mk_seq_replace_all(expr* a, expr* b, expr* c, expr_ref& else strs.push_back(str().mk_unit(str().mk_char(s1, i))); } - result = str().mk_concat(strs, m().get_sort(a)); + result = str().mk_concat(strs, a->get_sort()); return BR_REWRITE_FULL; } return BR_FAILED; @@ -1741,7 +1741,7 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) { zstring s1, s2; bool isc1 = str().is_string(a, s1); bool isc2 = str().is_string(b, s2); - sort* sort_a = m().get_sort(a); + sort* sort_a = a->get_sort(); if (isc1 && isc2) { result = m().mk_bool_val(s1.prefixof(s2)); TRACE("seq", tout << result << "\n";); @@ -1856,7 +1856,7 @@ br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) { result = m().mk_true(); return BR_DONE; } - sort* sort_a = m().get_sort(a); + sort* sort_a = a->get_sort(); if (str().is_empty(a)) { result = m().mk_true(); return BR_DONE; @@ -2075,7 +2075,7 @@ br_status seq_rewriter::mk_str_stoi(expr* a, expr_ref& result) { // if tail < 0 then tail else // if stoi(head) >= 0 and then stoi(head)*10+tail else -1 expr_ref tail(str().mk_stoi(as.back()), m()); - expr_ref head(str().mk_concat(as.size() - 1, as.c_ptr(), m().get_sort(a)), m()); + expr_ref head(str().mk_concat(as.size() - 1, as.c_ptr(), a->get_sort()), m()); expr_ref stoi_head(str().mk_stoi(head), m()); result = m().mk_ite(m_autil.mk_ge(stoi_head, m_autil.mk_int(0)), m_autil.mk_add(m_autil.mk_mul(m_autil.mk_int(10), stoi_head), tail), @@ -2184,7 +2184,7 @@ bool seq_rewriter::get_head_tail(expr* s, expr_ref& head, expr_ref& tail) { zstring s1; if (str().is_unit(s, h)) { head = h; - tail = str().mk_empty(m().get_sort(s)); + tail = str().mk_empty(s->get_sort()); return true; } if (str().is_string(s, s1) && s1.length() > 0) { @@ -2206,7 +2206,7 @@ bool seq_rewriter::get_head_tail_reversed(expr* s, expr_ref& head, expr_ref& tai expr* h = nullptr, *t = nullptr; zstring s1; if (str().is_unit(s, t)) { - head = str().mk_empty(m().get_sort(s)); + head = str().mk_empty(s->get_sort()); tail = t; return true; } @@ -2254,7 +2254,7 @@ expr_ref seq_rewriter::re_and(expr* cond, expr* r) { expr_ref _cond(cond, m()), _r(r, m()); if (m().is_true(cond)) return expr_ref(r, m()); - expr* re_empty = re().mk_empty(m().get_sort(r)); + expr* re_empty = re().mk_empty(r->get_sort()); if (m().is_false(cond)) return expr_ref(re_empty, m()); return expr_ref(m().mk_ite(cond, r, re_empty), m()); @@ -2341,7 +2341,7 @@ expr_ref seq_rewriter::is_nullable_rec(expr* r) { } else { SASSERT(m_util.is_seq(r)); - result = m().mk_eq(str().mk_empty(m().get_sort(r)), r); + result = m().mk_eq(str().mk_empty(r->get_sort()), r); } return result; } @@ -2961,7 +2961,7 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) { VERIFY(m_util.is_seq(seq_sort, ele_sort)); SASSERT(ele_sort == m().get_sort(ele)); expr* r1 = nullptr, *r2 = nullptr, *p = nullptr; - auto mk_empty = [&]() { return expr_ref(re().mk_empty(m().get_sort(r)), m()); }; + auto mk_empty = [&]() { return expr_ref(re().mk_empty(r->get_sort()), m()); }; unsigned lo = 0, hi = 0; if (re().is_concat(r, r1, r2)) { expr_ref is_n = is_nullable(r1); @@ -3245,7 +3245,7 @@ bool seq_rewriter::rewrite_contains_pattern(expr* a, expr* b, expr_ref& result) return false; expr_ref_vector fmls(m()); - sort* rs = m().get_sort(b); + sort* rs = b->get_sort(); expr_ref full(re().mk_full_seq(rs), m()), prefix(m()), suffix(m()); fmls.push_back(re().mk_in_re(y, b)); prefix = full; @@ -3376,7 +3376,7 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) { for (unsigned i = 0; i < len; ++i) { args.push_back(str().mk_unit(str().mk_nth_i(a, m_autil.mk_int(i)))); } - expr_ref in_re(re().mk_in_re(str().mk_concat(args, m().get_sort(a)), b), m()); + expr_ref in_re(re().mk_in_re(str().mk_concat(args, a->get_sort()), b), m()); result = m().mk_and(len_lim, in_re); return BR_REWRITE_FULL; } @@ -3596,7 +3596,7 @@ br_status seq_rewriter::mk_re_union(expr* a, expr* b, expr_ref& result) { br_status st = mk_re_union0(a, b, result); if (st != BR_FAILED) return st; - auto mk_full = [&]() { return re().mk_full_seq(m().get_sort(a)); }; + auto mk_full = [&]() { return re().mk_full_seq(a->get_sort()); }; if (are_complements(a, b)) { result = mk_full(); return BR_DONE; @@ -3665,11 +3665,11 @@ br_status seq_rewriter::mk_re_complement(expr* a, expr_ref& result) { return BR_REWRITE2; } if (re().is_empty(a)) { - result = re().mk_full_seq(m().get_sort(a)); + result = re().mk_full_seq(a->get_sort()); return BR_DONE; } if (re().is_full_seq(a)) { - result = re().mk_empty(m().get_sort(a)); + result = re().mk_empty(a->get_sort()); return BR_DONE; } if (re().is_complement(a, e1)) { @@ -3719,7 +3719,7 @@ br_status seq_rewriter::mk_re_inter(expr* a, expr* b, expr_ref& result) { br_status st = mk_re_inter0(a, b, result); if (st != BR_FAILED) return st; - auto mk_empty = [&]() { return re().mk_empty(m().get_sort(a)); }; + auto mk_empty = [&]() { return re().mk_empty(a->get_sort()); }; if (are_complements(a, b)) { result = mk_empty(); return BR_DONE; @@ -3770,7 +3770,7 @@ br_status seq_rewriter::mk_re_inter(expr* a, expr* b, expr_ref& result) { std::swap(a, b); expr* s = nullptr; if (re().is_to_re(a, s)) { - result = m().mk_ite(re().mk_in_re(s, b), a, re().mk_empty(m().get_sort(a))); + result = m().mk_ite(re().mk_in_re(s, b), a, re().mk_empty(a->get_sort())); return BR_REWRITE2; } return BR_FAILED; @@ -3793,11 +3793,11 @@ br_status seq_rewriter::mk_re_loop(func_decl* f, unsigned num_args, expr* const* hi2 = np > 1 ? f->get_parameter(1).get_int() : lo2; // (loop a 0 0) = "" if (np == 2 && lo2 > hi2) { - result = re().mk_empty(m().get_sort(args[0])); + result = re().mk_empty(args[0]->get_sort()); return BR_DONE; } if (np == 2 && hi2 == 0) { - result = re().mk_to_re(str().mk_empty(re().to_seq(m().get_sort(args[0])))); + result = re().mk_to_re(str().mk_empty(re().to_seq(args[0]->get_sort()))); return BR_DONE; } // (loop (loop a lo) lo2) = (loop lo*lo2) @@ -3863,7 +3863,7 @@ br_status seq_rewriter::mk_re_star(expr* a, expr_ref& result) { return BR_DONE; } if (re().is_full_char(a)) { - result = re().mk_full_seq(m().get_sort(a)); + result = re().mk_full_seq(a->get_sort()); return BR_DONE; } if (re().is_empty(a)) { @@ -3902,7 +3902,7 @@ br_status seq_rewriter::mk_re_star(expr* a, expr_ref& result) { if (m().is_ite(a, c, b1, c1)) { if ((re().is_full_char(b1) || re().is_full_seq(b1)) && (re().is_full_char(c1) || re().is_full_seq(c1))) { - result = re().mk_full_seq(m().get_sort(b1)); + result = re().mk_full_seq(b1->get_sort()); return BR_REWRITE2; } @@ -4077,7 +4077,7 @@ br_status seq_rewriter::reduce_re_is_empty(expr* r, expr_ref& result) { expr* r1, *r2, *r3, *r4; zstring s1, s2; unsigned lo, hi; - auto eq_empty = [&](expr* r) { return m().mk_eq(r, re().mk_empty(m().get_sort(r))); }; + auto eq_empty = [&](expr* r) { return m().mk_eq(r, re().mk_empty(r->get_sort())); }; if (re().is_union(r, r1, r2)) { result = m().mk_and(eq_empty(r1), eq_empty(r2)); return BR_REWRITE2; @@ -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) == m().get_sort(a)); + SASSERT(m().get_sort(ch) == 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) == m().get_sort(a)); + SASSERT(m().get_sort(ch) == a->get_sort()); new_eqs.push_back(ch, a); ++head1; if (s.length() == 1) { @@ -4375,7 +4375,7 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_pair_vector& new_eqs, bo void seq_rewriter::add_seqs(expr_ref_vector const& ls, expr_ref_vector const& rs, expr_ref_pair_vector& eqs) { if (!ls.empty() || !rs.empty()) { - sort * s = m().get_sort(ls.empty() ? rs[0] : ls[0]); + sort * s = (ls.empty() ? rs[0] : ls[0])->get_sort(); eqs.push_back(str().mk_concat(ls, s), str().mk_concat(rs, s)); } } @@ -4385,7 +4385,7 @@ bool seq_rewriter::reduce_contains(expr* a, expr* b, expr_ref_vector& disj) { m_lhs.reset(); str().get_concat(a, m_lhs); TRACE("seq", tout << expr_ref(a, m()) << " " << expr_ref(b, m()) << "\n";); - sort* sort_a = m().get_sort(a); + sort* sort_a = a->get_sort(); zstring s; for (unsigned i = 0; i < m_lhs.size(); ++i) { expr* e = m_lhs.get(i); @@ -4411,7 +4411,7 @@ bool seq_rewriter::reduce_contains(expr* a, expr* b, expr_ref_vector& disj) { } if (str().is_string(b, s)) { - expr* all = re().mk_full_seq(re().mk_re(m().get_sort(b))); + expr* all = re().mk_full_seq(re().mk_re(b->get_sort())); disj.push_back(re().mk_in_re(str().mk_concat(m_lhs.size() - i, m_lhs.c_ptr() + i, sort_a), re().mk_concat(all, re().mk_concat(re().mk_to_re(b), all)))); return true; @@ -4429,7 +4429,7 @@ bool seq_rewriter::reduce_contains(expr* a, expr* b, expr_ref_vector& disj) { expr* seq_rewriter::concat_non_empty(expr_ref_vector& es) { - sort* s = m().get_sort(es.get(0)); + sort* s = es[0]->get_sort(); unsigned j = 0; for (expr* e : es) { if (str().is_unit(e) || str().is_string(e)) @@ -4462,7 +4462,7 @@ bool seq_rewriter::set_empty(unsigned sz, expr* const* es, bool all, expr_ref_pa } } else { - emp = emp?emp:str().mk_empty(m().get_sort(es[i])); + emp = emp?emp:str().mk_empty(es[i]->get_sort()); eqs.push_back(emp, es[i]); } } @@ -4652,7 +4652,7 @@ bool seq_rewriter::reduce_subsequence(expr_ref_vector& ls, expr_ref_vector& rs, rs.shrink(j); SASSERT(ls.size() == rs.size()); if (!ls.empty()) { - sort* srt = m().get_sort(ls.get(0)); + sort* srt = ls[0]->get_sort(); eqs.push_back(str().mk_concat(ls, srt), str().mk_concat(rs, srt)); ls.reset(); diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index fe40c0d5a..d55751400 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -55,10 +55,10 @@ class sym_expr { public: ~sym_expr() { if (m_expr) m_expr->dec_ref(); } expr_ref accept(expr* e); - static sym_expr* mk_char(expr_ref& t) { return alloc(sym_expr, t_char, t, t, t.get_manager().get_sort(t), nullptr); } + static sym_expr* mk_char(expr_ref& t) { return alloc(sym_expr, t_char, t, t, t->get_sort(), nullptr); } static sym_expr* mk_char(ast_manager& m, expr* t) { expr_ref tr(t, m); return mk_char(tr); } static sym_expr* mk_pred(expr_ref& t, sort* s) { return alloc(sym_expr, t_pred, t, t, s, nullptr); } - static sym_expr* mk_range(expr_ref& lo, expr_ref& hi) { return alloc(sym_expr, t_range, lo, hi, lo.get_manager().get_sort(hi), nullptr); } + static sym_expr* mk_range(expr_ref& lo, expr_ref& hi) { return alloc(sym_expr, t_range, lo, hi, hi->get_sort(), nullptr); } static sym_expr* mk_not(ast_manager& m, sym_expr* e) { expr_ref f(m); e->inc_ref(); return alloc(sym_expr, t_not, f, f, e->get_sort(), e); } void inc_ref() { ++m_ref; } void dec_ref() { --m_ref; if (m_ref == 0) dealloc(this); } diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index b4521a216..5a7f4bffc 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -175,7 +175,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { if (k == OP_EQ) { // theory dispatch for = SASSERT(num == 2); - family_id s_fid = m().get_sort(args[0])->get_family_id(); + family_id s_fid = args[0]->get_sort()->get_family_id(); if (s_fid == m_a_rw.get_fid()) st = m_a_rw.mk_eq_core(args[0], args[1], result); else if (s_fid == m_bv_rw.get_fid()) @@ -199,7 +199,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { } if (k == OP_ITE) { SASSERT(num == 3); - family_id s_fid = m().get_sort(args[1])->get_family_id(); + family_id s_fid = args[1]->get_sort()->get_family_id(); if (s_fid == m_bv_rw.get_fid()) st = m_bv_rw.mk_ite_core(args[0], args[1], args[2], result); if (st != BR_FAILED) @@ -348,16 +348,16 @@ struct th_rewriter_cfg : public default_rewriter_cfg { family_id fid = t->get_family_id(); if (fid == m_a_rw.get_fid()) { switch (t->get_decl_kind()) { - case OP_ADD: n = m_a_util.mk_numeral(rational::zero(), m().get_sort(t)); return true; - case OP_MUL: n = m_a_util.mk_numeral(rational::one(), m().get_sort(t)); return true; + case OP_ADD: n = m_a_util.mk_numeral(rational::zero(), t->get_sort()); return true; + case OP_MUL: n = m_a_util.mk_numeral(rational::one(), t->get_sort()); return true; default: return false; } } if (fid == m_bv_rw.get_fid()) { switch (t->get_decl_kind()) { - case OP_BADD: n = m_bv_util.mk_numeral(rational::zero(), m().get_sort(t)); return true; - case OP_BMUL: n = m_bv_util.mk_numeral(rational::one(), m().get_sort(t)); return true; + case OP_BADD: n = m_bv_util.mk_numeral(rational::zero(), t->get_sort()); return true; + case OP_BMUL: n = m_bv_util.mk_numeral(rational::one(), t->get_sort()); return true; default: return false; } @@ -588,11 +588,11 @@ struct th_rewriter_cfg : public default_rewriter_cfg { decl_kind k = f->get_decl_kind(); if (k == OP_EQ) { SASSERT(num == 2); - fid = m().get_sort(args[0])->get_family_id(); + fid = args[0]->get_sort()->get_family_id(); } else if (k == OP_ITE) { SASSERT(num == 3); - fid = m().get_sort(args[1])->get_family_id(); + fid = args[1]->get_sort()->get_family_id(); } } app_ref tmp(m()); diff --git a/src/ast/rewriter/value_sweep.cpp b/src/ast/rewriter/value_sweep.cpp index 9595fd308..e7dff58cb 100644 --- a/src/ast/rewriter/value_sweep.cpp +++ b/src/ast/rewriter/value_sweep.cpp @@ -69,7 +69,7 @@ bool value_sweep::assign_next_value() { ++m_vhead; if (!get_value(v)) { unsigned index = m_rand() % m_range; - expr_ref val = m_gen.get_value(m.get_sort(v), index); + expr_ref val = m_gen.get_value(v->get_sort(), index); set_value_core(v, val); m_queue.push_back(v); return true; diff --git a/src/ast/static_features.cpp b/src/ast/static_features.cpp index c0897d33e..517aaaef7 100644 --- a/src/ast/static_features.cpp +++ b/src/ast/static_features.cpp @@ -172,7 +172,7 @@ void static_features::update_core(expr * e) { // even if a benchmark does not contain any theory interpreted function decls, we still have to install // the theory if the benchmark contains constants or function applications of an interpreted sort. - sort * s = m.get_sort(e); + sort * s = e->get_sort(); if (!m.is_uninterp(s)) mark_theory(s->get_family_id()); @@ -193,7 +193,7 @@ void static_features::update_core(expr * e) { acc_num(arg); // Must check whether arg is diff logic or not. // Otherwise, problem can be incorrectly tagged as diff logic. - sort * arg_s = m.get_sort(arg); + sort * arg_s = arg->get_sort(); family_id fid_arg = arg_s->get_family_id(); if (fid_arg == m_afid) { m_num_arith_terms++; @@ -263,7 +263,7 @@ void static_features::update_core(expr * e) { if (!is_arith_expr(to_app(e)->get_arg(0))) m_num_simple_eqs++; } - sort * s = m.get_sort(to_app(e)->get_arg(0)); + sort * s = to_app(e)->get_arg(0)->get_sort(); if (!m.is_uninterp(s)) { family_id fid = s->get_family_id(); if (fid != null_family_id && fid != m_bfid) @@ -281,7 +281,7 @@ void static_features::update_core(expr * e) { if (is_app(e) && to_app(e)->get_family_id() == m_srfid) m_has_sr = true; if (!m_has_arrays && m_arrayutil.is_array(e)) - check_array(m.get_sort(e)); + check_array(e->get_sort()); if (!m_has_ext_arrays && m_arrayutil.is_array(e) && !m_arrayutil.is_select(e) && !m_arrayutil.is_store(e)) m_has_ext_arrays = true; @@ -323,7 +323,7 @@ void static_features::update_core(expr * e) { m_num_uninterpreted_exprs++; if (to_app(e)->get_num_args() == 0) { m_num_uninterpreted_constants++; - sort * s = m.get_sort(e); + sort * s = e->get_sort(); if (!m.is_uninterp(s)) { family_id fid = s->get_family_id(); if (fid != null_family_id && fid != m_bfid) @@ -350,7 +350,7 @@ void static_features::update_core(expr * e) { } if (!_is_eq && !_is_gate) { for (expr * arg : *to_app(e)) { - sort * arg_s = m.get_sort(arg); + sort * arg_s = arg->get_sort(); if (!m.is_uninterp(arg_s)) { family_id fid_arg = arg_s->get_family_id(); if (fid_arg != fid && fid_arg != null_family_id) { diff --git a/src/ast/substitution/substitution_tree.cpp b/src/ast/substitution/substitution_tree.cpp index 809197c8f..438434f5b 100644 --- a/src/ast/substitution/substitution_tree.cpp +++ b/src/ast/substitution/substitution_tree.cpp @@ -73,7 +73,7 @@ void substitution_tree::linearize(svector & result) { for (unsigned i = 0; i < m_todo.size(); i++) { unsigned ireg_idx = m_todo[i]; expr * n = get_reg_value(ireg_idx); - var * ireg = m_manager.mk_var(ireg_idx, m_manager.get_sort(n)); + var * ireg = m_manager.mk_var(ireg_idx, n->get_sort()); if (is_var(n)) push(result, subst(ireg, n)); else { @@ -87,7 +87,7 @@ void substitution_tree::linearize(svector & result) { unsigned oreg = next_reg(); set_reg_value(oreg, to_app(n)->get_arg(j)); m_todo.push_back(oreg); - sort * s = m_manager.get_sort(get_reg_value(oreg)); + sort * s = get_reg_value(oreg)->get_sort(); new_args.push_back(m_manager.mk_var(oreg, s)); } new_app = m_manager.mk_app(to_app(n)->get_decl(), new_args.size(), new_args.c_ptr()); @@ -731,7 +731,7 @@ template bool substitution_tree::visit_vars(expr * e, st_visitor & st) { if (m_vars.empty()) return true; // continue - sort * s = m_manager.get_sort(e); + sort * s = e->get_sort(); unsigned s_id = s->get_decl_id(); if (s_id < m_vars.size()) { var_ref_vector * v = m_vars[s_id]; diff --git a/src/ast/well_sorted.cpp b/src/ast/well_sorted.cpp index ec1551637..fa8e2768b 100644 --- a/src/ast/well_sorted.cpp +++ b/src/ast/well_sorted.cpp @@ -56,7 +56,7 @@ struct well_sorted_proc { } for (unsigned i = 0; i < num_args; i++) { - sort * actual_sort = m_manager.get_sort(n->get_arg(i)); + sort * actual_sort = n->get_arg(i)->get_sort(); sort * expected_sort = decl->is_associative() ? decl->get_domain(0) : decl->get_domain(i); if (expected_sort != actual_sort) { TRACE("tc", tout << "sort mismatch on argument #" << i << ".\n" << mk_ismt2_pp(n, m_manager); diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index d39e30233..ae2eb1c80 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -221,7 +221,7 @@ func_decl * func_decls::find(ast_manager & m, unsigned num_args, expr * const * first(); ptr_buffer sorts; for (unsigned i = 0; i < num_args; i++) - sorts.push_back(m.get_sort(args[i])); + sorts.push_back(args[i]->get_sort()); return find(num_args, sorts.c_ptr(), range); } @@ -853,7 +853,7 @@ void cmd_context::insert(symbol const & s, unsigned arity, sort *const* domain, if (contains_macro(s, arity, domain)) { throw cmd_exception("named expression already defined"); } - if (contains_func_decl(s, arity, domain, m().get_sort(t))) { + if (contains_func_decl(s, arity, domain, t->get_sort())) { throw cmd_exception("invalid named expression, declaration already defined with this name ", s); } TRACE("insert_macro", tout << "new macro " << arity << "\n" << mk_pp(t, m()) << "\n";); @@ -895,10 +895,10 @@ void cmd_context::insert(symbol const & s, object_ref * r) { void cmd_context::model_add(symbol const & s, unsigned arity, sort *const* domain, expr * t) { if (!mc0()) m_mcs.set(m_mcs.size()-1, alloc(generic_model_converter, m(), "cmd_context")); if (m_solver.get() && !m_solver->mc0()) m_solver->set_model_converter(mc0()); - func_decl_ref fn(m().mk_func_decl(s, arity, domain, m().get_sort(t)), m()); + func_decl_ref fn(m().mk_func_decl(s, arity, domain, t->get_sort()), m()); func_decls & fs = m_func_decls.insert_if_not_there(s, func_decls()); fs.insert(m(), fn); - VERIFY(fn->get_range() == m().get_sort(t)); + VERIFY(fn->get_range() == t->get_sort()); mc0()->add(fn, t); if (!m_global_decls) m_func_decls_stack.push_back(sf_pair(s, fn)); @@ -1084,7 +1084,7 @@ void cmd_context::mk_app(symbol const & s, unsigned num_args, expr * const * arg decl_kind k = d.m_decl; // Hack: if d.m_next != 0, we use the sort of args[0] (if available) to decide which plugin we use. if (d.m_decl != 0 && num_args > 0) { - builtin_decl const & d2 = peek_builtin_decl(d, m().get_sort(args[0])->get_family_id()); + builtin_decl const & d2 = peek_builtin_decl(d, args[0]->get_sort()->get_family_id()); fid = d2.m_fid; k = d2.m_decl; } diff --git a/src/model/datatype_factory.cpp b/src/model/datatype_factory.cpp index 7e2f9ee56..e59ae14f2 100644 --- a/src/model/datatype_factory.cpp +++ b/src/model/datatype_factory.cpp @@ -63,7 +63,7 @@ expr * datatype_factory::get_last_fresh_value(sort * s) { bool datatype_factory::is_subterm_of_last_value(app* e) { expr* last; - if (!m_last_fresh_value.find(m_manager.get_sort(e), last)) { + if (!m_last_fresh_value.find(e->get_sort(), last)) { return false; } contains_app contains(m_manager, e); diff --git a/src/model/func_interp.cpp b/src/model/func_interp.cpp index dc5b78b0f..e327adcf6 100644 --- a/src/model/func_interp.cpp +++ b/src/model/func_interp.cpp @@ -297,7 +297,7 @@ void func_interp::compress() { } m_entries.reset(); reset_interp_cache(); - expr_ref new_else(m().mk_var(0, m().get_sort(m_else)), m()); + expr_ref new_else(m().mk_var(0, m_else->get_sort()), m()); m().inc_ref(new_else); m().dec_ref(m_else); m_else = new_else; @@ -318,7 +318,7 @@ bool func_interp::is_identity() const { } if (is_var(m_else)) return true; if (!m().is_value(m_else)) return false; - sort_size const& sz = m().get_sort(m_else)->get_num_elements(); + sort_size const& sz = m_else->get_sort()->get_num_elements(); if (!sz.is_finite()) return false; // @@ -340,7 +340,7 @@ expr * func_interp::get_interp_core() const { } if (vars.empty()) { for (unsigned i = 0; i < m_arity; i++) { - vars.push_back(m().mk_var(i, m().get_sort(curr->get_arg(i)))); + vars.push_back(m().mk_var(i, curr->get_arg(i)->get_sort())); } } ptr_buffer eqs; @@ -399,7 +399,7 @@ expr_ref func_interp::get_array_interp_core(func_decl * f) const { expr_ref_vector args(m()); array_util autil(m()); - sort_ref A(autil.mk_array_sort(domain.size(), domain.c_ptr(), m().get_sort(m_else)), m()); + sort_ref A(autil.mk_array_sort(domain.size(), domain.c_ptr(), m_else->get_sort()), m()); r = autil.mk_const_array(A, m_else); for (func_entry * curr : m_entries) { expr * res = curr->get_result(); diff --git a/src/model/model2expr.cpp b/src/model/model2expr.cpp index 08baffd8a..b29c8ca8c 100644 --- a/src/model/model2expr.cpp +++ b/src/model/model2expr.cpp @@ -70,7 +70,7 @@ static void mk_entry_cond(unsigned arity, func_entry const* entry, expr_ref& res // no-op } else { - conjs.push_back(m.mk_eq(m.mk_var(i, m.get_sort(e)), e)); + conjs.push_back(m.mk_eq(m.mk_var(i, e->get_sort()), e)); } } bool_rewriter(m).mk_and(conjs.size(), conjs.c_ptr(), result); diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index c319c50e3..c5c310cca 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -196,7 +196,7 @@ struct evaluator_cfg : public default_rewriter_cfg { if (k == OP_EQ) { // theory dispatch for = SASSERT(num == 2); - sort* s = m.get_sort(args[0]); + sort* s = args[0]->get_sort(); family_id s_fid = s->get_family_id(); if (s_fid == m_a_rw.get_fid()) st = m_a_rw.mk_eq_core(args[0], args[1], result); @@ -284,7 +284,7 @@ struct evaluator_cfg : public default_rewriter_cfg { if (m_array_as_stores && m_ar.is_array(val) && extract_array_func_interp(val, stores, else_case, _unused)) { - sort* srt = m.get_sort(val); + sort* srt = val->get_sort(); val = m_ar.mk_const_array(srt, else_case); for (unsigned i = stores.size(); i-- > 0; ) { expr_ref_vector args(m); @@ -400,7 +400,7 @@ struct evaluator_cfg : public default_rewriter_cfg { if (m.are_equal(else1, else2)) { // no op } - else if (m.are_distinct(else1, else2) && !(m.get_sort(else1)->get_info()->get_num_elements().is_finite())) { + else if (m.are_distinct(else1, else2) && !(else1->get_sort()->get_info()->get_num_elements().is_finite())) { result = m.mk_false(); return BR_DONE; } diff --git a/src/model/model_implicant.cpp b/src/model/model_implicant.cpp index 2cd78b6ca..ad0db9ca1 100644 --- a/src/model/model_implicant.cpp +++ b/src/model/model_implicant.cpp @@ -436,7 +436,7 @@ void model_implicant::eval_arith(app* e) { void model_implicant::inherit_value(expr* e, expr* v) { expr* w; SASSERT(!is_unknown(v)); - SASSERT(m.get_sort(e) == m.get_sort(v)); + SASSERT(e->get_sort() == v->get_sort()); if (is_x(v)) { set_x(e); } @@ -541,7 +541,7 @@ void model_implicant::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()) { @@ -888,7 +888,7 @@ expr_ref model_implicant::eval(model_ref& model, expr* e) { expr_ref_vector args(m); expr_ref else_case(m); if (extract_array_func_interp(result, stores, else_case)) { - result = m_array.mk_const_array(m.get_sort(e), else_case); + result = m_array.mk_const_array(e->get_sort(), else_case); while (!stores.empty() && stores.back().back() == else_case) { stores.pop_back(); } diff --git a/src/model/seq_factory.h b/src/model/seq_factory.h index 3928b6c25..ce395cef5 100644 --- a/src/model/seq_factory.h +++ b/src/model/seq_factory.h @@ -53,7 +53,7 @@ public: // generic method for setting unique sequences void set_prefix(expr* uniq) { m_trail.push_back(uniq); - m_unique_sequences.insert(m.get_sort(uniq), uniq); + m_unique_sequences.insert(uniq->get_sort(), uniq); } expr* get_some_value(sort* s) override { diff --git a/src/model/struct_factory.cpp b/src/model/struct_factory.cpp index 3e63e99de..31f86f883 100644 --- a/src/model/struct_factory.cpp +++ b/src/model/struct_factory.cpp @@ -43,7 +43,7 @@ struct_factory::~struct_factory() { } void struct_factory::register_value(expr * new_value) { - sort * s = m_manager.get_sort(new_value); + sort * s = new_value->get_sort(); value_set * set = get_value_set(s); if (!set->contains(new_value)) { m_values.push_back(new_value); diff --git a/src/model/value_factory.h b/src/model/value_factory.h index 76f9b71ac..8df61c181 100644 --- a/src/model/value_factory.h +++ b/src/model/value_factory.h @@ -202,7 +202,7 @@ public: } void register_value(expr * n) override { - sort * s = this->m_manager.get_sort(n); + sort * s = n->get_sort(); value_set * set = get_value_set(s); if (!set->m_values.contains(n)) { m_values.push_back(n); diff --git a/src/muz/base/bind_variables.cpp b/src/muz/base/bind_variables.cpp index 1e918b172..ee50cf503 100644 --- a/src/muz/base/bind_variables.cpp +++ b/src/muz/base/bind_variables.cpp @@ -89,7 +89,7 @@ expr_ref bind_variables::abstract(expr* term, cache_t& cache, unsigned scope) { cache.insert(e, v); } else { - var* v1 = m.mk_var(scope + v->get_idx(), m.get_sort(v)); + var* v1 = m.mk_var(scope + v->get_idx(), v->get_sort()); m_pinned.push_back(v1); cache.insert(e, v1); } diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index 5670bb8d2..8495dd9ab 100644 --- a/src/muz/base/dl_context.cpp +++ b/src/muz/base/dl_context.cpp @@ -782,13 +782,13 @@ namespace datalog { else if (is_var(e) && m.is_bool(e)) { m_engine_type = SPACER_ENGINE; } - else if (dt.is_datatype(m.get_sort(e))) { + else if (dt.is_datatype(e->get_sort())) { m_engine_type = SPACER_ENGINE; } - else if (is_large_bv(m.get_sort(e))) { + else if (is_large_bv(e->get_sort())) { m_engine_type = SPACER_ENGINE; } - else if (!m.get_sort(e)->get_num_elements().is_finite()) { + else if (!e->get_sort()->get_num_elements().is_finite()) { m_engine_type = SPACER_ENGINE; } else if (ar.is_array(e)) { diff --git a/src/muz/base/rule_properties.cpp b/src/muz/base/rule_properties.cpp index 5896504cf..0610fd95e 100644 --- a/src/muz/base/rule_properties.cpp +++ b/src/muz/base/rule_properties.cpp @@ -198,7 +198,7 @@ void rule_properties::insert(ptr_vector& rules, rule* r) { } void rule_properties::operator()(var* n) { - check_sort(m.get_sort(n)); + check_sort(n->get_sort()); } void rule_properties::operator()(quantifier* n) { @@ -245,7 +245,7 @@ void rule_properties::operator()(app* n) { else if (m_rec.is_defined(f)) { m_uninterp_funs.insert(f, m_rule); } - check_sort(m.get_sort(n)); + check_sort(n->get_sort()); } bool rule_properties::evaluates_to_numeral(expr * n, rational& val) { diff --git a/src/muz/bmc/dl_bmc_engine.cpp b/src/muz/bmc/dl_bmc_engine.cpp index a0233cc7b..aea8cad0b 100644 --- a/src/muz/bmc/dl_bmc_engine.cpp +++ b/src/muz/bmc/dl_bmc_engine.cpp @@ -435,7 +435,7 @@ namespace datalog { rule_vars[to_var(arg)->get_idx()] = 0; } else { - sort* srt = m.get_sort(arg); + sort* srt = arg->get_sort(); args.push_back(m.mk_var(rule_vars.size()+num_vars, srt)); conjs.push_back(m.mk_eq(args.back(), arg)); ++num_vars; @@ -604,7 +604,7 @@ namespace datalog { expr_ref_vector binding(m); ptr_vector arg_sorts; for (unsigned i = 0; i < args.size(); ++i) { - arg_sorts.push_back(m.get_sort(args[i])); + arg_sorts.push_back(args[i]->get_sort()); } for (unsigned i = 0; i < vars.size(); ++i) { if (vars[i]) { diff --git a/src/muz/fp/datalog_parser.cpp b/src/muz/fp/datalog_parser.cpp index 01530803e..66aa58602 100644 --- a/src/muz/fp/datalog_parser.cpp +++ b/src/muz/fp/datalog_parser.cpp @@ -959,9 +959,9 @@ protected: v = m.mk_var(idx, s); m_vars.insert(data.bare_str(), v); } - else if (s != m.get_sort(v)) { + else if (s != v->get_sort()) { throw default_exception(default_exception::fmt(), "sort: %s expected, but got: %s\n", - s->get_name().bare_str(), m.get_sort(v)->get_name().bare_str()); + s->get_name().bare_str(), v->get_sort()->get_name().bare_str()); } args.push_back(v); } diff --git a/src/muz/rel/dl_compiler.cpp b/src/muz/rel/dl_compiler.cpp index 387331353..589540b6f 100644 --- a/src/muz/rel/dl_compiler.cpp +++ b/src/muz/rel/dl_compiler.cpp @@ -902,7 +902,7 @@ namespace datalog { expr* e = it->m_value; if (!pos_vars.contains(v)) { single_res_expr.push_back(e); - make_add_unbound_column(r, v, pred, single_res, m.get_sort(e), single_res, dealloc, acc); + make_add_unbound_column(r, v, pred, single_res, e->get_sort(), single_res, dealloc, acc); TRACE("dl", tout << "Adding unbound column: " << mk_pp(e, m) << "\n";); } } diff --git a/src/muz/rel/dl_interval_relation.cpp b/src/muz/rel/dl_interval_relation.cpp index 75f9e7e42..5c5e446db 100644 --- a/src/muz/rel/dl_interval_relation.cpp +++ b/src/muz/rel/dl_interval_relation.cpp @@ -326,7 +326,7 @@ namespace datalog { for (unsigned i = 0; i < f.size(); ++i) { app_ref eq(m); expr* e = f[i]; - eq = m.mk_eq(m.mk_var(i, m.get_sort(e)), e); + eq = m.mk_eq(m.mk_var(i, e->get_sort()), e); r.filter_interpreted(eq.get()); } mk_union(r, nullptr, false); diff --git a/src/muz/rel/dl_mk_simple_joins.cpp b/src/muz/rel/dl_mk_simple_joins.cpp index 2aad88431..d87836566 100644 --- a/src/muz/rel/dl_mk_simple_joins.cpp +++ b/src/muz/rel/dl_mk_simple_joins.cpp @@ -162,7 +162,7 @@ namespace datalog { for (expr* arg : *t) { unsigned var_idx = to_var(arg)->get_idx(); if (!result.get(res_ofs - var_idx)) { - result[res_ofs - var_idx] = m.mk_var(next_var++, m.get_sort(arg)); + result[res_ofs - var_idx] = m.mk_var(next_var++, arg->get_sort()); } } } @@ -335,7 +335,7 @@ namespace datalog { var * v = to_var(arg); if (v->get_idx() == var_idx) { args.push_back(v); - domain.push_back(m.get_sort(v)); + domain.push_back(v->get_sort()); return true; } } @@ -594,7 +594,7 @@ namespace datalog { cost get_domain_size(expr* e) const { - return get_domain_size(m.get_sort(e)); + return get_domain_size(e->get_sort()); } cost get_domain_size(sort* s) const { diff --git a/src/muz/rel/udoc_relation.cpp b/src/muz/rel/udoc_relation.cpp index cf7161275..9ecdcefdf 100644 --- a/src/muz/rel/udoc_relation.cpp +++ b/src/muz/rel/udoc_relation.cpp @@ -263,7 +263,7 @@ namespace datalog { } uint64_t n, sz; ast_manager& m = get_ast_manager(); - if (dl.is_numeral(e, n) && dl.try_get_size(m.get_sort(e), sz)) { + if (dl.is_numeral(e, n) && dl.try_get_size(e->get_sort(), sz)) { num_bits = 0; while (sz > 0) ++num_bits, sz = sz/2; r = rational(n, rational::ui64()); diff --git a/src/muz/spacer/spacer_legacy_mev.cpp b/src/muz/spacer/spacer_legacy_mev.cpp index 944bd075f..f524d764a 100644 --- a/src/muz/spacer/spacer_legacy_mev.cpp +++ b/src/muz/spacer/spacer_legacy_mev.cpp @@ -363,7 +363,7 @@ void model_evaluator::inherit_value(expr* e, expr* v) { expr* w; SASSERT(!is_unknown(v)); - SASSERT(m.get_sort(e) == m.get_sort(v)); + SASSERT(e->get_sort() == v->get_sort()); if (is_x(v)) { set_x(e); } else if (m.is_bool(e)) { @@ -807,7 +807,7 @@ expr_ref model_evaluator::eval(const model_ref& model, expr* e){ expr_ref_vector args(m); expr_ref else_case(m); if (extract_array_func_interp(result, stores, else_case)) { - result = m_array.mk_const_array(m.get_sort(e), else_case); + result = m_array.mk_const_array(e->get_sort(), else_case); while (!stores.empty() && stores.back().back() == else_case) { stores.pop_back(); } diff --git a/src/muz/spacer/spacer_mev_array.cpp b/src/muz/spacer/spacer_mev_array.cpp index 8fa9c6d4c..526743b5f 100644 --- a/src/muz/spacer/spacer_mev_array.cpp +++ b/src/muz/spacer/spacer_mev_array.cpp @@ -198,7 +198,7 @@ void model_evaluator_array_util::eval(model& mdl, expr* e, expr_ref& r, bool mod expr_ref_vector args(m); expr_ref else_case(m); if (extract_array_func_interp(mdl, r, stores, else_case)) { - r = m_array.mk_const_array(m.get_sort(e), else_case); + r = m_array.mk_const_array(e->get_sort(), else_case); while (!stores.empty() && stores.back().back() == else_case) { stores.pop_back(); } diff --git a/src/muz/spacer/spacer_qe_project.cpp b/src/muz/spacer/spacer_qe_project.cpp index 18c8ba1bf..e528fdd56 100644 --- a/src/muz/spacer/spacer_qe_project.cpp +++ b/src/muz/spacer/spacer_qe_project.cpp @@ -273,13 +273,13 @@ namespace spacer_qe { if (a.is_le(lit, e1, e2) || a.is_ge(lit, e2, e1)) { if (!is_linear( mul, e1, c, ts) || !is_linear(-mul, e2, c, ts)) return false; - s = m.get_sort(e1); + s = e1->get_sort(); is_strict = is_not; } else if (a.is_lt(lit, e1, e2) || a.is_gt(lit, e2, e1)) { if (!is_linear( mul, e1, c, ts) || !is_linear(-mul, e2, c, ts)) return false; - s = m.get_sort(e1); + s = e1->get_sort(); is_strict = !is_not; } else if (m.is_eq(lit, e1, e2) && a.is_int_real (e1)) { @@ -311,7 +311,7 @@ namespace spacer_qe { if (is_not) is_diseq = true; else is_eq = true; } - s = m.get_sort(e1); + s = e1->get_sort(); } else { IF_VERBOSE(2, verbose_stream() << "can't project:" << mk_pp(lit, m) << "\n";); diff --git a/src/muz/transforms/dl_mk_array_blast.cpp b/src/muz/transforms/dl_mk_array_blast.cpp index e32ddf269..646320b6c 100644 --- a/src/muz/transforms/dl_mk_array_blast.cpp +++ b/src/muz/transforms/dl_mk_array_blast.cpp @@ -91,7 +91,7 @@ namespace datalog { r.get_vars(m, vars); m_next_var = vars.size() + 1; } - v = m.mk_var(m_next_var, m.get_sort(e)); + v = m.mk_var(m_next_var, e->get_sort()); m_defs.insert(e, v); ++m_next_var; } diff --git a/src/muz/transforms/dl_mk_bit_blast.cpp b/src/muz/transforms/dl_mk_bit_blast.cpp index 505d7d42b..a22de495e 100644 --- a/src/muz/transforms/dl_mk_bit_blast.cpp +++ b/src/muz/transforms/dl_mk_bit_blast.cpp @@ -186,7 +186,7 @@ namespace datalog { } else { m_args.push_back(arg); - m_f_vars.push_back(m.mk_var(idx++, m.get_sort(arg))); + m_f_vars.push_back(m.mk_var(idx++, arg->get_sort())); m_g_vars.push_back(m_f_vars.back()); } } @@ -200,7 +200,7 @@ namespace datalog { ptr_vector domain; for (expr* arg : m_args) { - domain.push_back(m.get_sort(arg)); + domain.push_back(arg->get_sort()); } g = m_context.mk_fresh_head_predicate(f->get_name(), symbol("bv"), m_args.size(), domain.c_ptr(), f); m_old_funcs.push_back(f); diff --git a/src/muz/transforms/dl_mk_coalesce.cpp b/src/muz/transforms/dl_mk_coalesce.cpp index 2ff4372c4..5e31de326 100644 --- a/src/muz/transforms/dl_mk_coalesce.cpp +++ b/src/muz/transforms/dl_mk_coalesce.cpp @@ -67,7 +67,7 @@ namespace datalog { bool_vector valid(sorts.size(), true); for (unsigned i = 0; i < sub.size(); ++i) { expr* e = sub[i]; - sort* s = m.get_sort(e); + sort* s = e->get_sort(); expr_ref w(m.mk_var(i, s), m); if (is_var(e)) { unsigned v = to_var(e)->get_idx(); @@ -87,7 +87,7 @@ namespace datalog { } else { SASSERT(m.is_value(e)); - SASSERT(m.get_sort(e) == m.get_sort(w)); + SASSERT(e->get_sort() == m.get_sort(w)); conjs.push_back(m.mk_eq(e, w)); } } diff --git a/src/muz/transforms/dl_mk_coi_filter.cpp b/src/muz/transforms/dl_mk_coi_filter.cpp index 79959d9bf..7839e28db 100644 --- a/src/muz/transforms/dl_mk_coi_filter.cpp +++ b/src/muz/transforms/dl_mk_coi_filter.cpp @@ -149,7 +149,7 @@ namespace datalog { for (unsigned j = 0; j < head->get_num_args(); ++j) { expr* arg = head->get_arg(j); if (!is_var(arg)) { - conj.push_back(m.mk_eq(m.mk_var(j, m.get_sort(arg)), arg)); + conj.push_back(m.mk_eq(m.mk_var(j, arg->get_sort()), arg)); } } fmls.push_back(mk_and(conj)); diff --git a/src/muz/transforms/dl_mk_quantifier_abstraction.cpp b/src/muz/transforms/dl_mk_quantifier_abstraction.cpp index f956ca429..bcd54d016 100644 --- a/src/muz/transforms/dl_mk_quantifier_abstraction.cpp +++ b/src/muz/transforms/dl_mk_quantifier_abstraction.cpp @@ -228,7 +228,7 @@ namespace datalog { unsigned sz = p->get_num_args(); for (unsigned i = 0; i < sz; ++i) { arg = p->get_arg(i); - sort* s = m.get_sort(arg); + sort* s = arg->get_sort(); while (a.is_array(s)) { unsigned arity = get_array_arity(s); for (unsigned j = 0; j < arity; ++j) { @@ -268,7 +268,7 @@ namespace datalog { unsigned sz = p->get_num_args(); for (unsigned i = 0; i < sz; ++i) { arg = ps->get_arg(i); - sort* s = m.get_sort(arg); + sort* s = arg->get_sort(); bool is_pattern = false; while (a.is_array(s)) { is_pattern = true; diff --git a/src/muz/transforms/dl_mk_separate_negated_tails.cpp b/src/muz/transforms/dl_mk_separate_negated_tails.cpp index 6da5a7931..74b1438dd 100644 --- a/src/muz/transforms/dl_mk_separate_negated_tails.cpp +++ b/src/muz/transforms/dl_mk_separate_negated_tails.cpp @@ -64,7 +64,7 @@ namespace datalog { expr* arg = p->get_arg(i); if (!m_vars.contains(arg)) { args.push_back(arg); - sorts.push_back(m.get_sort(arg)); + sorts.push_back(arg->get_sort()); } } fn = m.mk_fresh_func_decl(p->get_decl()->get_name(), symbol("N"), sorts.size(), sorts.c_ptr(), m.mk_bool_sort()); diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 8974a379a..b9e0b26c1 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -1009,7 +1009,7 @@ namespace opt { expr* context::mk_objective_fn(unsigned index, objective_t ty, unsigned sz, expr*const* args) { ptr_vector domain; for (unsigned i = 0; i < sz; ++i) { - domain.push_back(m.get_sort(args[i])); + domain.push_back(args[i]->get_sort()); } char const* name = ""; switch(ty) { diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index 266cb4420..f205c3bd1 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -1348,7 +1348,7 @@ namespace smt2 { expr_ref t(expr_stack().back(), m()); expr_stack().pop_back(); expr_ref_vector patterns(m()), cases(m()); - sort* srt = m().get_sort(t); + sort* srt = t->get_sort(); check_lparen_next("pattern bindings should be enclosed in a parenthesis"); if (curr_id_is_case()) { @@ -1400,7 +1400,7 @@ namespace smt2 { expr_ref result(m()); var_subst sub(m(), false); TRACE("parse_expr", tout << "term\n" << expr_ref(t, m()) << "\npatterns\n" << patterns << "\ncases\n" << cases << "\n";); - check_patterns(patterns, m().get_sort(t)); + check_patterns(patterns, t->get_sort()); for (unsigned i = patterns.size(); i > 0; ) { --i; expr_ref_vector subst(m()); @@ -1444,7 +1444,7 @@ namespace smt2 { // compute match condition and substitution // t is shifted by size of subst. expr_ref bind_match(expr* t, expr* pattern, expr_ref_vector& subst) { - if (m().get_sort(t) != m().get_sort(pattern)) { + if (t->get_sort() != m().get_sort(pattern)) { std::ostringstream str; str << "sorts of pattern " << expr_ref(pattern, m()) << " and term " << expr_ref(t, m()) << " are not aligned"; @@ -1767,7 +1767,7 @@ namespace smt2 { void check_qualifier(expr * t, bool has_as) { if (has_as) { sort * s = sort_stack().back(); - if (s != m().get_sort(t)) + if (s != t->get_sort()) throw parser_exception("invalid qualified identifier, sort mismatch"); sort_stack().pop_back(); } diff --git a/src/qe/mbp/mbp_arrays.cpp b/src/qe/mbp/mbp_arrays.cpp index 772a62869..acf8321c9 100644 --- a/src/qe/mbp/mbp_arrays.cpp +++ b/src/qe/mbp/mbp_arrays.cpp @@ -73,7 +73,7 @@ namespace { 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)); - unsigned arity = get_array_arity(m.get_sort(m_lhs)); + 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()); expr_ref_vector vec(m); @@ -95,12 +95,12 @@ namespace { m_arr_u.is_array (rhs) && m.get_sort(lhs) == m.get_sort(rhs)); 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 (auto const& v : diff_indices) { SASSERT(v.size() == get_array_arity(m.get_sort(m_lhs))); for (expr* e : v) - sorts.push_back (m.get_sort(e)); + sorts.push_back (e->get_sort()); } m_decl = m.mk_func_decl (symbol (PARTIAL_EQ), sorts.size (), sorts.c_ptr (), m.mk_bool_sort ()); } @@ -131,7 +131,7 @@ namespace { 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()); for (expr_ref_vector const& diff : m_diff_indices) { ptr_vector store_args; store_args.push_back (rhs); @@ -311,7 +311,7 @@ namespace mbp { // 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 @@ -804,7 +804,7 @@ namespace mbp { expr* reduce_core (app *a) { if (!m_arr_u.is_store (a->get_arg (0))) return a; expr* array = a->get_arg(0); - unsigned arity = get_array_arity(m.get_sort(array)); + unsigned arity = get_array_arity(array->get_sort()); expr* const* js = a->get_args() + 1; @@ -1015,7 +1015,7 @@ namespace mbp { 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); unsigned arity = get_array_arity(v_sort); bool is_numeric = true; @@ -1083,7 +1083,7 @@ namespace mbp { for (expr * x : m_idxs[0].idx) { std::stringstream name; name << "get" << (i++); - acc.push_back(mk_accessor_decl(m, symbol(name.str()), type_ref(m.get_sort(x)))); + acc.push_back(mk_accessor_decl(m, symbol(name.str()), type_ref(x->get_sort()))); } constructor_decl* constrs[1] = { mk_constructor_decl(symbol("tuple"), symbol("is-tuple"), acc.size(), acc.c_ptr()) }; datatype::def* dts = mk_datatype_decl(dt, symbol("tuple"), 0, nullptr, 1, constrs); @@ -1409,14 +1409,14 @@ namespace mbp { obj_map m_arrays; void add_index_sort(expr* n) { - sort* s = m.get_sort(n); + sort* s = n->get_sort(); if (!m_indices.contains(s)) { m_indices.insert(s, alloc(app_ref_vector, m)); } } void add_array(app* n) { - sort* s = m.get_sort(n); + sort* s = n->get_sort(); app_ref_vector* vs = nullptr; if (!m_arrays.find(s, vs)) { vs = alloc(app_ref_vector, m); @@ -1427,7 +1427,7 @@ namespace mbp { app_ref_vector* is_index(expr* n) { app_ref_vector* result = nullptr; - m_indices.find(m.get_sort(n), result); + m_indices.find(n->get_sort(), result); return result; } diff --git a/src/qe/mbp/mbp_datatypes.cpp b/src/qe/mbp/mbp_datatypes.cpp index a3230f541..2af469a1e 100644 --- a/src/qe/mbp/mbp_datatypes.cpp +++ b/src/qe/mbp/mbp_datatypes.cpp @@ -53,7 +53,7 @@ namespace mbp { try { - if (dt.is_recursive(m.get_sort(var))) { + if (dt.is_recursive(var->get_sort())) { project_rec(model, vars, lits); } else { @@ -198,7 +198,7 @@ namespace mbp { bool inserted = false; for (app* v : vars) { if (m.is_bool(v)) continue; - if (dt.is_datatype(m.get_sort(v))) continue; + if (dt.is_datatype(v->get_sort())) continue; inserted = true; has_var.mark(v); visited.mark(v); diff --git a/src/qe/mbp/mbp_term_graph.cpp b/src/qe/mbp/mbp_term_graph.cpp index bed96a0b7..ad180df26 100644 --- a/src/qe/mbp/mbp_term_graph.cpp +++ b/src/qe/mbp/mbp_term_graph.cpp @@ -1044,7 +1044,7 @@ namespace mbp { expr_ref_vector result(m); for (term *t : m_tg.m_terms) { expr* e = t->get_expr(); - if (m.get_sort(e)->get_family_id() != fid) continue; + if (e->get_sort()->get_family_id() != fid) continue; for (term * p : term::parents(t->get_root())) { expr* pe = p->get_expr(); if (!is_app(pe)) continue; diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp index 35ee148d5..2bd264cb9 100644 --- a/src/qe/qe.cpp +++ b/src/qe/qe.cpp @@ -1161,7 +1161,7 @@ namespace qe { expr* y = x; expr_abstract(m, 0, 1, &y, fml, result); symbol X(x->get_decl()->get_name()); - sort* s = m.get_sort(x); + sort* s = x->get_sort(); result = m.mk_exists(1, &s, &X, result); return result; } @@ -1273,7 +1273,7 @@ namespace qe { bool i_solver_context::has_plugin(app* x) { ast_manager& m = get_manager(); - family_id fid = m.get_sort(x)->get_family_id(); + family_id fid = x->get_sort()->get_family_id(); return 0 <= fid && fid < static_cast(m_plugins.size()) && @@ -1283,7 +1283,7 @@ namespace qe { qe_solver_plugin& i_solver_context::plugin(app* x) { ast_manager& m = get_manager(); SASSERT(has_plugin(x)); - return *(m_plugins[m.get_sort(x)->get_family_id()]); + return *(m_plugins[x->get_sort()->get_family_id()]); } void i_solver_context::mk_atom(expr* e, bool p, expr_ref& result) { diff --git a/src/qe/qe_datatype_plugin.cpp b/src/qe/qe_datatype_plugin.cpp index c458de334..20ed0baff 100644 --- a/src/qe/qe_datatype_plugin.cpp +++ b/src/qe/qe_datatype_plugin.cpp @@ -732,7 +732,7 @@ namespace qe { m_replace.apply_substitution(eqs.neq_atom(i), m.mk_false(), fml); } if (def) { - sort* s = m.get_sort(x); + sort* s = x->get_sort(); ptr_vector sorts; sorts.resize(eqs.num_neq_terms(), s); func_decl* diag = m.mk_func_decl(symbol("diag"), sorts.size(), sorts.c_ptr(), s); diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp index 947d298b9..cd17380ac 100644 --- a/src/qe/qe_lite.cpp +++ b/src/qe/qe_lite.cpp @@ -615,7 +615,7 @@ namespace qel { } bool is_unconstrained(var* x, expr* t, unsigned i, expr_ref_vector const& conjs) { - sort* s = m.get_sort(x); + sort* s = x->get_sort(); if (!m.is_fully_interp(s) || !s->get_num_elements().is_infinite()) return false; bool occ = occurs_var(x->get_idx(), t); for (unsigned j = 0; !occ && j < conjs.size(); ++j) { @@ -1421,7 +1421,7 @@ namespace fm { fm & m_owner; forbidden_proc(fm & o):m_owner(o) {} void operator()(::var * n) { - if (m_owner.is_var(n) && m_owner.m.get_sort(n)->get_family_id() == m_owner.m_util.get_family_id()) { + if (m_owner.is_var(n) && n->get_sort()->get_family_id() == m_owner.m_util.get_family_id()) { m_owner.m_forbidden_set.insert(n->get_idx()); } } diff --git a/src/qe/qe_mbp.cpp b/src/qe/qe_mbp.cpp index a1436fd44..d02112338 100644 --- a/src/qe/qe_mbp.cpp +++ b/src/qe/qe_mbp.cpp @@ -168,7 +168,7 @@ class mbproj::impl { expr* e1, * e2; if (m_array.is_select(n)) { for (expr* arg : *n) { - if (m.get_sort(arg) == m.get_sort(m_var) && arg != m_var) + if (arg->get_sort() == m.get_sort(m_var) && arg != m_var) m_res.push_back(arg); } } diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp index 6b5871186..0e1023402 100644 --- a/src/qe/qsat.cpp +++ b/src/qe/qsat.cpp @@ -794,7 +794,7 @@ namespace qe { void filter_vars(app_ref_vector const& vars) { for (app* v : vars) m_pred_abs.fmc()->hide(v); - for (app* v : vars) check_sort(m.get_sort(v)); + for (app* v : vars) check_sort(v->get_sort()); } void initialize_levels() { diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 727fbc1e3..61b74169d 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -825,7 +825,7 @@ private: SASSERT(value.size() == 1); val = value[0].sign() ? m.mk_not(v) : v; } - else if (is_uninterp_const(v) && bvutil.is_bv_sort(m.get_sort(v))) { + else if (is_uninterp_const(v) && bvutil.is_bv_sort(v->get_sort())) { SASSERT(value.size() == bvutil.get_bv_size(v)); if (m_exps.empty()) { m_exps.push_back(rational::one()); diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp index 6960fe444..346e53f13 100644 --- a/src/sat/smt/arith_solver.cpp +++ b/src/sat/smt/arith_solver.cpp @@ -313,7 +313,7 @@ namespace arith { expr* e2 = n2->get_expr(); if (m.is_ite(e1) || m.is_ite(e2)) return; - if (m.get_sort(e1) != m.get_sort(e2)) + if (e1->get_sort() != m.get_sort(e2)) return; reset_evidence(); for (auto const& ev : e) diff --git a/src/sat/smt/array_axioms.cpp b/src/sat/smt/array_axioms.cpp index 4d7a644c5..32530355d 100644 --- a/src/sat/smt/array_axioms.cpp +++ b/src/sat/smt/array_axioms.cpp @@ -214,7 +214,7 @@ namespace array { bool solver::assert_extensionality(expr* e1, expr* e2) { TRACE("array", tout << "extensionality-axiom: " << mk_bounded_pp(e1, m) << " == " << mk_bounded_pp(e2, m) << "\n";); ++m_stats.m_num_extensionality_axiom; - func_decl_ref_vector const& funcs = sort2diff(m.get_sort(e1)); + func_decl_ref_vector const& funcs = sort2diff(e1->get_sort()); expr_ref_vector args1(m), args2(m); args1.push_back(e1); args2.push_back(e2); @@ -359,7 +359,7 @@ namespace array { for (unsigned i = 1; i + 1 < num_args; ++i) { expr* arg = store->get_arg(i); - sort* srt = m.get_sort(arg); + sort* srt = arg->get_sort(); auto ep = mk_epsilon(srt); eqs.push_back(m.mk_eq(ep.first, arg)); args1.push_back(m.mk_app(ep.second, arg)); @@ -400,7 +400,7 @@ namespace array { bool solver::assert_congruent_axiom(expr* e1, expr* e2) { TRACE("array", tout << "congruence-axiom: " << mk_bounded_pp(e1, m) << " " << mk_bounded_pp(e2, m) << "\n";); ++m_stats.m_num_congruence_axiom; - sort* srt = m.get_sort(e1); + sort* srt = e1->get_sort(); unsigned dimension = get_array_arity(srt); expr_ref_vector args1(m), args2(m); args1.push_back(e1); @@ -504,7 +504,7 @@ namespace array { for (unsigned j = i; j-- > 0; ) { theory_var v2 = roots[j]; expr* e2 = var2expr(v2); - if (m.get_sort(e1) != m.get_sort(e2)) + if (e1->get_sort() != m.get_sort(e2)) continue; if (have_different_model_values(v1, v2)) continue; diff --git a/src/sat/smt/array_model.cpp b/src/sat/smt/array_model.cpp index 1ea6eb4de..90e01b4e3 100644 --- a/src/sat/smt/array_model.cpp +++ b/src/sat/smt/array_model.cpp @@ -47,7 +47,7 @@ namespace array { void solver::add_value(euf::enode* n, model& mdl, expr_ref_vector& values) { SASSERT(a.is_array(n->get_expr())); ptr_vector args; - sort* srt = m.get_sort(n->get_expr()); + sort* srt = n->get_expr()->get_sort(); unsigned arity = get_array_arity(srt); func_decl * f = mk_aux_decl_for_array_sort(m, srt); func_interp * fi = alloc(func_interp, m, arity); diff --git a/src/sat/smt/bv_ackerman.cpp b/src/sat/smt/bv_ackerman.cpp index a788e5cfd..b970c87fa 100644 --- a/src/sat/smt/bv_ackerman.cpp +++ b/src/sat/smt/bv_ackerman.cpp @@ -165,8 +165,8 @@ namespace bv { return; if (!s.var2enode(v1) || !s.var2enode(v2)) return; - sort* s1 = s.m.get_sort(s.var2expr(v1)); - sort* s2 = s.m.get_sort(s.var2expr(v2)); + sort* s1 = s.var2expr(v1)->get_sort(); + sort* s2 = s.var2expr(v2)->get_sort(); if (s1 != s2 || !s.bv.is_bv_sort(s1)) return; // IF_VERBOSE(0, verbose_stream() << "assert ackerman " << v1 << " " << v2 << "\n"); diff --git a/src/sat/smt/dt_solver.cpp b/src/sat/smt/dt_solver.cpp index df9c743fa..4caec96a3 100644 --- a/src/sat/smt/dt_solver.cpp +++ b/src/sat/smt/dt_solver.cpp @@ -121,7 +121,7 @@ namespace dt { m_stats.m_assert_cnstr++; SASSERT(dt.is_constructor(c)); SASSERT(is_datatype(e)); - SASSERT(c->get_range() == m.get_sort(e)); + SASSERT(c->get_range() == e->get_sort()); m_args.reset(); ptr_vector const& accessors = *dt.get_constructor_accessors(c); SASSERT(c->get_arity() == accessors.size()); @@ -223,7 +223,7 @@ namespace dt { assert_update_field_axioms(n); } else { - sort* s = m.get_sort(n->get_expr()); + sort* s = n->get_expr()->get_sort(); if (dt.get_datatype_num_constructors(s) == 1) assert_is_constructor_axiom(n, dt.get_datatype_constructors(s)->get(0)); else if (get_config().m_dt_lazy_splits == 0 || (get_config().m_dt_lazy_splits == 1 && !s->is_infinite())) @@ -242,7 +242,7 @@ namespace dt { v = m_find.find(v); enode* n = var2enode(v); - sort* srt = m.get_sort(n->get_expr()); + sort* srt = n->get_expr()->get_sort(); func_decl* non_rec_c = dt.get_non_rec_constructor(srt); unsigned non_rec_idx = dt.get_constructor_idx(non_rec_c); var_data* d = m_var_data[v]; @@ -388,7 +388,7 @@ namespace dt { unsigned num_unassigned = 0; unsigned unassigned_idx = UINT_MAX; enode* n = var2enode(v); - sort* srt = m.get_sort(n->get_expr()); + sort* srt = n->get_expr()->get_sort(); var_data* d = m_var_data[v]; if (d->m_recognizers.empty()) { theory_var w = recognizer->get_arg(0)->get_th_var(get_id()); @@ -565,7 +565,7 @@ namespace dt { } // explore `arg` (with parent) expr* earg = arg->get_expr(); - sort* s = m.get_sort(earg); + sort* s = earg->get_sort(); if (dt.is_datatype(s)) { m_parent.insert(arg->get_root(), parent); oc_push_stack(arg); @@ -732,7 +732,7 @@ namespace dt { SASSERT(!n->is_attached_to(get_id())); if (is_constructor(term) || is_update_field(term)) { for (enode* arg : euf::enode_args(n)) { - sort* s = m.get_sort(arg->get_expr()); + sort* s = arg->get_expr()->get_sort(); if (dt.is_datatype(s)) mk_var(arg); else if (m_autil.is_array(s) && dt.is_datatype(get_array_range(s))) { diff --git a/src/sat/smt/dt_solver.h b/src/sat/smt/dt_solver.h index 7015cfdd1..92300301f 100644 --- a/src/sat/smt/dt_solver.h +++ b/src/sat/smt/dt_solver.h @@ -77,7 +77,7 @@ namespace dt { bool is_accessor(enode * n) const { return is_accessor(n->get_expr()); } bool is_update_field(enode * n) const { return dt.is_update_field(n->get_expr()); } - bool is_datatype(expr* e) const { return dt.is_datatype(m.get_sort(e)); } + bool is_datatype(expr* e) const { return dt.is_datatype(e->get_sort()); } bool is_datatype(enode* n) const { return is_datatype(n->get_expr()); } void assert_eq_axiom(enode * lhs, expr * rhs, literal antecedent = sat::null_literal); diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp index 2a9e2a22d..f499de627 100644 --- a/src/sat/smt/euf_internalize.cpp +++ b/src/sat/smt/euf_internalize.cpp @@ -108,15 +108,15 @@ namespace euf { if (m.is_bool(e)) attach_lit(literal(si.add_bool_var(e), false), e); - if (!m.is_bool(e) && m.get_sort(e)->get_family_id() != null_family_id) { + if (!m.is_bool(e) && e->get_sort()->get_family_id() != null_family_id) { auto* e_ext = expr2solver(e); - auto* s_ext = sort2solver(m.get_sort(e)); + auto* s_ext = sort2solver(e->get_sort()); if (s_ext && s_ext != e_ext) - s_ext->apply_sort_cnstr(n, m.get_sort(e)); + s_ext->apply_sort_cnstr(n, e->get_sort()); } expr* a = nullptr, * b = nullptr; - if (m.is_eq(e, a, b) && m.get_sort(a)->get_family_id() != null_family_id) { - auto* s_ext = sort2solver(m.get_sort(a)); + if (m.is_eq(e, a, b) && a->get_sort()->get_family_id() != null_family_id) { + auto* s_ext = sort2solver(a->get_sort()); if (s_ext) s_ext->eq_internalized(n); } @@ -195,7 +195,7 @@ namespace euf { else { // g(f(x_i)) = x_i // f(x_1) = a + .... + f(x_n) = a >= 2 - sort* srt = m.get_sort(e->get_arg(0)); + sort* srt = e->get_arg(0)->get_sort(); SASSERT(!m.is_bool(srt)); sort_ref u(m.mk_fresh_sort("distinct-elems"), m); sort* u_ptr = u.get(); @@ -242,7 +242,7 @@ namespace euf { } else { // dist-f(x_1) = v_1 & ... & dist-f(x_n) = v_n - sort* srt = m.get_sort(e->get_arg(0)); + sort* srt = e->get_arg(0)->get_sort(); SASSERT(!m.is_bool(srt)); sort_ref u(m.mk_fresh_sort("distinct-elems"), m); func_decl_ref f(m.mk_fresh_func_decl("dist-f", "", 1, &srt, u), m); diff --git a/src/sat/smt/euf_model.cpp b/src/sat/smt/euf_model.cpp index 554f44a3c..9f95083c1 100644 --- a/src/sat/smt/euf_model.cpp +++ b/src/sat/smt/euf_model.cpp @@ -90,7 +90,7 @@ namespace euf { void solver::collect_dependencies(user_sort& us, deps_t& deps) { for (enode* n : m_egraph.nodes()) { expr* e = n->get_expr(); - sort* srt = m.get_sort(e); + sort* srt = e->get_sort(); auto* mb = sort2solver(srt); if (mb) mb->add_dep(n, deps); @@ -148,7 +148,7 @@ namespace euf { } continue; } - sort* srt = m.get_sort(e); + sort* srt = e->get_sort(); if (m.is_uninterp(srt)) us.add(n->get_root(), srt); else if (auto* mbS = sort2solver(srt)) diff --git a/src/sat/smt/fpa_solver.cpp b/src/sat/smt/fpa_solver.cpp index 01d7e286d..cbf767fc2 100644 --- a/src/sat/smt/fpa_solver.cpp +++ b/src/sat/smt/fpa_solver.cpp @@ -203,7 +203,7 @@ namespace fpa { add_units(mk_side_conditions()); } else - add_unit(eq_internalize(m_converter.unwrap(wrapped, m.get_sort(n)), n)); + add_unit(eq_internalize(m_converter.unwrap(wrapped, n->get_sort()), n)); } } else if (is_app(n) && to_app(n)->get_family_id() == get_id()) { @@ -295,7 +295,7 @@ namespace fpa { expr* a = values.get(n->get_arg(0)->get_root_id()); expr* b = values.get(n->get_arg(1)->get_root_id()); expr* c = values.get(n->get_arg(2)->get_root_id()); - value = m_converter.bv2fpa_value(m.get_sort(e), a, b, c); + value = m_converter.bv2fpa_value(e->get_sort(), a, b, c); } else if (m_fpa_util.is_bv2rm(e)) { SASSERT(n->num_args() == 1); @@ -307,12 +307,12 @@ namespace fpa { value = m_fpa_util.mk_round_toward_zero(); else if (m_fpa_util.is_float(e) && is_wrapped()) { expr* a = values.get(expr2enode(wrapped)->get_root_id()); - value = m_converter.bv2fpa_value(m.get_sort(e), a); + value = m_converter.bv2fpa_value(e->get_sort(), a); } else { SASSERT(m_fpa_util.is_float(e)); - unsigned ebits = m_fpa_util.get_ebits(m.get_sort(e)); - unsigned sbits = m_fpa_util.get_sbits(m.get_sort(e)); + unsigned ebits = m_fpa_util.get_ebits(e->get_sort()); + unsigned sbits = m_fpa_util.get_sbits(e->get_sort()); value = m_fpa_util.mk_pzero(ebits, sbits); } values.set(n->get_root_id(), value); diff --git a/src/sat/smt/q_mbi.cpp b/src/sat/smt/q_mbi.cpp index b4718c8c5..87f0deb5b 100644 --- a/src/sat/smt/q_mbi.cpp +++ b/src/sat/smt/q_mbi.cpp @@ -341,7 +341,7 @@ namespace q { if (!qb.is_free(idx)) continue; expr* v = qb.vars.get(qb.vars.size() - idx - 1); - sort* srt = m.get_sort(v); + sort* srt = v->get_sort(); expr_ref_vector veqs(m), meqs(m); auto const& nodes = ctx.get_egraph().nodes(); unsigned sz = nodes.size(); @@ -351,7 +351,7 @@ namespace q { auto* n = nodes[i]; expr* e = n->get_expr(); expr* val = ctx.node2value(n); - if (val && m.get_sort(e) == srt && !m.is_value(e) && !visited.is_marked(val)) { + if (val && e->get_sort() == srt && !m.is_value(e) && !visited.is_marked(val)) { visited.mark(val); veqs.push_back(m.mk_eq(v, e)); meqs.push_back(m.mk_eq(v, val)); @@ -484,7 +484,7 @@ namespace q { bool mbqi::next_offset(unsigned_vector& offsets, app_ref_vector const& vars, unsigned index, unsigned start) { auto* v = vars[index]; - sort* srt = m.get_sort(v); + sort* srt = v->get_sort(); auto const& nodes = ctx.get_egraph().nodes(); unsigned sz = nodes.size(); for (unsigned i = start; i < sz; ++i) { @@ -492,7 +492,7 @@ namespace q { if (n->generation() > 0) return false; expr* e = n->get_expr(); - if (m.get_sort(e) == srt && !m.is_value(e)) { + if (e->get_sort() == srt && !m.is_value(e)) { offsets[index] = i; return true; } diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp index 4aa900e76..a80e5c4d3 100644 --- a/src/sat/smt/q_solver.cpp +++ b/src/sat/smt/q_solver.cpp @@ -184,7 +184,7 @@ namespace q { if (!n->interpreted() && !m.is_uninterp(m.get_sort(n->get_expr()))) continue; expr* e = n->get_expr(); - sort* s = m.get_sort(e); + sort* s = e->get_sort(); if (m_unit_table.contains(s)) continue; m_unit_table.insert(s, e); diff --git a/src/shell/drat_frontend.cpp b/src/shell/drat_frontend.cpp index b7262e18c..9eccc659f 100644 --- a/src/shell/drat_frontend.cpp +++ b/src/shell/drat_frontend.cpp @@ -33,7 +33,7 @@ class smt_checker { m_fresh_exprs.reserve(i + 1); expr* r = m_fresh_exprs.get(i); if (!r) { - r = m.mk_fresh_const("sk", m.get_sort(e)); + r = m.mk_fresh_const("sk", e->get_sort()); m_fresh_exprs[i] = r; } return r; @@ -175,7 +175,7 @@ public: params.reset(); sorts.reset(); for (expr* arg : args) - sorts.push_back(m.get_sort(arg)); + sorts.push_back(arg->get_sort()); sort_ref rng(m); func_decl* f = nullptr; switch (sexpr->get_kind()) { diff --git a/src/smt/proto_model/proto_model.cpp b/src/smt/proto_model/proto_model.cpp index d0ec5cd1f..cd237d851 100644 --- a/src/smt/proto_model/proto_model.cpp +++ b/src/smt/proto_model/proto_model.cpp @@ -326,7 +326,7 @@ expr * proto_model::get_fresh_value(sort * s) { } void proto_model::register_value(expr * n) { - sort * s = m.get_sort(n); + sort * s = n->get_sort(); if (m.is_uninterp(s)) { m_user_sort_factory->register_value(n); } diff --git a/src/smt/seq_axioms.cpp b/src/smt/seq_axioms.cpp index 0ca0a5500..cf2eb2902 100644 --- a/src/smt/seq_axioms.cpp +++ b/src/smt/seq_axioms.cpp @@ -481,7 +481,7 @@ void seq_axioms::add_at_axiom(expr* e) { m_rewrite(i); expr_ref zero(a.mk_int(0), m); expr_ref one(a.mk_int(1), m); - expr_ref emp(seq.str.mk_empty(m.get_sort(e)), m); + expr_ref emp(seq.str.mk_empty(e->get_sort()), m); expr_ref len_s = mk_len(s); literal i_ge_0 = mk_ge(i, 0); literal i_ge_len_s = mk_ge(mk_sub(i, mk_len(s)), 0); @@ -497,7 +497,7 @@ void seq_axioms::add_at_axiom(expr* e) { } nth = es.back(); es.push_back(m_sk.mk_tail(s, i)); - add_axiom(~i_ge_0, i_ge_len_s, mk_seq_eq(s, seq.str.mk_concat(es, m.get_sort(e)))); + add_axiom(~i_ge_0, i_ge_len_s, mk_seq_eq(s, seq.str.mk_concat(es, e->get_sort()))); add_axiom(~i_ge_0, i_ge_len_s, mk_seq_eq(nth, e)); } else { @@ -746,7 +746,7 @@ void seq_axioms::add_lt_axiom(expr* n) { expr_ref e1(_e1, m), e2(_e2, m); m_rewrite(e1); m_rewrite(e2); - sort* s = m.get_sort(e1); + sort* s = e1->get_sort(); sort* char_sort = nullptr; VERIFY(seq.is_seq(s, char_sort)); literal lt = mk_literal(n); diff --git a/src/smt/seq_eq_solver.cpp b/src/smt/seq_eq_solver.cpp index 351ec1ed4..c8d3f73df 100644 --- a/src/smt/seq_eq_solver.cpp +++ b/src/smt/seq_eq_solver.cpp @@ -582,7 +582,7 @@ bool theory_seq::split_lengths(dependency* dep, if (lenY.is_zero()) { return set_empty(Y); } - b = mk_concat(bs, m.get_sort(X)); + b = mk_concat(bs, X->get_sort()); SASSERT(X != Y); @@ -738,7 +738,7 @@ bool theory_seq::branch_unit_variable(dependency* dep, expr* X, expr_ref_vector literal lit = mk_eq(m_autil.mk_int(lX), mk_len(X), false); switch (ctx.get_assignment(lit)) { case l_true: { - expr_ref R = mk_concat(lX, units.c_ptr(), m.get_sort(X)); + expr_ref R = mk_concat(lX, units.c_ptr(), X->get_sort()); return propagate_eq(dep, lit, X, R); } case l_undef: @@ -1314,7 +1314,7 @@ bool theory_seq::propagate_length_coherence(expr* e) { elems.push_back(head); seq = tail; } - expr_ref emp(m_util.str.mk_empty(m.get_sort(e)), m); + expr_ref emp(m_util.str.mk_empty(e->get_sort()), m); elems.push_back(seq); tail = mk_concat(elems.size(), elems.c_ptr()); // len(e) >= low => e = tail; @@ -1344,7 +1344,7 @@ bool theory_seq::propagate_length_coherence(expr* e) { bool theory_seq::check_length_coherence(expr* e) { if (is_var(e) && m_rep.is_root(e)) { if (!check_length_coherence0(e)) { - expr_ref emp(m_util.str.mk_empty(m.get_sort(e)), m); + expr_ref emp(m_util.str.mk_empty(e->get_sort()), m); expr_ref head(m), tail(m); // e = emp \/ e = unit(head.elem(e))*tail(e) m_sk.decompose(e, head, tail); @@ -1360,7 +1360,7 @@ bool theory_seq::check_length_coherence(expr* e) { bool theory_seq::check_length_coherence0(expr* e) { if (is_var(e) && m_rep.is_root(e)) { - expr_ref emp(m_util.str.mk_empty(m.get_sort(e)), m); + expr_ref emp(m_util.str.mk_empty(e->get_sort()), m); bool p = propagate_length_coherence(e); if (p || assume_equality(e, emp)) { diff --git a/src/smt/seq_skolem.cpp b/src/smt/seq_skolem.cpp index e6391660f..a9657b2ed 100644 --- a/src/smt/seq_skolem.cpp +++ b/src/smt/seq_skolem.cpp @@ -44,7 +44,7 @@ expr_ref seq_skolem::mk(symbol const& s, expr* e1, expr* e2, expr* e3, expr* e4, expr* es[4] = { e1, e2, e3, e4 }; unsigned len = e4?4:(e3?3:(e2?2:(e1?1:0))); if (!range) { - range = m.get_sort(e1); + range = e1->get_sort(); } expr_ref result(seq.mk_skolem(s, len, es, range), m); if (rw) @@ -93,7 +93,7 @@ decompose_main: } else if (seq.str.is_unit(e)) { head = e; - tail = seq.str.mk_empty(m.get_sort(e)); + tail = seq.str.mk_empty(e->get_sort()); m_rewrite(head); } else if (seq.str.is_concat(e, e1, e2) && seq.str.is_empty(e1)) { diff --git a/src/smt/smt_arith_value.cpp b/src/smt/smt_arith_value.cpp index 3f8e31f29..8984fe981 100644 --- a/src/smt/smt_arith_value.cpp +++ b/src/smt/smt_arith_value.cpp @@ -134,7 +134,7 @@ namespace smt { rational lo; bool s = false; if ((a.is_int_real(e) || b.is_bv(e)) && get_lo(e, lo, s) && !s) { - return expr_ref(a.mk_numeral(lo, m.get_sort(e)), m); + return expr_ref(a.mk_numeral(lo, e->get_sort()), m); } return expr_ref(e, m); } @@ -143,7 +143,7 @@ namespace smt { rational up; bool s = false; if ((a.is_int_real(e) || b.is_bv(e)) && get_up(e, up, s) && !s) { - return expr_ref(a.mk_numeral(up, m.get_sort(e)), m); + return expr_ref(a.mk_numeral(up, e->get_sort()), m); } return expr_ref(e, m); } @@ -152,7 +152,7 @@ namespace smt { rational lo, up; bool s = false; if (a.is_int_real(e) && get_lo(e, lo, s) && !s && get_up(e, up, s) && !s && lo == up) { - return expr_ref(a.mk_numeral(lo, m.get_sort(e)), m); + return expr_ref(a.mk_numeral(lo, e->get_sort()), m); } return expr_ref(e, m); } diff --git a/src/smt/smt_consequences.cpp b/src/smt/smt_consequences.cpp index b508372a1..35fbb6146 100644 --- a/src/smt/smt_consequences.cpp +++ b/src/smt/smt_consequences.cpp @@ -305,7 +305,7 @@ namespace smt { } else { if (!pushed) pushed = true, push(); - expr_ref c(m.mk_fresh_const("v", m.get_sort(v)), m); + expr_ref c(m.mk_fresh_const("v", v->get_sort()), m); expr_ref eq(m.mk_eq(c, v), m); assert_expr(eq); vars.push_back(c); diff --git a/src/smt/smt_induction.cpp b/src/smt/smt_induction.cpp index 9e4bd2179..4cd8ada8f 100644 --- a/src/smt/smt_induction.cpp +++ b/src/smt/smt_induction.cpp @@ -277,7 +277,7 @@ bool induction_lemmas::positions_dont_overlap(induction_positions_t const& posit */ void induction_lemmas::mk_hypothesis_substs(unsigned depth, expr* x, cond_substs_t& subst) { expr_ref_vector conds(m); - mk_hypothesis_substs_rec(depth, m.get_sort(x), x, conds, subst); + mk_hypothesis_substs_rec(depth, x->get_sort(), x, conds, subst); } void induction_lemmas::mk_hypothesis_substs_rec(unsigned depth, sort* s, expr* y, expr_ref_vector& conds, cond_substs_t& subst) { diff --git a/src/smt/smt_value_sort.cpp b/src/smt/smt_value_sort.cpp index 56768b91a..f2f9ff2bc 100644 --- a/src/smt/smt_value_sort.cpp +++ b/src/smt/smt_value_sort.cpp @@ -68,7 +68,7 @@ namespace smt { } bool is_value_sort(ast_manager& m, expr* e) { - return is_value_sort(m, m.get_sort(e)); + return is_value_sort(m, e->get_sort()); } } diff --git a/src/smt/tactic/ctx_solver_simplify_tactic.cpp b/src/smt/tactic/ctx_solver_simplify_tactic.cpp index e16f8d921..8307dff3f 100644 --- a/src/smt/tactic/ctx_solver_simplify_tactic.cpp +++ b/src/smt/tactic/ctx_solver_simplify_tactic.cpp @@ -230,7 +230,7 @@ protected: } } else if (!n2 && !m.is_value(arg)) { - n2 = mk_fresh(id, m.get_sort(arg)); + n2 = mk_fresh(id, arg->get_sort()); trail.push_back(n2); todo.push_back(expr_pos(self_pos, ++child_id, i, arg)); names.push_back(n2); diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp index f871bb464..10038a009 100644 --- a/src/smt/theory_array_base.cpp +++ b/src/smt/theory_array_base.cpp @@ -317,7 +317,7 @@ namespace smt { app * e2 = n2->get_owner(); func_decl_ref_vector * funcs = nullptr; - sort * s = m.get_sort(e1); + sort * s = e1->get_sort(); VERIFY(m_sort2skolem.find(s, funcs)); @@ -353,7 +353,7 @@ namespace smt { void theory_array_base::assert_congruent_core(enode * n1, enode * n2) { app * e1 = n1->get_owner(); app * e2 = n2->get_owner(); - sort* s = m.get_sort(e1); + sort* s = e1->get_sort(); unsigned dimension = get_array_arity(s); literal n1_eq_n2 = mk_eq(e1, e2, true); ctx.mark_as_relevant(n1_eq_n2); diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp index cc13ca707..47f67e9da 100644 --- a/src/smt/theory_array_full.cpp +++ b/src/smt/theory_array_full.cpp @@ -720,7 +720,7 @@ namespace smt { for (unsigned i = 1; i + 1 < num_args; ++i) { expr* arg = store_app->get_arg(i); - sort* srt = m.get_sort(arg); + sort* srt = arg->get_sort(); auto ep = mk_epsilon(srt); eqs.push_back(m.mk_eq(ep.first, arg)); args1.push_back(m.mk_app(ep.second, arg)); diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index fd5df0192..752e899aa 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -602,7 +602,7 @@ namespace smt { SASSERT(ctx.e_internalized(n)); SASSERT(m_util.is_bv2int(n)); TRACE("bv2int_bug", tout << "bv2int:\n" << mk_pp(n, m) << "\n";); - sort * int_sort = m.get_sort(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))); expr_ref_vector k_bits(m); @@ -1086,7 +1086,7 @@ namespace smt { 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 = m.get_sort(arg); + 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";); diff --git a/src/smt/theory_char.cpp b/src/smt/theory_char.cpp index e506f5278..3faa5f73e 100644 --- a/src/smt/theory_char.cpp +++ b/src/smt/theory_char.cpp @@ -121,7 +121,7 @@ namespace smt { bits.push_back(literal(ctx.get_bool_var(arg))); for (literal bit : bits) ctx.mark_as_relevant(bit); - expr_ref bits2char(seq.mk_skolem(m_bits2char, ebits.size(), ebits.c_ptr(), m.get_sort(e)), m); + expr_ref bits2char(seq.mk_skolem(m_bits2char, ebits.size(), ebits.c_ptr(), e->get_sort()), m); ctx.mark_as_relevant(bits2char.get()); enode* n1 = ensure_enode(e); enode* n2 = ensure_enode(bits2char); diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index d96a2c271..02296bcec 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -142,9 +142,9 @@ namespace smt { << mk_pp(c, m) << " " << mk_pp(e, m) << "\n";); m_stats.m_assert_cnstr++; SASSERT(m_util.is_constructor(c)); - SASSERT(m_util.is_datatype(m.get_sort(e))); + SASSERT(m_util.is_datatype(e->get_sort())); - SASSERT(c->get_range() == m.get_sort(e)); + SASSERT(c->get_range() == e->get_sort()); ptr_vector args; ptr_vector const & accessors = *m_util.get_constructor_accessors(c); SASSERT(c->get_arity() == accessors.size()); diff --git a/src/smt/theory_dense_diff_logic_def.h b/src/smt/theory_dense_diff_logic_def.h index 79e6c9ca0..e8af0aa75 100644 --- a/src/smt/theory_dense_diff_logic_def.h +++ b/src/smt/theory_dense_diff_logic_def.h @@ -45,7 +45,7 @@ namespace smt { template inline app * theory_dense_diff_logic::mk_zero_for(expr * n) { - return m_autil.mk_numeral(rational(0), m.get_sort(n)); + return m_autil.mk_numeral(rational(0), n->get_sort()); } template diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 9f8e9c4b0..802fb230d 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -459,7 +459,7 @@ namespace smt { } else { expr_ref wu(m); - wu = m.mk_eq(m_converter.unwrap(wrapped, m.get_sort(n)), n); + wu = m.mk_eq(m_converter.unwrap(wrapped, n->get_sort()), n); TRACE("t_fpa", tout << "w/u eq: " << std::endl << mk_ismt2_pp(wu, m) << std::endl;); assert_cnstr(wu); } diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 5abef0480..36811fbbe 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 (m.get_sort(e1) != m.get_sort(e2)) + if (e1->get_sort() != m.get_sort(e2)) return; if (m.is_ite(e1) || m.is_ite(e2)) return; diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index ad632143b..d293aa45a 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -482,7 +482,7 @@ bool theory_seq::fixed_length(expr* len_e, bool is_zero) { expr_ref seq(e, m), head(m), tail(m); if (lo.is_zero()) { - seq = m_util.str.mk_empty(m.get_sort(e)); + seq = m_util.str.mk_empty(e->get_sort()); } else if (!is_zero) { unsigned _lo = lo.get_unsigned(); @@ -1934,7 +1934,7 @@ model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) { expr* x = nullptr, *y = nullptr, *z = nullptr; if (false && m_util.str.is_concat(e, x, y) && m_util.str.is_unit(x, z) && ctx.e_internalized(z) && ctx.e_internalized(y)) { - sort* srt = m.get_sort(e); + sort* srt = e->get_sort(); seq_value_proc* sv = alloc(seq_value_proc, *this, n, srt); sv->add_unit(ctx.get_enode(z)); sv->add_string(y); @@ -1946,7 +1946,7 @@ model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) { SASSERT(m_todo.empty()); m_todo.push_back(e); get_ite_concat(m_concat, m_todo); - sort* srt = m.get_sort(e); + sort* srt = e->get_sort(); seq_value_proc* sv = alloc(seq_value_proc, *this, n, srt); unsigned end = m_concat.size(); @@ -2753,7 +2753,7 @@ literal theory_seq::mk_eq_empty(expr* _e, bool phase) { return false_literal; } } - emp = m_util.str.mk_empty(m.get_sort(e)); + emp = m_util.str.mk_empty(e->get_sort()); literal lit = mk_eq(e, emp, false); ctx.force_phase(phase?lit:~lit); diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 1d46b49c7..28161aea4 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -311,7 +311,7 @@ namespace smt { enode * en = ensure_enode(e); theory_var v = mk_var(en); (void)v; TRACE("str", tout << "refresh " << mk_pp(e, get_manager()) << ": v#" << v << std::endl;); - if (m.get_sort(e) == u.str.mk_string_sort()) { + if (e->get_sort() == u.str.mk_string_sort()) { m_basicstr_axiom_todo.push_back(en); } } @@ -6771,7 +6771,7 @@ namespace smt { bool theory_str::is_var(expr * e) const { ast_manager & m = get_manager(); - sort * ex_sort = m.get_sort(e); + sort * ex_sort = e->get_sort(); sort * str_sort = u.str.mk_string_sort(); // non-string-sort terms cannot be string variables if (ex_sort != str_sort) return false; diff --git a/src/solver/check_logic.cpp b/src/solver/check_logic.cpp index b35e49665..f2a8dbf98 100644 --- a/src/solver/check_logic.cpp +++ b/src/solver/check_logic.cpp @@ -273,7 +273,7 @@ struct check_logic::imp { void operator()(var * n) { if (!m_quantifiers) fail("logic does not support quantifiers"); - check_sort(m.get_sort(n)); + check_sort(n->get_sort()); } bool is_int(expr * t) { @@ -345,7 +345,7 @@ struct check_logic::imp { } bool is_arith(expr * t) const { - return m.get_sort(t)->get_family_id() == m_a_util.get_family_id(); + return t->get_sort()->get_family_id() == m_a_util.get_family_id(); } bool is_offset(app * t) { @@ -425,7 +425,7 @@ struct check_logic::imp { } void operator()(app * n) { - sort * s = m.get_sort(n); + sort * s = n->get_sort(); check_sort(s); func_decl * f = n->get_decl(); family_id fid = f->get_family_id(); diff --git a/src/tactic/arith/bv2real_rewriter.cpp b/src/tactic/arith/bv2real_rewriter.cpp index 2398a2a32..bb8c17f33 100644 --- a/src/tactic/arith/bv2real_rewriter.cpp +++ b/src/tactic/arith/bv2real_rewriter.cpp @@ -114,7 +114,7 @@ expr* bv2real_util::mk_bv2real_c(expr* s, expr* t, rational const& d, rational c sig.m_r = r; func_decl* f; if (!m_sig2decl.find(sig, f)) { - sort* domain[2] = { m_manager.get_sort(s), m_manager.get_sort(t) }; + sort* domain[2] = { s->get_sort(), t->get_sort() }; sort* real = m_arith.mk_real(); f = m_manager.mk_fresh_func_decl("bv2real", "", 2, domain, real); m_decls.push_back(f); diff --git a/src/tactic/arith/fix_dl_var_tactic.cpp b/src/tactic/arith/fix_dl_var_tactic.cpp index 08c8376c8..c5d119685 100644 --- a/src/tactic/arith/fix_dl_var_tactic.cpp +++ b/src/tactic/arith/fix_dl_var_tactic.cpp @@ -51,7 +51,7 @@ class fix_dl_var_tactic : public tactic { } bool is_arith(expr * n) { - sort * s = m.get_sort(n); + sort * s = n->get_sort(); return s->get_family_id() == m_util.get_family_id(); } diff --git a/src/tactic/arith/fm_tactic.cpp b/src/tactic/arith/fm_tactic.cpp index 0c6945054..c57a4900c 100644 --- a/src/tactic/arith/fm_tactic.cpp +++ b/src/tactic/arith/fm_tactic.cpp @@ -802,7 +802,7 @@ class fm_tactic : public tactic { forbidden_proc(imp & o):m_owner(o) {} void operator()(::var * n) {} void operator()(app * n) { - if (is_uninterp_const(n) && m_owner.m.get_sort(n)->get_family_id() == m_owner.m_util.get_family_id()) { + if (is_uninterp_const(n) && n->get_sort()->get_family_id() == m_owner.m_util.get_family_id()) { m_owner.m_forbidden_set.insert(n->get_decl()); } } diff --git a/src/tactic/arith/lia2pb_tactic.cpp b/src/tactic/arith/lia2pb_tactic.cpp index 86e11668f..93b387d0e 100644 --- a/src/tactic/arith/lia2pb_tactic.cpp +++ b/src/tactic/arith/lia2pb_tactic.cpp @@ -134,7 +134,7 @@ class lia2pb_tactic : public tactic { } } else { - sort * s = m_owner.m.get_sort(n); + sort * s = n->get_sort(); if (s->get_family_id() == m_owner.m_util.get_family_id()) throw_failed(n); } diff --git a/src/tactic/arith/normalize_bounds_tactic.cpp b/src/tactic/arith/normalize_bounds_tactic.cpp index a4673b992..957859cc7 100644 --- a/src/tactic/arith/normalize_bounds_tactic.cpp +++ b/src/tactic/arith/normalize_bounds_tactic.cpp @@ -104,7 +104,7 @@ class normalize_bounds_tactic : public tactic { for (expr * x : m_bm) { if (is_target(x, val)) { num_norm_bounds++; - sort * s = m.get_sort(x); + sort * s = x->get_sort(); app * x_prime = m.mk_fresh_const(nullptr, s); expr * def = m_util.mk_add(x_prime, m_util.mk_numeral(val, s)); subst.insert(x, def); diff --git a/src/tactic/arith/probe_arith.cpp b/src/tactic/arith/probe_arith.cpp index 1459af244..8a8dc9520 100644 --- a/src/tactic/arith/probe_arith.cpp +++ b/src/tactic/arith/probe_arith.cpp @@ -136,7 +136,7 @@ struct has_nlmul { has_nlmul(ast_manager& m):m(m), a(m) {} void throw_found(expr* e) { - TRACE("probe", tout << expr_ref(e, m) << ": " << sort_ref(m.get_sort(e), m) << "\n";); + TRACE("probe", tout << expr_ref(e, m) << ": " << sort_ref(e->get_sort(), m) << "\n";); throw found(); } @@ -356,7 +356,7 @@ static bool is_lp(goal const & g) { while (m.is_not(f, f)) sign = !sign; if (m.is_eq(f) && !sign) { - if (m.get_sort(to_app(f)->get_arg(0))->get_family_id() != u.get_family_id()) + if (to_app(f)->get_arg(0)->get_sort()->get_family_id() != u.get_family_id()) return false; continue; } @@ -438,7 +438,7 @@ struct is_non_nira_functor { is_non_nira_functor(ast_manager & _m, bool _int, bool _real, bool _quant, bool linear):m(_m), u(m), m_int(_int), m_real(_real), m_quant(_quant), m_linear(linear) {} void throw_found(expr* e) { - TRACE("probe", tout << expr_ref(e, m) << ": " << sort_ref(m.get_sort(e), m) << "\n";); + TRACE("probe", tout << expr_ref(e, m) << ": " << sort_ref(e->get_sort(), m) << "\n";); throw found(); } diff --git a/src/tactic/bv/bv_size_reduction_tactic.cpp b/src/tactic/bv/bv_size_reduction_tactic.cpp index 949a963ea..5b9a4b21e 100644 --- a/src/tactic/bv/bv_size_reduction_tactic.cpp +++ b/src/tactic/bv/bv_size_reduction_tactic.cpp @@ -217,7 +217,7 @@ public: return; } else if (l == u) { - new_def = m_util.mk_numeral(l, m.get_sort(v)); + new_def = m_util.mk_numeral(l, v->get_sort()); } else { // l < u @@ -312,7 +312,7 @@ public: return; } else if (l == u) { - new_def = m_util.mk_numeral(l, m.get_sort(v)); + new_def = m_util.mk_numeral(l, v->get_sort()); } else { // 0 <= l <= v <= u diff --git a/src/tactic/bv/bvarray2uf_rewriter.cpp b/src/tactic/bv/bvarray2uf_rewriter.cpp index f4f626349..014edc3e7 100644 --- a/src/tactic/bv/bvarray2uf_rewriter.cpp +++ b/src/tactic/bv/bvarray2uf_rewriter.cpp @@ -55,7 +55,7 @@ bvarray2uf_rewriter_cfg::~bvarray2uf_rewriter_cfg() { void bvarray2uf_rewriter_cfg::reset() {} sort * bvarray2uf_rewriter_cfg::get_index_sort(expr * e) { - return get_index_sort(m_manager.get_sort(e)); + return get_index_sort(e->get_sort()); } sort * bvarray2uf_rewriter_cfg::get_index_sort(sort * s) { @@ -71,7 +71,7 @@ sort * bvarray2uf_rewriter_cfg::get_index_sort(sort * s) { } sort * bvarray2uf_rewriter_cfg::get_value_sort(expr * e) { - return get_value_sort(m_manager.get_sort(e)); + return get_value_sort(e->get_sort()); } sort * bvarray2uf_rewriter_cfg::get_value_sort(sort * s) { @@ -82,7 +82,7 @@ sort * bvarray2uf_rewriter_cfg::get_value_sort(sort * s) { } bool bvarray2uf_rewriter_cfg::is_bv_array(expr * e) { - return is_bv_array(m_manager.get_sort(e)); + return is_bv_array(e->get_sort()); } bool bvarray2uf_rewriter_cfg::is_bv_array(sort * s) { diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp index 4ecfb2f57..ab0487a83 100644 --- a/src/tactic/core/elim_uncnstr_tactic.cpp +++ b/src/tactic/core/elim_uncnstr_tactic.cpp @@ -92,7 +92,7 @@ class elim_uncnstr_tactic : public tactic { return false; // variable already existed for this application } - v = m().mk_fresh_const(nullptr, m().get_sort(t)); + v = m().mk_fresh_const(nullptr, t->get_sort()); TRACE("elim_uncnstr_bug", tout << "eliminating:\n" << mk_ismt2_pp(t, m()) << "\n";); TRACE("elim_uncnstr_bug_ll", tout << "eliminating:\n" << mk_bounded_pp(t, m()) << "\n";); m_fresh_vars.push_back(v); @@ -131,7 +131,7 @@ class elim_uncnstr_tactic : public tactic { // return a term that is different from t. bool mk_diff(expr * t, expr_ref & r) { - sort * s = m().get_sort(t); + sort * s = t->get_sort(); if (m().is_bool(s)) { r = m().mk_not(t); return true; @@ -221,7 +221,7 @@ class elim_uncnstr_tactic : public tactic { return nullptr; } - sort * s = m().get_sort(arg1); + sort * s = arg1->get_sort(); // Remark: // I currently do not support unconstrained vars that have @@ -359,7 +359,7 @@ class elim_uncnstr_tactic : public tactic { return u; // v = ite(u, t, t + 1) if le // v = ite(u, t, t - 1) if !le - add_def(v, m().mk_ite(u, t, m_a_util.mk_add(t, m_a_util.mk_numeral(rational(le ? 1 : -1), m().get_sort(arg1))))); + add_def(v, m().mk_ite(u, t, m_a_util.mk_add(t, m_a_util.mk_numeral(rational(le ? 1 : -1), arg1->get_sort())))); return u; } @@ -405,7 +405,7 @@ class elim_uncnstr_tactic : public tactic { app * process_arith_mul(func_decl * f, unsigned num, expr * const * args) { if (num == 0) return nullptr; - sort * s = m().get_sort(args[0]); + sort * s = args[0]->get_sort(); if (uncnstr(num, args)) { app * r; if (!mk_fresh_uncnstr_var_for(f, num, args, r)) @@ -455,7 +455,7 @@ class elim_uncnstr_tactic : public tactic { if (num == 0) return nullptr; if (uncnstr(num, args)) { - sort * s = m().get_sort(args[0]); + sort * s = args[0]->get_sort(); app * r; if (!mk_fresh_uncnstr_var_for(f, num, args, r)) return r; @@ -474,7 +474,7 @@ class elim_uncnstr_tactic : public tactic { app * r; if (!mk_fresh_uncnstr_var_for(f, num, args, r)) return r; - sort * s = m().get_sort(args[1]); + sort * s = args[1]->get_sort(); if (m_mc) add_def(args[1], m_bv_util.mk_bv_mul(m_bv_util.mk_numeral(inv, s), r)); return r; @@ -492,7 +492,7 @@ class elim_uncnstr_tactic : public tactic { return r; unsigned high = m_bv_util.get_extract_high(f); unsigned low = m_bv_util.get_extract_low(f); - unsigned bv_size = m_bv_util.get_bv_size(m().get_sort(arg)); + unsigned bv_size = m_bv_util.get_bv_size(arg->get_sort()); if (bv_size == high - low + 1) { add_def(arg, r); } @@ -510,7 +510,7 @@ class elim_uncnstr_tactic : public tactic { app * process_bv_div(func_decl * f, expr * arg1, expr * arg2) { if (uncnstr(arg1) && uncnstr(arg2)) { - sort * s = m().get_sort(arg1); + sort * s = arg1->get_sort(); app * r; if (!mk_fresh_uncnstr_var_for(f, arg1, arg2, r)) return r; @@ -630,7 +630,7 @@ class elim_uncnstr_tactic : public tactic { return nullptr; case OP_BOR: if (num > 0 && uncnstr(num, args)) { - sort * s = m().get_sort(args[0]); + sort * s = args[0]->get_sort(); app * r; if (!mk_fresh_uncnstr_var_for(f, num, args, r)) return r; @@ -652,7 +652,7 @@ class elim_uncnstr_tactic : public tactic { app * r; if (!mk_fresh_uncnstr_var_for(f, num, args, r)) return r; - sort * s = m().get_sort(args[0]); + sort * s = args[0]->get_sort(); if (m_mc) add_def(args[0], m_ar_util.mk_const_array(s, r)); return r; diff --git a/src/tactic/core/reduce_invertible_tactic.cpp b/src/tactic/core/reduce_invertible_tactic.cpp index a9b3b71cd..06fde2757 100644 --- a/src/tactic/core/reduce_invertible_tactic.cpp +++ b/src/tactic/core/reduce_invertible_tactic.cpp @@ -409,7 +409,7 @@ private: // diagonal functions for other types depend on theory. return false; } - else if (is_var(v) && is_non_singleton_sort(m.get_sort(v))) { + else if (is_var(v) && is_non_singleton_sort(v->get_sort())) { new_v = m.mk_var(to_var(v)->get_idx(), m.mk_bool_sort()); return true; } @@ -484,7 +484,7 @@ private: TRACE("invertible_tactic", tout << mk_pp(v, m) << " " << mk_pp(p, m) << "\n";); t.mark_inverted(p); sub.insert(p, new_v); - new_sorts[i] = m.get_sort(new_v); + new_sorts[i] = new_v->get_sort(); has_new_var |= new_v != v; } } diff --git a/src/tactic/fd_solver/smtfd_solver.cpp b/src/tactic/fd_solver/smtfd_solver.cpp index 89ec15b05..d6a92b77d 100644 --- a/src/tactic/fd_solver/smtfd_solver.cpp +++ b/src/tactic/fd_solver/smtfd_solver.cpp @@ -1019,7 +1019,7 @@ namespace smtfd { expr_ref vA = eval_abs(arg); table& tT = ast2table(vT, m.get_sort(t)); // select table of t - table& tA = ast2table(vA, m.get_sort(arg)); // select table of arg + table& tA = ast2table(vA, arg->get_sort()); // select table of arg if (vT == vA) { return; @@ -1380,7 +1380,7 @@ namespace smtfd { } void register_value(expr* e) { - sort* s = m.get_sort(e); + sort* s = e->get_sort(); obj_hashtable* values = nullptr; if (!m_fresh.find(s, values)) { values = alloc(obj_hashtable); @@ -1478,7 +1478,7 @@ namespace smtfd { break; } expr* t = nullptr; - if (m_val2term.find(val, m.get_sort(v), t)) { + if (m_val2term.find(val, v->get_sort(), t)) { val = t; } else { diff --git a/src/tactic/generic_model_converter.cpp b/src/tactic/generic_model_converter.cpp index 930328085..db7e879b6 100644 --- a/src/tactic/generic_model_converter.cpp +++ b/src/tactic/generic_model_converter.cpp @@ -35,7 +35,7 @@ generic_model_converter::~generic_model_converter() { void generic_model_converter::add(func_decl * d, expr* e) { VERIFY(e); - VERIFY(d->get_range() == m.get_sort(e)); + VERIFY(d->get_range() == e->get_sort()); m_first_idx.insert_if_not_there(d, m_entries.size()); m_entries.push_back(entry(d, e, m, ADD)); } diff --git a/src/tactic/horn_subsume_model_converter.cpp b/src/tactic/horn_subsume_model_converter.cpp index fa3e82e64..869cf7b01 100644 --- a/src/tactic/horn_subsume_model_converter.cpp +++ b/src/tactic/horn_subsume_model_converter.cpp @@ -73,7 +73,7 @@ bool horn_subsume_model_converter::mk_horn( for (unsigned i = 0; i < arity; ++i) { expr* arg = head->get_arg(i); var_ref v(m); - v = m.mk_var(fv.size()+i, m.get_sort(arg)); + v = m.mk_var(fv.size()+i, arg->get_sort()); if (is_var(arg)) { unsigned w = to_var(arg)->get_idx(); diff --git a/src/tactic/model_converter.cpp b/src/tactic/model_converter.cpp index c50904ffb..2ac23f838 100644 --- a/src/tactic/model_converter.cpp +++ b/src/tactic/model_converter.cpp @@ -27,7 +27,7 @@ void model_converter::display_add(std::ostream& out, ast_manager& m, func_decl* VERIFY(e); smt2_pp_environment_dbg env(m); smt2_pp_environment* _env = m_env ? m_env : &env; - VERIFY(f->get_range() == m.get_sort(e)); + VERIFY(f->get_range() == e->get_sort()); ast_smt2_pp(out, f, e, *_env, params_ref(), 0, "model-add") << "\n"; } diff --git a/src/tactic/probe.cpp b/src/tactic/probe.cpp index 432c9d123..fe813c28f 100644 --- a/src/tactic/probe.cpp +++ b/src/tactic/probe.cpp @@ -430,7 +430,7 @@ class num_consts_probe : public probe { m_counter++; } else { - if (m.get_sort(n)->get_family_id() == m_fid) + if (n->get_sort()->get_family_id() == m_fid) m_counter++; } } diff --git a/src/tactic/sls/sls_evaluator.h b/src/tactic/sls/sls_evaluator.h index 91fee752c..8523c80a9 100644 --- a/src/tactic/sls/sls_evaluator.h +++ b/src/tactic/sls/sls_evaluator.h @@ -507,7 +507,7 @@ public: for (unsigned i = 0; i < n_args; i++) { expr * arg = a->get_arg(i); const mpz & v = m_tracker.get_value(arg); - m_temp_exprs.push_back(m_tracker.mpz2value(m_manager.get_sort(arg), v)); + m_temp_exprs.push_back(m_tracker.mpz2value(arg->get_sort(), v)); } expr_ref q(m_manager), temp(m_manager); q = m_manager.mk_app(a->get_decl(), m_temp_exprs.size(), m_temp_exprs.c_ptr()); diff --git a/src/test/egraph.cpp b/src/test/egraph.cpp index 54aceedad..508384f8f 100644 --- a/src/test/egraph.cpp +++ b/src/test/egraph.cpp @@ -16,7 +16,7 @@ static expr_ref mk_const(ast_manager& m, char const* name, sort* s) { static expr_ref mk_app(char const* name, expr_ref const& arg, sort* s) { ast_manager& m = arg.m(); - func_decl_ref f(m.mk_func_decl(symbol(name), m.get_sort(arg), s), m); + func_decl_ref f(m.mk_func_decl(symbol(name), arg->get_sort(), s), m); return expr_ref(m.mk_app(f, arg.get()), m); } diff --git a/src/test/fuzzing/expr_rand.cpp b/src/test/fuzzing/expr_rand.cpp index a15c8e0e1..8d20a4e92 100644 --- a/src/test/fuzzing/expr_rand.cpp +++ b/src/test/fuzzing/expr_rand.cpp @@ -34,7 +34,7 @@ void expr_rand::add_func_decl(func_decl* f) { } void expr_rand::add_expr(expr* t) { - sort* s = m_manager.get_sort(t); + sort* s = t->get_sort(); expr_ref_vector* vals = nullptr; if (!m_nodes.find(s, vals)) { vals = alloc(expr_ref_vector, m_manager); diff --git a/src/test/quant_solve.cpp b/src/test/quant_solve.cpp index d0c616166..3acdd0692 100644 --- a/src/test/quant_solve.cpp +++ b/src/test/quant_solve.cpp @@ -65,7 +65,7 @@ static void validate_quant_solutions(app* x, expr* fml, expr_ref_vector& guards) expr_abstract(m, 0, 1, &_x, fml, fml2); std::cout << mk_pp(fml2, m) << "\n"; symbol name(x->get_decl()->get_name()); - sort* s = m.get_sort(x); + sort* s = x->get_sort(); fml2 = m.mk_exists(1, &s, &name, fml2); std::cout << mk_pp(fml2, m) << "\n"; tmp = m.mk_not(m.mk_iff(fml2, tmp));