Support char smt-lib syntax (#4188)

Towards support for the strings standard.

Adds support to (_ char #x ... ) syntax for characters.

2 files changed, 51 insertions, 6 deletions

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index fff4bef85..2e6e70d6b 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -2294,7 +2294,7 @@ Term Solver::mkValHelper(T t) const
   return res;
 }
 
-Term Solver::mkRealFromStrHelper(std::string s) const
+Term Solver::mkRealFromStrHelper(const std::string& s) const
 {
   /* CLN and GMP handle this case differently, CLN interprets it as 0, GMP
    * throws an std::invalid_argument exception. For consistency, we treat it
@@ -2318,7 +2318,7 @@ Term Solver::mkBVFromIntHelper(uint32_t size, uint64_t val) const
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
-Term Solver::mkBVFromStrHelper(std::string s, uint32_t base) const
+Term Solver::mkBVFromStrHelper(const std::string& s, uint32_t base) const
 {
   CVC4_API_ARG_CHECK_EXPECTED(!s.empty(), s) << "a non-empty string";
   CVC4_API_ARG_CHECK_EXPECTED(base == 2 || base == 10 || base == 16, s)
@@ -2328,7 +2328,7 @@ Term Solver::mkBVFromStrHelper(std::string s, uint32_t base) const
 }
 
 Term Solver::mkBVFromStrHelper(uint32_t size,
-                               std::string s,
+                               const std::string& s,
                                uint32_t base) const
 {
   CVC4_API_ARG_CHECK_EXPECTED(!s.empty(), s) << "a non-empty string";
@@ -2353,6 +2353,20 @@ Term Solver::mkBVFromStrHelper(uint32_t size,
   return mkValHelper<CVC4::BitVector>(CVC4::BitVector(size, val));
 }
 
+Term Solver::mkCharFromStrHelper(const std::string& s) const
+{
+  CVC4_API_CHECK(s.find_first_not_of("0123456789abcdefABCDEF", 0)
+                     == std::string::npos
+                 && s.size() <= 5 && s.size() > 0)
+      << "Unexpected string for hexidecimal character " << s;
+  uint32_t val = static_cast<uint32_t>(std::stoul(s, 0, 16));
+  CVC4_API_CHECK(val < String::num_codes())
+      << "Not a valid code point for hexidecimal character " << s;
+  std::vector<unsigned> cpts;
+  cpts.push_back(val);
+  return mkValHelper<CVC4::String>(CVC4::String(cpts));
+}
+
 Term Solver::mkTermFromKind(Kind kind) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
@@ -2951,6 +2965,21 @@ Term Solver::mkString(const std::vector<unsigned>& s) const
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
+Term Solver::mkChar(const std::string& s) const
+{
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  return mkCharFromStrHelper(s);
+  CVC4_API_SOLVER_TRY_CATCH_END;
+}
+
+Term Solver::mkChar(const char* s) const
+{
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4_API_ARG_CHECK_NOT_NULLPTR(s);
+  return mkCharFromStrHelper(std::string(s));
+  CVC4_API_SOLVER_TRY_CATCH_END;
+}
+
 Term Solver::mkUniverseSet(Sort sort) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 1a1cd3b61..edff95a2f 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -2303,6 +2303,20 @@ class CVC4_PUBLIC Solver
   Term mkString(const std::vector<unsigned>& 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;
+
+  /**
+   * 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 char* s) const;
+
+  /**
    * Create a universe set of the given sort.
    * @param sort the sort of the set elements
    * @return the universe set constant
@@ -2812,18 +2826,20 @@ class CVC4_PUBLIC Solver
   template <typename T>
   Term mkValHelper(T t) const;
   /* Helper for mkReal functions that take a string as argument. */
-  Term mkRealFromStrHelper(std::string s) const;
+  Term mkRealFromStrHelper(const std::string& s) const;
   /* Helper for mkBitVector functions that take a string as argument. */
-  Term mkBVFromStrHelper(std::string s, uint32_t base) const;
+  Term mkBVFromStrHelper(const std::string& s, uint32_t base) const;
   /* Helper for mkBitVector functions that take a string and a size as
    * arguments. */
-  Term mkBVFromStrHelper(uint32_t size, std::string s, uint32_t base) const;
+  Term mkBVFromStrHelper(uint32_t size, const std::string& s, uint32_t base) const;
   /* Helper for mkBitVector functions that take an integer as argument. */
   Term mkBVFromIntHelper(uint32_t size, uint64_t val) const;
   /* Helper for setLogic. */
   void setLogicHelper(const std::string& logic) const;
   /* Helper for mkTerm functions that create Term from a Kind */
   Term mkTermFromKind(Kind kind) const;
+  /* Helper for mkChar functions that take a string as argument. */
+  Term mkCharFromStrHelper(const std::string& s) const;
 
   /**
    * Helper function that ensures that a given term is of sort real (as opposed