From 21102d14767364c222f1e7fe13de1f229d541dbc Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 17 Nov 2010 02:45:13 +0000 Subject: [PATCH] add some stats to UF/CC --- src/theory/uf/morgan/theory_uf_morgan.cpp | 32 ++++++- src/theory/uf/morgan/theory_uf_morgan.h | 9 +- src/util/congruence_closure.h | 43 ++++++++- src/util/stats.h | 107 +++++++++++++++++++--- 4 files changed, 172 insertions(+), 19 deletions(-) diff --git a/src/theory/uf/morgan/theory_uf_morgan.cpp b/src/theory/uf/morgan/theory_uf_morgan.cpp index cc0296d0a..ad8929692 100644 --- a/src/theory/uf/morgan/theory_uf_morgan.cpp +++ b/src/theory/uf/morgan/theory_uf_morgan.cpp @@ -37,7 +37,19 @@ TheoryUFMorgan::TheoryUFMorgan(int id, Context* ctxt, OutputChannel& out) : d_conflict(), d_trueNode(), d_falseNode(), - d_trueEqFalseNode() { + d_trueEqFalseNode(), + d_checkTimer("theory::uf::morgan::checkTime"), + d_propagateTimer("theory::uf::morgan::propagateTime"), + d_explainTimer("theory::uf::morgan::explainTime"), + d_ccExplanationLength("theory::uf::morgan::cc::averageExplanationLength", d_cc.getExplanationLength()), + d_ccNewSkolemVars("theory::uf::morgan::cc::newSkolemVariables", d_cc.getNewSkolemVars()) { + + StatisticsRegistry::registerStat(&d_checkTimer); + StatisticsRegistry::registerStat(&d_propagateTimer); + StatisticsRegistry::registerStat(&d_explainTimer); + StatisticsRegistry::registerStat(&d_ccExplanationLength); + StatisticsRegistry::registerStat(&d_ccNewSkolemVars); + NodeManager* nm = NodeManager::currentNM(); TypeNode boolType = nm->booleanType(); d_trueNode = nm->mkVar("TRUE_UF", boolType); @@ -52,6 +64,12 @@ TheoryUFMorgan::~TheoryUFMorgan() { d_trueNode = Node::null(); d_falseNode = Node::null(); d_trueEqFalseNode = Node::null(); + + StatisticsRegistry::unregisterStat(&d_checkTimer); + StatisticsRegistry::unregisterStat(&d_propagateTimer); + StatisticsRegistry::unregisterStat(&d_explainTimer); + StatisticsRegistry::unregisterStat(&d_ccExplanationLength); + StatisticsRegistry::unregisterStat(&d_ccNewSkolemVars); } RewriteResponse TheoryUFMorgan::postRewrite(TNode n, bool topLevel) { @@ -269,6 +287,8 @@ void TheoryUFMorgan::addDisequality(TNode eq) { } void TheoryUFMorgan::check(Effort level) { + TimerStat::CodeTimer codeTimer(d_checkTimer); + Debug("uf") << "uf: begin check(" << level << ")" << std::endl; while(!done()) { @@ -429,10 +449,20 @@ void TheoryUFMorgan::check(Effort level) { } void TheoryUFMorgan::propagate(Effort level) { + TimerStat::CodeTimer codeTimer(d_propagateTimer); + Debug("uf") << "uf: begin propagate(" << level << ")" << std::endl; Debug("uf") << "uf: end propagate(" << level << ")" << std::endl; } +void TheoryUFMorgan::explain(TNode n, Effort level) { + TimerStat::CodeTimer codeTimer(d_explainTimer); + + Debug("uf") << "uf: begin explain([" << n << "], " << level << ")" << std::endl; + Unimplemented(); + Debug("uf") << "uf: end explain([" << n << "], " << level << ")" << std::endl; +} + Node TheoryUFMorgan::getValue(TNode n, TheoryEngine* engine) { NodeManager* nodeManager = NodeManager::currentNM(); diff --git a/src/theory/uf/morgan/theory_uf_morgan.h b/src/theory/uf/morgan/theory_uf_morgan.h index d26e6ff8f..49b6a77ae 100644 --- a/src/theory/uf/morgan/theory_uf_morgan.h +++ b/src/theory/uf/morgan/theory_uf_morgan.h @@ -91,7 +91,12 @@ private: Node d_trueNode, d_falseNode, d_trueEqFalseNode; - //context::CDList d_activeAssertions; + // === STATISTICS === + TimerStat d_checkTimer;/*! time spent in check() */ + TimerStat d_propagateTimer;/*! time spent in propagate() */ + TimerStat d_explainTimer;/*! time spent in explain() */ + WrappedStat d_ccExplanationLength;/*! CC module expl length */ + WrappedStat d_ccNewSkolemVars;/*! CC module # skolem vars */ public: @@ -158,7 +163,7 @@ public: * Overloads void explain(TNode n, Effort level); from theory.h. * See theory/theory.h for more information about this method. */ - void explain(TNode n, Effort level) {} + void explain(TNode n, Effort level); /** * Gets a theory value. diff --git a/src/util/congruence_closure.h b/src/util/congruence_closure.h index 90ab11f9f..094fb1d03 100644 --- a/src/util/congruence_closure.h +++ b/src/util/congruence_closure.h @@ -35,6 +35,7 @@ #include "context/cdlist_context_memory.h" #include "util/exception.h" #include "theory/uf/morgan/stacking_map.h" +#include "util/stats.h" namespace CVC4 { @@ -104,7 +105,7 @@ class CongruenceClosure { OutputChannel* d_out; // typedef all of these so that iterators are easy to define - typedef theory::uf::morgan::StackingMap RepresentativeMap; + typedef theory::uf::morgan::StackingMap RepresentativeMap; typedef context::CDList > ClassList; typedef context::CDMap ClassLists; typedef context::CDList > UseList; @@ -142,6 +143,10 @@ class CongruenceClosure { typedef context::CDSet CareSet; CareSet d_careSet; + // === STATISTICS === + AverageStat d_explanationLength;/*! average explanation length */ + IntStat d_newSkolemVars;/*! new vars created */ + public: /** Construct a congruence closure module instance */ CongruenceClosure(context::Context* ctxt, OutputChannel* out) @@ -156,9 +161,13 @@ public: d_proof(ctxt), d_proofLabel(ctxt), d_proofRewrite(ctxt), - d_careSet(ctxt) { + d_careSet(ctxt), + d_explanationLength("congruence_closure::AverageExplanationLength"), + d_newSkolemVars("congruence_closure::NewSkolemVariables", 0) { } + ~CongruenceClosure() {} + /** * Add a term into CC consideration. This is context-dependent. * Calls OutputChannel::notifyCongruent(), so it can throw anything @@ -206,6 +215,7 @@ public: if(t.getKind() == kind::APPLY_UF) { EqMap::iterator i = d_eqMap.find(t); if(i == d_eqMap.end()) { + ++d_newSkolemVars; Node v = NodeManager::currentNM()->mkSkolem(t.getType()); addEq(NodeManager::currentNM()->mkNode(t.getType().isBoolean() ? kind::IFF : kind::EQUAL, t, v), TNode::null()); d_eqMap.insert(t, v); @@ -375,6 +385,30 @@ private: void merge(TNode ec1, TNode ec2); void mergeProof(TNode a, TNode b, TNode e); +public: + + // === STATISTICS ACCESSORS === + + /** + * Get access to the explanation-length statistic. Returns the + * statistic itself so that reference-statistics can be wrapped + * around it, useful since CongruenceClosure is a client class and + * shouldn't be directly registered with the StatisticsRegistry. + */ + const AverageStat& getExplanationLength() const throw() { + return d_explanationLength; + } + + /** + * Get access to the new-skolem-vars statistic. Returns the + * statistic itself so that reference-statistics can be wrapped + * around it, useful since CongruenceClosure is a client class and + * shouldn't be directly registered with the StatisticsRegistry. + */ + const IntStat& getNewSkolemVars() const throw() { + return d_newSkolemVars; + } + };/* class CongruenceClosure */ @@ -468,7 +502,8 @@ Node CongruenceClosure::buildRepresentativesOfApply(TNode apply, Assert(apply.getKind() == kind::APPLY_UF); NodeBuilder<> argspb(kindToBuild); // FIXME probably don't have to do find() of operator - argspb << find(apply.getOperator()); + Assert(find(apply.getOperator()) == apply.getOperator()); + argspb << apply.getOperator(); for(TNode::iterator i = apply.begin(); i != apply.end(); ++i) { argspb << find(*i); } @@ -922,8 +957,10 @@ Node CongruenceClosure::explain(Node a, Node b) Assert(pf.getNumChildren() > 0); if(pf.getNumChildren() == 1) { + d_explanationLength.addEntry(1.0); return pf[0]; } else { + d_explanationLength.addEntry(double(pf.getNumChildren())); return pf; } }/* explain() */ diff --git a/src/util/stats.h b/src/util/stats.h index 02b642939..c0660bf88 100644 --- a/src/util/stats.h +++ b/src/util/stats.h @@ -113,7 +113,7 @@ inline void StatisticsRegistry::registerStat(Stat* s) AlwaysAssert(d_registeredStats.find(s) == d_registeredStats.end()); d_registeredStats.insert(s); } -}/* StatisticsRegistry::registerStat */ +}/* StatisticsRegistry::registerStat() */ inline void StatisticsRegistry::unregisterStat(Stat* s) @@ -122,8 +122,7 @@ inline void StatisticsRegistry::unregisterStat(Stat* s) AlwaysAssert(d_registeredStats.find(s) != d_registeredStats.end()); d_registeredStats.erase(s); } -}/* StatisticsRegistry::unregisterStat */ - +}/* StatisticsRegistry::unregisterStat() */ /** @@ -131,14 +130,15 @@ inline void StatisticsRegistry::unregisterStat(Stat* s) * std::ostream& operator<<(std::ostream&, const T&); */ template -class DataStat : public Stat { +class ReadOnlyDataStat : public Stat { public: - DataStat(const std::string& s) : + typedef T payload_t; + + ReadOnlyDataStat(const std::string& s) : Stat(s) { } virtual const T& getData() const = 0; - virtual void setData(const T&) = 0; void flushInformation(std::ostream& out) const { if(__CVC4_USE_STATISTICS) { @@ -151,7 +151,19 @@ public: ss << getData(); return ss.str(); } -};/* class DataStat */ +};/* class DataStat */ + + +template +class DataStat : public ReadOnlyDataStat { +public: + DataStat(const std::string& s) : + ReadOnlyDataStat(s) { + } + + virtual void setData(const T&) = 0; + +};/* class DataStat */ /** T must have an assignment operator=(). */ @@ -185,7 +197,7 @@ public: Unreachable(); } } -};/* class ReferenceStat */ +};/* class ReferenceStat */ /** T must have an operator=() and a copy constructor. */ @@ -221,7 +233,47 @@ public: Unreachable(); } } -};/* class BackedStat */ +};/* class BackedStat */ + + +/** + * A wrapper Stat for another Stat. + * + * This type of Stat is useful in cases where a module (like the + * CongruenceClosure module) might keep its own statistics, but might + * be instantiated in many contexts by many clients. This makes such + * a statistic inappopriate to register with the StatisticsRegistry + * directly, as all would be output with the same name (and may be + * unregistered too quickly anyway). A WrappedStat allows the calling + * client (say, TheoryUF) to wrap the Stat from the client module, + * giving it a globally unique name. + */ +template +class WrappedStat : public ReadOnlyDataStat { + typedef typename Stat::payload_t T; + + const ReadOnlyDataStat& d_stat; + + /** Private copy constructor undefined (no copy permitted). */ + WrappedStat(const WrappedStat&) CVC4_UNDEFINED; + /** Private assignment operator undefined (no copy permitted). */ + WrappedStat& operator=(const WrappedStat&) CVC4_UNDEFINED; + +public: + + WrappedStat(const std::string& s, const ReadOnlyDataStat& stat) : + ReadOnlyDataStat(s), + d_stat(stat) { + } + + const T& getData() const { + if(__CVC4_USE_STATISTICS) { + return d_stat.getData(); + } else { + Unreachable(); + } + } +};/* class WrappedStat */ class IntStat : public BackedStat { @@ -280,10 +332,12 @@ public: } void addEntry(double e){ - double oldSum = n*getData(); - ++n; - double newSum = oldSum + e; - setData(newSum / n); + if(__CVC4_USE_STATISTICS) { + double oldSum = n*getData(); + ++n; + double newSum = oldSum + e; + setData(newSum / n); + } } };/* class AverageStat */ @@ -363,6 +417,11 @@ inline std::ostream& operator<<(std::ostream& os, const ::timespec& t) { } +/** + * A timer statistic. The timer can be started and stopped + * arbitrarily, like a stopwatch; the value of the statistic at the + * end is the accummulated time. + */ class TimerStat : public BackedStat< ::timespec > { // strange: timespec isn't placed in 'std' namespace ?! ::timespec d_start; @@ -370,6 +429,28 @@ class TimerStat : public BackedStat< ::timespec > { public: + /** + * Utility class to make it easier to call stop() at the end of a + * code block. When constructed, it starts the timer. When + * destructed, it stops the timer. + */ + class CodeTimer { + TimerStat& d_timer; + + /** Private copy constructor undefined (no copy permitted). */ + CodeTimer(const CodeTimer& timer) CVC4_UNDEFINED; + /** Private assignment operator undefined (no copy permitted). */ + CodeTimer& operator=(const CodeTimer& timer) CVC4_UNDEFINED; + + public: + CodeTimer(TimerStat& timer) : d_timer(timer) { + d_timer.start(); + } + ~CodeTimer() { + d_timer.stop(); + } + };/* class TimerStat::CodeTimer */ + TimerStat(const std::string& s) : BackedStat< ::timespec >(s, ::timespec()), d_running(false) { -- 2.30.2