From 49d149045461c5078b4cd86ec65081959a9c1d48 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 4 Nov 2022 12:48:30 -0700
Subject: [PATCH] add ad-hoc any-of for cross compatibility and simplifying
 interface

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/simplifiers/model_reconstruction_trail.h |  8 +++++---
 src/util/util.h                                  | 15 ++++++++++++---
 2 files changed, 17 insertions(+), 6 deletions(-)

diff --git a/src/ast/simplifiers/model_reconstruction_trail.h b/src/ast/simplifiers/model_reconstruction_trail.h
index 8f1ba4381..96d27e4c4 100644
--- a/src/ast/simplifiers/model_reconstruction_trail.h
+++ b/src/ast/simplifiers/model_reconstruction_trail.h
@@ -44,7 +44,10 @@ class model_reconstruction_trail {
         bool is_loose() const { return !m_removed.empty(); }
 
         bool intersects(ast_mark const& free_vars) const {
-            return std::any_of(m_subst->sub().begin(), m_subst->sub().end(), [&](auto const& kv) { return free_vars.is_marked(kv.m_key); });
+            for (auto const& [k, v] : m_subst->sub())
+                if (free_vars.is_marked(k))
+                    return true;
+            return false;
         }
 
 
@@ -61,8 +64,7 @@ class model_reconstruction_trail {
 
     bool intersects(ast_mark const& free_vars, dependent_expr const& d) {
         expr_ref term(d.fml(), d.get_manager());
-        auto iter = subterms::all(term);
-        return std::any_of(iter.begin(), iter.end(), [&](expr* t) { return free_vars.is_marked(t); });
+        return any_of(subterms::all(term), [&](expr* t) { return free_vars.is_marked(t); });
     }
 
     bool intersects(ast_mark const& free_vars, vector<dependent_expr> const& added) {
diff --git a/src/util/util.h b/src/util/util.h
index 9d129f9a7..c3f06d8d3 100644
--- a/src/util/util.h
+++ b/src/util/util.h
@@ -25,6 +25,7 @@ Revision History:
 #include<limits>
 #include<stdint.h>
 #include <string>
+#include <functional>
 
 #ifndef SIZE_MAX
 #define SIZE_MAX std::numeric_limits<std::size_t>::max()
@@ -179,9 +180,8 @@ void display(std::ostream & out, const IT & begin, const IT & end, const char *
 template<typename T>
 struct delete_proc {
     void operator()(T * ptr) { 
-    if (ptr) {
-        dealloc(ptr);
-    }
+    if (ptr) 
+        dealloc(ptr);    
     }
 };
 
@@ -360,6 +360,15 @@ void fatal_error(int error_code);
 void set_fatal_error_handler(void (*pfn)(int error_code));
 
 
+template<typename S, typename T>
+bool any_of(S& set, T& p) {
+    for (auto const& s : set)
+        if (p(s))
+            return true;
+    return false;
+}
+// #define any_of(S, p) { for (auto const& s : S) if (p(s)) return true; return false; }
+
 /**
    \brief Iterator for the [0..sz[0]) X [0..sz[1]) X ... X [0..sz[n-1]).
    it contains the current value.