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.

15 files changed, 442 insertions, 47 deletions

diff --git a/src/theory/quantifiers/Makefile.am b/src/theory/quantifiers/Makefile.am
index 316e2fbff..5172001fc 100644
--- a/src/theory/quantifiers/Makefile.am
+++ b/src/theory/quantifiers/Makefile.am
@@ -17,6 +17,10 @@ libquantifiers_la_SOURCES = \
 	instantiation_engine.cpp \
 	model_engine.h \
 	model_engine.cpp \
+	inst_when_mode.cpp \
+	inst_when_mode.h \
+	literal_match_mode.cpp \
+	literal_match_mode.h \
 	relevant_domain.h \
 	relevant_domain.cpp \
 	rep_set_iterator.h \
@@ -28,4 +32,6 @@ libquantifiers_la_SOURCES = \
 	model_builder.h \
 	model_builder.cpp
 
-EXTRA_DIST = kinds
\ No newline at end of file
+EXTRA_DIST = \
+	kinds \
+	options_handlers.h
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 1c6b47867..5d7317cbc 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -54,10 +54,10 @@ void FirstOrderModel::initialize(){
     initializeModelForTerm( f[1] );
   }
   //for debugging
-  if( Options::current()->printModelEngine ){
+  if( Trace.isOn("model-engine") ){
     for( std::map< TypeNode, std::vector< Node > >::iterator it = d_rep_set.d_type_reps.begin(); it != d_rep_set.d_type_reps.end(); ++it ){
       if( it->first.isSort() ){
-        Message() << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
+        Trace("model-engine") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
       }
     }
   }
@@ -181,4 +181,4 @@ void FirstOrderModel::toStream(std::ostream& out){
     out << std::endl;
   }
 #endif
-}
\ No newline at end of file
+}
diff --git a/src/theory/quantifiers/inst_when_mode.cpp b/src/theory/quantifiers/inst_when_mode.cpp
new file mode 100644
index 000000000..b60148c21
--- /dev/null
+++ b/src/theory/quantifiers/inst_when_mode.cpp
@@ -0,0 +1,47 @@
+/*********************                                                        */
+/*! \file inst_when_mode.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  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 [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include <iostream>
+#include "theory/quantifiers/inst_when_mode.h"
+
+namespace CVC4 {
+
+std::ostream& operator<<(std::ostream& out, theory::quantifiers::InstWhenMode mode) {
+  switch(mode) {
+  case theory::quantifiers::INST_WHEN_PRE_FULL:
+    out << "INST_WHEN_PRE_FULL";
+    break;
+  case theory::quantifiers::INST_WHEN_FULL:
+    out << "INST_WHEN_FULL";
+    break;
+  case theory::quantifiers::INST_WHEN_FULL_LAST_CALL:
+    out << "INST_WHEN_FULL_LAST_CALL";
+    break;
+  case theory::quantifiers::INST_WHEN_LAST_CALL:
+    out << "INST_WHEN_LAST_CALL";
+    break;
+  default:
+    out << "InstWhenMode!UNKNOWN";
+  }
+
+  return out;
+}
+
+}/* CVC4 namespace */
+
diff --git a/src/theory/quantifiers/inst_when_mode.h b/src/theory/quantifiers/inst_when_mode.h
new file mode 100644
index 000000000..2cfba4935
--- /dev/null
+++ b/src/theory/quantifiers/inst_when_mode.h
@@ -0,0 +1,49 @@
+/*********************                                                        */
+/*! \file inst_when_mode.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-2012  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 [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__INST_WHEN_MODE_H
+#define __CVC4__THEORY__QUANTIFIERS__INST_WHEN_MODE_H
+
+#include <iostream>
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+typedef enum {
+  /** Apply instantiation round before full effort (possibly at standard effort) */
+  INST_WHEN_PRE_FULL,
+  /** Apply instantiation round at full effort or above  */
+  INST_WHEN_FULL,
+  /** Apply instantiation round at full effort half the time, and last call always */
+  INST_WHEN_FULL_LAST_CALL,
+  /** Apply instantiation round at last call only */
+  INST_WHEN_LAST_CALL,
+} InstWhenMode;
+
+}/* CVC4::theory::quantifiers namespace */
+}/* CVC4::theory namespace */
+
+std::ostream& operator<<(std::ostream& out, theory::quantifiers::InstWhenMode mode) CVC4_PUBLIC;
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__INST_WHEN_MODE_H */
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 2b79cd8b9..fb3e6fb36 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -18,6 +18,7 @@
 
 #include "theory/theory_engine.h"
 #include "theory/uf/theory_uf_instantiator.h"
+#include "theory/quantifiers/options.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/first_order_model.h"
 
@@ -65,7 +66,7 @@ void InstantiationEngine::addCbqiLemma( Node f ){
 
 bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
   //if counterexample-based quantifier instantiation is active
-  if( Options::current()->cbqi ){
+  if( options::cbqi() ){
     //check if any cbqi lemma has not been added yet
     bool addedLemma = false;
     for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
@@ -136,9 +137,7 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
     return false;
   }else{
     Debug("inst-engine-ctrl") << "---Done. " << (int)d_quantEngine->d_lemmas_waiting.size() << std::endl;
-    if( Options::current()->printInstEngine ){
-      Message() << "Added lemmas = " << (int)d_quantEngine->d_lemmas_waiting.size() << std::endl;
-    }
+    Trace("inst-engine") << "Added lemmas = " << (int)d_quantEngine->d_lemmas_waiting.size() << std::endl;
     //flush lemmas to output channel
     d_quantEngine->flushLemmas( &d_quantEngine->getOutputChannel() );
     return true;
@@ -153,11 +152,11 @@ void InstantiationEngine::check( Theory::Effort e ){
   }
   //determine if we should perform check, based on instWhenMode
   bool performCheck = false;
-  if( Options::current()->instWhenMode==Options::INST_WHEN_FULL ){
+  if( options::instWhenMode()==INST_WHEN_FULL ){
     performCheck = ( e >= Theory::EFFORT_FULL );
-  }else if( Options::current()->instWhenMode==Options::INST_WHEN_FULL_LAST_CALL ){
+  }else if( options::instWhenMode()==INST_WHEN_FULL_LAST_CALL ){
     performCheck = ( ( e==Theory::EFFORT_FULL  && ierCounter%2==0 ) || e==Theory::EFFORT_LAST_CALL );
-  }else if( Options::current()->instWhenMode==Options::INST_WHEN_LAST_CALL ){
+  }else if( options::instWhenMode()==INST_WHEN_LAST_CALL ){
     performCheck = ( e >= Theory::EFFORT_LAST_CALL );
   }else{
     performCheck = true;
@@ -165,9 +164,9 @@ void InstantiationEngine::check( Theory::Effort e ){
   if( performCheck ){
     Debug("inst-engine") << "IE: Check " << e << " " << ierCounter << std::endl;
     double clSet = 0;
-    if( Options::current()->printInstEngine ){
+    if( Trace.isOn("inst-engine") ){
       clSet = double(clock())/double(CLOCKS_PER_SEC);
-      Message() << "---Instantiation Engine Round, effort = " << e << "---" << std::endl;
+      Trace("inst-engine") << "---Instantiation Engine Round, effort = " << e << "---" << std::endl;
     }
     bool quantActive = false;
     //for each quantifier currently asserted,
@@ -178,7 +177,7 @@ void InstantiationEngine::check( Theory::Effort e ){
                          << d_quantEngine->getModel()->getNumAssertedQuantifiers() << std::endl;
     for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
       Node n = d_quantEngine->getModel()->getAssertedQuantifier( i );
-      if( Options::current()->cbqi && hasAddedCbqiLemma( n ) ){
+      if( options::cbqi() && hasAddedCbqiLemma( n ) ){
         Node cel = d_ce_lit[ n ];
         bool active, value;
         bool ceValue = false;
@@ -232,21 +231,21 @@ void InstantiationEngine::check( Theory::Effort e ){
             Debug("inst-engine") << "No instantiation given, returning unknown..." << std::endl;
             d_quantEngine->getOutputChannel().setIncomplete();
           }else{
-            Assert( Options::current()->finiteModelFind );
+            Assert( options::finiteModelFind() );
             Debug("inst-engine") << "No instantiation given, defer to another engine..." << std::endl;
           }
         }
       }
     }else{
       if( e==Theory::EFFORT_LAST_CALL ){
-        if( Options::current()->cbqi ){
+        if( options::cbqi() ){
           debugSat( SAT_CBQI );
         }
       }
     }
-    if( Options::current()->printInstEngine ){
+    if( Trace.isOn("inst-engine") ){
       double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
-      Message() << "Finished instantiation engine, time = " << (clSet2-clSet) << std::endl;
+      Trace("inst-engine") << "Finished instantiation engine, time = " << (clSet2-clSet) << std::endl;
     }
   }
 }
@@ -302,9 +301,9 @@ bool InstantiationEngine::hasNonArithmeticVariable( Node f ){
 }
 
 bool InstantiationEngine::doCbqi( Node f ){
-  if( Options::current()->cbqiSetByUser ){
-    return Options::current()->cbqi;
-  }else if( Options::current()->cbqi ){
+  if( options::cbqi.wasSetByUser() ){
+    return options::cbqi();
+  }else if( options::cbqi() ){
     //if quantifier has a non-arithmetic variable, then do not use cbqi
     //if quantifier has an APPLY_UF term, then do not use cbqi
     return !hasNonArithmeticVariable( f ) && !hasApplyUf( f[1] );
diff --git a/src/theory/quantifiers/literal_match_mode.cpp b/src/theory/quantifiers/literal_match_mode.cpp
new file mode 100644
index 000000000..87b4b94fe
--- /dev/null
+++ b/src/theory/quantifiers/literal_match_mode.cpp
@@ -0,0 +1,43 @@
+/*********************                                                        */
+/*! \file literal_match_mode.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  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 [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include <iostream>
+#include "theory/quantifiers/literal_match_mode.h"
+
+namespace CVC4 {
+
+std::ostream& operator<<(std::ostream& out, theory::quantifiers::LiteralMatchMode mode) {
+  switch(mode) {
+  case theory::quantifiers::LITERAL_MATCH_NONE:
+    out << "LITERAL_MATCH_NONE";
+    break;
+  case theory::quantifiers::LITERAL_MATCH_PREDICATE:
+    out << "LITERAL_MATCH_PREDICATE";
+    break;
+  case theory::quantifiers::LITERAL_MATCH_EQUALITY:
+    out << "LITERAL_MATCH_EQUALITY";
+    break;
+  default:
+    out << "LiteralMatchMode!UNKNOWN";
+  }
+
+  return out;
+}
+
+}/* CVC4 namespace */
diff --git a/src/theory/quantifiers/literal_match_mode.h b/src/theory/quantifiers/literal_match_mode.h
new file mode 100644
index 000000000..189f0a235
--- /dev/null
+++ b/src/theory/quantifiers/literal_match_mode.h
@@ -0,0 +1,47 @@
+/*********************                                                        */
+/*! \file literal_match_mode.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-2012  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 [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__LITERAL_MATCH_MODE_H
+#define __CVC4__THEORY__QUANTIFIERS__LITERAL_MATCH_MODE_H
+
+#include <iostream>
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+typedef enum {
+  /** Do not consider polarity of patterns */
+  LITERAL_MATCH_NONE,
+  /** Consider polarity of boolean predicates only */
+  LITERAL_MATCH_PREDICATE,
+  /** Consider polarity of boolean predicates, as well as equalities */
+  LITERAL_MATCH_EQUALITY,
+} LiteralMatchMode;
+
+}/* CVC4::theory::quantifiers namespace */
+}/* CVC4::theory namespace */
+
+std::ostream& operator<<(std::ostream& out, theory::quantifiers::LiteralMatchMode mode) CVC4_PUBLIC;
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__LITERAL_MATCH_MODE_H */
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index 9cd5020fb..5d49c914f 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -90,11 +90,11 @@ void ModelEngineBuilder::processBuildModel( TheoryModel* m ) {
           }
         }
       }
-      if( Options::current()->printModelEngine ){
+      if( Trace.isOn("model-engine") ){
         if( d_addedLemmas>0 ){
-          Message() << "InstGen, added lemmas = " << d_addedLemmas << std::endl;
+          Trace("model-engine") << "InstGen, added lemmas = " << d_addedLemmas << std::endl;
         }else{
-          Message() << "No InstGen lemmas..." << std::endl;
+          Trace("model-engine") << "No InstGen lemmas..." << std::endl;
         }
       }
       Debug("fmf-model-debug") << "---> Added lemmas = " << d_addedLemmas << std::endl;
@@ -388,11 +388,11 @@ void ModelEngineBuilder::finishProcessBuildModel( TheoryModel* m ){
 }
 
 bool ModelEngineBuilder::optUseModel() {
-  return Options::current()->fmfModelBasedInst;
+  return options::fmfModelBasedInst();
 }
 
 bool ModelEngineBuilder::optInstGen(){
-  return Options::current()->fmfInstGen;
+  return options::fmfInstGen();
 }
 
 bool ModelEngineBuilder::optOneQuantPerRoundInstGen(){
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index ddaaa5b6f..4d91c8c95 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -21,6 +21,7 @@
 #include "theory/uf/theory_uf.h"
 #include "theory/uf/theory_uf_strong_solver.h"
 #include "theory/uf/theory_uf_instantiator.h"
+#include "theory/quantifiers/options.h"
 #include "theory/arrays/theory_arrays_model.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/term_database.h"
@@ -64,9 +65,9 @@ void ModelEngine::check( Theory::Effort e ){
     if( addedLemmas==0 ){
       //quantifiers are initialized, we begin an instantiation round
       double clSet = 0;
-      if( Options::current()->printModelEngine ){
+      if( Trace.isOn("model-engine") ){
         clSet = double(clock())/double(CLOCKS_PER_SEC);
-        Message() << "---Model Engine Round---" << std::endl;
+        Trace("model-engine") << "---Model Engine Round---" << std::endl;
       }
       Debug("fmf-model-debug") << "---Begin Instantiation Round---" << std::endl;
       ++(d_statistics.d_inst_rounds);
@@ -108,11 +109,11 @@ void ModelEngine::check( Theory::Effort e ){
         }
         Debug("fmf-model-debug") << "---> Added lemmas = " << addedLemmas << " / " << d_triedLemmas << " / ";
         Debug("fmf-model-debug") << d_testLemmas << " / " << d_relevantLemmas << " / " << d_totalLemmas << std::endl;
-        if( Options::current()->printModelEngine ){
-          Message() << "Added Lemmas = " << addedLemmas << " / " << d_triedLemmas << " / ";
-          Message() << d_testLemmas << " / " << d_relevantLemmas << " / " << d_totalLemmas << std::endl;
+        if( Trace.isOn("model-engine") ){
+          Trace("model-engine") << "Added Lemmas = " << addedLemmas << " / " << d_triedLemmas << " / ";
+          Trace("model-engine") << d_testLemmas << " / " << d_relevantLemmas << " / " << d_totalLemmas << std::endl;
           double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
-          Message() << "Finished model engine, time = " << (clSet2-clSet) << std::endl;
+          Trace("model-engine") << "Finished model engine, time = " << (clSet2-clSet) << std::endl;
         }
 #ifdef ME_PRINT_WARNINGS
         if( addedLemmas>10000 ){
@@ -145,11 +146,11 @@ void ModelEngine::assertNode( Node f ){
 }
 
 bool ModelEngine::optOneInstPerQuantRound(){
-  return Options::current()->fmfOneInstPerRound;
+  return options::fmfOneInstPerRound();
 }
 
 bool ModelEngine::optUseRelevantDomain(){
-  return Options::current()->fmfRelevantDomain;
+  return options::fmfRelevantDomain();
 }
 
 bool ModelEngine::optOneQuantPerRound(){
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
new file mode 100644
index 000000000..91e831092
--- /dev/null
+++ b/src/theory/quantifiers/options
@@ -0,0 +1,89 @@
+#
+# Option specification file for CVC4
+# See src/options/base_options for a description of this file format
+#
+
+module QUANTIFIERS "theory/quantifiers/options.h" Quantifiers
+
+# Whether to mini-scope quantifiers.
+# For example, forall x. ( P( x ) ^ Q( x ) ) will be rewritten to
+# ( forall x. P( x ) ) ^ ( forall x. Q( x ) )
+option miniscopeQuant /--disable-miniscope-quant bool :default true
+ disable miniscope quantifiers
+
+# Whether to mini-scope quantifiers based on formulas with no free variables.
+# For example, forall x. ( P( x ) V Q ) will be rewritten to
+# ( forall x. P( x ) ) V Q
+option miniscopeQuantFreeVar /--disable-miniscope-quant-fv bool :default true
+ disable miniscope quantifiers for ground subformulas
+
+# Whether to prenex (nested universal) quantifiers
+option prenexQuant /--disable-prenex-quant bool :default true
+ disable prenexing of quantified formulas
+
+# Whether to variable-eliminate quantifiers.
+# For example, forall x y. ( P( x, y ) V x != c ) will be rewritten to
+#   forall y. P( c, y )
+option varElimQuant --var-elim-quant bool :default false
+ enable variable elimination of quantified formulas
+
+# Whether to CNF quantifier bodies
+option cnfQuant --cnf-quant bool :default false
+ apply CNF conversion to quantified formulas
+
+# Whether to pre-skolemize quantifier bodies.
+# For example, forall x. ( P( x ) => (exists y. f( y ) = x) ) will be rewritten to
+#   forall x. P( x ) => f( S( x ) ) = x
+option preSkolemQuant --pre-skolem-quant bool :default false
+ apply skolemization eagerly to bodies of quantified formulas
+
+# Whether to use smart triggers
+option smartTriggers /--disable-smart-triggers bool :default true
+ disable smart triggers
+
+# Whether to consider terms in the bodies of quantifiers for matching
+option registerQuantBodyTerms --register-quant-body-terms bool :default false
+ consider ground terms within bodies of quantified formulas for matching
+
+option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :default CVC4::theory::quantifiers::INST_WHEN_FULL_LAST_CALL :include "theory/quantifiers/inst_when_mode.h" :handler CVC4::theory::quantifiers::stringToInstWhenMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkInstWhenMode :predicate-include "theory/quantifiers/options_handlers.h"
+ when to apply instantiation
+
+option eagerInstQuant --eager-inst-quant bool :default false
+ apply quantifier instantiation eagerly
+
+option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::LiteralMatchMode :default CVC4::theory::quantifiers::LITERAL_MATCH_NONE :include "theory/quantifiers/literal_match_mode.h" :handler CVC4::theory::quantifiers::stringToLiteralMatchMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkLiteralMatchMode :predicate-include "theory/quantifiers/options_handlers.h"
+ choose literal matching mode
+
+option cbqi --enable-cbqi/--disable-cbqi bool :default false
+ turns on counterexample-based quantifier instantiation [off by default]
+/turns off counterexample-based quantifier instantiation
+
+option userPatternsQuant /--ignore-user-patterns bool :default true
+ ignore user-provided patterns for quantifier instantiation
+
+option flipDecision --enable-flip-decision/ bool :default false
+ turns on flip decision heuristic
+
+option finiteModelFind --finite-model-find bool :default false
+ use finite model finding heuristic for quantifier instantiation
+
+option ufssRegions /--disable-uf-ss-regions bool :default true
+ disable region-based method for discovering cliques and splits in uf strong solver
+option ufssEagerSplits --uf-ss-eager-split bool :default false
+ add splits eagerly for uf strong solver
+option ufssColoringSat --uf-ss-coloring-sat bool :default false
+ use coloring-based SAT heuristic for uf strong solver
+
+option fmfModelBasedInst /--disable-fmf-mbqi bool :default true
+ disable model-based quantifier instantiation for finite model finding
+
+option fmfInstGen /--disable-fmf-inst-gen bool :default true
+ disable Inst-Gen instantiation techniques for finite model finding
+option fmfOneInstPerRound --fmf-one-inst-per-round bool :default false
+ only add one instantiation per quantifier per round for fmf
+option fmfInstEngine --fmf-inst-engine bool :default false
+ use instantiation engine in conjunction with finite model finding
+option fmfRelevantDomain --fmf-relevant-domain bool :default false
+ use relevant domain computation, similar to complete instantiation (Ge, deMoura 09)
+
+endmodule
diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h
new file mode 100644
index 000000000..24734e8c8
--- /dev/null
+++ b/src/theory/quantifiers/options_handlers.h
@@ -0,0 +1,111 @@
+/*********************                                                        */
+/*! \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-2012  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 [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__OPTIONS_HANDLERS_H
+#define __CVC4__THEORY__QUANTIFIERS__OPTIONS_HANDLERS_H
+
+#include <string>
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+static const std::string instWhenHelp = "\
+Modes currently supported by the --inst-when option:\n\
+\n\
+full\n\
++ Run instantiation round at full effort, before theory combination.\n\
+\n\
+full-last-call (default)\n\
++ Alternate running instantiation rounds at full effort and last\n\
+  call.  In other words, interleave instantiation and theory combination.\n\
+\n\
+last-call\n\
++ Run instantiation at last call effort, after theory combination.\n\
+\n\
+";
+
+static const std::string literalMatchHelp = "\
+Literal match modes currently supported by the --literal-match option:\n\
+\n\
+none (default)\n\
++ Do not use literal matching.\n\
+\n\
+predicate\n\
++ Consider the phase requirements of predicate literals when applying heuristic\n\
+  quantifier instantiation.  For example, the trigger P( x ) in the quantified \n\
+  formula forall( x ). ( P( x ) V ~Q( x ) ) will only be matched with ground\n\
+  terms P( t ) where P( t ) is in the equivalence class of false, and likewise\n\
+  Q( x ) with Q( s ) where Q( s ) is in the equivalence class of true.\n\
+\n\
+";
+
+inline InstWhenMode stringToInstWhenMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
+  if(optarg == "pre-full") {
+    return INST_WHEN_PRE_FULL;
+  } else if(optarg == "full") {
+    return INST_WHEN_FULL;
+  } else if(optarg == "full-last-call") {
+    return INST_WHEN_FULL_LAST_CALL;
+  } else if(optarg == "last-call") {
+    return INST_WHEN_LAST_CALL;
+  } else if(optarg == "help") {
+    puts(instWhenHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --inst-when: `") +
+                          optarg + "'.  Try --inst-when help.");
+  }
+}
+
+inline void checkInstWhenMode(std::string option, InstWhenMode mode, SmtEngine* smt) throw(OptionException) {
+  if(mode == INST_WHEN_PRE_FULL) {
+    throw OptionException(std::string("Mode pre-full for ") + option + " is not supported in this release.");
+  }
+}
+
+inline LiteralMatchMode stringToLiteralMatchMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
+  if(optarg ==  "none") {
+    return LITERAL_MATCH_NONE;
+  } else if(optarg ==  "predicate") {
+    return LITERAL_MATCH_PREDICATE;
+  } else if(optarg ==  "equality") {
+    return LITERAL_MATCH_EQUALITY;
+  } else if(optarg ==  "help") {
+    puts(literalMatchHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --literal-matching: `") +
+                          optarg + "'.  Try --literal-matching help.");
+  }
+}
+
+inline void checkLiteralMatchMode(std::string option, LiteralMatchMode mode, SmtEngine* smt) throw(OptionException) {
+  if(mode == LITERAL_MATCH_EQUALITY) {
+    throw OptionException(std::string("Mode equality for ") + option + " is not supported in this release.");
+  }
+}
+
+}/* CVC4::theory::quantifiers namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__OPTIONS_HANDLERS_H */
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index c397e9d05..800fa910c 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -15,6 +15,7 @@
  **/
 
 #include "theory/quantifiers/quantifiers_rewriter.h"
+#include "theory/quantifiers/options.h"
 
 using namespace std;
 using namespace CVC4;
@@ -690,14 +691,14 @@ Node QuantifiersRewriter::rewriteQuant( Node n, bool isNested, bool duringRewrit
 }
 
 bool QuantifiersRewriter::doMiniscopingNoFreeVar(){
-  return Options::current()->miniscopeQuantFreeVar;
+  return options::miniscopeQuantFreeVar();
 }
 
 bool QuantifiersRewriter::doMiniscopingAnd(){
-  if( Options::current()->miniscopeQuant ){
+  if( options::miniscopeQuant() ){
     return true;
   }else{
-    if( Options::current()->cbqi ){
+    if( options::cbqi() ){
       return true;
     }else{
       return false;
@@ -709,13 +710,13 @@ bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption,
   if( computeOption==COMPUTE_NNF ){
     return false;//TODO: compute NNF (current bad idea since arithmetic rewrites equalities)
   }else if( computeOption==COMPUTE_PRE_SKOLEM ){
-    return Options::current()->preSkolemQuant && !duringRewrite;
+    return options::preSkolemQuant() && !duringRewrite;
   }else if( computeOption==COMPUTE_PRENEX ){
-    return Options::current()->prenexQuant;
+    return options::prenexQuant();
   }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
-    return Options::current()->varElimQuant;
+    return options::varElimQuant();
   }else if( computeOption==COMPUTE_CNF ){
-    return Options::current()->cnfQuant && !duringRewrite;// || Options::current()->finiteModelFind;
+    return options::cnfQuant() && !duringRewrite;// || options::finiteModelFind();
   }else{
     return false;
   }
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 945c82bf9..bb8fafb14 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -61,7 +61,7 @@ void TermDb::addTermEfficient( Node n, std::set< Node >& added){
 
 void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
   //don't add terms in quantifier bodies
-  if( withinQuant && !Options::current()->registerQuantBodyTerms ){
+  if( withinQuant && !options::registerQuantBodyTerms() ){
     return;
   }
   if( d_processed.find( n )==d_processed.end() ){
@@ -82,7 +82,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
         uf::InstantiatorTheoryUf* d_ith = (uf::InstantiatorTheoryUf*)d_quantEngine->getInstantiator( THEORY_UF );
         for( int i=0; i<(int)n.getNumChildren(); i++ ){
           addTerm( n[i], added, withinQuant );
-          if( Options::current()->efficientEMatching ){
+          if( options::efficientEMatching() ){
             if( d_parents[n[i]][op].empty() ){
               //must add parent to equivalence class info
               Node nir = d_ith->getRepresentative( n[i] );
@@ -97,7 +97,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
               Assert(!getParents(n[i],op,i).empty());
             }
           }
-          if( Options::current()->eagerInstQuant ){
+          if( options::eagerInstQuant() ){
             if( !n.hasAttribute(InstLevelAttribute()) && n.getAttribute(InstLevelAttribute())==0 ){
               int addedLemmas = 0;
               for( int i=0; i<(int)d_ith->d_op_triggers[op].size(); i++ ){
@@ -115,7 +115,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
       }
     }
   }else{
-    if( Options::current()->efficientEMatching && !n.hasAttribute(InstConstantAttribute())){
+    if( options::efficientEMatching() && !n.hasAttribute(InstConstantAttribute())){
       //Efficient e-matching must be notified
       //The term in triggers are not important here
       Debug("term-db") << "New in this branch term " << n << std::endl;
@@ -196,7 +196,7 @@ Node TermDb::getModelBasisTerm( TypeNode tn, int i ){
     Node mbt;
     if( d_type_map[ tn ].empty() ){
       std::stringstream ss;
-      ss << Expr::setlanguage(Options::current()->outputLanguage);
+      ss << Expr::setlanguage(options::outputLanguage());
       ss << "e_" << tn;
       mbt = NodeManager::currentNM()->mkVar( ss.str(), tn );
     }else{
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 27310e21b..3d41d28b7 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -27,6 +27,7 @@
 #include <map>
 #include <time.h>
 #include "theory/quantifiers/theory_quantifiers_instantiator.h"
+#include "theory/quantifiers/options.h"
 #include "theory/quantifiers/term_database.h"
 
 using namespace std;
diff --git a/src/theory/quantifiers/theory_quantifiers_instantiator.cpp b/src/theory/quantifiers/theory_quantifiers_instantiator.cpp
index 84b6c65c7..8486a3a84 100644
--- a/src/theory/quantifiers/theory_quantifiers_instantiator.cpp
+++ b/src/theory/quantifiers/theory_quantifiers_instantiator.cpp
@@ -16,6 +16,7 @@
 
 #include "theory/quantifiers/theory_quantifiers_instantiator.h"
 #include "theory/quantifiers/theory_quantifiers.h"
+#include "theory/quantifiers/options.h"
 #include "theory/theory_engine.h"
 
 using namespace std;
@@ -32,7 +33,7 @@ Instantiator( c, ie, th ){
 
 void InstantiatorTheoryQuantifiers::assertNode( Node assertion ){
   Debug("quant-quant-assert") << "InstantiatorTheoryQuantifiers::check: " << assertion << std::endl;
-  if( Options::current()->cbqi ){
+  if( options::cbqi() ){
     if( assertion.hasAttribute(InstConstantAttribute()) ){
       Debug("quant-quant-assert") << "   -> has constraints from " << assertion.getAttribute(InstConstantAttribute()) << std::endl;
       setHasConstraintsFrom( assertion.getAttribute(InstConstantAttribute()) );