mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 03:07:07 +00:00
Code Activity

constify ids of builtin AST families + remove some dead code

Browse source
This commit is contained in:
Nuno Lopes 2021-04-04 18:13:52 +01:00
parent c47ab023e5
commit a6ef99d56e
4 changed files with 308 additions and 429 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

37
src/ast/arith_decl_plugin.cpp
View file

@ -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<arith_decl_plugin*>(m_manager.get_plugin(m_afid));
m_plugin = static_cast<arith_decl_plugin*>(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 {

188
src/ast/arith_decl_plugin.h
View file

@ -233,14 +233,10 @@ public:
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 arith_family_id; }
family_id get_family_id() const { return m_afid; }
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 @@ public:
}
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 @@ public:
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_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, 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_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, 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_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, m_afid, INT_SORT); }
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 @@ public:
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 @@ public:
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_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(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_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_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(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_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(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_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

219
src/ast/ast.cpp
View file

@ -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<expr * const *>(nullptr)))
if (decl == mk_func_decl(basic_family_id, PR_UNDEF, 0, nullptr, 0, static_cast<expr * const *>(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<int>(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<symbol> & 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<parameter> 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<symbol> & 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<expr> &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<expr> & 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<expr * const *>(nullptr));
return mk_app(model_value_family_id, OP_MODEL_VALUE, 2, p, 0, static_cast<expr * const *>(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<expr> 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<expr> 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<expr> 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<expr>& 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<expr> 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<expr> 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<expr> 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<expr> 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<expr> 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;
}

293
src/ast/ast.h
View file

@ -75,6 +75,14 @@ public:
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<func_decl> m_eq_decls; // cached eqs
ptr_vector<func_decl> m_ite_decls; // cached ites
ptr_vector<func_decl> 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<func_decl> m_monotonicity_decls;
ptr_vector<func_decl> m_transitivity_star_decls;
ptr_vector<func_decl> m_distributivity_decls;
ptr_vector<func_decl> m_assoc_flat_decls;
ptr_vector<func_decl> 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<func_decl> 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<func_decl> m_apply_def_decls;
ptr_vector<func_decl> m_nnf_pos_decls;
ptr_vector<func_decl> m_nnf_neg_decls;
ptr_vector<func_decl> 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 @@ protected:
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 @@ protected:
ptr_vector<decl_plugin> 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<func_decl, quantifier*> m_lambda_defs;
id_gen m_expr_id_gen;
@ -1616,13 +1567,7 @@ public:
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 @@ public:
void get_range(svector<family_id> & 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<basic_decl_plugin*>(get_plugin(m_basic_family_id)); }
basic_decl_plugin * get_basic_decl_plugin() const { return static_cast<basic_decl_plugin*>(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<user_sort_plugin*>(get_plugin(m_user_sort_family_id)); }
user_sort_plugin * get_user_sort_plugin() const { return static_cast<user_sort_plugin*>(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 @@ public:
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 @@ public:
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 @@ public:
bool is_label_lit(expr const * n, buffer<symbol> & 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 @@ public:
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 @@ public:
}
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 @@ public:
}
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<expr> const& args) { return mk_xor(args.size(), args.c_ptr()); }
app * mk_xor(ptr_vector<expr> const& args) { return mk_xor(args.size(), args.c_ptr()); }
app * mk_xor(ref_buffer<expr, ast_manager> 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<expr, ast_manager> const& args) { return mk_and(args.size(), args.c_ptr()); }
app * mk_and(ptr_vector<expr> const& args) { return mk_and(args.size(), args.c_ptr()); }
@ -2212,8 +2157,8 @@ public:
app * mk_or(ptr_vector<expr> const& args) { return mk_or(args.size(), args.c_ptr()); }
app * mk_or(ref_buffer<expr, ast_manager> const& args) { return mk_or(args.size(), args.c_ptr()); }
app * mk_or(ptr_buffer<expr> 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 @@ public:
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 @@ protected:
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 @@ public:
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<expr>& 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<proof, ast_manager>& premises,
obj_ref<expr, ast_manager>& conclusion,
@ -2303,9 +2248,9 @@ public:
vector<ref_vector<expr, ast_manager> >& 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);