From 01005a46f69e3d4e0c6012b676a1fe87352e6cb2 Mon Sep 17 00:00:00 2001
From: Matthew Parkinson <mattpark@microsoft.com>
Date: Mon, 15 Oct 2018 16:59:31 +0100
Subject: [PATCH] Made it more legal C++17

---
 src/muz/base/dl_rule_set.cpp                | 3 ++-
 src/muz/spacer/spacer_context.h             | 7 ++++---
 src/muz/spacer/spacer_quant_generalizer.cpp | 3 ++-
 src/qe/qe_vartest.h                         | 3 ++-
 4 files changed, 10 insertions(+), 6 deletions(-)

diff --git a/src/muz/base/dl_rule_set.cpp b/src/muz/base/dl_rule_set.cpp
index 80af80266..fdafefcdc 100644
--- a/src/muz/base/dl_rule_set.cpp
+++ b/src/muz/base/dl_rule_set.cpp
@@ -696,9 +696,10 @@ namespace datalog {
             }
             strats_index++;
         }
+        using namespace std::placeholders;
         //we have managed to topologicaly order all the components
         SASSERT(std::find_if(m_components.begin(), m_components.end(),
-            std::bind1st(std::not_equal_to<item_set*>(), (item_set*)0)) == m_components.end());
+            std::bind(std::not_equal_to<item_set*>(), (item_set*)0, _1)) == m_components.end());
 
         //reverse the strats array, so that the only the later components would depend on earlier ones
         std::reverse(m_strats.begin(), m_strats.end());
diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h
index 0d8b2daf6..614f46d29 100644
--- a/src/muz/spacer/spacer_context.h
+++ b/src/muz/spacer/spacer_context.h
@@ -28,6 +28,7 @@ Notes:
 #undef max
 #endif
 #include <queue>
+#include <functional>
 #include "util/scoped_ptr_vector.h"
 #include "muz/spacer/spacer_manager.h"
 #include "muz/spacer/spacer_prop_solver.h"
@@ -189,7 +190,7 @@ public:
     }
 };
 
-struct lemma_lt_proc : public std::binary_function<lemma*, lemma *, bool> {
+struct lemma_lt_proc : public std::function<bool(lemma*, lemma *)> {
     bool operator() (lemma *a, lemma *b) {
         return (a->level () < b->level ()) ||
             (a->level () == b->level () &&
@@ -727,11 +728,11 @@ inline std::ostream &operator<<(std::ostream &out, pob const &p) {
     return p.display(out);
 }
 
-struct pob_lt_proc : public std::binary_function<const pob*, const pob*, bool> {
+struct pob_lt_proc : public std::function<bool(const pob*, const pob*)> {
     bool operator() (const pob *pn1, const pob *pn2) const;
 };
 
-struct pob_gt_proc : public std::binary_function<const pob*, const pob*, bool> {
+struct pob_gt_proc : public std::function<bool(const pob*, const pob*)> {
     bool operator() (const pob *n1, const pob *n2) const {
         return pob_lt_proc()(n2, n1);
     }
diff --git a/src/muz/spacer/spacer_quant_generalizer.cpp b/src/muz/spacer/spacer_quant_generalizer.cpp
index a11ab4d9e..6443b9b7d 100644
--- a/src/muz/spacer/spacer_quant_generalizer.cpp
+++ b/src/muz/spacer/spacer_quant_generalizer.cpp
@@ -19,6 +19,7 @@ Revision History:
 
 --*/
 
+#include <functional>
 
 #include "muz/spacer/spacer_context.h"
 #include "muz/spacer/spacer_generalizers.h"
@@ -36,7 +37,7 @@ Revision History:
 using namespace spacer;
 
 namespace {
-struct index_lt_proc : public std::binary_function<app*, app *, bool> {
+struct index_lt_proc : public std::function<bool(app*, app*)> {
     arith_util m_arith;
     index_lt_proc(ast_manager &m) : m_arith(m) {}
     bool operator() (app *a, app *b) {
diff --git a/src/qe/qe_vartest.h b/src/qe/qe_vartest.h
index 52609893f..04acacbd9 100644
--- a/src/qe/qe_vartest.h
+++ b/src/qe/qe_vartest.h
@@ -21,9 +21,10 @@ Revision History:
 
 #include "ast/ast.h"
 #include "util/uint_set.h"
+#include <functional>
 
 // TBD: move under qe namespace
-class is_variable_proc : public std::unary_function<expr*,bool> {
+class is_variable_proc : public std::function<bool(expr*)> {
 public:
     virtual bool operator()(const expr* e) const = 0;
 };