diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp index 01b671c99..03ee77458 100644 --- a/src/ast/arith_decl_plugin.cpp +++ b/src/ast/arith_decl_plugin.cpp @@ -215,18 +215,8 @@ void arith_decl_plugin::set_manager(ast_manager * m, family_id id) { m_e = m->mk_const(e_decl); m->inc_ref(m_e); - func_decl * z_pw_z_int = m->mk_const_decl(symbol("0^0-int"), i, func_decl_info(id, OP_0_PW_0_INT)); - m_0_pw_0_int = m->mk_const(z_pw_z_int); - m->inc_ref(m_0_pw_0_int); - - func_decl * z_pw_z_real = m->mk_const_decl(symbol("0^0-real"), r, func_decl_info(id, OP_0_PW_0_REAL)); - m_0_pw_0_real = m->mk_const(z_pw_z_real); - m->inc_ref(m_0_pw_0_real); MK_OP(m_neg_root_decl, "neg-root", OP_NEG_ROOT, r); - MK_UNARY(m_div_0_decl, "/0", OP_DIV_0, r); - MK_UNARY(m_idiv_0_decl, "div0", OP_IDIV_0, i); - MK_UNARY(m_mod_0_decl, "mod0", OP_MOD_0, i); MK_UNARY(m_u_asin_decl, "asin-u", OP_U_ASIN, r); MK_UNARY(m_u_acos_decl, "acos-u", OP_U_ACOS, r); } @@ -279,12 +269,7 @@ arith_decl_plugin::arith_decl_plugin(): m_atanh_decl(0), m_pi(0), m_e(0), - m_0_pw_0_int(0), - m_0_pw_0_real(0), m_neg_root_decl(0), - m_div_0_decl(0), - m_idiv_0_decl(0), - m_mod_0_decl(0), m_u_asin_decl(0), m_u_acos_decl(0), m_convert_int_numerals_to_real(false) { @@ -339,12 +324,7 @@ void arith_decl_plugin::finalize() { DEC_REF(m_atanh_decl); DEC_REF(m_pi); DEC_REF(m_e); - DEC_REF(m_0_pw_0_int); - DEC_REF(m_0_pw_0_real); DEC_REF(m_neg_root_decl); - DEC_REF(m_div_0_decl); - DEC_REF(m_idiv_0_decl); - DEC_REF(m_mod_0_decl); DEC_REF(m_u_asin_decl); DEC_REF(m_u_acos_decl); m_manager->dec_array_ref(m_small_ints.size(), m_small_ints.c_ptr()); @@ -392,12 +372,12 @@ inline func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, bool is_real) { case OP_ATANH: return m_atanh_decl; case OP_PI: return m_pi->get_decl(); case OP_E: return m_e->get_decl(); - case OP_0_PW_0_INT: return m_0_pw_0_int->get_decl(); - case OP_0_PW_0_REAL: return m_0_pw_0_real->get_decl(); + //case OP_0_PW_0_INT: return m_0_pw_0_int->get_decl(); + //case OP_0_PW_0_REAL: return m_0_pw_0_real->get_decl(); case OP_NEG_ROOT: return m_neg_root_decl; - case OP_DIV_0: return m_div_0_decl; - case OP_IDIV_0: return m_idiv_0_decl; - case OP_MOD_0: return m_mod_0_decl; + //case OP_DIV_0: return m_div_0_decl; + //case OP_IDIV_0: return m_idiv_0_decl; + //case OP_MOD_0: return m_mod_0_decl; case OP_U_ASIN: return m_u_asin_decl; case OP_U_ACOS: return m_u_acos_decl; default: return 0; @@ -489,9 +469,9 @@ static bool has_real_arg(ast_manager * m, unsigned num_args, expr * const * args static bool is_const_op(decl_kind k) { return k == OP_PI || - k == OP_E || - k == OP_0_PW_0_INT || - k == OP_0_PW_0_REAL; + k == OP_E; + //k == OP_0_PW_0_INT || + //k == OP_0_PW_0_REAL; } func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h index a66ddd967..4b24ea5e6 100644 --- a/src/ast/arith_decl_plugin.h +++ b/src/ast/arith_decl_plugin.h @@ -70,12 +70,7 @@ enum arith_op_kind { OP_PI, OP_E, // under-specified symbols - OP_0_PW_0_INT, // 0^0 for integers - OP_0_PW_0_REAL, // 0^0 for reals OP_NEG_ROOT, // x^n when n is even and x is negative - OP_DIV_0, // x/0 - OP_IDIV_0, // x div 0 - OP_MOD_0, // x mod 0 OP_U_ASIN, // asin(x) for x < -1 or x > 1 OP_U_ACOS, // acos(x) for x < -1 or x > 1 LAST_ARITH_OP @@ -141,12 +136,7 @@ protected: app * m_pi; app * m_e; - app * m_0_pw_0_int; - app * m_0_pw_0_real; func_decl * m_neg_root_decl; - func_decl * m_div_0_decl; - func_decl * m_idiv_0_decl; - func_decl * m_mod_0_decl; func_decl * m_u_asin_decl; func_decl * m_u_acos_decl; ptr_vector m_small_ints; @@ -207,10 +197,6 @@ public: app * mk_e() const { return m_e; } - app * mk_0_pw_0_int() const { return m_0_pw_0_int; } - - app * mk_0_pw_0_real() const { return m_0_pw_0_real; } - virtual expr * get_some_value(sort * s); virtual bool is_considered_uninterpreted(func_decl * f) { @@ -218,12 +204,7 @@ public: return false; switch (f->get_decl_kind()) { - case OP_0_PW_0_INT: - case OP_0_PW_0_REAL: case OP_NEG_ROOT: - case OP_DIV_0: - case OP_IDIV_0: - case OP_MOD_0: case OP_U_ASIN: case OP_U_ACOS: return true; @@ -276,9 +257,9 @@ public: 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_DIV_0); } + //bool is_div0(expr const * n) const { return is_app_of(n, m_afid, OP_DIV_0); } 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_IDIV_0); } + //bool is_idiv0(expr const * n) const { return is_app_of(n, m_afid, OP_IDIV_0); } 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_to_real(expr const * n) const { return is_app_of(n, m_afid, OP_TO_REAL); } @@ -389,16 +370,16 @@ public: 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_add(unsigned num_args, expr * const * args) { return m_manager.mk_app(m_afid, OP_ADD, num_args, args); } - app * mk_add(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_ADD, arg1, arg2); } - app * mk_add(expr * arg1, expr * arg2, expr* arg3) { return m_manager.mk_app(m_afid, OP_ADD, arg1, arg2, arg3); } + app * mk_add(unsigned num_args, expr * const * args) const { return 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_sub(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_SUB, arg1, arg2); } - app * mk_sub(unsigned num_args, expr * const * args) { return m_manager.mk_app(m_afid, OP_SUB, num_args, args); } - app * mk_mul(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_MUL, arg1, arg2); } - app * mk_mul(expr * arg1, expr * arg2, expr* arg3) { return m_manager.mk_app(m_afid, OP_MUL, arg1, arg2, arg3); } - app * mk_mul(unsigned num_args, expr * const * args) { return m_manager.mk_app(m_afid, OP_MUL, num_args, args); } - app * mk_uminus(expr * arg) { return m_manager.mk_app(m_afid, OP_UMINUS, arg); } + 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 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); } @@ -425,11 +406,6 @@ public: app * mk_pi() { return plugin().mk_pi(); } app * mk_e() { return plugin().mk_e(); } - app * mk_0_pw_0_int() { return plugin().mk_0_pw_0_int(); } - app * mk_0_pw_0_real() { return plugin().mk_0_pw_0_real(); } - app * mk_div0(expr * arg) { return m_manager.mk_app(m_afid, OP_DIV_0, arg); } - app * mk_idiv0(expr * arg) { return m_manager.mk_app(m_afid, OP_IDIV_0, arg); } - app * mk_mod0(expr * arg) { return m_manager.mk_app(m_afid, OP_MOD_0, arg); } 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); } diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index 18556b71b..fc9b1ac1d 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -680,8 +680,7 @@ br_status arith_rewriter::mk_div_core(expr * arg1, expr * arg2, expr_ref & resul if (m_util.is_numeral(arg2, v2, is_int)) { SASSERT(!is_int); if (v2.is_zero()) { - result = m_util.mk_div0(arg1); - return BR_REWRITE1; + return BR_FAILED; } else if (m_util.is_numeral(arg1, v1, is_int)) { result = m_util.mk_numeral(v1/v2, false); @@ -734,10 +733,6 @@ br_status arith_rewriter::mk_idiv_core(expr * arg1, expr * arg2, expr_ref & resu result = m_util.mk_numeral(div(v1, v2), is_int); return BR_DONE; } - if (m_util.is_numeral(arg2, v2, is_int) && v2.is_zero()) { - result = m_util.mk_idiv0(arg1); - return BR_REWRITE1; - } return BR_FAILED; } diff --git a/src/ast/simplifier/arith_simplifier_plugin.cpp b/src/ast/simplifier/arith_simplifier_plugin.cpp index 8410ce143..bfe72b232 100644 --- a/src/ast/simplifier/arith_simplifier_plugin.cpp +++ b/src/ast/simplifier/arith_simplifier_plugin.cpp @@ -405,8 +405,6 @@ bool arith_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * co case OP_POWER: return false; case OP_ABS: SASSERT(num_args == 1); mk_abs(args[0], result); break; case OP_IRRATIONAL_ALGEBRAIC_NUM: return false; - case OP_DIV_0: return false; - case OP_IDIV_0: return false; default: return false; } diff --git a/src/qe/nlqsat.cpp b/src/qe/nlqsat.cpp index 0f2437982..3e5a9f24f 100644 --- a/src/qe/nlqsat.cpp +++ b/src/qe/nlqsat.cpp @@ -444,16 +444,12 @@ namespace qe { div_rewriter_cfg(nlqsat& s): m(s.m), a(s.m), m_zero(a.mk_real(0), m) {} ~div_rewriter_cfg() {} br_status reduce_app(func_decl* f, unsigned sz, expr* const* args, expr_ref& result, proof_ref& pr) { - if (is_decl_of(f, a.get_family_id(), OP_DIV) && sz == 2 && !a.is_numeral(args[1])) { + rational r; + if (is_decl_of(f, a.get_family_id(), OP_DIV) && sz == 2 && (!a.is_numeral(args[1], r) || r.is_zero())) { result = m.mk_fresh_const("div", a.mk_real()); m_divs.push_back(div(m, args[0], args[1], to_app(result))); return BR_DONE; } - if (is_decl_of(f, a.get_family_id(), OP_DIV_0) && sz == 1 && !a.is_numeral(args[0])) { - result = m.mk_fresh_const("div", a.mk_real()); - m_divs.push_back(div(m, args[0], m_zero, to_app(result))); - return BR_DONE; - } return BR_FAILED; } vector
const& divs() const { return m_divs; } @@ -507,10 +503,6 @@ namespace qe { m_has_divs = true; return; } - if (a.is_div0(n) && s.m_mode == qsat_t) { - m_has_divs = true; - return; - } TRACE("qe", tout << "not NRA: " << mk_pp(n, s.m) << "\n";); throw tactic_exception("not NRA"); } diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index a30e51133..b5e7db310 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -395,7 +395,8 @@ namespace smt { template theory_var theory_arith::internalize_div(app * n) { - if (!m_util.is_numeral(n->get_arg(1))) found_underspecified_op(n); + rational r; + if (!m_util.is_numeral(n->get_arg(1), r) || r.is_zero()) found_underspecified_op(n); found_underspecified_op(n); theory_var s = mk_binary_op(n); context & ctx = get_context(); @@ -406,7 +407,8 @@ namespace smt { template theory_var theory_arith::internalize_idiv(app * n) { - found_underspecified_op(n); + rational r; + if (!m_util.is_numeral(n->get_arg(1), r) || r.is_zero()) found_underspecified_op(n); theory_var s = mk_binary_op(n); context & ctx = get_context(); app * mod = m_util.mk_mod(n->get_arg(0), n->get_arg(1)); @@ -419,7 +421,8 @@ namespace smt { template theory_var theory_arith::internalize_mod(app * n) { TRACE("arith_mod", tout << "internalizing...\n" << mk_pp(n, get_manager()) << "\n";); - if (!m_util.is_numeral(n->get_arg(1))) found_underspecified_op(n); + rational r; + if (!m_util.is_numeral(n->get_arg(1), r) || r.is_zero()) found_underspecified_op(n); theory_var s = mk_binary_op(n); context & ctx = get_context(); if (!ctx.relevancy()) @@ -429,7 +432,8 @@ namespace smt { template theory_var theory_arith::internalize_rem(app * n) { - if (!m_util.is_numeral(n->get_arg(1))) found_underspecified_op(n); + rational r; + if (!m_util.is_numeral(n->get_arg(1), r) || r.is_zero()) found_underspecified_op(n); theory_var s = mk_binary_op(n); context & ctx = get_context(); if (!ctx.relevancy()) { @@ -734,11 +738,6 @@ namespace smt { return internalize_div(n); else if (m_util.is_idiv(n)) return internalize_idiv(n); - else if (is_app_of(n, get_id(), OP_IDIV_0) || is_app_of(n, get_id(), OP_DIV_0)) { - ctx.internalize(n->get_arg(0), false); - enode * e = mk_enode(n); - return mk_var(e); - } else if (m_util.is_mod(n)) return internalize_mod(n); else if (m_util.is_rem(n)) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 124fea910..c5e3ae350 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -292,9 +292,6 @@ namespace smt { } void found_not_handled(expr* n) { - if (a.is_div0(n)) { - return; - } m_not_handled = n; if (is_app(n) && is_underspecified(to_app(n))) { m_underspecified.push_back(to_app(n)); @@ -379,7 +376,12 @@ namespace smt { } else if (is_app(n) && a.get_family_id() == to_app(n)->get_family_id()) { app* t = to_app(n); - found_not_handled(n); + if (a.is_div(n, n1, n2) && is_numeral(n2, r)) { + // skip + } + else { + found_not_handled(n); + } internalize_args(t); mk_enode(t); theory_var v = mk_var(n); diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp index 0443a51ed..7e89794ce 100644 --- a/src/tactic/arith/purify_arith_tactic.cpp +++ b/src/tactic/arith/purify_arith_tactic.cpp @@ -297,11 +297,11 @@ struct purify_arith_proc { push_cnstr(OR(EQ(y, mk_real_zero()), EQ(u().mk_mul(y, k), x))); push_cnstr_pr(result_pr); - - if (complete()) { + rational r; + if (complete() && (!u().is_numeral(y, r) || r.is_zero())) { // y != 0 \/ k = div-0(x) push_cnstr(OR(NOT(EQ(y, mk_real_zero())), - EQ(k, u().mk_div0(x)))); + EQ(k, u().mk_div(x, mk_real_zero())))); push_cnstr_pr(result_pr); } } @@ -348,11 +348,12 @@ struct purify_arith_proc { push_cnstr(OR(u().mk_ge(y, zero), u().mk_lt(k2, u().mk_mul(u().mk_numeral(rational(-1), true), y)))); push_cnstr_pr(mod_pr); - if (complete()) { - push_cnstr(OR(NOT(EQ(y, zero)), EQ(k1, u().mk_idiv0(x)))); + rational r; + if (complete() && (!u().is_numeral(y, r) || r.is_zero())) { + push_cnstr(OR(NOT(EQ(y, zero)), EQ(k1, u().mk_idiv(x, zero)))); push_cnstr_pr(result_pr); - push_cnstr(OR(NOT(EQ(y, zero)), EQ(k2, u().mk_mod0(x)))); + push_cnstr(OR(NOT(EQ(y, zero)), EQ(k2, u().mk_mod(x, zero)))); push_cnstr_pr(mod_pr); } } @@ -414,7 +415,7 @@ struct purify_arith_proc { // (^ x 0) --> k | x != 0 implies k = 1, x = 0 implies k = 0^0 push_cnstr(OR(EQ(x, zero), EQ(k, one))); push_cnstr_pr(result_pr); - push_cnstr(OR(NOT(EQ(x, zero)), EQ(k, is_int ? u().mk_0_pw_0_int() : u().mk_0_pw_0_real()))); + push_cnstr(OR(NOT(EQ(x, zero)), EQ(k, u().mk_power(zero, zero)))); push_cnstr_pr(result_pr); } else if (!is_int) {