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

6 files changed, 13 insertions, 11 deletions

diff --git a/proofs/lfsc_checker/.gitignore b/proofs/lfsc_checker/.gitignore
index 1f799d15a..0712efe67 100644
--- 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
index 000000000..0543a154f
--- /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
index 000000000..77adcd7a9
--- /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 5f4353664..9ef902237 100644
--- 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 632aaa18a..0677533da 100644
--- 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 a500ec55d..78b57d3f6 100644
--- 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;