Fix strings preprocessing + incremental, fixes bug 682. Add initial infrastructure...

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 337c5104ca556f04103ac7ecef0a3993b4ca6a8e..a1eca35fa210e032379be7ac26e9dbb86e929c1a 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -88,7 +88,7 @@
 #include "theory/quantifiers/ce_guided_instantiation.h"
 #include "theory/quantifiers/options.h"
 #include "theory/datatypes/options.h"
-#include "theory/strings/theory_strings_preprocess.h"
+#include "theory/strings/theory_strings.h"
 #include "printer/options.h"
 
 #include "theory/arith/pseudoboolean_proc.h"
@@ -3297,8 +3297,7 @@ void SmtEnginePrivate::processAssertions() {
   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() );
+    ((theory::strings::TheoryStrings*)d_smt.d_theoryEngine->theoryOf(THEORY_STRINGS))->getPreprocess()->simplify( d_assertions.ref() );
     //for (unsigned i = 0; i < d_assertions.size(); ++ i) {
     //  d_assertions.replace( i, Rewriter::rewrite( d_assertions[i] ) );
     //}

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index f4019450de9fc2deca31631b3a345d43da80e805..997c477761d5e75d3472b1340447cc51fcbf1dd5 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -68,7 +68,9 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu
   d_loop_antec(u),
   d_length_intro_vars(u),
   d_registered_terms_cache(u),
+  d_preproc(u),
   d_preproc_cache(u),
+  d_extf_infer_cache(c),
   d_proxy_var(u),
   d_proxy_var_to_length(u),
   d_neg_ctn_eqlen(u),
@@ -2054,8 +2056,8 @@ void TheoryStrings::sendInfer( Node eq_exp, Node eq, const char * c ) {
     Trace("strings-assert") << "(assert (=> " << eq_exp << " " << eq << ")) ; infer " << c << std::endl;
     d_pending.push_back( eq );
     d_pending_exp[eq] = eq_exp;
-    d_infer.push_back(eq);
-    d_infer_exp.push_back(eq_exp);
+    d_infer.push_back( eq );
+    d_infer_exp.push_back( eq_exp );
   }
 }
 
@@ -3832,12 +3834,20 @@ void TheoryStrings::checkExtendedFuncsEval( int effort ) {
   for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){
     if( (*it).second ){
       Node n = (*it).first;
+      int n_pol = 0;
+      if( n.getType().isBoolean() ){
+        if( areEqual( n, d_true ) ){
+          n_pol = 1;
+        }else if( areEqual( n, d_false ) ){
+          n_pol = -1;
+        }
+      }
       Trace("strings-extf-debug") << "Check extf " << n << "..." << std::endl;
       if( effort==0 ){
         std::map< Node, bool > visited;
         collectVars( n, d_extf_vars[n], visited );
       }
-      //build up a best current substitution for the variables in the term
+      //build up a best current substitution for the variables in the term, exp is explanation for substitution
       std::vector< Node > exp;
       std::vector< Node > var;
       std::vector< Node > sub;
@@ -3873,7 +3883,7 @@ void TheoryStrings::checkExtendedFuncsEval( int effort ) {
           }
         }
       }
-
+      Node to_reduce;
       if( !var.empty() ){
         Node nr = n.substitute( var.begin(), var.end(), sub.begin(), sub.end() );
         Node nrc = Rewriter::rewrite( nr );
@@ -3929,16 +3939,46 @@ void TheoryStrings::checkExtendedFuncsEval( int effort ) {
               return;
             }
           }
+        }else if( ( nrc.getKind()==kind::OR && n_pol==-1 ) || ( nrc.getKind()==kind::AND && n_pol==1 ) ){
+          //infer the consequence of each
+          d_ext_func_terms[n] = false;
+          exp.push_back( n_pol==-1 ? n.negate() : n );
+          Trace("strings-extf-debug") << "  decomposable..." << std::endl;
+          Trace("strings-extf") << "  resolve extf : " << nr << " -> " << nrc << ", pol = " << n_pol << std::endl;
+          for( unsigned i=0; i<nrc.getNumChildren(); i++ ){
+            sendInfer( mkAnd( exp ), n_pol==-1 ? nrc[i].negate() : nrc[i], effort==0 ? "EXTF_d" : "EXTF_d-N" );
+          }
         //}else if( hasTerm( nrc ) && !areEqual( nrc, n ) ){
         //  Trace("strings-extf-debug") << "Reduction inference : " << nrc << " " << n << std::endl;  TODO?
         }else{
-          if( effort==1 ){
-            Trace("strings-extf") << "  cannot rewrite extf : " << nrc << std::endl;
-          }
+          to_reduce = nrc;
         }
       }else{
+        to_reduce = n;
+      }
+      if( !to_reduce.isNull() ){
+        //TODO
+        //checkExtfInference( n, to_reduce, n_pol, exp, effort );
         if( effort==1 ){
-          Trace("strings-extf") << "  cannot rewrite extf : " << n << std::endl;
+          Trace("strings-extf") << "  cannot rewrite extf : " << to_reduce << std::endl;
+        }
+      }
+    }
+  }
+}
+
+void TheoryStrings::checkExtfInference( Node n, Node nr, int n_pol, std::vector< Node >& exp, int effort ){
+  if( n_pol!=0 ){
+    if( d_extf_infer_cache.find( nr )==d_extf_infer_cache.end() ){
+      d_extf_infer_cache.insert( nr );
+      if( nr.getKind()==kind::STRING_STRCTN ){
+        if( ( n_pol==1 && nr[1].getKind()==kind::STRING_CONCAT ) || ( n_pol==-1 && nr[0].getKind()==kind::STRING_CONCAT ) ){
+          //one argument does (not) contain each of the components of the other argument
+          exp.push_back( n_pol==1 ? n : n.negate() );
+          int index = n_pol==1 ? 1 : 0;
+          for( unsigned i=0; i<nr[index].getNumChildren(); i++ ){
+            //TODO
+          }
         }
       }
     }

diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 7e09a8e5b10e71367dcaca250bcc5ba90e18fe0f..af06519c058b756b6c7727cca929a02d0b353f89 100644 (file)
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -157,7 +157,7 @@ private:
   std::vector< Node > d_pending;
   std::vector< Node > d_lemma_cache;
   std::map< Node, bool > d_pending_req_phase;
-  /** inferences */
+  /** inferences: maintained to ensure ref count for internally introduced nodes */
   NodeList d_infer;
   NodeList d_infer_exp;
   /** normal forms */
@@ -177,6 +177,8 @@ private:
   // preprocess cache
   StringsPreprocess d_preproc;
   NodeBoolMap d_preproc_cache;
+  // extended functions inferences cache
+  NodeSet d_extf_infer_cache;
 
   bool doPreprocess( Node atom );
   bool hasProcessed();
@@ -277,6 +279,7 @@ private:
   void checkInit();
   void checkConstantEquivalenceClasses( TermIndex* ti, std::vector< Node >& vecc );
   void checkExtendedFuncsEval( int effort = 0 );
+  void checkExtfInference( Node n, Node nr, int n_pol, std::vector< Node >& exp, int effort );
   void collectVars( Node n, std::map< Node, std::vector< Node > >& vars, std::map< Node, bool >& visited );
   void checkNormalForms();
   Node checkCycles( Node eqc, std::vector< Node >& curr, std::vector< Node >& exp );
@@ -319,6 +322,8 @@ public:
   void eqNotifyPostMerge(TNode t1, TNode t2);
   /** called when two equivalence classes are made disequal */
   void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
+  /** get preprocess */
+  StringsPreprocess * getPreprocess() { return &d_preproc; }
 protected:
   /** compute care graph */
   void computeCareGraph();
@@ -360,7 +365,7 @@ protected:
   void printConcat( std::vector< Node >& n, const char * c );
 
   void inferSubstitutionProxyVars( Node n, std::vector< Node >& vars, std::vector< Node >& subs, std::vector< Node >& unproc );
-  
+
   enum {
     sk_id_c_spt,
     sk_id_vc_spt,

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 4e2b00fb1a0d981c25b1a5e77c54a7f47ff6a591..b2b7bac5e3813f592d816d76496f953bfa4bc832 100644 (file)
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -25,7 +25,7 @@ namespace CVC4 {
 namespace theory {
 namespace strings {
 
-StringsPreprocess::StringsPreprocess() {
+StringsPreprocess::StringsPreprocess( context::UserContext* u ) : d_cache( u ){
   //Constants
   d_zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) );
 }
@@ -119,7 +119,9 @@ void StringsPreprocess::processRegExp( Node s, Node r, std::vector< Node > &ret
 bool StringsPreprocess::checkStarPlus( Node t ) {
   if( t.getKind() != kind::REGEXP_STAR && t.getKind() != kind::REGEXP_PLUS ) {
     for( unsigned i = 0; i<t.getNumChildren(); ++i ) {
-      if( checkStarPlus(t[i]) ) return true;
+      if( checkStarPlus(t[i]) ){
+        return true;
+      }
     }
     return false;
   } else {
@@ -151,7 +153,7 @@ int StringsPreprocess::checkFixLenVar( Node t ) {
   return ret;
 }
 Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes, bool during_pp ) {
-  std::hash_map<TNode, Node, TNodeHashFunction>::const_iterator i = d_cache.find(t);
+  NodeNodeMap::const_iterator i = d_cache.find(t);
   if(i != d_cache.end()) {
     return (*i).second.isNull() ? t : (*i).second;
   }
@@ -568,7 +570,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes, bool d
 }
 
 Node StringsPreprocess::decompose(Node t, std::vector< Node > & new_nodes, bool during_pp) {
-  std::hash_map<TNode, Node, TNodeHashFunction>::const_iterator i = d_cache.find(t);
+  NodeNodeMap::const_iterator i = d_cache.find(t);
   if(i != d_cache.end()) {
     return (*i).second.isNull() ? t : (*i).second;
   }

diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h
index 1255d93e0f1aaa005a57c526e101811f4b393263..a5ba1f6158912951e6322d11b2dfaff36895119f 100644 (file)
--- a/src/theory/strings/theory_strings_preprocess.h
+++ b/src/theory/strings/theory_strings_preprocess.h
@@ -23,14 +23,17 @@
 #include "util/hash.h"
 #include "theory/theory.h"
 #include "theory/rewriter.h"
+#include "context/cdchunk_list.h"
+#include "context/cdhashmap.h"
 
 namespace CVC4 {
 namespace theory {
 namespace strings {
 
 class StringsPreprocess {
+  typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
   // NOTE: this class is NOT context-dependent
-  std::hash_map<TNode, Node, TNodeHashFunction> d_cache;
+  NodeNodeMap d_cache;
   //Constants
   Node d_zero;
 private:
@@ -39,7 +42,7 @@ private:
   void processRegExp( Node s, Node r, std::vector< Node > &ret );
   Node simplify( Node t, std::vector< Node > &new_nodes, bool during_pp );
 public:
-  StringsPreprocess();
+  StringsPreprocess( context::UserContext* u );
 
   Node decompose( Node t, std::vector< Node > &new_nodes, bool during_pp = false );
   void simplify(std::vector< Node > &vec_node);

diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
index a8a8e968f0f1367acb019dbaa3df2223fdbf0716..45a7fb802183c2ad8a08ae56a09b806a32cea7fd 100644 (file)
--- a/test/regress/regress0/strings/Makefile.am
+++ b/test/regress/regress0/strings/Makefile.am
@@ -68,7 +68,8 @@ TESTS = \
   bug615.smt2 \
   kaluza-fl.smt2 \
   norn-ab.smt2 \
-  idof-rewrites.smt2
+  idof-rewrites.smt2 \
+  bug682.smt2
 
 FAILING_TESTS =
 

diff --git a/test/regress/regress0/strings/bug682.smt2 b/test/regress/regress0/strings/bug682.smt2
new file mode 100644 (file)
index 0000000..6617b6b
--- /dev/null
+++ b/test/regress/regress0/strings/bug682.smt2
@@ -0,0 +1,19 @@
+; COMMAND-LINE: --incremental --strings-exp
+(set-logic QF_S)
+
+(declare-fun a () String)
+(define-fun replace3 ((x String) (y String) (z String)) String (str.replace x y z) )
+
+(push 1)
+(assert (= (replace3 a "5" "3") "333"))
+(assert (str.contains a "5"))
+; EXPECT: sat
+(check-sat)
+(pop 1)
+
+(push 1)
+(assert (= (replace3 a "5" "3") "333"))
+(assert (str.contains a "5"))
+; EXPECT: sat
+(check-sat)
+(pop 1)