add re.nostr for the empty regular expression; add re.allchar for the regular expresssion containing all charactors

4 files changed, 10 insertions, 10 deletions

diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index 7f6893d7f..573aabe81 100644
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -173,7 +173,7 @@ int RegExpOpr::delta( Node r ) {
 			}

 			default: {

 				Trace("strings-error") << "Unsupported term: " << mkString( r ) << " in delta of RegExp." << std::endl;

-				AlwaysAssert( false );

+				Assert( false );

 				//return Node::null();

 			}

 		}

@@ -526,12 +526,12 @@ bool RegExpOpr::follow( Node r, CVC4::String c, std::vector< char > &vec_chars )
 			ret = 2;

 		}

 			break;*/

-		default:

-			//TODO: special sym: sigma, none, all

+		default: {

 			Trace("strings-error") << "Unsupported term: " << mkString( r ) << " in delta of RegExp." << std::endl;

 			//AlwaysAssert( false );

 			//return Node::null();

 			return false;

+		}

 	}

 }

 

@@ -791,7 +791,7 @@ void RegExpOpr::simplifyNRegExp( Node s, Node r, std::vector< Node > &new_nodes
 			}

 			default: {

 				Trace("strings-regexp") << "Unsupported term: " << r << " in simplifyNRegExp." << std::endl;

-				AlwaysAssert( false, "Unsupported Term" );

+				Assert( false, "Unsupported Term" );

 			}

 		}

 		conc = Rewriter::rewrite( conc );

@@ -907,7 +907,7 @@ void RegExpOpr::simplifyPRegExp( Node s, Node r, std::vector< Node > &new_nodes
 			}

 			default: {

 				Trace("strings-regexp") << "Unsupported term: " << r << " in simplifyPRegExp." << std::endl;

-				AlwaysAssert( false, "Unsupported Term" );

+				Assert( false, "Unsupported Term" );

 			}

 		}

 		conc = Rewriter::rewrite( conc );

diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h
index 32bfb2b3d..f9ae0a0ca 100644
--- a/src/theory/strings/regexp_operation.h
+++ b/src/theory/strings/regexp_operation.h
@@ -54,12 +54,12 @@ private:
 	void simplifyNRegExp( Node s, Node r, std::vector< Node > &new_nodes );

 	std::string niceChar( Node r );

 	int gcd ( int a, int b );

+	Node mkAllExceptOne( char c );

 

 public:

 	RegExpOpr();

 	bool checkConstRegExp( Node r );

     void simplify(Node t, std::vector< Node > &new_nodes, bool polarity);

-	Node mkAllExceptOne( char c );

 	Node complement( Node r );

 	int delta( Node r );

 	Node derivativeSingle( Node r, CVC4::String c );

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index bb79f337b..15958def8 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -99,8 +99,8 @@ void StringsPreprocess::processRegExp( Node s, Node r, std::vector< Node > &ret
 			break;
 		}
 		default: {
-			Trace("strings-preprocess") << "Unsupported term: " << r << " in simplifyRegExp." << std::endl;
-			AlwaysAssert( false, "Unsupported Term" );
+			Trace("strings-error") << "Unsupported term: " << r << " in simplifyRegExp." << std::endl;
+			Assert( false, "Unsupported Term" );
 		}
 	}
 }
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index c35e2b5c2..7196dc8f2 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -284,8 +284,8 @@ bool TheoryStringsRewriter::testConstStringInRegExp( CVC4::String &s, unsigned i
 			}
 		}
 		default: {
-			Trace("strings-postrewrite") << "Unsupported term: " << r << " in testConstStringInRegExp." << std::endl;
-			AlwaysAssert( false, "Unsupported Term" );
+			Trace("strings-error") << "Unsupported term: " << r << " in testConstStringInRegExp." << std::endl;
+			Assert( false, "Unsupported Term" );
 			return false;
 		}
 	}