From 6704a4be0298a0b19c69663965d187cb1b6ccbda Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 15 Oct 2018 12:52:19 -0700
Subject: [PATCH] Revert "Made Z3 compile for C++17 with MSVC"

---
 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, 6 insertions(+), 10 deletions(-)

diff --git a/src/muz/base/dl_rule_set.cpp b/src/muz/base/dl_rule_set.cpp
index fdafefcdc1c..80af80266ef 100644
--- a/src/muz/base/dl_rule_set.cpp
+++ b/src/muz/base/dl_rule_set.cpp
@@ -696,10 +696,9 @@ 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::bind(std::not_equal_to<item_set*>(), (item_set*)0, _1)) == m_components.end());
+            std::bind1st(std::not_equal_to<item_set*>(), (item_set*)0)) == 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 614f46d29e0..0d8b2daf6ff 100644
--- a/src/muz/spacer/spacer_context.h
+++ b/src/muz/spacer/spacer_context.h
@@ -28,7 +28,6 @@ Module Name:
 #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"
@@ -190,7 +189,7 @@ class lemma {
     }
 };
 
-struct lemma_lt_proc : public std::function<bool(lemma*, lemma *)> {
+struct lemma_lt_proc : public std::binary_function<lemma*, lemma *, bool> {
     bool operator() (lemma *a, lemma *b) {
         return (a->level () < b->level ()) ||
             (a->level () == b->level () &&
@@ -728,11 +727,11 @@ inline std::ostream &operator<<(std::ostream &out, pob const &p) {
     return p.display(out);
 }
 
-struct pob_lt_proc : public std::function<bool(const pob*, const pob*)> {
+struct pob_lt_proc : public std::binary_function<const pob*, const pob*, bool> {
     bool operator() (const pob *pn1, const pob *pn2) const;
 };
 
-struct pob_gt_proc : public std::function<bool(const pob*, const pob*)> {
+struct pob_gt_proc : public std::binary_function<const pob*, const pob*, bool> {
     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 6443b9b7d9a..a11ab4d9e25 100644
--- a/src/muz/spacer/spacer_quant_generalizer.cpp
+++ b/src/muz/spacer/spacer_quant_generalizer.cpp
@@ -19,7 +19,6 @@ Revision History:
 
 --*/
 
-#include <functional>
 
 #include "muz/spacer/spacer_context.h"
 #include "muz/spacer/spacer_generalizers.h"
@@ -37,7 +36,7 @@ Revision History:
 using namespace spacer;
 
 namespace {
-struct index_lt_proc : public std::function<bool(app*, app*)> {
+struct index_lt_proc : public std::binary_function<app*, app *, bool> {
     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 04acacbd909..52609893fa0 100644
--- a/src/qe/qe_vartest.h
+++ b/src/qe/qe_vartest.h
@@ -21,10 +21,9 @@ Revision History:
 
 #include "ast/ast.h"
 #include "util/uint_set.h"
-#include <functional>
 
 // TBD: move under qe namespace
-class is_variable_proc : public std::function<bool(expr*)> {
+class is_variable_proc : public std::unary_function<expr*,bool> {
 public:
     virtual bool operator()(const expr* e) const = 0;
 };