1 files changed, 15 insertions, 39 deletions

diff --git a/src/util/options.h b/src/util/options.h
index ce2bc71e7..c4e115b08 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -2,8 +2,8 @@
 /*! \file options.h
  ** \verbatim
  ** Original author: mdeters
- ** Major contributors: cconway
- ** Minor contributors (to current version): dejan, taking
+ ** Major contributors: taking, cconway
+ ** Minor contributors (to current version): dejan
  ** 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
@@ -71,11 +71,8 @@ struct CVC4_PUBLIC Options {
   /** The input language */
   InputLanguage inputLanguage;
 
-  /** Enumeration of UF implementation choices */
-  typedef enum { TIM, MORGAN } UfImplementation;
-
-  /** Which implementation of uninterpreted function theory to use */
-  UfImplementation uf_implementation;
+  /** The output language */
+  OutputLanguage outputLanguage;
 
   /** Should we print the help message? */
   bool help;
@@ -112,21 +109,16 @@ struct CVC4_PUBLIC Options {
     /** Simplify the assertions as they come in */
     SIMPLIFICATION_MODE_INCREMENTAL,
     /** Simplify the assertions all together once a check is requested */
-    SIMPLIFICATION_MODE_BATCH
+    SIMPLIFICATION_MODE_BATCH,
+    /** Don't do simplification */
+    SIMPLIFICATION_MODE_NONE
   } SimplificationMode;
 
-  /** When to perform nonclausal simplifications. */
+  /** When/whether to perform nonclausal simplifications. */
   SimplificationMode simplificationMode;
 
-  /** Enumeration of simplification styles (how much to simplify). */
-  typedef enum {
-    AGGRESSIVE_SIMPLIFICATION_STYLE,
-    TOPLEVEL_SIMPLIFICATION_STYLE,
-    NO_SIMPLIFICATION_STYLE
-  } SimplificationStyle;
-
-  /** Style of nonclausal simplifications to perform. */
-  SimplificationStyle simplificationStyle;
+  /** Whether to perform the static learning pass. */
+  bool doStaticLearning;
 
   /** Whether we're in interactive mode or not */
   bool interactive;
@@ -229,34 +221,18 @@ struct CVC4_PUBLIC Options {
 };/* struct Options */
 
 inline std::ostream& operator<<(std::ostream& out,
-                                Options::UfImplementation uf) CVC4_PUBLIC;
-
-inline std::ostream& operator<<(std::ostream& out,
-                                Options::UfImplementation uf) {
-  switch(uf) {
-  case Options::TIM:
-    out << "TIM";
-    break;
-  case Options::MORGAN:
-    out << "MORGAN";
-    break;
-  default:
-    out << "UfImplementation:UNKNOWN![" << unsigned(uf) << "]";
-  }
-
-  return out;
-}
-
-inline std::ostream& operator<<(std::ostream& out,
                                 Options::SimplificationMode mode) CVC4_PUBLIC;
 inline std::ostream& operator<<(std::ostream& out,
                                 Options::SimplificationMode mode) {
   switch(mode) {
+  case Options::SIMPLIFICATION_MODE_INCREMENTAL:
+    out << "SIMPLIFICATION_MODE_INCREMENTAL";
+    break;
   case Options::SIMPLIFICATION_MODE_BATCH:
     out << "SIMPLIFICATION_MODE_BATCH";
     break;
-  case Options::SIMPLIFICATION_MODE_INCREMENTAL:
-    out << "SIMPLIFICATION_MODE_INCREMENTAL";
+  case Options::SIMPLIFICATION_MODE_NONE:
+    out << "SIMPLIFICATION_MODE_NONE";
     break;
   default:
     out << "SimplificationMode:UNKNOWN![" << unsigned(mode) << "]";