mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

Add arith_decls for underspecified operators

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-12-26 11:35:00 -08:00
parent 2a286541e0
commit 53df82c314
3 changed files with 94 additions and 105 deletions
Download patch file Download diff file Expand all files Collapse all files

53
src/ast/arith_decl_plugin.cpp
View file

@ -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;
}

34
src/ast/arith_decl_plugin.h
View file

@ -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<app> m_small_ints;
ptr_vector<app> 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;

112
src/tactic/arith/purify_arith_tactic.cpp
View file

@ -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);