diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-11-17 02:45:13 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-11-17 02:45:13 +0000 |
commit | 21102d14767364c222f1e7fe13de1f229d541dbc (patch) | |
tree | 2c5d96ac0576086076766a1b0d55c2f7a95823f9 /src/util/congruence_closure.h | |
parent | c7a70635797fe4205b27d29546dd4fe763220794 (diff) |
add some stats to UF/CC
Diffstat (limited to 'src/util/congruence_closure.h')
-rw-r--r-- | src/util/congruence_closure.h | 43 |
1 files changed, 40 insertions, 3 deletions
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 <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; @@ -142,6 +143,10 @@ class CongruenceClosure { 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) @@ -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<OutputChannel>::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<OutputChannel>::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() */ |