Add getters to retrieve constants from api::Term (#5677)

This PR adds method to obtain constant values from api::Term that are either integers or strings.

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 80fb8a5fb70413998604d6aa47169104931a1538..8044508c7e5ea6fa506ce1087fbf3b4a9203597f 100644 (file)
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -2073,6 +2073,106 @@ CVC4::Expr Term::getExpr(void) const
 // to the new API. !!!
 const CVC4::Node& Term::getNode(void) const { return *d_node; }
 
+namespace detail {
+const Rational& getRational(const CVC4::Node& node)
+{
+  return node.getConst<Rational>();
+}
+Integer getInteger(const CVC4::Node& node)
+{
+  return node.getConst<Rational>().getNumerator();
+}
+template <typename T>
+bool checkIntegerBounds(const Integer& i)
+{
+  return i >= std::numeric_limits<T>::min()
+         && i <= std::numeric_limits<T>::max();
+}
+bool checkReal32Bounds(const Rational& r)
+{
+  return checkIntegerBounds<std::int32_t>(r.getNumerator())
+         && checkIntegerBounds<std::uint32_t>(r.getDenominator());
+}
+bool checkReal64Bounds(const Rational& r)
+{
+  return checkIntegerBounds<std::int64_t>(r.getNumerator())
+         && checkIntegerBounds<std::uint64_t>(r.getDenominator());
+}
+
+bool isInteger(const Node& node)
+{
+  return node.getKind() == CVC4::Kind::CONST_RATIONAL
+         && node.getConst<Rational>().isIntegral();
+}
+bool isInt32(const Node& node)
+{
+  return isInteger(node)
+         && checkIntegerBounds<std::int32_t>(getInteger(node));
+}
+bool isUInt32(const Node& node)
+{
+  return isInteger(node)
+         && checkIntegerBounds<std::uint32_t>(getInteger(node));
+}
+bool isInt64(const Node& node)
+{
+  return isInteger(node)
+         && checkIntegerBounds<std::int64_t>(getInteger(node));
+}
+bool isUInt64(const Node& node)
+{
+  return isInteger(node)
+         && checkIntegerBounds<std::uint64_t>(getInteger(node));
+}
+}  // namespace detail
+
+bool Term::isInt32() const { return detail::isInt32(*d_node); }
+std::int32_t Term::getInt32() const
+{
+  CVC4_API_CHECK(detail::isInt32(*d_node))
+      << "Term should be a Int32 when calling getInt32()";
+  return detail::getInteger(*d_node).getSignedInt();
+}
+bool Term::isUInt32() const { return detail::isUInt32(*d_node); }
+std::uint32_t Term::getUInt32() const
+{
+  CVC4_API_CHECK(detail::isUInt32(*d_node))
+      << "Term should be a UInt32 when calling getUInt32()";
+  return detail::getInteger(*d_node).getUnsignedInt();
+}
+bool Term::isInt64() const { return detail::isInt64(*d_node); }
+std::int64_t Term::getInt64() const
+{
+  CVC4_API_CHECK(detail::isInt64(*d_node))
+      << "Term should be a Int64 when calling getInt64()";
+  return detail::getInteger(*d_node).getLong();
+}
+bool Term::isUInt64() const { return detail::isUInt64(*d_node); }
+std::uint64_t Term::getUInt64() const
+{
+  CVC4_API_CHECK(detail::isUInt64(*d_node))
+      << "Term should be a UInt64 when calling getUInt64()";
+  return detail::getInteger(*d_node).getUnsignedLong();
+}
+bool Term::isInteger() const { return detail::isInteger(*d_node); }
+std::string Term::getInteger() const
+{
+  CVC4_API_CHECK(detail::isInteger(*d_node))
+      << "Term should be an Int when calling getIntString()";
+  return detail::getInteger(*d_node).toString();
+}
+
+bool Term::isString() const
+{
+  return d_node->getKind() == CVC4::Kind::CONST_STRING;
+}
+std::wstring Term::getString() const
+{
+  CVC4_API_CHECK(d_node->getKind() == CVC4::Kind::CONST_STRING)
+      << "Term should be a String when calling getString()";
+  return d_node->getConst<CVC4::String>().toWString();
+}
+
 std::ostream& operator<<(std::ostream& out, const Term& t)
 {
   out << t.toString();

diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index eb55e4007cfb4dd8d8b37f2cb1cbcc5ac862a7ee..98752c697fcfe9df768116a0001fefd3e65687a9 100644 (file)
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -1151,6 +1151,59 @@ class CVC4_PUBLIC Term
   // to the new API. !!!
   const CVC4::Node& getNode(void) const;
 
+  /**
+   * Returns true if the term is an integer that fits within std::int32_t.
+   */
+  bool isInt32() const;
+  /**
+   * Returns the stored integer as a std::int32_t. Asserts isInt32().
+   */
+  std::int32_t getInt32() const;
+  /**
+   * Returns true if the term is an integer that fits within std::uint32_t.
+   */
+  bool isUInt32() const;
+  /**
+   * Returns the stored integer as a std::uint32_t. Asserts isUInt32().
+   */
+  std::uint32_t getUInt32() const;
+  /**
+   * Returns true if the term is an integer that fits within std::int64_t.
+   */
+  bool isInt64() const;
+  /**
+   * Returns the stored integer as a std::int64_t. Asserts isInt64().
+   */
+  std::int64_t getInt64() const;
+  /**
+   * Returns true if the term is an integer that fits within std::uint64_t.
+   */
+  bool isUInt64() const;
+  /**
+   * Returns the stored integer as a std::uint64_t. Asserts isUInt64().
+   */
+  std::uint64_t getUInt64() const;
+  /**
+   * Returns true if the term is an integer.
+   */
+  bool isInteger() const;
+  /**
+   * Returns the stored integer in (decimal) string representation. Asserts
+   * isInteger().
+   */
+  std::string getInteger() const;
+
+  /**
+   * Returns true if the term is a string constant.
+   */
+  bool isString() const;
+  /**
+   * Returns the stored string constant. This method is not to be confused with
+   * toString() which returns the term in some string representation, whatever
+   * data it may hold. Asserts isString().
+   */
+  std::wstring getString() const;
+
  protected:
   /**
    * The associated solver object.

diff --git a/src/util/integer_gmp_imp.cpp b/src/util/integer_gmp_imp.cpp
index fec71b26b6a25aee8aaacdcad4fc40e61d6ea7e0..9cc8fb77357cc8b5425ee3c2eac5b6f3da6236c6 100644 (file)
--- a/src/util/integer_gmp_imp.cpp
+++ b/src/util/integer_gmp_imp.cpp
@@ -403,7 +403,7 @@ unsigned int Integer::getUnsignedInt() const
                 this,
                 "Overflow detected in Integer::getUnsignedInt()");
   CheckArgument(
-      fitsSignedInt(), this, "Overflow detected in Integer::getUnsignedInt()");
+      fitsUnsignedInt(), this, "Overflow detected in Integer::getUnsignedInt()");
   return (unsigned int)d_value.get_ui();
 }
 

diff --git a/src/util/string.cpp b/src/util/string.cpp
index 0d40ebb05d77764effdfb6d583555026fd421bbc..e625c21990ca198a64632ceb70c80a67355fc754 100644 (file)
--- a/src/util/string.cpp
+++ b/src/util/string.cpp
@@ -291,6 +291,16 @@ std::string String::toString(bool useEscSequences) const {
   return str.str();
 }
 
+std::wstring String::toWString() const
+{
+  std::wstring res(size(), static_cast<wchar_t>(0));
+  for (std::size_t i = 0; i < size(); ++i)
+  {
+    res[i] = static_cast<wchar_t>(d_str[i]);
+  }
+  return res;
+}
+
 bool String::isLeq(const String &y) const
 {
   for (unsigned i = 0; i < size(); ++i)

diff --git a/src/util/string.h b/src/util/string.h
index 7102ec1f2cf179f11653f48dd1f75ed2efd42ca4..9e503bb0771f29b79631fe69202717564ac7f9e1 100644 (file)
--- a/src/util/string.h
+++ b/src/util/string.h
@@ -114,6 +114,13 @@ class CVC4_PUBLIC String {
    *    CVC4::String( s ).toString() = s.
    */
   std::string toString(bool useEscSequences = false) const;
+  /* toWString
+   * Converts this string to a std::wstring.
+   *
+   * Unlike toString(), this method uses no escape sequences as both this class
+   * and std::wstring use 32bit characters.
+   */
+  std::wstring toWString() const;
   /** is this the empty string? */
   bool empty() const { return d_str.empty(); }
   /** is less than or equal to string y */

diff --git a/test/unit/api/term_black.cpp b/test/unit/api/term_black.cpp
index f616a1a300674addd0b32714bcae958cae08603d..6b032ebd6849ba3bfed3b802d7f6d213724f147f 100644 (file)
--- a/test/unit/api/term_black.cpp
+++ b/test/unit/api/term_black.cpp
@@ -671,6 +671,80 @@ TEST_F(TestApiTermBlack, termChildren)
   ASSERT_THROW(tnull[0], CVC4ApiException);
 }
 
+TEST_F(TestApiTermBlack, getInteger)
+{
+  Term int1 = d_solver.mkInteger("-18446744073709551616");
+  Term int2 = d_solver.mkInteger("-18446744073709551615");
+  Term int3 = d_solver.mkInteger("-4294967296");
+  Term int4 = d_solver.mkInteger("-4294967295");
+  Term int5 = d_solver.mkInteger("-10");
+  Term int6 = d_solver.mkInteger("0");
+  Term int7 = d_solver.mkInteger("10");
+  Term int8 = d_solver.mkInteger("4294967295");
+  Term int9 = d_solver.mkInteger("4294967296");
+  Term int10 = d_solver.mkInteger("18446744073709551615");
+  Term int11 = d_solver.mkInteger("18446744073709551616");
+
+  EXPECT_TRUE(!int1.isInt32() && !int1.isUInt32() && !int1.isInt64()
+              && !int1.isUInt64() && int1.isInteger());
+  EXPECT_EQ(int1.getInteger(), "-18446744073709551616");
+  EXPECT_TRUE(!int2.isInt32() && !int2.isUInt32() && !int2.isInt64()
+              && !int2.isUInt64() && int2.isInteger());
+  EXPECT_EQ(int2.getInteger(), "-18446744073709551615");
+  EXPECT_TRUE(!int3.isInt32() && !int3.isUInt32() && int3.isInt64()
+              && !int3.isUInt64() && int3.isInteger());
+  EXPECT_EQ(int3.getInt64(), -4294967296);
+  EXPECT_EQ(int3.getInteger(), "-4294967296");
+  EXPECT_TRUE(!int4.isInt32() && !int4.isUInt32() && int4.isInt64()
+              && !int4.isUInt64() && int4.isInteger());
+  EXPECT_EQ(int4.getInt64(), -4294967295);
+  EXPECT_EQ(int4.getInteger(), "-4294967295");
+  EXPECT_TRUE(int5.isInt32() && !int5.isUInt32() && int5.isInt64()
+              && !int5.isUInt64() && int5.isInteger());
+  EXPECT_EQ(int5.getInt32(), -10);
+  EXPECT_EQ(int5.getInt64(), -10);
+  EXPECT_EQ(int5.getInteger(), "-10");
+  EXPECT_TRUE(int6.isInt32() && int6.isUInt32() && int6.isInt64()
+              && int6.isUInt64() && int6.isInteger());
+  EXPECT_EQ(int6.getInt32(), 0);
+  EXPECT_EQ(int6.getUInt32(), 0);
+  EXPECT_EQ(int6.getInt64(), 0);
+  EXPECT_EQ(int6.getUInt64(), 0);
+  EXPECT_EQ(int6.getInteger(), "0");
+  EXPECT_TRUE(int7.isInt32() && int7.isUInt32() && int7.isInt64()
+              && int7.isUInt64() && int7.isInteger());
+  EXPECT_EQ(int7.getInt32(), 10);
+  EXPECT_EQ(int7.getUInt32(), 10);
+  EXPECT_EQ(int7.getInt64(), 10);
+  EXPECT_EQ(int7.getUInt64(), 10);
+  EXPECT_EQ(int7.getInteger(), "10");
+  EXPECT_TRUE(!int8.isInt32() && int8.isUInt32() && int8.isInt64()
+              && int8.isUInt64() && int8.isInteger());
+  EXPECT_EQ(int8.getUInt32(), 4294967295);
+  EXPECT_EQ(int8.getInt64(), 4294967295);
+  EXPECT_EQ(int8.getUInt64(), 4294967295);
+  EXPECT_EQ(int8.getInteger(), "4294967295");
+  EXPECT_TRUE(!int9.isInt32() && !int9.isUInt32() && int9.isInt64()
+              && int9.isUInt64() && int9.isInteger());
+  EXPECT_EQ(int9.getInt64(), 4294967296);
+  EXPECT_EQ(int9.getUInt64(), 4294967296);
+  EXPECT_EQ(int9.getInteger(), "4294967296");
+  EXPECT_TRUE(!int10.isInt32() && !int10.isUInt32() && !int10.isInt64()
+              && int10.isUInt64() && int10.isInteger());
+  EXPECT_EQ(int10.getUInt64(), 18446744073709551615ull);
+  EXPECT_EQ(int10.getInteger(), "18446744073709551615");
+  EXPECT_TRUE(!int11.isInt32() && !int11.isUInt32() && !int11.isInt64()
+              && !int11.isUInt64() && int11.isInteger());
+  EXPECT_EQ(int11.getInteger(), "18446744073709551616");
+}
+
+TEST_F(TestApiTermBlack, getString)
+{
+  Term s1 = d_solver.mkString("abcde");
+  EXPECT_TRUE(s1.isString());
+  EXPECT_EQ(s1.getString(), L"abcde");
+}
+
 TEST_F(TestApiTermBlack, substitute)
 {
   Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x");