fix #4811

Z3Prover · Nov 23, 2020 · 193ca57 · 193ca57
1 parent 65464f5
commit 193ca57
Show file tree

Hide file tree

Showing 4 changed files with 23 additions and 13 deletions.
diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp
@@ -483,7 +483,7 @@ expr * arith_rewriter::reduce_power(expr * arg, bool is_eq) {
                 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))));
+                new_args.push_back(mk_power(arg0, rational(2)));
             }
         }
         else {
@@ -1042,7 +1042,6 @@ br_status arith_rewriter::mk_idiv_core(expr * arg1, expr * arg2, expr_ref & resu
     } 
     return BR_FAILED;
 }
-
 
 //  
 // implement div ab ac = floor( ab / ac) = floor (b / c) = div b c 
@@ -1246,6 +1245,15 @@ br_status arith_rewriter::mk_rem_core(expr * arg1, expr * arg2, expr_ref & resul
     return BR_FAILED;
 }
 
+app* arith_rewriter_core::mk_power(expr* x, rational const& r) { 
+    SASSERT(r.is_unsigned() && r.is_pos());
+    bool is_int = m_util.is_int(x);
+    app* y = m_util.mk_power(x, m_util.mk_numeral(r, is_int));
+    if (is_int) 
+        y = m_util.mk_to_int(y);
+    return y;
+}
+
 br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & result) {
     numeral x, y;
     bool is_num_x    = m_util.is_numeral(arg1, x);
@@ -1446,6 +1454,9 @@ br_status arith_rewriter::mk_to_int_core(expr * arg, expr_ref & result) {
                 real_args.push_back(c);
             }
         }
+        if (real_args.empty() && m_util.is_power(arg))
+            return BR_FAILED;
+
         if (real_args.empty()) {
             result = m().mk_app(get_fid(), to_app(arg)->get_decl()->get_decl_kind(), int_args.size(), int_args.c_ptr());
             return BR_REWRITE1;

diff --git a/src/ast/rewriter/arith_rewriter.h b/src/ast/rewriter/arith_rewriter.h
@@ -44,6 +44,7 @@ class arith_rewriter_core {
     decl_kind mul_decl_kind() const { return OP_MUL; }
     bool use_power() const { return m_mul2power && !m_expand_power; }
     decl_kind power_decl_kind() const { return OP_POWER; }
+    app* mk_power(expr* x, rational const& r);
 public:
     arith_rewriter_core(ast_manager & m):m_util(m) {}
     bool is_zero(expr * n) const { return m_util.is_zero(n); }

diff --git a/src/ast/rewriter/bv_rewriter.h b/src/ast/rewriter/bv_rewriter.h
@@ -39,6 +39,7 @@ class bv_rewriter_core {
     decl_kind add_decl_kind() const { return OP_BADD; }
     decl_kind mul_decl_kind() const { return OP_BMUL; }
     bool use_power() const { return false; }
+    app* mk_power(expr* x, rational const& r) { UNREACHABLE(); return nullptr; }
     decl_kind power_decl_kind() const { UNREACHABLE(); return static_cast<decl_kind>(UINT_MAX); }
 
 public:

diff --git a/src/ast/rewriter/poly_rewriter_def.h b/src/ast/rewriter/poly_rewriter_def.h
@@ -89,28 +89,25 @@ expr * poly_rewriter<Config>::mk_mul_app(unsigned num_args, expr * const * args)
             expr * prev = get_power_body(args[0], k_prev);
             rational k;
             ptr_buffer<expr> new_args;
-#define PUSH_POWER() {                                                                          \
-                if (k_prev.is_one()) {                                                          \
-                    new_args.push_back(prev);                                                   \
-                }                                                                               \
-                else {                                                                          \
-                    expr * pargs[2] = { prev, mk_numeral(k_prev) };                             \
-                    new_args.push_back(m().mk_app(get_fid(), power_decl_kind(), 2, pargs));     \
-                }                                                                               \
-            }
+            auto push_power = [&]() { 
+                if (k_prev.is_one())                                                           
+                    new_args.push_back(prev);                                                   
+                else  
+                    new_args.push_back(mk_power(prev, k_prev));                                                                                            
+            };
 
             for (unsigned i = 1; i < num_args; i++) {
                 expr * arg = get_power_body(args[i], k);
                 if (arg == prev) {
                     k_prev += k;
                 }
                 else {
-                    PUSH_POWER();
+                    push_power();
                     prev   = arg;
                     k_prev = k;
                 }
             }
-            PUSH_POWER();
+            push_power();
             SASSERT(new_args.size() > 0);
             if (new_args.size() == 1) {
                 return new_args[0];