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.

2 files changed, 17 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);
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index b872985fb..408db1a2f 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -35,6 +35,7 @@
 #include "util/options.h"
 #include "util/result.h"
 #include "util/sexpr.h"
+#include "util/stats.h"
 
 // In terms of abstraction, this is below (and provides services to)
 // ValidityChecker and above (and requires the services of)
@@ -179,6 +180,14 @@ class CVC4_PUBLIC SmtEngine {
 
   friend class ::CVC4::smt::SmtEnginePrivate;
 
+  // === STATISTICS ===
+  /** time spent in definition-expansion */
+  TimerStat d_definitionExpansionTime;
+  /** time spent in non-clausal simplification */
+  TimerStat d_nonclausalSimplificationTime;
+  /** time spent in static learning */
+  TimerStat d_staticLearningTime;
+
 public:
 
   /**