From a6ef99d56e2dc4bc3f2e184828014a418205b5fd Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Sun, 4 Apr 2021 18:13:52 +0100 Subject: [PATCH] constify ids of builtin AST families + remove some dead code --- src/ast/arith_decl_plugin.cpp | 37 +++-- src/ast/arith_decl_plugin.h | 200 ++++++++++++----------- src/ast/ast.cpp | 219 +++++++++---------------- src/ast/ast.h | 293 ++++++++++++++-------------------- 4 files changed, 314 insertions(+), 435 deletions(-) diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp index 854e05732aa..3936808973f 100644 --- a/src/ast/arith_decl_plugin.cpp +++ b/src/ast/arith_decl_plugin.cpp @@ -696,7 +696,7 @@ expr * arith_decl_plugin::get_some_value(sort * s) { } bool arith_recognizers::is_numeral(expr const * n, rational & val, bool & is_int) const { - if (!is_app_of(n, m_afid, OP_NUM)) + if (!is_app_of(n, arith_family_id, OP_NUM)) return false; func_decl * decl = to_app(n)->get_decl(); val = decl->get_parameter(0).get_rational(); @@ -706,7 +706,7 @@ bool arith_recognizers::is_numeral(expr const * n, rational & val, bool & is_int bool arith_recognizers::is_irrational_algebraic_numeral(expr const * n) const { - return is_app(n) && to_app(n)->is_app_of(m_afid, OP_IRRATIONAL_ALGEBRAIC_NUM); + return is_app(n) && to_app(n)->is_app_of(arith_family_id, OP_IRRATIONAL_ALGEBRAIC_NUM); } @@ -740,18 +740,17 @@ bool arith_recognizers::is_int_expr(expr const *e) const { } arith_util::arith_util(ast_manager & m): - arith_recognizers(m.mk_family_id("arith")), m_manager(m), m_plugin(nullptr) { } void arith_util::init_plugin() { SASSERT(m_plugin == 0); - m_plugin = static_cast(m_manager.get_plugin(m_afid)); + m_plugin = static_cast(m_manager.get_plugin(arith_family_id)); } bool arith_util::is_irrational_algebraic_numeral2(expr const * n, algebraic_numbers::anum & val) { - if (!is_app_of(n, m_afid, OP_IRRATIONAL_ALGEBRAIC_NUM)) + if (!is_app_of(n, arith_family_id, OP_IRRATIONAL_ALGEBRAIC_NUM)) return false; am().set(val, to_irrational_algebraic_numeral(n)); return true; @@ -806,26 +805,26 @@ expr_ref arith_util::mk_add_simplify(unsigned sz, expr* const* args) { bool arith_util::is_considered_uninterpreted(func_decl* f, unsigned n, expr* const* args, func_decl_ref& f_out) { rational r; - if (is_decl_of(f, m_afid, OP_DIV) && n == 2 && is_numeral(args[1], r) && r.is_zero()) { + if (is_decl_of(f, arith_family_id, OP_DIV) && n == 2 && is_numeral(args[1], r) && r.is_zero()) { f_out = mk_div0(); return true; } - if (is_decl_of(f, m_afid, OP_IDIV) && n == 2 && is_numeral(args[1], r) && r.is_zero()) { + if (is_decl_of(f, arith_family_id, OP_IDIV) && n == 2 && is_numeral(args[1], r) && r.is_zero()) { sort* rs[2] = { mk_int(), mk_int() }; - f_out = m_manager.mk_func_decl(m_afid, OP_IDIV0, 0, nullptr, 2, rs, mk_int()); + f_out = m_manager.mk_func_decl(arith_family_id, OP_IDIV0, 0, nullptr, 2, rs, mk_int()); return true; } - if (is_decl_of(f, m_afid, OP_MOD) && n == 2 && is_numeral(args[1], r) && r.is_zero()) { + if (is_decl_of(f, arith_family_id, OP_MOD) && n == 2 && is_numeral(args[1], r) && r.is_zero()) { sort* rs[2] = { mk_int(), mk_int() }; - f_out = m_manager.mk_func_decl(m_afid, OP_MOD0, 0, nullptr, 2, rs, mk_int()); + f_out = m_manager.mk_func_decl(arith_family_id, OP_MOD0, 0, nullptr, 2, rs, mk_int()); return true; } - if (is_decl_of(f, m_afid, OP_REM) && n == 2 && is_numeral(args[1], r) && r.is_zero()) { + if (is_decl_of(f, arith_family_id, OP_REM) && n == 2 && is_numeral(args[1], r) && r.is_zero()) { sort* rs[2] = { mk_int(), mk_int() }; - f_out = m_manager.mk_func_decl(m_afid, OP_REM0, 0, nullptr, 2, rs, mk_int()); + f_out = m_manager.mk_func_decl(arith_family_id, OP_REM0, 0, nullptr, 2, rs, mk_int()); return true; } - if (is_decl_of(f, m_afid, OP_POWER) && n == 2 && is_numeral(args[1], r) && r.is_zero() && is_numeral(args[0], r) && r.is_zero()) { + if (is_decl_of(f, arith_family_id, OP_POWER) && n == 2 && is_numeral(args[1], r) && r.is_zero() && is_numeral(args[0], r) && r.is_zero()) { f_out = is_int(args[0]) ? mk_ipower0() : mk_rpower0(); return true; } @@ -837,33 +836,33 @@ bool arith_util::is_considered_uninterpreted(func_decl* f, unsigned n, expr* con func_decl* arith_util::mk_ipower0() { sort* s = mk_int(); sort* rs[2] = { s, s }; - return m_manager.mk_func_decl(m_afid, OP_POWER0, 0, nullptr, 2, rs, s); + return m_manager.mk_func_decl(arith_family_id, OP_POWER0, 0, nullptr, 2, rs, s); } func_decl* arith_util::mk_rpower0() { sort* s = mk_real(); sort* rs[2] = { s, s }; - return m_manager.mk_func_decl(m_afid, OP_POWER0, 0, nullptr, 2, rs, s); + return m_manager.mk_func_decl(arith_family_id, OP_POWER0, 0, nullptr, 2, rs, s); } func_decl* arith_util::mk_div0() { sort* rs[2] = { mk_real(), mk_real() }; - return m_manager.mk_func_decl(m_afid, OP_DIV0, 0, nullptr, 2, rs, mk_real()); + return m_manager.mk_func_decl(arith_family_id, OP_DIV0, 0, nullptr, 2, rs, mk_real()); } func_decl* arith_util::mk_idiv0() { sort* rs[2] = { mk_int(), mk_int() }; - return m_manager.mk_func_decl(m_afid, OP_IDIV0, 0, nullptr, 2, rs, mk_int()); + return m_manager.mk_func_decl(arith_family_id, OP_IDIV0, 0, nullptr, 2, rs, mk_int()); } func_decl* arith_util::mk_rem0() { sort* rs[2] = { mk_int(), mk_int() }; - return m_manager.mk_func_decl(m_afid, OP_REM0, 0, nullptr, 2, rs, mk_int()); + return m_manager.mk_func_decl(arith_family_id, OP_REM0, 0, nullptr, 2, rs, mk_int()); } func_decl* arith_util::mk_mod0() { sort* rs[2] = { mk_int(), mk_int() }; - return m_manager.mk_func_decl(m_afid, OP_MOD0, 0, nullptr, 2, rs, mk_int()); + return m_manager.mk_func_decl(arith_family_id, OP_MOD0, 0, nullptr, 2, rs, mk_int()); } bool arith_util::is_bounded(expr* n) const { diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h index 444af81b063..e61d4a716c9 100644 --- a/src/ast/arith_decl_plugin.h +++ b/src/ast/arith_decl_plugin.h @@ -233,14 +233,10 @@ class arith_decl_plugin : public decl_plugin { executed in different threads. */ class arith_recognizers { -protected: - family_id m_afid; public: - arith_recognizers(family_id id):m_afid(id) {} - - family_id get_family_id() const { return m_afid; } + family_id get_family_id() const { return arith_family_id; } - bool is_arith_expr(expr const * n) const { return is_app(n) && to_app(n)->get_family_id() == m_afid; } + bool is_arith_expr(expr const * n) const { return is_app(n) && to_app(n)->get_family_id() == arith_family_id; } bool is_irrational_algebraic_numeral(expr const * n) const; bool is_unsigned(expr const * n, unsigned& u) const { rational val; @@ -249,7 +245,7 @@ class arith_recognizers { } bool is_numeral(expr const * n, rational & val, bool & is_int) const; bool is_numeral(expr const * n, rational & val) const { bool is_int; return is_numeral(n, val, is_int); } - bool is_numeral(expr const * n) const { return is_app_of(n, m_afid, OP_NUM); } + bool is_numeral(expr const * n) const { return is_app_of(n, arith_family_id, OP_NUM); } bool is_zero(expr const * n) const { rational val; return is_numeral(n, val) && val.is_zero(); } bool is_minus_one(expr * n) const { rational tmp; return is_numeral(n, tmp) && tmp.is_minus_one(); } // return true if \c n is a term of the form (* -1 r) @@ -263,58 +259,58 @@ class arith_recognizers { bool is_int_expr(expr const * e) const; - bool is_le(expr const * n) const { return is_app_of(n, m_afid, OP_LE); } - bool is_ge(expr const * n) const { return is_app_of(n, m_afid, OP_GE); } - bool is_lt(expr const * n) const { return is_app_of(n, m_afid, OP_LT); } - bool is_gt(expr const * n) const { return is_app_of(n, m_afid, OP_GT); } - bool is_le(func_decl const * n) const { return is_decl_of(n, m_afid, OP_LE); } - bool is_ge(func_decl const * n) const { return is_decl_of(n, m_afid, OP_GE); } - bool is_lt(func_decl const * n) const { return is_decl_of(n, m_afid, OP_LT); } - bool is_gt(func_decl const * n) const { return is_decl_of(n, m_afid, OP_GT); } - - bool is_div0(func_decl const * n) const { return is_decl_of(n, m_afid, OP_DIV0); } - bool is_idiv0(func_decl const * n) const { return is_decl_of(n, m_afid, OP_IDIV0); } - bool is_rem0(func_decl const * n) const { return is_decl_of(n, m_afid, OP_REM0); } - bool is_mod0(func_decl const * n) const { return is_decl_of(n, m_afid, OP_MOD0); } - bool is_power0(func_decl const * n) const { return is_decl_of(n, m_afid, OP_POWER0); } - - bool is_add(expr const * n) const { return is_app_of(n, m_afid, OP_ADD); } - bool is_sub(expr const * n) const { return is_app_of(n, m_afid, OP_SUB); } - bool is_uminus(expr const * n) const { return is_app_of(n, m_afid, OP_UMINUS); } - bool is_mul(expr const * n) const { return is_app_of(n, m_afid, OP_MUL); } - bool is_div(expr const * n) const { return is_app_of(n, m_afid, OP_DIV); } - bool is_div0(expr const * n) const { return is_app_of(n, m_afid, OP_DIV0); } - bool is_idiv(expr const * n) const { return is_app_of(n, m_afid, OP_IDIV); } - bool is_idiv0(expr const * n) const { return is_app_of(n, m_afid, OP_IDIV0); } - bool is_mod(expr const * n) const { return is_app_of(n, m_afid, OP_MOD); } - bool is_rem(expr const * n) const { return is_app_of(n, m_afid, OP_REM); } - bool is_mod0(expr const * n) const { return is_app_of(n, m_afid, OP_MOD0); } - bool is_rem0(expr const * n) const { return is_app_of(n, m_afid, OP_REM0); } - bool is_to_real(expr const * n) const { return is_app_of(n, m_afid, OP_TO_REAL); } - bool is_to_int(expr const * n) const { return is_app_of(n, m_afid, OP_TO_INT); } - bool is_is_int(expr const * n) const { return is_app_of(n, m_afid, OP_IS_INT); } - bool is_power(expr const * n) const { return is_app_of(n, m_afid, OP_POWER); } - bool is_power0(expr const * n) const { return is_app_of(n, m_afid, OP_POWER0); } - - bool is_int(sort const * s) const { return is_sort_of(s, m_afid, INT_SORT); } + bool is_le(expr const * n) const { return is_app_of(n, arith_family_id, OP_LE); } + bool is_ge(expr const * n) const { return is_app_of(n, arith_family_id, OP_GE); } + bool is_lt(expr const * n) const { return is_app_of(n, arith_family_id, OP_LT); } + bool is_gt(expr const * n) const { return is_app_of(n, arith_family_id, OP_GT); } + bool is_le(func_decl const * n) const { return is_decl_of(n, arith_family_id, OP_LE); } + bool is_ge(func_decl const * n) const { return is_decl_of(n, arith_family_id, OP_GE); } + bool is_lt(func_decl const * n) const { return is_decl_of(n, arith_family_id, OP_LT); } + bool is_gt(func_decl const * n) const { return is_decl_of(n, arith_family_id, OP_GT); } + + bool is_div0(func_decl const * n) const { return is_decl_of(n, arith_family_id, OP_DIV0); } + bool is_idiv0(func_decl const * n) const { return is_decl_of(n, arith_family_id, OP_IDIV0); } + bool is_rem0(func_decl const * n) const { return is_decl_of(n, arith_family_id, OP_REM0); } + bool is_mod0(func_decl const * n) const { return is_decl_of(n, arith_family_id, OP_MOD0); } + bool is_power0(func_decl const * n) const { return is_decl_of(n, arith_family_id, OP_POWER0); } + + bool is_add(expr const * n) const { return is_app_of(n, arith_family_id, OP_ADD); } + bool is_sub(expr const * n) const { return is_app_of(n, arith_family_id, OP_SUB); } + bool is_uminus(expr const * n) const { return is_app_of(n, arith_family_id, OP_UMINUS); } + bool is_mul(expr const * n) const { return is_app_of(n, arith_family_id, OP_MUL); } + bool is_div(expr const * n) const { return is_app_of(n, arith_family_id, OP_DIV); } + bool is_div0(expr const * n) const { return is_app_of(n, arith_family_id, OP_DIV0); } + bool is_idiv(expr const * n) const { return is_app_of(n, arith_family_id, OP_IDIV); } + bool is_idiv0(expr const * n) const { return is_app_of(n, arith_family_id, OP_IDIV0); } + bool is_mod(expr const * n) const { return is_app_of(n, arith_family_id, OP_MOD); } + bool is_rem(expr const * n) const { return is_app_of(n, arith_family_id, OP_REM); } + bool is_mod0(expr const * n) const { return is_app_of(n, arith_family_id, OP_MOD0); } + bool is_rem0(expr const * n) const { return is_app_of(n, arith_family_id, OP_REM0); } + bool is_to_real(expr const * n) const { return is_app_of(n, arith_family_id, OP_TO_REAL); } + bool is_to_int(expr const * n) const { return is_app_of(n, arith_family_id, OP_TO_INT); } + bool is_is_int(expr const * n) const { return is_app_of(n, arith_family_id, OP_IS_INT); } + bool is_power(expr const * n) const { return is_app_of(n, arith_family_id, OP_POWER); } + bool is_power0(expr const * n) const { return is_app_of(n, arith_family_id, OP_POWER0); } + + bool is_int(sort const * s) const { return is_sort_of(s, arith_family_id, INT_SORT); } bool is_int(expr const * n) const { return is_int(n->get_sort()); } - bool is_real(sort const * s) const { return is_sort_of(s, m_afid, REAL_SORT); } + bool is_real(sort const * s) const { return is_sort_of(s, arith_family_id, REAL_SORT); } bool is_real(expr const * n) const { return is_real(n->get_sort()); } - bool is_int_real(sort const * s) const { return s->get_family_id() == m_afid; } + bool is_int_real(sort const * s) const { return s->get_family_id() == arith_family_id; } bool is_int_real(expr const * n) const { return is_int_real(n->get_sort()); } - bool is_sin(expr const* n) const { return is_app_of(n, m_afid, OP_SIN); } - bool is_cos(expr const* n) const { return is_app_of(n, m_afid, OP_COS); } - bool is_tan(expr const* n) const { return is_app_of(n, m_afid, OP_TAN); } - bool is_tanh(expr const* n) const { return is_app_of(n, m_afid, OP_TANH); } - bool is_asin(expr const* n) const { return is_app_of(n, m_afid, OP_ASIN); } - bool is_acos(expr const* n) const { return is_app_of(n, m_afid, OP_ACOS); } - bool is_atan(expr const* n) const { return is_app_of(n, m_afid, OP_ATAN); } - bool is_asinh(expr const* n) const { return is_app_of(n, m_afid, OP_ASINH); } - bool is_acosh(expr const* n) const { return is_app_of(n, m_afid, OP_ACOSH); } - bool is_atanh(expr const* n) const { return is_app_of(n, m_afid, OP_ATANH); } - bool is_pi(expr const * arg) const { return is_app_of(arg, m_afid, OP_PI); } - bool is_e(expr const * arg) const { return is_app_of(arg, m_afid, OP_E); } + bool is_sin(expr const* n) const { return is_app_of(n, arith_family_id, OP_SIN); } + bool is_cos(expr const* n) const { return is_app_of(n, arith_family_id, OP_COS); } + bool is_tan(expr const* n) const { return is_app_of(n, arith_family_id, OP_TAN); } + bool is_tanh(expr const* n) const { return is_app_of(n, arith_family_id, OP_TANH); } + bool is_asin(expr const* n) const { return is_app_of(n, arith_family_id, OP_ASIN); } + bool is_acos(expr const* n) const { return is_app_of(n, arith_family_id, OP_ACOS); } + bool is_atan(expr const* n) const { return is_app_of(n, arith_family_id, OP_ATAN); } + bool is_asinh(expr const* n) const { return is_app_of(n, arith_family_id, OP_ASINH); } + bool is_acosh(expr const* n) const { return is_app_of(n, arith_family_id, OP_ACOSH); } + bool is_atanh(expr const* n) const { return is_app_of(n, arith_family_id, OP_ATANH); } + bool is_pi(expr const * arg) const { return is_app_of(arg, arith_family_id, OP_PI); } + bool is_e(expr const * arg) const { return is_app_of(arg, arith_family_id, OP_E); } bool is_non_algebraic(expr const* n) const { return is_sin(n) || is_cos(n) || @@ -388,8 +384,8 @@ class arith_util : public arith_recognizers { bool is_irrational_algebraic_numeral2(expr const * n, algebraic_numbers::anum & val); algebraic_numbers::anum const & to_irrational_algebraic_numeral(expr const * n); - sort * mk_int() { return m_manager.mk_sort(m_afid, INT_SORT); } - sort * mk_real() { return m_manager.mk_sort(m_afid, REAL_SORT); } + sort * mk_int() { return m_manager.mk_sort(arith_family_id, INT_SORT); } + sort * mk_real() { return m_manager.mk_sort(arith_family_id, REAL_SORT); } func_decl* mk_rem0(); func_decl* mk_div0(); @@ -427,57 +423,57 @@ class arith_util : public arith_recognizers { app * mk_real(rational const& r) { return mk_numeral(r, false); } - app * mk_le(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_LE, arg1, arg2); } - app * mk_ge(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_GE, arg1, arg2); } - app * mk_lt(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_LT, arg1, arg2); } - app * mk_gt(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_GT, arg1, arg2); } - app * mk_divides(expr* arg1, expr* arg2) { return m_manager.mk_app(m_afid, OP_IDIVIDES, arg1, arg2); } - - app * mk_add(unsigned num_args, expr * const * args) const { return num_args == 1 && is_app(args[0]) ? to_app(args[0]) : m_manager.mk_app(m_afid, OP_ADD, num_args, args); } - app * mk_add(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_ADD, arg1, arg2); } - app * mk_add(expr * arg1, expr * arg2, expr* arg3) const { return m_manager.mk_app(m_afid, OP_ADD, arg1, arg2, arg3); } + app * mk_le(expr * arg1, expr * arg2) const { return m_manager.mk_app(arith_family_id, OP_LE, arg1, arg2); } + app * mk_ge(expr * arg1, expr * arg2) const { return m_manager.mk_app(arith_family_id, OP_GE, arg1, arg2); } + app * mk_lt(expr * arg1, expr * arg2) const { return m_manager.mk_app(arith_family_id, OP_LT, arg1, arg2); } + app * mk_gt(expr * arg1, expr * arg2) const { return m_manager.mk_app(arith_family_id, OP_GT, arg1, arg2); } + app * mk_divides(expr* arg1, expr* arg2) { return m_manager.mk_app(arith_family_id, OP_IDIVIDES, arg1, arg2); } + + app * mk_add(unsigned num_args, expr * const * args) const { return num_args == 1 && is_app(args[0]) ? to_app(args[0]) : m_manager.mk_app(arith_family_id, OP_ADD, num_args, args); } + app * mk_add(expr * arg1, expr * arg2) const { return m_manager.mk_app(arith_family_id, OP_ADD, arg1, arg2); } + app * mk_add(expr * arg1, expr * arg2, expr* arg3) const { return m_manager.mk_app(arith_family_id, OP_ADD, arg1, arg2, arg3); } app * mk_add(expr_ref_vector const& args) const { return mk_add(args.size(), args.c_ptr()); } - app * mk_sub(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_SUB, arg1, arg2); } - app * mk_sub(unsigned num_args, expr * const * args) const { return m_manager.mk_app(m_afid, OP_SUB, num_args, args); } - app * mk_mul(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_MUL, arg1, arg2); } - app * mk_mul(expr * arg1, expr * arg2, expr* arg3) const { return m_manager.mk_app(m_afid, OP_MUL, arg1, arg2, arg3); } - app * mk_mul(unsigned num_args, expr * const * args) const { return num_args == 1 && is_app(args[0]) ? to_app(args[0]) : m_manager.mk_app(m_afid, OP_MUL, num_args, args); } - app * mk_uminus(expr * arg) const { return m_manager.mk_app(m_afid, OP_UMINUS, arg); } - app * mk_div(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_DIV, arg1, arg2); } - app * mk_idiv(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_IDIV, arg1, arg2); } - app * mk_rem(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_REM, arg1, arg2); } - app * mk_mod(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_MOD, arg1, arg2); } - app * mk_div0(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_DIV0, arg1, arg2); } - app * mk_idiv0(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_IDIV0, arg1, arg2); } - app * mk_rem0(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_REM0, arg1, arg2); } - app * mk_mod0(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_MOD0, arg1, arg2); } - app * mk_to_real(expr * arg1) { return m_manager.mk_app(m_afid, OP_TO_REAL, arg1); } - app * mk_to_int(expr * arg1) { return m_manager.mk_app(m_afid, OP_TO_INT, arg1); } - app * mk_is_int(expr * arg1) { return m_manager.mk_app(m_afid, OP_IS_INT, arg1); } - app * mk_power(expr* arg1, expr* arg2) { return m_manager.mk_app(m_afid, OP_POWER, arg1, arg2); } - app * mk_power0(expr* arg1, expr* arg2) { return m_manager.mk_app(m_afid, OP_POWER0, arg1, arg2); } - - app * mk_sin(expr * arg) { return m_manager.mk_app(m_afid, OP_SIN, arg); } - app * mk_cos(expr * arg) { return m_manager.mk_app(m_afid, OP_COS, arg); } - app * mk_tan(expr * arg) { return m_manager.mk_app(m_afid, OP_TAN, arg); } - app * mk_asin(expr * arg) { return m_manager.mk_app(m_afid, OP_ASIN, arg); } - app * mk_acos(expr * arg) { return m_manager.mk_app(m_afid, OP_ACOS, arg); } - app * mk_atan(expr * arg) { return m_manager.mk_app(m_afid, OP_ATAN, arg); } - - app * mk_sinh(expr * arg) { return m_manager.mk_app(m_afid, OP_SINH, arg); } - app * mk_cosh(expr * arg) { return m_manager.mk_app(m_afid, OP_COSH, arg); } - app * mk_tanh(expr * arg) { return m_manager.mk_app(m_afid, OP_TANH, arg); } - app * mk_asinh(expr * arg) { return m_manager.mk_app(m_afid, OP_ASINH, arg); } - app * mk_acosh(expr * arg) { return m_manager.mk_app(m_afid, OP_ACOSH, arg); } - app * mk_atanh(expr * arg) { return m_manager.mk_app(m_afid, OP_ATANH, arg); } + app * mk_sub(expr * arg1, expr * arg2) const { return m_manager.mk_app(arith_family_id, OP_SUB, arg1, arg2); } + app * mk_sub(unsigned num_args, expr * const * args) const { return m_manager.mk_app(arith_family_id, OP_SUB, num_args, args); } + app * mk_mul(expr * arg1, expr * arg2) const { return m_manager.mk_app(arith_family_id, OP_MUL, arg1, arg2); } + app * mk_mul(expr * arg1, expr * arg2, expr* arg3) const { return m_manager.mk_app(arith_family_id, OP_MUL, arg1, arg2, arg3); } + app * mk_mul(unsigned num_args, expr * const * args) const { return num_args == 1 && is_app(args[0]) ? to_app(args[0]) : m_manager.mk_app(arith_family_id, OP_MUL, num_args, args); } + app * mk_uminus(expr * arg) const { return m_manager.mk_app(arith_family_id, OP_UMINUS, arg); } + app * mk_div(expr * arg1, expr * arg2) { return m_manager.mk_app(arith_family_id, OP_DIV, arg1, arg2); } + app * mk_idiv(expr * arg1, expr * arg2) { return m_manager.mk_app(arith_family_id, OP_IDIV, arg1, arg2); } + app * mk_rem(expr * arg1, expr * arg2) { return m_manager.mk_app(arith_family_id, OP_REM, arg1, arg2); } + app * mk_mod(expr * arg1, expr * arg2) { return m_manager.mk_app(arith_family_id, OP_MOD, arg1, arg2); } + app * mk_div0(expr * arg1, expr * arg2) { return m_manager.mk_app(arith_family_id, OP_DIV0, arg1, arg2); } + app * mk_idiv0(expr * arg1, expr * arg2) { return m_manager.mk_app(arith_family_id, OP_IDIV0, arg1, arg2); } + app * mk_rem0(expr * arg1, expr * arg2) { return m_manager.mk_app(arith_family_id, OP_REM0, arg1, arg2); } + app * mk_mod0(expr * arg1, expr * arg2) { return m_manager.mk_app(arith_family_id, OP_MOD0, arg1, arg2); } + app * mk_to_real(expr * arg1) { return m_manager.mk_app(arith_family_id, OP_TO_REAL, arg1); } + app * mk_to_int(expr * arg1) { return m_manager.mk_app(arith_family_id, OP_TO_INT, arg1); } + app * mk_is_int(expr * arg1) { return m_manager.mk_app(arith_family_id, OP_IS_INT, arg1); } + app * mk_power(expr* arg1, expr* arg2) { return m_manager.mk_app(arith_family_id, OP_POWER, arg1, arg2); } + app * mk_power0(expr* arg1, expr* arg2) { return m_manager.mk_app(arith_family_id, OP_POWER0, arg1, arg2); } + + app * mk_sin(expr * arg) { return m_manager.mk_app(arith_family_id, OP_SIN, arg); } + app * mk_cos(expr * arg) { return m_manager.mk_app(arith_family_id, OP_COS, arg); } + app * mk_tan(expr * arg) { return m_manager.mk_app(arith_family_id, OP_TAN, arg); } + app * mk_asin(expr * arg) { return m_manager.mk_app(arith_family_id, OP_ASIN, arg); } + app * mk_acos(expr * arg) { return m_manager.mk_app(arith_family_id, OP_ACOS, arg); } + app * mk_atan(expr * arg) { return m_manager.mk_app(arith_family_id, OP_ATAN, arg); } + + app * mk_sinh(expr * arg) { return m_manager.mk_app(arith_family_id, OP_SINH, arg); } + app * mk_cosh(expr * arg) { return m_manager.mk_app(arith_family_id, OP_COSH, arg); } + app * mk_tanh(expr * arg) { return m_manager.mk_app(arith_family_id, OP_TANH, arg); } + app * mk_asinh(expr * arg) { return m_manager.mk_app(arith_family_id, OP_ASINH, arg); } + app * mk_acosh(expr * arg) { return m_manager.mk_app(arith_family_id, OP_ACOSH, arg); } + app * mk_atanh(expr * arg) { return m_manager.mk_app(arith_family_id, OP_ATANH, arg); } app * mk_pi() { return plugin().mk_pi(); } app * mk_e() { return plugin().mk_e(); } - app * mk_neg_root(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_NEG_ROOT, arg1, arg2); } - app * mk_u_asin(expr * arg) { return m_manager.mk_app(m_afid, OP_U_ASIN, arg); } - app * mk_u_acos(expr * arg) { return m_manager.mk_app(m_afid, OP_U_ACOS, arg); } + app * mk_neg_root(expr * arg1, expr * arg2) { return m_manager.mk_app(arith_family_id, OP_NEG_ROOT, arg1, arg2); } + app * mk_u_asin(expr * arg) { return m_manager.mk_app(arith_family_id, OP_U_ASIN, arg); } + app * mk_u_acos(expr * arg) { return m_manager.mk_app(arith_family_id, OP_U_ACOS, arg); } /** \brief Return the equality (= lhs rhs), but it makes sure that diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 400ae7e9c02..fb370334d2a 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -700,54 +700,6 @@ func_decl * decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, para // // ----------------------------------- -basic_decl_plugin::basic_decl_plugin(): - m_bool_sort(nullptr), - m_true_decl(nullptr), - m_false_decl(nullptr), - m_and_decl(nullptr), - m_or_decl(nullptr), - m_xor_decl(nullptr), - m_not_decl(nullptr), - m_implies_decl(nullptr), - - m_proof_sort(nullptr), - m_undef_decl(nullptr), - m_true_pr_decl(nullptr), - m_asserted_decl(nullptr), - m_goal_decl(nullptr), - m_modus_ponens_decl(nullptr), - m_reflexivity_decl(nullptr), - m_symmetry_decl(nullptr), - m_transitivity_decl(nullptr), - m_quant_intro_decl(nullptr), - m_and_elim_decl(nullptr), - m_not_or_elim_decl(nullptr), - m_rewrite_decl(nullptr), - m_pull_quant_decl(nullptr), - m_push_quant_decl(nullptr), - m_elim_unused_vars_decl(nullptr), - m_der_decl(nullptr), - m_quant_inst_decl(nullptr), - - m_hypothesis_decl(nullptr), - m_iff_true_decl(nullptr), - m_iff_false_decl(nullptr), - m_commutativity_decl(nullptr), - m_def_axiom_decl(nullptr), - m_lemma_decl(nullptr), - - m_def_intro_decl(nullptr), - m_iff_oeq_decl(nullptr), - m_skolemize_decl(nullptr), - m_mp_oeq_decl(nullptr), - m_assumption_add_decl(nullptr), - m_lemma_add_decl(nullptr), - m_th_assumption_add_decl(nullptr), - m_th_lemma_add_decl(nullptr), - m_redundant_del_decl(nullptr), - m_hyper_res_decl0(nullptr) { -} - bool basic_decl_plugin::check_proof_sorts(basic_op_kind k, unsigned arity, sort * const * domain) const { if (k == PR_UNDEF) return arity == 0; @@ -1109,8 +1061,8 @@ sort* basic_decl_plugin::join(unsigned n, expr* const* es) { sort* basic_decl_plugin::join(sort* s1, sort* s2) { if (s1 == s2) return s1; - if (s1->get_family_id() == m_manager->m_arith_family_id && - s2->get_family_id() == m_manager->m_arith_family_id) { + if (s1->get_family_id() == arith_family_id && + s2->get_family_id() == arith_family_id) { if (s1->get_decl_kind() == REAL_SORT) { return s1; } @@ -1211,16 +1163,6 @@ expr * basic_decl_plugin::get_some_value(sort * s) { return nullptr; } -bool basic_recognizers::is_ite(expr const * n, expr * & t1, expr * & t2, expr * & t3) const { - if (is_ite(n)) { - t1 = to_app(n)->get_arg(0); - t2 = to_app(n)->get_arg(1); - t3 = to_app(n)->get_arg(2); - return true; - } - return false; -} - // ----------------------------------- // // label_decl_plugin @@ -1233,9 +1175,6 @@ label_decl_plugin::label_decl_plugin(): m_lbllit("lbl-lit") { } -label_decl_plugin::~label_decl_plugin() { -} - void label_decl_plugin::set_manager(ast_manager * m, family_id id) { decl_plugin::set_manager(m, id); } @@ -1442,27 +1381,27 @@ void ast_manager::init() { m_expr_id_gen.reset(0); m_decl_id_gen.reset(c_first_decl_id); m_some_value_proc = nullptr; - m_basic_family_id = mk_family_id("basic"); - m_label_family_id = mk_family_id("label"); - m_pattern_family_id = mk_family_id("pattern"); - m_model_value_family_id = mk_family_id("model-value"); - m_user_sort_family_id = mk_family_id("user-sort"); - m_arith_family_id = mk_family_id("arith"); + ENSURE(basic_family_id == mk_family_id("basic")); + ENSURE(label_family_id == mk_family_id("label")); + ENSURE(pattern_family_id == mk_family_id("pattern")); + ENSURE(model_value_family_id == mk_family_id("model-value")); + ENSURE(user_sort_family_id == mk_family_id("user-sort")); + ENSURE(arith_family_id == mk_family_id("arith")); basic_decl_plugin * plugin = alloc(basic_decl_plugin); - register_plugin(m_basic_family_id, plugin); + register_plugin(basic_family_id, plugin); m_bool_sort = plugin->mk_bool_sort(); inc_ref(m_bool_sort); m_proof_sort = plugin->mk_proof_sort(); inc_ref(m_proof_sort); - m_undef_proof = mk_const(m_basic_family_id, PR_UNDEF); + m_undef_proof = mk_const(basic_family_id, PR_UNDEF); inc_ref(m_undef_proof); - register_plugin(m_label_family_id, alloc(label_decl_plugin)); - register_plugin(m_pattern_family_id, alloc(pattern_decl_plugin)); - register_plugin(m_model_value_family_id, alloc(model_value_decl_plugin)); - register_plugin(m_user_sort_family_id, alloc(user_sort_plugin)); - m_true = mk_const(m_basic_family_id, OP_TRUE); + register_plugin(label_family_id, alloc(label_decl_plugin)); + register_plugin(pattern_family_id, alloc(pattern_decl_plugin)); + register_plugin(model_value_family_id, alloc(model_value_decl_plugin)); + register_plugin(user_sort_family_id, alloc(user_sort_plugin)); + m_true = mk_const(basic_family_id, OP_TRUE); inc_ref(m_true); - m_false = mk_const(m_basic_family_id, OP_FALSE); + m_false = mk_const(basic_family_id, OP_FALSE); inc_ref(m_false); } @@ -2176,7 +2115,7 @@ bool ast_manager::compatible_sorts(sort * s1, sort * s2) const { if (s1 == s2) return true; if (m_int_real_coercions) - return s1->get_family_id() == m_arith_family_id && s2->get_family_id() == m_arith_family_id; + return s1->get_family_id() == arith_family_id && s2->get_family_id() == arith_family_id; return false; } @@ -2184,7 +2123,7 @@ bool ast_manager::coercion_needed(func_decl * decl, unsigned num_args, expr * co SASSERT(m_int_real_coercions); if (decl->is_associative()) { sort * d = decl->get_domain(0); - if (d->get_family_id() == m_arith_family_id) { + if (d->get_family_id() == arith_family_id) { for (unsigned i = 0; i < num_args; i++) { if (d != args[i]->get_sort()) return true; @@ -2199,7 +2138,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 != args[i]->get_sort()) + if (d->get_family_id() == arith_family_id && d != args[i]->get_sort()) return true; } } @@ -2208,12 +2147,12 @@ bool ast_manager::coercion_needed(func_decl * decl, unsigned num_args, expr * co expr* ast_manager::coerce_to(expr* e, sort* s) { 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 != se && s->get_family_id() == arith_family_id && se->get_family_id() == arith_family_id) { if (s->get_decl_kind() == REAL_SORT) { - return mk_app(m_arith_family_id, OP_TO_REAL, e); + return mk_app(arith_family_id, OP_TO_REAL, e); } else { - return mk_app(m_arith_family_id, OP_TO_INT, e); + return mk_app(arith_family_id, OP_TO_INT, e); } } else { @@ -2246,7 +2185,7 @@ app * ast_manager::mk_app_core(func_decl * decl, unsigned num_args, expr * const if (m_trace_stream && r == new_node) { if (is_proof(r)) { - if (decl == mk_func_decl(m_basic_family_id, PR_UNDEF, 0, nullptr, 0, static_cast(nullptr))) + if (decl == mk_func_decl(basic_family_id, PR_UNDEF, 0, nullptr, 0, static_cast(nullptr))) return r; *m_trace_stream << "[mk-proof] #"; } else { @@ -2303,7 +2242,7 @@ app * ast_manager::mk_app(func_decl * decl, unsigned num_args, expr * const * ar !decl->is_left_associative() && !decl->is_chainable(); type_error |= (decl->get_arity() != num_args && num_args < 2 && - decl->get_family_id() == m_basic_family_id && !decl->is_associative()); + decl->get_family_id() == basic_family_id && !decl->is_associative()); if (type_error) { std::ostringstream buffer; @@ -2410,7 +2349,7 @@ app * ast_manager::mk_label(bool pos, unsigned num_names, symbol const * names, p.push_back(parameter(static_cast(pos))); for (unsigned i = 0; i < num_names; i++) p.push_back(parameter(names[i])); - return mk_app(m_label_family_id, OP_LABEL, p.size(), p.c_ptr(), 1, &n); + return mk_app(label_family_id, OP_LABEL, p.size(), p.c_ptr(), 1, &n); } app * ast_manager::mk_label(bool pos, symbol const & name, expr * n) { @@ -2418,7 +2357,7 @@ app * ast_manager::mk_label(bool pos, symbol const & name, expr * n) { } bool ast_manager::is_label(expr const * n, bool & pos, buffer & names) const { - if (!is_app_of(n, m_label_family_id, OP_LABEL)) { + if (!is_app_of(n, label_family_id, OP_LABEL)) { return false; } func_decl const * decl = to_app(n)->get_decl(); @@ -2433,7 +2372,7 @@ app * ast_manager::mk_label_lit(unsigned num_names, symbol const * names) { buffer p; for (unsigned i = 0; i < num_names; i++) p.push_back(parameter(names[i])); - return mk_app(m_label_family_id, OP_LABEL_LIT, p.size(), p.c_ptr(), 0, nullptr); + return mk_app(label_family_id, OP_LABEL_LIT, p.size(), p.c_ptr(), 0, nullptr); } app * ast_manager::mk_label_lit(symbol const & name) { @@ -2441,7 +2380,7 @@ app * ast_manager::mk_label_lit(symbol const & name) { } bool ast_manager::is_label_lit(expr const * n, buffer & names) const { - if (!is_app_of(n, m_label_family_id, OP_LABEL_LIT)) { + if (!is_app_of(n, label_family_id, OP_LABEL_LIT)) { return false; } func_decl const * decl = to_app(n)->get_decl(); @@ -2454,11 +2393,11 @@ app * ast_manager::mk_pattern(unsigned num_exprs, app * const * exprs) { for (unsigned i = 0; i < num_exprs; ++i) { if (!is_app(exprs[i])) throw default_exception("patterns cannot be variables or quantifiers"); } - return mk_app(m_pattern_family_id, OP_PATTERN, 0, nullptr, num_exprs, (expr*const*)exprs); + return mk_app(pattern_family_id, OP_PATTERN, 0, nullptr, num_exprs, (expr*const*)exprs); } bool ast_manager::is_pattern(expr const * n) const { - if (!is_app_of(n, m_pattern_family_id, OP_PATTERN)) { + if (!is_app_of(n, pattern_family_id, OP_PATTERN)) { return false; } for (unsigned i = 0; i < to_app(n)->get_num_args(); ++i) { @@ -2471,7 +2410,7 @@ bool ast_manager::is_pattern(expr const * n) const { bool ast_manager::is_pattern(expr const * n, ptr_vector &args) { - if (!is_app_of(n, m_pattern_family_id, OP_PATTERN)) { + if (!is_app_of(n, pattern_family_id, OP_PATTERN)) { return false; } for (unsigned i = 0; i < to_app(n)->get_num_args(); ++i) { @@ -2675,7 +2614,7 @@ quantifier * ast_manager::update_quantifier(quantifier * q, quantifier_kind k, u } app * ast_manager::mk_distinct(unsigned num_args, expr * const * args) { - return mk_app(m_basic_family_id, OP_DISTINCT, num_args, args); + return mk_app(basic_family_id, OP_DISTINCT, num_args, args); } app * ast_manager::mk_distinct_expanded(unsigned num_args, expr * const * args) { @@ -2729,7 +2668,7 @@ void ast_manager::linearize(expr_dependency * d, ptr_vector & ts) { app * ast_manager::mk_model_value(unsigned idx, sort * s) { parameter p[2] = { parameter(idx), parameter(s) }; - return mk_app(m_model_value_family_id, OP_MODEL_VALUE, 2, p, 0, static_cast(nullptr)); + return mk_app(model_value_family_id, OP_MODEL_VALUE, 2, p, 0, static_cast(nullptr)); } expr * ast_manager::get_some_value(sort * s, some_value_proc * p) { @@ -2794,18 +2733,18 @@ proof * ast_manager::mk_proof(family_id fid, decl_kind k, expr * arg1, expr * ar proof * ast_manager::mk_true_proof() { expr * f = mk_true(); - return mk_proof(m_basic_family_id, PR_TRUE, f); + return mk_proof(basic_family_id, PR_TRUE, f); } proof * ast_manager::mk_asserted(expr * f) { CTRACE("mk_asserted_bug", !is_bool(f), tout << mk_ismt2_pp(f, *this) << "\nsort: " << mk_ismt2_pp(f->get_sort(), *this) << "\n";); SASSERT(is_bool(f)); - return mk_proof(m_basic_family_id, PR_ASSERTED, f); + return mk_proof(basic_family_id, PR_ASSERTED, f); } proof * ast_manager::mk_goal(expr * f) { SASSERT(is_bool(f)); - return mk_proof(m_basic_family_id, PR_GOAL, f); + return mk_proof(basic_family_id, PR_GOAL, f); } proof * ast_manager::mk_modus_ponens(proof * p1, proof * p2) { @@ -2825,22 +2764,22 @@ proof * ast_manager::mk_modus_ponens(proof * p1, proof * p2) { return p1; expr * f = to_app(get_fact(p2))->get_arg(1); if (is_oeq(get_fact(p2))) - return mk_app(m_basic_family_id, PR_MODUS_PONENS_OEQ, p1, p2, f); - return mk_app(m_basic_family_id, PR_MODUS_PONENS, p1, p2, f); + return mk_app(basic_family_id, PR_MODUS_PONENS_OEQ, p1, p2, f); + return mk_app(basic_family_id, PR_MODUS_PONENS, p1, p2, f); } proof * ast_manager::mk_reflexivity(expr * e) { - return mk_app(m_basic_family_id, PR_REFLEXIVITY, mk_eq(e, e)); + return mk_app(basic_family_id, PR_REFLEXIVITY, mk_eq(e, e)); } proof * ast_manager::mk_oeq_reflexivity(expr * e) { - return mk_app(m_basic_family_id, PR_REFLEXIVITY, mk_oeq(e, e)); + return mk_app(basic_family_id, PR_REFLEXIVITY, mk_oeq(e, e)); } proof * ast_manager::mk_commutativity(app * f) { SASSERT(f->get_num_args() == 2); app * f_prime = mk_app(f->get_decl(), f->get_arg(1), f->get_arg(0)); - return mk_app(m_basic_family_id, PR_COMMUTATIVITY, mk_eq(f, f_prime)); + return mk_app(basic_family_id, PR_COMMUTATIVITY, mk_eq(f, f_prime)); } /** @@ -2850,7 +2789,7 @@ proof * ast_manager::mk_iff_true(proof * pr) { if (!pr) return pr; SASSERT(has_fact(pr)); SASSERT(is_bool(get_fact(pr))); - return mk_app(m_basic_family_id, PR_IFF_TRUE, pr, mk_iff(get_fact(pr), mk_true())); + return mk_app(basic_family_id, PR_IFF_TRUE, pr, mk_iff(get_fact(pr), mk_true())); } /** @@ -2861,7 +2800,7 @@ proof * ast_manager::mk_iff_false(proof * pr) { SASSERT(has_fact(pr)); SASSERT(is_not(get_fact(pr))); expr * p = to_app(get_fact(pr))->get_arg(0); - return mk_app(m_basic_family_id, PR_IFF_FALSE, pr, mk_iff(p, mk_false())); + return mk_app(basic_family_id, PR_IFF_FALSE, pr, mk_iff(p, mk_false())); } proof * ast_manager::mk_symmetry(proof * p) { @@ -2873,7 +2812,7 @@ proof * ast_manager::mk_symmetry(proof * p) { SASSERT(has_fact(p)); SASSERT(is_app(get_fact(p))); SASSERT(to_app(get_fact(p))->get_num_args() == 2); - return mk_app(m_basic_family_id, PR_SYMMETRY, p, + return mk_app(basic_family_id, PR_SYMMETRY, p, mk_app(to_app(get_fact(p))->get_decl(), to_app(get_fact(p))->get_arg(1), to_app(get_fact(p))->get_arg(0))); } @@ -2910,7 +2849,7 @@ proof * ast_manager::mk_transitivity(proof * p1, proof * p2) { // OEQ is compatible with EQ for transitivity. func_decl* f = to_app(get_fact(p1))->get_decl(); if (is_oeq(get_fact(p2))) f = to_app(get_fact(p2))->get_decl(); - return mk_app(m_basic_family_id, PR_TRANSITIVITY, p1, p2, mk_app(f, to_app(get_fact(p1))->get_arg(0), to_app(get_fact(p2))->get_arg(1))); + return mk_app(basic_family_id, PR_TRANSITIVITY, p1, p2, mk_app(f, to_app(get_fact(p1))->get_arg(0), to_app(get_fact(p2))->get_arg(1))); } @@ -2944,7 +2883,7 @@ proof * ast_manager::mk_transitivity(unsigned num_proofs, proof * const * proofs ptr_buffer args; args.append(num_proofs, (expr**) proofs); args.push_back(mk_eq(n1,n2)); - return mk_app(m_basic_family_id, PR_TRANSITIVITY_STAR, args.size(), args.c_ptr()); + return mk_app(basic_family_id, PR_TRANSITIVITY_STAR, args.size(), args.c_ptr()); } proof * ast_manager::mk_monotonicity(func_decl * R, app * f1, app * f2, unsigned num_proofs, proof * const * proofs) { @@ -2953,7 +2892,7 @@ proof * ast_manager::mk_monotonicity(func_decl * R, app * f1, app * f2, unsigned ptr_buffer args; args.append(num_proofs, (expr**) proofs); args.push_back(mk_app(R, f1, f2)); - proof* p = mk_app(m_basic_family_id, PR_MONOTONICITY, args.size(), args.c_ptr()); + proof* p = mk_app(basic_family_id, PR_MONOTONICITY, args.size(), args.c_ptr()); return p; } @@ -2961,20 +2900,20 @@ proof * ast_manager::mk_congruence(app * f1, app * f2, unsigned num_proofs, proo SASSERT(f1->get_sort() == f2->get_sort()); sort * s = f1->get_sort(); sort * d[2] = { s, s }; - return mk_monotonicity(mk_func_decl(m_basic_family_id, get_eq_op(f1), 0, nullptr, 2, d), f1, f2, num_proofs, proofs); + return mk_monotonicity(mk_func_decl(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(f1->get_sort() == f2->get_sort()); sort * s = f1->get_sort(); sort * d[2] = { s, s }; - return mk_monotonicity(mk_func_decl(m_basic_family_id, OP_OEQ, 0, nullptr, 2, d), f1, f2, num_proofs, proofs); + return mk_monotonicity(mk_func_decl(basic_family_id, OP_OEQ, 0, nullptr, 2, d), f1, f2, num_proofs, proofs); } proof * ast_manager::mk_bind_proof(quantifier * q, proof * p) { expr* b = mk_lambda(q->get_num_decls(), q->get_decl_sorts(), q->get_decl_names(), p); - return mk_app(m_basic_family_id, PR_BIND, b); + return mk_app(basic_family_id, PR_BIND, b); } proof * ast_manager::mk_quant_intro(quantifier * q1, quantifier * q2, proof * p) { @@ -2982,7 +2921,7 @@ proof * ast_manager::mk_quant_intro(quantifier * q1, quantifier * q2, proof * p) SASSERT(q1->get_num_decls() == q2->get_num_decls()); SASSERT(has_fact(p)); SASSERT(is_eq(get_fact(p)) || is_lambda(get_fact(p))); - return mk_app(m_basic_family_id, PR_QUANT_INTRO, p, mk_iff(q1, q2)); + return mk_app(basic_family_id, PR_QUANT_INTRO, p, mk_iff(q1, q2)); } proof * ast_manager::mk_oeq_quant_intro(quantifier * q1, quantifier * q2, proof * p) { @@ -2990,23 +2929,23 @@ proof * ast_manager::mk_oeq_quant_intro(quantifier * q1, quantifier * q2, proof SASSERT(q1->get_num_decls() == q2->get_num_decls()); SASSERT(has_fact(p)); SASSERT(is_oeq(get_fact(p)) || is_lambda(get_fact(p))); - return mk_app(m_basic_family_id, PR_QUANT_INTRO, p, mk_oeq(q1, q2)); + return mk_app(basic_family_id, PR_QUANT_INTRO, p, mk_oeq(q1, q2)); } proof * ast_manager::mk_distributivity(expr * s, expr * r) { - return mk_app(m_basic_family_id, PR_DISTRIBUTIVITY, mk_eq(s, r)); + return mk_app(basic_family_id, PR_DISTRIBUTIVITY, mk_eq(s, r)); } proof * ast_manager::mk_rewrite(expr * s, expr * t) { if (proofs_disabled()) return nullptr; - return mk_app(m_basic_family_id, PR_REWRITE, mk_eq(s, t)); + return mk_app(basic_family_id, PR_REWRITE, mk_eq(s, t)); } proof * ast_manager::mk_oeq_rewrite(expr * s, expr * t) { if (proofs_disabled()) return nullptr; - return mk_app(m_basic_family_id, PR_REWRITE, mk_oeq(s, t)); + return mk_app(basic_family_id, PR_REWRITE, mk_oeq(s, t)); } proof * ast_manager::mk_rewrite_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs) { @@ -3015,31 +2954,31 @@ proof * ast_manager::mk_rewrite_star(expr * s, expr * t, unsigned num_proofs, pr ptr_buffer args; args.append(num_proofs, (expr**) proofs); args.push_back(mk_eq(s, t)); - return mk_app(m_basic_family_id, PR_REWRITE_STAR, args.size(), args.c_ptr()); + return mk_app(basic_family_id, PR_REWRITE_STAR, args.size(), args.c_ptr()); } proof * ast_manager::mk_pull_quant(expr * e, quantifier * q) { if (proofs_disabled()) return nullptr; - return mk_app(m_basic_family_id, PR_PULL_QUANT, mk_iff(e, q)); + return mk_app(basic_family_id, PR_PULL_QUANT, mk_iff(e, q)); } proof * ast_manager::mk_push_quant(quantifier * q, expr * e) { if (proofs_disabled()) return nullptr; - return mk_app(m_basic_family_id, PR_PUSH_QUANT, mk_iff(q, e)); + return mk_app(basic_family_id, PR_PUSH_QUANT, mk_iff(q, e)); } proof * ast_manager::mk_elim_unused_vars(quantifier * q, expr * e) { if (proofs_disabled()) return nullptr; - return mk_app(m_basic_family_id, PR_ELIM_UNUSED_VARS, mk_iff(q, e)); + return mk_app(basic_family_id, PR_ELIM_UNUSED_VARS, mk_iff(q, e)); } proof * ast_manager::mk_der(quantifier * q, expr * e) { if (proofs_disabled()) return nullptr; - return mk_app(m_basic_family_id, PR_DER, mk_iff(q, e)); + return mk_app(basic_family_id, PR_DER, mk_iff(q, e)); } proof * ast_manager::mk_quant_inst(expr * not_q_or_i, unsigned num_bind, expr* const* binding) { @@ -3050,7 +2989,7 @@ proof * ast_manager::mk_quant_inst(expr * not_q_or_i, unsigned num_bind, expr* c params.push_back(parameter(binding[i])); SASSERT(params.back().is_ast()); } - return mk_app(m_basic_family_id, PR_QUANT_INST, num_bind, params.c_ptr(), 1, & not_q_or_i); + return mk_app(basic_family_id, PR_QUANT_INST, num_bind, params.c_ptr(), 1, & not_q_or_i); } bool ast_manager::is_quant_inst(expr const* e, expr*& not_q_or_i, ptr_vector& binding) const { @@ -3073,7 +3012,7 @@ bool ast_manager::is_rewrite(expr const* e, expr*& r1, expr*& r2) const { proof * ast_manager::mk_def_axiom(expr * ax) { if (proofs_disabled()) return nullptr; - return mk_app(m_basic_family_id, PR_DEF_AXIOM, ax); + return mk_app(basic_family_id, PR_DEF_AXIOM, ax); } proof * ast_manager::mk_unit_resolution(unsigned num_proofs, proof * const * proofs) { @@ -3149,7 +3088,7 @@ proof * ast_manager::mk_unit_resolution(unsigned num_proofs, proof * const * pro args.push_back(fact); } - proof * pr = mk_app(m_basic_family_id, PR_UNIT_RESOLUTION, args.size(), args.c_ptr()); + proof * pr = mk_app(basic_family_id, PR_UNIT_RESOLUTION, args.size(), args.c_ptr()); TRACE("unit_resolution", tout << "unit_resolution generating fact\n" << mk_ll_pp(pr, *this);); return pr; } @@ -3201,13 +3140,13 @@ proof * ast_manager::mk_unit_resolution(unsigned num_proofs, proof * const * pro SASSERT(num_matches != cls_sz || is_false(new_fact)); } #endif - proof * pr = mk_app(m_basic_family_id, PR_UNIT_RESOLUTION, args.size(), args.c_ptr()); + proof * pr = mk_app(basic_family_id, PR_UNIT_RESOLUTION, args.size(), args.c_ptr()); TRACE("unit_resolution", tout << "unit_resolution using fact\n" << mk_ll_pp(pr, *this);); return pr; } proof * ast_manager::mk_hypothesis(expr * h) { - return mk_app(m_basic_family_id, PR_HYPOTHESIS, h); + return mk_app(basic_family_id, PR_HYPOTHESIS, h); } proof * ast_manager::mk_lemma(proof * p, expr * lemma) { @@ -3215,12 +3154,12 @@ proof * ast_manager::mk_lemma(proof * p, expr * lemma) { SASSERT(has_fact(p)); CTRACE("mk_lemma", !is_false(get_fact(p)), tout << mk_ll_pp(p, *this) << "\n";); SASSERT(is_false(get_fact(p))); - return mk_app(m_basic_family_id, PR_LEMMA, p, lemma); + return mk_app(basic_family_id, PR_LEMMA, p, lemma); } proof * ast_manager::mk_def_intro(expr * new_def) { SASSERT(is_bool(new_def)); - return mk_proof(m_basic_family_id, PR_DEF_INTRO, new_def); + return mk_proof(basic_family_id, PR_DEF_INTRO, new_def); } proof * ast_manager::mk_apply_defs(expr * n, expr * def, unsigned num_proofs, proof * const * proofs) { @@ -3229,7 +3168,7 @@ proof * ast_manager::mk_apply_defs(expr * n, expr * def, unsigned num_proofs, pr ptr_buffer args; args.append(num_proofs, (expr**) proofs); args.push_back(mk_oeq(n, def)); - return mk_app(m_basic_family_id, PR_APPLY_DEF, args.size(), args.c_ptr()); + return mk_app(basic_family_id, PR_APPLY_DEF, args.size(), args.c_ptr()); } proof * ast_manager::mk_iff_oeq(proof * p) { @@ -3243,7 +3182,7 @@ proof * ast_manager::mk_iff_oeq(proof * p) { app * iff = to_app(get_fact(p)); expr * lhs = iff->get_arg(0); expr * rhs = iff->get_arg(1); - return mk_app(m_basic_family_id, PR_IFF_OEQ, p, mk_oeq(lhs, rhs)); + return mk_app(basic_family_id, PR_IFF_OEQ, p, mk_oeq(lhs, rhs)); } bool ast_manager::check_nnf_proof_parents(unsigned num_proofs, proof * const * proofs) const { @@ -3263,7 +3202,7 @@ proof * ast_manager::mk_nnf_pos(expr * s, expr * t, unsigned num_proofs, proof * ptr_buffer args; args.append(num_proofs, (expr**) proofs); args.push_back(mk_oeq(s, t)); - return mk_app(m_basic_family_id, PR_NNF_POS, args.size(), args.c_ptr()); + return mk_app(basic_family_id, PR_NNF_POS, args.size(), args.c_ptr()); } proof * ast_manager::mk_nnf_neg(expr * s, expr * t, unsigned num_proofs, proof * const * proofs) { @@ -3273,7 +3212,7 @@ proof * ast_manager::mk_nnf_neg(expr * s, expr * t, unsigned num_proofs, proof * ptr_buffer args; args.append(num_proofs, (expr**) proofs); args.push_back(mk_oeq(mk_not(s), t)); - return mk_app(m_basic_family_id, PR_NNF_NEG, args.size(), args.c_ptr()); + return mk_app(basic_family_id, PR_NNF_NEG, args.size(), args.c_ptr()); } proof * ast_manager::mk_skolemization(expr * q, expr * e) { @@ -3281,7 +3220,7 @@ proof * ast_manager::mk_skolemization(expr * q, expr * e) { return nullptr; SASSERT(is_bool(q)); SASSERT(is_bool(e)); - return mk_app(m_basic_family_id, PR_SKOLEMIZE, mk_oeq(q, e)); + return mk_app(basic_family_id, PR_SKOLEMIZE, mk_oeq(q, e)); } proof * ast_manager::mk_and_elim(proof * p, unsigned i) { @@ -3292,7 +3231,7 @@ proof * ast_manager::mk_and_elim(proof * p, unsigned i) { CTRACE("mk_and_elim", i >= to_app(get_fact(p))->get_num_args(), tout << "i: " << i << "\n" << mk_pp(get_fact(p), *this) << "\n";); SASSERT(i < to_app(get_fact(p))->get_num_args()); expr * f = to_app(get_fact(p))->get_arg(i); - return mk_app(m_basic_family_id, PR_AND_ELIM, p, f); + return mk_app(basic_family_id, PR_AND_ELIM, p, f); } proof * ast_manager::mk_not_or_elim(proof * p, unsigned i) { @@ -3309,14 +3248,14 @@ proof * ast_manager::mk_not_or_elim(proof * p, unsigned i) { f = to_app(c)->get_arg(0); else f = mk_not(c); - return mk_app(m_basic_family_id, PR_NOT_OR_ELIM, p, f); + return mk_app(basic_family_id, PR_NOT_OR_ELIM, p, f); } proof* ast_manager::mk_clause_trail_elem(proof *pr, expr* e, decl_kind k) { ptr_buffer args; if (pr) args.push_back(pr); args.push_back(e); - return mk_app(m_basic_family_id, k, 0, nullptr, args.size(), args.c_ptr()); + return mk_app(basic_family_id, k, 0, nullptr, args.size(), args.c_ptr()); } proof * ast_manager::mk_assumption_add(proof* pr, expr* e) { @@ -3342,7 +3281,7 @@ proof * ast_manager::mk_redundant_del(expr* e) { proof * ast_manager::mk_clause_trail(unsigned n, proof* const* ps) { ptr_buffer args; args.append(n, (expr**) ps); - return mk_app(m_basic_family_id, PR_CLAUSE_TRAIL, 0, nullptr, args.size(), args.c_ptr()); + return mk_app(basic_family_id, PR_CLAUSE_TRAIL, 0, nullptr, args.size(), args.c_ptr()); } proof * ast_manager::mk_th_lemma( @@ -3362,7 +3301,7 @@ proof * ast_manager::mk_th_lemma( } args.append(num_proofs, (expr**) proofs); args.push_back(fact); - return mk_app(m_basic_family_id, PR_TH_LEMMA, num_params+1, parameters.c_ptr(), args.size(), args.c_ptr()); + return mk_app(basic_family_id, PR_TH_LEMMA, num_params+1, parameters.c_ptr(), args.size(), args.c_ptr()); } proof* ast_manager::mk_hyper_resolve(unsigned num_premises, proof* const* premises, expr* concl, @@ -3398,8 +3337,8 @@ proof* ast_manager::mk_hyper_resolve(unsigned num_premises, proof* const* premis } sorts.push_back(mk_bool_sort()); args.push_back(concl); - app* result = mk_app(m_basic_family_id, PR_HYPER_RESOLVE, params.size(), params.c_ptr(), args.size(), args.c_ptr()); - SASSERT(result->get_family_id() == m_basic_family_id); + app* result = mk_app(basic_family_id, PR_HYPER_RESOLVE, params.size(), params.c_ptr(), args.size(), args.c_ptr()); + SASSERT(result->get_family_id() == basic_family_id); SASSERT(result->get_decl_kind() == PR_HYPER_RESOLVE); return result; } diff --git a/src/ast/ast.h b/src/ast/ast.h index add30569482..41f21d71688 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -75,6 +75,14 @@ class ast_exception : public default_exception { typedef int family_id; const family_id null_family_id = -1; +const family_id basic_family_id = 0; +const family_id label_family_id = 1; +const family_id pattern_family_id = 2; +const family_id model_value_family_id = 3; +const family_id user_sort_family_id = 4; +const family_id last_builtin_family_id = 4; + +const family_id arith_family_id = 5; // ----------------------------------- // @@ -1115,65 +1123,65 @@ enum basic_op_kind { class basic_decl_plugin : public decl_plugin { protected: - sort * m_bool_sort; - func_decl * m_true_decl; - func_decl * m_false_decl; - func_decl * m_and_decl; - func_decl * m_or_decl; - func_decl * m_xor_decl; - func_decl * m_not_decl; - func_decl * m_implies_decl; + sort * m_bool_sort = nullptr; + func_decl * m_true_decl = nullptr; + func_decl * m_false_decl = nullptr; + func_decl * m_and_decl = nullptr; + func_decl * m_or_decl = nullptr; + func_decl * m_xor_decl = nullptr; + func_decl * m_not_decl = nullptr; + func_decl * m_implies_decl = nullptr; ptr_vector m_eq_decls; // cached eqs ptr_vector m_ite_decls; // cached ites ptr_vector m_oeq_decls; // cached observational eqs - sort * m_proof_sort; - func_decl * m_undef_decl; - func_decl * m_true_pr_decl; - func_decl * m_asserted_decl; - func_decl * m_goal_decl; - func_decl * m_modus_ponens_decl; - func_decl * m_reflexivity_decl; - func_decl * m_symmetry_decl; - func_decl * m_transitivity_decl; - func_decl * m_quant_intro_decl; - func_decl * m_and_elim_decl; - func_decl * m_not_or_elim_decl; - func_decl * m_rewrite_decl; - func_decl * m_pull_quant_decl; - func_decl * m_push_quant_decl; - func_decl * m_elim_unused_vars_decl; - func_decl * m_der_decl; - func_decl * m_quant_inst_decl; + sort * m_proof_sort = nullptr; + func_decl * m_undef_decl = nullptr; + func_decl * m_true_pr_decl = nullptr; + func_decl * m_asserted_decl = nullptr; + func_decl * m_goal_decl = nullptr; + func_decl * m_modus_ponens_decl = nullptr; + func_decl * m_reflexivity_decl = nullptr; + func_decl * m_symmetry_decl = nullptr; + func_decl * m_transitivity_decl = nullptr; + func_decl * m_quant_intro_decl = nullptr; + func_decl * m_and_elim_decl = nullptr; + func_decl * m_not_or_elim_decl = nullptr; + func_decl * m_rewrite_decl = nullptr; + func_decl * m_pull_quant_decl = nullptr; + func_decl * m_push_quant_decl = nullptr; + func_decl * m_elim_unused_vars_decl = nullptr; + func_decl * m_der_decl = nullptr; + func_decl * m_quant_inst_decl = nullptr; ptr_vector m_monotonicity_decls; ptr_vector m_transitivity_star_decls; ptr_vector m_distributivity_decls; ptr_vector m_assoc_flat_decls; ptr_vector m_rewrite_star_decls; - func_decl * m_hypothesis_decl; - func_decl * m_iff_true_decl; - func_decl * m_iff_false_decl; - func_decl * m_commutativity_decl; - func_decl * m_def_axiom_decl; - func_decl * m_lemma_decl; + func_decl * m_hypothesis_decl = nullptr; + func_decl * m_iff_true_decl = nullptr; + func_decl * m_iff_false_decl = nullptr; + func_decl * m_commutativity_decl = nullptr; + func_decl * m_def_axiom_decl = nullptr; + func_decl * m_lemma_decl = nullptr; ptr_vector m_unit_resolution_decls; - func_decl * m_def_intro_decl; - func_decl * m_iff_oeq_decl; - func_decl * m_skolemize_decl; - func_decl * m_mp_oeq_decl; - func_decl * m_assumption_add_decl; - func_decl * m_lemma_add_decl; - func_decl * m_th_assumption_add_decl; - func_decl * m_th_lemma_add_decl; - func_decl * m_redundant_del_decl; + func_decl * m_def_intro_decl = nullptr; + func_decl * m_iff_oeq_decl = nullptr; + func_decl * m_skolemize_decl = nullptr; + func_decl * m_mp_oeq_decl = nullptr; + func_decl * m_assumption_add_decl = nullptr; + func_decl * m_lemma_add_decl = nullptr; + func_decl * m_th_assumption_add_decl = nullptr; + func_decl * m_th_lemma_add_decl = nullptr; + func_decl * m_redundant_del_decl = nullptr; ptr_vector m_apply_def_decls; ptr_vector m_nnf_pos_decls; ptr_vector m_nnf_neg_decls; ptr_vector m_th_lemma_decls; - func_decl * m_hyper_res_decl0; + func_decl * m_hyper_res_decl0 = nullptr; static bool is_proof(decl_kind k) { return k > LAST_BASIC_OP; } bool check_proof_sorts(basic_op_kind k, unsigned arity, sort * const * domain) const; @@ -1199,9 +1207,7 @@ class basic_decl_plugin : public decl_plugin { sort* join(unsigned n, sort*const* srts); sort* join(unsigned n, expr*const* es); public: - basic_decl_plugin(); - ~basic_decl_plugin() override {} void finalize() override; decl_plugin * mk_fresh() override { @@ -1255,7 +1261,6 @@ class label_decl_plugin : public decl_plugin { public: label_decl_plugin(); - ~label_decl_plugin() override; decl_plugin * mk_fresh() override { return alloc(label_decl_plugin); } @@ -1324,8 +1329,6 @@ enum model_value_op_kind { */ class model_value_decl_plugin : public decl_plugin { public: - model_value_decl_plugin() {} - decl_plugin * mk_fresh() override { return alloc(model_value_decl_plugin); } sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) override; @@ -1396,52 +1399,6 @@ inline bool has_labels(expr const * n) { } -class basic_recognizers { - family_id m_fid; -public: - basic_recognizers(family_id fid):m_fid(fid) {} - bool is_bool(sort const * s) const { return is_sort_of(s, m_fid, BOOL_SORT); } - bool is_bool(expr const * n) const { return is_bool(n->get_sort()); } - bool is_or(expr const * n) const { return is_app_of(n, m_fid, OP_OR); } - bool is_implies(expr const * n) const { return is_app_of(n, m_fid, OP_IMPLIES); } - bool is_and(expr const * n) const { return is_app_of(n, m_fid, OP_AND); } - bool is_not(expr const * n) const { return is_app_of(n, m_fid, OP_NOT); } - bool is_eq(expr const * n) const { return is_app_of(n, m_fid, OP_EQ); } - bool is_iff(expr const* n) const { return is_eq(n) && is_bool(to_app(n)->get_arg(0)); } - bool is_oeq(expr const * n) const { return is_app_of(n, m_fid, OP_OEQ); } - bool is_distinct(expr const * n) const { return is_app_of(n, m_fid, OP_DISTINCT); } - bool is_xor(expr const * n) const { return is_app_of(n, m_fid, OP_XOR); } - bool is_ite(expr const * n) const { return is_app_of(n, m_fid, OP_ITE); } - bool is_term_ite(expr const * n) const { return is_ite(n) && !is_bool(n); } - bool is_true(expr const * n) const { return is_app_of(n, m_fid, OP_TRUE); } - bool is_false(expr const * n) const { return is_app_of(n, m_fid, OP_FALSE); } - bool is_complement_core(expr const * n1, expr const * n2) const { - return (is_true(n1) && is_false(n2)) || (is_not(n1) && to_app(n1)->get_arg(0) == n2); - } - bool is_complement(expr const * n1, expr const * n2) const { return is_complement_core(n1, n2) || is_complement_core(n2, n1); } - bool is_or(func_decl const * d) const { return is_decl_of(d, m_fid, OP_OR); } - bool is_implies(func_decl const * d) const { return is_decl_of(d, m_fid, OP_IMPLIES); } - bool is_and(func_decl const * d) const { return is_decl_of(d, m_fid, OP_AND); } - bool is_not(func_decl const * d) const { return is_decl_of(d, m_fid, OP_NOT); } - bool is_eq(func_decl const * d) const { return is_decl_of(d, m_fid, OP_EQ); } - bool is_xor(func_decl const * d) const { return is_decl_of(d, m_fid, OP_XOR); } - bool is_ite(func_decl const * d) const { return is_decl_of(d, m_fid, OP_ITE); } - bool is_term_ite(func_decl const * d) const { return is_ite(d) && !is_bool(d->get_range()); } - bool is_distinct(func_decl const * d) const { return is_decl_of(d, m_fid, OP_DISTINCT); } - - MATCH_UNARY(is_not); - MATCH_BINARY(is_eq); - MATCH_BINARY(is_implies); - MATCH_BINARY(is_and); - MATCH_BINARY(is_or); - MATCH_BINARY(is_xor); - MATCH_TERNARY(is_and); - MATCH_TERNARY(is_or); - bool is_iff(expr const* n, expr*& lhs, expr*& rhs) const { return is_eq(n, lhs, rhs) && is_bool(lhs); } - - bool is_ite(expr const * n, expr * & t1, expr * & t2, expr * & t3) const; -}; - // ----------------------------------- // // Get Some Value functor @@ -1529,12 +1486,6 @@ class ast_manager { ptr_vector m_plugins; proof_gen_mode m_proof_mode; bool m_int_real_coercions; // If true, use hack that automatically introduces to_int/to_real when needed. - family_id m_basic_family_id; - family_id m_label_family_id; - family_id m_pattern_family_id; - family_id m_model_value_family_id; - family_id m_user_sort_family_id; - family_id m_arith_family_id; ast_table m_ast_table; obj_map m_lambda_defs; id_gen m_expr_id_gen; @@ -1616,13 +1567,7 @@ class ast_manager { symbol const & get_family_name(family_id fid) const { return m_family_manager.get_name(fid); } bool is_builtin_family_id(family_id fid) const { - return - fid == null_family_id || - fid == m_basic_family_id || - fid == m_label_family_id || - fid == m_pattern_family_id || - fid == m_model_value_family_id || - fid == m_user_sort_family_id; + return fid >= null_family_id && fid <= last_builtin_family_id; } reslimit& limit() { return m_limit; } @@ -1643,13 +1588,13 @@ class ast_manager { void get_range(svector & range) const { m_family_manager.get_range(range); } - family_id get_basic_family_id() const { return m_basic_family_id; } + family_id get_basic_family_id() const { return basic_family_id; } - basic_decl_plugin * get_basic_decl_plugin() const { return static_cast(get_plugin(m_basic_family_id)); } + basic_decl_plugin * get_basic_decl_plugin() const { return static_cast(get_plugin(basic_family_id)); } - family_id get_user_sort_family_id() const { return m_user_sort_family_id; } + family_id get_user_sort_family_id() const { return user_sort_family_id; } - user_sort_plugin * get_user_sort_plugin() const { return static_cast(get_plugin(m_user_sort_family_id)); } + user_sort_plugin * get_user_sort_plugin() const { return static_cast(get_plugin(user_sort_family_id)); } /** \brief Debugging support method: set the next expression identifier to be the least value id' s.t. @@ -1771,7 +1716,7 @@ class ast_manager { sort * mk_fresh_sort(char const * prefix = ""); - bool is_uninterp(sort const * s) const { return s->get_family_id() == null_family_id || s->get_family_id() == m_user_sort_family_id; } + bool is_uninterp(sort const * s) const { return s->get_family_id() == null_family_id || s->get_family_id() == user_sort_family_id; } /** \brief A sort is "fully" interpreted if it is interpreted, @@ -1992,14 +1937,14 @@ class ast_manager { return is_label(n, pos, names)?(l = to_app(n)->get_arg(0), true):false; } - bool is_label(expr const * n) const { return is_app_of(n, m_label_family_id, OP_LABEL); } + bool is_label(expr const * n) const { return is_app_of(n, label_family_id, OP_LABEL); } bool is_label(expr const * n, expr*& l) const { return is_label(n)?(l = to_app(n)->get_arg(0), true):false; } bool is_label(expr const * n, bool& pos) const { - if (is_app_of(n, m_label_family_id, OP_LABEL)) { + if (is_app_of(n, label_family_id, OP_LABEL)) { pos = to_app(n)->get_decl()->get_parameter(0).get_int() != 0; return true; } @@ -2014,9 +1959,9 @@ class ast_manager { bool is_label_lit(expr const * n, buffer & names) const; - bool is_label_lit(expr const * n) const { return is_app_of(n, m_label_family_id, OP_LABEL_LIT); } + bool is_label_lit(expr const * n) const { return is_app_of(n, label_family_id, OP_LABEL_LIT); } - family_id get_label_family_id() const { return m_label_family_id; } + family_id get_label_family_id() const { return label_family_id; } app * mk_pattern(unsigned num_exprs, app * const * exprs); @@ -2134,16 +2079,16 @@ class ast_manager { public: - bool is_or(expr const * n) const { return is_app_of(n, m_basic_family_id, OP_OR); } - bool is_implies(expr const * n) const { return is_app_of(n, m_basic_family_id, OP_IMPLIES); } - bool is_and(expr const * n) const { return is_app_of(n, m_basic_family_id, OP_AND); } - bool is_not(expr const * n) const { return is_app_of(n, m_basic_family_id, OP_NOT); } - bool is_eq(expr const * n) const { return is_app_of(n, m_basic_family_id, OP_EQ); } + bool is_or(expr const * n) const { return is_app_of(n, basic_family_id, OP_OR); } + bool is_implies(expr const * n) const { return is_app_of(n, basic_family_id, OP_IMPLIES); } + bool is_and(expr const * n) const { return is_app_of(n, basic_family_id, OP_AND); } + bool is_not(expr const * n) const { return is_app_of(n, basic_family_id, OP_NOT); } + bool is_eq(expr const * n) const { return is_app_of(n, basic_family_id, OP_EQ); } bool is_iff(expr const * n) const { return is_eq(n) && is_bool(to_app(n)->get_arg(0)); } - bool is_oeq(expr const * n) const { return is_app_of(n, m_basic_family_id, OP_OEQ); } - bool is_distinct(expr const * n) const { return is_app_of(n, m_basic_family_id, OP_DISTINCT); } - bool is_xor(expr const * n) const { return is_app_of(n, m_basic_family_id, OP_XOR); } - bool is_ite(expr const * n) const { return is_app_of(n, m_basic_family_id, OP_ITE); } + bool is_oeq(expr const * n) const { return is_app_of(n, basic_family_id, OP_OEQ); } + bool is_distinct(expr const * n) const { return is_app_of(n, basic_family_id, OP_DISTINCT); } + bool is_xor(expr const * n) const { return is_app_of(n, basic_family_id, OP_XOR); } + bool is_ite(expr const * n) const { return is_app_of(n, basic_family_id, OP_ITE); } bool is_term_ite(expr const * n) const { return is_ite(n) && !is_bool(n); } bool is_true(expr const * n) const { return n == m_true; } bool is_false(expr const * n) const { return n == m_false; } @@ -2152,16 +2097,16 @@ class ast_manager { } bool is_complement(expr const * n1, expr const * n2) const { return is_complement_core(n1, n2) || is_complement_core(n2, n1); } - bool is_or(func_decl const * d) const { return is_decl_of(d, m_basic_family_id, OP_OR); } - bool is_implies(func_decl const * d) const { return is_decl_of(d, m_basic_family_id, OP_IMPLIES); } - bool is_and(func_decl const * d) const { return is_decl_of(d, m_basic_family_id, OP_AND); } - bool is_not(func_decl const * d) const { return is_decl_of(d, m_basic_family_id, OP_NOT); } - bool is_eq(func_decl const * d) const { return is_decl_of(d, m_basic_family_id, OP_EQ); } - bool is_iff(func_decl const * d) const { return is_decl_of(d, m_basic_family_id, OP_EQ) && is_bool(d->get_range()); } - bool is_xor(func_decl const * d) const { return is_decl_of(d, m_basic_family_id, OP_XOR); } - bool is_ite(func_decl const * d) const { return is_decl_of(d, m_basic_family_id, OP_ITE); } + bool is_or(func_decl const * d) const { return is_decl_of(d, basic_family_id, OP_OR); } + bool is_implies(func_decl const * d) const { return is_decl_of(d, basic_family_id, OP_IMPLIES); } + bool is_and(func_decl const * d) const { return is_decl_of(d, basic_family_id, OP_AND); } + bool is_not(func_decl const * d) const { return is_decl_of(d, basic_family_id, OP_NOT); } + bool is_eq(func_decl const * d) const { return is_decl_of(d, basic_family_id, OP_EQ); } + bool is_iff(func_decl const * d) const { return is_decl_of(d, basic_family_id, OP_EQ) && is_bool(d->get_range()); } + bool is_xor(func_decl const * d) const { return is_decl_of(d, basic_family_id, OP_XOR); } + bool is_ite(func_decl const * d) const { return is_decl_of(d, basic_family_id, OP_ITE); } bool is_term_ite(func_decl const * d) const { return is_ite(d) && !is_bool(d->get_range()); } - bool is_distinct(func_decl const * d) const { return is_decl_of(d, m_basic_family_id, OP_DISTINCT); } + bool is_distinct(func_decl const * d) const { return is_decl_of(d, basic_family_id, OP_DISTINCT); } public: @@ -2187,22 +2132,22 @@ class ast_manager { } public: - app * mk_eq(expr * lhs, expr * rhs) { return mk_app(m_basic_family_id, get_eq_op(lhs), lhs, rhs); } - app * mk_iff(expr * lhs, expr * rhs) { return mk_app(m_basic_family_id, OP_EQ, lhs, rhs); } - app * mk_oeq(expr * lhs, expr * rhs) { return mk_app(m_basic_family_id, OP_OEQ, lhs, rhs); } - app * mk_xor(expr * lhs, expr * rhs) { return mk_app(m_basic_family_id, OP_XOR, lhs, rhs); } - app * mk_ite(expr * c, expr * t, expr * e) { return mk_app(m_basic_family_id, OP_ITE, c, t, e); } - app * mk_xor(unsigned num_args, expr * const * args) { return mk_app(m_basic_family_id, OP_XOR, num_args, args); } + app * mk_eq(expr * lhs, expr * rhs) { return mk_app(basic_family_id, get_eq_op(lhs), lhs, rhs); } + app * mk_iff(expr * lhs, expr * rhs) { return mk_app(basic_family_id, OP_EQ, lhs, rhs); } + app * mk_oeq(expr * lhs, expr * rhs) { return mk_app(basic_family_id, OP_OEQ, lhs, rhs); } + app * mk_xor(expr * lhs, expr * rhs) { return mk_app(basic_family_id, OP_XOR, lhs, rhs); } + app * mk_ite(expr * c, expr * t, expr * e) { return mk_app(basic_family_id, OP_ITE, c, t, e); } + app * mk_xor(unsigned num_args, expr * const * args) { return mk_app(basic_family_id, OP_XOR, num_args, args); } app * mk_xor(ptr_buffer const& args) { return mk_xor(args.size(), args.c_ptr()); } app * mk_xor(ptr_vector const& args) { return mk_xor(args.size(), args.c_ptr()); } app * mk_xor(ref_buffer const& args) { return mk_xor(args.size(), args.c_ptr()); } - app * mk_or(unsigned num_args, expr * const * args) { return mk_app(m_basic_family_id, OP_OR, num_args, args); } - app * mk_and(unsigned num_args, expr * const * args) { return mk_app(m_basic_family_id, OP_AND, num_args, args); } - app * mk_or(expr * arg1, expr * arg2) { return mk_app(m_basic_family_id, OP_OR, arg1, arg2); } - app * mk_and(expr * arg1, expr * arg2) { return mk_app(m_basic_family_id, OP_AND, arg1, arg2); } - app * mk_or(expr * arg1, expr * arg2, expr * arg3) { return mk_app(m_basic_family_id, OP_OR, arg1, arg2, arg3); } - app * mk_or(expr* a, expr* b, expr* c, expr* d) { expr* args[4] = { a, b, c, d }; return mk_app(m_basic_family_id, OP_OR, 4, args); } - app * mk_and(expr * arg1, expr * arg2, expr * arg3) { return mk_app(m_basic_family_id, OP_AND, arg1, arg2, arg3); } + app * mk_or(unsigned num_args, expr * const * args) { return mk_app(basic_family_id, OP_OR, num_args, args); } + app * mk_and(unsigned num_args, expr * const * args) { return mk_app(basic_family_id, OP_AND, num_args, args); } + app * mk_or(expr * arg1, expr * arg2) { return mk_app(basic_family_id, OP_OR, arg1, arg2); } + app * mk_and(expr * arg1, expr * arg2) { return mk_app(basic_family_id, OP_AND, arg1, arg2); } + app * mk_or(expr * arg1, expr * arg2, expr * arg3) { return mk_app(basic_family_id, OP_OR, arg1, arg2, arg3); } + app * mk_or(expr* a, expr* b, expr* c, expr* d) { expr* args[4] = { a, b, c, d }; return mk_app(basic_family_id, OP_OR, 4, args); } + app * mk_and(expr * arg1, expr * arg2, expr * arg3) { return mk_app(basic_family_id, OP_AND, arg1, arg2, arg3); } app * mk_and(ref_vector const& args) { return mk_and(args.size(), args.c_ptr()); } app * mk_and(ptr_vector const& args) { return mk_and(args.size(), args.c_ptr()); } @@ -2212,8 +2157,8 @@ class ast_manager { app * mk_or(ptr_vector const& args) { return mk_or(args.size(), args.c_ptr()); } app * mk_or(ref_buffer const& args) { return mk_or(args.size(), args.c_ptr()); } app * mk_or(ptr_buffer const& args) { return mk_or(args.size(), args.c_ptr()); } - app * mk_implies(expr * arg1, expr * arg2) { return mk_app(m_basic_family_id, OP_IMPLIES, arg1, arg2); } - app * mk_not(expr * n) { return mk_app(m_basic_family_id, OP_NOT, n); } + app * mk_implies(expr * arg1, expr * arg2) { return mk_app(basic_family_id, OP_IMPLIES, arg1, arg2); } + app * mk_not(expr * n) { return mk_app(basic_family_id, OP_NOT, n); } app * mk_distinct(unsigned num_args, expr * const * args); app * mk_distinct_expanded(unsigned num_args, expr * const * args); app * mk_true() const { return m_true; } @@ -2223,12 +2168,12 @@ class ast_manager { func_decl* mk_and_decl() { sort* domain[2] = { m_bool_sort, m_bool_sort }; - return mk_func_decl(m_basic_family_id, OP_AND, 0, nullptr, 2, domain); + return mk_func_decl(basic_family_id, OP_AND, 0, nullptr, 2, domain); } - func_decl* mk_not_decl() { return mk_func_decl(m_basic_family_id, OP_NOT, 0, nullptr, 1, &m_bool_sort); } + func_decl* mk_not_decl() { return mk_func_decl(basic_family_id, OP_NOT, 0, nullptr, 1, &m_bool_sort); } func_decl* mk_or_decl() { sort* domain[2] = { m_bool_sort, m_bool_sort }; - return mk_func_decl(m_basic_family_id, OP_OR, 0, nullptr, 2, domain); + return mk_func_decl(basic_family_id, OP_OR, 0, nullptr, 2, domain); } // ----------------------------------- @@ -2241,8 +2186,8 @@ class ast_manager { some_value_proc * m_some_value_proc; public: app * mk_model_value(unsigned idx, sort * s); - bool is_model_value(expr const * n) const { return is_app_of(n, m_model_value_family_id, OP_MODEL_VALUE); } - bool is_model_value(func_decl const * d) const { return is_decl_of(d, m_model_value_family_id, OP_MODEL_VALUE); } + bool is_model_value(expr const * n) const { return is_app_of(n, model_value_family_id, OP_MODEL_VALUE); } + bool is_model_value(func_decl const * d) const { return is_decl_of(d, model_value_family_id, OP_MODEL_VALUE); } expr * get_some_value(sort * s, some_value_proc * p); expr * get_some_value(sort * s); @@ -2276,26 +2221,26 @@ class ast_manager { bool is_undef_proof(expr const * e) const { return e == m_undef_proof; } - bool is_asserted(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_ASSERTED); } - bool is_hypothesis (expr const *e) const {return is_app_of (e, m_basic_family_id, PR_HYPOTHESIS);} - bool is_goal(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_GOAL); } - bool is_modus_ponens(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_MODUS_PONENS); } - bool is_reflexivity(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_REFLEXIVITY); } - bool is_symmetry(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_SYMMETRY); } - bool is_transitivity(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_TRANSITIVITY); } - bool is_monotonicity(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_MONOTONICITY); } - bool is_quant_intro(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_QUANT_INTRO); } - bool is_quant_inst(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_QUANT_INST); } - bool is_distributivity(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_DISTRIBUTIVITY); } - bool is_and_elim(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_AND_ELIM); } - bool is_not_or_elim(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_NOT_OR_ELIM); } - bool is_rewrite(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_REWRITE); } - bool is_rewrite_star(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_REWRITE_STAR); } - bool is_unit_resolution(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_UNIT_RESOLUTION); } - bool is_lemma(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_LEMMA); } + bool is_asserted(expr const * e) const { return is_app_of(e, basic_family_id, PR_ASSERTED); } + bool is_hypothesis (expr const *e) const {return is_app_of (e, basic_family_id, PR_HYPOTHESIS);} + bool is_goal(expr const * e) const { return is_app_of(e, basic_family_id, PR_GOAL); } + bool is_modus_ponens(expr const * e) const { return is_app_of(e, basic_family_id, PR_MODUS_PONENS); } + bool is_reflexivity(expr const * e) const { return is_app_of(e, basic_family_id, PR_REFLEXIVITY); } + bool is_symmetry(expr const * e) const { return is_app_of(e, basic_family_id, PR_SYMMETRY); } + bool is_transitivity(expr const * e) const { return is_app_of(e, basic_family_id, PR_TRANSITIVITY); } + bool is_monotonicity(expr const * e) const { return is_app_of(e, basic_family_id, PR_MONOTONICITY); } + bool is_quant_intro(expr const * e) const { return is_app_of(e, basic_family_id, PR_QUANT_INTRO); } + bool is_quant_inst(expr const * e) const { return is_app_of(e, basic_family_id, PR_QUANT_INST); } + bool is_distributivity(expr const * e) const { return is_app_of(e, basic_family_id, PR_DISTRIBUTIVITY); } + bool is_and_elim(expr const * e) const { return is_app_of(e, basic_family_id, PR_AND_ELIM); } + bool is_not_or_elim(expr const * e) const { return is_app_of(e, basic_family_id, PR_NOT_OR_ELIM); } + bool is_rewrite(expr const * e) const { return is_app_of(e, basic_family_id, PR_REWRITE); } + bool is_rewrite_star(expr const * e) const { return is_app_of(e, basic_family_id, PR_REWRITE_STAR); } + bool is_unit_resolution(expr const * e) const { return is_app_of(e, basic_family_id, PR_UNIT_RESOLUTION); } + bool is_lemma(expr const * e) const { return is_app_of(e, basic_family_id, PR_LEMMA); } bool is_quant_inst(expr const* e, expr*& not_q_or_i, ptr_vector& binding) const; bool is_rewrite(expr const* e, expr*& r1, expr*& r2) const; - bool is_hyper_resolve(proof* p) const { return is_app_of(p, m_basic_family_id, PR_HYPER_RESOLVE); } + bool is_hyper_resolve(proof* p) const { return is_app_of(p, basic_family_id, PR_HYPER_RESOLVE); } bool is_hyper_resolve(proof* p, ref_vector& premises, obj_ref& conclusion, @@ -2303,9 +2248,9 @@ class ast_manager { vector >& substs); - bool is_def_intro(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_DEF_INTRO); } - bool is_apply_def(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_APPLY_DEF); } - bool is_skolemize(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_SKOLEMIZE); } + bool is_def_intro(expr const * e) const { return is_app_of(e, basic_family_id, PR_DEF_INTRO); } + bool is_apply_def(expr const * e) const { return is_app_of(e, basic_family_id, PR_APPLY_DEF); } + bool is_skolemize(expr const * e) const { return is_app_of(e, basic_family_id, PR_SKOLEMIZE); } MATCH_UNARY(is_asserted); MATCH_UNARY(is_hypothesis);