1 files changed, 150 insertions, 0 deletions
diff --git a/src/options/options.h b/src/options/options.h
new file mode 100644
index 000000000..a3abdd54b
--- /dev/null
+++ b/src/options/options.h
@@ -0,0 +1,150 @@
+/*********************                                                        */
+/*! \file options.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** 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
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Global (command-line, set-option, ...) parameters for SMT.
+ **
+ ** Global (command-line, set-option, ...) parameters for SMT.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__OPTIONS__OPTIONS_H
+#define __CVC4__OPTIONS__OPTIONS_H
+
+#include <iostream>
+#include <fstream>
+#include <string>
+
+#include "util/exception.h"
+#include "util/language.h"
+#include "util/tls.h"
+
+namespace CVC4 {
+
+namespace options {
+  class OptionsHolder;
+}/* CVC4::options namespace */
+
+class ExprStream;
+class NodeManager;
+class NodeManagerScope;
+class SmtEngine;
+
+/** Class representing an option-parsing exception. */
+class CVC4_PUBLIC OptionException : public CVC4::Exception {
+public:
+  OptionException(const std::string& s) throw() :
+    CVC4::Exception("Error in option parsing: " + s) {
+  }
+};/* class OptionException */
+
+class CVC4_PUBLIC Options {
+  /** The struct that holds all option values. */
+  options::OptionsHolder* d_holder;
+
+  /** The current Options in effect */
+  static CVC4_THREADLOCAL(Options*) s_current;
+
+  /** Low-level assignment function for options */
+  template <class T>
+  void assign(T, std::string option, std::string value, SmtEngine* smt);
+  /** Low-level assignment function for bool-valued options */
+  template <class T>
+  void assignBool(T, std::string option, bool value, SmtEngine* smt);
+
+  friend class NodeManager;
+  friend class NodeManagerScope;
+  friend class SmtEngine;
+
+public:
+
+  /** Get the current Options in effect */
+  static inline Options& current() {
+    return *s_current;
+  }
+
+  Options();
+  Options(const Options& options);
+  ~Options();
+
+  /**
+   * Set the value of the given option.  Use of this default
+   * implementation causes a compile-time error; write-able
+   * options specialize this template with a real implementation.
+   */
+  template <class T>
+  void set(T, const typename T::type&) {
+    // Flag a compile-time error.  Write-able options specialize
+    // this template to provide an implementation.
+    T::you_are_trying_to_assign_to_a_read_only_option;
+  }
+
+  /** Get the value of the given option.  Const access only. */
+  template <class T>
+  const typename T::type& operator[](T) const;
+
+  /**
+   * Returns true iff the value of the given option was set
+   * by the user via a command-line option or SmtEngine::setOption().
+   * (Options::set() is low-level and doesn't count.)  Returns false
+   * otherwise.
+   */
+  template <class T>
+  bool wasSetByUser(T) const;
+
+  /**
+   * Get a description of the command-line flags accepted by
+   * parseOptions.  The returned string will be escaped so that it is
+   * suitable as an argument to printf. */
+  std::string getDescription() const;
+
+  /**
+   * Print overall command-line option usage message, prefixed by
+   * "msg"---which could be an error message causing the usage
+   * output in the first place, e.g. "no such option --foo"
+   */
+  static void printUsage(const std::string msg, std::ostream& out);
+
+  /**
+   * Print command-line option usage message for only the most-commonly
+   * used options.  The message is prefixed by "msg"---which could be
+   * an error message causing the usage output in the first place, e.g.
+   * "no such option --foo"
+   */
+  static void printShortUsage(const std::string msg, std::ostream& out);
+
+  /** Print help for the --lang command line option */
+  static void printLanguageHelp(std::ostream& out);
+
+  /**
+   * Initialize the options based on the given command-line arguments.
+   */
+  int parseOptions(int argc, char* argv[]) throw(OptionException);
+
+  /**
+   * Set the output language based on the given string.
+   */
+  void setOutputLanguage(const char* str) throw(OptionException);
+
+  /**
+   * Set the input language based on the given string.
+   */
+  void setInputLanguage(const char* str) throw(OptionException);
+
+};/* class Options */
+
+}/* CVC4 namespace */
+
+#include "options/base_options.h"
+
+#endif /* __CVC4__OPTIONS__OPTIONS_H */