From 529e62e01ee90eb7e48f0eb65ea8efb62165e823 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 19 Nov 2018 00:48:33 -0800
Subject: [PATCH] remove unsound rewrite

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/arith_rewriter.cpp |  2 +-
 src/util/ref_vector.h               | 26 ++++++++++++++++++++++++++
 src/util/vector.h                   | 16 ++++++++++++++++
 3 files changed, 43 insertions(+), 1 deletion(-)

diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp
index 72ce9c761..a19074c51 100644
--- a/src/ast/rewriter/arith_rewriter.cpp
+++ b/src/ast/rewriter/arith_rewriter.cpp
@@ -1209,7 +1209,7 @@ br_status arith_rewriter::mk_to_int_core(expr * arg, expr_ref & result) {
             result = m().mk_app(get_fid(), to_app(arg)->get_decl()->get_decl_kind(), int_args.size(), int_args.c_ptr());
             return BR_REWRITE1;
         }
-        if (!int_args.empty() && (m_util.is_add(arg) || m_util.is_mul(arg))) {
+        if (!int_args.empty() && m_util.is_add(arg)) {
             decl_kind k = to_app(arg)->get_decl()->get_decl_kind();
             expr_ref t1(m().mk_app(get_fid(), k, int_args.size(), int_args.c_ptr()), m());
             expr_ref t2(m().mk_app(get_fid(), k, real_args.size(), real_args.c_ptr()), m());
diff --git a/src/util/ref_vector.h b/src/util/ref_vector.h
index 1e6525a06..491f1515f 100644
--- a/src/util/ref_vector.h
+++ b/src/util/ref_vector.h
@@ -186,6 +186,7 @@ public:
             std::swap(m_nodes[i], m_nodes[sz-i-1]);
         }
     }
+
 };
 
 template<typename T, typename TManager>
@@ -304,6 +305,31 @@ public:
     
     // prevent abuse:
     ref_vector & operator=(ref_vector const & other) = delete;
+
+    ref_vector&& filter(std::function<bool(T)>& predicate) {
+        ref_vector result(m());
+        for (auto& t : *this)
+            if (predicate(t)) result.push_back(t);
+        return result;
+    }
+
+    template <typename S>
+    vector<S>&& map(std::function<S(T)>& f) {
+        vector<S> result;
+        for (auto& t : *this)
+            result.push_back(f(t));
+        return result;
+    }
+
+    ref_vector&& map(std::function<T(T)>& f) {
+        ref_vector result(m());
+        for (auto& t : *this)
+            result.push_back(f(t));
+        return result;
+    }
+
+
+
 };
 
 template<typename T>
diff --git a/src/util/vector.h b/src/util/vector.h
index edcee7449..7724841c1 100644
--- a/src/util/vector.h
+++ b/src/util/vector.h
@@ -28,6 +28,7 @@ Revision History:
 #include<algorithm>
 #include<type_traits>
 #include<memory.h>
+#include<functional>
 #include "util/memory_manager.h"
 #include "util/hash.h"
 #include "util/z3_exception.h"
@@ -230,6 +231,21 @@ public:
         return *this;
     }
 
+    vector&& filter(std::function<bool(T)>& predicate) {
+        vector result;
+        for (auto& t : *this)
+            if (predicate(t)) result.push_back(t);
+        return result;
+    }
+
+    template <typename S>
+    vector<S>&& map(std::function<S(T)>& f) {
+        vector<S> result;
+        for (auto& t : *this)
+            result.push_back(f(t));
+        return result;
+    }
+
     void reset() { 
         if (m_data) {
             if (CallDestructors) {