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);
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) {
}
void TheoryUFMorgan::check(Effort level) {
+ TimerStat::CodeTimer codeTimer(d_checkTimer);
+
Debug("uf") << "uf: begin check(" << level << ")" << std::endl;
while(!done()) {
}
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();
Node d_trueNode, d_falseNode, d_trueEqFalseNode;
- //context::CDList<Node> 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<AverageStat> d_ccExplanationLength;/*! CC module expl length */
+ WrappedStat<IntStat> d_ccNewSkolemVars;/*! CC module # skolem vars */
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.
#include "context/cdlist_context_memory.h"
#include "util/exception.h"
#include "theory/uf/morgan/stacking_map.h"
+#include "util/stats.h"
namespace CVC4 {
OutputChannel* d_out;
// typedef all of these so that iterators are easy to define
- typedef theory::uf::morgan::StackingMap <Node, NodeHashFunction> RepresentativeMap;
+ typedef theory::uf::morgan::StackingMap<Node, NodeHashFunction> RepresentativeMap;
typedef context::CDList<TNode, context::ContextMemoryAllocator<TNode> > ClassList;
typedef context::CDMap<Node, ClassList*, NodeHashFunction> ClassLists;
typedef context::CDList<TNode, context::ContextMemoryAllocator<TNode> > UseList;
typedef context::CDSet<Node, NodeHashFunction> 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)
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
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);
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 */
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);
}
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() */
AlwaysAssert(d_registeredStats.find(s) == d_registeredStats.end());
d_registeredStats.insert(s);
}
-}/* StatisticsRegistry::registerStat */
+}/* StatisticsRegistry::registerStat() */
inline void StatisticsRegistry::unregisterStat(Stat* s)
AlwaysAssert(d_registeredStats.find(s) != d_registeredStats.end());
d_registeredStats.erase(s);
}
-}/* StatisticsRegistry::unregisterStat */
-
+}/* StatisticsRegistry::unregisterStat() */
/**
* std::ostream& operator<<(std::ostream&, const T&);
*/
template <class T>
-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) {
ss << getData();
return ss.str();
}
-};/* class DataStat */
+};/* class DataStat<T> */
+
+
+template <class T>
+class DataStat : public ReadOnlyDataStat<T> {
+public:
+ DataStat(const std::string& s) :
+ ReadOnlyDataStat<T>(s) {
+ }
+
+ virtual void setData(const T&) = 0;
+
+};/* class DataStat<T> */
/** T must have an assignment operator=(). */
Unreachable();
}
}
-};/* class ReferenceStat */
+};/* class ReferenceStat<T> */
/** T must have an operator=() and a copy constructor. */
Unreachable();
}
}
-};/* class BackedStat */
+};/* class BackedStat<T> */
+
+
+/**
+ * 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 Stat>
+class WrappedStat : public ReadOnlyDataStat<typename Stat::payload_t> {
+ typedef typename Stat::payload_t T;
+
+ const ReadOnlyDataStat<T>& d_stat;
+
+ /** Private copy constructor undefined (no copy permitted). */
+ WrappedStat(const WrappedStat&) CVC4_UNDEFINED;
+ /** Private assignment operator undefined (no copy permitted). */
+ WrappedStat<T>& operator=(const WrappedStat&) CVC4_UNDEFINED;
+
+public:
+
+ WrappedStat(const std::string& s, const ReadOnlyDataStat<T>& stat) :
+ ReadOnlyDataStat<T>(s),
+ d_stat(stat) {
+ }
+
+ const T& getData() const {
+ if(__CVC4_USE_STATISTICS) {
+ return d_stat.getData();
+ } else {
+ Unreachable();
+ }
+ }
+};/* class WrappedStat<T> */
class IntStat : public BackedStat<int64_t> {
}
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 */
}
+/**
+ * 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;
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) {
projects / cvc5.git / commitdiff