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

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 519f330df7339fd231276899626c4985772ba58f..ae93176b26d26066f29559461bfd3f33d0075205 100644 (file)
--- 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 596d46c54ad4f98dbde5dc2210251c5ab2ed3cc7..8a839a1188e1fedcf18c4a08eddf897f3a599bcf 100644 (file)
--- 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 4ac178cbd9498211c596643090b5e6c4422f53cc..507c74c53a9e1543149af1122fad0cd4753be08d 100644 (file)
--- 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 d83df2a31118e64b211420ae21d9a54de2b85b34..7eda63f37b83848b8b8eaefcc1bd11f6f2789218 100644 (file)
--- 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 8978372e36c4111205094df22995610b4a3f7a66..581e2be0a53c721551ca9e29ff025823d8b953e5 100644 (file)
--- 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 155b7b2362915fb459d64c8fca5017d2d6b1d97e..d96644bee21de5fc045a3f9b7ada338b11fea314 100644 (file)
--- 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();
 };

diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
index eb88df9057b48e8c8f2770c7108576e509bfb4ae..b796fc80bd8b2b15eb0eeb23b8f82273fde697e5 100644 (file)
--- a/test/regress/regress0/strings/Makefile.am
+++ b/test/regress/regress0/strings/Makefile.am
@@ -50,8 +50,10 @@ TESTS = \
   loop008.smt2 \
   loop009.smt2 \
   reloop.smt2 \
-  unsound-0908.smt2 
-
+  unsound-0908.smt2 \
+  ilc-like.smt2 \ 
+  indexof-sym-simp.smt2 \
+  bug613.smt2
 
 FAILING_TESTS =
 

diff --git a/test/regress/regress0/strings/bug613.smt2 b/test/regress/regress0/strings/bug613.smt2
new file mode 100644 (file)
index 0000000..506076c
--- /dev/null
+++ b/test/regress/regress0/strings/bug613.smt2
@@ -0,0 +1,9 @@
+(set-logic QF_S)
+(set-info :status sat)
+(set-option :strings-exp true)
+
+(declare-fun s () String)
+(assert (= s "<a></a>"))
+(assert (< (str.indexof s "<a>" 0) (str.indexof s "</a>" 0)))
+
+(check-sat)

diff --git a/test/regress/regress0/strings/ilc-like.smt2 b/test/regress/regress0/strings/ilc-like.smt2
new file mode 100755 (executable)
index 0000000..a711c21
--- /dev/null
+++ b/test/regress/regress0/strings/ilc-like.smt2
@@ -0,0 +1,14 @@
+(set-logic ALL_SUPPORTED)\r
+(set-info :status sat)\r
+(set-option :strings-exp true)\r
+ \r
+(declare-fun s () String)\r
+(assert (= s "I like cookies."))\r
+ \r
+(declare-fun target () String)\r
+(assert (= target "like"))\r
+ \r
+(declare-fun location () Int)\r
+(assert (= location (str.indexof s target 0)))\r
+ \r
+(check-sat)
\ No newline at end of file

diff --git a/test/regress/regress0/strings/indexof-sym-simp.smt2 b/test/regress/regress0/strings/indexof-sym-simp.smt2
new file mode 100755 (executable)
index 0000000..7ae60f2
--- /dev/null
+++ b/test/regress/regress0/strings/indexof-sym-simp.smt2
@@ -0,0 +1,10 @@
+(set-logic ALL_SUPPORTED)\r
+(set-info :status unsat)\r
+(set-option :strings-exp true)\r
+(declare-fun s () String)\r
+(declare-fun t () String)\r
+(declare-fun r () String)\r
+; solvable if we do equality reasoning over str.indexof\r
+(assert (= t s))\r
+(assert (not (= (str.indexof t r 0) (str.indexof s r 0))))\r
+(check-sat)
\ No newline at end of file