add re.nostr for the empty regular expression; add re.allchar for the regular express...

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 873f3dce65d88f90a8369a589a9d8a5828320dbb..6e9f04ce94da72a0a5c8dc8aabab810a6eb45f21 100644 (file)
--- 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 b709d7f806dc33603ce7f5da674077a369680661..dd6eac0ff6c485a7be284ff51b72bf2c6d571aa9 100644 (file)
--- 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 7f6893d7f45f4dd42d825e9b06169da70418e555..573aabe8108c6edd940ac4fc83ee6dbbb758651b 100644 (file)
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -173,7 +173,7 @@ int RegExpOpr::delta( Node r ) {
                        }\r
                        default: {\r
                                Trace("strings-error") << "Unsupported term: " << mkString( r ) << " in delta of RegExp." << std::endl;\r
-                               AlwaysAssert( false );\r
+                               Assert( false );\r
                                //return Node::null();\r
                        }\r
                }\r
@@ -526,12 +526,12 @@ bool RegExpOpr::follow( Node r, CVC4::String c, std::vector< char > &vec_chars )
                        ret = 2;\r
                }\r
                        break;*/\r
-               default:\r
-                       //TODO: special sym: sigma, none, all\r
+               default: {\r
                        Trace("strings-error") << "Unsupported term: " << mkString( r ) << " in delta of RegExp." << std::endl;\r
                        //AlwaysAssert( false );\r
                        //return Node::null();\r
                        return false;\r
+               }\r
        }\r
 }\r
 \r
@@ -791,7 +791,7 @@ void RegExpOpr::simplifyNRegExp( Node s, Node r, std::vector< Node > &new_nodes
                        }\r
                        default: {\r
                                Trace("strings-regexp") << "Unsupported term: " << r << " in simplifyNRegExp." << std::endl;\r
-                               AlwaysAssert( false, "Unsupported Term" );\r
+                               Assert( false, "Unsupported Term" );\r
                        }\r
                }\r
                conc = Rewriter::rewrite( conc );\r
@@ -907,7 +907,7 @@ void RegExpOpr::simplifyPRegExp( Node s, Node r, std::vector< Node > &new_nodes
                        }\r
                        default: {\r
                                Trace("strings-regexp") << "Unsupported term: " << r << " in simplifyPRegExp." << std::endl;\r
-                               AlwaysAssert( false, "Unsupported Term" );\r
+                               Assert( false, "Unsupported Term" );\r
                        }\r
                }\r
                conc = Rewriter::rewrite( conc );\r

diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h
index 32bfb2b3d73dd8ac2119b52d90425debde287870..f9ae0a0ca6fb971feaf1c98c1f97f3e612c3b585 100644 (file)
--- 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 );\r
        std::string niceChar( Node r );\r
        int gcd ( int a, int b );\r
+       Node mkAllExceptOne( char c );\r
 \r
 public:\r
        RegExpOpr();\r
        bool checkConstRegExp( Node r );\r
     void simplify(Node t, std::vector< Node > &new_nodes, bool polarity);\r
-       Node mkAllExceptOne( char c );\r
        Node complement( Node r );\r
        int delta( Node r );\r
        Node derivativeSingle( Node r, CVC4::String c );\r

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index bb79f337b7750611377e661fec5550d107fa3288..15958def832299ae3015d8e14eb247a1a3156b51 100644 (file)
--- 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 c35e2b5c28de3fdad9832690ffee77679ab2ecf1..7196dc8f23047da8d832a0f0e71af589dc90831f 100644 (file)
--- 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 dadc5996ccfee8c0ae07856b5df094f154462e4d..7985f407232d8007460744dbd50e9c736953c189 100644 (file)
--- 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 */