From cd2d197bb944fec24c6ebdb7a696c2e9b4161bf2 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Mon, 3 Oct 2022 10:55:13 +0200
Subject: [PATCH] Add compact version of std::all_of

---
 src/math/polysat/clause.cpp |  4 ++--
 src/math/polysat/solver.cpp |  4 ++--
 src/util/util.h             | 18 ++++++++++++++----
 3 files changed, 18 insertions(+), 8 deletions(-)

diff --git a/src/math/polysat/clause.cpp b/src/math/polysat/clause.cpp
index 9f0a31c5b..e0604f807 100644
--- a/src/math/polysat/clause.cpp
+++ b/src/math/polysat/clause.cpp
@@ -29,14 +29,14 @@ namespace polysat {
     }
 
     bool clause::is_always_false(solver& s) const {
-        return std::all_of(m_literals.begin(), m_literals.end(), [&s](sat::literal lit) {
+        return all_of(m_literals, [&s](sat::literal lit) {
             signed_constraint c = s.m_constraints.lookup(lit);
             return c.is_always_false();
         });
     }
 
     bool clause::is_currently_false(solver& s) const {
-        return std::all_of(m_literals.begin(), m_literals.end(), [&s](sat::literal lit) {
+        return all_of(m_literals, [&s](sat::literal lit) {
             signed_constraint c = s.m_constraints.lookup(lit);
             return c.is_currently_false(s);
         });
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 722a6f390..448b5d3c6 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -630,7 +630,7 @@ namespace polysat {
         SASSERT(j.is_decision() || j.is_propagation());
         SASSERT(j.level() == m_level);
         SASSERT(!is_assigned(v));
-        SASSERT(std::all_of(assignment().begin(), assignment().end(), [v](auto p) { return p.first != v; }));
+        SASSERT(all_of(assignment(), [v](auto p) { return p.first != v; }));
         m_value[v] = val;
         m_search.push_assignment(v, val);
         m_trail.push_back(trail_instr_t::assign_i);
@@ -1154,7 +1154,7 @@ namespace polysat {
         for (sat::bool_var v = m_bvars.size(); v-- > 0; ) {
             sat::literal lit(v);            
             auto c = lit2cnstr(lit);  
-            if (!std::all_of(c->vars().begin(), c->vars().end(), [&](auto v) { return is_assigned(v); }))
+            if (!all_of(c->vars(), [this](auto w) { return is_assigned(w); }))
                 continue;
             ok &= (m_bvars.value(lit) != l_true) || !c.is_currently_false(*this);
             ok &= (m_bvars.value(lit) != l_false) || !c.is_currently_true(*this);
diff --git a/src/util/util.h b/src/util/util.h
index f08558f37..273129307 100644
--- a/src/util/util.h
+++ b/src/util/util.h
@@ -20,11 +20,13 @@ Revision History:
 
 #include "util/debug.h"
 #include "util/memory_manager.h"
-#include<ostream>
-#include<climits>
-#include<limits>
-#include<stdint.h>
+#include <ostream>
+#include <climits>
+#include <limits>
+#include <stdint.h>
 #include <string>
+#include <algorithm>
+#include <iterator>
 
 #ifndef SIZE_MAX
 #define SIZE_MAX std::numeric_limits<std::size_t>::max()
@@ -374,3 +376,11 @@ inline size_t megabytes_to_bytes(unsigned mb) {
         r = SIZE_MAX;    
     return r;
 }
+
+/** Compact version of std::all_of */
+template <typename Container, typename Predicate>
+bool all_of(Container const& c, Predicate f)
+{
+    using std::begin, std::end;  // allows begin(c) to also find c.begin()
+    return std::all_of(begin(c), end(c), std::forward<Predicate>(f));
+}