mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

purify

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-08-27 11:57:13 -07:00
parent b8a81bcb09
commit 3bfc3437f1
8 changed files with 44 additions and 101 deletions

36
src/ast/arith_decl_plugin.cpp
View file

@ -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,

46
src/ast/arith_decl_plugin.h
View file

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

7
src/ast/rewriter/arith_rewriter.cpp
View file

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

2
src/ast/simplifier/arith_simplifier_plugin.cpp
View file

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

12
src/qe/nlqsat.cpp
View file

@ -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<div> 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");
}

17
src/smt/theory_arith_core.h
View file

@ -395,7 +395,8 @@ namespace smt {
template<typename Ext>
theory_var theory_arith<Ext>::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<typename Ext>
theory_var theory_arith<Ext>::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<typename Ext>
theory_var theory_arith<Ext>::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<typename Ext>
theory_var theory_arith<Ext>::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))

10
src/smt/theory_lra.cpp
View file

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

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

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