diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 12 |
1 files 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<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; |