diff options
-rw-r--r-- | proofs/lfsc_checker/.gitignore | 1 | ||||
l--------- | proofs/lfsc_checker/config/ax_cxx_compile_stdcxx.m4 | 1 | ||||
l--------- | proofs/lfsc_checker/config/ax_cxx_compile_stdcxx_11.m4 | 1 | ||||
-rw-r--r-- | proofs/lfsc_checker/configure.ac | 4 | ||||
-rw-r--r-- | proofs/lfsc_checker/expr.h | 11 | ||||
-rw-r--r-- | src/theory/arith/approx_simplex.cpp | 6 |
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; |