diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-04-10 11:15:22 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-04-10 11:15:22 -0500 |
commit | 6b599f87b18186b811f187789e48c1e8c0774534 (patch) | |
tree | 009cae522584f5268cd3ed18dc183ffc337fc85e /src/theory/strings/solver_state.h | |
parent | 854d36b3ebb85579eefd654a18ed882b99649fb5 (diff) |
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.
Diffstat (limited to 'src/theory/strings/solver_state.h')
-rw-r--r-- | src/theory/strings/solver_state.h | 12 |
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. */ |