Bug fix negative contains cache.

1 files changed, 72 insertions, 66 deletions

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 0a5b27772..34ca52419 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -3282,10 +3282,11 @@ bool TheoryStrings::checkPosContains() {
 
 bool TheoryStrings::checkNegContains() {
   bool addedLemma = false;
+  //check for conflicts
   for( unsigned i=0; i<d_str_neg_ctn.size(); i++ ){
     if( !d_conflict ){
       Node atom = d_str_neg_ctn[i];
-      Trace("strings-ctn") << "We have nagetive contain assertion : (not " << atom << " )" << std::endl;
+      Trace("strings-ctn") << "We have negative contain assertion : (not " << atom << " )" << std::endl;
       if( areEqual( atom[1], d_emptyString ) ) {
         Node ant = NodeManager::currentNM()->mkNode( kind::AND, atom.negate(), atom[1].eqNode( d_emptyString ) );
         Node conc = Node::null();
@@ -3296,77 +3297,82 @@ bool TheoryStrings::checkNegContains() {
         Node conc = Node::null();
         sendLemma( ant, conc, "NEG-CTN Conflict 2" );
         addedLemma = true;
-      } else {
-        if(options::stringExp()) {
-          Node x = atom[0];
-          Node s = atom[1];
-          Node lenx = getLength(x);
-          Node lens = getLength(s);
-          if(areEqual(lenx, lens)) {
-            if(d_neg_ctn_eqlen.find(atom) == d_neg_ctn_eqlen.end()) {
-              Node eq = lenx.eqNode(lens);
-              Node antc = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, atom.negate(), eq ) );
-              Node xneqs = x.eqNode(s).negate();
-              d_neg_ctn_eqlen.insert( atom );
-              sendLemma( antc, xneqs, "NEG-CTN-EQL" );
-              addedLemma = true;
-            }
-          } else if(!areDisequal(lenx, lens)) {
-            if(d_neg_ctn_ulen.find(atom) == d_neg_ctn_ulen.end()) {
-              lenx = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, x);
-              lens = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s);
-              d_neg_ctn_ulen.insert( atom );
-              sendSplit(lenx, lens, "NEG-CTN-SP");
-              addedLemma = true;
-            }
-          } else {
-            if(d_neg_ctn_cached.find(atom) == d_neg_ctn_cached.end()) {
-              lenx = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, x);
-              lens = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s);
-              Node b1 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
-              Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b1);
-              Node g1 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode( kind::GEQ, b1, d_zero ),
-                    NodeManager::currentNM()->mkNode( kind::GEQ, NodeManager::currentNM()->mkNode( kind::MINUS, lenx, lens ), b1 ) ) );
-              Node b2 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
-              Node s2 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, x, NodeManager::currentNM()->mkNode( kind::PLUS, b1, b2 ), d_one);
-              Node s5 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, s, b2, d_one);
-
-              Node b2v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b2);//, s1, s3, s4, s6);
-
-              std::vector< Node > vec_nodes;
-              Node cc = NodeManager::currentNM()->mkNode( kind::GEQ, b2, d_zero );
-              vec_nodes.push_back(cc);
-              cc = NodeManager::currentNM()->mkNode( kind::GT, lens, b2 );
-              vec_nodes.push_back(cc);
-
-              cc = s2.eqNode(s5).negate();
-              vec_nodes.push_back(cc);
-
-              Node conc = NodeManager::currentNM()->mkNode(kind::AND, vec_nodes);
-              conc = NodeManager::currentNM()->mkNode( kind::EXISTS, b2v, conc );
-              conc = NodeManager::currentNM()->mkNode( kind::IMPLIES, g1, conc );
-              conc = NodeManager::currentNM()->mkNode( kind::FORALL, b1v, conc );
-              Node xlss = NodeManager::currentNM()->mkNode( kind::GT, lens, lenx );
-              conc = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::OR, xlss, conc ) );
-
-              d_neg_ctn_cached.insert( atom );
-              sendLemma( atom.negate(), conc, "NEG-CTN-BRK" );
-              //d_pending_req_phase[xlss] = true;
-              addedLemma = true;
-            }
+      } 
+    }
+  }
+  if( !d_conflict ){
+    //check for lemmas
+    if(options::stringExp()) {
+      for( unsigned i=0; i<d_str_neg_ctn.size(); i++ ){
+        Node atom = d_str_neg_ctn[i];
+        Node x = atom[0];
+        Node s = atom[1];
+        Node lenx = getLength(x);
+        Node lens = getLength(s);
+        if(areEqual(lenx, lens)) {
+          if(d_neg_ctn_eqlen.find(atom) == d_neg_ctn_eqlen.end()) {
+            Node eq = lenx.eqNode(lens);
+            Node antc = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, atom.negate(), eq ) );
+            Node xneqs = x.eqNode(s).negate();
+            d_neg_ctn_eqlen.insert( atom );
+            sendLemma( antc, xneqs, "NEG-CTN-EQL" );
+            addedLemma = true;
+          }
+        } else if(!areDisequal(lenx, lens)) {
+          if(d_neg_ctn_ulen.find(atom) == d_neg_ctn_ulen.end()) {
+            lenx = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, x);
+            lens = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s);
+            d_neg_ctn_ulen.insert( atom );
+            sendSplit(lenx, lens, "NEG-CTN-SP");
+            addedLemma = true;
           }
         } else {
-          throw LogicException("Strings Incomplete (due to Negative Contain) by default, try --strings-exp option.");
+          if(d_neg_ctn_cached.find(atom) == d_neg_ctn_cached.end()) {
+            lenx = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, x);
+            lens = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s);
+            Node b1 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
+            Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b1);
+            Node g1 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode( kind::GEQ, b1, d_zero ),
+                  NodeManager::currentNM()->mkNode( kind::GEQ, NodeManager::currentNM()->mkNode( kind::MINUS, lenx, lens ), b1 ) ) );
+            Node b2 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
+            Node s2 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, x, NodeManager::currentNM()->mkNode( kind::PLUS, b1, b2 ), d_one);
+            Node s5 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, s, b2, d_one);
+
+            Node b2v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b2);//, s1, s3, s4, s6);
+
+            std::vector< Node > vec_nodes;
+            Node cc = NodeManager::currentNM()->mkNode( kind::GEQ, b2, d_zero );
+            vec_nodes.push_back(cc);
+            cc = NodeManager::currentNM()->mkNode( kind::GT, lens, b2 );
+            vec_nodes.push_back(cc);
+
+            cc = s2.eqNode(s5).negate();
+            vec_nodes.push_back(cc);
+
+            Node conc = NodeManager::currentNM()->mkNode(kind::AND, vec_nodes);
+            conc = NodeManager::currentNM()->mkNode( kind::EXISTS, b2v, conc );
+            conc = NodeManager::currentNM()->mkNode( kind::IMPLIES, g1, conc );
+            conc = NodeManager::currentNM()->mkNode( kind::FORALL, b1v, conc );
+            Node xlss = NodeManager::currentNM()->mkNode( kind::GT, lens, lenx );
+            conc = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::OR, xlss, conc ) );
+
+            d_neg_ctn_cached.insert( atom );
+            sendLemma( atom.negate(), conc, "NEG-CTN-BRK" );
+            //d_pending_req_phase[xlss] = true;
+            addedLemma = true;
+          }
         }
       }
+      if( addedLemma ){
+        doPendingLemmas();
+      }
+    } else {
+      if( !d_str_neg_ctn.empty() ){
+        throw LogicException("Strings Incomplete (due to Negative Contain) by default, try --strings-exp option.");
+      }
     }
   }
-  if( addedLemma ){
-    doPendingLemmas();
-    return true;
-  } else {
-    return false;
-  }
+  return addedLemma;
 }
 
 CVC4::String TheoryStrings::getHeadConst( Node x ) {