minor clean-up, bring back derivatives

diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index 2c9ba4b3ffe12d1b6c69138f37039001eac0b071..b28c2fd9d717ccb1ed7b2b57467e5ba450f4993f 100644 (file)
--- a/src/theory/strings/kinds
+++ b/src/theory/strings/kinds
@@ -78,23 +78,8 @@ operator REGEXP_PLUS 1 "regexp +"
 operator REGEXP_OPT 1 "regexp ?"
 operator REGEXP_RANGE 2 "regexp range"
 
-constant REGEXP_EMPTY \
-       ::CVC4::RegExpEmpty \
-       ::CVC4::RegExpHashFunction \
-       "util/regexp.h" \
-       "a regexp contains nothing"
-
-constant REGEXP_SIGMA \
-       ::CVC4::RegExpSigma \
-       ::CVC4::RegExpHashFunction \
-       "util/regexp.h" \
-       "a regexp contains an arbitrary charactor"
-
-#constant REGEXP_ALL \
-#      ::CVC4::RegExp \
-#      ::CVC4::RegExpHashFunction \
-#      "util/string.h" \
-#      "a regexp contains all strings"
+operator REGEXP_EMPTY 0 "regexp empty"
+operator REGEXP_SIGMA 0 "regexp all charactors"
 
 typerule REGEXP_CONCAT ::CVC4::theory::strings::RegExpConcatTypeRule
 typerule REGEXP_UNION ::CVC4::theory::strings::RegExpUnionTypeRule

diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index 6869e45f370606cb7a3fa2bc0e39227bc296d59c..7f6893d7f45f4dd42d825e9b06169da70418e555 100644 (file)
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -36,14 +36,15 @@ RegExpOpr::RegExpOpr() {
     d_emptyString = NodeManager::currentNM()->mkConst( ::CVC4::String("") );\r
     d_true = NodeManager::currentNM()->mkConst( true );\r
     d_false = NodeManager::currentNM()->mkConst( false );\r
-    d_emptyRegexp = NodeManager::currentNM()->mkConst( kind::REGEXP_EMPTY );\r
        d_zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) );\r
        d_one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );\r
+       std::vector< Node > nvec;\r
+    d_emptyRegexp = NodeManager::currentNM()->mkNode( kind::REGEXP_EMPTY, nvec );\r
        // All Charactors = all printable ones 32-126\r
-       d_char_start = 'a';//' ';\r
-       d_char_end = 'c';//'~';\r
-       d_sigma = mkAllExceptOne( '\0' );\r
-       //d_sigma = NodeManager::currentNM()->mkConst( kind::REGEXP_SIGMA );\r
+       //d_char_start = 'a';//' ';\r
+       //d_char_end = 'c';//'~';\r
+       //d_sigma = mkAllExceptOne( '\0' );\r
+       d_sigma = NodeManager::currentNM()->mkNode( kind::REGEXP_SIGMA, nvec );\r
        d_sigma_star = NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, d_sigma );\r
 }\r
 \r

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 28ef43cf97e3d7f77143a03e5a4c6928a23f54df..072d28f9d453dcf915516f0e9368f313230f5256 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -62,7 +62,8 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu
     d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
     d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
     d_emptyString = NodeManager::currentNM()->mkConst( ::CVC4::String("") );
-       d_emptyRegexp = NodeManager::currentNM()->mkConst( kind::REGEXP_EMPTY );
+       std::vector< Node > nvec;
+       d_emptyRegexp = NodeManager::currentNM()->mkNode( kind::REGEXP_EMPTY, nvec );
        d_true = NodeManager::currentNM()->mkConst( true );
     d_false = NodeManager::currentNM()->mkConst( false );
 
@@ -2312,13 +2313,13 @@ bool TheoryStrings::checkMemberships() {
                                                        flag = false;
                                                        d_regexp_deriv_processed[atom] = true;
                                                }
-                                       } /*else if(splitRegExp( x, r, atom )) {
+                                       } else if(splitRegExp( x, r, atom )) {
                                                addedLemma = true; flag = false;
                                                d_regexp_deriv_processed[ atom ] = true;
-                                       }*/
+                                       }
                                }
                        } else {
-                               //TODO
+                               //TODO: will be removed soon. keep it for consistence
                                if(! options::stringExp()) {
                                        is_unk = true;
                                        break;

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index b118e389e1fd0c642a29301f101e525a6dfdcd32..c35e2b5c28de3fdad9832690ffee77679ab2ecf1 100644 (file)
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -138,7 +138,8 @@ Node TheoryStringsRewriter::prerewriteConcatRegExp( TNode node ) {
         }
     }
        if(emptyflag) {
-               retNode = NodeManager::currentNM()->mkConst( kind::REGEXP_EMPTY );
+               std::vector< Node > nvec;
+               retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_EMPTY, nvec );
        } else {
                if(!preNode.isNull()) {
                        node_vec.push_back( NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, preNode ) );
@@ -173,7 +174,8 @@ Node TheoryStringsRewriter::prerewriteOrRegExp(TNode node) {
                }
        }
        if(flag) {
-               retNode = node_vec.size() == 0 ? NodeManager::currentNM()->mkConst( kind::REGEXP_EMPTY ) :
+               std::vector< Node > nvec;
+               retNode = node_vec.size() == 0 ? NodeManager::currentNM()->mkNode( kind::REGEXP_EMPTY, nvec ) :
                                        node_vec.size() == 1 ? node_vec[0] : NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, node_vec);
        }
        Trace("strings-prerewrite") << "Strings::prerewriteOrRegExp end " << retNode << std::endl;