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, 12 insertions, 0 deletions

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. */