From aa6fb6fa3df0b1519e6763e72541c022396ab1dc Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 2 Apr 2020 00:01:21 -0500 Subject: Introduce enums for all string inferences, excluding the core solver (#4195) Introduce enum values for all calls to sendInference outside of the core solver. This included some minor refactoring. --- src/theory/strings/base_solver.cpp | 11 ++-- src/theory/strings/extf_solver.cpp | 16 +++--- src/theory/strings/extf_solver.h | 2 + src/theory/strings/infer_info.cpp | 21 ++++++++ src/theory/strings/infer_info.h | 92 +++++++++++++++++++++++++++++++++ src/theory/strings/regexp_operation.cpp | 4 +- src/theory/strings/regexp_solver.cpp | 33 ++++++++---- src/theory/strings/regexp_solver.h | 4 ++ src/theory/strings/sequences_stats.cpp | 9 ++++ src/theory/strings/sequences_stats.h | 46 ++++++++++++++++- src/theory/strings/theory_strings.cpp | 3 +- 11 files changed, 215 insertions(+), 26 deletions(-) diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp index af0e7cc37..076fc1cc5 100644 --- a/src/theory/strings/base_solver.cpp +++ b/src/theory/strings/base_solver.cpp @@ -127,7 +127,7 @@ void BaseSolver::checkInit() } } // infer the equality - d_im.sendInference(exp, n.eqNode(nc), "I_Norm"); + d_im.sendInference(exp, n.eqNode(nc), Inference::I_NORM); } else { @@ -172,7 +172,7 @@ void BaseSolver::checkInit() } AlwaysAssert(foundNEmpty); // infer the equality - d_im.sendInference(exp, n.eqNode(ns), "I_Norm_S"); + d_im.sendInference(exp, n.eqNode(ns), Inference::I_NORM_S); } d_congruent.insert(n); congruent[k]++; @@ -301,7 +301,7 @@ void BaseSolver::checkConstantEquivalenceClasses(TermIndex* ti, Assert(countc == vecc.size()); if (d_state.hasTerm(c)) { - d_im.sendInference(exp, n.eqNode(c), "I_CONST_MERGE"); + d_im.sendInference(exp, n.eqNode(c), Inference::I_CONST_MERGE); return; } else if (!d_im.hasProcessed()) @@ -333,7 +333,7 @@ void BaseSolver::checkConstantEquivalenceClasses(TermIndex* ti, exp.push_back(d_eqcToConstExp[nr]); d_im.addToExplanation(n, d_eqcToConstBase[nr], exp); } - d_im.sendInference(exp, d_false, "I_CONST_CONFLICT"); + d_im.sendInference(exp, d_false, Inference::I_CONST_CONFLICT); return; } else @@ -483,7 +483,8 @@ void BaseSolver::checkCardinality() if (!cons.isConst() || !cons.getConst()) { std::vector emptyVec; - d_im.sendInference(emptyVec, vec_node, cons, "CARDINALITY", true); + d_im.sendInference( + emptyVec, vec_node, cons, Inference::CARDINALITY, true); return; } } diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp index 47f36af4c..a1c04848a 100644 --- a/src/theory/strings/extf_solver.cpp +++ b/src/theory/strings/extf_solver.cpp @@ -42,6 +42,7 @@ ExtfSolver::ExtfSolver(context::Context* c, d_bsolver(bs), d_csolver(cs), d_extt(et), + d_statistics(stats), d_preproc(&skc, u, stats), d_hasExtf(c, false), d_extfInferCache(c) @@ -113,7 +114,7 @@ bool ExtfSolver::doReduction(int effort, Node n, bool& isCd) lexp.push_back(lenx.eqNode(lens)); lexp.push_back(n.negate()); Node xneqs = x.eqNode(s).negate(); - d_im.sendInference(lexp, xneqs, "NEG-CTN-EQL", true); + d_im.sendInference(lexp, xneqs, Inference::CTN_NEG_EQUAL, true); } // this depends on the current assertions, so we set that this // inference is context-dependent. @@ -158,7 +159,7 @@ bool ExtfSolver::doReduction(int effort, Node n, bool& isCd) Node eq = Rewriter::rewrite(x.eqNode(utils::mkNConcat(sk1, s, sk2))); std::vector exp_vec; exp_vec.push_back(n); - d_im.sendInference(d_emptyVec, exp_vec, eq, "POS-CTN", true); + d_im.sendInference(d_emptyVec, exp_vec, eq, Inference::CTN_POS, true); Trace("strings-extf-debug") << " resolve extf : " << n << " based on positive contain reduction." << std::endl; @@ -184,7 +185,7 @@ bool ExtfSolver::doReduction(int effort, Node n, bool& isCd) Trace("strings-red-lemma") << "Reduction_" << effort << " lemma : " << nnlem << std::endl; Trace("strings-red-lemma") << "...from " << n << std::endl; - d_im.sendInference(d_emptyVec, nnlem, "Reduction", true); + d_im.sendInference(d_emptyVec, nnlem, Inference::REDUCTION, true); Trace("strings-extf-debug") << " resolve extf : " << n << " based on reduction." << std::endl; isCd = false; @@ -363,8 +364,9 @@ void ExtfSolver::checkExtfEval(int effort) { Trace("strings-extf") << " resolve extf : " << sn << " -> " << nrc << std::endl; - d_im.sendInference( - einfo.d_exp, conc, effort == 0 ? "EXTF" : "EXTF-N", true); + Inference inf = effort == 0 ? Inference::EXTF : Inference::EXTF_N; + d_im.sendInference(einfo.d_exp, conc, inf, true); + d_statistics.d_cdSimplifications << n.getKind(); if (d_state.isInConflict()) { Trace("strings-extf-debug") << " conflict, return." << std::endl; @@ -514,7 +516,7 @@ void ExtfSolver::checkExtfInference(Node n, if (d_state.areEqual(conc, d_false)) { // we are in conflict - d_im.sendInference(in.d_exp, conc, "CTN_Decompose"); + d_im.sendInference(in.d_exp, conc, Inference::CTN_DECOMPOSE); } else if (d_extt->hasFunctionKind(conc.getKind())) { @@ -591,7 +593,7 @@ void ExtfSolver::checkExtfInference(Node n, exp_c.insert(exp_c.end(), d_extfInfoTmp[ofrom].d_exp.begin(), d_extfInfoTmp[ofrom].d_exp.end()); - d_im.sendInference(exp_c, conc, "CTN_Trans"); + d_im.sendInference(exp_c, conc, Inference::CTN_TRANS); } } } diff --git a/src/theory/strings/extf_solver.h b/src/theory/strings/extf_solver.h index 040871ffa..9ca72fed2 100644 --- a/src/theory/strings/extf_solver.h +++ b/src/theory/strings/extf_solver.h @@ -186,6 +186,8 @@ class ExtfSolver CoreSolver& d_csolver; /** the extended theory object for the theory of strings */ ExtTheory* d_extt; + /** Reference to the statistics for the theory of strings/sequences. */ + SequencesStatistics& d_statistics; /** preprocessing utility, for performing strings reductions */ StringsPreprocess d_preproc; /** Common constants */ diff --git a/src/theory/strings/infer_info.cpp b/src/theory/strings/infer_info.cpp index 3b4a6b857..1d0ee30ad 100644 --- a/src/theory/strings/infer_info.cpp +++ b/src/theory/strings/infer_info.cpp @@ -22,6 +22,11 @@ const char* toString(Inference i) { switch (i) { + case Inference::I_NORM_S: return "I_NORM_S"; + case Inference::I_CONST_MERGE: return "I_CONST_MERGE"; + case Inference::I_CONST_CONFLICT: return "I_CONST_CONFLICT"; + case Inference::I_NORM: return "I_NORM"; + case Inference::CARDINALITY: return "CARDINALITY"; case Inference::N_ENDPOINT_EMP: return "N_ENDPOINT_EMP"; case Inference::N_UNIFY: return "N_UNIFY"; case Inference::N_ENDPOINT_EQ: return "N_ENDPOINT_EQ"; @@ -34,6 +39,22 @@ const char* toString(Inference i) case Inference::SSPLIT_CST: return "SSPLIT_CST"; case Inference::SSPLIT_VAR: return "SSPLIT_VAR"; case Inference::FLOOP: return "FLOOP"; + case Inference::RE_NF_CONFLICT: return "RE_NF_CONFLICT"; + case Inference::RE_UNFOLD_POS: return "RE_UNFOLD_POS"; + case Inference::RE_UNFOLD_NEG: return "RE_UNFOLD_NEG"; + case Inference::RE_INTER_INCLUDE: return "RE_INTER_INCLUDE"; + case Inference::RE_INTER_CONF: return "RE_INTER_CONF"; + case Inference::RE_INTER_INFER: return "RE_INTER_INFER"; + case Inference::RE_DELTA: return "RE_DELTA"; + case Inference::RE_DELTA_CONF: return "RE_DELTA_CONF"; + case Inference::RE_DERIVE: return "RE_DERIVE"; + case Inference::EXTF: return "EXTF"; + case Inference::EXTF_N: return "EXTF_N"; + case Inference::CTN_TRANS: return "CTN_TRANS"; + case Inference::CTN_DECOMPOSE: return "CTN_DECOMPOSE"; + case Inference::CTN_NEG_EQUAL: return "CTN_NEG_EQUAL"; + case Inference::CTN_POS: return "CTN_POS"; + case Inference::REDUCTION: return "REDUCTION"; default: return "?"; } } diff --git a/src/theory/strings/infer_info.h b/src/theory/strings/infer_info.h index e13a5a2ff..252445cb4 100644 --- a/src/theory/strings/infer_info.h +++ b/src/theory/strings/infer_info.h @@ -38,6 +38,31 @@ namespace strings { */ enum class Inference : uint32_t { + //-------------------------------------- base solver + // initial normalize singular + // x1 = "" ^ ... ^ x_{i-1} = "" ^ x_{i+1} = "" ^ ... ^ xn = "" => + // x1 ++ ... ++ xn = xi + I_NORM_S, + // initial constant merge + // explain_constant(x, c) => x = c + // Above, explain_constant(x,c) is a basic explanation of why x must be equal + // to string constant c, which is computed by taking arguments of + // concatentation terms that are entailed to be constants. For example: + // ( y = "AB" ^ z = "C" ) => y ++ z = "ABC" + I_CONST_MERGE, + // initial constant conflict + // ( explain_constant(x, c1) ^ explain_constant(x, c2) ^ x = y) => false + // where c1 != c2. + I_CONST_CONFLICT, + // initial normalize + // Given two concatenation terms, this is applied when we find that they are + // equal after e.g. removing strings that are currently empty. For example: + // y = "" ^ z = "" => x ++ y = z ++ x + I_NORM, + // The cardinality inference for strings, see Liang et al CAV 2014. + CARDINALITY, + //-------------------------------------- end base solver + //-------------------------------------- core solver // Given two normal forms, infers that the remainder one of them has to be // empty. For example: // If x1 ++ x2 = y1 and x1 = y1, then x2 = "" @@ -94,6 +119,73 @@ enum class Inference : uint32_t // for fresh u, u1, u2. // This is the rule F-Loop from Figure 5 of Liang et al CAV 2014. FLOOP, + //-------------------------------------- end core solver + //-------------------------------------- regexp solver + // regular expression normal form conflict + // ( x in R ^ x = y ^ rewrite((str.in_re y R)) = false ) => false + // where y is the normal form computed for x. + RE_NF_CONFLICT, + // regular expression unfolding + // This is a general class of inferences of the form: + // (x in R) => F + // where F is formula expressing the next step of checking whether x is in + // R. For example: + // (x in (R)*) => + // x = "" V x in R V ( x = x1 ++ x2 ++ x3 ^ x1 in R ^ x2 in (R)* ^ x3 in R) + RE_UNFOLD_POS, + // Same as above, for negative memberships + RE_UNFOLD_NEG, + // intersection inclusion conflict + // (x in R1 ^ ~ x in R2) => false where [[includes(R2,R1)]] + // Where includes(R2,R1) is a heuristic check for whether R2 includes R1. + RE_INTER_INCLUDE, + // intersection conflict, using regexp intersection computation + // (x in R1 ^ x in R2) => false where [[intersect(R1, R2) = empty]] + RE_INTER_CONF, + // intersection inference + // (x in R1 ^ y in R2 ^ x = y) => (x in re.inter(R1,R2)) + RE_INTER_INFER, + // regular expression delta + // (x = "" ^ x in R) => C + // where "" in R holds if and only if C holds. + RE_DELTA, + // regular expression delta conflict + // (x = "" ^ x in R) => false + // where R does not accept the empty string. + RE_DELTA_CONF, + // regular expression derive ??? + RE_DERIVE, + //-------------------------------------- end regexp solver + //-------------------------------------- extended function solver + // All extended function inferences from context-dependent rewriting produced + // by constant substitutions. See Reynolds et al CAV 2017. These are + // inferences of the form: + // X = Y => f(X) = t when rewrite( f(Y) ) = t + // where X = Y is a vector of equalities, where some of Y may be constants. + EXTF, + // Same as above, for normal form substitutions. + EXTF_N, + // contain transitive + // ( str.contains( s, t ) ^ ~contains( s, r ) ) => ~contains( t, r ). + CTN_TRANS, + // contain decompose + // str.contains( x, str.++( y1, ..., yn ) ) => str.contains( x, yi ) or + // ~str.contains( str.++( x1, ..., xn ), y ) => ~str.contains( xi, y ) + CTN_DECOMPOSE, + // contain neg equal + // ( len( x ) = len( s ) ^ ~contains( x, s ) ) => x != s + CTN_NEG_EQUAL, + // contain positive + // str.contains( x, y ) => x = w1 ++ y ++ w2 + // where w1 and w2 are skolem variables. + CTN_POS, + // All reduction inferences of the form: + // f(x1, .., xn) = y ^ P(x1, ..., xn, y) + // where f is an extended function, y is the purification variable for + // f(x1, .., xn) and P is the reduction predicate for f + // (see theory_strings_preprocess). + REDUCTION, + //-------------------------------------- end extended function solver NONE, }; diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index 6453e1909..d104f3ade 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -844,8 +844,8 @@ void RegExpOpr::firstChars(Node r, std::set &pcset, SetNodes &pvset) void RegExpOpr::simplify(Node t, std::vector< Node > &new_nodes, bool polarity) { Trace("strings-regexp-simpl") << "RegExp-Simpl starts with " << t << ", polarity=" << polarity << std::endl; Assert(t.getKind() == kind::STRING_IN_REGEXP); - Node str = Rewriter::rewrite(t[0]); - Node re = Rewriter::rewrite(t[1]); + Node str = t[0]; + Node re = t[1]; if(polarity) { simplifyPRegExp( str, re, new_nodes ); } else { diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp index 30f9c4a73..f6ef92b4d 100644 --- a/src/theory/strings/regexp_solver.cpp +++ b/src/theory/strings/regexp_solver.cpp @@ -36,12 +36,14 @@ RegExpSolver::RegExpSolver(TheoryStrings& p, SolverState& s, InferenceManager& im, ExtfSolver& es, + SequencesStatistics& stats, context::Context* c, context::UserContext* u) : d_parent(p), d_state(s), d_im(im), d_esolver(es), + d_statistics(stats), d_regexp_ucached(u), d_regexp_ccached(c), d_processed_memberships(c) @@ -160,6 +162,7 @@ void RegExpSolver::check(const std::map >& mems) << "We have regular expression assertion : " << assertion << std::endl; Node atom = assertion.getKind() == NOT ? assertion[0] : assertion; + Assert(atom == Rewriter::rewrite(atom)); bool polarity = assertion.getKind() != NOT; if (polarity != (e == 0)) { @@ -222,7 +225,7 @@ void RegExpSolver::check(const std::map >& mems) std::vector exp_n; exp_n.push_back(assertion); Node conc = Node::null(); - d_im.sendInference(nfexp, exp_n, conc, "REGEXP NF Conflict"); + d_im.sendInference(nfexp, exp_n, conc, Inference::RE_NF_CONFLICT); addedLemma = true; break; } @@ -268,7 +271,18 @@ void RegExpSolver::check(const std::map >& mems) std::vector exp_n; exp_n.push_back(assertion); Node conc = nvec.size() == 1 ? nvec[0] : nm->mkNode(AND, nvec); - d_im.sendInference(rnfexp, exp_n, conc, "REGEXP_Unfold"); + Assert(atom.getKind() == STRING_IN_REGEXP); + if (polarity) + { + d_statistics.d_regexpUnfoldingsPos << atom[1].getKind(); + } + else + { + d_statistics.d_regexpUnfoldingsNeg << atom[1].getKind(); + } + Inference inf = + polarity ? Inference::RE_UNFOLD_POS : Inference::RE_UNFOLD_NEG; + d_im.sendInference(rnfexp, exp_n, conc, inf); addedLemma = true; if (changed) { @@ -387,7 +401,8 @@ bool RegExpSolver::checkEqcInclusion(std::vector& mems) } Node conc; - d_im.sendInference(vec_nodes, conc, "Intersect inclusion", true); + d_im.sendInference( + vec_nodes, conc, Inference::RE_INTER_INCLUDE, true); return false; } } @@ -470,7 +485,7 @@ bool RegExpSolver::checkEqcIntersect(const std::vector& mems) vec_nodes.push_back(mi[0].eqNode(m[0])); } Node conc; - d_im.sendInference(vec_nodes, conc, "INTERSECT CONFLICT", true); + d_im.sendInference(vec_nodes, conc, Inference::RE_INTER_CONF, true); // conflict, return return false; } @@ -490,7 +505,7 @@ bool RegExpSolver::checkEqcIntersect(const std::vector& mems) else { // new conclusion - // (x in R ^ y in R2 ^ x = y) => (x in intersect(R1,R2)) + // (x in R1 ^ y in R2 ^ x = y) => (x in intersect(R1,R2)) std::vector vec_nodes; vec_nodes.push_back(mi); vec_nodes.push_back(m); @@ -498,7 +513,7 @@ bool RegExpSolver::checkEqcIntersect(const std::vector& mems) { vec_nodes.push_back(mi[0].eqNode(m[0])); } - d_im.sendInference(vec_nodes, mres, "INTERSECT INFER", true); + d_im.sendInference(vec_nodes, mres, Inference::RE_INTER_INFER, true); // both are reduced d_parent.getExtTheory()->markReduced(m); d_parent.getExtTheory()->markReduced(mi); @@ -522,7 +537,7 @@ bool RegExpSolver::checkPDerivative( std::vector exp_n; exp_n.push_back(atom); exp_n.push_back(x.eqNode(d_emptyString)); - d_im.sendInference(nf_exp, exp_n, exp, "RegExp Delta"); + d_im.sendInference(nf_exp, exp_n, exp, Inference::RE_DELTA); addedLemma = true; d_regexp_ccached.insert(atom); return false; @@ -538,7 +553,7 @@ bool RegExpSolver::checkPDerivative( exp_n.push_back(atom); exp_n.push_back(x.eqNode(d_emptyString)); Node conc; - d_im.sendInference(nf_exp, exp_n, conc, "RegExp Delta CONFLICT"); + d_im.sendInference(nf_exp, exp_n, conc, Inference::RE_DELTA_CONF); addedLemma = true; d_regexp_ccached.insert(atom); return false; @@ -628,7 +643,7 @@ bool RegExpSolver::deriveRegExp(Node x, } std::vector exp_n; exp_n.push_back(atom); - d_im.sendInference(ant, exp_n, conc, "RegExp-Derive"); + d_im.sendInference(ant, exp_n, conc, Inference::RE_DERIVE); return true; } return false; diff --git a/src/theory/strings/regexp_solver.h b/src/theory/strings/regexp_solver.h index d18604752..1d065181b 100644 --- a/src/theory/strings/regexp_solver.h +++ b/src/theory/strings/regexp_solver.h @@ -26,6 +26,7 @@ #include "theory/strings/extf_solver.h" #include "theory/strings/inference_manager.h" #include "theory/strings/regexp_operation.h" +#include "theory/strings/sequences_stats.h" #include "theory/strings/solver_state.h" #include "util/string.h" @@ -49,6 +50,7 @@ class RegExpSolver SolverState& s, InferenceManager& im, ExtfSolver& es, + SequencesStatistics& stats, context::Context* c, context::UserContext* u); ~RegExpSolver() {} @@ -119,6 +121,8 @@ class RegExpSolver InferenceManager& d_im; /** reference to the extended function solver of the parent */ ExtfSolver& d_esolver; + /** Reference to the statistics for the theory of strings/sequences. */ + SequencesStatistics& d_statistics; // check membership constraints Node mkAnd(Node c1, Node c2); /** diff --git a/src/theory/strings/sequences_stats.cpp b/src/theory/strings/sequences_stats.cpp index fb13cdab2..5cd844290 100644 --- a/src/theory/strings/sequences_stats.cpp +++ b/src/theory/strings/sequences_stats.cpp @@ -23,7 +23,10 @@ namespace strings { SequencesStatistics::SequencesStatistics() : d_inferences("theory::strings::inferences"), + d_cdSimplifications("theory::strings::cdSimplifications"), d_reductions("theory::strings::reductions"), + d_regexpUnfoldingsPos("theory::strings::regexpUnfoldingsPos"), + d_regexpUnfoldingsNeg("theory::strings::regexpUnfoldingsNeg"), d_conflictsEqEngine("theory::strings::conflictsEqEngine", 0), d_conflictsEagerPrefix("theory::strings::conflictsEagerPrefix", 0), d_conflictsInfer("theory::strings::conflictsInfer", 0), @@ -35,7 +38,10 @@ SequencesStatistics::SequencesStatistics() d_lemmasInfer("theory::strings::lemmasInfer", 0) { smtStatisticsRegistry()->registerStat(&d_inferences); + smtStatisticsRegistry()->registerStat(&d_cdSimplifications); smtStatisticsRegistry()->registerStat(&d_reductions); + smtStatisticsRegistry()->registerStat(&d_regexpUnfoldingsPos); + smtStatisticsRegistry()->registerStat(&d_regexpUnfoldingsNeg); smtStatisticsRegistry()->registerStat(&d_conflictsEqEngine); smtStatisticsRegistry()->registerStat(&d_conflictsEagerPrefix); smtStatisticsRegistry()->registerStat(&d_conflictsInfer); @@ -49,7 +55,10 @@ SequencesStatistics::SequencesStatistics() SequencesStatistics::~SequencesStatistics() { smtStatisticsRegistry()->unregisterStat(&d_inferences); + smtStatisticsRegistry()->unregisterStat(&d_cdSimplifications); smtStatisticsRegistry()->unregisterStat(&d_reductions); + smtStatisticsRegistry()->unregisterStat(&d_regexpUnfoldingsPos); + smtStatisticsRegistry()->unregisterStat(&d_regexpUnfoldingsNeg); smtStatisticsRegistry()->unregisterStat(&d_conflictsEqEngine); smtStatisticsRegistry()->unregisterStat(&d_conflictsEagerPrefix); smtStatisticsRegistry()->unregisterStat(&d_conflictsInfer); diff --git a/src/theory/strings/sequences_stats.h b/src/theory/strings/sequences_stats.h index 83a16cb23..65f50dbbc 100644 --- a/src/theory/strings/sequences_stats.h +++ b/src/theory/strings/sequences_stats.h @@ -25,16 +25,58 @@ namespace CVC4 { namespace theory { namespace strings { +/** + * Statistics for the theory of strings. + * + * This is roughly broken up into the following parts: + * (1) Inferences, + * (2) Conflicts, + * (3) Lemmas. + * + * "Inferences" (1) are steps invoked during solving, which either trigger: + * (a) An internal update to the state of the solver (e.g. adding an inferred + * equality to the equality engine), + * (b) A call to OutputChannel::conflict, + * (c) A call to OutputChannel::lemma. + * For details, see InferenceManager. We track stats on each kind of + * inference that have been indicated by the solvers in TheoryStrings. + * Some kinds of inferences are further distinguished by the Kind of the node + * they operate on (see d_cdSimplifications, d_reductions, d_regexpUnfoldings). + * + * "Conflicts" (2) arise from various kinds of reasoning, listed below, + * where inferences are one of the possible methods for deriving conflicts. + * + * "Lemmas" (3) also arise from various kinds of reasoning, listed below, + * where inferences are one of the possible methods for deriving lemmas. + */ class SequencesStatistics { public: SequencesStatistics(); ~SequencesStatistics(); - + //--------------- inferences /** Counts the number of applications of each type of inference */ HistogramStat d_inferences; - /** Counts the number of applications of each type of reduction */ + /** + * Counts the number of applications of each type of context-dependent + * simplification. The sum of this map is equal to the number of EXTF or + * EXTF_N inferences. + */ + HistogramStat d_cdSimplifications; + /** + * Counts the number of applications of each type of reduction. The sum of + * this map is equal to the number of REDUCTION inferences (when + * options::stringLazyPreproc is true). + */ HistogramStat d_reductions; + /** + * Counts the number of applications of each type of regular expression + * positive (resp. negative) unfoldings. The sum of this map is equal to the + * number of RE_UNFOLD_POS (resp. RE_UNFOLD_NEG) inferences. + */ + HistogramStat d_regexpUnfoldingsPos; + HistogramStat d_regexpUnfoldingsNeg; + //--------------- end of inferences //--------------- conflicts, partition of calls to OutputChannel::conflict /** Number of equality engine conflicts */ IntStat d_conflictsEqEngine; diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index f9eeb2010..d5eb2dbbd 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -95,7 +95,8 @@ TheoryStrings::TheoryStrings(context::Context* c, d_csolver, extt, d_statistics)); - d_rsolver.reset(new RegExpSolver(*this, d_state, d_im, *d_esolver, c, u)); + d_rsolver.reset( + new RegExpSolver(*this, d_state, d_im, *d_esolver, d_statistics, c, u)); // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::STRING_LENGTH); -- cgit v1.2.3