diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-05-02 05:04:36 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-05-02 05:04:36 +0000 |
commit | 99c42d62491307279403059690fa31be1fb3af63 (patch) | |
tree | 8f8a40a893e1a59e28015201f907e2cecede3294 /src/smt/smt_engine.cpp | |
parent | bf837ea666980a0556d7881316f34be7ad1e2ea2 (diff) |
Minor fixes to various parts of CVC4, including the removal of the uintptr_t constructors for Type and Expr (which existed due to ANTLR limitations). These issues are now handled (as a hack, due to said limitations) in the parser rather than the CVC4 core.
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 45c697d0b..60346ab2e 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -128,7 +128,10 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) : d_context(em->getContext()), d_userContext(new Context()), d_exprManager(em), - d_nodeManager(d_exprManager->getNodeManager()) { + d_nodeManager(d_exprManager->getNodeManager()), + d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"), + d_nonclausalSimplificationTime("smt::SmtEngine::nonclausalSimplificationTime"), + d_staticLearningTime("smt::SmtEngine::staticLearningTime") { NodeManagerScope nms(d_nodeManager); @@ -448,6 +451,8 @@ Node SmtEnginePrivate::preprocess(SmtEngine& smt, TNode in) try { Node n; if(!Options::current()->lazyDefinitionExpansion) { + TimerStat::CodeTimer codeTimer(smt.d_definitionExpansionTime); + Chat() << "Expanding definitions: " << in << endl; Debug("expand") << "have: " << n << endl; hash_map<TNode, Node, TNodeHashFunction> cache; n = expandDefinitions(smt, in, cache); @@ -459,6 +464,8 @@ 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; + TimerStat::CodeTimer codeTimer(smt.d_staticLearningTime); NodeBuilder<> learned(kind::AND); learned << n; smt.d_theoryEngine->staticLearning(n, learned); |