New inference, option

4 files changed, 87 insertions, 27 deletions

diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml
index 44ca2c390..1d5f9286c 100644
--- a/src/options/strings_options.toml
+++ b/src/options/strings_options.toml
@@ -91,6 +91,15 @@ header = "options/strings_options.h"
   help       = "strings eager length lemmas"
 
 [[option]]
+  name       = "stringNfEqConflict"
+  category   = "regular"
+  long       = "strings-nf-eq-conf"
+  type       = "bool"
+  default    = "true"
+  read_only  = true
+  help       = "strings normal form equality conflict"
+
+[[option]]
   name       = "stringCheckEntailLen"
   category   = "regular"
   long       = "strings-check-entail-len"
diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index 1afdb6068..621653c52 100644
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -914,27 +914,53 @@ void CoreSolver::getNormalForms(Node eqc,
 void CoreSolver::processNEqc(std::vector<NormalForm>& normal_forms,
                              TypeNode stype)
 {
+  if (normal_forms.size()<=1)
+  {
+    return;
+  }
   //the possible inferences
   std::vector<CoreInferInfo> pinfer;
   // compute normal forms that are effectively unique
-  std::unordered_set<Node,NodeHashFunction> nfCache;
+  std::unordered_map<Node,size_t,NodeHashFunction> nfCache;
   std::vector<size_t> nfIndices;
-  for (size_t i=0, nnforms=normal_forms.size(); i++)
+  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::mkConcat(nfi.d_nf,stype);
+    Node ni = utils::mkNConcat(nfi.d_nf,stype);
     if (nfCache.find(ni)==nfCache.end())
     {
-      nfCache.insert(ni);
+      // compare against previous to see if already conflicting
+      if (options::stringNfEqConflict() && !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;
   
   // loop over all pairs 
-  for(unsigned i=0; i<nnfs-1; i++) {
+  for(unsigned i=0; i<nnfs-1; i++) 
+  {
     //unify each normalform[j] with normal_forms[i]
-    for(unsigned j=i+1; j<nnfs; 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
@@ -942,32 +968,54 @@ void CoreSolver::processNEqc(std::vector<NormalForm>& normal_forms,
       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
+    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 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..6503fd12f 100644
--- a/src/theory/strings/infer_info.h
+++ b/src/theory/strings/infer_info.h
@@ -92,6 +92,8 @@ 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
+  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 = ""