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

1 files changed, 11 insertions, 1 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 */