Merge from my post-smtcomp branch. Includes:

Dumping infrastructure.  Can dump preprocessed queries and clauses.  Can
also dump queries (for testing with another solver) to see if any conflicts
are missed, T-propagations are missed, all lemmas are T-valid, etc.  For a
full list of options see --dump=help.

CUDD building much cleaner.

Documentation and assertion fixes.

Printer improvements, printing of commands in language-defined way, etc.

Typechecker stuff in expr package now autogenerated, no need to manually
edit the expr package when adding a new theory.

CVC3 compatibility layer (builds as libcompat).

SWIG detection and language binding support (infrastructure).

Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode
(when not in compliance mode).

Copyright and file headers regenerated.

1 files changed, 28 insertions, 3 deletions

diff --git a/src/util/stats.cpp b/src/util/stats.cpp
index 70d486ff6..474d8fa7a 100644
--- a/src/util/stats.cpp
+++ b/src/util/stats.cpp
@@ -2,10 +2,10 @@
 /*! \file stats.cpp
  ** \verbatim
  ** Original author: taking
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -20,6 +20,13 @@
 #include "util/stats.h"
 #include "expr/node_manager.h"
 #include "expr/expr_manager_scope.h"
+#include "lib/clock_gettime.h"
+
+#ifdef CVC4_STATISTICS_ON
+#  define __CVC4_USE_STATISTICS true
+#else
+#  define __CVC4_USE_STATISTICS false
+#endif
 
 using namespace CVC4;
 
@@ -67,6 +74,24 @@ StatisticsRegistry::const_iterator StatisticsRegistry::end() {
   return NodeManager::currentNM()->getStatisticsRegistry()->d_registeredStats.end();
 }/* StatisticsRegistry::end() */
 
+void TimerStat::start() {
+  if(__CVC4_USE_STATISTICS) {
+    AlwaysAssert(!d_running);
+    clock_gettime(CLOCK_MONOTONIC, &d_start);
+    d_running = true;
+  }
+}/* TimerStat::start() */
+
+void TimerStat::stop() {
+  if(__CVC4_USE_STATISTICS) {
+    AlwaysAssert(d_running);
+    ::timespec end;
+    clock_gettime(CLOCK_MONOTONIC, &end);
+    d_data += end - d_start;
+    d_running = false;
+  }
+}/* TimerStat::stop() */
+
 RegisterStatistic::RegisterStatistic(ExprManager& em, Stat* stat) :
     d_em(&em), d_stat(stat) {
   ExprManagerScope ems(*d_em);