if CVC4_CLN_IMP
libutil_la_SOURCES += \
- rational_cln_imp.cpp
+ rational_cln_imp.cpp \
+ integer_cln_imp.cpp
endif
if CVC4_GMP_IMP
libutil_la_SOURCES += \
- rational_gmp_imp.cpp
+ rational_gmp_imp.cpp \
+ integer_gmp_imp.cpp
endif
EXTRA_DIST = \
rational_cln_imp.h \
integer_cln_imp.h \
+ integer_cln_imp.cpp \
rational_cln_imp.cpp \
rational_gmp_imp.h \
integer_gmp_imp.h \
+ integer_gmp_imp.cpp \
rational_gmp_imp.cpp \
rational.h.in \
integer.h.in \
--- /dev/null
+#include "cvc4autoconfig.h"
+#include "util/integer.h"
+#include <string>
+#include <sstream>
+
+#ifndef CVC4_CLN_IMP
+# error "This source should only ever be built if CVC4_CLN_IMP is on !"
+#endif /* CVC4_CLN_IMP */
+
+using namespace std;
+using namespace CVC4;
+
+
+void Integer::parseInt(const std::string& s, unsigned base) throw(std::invalid_argument) {
+ cln::cl_read_flags flags;
+ flags.syntax = cln::syntax_integer;
+ flags.lsyntax = cln::lsyntax_standard;
+ flags.rational_base = base;
+ if(base == 0) {
+ // infer base in a manner consistent with GMP
+ if(s[0] == '0') {
+ flags.lsyntax = cln::lsyntax_commonlisp;
+ std::string st = s;
+ if(s[1] == 'X' || s[1] == 'x') {
+ st.replace(0, 2, "#x");
+ } else if(s[1] == 'B' || s[1] == 'b') {
+ st.replace(0, 2, "#b");
+ } else {
+ st.replace(0, 1, "#o");
+ }
+ readInt(flags, st, base);
+ return;
+ } else {
+ flags.rational_base = 10;
+ }
+ }
+ readInt(flags, s, base);
+}
+
+void Integer::readInt(const cln::cl_read_flags& flags, const std::string& s, unsigned base) throw(std::invalid_argument) {
+ try {
+ // Removing leading zeroes, CLN has a bug for these inputs up to and
+ // including CLN v1.3.2.
+ // See http://www.ginac.de/CLN/cln.git/?a=commit;h=4a477b0cc3dd7fbfb23b25090ff8c8869c8fa21a for details.
+ size_t pos = s.find_first_not_of('0');
+ if(pos == std::string::npos) {
+ d_value = read_integer(flags, "0", NULL, NULL);
+ } else {
+ const char* cstr = s.c_str();
+ const char* start = cstr + pos;
+ const char* end = cstr + s.length();
+ d_value = read_integer(flags, start, end, NULL);
+ }
+ } catch(...) {
+ std::stringstream ss;
+ ss << "Integer() failed to parse value \"" << s << "\" in base " << base;
+ throw std::invalid_argument(ss.str());
+ }
+}
class CVC4_PUBLIC Integer {
private:
/**
- * Stores the value of the rational is stored in a C++ GMP integer class.
- * Using this instead of mpz_t allows for easier destruction.
+ * Stores the value of the rational is stored in a C++ CLN integer class.
*/
cln::cl_I d_value;
/**
- * Gets a reference to the gmp data that backs up the integer.
+ * Gets a reference to the cln data that backs up the integer.
* Only accessible to friend classes.
*/
- //const mpz_class& get_mpz() const { return d_value; }
const cln::cl_I& get_cl_I() const { return d_value; }
/**
- * Constructs an Integer by copying a GMP C++ primitive.
+ * Constructs an Integer by copying a CLN C++ primitive.
*/
- //Integer(const mpz_class& val) : d_value(val) {}
Integer(const cln::cl_I& val) : d_value(val) {}
- void readInt(const cln::cl_read_flags& flags, const std::string& s, unsigned base) throw(std::invalid_argument) {
- try {
- if(s.find_first_not_of('0') == std::string::npos) {
- // String of all zeroes, CLN has a bug for these inputs up to and
- // including CLN v1.3.2.
- // See http://www.ginac.de/CLN/cln.git/?a=commit;h=4a477b0cc3dd7fbfb23b25090ff8c8869c8fa21a for details.
- d_value = read_integer(flags, "0", NULL, NULL);
- } else {
- d_value = read_integer(flags, s.c_str(), NULL, NULL);
- }
- } catch(...) {
- std::stringstream ss;
- ss << "Integer() failed to parse value \"" << s << "\" in base " << base;
- throw std::invalid_argument(ss.str());
- }
- }
+ void readInt(const cln::cl_read_flags& flags, const std::string& s, unsigned base) throw(std::invalid_argument);
- void parseInt(const std::string& s, unsigned base) throw(std::invalid_argument) {
- cln::cl_read_flags flags;
- flags.syntax = cln::syntax_integer;
- flags.lsyntax = cln::lsyntax_standard;
- flags.rational_base = base;
- if(base == 0) {
- // infer base in a manner consistent with GMP
- if(s[0] == '0') {
- flags.lsyntax = cln::lsyntax_commonlisp;
- std::string st = s;
- if(s[1] == 'X' || s[1] == 'x') {
- st.replace(0, 2, "#x");
- } else if(s[1] == 'B' || s[1] == 'b') {
- st.replace(0, 2, "#b");
- } else {
- st.replace(0, 1, "#o");
- }
- readInt(flags, st, base);
- return;
- } else {
- flags.rational_base = 10;
- }
- }
- readInt(flags, s, base);
- }
+ void parseInt(const std::string& s, unsigned base) throw(std::invalid_argument);
public:
}
bool isBitSet(uint32_t i) const {
- return !extractBitRange(1, i).isZero();
+ return !extractBitRange(1, i).isZero();
}
-
+
Integer setBit(uint32_t i) const {
cln::cl_I mask(1);
- mask = mask << i;
- return Integer(cln::logior(d_value, mask));
+ mask = mask << i;
+ return Integer(cln::logior(d_value, mask));
}
-
+
Integer oneExtend(uint32_t size, uint32_t amount) const {
DebugCheckArgument((*this) < Integer(1).multiplyByPow2(size), size);
cln::cl_byte range(amount, size);
--- /dev/null
+/********************* */
+/*! \file integer_gmp_imp.cpp
+ ** \verbatim
+ ** Original author: Tim King
+ ** Major contributors: Morgan Deters, Christopher L. Conway
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief A multi-precision rational constant.
+ **
+ ** A multi-precision rational constant.
+ **/
+
+#include "cvc4autoconfig.h"
+#include "util/rational.h"
+#include <string>
+#include <sstream>
+#include <cmath>
+
+#ifndef CVC4_GMP_IMP
+# error "This source should only ever be built if CVC4_GMP_IMP is on !"
+#endif /* CVC4_GMP_IMP */
+
+using namespace std;
+using namespace CVC4;
+
+
+
+Integer::Integer(const char* s, unsigned base)
+ : d_value(s, base)
+{}
+
+Integer::Integer(const std::string& s, unsigned base)
+ : d_value(s, base)
+{}
* For more information about what is a valid rational string,
* see GMP's documentation for mpq_set_str().
*/
- explicit Integer(const char* s, unsigned base = 10): d_value(s, base) {}
- explicit Integer(const std::string& s, unsigned base = 10) : d_value(s, base) {}
+ explicit Integer(const char* s, unsigned base = 10);
+ explicit Integer(const std::string& s, unsigned base = 10);
Integer(const Integer& q) : d_value(q.d_value) {}
mpz_and(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
return Integer(result);
}
-
+
Integer bitwiseXor(const Integer& y) const {
mpz_class result;
mpz_xor(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
mpz_com(result.get_mpz_t(), d_value.get_mpz_t());
return Integer(result);
}
-
+
/**
* Return this*(2^pow).
*/
return Integer( result );
}
- /**
+ /**
* Returns the Integer obtained by setting the ith bit of the
- * current Integer to 1.
+ * current Integer to 1.
*/
Integer setBit(uint32_t i) const {
mpz_class res = d_value;
mpz_setbit(res.get_mpz_t(), i);
- return Integer(res);
+ return Integer(res);
}
bool isBitSet(uint32_t i) const {
- return !extractBitRange(1, i).isZero();
+ return !extractBitRange(1, i).isZero();
}
-
+
/**
* Returns the integer with the binary representation of size bits
* extended with amount 1's
using namespace std;
const char* largeVal = "4547897890548754897897897897890789078907890";
+const char* lotsOfLeadingZeroes = "00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001";
class IntegerBlack : public CxxTest::TestSuite {
TS_ASSERT_EQUALS( r, Integer(-1));
}
+
+ void testLeadingZeroes() {
+ string leadingZeroes(lotsOfLeadingZeroes);
+ Integer one(1u);
+ Integer one_from_string(leadingZeroes,2);
+ TS_ASSERT_EQUALS(one, one_from_string);
+ }
};
projects / cvc5.git / commitdiff