From: Clark Barrett <barrett@cs.nyu.edu>
Date: Fri, 19 Aug 2016 23:39:43 +0000 (-0700)
Subject: Added fitsSignedLong and fitsUnsignedLong
X-Git-Tag: cvc5-1.0.0~6040^2~1
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d28f9f38ead8ec010a38e021f92d5de95261afc9;p=cvc5.git

Added fitsSignedLong and fitsUnsignedLong
---

diff --git a/src/util/integer_cln_imp.cpp b/src/util/integer_cln_imp.cpp
index 0064f2904..aa6cb03af 100644
--- a/src/util/integer_cln_imp.cpp
+++ b/src/util/integer_cln_imp.cpp
@@ -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 */
diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h
index 177fc02cf..6bfebbaf1 100644
--- a/src/util/integer_cln_imp.h
+++ b/src/util/integer_cln_imp.h
@@ -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,
diff --git a/src/util/integer_gmp_imp.cpp b/src/util/integer_gmp_imp.cpp
index d165dbec3..e0472ac4c 100644
--- a/src/util/integer_gmp_imp.cpp
+++ b/src/util/integer_gmp_imp.cpp
@@ -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);
diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h
index 0c5665e38..3a95c6b85 100644
--- a/src/util/integer_gmp_imp.h
+++ b/src/util/integer_gmp_imp.h
@@ -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