add some stats to UF/CC

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<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:
 
@@ -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 <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() */
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 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) {
@@ -151,7 +151,19 @@ public:
     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=(). */
@@ -185,7 +197,7 @@ public:
       Unreachable();
     }
   }
-};/* class ReferenceStat */
+};/* class ReferenceStat<T> */
 
 
 /** T must have an operator=() and a copy constructor. */
@@ -221,7 +233,47 @@ public:
       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> {
@@ -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) {