Merge pull request #1880 from mjp41/c++17

Made Z3 compile for C++17 with MSVC

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());

src/muz/spacer/spacer_context.h

@@ -28,6 +28,7 @@ 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"
@@ -189,7 +190,7 @@ class lemma {
     }
 };
 
-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);
     }

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) {

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;
 };