Skip to content

Commit a6ef99d

Browse files
nunoplopesnunoplopes
committed
constify ids of builtin AST families + remove some dead code
1 parent c47ab02 commit a6ef99d

4 files changed

Lines changed: 314 additions & 435 deletions

File tree

‎src/ast/arith_decl_plugin.cpp‎

Lines changed: 18 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -696,7 +696,7 @@ expr * arith_decl_plugin::get_some_value(sort * s) {
696696
}
697697

698698
bool arith_recognizers::is_numeral(expr const * n, rational & val, bool & is_int) const {
699-
if (!is_app_of(n, m_afid, OP_NUM))
699+
if (!is_app_of(n, arith_family_id, OP_NUM))
700700
return false;
701701
func_decl * decl = to_app(n)->get_decl();
702702
val = decl->get_parameter(0).get_rational();
@@ -706,7 +706,7 @@ bool arith_recognizers::is_numeral(expr const * n, rational & val, bool & is_int
706706

707707

708708
bool arith_recognizers::is_irrational_algebraic_numeral(expr const * n) const {
709-
return is_app(n) && to_app(n)->is_app_of(m_afid, OP_IRRATIONAL_ALGEBRAIC_NUM);
709+
return is_app(n) && to_app(n)->is_app_of(arith_family_id, OP_IRRATIONAL_ALGEBRAIC_NUM);
710710
}
711711

712712

@@ -740,18 +740,17 @@ bool arith_recognizers::is_int_expr(expr const *e) const {
740740
}
741741

742742
arith_util::arith_util(ast_manager & m):
743-
arith_recognizers(m.mk_family_id("arith")),
744743
m_manager(m),
745744
m_plugin(nullptr) {
746745
}
747746

748747
void arith_util::init_plugin() {
749748
SASSERT(m_plugin == 0);
750-
m_plugin = static_cast<arith_decl_plugin*>(m_manager.get_plugin(m_afid));
749+
m_plugin = static_cast<arith_decl_plugin*>(m_manager.get_plugin(arith_family_id));
751750
}
752751

753752
bool arith_util::is_irrational_algebraic_numeral2(expr const * n, algebraic_numbers::anum & val) {
754-
if (!is_app_of(n, m_afid, OP_IRRATIONAL_ALGEBRAIC_NUM))
753+
if (!is_app_of(n, arith_family_id, OP_IRRATIONAL_ALGEBRAIC_NUM))
755754
return false;
756755
am().set(val, to_irrational_algebraic_numeral(n));
757756
return true;
@@ -806,26 +805,26 @@ expr_ref arith_util::mk_add_simplify(unsigned sz, expr* const* args) {
806805

807806
bool arith_util::is_considered_uninterpreted(func_decl* f, unsigned n, expr* const* args, func_decl_ref& f_out) {
808807
rational r;
809-
if (is_decl_of(f, m_afid, OP_DIV) && n == 2 && is_numeral(args[1], r) && r.is_zero()) {
808+
if (is_decl_of(f, arith_family_id, OP_DIV) && n == 2 && is_numeral(args[1], r) && r.is_zero()) {
810809
f_out = mk_div0();
811810
return true;
812811
}
813-
if (is_decl_of(f, m_afid, OP_IDIV) && n == 2 && is_numeral(args[1], r) && r.is_zero()) {
812+
if (is_decl_of(f, arith_family_id, OP_IDIV) && n == 2 && is_numeral(args[1], r) && r.is_zero()) {
814813
sort* rs[2] = { mk_int(), mk_int() };
815-
f_out = m_manager.mk_func_decl(m_afid, OP_IDIV0, 0, nullptr, 2, rs, mk_int());
814+
f_out = m_manager.mk_func_decl(arith_family_id, OP_IDIV0, 0, nullptr, 2, rs, mk_int());
816815
return true;
817816
}
818-
if (is_decl_of(f, m_afid, OP_MOD) && n == 2 && is_numeral(args[1], r) && r.is_zero()) {
817+
if (is_decl_of(f, arith_family_id, OP_MOD) && n == 2 && is_numeral(args[1], r) && r.is_zero()) {
819818
sort* rs[2] = { mk_int(), mk_int() };
820-
f_out = m_manager.mk_func_decl(m_afid, OP_MOD0, 0, nullptr, 2, rs, mk_int());
819+
f_out = m_manager.mk_func_decl(arith_family_id, OP_MOD0, 0, nullptr, 2, rs, mk_int());
821820
return true;
822821
}
823-
if (is_decl_of(f, m_afid, OP_REM) && n == 2 && is_numeral(args[1], r) && r.is_zero()) {
822+
if (is_decl_of(f, arith_family_id, OP_REM) && n == 2 && is_numeral(args[1], r) && r.is_zero()) {
824823
sort* rs[2] = { mk_int(), mk_int() };
825-
f_out = m_manager.mk_func_decl(m_afid, OP_REM0, 0, nullptr, 2, rs, mk_int());
824+
f_out = m_manager.mk_func_decl(arith_family_id, OP_REM0, 0, nullptr, 2, rs, mk_int());
826825
return true;
827826
}
828-
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()) {
827+
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()) {
829828
f_out = is_int(args[0]) ? mk_ipower0() : mk_rpower0();
830829
return true;
831830
}
@@ -837,33 +836,33 @@ bool arith_util::is_considered_uninterpreted(func_decl* f, unsigned n, expr* con
837836
func_decl* arith_util::mk_ipower0() {
838837
sort* s = mk_int();
839838
sort* rs[2] = { s, s };
840-
return m_manager.mk_func_decl(m_afid, OP_POWER0, 0, nullptr, 2, rs, s);
839+
return m_manager.mk_func_decl(arith_family_id, OP_POWER0, 0, nullptr, 2, rs, s);
841840
}
842841

843842
func_decl* arith_util::mk_rpower0() {
844843
sort* s = mk_real();
845844
sort* rs[2] = { s, s };
846-
return m_manager.mk_func_decl(m_afid, OP_POWER0, 0, nullptr, 2, rs, s);
845+
return m_manager.mk_func_decl(arith_family_id, OP_POWER0, 0, nullptr, 2, rs, s);
847846
}
848847

849848
func_decl* arith_util::mk_div0() {
850849
sort* rs[2] = { mk_real(), mk_real() };
851-
return m_manager.mk_func_decl(m_afid, OP_DIV0, 0, nullptr, 2, rs, mk_real());
850+
return m_manager.mk_func_decl(arith_family_id, OP_DIV0, 0, nullptr, 2, rs, mk_real());
852851
}
853852

854853
func_decl* arith_util::mk_idiv0() {
855854
sort* rs[2] = { mk_int(), mk_int() };
856-
return m_manager.mk_func_decl(m_afid, OP_IDIV0, 0, nullptr, 2, rs, mk_int());
855+
return m_manager.mk_func_decl(arith_family_id, OP_IDIV0, 0, nullptr, 2, rs, mk_int());
857856
}
858857

859858
func_decl* arith_util::mk_rem0() {
860859
sort* rs[2] = { mk_int(), mk_int() };
861-
return m_manager.mk_func_decl(m_afid, OP_REM0, 0, nullptr, 2, rs, mk_int());
860+
return m_manager.mk_func_decl(arith_family_id, OP_REM0, 0, nullptr, 2, rs, mk_int());
862861
}
863862

864863
func_decl* arith_util::mk_mod0() {
865864
sort* rs[2] = { mk_int(), mk_int() };
866-
return m_manager.mk_func_decl(m_afid, OP_MOD0, 0, nullptr, 2, rs, mk_int());
865+
return m_manager.mk_func_decl(arith_family_id, OP_MOD0, 0, nullptr, 2, rs, mk_int());
867866
}
868867

869868
bool arith_util::is_bounded(expr* n) const {

0 commit comments

Comments
 (0)