From 0e7bfa71e7bea8b832df00d00332b42bf8bca60b Mon Sep 17 00:00:00 2001
From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Fri, 28 Feb 2014 22:56:45 -0600
Subject: add re.nostr for the empty regular expression; add re.allchar for the
 regular expresssion containing all charactors

---
 src/theory/strings/regexp_operation.cpp          | 10 +++++-----
 src/theory/strings/regexp_operation.h            |  2 +-
 src/theory/strings/theory_strings_preprocess.cpp |  4 ++--
 src/theory/strings/theory_strings_rewriter.cpp   |  4 ++--
 4 files changed, 10 insertions(+), 10 deletions(-)

(limited to 'src/theory/strings')

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;
 		}
 	}
-- 
cgit v1.2.3