diff options
| -rw-r--r-- | src/theory/strings/core_solver.cpp | 8 | ||||
| -rw-r--r-- | src/theory/strings/extf_solver.cpp | 5 | ||||
| -rw-r--r-- | src/theory/strings/extf_solver.h | 4 | ||||
| -rw-r--r-- | src/theory/strings/inference_manager.cpp | 62 | ||||
| -rw-r--r-- | src/theory/strings/inference_manager.h | 34 | ||||
| -rw-r--r-- | src/theory/strings/sequences_stats.cpp | 30 | ||||
| -rw-r--r-- | src/theory/strings/sequences_stats.h | 26 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 40 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings_preprocess.cpp | 7 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings_preprocess.h | 87 |
10 files changed, 206 insertions, 97 deletions
diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp index ab3270016..3384499a2 100644 --- a/src/theory/strings/core_solver.cpp +++ b/src/theory/strings/core_solver.cpp @@ -1692,7 +1692,7 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi, // right Node sk_w = d_skCache.mkSkolem("w_loop"); Node sk_y = d_skCache.mkSkolem("y_loop"); - d_im.registerLength(sk_y, LENGTH_GEQ_ONE); + d_im.registerTermAtomic(sk_y, LENGTH_GEQ_ONE); Node sk_z = d_skCache.mkSkolem("z_loop"); // t1 * ... * tn = y * z Node conc1 = t_yz.eqNode(utils::mkNConcat(sk_y, sk_z)); @@ -1803,7 +1803,7 @@ void CoreSolver::processDeq( Node ni, Node nj ) { { Node sk = d_skCache.mkSkolemCached( nconst_k, SkolemCache::SK_ID_DC_SPT, "dc_spt"); - d_im.registerLength(sk, LENGTH_ONE); + d_im.registerTermAtomic(sk, LENGTH_ONE); Node skr = d_skCache.mkSkolemCached(nconst_k, SkolemCache::SK_ID_DC_SPT_REM, @@ -1852,7 +1852,7 @@ void CoreSolver::processDeq( Node ni, Node nj ) { i, j, SkolemCache::SK_ID_DEQ_Y, "y_dsplit"); Node sk3 = d_skCache.mkSkolemCached( i, j, SkolemCache::SK_ID_DEQ_Z, "z_dsplit"); - d_im.registerLength(sk3, LENGTH_GEQ_ONE); + d_im.registerTermAtomic(sk3, LENGTH_GEQ_ONE); Node lsk1 = utils::mkNLength(sk1); conc.push_back( lsk1.eqNode( li ) ); Node lsk2 = utils::mkNLength(sk2); @@ -2209,7 +2209,7 @@ void CoreSolver::doInferInfo(const InferInfo& ii) { for (const Node& n : sks.second) { - d_im.registerLength(n, sks.first); + d_im.registerTermAtomic(n, sks.first); } } } diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp index 6a3209344..47f36af4c 100644 --- a/src/theory/strings/extf_solver.cpp +++ b/src/theory/strings/extf_solver.cpp @@ -34,14 +34,15 @@ ExtfSolver::ExtfSolver(context::Context* c, SkolemCache& skc, BaseSolver& bs, CoreSolver& cs, - ExtTheory* et) + ExtTheory* et, + SequencesStatistics& stats) : d_state(s), d_im(im), d_skCache(skc), d_bsolver(bs), d_csolver(cs), d_extt(et), - d_preproc(&skc, u), + d_preproc(&skc, u, stats), d_hasExtf(c, false), d_extfInferCache(c) { diff --git a/src/theory/strings/extf_solver.h b/src/theory/strings/extf_solver.h index 4c848f430..040871ffa 100644 --- a/src/theory/strings/extf_solver.h +++ b/src/theory/strings/extf_solver.h @@ -26,6 +26,7 @@ #include "theory/strings/base_solver.h" #include "theory/strings/core_solver.h" #include "theory/strings/inference_manager.h" +#include "theory/strings/sequences_stats.h" #include "theory/strings/skolem_cache.h" #include "theory/strings/solver_state.h" #include "theory/strings/theory_strings_preprocess.h" @@ -88,7 +89,8 @@ class ExtfSolver SkolemCache& skc, BaseSolver& bs, CoreSolver& cs, - ExtTheory* et); + ExtTheory* et, + SequencesStatistics& stats); ~ExtfSolver(); /** check extended functions evaluation diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp index e931c5c1a..cb0c807cc 100644 --- a/src/theory/strings/inference_manager.cpp +++ b/src/theory/strings/inference_manager.cpp @@ -226,6 +226,7 @@ void InferenceManager::sendLemma(Node ant, Node conc, const char* c) << std::endl; Trace("strings-assert") << "(assert (not " << ant << ")) ; conflict " << c << std::endl; + ++(d_statistics.d_conflictsInfer); d_out.conflict(ant); d_state.setConflict(); return; @@ -369,7 +370,7 @@ Node InferenceManager::getSymbolicDefinition(Node n, return NodeManager::currentNM()->mkNode(n.getKind(), children); } -void InferenceManager::registerLength(Node n) +Node InferenceManager::registerTerm(Node n) { Assert(n.getType().isStringLike()); NodeManager* nm = NodeManager::currentNM(); @@ -384,15 +385,14 @@ void InferenceManager::registerLength(Node n) // can register length term if it does not rewrite if (lsum == lsumb) { - registerLength(n, LENGTH_SPLIT); - return; + registerTermAtomic(n, LENGTH_SPLIT); + return Node::null(); } } Node sk = d_skCache.mkSkolemCached(n, SkolemCache::SK_PURIFY, "lsym"); StringsProxyVarAttribute spva; sk.setAttribute(spva, true); Node eq = Rewriter::rewrite(sk.eqNode(n)); - Trace("strings-lemma") << "Strings::Lemma LENGTH Term : " << eq << std::endl; d_proxyVar[n] = sk; // If we are introducing a proxy for a constant or concat term, we do not // need to send lemmas about its length, since its length is already @@ -400,10 +400,8 @@ void InferenceManager::registerLength(Node n) if (n.isConst() || n.getKind() == STRING_CONCAT) { // do not send length lemma for sk. - registerLength(sk, LENGTH_IGNORE); + registerTermAtomic(sk, LENGTH_IGNORE); } - Trace("strings-assert") << "(assert " << eq << ")" << std::endl; - d_out.lemma(eq); Node skl = nm->mkNode(STRING_LENGTH, sk); if (n.getKind() == STRING_CONCAT) { @@ -431,14 +429,11 @@ void InferenceManager::registerLength(Node n) Assert(!lsum.isNull()); d_proxyVarToLength[sk] = lsum; Node ceq = Rewriter::rewrite(skl.eqNode(lsum)); - Trace("strings-lemma") << "Strings::Lemma LENGTH : " << ceq << std::endl; - Trace("strings-lemma-debug") - << " prerewrite : " << skl.eqNode(lsum) << std::endl; - Trace("strings-assert") << "(assert " << ceq << ")" << std::endl; - d_out.lemma(ceq); + + return nm->mkNode(AND, eq, ceq); } -void InferenceManager::registerLength(Node n, LengthStatus s) +void InferenceManager::registerTermAtomic(Node n, LengthStatus s) { if (d_lengthLemmaTermsCache.find(n) != d_lengthLemmaTermsCache.end()) { @@ -451,7 +446,25 @@ void InferenceManager::registerLength(Node n, LengthStatus s) // ignore it return; } + std::map<Node, bool> reqPhase; + Node lenLem = getRegisterTermAtomicLemma(n, s, reqPhase); + if (!lenLem.isNull()) + { + Trace("strings-lemma") << "Strings::Lemma REGISTER-TERM-ATOMIC : " << lenLem + << std::endl; + Trace("strings-assert") << "(assert " << lenLem << ")" << std::endl; + ++(d_statistics.d_lemmasRegisterTermAtomic); + d_out.lemma(lenLem); + } + for (const std::pair<const Node, bool>& rp : reqPhase) + { + d_out.requirePhase(rp.first, rp.second); + } +} +Node InferenceManager::getRegisterTermAtomicLemma( + Node n, LengthStatus s, std::map<Node, bool>& reqPhase) +{ NodeManager* nm = NodeManager::currentNM(); Node n_len = nm->mkNode(kind::STRING_LENGTH, n); @@ -463,8 +476,7 @@ void InferenceManager::registerLength(Node n, LengthStatus s) Trace("strings-lemma") << "Strings::Lemma SK-GEQ-ONE : " << len_geq_one << std::endl; Trace("strings-assert") << "(assert " << len_geq_one << ")" << std::endl; - d_out.lemma(len_geq_one); - return; + return len_geq_one; } if (s == LENGTH_ONE) @@ -473,11 +485,11 @@ void InferenceManager::registerLength(Node n, LengthStatus s) Trace("strings-lemma") << "Strings::Lemma SK-ONE : " << len_one << std::endl; Trace("strings-assert") << "(assert " << len_one << ")" << std::endl; - d_out.lemma(len_one); - return; + return len_one; } Assert(s == LENGTH_SPLIT); + std::vector<Node> lems; if (options::stringSplitEmp() || !options::stringLenGeqZ()) { Node n_len_eq_z = n_len.eqNode(d_zero); @@ -488,7 +500,7 @@ void InferenceManager::registerLength(Node n, LengthStatus s) if (!case_empty.isConst()) { Node lem = nm->mkNode(OR, case_empty, case_nempty); - d_out.lemma(lem); + lems.push_back(lem); Trace("strings-lemma") << "Strings::Lemma LENGTH >= 0 : " << lem << std::endl; // prefer trying the empty case first @@ -496,10 +508,10 @@ void InferenceManager::registerLength(Node n, LengthStatus s) // occur in the CNF stream. n_len_eq_z = Rewriter::rewrite(n_len_eq_z); Assert(!n_len_eq_z.isConst()); - d_out.requirePhase(n_len_eq_z, true); + reqPhase[n_len_eq_z] = true; n_len_eq_z_2 = Rewriter::rewrite(n_len_eq_z_2); Assert(!n_len_eq_z_2.isConst()); - d_out.requirePhase(n_len_eq_z_2, true); + reqPhase[n_len_eq_z_2] = true; } else if (!case_empty.getConst<bool>()) { @@ -507,7 +519,7 @@ void InferenceManager::registerLength(Node n, LengthStatus s) Trace("strings-lemma") << "Strings::Lemma LENGTH > 0 (non-empty): " << case_nempty << std::endl; - d_out.lemma(case_nempty); + lems.push_back(case_nempty); } else { @@ -523,8 +535,14 @@ void InferenceManager::registerLength(Node n, LengthStatus s) { Node n_len_geq = nm->mkNode(kind::GEQ, n_len, d_zero); n_len_geq = Rewriter::rewrite(n_len_geq); - d_out.lemma(n_len_geq); + lems.push_back(n_len_geq); + } + + if (lems.empty()) + { + return Node::null(); } + return lems.size() == 1 ? lems[0] : nm->mkNode(AND, lems); } void InferenceManager::addToExplanation(Node a, diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h index c9d483c73..bd2f85d29 100644 --- a/src/theory/strings/inference_manager.h +++ b/src/theory/strings/inference_manager.h @@ -210,18 +210,23 @@ class InferenceManager * exists, otherwise it returns null. */ Node getProxyVariableFor(Node n) const; - /** register length + /** register term + * + * This method is called on non-constant string terms n. It returns a lemma + * that should be sent on the output channel of theory of strings upon + * registration of this term, or null if no lemma is necessary. * - * This method is called on non-constant string terms n. It sends a lemma - * on the output channel that ensures that the length n satisfies its assigned - * status (given by argument s). + * If n is an atomic term, the method registerTermAtomic is called for n + * and s = LENGTH_SPLIT and no lemma is returned. */ - void registerLength(Node n); + Node registerTerm(Node n); /** register length * - * This method is called on non-constant string terms n. It sends a lemma - * on the output channel that ensures that the length n satisfies its assigned - * status (given by argument s). + * This method is called on non-constant string terms n that are "atomic" + * with respect to length. That is, the rewritten form of len(n) is itself. + * + * It sends a lemma on the output channel that ensures that the length n + * satisfies its assigned status (given by argument s). * * If the status is LENGTH_ONE, we send the lemma len( n ) = 1. * @@ -238,7 +243,7 @@ class InferenceManager * In contrast to the above functions, it makes immediate calls to the output * channel instead of adding them to pending lists. */ - void registerLength(Node n, LengthStatus s); + void registerTermAtomic(Node n, LengthStatus s); //---------------------------- end proxy variables and length elaboration //----------------------------constructing antecedants @@ -337,6 +342,17 @@ class InferenceManager * equality engine of this class. */ void sendInfer(Node eq_exp, Node eq, const char* c); + /** + * Get the lemma required for registering the length information for + * atomic term n given length status s. For details, see registerTermAtomic. + * + * Additionally, this method may map literals to a required polarity in the + * argument reqPhase, which should be processed by a call to requiredPhase by + * the caller of this method. + */ + Node getRegisterTermAtomicLemma(Node n, + LengthStatus s, + std::map<Node, bool>& reqPhase); /** the parent theory of strings object */ TheoryStrings& d_parent; diff --git a/src/theory/strings/sequences_stats.cpp b/src/theory/strings/sequences_stats.cpp index 0f1e93599..fb13cdab2 100644 --- a/src/theory/strings/sequences_stats.cpp +++ b/src/theory/strings/sequences_stats.cpp @@ -22,14 +22,42 @@ namespace theory { namespace strings { SequencesStatistics::SequencesStatistics() - : d_inferences("theory::strings::inferences") + : d_inferences("theory::strings::inferences"), + d_reductions("theory::strings::reductions"), + d_conflictsEqEngine("theory::strings::conflictsEqEngine", 0), + d_conflictsEagerPrefix("theory::strings::conflictsEagerPrefix", 0), + d_conflictsInfer("theory::strings::conflictsInfer", 0), + d_lemmasEagerPreproc("theory::strings::lemmasEagerPreproc", 0), + d_lemmasCmiSplit("theory::strings::lemmasCmiSplit", 0), + d_lemmasRegisterTerm("theory::strings::lemmasRegisterTerm", 0), + d_lemmasRegisterTermAtomic("theory::strings::lemmasRegisterTermAtomic", + 0), + d_lemmasInfer("theory::strings::lemmasInfer", 0) { smtStatisticsRegistry()->registerStat(&d_inferences); + smtStatisticsRegistry()->registerStat(&d_reductions); + smtStatisticsRegistry()->registerStat(&d_conflictsEqEngine); + smtStatisticsRegistry()->registerStat(&d_conflictsEagerPrefix); + smtStatisticsRegistry()->registerStat(&d_conflictsInfer); + smtStatisticsRegistry()->registerStat(&d_lemmasEagerPreproc); + smtStatisticsRegistry()->registerStat(&d_lemmasCmiSplit); + smtStatisticsRegistry()->registerStat(&d_lemmasRegisterTerm); + smtStatisticsRegistry()->registerStat(&d_lemmasRegisterTermAtomic); + smtStatisticsRegistry()->registerStat(&d_lemmasInfer); } SequencesStatistics::~SequencesStatistics() { smtStatisticsRegistry()->unregisterStat(&d_inferences); + smtStatisticsRegistry()->unregisterStat(&d_reductions); + smtStatisticsRegistry()->unregisterStat(&d_conflictsEqEngine); + smtStatisticsRegistry()->unregisterStat(&d_conflictsEagerPrefix); + smtStatisticsRegistry()->unregisterStat(&d_conflictsInfer); + smtStatisticsRegistry()->unregisterStat(&d_lemmasEagerPreproc); + smtStatisticsRegistry()->unregisterStat(&d_lemmasCmiSplit); + smtStatisticsRegistry()->unregisterStat(&d_lemmasRegisterTerm); + smtStatisticsRegistry()->unregisterStat(&d_lemmasRegisterTermAtomic); + smtStatisticsRegistry()->unregisterStat(&d_lemmasInfer); } } diff --git a/src/theory/strings/sequences_stats.h b/src/theory/strings/sequences_stats.h index b55178f4c..83a16cb23 100644 --- a/src/theory/strings/sequences_stats.h +++ b/src/theory/strings/sequences_stats.h @@ -17,6 +17,7 @@ #ifndef CVC4__THEORY__STRINGS__SEQUENCES_STATS_H #define CVC4__THEORY__STRINGS__SEQUENCES_STATS_H +#include "expr/kind.h" #include "theory/strings/infer_info.h" #include "util/statistics_registry.h" @@ -30,11 +31,32 @@ class SequencesStatistics SequencesStatistics(); ~SequencesStatistics(); - /** Counts the number of inferences made of each type of inference */ + /** Counts the number of applications of each type of inference */ HistogramStat<Inference> d_inferences; + /** Counts the number of applications of each type of reduction */ + HistogramStat<Kind> d_reductions; + //--------------- conflicts, partition of calls to OutputChannel::conflict + /** Number of equality engine conflicts */ + IntStat d_conflictsEqEngine; + /** Number of eager prefix conflicts */ + IntStat d_conflictsEagerPrefix; + /** Number of inference conflicts */ + IntStat d_conflictsInfer; + //--------------- end of conflicts + //--------------- lemmas, partition of calls to OutputChannel::lemma + /** Number of lemmas added due to eager preprocessing */ + IntStat d_lemmasEagerPreproc; + /** Number of collect model info splits */ + IntStat d_lemmasCmiSplit; + /** Number of lemmas added due to registering terms */ + IntStat d_lemmasRegisterTerm; + /** Number of lemmas added due to registering atomic terms */ + IntStat d_lemmasRegisterTermAtomic; + /** Number of lemmas added due to inferences */ + IntStat d_lemmasInfer; + //--------------- end of lemmas }; - } } } diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 789099ee4..16183abdd 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -69,7 +69,7 @@ TheoryStrings::TheoryStrings(context::Context* c, const LogicInfo& logicInfo) : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo), d_notify(*this), - d_equalityEngine(d_notify, c, "theory::strings", true), + d_equalityEngine(d_notify, c, "theory::strings::ee", true), d_state(c, d_equalityEngine, d_valuation), d_im(*this, c, u, d_state, d_sk_cache, out, d_statistics), d_pregistered_terms_cache(u), @@ -85,8 +85,15 @@ TheoryStrings::TheoryStrings(context::Context* c, { setupExtTheory(); ExtTheory* extt = getExtTheory(); - d_esolver.reset(new ExtfSolver( - c, u, d_state, d_im, d_sk_cache, d_bsolver, d_csolver, extt)); + d_esolver.reset(new ExtfSolver(c, + u, + d_state, + d_im, + d_sk_cache, + d_bsolver, + d_csolver, + extt, + d_statistics)); d_rsolver.reset(new RegExpSolver(*this, d_state, d_im, *d_esolver, c, u)); // The kinds we are treating as function application in congruence @@ -464,6 +471,7 @@ bool TheoryStrings::collectModelInfoType( for (const Node& sl : len_splits) { Node spl = nm->mkNode(OR, sl, sl.negate()); + ++(d_statistics.d_lemmasCmiSplit); d_out->lemma(spl); } return false; @@ -779,6 +787,7 @@ void TheoryStrings::conflict(TNode a, TNode b){ Node conflictNode; conflictNode = explain( a.eqNode(b) ); Trace("strings-conflict") << "CONFLICT: Eq engine conflict : " << conflictNode << std::endl; + ++(d_statistics.d_conflictsEqEngine); d_out->conflict( conflictNode ); } } @@ -947,6 +956,7 @@ void TheoryStrings::assertPendingFact(Node atom, bool polarity, Node exp) { d_state.setConflict(); Trace("strings-conflict") << "CONFLICT: Eager prefix : " << conflictNode << std::endl; + ++(d_statistics.d_conflictsEagerPrefix); d_out->conflict(conflictNode); } } @@ -1078,12 +1088,13 @@ void TheoryStrings::registerTerm(Node n, int effort) NodeManager* nm = NodeManager::currentNM(); Debug("strings-register") << "TheoryStrings::registerTerm() " << n << ", effort = " << effort << std::endl; + Node regTermLem; if (tn.isStringLike()) { // register length information: // for variables, split on empty vs positive length // for concat/const/replace, introduce proxy var and state length relation - d_im.registerLength(n); + regTermLem = d_im.registerTerm(n); } else if (n.getKind() == STRING_TO_CODE) { @@ -1095,20 +1106,22 @@ void TheoryStrings::registerTerm(Node n, int effort) AND, nm->mkNode(GEQ, n, d_zero), nm->mkNode(LT, n, nm->mkConst(Rational(CVC4::String::num_codes())))); - Node lem = nm->mkNode(ITE, code_len, code_range, code_eq_neg1); - Trace("strings-lemma") << "Strings::Lemma CODE : " << lem << std::endl; - Trace("strings-assert") << "(assert " << lem << ")" << std::endl; - d_out->lemma(lem); + regTermLem = nm->mkNode(ITE, code_len, code_range, code_eq_neg1); } else if (n.getKind() == STRING_STRIDOF) { Node len = utils::mkNLength(n[0]); - Node lem = nm->mkNode(AND, - nm->mkNode(GEQ, n, nm->mkConst(Rational(-1))), - nm->mkNode(LEQ, n, len)); - Trace("strings-lemma") << "Strings::Lemma IDOF range : " << lem + regTermLem = nm->mkNode(AND, + nm->mkNode(GEQ, n, nm->mkConst(Rational(-1))), + nm->mkNode(LEQ, n, len)); + } + if (!regTermLem.isNull()) + { + Trace("strings-lemma") << "Strings::Lemma REG-TERM : " << regTermLem << std::endl; - d_out->lemma(lem); + Trace("strings-assert") << "(assert " << regTermLem << ")" << std::endl; + ++(d_statistics.d_lemmasRegisterTerm); + d_out->lemma(regTermLem); } } @@ -1153,6 +1166,7 @@ Node TheoryStrings::ppRewrite(TNode atom) { Trace("strings-ppr") << " rewrote " << atom << " -> " << ret << ", with " << new_nodes.size() << " lemmas." << std::endl; for( unsigned i=0; i<new_nodes.size(); i++ ){ Trace("strings-ppr") << " lemma : " << new_nodes[i] << std::endl; + ++(d_statistics.d_lemmasEagerPreproc); d_out->lemma( new_nodes[i] ); } return ret; diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index d4183700d..b35c4a921 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -31,8 +31,10 @@ namespace CVC4 { namespace theory { namespace strings { -StringsPreprocess::StringsPreprocess(SkolemCache *sc, context::UserContext *u) - : d_sc(sc) +StringsPreprocess::StringsPreprocess(SkolemCache* sc, + context::UserContext* u, + SequencesStatistics& stats) + : d_sc(sc), d_statistics(stats) { //Constants d_zero = NodeManager::currentNM()->mkConst(Rational(0)); @@ -637,6 +639,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Trace("strings-preprocess") << " " << new_nodes[i] << std::endl; } } + d_statistics.d_reductions << t.getKind(); } else { diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h index b96d619ef..155b9014c 100644 --- a/src/theory/strings/theory_strings_preprocess.h +++ b/src/theory/strings/theory_strings_preprocess.h @@ -22,6 +22,7 @@ #include <vector> #include "context/cdhashmap.h" #include "theory/rewriter.h" +#include "theory/strings/sequences_stats.h" #include "theory/strings/skolem_cache.h" #include "theory/theory.h" #include "util/hash.h" @@ -38,48 +39,52 @@ namespace strings { * reductions" inference schema of TheoryStrings. */ class StringsPreprocess { -public: - StringsPreprocess(SkolemCache *sc, context::UserContext *u); - ~StringsPreprocess(); - /** - * Returns a node t' such that - * (exists k) new_nodes => t = t' - * is valid, where k are the free skolems introduced when constructing - * new_nodes. - */ - Node simplify(Node t, std::vector<Node> &new_nodes); - /** - * Applies simplifyRec on t until a fixed point is reached, and returns - * the resulting term t', which is such that - * (exists k) new_nodes => t = t' - * is valid, where k are the free skolems introduced when constructing - * new_nodes. - */ - Node processAssertion(Node t, std::vector<Node> &new_nodes); - /** - * Replaces all formulas t in vec_node with an equivalent formula t' that - * contains no free instances of extended functions (that is, extended - * functions may only appear beneath quantifiers). This applies simplifyRec - * on each assertion in vec_node until a fixed point is reached. - */ - void processAssertions(std::vector<Node> &vec_node); + public: + StringsPreprocess(SkolemCache* sc, + context::UserContext* u, + SequencesStatistics& stats); + ~StringsPreprocess(); + /** + * Returns a node t' such that + * (exists k) new_nodes => t = t' + * is valid, where k are the free skolems introduced when constructing + * new_nodes. + */ + Node simplify(Node t, std::vector<Node>& new_nodes); + /** + * Applies simplifyRec on t until a fixed point is reached, and returns + * the resulting term t', which is such that + * (exists k) new_nodes => t = t' + * is valid, where k are the free skolems introduced when constructing + * new_nodes. + */ + Node processAssertion(Node t, std::vector<Node>& new_nodes); + /** + * Replaces all formulas t in vec_node with an equivalent formula t' that + * contains no free instances of extended functions (that is, extended + * functions may only appear beneath quantifiers). This applies simplifyRec + * on each assertion in vec_node until a fixed point is reached. + */ + void processAssertions(std::vector<Node>& vec_node); -private: - /** commonly used constants */ - Node d_zero; - Node d_one; - Node d_neg_one; - Node d_empty_str; - /** pointer to the skolem cache used by this class */ - SkolemCache *d_sc; - /** - * Applies simplify to all top-level extended function subterms of t. New - * assertions created in this reduction are added to new_nodes. The argument - * visited stores a cache of previous results. - */ - Node simplifyRec(Node t, - std::vector<Node> &new_nodes, - std::map<Node, Node> &visited); + private: + /** commonly used constants */ + Node d_zero; + Node d_one; + Node d_neg_one; + Node d_empty_str; + /** pointer to the skolem cache used by this class */ + SkolemCache* d_sc; + /** Reference to the statistics for the theory of strings/sequences. */ + SequencesStatistics& d_statistics; + /** + * Applies simplify to all top-level extended function subterms of t. New + * assertions created in this reduction are added to new_nodes. The argument + * visited stores a cache of previous results. + */ + Node simplifyRec(Node t, + std::vector<Node>& new_nodes, + std::map<Node, Node>& visited); }; }/* CVC4::theory::strings namespace */ |