From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 17 Jul 2019 15:14:22 +0000 (-0400)
Subject: Minor clean in strings. (#3093)
X-Git-Tag: cvc5-1.0.0~4090
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4c15812fb3475a15400fa7e4cc3aedb51a257adf;p=cvc5.git

Minor clean in strings. (#3093)
---

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 435d1d8c7..5e7061d22 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -1310,21 +1310,6 @@ void TheoryStrings::assertPendingFact(Node atom, bool polarity, Node exp) {
     Trace("strings-pending-debug") << "  Finished assert equality" << std::endl;
   } else {
     d_equalityEngine.assertPredicate( atom, polarity, exp );
-    //process extf
-    if( atom.getKind()==kind::STRING_IN_REGEXP ){
-      if( polarity && atom[1].getKind()==kind::REGEXP_RANGE ){
-        if( d_extf_infer_cache_u.find( atom )==d_extf_infer_cache_u.end() ){
-          d_extf_infer_cache_u.insert( atom );
-          //length of first argument is one
-          Node conc = d_one.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, atom[0] ) );
-          Node lem = NodeManager::currentNM()->mkNode( kind::OR, atom.negate(), conc );
-          Trace("strings-lemma") << "Strings::Lemma RE-Range-Len : " << lem << std::endl;
-          d_out->lemma( lem );
-        }
-      }
-    }
-    //register the atom here, since it may not create a new equivalence class
-    //getExtTheory()->registerTerm( atom );
   }
   Trace("strings-pending-debug") << "  Now collect terms" << std::endl;
   // Collect extended function terms in the atom. Notice that we must register
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 37e7d004f..a84f2b212 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -1233,7 +1233,7 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) {
     }
     else if (x.getKind() == STRING_CONCAT)
     {
-      // (str.in.re (str.++ x1 ... xn) (str.* R)) -->
+      // (str.in.re (str.++ x1 ... xn) (re.* R)) -->
       //   (str.in.re x1 (re.* R)) AND ... AND (str.in.re xn (re.* R))
       //     if the length of all strings in R is one.
       Node flr = getFixedLengthForRegexp(r[0]);