fix combinator signatures

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/cmd_context/pdecl.h

@@ -36,7 +36,7 @@ protected:
     void inc_ref() { m_ref_count++; }
     void dec_ref() { SASSERT(m_ref_count > 0); --m_ref_count; }
     virtual bool is_psort() const { return false; }
-    virtual size_t obj_size() const = 0;
+    virtual size_t obj_size() const { UNREACHABLE(); return sizeof(*this); }
     pdecl(unsigned id, unsigned num_params):m_id(id), m_num_params(num_params), m_ref_count(0) {}
     virtual void finalize(pdecl_manager & m) {}
     virtual ~pdecl() {}
@@ -74,9 +74,9 @@ public:
     virtual bool is_sort_wrapper() const { return false; }
     virtual sort * instantiate(pdecl_manager & m, sort * const * s) { return nullptr; }
     // we use hash-consing for psorts.
-    virtual char const * hcons_kind() const = 0;
+    virtual char const * hcons_kind() const { UNREACHABLE(); return nullptr; }
-    virtual unsigned hcons_hash() const = 0;
+    virtual unsigned hcons_hash() const { UNREACHABLE(); return 0; }
-    virtual bool hcons_eq(psort const * other) const = 0;
+    virtual bool hcons_eq(psort const * other) const { UNREACHABLE(); return false; }
     void reset_cache(pdecl_manager& m) override;
 };
 

src/util/ref_vector.h

@@ -306,28 +306,52 @@ public:
     // prevent abuse:
     ref_vector & operator=(ref_vector const & other) = delete;
 
-    ref_vector&& filter(std::function<bool(T)>& predicate) {
+    bool containsp(std::function<bool(T)>& predicate) const {
+        for (auto const& t : *this)
+            if (predicate(t)) 
+                return true;
+        return false;
+    }
+
+    ref_vector filter_pure(std::function<bool(T)>& predicate) const {
         ref_vector result(m());
         for (auto& t : *this)
-            if (predicate(t)) result.push_back(t);
+            if (predicate(t)) 
+                result.push_back(t);
         return result;
     }
 
+    ref_vector& filter_update(std::function<bool(T)>& predicate) {
+        unsigned j = 0;
+        for (auto& t : *this)
+            if (predicate(t)) 
+                set(j++, t);
+        shrink(j);
+        return *this;
+    }
+
     template <typename S>
-    vector<S>&& map(std::function<S(T)>& f) {
+    vector<S> mapv_pure(std::function<S(T)>& f) const {
         vector<S> result;
         for (auto& t : *this)
             result.push_back(f(t));
         return result;
     }
 
-    ref_vector&& map(std::function<T(T)>& f) {
+    ref_vector map_pure(std::function<T(T)>& f) const {
         ref_vector result(m());
         for (auto& t : *this)
             result.push_back(f(t));
         return result;
     }
 
+    ref_vector& map_update(std::function<T(T)>& f)  {
+        unsigned j = 0;
+        for (auto& t : *this)
+            set(j++, f(t));
+        return *this;
+    }
+
 
 
 };

src/util/vector.h

@@ -231,21 +231,51 @@ public:
         return *this;
     }
 
-    vector&& filter(std::function<bool(T)>& predicate) {
+    bool containsp(std::function<bool(T)>& predicate) const {
+        for (auto const& t : *this)
+            if (predicate(t)) 
+                return true;
+        return false;
+    }
+
+    /**
+     * retain elements that satisfy predicate. aka 'where'.
+     */
+    vector filter_pure(std::function<bool(T)>& predicate) const {
         vector result;
         for (auto& t : *this)
-            if (predicate(t)) result.push_back(t);
+            if (predicate(t)) 
+                result.push_back(t);
         return result;
     }
 
+    vector& filter_update(std::function<bool(T)>& predicate) {
+        unsigned j = 0;
+        for (auto& t : *this)
+            if (predicate(t)) 
+                set(j++, t);
+        shrink(j);
+        return *this;
+    }
+
+    /**
+     * update elements using f, aka 'select'
+     */
     template <typename S>
-    vector<S>&& map(std::function<S(T)>& f) {
+    vector<S> map_pure(std::function<S(T)>& f) const {
         vector<S> result;
         for (auto& t : *this)
             result.push_back(f(t));
         return result;
     }
 
+    vector& map_update(std::function<T(T)>& f) {
+        unsigned j = 0;
+        for (auto& t : *this)
+            set(j++, f(t));
+        return *this;
+    }
+
     void reset() { 
         if (m_data) {
             if (CallDestructors) {