src/util/integer_cln_imp.cpp

   1 /*********************                                                        */
   2 /*! \file integer_cln_imp.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Tim King, Aina Niemetz, Clark Barrett
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2018 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 void Integer::parseInt(const std::string& s, unsigned base)
  63 {
  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,
  90                       const std::string& s,
  91                       unsigned base)
  92 {
  93   try {
  94     // Removing leading zeroes, CLN has a bug for these inputs up to and
  95     // including CLN v1.3.2.
  96     // See http://www.ginac.de/CLN/cln.git/?a=commit;h=4a477b0cc3dd7fbfb23b25090ff8c8869c8fa21a for details.
  97     size_t pos = s.find_first_not_of('0');
  98     if(pos == std::string::npos) {
  99       d_value = read_integer(flags, "0", NULL, NULL);
 100     } else {
 101       const char* cstr = s.c_str();
 102       const char* start = cstr + pos;
 103       const char* end = cstr + s.length();
 104       d_value = read_integer(flags, start, end, NULL);
 105     }
 106   } catch(...) {
 107     std::stringstream ss;
 108     ss << "Integer() failed to parse value \"" << s << "\" in base " << base;
 109     throw std::invalid_argument(ss.str());
 110   }
 111 }
 112
 113 bool Integer::fitsSignedInt() const {
 114   // http://www.ginac.de/CLN/cln.html#Conversions
 115   // TODO improve performance
 116   Assert(s_slowSignedIntMin <= s_fastSignedIntMin);
 117   Assert(s_fastSignedIntMin <= s_fastSignedIntMax);
 118   Assert(s_fastSignedIntMax <= s_slowSignedIntMax);
 119
 120   return (d_value <= s_fastSignedIntMax || d_value <= s_slowSignedIntMax) &&
 121     (d_value >= s_fastSignedIntMin || d_value >= s_slowSignedIntMax);
 122 }
 123
 124 bool Integer::fitsUnsignedInt() const {
 125   // TODO improve performance
 126   Assert(s_fastUnsignedIntMax <= s_slowUnsignedIntMax);
 127   return sgn() >= 0 &&
 128     (d_value <= s_fastUnsignedIntMax || d_value <= s_slowUnsignedIntMax);
 129 }
 130
 131 signed int Integer::getSignedInt() const {
 132   // ensure there isn't overflow
 133   CheckArgument(fitsSignedInt(), this, "Overflow detected in Integer::getSignedInt()");
 134   return cln::cl_I_to_int(d_value);
 135 }
 136
 137 unsigned int Integer::getUnsignedInt() const {
 138   // ensure there isn't overflow
 139   CheckArgument(fitsUnsignedInt(), this, "Overflow detected in Integer::getUnsignedInt()");
 140   return cln::cl_I_to_uint(d_value);
 141 }
 142
 143 bool Integer::fitsSignedLong() const {
 144   return d_value <= s_signedLongMax && d_value >= s_signedLongMin;
 145 }
 146
 147 bool Integer::fitsUnsignedLong() const {
 148   return sgn() >= 0 && d_value <= s_unsignedLongMax;
 149 }
 150
 151 Integer Integer::pow(unsigned long int exp) const {
 152   if (exp == 0) {
 153     return Integer(1);
 154   } else {
 155     Assert(exp > 0);
 156     cln::cl_I result = cln::expt_pos(d_value, exp);
 157     return Integer(result);
 158   }
 159 }
 160
 161 Integer Integer::modAdd(const Integer& y, const Integer& m) const
 162 {
 163   cln::cl_modint_ring ry = cln::find_modint_ring(m.d_value);
 164   cln::cl_MI xm = ry->canonhom(d_value);
 165   cln::cl_MI ym = ry->canonhom(y.d_value);
 166   cln::cl_MI res = xm + ym;
 167   return Integer(ry->retract(res));
 168 }
 169
 170 Integer Integer::modMultiply(const Integer& y, const Integer& m) const
 171 {
 172   cln::cl_modint_ring ry = cln::find_modint_ring(m.d_value);
 173   cln::cl_MI xm = ry->canonhom(d_value);
 174   cln::cl_MI ym = ry->canonhom(y.d_value);
 175   cln::cl_MI res = xm * ym;
 176   return Integer(ry->retract(res));
 177 }
 178
 179 Integer Integer::modInverse(const Integer& m) const
 180 {
 181   PrettyCheckArgument(m > 0, m, "m must be greater than zero");
 182   cln::cl_modint_ring ry = cln::find_modint_ring(m.d_value);
 183   cln::cl_MI xm = ry->canonhom(d_value);
 184   /* normalize to modulo m for coprime check */
 185   cln::cl_I x = ry->retract(xm);
 186   if (x == 0 || cln::gcd(x, m.d_value) != 1)
 187   {
 188     return Integer(-1);
 189   }
 190   cln::cl_MI res = cln::recip(xm);
 191   return Integer(ry->retract(res));
 192 }
 193 } /* namespace CVC4 */