src/util/integer_cln_imp.cpp

   1 #include "cvc4autoconfig.h"
   2 #include "util/integer.h"
   3 #include <string>
   4 #include <sstream>
   5
   6 #ifndef CVC4_CLN_IMP
   7 #  error "This source should only ever be built if CVC4_CLN_IMP is on !"
   8 #endif /* CVC4_CLN_IMP */
   9
  10 using namespace std;
  11 using namespace CVC4;
  12
  13
  14 void Integer::parseInt(const std::string& s, unsigned base) throw(std::invalid_argument) {
  15   cln::cl_read_flags flags;
  16   flags.syntax = cln::syntax_integer;
  17   flags.lsyntax = cln::lsyntax_standard;
  18   flags.rational_base = base;
  19   if(base == 0) {
  20     // infer base in a manner consistent with GMP
  21     if(s[0] == '0') {
  22       flags.lsyntax = cln::lsyntax_commonlisp;
  23       std::string st = s;
  24       if(s[1] == 'X' || s[1] == 'x') {
  25         st.replace(0, 2, "#x");
  26       } else if(s[1] == 'B' || s[1] == 'b') {
  27         st.replace(0, 2, "#b");
  28       } else {
  29         st.replace(0, 1, "#o");
  30       }
  31       readInt(flags, st, base);
  32       return;
  33     } else {
  34       flags.rational_base = 10;
  35     }
  36   }
  37   readInt(flags, s, base);
  38 }
  39
  40 void Integer::readInt(const cln::cl_read_flags& flags, const std::string& s, unsigned base) throw(std::invalid_argument) {
  41   try {
  42     // Removing leading zeroes, CLN has a bug for these inputs up to and
  43     // including CLN v1.3.2.
  44     // See http://www.ginac.de/CLN/cln.git/?a=commit;h=4a477b0cc3dd7fbfb23b25090ff8c8869c8fa21a for details.
  45     size_t pos = s.find_first_not_of('0');
  46     if(pos == std::string::npos) {
  47       d_value = read_integer(flags, "0", NULL, NULL);
  48     } else {
  49       const char* cstr = s.c_str();
  50       const char* start = cstr + pos;
  51       const char* end = cstr + s.length();
  52       d_value = read_integer(flags, start, end, NULL);
  53     }
  54   } catch(...) {
  55     std::stringstream ss;
  56     ss << "Integer() failed to parse value \"" << s << "\" in base " << base;
  57     throw std::invalid_argument(ss.str());
  58   }
  59 }
  60
  61 bool Integer::fitsSignedInt() const {
  62   // TODO improve performance
  63   return d_value <= std::numeric_limits<signed int>::max() &&
  64     d_value >= std::numeric_limits<signed int>::min();
  65 }
  66
  67 bool Integer::fitsUnsignedInt() const {
  68   // TODO improve performance
  69   return sgn() >= 0 && d_value <= std::numeric_limits<unsigned int>::max();
  70 }
  71
  72 signed int Integer::getSignedInt() const {
  73   // ensure there isn't overflow
  74   CheckArgument(fitsSignedInt(), this, "Overflow detected in Integer::getSignedInt()");
  75   return cln::cl_I_to_int(d_value);
  76 }
  77
  78 unsigned int Integer::getUnsignedInt() const {
  79   // ensure there isn't overflow
  80   CheckArgument(fitsUnsignedInt(), this, "Overflow detected in Integer::getUnsignedInt()");
  81   return cln::cl_I_to_uint(d_value);
  82 }