src/options/options.h

   1 /*********************                                                        */
   2 /*! \file options.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Tim King, Morgan Deters, Paul Meng
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing 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 <fstream>
  23 #include <ostream>
  24 #include <string>
  25 #include <vector>
  26
  27 #include "base/listener.h"
  28 #include "base/modal_exception.h"
  29 #include "base/tls.h"
  30 #include "options/argument_extender.h"
  31 #include "options/language.h"
  32 #include "options/option_exception.h"
  33 #include "options/printer_modes.h"
  34
  35 namespace CVC4 {
  36
  37 namespace options {
  38   struct OptionsHolder;
  39   class OptionsHandler;
  40 }/* CVC4::options namespace */
  41
  42 class CVC4_PUBLIC Options {
  43   /** The struct that holds all option values. */
  44   options::OptionsHolder* d_holder;
  45
  46   /** The handler for the options of the theory. */
  47   options::OptionsHandler* d_handler;
  48
  49   /** The current Options in effect */
  50   static CVC4_THREAD_LOCAL Options* s_current;
  51
  52   /** Listeners for options::forceLogicString being set. */
  53   ListenerCollection d_forceLogicListeners;
  54
  55   /** Listeners for notifyBeforeSearch. */
  56   ListenerCollection d_beforeSearchListeners;
  57
  58   /** Listeners for options::tlimit. */
  59   ListenerCollection d_tlimitListeners;
  60
  61   /** Listeners for options::tlimit-per. */
  62   ListenerCollection d_tlimitPerListeners;
  63
  64   /** Listeners for options::rlimit. */
  65   ListenerCollection d_rlimitListeners;
  66
  67   /** Listeners for options::tlimit-per. */
  68   ListenerCollection d_rlimitPerListeners;
  69
  70   /** Listeners for options::useTheoryList. */
  71   ListenerCollection d_useTheoryListListeners;
  72
  73   /** Listeners for options::defaultExprDepth. */
  74   ListenerCollection d_setDefaultExprDepthListeners;
  75
  76   /** Listeners for options::defaultDagThresh. */
  77   ListenerCollection d_setDefaultDagThreshListeners;
  78
  79   /** Listeners for options::printExprTypes. */
  80   ListenerCollection d_setPrintExprTypesListeners;
  81
  82   /** Listeners for options::dumpModeString. */
  83   ListenerCollection d_setDumpModeListeners;
  84
  85   /** Listeners for options::printSuccess. */
  86   ListenerCollection d_setPrintSuccessListeners;
  87
  88   /** Listeners for options::dumpToFileName. */
  89   ListenerCollection d_dumpToFileListeners;
  90
  91   /** Listeners for options::regularChannelName. */
  92   ListenerCollection d_setRegularChannelListeners;
  93
  94   /** Listeners for options::diagnosticChannelName. */
  95   ListenerCollection d_setDiagnosticChannelListeners;
  96
  97   /** Listeners for options::replayFilename. */
  98   ListenerCollection d_setReplayFilenameListeners;
  99
 100
 101   static ListenerCollection::Registration* registerAndNotify(
 102       ListenerCollection& collection, Listener* listener, bool notify);
 103
 104   /** Low-level assignment function for options */
 105   template <class T>
 106   void assign(T, std::string option, std::string value);
 107   /** Low-level assignment function for bool-valued options */
 108   template <class T>
 109   void assignBool(T, std::string option, bool value);
 110
 111   friend class options::OptionsHandler;
 112
 113   /**
 114    * Options cannot be copied as they are given an explicit list of
 115    * Listeners to respond to.
 116    */
 117   Options(const Options& options) CVC4_UNDEFINED;
 118
 119   /**
 120    * Options cannot be assigned as they are given an explicit list of
 121    * Listeners to respond to.
 122    */
 123   Options& operator=(const Options& options) CVC4_UNDEFINED;
 124
 125   static std::string formatThreadOptionException(const std::string& option);
 126
 127   static const size_t s_maxoptlen = 128;
 128   static const unsigned s_preemptAdditional = 6;
 129
 130 public:
 131   class CVC4_PUBLIC OptionsScope {
 132   private:
 133     Options* d_oldOptions;
 134   public:
 135     OptionsScope(Options* newOptions) :
 136         d_oldOptions(Options::s_current)
 137     {
 138       Options::s_current = newOptions;
 139     }
 140     ~OptionsScope(){
 141       Options::s_current = d_oldOptions;
 142     }
 143   };
 144
 145   /** Return true if current Options are null */
 146   static inline bool isCurrentNull() {
 147     return s_current == NULL;
 148   }
 149
 150   /** Get the current Options in effect */
 151   static inline Options* current() {
 152     return s_current;
 153   }
 154
 155   Options();
 156   ~Options();
 157
 158   /**
 159    * Copies the value of the options stored in OptionsHolder into the current
 160    * Options object.
 161    * This does not copy the listeners in the Options object.
 162    */
 163   void copyValues(const Options& options);
 164
 165   /**
 166    * Set the value of the given option.  Use of this default
 167    * implementation causes a compile-time error; write-able
 168    * options specialize this template with a real implementation.
 169    */
 170   template <class T>
 171   void set(T, const typename T::type&) {
 172     // Flag a compile-time error.  Write-able options specialize
 173     // this template to provide an implementation.
 174     T::you_are_trying_to_assign_to_a_read_only_option;
 175   }
 176
 177   /**
 178    * Set the value of the given option by key.
 179    */
 180   void setOption(const std::string& key, const std::string& optionarg)
 181       throw(OptionException, ModalException);
 182
 183
 184   /** Get the value of the given option.  Const access only. */
 185   template <class T>
 186   const typename T::type& operator[](T) const;
 187
 188   /**
 189    * Gets the value of the given option by key and returns value as a string.
 190    */
 191   std::string getOption(const std::string& key) const
 192     throw(OptionException);
 193
 194   // Get accessor functions.
 195   InputLanguage getInputLanguage() const;
 196   InstFormatMode getInstFormatMode() const;
 197   OutputLanguage getOutputLanguage() const;
 198   bool getCheckProofs() const;
 199   bool getContinuedExecution() const;
 200   bool getDumpInstantiations() const;
 201   bool getDumpModels() const;
 202   bool getDumpProofs() const;
 203   bool getDumpSynth() const;
 204   bool getDumpUnsatCores() const;
 205   bool getEarlyExit() const;
 206   bool getFallbackSequential() const;
 207   bool getFilesystemAccess() const;
 208   bool getForceNoLimitCpuWhileDump() const;
 209   bool getHelp() const;
 210   bool getIncrementalParallel() const;
 211   bool getIncrementalSolving() const;
 212   bool getInteractive() const;
 213   bool getInteractivePrompt() const;
 214   bool getLanguageHelp() const;
 215   bool getMemoryMap() const;
 216   bool getParseOnly() const;
 217   bool getProduceModels() const;
 218   bool getProof() const;
 219   bool getSegvSpin() const;
 220   bool getSemanticChecks() const;
 221   bool getStatistics() const;
 222   bool getStatsEveryQuery() const;
 223   bool getStatsHideZeros() const;
 224   bool getStrictParsing() const;
 225   int getTearDownIncremental() const;
 226   bool getVersion() const;
 227   bool getWaitToJoin() const;
 228   const std::string& getForceLogicString() const;
 229   const std::vector<std::string>& getThreadArgv() const;
 230   int getSharingFilterByLength() const;
 231   int getThreadId() const;
 232   int getVerbosity() const;
 233   std::istream* getIn() const;
 234   std::ostream* getErr();
 235   std::ostream* getOut();
 236   std::ostream* getOutConst() const; // TODO: Remove this.
 237   std::string getBinaryName() const;
 238   std::string getReplayInputFilename() const;
 239   unsigned getParseStep() const;
 240   unsigned getThreadStackSize() const;
 241   unsigned getThreads() const;
 242
 243
 244   // TODO: Document these.
 245   void setInputLanguage(InputLanguage);
 246   void setInteractive(bool);
 247   void setOut(std::ostream*);
 248   void setOutputLanguage(OutputLanguage);
 249   void setSharingFilterByLength(int length);
 250   void setThreadId(int);
 251
 252   bool wasSetByUserCeGuidedInst() const;
 253   bool wasSetByUserDumpSynth() const;
 254   bool wasSetByUserEarlyExit() const;
 255   bool wasSetByUserForceLogicString() const;
 256   bool wasSetByUserIncrementalSolving() const;
 257   bool wasSetByUserInteractive() const;
 258   bool wasSetByUserThreadStackSize() const;
 259   bool wasSetByUserThreads() const;
 260
 261   // Static accessor functions.
 262   // TODO: Document these.
 263   static int currentGetSharingFilterByLength();
 264   static int currentGetThreadId();
 265   static std::ostream* currentGetOut();
 266
 267   /**
 268    * Returns true iff the value of the given option was set
 269    * by the user via a command-line option or SmtEngine::setOption().
 270    * (Options::set() is low-level and doesn't count.)  Returns false
 271    * otherwise.
 272    */
 273   template <class T>
 274   bool wasSetByUser(T) const;
 275
 276   /**
 277    * Get a description of the command-line flags accepted by
 278    * parseOptions.  The returned string will be escaped so that it is
 279    * suitable as an argument to printf. */
 280   std::string getDescription() const;
 281
 282   /**
 283    * Print overall command-line option usage message, prefixed by
 284    * "msg"---which could be an error message causing the usage
 285    * output in the first place, e.g. "no such option --foo"
 286    */
 287   static void printUsage(const std::string msg, std::ostream& out);
 288
 289   /**
 290    * Print command-line option usage message for only the most-commonly
 291    * used options.  The message is prefixed by "msg"---which could be
 292    * an error message causing the usage output in the first place, e.g.
 293    * "no such option --foo"
 294    */
 295   static void printShortUsage(const std::string msg, std::ostream& out);
 296
 297   /** Print help for the --lang command line option */
 298   static void printLanguageHelp(std::ostream& out);
 299
 300   /**
 301    * Look up long command-line option names that bear some similarity
 302    * to the given name.  Returns an empty string if there are no
 303    * suggestions.
 304    */
 305   static std::string suggestCommandLineOptions(const std::string& optionName);
 306
 307   /**
 308    * Look up SMT option names that bear some similarity to
 309    * the given name.  Don't include the initial ":".  This might be
 310    * useful in case of typos.  Can return an empty vector if there are
 311    * no suggestions.
 312    */
 313   static std::vector<std::string> suggestSmtOptions(
 314       const std::string& optionName);
 315
 316   /**
 317    * Initialize the Options object options based on the given
 318    * command-line arguments given in argc and argv.  The return value
 319    * is what's left of the command line (that is, the non-option
 320    * arguments).
 321    *
 322    * This function uses getopt_long() and is not thread safe.
 323    *
 324    * Preconditions: options and argv must be non-null.
 325    */
 326   static std::vector<std::string> parseOptions(Options* options,
 327                                                int argc, char* argv[])
 328     throw(OptionException);
 329
 330   /**
 331    * Get the setting for all options.
 332    */
 333   std::vector<std::vector<std::string> > getOptions() const;
 334
 335   /**
 336    * Registers a listener for the notification, notifyBeforeSearch.
 337    *
 338    * The memory for the Registration is controlled by the user and must
 339    * be destroyed before the Options object is.
 340    *
 341    * This has multiple usages so having a notifyIfSet flag does not add
 342    * clarity. Users should check the relevant flags before registering this.
 343    */
 344   ListenerCollection::Registration* registerBeforeSearchListener(
 345       Listener* listener);
 346
 347
 348   /**
 349    * Registers a listener for options::forceLogic being set.
 350    *
 351    * If notifyIfSet is true, this calls notify on the listener
 352    * if the option was set by the user.
 353    *
 354    * The memory for the Registration is controlled by the user and must
 355    * be destroyed before the Options object is.
 356    */
 357   ListenerCollection::Registration* registerForceLogicListener(
 358       Listener* listener, bool notifyIfSet);
 359
 360   /**
 361    * Registers a listener for options::tlimit being set.
 362    *
 363    * If notifyIfSet is true, this calls notify on the listener
 364    * if the option was set by the user.
 365    *
 366    * The memory for the Registration is controlled by the user and must
 367    * be destroyed before the Options object is.
 368    */
 369   ListenerCollection::Registration* registerTlimitListener(
 370       Listener* listener, bool notifyIfSet);
 371
 372   /**
 373    * Registers a listener for options::tlimit-per being set.
 374    *
 375    * If notifyIfSet is true, this calls notify on the listener
 376    * if the option was set by the user.
 377    *
 378    * The memory for the Registration is controlled by the user and must
 379    * be destroyed before the Options object is.
 380    */
 381   ListenerCollection::Registration* registerTlimitPerListener(
 382       Listener* listener, bool notifyIfSet);
 383
 384
 385   /**
 386    * Registers a listener for options::rlimit being set.
 387    *
 388    * If notifyIfSet is true, this calls notify on the listener
 389    * if the option was set by the user.
 390    *
 391    * The memory for the Registration is controlled by the user and must
 392    * be destroyed before the Options object is.
 393    */
 394   ListenerCollection::Registration* registerRlimitListener(
 395       Listener* listener, bool notifyIfSet);
 396
 397   /**
 398    * Registers a listener for options::rlimit-per being set.
 399    *
 400    * If notifyIfSet is true, this calls notify on the listener
 401    * if the option was set by the user.
 402    *
 403    * The memory for the Registration is controlled by the user and must
 404    * be destroyed before the Options object is.
 405    */
 406   ListenerCollection::Registration* registerRlimitPerListener(
 407       Listener* listener, bool notifyIfSet);
 408
 409   /**
 410    * Registers a listener for options::useTheoryList being set.
 411    *
 412    * If notifyIfSet is true, this calls notify on the listener
 413    * if the option was set by the user.
 414    *
 415    * The memory for the Registration is controlled by the user and must
 416    * be destroyed before the Options object is.
 417    */
 418   ListenerCollection::Registration* registerUseTheoryListListener(
 419       Listener* listener, bool notifyIfSet);
 420
 421
 422   /**
 423    * Registers a listener for options::defaultExprDepth being set.
 424    *
 425    * If notifyIfSet is true, this calls notify on the listener
 426    * if the option was set by the user.
 427    *
 428    * The memory for the Registration is controlled by the user and must
 429    * be destroyed before the Options object is.
 430    */
 431   ListenerCollection::Registration* registerSetDefaultExprDepthListener(
 432       Listener* listener, bool notifyIfSet);
 433
 434   /**
 435    * Registers a listener for options::defaultDagThresh being set.
 436    *
 437    * If notifyIfSet is true, this calls notify on the listener
 438    * if the option was set by the user.
 439    *
 440    * The memory for the Registration is controlled by the user and must
 441    * be destroyed before the Options object is.
 442    */
 443   ListenerCollection::Registration* registerSetDefaultExprDagListener(
 444       Listener* listener, bool notifyIfSet);
 445
 446   /**
 447    * Registers a listener for options::printExprTypes being set.
 448    *
 449    * If notifyIfSet is true, this calls notify on the listener
 450    * if the option was set by the user.
 451    *
 452    * The memory for the Registration is controlled by the user and must
 453    * be destroyed before the Options object is.
 454    */
 455   ListenerCollection::Registration* registerSetPrintExprTypesListener(
 456       Listener* listener, bool notifyIfSet);
 457
 458   /**
 459    * Registers a listener for options::dumpModeString being set.
 460    *
 461    * If notifyIfSet is true, this calls notify on the listener
 462    * if the option was set by the user.
 463    *
 464    * The memory for the Registration is controlled by the user and must
 465    * be destroyed before the Options object is.
 466    */
 467   ListenerCollection::Registration* registerSetDumpModeListener(
 468       Listener* listener, bool notifyIfSet);
 469
 470   /**
 471    * Registers a listener for options::printSuccess being set.
 472    *
 473    * If notifyIfSet is true, this calls notify on the listener
 474    * if the option was set by the user.
 475    *
 476    * The memory for the Registration is controlled by the user and must
 477    * be destroyed before the Options object is.
 478    */
 479   ListenerCollection::Registration* registerSetPrintSuccessListener(
 480       Listener* listener, bool notifyIfSet);
 481
 482   /**
 483    * Registers a listener for options::dumpToFileName being set.
 484    *
 485    * If notifyIfSet is true, this calls notify on the listener
 486    * if the option was set by the user.
 487    *
 488    * The memory for the Registration is controlled by the user and must
 489    * be destroyed before the Options object is.
 490    */
 491   ListenerCollection::Registration* registerDumpToFileNameListener(
 492       Listener* listener, bool notifyIfSet);
 493
 494   /**
 495    * Registers a listener for options::regularChannelName being set.
 496    *
 497    * If notifyIfSet is true, this calls notify on the listener
 498    * if the option was set by the user.
 499    *
 500    * The memory for the Registration is controlled by the user and must
 501    * be destroyed before the Options object is.
 502    */
 503   ListenerCollection::Registration* registerSetRegularOutputChannelListener(
 504       Listener* listener, bool notifyIfSet);
 505
 506   /**
 507    * Registers a listener for options::diagnosticChannelName being set.
 508    *
 509    * If notifyIfSet is true, this calls notify on the listener
 510    * if the option was set by the user.
 511    *
 512    * The memory for the Registration is controlled by the user and must
 513    * be destroyed before the Options object is.
 514    */
 515   ListenerCollection::Registration* registerSetDiagnosticOutputChannelListener(
 516       Listener* listener, bool notifyIfSet);
 517
 518   /**
 519    * Registers a listener for options::replayLogFilename being set.
 520    *
 521    * If notifyIfSet is true, this calls notify on the listener
 522    * if the option was set by the user.
 523    *
 524    * The memory for the Registration is controlled by the user and must
 525    * be destroyed before the Options object is.
 526    */
 527   ListenerCollection::Registration* registerSetReplayLogFilename(
 528       Listener* listener, bool notifyIfSet);
 529
 530   /** Sends a std::flush to getErr(). */
 531   void flushErr();
 532
 533   /** Sends a std::flush to getOut(). */
 534   void flushOut();
 535
 536  private:
 537
 538   /**
 539    * Internal procedure for implementing the parseOptions function.
 540    * Initializes the options object based on the given command-line
 541    * arguments. This uses an ArgumentExtender containing the
 542    * command-line arguments. Nonoptions are stored into nonoptions.
 543    *
 544    * This is not thread safe.
 545    *
 546    * Preconditions: options, extender and nonoptions are non-null.
 547    */
 548   static void parseOptionsRecursive(Options* options,
 549                                     options::ArgumentExtender* extender,
 550                                     std::vector<std::string>* nonoptions)
 551     throw(OptionException);
 552 };/* class Options */
 553
 554 }/* CVC4 namespace */
 555
 556 #endif /* __CVC4__OPTIONS__OPTIONS_H */