Infer emptiness instead of splitting when a string equality rewrites to a constant (#3218)

4 files changed, 42 insertions, 9 deletions

diff --git a/src/theory/strings/infer_info.cpp b/src/theory/strings/infer_info.cpp
index a20f608a6..b2c88d068 100644
--- a/src/theory/strings/infer_info.cpp
+++ b/src/theory/strings/infer_info.cpp
@@ -24,6 +24,7 @@ std::ostream& operator<<(std::ostream& out, Inference i)
 {
   switch (i)
   {
+    case INFER_INFER_EMP: out << "Infer-Emp"; break;
     case INFER_SSPLIT_CST_PROP: out << "S-Split(CST-P)-prop"; break;
     case INFER_SSPLIT_VAR_PROP: out << "S-Split(VAR)-prop"; break;
     case INFER_LEN_SPLIT: out << "Len-Split(Len)"; break;
diff --git a/src/theory/strings/infer_info.h b/src/theory/strings/infer_info.h
index 9b19eba4b..745a499d3 100644
--- a/src/theory/strings/infer_info.h
+++ b/src/theory/strings/infer_info.h
@@ -33,10 +33,17 @@ namespace strings {
 enum Inference
 {
   INFER_NONE = 0,
+  // infer empty, for example:
+  //     (~) x = ""
+  // This is inferred when we encounter an x such that x = "" rewrites to a
+  // constant. This inference is used for instance when we otherwise would have
+  // split on the emptiness of x but the rewriter tells us the emptiness of x
+  // can be inferred.
+  INFER_INFER_EMP = 1,
   // string split constant propagation, for example:
   //     x = y, x = "abc", y = y1 ++ "b" ++ y2
   //       implies y1 = "a" ++ y1'
-  INFER_SSPLIT_CST_PROP = 1,
+  INFER_SSPLIT_CST_PROP,
   // string split variable propagation, for example:
   //     x = y, x = x1 ++ x2, y = y1 ++ y2, len( x1 ) >= len( y1 )
   //       implies x1 = y1 ++ x1'
diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
index f064a26e2..6cc1e7b44 100644
--- a/src/theory/strings/inference_manager.cpp
+++ b/src/theory/strings/inference_manager.cpp
@@ -106,10 +106,6 @@ void InferenceManager::sendInference(const std::vector<Node>& exp,
                                      bool asLemma)
 {
   eq = eq.isNull() ? d_false : Rewriter::rewrite(eq);
-  if (eq == d_true)
-  {
-    return;
-  }
   if (Trace.isOn("strings-infer-debug"))
   {
     Trace("strings-infer-debug")
@@ -123,6 +119,10 @@ void InferenceManager::sendInference(const std::vector<Node>& exp,
       Trace("strings-infer-debug") << "  N:" << exp_n[i] << std::endl;
     }
   }
+  if (eq == d_true)
+  {
+    return;
+  }
   // check if we should send a lemma or an inference
   if (asLemma || eq == d_false || eq.getKind() == OR || !exp_n.empty()
       || options::stringInferAsLemmas())
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 1eb2e8e00..2f51000ab 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -3160,8 +3160,9 @@ void TheoryStrings::processNEqc(std::vector<NormalForm>& normal_forms)
   unsigned max_index = 0;
   for (unsigned i = 0, size = pinfer.size(); i < size; i++)
   {
-    Trace("strings-solve") << "From " << pinfer[i].d_i << " / " << pinfer[i].d_j
-                           << " (rev=" << pinfer[i].d_rev << ") : ";
+    Trace("strings-solve") << "#" << i << ": From " << pinfer[i].d_i << " / "
+                           << pinfer[i].d_j << " (rev=" << pinfer[i].d_rev
+                           << ") : ";
     Trace("strings-solve") << pinfer[i].d_conc << " by " << pinfer[i].d_id
                            << std::endl;
     if (!set_use_index || pinfer[i].d_id < min_id
@@ -3173,6 +3174,7 @@ void TheoryStrings::processNEqc(std::vector<NormalForm>& normal_forms)
       set_use_index = true;
     }
   }
+  Trace("strings-solve") << "...choose #" << use_index << std::endl;
   doInferInfo(pinfer[use_index]);
 }
 
@@ -3400,9 +3402,32 @@ void TheoryStrings::processSimpleNEq(NormalForm& nfi,
                 Assert( other_str.getKind()!=kind::STRING_CONCAT, "Other string is not CONCAT." );
                 if( !d_equalityEngine.areDisequal( other_str, d_emptyString, true ) ){
                   Node eq = other_str.eqNode( d_emptyString );
+                  eq = Rewriter::rewrite(eq);
+                  if (eq.isConst())
+                  {
+                    // If the equality rewrites to a constant, we must use the
+                    // purify variable for this string to communicate that
+                    // we have inferred whether it is empty.
+                    Node p = d_sk_cache.mkSkolemCached(
+                        other_str, SkolemCache::SK_PURIFY, "lsym");
+                    Node pEq = p.eqNode(d_emptyString);
+                    // should not be constant
+                    Assert(!Rewriter::rewrite(pEq).isConst());
+                    // infer the purification equality, and the (dis)equality
+                    // with the empty string in the direction that the rewriter
+                    // inferred
+                    info.d_conc =
+                        nm->mkNode(AND,
+                                   p.eqNode(other_str),
+                                   !eq.getConst<bool>() ? pEq.negate() : pEq);
+                    info.d_id = INFER_INFER_EMP;
+                  }
+                  else
+                  {
+                    info.d_conc = nm->mkNode(OR, eq, eq.negate());
+                    info.d_id = INFER_LEN_SPLIT_EMP;
+                  }
                   //set info
-                  info.d_conc = NodeManager::currentNM()->mkNode( kind::OR, eq, eq.negate() );
-                  info.d_id = INFER_LEN_SPLIT_EMP;
                   info_valid = true;
                 }else{
                   if( !isRev ){  //FIXME