Some fixes to recent strings commits.

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index df568f1abe807e86da0e2fffcc1d811f817b64db..39ccc70c474aea5ad3d41ca7e98c85a0aab22adc 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -988,8 +988,8 @@ void SmtEngine::setLogicInternal() throw() {
          ) ||
         // Quantifiers
         d_logic.isQuantified() ||
-               // Strings
-               d_logic.isTheoryEnabled(THEORY_STRINGS)
+        // Strings
+        d_logic.isTheoryEnabled(THEORY_STRINGS)
         ? decision::DECISION_STRATEGY_JUSTIFICATION
         : decision::DECISION_STRATEGY_INTERNAL
       );
@@ -1008,7 +1008,7 @@ void SmtEngine::setLogicInternal() throw() {
          d_logic.isPure(THEORY_ARITH) && d_logic.isLinear() && !d_logic.isDifferenceLogic() &&  !d_logic.areIntegersUsed()
          ) ||
         // Quantifiers
-        d_logic.isQuantified() 
+        d_logic.isQuantified()
         ? true : false
       );
 
@@ -2861,12 +2861,12 @@ void SmtEnginePrivate::processAssertions() {
 
   // Assertions ARE guaranteed to be rewritten by this point
 
-  if( d_smt.d_logic.isTheoryEnabled(THEORY_STRINGS) ){
-       CVC4::theory::strings::StringsPreprocess sp;
-       sp.simplify( d_assertionsToPreprocess );
+  if( d_smt.d_logic.isTheoryEnabled(THEORY_STRINGS) ) {
+    CVC4::theory::strings::StringsPreprocess sp;
+    sp.simplify( d_assertionsToPreprocess );
     for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
-               d_assertionsToPreprocess[i] = Rewriter::rewrite( d_assertionsToPreprocess[i] );
-       }
+      d_assertionsToPreprocess[i] = Rewriter::rewrite( d_assertionsToPreprocess[i] );
+    }
   }
 
   dumpAssertions("pre-skolem-quant", d_assertionsToPreprocess);

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

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index d4f08fcdd2a0c632f26bd5f7a1f5facae81462a9..78710e4b980c22184f53821fd8fe61bed74aebab 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -371,7 +371,7 @@ void TheoryEngine::check(Theory::Effort effort) {
 
     // Must consult quantifiers theory for last call to ensure sat, or otherwise add a lemma
     if( effort == Theory::EFFORT_FULL && ! d_inConflict && ! needCheck() ) {
-               //d_theoryTable[THEORY_STRINGS]->check(Theory::EFFORT_LAST_CALL);
+      //d_theoryTable[THEORY_STRINGS]->check(Theory::EFFORT_LAST_CALL);
       if(d_logicInfo.isQuantified()) {
         // quantifiers engine must pass effort last call check
         d_quantEngine->check(Theory::EFFORT_LAST_CALL);

diff --git a/test/regress/regress0/strings/loop007.smt2 b/test/regress/regress0/strings/loop007.smt2
index 8d789edb31ad861164066577ae8fa1c851cf0bde..0534d8b5341c8ebb7a87c5af5169b69a82f1bdaa 100644 (file)
--- a/test/regress/regress0/strings/loop007.smt2
+++ b/test/regress/regress0/strings/loop007.smt2
@@ -1,10 +1,10 @@
-(set-logic ALL_SUPPORTED)\r
-(set-info :status sat)\r
-\r
-(declare-fun x () String)\r
-(declare-fun y () String)\r
-\r
-(assert (= (str.++ x y "aa") (str.++ "aa" y x)))\r
-(assert (= (str.len x) 1))\r
-\r
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+
+(declare-fun x () String)
+(declare-fun y () String)
+
+(assert (= (str.++ x y "aa") (str.++ "aa" y x)))
+(assert (= (str.len x) 1))
+
 (check-sat)
\ No newline at end of file

diff --git a/test/regress/regress0/strings/model001.smt2 b/test/regress/regress0/strings/model001.smt2
index e4e35f40d7d5a1a4ac6ef19addf92fb485886907..2832b5c96aab9825dcf5031ef9bea21dd25fb069 100644 (file)
--- a/test/regress/regress0/strings/model001.smt2
+++ b/test/regress/regress0/strings/model001.smt2
@@ -1,12 +1,12 @@
-(set-logic ALL_SUPPORTED)\r
-(set-info :status sat)\r
-(set-option :produce-models true)\r
-\r
-(declare-fun x () String)\r
-(declare-fun y () String)\r
-\r
-(assert (not (= x y)))\r
-(assert (= (str.len x) (str.len y)))\r
-\r
-(check-sat)\r
-;(get-model)\r
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(set-option :produce-models true)
+
+(declare-fun x () String)
+(declare-fun y () String)
+
+(assert (not (= x y)))
+(assert (= (str.len x) (str.len y)))
+
+(check-sat)
+;(get-model)