Options merge. This commit:

1. changes the way options are declared (see http://church.cims.nyu.edu/wiki/Options)
2. moves module-specific options enumerations (SimplificationMode, DecisionMode, ArithUnateLemmaMode, etc.) to their own header files, also they are no longer inside the Options:: class namespace.
3. includes many SMT-LIBv2 compliance fixes, especially to (set-option..) and (get-option..)

The biggest syntactical changes (outside of adding new options) you'll notice are in accessing and setting options:

* to access an option, write (e.g.) options::unconstrainedSimp() instead of Options::current()->unconstrainedSimp.
* to determine if an option value was set by the user, check (e.g.) options::unconstrainedSimp.wasSetByUser().
* ensure that you have the option available (you have to #include the right module's options.h file, e.g. #include "theory/uf/options.h" for UF options)
*** this point is important.  If you access an option and it tells you the option doesn't exist, you aren't #including the appropriate options.h header file ***

Note that if you want an option to be directly set (i.e., other than via command-line parsing or SmtEngine::setOption()), you need to mark the option :read-write in its options file (otherwise it's read-only), and you then write (e.g.) options::unconstrainedSimp.set(true).

Adding new options is incredibly simple for primitive types (int, unsigned, bool, string, double).  For option settings that you need to turn into a member of an enumerated type, you write a custom "handler" for the option---this is no additional work than it was before, and there are many examples to copy from (a good one is stringToSimplificationMode() in src/smt/options_handlers.h).

Benefits of the new options system include:

1. changes to options declarations don't require a full-source rebuild (you only have to rebuild those sources that depend on the set of options that changed).
2. lots of sanity checks (that the same option isn't declared twice, that option values are in range for their type, that all options are documented properly, etc.)
3. consistency: Boolean-valued option --foo gets a --no-foo automatically, documentation is generated consistently, the option-parsing matches the documented option name, etc.
4. setting options programmatically via SmtEngine::setOption() is enabled, and behaves the same as command-line equivalents (including checking the value is in range, etc.)
5. the notion of options being "set by the user" is now primitive; you can use (e.g.) options::unconstrainedSimp.wasSetByUser() instead of having to use (and maintain) a separate Boolean option for the purpose

I've taken lots of care not to break anything.  Hopefully, I've succeeded in that.

11 files changed, 138 insertions, 29 deletions

diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index 6baa4613f..38cb8250c 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -56,6 +56,7 @@ EXTRA_DIST = \
 	expr_template.h \
 	expr_template.cpp \
 	type_checker_template.cpp \
+	options_handlers.h \
 	mkkind \
 	mkmetakind \
 	mkexpr \
@@ -154,3 +155,6 @@ type_checker.cpp: type_checker_template.cpp mkexpr @top_builddir@/src/theory/.su
 		$< \
 		`cat @top_builddir@/src/theory/.subdirs` \
 	> $@) || (rm -f $@ && exit 1)
+
+.PHONY: builts
+builts: $(BUILT_SOURCES)
diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 12830a618..c127aca75 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -902,7 +902,7 @@ void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine) throw() {
     stringstream ss;
     ss << d_status;
     SExpr status = ss.str();
-    smtEngine->setInfo(":status", status);
+    smtEngine->setInfo("status", status);
     d_commandStatus = CommandSuccess::instance();
   } catch(exception& e) {
     d_commandStatus = new CommandFailure(e.what());
@@ -1074,7 +1074,13 @@ std::string GetOptionCommand::getFlag() const throw() {
 
 void GetOptionCommand::invoke(SmtEngine* smtEngine) throw() {
   try {
-    d_result = smtEngine->getOption(d_flag).getValue();
+    vector<SExpr> v;
+    v.push_back(SExpr(SExpr::Keyword(string(":") + d_flag)));
+    v.push_back(smtEngine->getOption(d_flag));
+    stringstream ss;
+    
+    ss << SExpr(v);
+    d_result = ss.str();
     d_commandStatus = CommandSuccess::instance();
   } catch(BadOptionException&) {
     d_commandStatus = new CommandUnsupported();
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 25578399f..a8491c937 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -20,7 +20,7 @@
 #include "expr/expr_manager.h"
 #include "expr/variable_type_map.h"
 #include "context/context.h"
-#include "util/options.h"
+#include "options/options.h"
 #include "util/stats.h"
 
 #include <map>
@@ -126,7 +126,7 @@ ExprManager::~ExprManager() throw() {
   }
 }
 
-const Options* ExprManager::getOptions() const {
+const Options& ExprManager::getOptions() const {
   return d_nodeManager->getOptions();
 }
 
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index fdc1e1159..b762da3ea 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -42,7 +42,7 @@ namespace CVC4 {
 class Expr;
 class SmtEngine;
 class NodeManager;
-struct Options;
+class Options;
 class IntStat;
 class ExprManagerMapCollection;
 
@@ -124,7 +124,7 @@ public:
   ~ExprManager() throw();
 
   /** Get this node manager's options */
-  const Options* getOptions() const;
+  const Options& getOptions() const;
 
   /** Get the type for booleans */
   BooleanType booleanType() const;
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index dc82daec4..a2e861118 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -36,7 +36,7 @@ ${includes}
 #include "util/exception.h"
 #include "util/language.h"
 #include "util/hash.h"
-#include "util/options.h"
+#include "expr/options.h"
 
 // This is a hack, but an important one: if there's an error, the
 // compiler directs the user to the template file instead of the
@@ -683,8 +683,8 @@ public:
     long& l = out.iword(s_iosIndex);
     if(l == 0) {
       // set the default print depth on this ostream
-      if(Options::current() != NULL) {
-        l = Options::current()->defaultExprDepth;
+      if(&Options::current() != NULL) {
+        l = options::defaultExprDepth();
       }
       if(l == 0) {
         l = s_defaultPrintDepth;
@@ -909,8 +909,8 @@ public:
     if(l == 0) {
       // set the default language on this ostream
       // (offset by one to detect whether default has been set yet)
-      if(Options::current() != NULL) {
-        l = Options::current()->outputLanguage + 1;
+      if(&Options::current() != NULL) {
+        l = options::outputLanguage() + 1;
       }
       if(l <= 0 || l > language::output::LANG_MAX) {
         // if called from outside the library, we may not have options
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index fcb503d37..fa9b1c011 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -742,7 +742,7 @@ public:
 
 #include "expr/node.h"
 #include "expr/node_manager.h"
-#include "util/options.h"
+#include "expr/options.h"
 
 namespace CVC4 {
 
@@ -1301,7 +1301,7 @@ inline void NodeBuilder<nchild_thresh>::maybeCheckType(const TNode n) const
     throw(TypeCheckingExceptionPrivate, AssertionException) {
   /* force an immediate type check, if early type checking is
      enabled and the current node isn't a variable or constant */
-  if( d_nm->getOptions()->earlyTypeChecking ) {
+  if( d_nm->getOptions()[options::earlyTypeChecking] ) {
     kind::MetaKind mk = n.getMetaKind();
     if( mk != kind::metakind::VARIABLE
         && mk != kind::metakind::CONSTANT ) {
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 1abcf398b..fc2eec774 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -21,7 +21,7 @@
 #include "expr/node_manager.h"
 
 #include "util/Assert.h"
-#include "util/options.h"
+#include "options/options.h"
 #include "util/stats.h"
 #include "util/tls.h"
 
@@ -82,7 +82,7 @@ struct NVReclaim {
 
 NodeManager::NodeManager(context::Context* ctxt,
                          ExprManager* exprManager) :
-  d_options(),
+  d_options(new Options()),
   d_statisticsRegistry(new StatisticsRegistry()),
   next_id(0),
   d_attrManager(ctxt),
@@ -92,11 +92,10 @@ NodeManager::NodeManager(context::Context* ctxt,
   init();
 }
 
-
 NodeManager::NodeManager(context::Context* ctxt,
                          ExprManager* exprManager,
                          const Options& options) :
-  d_options(options),
+  d_options(new Options(options)),
   d_statisticsRegistry(new StatisticsRegistry()),
   next_id(0),
   d_attrManager(ctxt),
@@ -154,6 +153,7 @@ NodeManager::~NodeManager() {
   }
 
   delete d_statisticsRegistry;
+  delete d_options;
 }
 
 void NodeManager::reclaimZombies() {
@@ -253,7 +253,7 @@ TypeNode NodeManager::getType(TNode n, bool check)
 
   Debug("getType") << "getting type for " << n << std::endl;
 
-  if(needsCheck && !d_options.earlyTypeChecking) {
+  if(needsCheck && !(*d_options)[options::earlyTypeChecking]) {
     /* Iterate and compute the children bottom up. This avoids stack
        overflows in computeType() when the Node graph is really deep,
        which should only affect us when we're type checking lazily. */
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 6c34eb4a3..501a0f4fd 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -41,7 +41,7 @@
 #include "util/subrange_bound.h"
 #include "util/configuration_private.h"
 #include "util/tls.h"
-#include "util/options.h"
+#include "options/options.h"
 
 namespace CVC4 {
 
@@ -83,7 +83,7 @@ class NodeManager {
 
   static CVC4_THREADLOCAL(NodeManager*) s_current;
 
-  Options d_options;
+  Options* d_options;
   StatisticsRegistry* d_statisticsRegistry;
 
   NodeValuePool d_nodeValuePool;
@@ -267,13 +267,13 @@ public:
   static NodeManager* currentNM() { return s_current; }
 
   /** Get this node manager's options (const version) */
-  const Options* getOptions() const {
-    return &d_options;
+  const Options& getOptions() const {
+    return *d_options;
   }
 
   /** Get this node manager's options (non-const version) */
-  Options* getOptions() {
-    return &d_options;
+  Options& getOptions() {
+    return *d_options;
   }
 
   /** Get this node manager's statistics registry */
@@ -791,14 +791,14 @@ public:
     // Expr is destructed, there's no active node manager.
     //Assert(nm != NULL);
     NodeManager::s_current = nm;
-    Options::s_current = nm ? &nm->d_options : NULL;
+    Options::s_current = nm ? nm->d_options : NULL;
     Debug("current") << "node manager scope: "
                      << NodeManager::s_current << "\n";
   }
 
   ~NodeManagerScope() {
     NodeManager::s_current = d_oldNodeManager;
-    Options::s_current = d_oldNodeManager ? &d_oldNodeManager->d_options : NULL;
+    Options::s_current = d_oldNodeManager ? d_oldNodeManager->d_options : NULL;
     Debug("current") << "node manager scope: "
                      << "returning to " << NodeManager::s_current << "\n";
   }
diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp
index dbf706c45..587f3873b 100644
--- a/src/expr/node_value.cpp
+++ b/src/expr/node_value.cpp
@@ -25,6 +25,7 @@
 #include "expr/kind.h"
 #include "expr/metakind.h"
 #include "util/language.h"
+#include "options/options.h"
 #include "printer/printer.h"
 #include <sstream>
 
@@ -37,11 +38,12 @@ NodeValue NodeValue::s_null(0);
 
 string NodeValue::toString() const {
   stringstream ss;
-  OutputLanguage outputLanguage = (this == &s_null) ? language::output::LANG_AST : Options::current()->outputLanguage;
+
+  OutputLanguage outlang = (this == &s_null) ? language::output::LANG_AST : options::outputLanguage();
   toStream(ss, -1, false,
-           outputLanguage == language::output::LANG_AUTO ?
+           outlang == language::output::LANG_AUTO ?
              language::output::LANG_AST :
-             outputLanguage);
+             outlang);
   return ss.str();
 }
 
diff --git a/src/expr/options b/src/expr/options
new file mode 100644
index 000000000..24810962e
--- /dev/null
+++ b/src/expr/options
@@ -0,0 +1,25 @@
+#
+# Option specification file for CVC4
+# See src/options/base_options for a description of this file format
+#
+
+module EXPR "expr/options.h" Expression package
+
+option defaultExprDepth --default-expr-depth=N int :predicate CVC4::expr::setDefaultExprDepth :predicate-include "expr/options_handlers.h"
+ print exprs to depth N (0 == default, -1 == no limit)
+option - --default-dag-thresh=N argument :handler CVC4::expr::setDefaultDagThresh :handler-include "expr/options_handlers.h"
+ dagify common subexprs appearing > N times (1 == default, 0 == don't dagify)
+option - --print-expr-types void :handler CVC4::expr::setPrintExprTypes :handler-include "expr/options_handlers.h"
+ print types with variables when printing exprs
+
+option earlyTypeChecking --eager-type-checking/--lazy-type-checking bool :default USE_EARLY_TYPE_CHECKING_BY_DEFAULT
+ type check expressions immediately on creation (debug builds only)
+/type check expressions only when necessary (default)
+
+# --no-type-checking will override any --early-type-checking or --lazy-type-checking option
+# --lazy-type-checking is linked because earlyTypeChecking should be set false too
+option typeChecking /--no-type-checking bool :default DO_SEMANTIC_CHECKS_BY_DEFAULT :link /--lazy-type-checking
+ never type check expressions
+
+endmodule
+
diff --git a/src/expr/options_handlers.h b/src/expr/options_handlers.h
new file mode 100644
index 000000000..a17445188
--- /dev/null
+++ b/src/expr/options_handlers.h
@@ -0,0 +1,72 @@
+/*********************                                                        */
+/*! \file options_handlers.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** 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
+ ** information.\endverbatim
+ **
+ ** \brief Custom handlers and predicates for expression package options
+ **
+ ** Custom handlers and predicates for expression package options.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__EXPR__OPTIONS_HANDLERS_H
+#define __CVC4__EXPR__OPTIONS_HANDLERS_H
+
+#include "util/output.h"
+#include "util/dump.h"
+
+namespace CVC4 {
+namespace expr {
+
+inline void setDefaultExprDepth(std::string option, int depth, SmtEngine* smt) {
+  if(depth < -1) {
+    throw OptionException("--default-expr-depth requires a positive argument, or -1.");
+  }
+
+  Debug.getStream() << Expr::setdepth(depth);
+  Trace.getStream() << Expr::setdepth(depth);
+  Notice.getStream() << Expr::setdepth(depth);
+  Chat.getStream() << Expr::setdepth(depth);
+  Message.getStream() << Expr::setdepth(depth);
+  Warning.getStream() << Expr::setdepth(depth);
+  // intentionally exclude Dump stream from this list
+}
+
+inline void setDefaultDagThresh(std::string option, std::string optarg, SmtEngine* smt) {
+  int dag = atoi(optarg.c_str());
+  if(dag < 0) {
+    throw OptionException("--default-dag-thresh requires a nonnegative argument.");
+  }
+
+  Debug.getStream() << Expr::dag(dag);
+  Trace.getStream() << Expr::dag(dag);
+  Notice.getStream() << Expr::dag(dag);
+  Chat.getStream() << Expr::dag(dag);
+  Message.getStream() << Expr::dag(dag);
+  Warning.getStream() << Expr::dag(dag);
+  Dump.getStream() << Expr::dag(dag);
+}
+
+inline void setPrintExprTypes(std::string option, SmtEngine* smt) {
+  Debug.getStream() << Expr::printtypes(true);
+  Trace.getStream() << Expr::printtypes(true);
+  Notice.getStream() << Expr::printtypes(true);
+  Chat.getStream() << Expr::printtypes(true);
+  Message.getStream() << Expr::printtypes(true);
+  Warning.getStream() << Expr::printtypes(true);
+  // intentionally exclude Dump stream from this list
+}
+
+}/* CVC4::expr namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__EXPR__OPTIONS_HANDLERS_H */