From 035f2bb0dae81519e550a9c865c2aab93eac2dc2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 9 Dec 2015 08:41:59 -0800 Subject: [PATCH] disable unsound simplification of root objects, and incorrect evaluation of negative even roots Signed-off-by: Nikolaj Bjorner --- src/ast/arith_decl_plugin.h | 1 + src/ast/rewriter/arith_rewriter.cpp | 30 ++++++++++++++++-------- src/nlsat/tactic/nlsat_tactic.cpp | 1 + src/tactic/arith/purify_arith_tactic.cpp | 16 +++++++------ 4 files changed, 31 insertions(+), 17 deletions(-) diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h index cfb6f5469..e185b241b 100644 --- a/src/ast/arith_decl_plugin.h +++ b/src/ast/arith_decl_plugin.h @@ -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); } diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index be088d2b5..81a610c50 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -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; diff --git a/src/nlsat/tactic/nlsat_tactic.cpp b/src/nlsat/tactic/nlsat_tactic.cpp index 0f2c80c29..348e68da1 100644 --- a/src/nlsat/tactic/nlsat_tactic.cpp +++ b/src/nlsat/tactic/nlsat_tactic.cpp @@ -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); diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp index e18c6e90b..ac383c39a 100644 --- a/src/tactic/arith/purify_arith_tactic.cpp +++ b/src/tactic/arith/purify_arith_tactic.cpp @@ -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 {