From: Tim King <taking@cs.nyu.edu>
Date: Sat, 1 Dec 2012 02:09:02 +0000 (+0000)
Subject: Fix for a CLN related bug on 32 bit systems. Integer((1<<29)+1) and Integer((long... 
X-Git-Tag: cvc5-1.0.0~7496
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b66fc3eac2717e8a887f1d4603c15cbcb7460e98;p=cvc5.git

Fix for a CLN related bug on 32 bit systems. Integer((1<<29)+1) and Integer((long int)((1<<29)+1)) gave different values.  This was confirmed on vm-int1.cims.nyu.edu. See ginac.de/CLN/cln_3.html#SEC15 for more details. rational_white and integer_white have tests covering this.
---

diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h
index 07e85c118..211c40741 100644
--- a/src/util/integer_cln_imp.h
+++ b/src/util/integer_cln_imp.h
@@ -120,8 +120,8 @@ public:
 
   Integer(const Integer& q) : d_value(q.d_value) {}
 
-  Integer(  signed int z) : d_value(z) {}
-  Integer(unsigned int z) : d_value(z) {}
+  Integer(  signed int z) : d_value((signed long int)z) {}
+  Integer(unsigned int z) : d_value((unsigned long int)z) {}
   Integer(  signed long int z) : d_value(z) {}
   Integer(unsigned long int z) : d_value(z) {}
 
@@ -192,35 +192,17 @@ public:
     return *this;
   }
 
-  /*
-  Integer operator/(const Integer& y) const {
-    return Integer( cln::floor1(d_value, y.d_value) );
-  }
-  Integer& operator/=(const Integer& y) {
-    d_value = cln::floor1(d_value, y.d_value);
-    return *this;
-  }
-
-  Integer operator%(const Integer& y) const {
-    return Integer( cln::floor2(d_value, y.d_value).remainder );
-  }
-  Integer& operator%=(const Integer& y) {
-    d_value = cln::floor2(d_value, y.d_value).remainder;
-    return *this;
-  }
-  */
-
 
   Integer bitwiseOr(const Integer& y) const {
-    return Integer(cln::logior(d_value, y.d_value));  
+    return Integer(cln::logior(d_value, y.d_value));
   }
 
   Integer bitwiseAnd(const Integer& y) const {
-    return Integer(cln::logand(d_value, y.d_value));  
+    return Integer(cln::logand(d_value, y.d_value));
   }
 
   Integer bitwiseXor(const Integer& y) const {
-    return Integer(cln::logxor(d_value, y.d_value));  
+    return Integer(cln::logxor(d_value, y.d_value));
   }
 
   Integer bitwiseNot() const {
@@ -401,8 +383,6 @@ public:
     return d_value == -1;
   }
 
-  //friend std::ostream& operator<<(std::ostream& os, const Integer& n);
-
   long getLong() const {
     // ensure there isn't overflow
     CheckArgument(d_value <= std::numeric_limits<long>::max(), this,
@@ -445,7 +425,7 @@ public:
    */
   unsigned isPow2() const {
     if (d_value <= 0) return 0;
-    // power2p returns n such that d_value = 2^(n-1) 
+    // power2p returns n such that d_value = 2^(n-1)
     return cln::power2p(d_value);
   }
 
diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h
index 4877c0ea6..88327b400 100644
--- a/src/util/rational_cln_imp.h
+++ b/src/util/rational_cln_imp.h
@@ -125,8 +125,8 @@ public:
   /**
    * Constructs a canonical Rational from a numerator.
    */
-  Rational(signed int n) : d_value(n) { }
-  Rational(unsigned int n) : d_value(n) { }
+  Rational(signed int n) : d_value((signed long int)n) { }
+  Rational(unsigned int n) : d_value((unsigned long int)n) { }
   Rational(signed long int n) : d_value(n) { }
   Rational(unsigned long int n) : d_value(n) { }
 
@@ -138,10 +138,10 @@ public:
   /**
    * Constructs a canonical Rational from a numerator and denominator.
    */
-  Rational(signed int n, signed int d) : d_value(n) {
+  Rational(signed int n, signed int d) : d_value((signed long int)n) {
     d_value /= d;
   }
-  Rational(unsigned int n, unsigned int d) : d_value(n) {
+  Rational(unsigned int n, unsigned int d) : d_value((unsigned long int)n) {
     d_value /= d;
   }
   Rational(signed long int n, signed long int d) : d_value(n) {