From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Mon, 18 Mar 2019 23:07:03 +0000 (-0700)
Subject: BitVector: Allow base 10 in constructor. (#2870)
X-Git-Tag: cvc5-1.0.0~4235
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7e3457b0e16cacef456287ae761c5293be1209d5;p=cvc5.git

BitVector: Allow base 10 in constructor. (#2870)
---

diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index b6049d5b3..2c266b11d 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -2047,7 +2047,14 @@ class CVC4_PUBLIC Solver
   Term mkBitVector(const char* s, uint32_t base = 2) const;
 
   /**
-   * Create a bit-vector constant from a given string.
+   * Create a bit-vector constant from a given string of base 2, 10 or 16.
+   *
+   * The size of resulting bit-vector is
+   * - base  2: the size of the binary string
+   * - base 10: the min. size required to represent the decimal as a bit-vector
+   * - base 16: the max. size required to represent the hexadecimal as a
+   *            bit-vector (4 * size of the given value string)
+   *
    * @param s the string representation of the constant
    * @param base the base of the string representation (2, 10, or 16)
    * @return the bit-vector constant
@@ -2055,7 +2062,9 @@ class CVC4_PUBLIC Solver
   Term mkBitVector(const std::string& s, uint32_t base = 2) const;
 
   /**
-   * Create a bit-vector constant of a given bit-width from a given string.
+   * Create a bit-vector constant of a given bit-width from a given string of
+   * base 2, 10 or 16.
+   *
    * @param size the bit-width of the constant
    * @param s the string representation of the constant
    * @param base the base of the string representation (2, 10, or 16)
@@ -2064,7 +2073,8 @@ class CVC4_PUBLIC Solver
   Term mkBitVector(uint32_t size, const char* s, uint32_t base) const;
 
   /**
-   * Create a bit-vector constant of a given bit-width from a given string.
+   * Create a bit-vector constant of a given bit-width from a given string of
+   * base 2, 10 or 16.
    * @param size the bit-width of the constant
    * @param s the string representation of the constant
    * @param base the base of the string representation (2, 10, or 16)
diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index 13c1f14dd..034a7774b 100644
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -66,11 +66,29 @@ class CVC4_PUBLIC BitVector
   {
   }
 
+  /**
+   * BitVector constructor.
+   *
+   * The value of the bit-vector is passed in as string of base 2, 10 or 16.
+   * The size of resulting bit-vector is
+   * - base  2: the size of the binary string
+   * - base 10: the min. size required to represent the decimal as a bit-vector
+   * - base 16: the max. size required to represent the hexadecimal as a
+   *            bit-vector (4 * size of the given value string)
+   *
+   * @param num The value of the bit-vector in string representation.
+   * @param base The base of the string representation.
+   */
   BitVector(const std::string& num, unsigned base = 2)
   {
-    CheckArgument(base == 2 || base == 16, base);
-    d_size = base == 2 ? num.size() : num.size() * 4;
+    CheckArgument(base == 2 || base == 10 || base == 16, base);
     d_value = Integer(num, base);
+    switch (base)
+    {
+      case 10: d_size = d_value.length(); break;
+      case 16: d_size = num.size() * 4; break;
+      default: d_size = num.size();
+    }
   }
 
   ~BitVector() {}
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index e3f9e0852..c42854fce 100644
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -267,16 +267,23 @@ void SolverBlack::testMkBitVector()
 {
   uint32_t size0 = 0, size1 = 8, size2 = 32, val1 = 2;
   uint64_t val2 = 2;
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector(size1, val1));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector(size2, val2));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector("1010", 2));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector("1010", 10));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector("1234", 10));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector("1010", 16));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector("a09f", 16));
   TS_ASSERT_THROWS(d_solver->mkBitVector(size0, val1), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkBitVector(size0, val2), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkBitVector("", 2), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkBitVector("10", 3), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkBitVector("20", 2), CVC4ApiException&);
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector(size1, val1));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector(size2, val2));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector("1010", 2));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector("1010", 16));
   TS_ASSERT_THROWS(d_solver->mkBitVector(8, "101010101", 2), CVC4ApiException&);
+  TS_ASSERT_EQUALS(d_solver->mkBitVector("1010", 2),
+                   d_solver->mkBitVector("10", 10));
+  TS_ASSERT_EQUALS(d_solver->mkBitVector("1010", 2),
+                   d_solver->mkBitVector("a", 16));
   TS_ASSERT_EQUALS(d_solver->mkBitVector(8, "01010101", 2).toString(),
                    "0bin01010101");
   TS_ASSERT_EQUALS(d_solver->mkBitVector(8, "F", 16).toString(),