Lazy preprocessing of extended operators in strings. Add regressions. Fixes bug 613.

6 files changed, 88 insertions, 38 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 519f330df..ae93176b2 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3294,17 +3294,18 @@ void SmtEnginePrivate::processAssertions() {
     dumpAssertions("post-bv-to-bool", d_assertions);
     Trace("smt") << "POST bvToBool" << endl;
   }
-
-  if( d_smt.d_logic.isTheoryEnabled(THEORY_STRINGS) ) {
-    Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-strings-preprocess" << endl;
-    dumpAssertions("pre-strings-pp", d_assertions);
-    CVC4::theory::strings::StringsPreprocess sp;
-    sp.simplify( d_assertions.ref() );
-    //for (unsigned i = 0; i < d_assertions.size(); ++ i) {
-    //  d_assertions.replace( i, Rewriter::rewrite( d_assertions[i] ) );
-    //}
-    Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-strings-preprocess" << endl;
-    dumpAssertions("post-strings-pp", d_assertions);
+  if( !options::stringLazyPreproc() ){
+    if( d_smt.d_logic.isTheoryEnabled(THEORY_STRINGS) ) {
+      Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-strings-preprocess" << endl;
+      dumpAssertions("pre-strings-pp", d_assertions);
+      CVC4::theory::strings::StringsPreprocess sp;
+      sp.simplify( d_assertions.ref() );
+      //for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+      //  d_assertions.replace( i, Rewriter::rewrite( d_assertions[i] ) );
+      //}
+      Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-strings-preprocess" << endl;
+      dumpAssertions("post-strings-pp", d_assertions);
+    }
   }
   if( d_smt.d_logic.isQuantified() ){
     Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-quant-preprocess" << endl;
diff --git a/src/theory/strings/options b/src/theory/strings/options
index 596d46c54..8a839a118 100644
--- a/src/theory/strings/options
+++ b/src/theory/strings/options
@@ -32,4 +32,7 @@ option stringIgnNegMembership strings-inm --strings-inm bool :default false
 #expert-option stringCharCardinality strings-alphabet-card --strings-alphabet-card=N int16_t :default 128 :read-write
 # the cardinality of the characters used by the theory of strings, default 128 (for standard ASCII) or 256 (for extended ASCII)
 
+option stringLazyPreproc strings-lazy-pp --strings-lazy-pp bool :default true
+ perform string preprocessing lazily
+
 endmodule
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 4ac178cbd..507c74c53 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -74,10 +74,14 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu
   d_equalityEngine.addFunctionKind(kind::STRING_SUBSTR_TOTAL);
   d_equalityEngine.addFunctionKind(kind::STRING_ITOS);
   d_equalityEngine.addFunctionKind(kind::STRING_STOI);
-  //d_equalityEngine.addFunctionKind(kind::STRING_U16TOS);
-  //d_equalityEngine.addFunctionKind(kind::STRING_STOU16);
-  //d_equalityEngine.addFunctionKind(kind::STRING_U32TOS);
-  //d_equalityEngine.addFunctionKind(kind::STRING_STOU32);
+  if( options::stringLazyPreproc() ){
+    d_equalityEngine.addFunctionKind(kind::STRING_U16TOS);
+    d_equalityEngine.addFunctionKind(kind::STRING_STOU16);
+    d_equalityEngine.addFunctionKind(kind::STRING_U32TOS);
+    d_equalityEngine.addFunctionKind(kind::STRING_STOU32);
+    d_equalityEngine.addFunctionKind(kind::STRING_STRIDOF);
+    d_equalityEngine.addFunctionKind(kind::STRING_STRREPL);
+  }
 
   d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
   d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
@@ -593,9 +597,37 @@ void TheoryStrings::check(Effort e) {
     TNode fact = assertion.assertion;
 
     Trace("strings-assertion") << "get assertion: " << fact << endl;
-
     polarity = fact.getKind() != kind::NOT;
     atom = polarity ? fact : fact[0];
+
+    //run preprocess
+    if( options::stringLazyPreproc() ){
+      std::map< Node, Node >::iterator itp = d_preproc_cache.find( atom );
+      if( itp==d_preproc_cache.end() ){
+        std::vector< Node > new_nodes;
+        Node res = d_preproc.decompose( atom, new_nodes );
+        d_preproc_cache[atom] = res;
+        if( atom!=res ){
+          Trace("strings-assertion-debug") << "...preprocessed to : " << res << std::endl;
+          Node plem = NodeManager::currentNM()->mkNode( kind::IFF, atom, res );
+          plem = Rewriter::rewrite( plem );
+          d_out->lemma( plem );
+          Trace("strings-pp-lemma") << "Preprocess eq lemma : " << plem << std::endl;
+          Trace("strings-pp-lemma") << "...from " << fact << std::endl;
+        }else{
+          Trace("strings-assertion-debug") << "...preprocess ok." << std::endl;
+        }
+        if( !new_nodes.empty() ){
+          Node nnlem = new_nodes.size()==1 ? new_nodes[0] : NodeManager::currentNM()->mkNode( kind::AND, new_nodes );
+          nnlem = Rewriter::rewrite( nnlem );
+          Trace("strings-assertion-debug") << "...new nodes : " << nnlem << std::endl;
+          Trace("strings-pp-lemma") << "Preprocess lemma : " << nnlem << std::endl;
+          Trace("strings-pp-lemma") << "...from " << fact << std::endl;
+          d_out->lemma( nnlem );
+        }
+      }
+    }
+
     //must record string in regular expressions
     if ( atom.getKind() == kind::STRING_IN_REGEXP ) {
       addMembership(assertion);
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index d83df2a31..7eda63f37 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -173,6 +173,9 @@ private:
   std::vector< Node > d_terms_cache;
   void collectTerm( Node n );
   void appendTermLemma();
+  // preprocess cache
+  StringsPreprocess d_preproc;
+  std::map< Node, Node > d_preproc_cache;
 
   /////////////////////////////////////////////////////////////////////////////
   // MODEL GENERATION
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 8978372e3..581e2be0a 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -244,7 +244,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
       //t3 = s2
       Node c4 = t[1].eqNode( sk3 );
       //~contain(t2, s2)
-      Node c5 = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, 
+      Node c5 = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN,
                   NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, sk2,
                     NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, t[1], d_zero,
                       NodeManager::currentNM()->mkNode(kind::MINUS,
@@ -259,8 +259,13 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
       Node cond = skk.eqNode( negone );
       Node rr = NodeManager::currentNM()->mkNode( kind::ITE, cond, left, right );
       new_nodes.push_back( rr );
-      d_cache[t] = skk;
-      retNode = skk;
+      if( options::stringLazyPreproc() ){
+        new_nodes.push_back( t.eqNode( skk ) );
+        d_cache[t] = Node::null();
+      }else{
+        d_cache[t] = skk;
+        retNode = skk;
+      }
     } else {
       throw LogicException("string indexof not supported in default mode, try --strings-exp");
     }
@@ -373,12 +378,17 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
               t.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT,
                 NodeManager::currentNM()->mkConst(::CVC4::String("-")), pret))));
       new_nodes.push_back( conc );*/
-
-      d_cache[t] = pret;
+      if( options::stringLazyPreproc() && t!=pret ){
+        new_nodes.push_back( t.eqNode( pret ) );
+        d_cache[t] = Node::null();
+      }else{
+        d_cache[t] = pret;
+        retNode = pret;
+      }
+      //don't rewrite processed
       if(t != pret) {
         d_cache[pret] = pret;
       }
-      retNode = pret;
     } else {
       throw LogicException("string int.to.str not supported in default mode, try --strings-exp");
     }
@@ -488,12 +498,16 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
       Node conc = NodeManager::currentNM()->mkNode(kind::ITE, pret.eqNode(negone),
               NodeManager::currentNM()->mkNode(kind::OR, cc1, cc2), cc3);
       new_nodes.push_back( conc );
-
-      d_cache[t] = pret;
+      if( options::stringLazyPreproc() && t!=pret ){
+        new_nodes.push_back( t.eqNode( pret ) );
+        d_cache[t] = Node::null();
+      }else{
+        d_cache[t] = pret;
+        retNode = pret;
+      }
       if(t != pret) {
         d_cache[pret] = pret;
       }
-      retNode = pret;
     } else {
       throw LogicException("string int.to.str not supported in default mode, try --strings-exp");
     }
@@ -511,8 +525,8 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
       Node c3 = NodeManager::currentNM()->mkNode(kind::STRING_STRCTN,
                   NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, sk1,
                      NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, y, d_zero,
-                        NodeManager::currentNM()->mkNode(kind::MINUS, 
-                          NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, y), 
+                        NodeManager::currentNM()->mkNode(kind::MINUS,
+                          NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, y),
                           NodeManager::currentNM()->mkConst(::CVC4::Rational(1))))), y).negate();
       Node rr = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::ITE, cond,
               NodeManager::currentNM()->mkNode( kind::AND, c1, c2, c3),
@@ -520,9 +534,13 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
       new_nodes.push_back( rr );
       rr = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::GT, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, y), d_zero) );
       new_nodes.push_back( rr );
-
-      d_cache[t] = skw;
-      retNode = skw;
+      if( options::stringLazyPreproc() ){
+        new_nodes.push_back( t.eqNode( skw ) );
+        d_cache[t] = Node::null();
+      }else{
+        d_cache[t] = skw;
+        retNode = skw;
+      }
     } else {
       throw LogicException("string replace not supported in default mode, try --strings-exp");
     }
@@ -609,13 +627,6 @@ void StringsPreprocess::simplify(std::vector< Node > &vec_node) {
     }
   }
 }
-/*
-void StringsPreprocess::simplify(std::vector< Node > &vec_node) {
-  std::vector< Node > new_nodes;
-  simplify(vec_node, new_nodes);
-  vec_node.insert( vec_node.end(), new_nodes.begin(), new_nodes.end() );
-}
-*/
 
 }/* CVC4::theory::strings namespace */
 }/* CVC4::theory namespace */
diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h
index 155b7b236..d96644bee 100644
--- a/src/theory/strings/theory_strings_preprocess.h
+++ b/src/theory/strings/theory_strings_preprocess.h
@@ -38,8 +38,8 @@ private:
   int checkFixLenVar( Node t );
   void processRegExp( Node s, Node r, std::vector< Node > &ret );
   Node simplify( Node t, std::vector< Node > &new_nodes );
-  Node decompose( Node t, std::vector< Node > &new_nodes );
 public:
+  Node decompose( Node t, std::vector< Node > &new_nodes );
   void simplify(std::vector< Node > &vec_node);
   StringsPreprocess();
 };