src/options/options.h

   1 /*********************                                                        */
   2 /*! \file options.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Tim King, Morgan Deters, Kshitij Bansal
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2016 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/printer_modes.h"
  33 #include "options/option_exception.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_THREADLOCAL(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 setCeGuidedInst(bool);
 246   void setDumpSynth(bool);
 247   void setInputLanguage(InputLanguage);
 248   void setInteractive(bool);
 249   void setOut(std::ostream*);
 250   void setOutputLanguage(OutputLanguage);
 251   void setSharingFilterByLength(int length);
 252   void setThreadId(int);
 253
 254   bool wasSetByUserCeGuidedInst() const;
 255   bool wasSetByUserDumpSynth() const;
 256   bool wasSetByUserEarlyExit() const;
 257   bool wasSetByUserForceLogicString() const;
 258   bool wasSetByUserIncrementalSolving() const;
 259   bool wasSetByUserInteractive() const;
 260   bool wasSetByUserThreadStackSize() const;
 261   bool wasSetByUserThreads() const;
 262
 263   // Static accessor functions.
 264   // TODO: Document these.
 265   static int currentGetSharingFilterByLength();
 266   static int currentGetThreadId();
 267   static std::ostream* currentGetOut();
 268
 269   /**
 270    * Returns true iff the value of the given option was set
 271    * by the user via a command-line option or SmtEngine::setOption().
 272    * (Options::set() is low-level and doesn't count.)  Returns false
 273    * otherwise.
 274    */
 275   template <class T>
 276   bool wasSetByUser(T) const;
 277
 278   /**
 279    * Get a description of the command-line flags accepted by
 280    * parseOptions.  The returned string will be escaped so that it is
 281    * suitable as an argument to printf. */
 282   std::string getDescription() const;
 283
 284   /**
 285    * Print overall command-line option usage message, prefixed by
 286    * "msg"---which could be an error message causing the usage
 287    * output in the first place, e.g. "no such option --foo"
 288    */
 289   static void printUsage(const std::string msg, std::ostream& out);
 290
 291   /**
 292    * Print command-line option usage message for only the most-commonly
 293    * used options.  The message is prefixed by "msg"---which could be
 294    * an error message causing the usage output in the first place, e.g.
 295    * "no such option --foo"
 296    */
 297   static void printShortUsage(const std::string msg, std::ostream& out);
 298
 299   /** Print help for the --lang command line option */
 300   static void printLanguageHelp(std::ostream& out);
 301
 302   /**
 303    * Look up long command-line option names that bear some similarity
 304    * to the given name.  Returns an empty string if there are no
 305    * suggestions.
 306    */
 307   static std::string suggestCommandLineOptions(const std::string& optionName) throw();
 308
 309   /**
 310    * Look up SMT option names that bear some similarity to
 311    * the given name.  Don't include the initial ":".  This might be
 312    * useful in case of typos.  Can return an empty vector if there are
 313    * no suggestions.
 314    */
 315   static std::vector<std::string> suggestSmtOptions(const std::string& optionName) throw();
 316
 317   /**
 318    * Initialize the Options object options based on the given
 319    * command-line arguments given in argc and argv.  The return value
 320    * is what's left of the command line (that is, the non-option
 321    * arguments).
 322    *
 323    * This function uses getopt_long() and is not thread safe.
 324    *
 325    * Preconditions: options and argv must be non-null.
 326    */
 327   static std::vector<std::string> parseOptions(Options* options,
 328                                                int argc, char* argv[])
 329     throw(OptionException);
 330
 331   /**
 332    * Get the setting for all options.
 333    */
 334   std::vector< std::vector<std::string> > getOptions() const throw();
 335
 336
 337   /**
 338    * Registers a listener for the notification, notifyBeforeSearch.
 339    *
 340    * The memory for the Registration is controlled by the user and must
 341    * be destroyed before the Options object is.
 342    *
 343    * This has multiple usages so having a notifyIfSet flag does not add
 344    * clarity. Users should check the relevant flags before registering this.
 345    */
 346   ListenerCollection::Registration* registerBeforeSearchListener(
 347       Listener* listener);
 348
 349
 350   /**
 351    * Registers a listener for options::forceLogic being set.
 352    *
 353    * If notifyIfSet is true, this calls notify on the listener
 354    * if the option was set by the user.
 355    *
 356    * The memory for the Registration is controlled by the user and must
 357    * be destroyed before the Options object is.
 358    */
 359   ListenerCollection::Registration* registerForceLogicListener(
 360       Listener* listener, bool notifyIfSet);
 361
 362   /**
 363    * Registers a listener for options::tlimit being set.
 364    *
 365    * If notifyIfSet is true, this calls notify on the listener
 366    * if the option was set by the user.
 367    *
 368    * The memory for the Registration is controlled by the user and must
 369    * be destroyed before the Options object is.
 370    */
 371   ListenerCollection::Registration* registerTlimitListener(
 372       Listener* listener, bool notifyIfSet);
 373
 374   /**
 375    * Registers a listener for options::tlimit-per being set.
 376    *
 377    * If notifyIfSet is true, this calls notify on the listener
 378    * if the option was set by the user.
 379    *
 380    * The memory for the Registration is controlled by the user and must
 381    * be destroyed before the Options object is.
 382    */
 383   ListenerCollection::Registration* registerTlimitPerListener(
 384       Listener* listener, bool notifyIfSet);
 385
 386
 387   /**
 388    * Registers a listener for options::rlimit being set.
 389    *
 390    * If notifyIfSet is true, this calls notify on the listener
 391    * if the option was set by the user.
 392    *
 393    * The memory for the Registration is controlled by the user and must
 394    * be destroyed before the Options object is.
 395    */
 396   ListenerCollection::Registration* registerRlimitListener(
 397       Listener* listener, bool notifyIfSet);
 398
 399   /**
 400    * Registers a listener for options::rlimit-per being set.
 401    *
 402    * If notifyIfSet is true, this calls notify on the listener
 403    * if the option was set by the user.
 404    *
 405    * The memory for the Registration is controlled by the user and must
 406    * be destroyed before the Options object is.
 407    */
 408   ListenerCollection::Registration* registerRlimitPerListener(
 409       Listener* listener, bool notifyIfSet);
 410
 411   /**
 412    * Registers a listener for options::useTheoryList being set.
 413    *
 414    * If notifyIfSet is true, this calls notify on the listener
 415    * if the option was set by the user.
 416    *
 417    * The memory for the Registration is controlled by the user and must
 418    * be destroyed before the Options object is.
 419    */
 420   ListenerCollection::Registration* registerUseTheoryListListener(
 421       Listener* listener, bool notifyIfSet);
 422
 423
 424   /**
 425    * Registers a listener for options::defaultExprDepth being set.
 426    *
 427    * If notifyIfSet is true, this calls notify on the listener
 428    * if the option was set by the user.
 429    *
 430    * The memory for the Registration is controlled by the user and must
 431    * be destroyed before the Options object is.
 432    */
 433   ListenerCollection::Registration* registerSetDefaultExprDepthListener(
 434       Listener* listener, bool notifyIfSet);
 435
 436   /**
 437    * Registers a listener for options::defaultDagThresh being set.
 438    *
 439    * If notifyIfSet is true, this calls notify on the listener
 440    * if the option was set by the user.
 441    *
 442    * The memory for the Registration is controlled by the user and must
 443    * be destroyed before the Options object is.
 444    */
 445   ListenerCollection::Registration* registerSetDefaultExprDagListener(
 446       Listener* listener, bool notifyIfSet);
 447
 448   /**
 449    * Registers a listener for options::printExprTypes being set.
 450    *
 451    * If notifyIfSet is true, this calls notify on the listener
 452    * if the option was set by the user.
 453    *
 454    * The memory for the Registration is controlled by the user and must
 455    * be destroyed before the Options object is.
 456    */
 457   ListenerCollection::Registration* registerSetPrintExprTypesListener(
 458       Listener* listener, bool notifyIfSet);
 459
 460   /**
 461    * Registers a listener for options::dumpModeString being set.
 462    *
 463    * If notifyIfSet is true, this calls notify on the listener
 464    * if the option was set by the user.
 465    *
 466    * The memory for the Registration is controlled by the user and must
 467    * be destroyed before the Options object is.
 468    */
 469   ListenerCollection::Registration* registerSetDumpModeListener(
 470       Listener* listener, bool notifyIfSet);
 471
 472   /**
 473    * Registers a listener for options::printSuccess being set.
 474    *
 475    * If notifyIfSet is true, this calls notify on the listener
 476    * if the option was set by the user.
 477    *
 478    * The memory for the Registration is controlled by the user and must
 479    * be destroyed before the Options object is.
 480    */
 481   ListenerCollection::Registration* registerSetPrintSuccessListener(
 482       Listener* listener, bool notifyIfSet);
 483
 484   /**
 485    * Registers a listener for options::dumpToFileName being set.
 486    *
 487    * If notifyIfSet is true, this calls notify on the listener
 488    * if the option was set by the user.
 489    *
 490    * The memory for the Registration is controlled by the user and must
 491    * be destroyed before the Options object is.
 492    */
 493   ListenerCollection::Registration* registerDumpToFileNameListener(
 494       Listener* listener, bool notifyIfSet);
 495
 496   /**
 497    * Registers a listener for options::regularChannelName being set.
 498    *
 499    * If notifyIfSet is true, this calls notify on the listener
 500    * if the option was set by the user.
 501    *
 502    * The memory for the Registration is controlled by the user and must
 503    * be destroyed before the Options object is.
 504    */
 505   ListenerCollection::Registration* registerSetRegularOutputChannelListener(
 506       Listener* listener, bool notifyIfSet);
 507
 508   /**
 509    * Registers a listener for options::diagnosticChannelName being set.
 510    *
 511    * If notifyIfSet is true, this calls notify on the listener
 512    * if the option was set by the user.
 513    *
 514    * The memory for the Registration is controlled by the user and must
 515    * be destroyed before the Options object is.
 516    */
 517   ListenerCollection::Registration* registerSetDiagnosticOutputChannelListener(
 518       Listener* listener, bool notifyIfSet);
 519
 520   /**
 521    * Registers a listener for options::replayLogFilename being set.
 522    *
 523    * If notifyIfSet is true, this calls notify on the listener
 524    * if the option was set by the user.
 525    *
 526    * The memory for the Registration is controlled by the user and must
 527    * be destroyed before the Options object is.
 528    */
 529   ListenerCollection::Registration* registerSetReplayLogFilename(
 530       Listener* listener, bool notifyIfSet);
 531
 532   /** Sends a std::flush to getErr(). */
 533   void flushErr();
 534
 535   /** Sends a std::flush to getOut(). */
 536   void flushOut();
 537
 538  private:
 539
 540   /**
 541    * Internal procedure for implementing the parseOptions function.
 542    * Initializes the options object based on the given command-line
 543    * arguments. This uses an ArgumentExtender containing the
 544    * command-line arguments. Nonoptions are stored into nonoptions.
 545    *
 546    * This is not thread safe.
 547    *
 548    * Preconditions: options, extender and nonoptions are non-null.
 549    */
 550   static void parseOptionsRecursive(Options* options,
 551                                     options::ArgumentExtender* extender,
 552                                     std::vector<std::string>* nonoptions)
 553     throw(OptionException);
 554 };/* class Options */
 555
 556 }/* CVC4 namespace */
 557
 558 #endif /* __CVC4__OPTIONS__OPTIONS_H */