mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

disable unsound simplification of root objects, and incorrect evaluation of negative even roots

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-12-09 08:41:59 -08:00
parent 8949790c16
commit 035f2bb0da
4 changed files with 31 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/ast/arith_decl_plugin.h
View file

@ -281,6 +281,7 @@ public:
MATCH_BINARY(is_rem);
MATCH_BINARY(is_div);
MATCH_BINARY(is_idiv);
MATCH_BINARY(is_power);
bool is_pi(expr * arg) { return is_app_of(arg, m_afid, OP_PI); }
bool is_e(expr * arg) { return is_app_of(arg, m_afid, OP_E); }

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

@ -264,9 +264,10 @@ bool arith_rewriter::is_reduce_power_target(expr * arg, bool is_eq) {
}
for (unsigned i = 0; i < sz; i++) {
expr * arg = args[i];
if (m_util.is_power(arg)) {
expr* arg0, *arg1;
if (m_util.is_power(arg, arg0, arg1)) {
rational k;
if (m_util.is_numeral(to_app(arg)->get_arg(1), k) && k.is_int() && ((is_eq && k > rational(1)) || (!is_eq && k > rational(2))))
if (m_util.is_numeral(arg1, k) && k.is_int() && ((is_eq && k > rational(1)) || (!is_eq && k > rational(2))))
return true;
}
}
@ -290,11 +291,15 @@ expr * arith_rewriter::reduce_power(expr * arg, bool is_eq) {
rational k;
for (unsigned i = 0; i < sz; i++) {
expr * arg = args[i];
if (m_util.is_power(arg) && m_util.is_numeral(to_app(arg)->get_arg(1), k) && k.is_int() && ((is_eq && k > rational(1)) || (!is_eq && k > rational(2)))) {
if (is_eq || !k.is_even())
new_args.push_back(to_app(arg)->get_arg(0));
else
new_args.push_back(m_util.mk_power(to_app(arg)->get_arg(0), m_util.mk_numeral(rational(2), m_util.is_int(arg))));
expr * arg0, *arg1;
if (m_util.is_power(arg, arg0, arg1) && m_util.is_numeral(arg1, k) && k.is_int() &&
((is_eq && k > rational(1)) || (!is_eq && k > rational(2)))) {
if (is_eq || !k.is_even()) {
new_args.push_back(arg0);
}
else {
new_args.push_back(m_util.mk_power(arg0, m_util.mk_numeral(rational(2), m_util.is_int(arg))));
}
}
else {
new_args.push_back(arg);
@ -788,6 +793,7 @@ br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & res
bool is_num_y = m_util.is_numeral(arg2, y);
bool is_int_sort = m_util.is_int(arg1);
TRACE("arith", tout << mk_pp(arg1, m()) << " " << mk_pp(arg2, m()) << "\n";);
if ((is_num_x && x.is_one()) ||
(is_num_y && y.is_one())) {
result = arg1;
@ -821,11 +827,12 @@ br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & res
}
}
if (m_util.is_power(arg1) && is_num_y && y.is_int() && !y.is_zero()) {
expr* arg10, *arg11;
if (m_util.is_power(arg1, arg10, arg11) && is_num_y && y.is_int() && !y.is_zero()) {
// (^ (^ t y2) y) --> (^ t (* y2 y)) If y2 > 0 && y != 0 && y and y2 are integers
rational y2;
if (m_util.is_numeral(to_app(arg1)->get_arg(1), y2) && y2.is_int() && y2.is_pos()) {
result = m_util.mk_power(to_app(arg1)->get_arg(0), m_util.mk_numeral(y*y2, is_int_sort));
if (m_util.is_numeral(arg11, y2) && y2.is_int() && y2.is_pos()) {
result = m_util.mk_power(arg10, m_util.mk_numeral(y*y2, is_int_sort));
return BR_REWRITE1;
}
}
@ -888,6 +895,9 @@ br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & res
if (is_num_x) {
rational xk, r;
xk = power(x, u_num_y);
if (xk.is_neg() && u_den_y % 2 == 0) {
return BR_FAILED;
}
if (xk.root(u_den_y, r)) {
if (is_neg_y)
r = rational(1)/r;

1
src/nlsat/tactic/nlsat_tactic.cpp
View file

@ -135,6 +135,7 @@ class nlsat_tactic : public tactic {
fail_if_proof_generation("nlsat", g);
TRACE("nlsat", g->display(tout););
expr2var a2b(m);
expr2var t2x(m);
m_g2nl(*g, m_params, m_solver, a2b, t2x);

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

@ -347,7 +347,7 @@ struct purify_arith_proc {
expr * x = args[0];
expr * zero = u().mk_numeral(rational(0), is_int);
expr * one = u().mk_numeral(rational(1), is_int);
if (y.is_zero()) {
if (y.is_zero() && complete()) {
// (^ 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);
@ -366,7 +366,7 @@ struct purify_arith_proc {
push_cnstr(EQ(x, u().mk_power(k, u().mk_numeral(n, false))));
push_cnstr_pr(result_pr);
}
else {
else if (complete()) {
SASSERT(n.is_even());
// (^ x (/ 1 n)) --> k | x >= 0 implies (x = k^n and k >= 0), x < 0 implies k = neg-root(x, n)
// when n is even
@ -374,11 +374,13 @@ struct purify_arith_proc {
AND(EQ(x, u().mk_power(k, u().mk_numeral(n, false))),
u().mk_ge(k, zero))));
push_cnstr_pr(result_pr);
if (complete()) {
push_cnstr(OR(u().mk_ge(x, zero),
EQ(k, u().mk_neg_root(x, u().mk_numeral(n, false)))));
push_cnstr_pr(result_pr);
}
push_cnstr(OR(u().mk_ge(x, zero),
EQ(k, u().mk_neg_root(x, u().mk_numeral(n, false)))));
push_cnstr_pr(result_pr);
}
else {
return BR_FAILED;
}
}
else {