GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/options/options_handler.h Lines: 0 6 0.0 %
Date: 2021-03-23 Branches: 0 8 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file options_handler.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Tim King, Mathias Preiner, Aina Niemetz
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 Interface for custom handlers and predicates options.
13
 **
14
 ** Interface for custom handlers and predicates options.
15
 **/
16
17
#include "cvc4_private.h"
18
19
#ifndef CVC4__OPTIONS__OPTIONS_HANDLER_H
20
#define CVC4__OPTIONS__OPTIONS_HANDLER_H
21
22
#include <ostream>
23
#include <string>
24
25
#include "options/base_handlers.h"
26
#include "options/bv_options.h"
27
#include "options/decision_options.h"
28
#include "options/language.h"
29
#include "options/option_exception.h"
30
#include "options/printer_modes.h"
31
#include "options/quantifiers_options.h"
32
33
namespace CVC4 {
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
public:
46
  OptionsHandler(Options* options);
47
48
  void unsignedGreater0(const std::string& option, unsigned value) {
49
    options::greater(0)(option, value);
50
  }
51
52
  void unsignedLessEqual2(const std::string& option, unsigned value) {
53
    options::less_equal(2)(option, value);
54
  }
55
56
  void doubleGreaterOrEqual0(const std::string& option, double value) {
57
    options::greater_equal(0.0)(option, value);
58
  }
59
60
  void doubleLessOrEqual1(const std::string& option, double value) {
61
    options::less_equal(1.0)(option, value);
62
  }
63
64
  // theory/quantifiers/options_handlers.h
65
  void checkInstWhenMode(std::string option, InstWhenMode mode);
66
67
  // theory/bv/options_handlers.h
68
  void abcEnabledBuild(std::string option, bool value);
69
  void abcEnabledBuild(std::string option, std::string value);
70
71
  template<class T> void checkSatSolverEnabled(std::string option, T m);
72
73
  void checkBvSatSolver(std::string option, SatSolverMode m);
74
  void checkBitblastMode(std::string option, BitblastMode m);
75
76
  void setBitblastAig(std::string option, bool arg);
77
78
  // printer/options_handlers.h
79
  InstFormatMode stringToInstFormatMode(std::string option, std::string optarg);
80
81
  // decision/options_handlers.h
82
  void setDecisionModeStopOnly(std::string option, DecisionMode m);
83
84
  /**
85
   * Throws a ModalException if this option is being set after final
86
   * initialization.
87
   */
88
  void setProduceAssertions(std::string option, bool value);
89
  void proofEnabledBuild(std::string option, bool value);
90
  void LFSCEnabledBuild(std::string option, bool value);
91
92
  void statsEnabledBuild(std::string option, bool value);
93
94
  unsigned long limitHandler(std::string option, std::string optarg);
95
96
  /* expr/options_handlers.h */
97
  void setDefaultExprDepthPredicate(std::string option, int depth);
98
  void setDefaultDagThreshPredicate(std::string option, int dag);
99
100
  /* main/options_handlers.h */
101
  void copyright(std::string option);
102
  void showConfiguration(std::string option);
103
  void showDebugTags(std::string option);
104
  void showTraceTags(std::string option);
105
  void threadN(std::string option);
106
107
  /* options/base_options_handlers.h */
108
  void setVerbosity(std::string option, int value);
109
  void increaseVerbosity(std::string option);
110
  void decreaseVerbosity(std::string option);
111
  OutputLanguage stringToOutputLanguage(std::string option, std::string optarg);
112
  InputLanguage stringToInputLanguage(std::string option, std::string optarg);
113
  void enableTraceTag(std::string option, std::string optarg);
114
  void enableDebugTag(std::string option, std::string optarg);
115
116
 private:
117
118
  /** Pointer to the containing Options object.*/
119
  Options* d_options;
120
121
  /* Help strings */
122
  static const std::string s_instFormatHelp;
123
124
}; /* class OptionHandler */
125
126
template<class T>
127
void OptionsHandler::checkSatSolverEnabled(std::string option, T m)
128
{
129
#if !defined(CVC4_USE_CRYPTOMINISAT) && !defined(CVC4_USE_CADICAL) \
130
    && !defined(CVC4_USE_KISSAT)
131
  std::stringstream ss;
132
  ss << "option `" << option
133
     << "' requires CVC4 to be built with CryptoMiniSat or CaDiCaL or Kissat";
134
  throw OptionException(ss.str());
135
#endif
136
}
137
138
}/* CVC4::options namespace */
139
}/* CVC4 namespace */
140
141
#endif /*  CVC4__OPTIONS__OPTIONS_HANDLER_H */