Change remaining hash_set -> unordered_set (#208)

The nightly competition build has been failing due to a remaining use of
hash_set in approx_simplex.cpp. This commit changes the remaining uses
of hash_set to unordered_set.
The remaining uses of hash_set were in LFSC. Switching to C++11 for LFSC
required changing the configure.ac for LFSC to require C++11 support to
make sure that it can be compiled independently from the rest of CVC4 (some
of our Travis tests do that as well). To have the macros for these additional
checks available, the commit adds a symlink to the files in config that contain
the macros). I did not find a way to add macros from a parent's folder that
did not break `make distcheck

diff --git a/proofs/lfsc_checker/.gitignore b/proofs/lfsc_checker/.gitignore
index 1f799d15ae76cdb90136a1a77367e48c2780bf49..0712efe67b5baf31fbcee637ee8e7f18b2d371ee 100644 (file)
--- a/proofs/lfsc_checker/.gitignore
+++ b/proofs/lfsc_checker/.gitignore
@@ -12,5 +12,4 @@ Makefile.in
 /aclocal.m4
 *~
 \#*\#
-/config/
 *.swp

diff --git a/proofs/lfsc_checker/config/ax_cxx_compile_stdcxx.m4 b/proofs/lfsc_checker/config/ax_cxx_compile_stdcxx.m4
new file mode 120000 (symlink)
index 0000000..0543a15
--- /dev/null
+++ b/proofs/lfsc_checker/config/ax_cxx_compile_stdcxx.m4
@@ -0,0 +1 @@
+../../../config/ax_cxx_compile_stdcxx.m4
\ No newline at end of file

diff --git a/proofs/lfsc_checker/config/ax_cxx_compile_stdcxx_11.m4 b/proofs/lfsc_checker/config/ax_cxx_compile_stdcxx_11.m4
new file mode 120000 (symlink)
index 0000000..77adcd7
--- /dev/null
+++ b/proofs/lfsc_checker/config/ax_cxx_compile_stdcxx_11.m4
@@ -0,0 +1 @@
+../../../config/ax_cxx_compile_stdcxx_11.m4
\ No newline at end of file

diff --git a/proofs/lfsc_checker/configure.ac b/proofs/lfsc_checker/configure.ac
index 5f4353664d7ec9f3aa05cc8e5d0c0d83be9b0f4e..9ef9022379d5285adb4dbef260dab2c68264ff65 100644 (file)
--- a/proofs/lfsc_checker/configure.ac
+++ b/proofs/lfsc_checker/configure.ac
@@ -27,6 +27,10 @@ AC_DISABLE_STATIC
 AC_PROG_CXX
 AC_PROG_CC
 
+# C++11 support in the compiler is now mandatory. Check for support and add
+# switches if necessary.
+AX_CXX_COMPILE_STDCXX_11([ext], [mandatory])
+
 # Checks for libraries.
 # FIXME: Replace `main' with a function in `-lgmp':
 AC_CHECK_LIB([gmp], [__gmpz_init])

diff --git a/proofs/lfsc_checker/expr.h b/proofs/lfsc_checker/expr.h
index 632aaa18afc859601a190b3eee90f0382529ceba..0677533da8689eb52c0450efb460c606c45118e0 100644 (file)
--- a/proofs/lfsc_checker/expr.h
+++ b/proofs/lfsc_checker/expr.h
@@ -2,11 +2,12 @@
 #define sc2__expr_h
 
 #include <stdint.h>
-#include <ext/hash_set>
 #include <iostream>
 #include <map>
 #include <string>
+#include <unordered_set>
 #include <vector>
+
 #include "chunking_memory_management.h"
 #include "gmp.h"
 
@@ -57,21 +58,17 @@ enum { NOT_CEXPR = 0, // for INT_EXPR, HOLE_EXPR, SYM_EXPR, SYMS_EXPR
 class Expr;
 class SymExpr;
 
-namespace __gnu_cxx {
-template <>
-struct hash<Expr *> {
+struct hashExprPtr {
   size_t operator()(const Expr *x) const {
     return reinterpret_cast<uintptr_t>(x);
   }
 };
-}
 
 struct eqExprPtr {
   bool operator()(const Expr *e1, const Expr *e2) const { return e1 == e2; }
 };
 
-typedef __gnu_cxx::hash_set<Expr *, __gnu_cxx::hash<Expr *>, eqExprPtr>
-    expr_ptr_set_t;
+typedef std::unordered_set<Expr *, hashExprPtr, eqExprPtr> expr_ptr_set_t;
 
 class Expr {
 protected:

diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp
index a500ec55db8c8035b3b5596b1f4a09088fde9a0b..78b57d3f663717872f3d5707ed6860c5785cd602 100644 (file)
--- a/src/theory/arith/approx_simplex.cpp
+++ b/src/theory/arith/approx_simplex.cpp
@@ -16,10 +16,10 @@
  **/
 #include "theory/arith/approx_simplex.h"
 
+#include <math.h>
 #include <cfloat>
 #include <cmath>
-#include <map>
-#include <math.h>
+#include <unordered_set>
 
 #include "base/output.h"
 #include "cvc4autoconfig.h"
@@ -2043,7 +2043,7 @@ bool ApproxGLPK::checkCutOnPad(int nid, const CutInfo& cut) const{
 
   const DenseMap<Rational>& constructedLhs = d_pad.d_cut.lhs;
   const Rational& constructedRhs = d_pad.d_cut.rhs;
-  hash_set<ArithVar> visited;
+  std::unordered_set<ArithVar> visited;
 
   if(constructedLhs.empty()){
     Debug("approx::checkCutOnPad") << "its empty?" <<endl;