From 00dab30ea037e05c704eb6fed1664fadd5d6a701 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 18 Feb 2021 13:18:58 -0800
Subject: [PATCH] remove binary_function

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz/spacer/spacer_context.h             | 8 +++++---
 src/muz/spacer/spacer_quant_generalizer.cpp | 2 +-
 2 files changed, 6 insertions(+), 4 deletions(-)

diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h
index 85eadc96b..9b618a2c5 100644
--- a/src/muz/spacer/spacer_context.h
+++ b/src/muz/spacer/spacer_context.h
@@ -24,6 +24,8 @@ Notes:
 
 #include <queue>
 #include <fstream>
+#include <functional>
+#include <algorithm>
 
 #include "util/scoped_ptr_vector.h"
 #include "muz/spacer/spacer_manager.h"
@@ -186,7 +188,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 () &&
@@ -729,11 +731,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 e85b7648e..651871e5a 100644
--- a/src/muz/spacer/spacer_quant_generalizer.cpp
+++ b/src/muz/spacer/spacer_quant_generalizer.cpp
@@ -36,7 +36,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) {