From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Fri, 28 Feb 2014 19:04:33 +0000 (-0600)
Subject: minor clean-up, bring back derivatives
X-Git-Tag: cvc5-1.0.0~7053
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fb4104e7c5a88741f9ffd55384198af31435df9e;p=cvc5.git

minor clean-up, bring back derivatives
---

diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index 2c9ba4b3f..b28c2fd9d 100644
--- 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 6869e45f3..7f6893d7f 100644
--- 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("") );
     d_true = NodeManager::currentNM()->mkConst( true );
     d_false = NodeManager::currentNM()->mkConst( false );
-    d_emptyRegexp = NodeManager::currentNM()->mkConst( kind::REGEXP_EMPTY );
 	d_zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) );
 	d_one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
+	std::vector< Node > nvec;
+    d_emptyRegexp = NodeManager::currentNM()->mkNode( kind::REGEXP_EMPTY, nvec );
 	// All Charactors = all printable ones 32-126
-	d_char_start = 'a';//' ';
-	d_char_end = 'c';//'~';
-	d_sigma = mkAllExceptOne( '\0' );
-	//d_sigma = NodeManager::currentNM()->mkConst( kind::REGEXP_SIGMA );
+	//d_char_start = 'a';//' ';
+	//d_char_end = 'c';//'~';
+	//d_sigma = mkAllExceptOne( '\0' );
+	d_sigma = NodeManager::currentNM()->mkNode( kind::REGEXP_SIGMA, nvec );
 	d_sigma_star = NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, d_sigma );
 }
 
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 28ef43cf9..072d28f9d 100644
--- 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 b118e389e..c35e2b5c2 100644
--- 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;