Add more getters for api::Term (#6496)

This PR adds more getter functions for api::Term to retrieve values from constant terms (and terms that the average API use might consider constant).
It also introduces std::wstring as regular representation for string constants instead of std::vector<uint32> for the SMT-LIB parser and the String class.

13 files changed, 1035 insertions, 241 deletions

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 066ea0082..d7959c950 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -2309,20 +2309,6 @@ bool Term::isNull() const
   CVC5_API_TRY_CATCH_END;
 }
 
-Term Term::getConstArrayBase() const
-{
-  NodeManagerScope scope(d_solver->getNodeManager());
-  CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_CHECK_NOT_NULL;
-  // CONST_ARRAY kind maps to STORE_ALL internal kind
-  CVC5_API_CHECK(d_node->getKind() == cvc5::Kind::STORE_ALL)
-      << "Expecting a CONST_ARRAY Term when calling getConstArrayBase()";
-  //////// all checks before this line
-  return Term(d_solver, d_node->getConst<ArrayStoreAll>().getValue());
-  ////////
-  CVC5_API_TRY_CATCH_END;
-}
-
 std::vector<Term> Term::getConstSequenceElements() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
@@ -2559,7 +2545,14 @@ const cvc5::Node& Term::getNode(void) const { return *d_node; }
 namespace detail {
 const Rational& getRational(const cvc5::Node& node)
 {
-  return node.getConst<Rational>();
+  switch (node.getKind())
+  {
+    case cvc5::Kind::CAST_TO_REAL: return node[0].getConst<Rational>();
+    case cvc5::Kind::CONST_RATIONAL: return node.getConst<Rational>();
+    default:
+      CVC5_API_CHECK(false) << "Node is not a rational.";
+      return node.getConst<Rational>();
+  }
 }
 Integer getInteger(const cvc5::Node& node)
 {
@@ -2582,6 +2575,20 @@ bool checkReal64Bounds(const Rational& r)
          && checkIntegerBounds<std::uint64_t>(r.getDenominator());
 }
 
+bool isReal(const Node& node)
+{
+  return node.getKind() == cvc5::Kind::CONST_RATIONAL
+         || node.getKind() == cvc5::Kind::CAST_TO_REAL;
+}
+bool isReal32(const Node& node)
+{
+  return isReal(node) && checkReal32Bounds(getRational(node));
+}
+bool isReal64(const Node& node)
+{
+  return isReal(node) && checkReal64Bounds(getRational(node));
+}
+
 bool isInteger(const Node& node)
 {
   return node.getKind() == cvc5::Kind::CONST_RATIONAL
@@ -2605,7 +2612,7 @@ bool isUInt64(const Node& node)
 }
 }  // namespace detail
 
-bool Term::isInt32() const
+bool Term::isInt32Value() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK_NOT_NULL;
@@ -2615,45 +2622,62 @@ bool Term::isInt32() const
   CVC5_API_TRY_CATCH_END;
 }
 
-std::int32_t Term::getInt32() const
+std::int32_t Term::getInt32Value() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK_NOT_NULL;
-  CVC5_API_CHECK(detail::isInt32(*d_node))
-      << "Term should be a Int32 when calling getInt32()";
+  CVC5_API_ARG_CHECK_EXPECTED(detail::isInt32(*d_node), *d_node)
+      << "Term to be a 32-bit integer value when calling getInt32Value()";
   //////// all checks before this line
   return detail::getInteger(*d_node).getSignedInt();
   ////////
   CVC5_API_TRY_CATCH_END;
 }
 
-bool Term::isUInt32() const { return detail::isUInt32(*d_node); }
-std::uint32_t Term::getUInt32() const
+bool Term::isUInt32Value() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK_NOT_NULL;
+  //////// all checks before this line
+  return detail::isUInt32(*d_node);
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+std::uint32_t Term::getUInt32Value() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK_NOT_NULL;
-  CVC5_API_CHECK(detail::isUInt32(*d_node))
-      << "Term should be a UInt32 when calling getUInt32()";
+  CVC5_API_ARG_CHECK_EXPECTED(detail::isUInt32(*d_node), *d_node)
+      << "Term to be a unsigned 32-bit integer value when calling "
+         "getUInt32Value()";
   //////// all checks before this line
   return detail::getInteger(*d_node).getUnsignedInt();
   ////////
   CVC5_API_TRY_CATCH_END;
 }
 
-bool Term::isInt64() const { return detail::isInt64(*d_node); }
-std::int64_t Term::getInt64() const
+bool Term::isInt64Value() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK_NOT_NULL;
-  CVC5_API_CHECK(detail::isInt64(*d_node))
-      << "Term should be a Int64 when calling getInt64()";
+  //////// all checks before this line
+  return detail::isInt64(*d_node);
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+std::int64_t Term::getInt64Value() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK_NOT_NULL;
+  CVC5_API_ARG_CHECK_EXPECTED(detail::isInt64(*d_node), *d_node)
+      << "Term to be a 64-bit integer value when calling getInt64Value()";
   //////// all checks before this line
   return detail::getInteger(*d_node).getLong();
   ////////
   CVC5_API_TRY_CATCH_END;
 }
 
-bool Term::isUInt64() const
+bool Term::isUInt64Value() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK_NOT_NULL;
@@ -2663,32 +2687,41 @@ bool Term::isUInt64() const
   CVC5_API_TRY_CATCH_END;
 }
 
-std::uint64_t Term::getUInt64() const
+std::uint64_t Term::getUInt64Value() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK_NOT_NULL;
-  CVC5_API_CHECK(detail::isUInt64(*d_node))
-      << "Term should be a UInt64 when calling getUInt64()";
+  CVC5_API_ARG_CHECK_EXPECTED(detail::isUInt64(*d_node), *d_node)
+      << "Term to be a unsigned 64-bit integer value when calling "
+         "getUInt64Value()";
   //////// all checks before this line
   return detail::getInteger(*d_node).getUnsignedLong();
   ////////
   CVC5_API_TRY_CATCH_END;
 }
 
-bool Term::isInteger() const { return detail::isInteger(*d_node); }
-std::string Term::getInteger() const
+bool Term::isIntegerValue() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK_NOT_NULL;
+  //////// all checks before this line
+  return detail::isInteger(*d_node);
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+std::string Term::getIntegerValue() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK_NOT_NULL;
-  CVC5_API_CHECK(detail::isInteger(*d_node))
-      << "Term should be an Int when calling getIntString()";
+  CVC5_API_ARG_CHECK_EXPECTED(detail::isInteger(*d_node), *d_node)
+      << "Term to be an integer value when calling getIntegerValue()";
   //////// all checks before this line
   return detail::getInteger(*d_node).toString();
   ////////
   CVC5_API_TRY_CATCH_END;
 }
 
-bool Term::isString() const
+bool Term::isStringValue() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK_NOT_NULL;
@@ -2698,12 +2731,13 @@ bool Term::isString() const
   CVC5_API_TRY_CATCH_END;
 }
 
-std::wstring Term::getString() const
+std::wstring Term::getStringValue() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK_NOT_NULL;
-  CVC5_API_CHECK(d_node->getKind() == cvc5::Kind::CONST_STRING)
-      << "Term should be a String when calling getString()";
+  CVC5_API_ARG_CHECK_EXPECTED(d_node->getKind() == cvc5::Kind::CONST_STRING,
+                              *d_node)
+      << "Term to be a string value when calling getStringValue()";
   //////// all checks before this line
   return d_node->getConst<cvc5::String>().toWString();
   ////////
@@ -2720,6 +2754,387 @@ std::vector<Node> Term::termVectorToNodes(const std::vector<Term>& terms)
   return res;
 }
 
+bool Term::isReal32Value() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK_NOT_NULL;
+  //////// all checks before this line
+  return detail::isReal32(*d_node);
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+std::pair<std::int32_t, std::uint32_t> Term::getReal32Value() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK_NOT_NULL;
+  CVC5_API_ARG_CHECK_EXPECTED(detail::isReal32(*d_node), *d_node)
+      << "Term to be a 32-bit rational value when calling getReal32Value()";
+  //////// all checks before this line
+  const Rational& r = detail::getRational(*d_node);
+  return std::make_pair(r.getNumerator().getSignedInt(),
+                        r.getDenominator().getUnsignedInt());
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+bool Term::isReal64Value() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK_NOT_NULL;
+  //////// all checks before this line
+  return detail::isReal64(*d_node);
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+std::pair<std::int64_t, std::uint64_t> Term::getReal64Value() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK_NOT_NULL;
+  CVC5_API_ARG_CHECK_EXPECTED(detail::isReal64(*d_node), *d_node)
+      << "Term to be a 64-bit rational value when calling getReal64Value()";
+  //////// all checks before this line
+  const Rational& r = detail::getRational(*d_node);
+  return std::make_pair(r.getNumerator().getLong(),
+                        r.getDenominator().getUnsignedLong());
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+bool Term::isRealValue() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK_NOT_NULL;
+  //////// all checks before this line
+  return detail::isReal(*d_node);
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+std::string Term::getRealValue() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK_NOT_NULL;
+  CVC5_API_ARG_CHECK_EXPECTED(detail::isReal(*d_node), *d_node)
+      << "Term to be a rational value when calling getRealValue()";
+  //////// all checks before this line
+  return detail::getRational(*d_node).toString();
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+
+bool Term::isConstArray() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK_NOT_NULL;
+  //////// all checks before this line
+  return d_node->getKind() == cvc5::Kind::STORE_ALL;
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+Term Term::getConstArrayBase() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK_NOT_NULL;
+  CVC5_API_ARG_CHECK_EXPECTED(d_node->getKind() == cvc5::Kind::STORE_ALL,
+                              *d_node)
+      << "Term to be a constant array when calling getConstArrayBase()";
+  //////// all checks before this line
+  const auto& ar = d_node->getConst<ArrayStoreAll>();
+  return Term(d_solver, ar.getValue());
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+
+bool Term::isBooleanValue() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK_NOT_NULL;
+  //////// all checks before this line
+  return d_node->getKind() == cvc5::Kind::CONST_BOOLEAN;
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+bool Term::getBooleanValue() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK_NOT_NULL;
+  CVC5_API_ARG_CHECK_EXPECTED(d_node->getKind() == cvc5::Kind::CONST_BOOLEAN,
+                              *d_node)
+      << "Term to be a Boolean value when calling getBooleanValue()";
+  //////// all checks before this line
+  return d_node->getConst<bool>();
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+
+bool Term::isBitVectorValue() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK_NOT_NULL;
+  //////// all checks before this line
+  return d_node->getKind() == cvc5::Kind::CONST_BITVECTOR;
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+std::string Term::getBitVectorValue(std::uint32_t base) const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK_NOT_NULL;
+  CVC5_API_ARG_CHECK_EXPECTED(d_node->getKind() == cvc5::Kind::CONST_BITVECTOR,
+                              *d_node)
+      << "Term to be a bit-vector value when calling getBitVectorValue()";
+  //////// all checks before this line
+  return d_node->getConst<BitVector>().toString(base);
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+
+bool Term::isAbstractValue() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK_NOT_NULL;
+  //////// all checks before this line
+  return d_node->getKind() == cvc5::Kind::ABSTRACT_VALUE;
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+std::string Term::getAbstractValue() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK_NOT_NULL;
+  CVC5_API_ARG_CHECK_EXPECTED(d_node->getKind() == cvc5::Kind::ABSTRACT_VALUE,
+                              *d_node)
+      << "Term to be an abstract value when calling "
+         "getAbstractValue()";
+  //////// all checks before this line
+  return d_node->getConst<AbstractValue>().getIndex().toString();
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+
+bool Term::isTupleValue() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK_NOT_NULL;
+  //////// all checks before this line
+  return d_node->getKind() == cvc5::Kind::APPLY_CONSTRUCTOR && d_node->isConst()
+         && d_node->getType().getDType().isTuple();
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+std::vector<Term> Term::getTupleValue() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK_NOT_NULL;
+  CVC5_API_ARG_CHECK_EXPECTED(d_node->getKind() == cvc5::Kind::APPLY_CONSTRUCTOR
+                                  && d_node->isConst()
+                                  && d_node->getType().getDType().isTuple(),
+                              *d_node)
+      << "Term to be a tuple value when calling getTupleValue()";
+  //////// all checks before this line
+  std::vector<Term> res;
+  for (size_t i = 0, n = d_node->getNumChildren(); i < n; ++i)
+  {
+    res.emplace_back(Term(d_solver, (*d_node)[i]));
+  }
+  return res;
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+
+bool Term::isFloatingPointPosZero() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK_NOT_NULL;
+  //////// all checks before this line
+  if (d_node->getKind() == cvc5::Kind::CONST_FLOATINGPOINT)
+  {
+    const auto& fp = d_node->getConst<FloatingPoint>();
+    return fp.isZero() && fp.isPositive();
+  }
+  return false;
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+bool Term::isFloatingPointNegZero() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK_NOT_NULL;
+  //////// all checks before this line
+  if (d_node->getKind() == cvc5::Kind::CONST_FLOATINGPOINT)
+  {
+    const auto& fp = d_node->getConst<FloatingPoint>();
+    return fp.isZero() && fp.isNegative();
+  }
+  return false;
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+bool Term::isFloatingPointPosInf() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK_NOT_NULL;
+  //////// all checks before this line
+  if (d_node->getKind() == cvc5::Kind::CONST_FLOATINGPOINT)
+  {
+    const auto& fp = d_node->getConst<FloatingPoint>();
+    return fp.isInfinite() && fp.isPositive();
+  }
+  return false;
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+bool Term::isFloatingPointNegInf() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK_NOT_NULL;
+  //////// all checks before this line
+  if (d_node->getKind() == cvc5::Kind::CONST_FLOATINGPOINT)
+  {
+    const auto& fp = d_node->getConst<FloatingPoint>();
+    return fp.isInfinite() && fp.isNegative();
+  }
+  return false;
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+bool Term::isFloatingPointNaN() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK_NOT_NULL;
+  //////// all checks before this line
+  return d_node->getKind() == cvc5::Kind::CONST_FLOATINGPOINT
+         && d_node->getConst<FloatingPoint>().isNaN();
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+bool Term::isFloatingPointValue() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK_NOT_NULL;
+  //////// all checks before this line
+  return d_node->getKind() == cvc5::Kind::CONST_FLOATINGPOINT;
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+std::tuple<std::uint32_t, std::uint32_t, Term> Term::getFloatingPointValue()
+    const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK_NOT_NULL;
+  CVC5_API_ARG_CHECK_EXPECTED(
+      d_node->getKind() == cvc5::Kind::CONST_FLOATINGPOINT, *d_node)
+      << "Term to be a floating-point value when calling "
+         "getFloatingPointValue()";
+  //////// all checks before this line
+  const auto& fp = d_node->getConst<FloatingPoint>();
+  return std::make_tuple(fp.getSize().exponentWidth(),
+                         fp.getSize().significandWidth(),
+                         d_solver->mkValHelper<BitVector>(fp.pack()));
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+
+bool Term::isSetValue() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK_NOT_NULL;
+  //////// all checks before this line
+  return d_node->getType().isSet() && d_node->isConst();
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+
+void Term::collectSet(std::set<Term>& set,
+                      const cvc5::Node& node,
+                      const Solver* slv)
+{
+  // We asserted that node has a set type, and node.isConst()
+  // Thus, node only contains of EMPTYSET, UNION and SINGLETON.
+  switch (node.getKind())
+  {
+    case cvc5::Kind::EMPTYSET: break;
+    case cvc5::Kind::SINGLETON: set.emplace(Term(slv, node[0])); break;
+    case cvc5::Kind::UNION:
+    {
+      for (const auto& sub : node)
+      {
+        collectSet(set, sub, slv);
+      }
+      break;
+    }
+    default:
+      CVC5_API_ARG_CHECK_EXPECTED(false, node)
+          << "Term to be a set value when calling getSetValue()";
+      break;
+  }
+}
+
+std::set<Term> Term::getSetValue() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK_NOT_NULL;
+  CVC5_API_ARG_CHECK_EXPECTED(d_node->getType().isSet() && d_node->isConst(),
+                              *d_node)
+      << "Term to be a set value when calling getSetValue()";
+  //////// all checks before this line
+  std::set<Term> res;
+  Term::collectSet(res, *d_node, d_solver);
+  return res;
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+
+bool Term::isSequenceValue() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK_NOT_NULL;
+  //////// all checks before this line
+  return d_node->getKind() == cvc5::Kind::CONST_SEQUENCE;
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+std::vector<Term> Term::getSequenceValue() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK_NOT_NULL;
+  CVC5_API_ARG_CHECK_EXPECTED(d_node->getKind() == cvc5::Kind::CONST_SEQUENCE,
+                              *d_node)
+      << "Term to be a sequence value when calling getSequenceValue()";
+  //////// all checks before this line
+  std::vector<Term> res;
+  const Sequence& seq = d_node->getConst<Sequence>();
+  for (const auto& node: seq.getVec())
+  {
+    res.emplace_back(Term(d_solver, node));
+  }
+  return res;
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+
+bool Term::isUninterpretedValue() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK_NOT_NULL;
+  //////// all checks before this line
+  return d_node->getKind() == cvc5::Kind::UNINTERPRETED_CONSTANT;
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+std::pair<Sort, std::int32_t> Term::getUninterpretedValue() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK_NOT_NULL;
+  CVC5_API_ARG_CHECK_EXPECTED(
+      d_node->getKind() == cvc5::Kind::UNINTERPRETED_CONSTANT, *d_node)
+      << "Term to be an uninterpreted value when calling "
+         "getUninterpretedValue()";
+  //////// all checks before this line
+  const auto& uc = d_node->getConst<UninterpretedConstant>();
+  return std::make_pair(Sort(d_solver, uc.getType()),
+                        uc.getIndex().toUnsignedInt());
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+
 std::ostream& operator<<(std::ostream& out, const Term& t)
 {
   out << t.toString();
@@ -4445,21 +4860,6 @@ Term Solver::mkBVFromStrHelper(uint32_t size,
   return mkValHelper<cvc5::BitVector>(cvc5::BitVector(size, val));
 }
 
-Term Solver::mkCharFromStrHelper(const std::string& s) const
-{
-  CVC5_API_CHECK(s.find_first_not_of("0123456789abcdefABCDEF", 0)
-                     == std::string::npos
-                 && s.size() <= 5 && s.size() > 0)
-      << "Unexpected string for hexadecimal character " << s;
-  uint32_t val = static_cast<uint32_t>(std::stoul(s, 0, 16));
-  CVC5_API_CHECK(val < String::num_codes())
-      << "Not a valid code point for hexadecimal character " << s;
-  //////// all checks before this line
-  std::vector<unsigned> cpts;
-  cpts.push_back(val);
-  return mkValHelper<cvc5::String>(cvc5::String(cpts));
-}
-
 Term Solver::getValueHelper(const Term& term) const
 {
   // Note: Term is checked in the caller to avoid double checks
@@ -5296,17 +5696,7 @@ Term Solver::mkString(const std::string& s, bool useEscSequences) const
   CVC5_API_TRY_CATCH_END;
 }
 
-Term Solver::mkString(const unsigned char c) const
-{
-  NodeManagerScope scope(getNodeManager());
-  CVC5_API_TRY_CATCH_BEGIN;
-  //////// all checks before this line
-  return mkValHelper<cvc5::String>(cvc5::String(std::string(1, c)));
-  ////////
-  CVC5_API_TRY_CATCH_END;
-}
-
-Term Solver::mkString(const std::vector<uint32_t>& s) const
+Term Solver::mkString(const std::wstring& s) const
 {
   NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
@@ -5316,16 +5706,6 @@ Term Solver::mkString(const std::vector<uint32_t>& s) const
   CVC5_API_TRY_CATCH_END;
 }
 
-Term Solver::mkChar(const std::string& s) const
-{
-  NodeManagerScope scope(getNodeManager());
-  CVC5_API_TRY_CATCH_BEGIN;
-  //////// all checks before this line
-  return mkCharFromStrHelper(s);
-  ////////
-  CVC5_API_TRY_CATCH_END;
-}
-
 Term Solver::mkEmptySequence(const Sort& sort) const
 {
   NodeManagerScope scope(getNodeManager());
diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 16f58ee80..42d162e18 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -1054,13 +1054,6 @@ class CVC5_EXPORT Term
   bool isNull() const;
 
   /**
-   *  Return the base (element stored at all indices) of a constant array
-   *  throws an exception if the kind is not CONST_ARRAY
-   *  @return the base value
-   */
-  Term getConstArrayBase() const;
-
-  /**
    *  Return the elements of a constant sequence
    *  throws an exception if the kind is not CONST_SEQUENCE
    *  @return the elements of the constant sequence.
@@ -1213,63 +1206,215 @@ class CVC5_EXPORT Term
   const_iterator end() const;
 
   /**
-   * @return true if the term is an integer that fits within std::int32_t.
+   * @return true if the term is an integer value that fits within int32_t.
    */
-  bool isInt32() const;
+  bool isInt32Value() const;
   /**
-   * @return the stored integer as a std::int32_t.
-   * Note: Asserts isInt32().
+   * Asserts isInt32Value().
+   * @return the integer term as a int32_t.
    */
-  std::int32_t getInt32() const;
+  int32_t getInt32Value() const;
   /**
-   * @return true if the term is an integer that fits within std::uint32_t.
+   * @return true if the term is an integer value that fits within uint32_t.
    */
-  bool isUInt32() const;
+  bool isUInt32Value() const;
   /**
-   * @return the stored integer as a std::uint32_t.
-   * Note: Asserts isUInt32().
+   * Asserts isUInt32Value().
+   * @return the integer term as a uint32_t.
    */
-  std::uint32_t getUInt32() const;
+  uint32_t getUInt32Value() const;
   /**
-   * @return true if the term is an integer that fits within std::int64_t.
+   * @return true if the term is an integer value that fits within int64_t.
    */
-  bool isInt64() const;
+  bool isInt64Value() const;
   /**
-   * @return the stored integer as a std::int64_t.
-   * Note: Asserts isInt64().
+   * Asserts isInt64Value().
+   * @return the integer term as a int64_t.
    */
-  std::int64_t getInt64() const;
+  int64_t getInt64Value() const;
   /**
-   * @return true if the term is an integer that fits within std::uint64_t.
+   * @return true if the term is an integer value that fits within uint64_t.
    */
-  bool isUInt64() const;
+  bool isUInt64Value() const;
   /**
-   * @return the stored integer as a std::uint64_t.
-   * Note: Asserts isUInt64().
+   * Asserts isUInt64Value().
+   * @return the integer term as a uint64_t.
    */
-  std::uint64_t getUInt64() const;
+  uint64_t getUInt64Value() const;
   /**
-   * @return true if the term is an integer.
+   * @return true if the term is an integer value.
    */
-  bool isInteger() const;
+  bool isIntegerValue() const;
   /**
-   * @return the stored integer in (decimal) string representation.
-   * Note: Asserts isInteger().
+   * Asserts isIntegerValue().
+   * @return the integer term in (decimal) string representation.
    */
-  std::string getInteger() const;
+  std::string getIntegerValue() const;
 
   /**
-   * @return true if the term is a string constant.
+   * @return true if the term is a string value.
    */
-  bool isString() const;
+  bool isStringValue() const;
   /**
-   * @return the stored string constant.
-   *
-   * Note: This method is not to be confused with toString() which returns the
-   *       term in some string representation, whatever data it may hold.
-   *       Asserts isString().
+   * Note: This method is not to be confused with toString() which returns
+   * the term in some string representation, whatever data it may hold. Asserts
+   * isStringValue().
+   * @return the string term as a native string value.
+   */
+  std::wstring getStringValue() const;
+
+  /**
+   * @return true if the term is a rational value whose numerator and
+   * denominator fit within int32_t and uint32_t, respectively.
+   */
+  bool isReal32Value() const;
+  /**
+   * Asserts isReal32Value().
+   * @return the representation of a rational value as a pair of its numerator
+   * and denominator.
+   */
+  std::pair<int32_t, uint32_t> getReal32Value() const;
+  /**
+   * @return true if the term is a rational value whose numerator and
+   * denominator fit within int64_t and uint64_t, respectively.
    */
-  std::wstring getString() const;
+  bool isReal64Value() const;
+  /**
+   * Asserts isReal64Value().
+   * @return the representation of a rational value as a pair of its numerator
+   * and denominator.
+   */
+  std::pair<int64_t, uint64_t> getReal64Value() const;
+  /**
+   * @return true if the term is a rational value.
+   */
+  bool isRealValue() const;
+  /**
+   * Asserts isRealValue().
+   * @return the representation of a rational value as a (decimal) string.
+   */
+  std::string getRealValue() const;
+
+  /**
+   * @return true if the term is a constant array.
+   */
+  bool isConstArray() const;
+  /**
+   * Asserts isConstArray().
+   * @return the base (element stored at all indices) of a constant array
+   */
+  Term getConstArrayBase() const;
+
+  /**
+   * @return true if the term is a Boolean value.
+   */
+  bool isBooleanValue() const;
+  /**
+   * Asserts isBooleanValue().
+   * @return the representation of a Boolean value as a native Boolean value.
+   */
+  bool getBooleanValue() const;
+
+  /**
+   * @return true if the term is a bit-vector value.
+   */
+  bool isBitVectorValue() const;
+  /**
+   * Asserts isBitVectorValue().
+   * @return the representation of a bit-vector value in string representation.
+   * Supported bases are 2 (bit string), 10 (decimal string) or 16 (hexadecimal
+   * string).
+   */
+  std::string getBitVectorValue(uint32_t base = 2) const;
+
+  /**
+   * @return true if the term is an abstract value.
+   */
+  bool isAbstractValue() const;
+  /**
+   * Asserts isAbstractValue().
+   * @return the representation of an abstract value as a string.
+   */
+  std::string getAbstractValue() const;
+
+  /**
+   * @return true if the term is a tuple value.
+   */
+  bool isTupleValue() const;
+  /**
+   * Asserts isTupleValue().
+   * @return the representation of a tuple value as a vector of terms.
+   */
+  std::vector<Term> getTupleValue() const;
+
+  /**
+   * @return true if the term is the floating-point value for positive zero.
+   */
+  bool isFloatingPointPosZero() const;
+  /**
+   * @return true if the term is the floating-point value for negative zero.
+   */
+  bool isFloatingPointNegZero() const;
+  /**
+   * @return true if the term is the floating-point value for positive
+   * infinity.
+   */
+  bool isFloatingPointPosInf() const;
+  /**
+   * @return true if the term is the floating-point value for negative
+   * infinity.
+   */
+  bool isFloatingPointNegInf() const;
+  /**
+   * @return true if the term is the floating-point value for not a number.
+   */
+  bool isFloatingPointNaN() const;
+  /**
+   * @return true if the term is a floating-point value.
+   */
+  bool isFloatingPointValue() const;
+  /**
+   * Asserts isFloatingPointValue().
+   * @return the representation of a floating-point value as a tuple of the
+   * exponent width, the significand width and a bit-vector value.
+   */
+  std::tuple<uint32_t, uint32_t, Term> getFloatingPointValue() const;
+
+  /**
+   * @return true if the term is a set value.
+   */
+  bool isSetValue() const;
+  /**
+   * Asserts isSetValue().
+   * @return the representation of a set value as a set of terms.
+   */
+  std::set<Term> getSetValue() const;
+
+  /**
+   * @return true if the term is a sequence value.
+   */
+  bool isSequenceValue() const;
+  /**
+   * Asserts isSequenceValue().
+   * Note that it is usually necessary for sequences to call
+   * `Solver::simplify()` to turn a sequence that is constructed by, e.g.,
+   * concatenation of unit sequences, into a sequence value.
+   * @return the representation of a sequence value as a vector of terms.
+   */
+  std::vector<Term> getSequenceValue() const;
+
+  /**
+   * @return true if the term is a value from an uninterpreted sort.
+   */
+  bool isUninterpretedValue() const;
+  /**
+  bool @return() const;
+   * Asserts isUninterpretedValue().
+   * @return the representation of an uninterpreted value as a pair of its
+  sort and its
+   * index.
+   */
+  std::pair<Sort, int32_t> getUninterpretedValue() const;
 
  protected:
   /**
@@ -1281,6 +1426,15 @@ class CVC5_EXPORT Term
   /** Helper to convert a vector of Terms to internal Nodes. */
   std::vector<Node> static termVectorToNodes(const std::vector<Term>& terms);
 
+  /** Helper method to collect all elements of a set. */
+  static void collectSet(std::set<Term>& set,
+                         const cvc5::Node& node,
+                         const Solver* slv);
+  /** Helper method to collect all elements of a sequence. */
+  static void collectSequence(std::vector<Term>& seq,
+                              const cvc5::Node& node,
+                              const Solver* slv);
+
   /**
    * Constructor.
    * @param slv the associated solver object
@@ -3070,35 +3224,23 @@ class CVC5_EXPORT Solver
   Term mkSepNil(const Sort& sort) const;
 
   /**
-   * Create a String constant.
+   * Create a String constant from a `std::string` which may contain SMT-LIB
+   * compatible escape sequences like `\u1234` to encode unicode characters.
    * @param s the string this constant represents
-   * @param useEscSequences determines whether escape sequences in \p s should
-   * be converted to the corresponding character
+   * @param useEscSequences determines whether escape sequences in `s` should
+   * be converted to the corresponding unicode character
    * @return the String constant
    */
   Term mkString(const std::string& s, bool useEscSequences = false) const;
 
   /**
-   * Create a String constant.
-   * @param c the character this constant represents
-   * @return the String constant
-   */
-  Term mkString(const unsigned char c) const;
-
-  /**
-   * Create a String constant.
-   * @param s a list of unsigned (unicode) values this constant represents as
-   * string
+   * Create a String constant from a `std::wstring`.
+   * This method does not support escape sequences as `std::wstring` already
+   * supports unicode characters.
+   * @param s the string this constant represents
    * @return the String constant
    */
-  Term mkString(const std::vector<uint32_t>& s) const;
-
-  /**
-   * Create a character constant from a given string.
-   * @param s the string denoting the code point of the character (in base 16)
-   * @return the character constant
-   */
-  Term mkChar(const std::string& s) const;
+  Term mkString(const std::wstring& s) const;
 
   /**
    * Create an empty sequence of the given element sort.
@@ -3216,12 +3358,14 @@ class CVC5_EXPORT Solver
 
   /**
    * Create an abstract value constant.
+   * The given index needs to be a positive integer in base 10.
    * @param index Index of the abstract value
    */
   Term mkAbstractValue(const std::string& index) const;
 
   /**
    * Create an abstract value constant.
+   * The given index needs to be positive.
    * @param index Index of the abstract value
    */
   Term mkAbstractValue(uint64_t index) const;
diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index a044c79f5..24f8ac0a0 100644
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -1,6 +1,7 @@
 # import dereference and increment operators
 from cython.operator cimport dereference as deref, preincrement as inc
 from libc.stdint cimport int32_t, int64_t, uint32_t, uint64_t
+from libc.stddef cimport wchar_t
 from libcpp.set cimport set
 from libcpp.string cimport string
 from libcpp.vector cimport vector
@@ -19,6 +20,9 @@ cdef extern from "<functional>" namespace "std" nogil:
         hash()
         size_t operator()(T t)
 
+cdef extern from "<string>" namespace "std":
+    cdef cppclass wstring:
+        wstring(const wchar_t*, size_t) except +
 
 cdef extern from "api/cpp/cvc5.h" namespace "cvc5":
     cdef cppclass Options:
@@ -191,7 +195,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         Term mkEmptySet(Sort s) except +
         Term mkSepNil(Sort sort) except +
         Term mkString(const string& s) except +
-        Term mkString(const vector[unsigned]& s) except +
+        Term mkString(const wstring& s) except +
         Term mkEmptySequence(Sort sort) except +
         Term mkUniverseSet(Sort sort) except +
         Term mkBitVector(uint32_t size) except +
@@ -372,7 +376,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
             Term operator*() except +
         const_iterator begin() except +
         const_iterator end() except +
-        bint isInteger() except +
+        bint isIntegerValue() except +
 
     cdef cppclass TermHashFunction:
         TermHashFunction() except +
diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index a512a17a8..6d197168d 100644
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -3,6 +3,7 @@ from fractions import Fraction
 import sys
 
 from libc.stdint cimport int32_t, int64_t, uint32_t, uint64_t
+from libc.stddef cimport wchar_t
 
 from libcpp.pair cimport pair
 from libcpp.set cimport set
@@ -26,9 +27,14 @@ from cvc5 cimport ROUND_TOWARD_NEGATIVE, ROUND_TOWARD_ZERO
 from cvc5 cimport ROUND_NEAREST_TIES_TO_AWAY
 from cvc5 cimport Term as c_Term
 from cvc5 cimport hash as c_hash
+from cvc5 cimport wstring as c_wstring
 
 from cvc5kinds cimport Kind as c_Kind
 
+cdef extern from "Python.h":
+    wchar_t* PyUnicode_AsWideCharString(object, Py_ssize_t *)
+    void PyMem_Free(void*)
+
 ################################## DECORATORS #################################
 def expand_list_arg(num_req_args=0):
     '''
@@ -735,23 +741,12 @@ cdef class Solver:
         term.cterm = self.csolver.mkSepNil(sort.csort)
         return term
 
-    def mkString(self, str_or_vec):
+    def mkString(self, str s):
         cdef Term term = Term(self)
-        cdef vector[unsigned] v
-        if isinstance(str_or_vec, str):
-            for u in str_or_vec:
-                v.push_back(<unsigned> ord(u))
-            term.cterm = self.csolver.mkString(<const vector[unsigned]&> v)
-        elif isinstance(str_or_vec, list):
-            for u in str_or_vec:
-                if not isinstance(u, int):
-                    raise ValueError("List should contain ints but got: {}"
-                                     .format(str_or_vec))
-                v.push_back(<unsigned> u)
-            term.cterm = self.csolver.mkString(<const vector[unsigned]&> v)
-        else:
-            raise ValueError("Expected string or vector of ASCII codes"
-                             " but got: {}".format(str_or_vec))
+        cdef Py_ssize_t size
+        cdef wchar_t* tmp = PyUnicode_AsWideCharString(s, &size)
+        term.cterm = self.csolver.mkString(c_wstring(tmp, size))
+        PyMem_Free(tmp)
         return term
 
     def mkEmptySequence(self, Sort sort):
@@ -1599,7 +1594,7 @@ cdef class Term:
         return term
 
     def isInteger(self):
-        return self.cterm.isInteger()
+        return self.cterm.isIntegerValue()
     
     def toPythonObj(self):
         '''
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index f3a0d5c83..d57ec0c9a 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -741,7 +741,7 @@ void Parser::reset() {}
 
 SymbolManager* Parser::getSymbolManager() { return d_symman; }
 
-std::vector<unsigned> Parser::processAdHocStringEsc(const std::string& s)
+std::wstring Parser::processAdHocStringEsc(const std::string& s)
 {
   std::wstring ws;
   {
@@ -763,7 +763,7 @@ std::vector<unsigned> Parser::processAdHocStringEsc(const std::string& s)
     }
   }
 
-  std::vector<unsigned> str;
+  std::wstring res;
   unsigned i = 0;
   while (i < ws.size())
   {
@@ -771,7 +771,7 @@ std::vector<unsigned> Parser::processAdHocStringEsc(const std::string& s)
     if (ws[i] != '\\')
     {
       // don't worry about printable here
-      str.push_back(static_cast<unsigned>(ws[i]));
+      res.push_back(ws[i]);
       ++i;
       continue;
     }
@@ -789,49 +789,49 @@ std::vector<unsigned> Parser::processAdHocStringEsc(const std::string& s)
     {
       case 'n':
       {
-        str.push_back(static_cast<unsigned>('\n'));
+        res.push_back('\n');
         i++;
       }
       break;
       case 't':
       {
-        str.push_back(static_cast<unsigned>('\t'));
+        res.push_back('\t');
         i++;
       }
       break;
       case 'v':
       {
-        str.push_back(static_cast<unsigned>('\v'));
+        res.push_back('\v');
         i++;
       }
       break;
       case 'b':
       {
-        str.push_back(static_cast<unsigned>('\b'));
+        res.push_back('\b');
         i++;
       }
       break;
       case 'r':
       {
-        str.push_back(static_cast<unsigned>('\r'));
+        res.push_back('\r');
         i++;
       }
       break;
       case 'f':
       {
-        str.push_back(static_cast<unsigned>('\f'));
+        res.push_back('\f');
         i++;
       }
       break;
       case 'a':
       {
-        str.push_back(static_cast<unsigned>('\a'));
+        res.push_back('\a');
         i++;
       }
       break;
       case '\\':
       {
-        str.push_back(static_cast<unsigned>('\\'));
+        res.push_back('\\');
         i++;
       }
       break;
@@ -846,7 +846,7 @@ std::vector<unsigned> Parser::processAdHocStringEsc(const std::string& s)
             shex << ws[i + 1] << ws[i + 2];
             unsigned val;
             shex >> std::hex >> val;
-            str.push_back(val);
+            res.push_back(val);
             i += 3;
             isValid = true;
           }
@@ -875,25 +875,25 @@ std::vector<unsigned> Parser::processAdHocStringEsc(const std::string& s)
                 && ws[i + 2] < '8')
             {
               num = num * 8 + static_cast<unsigned>(ws[i + 2]) - 48;
-              str.push_back(num);
+              res.push_back(num);
               i += 3;
             }
             else
             {
-              str.push_back(num);
+              res.push_back(num);
               i += 2;
             }
           }
           else
           {
-            str.push_back(num);
+            res.push_back(num);
             i++;
           }
         }
       }
     }
   }
-  return str;
+  return res;
 }
 
 api::Term Parser::mkStringConstant(const std::string& s)
@@ -903,9 +903,18 @@ api::Term Parser::mkStringConstant(const std::string& s)
     return d_solver->mkString(s, true);
   }
   // otherwise, we must process ad-hoc escape sequences
-  std::vector<unsigned> str = processAdHocStringEsc(s);
+  std::wstring str = processAdHocStringEsc(s);
   return d_solver->mkString(str);
 }
 
+api::Term Parser::mkCharConstant(const std::string& s)
+{
+  Assert(s.find_first_not_of("0123456789abcdefABCDEF", 0) == std::string::npos
+         && s.size() <= 5 && s.size() > 0)
+      << "Unexpected string for hexadecimal character " << s;
+  wchar_t val = static_cast<wchar_t>(std::stoul(s, 0, 16));
+  return d_solver->mkString(std::wstring(1, val));
+}
+
 }  // namespace parser
 }  // namespace cvc5
diff --git a/src/parser/parser.h b/src/parser/parser.h
index b127221d7..8add1c698 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -757,6 +757,14 @@ public:
    */
   api::Term mkStringConstant(const std::string& s);
 
+  /**
+   * Make string constant from a single character in hex representation
+   *
+   * This makes the string constant based on the character from the strings,
+   * represented as a hexadecimal code point.
+   */
+  api::Term mkCharConstant(const std::string& s);
+
   /** ad-hoc string escaping
    *
    * Returns the (internal) vector of code points corresponding to processing
@@ -767,7 +775,7 @@ public:
    * \\, \x[N] and octal escape sequences of the form \[c1]([c2]([c3])?)? where
    * c1, c2, c3 are digits from 0 to 7.
    */
-  std::vector<unsigned> processAdHocStringEsc(const std::string& s);
+  std::wstring processAdHocStringEsc(const std::string& s);
 }; /* class Parser */
 
 }  // namespace parser
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 58f229cfe..483da3ff0 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1726,7 +1726,7 @@ termAtomic[cvc5::api::Term& atomTerm]
     | CHAR_TOK HEX_LITERAL 
       {
         std::string hexStr = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2);
-        atomTerm = SOLVER->mkChar(hexStr);
+        atomTerm = PARSER_STATE->mkCharConstant(hexStr);
       }
     | sym=SIMPLE_SYMBOL nonemptyNumeralList[numerals]
       {
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 7893dd333..c22b95af2 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -1046,11 +1046,11 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
   else if (p.d_kind == api::APPLY_SELECTOR && !p.d_expr.isNull())
   {
     // tuple selector case
-    if (!p.d_expr.isUInt64())
+    if (!p.d_expr.isUInt64Value())
     {
       parseError("index of tupSel is larger than size of uint64_t");
     }
-    uint64_t n = p.d_expr.getUInt64();
+    uint64_t n = p.d_expr.getUInt64Value();
     if (args.size() != 1)
     {
       parseError("tupSel should only be applied to one tuple argument");
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index e49658c9d..e4e8aff1a 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -51,10 +51,10 @@ std::string sexprToString(api::Term sexpr)
   // call Term::toString as its result depends on the output language.
   // Notice that we only check for string constants. The sexprs generated by the
   // parser don't contains other constants, so we can ignore them.
-  if (sexpr.isString())
+  if (sexpr.isStringValue())
   {
     // convert std::wstring to std::string
-    std::wstring wstring = sexpr.getString();
+    std::wstring wstring = sexpr.getStringValue();
     return std::string(wstring.cbegin(), wstring.cend());
   }
 
diff --git a/src/util/string.cpp b/src/util/string.cpp
index 5f2bd5b83..50b0a7199 100644
--- a/src/util/string.cpp
+++ b/src/util/string.cpp
@@ -30,6 +30,15 @@ namespace cvc5 {
 
 static_assert(UCHAR_MAX == 255, "Unsigned char is assumed to have 256 values.");
 
+String::String(const std::wstring& s)
+{
+  d_str.resize(s.size());
+  for (size_t i = 0, n = s.size(); i < n; ++i)
+  {
+    d_str[i] = static_cast<unsigned>(s[i]);
+  }
+}
+
 String::String(const std::vector<unsigned> &s) : d_str(s)
 {
 #ifdef CVC5_ASSERTIONS
diff --git a/src/util/string.h b/src/util/string.h
index 6e9bb2866..3f6384082 100644
--- a/src/util/string.h
+++ b/src/util/string.h
@@ -69,6 +69,7 @@ class String
       : d_str(toInternal(s, useEscSequences))
   {
   }
+  explicit String(const std::wstring& s);
   explicit String(const char* s, bool useEscSequences = false)
       : d_str(toInternal(std::string(s), useEscSequences))
   {
diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp
index f7e6a3783..bc8f3ed74 100644
--- a/test/unit/api/solver_black.cpp
+++ b/test/unit/api/solver_black.cpp
@@ -684,16 +684,6 @@ TEST_F(TestApiBlackSolver, mkString)
             "\"asdf\\u{5c}nasdf\"");
 }
 
-TEST_F(TestApiBlackSolver, mkChar)
-{
-  ASSERT_NO_THROW(d_solver.mkChar(std::string("0123")));
-  ASSERT_NO_THROW(d_solver.mkChar("aA"));
-  ASSERT_THROW(d_solver.mkChar(""), CVC5ApiException);
-  ASSERT_THROW(d_solver.mkChar("0g0"), CVC5ApiException);
-  ASSERT_THROW(d_solver.mkChar("100000"), CVC5ApiException);
-  ASSERT_EQ(d_solver.mkChar("abc"), d_solver.mkChar("ABC"));
-}
-
 TEST_F(TestApiBlackSolver, mkTerm)
 {
   Sort bv32 = d_solver.mkBitVectorSort(32);
diff --git a/test/unit/api/term_black.cpp b/test/unit/api/term_black.cpp
index 9dd803c93..50ef8bf0f 100644
--- a/test/unit/api/term_black.cpp
+++ b/test/unit/api/term_black.cpp
@@ -689,64 +689,318 @@ TEST_F(TestApiBlackTerm, getInteger)
   ASSERT_THROW(d_solver.mkInteger("-01"), CVC5ApiException);
   ASSERT_THROW(d_solver.mkInteger("-00"), CVC5ApiException);
 
-  ASSERT_TRUE(!int1.isInt32() && !int1.isUInt32() && !int1.isInt64()
-              && !int1.isUInt64() && int1.isInteger());
-  ASSERT_EQ(int1.getInteger(), "-18446744073709551616");
-  ASSERT_TRUE(!int2.isInt32() && !int2.isUInt32() && !int2.isInt64()
-              && !int2.isUInt64() && int2.isInteger());
-  ASSERT_EQ(int2.getInteger(), "-18446744073709551615");
-  ASSERT_TRUE(!int3.isInt32() && !int3.isUInt32() && int3.isInt64()
-              && !int3.isUInt64() && int3.isInteger());
-  ASSERT_EQ(int3.getInt64(), -4294967296);
-  ASSERT_EQ(int3.getInteger(), "-4294967296");
-  ASSERT_TRUE(!int4.isInt32() && !int4.isUInt32() && int4.isInt64()
-              && !int4.isUInt64() && int4.isInteger());
-  ASSERT_EQ(int4.getInt64(), -4294967295);
-  ASSERT_EQ(int4.getInteger(), "-4294967295");
-  ASSERT_TRUE(int5.isInt32() && !int5.isUInt32() && int5.isInt64()
-              && !int5.isUInt64() && int5.isInteger());
-  ASSERT_EQ(int5.getInt32(), -10);
-  ASSERT_EQ(int5.getInt64(), -10);
-  ASSERT_EQ(int5.getInteger(), "-10");
-  ASSERT_TRUE(int6.isInt32() && int6.isUInt32() && int6.isInt64()
-              && int6.isUInt64() && int6.isInteger());
-  ASSERT_EQ(int6.getInt32(), 0);
-  ASSERT_EQ(int6.getUInt32(), 0);
-  ASSERT_EQ(int6.getInt64(), 0);
-  ASSERT_EQ(int6.getUInt64(), 0);
-  ASSERT_EQ(int6.getInteger(), "0");
-  ASSERT_TRUE(int7.isInt32() && int7.isUInt32() && int7.isInt64()
-              && int7.isUInt64() && int7.isInteger());
-  ASSERT_EQ(int7.getInt32(), 10);
-  ASSERT_EQ(int7.getUInt32(), 10);
-  ASSERT_EQ(int7.getInt64(), 10);
-  ASSERT_EQ(int7.getUInt64(), 10);
-  ASSERT_EQ(int7.getInteger(), "10");
-  ASSERT_TRUE(!int8.isInt32() && int8.isUInt32() && int8.isInt64()
-              && int8.isUInt64() && int8.isInteger());
-  ASSERT_EQ(int8.getUInt32(), 4294967295);
-  ASSERT_EQ(int8.getInt64(), 4294967295);
-  ASSERT_EQ(int8.getUInt64(), 4294967295);
-  ASSERT_EQ(int8.getInteger(), "4294967295");
-  ASSERT_TRUE(!int9.isInt32() && !int9.isUInt32() && int9.isInt64()
-              && int9.isUInt64() && int9.isInteger());
-  ASSERT_EQ(int9.getInt64(), 4294967296);
-  ASSERT_EQ(int9.getUInt64(), 4294967296);
-  ASSERT_EQ(int9.getInteger(), "4294967296");
-  ASSERT_TRUE(!int10.isInt32() && !int10.isUInt32() && !int10.isInt64()
-              && int10.isUInt64() && int10.isInteger());
-  ASSERT_EQ(int10.getUInt64(), 18446744073709551615ull);
-  ASSERT_EQ(int10.getInteger(), "18446744073709551615");
-  ASSERT_TRUE(!int11.isInt32() && !int11.isUInt32() && !int11.isInt64()
-              && !int11.isUInt64() && int11.isInteger());
-  ASSERT_EQ(int11.getInteger(), "18446744073709551616");
+  ASSERT_TRUE(!int1.isInt32Value() && !int1.isUInt32Value()
+              && !int1.isInt64Value() && !int1.isUInt64Value()
+              && int1.isIntegerValue());
+  ASSERT_EQ(int1.getIntegerValue(), "-18446744073709551616");
+  ASSERT_TRUE(!int2.isInt32Value() && !int2.isUInt32Value()
+              && !int2.isInt64Value() && !int2.isUInt64Value()
+              && int2.isIntegerValue());
+  ASSERT_EQ(int2.getIntegerValue(), "-18446744073709551615");
+  ASSERT_TRUE(!int3.isInt32Value() && !int3.isUInt32Value()
+              && int3.isInt64Value() && !int3.isUInt64Value()
+              && int3.isIntegerValue());
+  ASSERT_EQ(int3.getInt64Value(), -4294967296);
+  ASSERT_EQ(int3.getIntegerValue(), "-4294967296");
+  ASSERT_TRUE(!int4.isInt32Value() && !int4.isUInt32Value()
+              && int4.isInt64Value() && !int4.isUInt64Value()
+              && int4.isIntegerValue());
+  ASSERT_EQ(int4.getInt64Value(), -4294967295);
+  ASSERT_EQ(int4.getIntegerValue(), "-4294967295");
+  ASSERT_TRUE(int5.isInt32Value() && !int5.isUInt32Value()
+              && int5.isInt64Value() && !int5.isUInt64Value()
+              && int5.isIntegerValue());
+  ASSERT_EQ(int5.getInt32Value(), -10);
+  ASSERT_EQ(int5.getInt64Value(), -10);
+  ASSERT_EQ(int5.getIntegerValue(), "-10");
+  ASSERT_TRUE(int6.isInt32Value() && int6.isUInt32Value() && int6.isInt64Value()
+              && int6.isUInt64Value() && int6.isIntegerValue());
+  ASSERT_EQ(int6.getInt32Value(), 0);
+  ASSERT_EQ(int6.getUInt32Value(), 0);
+  ASSERT_EQ(int6.getInt64Value(), 0);
+  ASSERT_EQ(int6.getUInt64Value(), 0);
+  ASSERT_EQ(int6.getIntegerValue(), "0");
+  ASSERT_TRUE(int7.isInt32Value() && int7.isUInt32Value() && int7.isInt64Value()
+              && int7.isUInt64Value() && int7.isIntegerValue());
+  ASSERT_EQ(int7.getInt32Value(), 10);
+  ASSERT_EQ(int7.getUInt32Value(), 10);
+  ASSERT_EQ(int7.getInt64Value(), 10);
+  ASSERT_EQ(int7.getUInt64Value(), 10);
+  ASSERT_EQ(int7.getIntegerValue(), "10");
+  ASSERT_TRUE(!int8.isInt32Value() && int8.isUInt32Value()
+              && int8.isInt64Value() && int8.isUInt64Value()
+              && int8.isIntegerValue());
+  ASSERT_EQ(int8.getUInt32Value(), 4294967295);
+  ASSERT_EQ(int8.getInt64Value(), 4294967295);
+  ASSERT_EQ(int8.getUInt64Value(), 4294967295);
+  ASSERT_EQ(int8.getIntegerValue(), "4294967295");
+  ASSERT_TRUE(!int9.isInt32Value() && !int9.isUInt32Value()
+              && int9.isInt64Value() && int9.isUInt64Value()
+              && int9.isIntegerValue());
+  ASSERT_EQ(int9.getInt64Value(), 4294967296);
+  ASSERT_EQ(int9.getUInt64Value(), 4294967296);
+  ASSERT_EQ(int9.getIntegerValue(), "4294967296");
+  ASSERT_TRUE(!int10.isInt32Value() && !int10.isUInt32Value()
+              && !int10.isInt64Value() && int10.isUInt64Value()
+              && int10.isIntegerValue());
+  ASSERT_EQ(int10.getUInt64Value(), 18446744073709551615ull);
+  ASSERT_EQ(int10.getIntegerValue(), "18446744073709551615");
+  ASSERT_TRUE(!int11.isInt32Value() && !int11.isUInt32Value()
+              && !int11.isInt64Value() && !int11.isUInt64Value()
+              && int11.isIntegerValue());
+  ASSERT_EQ(int11.getIntegerValue(), "18446744073709551616");
 }
 
 TEST_F(TestApiBlackTerm, getString)
 {
   Term s1 = d_solver.mkString("abcde");
-  ASSERT_TRUE(s1.isString());
-  ASSERT_EQ(s1.getString(), L"abcde");
+  ASSERT_TRUE(s1.isStringValue());
+  ASSERT_EQ(s1.getStringValue(), L"abcde");
+}
+
+TEST_F(TestApiBlackTerm, getReal)
+{
+  Term real1 = d_solver.mkReal("0");
+  Term real2 = d_solver.mkReal(".0");
+  Term real3 = d_solver.mkReal("-17");
+  Term real4 = d_solver.mkReal("-3/5");
+  Term real5 = d_solver.mkReal("12.7");
+  Term real6 = d_solver.mkReal("1/4294967297");
+  Term real7 = d_solver.mkReal("4294967297");
+  Term real8 = d_solver.mkReal("1/18446744073709551617");
+  Term real9 = d_solver.mkReal("18446744073709551617");
+
+  ASSERT_TRUE(real1.isRealValue() && real1.isReal64Value()
+              && real1.isReal32Value());
+  ASSERT_TRUE(real2.isRealValue() && real2.isReal64Value()
+              && real2.isReal32Value());
+  ASSERT_TRUE(real3.isRealValue() && real3.isReal64Value()
+              && real3.isReal32Value());
+  ASSERT_TRUE(real4.isRealValue() && real4.isReal64Value()
+              && real4.isReal32Value());
+  ASSERT_TRUE(real5.isRealValue() && real5.isReal64Value()
+              && real5.isReal32Value());
+  ASSERT_TRUE(real6.isRealValue() && real6.isReal64Value());
+  ASSERT_TRUE(real7.isRealValue() && real7.isReal64Value());
+  ASSERT_TRUE(real8.isRealValue());
+  ASSERT_TRUE(real9.isRealValue());
+
+  ASSERT_EQ(std::make_pair(0, 1u), real1.getReal32Value());
+  ASSERT_EQ(std::make_pair(0l, 1ul), real1.getReal64Value());
+  ASSERT_EQ("0", real1.getRealValue());
+
+  ASSERT_EQ(std::make_pair(0, 1u), real2.getReal32Value());
+  ASSERT_EQ(std::make_pair(0l, 1ul), real2.getReal64Value());
+  ASSERT_EQ("0", real2.getRealValue());
+
+  ASSERT_EQ(std::make_pair(-17, 1u), real3.getReal32Value());
+  ASSERT_EQ(std::make_pair(-17l, 1ul), real3.getReal64Value());
+  ASSERT_EQ("-17", real3.getRealValue());
+
+  ASSERT_EQ(std::make_pair(-3, 5u), real4.getReal32Value());
+  ASSERT_EQ(std::make_pair(-3l, 5ul), real4.getReal64Value());
+  ASSERT_EQ("-3/5", real4.getRealValue());
+
+  ASSERT_EQ(std::make_pair(127, 10u), real5.getReal32Value());
+  ASSERT_EQ(std::make_pair(127l, 10ul), real5.getReal64Value());
+  ASSERT_EQ("127/10", real5.getRealValue());
+
+  ASSERT_EQ(std::make_pair(1l, 4294967297ul), real6.getReal64Value());
+  ASSERT_EQ("1/4294967297", real6.getRealValue());
+
+  ASSERT_EQ(std::make_pair(4294967297l, 1ul), real7.getReal64Value());
+  ASSERT_EQ("4294967297", real7.getRealValue());
+
+  ASSERT_EQ("1/18446744073709551617", real8.getRealValue());
+
+  ASSERT_EQ("18446744073709551617", real9.getRealValue());
+}
+
+TEST_F(TestApiBlackTerm, getConstArrayBase)
+{
+  Sort intsort = d_solver.getIntegerSort();
+  Sort arrsort = d_solver.mkArraySort(intsort, intsort);
+  Term one = d_solver.mkInteger(1);
+  Term constarr = d_solver.mkConstArray(arrsort, one);
+
+  ASSERT_TRUE(constarr.isConstArray());
+  ASSERT_EQ(one, constarr.getConstArrayBase());
+}
+
+TEST_F(TestApiBlackTerm, getBoolean)
+{
+  Term b1 = d_solver.mkBoolean(true);
+  Term b2 = d_solver.mkBoolean(false);
+
+  ASSERT_TRUE(b1.isBooleanValue());
+  ASSERT_TRUE(b2.isBooleanValue());
+  ASSERT_TRUE(b1.getBooleanValue());
+  ASSERT_FALSE(b2.getBooleanValue());
+}
+
+TEST_F(TestApiBlackTerm, getBitVector)
+{
+  Term b1 = d_solver.mkBitVector(8, 15);
+  Term b2 = d_solver.mkBitVector("00001111", 2);
+  Term b3 = d_solver.mkBitVector("15", 10);
+  Term b4 = d_solver.mkBitVector("0f", 16);
+  Term b5 = d_solver.mkBitVector(8, "00001111", 2);
+  Term b6 = d_solver.mkBitVector(8, "15", 10);
+  Term b7 = d_solver.mkBitVector(8, "0f", 16);
+
+  ASSERT_TRUE(b1.isBitVectorValue());
+  ASSERT_TRUE(b2.isBitVectorValue());
+  ASSERT_TRUE(b3.isBitVectorValue());
+  ASSERT_TRUE(b4.isBitVectorValue());
+  ASSERT_TRUE(b5.isBitVectorValue());
+  ASSERT_TRUE(b6.isBitVectorValue());
+  ASSERT_TRUE(b7.isBitVectorValue());
+
+  ASSERT_EQ("00001111", b1.getBitVectorValue(2));
+  ASSERT_EQ("15", b1.getBitVectorValue(10));
+  ASSERT_EQ("f", b1.getBitVectorValue(16));
+  ASSERT_EQ("00001111", b2.getBitVectorValue(2));
+  ASSERT_EQ("15", b2.getBitVectorValue(10));
+  ASSERT_EQ("f", b2.getBitVectorValue(16));
+  ASSERT_EQ("1111", b3.getBitVectorValue(2));
+  ASSERT_EQ("15", b3.getBitVectorValue(10));
+  ASSERT_EQ("f", b3.getBitVectorValue(16));
+  ASSERT_EQ("00001111", b4.getBitVectorValue(2));
+  ASSERT_EQ("15", b4.getBitVectorValue(10));
+  ASSERT_EQ("f", b4.getBitVectorValue(16));
+  ASSERT_EQ("00001111", b5.getBitVectorValue(2));
+  ASSERT_EQ("15", b5.getBitVectorValue(10));
+  ASSERT_EQ("f", b5.getBitVectorValue(16));
+  ASSERT_EQ("00001111", b6.getBitVectorValue(2));
+  ASSERT_EQ("15", b6.getBitVectorValue(10));
+  ASSERT_EQ("f", b6.getBitVectorValue(16));
+  ASSERT_EQ("00001111", b7.getBitVectorValue(2));
+  ASSERT_EQ("15", b7.getBitVectorValue(10));
+  ASSERT_EQ("f", b7.getBitVectorValue(16));
+}
+
+TEST_F(TestApiBlackTerm, getAbstractValue)
+{
+  Term v1 = d_solver.mkAbstractValue(1);
+  Term v2 = d_solver.mkAbstractValue("15");
+  Term v3 = d_solver.mkAbstractValue("18446744073709551617");
+
+  ASSERT_TRUE(v1.isAbstractValue());
+  ASSERT_TRUE(v2.isAbstractValue());
+  ASSERT_TRUE(v3.isAbstractValue());
+  ASSERT_EQ("1", v1.getAbstractValue());
+  ASSERT_EQ("15", v2.getAbstractValue());
+  ASSERT_EQ("18446744073709551617", v3.getAbstractValue());
+}
+
+TEST_F(TestApiBlackTerm, getTuple)
+{
+  Sort s1 = d_solver.getIntegerSort();
+  Sort s2 = d_solver.getRealSort();
+  Sort s3 = d_solver.getStringSort();
+
+  Term t1 = d_solver.mkInteger(15);
+  Term t2 = d_solver.mkReal(17, 25);
+  Term t3 = d_solver.mkString("abc");
+
+  Term tup = d_solver.mkTuple({s1, s2, s3}, {t1, t2, t3});
+
+  ASSERT_TRUE(tup.isTupleValue());
+  ASSERT_EQ(std::vector<Term>({t1, t2, t3}), tup.getTupleValue());
+}
+
+TEST_F(TestApiBlackTerm, getFloatingPoint)
+{
+  Term bvval = d_solver.mkBitVector("0000110000000011");
+  Term fp = d_solver.mkFloatingPoint(5, 11, bvval);
+
+  ASSERT_TRUE(fp.isFloatingPointValue());
+  ASSERT_FALSE(fp.isFloatingPointPosZero());
+  ASSERT_FALSE(fp.isFloatingPointNegZero());
+  ASSERT_FALSE(fp.isFloatingPointPosInf());
+  ASSERT_FALSE(fp.isFloatingPointNegInf());
+  ASSERT_FALSE(fp.isFloatingPointNaN());
+  ASSERT_EQ(std::make_tuple(5u, 11u, bvval), fp.getFloatingPointValue());
+
+  ASSERT_TRUE(d_solver.mkPosZero(5, 11).isFloatingPointPosZero());
+  ASSERT_TRUE(d_solver.mkNegZero(5, 11).isFloatingPointNegZero());
+  ASSERT_TRUE(d_solver.mkPosInf(5, 11).isFloatingPointPosInf());
+  ASSERT_TRUE(d_solver.mkNegInf(5, 11).isFloatingPointNegInf());
+  ASSERT_TRUE(d_solver.mkNaN(5, 11).isFloatingPointNaN());
+}
+
+TEST_F(TestApiBlackTerm, getSet)
+{
+  Sort s = d_solver.mkSetSort(d_solver.getIntegerSort());
+
+  Term i1 = d_solver.mkInteger(5);
+  Term i2 = d_solver.mkInteger(7);
+
+  Term s1 = d_solver.mkEmptySet(s);
+  Term s2 = d_solver.mkTerm(Kind::SINGLETON, i1);
+  Term s3 = d_solver.mkTerm(Kind::SINGLETON, i1);
+  Term s4 = d_solver.mkTerm(Kind::SINGLETON, i2);
+  Term s5 =
+      d_solver.mkTerm(Kind::UNION, s2, d_solver.mkTerm(Kind::UNION, s3, s4));
+
+  ASSERT_TRUE(s1.isSetValue());
+  ASSERT_TRUE(s2.isSetValue());
+  ASSERT_TRUE(s3.isSetValue());
+  ASSERT_TRUE(s4.isSetValue());
+  ASSERT_FALSE(s5.isSetValue());
+  s5 = d_solver.simplify(s5);
+  ASSERT_TRUE(s5.isSetValue());
+
+  ASSERT_EQ(std::set<Term>({}), s1.getSetValue());
+  ASSERT_EQ(std::set<Term>({i1}), s2.getSetValue());
+  ASSERT_EQ(std::set<Term>({i1}), s3.getSetValue());
+  ASSERT_EQ(std::set<Term>({i2}), s4.getSetValue());
+  ASSERT_EQ(std::set<Term>({i1, i2}), s5.getSetValue());
+}
+
+TEST_F(TestApiBlackTerm, getSequence)
+{
+  Sort s = d_solver.mkSequenceSort(d_solver.getIntegerSort());
+
+  Term i1 = d_solver.mkInteger(5);
+  Term i2 = d_solver.mkInteger(7);
+
+  Term s1 = d_solver.mkEmptySequence(s);
+  Term s2 = d_solver.mkTerm(Kind::SEQ_UNIT, i1);
+  Term s3 = d_solver.mkTerm(Kind::SEQ_UNIT, i1);
+  Term s4 = d_solver.mkTerm(Kind::SEQ_UNIT, i2);
+  Term s5 = d_solver.mkTerm(
+      Kind::SEQ_CONCAT, s2, d_solver.mkTerm(Kind::SEQ_CONCAT, s3, s4));
+
+  ASSERT_TRUE(s1.isSequenceValue());
+  ASSERT_TRUE(!s2.isSequenceValue());
+  ASSERT_TRUE(!s3.isSequenceValue());
+  ASSERT_TRUE(!s4.isSequenceValue());
+  ASSERT_TRUE(!s5.isSequenceValue());
+
+  s2 = d_solver.simplify(s2);
+  s3 = d_solver.simplify(s3);
+  s4 = d_solver.simplify(s4);
+  s5 = d_solver.simplify(s5);
+
+  ASSERT_EQ(std::vector<Term>({}), s1.getSequenceValue());
+  ASSERT_EQ(std::vector<Term>({i1}), s2.getSequenceValue());
+  ASSERT_EQ(std::vector<Term>({i1}), s3.getSequenceValue());
+  ASSERT_EQ(std::vector<Term>({i2}), s4.getSequenceValue());
+  ASSERT_EQ(std::vector<Term>({i1, i1, i2}), s5.getSequenceValue());
+}
+
+TEST_F(TestApiBlackTerm, getUninterpretedConst)
+{
+  Sort s = d_solver.mkUninterpretedSort("test");
+  Term t1 = d_solver.mkUninterpretedConst(s, 3);
+  Term t2 = d_solver.mkUninterpretedConst(s, 5);
+
+  ASSERT_TRUE(t1.isUninterpretedValue());
+  ASSERT_TRUE(t2.isUninterpretedValue());
+
+  ASSERT_EQ(std::make_pair(s, 3), t1.getUninterpretedValue());
+  ASSERT_EQ(std::make_pair(s, 5), t2.getUninterpretedValue());
 }
 
 TEST_F(TestApiBlackTerm, substitute)