src/options/options_handler.h

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Tim King, Mathias Preiner, Aina Niemetz
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 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.
  11  * ****************************************************************************
  12  *
  13  * Interface for custom handlers and predicates options.
  14  */
  15
  16 #include "cvc5_private.h"
  17
  18 #ifndef CVC5__OPTIONS__OPTIONS_HANDLER_H
  19 #define CVC5__OPTIONS__OPTIONS_HANDLER_H
  20
  21 #include <ostream>
  22 #include <sstream>
  23 #include <string>
  24
  25 #include "options/base_options.h"
  26 #include "options/bv_options.h"
  27 #include "options/decision_options.h"
  28 #include "options/language.h"
  29 #include "options/managed_streams.h"
  30 #include "options/option_exception.h"
  31 #include "options/quantifiers_options.h"
  32
  33 namespace cvc5 {
  34
  35 class Options;
  36
  37 namespace options {
  38
  39 /**
  40  * Class that responds to command line options being set.
  41  *
  42  * Most functions can throw an OptionException on failure.
  43  */
  44 class OptionsHandler
  45 {
  46  public:
  47   OptionsHandler(Options* options);
  48
  49   template <typename T>
  50   void checkMinimum(const std::string& flag, T value, T minimum) const
  51   {
  52     if (value < minimum)
  53     {
  54       std::stringstream ss;
  55       ss << flag << " = " << value
  56          << " is not a legal setting, value should be at least " << minimum
  57          << ".";
  58       throw OptionException(ss.str());
  59     }
  60   }
  61   template <typename T>
  62   void checkMaximum(const std::string& flag, T value, T maximum) const
  63   {
  64     if (value > maximum)
  65     {
  66       std::stringstream ss;
  67       ss << flag << " = " << value
  68          << " is not a legal setting, value should be at most " << maximum
  69          << ".";
  70       throw OptionException(ss.str());
  71     }
  72   }
  73
  74   /******************************* base options *******************************/
  75   /** Apply the error output stream to the different output channels */
  76   void setErrStream(const std::string& flag, const ManagedErr& me);
  77
  78   /** Convert option value to Language enum */
  79   Language stringToLanguage(const std::string& flag, const std::string& optarg);
  80   /** Check that lang is not LANG_AST (not allowed as input language) */
  81   void languageIsNotAST(const std::string& flag, Language lang);
  82   /** Apply the output language to the default output stream */
  83   void applyOutputLanguage(const std::string& flag, Language lang);
  84   /** Apply verbosity to the different output channels */
  85   void setVerbosity(const std::string& flag, int value);
  86   /** Decrease verbosity and call setVerbosity */
  87   void decreaseVerbosity(const std::string& flag, bool value);
  88   /** Increase verbosity and call setVerbosity */
  89   void increaseVerbosity(const std::string& flag, bool value);
  90   /** If statistics are disabled, disable statistics sub-options */
  91   void setStats(const std::string& flag, bool value);
  92   /** If statistics sub-option is disabled, enable statistics */
  93   void setStatsDetail(const std::string& flag, bool value);
  94   /** Enable a particular trace tag */
  95   void enableTraceTag(const std::string& flag, const std::string& optarg);
  96   /** Enable a particular debug tag */
  97   void enableDebugTag(const std::string& flag, const std::string& optarg);
  98   /** Enable a particular output tag */
  99   void enableOutputTag(const std::string& flag, OutputTag optarg);
 100   /** Apply print success flag to the different output channels */
 101   void setPrintSuccess(const std::string& flag, bool value);
 102   /** Pass the resource weight specification to the resource manager */
 103   void setResourceWeight(const std::string& flag, const std::string& optarg);
 104
 105   /******************************* bv options *******************************/
 106
 107   /** Check that abc is enabled */
 108   void abcEnabledBuild(const std::string& flag, bool value);
 109   /** Check that abc is enabled */
 110   void abcEnabledBuild(const std::string& flag, const std::string& value);
 111   /** Check that the sat solver mode is compatible with other bv options */
 112   void checkBvSatSolver(const std::string& flag, SatSolverMode m);
 113   /** Check that we use eager bitblasting for aig */
 114   void setBitblastAig(const std::string& flag, bool arg);
 115
 116   /******************************* expr options *******************************/
 117   /** Set ExprSetDepth on all output streams */
 118   void setDefaultExprDepth(const std::string& flag, int64_t depth);
 119   /** Set ExprDag on all output streams */
 120   void setDefaultDagThresh(const std::string& flag, int64_t dag);
 121
 122   /******************************* main options *******************************/
 123   /** Show the solver build configuration and exit */
 124   void showConfiguration(const std::string& flag, bool value);
 125   /** Show copyright information and exit */
 126   void showCopyright(const std::string& flag, bool value);
 127   /** Show version information and exit */
 128   void showVersion(const std::string& flag, bool value);
 129   /** Show all debug tags and exit */
 130   void showDebugTags(const std::string& flag, bool value);
 131   /** Show all trace tags and exit */
 132   void showTraceTags(const std::string& flag, bool value);
 133
 134  private:
 135   /** Pointer to the containing Options object.*/
 136   Options* d_options;
 137 }; /* class OptionHandler */
 138
 139 }  // namespace options
 140 }  // namespace cvc5
 141
 142 #endif /*  CVC5__OPTIONS__OPTIONS_HANDLER_H */