Added fitsSignedLong and fitsUnsignedLong
authorClark Barrett <barrett@cs.nyu.edu>
Fri, 19 Aug 2016 23:39:43 +0000 (16:39 -0700)
committerClark Barrett <barrett@cs.nyu.edu>
Fri, 19 Aug 2016 23:39:43 +0000 (16:39 -0700)
src/util/integer_cln_imp.cpp
src/util/integer_cln_imp.h
src/util/integer_gmp_imp.cpp
src/util/integer_gmp_imp.h

index 0064f2904cf0571638926aace16d9fee36eab6a3..aa6cb03afb2402f7f192a37f32d223f97dab4c77 100644 (file)
@@ -40,6 +40,10 @@ signed long Integer::s_slowSignedIntMax =  (signed long) std::numeric_limits<sig
 unsigned int Integer::s_fastUnsignedIntMax = (1<<29)-1;
 unsigned long Integer::s_slowUnsignedIntMax =  (unsigned long) std::numeric_limits<unsigned int>::max();
 
+unsigned long Integer::s_signedLongMin = std::numeric_limits<signed long>::min();
+unsigned long Integer::s_signedLongMax = std::numeric_limits<signed long>::max();
+unsigned long Integer::s_unsignedLongMax = std::numeric_limits<unsigned long>::max();
+
 Integer Integer::oneExtend(uint32_t size, uint32_t amount) const {
   DebugCheckArgument((*this) < Integer(1).multiplyByPow2(size), size);
   cln::cl_byte range(amount, size);
@@ -133,4 +137,12 @@ unsigned int Integer::getUnsignedInt() const {
   return cln::cl_I_to_uint(d_value);
 }
 
+bool Integer::fitsSignedLong() const {
+  return d_value <= s_signedLongMax && d_value >= s_signedLongMin;
+}
+
+bool Integer::fitsUnsignedLong() const {
+  return sgn() >= 0 && d_value <= s_unsignedLongMax;
+}
+
 } /* namespace CVC4 */
index 177fc02cf6eb90546e3f6a7f10fe045bbeee3c2d..6bfebbaf1e66185dc76b4ca4ae0c6c3c0bc4b016 100644 (file)
@@ -66,7 +66,9 @@ private:
   static signed long s_slowSignedIntMax; /*  std::numeric_limits<signed int>::max() */
   static signed long s_slowSignedIntMin; /*  std::numeric_limits<signed int>::min() */
   static unsigned long s_slowUnsignedIntMax; /*  std::numeric_limits<unsigned int>::max() */
-
+  static unsigned long s_signedLongMin;
+  static unsigned long s_signedLongMax;
+  static unsigned long s_unsignedLongMax;
 public:
 
   /** Constructs a rational with the value 0. */
@@ -425,6 +427,10 @@ public:
 
   unsigned int getUnsignedInt() const;
 
+  bool fitsSignedLong() const;
+
+  bool fitsUnsignedLong() const;
+
   long getLong() const {
     // ensure there isn't overflow
     CheckArgument(d_value <= std::numeric_limits<long>::max(), this,
index d165dbec3b2e79abc9b32a8cd0b1324212e38cc4..e0472ac4cfd323534e31405f14074fda656c4b48 100644 (file)
@@ -73,6 +73,14 @@ unsigned int Integer::getUnsignedInt() const {
   return (unsigned int) d_value.get_ui();
 }
 
+bool Integer::fitsSignedLong() const {
+  return d_value.fits_slong_p();
+}
+
+bool Integer::fitsUnsignedLong() const {
+  return d_value.fits_ulong_p();
+}
+
 Integer Integer::oneExtend(uint32_t size, uint32_t amount) const {
   // check that the size is accurate
   DebugCheckArgument((*this) < Integer(1).multiplyByPow2(size), size);
index 0c5665e38903f8645defe0c829ea5f8f387e3064..3a95c6b85accc129f680c5d27ac750408d767471 100644 (file)
@@ -411,6 +411,10 @@ public:
 
   unsigned int getUnsignedInt() const;
 
+  bool fitsSignedLong() const;
+
+  bool fitsUnsignedLong() const;
+
   long getLong() const {
     long si = d_value.get_si();
     // ensure there wasn't overflow