From c85ad30f2a291818a27a220833d219c1cbbb2a51 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 2 May 2011 05:31:00 +0000 Subject: [PATCH] fix a performance issue from last commit --- src/smt/smt_engine.cpp | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) 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 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; -- 2.30.2