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.

1 files changed, 19 insertions, 0 deletions

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; }