fix a performance issue from last commit

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 60346ab2e99cacb37675c50858c9c334195dbea7..b01260815d15546f8e787cc31c0b0b1cd535af1e 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -135,6 +135,10 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
 
   NodeManagerScope nms(d_nodeManager);
 
+  StatisticsRegistry::registerStat(&d_definitionExpansionTime);
+  StatisticsRegistry::registerStat(&d_nonclausalSimplificationTime);
+  StatisticsRegistry::registerStat(&d_staticLearningTime);
+
   // We have mutual dependancy here, so we add the prop engine to the theory
   // engine later (it is non-essential there)
   d_theoryEngine = new TheoryEngine(d_context);
@@ -192,6 +196,10 @@ SmtEngine::~SmtEngine() {
 
   d_definedFunctions->deleteSelf();
 
+  StatisticsRegistry::unregisterStat(&d_definitionExpansionTime);
+  StatisticsRegistry::unregisterStat(&d_nonclausalSimplificationTime);
+  StatisticsRegistry::unregisterStat(&d_staticLearningTime);
+
   delete d_userContext;
 
   delete d_theoryEngine;
@@ -452,7 +460,7 @@ Node SmtEnginePrivate::preprocess(SmtEngine& smt, TNode in)
     Node n;
     if(!Options::current()->lazyDefinitionExpansion) {
       TimerStat::CodeTimer codeTimer(smt.d_definitionExpansionTime);
-      Chat() << "Expanding definitions: " << in << endl;
+      //Chat() << "Expanding definitions: " << in << endl;
       Debug("expand") << "have: " << n << endl;
       hash_map<TNode, Node, TNodeHashFunction> cache;
       n = expandDefinitions(smt, in, cache);
@@ -464,7 +472,7 @@ Node SmtEnginePrivate::preprocess(SmtEngine& smt, TNode in)
     // For now, don't re-statically-learn from learned facts; this could
     // be useful though (e.g., theory T1 could learn something further
     // from something learned previously by T2).
-    Chat() << "Performing static learning: " << n << endl;
+    //Chat() << "Performing static learning: " << n << endl;
     TimerStat::CodeTimer codeTimer(smt.d_staticLearningTime);
     NodeBuilder<> learned(kind::AND);
     learned << n;