6 files changed, 58 insertions, 8 deletions
diff --git a/src/util/integer.h.in b/src/util/integer.h.in
index 1fdaf0215..1f0174083 100644
--- a/src/util/integer.h.in
+++ b/src/util/integer.h.in
@@ -5,18 +5,23 @@
  ** Major contributors: none
  ** Minor contributors (to current version): dejan, cconway, mdeters
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief A multiprecision integer constant
+ ** \brief A multi-precision integer constant
  **
- ** A multiprecision integer constant.
+ ** A multi-precision integer constant.
  **/
 
-// this is used to avoid a public header dependence on cvc4autoconfig.h
+// these gestures are used to avoid a public header dependence on cvc4autoconfig.h
+
+#if @CVC4_NEED_INT64_T_OVERLOADS@
+#  define CVC4_NEED_INT64_T_OVERLOADS
+#endif
+
 #if /* use CLN */ @CVC4_USE_CLN_IMP@
 #  define CVC4_CLN_IMP
 #endif /* @CVC4_USE_CLN_IMP@ */
diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h
index 8f7daf4f5..7fd6a2694 100644
--- a/src/util/integer_cln_imp.h
+++ b/src/util/integer_cln_imp.h
@@ -120,8 +120,12 @@ public:
   Integer(  signed long int z) : d_value(z) {}
   Integer(unsigned long int z) : d_value(z) {}
 
-  ~Integer() {}
+#ifdef CVC4_NEED_INT64_T_OVERLOADS
+  Integer( int64_t z) : d_value(static_cast<long>(z)) {}
+  Integer(uint64_t z) : d_value(static_cast<unsigned long>(z)) {}
+#endif /* CVC4_NEED_INT64_T_OVERLOADS */
 
+  ~Integer() {}
 
   Integer& operator=(const Integer& x){
     if(this == &x) return *this;
diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h
index c553baff9..5b6468a9e 100644
--- a/src/util/integer_gmp_imp.h
+++ b/src/util/integer_gmp_imp.h
@@ -72,8 +72,12 @@ public:
   Integer(  signed long int z) : d_value(z) {}
   Integer(unsigned long int z) : d_value(z) {}
 
-  ~Integer() {}
+#ifdef CVC4_NEED_INT64_T_OVERLOADS
+  Integer( int64_t z) : d_value(static_cast<long>(z)) {}
+  Integer(uint64_t z) : d_value(static_cast<unsigned long>(z)) {}
+#endif /* CVC4_NEED_INT64_T_OVERLOADS */
 
+  ~Integer() {}
 
   Integer& operator=(const Integer& x){
     if(this == &x) return *this;
diff --git a/src/util/rational.h.in b/src/util/rational.h.in
index f97559377..c8e42a253 100644
--- a/src/util/rational.h.in
+++ b/src/util/rational.h.in
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): dejan, mdeters, cconway
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -16,7 +16,12 @@
  ** A multi-precision rational constant.
  **/
 
-// this is used to avoid a public header dependence on cvc4autoconfig.h
+// these gestures are used to avoid a public header dependence on cvc4autoconfig.h
+
+#if @CVC4_NEED_INT64_T_OVERLOADS@
+#  define CVC4_NEED_INT64_T_OVERLOADS
+#endif
+
 #if /* use CLN */ @CVC4_USE_CLN_IMP@
 #  define CVC4_CLN_IMP
 #endif /* @CVC4_USE_CLN_IMP@ */
diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h
index 4247a1e63..182e813cd 100644
--- a/src/util/rational_cln_imp.h
+++ b/src/util/rational_cln_imp.h
@@ -131,6 +131,11 @@ public:
   Rational(signed long int n) : d_value(n) { }
   Rational(unsigned long int n) : d_value(n) { }
 
+#ifdef CVC4_NEED_INT64_T_OVERLOADS
+  Rational(int64_t n) : d_value(static_cast<long>(n)) { }
+  Rational(uint64_t n) : d_value(static_cast<unsigned long>(n)) { }
+#endif /* CVC4_NEED_INT64_T_OVERLOADS */
+
   /**
    * Constructs a canonical Rational from a numerator and denominator.
    */
@@ -147,6 +152,15 @@ public:
     d_value /= d;
   }
 
+#ifdef CVC4_NEED_INT64_T_OVERLOADS
+  Rational(int64_t n, int64_t d) : d_value(static_cast<long>(n)) {
+    d_value /= static_cast<long>(d);
+  }
+  Rational(uint64_t n, uint64_t d) : d_value(static_cast<unsigned long>(n)) {
+    d_value /= static_cast<unsigned long>(d);
+  }
+#endif /* CVC4_NEED_INT64_T_OVERLOADS */
+
   Rational(const Integer& n, const Integer& d) :
     d_value(n.get_cl_I())
   {
diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h
index 0c8a46f33..b86dc32f2 100644
--- a/src/util/rational_gmp_imp.h
+++ b/src/util/rational_gmp_imp.h
@@ -111,6 +111,15 @@ public:
     d_value.canonicalize();
   }
 
+#ifdef CVC4_NEED_INT64_T_OVERLOADS
+  Rational(int64_t n) : d_value(static_cast<long>(n), 1) {
+    d_value.canonicalize();
+  }
+  Rational(uint64_t n) : d_value(static_cast<unsigned long>(n), 1) {
+    d_value.canonicalize();
+  }
+#endif /* CVC4_NEED_INT64_T_OVERLOADS */
+
   /**
    * Constructs a canonical Rational from a numerator and denominator.
    */
@@ -127,6 +136,15 @@ public:
     d_value.canonicalize();
   }
 
+#ifdef CVC4_NEED_INT64_T_OVERLOADS
+  Rational(int64_t n, int64_t d) : d_value(static_cast<long>(n), static_cast<long>(d)) {
+    d_value.canonicalize();
+  }
+  Rational(uint64_t n, uint64_t d) : d_value(static_cast<unsigned long>(n), static_cast<unsigned long>(d)) {
+    d_value.canonicalize();
+  }
+#endif /* CVC4_NEED_INT64_T_OVERLOADS */
+
   Rational(const Integer& n, const Integer& d) :
     d_value(n.get_mpz(), d.get_mpz())
   {