Add partial string support (#327)

Added string support for StrLt "str.<", StrLeq "str.<=", StrLen "str.len", StrConcat, "str.++".

cvc5/include/cvc5_solver.h

@@ -100,6 +100,8 @@ class Cvc5Solver : public AbsSmtSolver
 
   Term make_term(bool b) const override;
   Term make_term(int64_t i, const Sort & sort) const override;
+  Term make_term(const std::string& s, bool useEscSequences, const Sort & sort) const override;
+  Term make_term(const std::wstring& s, const Sort & sort) const override;
   Term make_term(const std::string val,
                  const Sort & sort,
                  uint64_t base = 10) const override;
@@ -127,7 +129,7 @@ class Cvc5Solver : public AbsSmtSolver
   // getters for solver-specific objects
   // for interacting with third-party cvc5-specific software
   ::cvc5::Solver & get_cvc5_solver() { return solver; };
-
+  
  protected:
   ::cvc5::Solver solver;
 

cvc5/include/cvc5_term.h

@@ -64,6 +64,7 @@ class Cvc5Term : public AbsTerm
   bool is_symbolic_const() const override;
   bool is_value() const override;
   virtual std::string to_string() override;
+  virtual std::wstring getStringValue() const override;
   uint64_t to_int() const override;
   /** Iterators for traversing the children
    */

cvc5/src/cvc5_solver.cpp

@@ -92,8 +92,13 @@ const std::unordered_map<PrimOp, ::cvc5::Kind> primop2kind(
       { Rotate_Right, ::cvc5::Kind::BITVECTOR_ROTATE_RIGHT },
       // Conversion
       { BV_To_Nat, ::cvc5::Kind::BITVECTOR_TO_NAT },
-      // Indexed Op
       { Int_To_BV, ::cvc5::Kind::INT_TO_BITVECTOR },
+      // String Op
+      { StrLt, ::cvc5::Kind::STRING_LT },
+      { StrLeq, ::cvc5::Kind::STRING_LEQ },
+      { StrLen, ::cvc5::Kind::STRING_LENGTH }, 
+      { StrConcat, ::cvc5::Kind::STRING_CONCAT },
+      // Indexed Op
       { Select, ::cvc5::Kind::SELECT },
       { Store, ::cvc5::Kind::STORE },
       { Forall, ::cvc5::Kind::FORALL },
@@ -163,7 +168,7 @@ Term Cvc5Solver::make_term(int64_t i, const Sort & sort) const
     else if (sk == REAL)
     {
       c = solver.mkReal(i);
-    }
+    }   
     else if (sk == BV)
     {
       // cvc5 uses unsigned integers for mkBitVector
@@ -187,6 +192,58 @@ Term Cvc5Solver::make_term(int64_t i, const Sort & sort) const
   }
 }
 
+Term Cvc5Solver::make_term(const std::string& s, bool useEscSequences, const Sort & sort) const
+{
+  try
+  {
+    SortKind sk = sort->get_sort_kind();
+    ::cvc5::Term c;
+
+    if (sk == STRING)
+    {
+      c = solver.mkString(s, useEscSequences);
+    }    
+    else
+    {
+      std::string msg = "Can't create a string constant for sort ";
+      msg += sort->to_string();
+      throw IncorrectUsageException(msg.c_str());
+    }
+
+    return std::make_shared<Cvc5Term>(c);
+  }
+  catch (::cvc5::CVC5ApiException & e)
+  {
+    throw IncorrectUsageException(e.what());
+  }
+}
+
+Term Cvc5Solver::make_term(const std::wstring& s, const Sort & sort) const
+{
+  try
+  {
+    SortKind sk = sort->get_sort_kind();
+    ::cvc5::Term c;
+
+    if (sk == STRING)
+    {
+      c = solver.mkString(s);
+    }    
+    else
+    {
+      std::string msg = "Can't create string constant for sort ";
+      msg += sort->to_string();
+      throw IncorrectUsageException(msg.c_str());
+    }
+
+    return std::make_shared<Cvc5Term>(c);
+  }
+  catch (::cvc5::CVC5ApiException & e)
+  {
+    throw IncorrectUsageException(e.what());
+  }
+}
+
 Term Cvc5Solver::make_term(std::string val,
                            const Sort & sort,
                            uint64_t base) const
@@ -478,6 +535,10 @@ Sort Cvc5Solver::make_sort(SortKind sk) const
     {
       return std::make_shared<Cvc5Sort>(solver.getRealSort());
     }
+    else if (sk == STRING)
+    {
+      return std::make_shared<Cvc5Sort>(solver.getStringSort());
+    }    
     else
     {
       std::string msg("Can't create sort with sort constructor ");

cvc5/src/cvc5_sort.cpp

@@ -126,6 +126,10 @@ SortKind Cvc5Sort::get_sort_kind() const
   {
     return REAL;
   }
+  else if (sort.isString())
+  {
+    return STRING;
+  }
   else if (sort.isArray())
   {
     return ARRAY;

cvc5/src/cvc5_term.cpp

@@ -104,6 +104,11 @@ const std::unordered_map<::cvc5::Kind, PrimOp> kind2primop(
       { ::cvc5::Kind::BITVECTOR_ROTATE_RIGHT, Rotate_Right },
       // Conversion
       { ::cvc5::Kind::BITVECTOR_TO_NAT, BV_To_Nat },
+      // String Op
+      { ::cvc5::Kind::STRING_LT, StrLt },
+      { ::cvc5::Kind::STRING_LEQ, StrLeq },
+      { ::cvc5::Kind::STRING_LENGTH, StrLen },
+      { ::cvc5::Kind::STRING_CONCAT, StrConcat },
       // Indexed Op
       { ::cvc5::Kind::INT_TO_BITVECTOR, Int_To_BV },
       { ::cvc5::Kind::SELECT, Select },
@@ -282,6 +287,8 @@ bool Cvc5Term::is_value() const
 
 std::string Cvc5Term::to_string() { return term.toString(); }
 
+std::wstring Cvc5Term::getStringValue() const { return term.getStringValue(); }
+
 uint64_t Cvc5Term::to_int() const
 {
   std::string val = term.toString();

include/logging_solver.h

@@ -57,6 +57,8 @@ class LoggingSolver : public AbsSmtSolver
 
   Term make_term(bool b) const override;
   Term make_term(int64_t i, const Sort & sort) const override;
+  Term make_term(const std::string& s, bool useEscSequences, const Sort & sort) const override;
+  Term make_term(const std::wstring& s, const Sort & sort) const override;
   Term make_term(const std::string val,
                  const Sort & sort,
                  uint64_t base = 10) const override;

include/logging_term.h

@@ -45,6 +45,7 @@ class LoggingTerm : public AbsTerm
   Op get_op() const override;
   Sort get_sort() const override;
   std::string to_string() override;
+  std::wstring getStringValue() const override;
   bool is_symbol() const override;
   bool is_param() const override;
   bool is_symbolic_const() const override;

include/ops.h

@@ -98,6 +98,11 @@ enum PrimOp
   // BitVector Conversion
   BV_To_Nat,
   Int_To_BV,
+  // Strings
+  StrLt,
+  StrLeq,
+  StrLen,
+  StrConcat,
   /* Array Theory */
   Select,
   Store,

include/printing_solver.h

@@ -97,6 +97,9 @@ class PrintingSolver : public AbsSmtSolver
 
   Term make_term(bool b) const override;
   Term make_term(int64_t i, const Sort & sort) const override;
+  Term make_term(const std::string& s, bool useEscSequences, const Sort & sort) const override;
+  Term make_term(const std::wstring& s, const Sort & sort) const override;
+
   Term make_term(const std::string val,
                  const Sort & sort,
                  uint64_t base = 10) const override;

include/smtlibparser_maps.h

@@ -96,6 +96,12 @@ const std::unordered_map<std::string, std::unordered_map<std::string, PrimOp>>
               { "repeat", Repeat },
               { "rotate_left", Rotate_Left },
               { "rotate_right", Rotate_Right } } },
+          // Strings
+          { "S",
+            { { "str.<", StrLt },
+              { "str.<=", StrLeq},
+              { "str.len", StrLen}, 
+              { "str.++", StrConcat} } },
           // ArraysEx
           { "A",
             {

include/solver.h

@@ -210,6 +210,29 @@ class AbsSmtSolver
    */
   virtual Term make_term(int64_t i, const Sort & sort) const = 0;
 
+  /* Make a string value term from an `std::string` which may contain SMT-LIB compatible
+   * escape sequences like `\u1000` or `\u{20}` to encode unicode characters.
+   * @param s is the value
+   * @param useEscSequences determines whether escape sequence in `s` should
+   * be converted to the corresponding unicode character
+   * @param sort the sort to create
+   * @return a value term with Sort sort and value s
+   */
+
+  virtual Term make_term(const std::string& s, bool useEscSequences, const Sort & sort) const{
+        throw NotImplementedException("Strings not supported for this solver.");
+  }
+
+  /* Make a string value term
+   * @param s is the value
+   * @param sort the sort to create
+   * @return a value term with Sort sort and value s
+   */  
+  virtual Term make_term(const std::wstring& s, const Sort & sort) const{
+        throw NotImplementedException("Strings not supported for this solver.");
+  }
+
+
   /* Make a bit-vector, int, real or (in the future) string value term
    * @param val the numeric value as a string, or a string value
    * @param sort the sort to create

include/solver_enums.h

@@ -50,6 +50,8 @@ enum SolverAttribute
   THEORY_INT,
   // supports real theory
   THEORY_REAL,
+  // supports STR theory
+  THEORY_STR,
   // supports array models
   ARRAY_MODELS,
   // supports constant arrays

include/sort.h

@@ -38,6 +38,7 @@ enum SortKind
   BV,
   INT,
   REAL,
+  STRING,
   FUNCTION,
   UNINTERPRETED,
   // an uninterpreted sort constructor (has non-zero arity and takes subsort

include/sort_inference.h

@@ -173,6 +173,8 @@ bool real_sorts(const SortVec & sorts);
 
 bool int_sorts(const SortVec & sorts);
 
+bool string_sorts(const SortVec & sorts);
+
 bool arithmetic_sorts(const SortVec & sorts);
 
 bool array_sorts(const SortVec & sorts);
@@ -191,6 +193,8 @@ Sort real_sort(Op op, const AbsSmtSolver * solver, const SortVec & sorts);
 
 Sort int_sort(Op op, const AbsSmtSolver * solver, const SortVec & sorts);
 
+Sort string_sort(Op op, const AbsSmtSolver * solver, const SortVec & sorts);
+
 Sort ite_sort(Op op, const AbsSmtSolver * solver, const SortVec & sorts);
 
 Sort extract_sort(Op op, const AbsSmtSolver * solver, const SortVec & sorts);

include/term.h

@@ -27,6 +27,7 @@
 #include "ops.h"
 #include "smt_defs.h"
 #include "sort.h"
+#include "exceptions.h"
 
 namespace smt {
 
@@ -51,6 +52,10 @@ class AbsTerm
   virtual Sort get_sort() const = 0;
   /* to_string in smt2 format */
   virtual std::string to_string() = 0;
+  /* returns the string term as a native string value */
+  virtual std::wstring getStringValue() const{
+    throw NotImplementedException("Strings not supported for this solver.");
+  }
   /* returns true iff this term is a symbol */
   virtual bool is_symbol() const = 0;
   /* returns true iff this term is a parameter (to be bound by a quantifier) */

src/logging_solver.cpp

@@ -34,7 +34,7 @@ namespace smt {
    have no Op or children
  */
 const unordered_set<SortKind> supported_sortkinds_for_get_value(
-    { BOOL, BV, INT, REAL, ARRAY });
+    { BOOL, BV, INT, STRING, REAL, ARRAY });
 
 /* LoggingSolver */
 
@@ -205,6 +205,45 @@ Term LoggingSolver::make_term(int64_t i, const Sort & sort) const
   return res;
 }
 
+Term LoggingSolver::make_term(const std::string& s, bool useEscSequences, const Sort & sort) const
+{
+  shared_ptr<LoggingSort> lsort = static_pointer_cast<LoggingSort>(sort);
+  Term wrapped_res = wrapped_solver->make_term(s, useEscSequences, lsort->wrapped_sort);
+  Term res = std::make_shared<LoggingTerm>(
+      wrapped_res, sort, Op(), TermVec{}, next_term_id);
+
+  // check hash table
+  // lookup modifies term in place and returns true if it's a known term
+  // i.e. returns existing term and destroying the unnecessary new one
+  if (!hashtable->lookup(res))
+  {
+    // this is the first time this term was created
+    hashtable->insert(res);
+    next_term_id++;
+  }
+
+  return res;
+}
+
+Term LoggingSolver::make_term(const std::wstring& s, const Sort & sort) const{
+  shared_ptr<LoggingSort> lsort = static_pointer_cast<LoggingSort>(sort);
+  Term wrapped_res = wrapped_solver->make_term(s, lsort->wrapped_sort);
+  Term res = std::make_shared<LoggingTerm>(
+      wrapped_res, sort, Op(), TermVec{}, next_term_id);
+
+  // check hash table
+  // lookup modifies term in place and returns true if it's a known term
+  // i.e. returns existing term and destroying the unnecessary new one
+  if (!hashtable->lookup(res))
+  {
+    // this is the first time this term was created
+    hashtable->insert(res);
+    next_term_id++;
+  }
+
+  return res;
+}
+
 Term LoggingSolver::make_term(const string name,
                               const Sort & sort,
                               uint64_t base) const

src/logging_sort.cpp

@@ -37,7 +37,7 @@ Sort make_uninterpreted_logging_sort(Sort s,
 
 Sort make_logging_sort(SortKind sk, Sort s)
 {
-  if (sk != BOOL && sk != INT && sk != REAL)
+  if (sk != BOOL && sk != INT && sk != REAL && sk != STRING)
   {
     throw IncorrectUsageException("Can't create sort from " + to_string(sk));
   }
@@ -135,7 +135,8 @@ bool LoggingSort::compare(const Sort & s) const
   {
     case BOOL:
     case INT:
-    case REAL: { return true;
+    case REAL:
+    case STRING: { return true;
     }
     case BV: { return get_width() == s->get_width();
     }

src/logging_term.cpp

@@ -164,6 +164,11 @@ string LoggingTerm::to_string()
   }
 }
 
+wstring LoggingTerm::getStringValue() const
+{
+  return wrapped_term->getStringValue();
+}
+
 bool LoggingTerm::is_symbol() const
 {
   // functions, parameters, and symbolic constants are all symbols

src/ops.cpp

@@ -85,6 +85,10 @@ const std::unordered_map<PrimOp, std::string> primop2str(
       { Rotate_Right, "rotate_right" },
       { BV_To_Nat, "bv2nat" },
       { Int_To_BV, "int2bv" },
+      { StrLt, "str.<"},
+      { StrLeq, "str.<="},
+      { StrLen, "str.len"}, 
+      { StrConcat, "str.++"},
       { Select, "select" },
       { Store, "store" },
       { Forall, "forall" },
@@ -167,6 +171,10 @@ const std::unordered_map<PrimOp, std::pair<size_t, size_t>> primop2arity(
       { Rotate_Right, { 1, 1 } },
       { BV_To_Nat, { 1, 1 } },
       { Int_To_BV, { 1, 1 } },
+      { StrLt, { 2, 2} },
+      { StrLeq, { 2, 2} },
+      { StrLen, { 1, 1} },
+      { StrConcat, { 2, INT_MAX} },
       { Select, { 2, 2 } },
       { Store, { 3, 3 } },
       // to make term traversal easier considering the differences