Normal form equality conflicts

4 files changed, 95 insertions, 36 deletions

diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index 0334fa772..112ec2347 100644
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -1006,55 +1006,108 @@ void CoreSolver::getNormalForms(Node eqc,
 void CoreSolver::processNEqc(std::vector<NormalForm>& normal_forms,
                              TypeNode stype)
 {
+  if (normal_forms.size()<=1)
+  {
+    return;
+  }
+  // compute normal forms that are effectively unique
+  std::unordered_map<Node,size_t,NodeHashFunction> nfCache;
+  std::vector<size_t> nfIndices;
+  bool foundConflict = false;
+  size_t nfConfJ = 0;
+  size_t nfConfI = 0;
+  for (size_t i=0, nnforms=normal_forms.size(); i<nnforms; i++)
+  {
+    NormalForm& nfi = normal_forms[i];
+    Node ni = utils::mkNConcat(nfi.d_nf,stype);
+    if (nfCache.find(ni)==nfCache.end())
+    {
+      // compare against previous to see if already conflicting
+      if (!foundConflict)
+      {
+        for (const std::pair<const Node, size_t >& nj : nfCache)
+        {
+          Node eq = ni.eqNode(nj.first);
+          eq = Rewriter::rewrite(eq);
+          if (eq==d_false)
+          {
+            nfConfJ = nj.second;
+            nfConfI = i;
+            foundConflict = true;
+            break;
+          }
+        }
+      }
+      nfCache[ni] = i;
+      nfIndices.push_back(i);
+    }
+  }
+  size_t nnfs = nfIndices.size();
+  Trace("strings-solve") << "CoreSolver::processNEqc: " << nnfs << "/" << normal_forms.size() << " normal forms are unique." << std::endl;
+
   //the possible inferences
   std::vector<CoreInferInfo> pinfer;
   // loop over all pairs 
-  for(unsigned i=0; i<normal_forms.size()-1; i++) {
+  for(unsigned i=0; i<nnfs-1; i++) 
+  {
     //unify each normalform[j] with normal_forms[i]
-    for(unsigned j=i+1; j<normal_forms.size(); j++ ) {
-      NormalForm& nfi = normal_forms[i];
-      NormalForm& nfj = normal_forms[j];
+    for(unsigned j=i+1; j<nnfs; j++ ) 
+    {
+      NormalForm& nfi = normal_forms[nfIndices[i]];
+      NormalForm& nfj = normal_forms[nfIndices[j]];
       //ensure that normal_forms[i] and normal_forms[j] are the same modulo equality, add to pinfer if not
       Trace("strings-solve") << "Strings: Process normal form #" << i << " against #" << j << "..." << std::endl;
-      /*
-      Node nti = utils::mkConcat(nfi.d_nf,stype);
-      Node ntj = utils::mkConcat(nfi.d_nf,stype);
-      Node eq = nti.eqNode(ntj);
-      Node eqr = Rewriter::rewrite(eq);
-      if (eqr==d_false)
-      {
-        AlwaysAssert(false);
-      }
-      */
       if (isNormalFormPair(nfi.d_base, nfj.d_base))
       {
         Trace("strings-solve") << "Strings: Already cached." << std::endl;
-      }else{
-        //process the reverse direction first (check for easy conflicts and inferences)
-        unsigned rindex = 0;
-        nfi.reverse();
-        nfj.reverse();
-        processSimpleNEq(nfi, nfj, rindex, true, 0, pinfer, stype);
-        nfi.reverse();
-        nfj.reverse();
-        if (d_im.hasProcessed())
-        {
-          return;
-        }
-        //AJR: for less aggressive endpoint inference
-        //rindex = 0;
+        continue;
+      }
+      //process the reverse direction first (check for easy conflicts and inferences)
+      unsigned rindex = 0;
+      nfi.reverse();
+      nfj.reverse();
+      processSimpleNEq(nfi, nfj, rindex, true, 0, pinfer, stype);
+      nfi.reverse();
+      nfj.reverse();
+      if (d_im.hasProcessed())
+      {
+        break;
+      }
+      //AJR: for less aggressive endpoint inference
+      //rindex = 0;
 
-        unsigned index = 0;
-        processSimpleNEq(nfi, nfj, index, false, rindex, pinfer, stype);
-        if (d_im.hasProcessed())
-        {
-          return;
-        }
+      unsigned index = 0;
+      processSimpleNEq(nfi, nfj, index, false, rindex, pinfer, stype);
+      if (d_im.hasProcessed())
+      {
+        break;
       }
     }
+    if (d_im.hasProcessed())
+    {
+      break;
+    }
+  }
+  if (d_state.isInConflict())
+  {
+    // conflict, we are done
+    return;
+  }
+  else if (foundConflict)
+  {
+    // normal form equality conflict takes precedence over lemmas and facts
+    std::vector<Node> exp;
+    NormalForm& nfj = normal_forms[nfConfJ];
+    NormalForm& nfi = normal_forms[nfConfI];
+    exp.insert(exp.end(),nfj.d_exp.begin(),nfj.d_exp.end());
+    exp.insert(exp.end(),nfi.d_exp.begin(),nfi.d_exp.end());
+    exp.push_back(nfi.d_base.eqNode(nfj.d_base));
+    d_im.sendInference(exp, d_false, Inference::N_EQ_CONF);
+    return;
   }
-  if (pinfer.empty())
+  else if (d_im.hasProcessed() || pinfer.empty())
   {
+    // either already sent a lemma or fact, or there are no possible inferences
     return;
   }
   // now, determine which of the possible inferences we want to add
diff --git a/src/theory/strings/infer_info.cpp b/src/theory/strings/infer_info.cpp
index 03cf23783..18fe9bc56 100644
--- a/src/theory/strings/infer_info.cpp
+++ b/src/theory/strings/infer_info.cpp
@@ -37,6 +37,7 @@ const char* toString(Inference i)
     case Inference::F_ENDPOINT_EMP: return "F_ENDPOINT_EMP";
     case Inference::F_ENDPOINT_EQ: return "F_ENDPOINT_EQ";
     case Inference::F_NCTN: return "F_NCTN";
+    case Inference::N_EQ_CONF: return "N_EQ_CONF";
     case Inference::N_ENDPOINT_EMP: return "N_ENDPOINT_EMP";
     case Inference::N_UNIFY: return "N_UNIFY";
     case Inference::N_ENDPOINT_EQ: return "N_ENDPOINT_EQ";
diff --git a/src/theory/strings/infer_info.h b/src/theory/strings/infer_info.h
index 1b190a2db..b7e292226 100644
--- a/src/theory/strings/infer_info.h
+++ b/src/theory/strings/infer_info.h
@@ -107,6 +107,10 @@ enum class Inference : uint32_t
   // x = c ^ x = y => false when rewrite( contains( y, c ) ) = false
   // Proof: substitution+rewriting, CTN_NOT_EQUAL
   F_NCTN,
+  // Normal form equality conflict
+  //   x = N[x] ^ y = N[y] ^ x=y => false
+  // where Rewriter::rewrite(N[x]=N[y]) = false.
+  N_EQ_CONF,
   // Given two normal forms, infers that the remainder one of them has to be
   // empty. For example:
   //    If x1 ++ x2 = y1 and x1 = y1, then x2 = ""
diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp
index 636390d8d..e3d0a1a6c 100644
--- a/src/theory/strings/infer_proof_cons.cpp
+++ b/src/theory/strings/infer_proof_cons.cpp
@@ -166,6 +166,7 @@ Node InferProofCons::convert(Inference infer,
     case Inference::F_UNIFY:
     case Inference::F_ENDPOINT_EMP:
     case Inference::F_ENDPOINT_EQ:
+    case Inference::N_EQ_CONF:
     case Inference::N_CONST:
     case Inference::N_UNIFY:
     case Inference::N_ENDPOINT_EMP:
@@ -305,7 +306,7 @@ Node InferProofCons::convert(Inference infer,
           // 2+ children.
         }
       }
-      else if (infer == Inference::N_CONST || infer == Inference::F_CONST)
+      else if (infer == Inference::N_CONST || infer == Inference::F_CONST || infer == Inference::N_EQ_CONF)
       {
         // should be a constant conflict
         std::vector<Node> childrenC;