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

7 files changed, 23 insertions, 23 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 873f3dce6..6e9f04ce9 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1032,6 +1032,12 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
   | str[s,false]
     { expr = MK_CONST( ::CVC4::String(s) ); }
 
+  | RENOSTR_TOK
+    { std::vector< Expr > nvec; expr = MK_EXPR( CVC4::kind::REGEXP_EMPTY, nvec ); }
+
+  | REALLCHAR_TOK
+    { std::vector< Expr > nvec; expr = MK_EXPR( CVC4::kind::REGEXP_SIGMA, nvec ); }
+
   | EMPTYSET_TOK
     { expr = MK_CONST( ::CVC4::EmptySet()); }
 
@@ -1294,12 +1300,12 @@ builtinOp[CVC4::Kind& kind]
   | STRREPL_TOK    { $kind = CVC4::kind::STRING_STRREPL; }
   | STRPREF_TOK    { $kind = CVC4::kind::STRING_PREFIX; }
   | STRSUFF_TOK    { $kind = CVC4::kind::STRING_SUFFIX; }
-  | STRITOS_TOK      { $kind = CVC4::kind::STRING_ITOS; }
-  | STRSTOI_TOK      { $kind = CVC4::kind::STRING_STOI; }
+  | STRITOS_TOK    { $kind = CVC4::kind::STRING_ITOS; }
+  | STRSTOI_TOK    { $kind = CVC4::kind::STRING_STOI; }
   | STRINRE_TOK    { $kind = CVC4::kind::STRING_IN_REGEXP; }
   | STRTORE_TOK    { $kind = CVC4::kind::STRING_TO_REGEXP; }
   | RECON_TOK      { $kind = CVC4::kind::REGEXP_CONCAT; }
-  | REUNION_TOK       { $kind = CVC4::kind::REGEXP_UNION; }
+  | REUNION_TOK    { $kind = CVC4::kind::REGEXP_UNION; }
   | REINTER_TOK    { $kind = CVC4::kind::REGEXP_INTER; }
   | RESTAR_TOK     { $kind = CVC4::kind::REGEXP_STAR; }
   | REPLUS_TOK     { $kind = CVC4::kind::REGEXP_PLUS; }
@@ -1705,6 +1711,8 @@ RESTAR_TOK : 're.*';
 REPLUS_TOK : 're.+';
 REOPT_TOK : 're.opt';
 RERANGE_TOK : 're.range';
+RENOSTR_TOK : 're.nostr';
+REALLCHAR_TOK : 're.allchar';
 
 SETUNION_TOK: 'union';
 SETINT_TOK: 'intersection';
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index b709d7f80..dd6eac0ff 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -346,6 +346,8 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   case kind::REGEXP_PLUS: out << "re.+ "; break;
   case kind::REGEXP_OPT: out << "re.opt "; break;
   case kind::REGEXP_RANGE: out << "re.range "; break;
+  case kind::REGEXP_EMPTY: out << "re.nostr "; break;
+  case kind::REGEXP_SIGMA: out << "re.allchar "; break;
 
     // bv theory
   case kind::BITVECTOR_CONCAT: out << "concat "; break;
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;
 		}
 	}
diff --git a/src/util/regexp.h b/src/util/regexp.h
index dadc5996c..7985f4072 100644
--- a/src/util/regexp.h
+++ b/src/util/regexp.h
@@ -404,16 +404,6 @@ struct CVC4_PUBLIC RegExpHashFunction {
 
 std::ostream& operator <<(std::ostream& os, const RegExp& s) CVC4_PUBLIC;
 
-class CVC4_PUBLIC RegExpEmpty : public RegExp {
-public:
-	RegExpEmpty() : RegExp(0) {}
-};
-
-class CVC4_PUBLIC RegExpSigma : public RegExp {
-public:
-	RegExpSigma() : RegExp(2) {}
-};
-
 }/* CVC4 namespace */
 
 #endif /* __CVC4__REGEXP_H */