From: Andrew Reynolds Date: Tue, 16 Mar 2021 19:14:33 +0000 (-0500) Subject: Further standardization of strings statistics (#6128) X-Git-Tag: cvc5-1.0.0~2068 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8c11c5b2683aa13160447aef302d82115a08081a;p=cvc5.git Further standardization of strings statistics (#6128) Also eliminates use of raw output channel in strings. --- diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index 7eeba8497..e53ba35f8 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -292,6 +292,10 @@ const char* toString(InferenceId i) case InferenceId::STRINGS_CTN_POS: return "STRINGS_CTN_POS"; case InferenceId::STRINGS_REDUCTION: return "STRINGS_REDUCTION"; case InferenceId::STRINGS_PREFIX_CONFLICT: return "STRINGS_PREFIX_CONFLICT"; + case InferenceId::STRINGS_REGISTER_TERM_ATOMIC: + return "STRINGS_REGISTER_TERM_ATOMIC"; + case InferenceId::STRINGS_REGISTER_TERM: return "STRINGS_REGISTER_TERM"; + case InferenceId::STRINGS_CMI_SPLIT: return "STRINGS_CMI_SPLIT"; case InferenceId::UF_HO_APP_ENCODE: return "UF_HO_APP_ENCODE"; case InferenceId::UF_HO_APP_CONV_SKOLEM: return "UF_HO_APP_CONV_SKOLEM"; diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h index b6d0d3c25..4af7761a0 100644 --- a/src/theory/inference_id.h +++ b/src/theory/inference_id.h @@ -384,7 +384,6 @@ enum class InferenceId STRINGS_CARD_SP, // The cardinality inference for strings, see Liang et al CAV 2014. STRINGS_CARDINALITY, - //-------------------- end base solver //-------------------- core solver // A cycle in the empty string equivalence class, e.g.: // x ++ y = "" => x = "" @@ -522,14 +521,12 @@ enum class InferenceId // is unknown, we apply the inference: // len(s) != len(t) V len(s) = len(t) STRINGS_DEQ_LENGTH_SP, - //-------------------- end core solver //-------------------- codes solver // str.to_code( v ) = rewrite( str.to_code(c) ) // where v is the proxy variable for c. STRINGS_CODE_PROXY, // str.code(x) = -1 V str.code(x) != str.code(y) V x = y STRINGS_CODE_INJ, - //-------------------- end codes solver //-------------------- regexp solver // regular expression normal form conflict // ( x in R ^ x = y ^ rewrite((str.in_re y R)) = false ) => false @@ -565,7 +562,6 @@ enum class InferenceId STRINGS_RE_DELTA_CONF, // regular expression derive ??? STRINGS_RE_DERIVE, - //-------------------- end regexp solver //-------------------- extended function solver // Standard extended function inferences from context-dependent rewriting // produced by constant substitutions. See Reynolds et al CAV 2017. These are @@ -611,11 +607,16 @@ enum class InferenceId // f(x1, .., xn) and P is the reduction predicate for f // (see theory_strings_preprocess). STRINGS_REDUCTION, - //-------------------- end extended function solver //-------------------- prefix conflict // prefix conflict (coarse-grained) STRINGS_PREFIX_CONFLICT, - //-------------------- end prefix conflict + //-------------------- other + // a lemma added during term registration for an atomic term + STRINGS_REGISTER_TERM_ATOMIC, + // a lemma added during term registration + STRINGS_REGISTER_TERM, + // a split during collect model info + STRINGS_CMI_SPLIT, //-------------------------------------- end strings theory //-------------------------------------- uf theory diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp index b746f2961..3c5bcc98d 100644 --- a/src/theory/strings/core_solver.cpp +++ b/src/theory/strings/core_solver.cpp @@ -1941,7 +1941,7 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi, SkolemCache* skc = d_termReg.getSkolemCache(); Node sk_w = skc->mkSkolem("w_loop"); Node sk_y = skc->mkSkolem("y_loop"); - d_termReg.registerTermAtomic(sk_y, LENGTH_GEQ_ONE); + iinfo.d_skolems[LENGTH_GEQ_ONE].push_back(sk_y); Node sk_z = skc->mkSkolem("z_loop"); // t1 * ... * tn = y * z Node conc1 = t_yz.eqNode(utils::mkNConcat(sk_y, sk_z)); diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp index 0daaac29b..0d4839238 100644 --- a/src/theory/strings/inference_manager.cpp +++ b/src/theory/strings/inference_manager.cpp @@ -372,8 +372,6 @@ TrustNode InferenceManager::processLemma(InferInfo& ii, LemmaProperty& p) << ii.getId() << std::endl; Trace("strings-lemma") << "Strings::Lemma: " << tlem.getNode() << " by " << ii.getId() << std::endl; - ++(d_statistics.d_lemmasInfer); - return tlem; } diff --git a/src/theory/strings/sequences_stats.cpp b/src/theory/strings/sequences_stats.cpp index ec6b5e89b..c679bc414 100644 --- a/src/theory/strings/sequences_stats.cpp +++ b/src/theory/strings/sequences_stats.cpp @@ -31,13 +31,7 @@ SequencesStatistics::SequencesStatistics() d_rewrites("theory::strings::rewrites"), d_conflictsEqEngine("theory::strings::conflictsEqEngine", 0), d_conflictsEager("theory::strings::conflictsEager", 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) + d_conflictsInfer("theory::strings::conflictsInfer", 0) { smtStatisticsRegistry()->registerStat(&d_checkRuns); smtStatisticsRegistry()->registerStat(&d_strategyRuns); @@ -50,11 +44,6 @@ SequencesStatistics::SequencesStatistics() smtStatisticsRegistry()->registerStat(&d_conflictsEqEngine); smtStatisticsRegistry()->registerStat(&d_conflictsEager); 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() @@ -70,11 +59,6 @@ SequencesStatistics::~SequencesStatistics() smtStatisticsRegistry()->unregisterStat(&d_conflictsEqEngine); smtStatisticsRegistry()->unregisterStat(&d_conflictsEager); 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 01075eb26..1a0e94cdb 100644 --- a/src/theory/strings/sequences_stats.h +++ b/src/theory/strings/sequences_stats.h @@ -47,9 +47,6 @@ namespace strings { * * "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 { @@ -98,18 +95,6 @@ class SequencesStatistics /** 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/term_registry.cpp b/src/theory/strings/term_registry.cpp index 628b2798d..9497b9661 100644 --- a/src/theory/strings/term_registry.cpp +++ b/src/theory/strings/term_registry.cpp @@ -19,6 +19,7 @@ #include "options/strings_options.h" #include "smt/logic_exception.h" #include "theory/rewriter.h" +#include "theory/strings/inference_manager.h" #include "theory/strings/theory_strings_utils.h" #include "theory/strings/word.h" @@ -37,11 +38,10 @@ typedef expr::Attribute StringsProxyVarAttribute; TermRegistry::TermRegistry(SolverState& s, - OutputChannel& out, SequencesStatistics& statistics, ProofNodeManager* pnm) : d_state(s), - d_out(out), + d_im(nullptr), d_statistics(statistics), d_hasStrCode(false), d_functionsTerms(s.getSatContext()), @@ -65,6 +65,8 @@ TermRegistry::TermRegistry(SolverState& s, TermRegistry::~TermRegistry() {} +void TermRegistry::finishInit(InferenceManager* im) { d_im = im; } + Node TermRegistry::eagerReduce(Node t, SkolemCache* sc) { NodeManager* nm = NodeManager::currentNM(); @@ -162,7 +164,7 @@ void TermRegistry::preRegisterTerm(TNode n) } else if (k == STRING_IN_REGEXP) { - d_out.requirePhase(n, true); + d_im->requirePhase(n, true); ee->addTriggerPredicate(n); ee->addTerm(n[0]); ee->addTerm(n[1]); @@ -302,8 +304,7 @@ void TermRegistry::registerTerm(Node n, int effort) << std::endl; Trace("strings-assert") << "(assert " << regTermLem.getNode() << ")" << std::endl; - ++(d_statistics.d_lemmasRegisterTerm); - d_out.trustedLemma(regTermLem); + d_im->trustedLemma(regTermLem, InferenceId::STRINGS_REGISTER_TERM); } } @@ -416,12 +417,11 @@ void TermRegistry::registerTermAtomic(Node n, LengthStatus s) << std::endl; Trace("strings-assert") << "(assert " << lenLem.getNode() << ")" << std::endl; - ++(d_statistics.d_lemmasRegisterTermAtomic); - d_out.trustedLemma(lenLem); + d_im->trustedLemma(lenLem, InferenceId::STRINGS_REGISTER_TERM_ATOMIC); } for (const std::pair& rp : reqPhase) { - d_out.requirePhase(rp.first, rp.second); + d_im->requirePhase(rp.first, rp.second); } } diff --git a/src/theory/strings/term_registry.h b/src/theory/strings/term_registry.h index 261ba277c..a3d1d1e0e 100644 --- a/src/theory/strings/term_registry.h +++ b/src/theory/strings/term_registry.h @@ -32,6 +32,7 @@ namespace CVC4 { namespace theory { namespace strings { +class InferenceManager; /** * This class manages all the (pre)registration tasks for terms. These tasks * include: @@ -50,10 +51,11 @@ class TermRegistry public: TermRegistry(SolverState& s, - OutputChannel& out, SequencesStatistics& statistics, ProofNodeManager* pnm); ~TermRegistry(); + /** Finish initialize, which sets the inference manager */ + void finishInit(InferenceManager* im); /** The eager reduce routine * * Constructs a lemma for t that is incomplete, but communicates pertinent @@ -205,8 +207,8 @@ class TermRegistry uint32_t d_cardSize; /** Reference to the solver state of the theory of strings. */ SolverState& d_state; - /** Reference to the output channel of the theory of strings. */ - OutputChannel& d_out; + /** Pointer to the inference manager of the theory of strings. */ + InferenceManager* d_im; /** Reference to the statistics for the theory of strings/sequences. */ SequencesStatistics& d_statistics; /** have we asserted any str.code terms? */ diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index fbede89f0..2a5d043f5 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -47,7 +47,7 @@ TheoryStrings::TheoryStrings(context::Context* c, d_statistics(), d_state(c, u, d_valuation), d_eagerSolver(d_state), - d_termReg(d_state, out, d_statistics, pnm), + d_termReg(d_state, d_statistics, pnm), d_extTheoryCb(), d_extTheory(d_extTheoryCb, c, u, out), d_im(*this, d_state, d_termReg, d_extTheory, d_statistics, pnm), @@ -71,6 +71,7 @@ TheoryStrings::TheoryStrings(context::Context* c, d_regexp_elim(options::regExpElimAgg(), pnm, u), d_stringsFmf(c, u, valuation, d_termReg) { + d_termReg.finishInit(&d_im); d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) ); d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) ); @@ -167,21 +168,7 @@ bool TheoryStrings::areCareDisequal( TNode x, TNode y ) { bool TheoryStrings::propagateLit(TNode literal) { - Debug("strings-propagate") - << "TheoryStrings::propagateLit(" << literal << ")" << std::endl; - // If already in conflict, no more propagation - if (d_state.isInConflict()) - { - Debug("strings-propagate") << "TheoryStrings::propagateLit(" << literal - << "): already in conflict" << std::endl; - return false; - } - // Propagate out - bool ok = d_out->propagate(literal); - if (!ok) { - d_state.notifyInConflict(); - } - return ok; + return d_im.propagateLit(literal); } TrustNode TheoryStrings::explain(TNode literal) @@ -455,8 +442,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); + d_im.lemma(spl, InferenceId::STRINGS_CMI_SPLIT); Trace("strings-lemma") << "Strings::CollectModelInfoSplit: " << spl << std::endl; }