src/util/integer_cln_imp.cpp

   1 /*********************                                                        */
   2 /*! \file integer_cln_imp.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Tim King, Morgan Deters
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief [[ Add one-line brief description here ]]
  13  **
  14  ** [[ Add lengthier description here ]]
  15  ** \todo document this file
  16  **/
  17 #include "util/integer.h"
  18
  19 #include <sstream>
  20 #include <string>
  21
  22 #include "cvc4autoconfig.h"
  23
  24
  25 #ifndef CVC4_CLN_IMP
  26 #  error "This source should only ever be built if CVC4_CLN_IMP is on !"
  27 #endif /* CVC4_CLN_IMP */
  28
  29 #include "base/cvc4_assert.h"
  30
  31 using namespace std;
  32
  33 namespace CVC4 {
  34
  35 signed int Integer::s_fastSignedIntMin = -(1<<29);
  36 signed int Integer::s_fastSignedIntMax = (1<<29)-1;
  37 signed long Integer::s_slowSignedIntMin = (signed long) std::numeric_limits<signed int>::min();
  38 signed long Integer::s_slowSignedIntMax =  (signed long) std::numeric_limits<signed int>::max();
  39
  40 unsigned int Integer::s_fastUnsignedIntMax = (1<<29)-1;
  41 unsigned long Integer::s_slowUnsignedIntMax =  (unsigned long) std::numeric_limits<unsigned int>::max();
  42
  43 unsigned long Integer::s_signedLongMin = std::numeric_limits<signed long>::min();
  44 unsigned long Integer::s_signedLongMax = std::numeric_limits<signed long>::max();
  45 unsigned long Integer::s_unsignedLongMax = std::numeric_limits<unsigned long>::max();
  46
  47 Integer Integer::oneExtend(uint32_t size, uint32_t amount) const {
  48   DebugCheckArgument((*this) < Integer(1).multiplyByPow2(size), size);
  49   cln::cl_byte range(amount, size);
  50   cln::cl_I allones = (cln::cl_I(1) << (size + amount))- 1; // 2^size - 1
  51   Integer temp(allones);
  52
  53   return Integer(cln::deposit_field(allones, d_value, range));
  54 }
  55
  56
  57 Integer Integer::exactQuotient(const Integer& y) const {
  58   DebugCheckArgument(y.divides(*this), y);
  59   return Integer( cln::exquo(d_value, y.d_value) );
  60 }
  61
  62
  63 void Integer::parseInt(const std::string& s, unsigned base) throw(std::invalid_argument) {
  64   cln::cl_read_flags flags;
  65   flags.syntax = cln::syntax_integer;
  66   flags.lsyntax = cln::lsyntax_standard;
  67   flags.rational_base = base;
  68   if(base == 0) {
  69     // infer base in a manner consistent with GMP
  70     if(s[0] == '0') {
  71       flags.lsyntax = cln::lsyntax_commonlisp;
  72       std::string st = s;
  73       if(s[1] == 'X' || s[1] == 'x') {
  74         st.replace(0, 2, "#x");
  75       } else if(s[1] == 'B' || s[1] == 'b') {
  76         st.replace(0, 2, "#b");
  77       } else {
  78         st.replace(0, 1, "#o");
  79       }
  80       readInt(flags, st, base);
  81       return;
  82     } else {
  83       flags.rational_base = 10;
  84     }
  85   }
  86   readInt(flags, s, base);
  87 }
  88
  89 void Integer::readInt(const cln::cl_read_flags& flags, const std::string& s, unsigned base) throw(std::invalid_argument) {
  90   try {
  91     // Removing leading zeroes, CLN has a bug for these inputs up to and
  92     // including CLN v1.3.2.
  93     // See http://www.ginac.de/CLN/cln.git/?a=commit;h=4a477b0cc3dd7fbfb23b25090ff8c8869c8fa21a for details.
  94     size_t pos = s.find_first_not_of('0');
  95     if(pos == std::string::npos) {
  96       d_value = read_integer(flags, "0", NULL, NULL);
  97     } else {
  98       const char* cstr = s.c_str();
  99       const char* start = cstr + pos;
 100       const char* end = cstr + s.length();
 101       d_value = read_integer(flags, start, end, NULL);
 102     }
 103   } catch(...) {
 104     std::stringstream ss;
 105     ss << "Integer() failed to parse value \"" << s << "\" in base " << base;
 106     throw std::invalid_argument(ss.str());
 107   }
 108 }
 109
 110 bool Integer::fitsSignedInt() const {
 111   // http://www.ginac.de/CLN/cln.html#Conversions
 112   // TODO improve performance
 113   Assert(s_slowSignedIntMin <= s_fastSignedIntMin);
 114   Assert(s_fastSignedIntMin <= s_fastSignedIntMax);
 115   Assert(s_fastSignedIntMax <= s_slowSignedIntMax);
 116
 117   return (d_value <= s_fastSignedIntMax || d_value <= s_slowSignedIntMax) &&
 118     (d_value >= s_fastSignedIntMin || d_value >= s_slowSignedIntMax);
 119 }
 120
 121 bool Integer::fitsUnsignedInt() const {
 122   // TODO improve performance
 123   Assert(s_fastUnsignedIntMax <= s_slowUnsignedIntMax);
 124   return sgn() >= 0 &&
 125     (d_value <= s_fastUnsignedIntMax || d_value <= s_slowUnsignedIntMax);
 126 }
 127
 128 signed int Integer::getSignedInt() const {
 129   // ensure there isn't overflow
 130   CheckArgument(fitsSignedInt(), this, "Overflow detected in Integer::getSignedInt()");
 131   return cln::cl_I_to_int(d_value);
 132 }
 133
 134 unsigned int Integer::getUnsignedInt() const {
 135   // ensure there isn't overflow
 136   CheckArgument(fitsUnsignedInt(), this, "Overflow detected in Integer::getUnsignedInt()");
 137   return cln::cl_I_to_uint(d_value);
 138 }
 139
 140 bool Integer::fitsSignedLong() const {
 141   return d_value <= s_signedLongMax && d_value >= s_signedLongMin;
 142 }
 143
 144 bool Integer::fitsUnsignedLong() const {
 145   return sgn() >= 0 && d_value <= s_unsignedLongMax;
 146 }
 147
 148 } /* namespace CVC4 */