GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/options/options.h Lines: 11 11 100.0 %
Date: 2021-03-22 Branches: 0 0 0.0 %

Line Exec Source
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-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.\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 "cvc4_export.h"
30
#include "options/language.h"
31
#include "options/option_exception.h"
32
#include "options/printer_modes.h"
33
34
namespace CVC4 {
35
36
namespace api {
37
class Solver;
38
}
39
namespace options {
40
  struct OptionsHolder;
41
  class OptionsHandler;
42
}/* CVC4::options namespace */
43
44
class OptionsListener;
45
46
class CVC4_EXPORT Options
47
{
48
  friend api::Solver;
49
  /** The struct that holds all option values. */
50
  options::OptionsHolder* d_holder;
51
52
  /** The handler for the options of the theory. */
53
  options::OptionsHandler* d_handler;
54
55
  /** The current Options in effect */
56
  static thread_local Options* s_current;
57
58
  /** Low-level assignment function for options */
59
  template <class T>
60
  void assign(T, std::string option, std::string value);
61
  /** Low-level assignment function for bool-valued options */
62
  template <class T>
63
  void assignBool(T, std::string option, bool value);
64
65
  friend class options::OptionsHandler;
66
67
  /**
68
   * Options cannot be copied as they are given an explicit list of
69
   * Listeners to respond to.
70
   */
71
  Options(const Options& options) = delete;
72
73
  /**
74
   * Options cannot be assigned as they are given an explicit list of
75
   * Listeners to respond to.
76
   */
77
  Options& operator=(const Options& options) = delete;
78
79
  static std::string formatThreadOptionException(const std::string& option);
80
81
  static const size_t s_maxoptlen = 128;
82
  static const unsigned s_preemptAdditional = 6;
83
84
public:
85
 class OptionsScope
86
 {
87
  private:
88
    Options* d_oldOptions;
89
  public:
90
146190
    OptionsScope(Options* newOptions) :
91
341784664
        d_oldOptions(Options::s_current)
92
    {
93
146190
      Options::s_current = newOptions;
94
146190
    }
95
292338
    ~OptionsScope(){
96
146169
      Options::s_current = d_oldOptions;
97
146169
    }
98
 };
99
100
  /** Return true if current Options are null */
101
120256
  static inline bool isCurrentNull() {
102
120256
    return s_current == NULL;
103
  }
104
105
  /** Get the current Options in effect */
106
341079669
  static inline Options* current() {
107
341079669
    return s_current;
108
  }
109
110
  Options(OptionsListener* ol = nullptr);
111
  ~Options();
112
113
  /**
114
   * Copies the value of the options stored in OptionsHolder into the current
115
   * Options object.
116
   * This does not copy the listeners in the Options object.
117
   */
118
  void copyValues(const Options& options);
119
120
  /**
121
   * Set the value of the given option.  Use of this default
122
   * implementation causes a compile-time error; write-able
123
   * options specialize this template with a real implementation.
124
   */
125
  template <class T>
126
  void set(T, const typename T::type&) {
127
    // Flag a compile-time error.  Write-able options specialize
128
    // this template to provide an implementation.
129
    T::you_are_trying_to_assign_to_a_read_only_option;
130
  }
131
132
  /**
133
   * Set the value of the given option by key.
134
   *
135
   * Throws OptionException or ModalException on failures.
136
   */
137
  void setOption(const std::string& key, const std::string& optionarg);
138
139
  /** Get the value of the given option.  Const access only. */
140
  template <class T>
141
  const typename T::type& operator[](T) const;
142
143
  /**
144
   * Gets the value of the given option by key and returns value as a string.
145
   *
146
   * Throws OptionException on failures, such as key not being the name of an
147
   * option.
148
   */
149
  std::string getOption(const std::string& key) const;
150
151
  // Get accessor functions.
152
  InputLanguage getInputLanguage() const;
153
  options::InstFormatMode getInstFormatMode() const;
154
  OutputLanguage getOutputLanguage() const;
155
  bool getUfHo() const;
156
  bool getDumpInstantiations() const;
157
  bool getDumpModels() const;
158
  bool getDumpProofs() const;
159
  bool getDumpUnsatCores() const;
160
  bool getEarlyExit() const;
161
  bool getFilesystemAccess() const;
162
  bool getForceNoLimitCpuWhileDump() const;
163
  bool getHelp() const;
164
  bool getIncrementalSolving() const;
165
  bool getInteractive() const;
166
  bool getInteractivePrompt() const;
167
  bool getLanguageHelp() const;
168
  bool getMemoryMap() const;
169
  bool getParseOnly() const;
170
  bool getProduceModels() const;
171
  bool getSegvSpin() const;
172
  bool getSemanticChecks() const;
173
  bool getStatistics() const;
174
  bool getStatsEveryQuery() const;
175
  bool getStatsHideZeros() const;
176
  bool getStrictParsing() const;
177
  int getTearDownIncremental() const;
178
  unsigned long getCumulativeTimeLimit() const;
179
  bool getVersion() const;
180
  const std::string& getForceLogicString() const;
181
  int getVerbosity() const;
182
  std::istream* getIn() const;
183
  std::ostream* getErr();
184
  std::ostream* getOut();
185
  std::ostream* getOutConst() const; // TODO: Remove this.
186
  std::string getBinaryName() const;
187
  unsigned getParseStep() const;
188
189
  // TODO: Document these.
190
  void setInputLanguage(InputLanguage);
191
  void setInteractive(bool);
192
  void setOut(std::ostream*);
193
  void setOutputLanguage(OutputLanguage);
194
195
  bool wasSetByUserEarlyExit() const;
196
  bool wasSetByUserForceLogicString() const;
197
  bool wasSetByUserIncrementalSolving() const;
198
  bool wasSetByUserInteractive() const;
199
200
  // Static accessor functions.
201
  // TODO: Document these.
202
  static std::ostream* currentGetOut();
203
204
  /**
205
   * Returns true iff the value of the given option was set
206
   * by the user via a command-line option or SmtEngine::setOption().
207
   * (Options::set() is low-level and doesn't count.)  Returns false
208
   * otherwise.
209
   */
210
  template <class T>
211
  bool wasSetByUser(T) const;
212
213
  /**
214
   * Get a description of the command-line flags accepted by
215
   * parseOptions.  The returned string will be escaped so that it is
216
   * suitable as an argument to printf. */
217
  std::string getDescription() const;
218
219
  /**
220
   * Print overall command-line option usage message, prefixed by
221
   * "msg"---which could be an error message causing the usage
222
   * output in the first place, e.g. "no such option --foo"
223
   */
224
  static void printUsage(const std::string msg, std::ostream& out);
225
226
  /**
227
   * Print command-line option usage message for only the most-commonly
228
   * used options.  The message is prefixed by "msg"---which could be
229
   * an error message causing the usage output in the first place, e.g.
230
   * "no such option --foo"
231
   */
232
  static void printShortUsage(const std::string msg, std::ostream& out);
233
234
  /** Print help for the --lang command line option */
235
  static void printLanguageHelp(std::ostream& out);
236
237
  /**
238
   * Look up long command-line option names that bear some similarity
239
   * to the given name.  Returns an empty string if there are no
240
   * suggestions.
241
   */
242
  static std::string suggestCommandLineOptions(const std::string& optionName);
243
244
  /**
245
   * Look up SMT option names that bear some similarity to
246
   * the given name.  Don't include the initial ":".  This might be
247
   * useful in case of typos.  Can return an empty vector if there are
248
   * no suggestions.
249
   */
250
  static std::vector<std::string> suggestSmtOptions(
251
      const std::string& optionName);
252
253
  /**
254
   * Initialize the Options object options based on the given
255
   * command-line arguments given in argc and argv.  The return value
256
   * is what's left of the command line (that is, the non-option
257
   * arguments).
258
   *
259
   * This function uses getopt_long() and is not thread safe.
260
   *
261
   * Throws OptionException on failures.
262
   *
263
   * Preconditions: options and argv must be non-null.
264
   */
265
  static std::vector<std::string> parseOptions(Options* options,
266
                                               int argc,
267
                                               char* argv[]);
268
269
  /**
270
   * Get the setting for all options.
271
   */
272
  std::vector<std::vector<std::string> > getOptions() const;
273
274
  /** Set the generic listener associated with this class to ol */
275
  void setListener(OptionsListener* ol);
276
277
  /** Sends a std::flush to getErr(). */
278
  void flushErr();
279
280
  /** Sends a std::flush to getOut(). */
281
  void flushOut();
282
283
 private:
284
  /** Pointer to the options listener, if one exists */
285
  OptionsListener* d_olisten;
286
  /**
287
   * Helper method for setOption, updates this object for setting the given
288
   * option.
289
   */
290
  void setOptionInternal(const std::string& key, const std::string& optionarg);
291
  /**
292
   * Internal procedure for implementing the parseOptions function.
293
   * Initializes the options object based on the given command-line
294
   * arguments. The command line arguments are stored in argc/argv.
295
   * Nonoptions are stored into nonoptions.
296
   *
297
   * This is not thread safe.
298
   *
299
   * Throws OptionException on failures.
300
   *
301
   * Preconditions: options, extender and nonoptions are non-null.
302
   */
303
  static void parseOptionsRecursive(Options* options,
304
                                    int argc,
305
                                    char* argv[],
306
                                    std::vector<std::string>* nonoptions);
307
}; /* class Options */
308
309
}/* CVC4 namespace */
310
311
#endif /* CVC4__OPTIONS__OPTIONS_H */