Normal form equality conflicts and uniqueness check (#4497)

This adds a new inference schema to strings that was discovered by the internal proof checker. It says that we are in conflict when an equality between the normal forms of two terms in the same equivalence class rewrites to false.

It also improves the efficiency of processing normal forms by only considering normal forms that are unique up to rewriting.

4 files changed, 126 insertions, 49 deletions

diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index 9989c89f4..aca43e8c8 100644
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -618,7 +618,7 @@ void CoreSolver::normalizeEquivalenceClass(Node eqc, TypeNode stype)
       return;
     }
     // process the normal forms
-    processNEqc(normal_forms, stype);
+    processNEqc(eqc, normal_forms, stype);
     if (d_im.hasProcessed())
     {
       return;
@@ -879,81 +879,151 @@ void CoreSolver::getNormalForms(Node eqc,
           }
         }
         Trace("strings-solve") << std::endl;
-        
       }
     } else {
       Trace("strings-solve") << "--- Single normal form for equivalence class " << eqc << std::endl;
     }
-    
-    //if equivalence class is constant, approximate as containment, infer conflicts
-    Node c = d_bsolver.getConstantEqc( eqc );
-    if( !c.isNull() ){
-      Trace("strings-solve") << "Eqc is constant " << c << std::endl;
-      for (unsigned i = 0, size = normal_forms.size(); i < size; i++)
+  }
+}
+
+void CoreSolver::processNEqc(Node eqc,
+                             std::vector<NormalForm>& normal_forms,
+                             TypeNode stype)
+{
+  if (normal_forms.size() <= 1)
+  {
+    return;
+  }
+  // if equivalence class is constant, approximate as containment, infer
+  // conflicts
+  Node c = d_bsolver.getConstantEqc(eqc);
+  // the possible inferences
+  std::vector<CoreInferInfo> pinfer;
+  // compute normal forms that are effectively unique
+  std::unordered_map<Node, size_t, NodeHashFunction> nfCache;
+  std::vector<size_t> nfIndices;
+  bool hasConstIndex = false;
+  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())
+    {
+      // If the equivalence class is entailed to be constant, check
+      // if the normal form cannot be contained in that constant.
+      if (!c.isNull())
       {
-        NormalForm& nf = normal_forms[i];
         int firstc, lastc;
-        if (!StringsEntail::canConstantContainList(c, nf.d_nf, firstc, lastc))
+        if (!StringsEntail::canConstantContainList(c, nfi.d_nf, firstc, lastc))
         {
-          Node n = nf.d_base;
+          Node n = nfi.d_base;
           //conflict
           Trace("strings-solve") << "Normal form for " << n << " cannot be contained in constant " << c << std::endl;
-          //conflict, explanation is n = base ^ base = c ^ relevant porition of ( n = N[n] )
+          // conflict, explanation is:
+          //  n = base ^ base = c ^ relevant porition of ( n = N[n] )
           std::vector< Node > exp;
           d_bsolver.explainConstantEqc(n,eqc,exp);
           // Notice although not implemented, this can be minimized based on
           // firstc/lastc, normal_forms_exp_depend.
-          exp.insert(exp.end(), nf.d_exp.begin(), nf.d_exp.end());
-          Node conc = d_false;
-          d_im.sendInference(exp, conc, Inference::N_NCTN);
+          exp.insert(exp.end(), nfi.d_exp.begin(), nfi.d_exp.end());
+          d_im.sendInference(exp, d_false, Inference::N_NCTN);
+          return;
         }
       }
+
+      nfCache[ni] = i;
+      if (ni.isConst())
+      {
+        hasConstIndex = true;
+        nfIndices.insert(nfIndices.begin(), i);
+      }
+      else
+      {
+        nfIndices.push_back(i);
+      }
     }
   }
-}
+  size_t nnfs = nfIndices.size();
+  Trace("strings-solve") << "CoreSolver::processNEqc: " << nnfs << "/"
+                         << normal_forms.size() << " normal forms are unique."
+                         << std::endl;
 
-void CoreSolver::processNEqc(std::vector<NormalForm>& normal_forms,
-                             TypeNode stype)
-{
-  //the possible inferences
-  std::vector<CoreInferInfo> pinfer;
-  // loop over all pairs 
-  for(unsigned i=0; i<normal_forms.size()-1; i++) {
+  // loop over all pairs
+  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;
       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 (hasConstIndex || d_im.hasProcessed())
+    {
+      break;
+    }
+  }
+  if (d_state.isInConflict())
+  {
+    // conflict, we are done
+    return;
+  }
+  // Go back and check for normal form equality conflicts. These take
+  // precedence over any facts and lemmas.
+  for (const std::pair<const Node, size_t>& ni : nfCache)
+  {
+    for (const std::pair<const Node, size_t>& nj : nfCache)
+    {
+      if (ni.first >= nj.first)
+      {
+        // avoid duplicate comparisons
+        continue;
+      }
+      Node eq = ni.first.eqNode(nj.first);
+      eq = Rewriter::rewrite(eq);
+      if (eq == d_false)
+      {
+        std::vector<Node> exp;
+        NormalForm& nfi = normal_forms[ni.second];
+        NormalForm& nfj = normal_forms[nj.second];
+        exp.insert(exp.end(), nfi.d_exp.begin(), nfi.d_exp.end());
+        exp.insert(exp.end(), nfj.d_exp.begin(), nfj.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())
+  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/core_solver.h b/src/theory/strings/core_solver.h
index 4328b8462..029f1c850 100644
--- a/src/theory/strings/core_solver.h
+++ b/src/theory/strings/core_solver.h
@@ -275,7 +275,7 @@ class CoreSolver
                       TypeNode stype);
   /** process normalize equivalence class
    *
-   * This is called when an equivalence class contains a set of terms that
+   * This is called when an equivalence class eqc contains a set of terms that
    * have normal forms given by the argument normal_forms. It either
    * verifies that all normal forms in this vector are identical, or otherwise
    * adds a conflict, lemma, or inference via the sendInference method.
@@ -288,7 +288,9 @@ class CoreSolver
    *
    * stype is the string-like type of the equivalence class we are processing.
    */
-  void processNEqc(std::vector<NormalForm>& normal_forms, TypeNode stype);
+  void processNEqc(Node eqc,
+                   std::vector<NormalForm>& normal_forms,
+                   TypeNode stype);
   /** process simple normal equality
    *
    * This method is called when two equal terms have normal forms nfi and nfj.
diff --git a/src/theory/strings/infer_info.cpp b/src/theory/strings/infer_info.cpp
index 9c4ebafa1..e26a49e4e 100644
--- a/src/theory/strings/infer_info.cpp
+++ b/src/theory/strings/infer_info.cpp
@@ -35,6 +35,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 fca528d1b..5aecf52cb 100644
--- a/src/theory/strings/infer_info.h
+++ b/src/theory/strings/infer_info.h
@@ -92,6 +92,10 @@ enum class Inference : uint32_t
   // Flat form not contained
   // x = c ^ x = y => false when rewrite( contains( y, c ) ) = false
   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 = ""