Add partial string support

contrib/setup-cvc5.sh

@@ -26,7 +26,12 @@ if [ ! -d "$DEPS/cvc5" ]; then
     make -j$NUM_CORES
     cd $DIR
 else
-    echo "$DEPS/cvc5 already exists. If you want to rebuild, please remove it manually."
+#    echo "$DEPS/cvc5 already exists. If you want to rebuild, please remove it manually."
+    cd $DEPS
+    cd cvc5
+    cd build
+    make -j$NUM_CORES
+    cd $DIR
 fi
 
 if [ -f $DEPS/cvc5/build/src/libcvc5.a ] && [ -f $DEPS/cvc5/build/src/parser/libcvc5parser.a ]; then

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/src/cvc5_solver.cpp

@@ -94,6 +94,10 @@ const std::unordered_map<PrimOp, ::cvc5::Kind> primop2kind(
       { BV_To_Nat, ::cvc5::BITVECTOR_TO_NAT },
       // Indexed Op
       { Int_To_BV, ::cvc5::INT_TO_BITVECTOR },
+      { StrLt, ::cvc5::STRING_LT },
+      { StrLeq, ::cvc5::STRING_LEQ },
+      { StrLen, ::cvc5::STRING_LENGTH }, 
+      { StrConcat, ::cvc5::STRING_CONCAT },
       { Select, ::cvc5::SELECT },
       { Store, ::cvc5::STORE },
       { Forall, ::cvc5::FORALL },
@@ -163,7 +167,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 +191,60 @@ 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 constant with string and useEscSequences";
+      msg += useEscSequences;
+      msg += " 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 constant with wstring 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 +536,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

@@ -50,6 +50,7 @@ const std::unordered_map<::cvc5::Kind, PrimOp> kind2primop(
       { ::cvc5::NEG, Negate },
       { ::cvc5::MULT, Mult },
       { ::cvc5::DIVISION, Div },
+      { ::cvc5::INTS_DIVISION, IntDiv },
       { ::cvc5::LT, Lt },
       { ::cvc5::LEQ, Le },
       { ::cvc5::GT, Gt },
@@ -104,6 +105,11 @@ const std::unordered_map<::cvc5::Kind, PrimOp> kind2primop(
       { ::cvc5::BITVECTOR_ROTATE_RIGHT, Rotate_Right },
       // Conversion
       { ::cvc5::BITVECTOR_TO_NAT, BV_To_Nat },
+      // String Op
+      { ::cvc5::STRING_LT, StrLt },
+      { ::cvc5::STRING_LEQ, StrLeq },
+      { ::cvc5::STRING_LENGTH, StrLen },
+      { ::cvc5::STRING_CONCAT, StrConcat },
       // Indexed Op
       { ::cvc5::INT_TO_BITVECTOR, Int_To_BV },
       { ::cvc5::SELECT, Select },

include/generic_solver.h

@@ -127,6 +127,11 @@ class GenericSolver : public AbsSmtSolver
    */
   Term make_value(bool b) const;
   Term make_value(int64_t i, const Sort & sort) const;
+  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_value(const std::string& s, bool useEscSequences, const Sort & sort) const;
+  Term make_value(const std::wstring& s, const Sort & sort) const;
+
   Term make_value(const std::string val,
                   const Sort & sort,
                   uint64_t base = 10) const;

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/ops.h

@@ -97,6 +97,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
+          { "STRING",
+            { { "str.<", StrLt },
+              { "str.<=", StrLeq},
+              { "str.len", StrLen}, 
+              { "str.++", StrConcat} } },
           // ArraysEx
           { "A",
             {

include/solver.h

@@ -210,6 +210,28 @@ class AbsSmtSolver
    */
   virtual Term make_term(int64_t i, const Sort & sort) const = 0;
 
+  /* Make a string value term
+   * @param s is the value
+   * @param useEscSequences is the useEscSequences in String constructor
+   * @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/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);

src/generic_solver.cpp

@@ -851,6 +851,36 @@ Term GenericSolver::make_value(int64_t i, const Sort & sort) const
   }
 }
 
+Term GenericSolver::make_term(const std::string& s, bool useEscSequences, const Sort & sort) const
+{
+  Term value_term = make_value(s, useEscSequences, sort);
+  return store_term(value_term);
+}
+Term GenericSolver::make_term(const std::wstring& s, const Sort & sort) const
+{
+  Term value_term = make_value(s, sort);
+  return store_term(value_term);
+}
+
+Term GenericSolver::make_value(const std::string& s, bool useEscSequences, const Sort & sort) const
+{
+  SortKind sk = sort->get_sort_kind();
+  assert(sk == STRING);
+  string repr;
+  repr = std::to_string(s);
+  Term term = std::make_shared<GenericTerm>(sort, Op(), TermVec{}, repr); //figure out how to handle useEscSequences
+  return term;
+}
+Term GenericSolver::make_value(const std::wstring& s, const Sort & sort) const
+{
+  SortKind sk = sort->get_sort_kind();
+  assert(sk == STRING);
+  string repr;
+  repr = std::to_string(s);
+  Term term = std::make_shared<GenericTerm>(sort, Op(), TermVec{}, repr);
+  return term;
+}
+
 Term GenericSolver::make_term(const string val,
                               const Sort & sort,
                               uint64_t base) const

src/generic_sort.cpp

@@ -38,7 +38,7 @@ Sort make_uninterpreted_generic_sort(Sort sort_cons,
 
 Sort make_generic_sort(SortKind sk)
 {
-  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));
   }
@@ -217,7 +217,8 @@ bool GenericSort::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();
     }
@@ -279,7 +280,8 @@ const std::unordered_map<SortKind, std::string> sortkind2smtlib(
     { { ARRAY, "Array" },
       { BOOL, "Bool" },
       { INT, "Int" },
-      { REAL, "Real" }});
+      { REAL, "Real" },
+      { STRING, "String" }});
 
 std::string to_smtlib(SortKind sk)
 {

src/logging_solver.cpp

@@ -205,6 +205,46 @@ 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