2 files changed, 19 insertions, 10 deletions
diff --git a/src/util/integer.h b/src/util/integer.h
index 1ac8eab78..c86e836c7 100644
--- a/src/util/integer.h
+++ b/src/util/integer.h
@@ -12,13 +12,13 @@
  **
  ** A multiprecision integer constant.
  **/
-#include <gmpxx.h>
-#include <string>
-
 
 #ifndef __CVC4__INTEGER_H
 #define __CVC4__INTEGER_H
 
+#include <gmpxx.h>
+#include <string>
+
 namespace CVC4 {
 
 /** Hashes the gmp integer primitive in a word by word fashion. */
@@ -148,10 +148,14 @@ public:
   friend class CVC4::Rational;
 };/* class Integer */
 
-std::ostream& operator<<(std::ostream& os, const Integer& n);
+struct IntegerHashFcn {
+  static inline size_t hash(const CVC4::Integer& i) {
+    return i.hash();
+  }
+};
 
+std::ostream& operator<<(std::ostream& os, const Integer& n);
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4__RATIONAL_H */
-
+#endif /* __CVC4__INTEGER_H */
diff --git a/src/util/rational.h b/src/util/rational.h
index b22f44a2c..fdd125587 100644
--- a/src/util/rational.h
+++ b/src/util/rational.h
@@ -19,13 +19,13 @@
  ** different than the values used to construct the Rational.
  **/
 
+#ifndef __CVC4__RATIONAL_H
+#define __CVC4__RATIONAL_H
+
 #include <gmpxx.h>
 #include <string>
 #include "integer.h"
 
-#ifndef __CVC4__RATIONAL_H
-#define __CVC4__RATIONAL_H
-
 namespace CVC4 {
 
 class Rational {
@@ -181,9 +181,14 @@ public:
 
 };/* class Rational */
 
+struct RationalHashFcn {
+  static inline size_t hash(const CVC4::Rational& r) {
+    return r.hash();
+  }
+};
+
 std::ostream& operator<<(std::ostream& os, const Rational& n);
 
 }/* CVC4 namespace */
 
 #endif /* __CVC4__RATIONAL_H */
-