src/options/options.h

   1 /*********************                                                        */
   2 /*! \file options.h
   3  ** \verbatim
   4  ** Original author: Morgan Deters
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2013  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 #include "util/sexpr.h"
  31
  32 namespace CVC4 {
  33
  34 namespace options {
  35   struct OptionsHolder;
  36 }/* CVC4::options namespace */
  37
  38 class ExprStream;
  39 class NodeManager;
  40 class NodeManagerScope;
  41 class SmtEngine;
  42
  43 class CVC4_PUBLIC Options {
  44   /** The struct that holds all option values. */
  45   options::OptionsHolder* d_holder;
  46
  47   /** The current Options in effect */
  48   static CVC4_THREADLOCAL(Options*) s_current;
  49
  50   /** Low-level assignment function for options */
  51   template <class T>
  52   void assign(T, std::string option, std::string value, SmtEngine* smt);
  53   /** Low-level assignment function for bool-valued options */
  54   template <class T>
  55   void assignBool(T, std::string option, bool value, SmtEngine* smt);
  56
  57   friend class NodeManager;
  58   friend class NodeManagerScope;
  59   friend class SmtEngine;
  60
  61 public:
  62
  63   /** Get the current Options in effect */
  64   static inline Options& current() {
  65     return *s_current;
  66   }
  67
  68   Options();
  69   Options(const Options& options);
  70   ~Options();
  71
  72   /**
  73    * Set the value of the given option.  Use of this default
  74    * implementation causes a compile-time error; write-able
  75    * options specialize this template with a real implementation.
  76    */
  77   template <class T>
  78   void set(T, const typename T::type&) {
  79     // Flag a compile-time error.  Write-able options specialize
  80     // this template to provide an implementation.
  81     T::you_are_trying_to_assign_to_a_read_only_option;
  82   }
  83
  84   /** Get the value of the given option.  Const access only. */
  85   template <class T>
  86   const typename T::type& operator[](T) const;
  87
  88   /**
  89    * Returns true iff the value of the given option was set
  90    * by the user via a command-line option or SmtEngine::setOption().
  91    * (Options::set() is low-level and doesn't count.)  Returns false
  92    * otherwise.
  93    */
  94   template <class T>
  95   bool wasSetByUser(T) const;
  96
  97   /**
  98    * Get a description of the command-line flags accepted by
  99    * parseOptions.  The returned string will be escaped so that it is
 100    * suitable as an argument to printf. */
 101   std::string getDescription() const;
 102
 103   /**
 104    * Print overall command-line option usage message, prefixed by
 105    * "msg"---which could be an error message causing the usage
 106    * output in the first place, e.g. "no such option --foo"
 107    */
 108   static void printUsage(const std::string msg, std::ostream& out);
 109
 110   /**
 111    * Print command-line option usage message for only the most-commonly
 112    * used options.  The message is prefixed by "msg"---which could be
 113    * an error message causing the usage output in the first place, e.g.
 114    * "no such option --foo"
 115    */
 116   static void printShortUsage(const std::string msg, std::ostream& out);
 117
 118   /** Print help for the --lang command line option */
 119   static void printLanguageHelp(std::ostream& out);
 120
 121   /**
 122    * Look up long command-line option names that bear some similarity to
 123    * the given name.  Don't include the initial "--".  This might be
 124    * useful in case of typos.  Can return an empty vector if there are
 125    * no suggestions.
 126    */
 127   static std::vector<std::string> suggestCommandLineOptions(const std::string& optionName) throw();
 128
 129   /**
 130    * Look up SMT option names that bear some similarity to
 131    * the given name.  Don't include the initial ":".  This might be
 132    * useful in case of typos.  Can return an empty vector if there are
 133    * no suggestions.
 134    */
 135   static std::vector<std::string> suggestSmtOptions(const std::string& optionName) throw();
 136
 137   /**
 138    * Initialize the options based on the given command-line arguments.
 139    * The return value is what's left of the command line (that is, the
 140    * non-option arguments).
 141    */
 142   std::vector<std::string> parseOptions(int argc, char* argv[]) throw(OptionException);
 143
 144   /**
 145    * Get the setting for all options.
 146    */
 147   SExpr getOptions() const throw();
 148
 149 };/* class Options */
 150
 151 }/* CVC4 namespace */
 152
 153 #include "options/base_options.h"
 154
 155 #endif /* __CVC4__OPTIONS__OPTIONS_H */