Some fixes to recent strings commits.

3 files changed, 181 insertions, 163 deletions

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index d62fd4c9e..8fa4345e5 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -1,120 +1,135 @@
-/*********************                                                        */

-/*! \file theory_strings_preprocess.cpp

- ** \verbatim

- ** Original author: Tianyi Liang

- ** Major contributors: Tianyi Liang, Andrew Reynolds

- ** Minor contributors (to current version): none

- ** This file is part of the CVC4 prototype.

- ** Copyright (c) 2013-2013  New York University and The University of Iowa

- ** See the file COPYING in the top-level source directory for licensing

- ** information.\endverbatim

- **

- ** \brief Strings Preprocess

- **

- ** Strings Preprocess.

- **/

-

-#include "theory/strings/theory_strings_preprocess.h"

-#include "expr/kind.h"

-

-namespace CVC4 {

-namespace theory {

-namespace strings {

-

-void StringsPreprocess::simplifyRegExp( Node s, Node r, std::vector< Node > &ret ) {

-	int k = r.getKind();

-	switch( k ) {

-		case kind::STRING_TO_REGEXP:

-		{

-			Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, s, r[0] );

-			ret.push_back( eq );

-		}

-			break;

-		case kind::REGEXP_CONCAT:

-		{

-			std::vector< Node > cc;

-			for(unsigned i=0; i<r.getNumChildren(); ++i) {

-				Node sk = NodeManager::currentNM()->mkSkolem( "recsym_$$", s.getType(), "created for regular expression concat" );

-				simplifyRegExp( sk, r[i], ret );

-				cc.push_back( sk );

-			}

-			Node cc_eq = NodeManager::currentNM()->mkNode( kind::EQUAL, s, 

-						NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, cc ) );

-			ret.push_back( cc_eq );

-		}

-			break;

-		case kind::REGEXP_OR:

-		{

-			std::vector< Node > c_or;

-			for(unsigned i=0; i<r.getNumChildren(); ++i) {

-				simplifyRegExp( s, r[i], c_or );

-			}

-			Node eq = NodeManager::currentNM()->mkNode( kind::OR, c_or );

-			ret.push_back( eq );

-		}

-			break;

-		case kind::REGEXP_INTER:

-			for(unsigned i=0; i<r.getNumChildren(); ++i) {

-				simplifyRegExp( s, r[i], ret );

-			}

-			break;

-		case kind::REGEXP_STAR:

-		{

-			Node sk = NodeManager::currentNM()->mkSkolem( "ressym_$$", s.getType(), "created for regular expression star" );

-			Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL,

-						NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk, s ),

-						NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, s, sk ));

-			ret.push_back( eq );

-			simplifyRegExp( sk, r[0], ret );

-		}

-			break;

-		case kind::REGEXP_OPT:

-		{

-			Node eq_empty = NodeManager::currentNM()->mkNode( kind::EQUAL, s, NodeManager::currentNM()->mkConst( ::CVC4::String("") ) );

-			std::vector< Node > rr;

-			simplifyRegExp( s, r[0], rr );

-			Node nrr = rr.size()==1 ? rr[0] : NodeManager::currentNM()->mkNode( kind::AND, rr );

-			ret.push_back( NodeManager::currentNM()->mkNode( kind::OR, eq_empty, nrr) );

-		}

-			break;

-		default:

-			//TODO:case kind::REGEXP_PLUS:

-			//TODO: special sym: sigma, none, all

-			break;

-	}

-}

-

-Node StringsPreprocess::simplify( Node t ) {

-	if( t.getKind() == kind::STRING_IN_REGEXP ){

-		// t0 in t1

-		//rewrite it

-		std::vector< Node > ret;

-		simplifyRegExp( t[0], t[1], ret );

-

-		return ret.size() == 1 ? ret[0] : NodeManager::currentNM()->mkNode( kind::AND, ret );

-    }else if( t.getNumChildren()>0 ){

-		std::vector< Node > cc;

-		if (t.getMetaKind() == kind::metakind::PARAMETERIZED) {

-			cc.push_back(t.getOperator());

-		}

-		bool changed = false;

-		for( unsigned i=0; i<t.getNumChildren(); i++ ){

-			Node tn = simplify( t[i] );

-			cc.push_back( tn );

-			changed = changed || tn!=t[i];

-		}

-		return changed ? NodeManager::currentNM()->mkNode( t.getKind(), cc ) : t;

-	}else{

-		return t;

-	}

-}

-

-void StringsPreprocess::simplify(std::vector< Node > &vec_node) {

-	for( unsigned i=0; i<vec_node.size(); i++ ){

-		vec_node[i] = simplify( vec_node[i] );

-	}

-}

-

-}/* CVC4::theory::strings namespace */

-}/* CVC4::theory namespace */

-}/* CVC4 namespace */

+/*********************                                                        */
+/*! \file theory_strings_preprocess.cpp
+ ** \verbatim
+ ** Original author: Tianyi Liang
+ ** Major contributors: Tianyi Liang, Andrew Reynolds
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2013-2013  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Strings Preprocess
+ **
+ ** Strings Preprocess.
+ **/
+
+#include "theory/strings/theory_strings_preprocess.h"
+#include "expr/kind.h"
+
+namespace CVC4 {
+namespace theory {
+namespace strings {
+
+void StringsPreprocess::simplifyRegExp( Node s, Node r, std::vector< Node > &ret ) {
+	int k = r.getKind();
+	switch( k ) {
+		case kind::STRING_TO_REGEXP:
+		{
+			Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, s, r[0] );
+			ret.push_back( eq );
+		}
+			break;
+		case kind::REGEXP_CONCAT:
+		{
+			std::vector< Node > cc;
+			for(unsigned i=0; i<r.getNumChildren(); ++i) {
+				Node sk = NodeManager::currentNM()->mkSkolem( "recsym_$$", s.getType(), "created for regular expression concat" );
+				simplifyRegExp( sk, r[i], ret );
+				cc.push_back( sk );
+			}
+			Node cc_eq = NodeManager::currentNM()->mkNode( kind::EQUAL, s, 
+						NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, cc ) );
+			ret.push_back( cc_eq );
+		}
+			break;
+		case kind::REGEXP_OR:
+		{
+			std::vector< Node > c_or;
+			for(unsigned i=0; i<r.getNumChildren(); ++i) {
+				simplifyRegExp( s, r[i], c_or );
+			}
+			Node eq = NodeManager::currentNM()->mkNode( kind::OR, c_or );
+			ret.push_back( eq );
+		}
+			break;
+		case kind::REGEXP_INTER:
+			for(unsigned i=0; i<r.getNumChildren(); ++i) {
+				simplifyRegExp( s, r[i], ret );
+			}
+			break;
+		case kind::REGEXP_STAR:
+		{
+			Node sk = NodeManager::currentNM()->mkSkolem( "ressym_$$", s.getType(), "created for regular expression star" );
+			Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL,
+						NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk, s ),
+						NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, s, sk ));
+			ret.push_back( eq );
+			simplifyRegExp( sk, r[0], ret );
+		}
+			break;
+		case kind::REGEXP_OPT:
+		{
+			Node eq_empty = NodeManager::currentNM()->mkNode( kind::EQUAL, s, NodeManager::currentNM()->mkConst( ::CVC4::String("") ) );
+			std::vector< Node > rr;
+			simplifyRegExp( s, r[0], rr );
+			Node nrr = rr.size()==1 ? rr[0] : NodeManager::currentNM()->mkNode( kind::AND, rr );
+			ret.push_back( NodeManager::currentNM()->mkNode( kind::OR, eq_empty, nrr) );
+		}
+			break;
+		default:
+			//TODO:case kind::REGEXP_PLUS:
+			//TODO: special sym: sigma, none, all
+			break;
+	}
+}
+
+Node StringsPreprocess::simplify( Node t ) {
+    std::hash_map<TNode, Node, TNodeHashFunction>::const_iterator i = d_cache.find(t);
+    if(i != d_cache.end()) {
+      return (*i).second.isNull() ? t : (*i).second;
+    }
+
+	if( t.getKind() == kind::STRING_IN_REGEXP ){
+		// t0 in t1
+		//rewrite it
+		std::vector< Node > ret;
+		simplifyRegExp( t[0], t[1], ret );
+
+		Node n = ret.size() == 1 ? ret[0] : NodeManager::currentNM()->mkNode( kind::AND, ret );
+		d_cache[t] = (t == n) ? Node::null() : n;
+		return n;
+    }else if( t.getNumChildren()>0 ){
+		std::vector< Node > cc;
+		if (t.getMetaKind() == kind::metakind::PARAMETERIZED) {
+			cc.push_back(t.getOperator());
+		}
+		bool changed = false;
+		for( unsigned i=0; i<t.getNumChildren(); i++ ){
+			Node tn = simplify( t[i] );
+			cc.push_back( tn );
+			changed = changed || tn!=t[i];
+		}
+		if(changed) {
+			Node n = NodeManager::currentNM()->mkNode( t.getKind(), cc );
+			d_cache[t] = n;
+			return n;
+		} else {
+			d_cache[t] = Node::null();
+			return t;
+		}
+	}else{
+		d_cache[t] = Node::null();
+		return t;
+	}
+}
+
+void StringsPreprocess::simplify(std::vector< Node > &vec_node) {
+	for( unsigned i=0; i<vec_node.size(); i++ ){
+		vec_node[i] = simplify( vec_node[i] );
+	}
+}
+
+}/* CVC4::theory::strings namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h
index 2b2e7dfea..f82a3cf24 100644
--- a/src/theory/strings/theory_strings_preprocess.h
+++ b/src/theory/strings/theory_strings_preprocess.h
@@ -1,41 +1,44 @@
-/*********************                                                        */

-/*! \file theory_strings_preprocess.h

- ** \verbatim

- ** Original author: Tianyi Liang

- ** Major contributors: Tianyi Liang, Andrew Reynolds

- ** Minor contributors (to current version): none

- ** This file is part of the CVC4 prototype.

- ** Copyright (c) 2013-2013  New York University and The University of Iowa

- ** See the file COPYING in the top-level source directory for licensing

- ** information.\endverbatim

- **

- ** \brief Strings Preprocess

- **

- ** Strings Preprocess.

- **/

-

-#include "cvc4_private.h"

-

-#ifndef __CVC4__THEORY__STRINGS__PREPROCESS_H

-#define __CVC4__THEORY__STRINGS__PREPROCESS_H

-

-#include <vector>

-#include "theory/theory.h"

-

-namespace CVC4 {

-namespace theory {

-namespace strings {

-

-class StringsPreprocess {

-private:

-	void simplifyRegExp( Node s, Node r, std::vector< Node > &ret );

-	Node simplify( Node t );

-public:

-void simplify(std::vector< Node > &vec_node);

-};

-

-}/* CVC4::theory::strings namespace */

-}/* CVC4::theory namespace */

-}/* CVC4 namespace */

-

-#endif /* __CVC4__THEORY__STRINGS__PREPROCESS_H */

+/*********************                                                        */
+/*! \file theory_strings_preprocess.h
+ ** \verbatim
+ ** Original author: Tianyi Liang
+ ** Major contributors: Tianyi Liang, Andrew Reynolds
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2013-2013  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Strings Preprocess
+ **
+ ** Strings Preprocess.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__STRINGS__PREPROCESS_H
+#define __CVC4__THEORY__STRINGS__PREPROCESS_H
+
+#include <vector>
+#include "util/hash.h"
+#include "theory/theory.h"
+
+namespace CVC4 {
+namespace theory {
+namespace strings {
+
+class StringsPreprocess {
+	// NOTE: this class is NOT context-dependent
+	std::hash_map<TNode, Node, TNodeHashFunction> d_cache;
+private:
+	void simplifyRegExp( Node s, Node r, std::vector< Node > &ret );
+	Node simplify( Node t );
+public:
+void simplify(std::vector< Node > &vec_node);
+};
+
+}/* CVC4::theory::strings namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__STRINGS__PREPROCESS_H */
diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h
index 9c3d6c71e..8fc630206 100644
--- a/src/theory/strings/theory_strings_type_rules.h
+++ b/src/theory/strings/theory_strings_type_rules.h
@@ -181,9 +181,9 @@ public:
     if (!t.isString()) {
       throw TypeCheckingExceptionPrivate(n, "expecting string terms");
     }
-	if( (*it).getKind() != kind::CONST_STRING ) {
+    if( (*it).getKind() != kind::CONST_STRING ) {
       throw TypeCheckingExceptionPrivate(n, "expecting constant string terms");
-	}
+    }
     if(++it != it_end) {
       throw TypeCheckingExceptionPrivate(n, "too many terms");
     }