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.

1 files changed, 9 insertions, 0 deletions

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:
 
   /**