Skip to content

Commit

Permalink
constify ids of builtin AST families + remove some dead code
Browse files Browse the repository at this point in the history
  • Loading branch information
@nunoplopes
nunoplopes committed Apr 4, 2021
1 parent c47ab02 commit a6ef99d
Show file tree
Hide file tree
Showing 4 changed files with 314 additions and 435 deletions.
37 changes: 18 additions & 19 deletions src/ast/arith_decl_plugin.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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();
Expand All @@ -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);
}


Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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;
}
Expand All @@ -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 {
Expand Down
Loading

0 comments on commit a6ef99d

Please sign in to comment.