From: Gereon Kremer Date: Thu, 18 Feb 2021 22:59:37 +0000 (+0100) Subject: Add statistic for InferenceId to TheoryInferenceManager. (#5913) X-Git-Tag: cvc5-1.0.0~2263 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=251bd84f628be2ce5ac2159b48112d9383c071c3;p=cvc5.git Add statistic for InferenceId to TheoryInferenceManager. (#5913) This PR uses the IntegralHistogramStat to obtain statistics about the sent inferences within the TheoryInferenceManager. All theories are adapted to provide a proper name (prefix) for the name of the statistic. --- diff --git a/src/theory/arith/inference_manager.cpp b/src/theory/arith/inference_manager.cpp index aa0aa4f2a..c406c0ce6 100644 --- a/src/theory/arith/inference_manager.cpp +++ b/src/theory/arith/inference_manager.cpp @@ -25,7 +25,7 @@ namespace arith { InferenceManager::InferenceManager(TheoryArith& ta, ArithState& astate, ProofNodeManager* pnm) - : InferenceManagerBuffered(ta, astate, pnm) + : InferenceManagerBuffered(ta, astate, pnm, "theory::arith") { } diff --git a/src/theory/arrays/inference_manager.cpp b/src/theory/arrays/inference_manager.cpp index afcc9a719..a4b8ecd44 100644 --- a/src/theory/arrays/inference_manager.cpp +++ b/src/theory/arrays/inference_manager.cpp @@ -27,10 +27,9 @@ namespace arrays { InferenceManager::InferenceManager(Theory& t, TheoryState& state, ProofNodeManager* pnm) - : TheoryInferenceManager(t, state, pnm), - d_lemmaPg(pnm ? new EagerProofGenerator(pnm, - state.getUserContext(), - "ArrayLemmaProofGenerator") + : TheoryInferenceManager(t, state, pnm, "theory::arrays"), + d_lemmaPg(pnm ? new EagerProofGenerator( + pnm, state.getUserContext(), "ArrayLemmaProofGenerator") : nullptr) { } diff --git a/src/theory/bags/inference_manager.cpp b/src/theory/bags/inference_manager.cpp index 0ccd06922..827be4c7f 100644 --- a/src/theory/bags/inference_manager.cpp +++ b/src/theory/bags/inference_manager.cpp @@ -24,7 +24,7 @@ namespace bags { InferenceManager::InferenceManager(Theory& t, SolverState& s, ProofNodeManager* pnm) - : InferenceManagerBuffered(t, s, pnm), d_state(s) + : InferenceManagerBuffered(t, s, pnm, "theory::bags"), d_state(s) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index f6e056f42..55a0ff46b 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -39,7 +39,7 @@ TheoryBV::TheoryBV(context::Context* c, d_ufRemByZero(), d_rewriter(), d_state(c, u, valuation), - d_im(*this, d_state, nullptr), + d_im(*this, d_state, nullptr, "theory::bv"), d_notify(d_im) { switch (options::bvSolver()) diff --git a/src/theory/datatypes/inference_manager.cpp b/src/theory/datatypes/inference_manager.cpp index 496881a33..b4a536b14 100644 --- a/src/theory/datatypes/inference_manager.cpp +++ b/src/theory/datatypes/inference_manager.cpp @@ -28,7 +28,7 @@ namespace datatypes { InferenceManager::InferenceManager(Theory& t, TheoryState& state, ProofNodeManager* pnm) - : InferenceManagerBuffered(t, state, pnm), + : InferenceManagerBuffered(t, state, pnm, "theory::datatypes"), d_inferenceLemmas("theory::datatypes::inferenceLemmas"), d_inferenceFacts("theory::datatypes::inferenceFacts"), d_inferenceConflicts("theory::datatypes::inferenceConflicts"), @@ -38,7 +38,7 @@ InferenceManager::InferenceManager(Theory& t, d_lemPg(pnm == nullptr ? nullptr : new EagerProofGenerator( - pnm, state.getUserContext(), "datatypes::lemPg")) + pnm, state.getUserContext(), "datatypes::lemPg")) { d_false = NodeManager::currentNM()->mkConst(false); smtStatisticsRegistry()->registerStat(&d_inferenceLemmas); diff --git a/src/theory/inference_manager_buffered.cpp b/src/theory/inference_manager_buffered.cpp index 6789043b1..f4ede969a 100644 --- a/src/theory/inference_manager_buffered.cpp +++ b/src/theory/inference_manager_buffered.cpp @@ -24,8 +24,10 @@ namespace theory { InferenceManagerBuffered::InferenceManagerBuffered(Theory& t, TheoryState& state, - ProofNodeManager* pnm) - : TheoryInferenceManager(t, state, pnm), d_processingPendingLemmas(false) + ProofNodeManager* pnm, + const std::string& name) + : TheoryInferenceManager(t, state, pnm, name), + d_processingPendingLemmas(false) { } diff --git a/src/theory/inference_manager_buffered.h b/src/theory/inference_manager_buffered.h index f9cddadd3..d12bd40b3 100644 --- a/src/theory/inference_manager_buffered.h +++ b/src/theory/inference_manager_buffered.h @@ -34,7 +34,8 @@ class InferenceManagerBuffered : public TheoryInferenceManager public: InferenceManagerBuffered(Theory& t, TheoryState& state, - ProofNodeManager* pnm); + ProofNodeManager* pnm, + const std::string& name); virtual ~InferenceManagerBuffered() {} /** * Do we have a pending fact or lemma? diff --git a/src/theory/quantifiers/quantifiers_inference_manager.cpp b/src/theory/quantifiers/quantifiers_inference_manager.cpp index 652c42839..faecb7c91 100644 --- a/src/theory/quantifiers/quantifiers_inference_manager.cpp +++ b/src/theory/quantifiers/quantifiers_inference_manager.cpp @@ -20,7 +20,7 @@ namespace quantifiers { QuantifiersInferenceManager::QuantifiersInferenceManager( Theory& t, QuantifiersState& state, ProofNodeManager* pnm) - : InferenceManagerBuffered(t, state, pnm) + : InferenceManagerBuffered(t, state, pnm, "theory::quantifiers") { } diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index db7fa2c6c..2a409a304 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -49,7 +49,7 @@ TheorySep::TheorySep(context::Context* c, d_lemmas_produced_c(u), d_bounds_init(false), d_state(c, u, valuation), - d_im(*this, d_state, nullptr), + d_im(*this, d_state, nullptr, "theory::sep"), d_notify(*this), d_reduce(u), d_spatial_assertions(c) diff --git a/src/theory/sets/inference_manager.cpp b/src/theory/sets/inference_manager.cpp index 161a66bfe..dd2b96703 100644 --- a/src/theory/sets/inference_manager.cpp +++ b/src/theory/sets/inference_manager.cpp @@ -26,7 +26,7 @@ namespace sets { InferenceManager::InferenceManager(Theory& t, SolverState& s, ProofNodeManager* pnm) - : InferenceManagerBuffered(t, s, pnm), d_state(s) + : InferenceManagerBuffered(t, s, pnm, "theory::sets"), d_state(s) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp index 8c487d7c1..717a34eea 100644 --- a/src/theory/strings/inference_manager.cpp +++ b/src/theory/strings/inference_manager.cpp @@ -34,7 +34,7 @@ InferenceManager::InferenceManager(Theory& t, ExtTheory& e, SequencesStatistics& statistics, ProofNodeManager* pnm) - : InferenceManagerBuffered(t, s, pnm), + : InferenceManagerBuffered(t, s, pnm, "theory::strings"), d_state(s), d_termReg(tr), d_extt(e), diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp index a56d616d9..a1c1545bf 100644 --- a/src/theory/theory_inference_manager.cpp +++ b/src/theory/theory_inference_manager.cpp @@ -14,6 +14,7 @@ #include "theory/theory_inference_manager.h" +#include "smt/smt_statistics_registry.h" #include "theory/theory.h" #include "theory/uf/equality_engine.h" @@ -24,7 +25,8 @@ namespace theory { TheoryInferenceManager::TheoryInferenceManager(Theory& t, TheoryState& state, - ProofNodeManager* pnm) + ProofNodeManager* pnm, + const std::string& name) : d_theory(t), d_theoryState(state), d_out(t.getOutputChannel()), @@ -34,11 +36,24 @@ TheoryInferenceManager::TheoryInferenceManager(Theory& t, d_lemmasSent(t.getUserContext()), d_numConflicts(0), d_numCurrentLemmas(0), - d_numCurrentFacts(0) + d_numCurrentFacts(0), + d_conflictIdStats(name + "::inferencesConflict"), + d_factIdStats(name + "::inferencesFact"), + d_lemmaIdStats(name + "::inferencesLemma") { // don't add true lemma Node truen = NodeManager::currentNM()->mkConst(true); d_lemmasSent.insert(truen); + smtStatisticsRegistry()->registerStat(&d_conflictIdStats); + smtStatisticsRegistry()->registerStat(&d_factIdStats); + smtStatisticsRegistry()->registerStat(&d_lemmaIdStats); +} + +TheoryInferenceManager::~TheoryInferenceManager() +{ + smtStatisticsRegistry()->unregisterStat(&d_conflictIdStats); + smtStatisticsRegistry()->unregisterStat(&d_factIdStats); + smtStatisticsRegistry()->unregisterStat(&d_lemmaIdStats); } void TheoryInferenceManager::setEqualityEngine(eq::EqualityEngine* ee) @@ -89,6 +104,7 @@ void TheoryInferenceManager::conflict(TNode conf, InferenceId id) { if (!d_theoryState.isInConflict()) { + d_conflictIdStats << id; d_theoryState.notifyInConflict(); d_out.conflict(conf); ++d_numConflicts; @@ -99,6 +115,7 @@ void TheoryInferenceManager::trustedConflict(TrustNode tconf, InferenceId id) { if (!d_theoryState.isInConflict()) { + d_conflictIdStats << id; d_theoryState.notifyInConflict(); d_out.trustedConflict(tconf); } @@ -230,6 +247,7 @@ bool TheoryInferenceManager::trustedLemma(const TrustNode& tlem, return false; } } + d_lemmaIdStats << id; d_numCurrentLemmas++; d_out.trustedLemma(tlem, p); return true; @@ -318,6 +336,7 @@ bool TheoryInferenceManager::assertInternalFact(TNode atom, InferenceId id, TNode exp) { + d_factIdStats << id; return processInternalFact(atom, pol, PfRule::UNKNOWN, {exp}, {}, nullptr); } @@ -329,6 +348,7 @@ bool TheoryInferenceManager::assertInternalFact(TNode atom, const std::vector& args) { Assert(pfr != PfRule::UNKNOWN); + d_factIdStats << id; return processInternalFact(atom, pol, pfr, exp, args, nullptr); } @@ -339,6 +359,7 @@ bool TheoryInferenceManager::assertInternalFact(TNode atom, ProofGenerator* pg) { Assert(pg != nullptr); + d_factIdStats << id; return processInternalFact(atom, pol, PfRule::ASSUME, exp, {}, pg); } diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h index 7a125789b..0142f814a 100644 --- a/src/theory/theory_inference_manager.h +++ b/src/theory/theory_inference_manager.h @@ -70,8 +70,11 @@ class TheoryInferenceManager /** * Constructor, note that state should be the official state of theory t. */ - TheoryInferenceManager(Theory& t, TheoryState& state, ProofNodeManager* pnm); - virtual ~TheoryInferenceManager() {} + TheoryInferenceManager(Theory& t, + TheoryState& state, + ProofNodeManager* pnm, + const std::string& name); + virtual ~TheoryInferenceManager(); /** * Set equality engine, ee is a pointer to the official equality engine * of theory. @@ -432,6 +435,12 @@ class TheoryInferenceManager uint32_t d_numCurrentLemmas; /** The number of internal facts added since the last call to reset. */ uint32_t d_numCurrentFacts; + /** Statistics for conflicts sent via this inference manager. */ + IntegralHistogramStat d_conflictIdStats; + /** Statistics for facts sent via this inference manager. */ + IntegralHistogramStat d_factIdStats; + /** Statistics for lemmas sent via this inference manager. */ + IntegralHistogramStat d_lemmaIdStats; }; } // namespace theory diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 3ad94c571..0328080ee 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -51,7 +51,7 @@ TheoryUF::TheoryUF(context::Context* c, d_functionsTerms(c), d_symb(u, instanceName), d_state(c, u, valuation), - d_im(*this, d_state, pnm), + d_im(*this, d_state, pnm, "theory::uf"), d_notify(d_im, *this) { d_true = NodeManager::currentNM()->mkConst( true );