From: Andrew Reynolds Date: Tue, 26 May 2020 17:41:31 +0000 (-0500) Subject: Convert more uses of strings to words (#4527) X-Git-Tag: cvc5-1.0.0~3286 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=114a215e9b33effb361c4b000fb23085ce9f079a;p=cvc5.git Convert more uses of strings to words (#4527) --- diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp index df5263c45..16c83de78 100644 --- a/src/theory/strings/base_solver.cpp +++ b/src/theory/strings/base_solver.cpp @@ -33,7 +33,6 @@ BaseSolver::BaseSolver(context::Context* c, InferenceManager& im) : d_state(s), d_im(im), d_congruent(c) { - d_emptyString = NodeManager::currentNM()->mkConst(::CVC4::String("")); d_false = NodeManager::currentNM()->mkConst(false); d_cardSize = utils::getAlphabetCardinality(); } @@ -50,7 +49,6 @@ void BaseSolver::checkInit() std::map ncongruent; std::map congruent; eq::EqualityEngine* ee = d_state.getEqualityEngine(); - Assert(d_state.getRepresentative(d_emptyString) == d_emptyString); eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee); while (!eqcs_i.isFinished()) { @@ -58,9 +56,11 @@ void BaseSolver::checkInit() TypeNode tn = eqc.getType(); if (!tn.isRegExp()) { + Node emps; if (tn.isString()) { d_stringsEqc.push_back(eqc); + emps = Word::mkEmptyWord(tn); } Node var; eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, ee); @@ -85,7 +85,7 @@ void BaseSolver::checkInit() if (d_congruent.find(n) == d_congruent.end()) { std::vector c; - Node nc = d_termIndex[k].add(n, 0, d_state, d_emptyString, c); + Node nc = d_termIndex[k].add(n, 0, d_state, emps, c); if (nc != n) { // check if we have inferred a new equality by removal of empty @@ -101,14 +101,13 @@ void BaseSolver::checkInit() for (unsigned t = 0; t < 2; t++) { Node nn = t == 0 ? nc : n; - while ( - count[t] < nn.getNumChildren() - && (nn[count[t]] == d_emptyString - || d_state.areEqual(nn[count[t]], d_emptyString))) + while (count[t] < nn.getNumChildren() + && (nn[count[t]] == emps + || d_state.areEqual(nn[count[t]], emps))) { - if (nn[count[t]] != d_emptyString) + if (nn[count[t]] != emps) { - exp.push_back(nn[count[t]].eqNode(d_emptyString)); + exp.push_back(nn[count[t]].eqNode(emps)); } count[t]++; } @@ -160,11 +159,11 @@ void BaseSolver::checkInit() bool foundNEmpty = false; for (const Node& nnc : n) { - if (d_state.areEqual(nnc, d_emptyString)) + if (d_state.areEqual(nnc, emps)) { - if (nnc != d_emptyString) + if (nnc != emps) { - exp.push_back(nnc.eqNode(d_emptyString)); + exp.push_back(nnc.eqNode(emps)); } } else @@ -293,10 +292,11 @@ void BaseSolver::checkConstantEquivalenceClasses(TermIndex* ti, while (count < n.getNumChildren()) { // Add explanations for the empty children + Node emps; while (count < n.getNumChildren() - && d_state.areEqual(n[count], d_emptyString)) + && d_state.isEqualEmptyWord(n[count], emps)) { - d_im.addToExplanation(n[count], d_emptyString, exp); + d_im.addToExplanation(n[count], emps, exp); count++; } if (count < n.getNumChildren()) diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index aa85d1056..2d2ec0af0 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -3044,10 +3044,9 @@ Node SequencesRewriter::canonicalStrForSymbolicLength(Node len, TypeNode stype) { res = nm->mkConst(String(std::string(u, 'A'))); } - else - { - Unimplemented() << "canonicalStrForSymbolicLength for non-string"; - } + // we could do this for sequences, but we need to be careful: some + // sorts do not permit values that the solver can handle (e.g. uninterpreted + // sorts and arrays). } else if (len.getKind() == PLUS) { @@ -3075,6 +3074,10 @@ Node SequencesRewriter::canonicalStrForSymbolicLength(Node len, TypeNode stype) Integer intReps = ratReps.getNumerator(); Node nRep = canonicalStrForSymbolicLength(len[1], stype); + if (nRep.isNull()) + { + return Node::null(); + } std::vector nRepChildren; utils::getConcat(nRep, nRepChildren); NodeBuilder<> concatBuilder(STRING_CONCAT); diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp index 1766a4b24..622e919f7 100644 --- a/src/theory/strings/solver_state.cpp +++ b/src/theory/strings/solver_state.cpp @@ -264,6 +264,20 @@ Node SolverState::explainNonEmpty(Node s) return Node::null(); } +bool SolverState::isEqualEmptyWord(Node s, Node& emps) +{ + Node sr = getRepresentative(s); + if (sr.isConst()) + { + if (Word::getLength(sr) == 0) + { + emps = sr; + return true; + } + } + return false; +} + 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 bd5bb2926..d43c600f4 100644 --- a/src/theory/strings/solver_state.h +++ b/src/theory/strings/solver_state.h @@ -135,6 +135,13 @@ class SolverState * in the equality engine. */ Node explainNonEmpty(Node s); + /** + * Is equal empty word? Returns true if s is equal to the empty word (of + * its type). If this method returns true, it updates emps to be that word. + * This is an optimization so that the relevant empty word does not need to + * be constructed to check if s is equal to the empty word. + */ + bool isEqualEmptyWord(Node s, Node& emps); /** * 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 diff --git a/src/theory/strings/strings_entail.cpp b/src/theory/strings/strings_entail.cpp index 097964672..311eda554 100644 --- a/src/theory/strings/strings_entail.cpp +++ b/src/theory/strings/strings_entail.cpp @@ -905,7 +905,7 @@ Node StringsEntail::getStringOrEmpty(Node n) Node StringsEntail::inferEqsFromContains(Node x, Node y) { NodeManager* nm = NodeManager::currentNM(); - Node emp = nm->mkConst(String("")); + Node emp = Word::mkEmptyWord(x.getType()); Assert(x.getType() == y.getType()); TypeNode stype = x.getType();