mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

fix #2831 again

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-12-28 18:44:33 -08:00
parent 2f8303393b
commit ce4e71fbe9
3 changed files with 37 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/ast/arith_decl_plugin.cpp
View file

@ -811,13 +811,24 @@ bool arith_util::is_considered_uninterpreted(func_decl* f, unsigned n, expr* con
return true;
}
if (is_decl_of(f, m_afid, OP_POWER) && is_numeral(args[1], r) && r.is_zero() && is_numeral(args[0], r) && r.is_zero()) {
sort* rs[2] = { mk_real(), mk_real() };
f_out = m_manager.mk_func_decl(m_afid, OP_POWER0, 0, nullptr, 2, rs, mk_real());
f_out = is_int(args[0]) ? mk_ipower0() : mk_rpower0();
return true;
}
return plugin().is_considered_uninterpreted(f);
}
func_decl* arith_util::mk_ipower0() {
sort* s = mk_int();
sort* rs[2] = { s, s };
return m_manager.mk_func_decl(m_afid, OP_POWER0, 0, nullptr, 2, rs, s);
}
func_decl* arith_util::mk_rpower0() {
sort* s = mk_real();
sort* rs[2] = { s, s };
return m_manager.mk_func_decl(m_afid, OP_POWER0, 0, nullptr, 2, rs, s);
}
func_decl* arith_util::mk_div0() {
sort* rs[2] = { mk_real(), mk_real() };
return m_manager.mk_func_decl(m_afid, OP_DIV0, 0, nullptr, 2, rs, mk_real());

2
src/ast/arith_decl_plugin.h
View file

@ -369,6 +369,8 @@ public:
func_decl* mk_div0();
func_decl* mk_idiv0();
func_decl* mk_ipower0();
func_decl* mk_rpower0();
app * mk_numeral(rational const & val, bool is_int) const {

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

@ -194,6 +194,7 @@ struct purify_arith_proc {
expr_ref_vector m_new_cnstrs;
proof_ref_vector m_new_cnstr_prs;
svector<div_def> m_divs, m_idivs;
expr_ref m_ipower0, m_rpower0;
expr_ref m_subst;
proof_ref m_subst_pr;
expr_ref_vector m_new_vars;
@ -203,7 +204,9 @@ struct purify_arith_proc {
m_pinned(o.m()),
m_new_cnstrs(o.m()),
m_new_cnstr_prs(o.m()),
m_subst(o.m()),
m_ipower0(o.m()),
m_rpower0(o.m()),
m_subst(o.m()),
m_subst_pr(o.m()),
m_new_vars(o.m()) {
}
@ -407,11 +410,8 @@ struct purify_arith_proc {
if (already_processed(t, result, result_pr))
return BR_DONE;
bool is_int = u().is_int(args[0]);
expr * x = args[0];
rational xr;
if (u().is_numeral(x, xr) && xr.is_zero())
return BR_FAILED;
bool is_int = u().is_int(x);
expr * k = mk_fresh_var(is_int);
result = k;
@ -421,10 +421,20 @@ struct purify_arith_proc {
expr_ref zero(u().mk_numeral(rational(0), is_int), m());
expr_ref one(u().mk_numeral(rational(1), is_int), m());
if (y.is_zero()) {
expr* p0;
if (is_int) {
if (!m_ipower0) m_ipower0 = mk_fresh_var(true);
p0 = m_ipower0;
}
else {
if (!m_rpower0) m_rpower0 = mk_fresh_var(false);
p0 = m_rpower0;
}
// (^ 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, u().mk_power(zero, zero))));
push_cnstr(OR(NOT(EQ(x, zero)), EQ(k, p0)));
push_cnstr_pr(result_pr);
}
else if (!is_int) {
@ -824,6 +834,12 @@ struct purify_arith_proc {
}
fmc->add(u().mk_idiv0(), body);
}
if (r.cfg().m_ipower0) {
fmc->add(u().mk_ipower0(), r.cfg().m_ipower0);
}
if (r.cfg().m_rpower0) {
fmc->add(u().mk_rpower0(), r.cfg().m_rpower0);
}
}
if (produce_models && !m_sin_cos.empty()) {
generic_model_converter* emc = alloc(generic_model_converter, m(), "purify_sin_cos");