diff options
| -rw-r--r-- | src/theory/strings/extf_solver.cpp | 48 | ||||
| -rw-r--r-- | src/theory/strings/extf_solver.h | 7 | ||||
| -rw-r--r-- | src/theory/strings/inference_manager.cpp | 99 | ||||
| -rw-r--r-- | src/theory/strings/inference_manager.h | 52 | ||||
| -rw-r--r-- | src/theory/strings/regexp_solver.cpp | 27 | ||||
| -rw-r--r-- | src/theory/strings/regexp_solver.h | 10 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 153 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings.h | 21 |
8 files changed, 221 insertions, 196 deletions
diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp index 1bcd67cb4..775b4a796 100644 --- a/src/theory/strings/extf_solver.cpp +++ b/src/theory/strings/extf_solver.cpp @@ -35,7 +35,7 @@ ExtfSolver::ExtfSolver(context::Context* c, StringsRewriter& rewriter, BaseSolver& bs, CoreSolver& cs, - ExtTheory* et, + ExtTheory& et, SequencesStatistics& statistics) : d_state(s), d_im(im), @@ -50,19 +50,19 @@ ExtfSolver::ExtfSolver(context::Context* c, d_extfInferCache(c), d_reduced(u) { - d_extt->addFunctionKind(kind::STRING_SUBSTR); - d_extt->addFunctionKind(kind::STRING_STRIDOF); - d_extt->addFunctionKind(kind::STRING_ITOS); - d_extt->addFunctionKind(kind::STRING_STOI); - d_extt->addFunctionKind(kind::STRING_STRREPL); - d_extt->addFunctionKind(kind::STRING_STRREPLALL); - d_extt->addFunctionKind(kind::STRING_STRCTN); - d_extt->addFunctionKind(kind::STRING_IN_REGEXP); - d_extt->addFunctionKind(kind::STRING_LEQ); - d_extt->addFunctionKind(kind::STRING_TO_CODE); - d_extt->addFunctionKind(kind::STRING_TOLOWER); - d_extt->addFunctionKind(kind::STRING_TOUPPER); - d_extt->addFunctionKind(kind::STRING_REV); + d_extt.addFunctionKind(kind::STRING_SUBSTR); + d_extt.addFunctionKind(kind::STRING_STRIDOF); + d_extt.addFunctionKind(kind::STRING_ITOS); + d_extt.addFunctionKind(kind::STRING_STOI); + d_extt.addFunctionKind(kind::STRING_STRREPL); + d_extt.addFunctionKind(kind::STRING_STRREPLALL); + d_extt.addFunctionKind(kind::STRING_STRCTN); + d_extt.addFunctionKind(kind::STRING_IN_REGEXP); + d_extt.addFunctionKind(kind::STRING_LEQ); + d_extt.addFunctionKind(kind::STRING_TO_CODE); + d_extt.addFunctionKind(kind::STRING_TOLOWER); + d_extt.addFunctionKind(kind::STRING_TOUPPER); + d_extt.addFunctionKind(kind::STRING_REV); d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); @@ -126,7 +126,7 @@ bool ExtfSolver::doReduction(int effort, Node n) } // this depends on the current assertions, so this // inference is context-dependent - d_extt->markReduced(n, true); + d_extt.markReduced(n, true); return true; } else @@ -173,7 +173,7 @@ bool ExtfSolver::doReduction(int effort, Node n) Trace("strings-red-lemma") << "Reduction (positive contains) lemma : " << n << " => " << eq << std::endl; // context-dependent because it depends on the polarity of n itself - d_extt->markReduced(n, true); + d_extt.markReduced(n, true); } else if (k != kind::STRING_TO_CODE) { @@ -206,7 +206,7 @@ void ExtfSolver::checkExtfReductions(int effort) // Notice we don't make a standard call to ExtTheory::doReductions here, // since certain optimizations like context-dependent reductions and // stratifying effort levels are done in doReduction below. - std::vector<Node> extf = d_extt->getActive(); + std::vector<Node> extf = d_extt.getActive(); Trace("strings-process") << " checking " << extf.size() << " active extf" << std::endl; for (const Node& n : extf) @@ -234,7 +234,7 @@ void ExtfSolver::checkExtfEval(int effort) d_extfInfoTmp.clear(); NodeManager* nm = NodeManager::currentNM(); bool has_nreduce = false; - std::vector<Node> terms = d_extt->getActive(); + std::vector<Node> terms = d_extt.getActive(); for (const Node& n : terms) { // Setup information about n, including if it is equal to a constant. @@ -281,7 +281,7 @@ void ExtfSolver::checkExtfEval(int effort) { if (effort < 3) { - d_extt->markReduced(n); + d_extt.markReduced(n); Trace("strings-extf-debug") << " resolvable by evaluation..." << std::endl; std::vector<Node> exps; @@ -445,7 +445,7 @@ void ExtfSolver::checkExtfEval(int effort) } Trace("strings-extf-list") << std::endl; } - if (d_extt->isActive(n) && einfo.d_modelActive) + if (d_extt.isActive(n) && einfo.d_modelActive) { has_nreduce = true; } @@ -525,10 +525,10 @@ void ExtfSolver::checkExtfInference(Node n, // we are in conflict d_im.sendInference(in.d_exp, conc, Inference::CTN_DECOMPOSE); } - else if (d_extt->hasFunctionKind(conc.getKind())) + else if (d_extt.hasFunctionKind(conc.getKind())) { // can mark as reduced, since model for n implies model for conc - d_extt->markReduced(conc); + d_extt.markReduced(conc); } } } @@ -613,7 +613,7 @@ void ExtfSolver::checkExtfInference(Node n, // satisfied by all models of str.contains( x, y ) ^ x=z and thus can // be ignored. Trace("strings-extf-debug") << " redundant." << std::endl; - d_extt->markReduced(n); + d_extt.markReduced(n); } } return; @@ -680,7 +680,7 @@ bool ExtfSolver::hasExtendedFunctions() const { return d_hasExtf.get(); } std::vector<Node> ExtfSolver::getActive(Kind k) const { - return d_extt->getActive(k); + return d_extt.getActive(k); } } // namespace strings diff --git a/src/theory/strings/extf_solver.h b/src/theory/strings/extf_solver.h index c5dd24f70..fb9b836db 100644 --- a/src/theory/strings/extf_solver.h +++ b/src/theory/strings/extf_solver.h @@ -91,7 +91,7 @@ class ExtfSolver StringsRewriter& rewriter, BaseSolver& bs, CoreSolver& cs, - ExtTheory* et, + ExtTheory& et, SequencesStatistics& statistics); ~ExtfSolver(); @@ -147,6 +147,7 @@ class ExtfSolver * checkExtfEval. */ const std::map<Node, ExtfInfoTmp>& getInfo() const; + //---------------------------------- information about ExtTheory /** Are there any active extended functions? */ bool hasExtendedFunctions() const; /** @@ -154,7 +155,7 @@ class ExtfSolver * context (see ExtTheory::getActive). */ std::vector<Node> getActive(Kind k) const; - + //---------------------------------- end information about ExtTheory private: /** do reduction * @@ -190,7 +191,7 @@ class ExtfSolver /** reference to the core solver, used for certain queries */ CoreSolver& d_csolver; /** the extended theory object for the theory of strings */ - ExtTheory* d_extt; + ExtTheory& d_extt; /** Reference to the statistics for the theory of strings/sequences. */ SequencesStatistics& d_statistics; /** preprocessing utility, for performing strings reductions */ diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp index b6bbcb7df..9d1c6fac4 100644 --- a/src/theory/strings/inference_manager.cpp +++ b/src/theory/strings/inference_manager.cpp @@ -14,11 +14,9 @@ #include "theory/strings/inference_manager.h" -#include "expr/kind.h" #include "options/strings_options.h" #include "theory/ext_theory.h" #include "theory/rewriter.h" -#include "theory/strings/theory_strings.h" #include "theory/strings/theory_strings_utils.h" #include "theory/strings/word.h" @@ -30,16 +28,16 @@ namespace CVC4 { namespace theory { namespace strings { -InferenceManager::InferenceManager(TheoryStrings& p, - context::Context* c, +InferenceManager::InferenceManager(context::Context* c, context::UserContext* u, SolverState& s, TermRegistry& tr, + ExtTheory& e, OutputChannel& out, SequencesStatistics& statistics) - : d_parent(p), - d_state(s), + : d_state(s), d_termReg(tr), + d_extt(e), d_out(out), d_statistics(statistics), d_keep(c) @@ -51,6 +49,14 @@ InferenceManager::InferenceManager(TheoryStrings& p, d_false = nm->mkConst(false); } +void InferenceManager::sendAssumption(TNode lit) +{ + bool polarity = lit.getKind() != kind::NOT; + TNode atom = polarity ? lit : lit[0]; + // assert pending fact + assertPendingFact(atom, polarity, lit); +} + bool InferenceManager::sendInternalInference(std::vector<Node>& exp, Node conc, Inference infer) @@ -294,6 +300,8 @@ void InferenceManager::sendPhaseRequirement(Node lit, bool pol) d_pendingReqPhase[lit] = pol; } +void InferenceManager::setIncomplete() { d_out.setIncomplete(); } + void InferenceManager::addToExplanation(Node a, Node b, std::vector<Node>& exp) const @@ -328,14 +336,14 @@ void InferenceManager::doPendingFacts() { bool polarity = lit.getKind() != NOT; TNode atom = polarity ? lit : lit[0]; - d_parent.assertPendingFact(atom, polarity, exp); + assertPendingFact(atom, polarity, exp); } } else { bool polarity = fact.getKind() != NOT; TNode atom = polarity ? fact : fact[0]; - d_parent.assertPendingFact(atom, polarity, exp); + assertPendingFact(atom, polarity, exp); } i++; } @@ -364,6 +372,68 @@ void InferenceManager::doPendingLemmas() d_pendingReqPhase.clear(); } +void InferenceManager::assertPendingFact(Node atom, bool polarity, Node exp) +{ + eq::EqualityEngine* ee = d_state.getEqualityEngine(); + Trace("strings-pending") << "Assert pending fact : " << atom << " " + << polarity << " from " << exp << std::endl; + Assert(atom.getKind() != OR) << "Infer error: a split."; + if (atom.getKind() == EQUAL) + { + // we must ensure these terms are registered + Trace("strings-pending-debug") << " Register term" << std::endl; + for (const Node& t : atom) + { + // terms in the equality engine are already registered, hence skip + // currently done for only string-like terms, but this could potentially + // be avoided. + if (!ee->hasTerm(t) && t.getType().isStringLike()) + { + d_termReg.registerTerm(t, 0); + } + } + Trace("strings-pending-debug") << " Now assert equality" << std::endl; + ee->assertEquality(atom, polarity, exp); + Trace("strings-pending-debug") << " Finished assert equality" << std::endl; + } + else + { + ee->assertPredicate(atom, polarity, exp); + if (atom.getKind() == STRING_IN_REGEXP) + { + if (polarity && atom[1].getKind() == REGEXP_CONCAT) + { + Node eqc = ee->getRepresentative(atom[0]); + d_state.addEndpointsToEqcInfo(atom, atom[1], eqc); + } + } + } + // process the conflict + if (!d_state.isInConflict()) + { + Node pc = d_state.getPendingConflict(); + if (!pc.isNull()) + { + std::vector<Node> a; + a.push_back(pc); + Trace("strings-pending") + << "Process pending conflict " << pc << std::endl; + Node conflictNode = mkExplain(a); + d_state.setConflict(); + Trace("strings-conflict") + << "CONFLICT: Eager prefix : " << conflictNode << std::endl; + ++(d_statistics.d_conflictsEagerPrefix); + d_out.conflict(conflictNode); + } + } + Trace("strings-pending-debug") << " Now collect terms" << std::endl; + // Collect extended function terms in the atom. Notice that we must register + // all extended functions occurring in assertions and shared terms. We + // make a similar call to registerTermRec in TheoryStrings::addSharedTerm. + d_extt.registerTermRec(atom); + Trace("strings-pending-debug") << " Finished collect terms" << std::endl; +} + bool InferenceManager::hasProcessed() const { return d_state.isInConflict() || !d_pendingLem.empty() || !d_pending.empty(); @@ -421,7 +491,7 @@ Node InferenceManager::mkExplain(const std::vector<Node>& a, } else { - ant = NodeManager::currentNM()->mkNode(kind::AND, antec_exp); + ant = NodeManager::currentNM()->mkNode(AND, antec_exp); } return ant; } @@ -466,18 +536,21 @@ void InferenceManager::explain(TNode literal, } } } -void InferenceManager::setIncomplete() { d_out.setIncomplete(); } void InferenceManager::markCongruent(Node a, Node b) { Assert(a.getKind() == b.getKind()); - ExtTheory* eth = d_parent.getExtTheory(); - if (eth->hasFunctionKind(a.getKind())) + if (d_extt.hasFunctionKind(a.getKind())) { - eth->markCongruent(a, b); + d_extt.markCongruent(a, b); } } +void InferenceManager::markReduced(Node n, bool contextDepend) +{ + d_extt.markReduced(n, contextDepend); +} + } // namespace strings } // namespace theory } // namespace CVC4 diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h index c1550328c..041724d8d 100644 --- a/src/theory/strings/inference_manager.h +++ b/src/theory/strings/inference_manager.h @@ -23,6 +23,7 @@ #include "context/cdhashset.h" #include "context/context.h" #include "expr/node.h" +#include "theory/ext_theory.h" #include "theory/output_channel.h" #include "theory/strings/infer_info.h" #include "theory/strings/sequences_stats.h" @@ -34,8 +35,6 @@ namespace CVC4 { namespace theory { namespace strings { -class TheoryStrings; - /** Inference Manager * * The purpose of this class is to process inference steps for strategies @@ -72,15 +71,22 @@ class InferenceManager typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap; public: - InferenceManager(TheoryStrings& p, - context::Context* c, + InferenceManager(context::Context* c, context::UserContext* u, SolverState& s, TermRegistry& tr, + ExtTheory& e, OutputChannel& out, SequencesStatistics& statistics); ~InferenceManager() {} + /** send assumption + * + * This is called when a fact is asserted to TheoryStrings. It adds lit + * to the equality engine maintained by this class immediately. + */ + void sendAssumption(TNode lit); + /** send internal inferences * * This is called when we have inferred exp => conc, where exp is a set @@ -175,6 +181,12 @@ class InferenceManager * decided with polarity pol. */ void sendPhaseRequirement(Node lit, bool pol); + /** + * Set that we are incomplete for the current set of assertions (in other + * words, we must answer "unknown" instead of "sat"); this calls the output + * channel's setIncomplete method. + */ + void setIncomplete(); //----------------------------constructing antecedants /** @@ -189,7 +201,7 @@ class InferenceManager * * This method asserts pending facts (d_pending) with explanations * (d_pendingExp) to the equality engine of the theory of strings via calls - * to assertPendingFact in the theory of strings. + * to assertPendingFact. * * It terminates early if a conflict is encountered, for instance, by * equality reasoning within the equality engine. @@ -239,12 +251,7 @@ class InferenceManager * the node corresponding to their conjunction. */ void explain(TNode literal, std::vector<TNode>& assumptions) const; - /** - * Set that we are incomplete for the current set of assertions (in other - * words, we must answer "unknown" instead of "sat"); this calls the output - * channel's setIncomplete method. - */ - void setIncomplete(); + // ------------------------------------------------- extended theory /** * Mark that terms a and b are congruent in the current context. * This makes a call to markCongruent in the extended theory object of @@ -252,8 +259,24 @@ class InferenceManager * theory. */ void markCongruent(Node a, Node b); + /** + * Mark that extended function is reduced. If contextDepend is true, + * then this mark is SAT-context dependent, otherwise it is user-context + * dependent (see ExtTheory::markReduced). + */ + void markReduced(Node n, bool contextDepend = true); + // ------------------------------------------------- end extended theory private: + /** assert pending fact + * + * This asserts atom with polarity to the equality engine of this class, + * where exp is the explanation of why (~) atom holds. + * + * This call may trigger further initialization steps involving the terms + * of atom, including calls to registerTerm. + */ + void assertPendingFact(Node atom, bool polarity, Node exp); /** * Indicates that ant => conc should be sent on the output channel of this * class. This will either trigger an immediate call to the conflict @@ -272,14 +295,13 @@ class InferenceManager * equality engine of this class. */ void sendInfer(Node eq_exp, Node eq, Inference infer); - - /** the parent theory of strings object */ - TheoryStrings& d_parent; /** Reference to the solver state of the theory of strings. */ SolverState& d_state; /** Reference to the term registry of theory of strings */ TermRegistry& d_termReg; - /** Reference to the output channel of the theory of strings. */ + /** the extended theory object for the theory of strings */ + ExtTheory& d_extt; + /** A reference to the output channel of the theory of strings. */ OutputChannel& d_out; /** Reference to the statistics for the theory of strings/sequences. */ SequencesStatistics& d_statistics; diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp index 540a10a9e..db7e2d836 100644 --- a/src/theory/strings/regexp_solver.cpp +++ b/src/theory/strings/regexp_solver.cpp @@ -20,7 +20,6 @@ #include "options/strings_options.h" #include "theory/ext_theory.h" -#include "theory/strings/theory_strings.h" #include "theory/strings/theory_strings_utils.h" #include "theory/theory_model.h" @@ -32,16 +31,16 @@ namespace CVC4 { namespace theory { namespace strings { -RegExpSolver::RegExpSolver(TheoryStrings& p, - SolverState& s, +RegExpSolver::RegExpSolver(SolverState& s, InferenceManager& im, + CoreSolver& cs, ExtfSolver& es, SequencesStatistics& stats, context::Context* c, context::UserContext* u) - : d_parent(p), - d_state(s), + : d_state(s), d_im(im), + d_csolver(cs), d_esolver(es), d_statistics(stats), d_regexp_ucached(u), @@ -194,7 +193,7 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems) Node nx = x; if (!x.isConst()) { - nx = d_parent.getNormalString(x, nfexp); + nx = d_csolver.getNormalString(x, nfexp); } // If r is not a constant regular expression, we update it based on // normal forms, which may concretize its variables. @@ -303,7 +302,7 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems) else { // otherwise we are incomplete - d_parent.getOutputChannel().setIncomplete(); + d_im.setIncomplete(); } } if (d_state.isInConflict()) @@ -367,14 +366,14 @@ bool RegExpSolver::checkEqcInclusion(std::vector<Node>& mems) { // ~str.in.re(x, R1) includes ~str.in.re(x, R2) ---> // mark ~str.in.re(x, R2) as reduced - d_parent.getExtTheory()->markReduced(m2Lit); + d_im.markReduced(m2Lit); remove.insert(m2); } else { // str.in.re(x, R1) includes str.in.re(x, R2) ---> // mark str.in.re(x, R1) as reduced - d_parent.getExtTheory()->markReduced(m1Lit); + d_im.markReduced(m1Lit); remove.insert(m1); // We don't need to process m1 anymore @@ -495,12 +494,12 @@ bool RegExpSolver::checkEqcIntersect(const std::vector<Node>& mems) { // if R1 = intersect( R1, R2 ), then x in R1 ^ x in R2 is equivalent // to x in R1, hence x in R2 can be marked redundant. - d_parent.getExtTheory()->markReduced(m); + d_im.markReduced(m); } else if (mres == m) { // same as above, opposite direction - d_parent.getExtTheory()->markReduced(mi); + d_im.markReduced(mi); } else { @@ -515,8 +514,8 @@ bool RegExpSolver::checkEqcIntersect(const std::vector<Node>& mems) } d_im.sendInference(vec_nodes, mres, Inference::RE_INTER_INFER, true); // both are reduced - d_parent.getExtTheory()->markReduced(m); - d_parent.getExtTheory()->markReduced(mi); + d_im.markReduced(m); + d_im.markReduced(mi); // do not send more than one lemma for this class return true; } @@ -660,7 +659,7 @@ Node RegExpSolver::getNormalSymRegExp(Node r, std::vector<Node>& nf_exp) { if (!r[0].isConst()) { - Node tmp = d_parent.getNormalString(r[0], nf_exp); + Node tmp = d_csolver.getNormalString(r[0], nf_exp); if (tmp != r[0]) { ret = NodeManager::currentNM()->mkNode(STRING_TO_REGEXP, tmp); diff --git a/src/theory/strings/regexp_solver.h b/src/theory/strings/regexp_solver.h index 1d065181b..b44c6c8d9 100644 --- a/src/theory/strings/regexp_solver.h +++ b/src/theory/strings/regexp_solver.h @@ -34,8 +34,6 @@ namespace CVC4 { namespace theory { namespace strings { -class TheoryStrings; - class RegExpSolver { typedef context::CDList<Node> NodeList; @@ -46,9 +44,9 @@ class RegExpSolver typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; public: - RegExpSolver(TheoryStrings& p, - SolverState& s, + RegExpSolver(SolverState& s, InferenceManager& im, + CoreSolver& cs, ExtfSolver& es, SequencesStatistics& stats, context::Context* c, @@ -113,12 +111,12 @@ class RegExpSolver Node d_emptyRegexp; Node d_true; 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; + /** reference to the core solver, used for certain queries */ + CoreSolver& d_csolver; /** reference to the extended function solver of the parent */ ExtfSolver& d_esolver; /** Reference to the statistics for the theory of strings/sequences. */ diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 3e490f285..9e14d6a3f 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -73,10 +73,10 @@ TheoryStrings::TheoryStrings(context::Context* c, d_equalityEngine(d_notify, c, "theory::strings::ee", true), d_state(c, d_equalityEngine, d_valuation), d_termReg(c, u, d_equalityEngine, out, d_statistics), - d_im(*this, c, u, d_state, d_termReg, out, d_statistics), + d_im(nullptr), d_rewriter(&d_statistics.d_rewrites), - d_bsolver(c, u, d_state, d_im), - d_csolver(c, u, d_state, d_im, d_termReg, d_bsolver), + d_bsolver(nullptr), + d_csolver(nullptr), d_esolver(nullptr), d_rsolver(nullptr), d_stringsFmf(c, u, valuation, d_termReg), @@ -84,18 +84,24 @@ TheoryStrings::TheoryStrings(context::Context* c, { setupExtTheory(); ExtTheory* extt = getExtTheory(); + // initialize the inference manager, which requires the extended theory + d_im.reset( + new InferenceManager(c, u, d_state, d_termReg, *extt, out, d_statistics)); + // initialize the solvers + d_bsolver.reset(new BaseSolver(c, u, d_state, *d_im)); + d_csolver.reset(new CoreSolver(c, u, d_state, *d_im, d_termReg, *d_bsolver)); d_esolver.reset(new ExtfSolver(c, u, d_state, - d_im, + *d_im, d_termReg, d_rewriter, - d_bsolver, - d_csolver, - extt, + *d_bsolver, + *d_csolver, + *extt, d_statistics)); - d_rsolver.reset( - new RegExpSolver(*this, d_state, d_im, *d_esolver, d_statistics, c, u)); + d_rsolver.reset(new RegExpSolver( + d_state, *d_im, *d_csolver, *d_esolver, d_statistics, c, u)); // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::STRING_LENGTH); @@ -143,11 +149,6 @@ bool TheoryStrings::areCareDisequal( TNode x, TNode y ) { return false; } -Node TheoryStrings::getNormalString(Node x, std::vector<Node>& nf_exp) -{ - return d_csolver.getNormalString(x, nf_exp); -} - void TheoryStrings::setMasterEqualityEngine(eq::EqualityEngine* eq) { d_equalityEngine.setMasterEqualityEngine(eq); } @@ -201,7 +202,7 @@ bool TheoryStrings::propagate(TNode literal) { Node TheoryStrings::explain( TNode literal ){ Debug("strings-explain") << "explain called on " << literal << std::endl; std::vector< TNode > assumptions; - d_im.explain(literal, assumptions); + d_im->explain(literal, assumptions); if( assumptions.empty() ){ return d_true; }else if( assumptions.size()==1 ){ @@ -365,7 +366,7 @@ bool TheoryStrings::collectModelInfoType( //check if col[i][j] has only variables if (!eqc.isConst()) { - NormalForm& nfe = d_csolver.getNormalForm(eqc); + NormalForm& nfe = d_csolver->getNormalForm(eqc); if (nfe.d_nf.size() == 1) { // does it have a code and the length of these equivalence classes are @@ -499,7 +500,7 @@ bool TheoryStrings::collectModelInfoType( //step 4 : assign constants to all other equivalence classes for( unsigned i=0; i<nodes.size(); i++ ){ if( processed.find( nodes[i] )==processed.end() ){ - NormalForm& nf = d_csolver.getNormalForm(nodes[i]); + NormalForm& nf = d_csolver->getNormalForm(nodes[i]); if (Trace.isOn("strings-model")) { Trace("strings-model") @@ -586,8 +587,6 @@ void TheoryStrings::check(Effort e) { TimerStat::CodeTimer checkTimer(d_checkTime); - bool polarity; - TNode atom; // Trace("strings-process") << "Theory of strings, check : " << e << std::endl; Trace("strings-check-debug") << "Theory of strings, check : " << e << std::endl; @@ -598,13 +597,9 @@ void TheoryStrings::check(Effort e) { TNode fact = assertion.d_assertion; Trace("strings-assertion") << "get assertion: " << fact << endl; - polarity = fact.getKind() != kind::NOT; - atom = polarity ? fact : fact[0]; - - //assert pending fact - assertPendingFact( atom, polarity, fact ); + d_im->sendAssumption(fact); } - d_im.doPendingFacts(); + d_im->doPendingFacts(); Assert(d_strategy_init); std::map<Effort, std::pair<unsigned, unsigned> >::iterator itsr = @@ -661,10 +656,10 @@ void TheoryStrings::check(Effort e) { Trace("strings-check") << " * Run strategy..." << std::endl; runStrategy(sbegin, send); // flush the facts - addedFact = d_im.hasPendingFact(); - addedLemma = d_im.hasPendingLemma(); - d_im.doPendingFacts(); - d_im.doPendingLemmas(); + addedFact = d_im->hasPendingFact(); + addedLemma = d_im->hasPendingLemma(); + d_im->doPendingFacts(); + d_im->doPendingLemmas(); if (Trace.isOn("strings-check")) { Trace("strings-check") << " ...finish run strategy: "; @@ -681,8 +676,8 @@ void TheoryStrings::check(Effort e) { } while (!d_state.isInConflict() && !addedLemma && addedFact); } Trace("strings-check") << "Theory of strings, done check : " << e << std::endl; - Assert(!d_im.hasPendingFact()); - Assert(!d_im.hasPendingLemma()); + Assert(!d_im->hasPendingFact()); + Assert(!d_im->hasPendingLemma()); } bool TheoryStrings::needsCheckLastEffort() { @@ -831,68 +826,16 @@ void TheoryStrings::computeCareGraph(){ } } -void TheoryStrings::assertPendingFact(Node atom, bool polarity, Node exp) { - Trace("strings-pending") << "Assert pending fact : " << atom << " " << polarity << " from " << exp << std::endl; - Assert(atom.getKind() != kind::OR) << "Infer error: a split."; - if( atom.getKind()==kind::EQUAL ){ - Trace("strings-pending-debug") << " Register term" << std::endl; - for( unsigned j=0; j<2; j++ ) { - if (!d_equalityEngine.hasTerm(atom[j]) - && atom[j].getType().isStringLike()) - { - d_termReg.registerTerm(atom[j], 0); - } - } - Trace("strings-pending-debug") << " Now assert equality" << std::endl; - d_equalityEngine.assertEquality( atom, polarity, exp ); - Trace("strings-pending-debug") << " Finished assert equality" << std::endl; - } else { - d_equalityEngine.assertPredicate( atom, polarity, exp ); - if (atom.getKind() == STRING_IN_REGEXP) - { - if (polarity && atom[1].getKind() == REGEXP_CONCAT) - { - Node eqc = d_equalityEngine.getRepresentative(atom[0]); - d_state.addEndpointsToEqcInfo(atom, atom[1], eqc); - } - } - } - // process the conflict - if (!d_state.isInConflict()) - { - Node pc = d_state.getPendingConflict(); - if (!pc.isNull()) - { - std::vector<Node> a; - a.push_back(pc); - Trace("strings-pending") - << "Process pending conflict " << pc << std::endl; - Node conflictNode = d_im.mkExplain(a); - d_state.setConflict(); - Trace("strings-conflict") - << "CONFLICT: Eager prefix : " << conflictNode << std::endl; - ++(d_statistics.d_conflictsEagerPrefix); - d_out->conflict(conflictNode); - } - } - Trace("strings-pending-debug") << " Now collect terms" << std::endl; - // Collect extended function terms in the atom. Notice that we must register - // all extended functions occurring in assertions and shared terms. We - // make a similar call to registerTermRec in addSharedTerm. - getExtTheory()->registerTermRec( atom ); - Trace("strings-pending-debug") << " Finished collect terms" << std::endl; -} - void TheoryStrings::checkRegisterTermsPreNormalForm() { - const std::vector<Node>& seqc = d_bsolver.getStringEqc(); + const std::vector<Node>& seqc = d_bsolver->getStringEqc(); for (const Node& eqc : seqc) { eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, &d_equalityEngine); while (!eqc_i.isFinished()) { Node n = (*eqc_i); - if (!d_bsolver.isCongruent(n)) + if (!d_bsolver->isCongruent(n)) { d_termReg.registerTerm(n, 2); } @@ -914,10 +857,10 @@ void TheoryStrings::checkCodes() // str.code applied to the proxy variables for each equivalence classes that // are constants of size one std::vector<Node> const_codes; - const std::vector<Node>& seqc = d_bsolver.getStringEqc(); + const std::vector<Node>& seqc = d_bsolver->getStringEqc(); for (const Node& eqc : seqc) { - NormalForm& nfe = d_csolver.getNormalForm(eqc); + NormalForm& nfe = d_csolver->getNormalForm(eqc); if (nfe.d_nf.size() == 1 && nfe.d_nf[0].isConst()) { Node c = nfe.d_nf[0]; @@ -931,7 +874,8 @@ void TheoryStrings::checkCodes() Node vc = nm->mkNode(STRING_TO_CODE, cp); if (!d_state.areEqual(cc, vc)) { - d_im.sendInference(d_empty_vec, cc.eqNode(vc), Inference::CODE_PROXY); + std::vector<Node> emptyVec; + d_im->sendInference(emptyVec, cc.eqNode(vc), Inference::CODE_PROXY); } const_codes.push_back(vc); } @@ -945,7 +889,7 @@ void TheoryStrings::checkCodes() } } } - if (d_im.hasProcessed()) + if (d_im->hasProcessed()) { return; } @@ -968,8 +912,9 @@ void TheoryStrings::checkCodes() Node eqn = c1[0].eqNode(c2[0]); // str.code(x)==-1 V str.code(x)!=str.code(y) V x==y Node inj_lem = nm->mkNode(kind::OR, eq_no, deq, eqn); - d_im.sendPhaseRequirement(deq, false); - d_im.sendInference(d_empty_vec, inj_lem, Inference::CODE_INJ); + d_im->sendPhaseRequirement(deq, false); + std::vector<Node> emptyVec; + d_im->sendInference(emptyVec, inj_lem, Inference::CODE_INJ); } } } @@ -978,10 +923,10 @@ void TheoryStrings::checkCodes() void TheoryStrings::checkRegisterTermsNormalForms() { - const std::vector<Node>& seqc = d_bsolver.getStringEqc(); + const std::vector<Node>& seqc = d_bsolver->getStringEqc(); for (const Node& eqc : seqc) { - NormalForm& nfi = d_csolver.getNormalForm(eqc); + NormalForm& nfi = d_csolver->getNormalForm(eqc); // check if there is a length term for this equivalence class EqcInfo* ei = d_state.getOrMakeEqcInfo(eqc, false); Node lt = ei ? ei->d_lengthTerm : Node::null(); @@ -1039,25 +984,25 @@ void TheoryStrings::runInferStep(InferStep s, int effort) Trace("strings-process") << "..." << std::endl; switch (s) { - case CHECK_INIT: d_bsolver.checkInit(); break; - case CHECK_CONST_EQC: d_bsolver.checkConstantEquivalenceClasses(); break; + case CHECK_INIT: d_bsolver->checkInit(); break; + case CHECK_CONST_EQC: d_bsolver->checkConstantEquivalenceClasses(); break; case CHECK_EXTF_EVAL: d_esolver->checkExtfEval(effort); break; - case CHECK_CYCLES: d_csolver.checkCycles(); break; - case CHECK_FLAT_FORMS: d_csolver.checkFlatForms(); break; + case CHECK_CYCLES: d_csolver->checkCycles(); break; + case CHECK_FLAT_FORMS: d_csolver->checkFlatForms(); break; case CHECK_REGISTER_TERMS_PRE_NF: checkRegisterTermsPreNormalForm(); break; - case CHECK_NORMAL_FORMS_EQ: d_csolver.checkNormalFormsEq(); break; - case CHECK_NORMAL_FORMS_DEQ: d_csolver.checkNormalFormsDeq(); break; + case CHECK_NORMAL_FORMS_EQ: d_csolver->checkNormalFormsEq(); break; + case CHECK_NORMAL_FORMS_DEQ: d_csolver->checkNormalFormsDeq(); break; case CHECK_CODES: checkCodes(); break; - case CHECK_LENGTH_EQC: d_csolver.checkLengthsEqc(); break; + case CHECK_LENGTH_EQC: d_csolver->checkLengthsEqc(); break; case CHECK_REGISTER_TERMS_NF: checkRegisterTermsNormalForms(); break; case CHECK_EXTF_REDUCTION: d_esolver->checkExtfReductions(effort); break; case CHECK_MEMBERSHIP: d_rsolver->checkMemberships(); break; - case CHECK_CARDINALITY: d_bsolver.checkCardinality(); break; + case CHECK_CARDINALITY: d_bsolver->checkCardinality(); break; default: Unreachable(); break; } Trace("strings-process") << "Done " << s - << ", addedFact = " << d_im.hasPendingFact() - << ", addedLemma = " << d_im.hasPendingLemma() + << ", addedFact = " << d_im->hasPendingFact() + << ", addedLemma = " << d_im->hasPendingLemma() << ", conflict = " << d_state.isInConflict() << std::endl; } @@ -1165,7 +1110,7 @@ void TheoryStrings::runStrategy(unsigned sbegin, unsigned send) InferStep curr = d_infer_steps[i]; if (curr == BREAK) { - if (d_im.hasProcessed()) + if (d_im->hasProcessed()) { break; } diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 4a61730f4..2e78198e3 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -200,18 +200,6 @@ class TheoryStrings : public Theory { SolverState& d_state; };/* class TheoryStrings::NotifyClass */ - //--------------------------- helper functions - /** get normal string - * - * This method returns the node that is equivalent to the normal form of x, - * and adds the corresponding explanation to nf_exp. - * - * For example, if x = y ++ z is an assertion in the current context, then - * this method returns the term y ++ z and adds x = y ++ z to nf_exp. - */ - Node getNormalString(Node x, std::vector<Node>& nf_exp); - //-------------------------- end helper functions - private: // Constants Node d_emptyString; @@ -238,10 +226,9 @@ class TheoryStrings : public Theory { /** The term registry for this theory */ TermRegistry d_termReg; /** The (custom) output channel of the theory of strings */ - InferenceManager d_im; - std::vector< Node > d_empty_vec; -private: + std::unique_ptr<InferenceManager> d_im; + private: std::map< Node, Node > d_eqc_to_len_term; @@ -318,12 +305,12 @@ private: * The base solver, responsible for reasoning about congruent terms and * inferring constants for equivalence classes. */ - BaseSolver d_bsolver; + std::unique_ptr<BaseSolver> d_bsolver; /** * The core solver, responsible for reasoning about string concatenation * with length constraints. */ - CoreSolver d_csolver; + std::unique_ptr<CoreSolver> d_csolver; /** * Extended function solver, responsible for reductions and simplifications * involving extended string functions. |