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 Integer Integer::oneExtend(uint32_t size, uint32_t amount) const {
  44   DebugCheckArgument((*this) < Integer(1).multiplyByPow2(size), size);
  45   cln::cl_byte range(amount, size);
  46   cln::cl_I allones = (cln::cl_I(1) << (size + amount))- 1; // 2^size - 1
  47   Integer temp(allones);
  48
  49   return Integer(cln::deposit_field(allones, d_value, range));
  50 }
  51
  52
  53 Integer Integer::exactQuotient(const Integer& y) const {
  54   DebugCheckArgument(y.divides(*this), y);
  55   return Integer( cln::exquo(d_value, y.d_value) );
  56 }
  57
  58
  59 void Integer::parseInt(const std::string& s, unsigned base) throw(std::invalid_argument) {
  60   cln::cl_read_flags flags;
  61   flags.syntax = cln::syntax_integer;
  62   flags.lsyntax = cln::lsyntax_standard;
  63   flags.rational_base = base;
  64   if(base == 0) {
  65     // infer base in a manner consistent with GMP
  66     if(s[0] == '0') {
  67       flags.lsyntax = cln::lsyntax_commonlisp;
  68       std::string st = s;
  69       if(s[1] == 'X' || s[1] == 'x') {
  70         st.replace(0, 2, "#x");
  71       } else if(s[1] == 'B' || s[1] == 'b') {
  72         st.replace(0, 2, "#b");
  73       } else {
  74         st.replace(0, 1, "#o");
  75       }
  76       readInt(flags, st, base);
  77       return;
  78     } else {
  79       flags.rational_base = 10;
  80     }
  81   }
  82   readInt(flags, s, base);
  83 }
  84
  85 void Integer::readInt(const cln::cl_read_flags& flags, const std::string& s, unsigned base) throw(std::invalid_argument) {
  86   try {
  87     // Removing leading zeroes, CLN has a bug for these inputs up to and
  88     // including CLN v1.3.2.
  89     // See http://www.ginac.de/CLN/cln.git/?a=commit;h=4a477b0cc3dd7fbfb23b25090ff8c8869c8fa21a for details.
  90     size_t pos = s.find_first_not_of('0');
  91     if(pos == std::string::npos) {
  92       d_value = read_integer(flags, "0", NULL, NULL);
  93     } else {
  94       const char* cstr = s.c_str();
  95       const char* start = cstr + pos;
  96       const char* end = cstr + s.length();
  97       d_value = read_integer(flags, start, end, NULL);
  98     }
  99   } catch(...) {
 100     std::stringstream ss;
 101     ss << "Integer() failed to parse value \"" << s << "\" in base " << base;
 102     throw std::invalid_argument(ss.str());
 103   }
 104 }
 105
 106 bool Integer::fitsSignedInt() const {
 107   // http://www.ginac.de/CLN/cln.html#Conversions
 108   // TODO improve performance
 109   Assert(s_slowSignedIntMin <= s_fastSignedIntMin);
 110   Assert(s_fastSignedIntMin <= s_fastSignedIntMax);
 111   Assert(s_fastSignedIntMax <= s_slowSignedIntMax);
 112
 113   return (d_value <= s_fastSignedIntMax || d_value <= s_slowSignedIntMax) &&
 114     (d_value >= s_fastSignedIntMin || d_value >= s_slowSignedIntMax);
 115 }
 116
 117 bool Integer::fitsUnsignedInt() const {
 118   // TODO improve performance
 119   Assert(s_fastUnsignedIntMax <= s_slowUnsignedIntMax);
 120   return sgn() >= 0 &&
 121     (d_value <= s_fastUnsignedIntMax || d_value <= s_slowUnsignedIntMax);
 122 }
 123
 124 signed int Integer::getSignedInt() const {
 125   // ensure there isn't overflow
 126   CheckArgument(fitsSignedInt(), this, "Overflow detected in Integer::getSignedInt()");
 127   return cln::cl_I_to_int(d_value);
 128 }
 129
 130 unsigned int Integer::getUnsignedInt() const {
 131   // ensure there isn't overflow
 132   CheckArgument(fitsUnsignedInt(), this, "Overflow detected in Integer::getUnsignedInt()");
 133   return cln::cl_I_to_uint(d_value);
 134 }
 135
 136 } /* namespace CVC4 */