diff options
author | Tim King <taking@cs.nyu.edu> | 2014-04-01 16:54:36 -0400 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2014-04-01 16:54:36 -0400 |
commit | 98df8ccdd49674c02360a0662fbc1765ace2d5bf (patch) | |
tree | b80e3c78a79b45401a21a9bfb03bf63174e55199 /src/util/integer_cln_imp.cpp | |
parent | e347f43940c53a8dfdaa022bc19900fcee631c08 (diff) |
Fixing bug 552. There was a bug when integers are made using a string with a lot of leading 0s on old versions of CLN.1.3.x
Diffstat (limited to 'src/util/integer_cln_imp.cpp')
-rw-r--r-- | src/util/integer_cln_imp.cpp | 59 |
1 files changed, 59 insertions, 0 deletions
diff --git a/src/util/integer_cln_imp.cpp b/src/util/integer_cln_imp.cpp new file mode 100644 index 000000000..383f27688 --- /dev/null +++ b/src/util/integer_cln_imp.cpp @@ -0,0 +1,59 @@ +#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()); + } +} |