* Models' SubstitutionMaps are now attached to the user context

  (rather than SAT context)
* Enable part of CVC3 system test (resolves bug 375)
* Fix infinite recursion in beta reduction code (resolves bug 417)
* Some model-building assertions have been added
* Other minor changes

(this commit was certified error- and warning-free by the test-and-commit script.)

1 files changed, 7 insertions, 0 deletions

diff --git a/src/util/hash.h b/src/util/hash.h
index 2420b7acd..1d360783a 100644
--- a/src/util/hash.h
+++ b/src/util/hash.h
@@ -54,6 +54,13 @@ struct StringHashFunction {
   }
 };/* struct StringHashFunction */
 
+template <class T, class U, class HashT = std::hash<T>, class HashU = std::hash<U> >
+struct PairHashFunction {
+  size_t operator()(const std::pair<T, U>& pr) const {
+    return HashT()(pr.first) ^ HashU()(pr.second);
+  }
+};/* struct PairHashFunction */
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__HASH_H */