Fix congruence check in strings, fixes bug 686.

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index d985977d6635948029ddef46c2ec5cd593ad9049..02a1db47a1931cab4834f8a850c42b498f83eaeb 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -71,6 +71,7 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu
   d_preproc(u),
   d_preproc_cache(u),
   d_extf_infer_cache(c),
+  d_congruent(c),
   d_proxy_var(u),
   d_proxy_var_to_length(u),
   d_neg_ctn_eqlen(u),
@@ -571,8 +572,8 @@ void TheoryStrings::check(Effort e) {
 
     bool addedLemma = false;
     bool addedFact;
-    d_congruent.clear();
     do{
+      Trace("strings-process") << "----check, next round---" << std::endl;
       checkInit();
       Trace("strings-process") << "Done check init, addedFact = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl;
       if( !hasProcessed() ){
@@ -873,7 +874,7 @@ bool TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std
   eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
   while( !eqc_i.isFinished() ) {
     Node n = (*eqc_i);
-    if( std::find( d_congruent.begin(), d_congruent.end(), n )==d_congruent.end() ){
+    if( d_congruent.find( n )==d_congruent.end() ){
       if( n.getKind() == kind::CONST_STRING || n.getKind() == kind::STRING_CONCAT ) {
         Trace("strings-process-debug") << "Get Normal Form : Process term " << n << " in eqc " << eqc << std::endl;
         std::vector<Node> nf_n;
@@ -1607,7 +1608,7 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
     eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
     while( !eqc_i.isFinished() ) {
       Node n = (*eqc_i);
-      if( std::find( d_congruent.begin(), d_congruent.end(), n )==d_congruent.end() ){
+      if( d_congruent.find( n )==d_congruent.end() ){
         if( n.getKind()==kind::STRING_CONCAT ){
           //std::vector< Node > exp;
           //exp.push_back( n.eqNode( d_emptyString ) );
@@ -2515,7 +2516,7 @@ Node TheoryStrings::checkCycles( Node eqc, std::vector< Node >& curr, std::vecto
     eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
     while( !eqc_i.isFinished() ) {
       Node n = (*eqc_i);
-      if( std::find( d_congruent.begin(), d_congruent.end(), n )==d_congruent.end() ){
+      if( d_congruent.find( n )==d_congruent.end() ){
         Trace("strings-cycle") << eqc << " check term : " << n << " in " << eqc << std::endl;
         if( n.getKind() == kind::STRING_CONCAT ) {
           if( eqc!=d_emptyString_r ){
@@ -2989,7 +2990,7 @@ bool TheoryStrings::normalizePosMemberships(std::map< Node, std::vector< Node >
         //conflict
         Node antec = exp.size() == 1? exp[0] : NodeManager::currentNM()->mkNode(kind::AND, exp);
         Node conc;
-        sendLemma(antec, conc, "INTERSEC CONFLICT");
+        sendLemma(antec, conc, "INTERSECT CONFLICT");
         addLemma = true;
         break;
       }
@@ -3214,7 +3215,7 @@ void TheoryStrings::checkMemberships() {
               }
               Node antec = vec_nodes.size() == 1? vec_nodes[0] : NodeManager::currentNM()->mkNode(kind::AND, vec_nodes);
               Node conc;
-              sendLemma(antec, conc, "INTERSEC CONFLICT");
+              sendLemma(antec, conc, "INTERSECT CONFLICT");
               addedLemma = true;
               break;
             }
@@ -3232,7 +3233,7 @@ void TheoryStrings::checkMemberships() {
     }
   //}
 
-  Trace("regexp-debug") << "... No Intersec Conflict in Memberships, addedLemma: " << addedLemma << std::endl;
+  Trace("regexp-debug") << "... No Intersect Conflict in Memberships, addedLemma: " << addedLemma << std::endl;
   if(!addedLemma) {
     for( unsigned i=0; i<d_regexp_memberships.size(); i++ ) {
       //check regular expression membership
@@ -3587,7 +3588,7 @@ void TheoryStrings::checkInit() {
         }else if( n.getNumChildren()>0 ){
           Kind k = n.getKind();
           if( k!=kind::EQUAL ){
-            if( std::find( d_congruent.begin(), d_congruent.end(), n )==d_congruent.end() ){
+            if( d_congruent.find( n )==d_congruent.end() ){
               std::vector< Node > c;
               Node nc = d_term_index[k].add( n, 0, this, d_emptyString_r, c );
               if( nc!=n ){
@@ -3633,7 +3634,7 @@ void TheoryStrings::checkInit() {
                 }
                 //this node is congruent to another one, we can ignore it
                 Trace("strings-process-debug") << "  congruent term : " << n << std::endl;
-                d_congruent.push_back( n );
+                d_congruent.insert( n );
                 congruent[k]++;
               }else if( k==kind::STRING_CONCAT && c.size()==1 ){
                 Trace("strings-process-debug") << "  congruent term by singular : " << n << " " << c[0] << std::endl;
@@ -3659,7 +3660,7 @@ void TheoryStrings::checkInit() {
                   //infer the equality
                   sendInfer( mkAnd( exp ), n.eqNode( c[0] ), "I_Norm_S" );
                 }
-                d_congruent.push_back( n );
+                d_congruent.insert( n );
                 congruent[k]++;
               }else{
                 ncongruent[k]++;
@@ -3908,6 +3909,8 @@ void TheoryStrings::checkExtendedFuncsEval( int effort ) {
           Trace("strings-extf") << "  cannot rewrite extf : " << to_reduce << std::endl;
         }
       }
+    }else{
+      Trace("strings-extf-debug")  << "  already reduced " << (*it).first << std::endl;
     }
   }
   /*
@@ -4039,6 +4042,7 @@ void TheoryStrings::checkExtendedFuncs() {
 #ifdef LAZY_ADD_MEMBERSHIP
       for( std::map< bool, std::vector< Node > >::iterator it=pnMem.begin(); it != pnMem.end(); ++it ){
         for( unsigned i=0; i<it->second.size(); i++ ){
+          Trace("strings-process-debug") << "  add membership : " << it->second[i] << ", pol = " << it->first << std::endl;
           addMembership( it->first ? it->second[i] : it->second[i].negate() );
         }
       }

diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index f57bf43f8f70d350215b7b0e284904cc5b8ce8f4..84f137ca54d7fb39c7b7462a1d1d87524d68f0c1 100644 (file)
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -180,7 +180,7 @@ private:
   void addToExplanation( Node lit, std::vector< Node >& exp );
 
 private:
-  std::vector< Node > d_congruent;
+  NodeSet d_congruent;
   std::map< Node, Node > d_eqc_to_const;
   std::map< Node, Node > d_eqc_to_const_base;
   std::map< Node, Node > d_eqc_to_const_exp;

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

diff --git a/test/regress/regress0/strings/bug686dd.smt2 b/test/regress/regress0/strings/bug686dd.smt2
new file mode 100644 (file)
index 0000000..7db4b86
--- /dev/null
+++ b/test/regress/regress0/strings/bug686dd.smt2
@@ -0,0 +1,13 @@
+(set-logic UFDTSLIA)\r
+(set-info :status sat)\r
+\r
+(declare-datatypes () ( (T (TC (TCb String))) ) )\r
+\r
+(declare-fun root5 () String)\r
+(declare-fun root6 () T)\r
+\r
+(assert (and \r
+(str.in.re root5 (re.loop (re.range "0" "9") 4 4) )\r
+(str.in.re (TCb root6) (re.loop (re.range "0" "9") 4 4) )\r
+) )\r
+(check-sat)\r