From: Morgan Deters <mdeters@gmail.com>
Date: Tue, 14 Aug 2012 20:08:29 +0000 (+0000)
Subject: Fixes to integer wrapper classes:
X-Git-Tag: cvc5-1.0.0~7869
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d8fd737fb9ca867f53a287de1c4a87f16a6834f7;p=cvc5.git

Fixes to integer wrapper classes:
* more uniform interface between the CLN and GMP wrappers
* support base inference (base == 0) on parsing strings with the CLN wrapper; this was a difference from the GMP wrapper (resolves bug #372)
---

diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h
index 71d6d5b6d..8f7daf4f5 100644
--- a/src/util/integer_cln_imp.h
+++ b/src/util/integer_cln_imp.h
@@ -58,6 +58,42 @@ private:
   //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 {
+      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 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);
+  }
+
 public:
 
   /** Constructs a rational with the value 0. */
@@ -69,32 +105,12 @@ public:
    * For more information about what is a valid rational string,
    * see GMP's documentation for mpq_set_str().
    */
-  explicit Integer(const char * s, int base = 10) throw (std::invalid_argument){
-    cln::cl_read_flags flags;
-    flags.syntax = cln::syntax_integer;
-    flags.lsyntax = cln::lsyntax_standard;
-    flags.rational_base = base;
-    try{
-      d_value = read_integer(flags, s, NULL, NULL);
-    }catch(...){
-      std::stringstream ss;
-      ss << "Integer() failed to parse value \"" <<s << "\" in base=" <<base;
-      throw std::invalid_argument(ss.str());
-    }
+  explicit Integer(const char* sp, unsigned base = 10) throw (std::invalid_argument) {
+    parseInt(std::string(sp), base);
   }
 
-  Integer(const std::string& s, int base = 10) throw (std::invalid_argument) {
-    cln::cl_read_flags flags;
-    flags.syntax = cln::syntax_integer;
-    flags.lsyntax = cln::lsyntax_standard;
-    flags.rational_base = base;
-    try{
-      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());
-    }
+  explicit Integer(const std::string& s, unsigned base = 10) throw (std::invalid_argument) {
+    parseInt(s, base);
   }
 
   Integer(const Integer& q) : d_value(q.d_value) {}
diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h
index ea7967023..c553baff9 100644
--- a/src/util/integer_gmp_imp.h
+++ b/src/util/integer_gmp_imp.h
@@ -62,8 +62,8 @@ public:
    * For more information about what is a valid rational string,
    * see GMP's documentation for mpq_set_str().
    */
-  explicit Integer(const char * s, int base = 10): d_value(s,base) {}
-  Integer(const std::string& s, unsigned base = 10) : d_value(s, base) {}
+  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) {}
 
   Integer(const Integer& q) : d_value(q.d_value) {}
 
diff --git a/test/unit/util/integer_black.h b/test/unit/util/integer_black.h
index 06be9e57d..a2641e118 100644
--- a/test/unit/util/integer_black.h
+++ b/test/unit/util/integer_black.h
@@ -283,6 +283,26 @@ public:
     TS_ASSERT_EQUALS(res, large.toString());
   }
 
+  void testBaseInference() {
+    TS_ASSERT_EQUALS(Integer("0xa", 0), 10);
+    TS_ASSERT_EQUALS(Integer("0xff", 0), 255);
+    TS_ASSERT_EQUALS(Integer("011", 0), 9);
+    TS_ASSERT_EQUALS(Integer("0b1010", 0), 10);
+    TS_ASSERT_EQUALS(Integer("-1", 0), -1);
+    TS_ASSERT_EQUALS(Integer("42", 0), 42);
+  }
+
+  void testParseErrors() {
+    TS_ASSERT_THROWS(Integer("abracadabra"), std::invalid_argument);
+    TS_ASSERT_THROWS(Integer("+-1"), std::invalid_argument);
+    TS_ASSERT_THROWS(Integer("-+1"), std::invalid_argument);
+    TS_ASSERT_THROWS(Integer("5i"), std::invalid_argument);
+    TS_ASSERT_THROWS(Integer("10xyz"), std::invalid_argument);
+    TS_ASSERT_THROWS(Integer("0xff", 10), std::invalid_argument);
+    TS_ASSERT_THROWS(Integer("#x5", 0), std::invalid_argument);
+    TS_ASSERT_THROWS(Integer("0b123", 0), std::invalid_argument);
+  }
+
   void testPow() {
     TS_ASSERT_EQUALS( Integer(1), Integer(1).pow(0) );
     TS_ASSERT_EQUALS( Integer(1), Integer(5).pow(0) );
diff --git a/test/unit/util/subrange_bound_white.h b/test/unit/util/subrange_bound_white.h
index d7587d679..762c43809 100644
--- a/test/unit/util/subrange_bound_white.h
+++ b/test/unit/util/subrange_bound_white.h
@@ -39,7 +39,7 @@ public:
   }
 
   void testZero() {
-    SubrangeBound b1(0), b2(string("0")), b3(Integer("1"));
+    SubrangeBound b1(0), b2(Integer("0")), b3(Integer("1"));
     TS_ASSERT( b1.hasBound() && b2.hasBound() && b3.hasBound() );
     TS_ASSERT( b1.getBound() == 0 && b2.getBound() == 0 && b3.getBound() == 1 );
     TS_ASSERT( b1 == b2 ); TS_ASSERT( b2 == b1 );
@@ -57,7 +57,7 @@ public:
   }
 
   void testOne() {
-    SubrangeBound b(string("1"));
+    SubrangeBound b(Integer("1"));
     TS_ASSERT( b.hasBound() );
     TS_ASSERT( b.getBound() == 1 );
     ss.str(""); ss << b;