support for SMT-LIBv2 :named attributes, and attributes in general; zero-ary define-fun; several set-info, set-option, get-option, get-info improvementss

12 files changed, 278 insertions, 109 deletions

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 8c90f337e..15fea22da 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -352,7 +352,9 @@ GetInfoCommand::GetInfoCommand(std::string flag) :
 
 void GetInfoCommand::invoke(SmtEngine* smtEngine) {
   try {
-    d_result = smtEngine->getInfo(d_flag).getValue();
+    stringstream ss;
+    ss << smtEngine->getInfo(d_flag);
+    d_result = ss.str();
   } catch(BadOptionException& bo) {
     d_result = "unsupported";
   }
diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind
index c4968af26..351893feb 100755
--- a/src/expr/mkmetakind
+++ b/src/expr/mkmetakind
@@ -195,9 +195,9 @@ struct ConstantMapReverse< ::CVC4::kind::$1 > {
 }
 
 function registerOperatorToKind {
-	operatorKind=$1
-	applyKind=$2
-	metakind_operatorKinds="${metakind_operatorKinds}    case kind::$applyKind: return kind::$operatorKind;
+  operatorKind=$1
+  applyKind=$2
+  metakind_operatorKinds="${metakind_operatorKinds}    case kind::$applyKind: return kind::$operatorKind;
 ";
 }
 
@@ -227,8 +227,14 @@ function register_metakind {
     exit 1
   fi
 
-  if [ $mk = OPERATOR ] || [ $mk = PARAMETERIZED -a "$k" != SORT_TYPE ]; then
-    if [ $lb = 0 ]; then
+  if [ $mk = OPERATOR -o $mk = PARAMETERIZED ]; then
+    if [ $mk = PARAMETERIZED -a "$k" = SORT_TYPE ]; then
+      # exception: zero-ary SORT_TYPE is permitted for sort constructors
+      :
+    elif [ $mk = PARAMETERIZED -a "$k" = APPLY ]; then
+      # exception: zero-ary APPLY is permitted for defined zero-ary functions
+      :
+    elif [ $lb = 0 ]; then
       echo "$kf:$lineno: error in range \`$nc' for \`$k': $mk-kinded kinds must always take at least one child" >&2
       exit 1
     fi
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 297a2d804..09e65526d 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -103,7 +103,9 @@ bool Parser::isFunction(const std::string& name) {
 
 /* Returns true if name is bound to a defined function. */
 bool Parser::isDefinedFunction(const std::string& name) {
-  return isFunction(name) && d_declScope.isBoundDefinedFunction(name);
+  // more permissive in type than isFunction(), because defined
+  // functions can be zero-ary and declared functions cannot.
+  return d_declScope.isBoundDefinedFunction(name);
 }
 
 /* Returns true if name is bound to a function returning boolean. */
@@ -286,50 +288,42 @@ void Parser::addOperator(Kind kind) {
   d_logicOperators.insert(kind);
 }
 
+void Parser::preemptCommand(Command* cmd) {
+  d_commandQueue.push_back(cmd);
+}
+
 Command* Parser::nextCommand() throw(ParserException) {
   Debug("parser") << "nextCommand()" << std::endl;
   Command* cmd = NULL;
-  if(!done()) {
-    try {
-      cmd = d_input->parseCommand();
-      if(cmd == NULL) {
-        setDone();
-      }
-    } catch(ParserException& e) {
+  if(!d_commandQueue.empty()) {
+    cmd = d_commandQueue.front();
+    d_commandQueue.pop_front();
+    if(cmd == NULL) {
       setDone();
-      throw;
-    } catch(Exception& e) {
-      setDone();
-      stringstream ss;
-      ss << e;
-      parseError( ss.str() );
     }
-  }
-  Debug("parser") << "nextCommand() => " << cmd << std::endl;
-  return cmd;
-}
-
-Expr Parser::nextExpression() throw(ParserException) {
-  Debug("parser") << "nextExpression()" << std::endl;
-  Expr result;
-  if(!done()) {
-    try {
-      result = d_input->parseExpr();
-      if(result.isNull()) {
+  } else {
+    if(!done()) {
+      try {
+        cmd = d_input->parseCommand();
+        d_commandQueue.push_back(cmd);
+        cmd = d_commandQueue.front();
+        d_commandQueue.pop_front();
+        if(cmd == NULL) {
+          setDone();
+        }
+      } catch(ParserException& e) {
         setDone();
+        throw;
+      } catch(Exception& e) {
+        setDone();
+        stringstream ss;
+        ss << e;
+        parseError( ss.str() );
       }
-    } catch(ParserException& e) {
-      setDone();
-      throw;
-    } catch(Exception& e) {
-      setDone();
-      stringstream ss;
-      ss << e;
-      parseError( ss.str() );
     }
   }
-  Debug("parser") << "nextExpression() => " << result << std::endl;
-  return result;
+  Debug("parser") << "nextCommand() => " << cmd << std::endl;
+  return cmd;
 }
 
 
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 1c492c843..bc0142089 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -23,6 +23,7 @@
 
 #include <string>
 #include <set>
+#include <list>
 
 #include "input.h"
 #include "parser_exception.h"
@@ -124,6 +125,13 @@ class CVC4_PUBLIC Parser {
   /** The set of operators available in the current logic. */
   std::set<Kind> d_logicOperators;
 
+  /**
+   * "Preemption commands": extra commands implied by subterms that
+   * should be issued before the currently-being-parsed command is
+   * issued.  Used to support SMT-LIBv2 ":named" attribute on terms.
+   */
+  std::list<Command*> d_commandQueue;
+
   /** Lookup a symbol in the given namespace. */
   Expr getSymbol(const std::string& var_name, SymbolType type);
 
@@ -315,12 +323,20 @@ public:
   const std::vector<Type>
   mkSorts(const std::vector<std::string>& names);
 
-  /** Add an operator to the current legal set.
+  /**
+   * Add an operator to the current legal set.
    *
    * @param kind the built-in operator to add
    */
   void addOperator(Kind kind);
 
+  /**
+   * Preempt the next returned command with other ones; used to
+   * support the :named attribute in SMT-LIBv2, which implicitly
+   * inserts a new command before the current one.
+   */
+  void preemptCommand(Command* cmd);
+
   /** Is the symbol bound to a boolean variable? */
   bool isBoolean(const std::string& name);
 
@@ -334,7 +350,6 @@ public:
   bool isPredicate(const std::string& name);
 
   Command* nextCommand() throw(ParserException);
-  Expr nextExpression() throw(ParserException);
 
   inline void parseError(const std::string& msg) throw (ParserException) {
     d_input->parseError(msg);
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 4c447f9c1..ddfd1804e 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -196,7 +196,7 @@ command returns [CVC4::Command* cmd]
     sortSymbol[t]
     { Debug("parser") << "declare fun: '" << name << "'" << std::endl;
       if( sorts.size() > 0 ) {
-        t = EXPR_MANAGER->mkFunctionType(sorts,t);
+        t = EXPR_MANAGER->mkFunctionType(sorts, t);
       }
       PARSER_STATE->mkVar(name, t);
       $cmd = new DeclarationCommand(name,t); }
@@ -215,7 +215,7 @@ command returns [CVC4::Command* cmd]
             ++i) {
           sorts.push_back((*i).second);
         }
-        t = EXPR_MANAGER->mkFunctionType(sorts,t);
+        t = EXPR_MANAGER->mkFunctionType(sorts, t);
       }
       PARSER_STATE->pushScope();
       for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
@@ -320,6 +320,7 @@ term[CVC4::Expr& expr]
   Kind kind;
   std::string name;
   std::vector<Expr> args;
+  SExpr sexpr;
 }
   : /* a built-in operator application */
     LPAREN_TOK builtinOp[kind] termList[args,expr] RPAREN_TOK
@@ -361,8 +362,9 @@ term[CVC4::Expr& expr]
         PARSER_STATE->getFunction(name) :
         PARSER_STATE->getVariable(name);
       args[0] = expr;
-      // TODO: check arity
-      expr = MK_EXPR(isDefinedFunction ? CVC4::kind::APPLY : CVC4::kind::APPLY_UF, args); }
+      expr = MK_EXPR(isDefinedFunction ?
+                     CVC4::kind::APPLY :
+                     CVC4::kind::APPLY_UF, args); }
 
   | /* a let binding */
     LPAREN_TOK LET_TOK LPAREN_TOK
@@ -374,9 +376,38 @@ term[CVC4::Expr& expr]
     RPAREN_TOK
     { PARSER_STATE->popScope(); }
 
-  | /* a variable */
-    symbol[name,CHECK_DECLARED,SYM_VARIABLE]
-    { expr = PARSER_STATE->getVariable(name); }
+    /* a variable */
+  | symbol[name,CHECK_DECLARED,SYM_VARIABLE]
+    { const bool isDefinedFunction =
+        PARSER_STATE->isDefinedFunction(name);
+      if(isDefinedFunction) {
+        expr = MK_EXPR(CVC4::kind::APPLY,
+                       PARSER_STATE->getFunction(name));
+      } else {
+        expr = PARSER_STATE->getVariable(name);
+      }
+    }
+
+    /* attributed expressions */
+  | LPAREN_TOK ATTRIBUTE_TOK term[expr] KEYWORD symbolicExpr[sexpr] RPAREN_TOK
+    { std::string attr = AntlrInput::tokenText($KEYWORD);
+      if(attr == ":named") {
+        name = sexpr.getValue();
+        // FIXME ensure expr is a closed subterm
+        // check that sexpr is a fresh function symbol
+        PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE);
+        // define it
+        Expr func = PARSER_STATE->mkFunction(name, expr.getType());
+        // bind name to expr with define-fun
+        Command* c =
+          new DefineFunctionCommand(func, std::vector<Expr>(), expr);
+        PARSER_STATE->preemptCommand(c);
+      } else {
+        std::stringstream ss;
+        ss << "Attribute `" << attr << "' not supported";
+        PARSER_STATE->parseError(ss.str());
+      }
+    }
 
     /* constants */
   | INTEGER_LITERAL
@@ -558,6 +589,7 @@ GET_ASSERTIONS_TOK : 'get-assertions';
 EXIT_TOK : 'exit';
 ITE_TOK : 'ite';
 LET_TOK : 'let';
+ATTRIBUTE_TOK : '!';
 LPAREN_TOK : '(';
 RPAREN_TOK : ')';
 SET_LOGIC_TOK : 'set-logic';
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 5de1cd0b1..edf49c7ac 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -31,6 +31,7 @@
 #include "util/output.h"
 #include "util/exception.h"
 #include "util/options.h"
+#include "util/configuration.h"
 #include "prop/prop_engine.h"
 #include "theory/theory_engine.h"
 
@@ -121,7 +122,7 @@ SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw() :
   d_propEngine(NULL),
   d_assertionList(NULL),
   d_haveAdditions(false),
-  d_lastResult() {
+  d_status() {
 
   NodeManagerScope nms(d_nodeManager);
 
@@ -166,7 +167,6 @@ void SmtEngine::setInfo(const string& key, const SExpr& value)
   throw(BadOptionException) {
   Debug("smt") << "SMT setInfo(" << key << ", " << value << ")" << endl;
   if(key == ":name" ||
-     key == ":status" ||
      key == ":source" ||
      key == ":category" ||
      key == ":difficulty" ||
@@ -174,15 +174,68 @@ void SmtEngine::setInfo(const string& key, const SExpr& value)
      key == ":notes") {
     // ignore these
     return;
+  } else if(key == ":status") {
+    string s;
+    if(value.isAtom()) {
+      s = value.getValue();
+    }
+    if(s != "sat" && s != "unsat" && s != "unknown") {
+      throw BadOptionException("argument to (set-info :status ..) must be "
+                               "`sat' or `unsat' or `unknown'");
+    }
+    if(s == "sat") {
+      d_status = Result::SAT;
+    } else if(s == "unsat") {
+      d_status = Result::UNSAT;
+    } else if(s == "unknown") {
+      d_status = Result::SAT_UNKNOWN;
+    } else {
+      Unreachable();
+    }
+    return;
   }
   throw BadOptionException();
 }
 
-const SExpr& SmtEngine::getInfo(const string& key) const
+SExpr SmtEngine::getInfo(const string& key) const
   throw(BadOptionException) {
   Debug("smt") << "SMT getInfo(" << key << ")" << endl;
-  // FIXME implement me
-  throw BadOptionException();
+  if(key == ":all-statistics") {
+    vector<SExpr> stats;
+    for(StatisticsRegistry::const_iterator i = StatisticsRegistry::begin();
+        i != StatisticsRegistry::end();
+        ++i) {
+      vector<SExpr> v;
+      v.push_back((*i)->getName());
+      v.push_back((*i)->getValue());
+      stats.push_back(v);
+    }
+    return stats;
+  } else if(key == ":error-behavior") {
+    return SExpr("immediate-exit");
+  } else if(key == ":name") {
+    return Configuration::getName();
+  } else if(key == ":version") {
+    return Configuration::getVersionString();
+  } else if(key == ":authors") {
+    return Configuration::about();
+  } else if(key == ":status") {
+    enum Result::SAT status = d_status.asSatisfiabilityResult().isSAT();
+    switch(status) {
+    case Result::SAT:
+      return SExpr("sat");
+    case Result::UNSAT:
+      return SExpr("unsat");
+    case Result::SAT_UNKNOWN:
+      return SExpr("unknown");
+    default:
+      Unhandled(status);
+    }
+  } else if(key == ":reason-unknown") {
+    throw BadOptionException();
+  } else {
+    throw BadOptionException();
+  }
 }
 
 void SmtEngine::setOption(const string& key, const SExpr& value)
@@ -192,11 +245,34 @@ void SmtEngine::setOption(const string& key, const SExpr& value)
   throw BadOptionException();
 }
 
-const SExpr& SmtEngine::getOption(const string& key) const
+SExpr SmtEngine::getOption(const string& key) const
   throw(BadOptionException) {
   Debug("smt") << "SMT getOption(" << key << ")" << endl;
-  // FIXME implement me
-  throw BadOptionException();
+  if(key == ":print-success") {
+    return SExpr("true");
+  } else if(key == ":expand-definitions") {
+    throw BadOptionException();
+  } else if(key == ":interactive-mode") {
+    throw BadOptionException();
+  } else if(key == ":produce-proofs") {
+    throw BadOptionException();
+  } else if(key == ":produce-unsat-cores") {
+    throw BadOptionException();
+  } else if(key == ":produce-models") {
+    throw BadOptionException();
+  } else if(key == ":produce-assignments") {
+    throw BadOptionException();
+  } else if(key == ":regular-output-channel") {
+    return SExpr("stdout");
+  } else if(key == ":diagnostic-output-channel") {
+    return SExpr("stderr");
+  } else if(key == ":random-seed") {
+    throw BadOptionException();
+  } else if(key == ":verbosity") {
+    throw BadOptionException();
+  } else {
+    throw BadOptionException();
+  }
 }
 
 void SmtEngine::defineFunction(Expr func,
@@ -205,12 +281,14 @@ void SmtEngine::defineFunction(Expr func,
   Debug("smt") << "SMT defineFunction(" << func << ")" << endl;
   NodeManagerScope nms(d_nodeManager);
   Type formulaType = formula.getType(true);// type check body
-  if(formulaType != FunctionType(func.getType()).getRangeType()) {
+  Type funcType = func.getType();
+  Type rangeType = funcType.isFunction() ?
+    FunctionType(funcType).getRangeType() : funcType;
+  if(formulaType != rangeType) {
     stringstream ss;
     ss << "Defined function's declared type does not match that of body\n"
        << "The function  : " << func << "\n"
-       << "Its range type: "
-       << FunctionType(func.getType()).getRangeType() << "\n"
+       << "Its range type: " << rangeType << "\n"
        << "The body      : " << formula << "\n"
        << "Body type     : " << formulaType;
     throw TypeCheckingException(func, ss.str());
@@ -225,7 +303,9 @@ void SmtEngine::defineFunction(Expr func,
   }
   TNode formulaNode = formula.getTNode();
   DefinedFunction def(funcNode, formalsNodes, formulaNode);
-  d_haveAdditions = true;
+  // Permit (check-sat) (define-fun ...) (get-value ...) sequences.
+  // Otherwise, (check-sat) (get-value ((! foo :named bar))) breaks
+  // d_haveAdditions = true;
   d_definedFunctions->insert(funcNode, def);
 }
 
@@ -335,7 +415,7 @@ Result SmtEngine::checkSat(const BoolExpr& e) {
   ensureBoolean(e);// ensure expr is type-checked at this point
   SmtEnginePrivate::addFormula(*this, e.getNode());
   Result r = check().asSatisfiabilityResult();
-  d_lastResult = r;
+  d_status = r;
   d_haveAdditions = false;
   Debug("smt") << "SMT checkSat(" << e << ") ==> " << r << endl;
   return r;
@@ -348,7 +428,7 @@ Result SmtEngine::query(const BoolExpr& e) {
   ensureBoolean(e);// ensure expr is type-checked at this point
   SmtEnginePrivate::addFormula(*this, e.getNode().notNode());
   Result r = check().asValidityResult();
-  d_lastResult = r;
+  d_status = r;
   d_haveAdditions = false;
   Debug("smt") << "SMT query(" << e << ") ==> " << r << endl;
   return r;
@@ -389,7 +469,7 @@ Expr SmtEngine::getValue(Expr e)
       "Cannot get value when produce-models options is off.";
     throw ModalException(msg);
   }
-  if(d_lastResult.asSatisfiabilityResult() != Result::SAT ||
+  if(d_status.asSatisfiabilityResult() != Result::SAT ||
      d_haveAdditions) {
     const char* msg =
       "Cannot get value unless immediately proceded by SAT/INVALID response.";
@@ -457,9 +537,8 @@ void SmtEngine::pop() {
   d_context->pop();
   Debug("userpushpop") << "SmtEngine: popped to level "
                        << d_context->getLevel() << endl;
-  // clear out last result: get-value/get-assignment no longer
-  // available here
-  d_lastResult = Result();
+  // FIXME: should we reset d_status here?
+  // SMT-LIBv2 spec seems to imply no, but it would make sense to..
 }
 
 }/* CVC4 namespace */
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index efa48e517..7272762d8 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -119,9 +119,9 @@ class CVC4_PUBLIC SmtEngine {
   bool d_haveAdditions;
 
   /**
-   * Result of last checkSat/query.
+   * Most recent result of last checkSat/query or (set-info :status).
    */
-  Result d_lastResult;
+  Result d_status;
 
   /**
    * This is called by the destructor, just before destroying the
@@ -173,7 +173,7 @@ public:
   /**
    * Query information about the SMT environment.
    */
-  const SExpr& getInfo(const std::string& key) const
+  SExpr getInfo(const std::string& key) const
     throw(BadOptionException);
 
   /**
@@ -185,7 +185,7 @@ public:
   /**
    * Get an aspect of the current SMT execution environment.
    */
-  const SExpr& getOption(const std::string& key) const
+  SExpr getOption(const std::string& key) const
     throw(BadOptionException);
 
   /**
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index 47ee8cbfc..ad442fc2f 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -119,7 +119,7 @@ constant BUILTIN \
     "The kind of nodes representing built-in operators"
 
 variable FUNCTION "function"
-parameterized APPLY FUNCTION 1: "defined function application"
+parameterized APPLY FUNCTION 0: "defined function application"
 
 operator EQUAL 2 "equality"
 operator DISTINCT 2: "disequality"
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index aee147eff..ec98e61d2 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -37,23 +37,29 @@ class ApplyTypeRule {
     throw (TypeCheckingExceptionPrivate) {
     TNode f = n.getOperator();
     TypeNode fType = f.getType(check);
-    if( !fType.isFunction() ) {
+    if( !fType.isFunction() && n.getNumChildren() > 0 ) {
       throw TypeCheckingExceptionPrivate(n, "operator does not have function type");
     }
     if( check ) {
-      if (n.getNumChildren() != fType.getNumChildren() - 1) {
-        throw TypeCheckingExceptionPrivate(n, "number of arguments does not match the function type");
-      }
-      TNode::iterator argument_it = n.begin();
-      TNode::iterator argument_it_end = n.end();
-      TypeNode::iterator argument_type_it = fType.begin();
-      for(; argument_it != argument_it_end; ++argument_it) {
-        if((*argument_it).getType() != *argument_type_it) {
-          throw TypeCheckingExceptionPrivate(n, "argument types do not match the function type");
+      if(fType.isFunction()) {
+        if(n.getNumChildren() != fType.getNumChildren() - 1) {
+          throw TypeCheckingExceptionPrivate(n, "number of arguments does not match the function type");
+        }
+        TNode::iterator argument_it = n.begin();
+        TNode::iterator argument_it_end = n.end();
+        TypeNode::iterator argument_type_it = fType.begin();
+        for(; argument_it != argument_it_end; ++argument_it) {
+          if((*argument_it).getType() != *argument_type_it) {
+            throw TypeCheckingExceptionPrivate(n, "argument types do not match the function type");
+          }
+        }
+      } else {
+        if( n.getNumChildren() > 0 ) {
+          throw TypeCheckingExceptionPrivate(n, "number of arguments does not match the function type");
         }
       }
     }
-    return fType.getRangeType();
+    return fType.isFunction() ? fType.getRangeType() : fType;
   }
 };/* class ApplyTypeRule */
 
diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp
index 403f6f84b..9b463f797 100644
--- a/src/util/configuration.cpp
+++ b/src/util/configuration.cpp
@@ -18,13 +18,20 @@
  ** configuration information about the CVC4 library.
  **/
 
+#include <string>
+
 #include "util/configuration.h"
 #include "util/configuration_private.h"
+#include "cvc4autoconfig.h"
 
 using namespace std;
 
 namespace CVC4 {
 
+string Configuration::getName() {
+  return PACKAGE_NAME;
+}
+
 bool Configuration::isDebugBuild() {
   return IS_DEBUG_BUILD;
 }
diff --git a/src/util/configuration.h b/src/util/configuration.h
index 907cd1d31..33c0a7407 100644
--- a/src/util/configuration.h
+++ b/src/util/configuration.h
@@ -37,6 +37,8 @@ class CVC4_PUBLIC Configuration {
 
 public:
 
+  static std::string getName();
+
   static bool isDebugBuild();
 
   static bool isTracingBuild();
diff --git a/src/util/stats.h b/src/util/stats.h
index 43b48140e..d6b463e65 100644
--- a/src/util/stats.h
+++ b/src/util/stats.h
@@ -24,6 +24,7 @@
 
 #include <string>
 #include <ostream>
+#include <sstream>
 #include <iomanip>
 #include <set>
 #include <ctime>
@@ -44,16 +45,28 @@ class CVC4_PUBLIC Stat;
 
 class CVC4_PUBLIC StatisticsRegistry {
 private:
-  struct StatCmp;
+  struct StatCmp {
+    inline bool operator()(const Stat* s1, const Stat* s2) const;
+  };/* class StatisticsRegistry::StatCmp */
 
   typedef std::set< Stat*, StatCmp > StatSet;
   static StatSet d_registeredStats;
 
 public:
+
+  typedef StatSet::const_iterator const_iterator;
+
   static void flushStatistics(std::ostream& out);
 
   static inline void registerStat(Stat* s) throw(AssertionException);
   static inline void unregisterStat(Stat* s) throw(AssertionException);
+
+  static inline const_iterator begin() {
+    return d_registeredStats.begin();
+  }
+  static inline const_iterator end() {
+    return d_registeredStats.end();
+  }
 };/* class StatisticsRegistry */
 
 
@@ -65,8 +78,8 @@ private:
 
 public:
 
-  Stat(const std::string& s) throw(CVC4::AssertionException) : d_name(s)
-  {
+  Stat(const std::string& s) throw(CVC4::AssertionException) :
+    d_name(s) {
     if(__CVC4_USE_STATISTICS) {
       AlwaysAssert(d_name.find(s_delim) == std::string::npos);
     }
@@ -85,18 +98,17 @@ public:
   const std::string& getName() const {
     return d_name;
   }
-};/* class Stat */
-
 
-struct StatisticsRegistry::StatCmp {
-  bool operator()(const Stat* s1, const Stat* s2) const
-  {
-    return (s1->getName()) < (s2->getName());
-  }
-};/* class StatCmp */
+  virtual std::string getValue() const = 0;
+};/* class Stat */
 
+inline bool StatisticsRegistry::StatCmp::operator()(const Stat* s1,
+                                                    const Stat* s2) const {
+  return s1->getName() < s2->getName();
+}
 
-inline void StatisticsRegistry::registerStat(Stat* s) throw(AssertionException) {
+inline void StatisticsRegistry::registerStat(Stat* s)
+  throw(AssertionException) {
   if(__CVC4_USE_STATISTICS) {
     AlwaysAssert(d_registeredStats.find(s) == d_registeredStats.end());
     d_registeredStats.insert(s);
@@ -104,7 +116,8 @@ inline void StatisticsRegistry::registerStat(Stat* s) throw(AssertionException)
 }/* StatisticsRegistry::registerStat */
 
 
-inline void StatisticsRegistry::unregisterStat(Stat* s) throw(AssertionException) {
+inline void StatisticsRegistry::unregisterStat(Stat* s)
+  throw(AssertionException) {
   if(__CVC4_USE_STATISTICS) {
     AlwaysAssert(d_registeredStats.find(s) != d_registeredStats.end());
     d_registeredStats.erase(s);
@@ -120,7 +133,9 @@ inline void StatisticsRegistry::unregisterStat(Stat* s) throw(AssertionException
 template <class T>
 class DataStat : public Stat {
 public:
-  DataStat(const std::string& s) : Stat(s) {}
+  DataStat(const std::string& s) :
+    Stat(s) {
+  }
 
   virtual const T& getData() const = 0;
   virtual void setData(const T&) = 0;
@@ -130,6 +145,12 @@ public:
       out << getData();
     }
   }
+
+  std::string getValue() const {
+    std::stringstream ss;
+    ss << getData();
+    return ss.str();
+  }
 };/* class DataStat */
 
 
@@ -140,13 +161,14 @@ private:
   const T* d_data;
 
 public:
-  ReferenceStat(const std::string& s):
-    DataStat<T>(s), d_data(NULL)
-  {}
+  ReferenceStat(const std::string& s) :
+    DataStat<T>(s),
+    d_data(NULL) {
+  }
 
-  ReferenceStat(const std::string& s, const T& data):
-    DataStat<T>(s), d_data(NULL)
-  {
+  ReferenceStat(const std::string& s, const T& data) :
+    DataStat<T>(s),
+    d_data(NULL) {
     setData(data);
   }
 
@@ -155,6 +177,7 @@ public:
       d_data = &t;
     }
   }
+
   const T& getData() const {
     if(__CVC4_USE_STATISTICS) {
       return *d_data;
@@ -173,8 +196,10 @@ protected:
 
 public:
 
-  BackedStat(const std::string& s, const T& init): DataStat<T>(s), d_data(init)
-  {}
+  BackedStat(const std::string& s, const T& init) :
+    DataStat<T>(s),
+    d_data(init) {
+  }
 
   void setData(const T& t) {
     if(__CVC4_USE_STATISTICS) {
@@ -202,8 +227,9 @@ public:
 class IntStat : public BackedStat<int64_t> {
 public:
 
-  IntStat(const std::string& s, int64_t init): BackedStat<int64_t>(s, init)
-  {}
+  IntStat(const std::string& s, int64_t init) :
+    BackedStat<int64_t>(s, init) {
+  }
 
   IntStat& operator++() {
     if(__CVC4_USE_STATISTICS) {