diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp index f2dccf065..752bad072 100644 --- a/src/ast/arith_decl_plugin.cpp +++ b/src/ast/arith_decl_plugin.cpp @@ -206,6 +206,21 @@ void arith_decl_plugin::set_manager(ast_manager * m, family_id id) { func_decl * e_decl = m->mk_const_decl(symbol("euler"), r, func_decl_info(id, OP_E)); 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); } arith_decl_plugin::arith_decl_plugin(): @@ -253,7 +268,15 @@ arith_decl_plugin::arith_decl_plugin(): m_acosh_decl(0), m_atanh_decl(0), m_pi(0), - m_e(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) { } arith_decl_plugin::~arith_decl_plugin() { @@ -303,6 +326,14 @@ 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()); m_manager->dec_array_ref(m_small_reals.size(), m_small_reals.c_ptr()); } @@ -347,6 +378,14 @@ 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_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_U_ASIN: return m_u_asin_decl; + case OP_U_ACOS: return m_u_acos_decl; default: return 0; } } @@ -426,12 +465,20 @@ static bool has_real_arg(ast_manager * m, unsigned num_args, expr * const * args return true; return false; } + +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; +} func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { if (k == OP_NUM) return mk_num_decl(num_parameters, parameters, arity); - if (arity == 0 && k != OP_PI && k != OP_E) { + if (arity == 0 && !is_const_op(k)) { m_manager->raise_exception("no arguments supplied to arithmetical operator"); return 0; } @@ -448,7 +495,7 @@ func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters unsigned num_args, expr * const * args, sort * range) { if (k == OP_NUM) return mk_num_decl(num_parameters, parameters, num_args); - if (num_args == 0 && k != OP_PI && k != OP_E) { + if (num_args == 0 && !is_const_op(k)) { m_manager->raise_exception("no arguments supplied to arithmetical operator"); return 0; } diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h index e63e866c3..53ab1881b 100644 --- a/src/ast/arith_decl_plugin.h +++ b/src/ast/arith_decl_plugin.h @@ -35,6 +35,7 @@ enum arith_sort_kind { enum arith_op_kind { OP_NUM, // rational & integers OP_IRRATIONAL_ALGEBRAIC_NUM, // irrationals that are roots of polynomials with integer coefficients + // OP_LE, OP_GE, OP_LT, @@ -67,6 +68,15 @@ enum arith_op_kind { // constants 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 }; @@ -126,7 +136,16 @@ 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; ptr_vector m_small_reals; @@ -182,6 +201,10 @@ 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 void set_cancel(bool f); @@ -339,6 +362,15 @@ 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); } + /** \brief Return the equality (= lhs rhs), but it makes sure that if one of the arguments is a numeral, then it will be in the right-hand-side; diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp index d2292ede9..169e27927 100644 --- a/src/tactic/arith/purify_arith_tactic.cpp +++ b/src/tactic/arith/purify_arith_tactic.cpp @@ -99,93 +99,15 @@ Rules (mod t1 t2) --> k2 | same constraints as above */ -struct purify_arith_decls { - ast_manager & m; - func_decl * m_int_0_pw_0_decl; // decl for: int 0^0 - func_decl * m_real_0_pw_0_decl; // decl for: rel 0^0 - func_decl * m_neg_root_decl; // decl for: even root of negative (real) number - func_decl * m_div_0_decl; // decl for: x/0 - func_decl * m_idiv_0_decl; // decl for: div(x, 0) - func_decl * m_mod_0_decl; // decl for: mod(x, 0) - func_decl * m_asin_u_decl; // decl for: asin(x) when x < -1 or x > 1 - func_decl * m_acos_u_decl; // decl for: acos(x) when x < -1 or x > 1 - - void inc_refs() { - m.inc_ref(m_int_0_pw_0_decl); - m.inc_ref(m_real_0_pw_0_decl); - m.inc_ref(m_neg_root_decl); - m.inc_ref(m_div_0_decl); - m.inc_ref(m_idiv_0_decl); - m.inc_ref(m_mod_0_decl); - m.inc_ref(m_asin_u_decl); - m.inc_ref(m_acos_u_decl); - } - - void dec_refs() { - m.dec_ref(m_int_0_pw_0_decl); - m.dec_ref(m_real_0_pw_0_decl); - m.dec_ref(m_neg_root_decl); - m.dec_ref(m_div_0_decl); - m.dec_ref(m_idiv_0_decl); - m.dec_ref(m_mod_0_decl); - m.dec_ref(m_asin_u_decl); - m.dec_ref(m_acos_u_decl); - } - - purify_arith_decls(arith_util & u): - m(u.get_manager()) { - sort * i = u.mk_int(); - sort * r = u.mk_real(); - m_int_0_pw_0_decl = m.mk_const_decl(symbol("0^0-int"), i); - m_real_0_pw_0_decl = m.mk_const_decl(symbol("0^0-real"), r); - sort * rr[2] = { r, r }; - m_neg_root_decl = m.mk_func_decl(symbol("neg-root"), 2, rr, r); - m_div_0_decl = m.mk_func_decl(symbol("/0"), 1, &r, r); - m_idiv_0_decl = m.mk_func_decl(symbol("div0"), 1, &i, i); - m_mod_0_decl = m.mk_func_decl(symbol("mod0"), 1, &i, i); - m_asin_u_decl = m.mk_func_decl(symbol("asin-u"), 1, &r, r); - m_acos_u_decl = m.mk_func_decl(symbol("acos-u"), 1, &r, r); - inc_refs(); - } - - purify_arith_decls(ast_manager & _m, - func_decl * int_0_pw_0, - func_decl * real_0_pw_0, - func_decl * neg_root, - func_decl * div_0, - func_decl * idiv_0, - func_decl * mod_0, - func_decl * asin_u, - func_decl * acos_u - ): - m(_m), - m_int_0_pw_0_decl(int_0_pw_0), - m_real_0_pw_0_decl(real_0_pw_0), - m_neg_root_decl(neg_root), - m_div_0_decl(div_0), - m_idiv_0_decl(idiv_0), - m_mod_0_decl(mod_0), - m_asin_u_decl(asin_u), - m_acos_u_decl(acos_u) { - inc_refs(); - } - - ~purify_arith_decls() { - dec_refs(); - } -}; - struct purify_arith_proc { arith_util & m_util; - purify_arith_decls & m_aux_decls; bool m_produce_proofs; bool m_elim_root_objs; bool m_elim_inverses; bool m_complete; - purify_arith_proc(arith_util & u, purify_arith_decls & d, bool produce_proofs, bool elim_root_objs, bool elim_inverses, bool complete): + purify_arith_proc(arith_util & u, bool produce_proofs, bool elim_root_objs, bool elim_inverses, bool complete): m_util(u), - m_aux_decls(d), m_produce_proofs(produce_proofs), m_elim_root_objs(elim_root_objs), m_elim_inverses(elim_inverses), @@ -247,15 +169,6 @@ struct purify_arith_proc { expr * mk_fresh_int_var() { return mk_fresh_var(true); } - func_decl * div0_decl() { return m_owner.m_aux_decls.m_div_0_decl; } - func_decl * idiv0_decl() { return m_owner.m_aux_decls.m_idiv_0_decl; } - func_decl * mod0_decl() { return m_owner.m_aux_decls.m_mod_0_decl; } - func_decl * int_0_pw_0_decl() { return m_owner.m_aux_decls.m_int_0_pw_0_decl; } - func_decl * real_0_pw_0_decl() { return m_owner.m_aux_decls.m_real_0_pw_0_decl; } - func_decl * neg_root_decl() { return m_owner.m_aux_decls.m_neg_root_decl; } - func_decl * asin_u_decl() { return m_owner.m_aux_decls.m_asin_u_decl; } - func_decl * acos_u_decl() { return m_owner.m_aux_decls.m_acos_u_decl; } - expr * mk_int_zero() { return u().mk_numeral(rational(0), true); } expr * mk_real_zero() { return u().mk_numeral(rational(0), false); } @@ -332,7 +245,7 @@ struct purify_arith_proc { if (complete()) { // y != 0 \/ k = div-0(x) push_cnstr(OR(NOT(EQ(y, mk_real_zero())), - EQ(k, m().mk_app(div0_decl(), x)))); + EQ(k, u().mk_div0(x)))); push_cnstr_pr(result_pr); } } @@ -380,10 +293,10 @@ struct purify_arith_proc { push_cnstr_pr(mod_pr); if (complete()) { - push_cnstr(OR(NOT(EQ(y, zero)), EQ(k1, m().mk_app(idiv0_decl(), x)))); + push_cnstr(OR(NOT(EQ(y, zero)), EQ(k1, u().mk_idiv0(x)))); push_cnstr_pr(result_pr); - push_cnstr(OR(NOT(EQ(y, zero)), EQ(k2, m().mk_app(mod0_decl(), x)))); + push_cnstr(OR(NOT(EQ(y, zero)), EQ(k2, u().mk_mod0(x)))); push_cnstr_pr(mod_pr); } } @@ -445,8 +358,7 @@ struct purify_arith_proc { push_cnstr(OR(EQ(x, zero), EQ(k, one))); push_cnstr_pr(result_pr); if (complete()) { - func_decl * z_pw_z = is_int ? int_0_pw_0_decl() : real_0_pw_0_decl(); - push_cnstr(OR(NOT(EQ(x, zero)), EQ(k, m().mk_const(z_pw_z)))); + 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_pr(result_pr); } } @@ -470,7 +382,7 @@ struct purify_arith_proc { push_cnstr_pr(result_pr); if (complete()) { push_cnstr(OR(u().mk_ge(x, zero), - EQ(k, m().mk_app(neg_root_decl(), x, u().mk_numeral(n, false))))); + EQ(k, u().mk_neg_root(x, u().mk_numeral(n, false))))); push_cnstr_pr(result_pr); } } @@ -561,10 +473,10 @@ struct purify_arith_proc { // x < -1 implies k = asin_u(x) // x > 1 implies k = asin_u(x) push_cnstr(OR(u().mk_ge(x, mone), - EQ(k, m().mk_app(asin_u_decl(), x)))); + EQ(k, u().mk_u_asin(x)))); push_cnstr_pr(result_pr); push_cnstr(OR(u().mk_le(x, one), - EQ(k, m().mk_app(asin_u_decl(), x)))); + EQ(k, u().mk_u_asin(x)))); push_cnstr_pr(result_pr); } return BR_DONE; @@ -603,10 +515,10 @@ struct purify_arith_proc { // x < -1 implies k = acos_u(x) // x > 1 implies k = acos_u(x) push_cnstr(OR(u().mk_ge(x, mone), - EQ(k, m().mk_app(acos_u_decl(), x)))); + EQ(k, u().mk_u_acos(x)))); push_cnstr_pr(result_pr); push_cnstr(OR(u().mk_le(x, one), - EQ(k, m().mk_app(acos_u_decl(), x)))); + EQ(k, u().mk_u_acos(x)))); push_cnstr_pr(result_pr); } return BR_DONE; @@ -835,12 +747,10 @@ struct purify_arith_proc { class purify_arith_tactic : public tactic { arith_util m_util; - purify_arith_decls m_aux_decls; params_ref m_params; public: purify_arith_tactic(ast_manager & m, params_ref const & p): m_util(m), - m_aux_decls(m_util), m_params(p) { } @@ -879,7 +789,7 @@ public: bool elim_root_objs = m_params.get_bool("elim_root_objects", true); bool elim_inverses = m_params.get_bool("elim_inverses", true); bool complete = m_params.get_bool("complete", true); - purify_arith_proc proc(m_util, m_aux_decls, produce_proofs, elim_root_objs, elim_inverses, complete); + purify_arith_proc proc(m_util, produce_proofs, elim_root_objs, elim_inverses, complete); proc(*(g.get()), mc, produce_models);