src/options/options.h

   1 /*********************                                                        */
   2 /*! \file options.h
   3  ** \verbatim
   4  ** Original author: mdeters
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): dejan, cconway
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009-2012  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief Global (command-line, set-option, ...) parameters for SMT.
  13  **
  14  ** Global (command-line, set-option, ...) parameters for SMT.
  15  **/
  16
  17 #include "cvc4_public.h"
  18
  19 #ifndef __CVC4__OPTIONS__OPTIONS_H
  20 #define __CVC4__OPTIONS__OPTIONS_H
  21
  22 #include <iostream>
  23 #include <fstream>
  24 #include <string>
  25 #include <vector>
  26
  27 #include "options/option_exception.h"
  28 #include "util/language.h"
  29 #include "util/tls.h"
  30
  31 namespace CVC4 {
  32
  33 namespace options {
  34   struct OptionsHolder;
  35 }/* CVC4::options namespace */
  36
  37 class ExprStream;
  38 class NodeManager;
  39 class NodeManagerScope;
  40 class SmtEngine;
  41
  42 class CVC4_PUBLIC Options {
  43   /** The struct that holds all option values. */
  44   options::OptionsHolder* d_holder;
  45
  46   /** The current Options in effect */
  47   static CVC4_THREADLOCAL(Options*) s_current;
  48
  49   /** Low-level assignment function for options */
  50   template <class T>
  51   void assign(T, std::string option, std::string value, SmtEngine* smt);
  52   /** Low-level assignment function for bool-valued options */
  53   template <class T>
  54   void assignBool(T, std::string option, bool value, SmtEngine* smt);
  55
  56   friend class NodeManager;
  57   friend class NodeManagerScope;
  58   friend class SmtEngine;
  59
  60 public:
  61
  62   /** Get the current Options in effect */
  63   static inline Options& current() {
  64     return *s_current;
  65   }
  66
  67   Options();
  68   Options(const Options& options);
  69   ~Options();
  70
  71   /**
  72    * Set the value of the given option.  Use of this default
  73    * implementation causes a compile-time error; write-able
  74    * options specialize this template with a real implementation.
  75    */
  76   template <class T>
  77   void set(T, const typename T::type&) {
  78     // Flag a compile-time error.  Write-able options specialize
  79     // this template to provide an implementation.
  80     T::you_are_trying_to_assign_to_a_read_only_option;
  81   }
  82
  83   /** Get the value of the given option.  Const access only. */
  84   template <class T>
  85   const typename T::type& operator[](T) const;
  86
  87   /**
  88    * Returns true iff the value of the given option was set
  89    * by the user via a command-line option or SmtEngine::setOption().
  90    * (Options::set() is low-level and doesn't count.)  Returns false
  91    * otherwise.
  92    */
  93   template <class T>
  94   bool wasSetByUser(T) const;
  95
  96   /**
  97    * Get a description of the command-line flags accepted by
  98    * parseOptions.  The returned string will be escaped so that it is
  99    * suitable as an argument to printf. */
 100   std::string getDescription() const;
 101
 102   /**
 103    * Print overall command-line option usage message, prefixed by
 104    * "msg"---which could be an error message causing the usage
 105    * output in the first place, e.g. "no such option --foo"
 106    */
 107   static void printUsage(const std::string msg, std::ostream& out);
 108
 109   /**
 110    * Print command-line option usage message for only the most-commonly
 111    * used options.  The message is prefixed by "msg"---which could be
 112    * an error message causing the usage output in the first place, e.g.
 113    * "no such option --foo"
 114    */
 115   static void printShortUsage(const std::string msg, std::ostream& out);
 116
 117   /** Print help for the --lang command line option */
 118   static void printLanguageHelp(std::ostream& out);
 119
 120   /**
 121    * Initialize the options based on the given command-line arguments.
 122    * The return value is what's left of the command line (that is, the
 123    * non-option arguments).
 124    */
 125   std::vector<std::string> parseOptions(int argc, char* argv[]) throw(OptionException);
 126
 127 };/* class Options */
 128
 129 }/* CVC4 namespace */
 130
 131 #include "options/base_options.h"
 132
 133 #endif /* __CVC4__OPTIONS__OPTIONS_H */