From 6b599f87b18186b811f187789e48c1e8c0774534 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 10 Apr 2020 11:15:22 -0500 Subject: [PATCH] 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. --- src/theory/strings/core_solver.cpp | 26 ++++++++++++++------------ src/theory/strings/solver_state.cpp | 19 +++++++++++++++++++ src/theory/strings/solver_state.h | 12 ++++++++++++ 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& 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 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& it : d_eqcInfo) @@ -240,6 +243,22 @@ Node SolverState::getLength(Node t, std::vector& 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& exp, Node te); /** shorthand for getLengthExp(t, exp, t) */ Node getLength(Node t, std::vector& 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 >& cols, std::vector& 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. */ -- 2.30.2