This commit adds TypeNode::leastCommonTypeNode(). The special case for arithmetic in TypeNode::operator==() has been removed. A number of faulty type checking checks were switched to use isSubtypeOf. The resolves bug #339

3 files changed, 58 insertions, 2 deletions

diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h
index d3e5c07ca..43b77df6a 100644
--- a/src/util/integer_cln_imp.h
+++ b/src/util/integer_cln_imp.h
@@ -443,10 +443,20 @@ public:
 
 /*   cl_I xgcd (const cl_I& a, const cl_I& b, cl_I* u, cl_I* v) */
 /* This function ("extended gcd") returns the greatest common divisor g of a and b and at the same time the representation of g as an integral linear combination of a and b: u and v with u*a+v*b = g, g >= 0. u and v will be normalized to be of smallest possible absolute value, in the following sense: If a and b are non-zero, and abs(a) != abs(b), u and v will satisfy the inequalities abs(u) <= abs(b)/(2*g), abs(v) <= abs(a)/(2*g). */
-  static void extendedGcd(Integer& g, Integer& s, Integer& t, const Integer& a, const Integer& b){    
+  static void extendedGcd(Integer& g, Integer& s, Integer& t, const Integer& a, const Integer& b){
     g.d_value = cln::xgcd(a.d_value, b.d_value, &s.d_value, &t.d_value);
   }
 
+  /** Returns a reference to the minimum of two integers. */
+  static const Integer& min(const Integer& a, const Integer& b){
+    return (a <=b ) ? a : b;
+  }
+
+  /** Returns a reference to the maximum of two integers. */
+  static const Integer& max(const Integer& a, const Integer& b){
+    return (a >= b ) ? a : b;
+  }
+
   friend class CVC4::Rational;
 };/* class Integer */
 
diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h
index 74b4adad0..f5254a3d2 100644
--- a/src/util/integer_gmp_imp.h
+++ b/src/util/integer_gmp_imp.h
@@ -400,10 +400,20 @@ public:
   }
 
   static void extendedGcd(Integer& g, Integer& s, Integer& t, const Integer& a, const Integer& b){
+    //see the documentation for:
     //mpz_gcdext (mpz_t g, mpz_t s, mpz_t t, mpz_t a, mpz_t b);
     mpz_gcdext (g.d_value.get_mpz_t(), s.d_value.get_mpz_t(), t.d_value.get_mpz_t(), a.d_value.get_mpz_t(), b.d_value.get_mpz_t());
   }
 
+  /** Returns a reference to the minimum of two integers. */
+  static const Integer& min(const Integer& a, const Integer& b){
+    return (a <=b ) ? a : b;
+  }
+
+  /** Returns a reference to the maximum of two integers. */
+  static const Integer& max(const Integer& a, const Integer& b){
+    return (a >= b ) ? a : b;
+  }
 
   friend class CVC4::Rational;
 };/* class Integer */
diff --git a/src/util/subrange_bound.h b/src/util/subrange_bound.h
index 9d4d446bd..063e59a0f 100644
--- a/src/util/subrange_bound.h
+++ b/src/util/subrange_bound.h
@@ -57,7 +57,7 @@ public:
   }
 
   /** Get the finite SubrangeBound, failing an assertion if infinite. */
-  Integer getBound() const throw(IllegalArgumentException) {
+  const Integer& getBound() const throw(IllegalArgumentException) {
     CheckArgument(!d_nobound, this, "SubrangeBound is infinite");
     return d_bound;
   }
@@ -130,6 +130,23 @@ public:
       ( hasBound() && b.hasBound() && getBound() <= b.getBound() );
   }
 
+
+  static SubrangeBound min(const SubrangeBound& a, const SubrangeBound& b){
+    if(a.hasBound() && b.hasBound()){
+      return SubrangeBound(Integer::min(a.getBound(), b.getBound()));
+    }else{
+      return SubrangeBound();
+    }
+  }
+
+ static SubrangeBound max(const SubrangeBound& a, const SubrangeBound& b){
+    if(a.hasBound() && b.hasBound()){
+      return SubrangeBound(Integer::max(a.getBound(), b.getBound()));
+    }else{
+      return SubrangeBound();
+    }
+ }
+
 };/* class SubrangeBound */
 
 class CVC4_PUBLIC SubrangeBounds {
@@ -192,6 +209,25 @@ public:
     return lower <= bounds.lower && upper >= bounds.upper;
   }
 
+  /**
+   * Returns true if the join of two subranges is not (- infinity, + infinity).
+   */
+  static bool joinIsBounded(const SubrangeBounds& a, const SubrangeBounds& b){
+    return (a.lower.hasBound() && b.lower.hasBound()) ||
+      (a.upper.hasBound() && b.upper.hasBound());
+  }
+
+  /**
+   * Returns the join of two subranges, a and b.
+   * precondition: joinIsBounded(a,b) is true
+   */
+  static SubrangeBounds join(const SubrangeBounds& a, const SubrangeBounds& b){
+    Assert(joinIsBounded(a,b));
+    SubrangeBound newLower = SubrangeBound::min(a.lower, b.lower);
+    SubrangeBound newUpper = SubrangeBound::max(a.upper, b.upper);
+    return SubrangeBounds(newLower, newUpper);
+  }
+
 };/* class SubrangeBounds */
 
 struct CVC4_PUBLIC SubrangeBoundsHashStrategy {