Support for str.<= and str.< (#1882)

17 files changed, 248 insertions, 26 deletions

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 09dccdfbd..133cc12c1 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -154,6 +154,8 @@ void Smt2::addStringOperators() {
   addOperator(kind::REGEXP_RANGE, "re.range");
   addOperator(kind::REGEXP_LOOP, "re.loop");
   addOperator(kind::STRING_CODE, "str.code");
+  addOperator(kind::STRING_LT, "str.<");
+  addOperator(kind::STRING_LEQ, "str.<=");
 }
 
 void Smt2::addFloatingPointOperators() {
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 2c6a26335..36076ec3c 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -521,6 +521,8 @@ void Smt2Printer::toStream(std::ostream& out,
   case kind::STRING_STRREPL:
   case kind::STRING_PREFIX:
   case kind::STRING_SUFFIX:
+  case kind::STRING_LEQ:
+  case kind::STRING_LT:
   case kind::STRING_ITOS:
   case kind::STRING_STOI:
   case kind::STRING_CODE:
@@ -1061,6 +1063,9 @@ static string smtKindString(Kind k, Variant v)
   case kind::STRING_STRREPL: return "str.replace" ;
   case kind::STRING_PREFIX: return "str.prefixof" ;
   case kind::STRING_SUFFIX: return "str.suffixof" ;
+  case kind::STRING_LEQ: return "str.<=";
+  case kind::STRING_LT: return "str.<";
+  case kind::STRING_CODE: return "str.code";
   case kind::STRING_ITOS:
     return v == smt2_6_1_variant ? "str.from-int" : "int.to.str";
   case kind::STRING_STOI:
diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index 34237f69e..d931e99bc 100644
--- a/src/theory/strings/kinds
+++ b/src/theory/strings/kinds
@@ -18,6 +18,8 @@ operator STRING_LENGTH 1 "string length"
 operator STRING_SUBSTR 3 "string substr"
 operator STRING_CHARAT 2 "string charat"
 operator STRING_STRCTN 2 "string contains"
+operator STRING_LT 2 "string less than"
+operator STRING_LEQ 2 "string less than or equal"
 operator STRING_STRIDOF 3 "string indexof"
 operator STRING_STRREPL 3 "string replace"
 operator STRING_PREFIX 2 "string prefixof"
@@ -97,7 +99,9 @@ typerule STRING_CONCAT ::CVC4::theory::strings::StringConcatTypeRule
 typerule STRING_LENGTH ::CVC4::theory::strings::StringLengthTypeRule
 typerule STRING_SUBSTR ::CVC4::theory::strings::StringSubstrTypeRule
 typerule STRING_CHARAT ::CVC4::theory::strings::StringCharAtTypeRule
-typerule STRING_STRCTN ::CVC4::theory::strings::StringContainTypeRule
+typerule STRING_STRCTN ::CVC4::theory::strings::StringRelationTypeRule
+typerule STRING_LT ::CVC4::theory::strings::StringRelationTypeRule
+typerule STRING_LEQ ::CVC4::theory::strings::StringRelationTypeRule
 typerule STRING_STRIDOF ::CVC4::theory::strings::StringIndexOfTypeRule
 typerule STRING_STRREPL ::CVC4::theory::strings::StringReplaceTypeRule
 typerule STRING_PREFIX ::CVC4::theory::strings::StringPrefixOfTypeRule
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index b77a616b3..3da652457 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -124,6 +124,7 @@ TheoryStrings::TheoryStrings(context::Context* c,
   getExtTheory()->addFunctionKind(kind::STRING_STRREPL);
   getExtTheory()->addFunctionKind(kind::STRING_STRCTN);
   getExtTheory()->addFunctionKind(kind::STRING_IN_REGEXP);
+  getExtTheory()->addFunctionKind(kind::STRING_LEQ);
   getExtTheory()->addFunctionKind(kind::STRING_CODE);
 
   // The kinds we are treating as function application in congruence
@@ -133,6 +134,7 @@ TheoryStrings::TheoryStrings(context::Context* c,
   d_equalityEngine.addFunctionKind(kind::STRING_CODE);
   if( options::stringLazyPreproc() ){
     d_equalityEngine.addFunctionKind(kind::STRING_STRCTN);
+    d_equalityEngine.addFunctionKind(kind::STRING_LEQ);
     d_equalityEngine.addFunctionKind(kind::STRING_SUBSTR);
     d_equalityEngine.addFunctionKind(kind::STRING_ITOS);
     d_equalityEngine.addFunctionKind(kind::STRING_STOI);
@@ -142,6 +144,7 @@ TheoryStrings::TheoryStrings(context::Context* c,
 
   d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
   d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
+  d_neg_one = NodeManager::currentNM()->mkConst(Rational(-1));
   d_emptyString = NodeManager::currentNM()->mkConst( ::CVC4::String("") );
   std::vector< Node > nvec;
   d_emptyRegexp = NodeManager::currentNM()->mkNode( kind::REGEXP_EMPTY, nvec );
@@ -436,7 +439,8 @@ int TheoryStrings::getReduction( int effort, Node n, Node& nr ) {
           Assert(k == STRING_SUBSTR || k == STRING_STRCTN || k == STRING_STRIDOF
                  || k == STRING_ITOS
                  || k == STRING_STOI
-                 || k == STRING_STRREPL);
+                 || k == STRING_STRREPL
+                 || k == STRING_LEQ);
           std::vector< Node > new_nodes;
           Node res = d_preproc.simplify( n, new_nodes );
           Assert( res!=n );
@@ -547,8 +551,9 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m)
         Assert(d_normal_forms.find(eqc) != d_normal_forms.end());
         if (d_normal_forms[eqc].size() == 1)
         {
-          // does it have a code?
-          if (d_has_str_code)
+          // does it have a code and the length of these equivalence classes are
+          // one?
+          if (d_has_str_code && lts_values[i] == d_one)
           {
             EqcInfo* eip = getOrMakeEqcInfo(eqc, false);
             if (eip && !eip->d_code_term.get().isNull())
@@ -563,7 +568,7 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m)
               vec.push_back(String::convertCodeToUnsignedInt(cvalue));
               Node mv = nm->mkConst(String(vec));
               pure_eq_assign[eqc] = mv;
-              m->getEqualityEngine()->addTerm( mv );
+              m->getEqualityEngine()->addTerm(mv);
             }
           }
           pure_eq.push_back(eqc);
@@ -579,7 +584,8 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m)
     //assign a new length if necessary
     if( !pure_eq.empty() ){
       if( lts_values[i].isNull() ){
-        unsigned lvalue = 0;
+        // start with length two (other lengths have special precendence)
+        unsigned lvalue = 2;
         while( values_used.find( lvalue )!=values_used.end() ){
           lvalue++;
         }
@@ -671,16 +677,22 @@ void TheoryStrings::preRegisterTerm(TNode n) {
   if( d_pregistered_terms_cache.find(n) == d_pregistered_terms_cache.end() ) {
     d_pregistered_terms_cache.insert(n);
     //check for logic exceptions
+    Kind k = n.getKind();
     if( !options::stringExp() ){
-      if( n.getKind()==kind::STRING_STRIDOF ||
-          n.getKind() == kind::STRING_ITOS || n.getKind() == kind::STRING_STOI ||
-          n.getKind() == kind::STRING_STRREPL || n.getKind() == kind::STRING_STRCTN ){
+      if (k == kind::STRING_STRIDOF || k == kind::STRING_ITOS
+          || k == kind::STRING_STOI
+          || k == kind::STRING_STRREPL
+          || k == kind::STRING_STRCTN
+          || k == STRING_LEQ)
+      {
         std::stringstream ss;
-        ss << "Term of kind " << n.getKind() << " not supported in default mode, try --strings-exp";
+        ss << "Term of kind " << k
+           << " not supported in default mode, try --strings-exp";
         throw LogicException(ss.str());
       }
     }
-    switch( n.getKind() ) {
+    switch (k)
+    {
       case kind::EQUAL: {
         d_equalityEngine.addTriggerEquality(n);
         break;
@@ -702,7 +714,7 @@ void TheoryStrings::preRegisterTerm(TNode n) {
           // not belong to this theory.
           if (options::stringFMF()
               && (n.isVar() ? d_all_skolems.find(n) == d_all_skolems.end()
-                            : kindToTheoryId(n.getKind()) != THEORY_STRINGS))
+                            : kindToTheoryId(k) != THEORY_STRINGS))
           {
             d_input_vars.insert(n);
           }
@@ -720,7 +732,9 @@ void TheoryStrings::preRegisterTerm(TNode n) {
           }
         }
         //concat terms do not contribute to theory combination?  TODO: verify
-        if( n.hasOperator() && kindToTheoryId( n.getKind() )==THEORY_STRINGS && n.getKind()!=kind::STRING_CONCAT ){
+        if (n.hasOperator() && kindToTheoryId(k) == THEORY_STRINGS
+            && k != kind::STRING_CONCAT)
+        {
           d_functionsTerms.push_back( n );
         }
       }
@@ -2218,13 +2232,15 @@ void TheoryStrings::checkNormalForms(){
       cmps.pop_back();
       for (const Node& c2 : cmps)
       {
-        Trace("strings-code-debug") << "Compare codes : " << c1 << " " << c2
-                                    << std::endl;
-        if (!areDisequal(c1, c2))
+        Trace("strings-code-debug")
+            << "Compare codes : " << c1 << " " << c2 << std::endl;
+        if (!areDisequal(c1, c2) && !areEqual(c1, d_neg_one))
         {
+          Node eq_no = c1.eqNode(d_neg_one);
+          Node deq = c1.eqNode(c2).negate();
           Node eqn = c1[0].eqNode(c2[0]);
-          Node eq = c1.eqNode(c2);
-          Node inj_lem = nm->mkNode(kind::OR, eq.negate(), eqn);
+          // str.code(x)==-1 V str.code(x)!=str.code(y) V x==y
+          Node inj_lem = nm->mkNode(kind::OR, eq_no, deq, eqn);
           sendInference(d_empty_vec, inj_lem, "Code_Inj");
         }
       }
@@ -3520,9 +3536,8 @@ void TheoryStrings::registerTerm( Node n, int effort ) {
         d_has_str_code = true;
         NodeManager* nm = NodeManager::currentNM();
         // ite( str.len(s)==1, 0 <= str.code(s) < num_codes, str.code(s)=-1 )
-        Node neg_one = nm->mkConst(Rational(-1));
         Node code_len = mkLength(n[0]).eqNode(d_one);
-        Node code_eq_neg1 = n.eqNode(nm->mkConst(Rational(-1)));
+        Node code_eq_neg1 = n.eqNode(d_neg_one);
         Node code_range = nm->mkNode(
             kind::AND,
             nm->mkNode(kind::GEQ, n, d_zero),
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 85d2754a8..bd5a797ae 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -196,6 +196,7 @@ private:
   Node d_false;
   Node d_zero;
   Node d_one;
+  Node d_neg_one;
   CVC4::Rational RMAXINT;
   unsigned d_card_size;
   // Helper functions
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index d412eaa33..fac7fccf2 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -23,6 +23,8 @@
 #include "proof/proof_manager.h"
 #include "smt/logic_exception.h"
 
+using namespace CVC4;
+using namespace CVC4::kind;
 
 namespace CVC4 {
 namespace theory {
@@ -30,8 +32,9 @@ namespace strings {
 
 StringsPreprocess::StringsPreprocess( context::UserContext* u ){
   //Constants
-  d_zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) );
-  d_one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
+  d_zero = NodeManager::currentNM()->mkConst(Rational(0));
+  d_one = NodeManager::currentNM()->mkConst(Rational(1));
+  d_empty_str = NodeManager::currentNM()->mkConst(String(""));
 }
 
 StringsPreprocess::~StringsPreprocess(){
@@ -472,6 +475,58 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
                 );
     retNode = NodeManager::currentNM()->mkNode( kind::EXISTS, b1v, body );
   }
+  else if (t.getKind() == kind::STRING_LEQ)
+  {
+    Node ltp = nm->mkSkolem("ltp", nm->booleanType());
+    Node k = nm->mkSkolem("k", nm->integerType());
+
+    std::vector<Node> conj;
+    conj.push_back(nm->mkNode(GEQ, k, d_zero));
+    Node substr[2];
+    Node code[2];
+    for (unsigned r = 0; r < 2; r++)
+    {
+      Node ta = t[r];
+      Node tb = t[1 - r];
+      substr[r] = nm->mkNode(STRING_SUBSTR, ta, d_zero, k);
+      code[r] =
+          nm->mkNode(STRING_CODE, nm->mkNode(STRING_SUBSTR, ta, k, d_one));
+      conj.push_back(nm->mkNode(LEQ, k, nm->mkNode(STRING_LENGTH, ta)));
+    }
+    conj.push_back(substr[0].eqNode(substr[1]));
+    std::vector<Node> ite_ch;
+    ite_ch.push_back(ltp);
+    for (unsigned r = 0; r < 2; r++)
+    {
+      ite_ch.push_back(nm->mkNode(LT, code[r], code[1 - r]));
+    }
+    conj.push_back(nm->mkNode(ITE, ite_ch));
+
+    // Intuitively, the reduction says either x and y are equal, or they have
+    // some (maximal) common prefix after which their characters at position k
+    // are distinct, and the comparison of their code matches the return value
+    // of the overall term.
+    // Notice the below reduction relies on the semantics of str.code being -1
+    // for the empty string. In particular, say x = "a" and y = "ab", then the
+    // reduction below is satisfied for k = 1, since
+    //   str.code(substr( "a", 1, 1 )) = str.code( "" ) = -1 <
+    //   str.code(substr( "ab", 1, 1 )) = str.code( "b" ) = 66
+
+    // assert:
+    //  IF x=y
+    //  THEN: ltp
+    //  ELSE: k >= 0 AND k <= len( x ) AND k <= len( y ) AND
+    //        substr( x, 0, k ) = substr( y, 0, k ) AND
+    //        IF    ltp
+    //        THEN: str.code(substr( x, k, 1 )) < str.code(substr( y, k, 1 ))
+    //        ELSE: str.code(substr( x, k, 1 )) > str.code(substr( y, k, 1 ))
+    Node assert =
+        nm->mkNode(ITE, t[0].eqNode(t[1]), ltp, nm->mkNode(AND, conj));
+    new_nodes.push_back(assert);
+
+    // Thus, str.<=( x, y ) = p_lt
+    retNode = ltp;
+  }
 
   if( t!=retNode ){
     Trace("strings-preprocess") << "StringsPreprocess::simplify: " << t << " -> " << retNode << std::endl;
diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h
index 41987265e..d342cba72 100644
--- a/src/theory/strings/theory_strings_preprocess.h
+++ b/src/theory/strings/theory_strings_preprocess.h
@@ -33,6 +33,7 @@ class StringsPreprocess {
   //Constants
   Node d_zero;
   Node d_one;
+  Node d_empty_str;
   //mapping from kinds to UF
   std::map< Kind, std::map< unsigned, Node > > d_uf;
   //get UF for node
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index cfd0f6e73..a426c0306 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -1176,6 +1176,18 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
     retNode = rewriteSubstr(node);
   }else if( node.getKind() == kind::STRING_STRCTN ){
     retNode = rewriteContains( node );
+  }
+  else if (node.getKind() == kind::STRING_LT)
+  {
+    NodeManager* nm = NodeManager::currentNM();
+    // eliminate s < t ---> s != t AND s <= t
+    retNode = nm->mkNode(AND,
+                         node[0].eqNode(node[1]).negate(),
+                         nm->mkNode(STRING_LEQ, node[0], node[1]));
+  }
+  else if (node.getKind() == kind::STRING_LEQ)
+  {
+    retNode = rewriteStringLeq(node);
   }else if( node.getKind()==kind::STRING_STRIDOF ){
     retNode = rewriteIndexof( node );
   }else if( node.getKind() == kind::STRING_STRREPL ){
@@ -2187,6 +2199,60 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) {
   return node;
 }
 
+Node TheoryStringsRewriter::rewriteStringLeq(Node n)
+{
+  Assert(n.getKind() == kind::STRING_LEQ);
+  NodeManager* nm = NodeManager::currentNM();
+  if (n[0] == n[1])
+  {
+    Node ret = nm->mkConst(true);
+    return returnRewrite(n, ret, "str-leq-id");
+  }
+  if (n[0].isConst() && n[1].isConst())
+  {
+    String s = n[0].getConst<String>();
+    String t = n[1].getConst<String>();
+    Node ret = nm->mkConst(s.isLeq(t));
+    return returnRewrite(n, ret, "str-leq-eval");
+  }
+  // empty strings
+  for (unsigned i = 0; i < 2; i++)
+  {
+    if (n[i].isConst() && n[i].getConst<String>().isEmptyString())
+    {
+      Node ret = i == 0 ? nm->mkConst(true) : n[0].eqNode(n[1]);
+      return returnRewrite(n, ret, "str-leq-empty");
+    }
+  }
+
+  std::vector<Node> n1;
+  getConcat(n[0], n1);
+  std::vector<Node> n2;
+  getConcat(n[1], n2);
+  Assert(!n1.empty() && !n2.empty());
+
+  // constant prefixes
+  if (n1[0].isConst() && n2[0].isConst() && n1[0] != n2[0])
+  {
+    String s = n1[0].getConst<String>();
+    String t = n2[0].getConst<String>();
+    // only need to truncate if s is longer
+    if (s.size() > t.size())
+    {
+      s = s.prefix(t.size());
+    }
+    // if prefix is not leq, then entire string is not leq
+    if (!s.isLeq(t))
+    {
+      Node ret = nm->mkConst(false);
+      return returnRewrite(n, ret, "str-leq-cprefix");
+    }
+  }
+
+  Trace("strings-rewrite-nf") << "No rewrites for : " << n << std::endl;
+  return n;
+}
+
 Node TheoryStringsRewriter::rewritePrefixSuffix(Node n)
 {
   Assert(n.getKind() == kind::STRING_PREFIX
diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h
index f7e65f3a9..8befb5e0f 100644
--- a/src/theory/strings/theory_strings_rewriter.h
+++ b/src/theory/strings/theory_strings_rewriter.h
@@ -103,6 +103,12 @@ private:
   * Returns the rewritten form of node.
   */
   static Node rewriteReplace(Node node);
+  /** rewrite string less than or equal
+  * This is the entry point for post-rewriting terms n of the form
+  *   str.<=( t, s )
+  * Returns the rewritten form of n.
+  */
+  static Node rewriteStringLeq(Node n);
   /** rewrite prefix/suffix
   * This is the entry point for post-rewriting terms n of the form
   *   str.prefixof( s, t ) / str.suffixof( s, t )
diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h
index b4629b338..e9e87f29a 100644
--- a/src/theory/strings/theory_strings_type_rules.h
+++ b/src/theory/strings/theory_strings_type_rules.h
@@ -91,18 +91,21 @@ public:
   }
 };
 
-class StringContainTypeRule {
-public:
+class StringRelationTypeRule
+{
+ public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
   {
     if( check ) {
       TypeNode t = n[0].getType(check);
       if (!t.isString()) {
-        throw TypeCheckingExceptionPrivate(n, "expecting an original string term in string contain");
+        throw TypeCheckingExceptionPrivate(
+            n, "expecting a string term in string relation");
       }
       t = n[1].getType(check);
       if (!t.isString()) {
-        throw TypeCheckingExceptionPrivate(n, "expecting a target string term in string contain");
+        throw TypeCheckingExceptionPrivate(
+            n, "expecting a string term in string relation");
       }
     }
     return nodeManager->booleanType();
diff --git a/src/util/regexp.cpp b/src/util/regexp.cpp
index 4cbda5147..bfd9cc3a7 100644
--- a/src/util/regexp.cpp
+++ b/src/util/regexp.cpp
@@ -298,6 +298,26 @@ std::string String::toString(bool useEscSequences) const {
   return str;
 }
 
+bool String::isLeq(const String &y) const
+{
+  for (unsigned i = 0; i < size(); ++i)
+  {
+    if (i >= y.size())
+    {
+      return false;
+    }
+    if (d_str[i] > y.d_str[i])
+    {
+      return false;
+    }
+    if (d_str[i] < y.d_str[i])
+    {
+      return true;
+    }
+  }
+  return true;
+}
+
 bool String::isRepeated() const {
   if (size() > 1) {
     unsigned int f = d_str[0];
diff --git a/src/util/regexp.h b/src/util/regexp.h
index c8b491475..8b99dfd87 100644
--- a/src/util/regexp.h
+++ b/src/util/regexp.h
@@ -131,6 +131,8 @@ class CVC4_PUBLIC String {
   bool empty() const { return d_str.empty(); }
   /** is this the empty string? */
   bool isEmptyString() const { return empty(); }
+  /** is less than or equal to string y */
+  bool isLeq(const String& y) const;
   /** Return the length of the string */
   std::size_t size() const { return d_str.size(); }
 
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 8584eeca9..cf702ed7c 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -776,6 +776,7 @@ REG0_TESTS = \
 	regress0/strings/bug002.smt2 \
 	regress0/strings/bug612.smt2 \
 	regress0/strings/bug613.smt2 \
+	regress0/strings/code-sat-neg-one.smt2 \
 	regress0/strings/escchar.smt2 \
 	regress0/strings/escchar_25.smt2 \
 	regress0/strings/idof-rewrites.smt2 \
@@ -1452,6 +1453,9 @@ REG1_TESTS = \
 	regress1/strings/str007.smt2 \
 	regress1/strings/string-unsound-sem.smt2 \
 	regress1/strings/strings-index-empty.smt2 \
+	regress1/strings/strings-leq-trans-unsat.smt2 \
+	regress1/strings/strings-lt-len5.smt2 \
+	regress1/strings/strings-lt-simple.smt2 \
 	regress1/strings/strip-endpt-sound.smt2 \
 	regress1/strings/str-code-sat.smt2 \
 	regress1/strings/str-code-unsat.smt2 \
diff --git a/test/regress/regress0/strings/code-sat-neg-one.smt2 b/test/regress/regress0/strings/code-sat-neg-one.smt2
new file mode 100644
index 000000000..c69276a4f
--- /dev/null
+++ b/test/regress/regress0/strings/code-sat-neg-one.smt2
@@ -0,0 +1,7 @@
+(set-logic QF_SLIA)
+(set-info :status sat)
+(declare-fun x () String)
+(declare-fun y () String)
+(assert (not (= x y)))
+(assert (= (str.code x) (str.code y)))
+(check-sat)
diff --git a/test/regress/regress1/strings/strings-leq-trans-unsat.smt2 b/test/regress/regress1/strings/strings-leq-trans-unsat.smt2
new file mode 100644
index 000000000..de3946ef0
--- /dev/null
+++ b/test/regress/regress1/strings/strings-leq-trans-unsat.smt2
@@ -0,0 +1,14 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: unsat
+(set-logic QF_SLIA)
+(set-info :status unsat)
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+(declare-fun w () String)
+(assert (str.<= x y))
+(assert (str.<= y w))
+(declare-fun xp () String)
+(assert (= x (str.++ "G" xp)))
+(assert (= w "E"))
+(check-sat)
diff --git a/test/regress/regress1/strings/strings-lt-len5.smt2 b/test/regress/regress1/strings/strings-lt-len5.smt2
new file mode 100644
index 000000000..aeabfdf75
--- /dev/null
+++ b/test/regress/regress1/strings/strings-lt-len5.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: sat
+(set-logic QF_SLIA)
+(set-info :status sat)
+(declare-fun y () String)
+(assert (> (str.len y) 5))
+(assert (str.< "ACAAB" y))
+(assert (str.< y "ACAAD"))
+(check-sat)
diff --git a/test/regress/regress1/strings/strings-lt-simple.smt2 b/test/regress/regress1/strings/strings-lt-simple.smt2
new file mode 100644
index 000000000..e077cf1f7
--- /dev/null
+++ b/test/regress/regress1/strings/strings-lt-simple.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: sat
+(set-logic QF_SLIA)
+(set-info :status sat)
+(declare-fun y () String)
+(assert (str.< "AC" y))
+(assert (str.< y "AF"))
+(check-sat)