8ac5e011d6
GitOrigin-RevId: 2c3273caa153ee8eb5786bc8141b85b859e7efd7
76 lines
2.8 KiB
Diff
76 lines
2.8 KiB
Diff
commit 4eb28b907e89be05d92eb704115f821b9b848e60
|
|
Author: Matthew Dawson <matthew@mjdsystems.ca>
|
|
Date: Sun Oct 16 22:06:03 2016 -0400
|
|
|
|
Fix gcc v6 compile failures.
|
|
|
|
* Use std::hash<const char*> over std::hash<char *>, as throwing away the const is not allowed.
|
|
* Use Hash::hash by default in CDMap over std::hash, to get Hash::hash<CVC3::expr>
|
|
|
|
diff --git a/src/expr/expr_value.cpp b/src/expr/expr_value.cpp
|
|
index 0c85ff6..e4dd251 100644
|
|
--- a/src/expr/expr_value.cpp
|
|
+++ b/src/expr/expr_value.cpp
|
|
@@ -29,7 +29,7 @@ namespace CVC3 {
|
|
// Class ExprValue static members
|
|
////////////////////////////////////////////////////////////////////////
|
|
|
|
-std::hash<char*> ExprValue::s_charHash;
|
|
+std::hash<const char*> ExprValue::s_charHash;
|
|
std::hash<long int> ExprValue::s_intHash;
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
diff --git a/src/include/cdmap.h b/src/include/cdmap.h
|
|
index faf682a..c3b094c 100644
|
|
--- a/src/include/cdmap.h
|
|
+++ b/src/include/cdmap.h
|
|
@@ -43,9 +43,9 @@ namespace CVC3 {
|
|
// Auxiliary class: almost the same as CDO (see cdo.h), but on
|
|
// setNull() call it erases itself from the map.
|
|
|
|
-template <class Key, class Data, class HashFcn = std::hash<Key> > class CDMap;
|
|
+template <class Key, class Data, class HashFcn = Hash::hash<Key> > class CDMap;
|
|
|
|
-template <class Key, class Data, class HashFcn = std::hash<Key> >
|
|
+template <class Key, class Data, class HashFcn = Hash::hash<Key> >
|
|
class CDOmap :public ContextObj {
|
|
Key d_key;
|
|
Data d_data;
|
|
diff --git a/src/include/expr_hash.h b/src/include/expr_hash.h
|
|
index b2107d7..baa2eab 100644
|
|
--- a/src/include/expr_hash.h
|
|
+++ b/src/include/expr_hash.h
|
|
@@ -20,7 +20,6 @@
|
|
* hash_set over Expr class.
|
|
*/
|
|
/*****************************************************************************/
|
|
-
|
|
#ifndef _cvc3__expr_h_
|
|
#include "expr.h"
|
|
#endif
|
|
diff --git a/src/include/expr_value.h b/src/include/expr_value.h
|
|
index 95102b2..f53aa4d 100644
|
|
--- a/src/include/expr_value.h
|
|
+++ b/src/include/expr_value.h
|
|
@@ -179,7 +179,7 @@ protected:
|
|
// Static hash functions. They don't depend on the context
|
|
// (ExprManager and such), so it is still thread-safe to have them
|
|
// static.
|
|
- static std::hash<char*> s_charHash;
|
|
+ static std::hash<const char*> s_charHash;
|
|
static std::hash<long int> s_intHash;
|
|
|
|
static size_t pointerHash(void* p) { return s_intHash((long int)p); }
|
|
diff --git a/src/theory_core/theory_core.cpp b/src/theory_core/theory_core.cpp
|
|
index df5289f..37ccab9 100644
|
|
--- a/src/theory_core/theory_core.cpp
|
|
+++ b/src/theory_core/theory_core.cpp
|
|
@@ -710,7 +710,7 @@ TheoryCore::TheoryCore(ContextManager* cm,
|
|
// d_termTheorems(cm->getCurrentContext()),
|
|
d_predicates(cm->getCurrentContext()),
|
|
d_solver(NULL),
|
|
- d_simplifyInPlace(false),
|
|
+ d_simplifyInPlace(NULL),
|
|
d_currentRecursiveSimplifier(NULL),
|
|
d_resourceLimit(0),
|
|
d_timeBase(0),
|