Make strings robust to regular expression variables. (#2255)

The theory solver for strings does not support regular expression variables. With this PR, we properly throw an exception if it is given one.

However, the rewriter needs to handle regular expression variables (for various reasons: rewriting an expression before its asserted, sygus explanation generalization, etc.).  This corrects a few miscellaneous issues in the strings rewriter to make it sound for these cases.

It also corrects a seg fault in simpleRegexpConsume when testing memberships `(str.in.re "" R)`, where R is a *non-constant* regular expression (which will now be allowed if variables are allowed).

This is in preparation for adding `RegLan` as a token to the smt2/sygus parsers.

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index cb1f006b34cd4652ea93b2356426225726347741..2ce3258622075cf8ce9108dcb3dd74a76897f40a 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -701,6 +701,8 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m)
 void TheoryStrings::preRegisterTerm(TNode n) {
   if( d_pregistered_terms_cache.find(n) == d_pregistered_terms_cache.end() ) {
     d_pregistered_terms_cache.insert(n);
+    Trace("strings-preregister")
+        << "TheoryString::preregister : " << n << std::endl;
     //check for logic exceptions
     Kind k = n.getKind();
     if( !options::stringExp() ){
@@ -732,6 +734,12 @@ void TheoryStrings::preRegisterTerm(TNode n) {
       default: {
         registerTerm(n, 0);
         TypeNode tn = n.getType();
+        if (tn.isRegExp() && n.isVar())
+        {
+          std::stringstream ss;
+          ss << "Regular expression variables are not supported.";
+          throw LogicException(ss.str());
+        }
         if( tn.isString() ) {
           // if finite model finding is enabled,
           // then we minimize the length of this term if it is a variable

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 9651fe980fe1185fd063655c63ae9af3ef1c5678..fe92dd8ff5d7a977fe043392017c9ebe2933af97 100644 (file)
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -73,8 +73,15 @@ Node TheoryStringsRewriter::simpleRegexpConsume( std::vector< Node >& mchildren,
         }else if( xc.isConst() ){
           //check for constants
           CVC4::String s = xc.getConst<String>();
-          Assert( s.size()>0 );
-          if( rc.getKind() == kind::REGEXP_RANGE || rc.getKind()==kind::REGEXP_SIGMA ){
+          if (s.size() == 0)
+          {
+            // ignore and continue
+            mchildren.pop_back();
+            do_next = true;
+          }
+          else if (rc.getKind() == kind::REGEXP_RANGE
+                   || rc.getKind() == kind::REGEXP_SIGMA)
+          {
             CVC4::String ss( t==0 ? s.getLastChar() : s.getFirstChar() );
             if( testConstStringInRegExp( ss, 0, rc ) ){
               //strip off one character
@@ -698,6 +705,10 @@ Node TheoryStringsRewriter::rewriteLoopRegExp(TNode node)
 bool TheoryStringsRewriter::isConstRegExp( TNode t ) {
   if( t.getKind()==kind::STRING_TO_REGEXP ) {
     return t[0].isConst();
+  }
+  else if (t.isVar())
+  {
+    return false;
   }else{
     for( unsigned i = 0; i<t.getNumChildren(); ++i ) {
       if( !isConstRegExp(t[i]) ){
@@ -711,6 +722,7 @@ bool TheoryStringsRewriter::isConstRegExp( TNode t ) {
 bool TheoryStringsRewriter::testConstStringInRegExp( CVC4::String &s, unsigned int index_start, TNode r ) {
   Assert( index_start <= s.size() );
   Trace("regexp-debug") << "Checking " << s << " in " << r << ", starting at " << index_start << std::endl;
+  Assert(!r.isVar());
   int k = r.getKind();
   switch( k ) {
     case kind::STRING_TO_REGEXP: {