From 207245fef36ccad1281fefe9d3f3403cd4f6d15b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 16 Oct 2019 18:44:17 -0500 Subject: [PATCH] Solver state for theory of strings (#3181) This refactors the theory of strings to use a solver state object, which manages state information regarding assertions. It also deletes some unused/undefined functions in theory_strings.h. There are no major changes to the behavior of the code or its documentation in this PR. This is work towards #1881. --- src/CMakeLists.txt | 2 + src/theory/strings/inference_manager.cpp | 46 +- src/theory/strings/inference_manager.h | 26 +- src/theory/strings/regexp_solver.cpp | 10 +- src/theory/strings/regexp_solver.h | 4 + src/theory/strings/solver_state.cpp | 283 +++++++ src/theory/strings/solver_state.h | 187 +++++ src/theory/strings/theory_strings.cpp | 771 ++++++++------------ src/theory/strings/theory_strings.h | 159 +--- src/theory/strings/theory_strings_utils.cpp | 26 +- src/theory/strings/theory_strings_utils.h | 22 +- 11 files changed, 879 insertions(+), 657 deletions(-) create mode 100644 src/theory/strings/solver_state.cpp create mode 100644 src/theory/strings/solver_state.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index a24a2e31a..14d4ef8ae 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -662,6 +662,8 @@ libcvc4_add_sources( theory/strings/regexp_solver.h theory/strings/skolem_cache.cpp theory/strings/skolem_cache.h + theory/strings/solver_state.cpp + theory/strings/solver_state.h theory/strings/theory_strings.cpp theory/strings/theory_strings.h theory/strings/theory_strings_preprocess.cpp diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp index 56a46eed5..5c08fdee3 100644 --- a/src/theory/strings/inference_manager.cpp +++ b/src/theory/strings/inference_manager.cpp @@ -32,9 +32,9 @@ namespace strings { InferenceManager::InferenceManager(TheoryStrings& p, context::Context* c, context::UserContext* u, - eq::EqualityEngine& ee, + SolverState& s, OutputChannel& out) - : d_parent(p), d_ee(ee), d_out(out), d_keep(c) + : d_parent(p), d_state(s), d_out(out), d_keep(c) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); @@ -63,15 +63,15 @@ bool InferenceManager::sendInternalInference(std::vector& exp, { for (unsigned i = 0; i < 2; i++) { - if (!lit[i].isConst() && !d_parent.hasTerm(lit[i])) + if (!lit[i].isConst() && !d_state.hasTerm(lit[i])) { // introduces a new non-constant term, do not infer return false; } } // does it already hold? - if (pol ? d_parent.areEqual(lit[0], lit[1]) - : d_parent.areDisequal(lit[0], lit[1])) + if (pol ? d_state.areEqual(lit[0], lit[1]) + : d_state.areDisequal(lit[0], lit[1])) { return true; } @@ -85,12 +85,12 @@ bool InferenceManager::sendInternalInference(std::vector& exp, return true; } } - else if (!d_parent.hasTerm(lit)) + else if (!d_state.hasTerm(lit)) { // introduces a new non-constant term, do not infer return false; } - else if (d_parent.areEqual(lit, pol ? d_true : d_false)) + else if (d_state.areEqual(lit, pol ? d_true : d_false)) { // already holds return true; @@ -192,7 +192,7 @@ void InferenceManager::sendLemma(Node ant, Node conc, const char* c) Trace("strings-assert") << "(assert (not " << ant << ")) ; conflict " << c << std::endl; d_out.conflict(ant); - d_parent.d_conflict = true; + d_state.setConflict(); return; } Node lem; @@ -279,10 +279,31 @@ void InferenceManager::sendPhaseRequirement(Node lit, bool pol) d_pendingReqPhase[lit] = pol; } +void InferenceManager::addToExplanation(Node a, + Node b, + std::vector& exp) const +{ + if (a != b) + { + Debug("strings-explain") + << "Add to explanation : " << a << " == " << b << std::endl; + Assert(d_state.areEqual(a, b)); + exp.push_back(a.eqNode(b)); + } +} + +void InferenceManager::addToExplanation(Node lit, std::vector& exp) const +{ + if (!lit.isNull()) + { + exp.push_back(lit); + } +} + void InferenceManager::doPendingFacts() { size_t i = 0; - while (!hasConflict() && i < d_pending.size()) + while (!d_state.isInConflict() && i < d_pending.size()) { Node fact = d_pending[i]; Node exp = d_pendingExp[fact]; @@ -309,7 +330,7 @@ void InferenceManager::doPendingFacts() void InferenceManager::doPendingLemmas() { - if (!hasConflict()) + if (!d_state.isInConflict()) { for (const Node& lc : d_pendingLem) { @@ -327,7 +348,10 @@ void InferenceManager::doPendingLemmas() d_pendingReqPhase.clear(); } -bool InferenceManager::hasConflict() const { return d_parent.d_conflict; } +bool InferenceManager::hasProcessed() const +{ + return d_state.isInConflict() || !d_pendingLem.empty() || !d_pending.empty(); +} void InferenceManager::inferSubstitutionProxyVars( Node n, diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h index bb78b4a1a..85855fab9 100644 --- a/src/theory/strings/inference_manager.h +++ b/src/theory/strings/inference_manager.h @@ -25,6 +25,7 @@ #include "expr/node.h" #include "theory/output_channel.h" #include "theory/strings/infer_info.h" +#include "theory/strings/solver_state.h" #include "theory/uf/equality_engine.h" namespace CVC4 { @@ -70,7 +71,7 @@ class InferenceManager InferenceManager(TheoryStrings& p, context::Context* c, context::UserContext* u, - eq::EqualityEngine& ee, + SolverState& s, OutputChannel& out); ~InferenceManager() {} @@ -162,6 +163,15 @@ class InferenceManager * decided with polarity pol. */ void sendPhaseRequirement(Node lit, bool pol); + //----------------------------constructing antecedants + /** + * Adds equality a = b to the vector exp if a and b are distinct terms. It + * must be the case that areEqual( a, b ) holds in this context. + */ + void addToExplanation(Node a, Node b, std::vector& exp) const; + /** Adds lit to the vector exp if it is non-null */ + void addToExplanation(Node lit, std::vector& exp) const; + //----------------------------end constructing antecedants /** Do pending facts * * This method asserts pending facts (d_pending) with explanations @@ -196,16 +206,11 @@ class InferenceManager * this returns true if we have a pending fact or lemma, or have encountered * a conflict. */ - bool hasProcessed() const - { - return hasConflict() || !d_pendingLem.empty() || !d_pending.empty(); - } + bool hasProcessed() const; /** Do we have a pending fact to add to the equality engine? */ bool hasPendingFact() const { return !d_pending.empty(); } /** Do we have a pending lemma to send on the output channel? */ bool hasPendingLemma() const { return !d_pendingLem.empty(); } - /** Are we in conflict? */ - bool hasConflict() const; private: /** @@ -229,11 +234,10 @@ class InferenceManager /** the parent theory of strings object */ TheoryStrings& d_parent; - /** the equality engine - * - * This is a reference to the equality engine of the theory of strings. + /** + * This is a reference to the solver state of the theory of strings. */ - eq::EqualityEngine& d_ee; + SolverState& d_state; /** the output channel * * This is a reference to the output channel of the theory of strings. diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp index db4c9012c..0e44c9461 100644 --- a/src/theory/strings/regexp_solver.cpp +++ b/src/theory/strings/regexp_solver.cpp @@ -34,10 +34,12 @@ namespace theory { namespace strings { RegExpSolver::RegExpSolver(TheoryStrings& p, + SolverState& s, InferenceManager& im, context::Context* c, context::UserContext* u) : d_parent(p), + d_state(s), d_im(im), d_regexp_ucached(u), d_regexp_ccached(c), @@ -134,7 +136,7 @@ void RegExpSolver::check(const std::map >& mems) bool flag = true; Node x = atom[0]; Node r = atom[1]; - Assert(rep == d_parent.getRepresentative(x)); + Assert(rep == d_state.getRepresentative(x)); // The following code takes normal forms into account for the purposes // of simplifying a regular expression membership x in R. For example, // if x = "A" in the current context, then we may be interested in @@ -250,7 +252,7 @@ void RegExpSolver::check(const std::map >& mems) repUnfold.insert(rep); } } - if (d_im.hasConflict()) + if (d_state.isInConflict()) { break; } @@ -259,7 +261,7 @@ void RegExpSolver::check(const std::map >& mems) } if (addedLemma) { - if (!d_im.hasConflict()) + if (!d_state.isInConflict()) { for (unsigned i = 0; i < processed.size(); i++) { @@ -468,7 +470,7 @@ bool RegExpSolver::checkEqcIntersect(const std::vector& mems) bool RegExpSolver::checkPDerivative( Node x, Node r, Node atom, bool& addedLemma, std::vector& nf_exp) { - if (d_parent.areEqual(x, d_emptyString)) + if (d_state.areEqual(x, d_emptyString)) { Node exp; switch (d_regexp_opr.delta(r, exp)) diff --git a/src/theory/strings/regexp_solver.h b/src/theory/strings/regexp_solver.h index c4d6afda0..0b84ebc79 100644 --- a/src/theory/strings/regexp_solver.h +++ b/src/theory/strings/regexp_solver.h @@ -25,6 +25,7 @@ #include "expr/node.h" #include "theory/strings/inference_manager.h" #include "theory/strings/regexp_operation.h" +#include "theory/strings/solver_state.h" #include "util/regexp.h" namespace CVC4 { @@ -44,6 +45,7 @@ class RegExpSolver public: RegExpSolver(TheoryStrings& p, + SolverState& s, InferenceManager& im, context::Context* c, context::UserContext* u); @@ -100,6 +102,8 @@ class RegExpSolver Node d_false; /** the parent of this object */ TheoryStrings& d_parent; + /** The solver state of the parent of this object */ + SolverState& d_state; /** the output channel of the parent of this object */ InferenceManager& d_im; // check membership constraints diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp new file mode 100644 index 000000000..c370558b5 --- /dev/null +++ b/src/theory/strings/solver_state.cpp @@ -0,0 +1,283 @@ +/********************* */ +/*! \file solver_state.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of the solver state of the theory of strings. + **/ + +#include "theory/strings/solver_state.h" + +#include "theory/strings/theory_strings_utils.h" + +using namespace std; +using namespace CVC4::context; +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace strings { + +EqcInfo::EqcInfo(context::Context* c) + : d_lengthTerm(c), + d_codeTerm(c), + d_cardinalityLemK(c), + d_normalizedLength(c), + d_prefixC(c), + d_suffixC(c) +{ +} + +Node EqcInfo::addEndpointConst(Node t, Node c, bool isSuf) +{ + // check conflict + Node prev = isSuf ? d_suffixC : d_prefixC; + if (!prev.isNull()) + { + Trace("strings-eager-pconf-debug") << "Check conflict " << prev << ", " << t + << " post=" << isSuf << std::endl; + Node prevC = utils::getConstantEndpoint(prev, isSuf); + Assert(!prevC.isNull()); + Assert(prevC.getKind() == CONST_STRING); + if (c.isNull()) + { + c = utils::getConstantEndpoint(t, isSuf); + Assert(!c.isNull()); + } + Assert(c.getKind() == CONST_STRING); + bool conflict = false; + // if the constant prefixes are different + if (c != prevC) + { + // conflicts between constants should be handled by equality engine + Assert(!t.isConst() || !prev.isConst()); + Trace("strings-eager-pconf-debug") + << "Check conflict constants " << prevC << ", " << c << std::endl; + const String& ps = prevC.getConst(); + const String& cs = c.getConst(); + unsigned pvs = ps.size(); + unsigned cvs = cs.size(); + if (pvs == cvs || (pvs > cvs && t.isConst()) + || (cvs > pvs && prev.isConst())) + { + // If equal length, cannot be equal due to node check above. + // If one is fully constant and has less length than the other, then the + // other will not fit and we are in conflict. + conflict = true; + } + else + { + const String& larges = pvs > cvs ? ps : cs; + const String& smalls = pvs > cvs ? cs : ps; + if (isSuf) + { + conflict = !larges.hasSuffix(smalls); + } + else + { + conflict = !larges.hasPrefix(smalls); + } + } + if (!conflict && (pvs > cvs || prev.isConst())) + { + // current is subsumed, either shorter prefix or the other is a full + // constant + return Node::null(); + } + } + else if (!t.isConst()) + { + // current is subsumed since the other may be a full constant + return Node::null(); + } + if (conflict) + { + Trace("strings-eager-pconf") + << "Conflict for " << prevC << ", " << c << std::endl; + std::vector ccs; + Node r[2]; + for (unsigned i = 0; i < 2; i++) + { + Node tp = i == 0 ? t : prev; + if (tp.getKind() == STRING_IN_REGEXP) + { + ccs.push_back(tp); + r[i] = tp[0]; + } + else + { + r[i] = tp; + } + } + if (r[0] != r[1]) + { + ccs.push_back(r[0].eqNode(r[1])); + } + Assert(!ccs.empty()); + Node ret = + ccs.size() == 1 ? ccs[0] : NodeManager::currentNM()->mkNode(AND, ccs); + Trace("strings-eager-pconf") + << "String: eager prefix conflict: " << ret << std::endl; + return ret; + } + } + if (isSuf) + { + d_suffixC = t; + } + else + { + d_prefixC = t; + } + return Node::null(); +} + +SolverState::SolverState(context::Context* c, eq::EqualityEngine& ee) + : d_context(c), d_ee(ee), d_conflict(c, false), d_pendingConflict(c) +{ +} +SolverState::~SolverState() +{ + for (std::pair& it : d_eqcInfo) + { + delete it.second; + } +} + +Node SolverState::getRepresentative(Node t) const +{ + if (d_ee.hasTerm(t)) + { + return d_ee.getRepresentative(t); + } + return t; +} + +bool SolverState::hasTerm(Node a) const { return d_ee.hasTerm(a); } + +bool SolverState::areEqual(Node a, Node b) const +{ + if (a == b) + { + return true; + } + else if (hasTerm(a) && hasTerm(b)) + { + return d_ee.areEqual(a, b); + } + return false; +} + +bool SolverState::areDisequal(Node a, Node b) const +{ + if (a == b) + { + return false; + } + else if (hasTerm(a) && hasTerm(b)) + { + Node ar = d_ee.getRepresentative(a); + Node br = d_ee.getRepresentative(b); + return (ar != br && ar.isConst() && br.isConst()) + || d_ee.areDisequal(ar, br, false); + } + Node ar = getRepresentative(a); + Node br = getRepresentative(b); + return ar != br && ar.isConst() && br.isConst(); +} + +eq::EqualityEngine* SolverState::getEqualityEngine() const { return &d_ee; } + +EqcInfo* SolverState::getOrMakeEqcInfo(Node eqc, bool doMake) +{ + std::map::iterator eqc_i = d_eqcInfo.find(eqc); + if (eqc_i != d_eqcInfo.end()) + { + return eqc_i->second; + } + if (doMake) + { + EqcInfo* ei = new EqcInfo(d_context); + d_eqcInfo[eqc] = ei; + return ei; + } + return nullptr; +} + +void SolverState::addEndpointsToEqcInfo(Node t, Node concat, Node eqc) +{ + Assert(concat.getKind() == STRING_CONCAT + || concat.getKind() == REGEXP_CONCAT); + EqcInfo* ei = nullptr; + // check each side + for (unsigned r = 0; r < 2; r++) + { + unsigned index = r == 0 ? 0 : concat.getNumChildren() - 1; + Node c = utils::getConstantComponent(concat[index]); + if (!c.isNull()) + { + if (ei == nullptr) + { + ei = getOrMakeEqcInfo(eqc); + } + Trace("strings-eager-pconf-debug") + << "New term: " << concat << " for " << t << " with prefix " << c + << " (" << (r == 1) << ")" << std::endl; + setPendingConflictWhen(ei->addEndpointConst(t, c, r == 1)); + } + } +} + +Node SolverState::getLengthExp(Node t, std::vector& exp, Node te) +{ + Assert(areEqual(t, te)); + Node lt = utils::mkNLength(te); + if (hasTerm(lt)) + { + // use own length if it exists, leads to shorter explanation + return lt; + } + EqcInfo* ei = getOrMakeEqcInfo(t, false); + Node lengthTerm = ei ? ei->d_lengthTerm : Node::null(); + if (lengthTerm.isNull()) + { + // typically shouldnt be necessary + lengthTerm = t; + } + Debug("strings") << "SolverState::getLengthTerm " << t << " is " << lengthTerm + << std::endl; + if (te != lengthTerm) + { + exp.push_back(te.eqNode(lengthTerm)); + } + return Rewriter::rewrite( + NodeManager::currentNM()->mkNode(STRING_LENGTH, lengthTerm)); +} + +Node SolverState::getLength(Node t, std::vector& exp) +{ + return getLengthExp(t, exp, t); +} + +void SolverState::setConflict() { d_conflict = true; } +bool SolverState::isInConflict() const { return d_conflict; } + +void SolverState::setPendingConflictWhen(Node conf) +{ + if (!conf.isNull() && d_pendingConflict.get().isNull()) + { + d_pendingConflict = conf; + } +} + +Node SolverState::getPendingConflict() const { return d_pendingConflict; } + +} // namespace strings +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/strings/solver_state.h b/src/theory/strings/solver_state.h new file mode 100644 index 000000000..f14b4b4af --- /dev/null +++ b/src/theory/strings/solver_state.h @@ -0,0 +1,187 @@ +/********************* */ +/*! \file solver_state.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The solver state of the theory of strings + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__STRINGS__SOLVER_STATE_H +#define CVC4__THEORY__STRINGS__SOLVER_STATE_H + +#include + +#include "context/cdo.h" +#include "context/context.h" +#include "expr/node.h" +#include "theory/uf/equality_engine.h" + +namespace CVC4 { +namespace theory { +namespace strings { + +/** + * SAT-context-dependent information about an equivalence class. This + * information is updated eagerly as assertions are processed by the theory of + * strings at standard effort. + */ +class EqcInfo +{ + public: + EqcInfo(context::Context* c); + ~EqcInfo() {} + /** add prefix constant + * + * This informs this equivalence class info that a term t in its + * equivalence class has a constant prefix (if isSuf=true) or suffix + * (if isSuf=false). The constant c (if non-null) is the value of that + * constant, if it has been computed already. + * + * If this method returns a non-null node ret, then ret is a conjunction + * corresponding to a conflict that holds in the current context. + */ + Node addEndpointConst(Node t, Node c, bool isSuf); + /** + * If non-null, this is a term x from this eq class such that str.len( x ) + * occurs as a term in this SAT context. + */ + context::CDO d_lengthTerm; + /** + * If non-null, this is a term x from this eq class such that str.code( x ) + * occurs as a term in this SAT context. + */ + context::CDO d_codeTerm; + context::CDO d_cardinalityLemK; + context::CDO d_normalizedLength; + /** + * A node that explains the longest constant prefix known of this + * equivalence class. This can either be: + * (1) A term from this equivalence class, including a constant "ABC" or + * concatenation term (str.++ "ABC" ...), or + * (2) A membership of the form (str.in.re x R) where x is in this + * equivalence class and R is a regular expression of the form + * (str.to.re "ABC") or (re.++ (str.to.re "ABC") ...). + */ + context::CDO d_prefixC; + /** same as above, for suffix. */ + context::CDO d_suffixC; +}; + +/** + * Solver state for strings. + * + * The purpose of this class is track and provide query functions for the state + * of the assertions for the theory of strings. This includes: + * (1) Equality queries via the equality engine, + * (2) Whether the set of assertions is in conflict. + * (3) Equivalence class information as in the class above. + */ +class SolverState +{ + public: + SolverState(context::Context* c, eq::EqualityEngine& ee); + ~SolverState(); + //-------------------------------------- equality information + /** + * Get the representative of t in the equality engine of this class, or t + * itself if it is not registered as a term. + */ + Node getRepresentative(Node t) const; + /** Is t registered as a term in the equality engine of this class? */ + bool hasTerm(Node a) const; + /** + * Are a and b equal according to the equality engine of this class? Also + * returns true if a and b are identical. + */ + bool areEqual(Node a, Node b) const; + /** + * Are a and b disequal according to the equality engine of this class? Also + * returns true if the representative of a and b are distinct constants. + */ + bool areDisequal(Node a, Node b) const; + /** get equality engine */ + eq::EqualityEngine* getEqualityEngine() const; + //-------------------------------------- end equality information + //------------------------------------------ conflicts + /** + * Set that the current state of the solver is in conflict. This should be + * called immediately after a call to conflict(...) on the output channel of + * the theory of strings. + */ + void setConflict(); + /** Are we currently in conflict? */ + bool isInConflict() const; + /** set pending conflict + * + * If conf is non-null, this is called when conf is a conjunction of literals + * that hold in the current context that are unsatisfiable. It is set as the + * "pending conflict" to be processed as a conflict lemma on the output + * channel of this class. It is not sent out immediately since it may require + * explanation from the equality engine, and may be called at any time, e.g. + * during a merge operation, when the equality engine is not in a state to + * provide explanations. + */ + void setPendingConflictWhen(Node conf); + /** get the pending conflict, or null if none exist */ + Node getPendingConflict() const; + //------------------------------------------ end conflicts + /** get length with explanation + * + * If possible, this returns an arithmetic term that exists in the current + * context that is equal to the length of te, or otherwise returns the + * length of t. It adds to exp literals that hold in the current context that + * explain why that term is equal to the length of t. For example, if + * we have assertions: + * len( x ) = 5 ^ z = x ^ x = y, + * then getLengthExp( z, exp, y ) returns len( x ) and adds { z = x } to + * exp. On the other hand, getLengthExp( z, exp, x ) returns len( x ) and + * adds nothing to exp. + */ + Node getLengthExp(Node t, std::vector& exp, Node te); + /** shorthand for getLengthExp(t, exp, t) */ + Node getLength(Node t, std::vector& exp); + /** + * 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 + * should currently be a representative of the equality engine of this class. + */ + EqcInfo* getOrMakeEqcInfo(Node eqc, bool doMake = true); + + /** add endpoints to eqc info + * + * This method is called when term t is the explanation for why equivalence + * class eqc may have a constant endpoint due to a concatentation term concat. + * For example, we may call this method on: + * t := (str.++ x y), concat := (str.++ x y), eqc + * for some eqc that is currently equal to t. Another example is: + * t := (str.in.re z (re.++ r s)), concat := (re.++ r s), eqc + * for some eqc that is currently equal to z. + */ + void addEndpointsToEqcInfo(Node t, Node concat, Node eqc); + + private: + /** 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. */ + eq::EqualityEngine& d_ee; + /** Are we in conflict? */ + context::CDO d_conflict; + /** The pending conflict if one exists */ + context::CDO d_pendingConflict; + /** Map from representatives to their equivalence class information */ + std::map d_eqcInfo; +}; /* class TheoryStrings */ + +} // namespace strings +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__STRINGS__THEORY_STRINGS_H */ diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index caaded4c3..b0681b1ff 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -61,7 +61,12 @@ std::ostream& operator<<(std::ostream& out, InferStep s) return out; } -Node TheoryStrings::TermIndex::add( TNode n, unsigned index, TheoryStrings* t, Node er, std::vector< Node >& c ) { +Node TheoryStrings::TermIndex::add(TNode n, + unsigned index, + const SolverState& s, + Node er, + std::vector& c) +{ if( index==n.getNumChildren() ){ if( d_data.isNull() ){ d_data = n; @@ -69,13 +74,13 @@ Node TheoryStrings::TermIndex::add( TNode n, unsigned index, TheoryStrings* t, N return d_data; }else{ Assert( indexgetRepresentative( n[index] ); + TNode nir = s.getRepresentative(n[index]); //if it is empty, and doing CONCAT, ignore if( nir==er && n.getKind()==kind::STRING_CONCAT ){ - return add( n, index+1, t, er, c ); + return add(n, index + 1, s, er, c); }else{ c.push_back( nir ); - return d_children[nir].add( n, index+1, t, er, c ); + return d_children[nir].add(n, index + 1, s, er, c); } } } @@ -88,16 +93,15 @@ TheoryStrings::TheoryStrings(context::Context* c, : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo), d_notify(*this), d_equalityEngine(d_notify, c, "theory::strings", true), - d_im(*this, c, u, d_equalityEngine, out), + d_state(c, d_equalityEngine), + d_im(*this, c, u, d_state, out), d_conflict(c, false), - d_pendingConflict(c), d_nf_pairs(c), d_pregistered_terms_cache(u), d_registered_terms_cache(u), d_length_lemma_terms_cache(u), d_preproc(&d_sk_cache, u), d_extf_infer_cache(c), - d_extf_infer_cache_u(u), d_ee_disequalities(c), d_congruent(c), d_proxy_var(u), @@ -105,7 +109,7 @@ TheoryStrings::TheoryStrings(context::Context* c, d_functionsTerms(c), d_has_extf(c, false), d_has_str_code(false), - d_regexp_solver(*this, d_im, c, u), + d_regexp_solver(*this, d_state, d_im, c, u), d_input_vars(u), d_input_var_lsum(u), d_cardinality_lits(u), @@ -156,47 +160,7 @@ TheoryStrings::TheoryStrings(context::Context* c, } TheoryStrings::~TheoryStrings() { - for( std::map< Node, EqcInfo* >::iterator it = d_eqc_info.begin(); it != d_eqc_info.end(); ++it ){ - delete it->second; - } -} - -Node TheoryStrings::getRepresentative( Node t ) { - if( d_equalityEngine.hasTerm( t ) ){ - return d_equalityEngine.getRepresentative( t ); - }else{ - return t; - } -} -bool TheoryStrings::hasTerm( Node a ){ - return d_equalityEngine.hasTerm( a ); -} - -bool TheoryStrings::areEqual( Node a, Node b ){ - if( a==b ){ - return true; - }else if( hasTerm( a ) && hasTerm( b ) ){ - return d_equalityEngine.areEqual( a, b ); - }else{ - return false; - } -} - -bool TheoryStrings::areDisequal( Node a, Node b ){ - if( a==b ){ - return false; - }else{ - if( hasTerm( a ) && hasTerm( b ) ) { - Node ar = d_equalityEngine.getRepresentative( a ); - Node br = d_equalityEngine.getRepresentative( b ); - return ( ar!=br && ar.isConst() && br.isConst() ) || d_equalityEngine.areDisequal( ar, br, false ); - }else{ - Node ar = getRepresentative( a ); - Node br = getRepresentative( b ); - return ar!=br && ar.isConst() && br.isConst(); - } - } } bool TheoryStrings::areCareDisequal( TNode x, TNode y ) { @@ -213,41 +177,18 @@ bool TheoryStrings::areCareDisequal( TNode x, TNode y ) { return false; } -Node TheoryStrings::getLengthExp( Node t, std::vector< Node >& exp, Node te ){ - Assert( areEqual( t, te ) ); - Node lt = mkLength( te ); - if( hasTerm( lt ) ){ - // use own length if it exists, leads to shorter explanation - return lt; - }else{ - EqcInfo * ei = getOrMakeEqcInfo( t, false ); - Node length_term = ei ? ei->d_length_term : Node::null(); - if( length_term.isNull() ){ - //typically shouldnt be necessary - length_term = t; - } - Debug("strings") << "TheoryStrings::getLengthTerm " << t << " is " << length_term << std::endl; - addToExplanation( length_term, te, exp ); - return Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, length_term ) ); - } -} - -Node TheoryStrings::getLength( Node t, std::vector< Node >& exp ) { - return getLengthExp( t, exp, t ); -} - Node TheoryStrings::getNormalString(Node x, std::vector& nf_exp) { if (!x.isConst()) { - Node xr = getRepresentative(x); + Node xr = d_state.getRepresentative(x); std::map::iterator it = d_normal_form.find(xr); if (it != d_normal_form.end()) { NormalForm& nf = it->second; - Node ret = mkConcat(nf.d_nf); + Node ret = utils::mkNConcat(nf.d_nf); nf_exp.insert(nf_exp.end(), nf.d_exp.begin(), nf.d_exp.end()); - addToExplanation(x, nf.d_base, nf_exp); + d_im.addToExplanation(x, nf.d_base, nf_exp); Trace("strings-debug") << "Term: " << x << " has a normal form " << ret << std::endl; return ret; @@ -263,7 +204,7 @@ Node TheoryStrings::getNormalString(Node x, std::vector& nf_exp) Node nc = getNormalString(x[i], nf_exp); vec_nodes.push_back(nc); } - return mkConcat(vec_nodes); + return utils::mkNConcat(vec_nodes); } } return x; @@ -326,8 +267,8 @@ void TheoryStrings::explain(TNode literal, std::vector& assumptions) { std::vector< TNode > tassumptions; if (atom.getKind() == kind::EQUAL) { if( atom[0]!=atom[1] ){ - Assert( hasTerm( atom[0] ) ); - Assert( hasTerm( atom[1] ) ); + Assert(d_equalityEngine.hasTerm(atom[0])); + Assert(d_equalityEngine.hasTerm(atom[1])); d_equalityEngine.explainEquality(atom[0], atom[1], polarity, tassumptions); } } else { @@ -385,7 +326,7 @@ Node TheoryStrings::getCurrentSubstitutionFor(int effort, Trace("strings-subs") << " model val : " << mv << std::endl; return mv; } - Node nr = getRepresentative(n); + Node nr = d_state.getRepresentative(n); std::map::iterator itc = d_eqc_to_const.find(nr); if (itc != d_eqc_to_const.end()) { @@ -399,7 +340,7 @@ Node TheoryStrings::getCurrentSubstitutionFor(int effort, } if (!d_eqc_to_const_base[nr].isNull()) { - addToExplanation(n, d_eqc_to_const_base[nr], exp); + d_im.addToExplanation(n, d_eqc_to_const_base[nr], exp); } return itc->second; } @@ -413,7 +354,7 @@ Node TheoryStrings::getCurrentSubstitutionFor(int effort, << " " << nr << std::endl; if (!nfnr.d_base.isNull()) { - addToExplanation(n, nfnr.d_base, exp); + d_im.addToExplanation(n, nfnr.d_base, exp); } return ns; } @@ -451,9 +392,9 @@ bool TheoryStrings::doReduction(int effort, Node n, bool& isCd) Node x = n[0]; Node s = n[1]; std::vector lexp; - Node lenx = getLength(x, lexp); - Node lens = getLength(s, lexp); - if (areEqual(lenx, lens)) + Node lenx = d_state.getLength(x, lexp); + Node lens = d_state.getLength(s, lexp); + if (d_state.areEqual(lenx, lens)) { Trace("strings-extf-debug") << " resolve extf : " << n @@ -461,7 +402,7 @@ bool TheoryStrings::doReduction(int effort, Node n, bool& isCd) // We can reduce negative contains to a disequality when lengths are // equal. In other words, len( x ) = len( s ) implies // ~contains( x, s ) reduces to x != s. - if (!areDisequal(x, s)) + if (!d_state.areDisequal(x, s)) { // len( x ) = len( s ) ^ ~contains( x, s ) => x != s lexp.push_back(lenx.eqNode(lens)); @@ -509,7 +450,7 @@ bool TheoryStrings::doReduction(int effort, Node n, bool& isCd) d_sk_cache.mkSkolemCached(x, s, SkolemCache::SK_FIRST_CTN_PRE, "sc1"); Node sk2 = d_sk_cache.mkSkolemCached(x, s, SkolemCache::SK_FIRST_CTN_POST, "sc2"); - Node eq = Rewriter::rewrite(x.eqNode(mkConcat(sk1, s, sk2))); + Node eq = Rewriter::rewrite(x.eqNode(utils::mkNConcat(sk1, s, sk2))); std::vector exp_vec; exp_vec.push_back(n); d_im.sendInference(d_empty_vec, exp_vec, eq, "POS-CTN", true); @@ -607,7 +548,7 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m) { if (s.getType().isString()) { - Node r = getRepresentative(s); + Node r = d_state.getRepresentative(s); repSet.insert(r); } } @@ -682,11 +623,11 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m) // one? if (d_has_str_code && lts_values[i] == d_one) { - EqcInfo* eip = getOrMakeEqcInfo(eqc, false); - if (eip && !eip->d_code_term.get().isNull()) + EqcInfo* eip = d_state.getOrMakeEqcInfo(eqc, false); + if (eip && !eip->d_codeTerm.get().isNull()) { // its value must be equal to its code - Node ct = nm->mkNode(kind::STRING_CODE, eip->d_code_term.get()); + Node ct = nm->mkNode(kind::STRING_CODE, eip->d_codeTerm.get()); Node ctv = d_valuation.getModelValue(ct); unsigned cvalue = ctv.getConst().getNumerator().toUnsignedInt(); @@ -812,7 +753,7 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m) Trace("strings-model") << " ++ "; } Trace("strings-model") << n; - Node r = getRepresentative(n); + Node r = d_state.getRepresentative(n); if (!r.isConst() && processed.find(r) == processed.end()) { Trace("strings-model") << "(UNPROCESSED)"; @@ -823,11 +764,11 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m) std::vector< Node > nc; for (const Node& n : nf.d_nf) { - Node r = getRepresentative(n); + Node r = d_state.getRepresentative(n); Assert( r.isConst() || processed.find( r )!=processed.end() ); nc.push_back(r.isConst() ? r : processed[r]); } - Node cc = mkConcat( nc ); + Node cc = utils::mkNConcat(nc); Assert( cc.getKind()==kind::CONST_STRING ); Trace("strings-model") << "*** Determined constant " << cc << " for " << nodes[i] << std::endl; processed[nodes[i]] = cc; @@ -956,7 +897,8 @@ void TheoryStrings::check(Effort e) { bool polarity; TNode atom; - if( !done() && !hasTerm( d_emptyString ) ) { + if (!done() && !d_equalityEngine.hasTerm(d_emptyString)) + { preRegisterTerm( d_emptyString ); } @@ -1001,11 +943,16 @@ void TheoryStrings::check(Effort e) { ++eqc2_i; } Trace("strings-eqc") << " } " << std::endl; - EqcInfo * ei = getOrMakeEqcInfo( eqc, false ); + EqcInfo* ei = d_state.getOrMakeEqcInfo(eqc, false); if( ei ){ - Trace("strings-eqc-debug") << "* Length term : " << ei->d_length_term.get() << std::endl; - Trace("strings-eqc-debug") << "* Cardinality lemma k : " << ei->d_cardinality_lem_k.get() << std::endl; - Trace("strings-eqc-debug") << "* Normalization length lemma : " << ei->d_normalized_length.get() << std::endl; + Trace("strings-eqc-debug") + << "* Length term : " << ei->d_lengthTerm.get() << std::endl; + Trace("strings-eqc-debug") + << "* Cardinality lemma k : " << ei->d_cardinalityLemK.get() + << std::endl; + Trace("strings-eqc-debug") + << "* Normalization length lemma : " + << ei->d_normalizedLength.get() << std::endl; } } ++eqcs2_i; @@ -1097,7 +1044,7 @@ void TheoryStrings::checkMemberships() bool pol = d_extf_info_tmp[n].d_const.getConst(); Trace("strings-process-debug") << " add membership : " << n << ", pol = " << pol << std::endl; - Node r = getRepresentative(n[0]); + Node r = d_state.getRepresentative(n[0]); assertedMems[r].push_back(pol ? n : n.negate()); } else @@ -1109,136 +1056,6 @@ void TheoryStrings::checkMemberships() d_regexp_solver.check(assertedMems); } -TheoryStrings::EqcInfo::EqcInfo(context::Context* c) - : d_length_term(c), - d_code_term(c), - d_cardinality_lem_k(c), - d_normalized_length(c), - d_prefixC(c), - d_suffixC(c) -{ -} - -Node TheoryStrings::EqcInfo::addEndpointConst(Node t, Node c, bool isSuf) -{ - // check conflict - Node prev = isSuf ? d_suffixC : d_prefixC; - if (!prev.isNull()) - { - Trace("strings-eager-pconf-debug") << "Check conflict " << prev << ", " << t - << " post=" << isSuf << std::endl; - Node prevC = utils::getConstantEndpoint(prev, isSuf); - Assert(!prevC.isNull()); - Assert(prevC.getKind() == CONST_STRING); - if (c.isNull()) - { - c = utils::getConstantEndpoint(t, isSuf); - Assert(!c.isNull()); - } - Assert(c.getKind() == CONST_STRING); - bool conflict = false; - // if the constant prefixes are different - if (c != prevC) - { - // conflicts between constants should be handled by equality engine - Assert(!t.isConst() || !prev.isConst()); - Trace("strings-eager-pconf-debug") - << "Check conflict constants " << prevC << ", " << c << std::endl; - const String& ps = prevC.getConst(); - const String& cs = c.getConst(); - unsigned pvs = ps.size(); - unsigned cvs = cs.size(); - if (pvs == cvs || (pvs > cvs && t.isConst()) - || (cvs > pvs && prev.isConst())) - { - // If equal length, cannot be equal due to node check above. - // If one is fully constant and has less length than the other, then the - // other will not fit and we are in conflict. - conflict = true; - } - else - { - const String& larges = pvs > cvs ? ps : cs; - const String& smalls = pvs > cvs ? cs : ps; - if (isSuf) - { - conflict = !larges.hasSuffix(smalls); - } - else - { - conflict = !larges.hasPrefix(smalls); - } - } - if (!conflict && (pvs > cvs || prev.isConst())) - { - // current is subsumed, either shorter prefix or the other is a full - // constant - return Node::null(); - } - } - else if (!t.isConst()) - { - // current is subsumed since the other may be a full constant - return Node::null(); - } - if (conflict) - { - Trace("strings-eager-pconf") - << "Conflict for " << prevC << ", " << c << std::endl; - std::vector ccs; - Node r[2]; - for (unsigned i = 0; i < 2; i++) - { - Node tp = i == 0 ? t : prev; - if (tp.getKind() == STRING_IN_REGEXP) - { - ccs.push_back(tp); - r[i] = tp[0]; - } - else - { - r[i] = tp; - } - } - if (r[0] != r[1]) - { - ccs.push_back(r[0].eqNode(r[1])); - } - Assert(!ccs.empty()); - Node ret = - ccs.size() == 1 ? ccs[0] : NodeManager::currentNM()->mkNode(AND, ccs); - Trace("strings-eager-pconf") - << "String: eager prefix conflict: " << ret << std::endl; - return ret; - } - } - if (isSuf) - { - d_suffixC = t; - } - else - { - d_prefixC = t; - } - return Node::null(); -} - -TheoryStrings::EqcInfo * TheoryStrings::getOrMakeEqcInfo( Node eqc, bool doMake ) { - std::map< Node, EqcInfo* >::iterator eqc_i = d_eqc_info.find( eqc ); - if( eqc_i==d_eqc_info.end() ){ - if( doMake ){ - EqcInfo* ei = new EqcInfo( getSatContext() ); - d_eqc_info[eqc] = ei; - return ei; - }else{ - return NULL; - } - }else{ - return (*eqc_i).second; - } -} - - /** Conflict when merging two constants */ void TheoryStrings::conflict(TNode a, TNode b){ if( !d_conflict ){ @@ -1258,14 +1075,14 @@ void TheoryStrings::eqNotifyNewClass(TNode t){ { Trace("strings-debug") << "New length eqc : " << t << std::endl; Node r = d_equalityEngine.getRepresentative(t[0]); - EqcInfo* ei = getOrMakeEqcInfo(r); + EqcInfo* ei = d_state.getOrMakeEqcInfo(r); if (k == kind::STRING_LENGTH) { - ei->d_length_term = t[0]; + ei->d_lengthTerm = t[0]; } else { - ei->d_code_term = t[0]; + ei->d_codeTerm = t[0]; } //we care about the length of this string registerTerm( t[0], 1 ); @@ -1273,69 +1090,48 @@ void TheoryStrings::eqNotifyNewClass(TNode t){ } else if (k == CONST_STRING) { - EqcInfo* ei = getOrMakeEqcInfo(t); + EqcInfo* ei = d_state.getOrMakeEqcInfo(t); ei->d_prefixC = t; ei->d_suffixC = t; return; } else if (k == STRING_CONCAT) { - addEndpointsToEqcInfo(t, t, t); - } -} - -void TheoryStrings::addEndpointsToEqcInfo(Node t, Node concat, Node eqc) -{ - Assert(concat.getKind() == STRING_CONCAT - || concat.getKind() == REGEXP_CONCAT); - EqcInfo* ei = nullptr; - // check each side - for (unsigned r = 0; r < 2; r++) - { - unsigned index = r == 0 ? 0 : concat.getNumChildren() - 1; - Node c = utils::getConstantComponent(concat[index]); - if (!c.isNull()) - { - if (ei == nullptr) - { - ei = getOrMakeEqcInfo(eqc); - } - Trace("strings-eager-pconf-debug") - << "New term: " << concat << " for " << t << " with prefix " << c - << " (" << (r == 1) << ")" << std::endl; - setPendingConflictWhen(ei->addEndpointConst(t, c, r == 1)); - } + d_state.addEndpointsToEqcInfo(t, t, t); } } /** called when two equivalance classes will merge */ void TheoryStrings::eqNotifyPreMerge(TNode t1, TNode t2){ - EqcInfo * e2 = getOrMakeEqcInfo(t2, false); + EqcInfo* e2 = d_state.getOrMakeEqcInfo(t2, false); if( e2 ){ - EqcInfo * e1 = getOrMakeEqcInfo( t1 ); + EqcInfo* e1 = d_state.getOrMakeEqcInfo(t1); //add information from e2 to e1 - if( !e2->d_length_term.get().isNull() ){ - e1->d_length_term.set( e2->d_length_term ); + if (!e2->d_lengthTerm.get().isNull()) + { + e1->d_lengthTerm.set(e2->d_lengthTerm); } - if (!e2->d_code_term.get().isNull()) + if (!e2->d_codeTerm.get().isNull()) { - e1->d_code_term.set(e2->d_code_term); + e1->d_codeTerm.set(e2->d_codeTerm); } if (!e2->d_prefixC.get().isNull()) { - setPendingConflictWhen( + d_state.setPendingConflictWhen( e1->addEndpointConst(e2->d_prefixC, Node::null(), false)); } if (!e2->d_suffixC.get().isNull()) { - setPendingConflictWhen( + d_state.setPendingConflictWhen( e1->addEndpointConst(e2->d_suffixC, Node::null(), true)); } - if( e2->d_cardinality_lem_k.get()>e1->d_cardinality_lem_k.get() ) { - e1->d_cardinality_lem_k.set( e2->d_cardinality_lem_k ); + if (e2->d_cardinalityLemK.get() > e1->d_cardinalityLemK.get()) + { + e1->d_cardinalityLemK.set(e2->d_cardinalityLemK); } - if( !e2->d_normalized_length.get().isNull() ){ - e1->d_normalized_length.set( e2->d_normalized_length ); + if (!e2->d_normalizedLength.get().isNull()) + { + e1->d_normalizedLength.set(e2->d_normalizedLength); } } } @@ -1481,19 +1277,20 @@ void TheoryStrings::assertPendingFact(Node atom, bool polarity, Node exp) { if (polarity && atom[1].getKind() == REGEXP_CONCAT) { Node eqc = d_equalityEngine.getRepresentative(atom[0]); - addEndpointsToEqcInfo(atom, atom[1], eqc); + d_state.addEndpointsToEqcInfo(atom, atom[1], eqc); } } } // process the conflict if (!d_conflict) { - if (!d_pendingConflict.get().isNull()) + Node pc = d_state.getPendingConflict(); + if (!pc.isNull()) { std::vector a; - a.push_back(d_pendingConflict.get()); - Trace("strings-pending") << "Process pending conflict " - << d_pendingConflict.get() << std::endl; + a.push_back(pc); + Trace("strings-pending") + << "Process pending conflict " << pc << std::endl; Node conflictNode = mkExplain(a); d_conflict = true; Trace("strings-conflict") @@ -1509,28 +1306,6 @@ void TheoryStrings::assertPendingFact(Node atom, bool polarity, Node exp) { Trace("strings-pending-debug") << " Finished collect terms" << std::endl; } -void TheoryStrings::setPendingConflictWhen(Node conf) -{ - if (!conf.isNull() && d_pendingConflict.get().isNull()) - { - d_pendingConflict = conf; - } -} - -void TheoryStrings::addToExplanation( Node a, Node b, std::vector< Node >& exp ) { - if( a!=b ){ - Debug("strings-explain") << "Add to explanation : " << a << " == " << b << std::endl; - Assert( areEqual( a, b ) ); - exp.push_back( a.eqNode( b ) ); - } -} - -void TheoryStrings::addToExplanation( Node lit, std::vector< Node >& exp ) { - if( !lit.isNull() ){ - exp.push_back( lit ); - } -} - void TheoryStrings::checkInit() { //build term index d_eqc_to_const.clear(); @@ -1542,7 +1317,7 @@ void TheoryStrings::checkInit() { std::map< Kind, unsigned > ncongruent; std::map< Kind, unsigned > congruent; - d_emptyString_r = getRepresentative( d_emptyString ); + d_emptyString_r = d_state.getRepresentative(d_emptyString); eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); while( !eqcs_i.isFinished() ){ Node eqc = (*eqcs_i); @@ -1561,7 +1336,7 @@ void TheoryStrings::checkInit() { d_eqc_to_const_exp[eqc] = Node::null(); }else if( tn.isInteger() ){ if( n.getKind()==kind::STRING_LENGTH ){ - Node nr = getRepresentative( n[0] ); + Node nr = d_state.getRepresentative(n[0]); d_eqc_to_len_term[nr] = n[0]; } }else if( n.getNumChildren()>0 ){ @@ -1569,18 +1344,23 @@ void TheoryStrings::checkInit() { if( k!=kind::EQUAL ){ if( d_congruent.find( n )==d_congruent.end() ){ std::vector< Node > c; - Node nc = d_term_index[k].add( n, 0, this, d_emptyString_r, c ); + Node nc = d_term_index[k].add(n, 0, d_state, d_emptyString_r, c); if( nc!=n ){ //check if we have inferred a new equality by removal of empty components - if( n.getKind()==kind::STRING_CONCAT && !areEqual( nc, n ) ){ + if (n.getKind() == kind::STRING_CONCAT + && !d_state.areEqual(nc, n)) + { std::vector< Node > exp; unsigned count[2] = { 0, 0 }; while( count[0]hasFunctionKind( n.getKind() ) ){ + } + else if (getExtTheory()->hasFunctionKind(n.getKind())) + { //mark as congruent : only process if neither has been reduced getExtTheory()->markCongruent( nc, n ); } @@ -1612,17 +1394,21 @@ void TheoryStrings::checkInit() { }else if( k==kind::STRING_CONCAT && c.size()==1 ){ Trace("strings-process-debug") << " congruent term by singular : " << n << " " << c[0] << std::endl; //singular case - if( !areEqual( c[0], n ) ){ + if (!d_state.areEqual(c[0], n)) + { Node ns; std::vector< Node > exp; //explain empty components bool foundNEmpty = false; for( unsigned i=0; id_data; if( !n.isNull() ){ //construct the constant - Node c = mkConcat( vecc ); - if( !areEqual( n, c ) ){ + Node c = utils::mkNConcat(vecc); + if (!d_state.areEqual(n, c)) + { Trace("strings-debug") << "Constant eqc : " << c << " for " << n << std::endl; Trace("strings-debug") << " "; for( unsigned i=0; i exp; while( count::iterator it = d_eqc_to_const.find( nr ); if( it==d_eqc_to_const.end() ){ Trace("strings-debug") << "Set eqc const " << n << " to " << c << std::endl; @@ -1732,11 +1525,11 @@ void TheoryStrings::checkConstantEquivalenceClasses( TermIndex* ti, std::vector< Trace("strings-debug") << "Conflict, other constant was " << it->second << ", this constant was " << c << std::endl; if( d_eqc_to_const_exp[nr].isNull() ){ // n==c ^ n == c' => false - addToExplanation( n, it->second, exp ); + d_im.addToExplanation(n, it->second, exp); }else{ // n==c ^ n == d_eqc_to_const_base[nr] == c' => false exp.push_back( d_eqc_to_const_exp[nr] ); - addToExplanation( n, d_eqc_to_const_base[nr], exp ); + d_im.addToExplanation(n, d_eqc_to_const_base[nr], exp); } d_im.sendInference(exp, d_false, "I_CONST_CONFLICT"); return; @@ -1770,7 +1563,7 @@ void TheoryStrings::checkExtfEval( int effort ) { { // Setup information about n, including if it is equal to a constant. ExtfInfoTmp& einfo = d_extf_info_tmp[n]; - Node r = getRepresentative(n); + Node r = d_state.getRepresentative(n); std::map::iterator itcit = d_eqc_to_const.find(r); if (itcit != d_eqc_to_const.end()) { @@ -1853,7 +1646,8 @@ void TheoryStrings::checkExtfEval( int effort ) { Node conc; if( !nrs.isNull() ){ Trace("strings-extf-debug") << " symbolic def : " << nrs << std::endl; - if( !areEqual( nrs, nrc ) ){ + if (!d_state.areEqual(nrs, nrc)) + { //infer symbolic unit if( n.getType().isBoolean() ){ conc = nrc==d_true ? nrs : nrs.negate(); @@ -1863,12 +1657,16 @@ void TheoryStrings::checkExtfEval( int effort ) { einfo.d_exp.clear(); } }else{ - if( !areEqual( n, nrc ) ){ + if (!d_state.areEqual(n, nrc)) + { if( n.getType().isBoolean() ){ - if( areEqual( n, nrc==d_true ? d_false : d_true ) ){ + if (d_state.areEqual(n, nrc == d_true ? d_false : d_true)) + { einfo.d_exp.push_back(nrc == d_true ? n.negate() : n); conc = d_false; - }else{ + } + else + { conc = nrc==d_true ? n : n.negate(); } }else{ @@ -1887,7 +1685,8 @@ void TheoryStrings::checkExtfEval( int effort ) { } }else{ //check if it is already equal, if so, mark as reduced. Otherwise, do nothing. - if( areEqual( n, nrc ) ){ + if (d_state.areEqual(n, nrc)) + { Trace("strings-extf") << " resolved extf, since satisfied by model: " << n << std::endl; einfo.d_model_active = false; } @@ -1966,13 +1765,13 @@ void TheoryStrings::checkExtfInference( Node n, Node nr, ExtfInfoTmp& in, int ef else { // otherwise, must explain via base node - Node r = getRepresentative(n); + Node r = d_state.getRepresentative(n); // we have that: // d_eqc_to_const_exp[r] => d_eqc_to_const_base[r] = in.d_const // thus: // n = d_eqc_to_const_base[r] ^ d_eqc_to_const_exp[r] => n = in.d_const Assert(d_eqc_to_const_base.find(r) != d_eqc_to_const_base.end()); - addToExplanation(n, d_eqc_to_const_base[r], in.d_exp); + d_im.addToExplanation(n, d_eqc_to_const_base[r], in.d_exp); Assert(d_eqc_to_const_exp.find(r) != d_eqc_to_const_exp.end()); in.d_exp.insert(in.d_exp.end(), d_eqc_to_const_exp[r].begin(), @@ -2016,9 +1815,9 @@ void TheoryStrings::checkExtfInference( Node n, Node nr, ExtfInfoTmp& in, int ef Node conc = nm->mkNode(STRING_STRCTN, children); conc = Rewriter::rewrite(pol ? conc : conc.negate()); // check if it already (does not) hold - if (hasTerm(conc)) + if (d_state.hasTerm(conc)) { - if (areEqual(conc, d_false)) + if (d_state.areEqual(conc, d_false)) { // we are in conflict d_im.sendInference(in.d_exp, conc, "CTN_Decompose"); @@ -2082,12 +1881,12 @@ void TheoryStrings::checkExtfInference( Node n, Node nr, ExtfInfoTmp& in, int ef Node lit = pol ? conc : conc[0]; if (lit.getKind() == EQUAL) { - do_infer = pol ? !areEqual(lit[0], lit[1]) - : !areDisequal(lit[0], lit[1]); + do_infer = pol ? !d_state.areEqual(lit[0], lit[1]) + : !d_state.areDisequal(lit[0], lit[1]); } else { - do_infer = !areEqual(lit, pol ? d_true : d_false); + do_infer = !d_state.areEqual(lit, pol ? d_true : d_false); } if (do_infer) { @@ -2231,9 +2030,6 @@ void TheoryStrings::debugPrintFlatForms( const char * tc ){ Trace( tc ) << std::endl; } -void TheoryStrings::debugPrintNormalForms( const char * tc ) { -} - struct sortConstLength { std::map< Node, unsigned > d_const_length; bool operator() (Node i, Node j) { @@ -2324,7 +2120,7 @@ void TheoryStrings::checkFlatForms() // of ( n = f[n] ) std::vector exp; Assert(d_eqc_to_const_base.find(eqc) != d_eqc_to_const_base.end()); - addToExplanation(n, d_eqc_to_const_base[eqc], exp); + d_im.addToExplanation(n, d_eqc_to_const_base[eqc], exp); Assert(d_eqc_to_const_exp.find(eqc) != d_eqc_to_const_exp.end()); if (!d_eqc_to_const_exp[eqc].isNull()) { @@ -2337,7 +2133,7 @@ void TheoryStrings::checkFlatForms() Assert(e >= 0 && e < (int)d_flat_form_index[n].size()); Assert(d_flat_form_index[n][e] >= 0 && d_flat_form_index[n][e] < (int)n.getNumChildren()); - addToExplanation( + d_im.addToExplanation( d_flat_form[n][e], n[d_flat_form_index[n][e]], exp); } } @@ -2435,7 +2231,7 @@ void TheoryStrings::checkFlatForm(std::vector& eqc, Node curr_c = getConstantEqc(curr); Node ac = a[d_flat_form_index[a][count]]; std::vector lexp; - Node lcurr = getLength(ac, lexp); + Node lcurr = d_state.getLength(ac, lexp); for (unsigned i = 1; i < eqc_size; i++) { b = eqc[i]; @@ -2467,7 +2263,7 @@ void TheoryStrings::checkFlatForm(std::vector& eqc, { Node bc = b[d_flat_form_index[b][count]]; inelig.push_back(b); - Assert(!areEqual(curr, cc)); + Assert(!d_state.areEqual(curr, cc)); Node cc_c = getConstantEqc(cc); if (!curr_c.isNull() && !cc_c.isNull()) { @@ -2477,10 +2273,10 @@ void TheoryStrings::checkFlatForm(std::vector& eqc, cc_c, curr_c, index, isRev); if (s.isNull()) { - addToExplanation(ac, d_eqc_to_const_base[curr], exp); - addToExplanation(d_eqc_to_const_exp[curr], exp); - addToExplanation(bc, d_eqc_to_const_base[cc], exp); - addToExplanation(d_eqc_to_const_exp[cc], exp); + d_im.addToExplanation(ac, d_eqc_to_const_base[curr], exp); + d_im.addToExplanation(d_eqc_to_const_exp[curr], exp); + d_im.addToExplanation(bc, d_eqc_to_const_base[cc], exp); + d_im.addToExplanation(d_eqc_to_const_exp[cc], exp); conc = d_false; inf_type = 0; break; @@ -2497,8 +2293,8 @@ void TheoryStrings::checkFlatForm(std::vector& eqc, { // if lengths are the same, apply LengthEq std::vector lexp2; - Node lcc = getLength(bc, lexp2); - if (areEqual(lcurr, lcc)) + Node lcc = d_state.getLength(bc, lexp2); + if (d_state.areEqual(lcurr, lcc)) { Trace("strings-ff-debug") << "Infer " << ac << " == " << bc << " since " << lcurr @@ -2519,7 +2315,7 @@ void TheoryStrings::checkFlatForm(std::vector& eqc, } exp.insert(exp.end(), lexp.begin(), lexp.end()); exp.insert(exp.end(), lexp2.begin(), lexp2.end()); - addToExplanation(lcurr, lcc, exp); + d_im.addToExplanation(lcurr, lcc, exp); conc = ac.eqNode(bc); inf_type = 1; break; @@ -2535,13 +2331,13 @@ void TheoryStrings::checkFlatForm(std::vector& eqc, Trace("strings-ff-debug") << "Found inference : " << conc << " based on equality " << a << " == " << b << ", " << isRev << " " << inf_type << std::endl; - addToExplanation(a, b, exp); + d_im.addToExplanation(a, b, exp); // explain why prefixes up to now were the same for (unsigned j = 0; j < count; j++) { Trace("strings-ff-debug") << "Add at " << d_flat_form_index[a][j] << " " << d_flat_form_index[b][j] << std::endl; - addToExplanation( + d_im.addToExplanation( a[d_flat_form_index[a][j]], b[d_flat_form_index[b][j]], exp); } // explain why other components up to now are empty @@ -2564,9 +2360,9 @@ void TheoryStrings::checkFlatForm(std::vector& eqc, int endj = isRev ? c.getNumChildren() : jj; for (int j = startj; j < endj; j++) { - if (areEqual(c[j], d_emptyString)) + if (d_state.areEqual(c[j], d_emptyString)) { - addToExplanation(c[j], d_emptyString, exp); + d_im.addToExplanation(c[j], d_emptyString, exp); } } } @@ -2615,7 +2411,7 @@ Node TheoryStrings::checkCycles( Node eqc, std::vector< Node >& curr, std::vecto d_eqc[eqc].push_back( n ); } for( unsigned i=0; i& curr, std::vecto Node ncy = checkCycles( nr, curr, exp ); if( !ncy.isNull() ){ Trace("strings-cycle") << eqc << " cycle: " << ncy << " at " << n << "[" << i << "] : " << n[i] << std::endl; - addToExplanation( n, eqc, exp ); - addToExplanation( nr, n[i], exp ); + d_im.addToExplanation(n, eqc, exp); + d_im.addToExplanation(nr, n[i], exp); if( ncy==eqc ){ //can infer all other components must be empty for( unsigned j=0; j::iterator itn = nf_to_eqc.find(nf_term); if (itn != nf_to_eqc.end()) { @@ -2778,7 +2575,7 @@ void TheoryStrings::checkCodes() Node cp = getProxyVariableFor(c); AlwaysAssert(!cp.isNull()); Node vc = nm->mkNode(STRING_CODE, cp); - if (!areEqual(cc, vc)) + if (!d_state.areEqual(cc, vc)) { d_im.sendInference(d_empty_vec, cc.eqNode(vc), "Code_Proxy"); } @@ -2786,10 +2583,10 @@ void TheoryStrings::checkCodes() } else { - EqcInfo* ei = getOrMakeEqcInfo(eqc, false); - if (ei && !ei->d_code_term.get().isNull()) + EqcInfo* ei = d_state.getOrMakeEqcInfo(eqc, false); + if (ei && !ei->d_codeTerm.get().isNull()) { - Node vc = nm->mkNode(kind::STRING_CODE, ei->d_code_term.get()); + Node vc = nm->mkNode(kind::STRING_CODE, ei->d_codeTerm.get()); nconst_codes.push_back(vc); } } @@ -2810,7 +2607,7 @@ void TheoryStrings::checkCodes() { Trace("strings-code-debug") << "Compare codes : " << c1 << " " << c2 << std::endl; - if (!areDisequal(c1, c2) && !areEqual(c1, d_neg_one)) + if (!d_state.areDisequal(c1, c2) && !d_state.areEqual(c1, d_neg_one)) { Node eq_no = c1.eqNode(d_neg_one); Node deq = c1.eqNode(c2).negate(); @@ -2828,19 +2625,22 @@ void TheoryStrings::checkCodes() //compute d_normal_forms_(base,exp,exp_depend)[eqc] void TheoryStrings::normalizeEquivalenceClass( Node eqc ) { Trace("strings-process-debug") << "Process equivalence class " << eqc << std::endl; - if( areEqual( eqc, d_emptyString ) ) { + if (d_state.areEqual(eqc, d_emptyString)) + { #ifdef CVC4_ASSERTIONS for( unsigned j=0; j exp; Assert( d_eqc_to_const_base.find( eqc )!=d_eqc_to_const_base.end() ); - addToExplanation( n, d_eqc_to_const_base[eqc], exp ); + d_im.addToExplanation(n, d_eqc_to_const_base[eqc], exp); Assert( d_eqc_to_const_exp.find( eqc )!=d_eqc_to_const_exp.end() ); if( !d_eqc_to_const_exp[eqc].isNull() ){ exp.push_back( d_eqc_to_const_exp[eqc] ); @@ -3251,7 +3050,7 @@ void TheoryStrings::processSimpleNEq(NormalForm& nfi, //can infer that this string must be empty Node eq = nfkv[index_k].eqNode(d_emptyString); //Trace("strings-lemma") << "Strings: Infer " << eq << " from " << eq_exp << std::endl; - Assert(!areEqual(d_emptyString, nfkv[index_k])); + Assert(!d_state.areEqual(d_emptyString, nfkv[index_k])); d_im.sendInference(curr_exp, eq, "N_EndpointEmp"); index_k++; } @@ -3265,12 +3064,13 @@ void TheoryStrings::processSimpleNEq(NormalForm& nfi, index++; success = true; }else{ - Assert(!areEqual(nfiv[index], nfjv[index])); + Assert(!d_state.areEqual(nfiv[index], nfjv[index])); std::vector< Node > temp_exp; - Node length_term_i = getLength(nfiv[index], temp_exp); - Node length_term_j = getLength(nfjv[index], temp_exp); + Node length_term_i = d_state.getLength(nfiv[index], temp_exp); + Node length_term_j = d_state.getLength(nfjv[index], temp_exp); // check length(nfiv[index]) == length(nfjv[index]) - if( areEqual( length_term_i, length_term_j ) ){ + if (d_state.areEqual(length_term_i, length_term_j)) + { Trace("strings-solve-debug") << "Simple Case 2 : string lengths are equal" << std::endl; Node eq = nfiv[index].eqNode(nfjv[index]); //eq = Rewriter::rewrite( eq ); @@ -3306,13 +3106,16 @@ void TheoryStrings::processSimpleNEq(NormalForm& nfi, eqnc.push_back(nfkv[index_l]); } } - eqn.push_back( mkConcat( eqnc ) ); + eqn.push_back(utils::mkNConcat(eqnc)); } - if( !areEqual( eqn[0], eqn[1] ) ){ + if (!d_state.areEqual(eqn[0], eqn[1])) + { d_im.sendInference( antec, eqn[0].eqNode(eqn[1]), "N_EndpointEq", true); return; - }else{ + } + else + { Assert(nfiv.size() == nfjv.size()); index = nfiv.size() - rproc; } @@ -3367,11 +3170,11 @@ void TheoryStrings::processSimpleNEq(NormalForm& nfi, bool info_valid = false; Assert(index < nfiv.size() - rproc && index < nfjv.size() - rproc); std::vector< Node > lexp; - Node length_term_i = getLength(nfiv[index], lexp); - Node length_term_j = getLength(nfjv[index], lexp); + Node length_term_i = d_state.getLength(nfiv[index], lexp); + Node length_term_j = d_state.getLength(nfjv[index], lexp); //split on equality between string lengths (note that splitting on equality between strings is worse since it is harder to process) - if (!areDisequal(length_term_i, length_term_j) - && !areEqual(length_term_i, length_term_j) + if (!d_state.areDisequal(length_term_i, length_term_j) + && !d_state.areEqual(length_term_i, length_term_j) && !nfiv[index].isConst() && !nfjv[index].isConst()) { // AJR: remove the latter 2 conditions? Trace("strings-solve-debug") << "Non-simple Case 1 : string lengths neither equal nor disequal" << std::endl; @@ -3494,7 +3297,9 @@ void TheoryStrings::processSimpleNEq(NormalForm& nfi, "c_spt"); Trace("strings-csp") << "Const Split: " << prea << " is removed from " << stra << " due to " << strb << ", p=" << p << std::endl; //set info - info.d_conc = other_str.eqNode( isRev ? mkConcat( sk, prea ) : mkConcat(prea, sk) ); + info.d_conc = other_str.eqNode( + isRev ? utils::mkNConcat(sk, prea) + : utils::mkNConcat(prea, sk)); info.d_new_skolem[LENGTH_SPLIT].push_back(sk); info.d_id = INFER_SSPLIT_CST_PROP; info_valid = true; @@ -3517,10 +3322,17 @@ void TheoryStrings::processSimpleNEq(NormalForm& nfi, : SkolemCache::SK_ID_VC_BIN_SPT, "cb_spt"); Trace("strings-csp") << "Const Split: " << c_firstHalf << " is removed from " << const_str << " (binary) " << std::endl; - info.d_conc = NodeManager::currentNM()->mkNode( kind::OR, other_str.eqNode( isRev ? mkConcat( sk, c_firstHalf ) : mkConcat( c_firstHalf, sk ) ), - NodeManager::currentNM()->mkNode( kind::AND, - sk.eqNode( d_emptyString ).negate(), - c_firstHalf.eqNode( isRev ? mkConcat( sk, other_str ) : mkConcat( other_str, sk ) ) ) ); + info.d_conc = nm->mkNode( + OR, + other_str.eqNode( + isRev ? utils::mkNConcat(sk, c_firstHalf) + : utils::mkNConcat(c_firstHalf, sk)), + nm->mkNode( + AND, + sk.eqNode(d_emptyString).negate(), + c_firstHalf.eqNode( + isRev ? utils::mkNConcat(sk, other_str) + : utils::mkNConcat(other_str, sk)))); info.d_new_skolem[LENGTH_SPLIT].push_back(sk); info.d_id = INFER_SSPLIT_CST_BINARY; info_valid = true; @@ -3533,7 +3345,9 @@ void TheoryStrings::processSimpleNEq(NormalForm& nfi, : SkolemCache::SK_ID_VC_SPT, "c_spt"); Trace("strings-csp") << "Const Split: " << firstChar << " is removed from " << const_str << " (serial) " << std::endl; - info.d_conc = other_str.eqNode( isRev ? mkConcat( sk, firstChar ) : mkConcat(firstChar, sk) ); + info.d_conc = other_str.eqNode( + isRev ? utils::mkNConcat(sk, firstChar) + : utils::mkNConcat(firstChar, sk)); info.d_new_skolem[LENGTH_SPLIT].push_back(sk); info.d_id = INFER_SSPLIT_CST; info_valid = true; @@ -3585,12 +3399,12 @@ void TheoryStrings::processSimpleNEq(NormalForm& nfi, "v_spt"); // must add length requirement info.d_new_skolem[LENGTH_GEQ_ONE].push_back(sk); - Node eq1 = - nfiv[index].eqNode(isRev ? mkConcat(sk, nfjv[index]) - : mkConcat(nfjv[index], sk)); - Node eq2 = - nfjv[index].eqNode(isRev ? mkConcat(sk, nfiv[index]) - : mkConcat(nfiv[index], sk)); + Node eq1 = nfiv[index].eqNode( + isRev ? utils::mkNConcat(sk, nfjv[index]) + : utils::mkNConcat(nfjv[index], sk)); + Node eq2 = nfjv[index].eqNode( + isRev ? utils::mkNConcat(sk, nfiv[index]) + : utils::mkNConcat(nfiv[index], sk)); if( lentTestSuccess!=-1 ){ info.d_antn.push_back( lentTestExp ); @@ -3686,15 +3500,15 @@ TheoryStrings::ProcessLoopResult TheoryStrings::processLoop(NormalForm& nfi, Trace("strings-loop") << " ... (X)= " << vecoi[index] << std::endl; Trace("strings-loop") << " ... T(Y.Z)= "; std::vector vec_t(veci.begin() + index, veci.begin() + loop_index); - Node t_yz = mkConcat(vec_t); + Node t_yz = utils::mkNConcat(vec_t); Trace("strings-loop") << " (" << t_yz << ")" << std::endl; Trace("strings-loop") << " ... S(Z.Y)= "; std::vector vec_s(vecoi.begin() + index + 1, vecoi.end()); - Node s_zy = mkConcat(vec_s); + Node s_zy = utils::mkNConcat(vec_s); Trace("strings-loop") << s_zy << std::endl; Trace("strings-loop") << " ... R= "; std::vector vec_r(veci.begin() + loop_index + 1, veci.end()); - Node r = mkConcat(vec_r); + Node r = utils::mkNConcat(vec_r); Trace("strings-loop") << r << std::endl; if (s_zy.isConst() && r.isConst() && r != d_emptyString) @@ -3731,7 +3545,7 @@ TheoryStrings::ProcessLoopResult TheoryStrings::processLoop(NormalForm& nfi, // the equality could rewrite to false if (!split_eqr.isConst()) { - if (!areDisequal(t, d_emptyString)) + if (!d_state.areDisequal(t, d_emptyString)) { // try to make t equal to empty to avoid loop info.d_conc = nm->mkNode(kind::OR, split_eq, split_eq.negate()); @@ -3786,12 +3600,12 @@ TheoryStrings::ProcessLoopResult TheoryStrings::processLoop(NormalForm& nfi, std::vector v2(vec_r); v2.insert(v2.begin(), y); v2.insert(v2.begin(), z); - restr = mkConcat(z, y); - cc = Rewriter::rewrite(s_zy.eqNode(mkConcat(v2))); + restr = utils::mkNConcat(z, y); + cc = Rewriter::rewrite(s_zy.eqNode(utils::mkNConcat(v2))); } else { - cc = Rewriter::rewrite(s_zy.eqNode(mkConcat(z, y))); + cc = Rewriter::rewrite(s_zy.eqNode(utils::mkNConcat(z, y))); } if (cc == d_false) { @@ -3831,13 +3645,13 @@ TheoryStrings::ProcessLoopResult TheoryStrings::processLoop(NormalForm& nfi, registerLength(sk_y, LENGTH_GEQ_ONE); Node sk_z = d_sk_cache.mkSkolem("z_loop"); // t1 * ... * tn = y * z - Node conc1 = t_yz.eqNode(mkConcat(sk_y, sk_z)); + Node conc1 = t_yz.eqNode(utils::mkNConcat(sk_y, sk_z)); // s1 * ... * sk = z * y * r vec_r.insert(vec_r.begin(), sk_y); vec_r.insert(vec_r.begin(), sk_z); - Node conc2 = s_zy.eqNode(mkConcat(vec_r)); - Node conc3 = vecoi[index].eqNode(mkConcat(sk_y, sk_w)); - Node restr = r == d_emptyString ? s_zy : mkConcat(sk_z, sk_y); + Node conc2 = s_zy.eqNode(utils::mkNConcat(vec_r)); + Node conc3 = vecoi[index].eqNode(utils::mkNConcat(sk_y, sk_w)); + Node restr = r == d_emptyString ? s_zy : utils::mkNConcat(sk_z, sk_y); str_in_re = nm->mkNode(kind::STRING_IN_REGEXP, sk_w, @@ -3864,7 +3678,6 @@ TheoryStrings::ProcessLoopResult TheoryStrings::processLoop(NormalForm& nfi, //return true for lemma, false if we succeed void TheoryStrings::processDeq( Node ni, Node nj ) { NodeManager* nm = NodeManager::currentNM(); - //Assert( areDisequal( ni, nj ) ); NormalForm& nfni = getNormalForm(ni); NormalForm& nfnj = getNormalForm(nj); if (nfni.d_nf.size() > 1 || nfnj.d_nf.size() > 1) @@ -3894,12 +3707,14 @@ void TheoryStrings::processDeq( Node ni, Node nj ) { Node i = nfi[index]; Node j = nfj[index]; Trace("strings-solve-debug") << "...Processing(DEQ) " << i << " " << j << std::endl; - if( !areEqual( i, j ) ){ + if (!d_state.areEqual(i, j)) + { Assert( i.getKind()!=kind::CONST_STRING || j.getKind()!=kind::CONST_STRING ); std::vector< Node > lexp; - Node li = getLength( i, lexp ); - Node lj = getLength( j, lexp ); - if( areDisequal( li, lj ) ){ + Node li = d_state.getLength(i, lexp); + Node lj = d_state.getLength(j, lexp); + if (d_state.areDisequal(li, lj)) + { if( i.getKind()==kind::CONST_STRING || j.getKind()==kind::CONST_STRING ){ //check if empty Node const_k = i.getKind() == kind::CONST_STRING ? i : j; @@ -3914,10 +3729,14 @@ void TheoryStrings::processDeq( Node ni, Node nj ) { //split on first character CVC4::String str = const_k.getConst(); Node firstChar = str.size() == 1 ? const_k : NodeManager::currentNM()->mkConst( str.prefix( 1 ) ); - if( areEqual( lnck, d_one ) ){ - if( areDisequal( firstChar, nconst_k ) ){ + if (d_state.areEqual(lnck, d_one)) + { + if (d_state.areDisequal(firstChar, nconst_k)) + { return; - }else if( !areEqual( firstChar, nconst_k ) ){ + } + else if (!d_state.areEqual(firstChar, nconst_k)) + { //splitting on demand : try to make them disequal if (d_im.sendSplit( firstChar, nconst_k, "S-Split(DEQL-Const)", false)) @@ -3925,7 +3744,9 @@ void TheoryStrings::processDeq( Node ni, Node nj ) { return; } } - }else{ + } + else + { Node sk = d_sk_cache.mkSkolemCached( nconst_k, SkolemCache::SK_ID_DC_SPT, "dc_spt"); registerLength(sk, LENGTH_ONE); @@ -3961,9 +3782,12 @@ void TheoryStrings::processDeq( Node ni, Node nj ) { antec.insert(antec.end(), nfni.d_exp.begin(), nfni.d_exp.end()); antec.insert(antec.end(), nfnj.d_exp.begin(), nfnj.d_exp.end()); //check disequal - if( areDisequal( ni, nj ) ){ + if (d_state.areDisequal(ni, nj)) + { antec.push_back( ni.eqNode( nj ).negate() ); - }else{ + } + else + { antec_new_lits.push_back( ni.eqNode( nj ).negate() ); } antec_new_lits.push_back( li.eqNode( lj ).negate() ); @@ -3977,24 +3801,30 @@ void TheoryStrings::processDeq( Node ni, Node nj ) { registerLength(sk3, LENGTH_GEQ_ONE); //Node nemp = sk3.eqNode(d_emptyString).negate(); //conc.push_back(nemp); - Node lsk1 = mkLength( sk1 ); + Node lsk1 = utils::mkNLength(sk1); conc.push_back( lsk1.eqNode( li ) ); - Node lsk2 = mkLength( sk2 ); + Node lsk2 = utils::mkNLength(sk2); conc.push_back( lsk2.eqNode( lj ) ); - conc.push_back( NodeManager::currentNM()->mkNode( kind::OR, j.eqNode( mkConcat( sk1, sk3 ) ), i.eqNode( mkConcat( sk2, sk3 ) ) ) ); + conc.push_back(nm->mkNode(OR, + j.eqNode(utils::mkNConcat(sk1, sk3)), + i.eqNode(utils::mkNConcat(sk2, sk3)))); d_im.sendInference( antec, antec_new_lits, nm->mkNode(AND, conc), "D-DISL-Split"); ++(d_statistics.d_deq_splits); return; } - }else if( areEqual( li, lj ) ){ - Assert( !areDisequal( i, j ) ); + } + else if (d_state.areEqual(li, lj)) + { + Assert(!d_state.areDisequal(i, j)); //splitting on demand : try to make them disequal if (d_im.sendSplit(i, j, "S-Split(DEQL)", false)) { return; } - }else{ + } + else + { //splitting on demand : try to make lengths equal if (d_im.sendSplit(li, lj, "D-Split")) { @@ -4054,8 +3884,8 @@ int TheoryStrings::processSimpleDeq( std::vector< Node >& nfi, std::vector< Node Trace("strings-solve-debug") << "Disequality normalize empty" << std::endl; std::vector< Node > ant; //we have a conflict : because the lengths are equal, the remainder needs to be empty, which will lead to a conflict - Node lni = getLengthExp(ni, ant, nfni.d_base); - Node lnj = getLengthExp(nj, ant, nfnj.d_base); + Node lni = d_state.getLengthExp(ni, ant, nfni.d_base); + Node lnj = d_state.getLengthExp(nj, ant, nfnj.d_base); ant.push_back( lni.eqNode( lnj ) ); ant.insert(ant.end(), nfni.d_exp.begin(), nfni.d_exp.end()); ant.insert(ant.end(), nfnj.d_exp.begin(), nfnj.d_exp.end()); @@ -4072,7 +3902,8 @@ int TheoryStrings::processSimpleDeq( std::vector< Node >& nfi, std::vector< Node Node i = nfi[index]; Node j = nfj[index]; Trace("strings-solve-debug") << "...Processing(QED) " << i << " " << j << std::endl; - if( !areEqual( i, j ) ) { + if (!d_state.areEqual(i, j)) + { if( i.getKind()==kind::CONST_STRING && j.getKind()==kind::CONST_STRING ) { unsigned int len_short = i.getConst().size() < j.getConst().size() ? i.getConst().size() : j.getConst().size(); bool isSameFix = isRev ? i.getConst().rstrncmp(j.getConst(), len_short): i.getConst().strncmp(j.getConst(), len_short); @@ -4102,13 +3933,16 @@ int TheoryStrings::processSimpleDeq( std::vector< Node >& nfi, std::vector< Node } }else{ std::vector< Node > lexp; - Node li = getLength( i, lexp ); - Node lj = getLength( j, lexp ); - if( areEqual( li, lj ) && areDisequal( i, j ) ){ + Node li = d_state.getLength(i, lexp); + Node lj = d_state.getLength(j, lexp); + if (d_state.areEqual(li, lj) && d_state.areDisequal(i, j)) + { Trace("strings-solve") << "Simple Case 2 : found equal length disequal sub strings " << i << " " << j << std::endl; //we are done: D-Remove return 1; - }else{ + } + else + { return 0; } } @@ -4256,7 +4090,7 @@ void TheoryStrings::registerTerm( Node n, int effort ) { { d_has_str_code = true; // ite( str.len(s)==1, 0 <= str.code(s) < num_codes, str.code(s)=-1 ) - Node code_len = mkLength(n[0]).eqNode(d_one); + Node code_len = utils::mkNLength(n[0]).eqNode(d_one); Node code_eq_neg1 = n.eqNode(d_neg_one); Node code_range = nm->mkNode( AND, @@ -4269,7 +4103,7 @@ void TheoryStrings::registerTerm( Node n, int effort ) { } else if (n.getKind() == STRING_STRIDOF) { - Node len = mkLength(n[0]); + Node len = utils::mkNLength(n[0]); Node lem = nm->mkNode(AND, nm->mkNode(GEQ, n, nm->mkConst(Rational(-1))), nm->mkNode(LT, n, len)); @@ -4358,22 +4192,6 @@ void TheoryStrings::registerLength(Node n, LengthStatus s) } } -Node TheoryStrings::mkConcat( Node n1, Node n2 ) { - return Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, n1, n2 ) ); -} - -Node TheoryStrings::mkConcat( Node n1, Node n2, Node n3 ) { - return Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, n1, n2, n3 ) ); -} - -Node TheoryStrings::mkConcat( const std::vector< Node >& c ) { - return Rewriter::rewrite( c.size()>1 ? NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, c ) : ( c.size()==1 ? c[0] : d_emptyString ) ); -} - -Node TheoryStrings::mkLength( Node t ) { - return Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t ) ); -} - Node TheoryStrings::mkExplain(const std::vector& a) { std::vector< Node > an; @@ -4396,8 +4214,8 @@ Node TheoryStrings::mkExplain(const std::vector& a, Debug("strings-explain") << "Add to explanation " << apc << std::endl; if (apc.getKind() == NOT && apc[0].getKind() == EQUAL) { - Assert(hasTerm(apc[0][0])); - Assert(hasTerm(apc[0][1])); + Assert(d_equalityEngine.hasTerm(apc[0][0])); + Assert(d_equalityEngine.hasTerm(apc[0][1])); // ensure that we are ready to explain the disequality AlwaysAssert(d_equalityEngine.areDisequal(apc[0][0], apc[0][1], true)); } @@ -4442,14 +4260,15 @@ void TheoryStrings::checkNormalFormsDeq() processed[n[0]][n[1]] = true; Node lt[2]; for( unsigned i=0; i<2; i++ ){ - EqcInfo* ei = getOrMakeEqcInfo( n[i], false ); - lt[i] = ei ? ei->d_length_term : Node::null(); + EqcInfo* ei = d_state.getOrMakeEqcInfo(n[i], false); + lt[i] = ei ? ei->d_lengthTerm : Node::null(); if( lt[i].isNull() ){ lt[i] = eq[i]; } lt[i] = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, lt[i] ); } - if( !areEqual( lt[0], lt[1] ) && !areDisequal( lt[0], lt[1] ) ){ + if (!d_state.areEqual(lt[0], lt[1]) && !d_state.areDisequal(lt[0], lt[1])) + { d_im.sendSplit(lt[0], lt[1], "DEQ-LENGTH-SP"); } } @@ -4480,7 +4299,7 @@ void TheoryStrings::checkNormalFormsDeq() } else { - if (areDisequal(cols[i][j], cols[i][k])) + if (d_state.areDisequal(cols[i][j], cols[i][k])) { Assert(!d_conflict); if (Trace.isOn("strings-solve")) @@ -4511,13 +4330,14 @@ void TheoryStrings::checkLengthsEqc() { NormalForm& nfi = getNormalForm(d_strings_eqc[i]); Trace("strings-process-debug") << "Process length constraints for " << d_strings_eqc[i] << std::endl; //check if there is a length term for this equivalence class - EqcInfo* ei = getOrMakeEqcInfo( d_strings_eqc[i], false ); - Node lt = ei ? ei->d_length_term : Node::null(); + EqcInfo* ei = d_state.getOrMakeEqcInfo(d_strings_eqc[i], false); + Node lt = ei ? ei->d_lengthTerm : Node::null(); if( !lt.isNull() ) { Node llt = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, lt ); //now, check if length normalization has occurred - if( ei->d_normalized_length.get().isNull() ) { - Node nf = mkConcat(nfi.d_nf); + if (ei->d_normalizedLength.get().isNull()) + { + Node nf = utils::mkNConcat(nfi.d_nf); if( Trace.isOn("strings-process-debug") ){ Trace("strings-process-debug") << " normal form is " << nf << " from base " << nfi.d_base @@ -4536,17 +4356,17 @@ void TheoryStrings::checkLengthsEqc() { Node lc = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, nf ); Node lcr = Rewriter::rewrite( lc ); Trace("strings-process-debug") << "Rewrote length " << lc << " to " << lcr << std::endl; - if (!areEqual(llt, lcr)) + if (!d_state.areEqual(llt, lcr)) { Node eq = llt.eqNode(lcr); - ei->d_normalized_length.set( eq ); + ei->d_normalizedLength.set(eq); d_im.sendInference(ant, eq, "LEN-NORM", true); } } }else{ Trace("strings-process-debug") << "No length term for eqc " << d_strings_eqc[i] << " " << d_eqc_to_len_term[d_strings_eqc[i]] << std::endl; if( !options::stringEagerLen() ){ - Node c = mkConcat(nfi.d_nf); + Node c = utils::mkNConcat(nfi.d_nf); registerTerm( c, 3 ); } } @@ -4594,9 +4414,12 @@ void TheoryStrings::checkCardinality() { bool success = true; while( rmkConst( Rational(r) ); - if( areDisequal( rr, lr ) ){ + if (d_state.areDisequal(rr, lr)) + { r++; - }else{ + } + else + { success = false; } } @@ -4612,7 +4435,8 @@ void TheoryStrings::checkCardinality() { itr1 != cols[i].end(); ++itr1) { for( std::vector< Node >::iterator itr2 = itr1 + 1; itr2 != cols[i].end(); ++itr2) { - if(!areDisequal( *itr1, *itr2 )) { + if (!d_state.areDisequal(*itr1, *itr2)) + { // add split lemma if (d_im.sendSplit(*itr1, *itr2, "CARD-SP")) { @@ -4621,9 +4445,12 @@ void TheoryStrings::checkCardinality() { } } } - EqcInfo* ei = getOrMakeEqcInfo( lr, true ); - Trace("strings-card") << "Previous cardinality used for " << lr << " is " << ((int)ei->d_cardinality_lem_k.get()-1) << std::endl; - if( int_k+1 > ei->d_cardinality_lem_k.get() ){ + EqcInfo* ei = d_state.getOrMakeEqcInfo(lr, true); + Trace("strings-card") + << "Previous cardinality used for " << lr << " is " + << ((int)ei->d_cardinalityLemK.get() - 1) << std::endl; + if (int_k + 1 > ei->d_cardinalityLemK.get()) + { Node k_node = NodeManager::currentNM()->mkConst( ::CVC4::Rational( int_k ) ); //add cardinality lemma Node dist = NodeManager::currentNM()->mkNode( kind::DISTINCT, cols[i] ); @@ -4640,7 +4467,7 @@ void TheoryStrings::checkCardinality() { Node len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, cols[i][0] ); Node cons = NodeManager::currentNM()->mkNode( kind::GEQ, len, k_node ); cons = Rewriter::rewrite( cons ); - ei->d_cardinality_lem_k.set( int_k+1 ); + ei->d_cardinalityLemK.set(int_k + 1); if( cons!=d_true ){ d_im.sendInference( d_empty_vec, vec_node, cons, "CARDINALITY", true); @@ -4653,18 +4480,6 @@ void TheoryStrings::checkCardinality() { Trace("strings-card") << "...end check cardinality" << std::endl; } -void TheoryStrings::getEquivalenceClasses( std::vector< Node >& eqcs ) { - eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); - while( !eqcs_i.isFinished() ) { - Node eqc = (*eqcs_i); - //if eqc.getType is string - if (eqc.getType().isString()) { - eqcs.push_back( eqc ); - } - ++eqcs_i; - } -} - void TheoryStrings::separateByLength(std::vector< Node >& n, std::vector< std::vector< Node > >& cols, std::vector< Node >& lts ) { @@ -4675,8 +4490,8 @@ void TheoryStrings::separateByLength(std::vector< Node >& n, for( unsigned i=0; id_length_term : Node::null(); + EqcInfo* ei = d_state.getOrMakeEqcInfo(eqc, false); + Node lt = ei ? ei->d_lengthTerm : Node::null(); if( !lt.isNull() ){ lt = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, lt ); Node r = d_equalityEngine.getRepresentative( lt ); diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 94811636c..9db40f8fe 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -31,6 +31,7 @@ #include "theory/strings/regexp_operation.h" #include "theory/strings/regexp_solver.h" #include "theory/strings/skolem_cache.h" +#include "theory/strings/solver_state.h" #include "theory/strings/theory_strings_preprocess.h" #include "theory/theory.h" #include "theory/uf/equality_engine.h" @@ -191,42 +192,7 @@ class TheoryStrings : public Theory { } };/* class TheoryStrings::NotifyClass */ - //--------------------------- equality engine - /** - * Get the representative of t in the equality engine of this class, or t - * itself if it is not registered as a term. - */ - Node getRepresentative(Node t); - /** Is t registered as a term in the equality engine of this class? */ - bool hasTerm(Node a); - /** - * Are a and b equal according to the equality engine of this class? Also - * returns true if a and b are identical. - */ - bool areEqual(Node a, Node b); - /** - * Are a and b disequal according to the equality engine of this class? Also - * returns true if the representative of a and b are distinct constants. - */ - bool areDisequal(Node a, Node b); - //--------------------------- end equality engine - //--------------------------- helper functions - /** get length with explanation - * - * If possible, this returns an arithmetic term that exists in the current - * context that is equal to the length of te, or otherwise returns the - * length of t. It adds to exp literals that hold in the current context that - * explain why that term is equal to the length of t. For example, if - * we have assertions: - * len( x ) = 5 ^ z = x ^ x = y, - * then getLengthExp( z, exp, y ) returns len( x ) and adds { z = x } to - * exp. On the other hand, getLengthExp( z, exp, x ) returns len( x ) and - * adds nothing to exp. - */ - Node getLengthExp(Node t, std::vector& exp, Node te); - /** shorthand for getLengthExp(t, exp, t) */ - Node getLength(Node t, std::vector& exp); /** get normal string * * This method returns the node that is equivalent to the normal form of x, @@ -252,12 +218,12 @@ class TheoryStrings : public Theory { NotifyClass d_notify; /** Equaltity engine */ eq::EqualityEngine d_equalityEngine; + /** The solver state object */ + SolverState d_state; /** The (custom) output channel of the theory of strings */ InferenceManager d_im; /** Are we in conflict */ context::CDO d_conflict; - /** Pending conflict */ - context::CDO d_pendingConflict; /** map from terms to their normal forms */ std::map d_normal_form; /** get normal form */ @@ -276,7 +242,6 @@ class TheoryStrings : public Theory { StringsPreprocess d_preproc; // extended functions inferences cache NodeSet d_extf_infer_cache; - NodeSet d_extf_infer_cache_u; std::vector< Node > d_empty_vec; // NodeList d_ee_disequalities; @@ -327,7 +292,11 @@ private: public: Node d_data; std::map< TNode, TermIndex > d_children; - Node add( TNode n, unsigned index, TheoryStrings* t, Node er, std::vector< Node >& c ); + Node add(TNode n, + unsigned index, + const SolverState& s, + Node er, + std::vector& c); void clear(){ d_children.clear(); } }; std::map< Kind, TermIndex > d_term_index; @@ -337,7 +306,6 @@ private: std::map< Node, std::vector< int > > d_flat_form_index; void debugPrintFlatForms( const char * tc ); - void debugPrintNormalForms( const char * tc ); ///////////////////////////////////////////////////////////////////////////// // MODEL GENERATION ///////////////////////////////////////////////////////////////////////////// @@ -359,55 +327,6 @@ private: EqualityStatus getEqualityStatus(TNode a, TNode b) override; private: - /** SAT-context-dependent information about an equivalence class */ - class EqcInfo { - public: - EqcInfo( context::Context* c ); - ~EqcInfo(){} - /** - * If non-null, this is a term x from this eq class such that str.len( x ) - * occurs as a term in this SAT context. - */ - context::CDO< Node > d_length_term; - /** - * If non-null, this is a term x from this eq class such that str.code( x ) - * occurs as a term in this SAT context. - */ - context::CDO d_code_term; - context::CDO< unsigned > d_cardinality_lem_k; - context::CDO< Node > d_normalized_length; - /** - * A node that explains the longest constant prefix known of this - * equivalence class. This can either be: - * (1) A term from this equivalence class, including a constant "ABC" or - * concatenation term (str.++ "ABC" ...), or - * (2) A membership of the form (str.in.re x R) where x is in this - * equivalence class and R is a regular expression of the form - * (str.to.re "ABC") or (re.++ (str.to.re "ABC") ...). - */ - context::CDO d_prefixC; - /** same as above, for suffix. */ - context::CDO d_suffixC; - /** add prefix constant - * - * This informs this equivalence class info that a term t in its - * equivalence class has a constant prefix (if isSuf=true) or suffix - * (if isSuf=false). The constant c (if non-null) is the value of that - * constant, if it has been computed already. - * - * If this method returns a non-null node ret, then ret is a conjunction - * corresponding to a conflict that holds in the current context. - */ - Node addEndpointConst(Node t, Node c, bool isSuf); - }; - /** map from representatives to information necessary for equivalence classes */ - std::map< Node, EqcInfo* > d_eqc_info; - /** - * 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 - * should currently be a representative of the equality engine of this class. - */ - EqcInfo * getOrMakeEqcInfo( Node eqc, bool doMake = true ); /** * Map string terms to their "proxy variables". Proxy variables are used are * intermediate variables so that length information can be communicated for @@ -643,15 +562,6 @@ private: int processSimpleDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj, unsigned& index, bool isRev ); //--------------------------end for checkNormalFormsDeq - //--------------------------------for checkMemberships - // check membership constraints - Node mkRegExpAntec(Node atom, Node ant); - bool checkPDerivative( Node x, Node r, Node atom, bool &addedLemma, std::vector< Node > &nf_exp); - //check contains - void checkPosContains( std::vector< Node >& posContains ); - void checkNegContains( std::vector< Node >& negContains ); - //--------------------------------end for checkMemberships - private: void addCarePairs(TNodeTrie* t1, TNodeTrie* t2, @@ -698,41 +608,12 @@ private: * of atom, including calls to registerTerm. */ void assertPendingFact(Node atom, bool polarity, Node exp); - /** add endpoints to eqc info - * - * This method is called when term t is the explanation for why equivalence - * class eqc may have a constant endpoint due to a concatentation term concat. - * For example, we may call this method on: - * t := (str.++ x y), concat := (str.++ x y), eqc - * for some eqc that is currently equal to t. Another example is: - * t := (str.in.re z (re.++ r s)), concat := (re.++ r s), eqc - * for some eqc that is currently equal to z. - */ - void addEndpointsToEqcInfo(Node t, Node concat, Node eqc); - /** set pending conflict - * - * If conf is non-null, this is called when conf is a conjunction of literals - * that hold in the current context that are unsatisfiable. It is set as the - * "pending conflict" to be processed as a conflict lemma on the output - * channel of this class. It is not sent out immediately since it may require - * explanation from the equality engine, and may be called at any time, e.g. - * during a merge operation, when the equality engine is not in a state to - * provide explanations. - */ - void setPendingConflictWhen(Node conf); /** * This processes the infer info ii as an inference. In more detail, it calls * the inference manager to process the inference, it introduces Skolems, and * updates the set of normal form pairs. */ void doInferInfo(const InferInfo& ii); - /** - * Adds equality a = b to the vector exp if a and b are distinct terms. It - * must be the case that areEqual( a, b ) holds in this context. - */ - void addToExplanation(Node a, Node b, std::vector& exp); - /** Adds lit to the vector exp if it is non-null */ - void addToExplanation(Node lit, std::vector& exp); /** Register term * @@ -754,18 +635,6 @@ private: */ void registerTerm(Node n, int effort); - /** - * Are we in conflict? This returns true if this theory has called its output - * channel's conflict method in the current SAT context. - */ - bool inConflict() const { return d_conflict; } - - /** mkConcat **/ - inline Node mkConcat(Node n1, Node n2); - inline Node mkConcat(Node n1, Node n2, Node n3); - inline Node mkConcat(const std::vector& c); - inline Node mkLength(Node n); - /** make explanation * * This returns a node corresponding to the explanation of formulas in a, @@ -778,18 +647,6 @@ private: protected: - /** get equivalence classes - * - * This adds the representative of all equivalence classes to eqcs - */ - void getEquivalenceClasses(std::vector& eqcs); - /** get relevant equivalence classes - * - * This adds the representative of all equivalence classes that contain at - * least one term in termSet. - */ - void getRelevantEquivalenceClasses(std::vector& eqcs, - std::set& termSet); // separate into collections with equal length void separateByLength(std::vector& n, diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp index d764b87c1..03c2419c4 100644 --- a/src/theory/strings/theory_strings_utils.cpp +++ b/src/theory/strings/theory_strings_utils.cpp @@ -16,6 +16,8 @@ #include "theory/strings/theory_strings_utils.h" +#include "theory/rewriter.h" + using namespace CVC4::kind; namespace CVC4 { @@ -101,7 +103,7 @@ void getConcat(Node n, std::vector& c) } } -Node mkConcat(Kind k, std::vector& c) +Node mkConcat(Kind k, const std::vector& c) { Assert(!c.empty() || k == STRING_CONCAT); NodeManager* nm = NodeManager::currentNM(); @@ -109,6 +111,28 @@ Node mkConcat(Kind k, std::vector& c) : (c.size() == 1 ? c[0] : nm->mkConst(String(""))); } +Node mkNConcat(Node n1, Node n2) +{ + return Rewriter::rewrite( + NodeManager::currentNM()->mkNode(STRING_CONCAT, n1, n2)); +} + +Node mkNConcat(Node n1, Node n2, Node n3) +{ + return Rewriter::rewrite( + NodeManager::currentNM()->mkNode(STRING_CONCAT, n1, n2, n3)); +} + +Node mkNConcat(const std::vector& c) +{ + return Rewriter::rewrite(mkConcat(STRING_CONCAT, c)); +} + +Node mkNLength(Node t) +{ + return Rewriter::rewrite(NodeManager::currentNM()->mkNode(STRING_LENGTH, t)); +} + Node getConstantComponent(Node t) { Kind tk = t.getKind(); diff --git a/src/theory/strings/theory_strings_utils.h b/src/theory/strings/theory_strings_utils.h index cadc98df3..2c84bd516 100644 --- a/src/theory/strings/theory_strings_utils.h +++ b/src/theory/strings/theory_strings_utils.h @@ -56,7 +56,27 @@ void getConcat(Node n, std::vector& c); * Make the concatentation from vector c * The kind k is either STRING_CONCAT or REGEXP_CONCAT. */ -Node mkConcat(Kind k, std::vector& c); +Node mkConcat(Kind k, const std::vector& c); + +/** + * Returns the rewritten form of the string concatenation of n1 and n2. + */ +Node mkNConcat(Node n1, Node n2); + +/** + * Returns the rewritten form of the string concatenation of n1, n2 and n3. + */ +Node mkNConcat(Node n1, Node n2, Node n3); + +/** + * Returns the rewritten form of the string concatenation of nodes in c. + */ +Node mkNConcat(const std::vector& c); + +/** + * Returns the rewritten form of the length of string term t. + */ +Node mkNLength(Node t); /** * Get constant component. Returns the string constant represented by the -- 2.30.2