From: Morgan Deters <mdeters@gmail.com>
Date: Mon, 2 May 2011 05:31:00 +0000 (+0000)
Subject: fix a performance issue from last commit
X-Git-Tag: cvc5-1.0.0~8568
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c85ad30f2a291818a27a220833d219c1cbbb2a51;p=cvc5.git

fix a performance issue from last commit
---

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 60346ab2e..b01260815 100644
--- 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;