From 4c15812fb3475a15400fa7e4cc3aedb51a257adf Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 17 Jul 2019 11:14:22 -0400 Subject: [PATCH] Minor clean in strings. (#3093) --- src/theory/strings/theory_strings.cpp | 15 --------------- src/theory/strings/theory_strings_rewriter.cpp | 2 +- 2 files changed, 1 insertion(+), 16 deletions(-) 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]); -- 2.30.2