Explain non-emptiness by non-zero length in strings (#4257)

Several kinds of splitting lemmas in the strings solver can sometimes be avoided by observing that str.len(x) != 0 implies that x is non-empty. This generalizes the check for whether x is non-empty is explainable in the current context.

3 files changed, 45 insertions, 12 deletions

diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index 89d4a6f0c..abcd8189a 100644
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -987,7 +987,6 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
                                   TypeNode stype)
 {
   NodeManager* nm = NodeManager::currentNM();
-  eq::EqualityEngine* ee = d_state.getEqualityEngine();
   Node emp = Word::mkEmptyWord(stype);
 
   const std::vector<Node>& nfiv = nfi.d_nf;
@@ -1238,7 +1237,9 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
       Node nc = nfncv[index];
       Assert(!nc.isConst()) << "Other string is not constant.";
       Assert(nc.getKind() != STRING_CONCAT) << "Other string is not CONCAT.";
-      if (!ee->areDisequal(nc, emp, true))
+      // explanation for why nc is non-empty
+      Node expNonEmpty = d_state.explainNonEmpty(nc);
+      if (expNonEmpty.isNull())
       {
         // The non-constant side may be equal to the empty string. Split on
         // whether it is.
@@ -1273,8 +1274,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
 
       // At this point, we know that `nc` is non-empty, so we add that to our
       // explanation.
-      Node ncnz = nc.eqNode(emp).negate();
-      info.d_ant.push_back(ncnz);
+      info.d_ant.push_back(expNonEmpty);
 
       size_t ncIndex = index + 1;
       Node nextConstStr = nfnc.collectConstantStringAt(ncIndex);
@@ -1414,13 +1414,14 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
     for (unsigned xory = 0; xory < 2; xory++)
     {
       Node t = xory == 0 ? x : y;
-      Node tnz = x.eqNode(emp).negate();
-      if (ee->areDisequal(x, emp, true))
+      Node tnz = d_state.explainNonEmpty(x);
+      if (!tnz.isNull())
       {
         info.d_ant.push_back(tnz);
       }
       else
       {
+        tnz = x.eqNode(emp).negate();
         info.d_antn.push_back(tnz);
       }
     }
@@ -1566,7 +1567,8 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi,
     // the equality could rewrite to false
     if (!split_eqr.isConst())
     {
-      if (!d_state.areDisequal(t, emp))
+      Node expNonEmpty = d_state.explainNonEmpty(t);
+      if (expNonEmpty.isNull())
       {
         // try to make t equal to empty to avoid loop
         info.d_conc = nm->mkNode(kind::OR, split_eq, split_eq.negate());
@@ -1575,7 +1577,7 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi,
       }
       else
       {
-        info.d_ant.push_back(split_eq.negate());
+        info.d_ant.push_back(expNonEmpty);
       }
     }
     else
@@ -1701,7 +1703,6 @@ void CoreSolver::processDeq(Node ni, Node nj)
   NodeManager* nm = NodeManager::currentNM();
   NormalForm& nfni = getNormalForm(ni);
   NormalForm& nfnj = getNormalForm(nj);
-  eq::EqualityEngine* ee = d_state.getEqualityEngine();
 
   if (nfni.d_nf.size() <= 1 && nfnj.d_nf.size() <= 1)
   {
@@ -1782,8 +1783,8 @@ void CoreSolver::processDeq(Node ni, Node nj)
         Node ck = x.isConst() ? x : y;
         Node nck = x.isConst() ? y : x;
         Node nckLenTerm = x.isConst() ? yLenTerm : xLenTerm;
-        Node emp = Word::mkEmptyWord(nck.getType());
-        if (!ee->areDisequal(nck, emp, true))
+        Node expNonEmpty = d_state.explainNonEmpty(nck);
+        if (expNonEmpty.isNull())
         {
           // Either `x` or `y` is a constant and the other may be equal to the
           // empty string in the current context. We split on whether it
@@ -1791,6 +1792,7 @@ void CoreSolver::processDeq(Node ni, Node nj)
           //
           // E.g. x ++ x' ++ ... != "abc" ++ y' ++ ... ^ len(x) != len(y) --->
           //      x = "" v x != ""
+          Node emp = Word::mkEmptyWord(nck.getType());
           d_im.sendSplit(nck, emp, Inference::DEQ_DISL_EMP_SPLIT);
           return;
         }
@@ -1847,7 +1849,7 @@ void CoreSolver::processDeq(Node ni, Node nj)
               nck.eqNode(nm->mkNode(kind::STRING_CONCAT, firstChar, skr));
           std::vector<Node> antec(nfni.d_exp.begin(), nfni.d_exp.end());
           antec.insert(antec.end(), nfnj.d_exp.begin(), nfnj.d_exp.end());
-          antec.push_back(nck.eqNode(emp).negate());
+          antec.push_back(expNonEmpty);
           d_im.sendInference(
               antec,
               nm->mkNode(
diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp
index 30acba9fd..55539c802 100644
--- a/src/theory/strings/solver_state.cpp
+++ b/src/theory/strings/solver_state.cpp
@@ -15,6 +15,7 @@
 #include "theory/strings/solver_state.h"
 
 #include "theory/strings/theory_strings_utils.h"
+#include "theory/strings/word.h"
 
 using namespace std;
 using namespace CVC4::context;
@@ -34,7 +35,9 @@ SolverState::SolverState(context::Context* c,
       d_conflict(c, false),
       d_pendingConflict(c)
 {
+  d_zero = NodeManager::currentNM()->mkConst(Rational(0));
 }
+
 SolverState::~SolverState()
 {
   for (std::pair<const Node, EqcInfo*>& it : d_eqcInfo)
@@ -240,6 +243,22 @@ Node SolverState::getLength(Node t, std::vector<Node>& exp)
   return getLengthExp(t, exp, t);
 }
 
+Node SolverState::explainNonEmpty(Node s)
+{
+  Assert(s.getType().isStringLike());
+  Node emp = Word::mkEmptyWord(s.getType());
+  if (areDisequal(s, emp))
+  {
+    return s.eqNode(emp).negate();
+  }
+  Node sLen = utils::mkNLength(s);
+  if (areDisequal(sLen, d_zero))
+  {
+    return sLen.eqNode(d_zero).negate();
+  }
+  return Node::null();
+}
+
 void SolverState::setConflict() { d_conflict = true; }
 bool SolverState::isInConflict() const { return d_conflict; }
 
diff --git a/src/theory/strings/solver_state.h b/src/theory/strings/solver_state.h
index e3fe432d3..623a06941 100644
--- a/src/theory/strings/solver_state.h
+++ b/src/theory/strings/solver_state.h
@@ -118,6 +118,16 @@ class SolverState
   Node getLengthExp(Node t, std::vector<Node>& exp, Node te);
   /** shorthand for getLengthExp(t, exp, t) */
   Node getLength(Node t, std::vector<Node>& exp);
+  /** explain non-empty
+   *
+   * This returns an explanation of why string-like term is non-empty in the
+   * current context, if such an explanation exists. Otherwise, this returns
+   * the null node.
+   *
+   * Note that an explanation is a (conjunction of) literals that currently hold
+   * in the equality engine.
+   */
+  Node explainNonEmpty(Node s);
   /**
    * Get the above information for equivalence class eqc. If doMake is true,
    * we construct a new information class if one does not exist. The term eqc
@@ -153,6 +163,8 @@ class SolverState
                         std::vector<std::vector<Node> >& cols,
                         std::vector<Node>& lts);
  private:
+  /** Common constants */
+  Node d_zero;
   /** Pointer to the SAT context object used by the theory of strings. */
   context::Context* d_context;
   /** Reference to equality engine of the theory of strings. */