GCC Code Coverage Report
Directory: . Exec Total Coverage
File: build-coverage/src/options/theory_options.h Lines: 25 25 100.0 %
Date: 2021-03-23 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file module_template.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Mathias Preiner
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 Contains code for handling command-line options.
13
 **
14
 ** For each <module>_options.toml configuration file, mkoptions.py
15
 ** expands this template and generates a <module>_options.h file.
16
 **/
17
18
#include "cvc4_private.h"
19
20
#ifndef CVC4__OPTIONS__THEORY_H
21
#define CVC4__OPTIONS__THEORY_H
22
23
#include "options/options.h"
24
25
26
27
28
#define CVC4_OPTIONS__THEORY__FOR_OPTION_HOLDER \
29
  assignFunctionValues__option_t::type assignFunctionValues;\
30
  bool assignFunctionValues__setByUser__; \
31
  condenseFunctionValues__option_t::type condenseFunctionValues;\
32
  bool condenseFunctionValues__setByUser__; \
33
  eeMode__option_t::type eeMode;\
34
  bool eeMode__setByUser__; \
35
  relevanceFilter__option_t::type relevanceFilter;\
36
  bool relevanceFilter__setByUser__; \
37
  tcMode__option_t::type tcMode;\
38
  bool tcMode__setByUser__; \
39
  theoryOfMode__option_t::type theoryOfMode;\
40
  bool theoryOfMode__setByUser__;
41
42
43
namespace CVC4 {
44
45
namespace options {
46
47
48
enum class EqEngineMode
49
{
50
  DISTRIBUTED
51
};
52
std::ostream&
53
operator<<(std::ostream& os, EqEngineMode mode);
54
EqEngineMode
55
stringToEqEngineMode(const std::string& option, const std::string& optarg);
56
enum class TcMode
57
{
58
  CARE_GRAPH
59
};
60
std::ostream&
61
operator<<(std::ostream& os, TcMode mode);
62
TcMode
63
stringToTcMode(const std::string& option, const std::string& optarg);
64
enum class TheoryOfMode
65
{
66
  THEORY_OF_TYPE_BASED,
67
  THEORY_OF_TERM_BASED
68
};
69
std::ostream&
70
operator<<(std::ostream& os, TheoryOfMode mode);
71
TheoryOfMode
72
stringToTheoryOfMode(const std::string& option, const std::string& optarg);
73
74
extern struct assignFunctionValues__option_t
75
{
76
  typedef bool type;
77
  type operator()() const;
78
  bool wasSetByUser() const;
79
  void set(const type& v);
80
  const char* getName() const;
81
} thread_local assignFunctionValues;
82
extern struct condenseFunctionValues__option_t
83
{
84
  typedef bool type;
85
  type operator()() const;
86
  bool wasSetByUser() const;
87
  const char* getName() const;
88
} thread_local condenseFunctionValues;
89
extern struct eeMode__option_t
90
{
91
  typedef EqEngineMode type;
92
  type operator()() const;
93
  bool wasSetByUser() const;
94
  void set(const type& v);
95
  const char* getName() const;
96
} thread_local eeMode;
97
extern struct relevanceFilter__option_t
98
{
99
  typedef bool type;
100
  type operator()() const;
101
  bool wasSetByUser() const;
102
  void set(const type& v);
103
  const char* getName() const;
104
} thread_local relevanceFilter;
105
extern struct tcMode__option_t
106
{
107
  typedef TcMode type;
108
  type operator()() const;
109
  bool wasSetByUser() const;
110
  void set(const type& v);
111
  const char* getName() const;
112
} thread_local tcMode;
113
extern struct theoryOfMode__option_t
114
{
115
  typedef TheoryOfMode type;
116
  type operator()() const;
117
  bool wasSetByUser() const;
118
  void set(const type& v);
119
  const char* getName() const;
120
} thread_local theoryOfMode;
121
122
}  // namespace options
123
124
template <> void Options::set(
125
    options::assignFunctionValues__option_t,
126
    const options::assignFunctionValues__option_t::type& x);
127
template <> const options::assignFunctionValues__option_t::type& Options::operator[](
128
    options::assignFunctionValues__option_t) const;
129
template <> bool Options::wasSetByUser(options::assignFunctionValues__option_t) const;
130
template <> void Options::assignBool(
131
    options::assignFunctionValues__option_t,
132
    std::string option,
133
    bool value);
134
template <> const options::condenseFunctionValues__option_t::type& Options::operator[](
135
    options::condenseFunctionValues__option_t) const;
136
template <> bool Options::wasSetByUser(options::condenseFunctionValues__option_t) const;
137
template <> void Options::assignBool(
138
    options::condenseFunctionValues__option_t,
139
    std::string option,
140
    bool value);
141
template <> void Options::set(
142
    options::eeMode__option_t,
143
    const options::eeMode__option_t::type& x);
144
template <> const options::eeMode__option_t::type& Options::operator[](
145
    options::eeMode__option_t) const;
146
template <> bool Options::wasSetByUser(options::eeMode__option_t) const;
147
template <> void Options::assign(
148
    options::eeMode__option_t,
149
    std::string option,
150
    std::string value);
151
template <> void Options::set(
152
    options::relevanceFilter__option_t,
153
    const options::relevanceFilter__option_t::type& x);
154
template <> const options::relevanceFilter__option_t::type& Options::operator[](
155
    options::relevanceFilter__option_t) const;
156
template <> bool Options::wasSetByUser(options::relevanceFilter__option_t) const;
157
template <> void Options::assignBool(
158
    options::relevanceFilter__option_t,
159
    std::string option,
160
    bool value);
161
template <> void Options::set(
162
    options::tcMode__option_t,
163
    const options::tcMode__option_t::type& x);
164
template <> const options::tcMode__option_t::type& Options::operator[](
165
    options::tcMode__option_t) const;
166
template <> bool Options::wasSetByUser(options::tcMode__option_t) const;
167
template <> void Options::assign(
168
    options::tcMode__option_t,
169
    std::string option,
170
    std::string value);
171
template <> void Options::set(
172
    options::theoryOfMode__option_t,
173
    const options::theoryOfMode__option_t::type& x);
174
template <> const options::theoryOfMode__option_t::type& Options::operator[](
175
    options::theoryOfMode__option_t) const;
176
template <> bool Options::wasSetByUser(options::theoryOfMode__option_t) const;
177
template <> void Options::assign(
178
    options::theoryOfMode__option_t,
179
    std::string option,
180
    std::string value);
181
182
183
namespace options {
184
185
27861
inline assignFunctionValues__option_t::type assignFunctionValues__option_t::operator()() const
186
{
187
27861
  return (*Options::current())[*this];
188
}
189
inline bool assignFunctionValues__option_t::wasSetByUser() const
190
{
191
  return Options::current()->wasSetByUser(*this);
192
}
193
2
inline void assignFunctionValues__option_t::set(const assignFunctionValues__option_t::type& v)
194
{
195
2
  Options::current()->set(*this, v);
196
2
}
197
inline const char* assignFunctionValues__option_t::getName() const
198
{
199
  return "assign-function-values";
200
}
201
290649
inline condenseFunctionValues__option_t::type condenseFunctionValues__option_t::operator()() const
202
{
203
290649
  return (*Options::current())[*this];
204
}
205
inline bool condenseFunctionValues__option_t::wasSetByUser() const
206
{
207
  return Options::current()->wasSetByUser(*this);
208
}
209
inline const char* condenseFunctionValues__option_t::getName() const
210
{
211
  return "condense-function-values";
212
}
213
8997
inline eeMode__option_t::type eeMode__option_t::operator()() const
214
{
215
8997
  return (*Options::current())[*this];
216
}
217
inline bool eeMode__option_t::wasSetByUser() const
218
{
219
  return Options::current()->wasSetByUser(*this);
220
}
221
inline void eeMode__option_t::set(const eeMode__option_t::type& v)
222
{
223
  Options::current()->set(*this, v);
224
}
225
inline const char* eeMode__option_t::getName() const
226
{
227
  return "ee-mode";
228
}
229
9007
inline relevanceFilter__option_t::type relevanceFilter__option_t::operator()() const
230
{
231
9007
  return (*Options::current())[*this];
232
}
233
7
inline bool relevanceFilter__option_t::wasSetByUser() const
234
{
235
7
  return Options::current()->wasSetByUser(*this);
236
}
237
7
inline void relevanceFilter__option_t::set(const relevanceFilter__option_t::type& v)
238
{
239
7
  Options::current()->set(*this, v);
240
7
}
241
inline const char* relevanceFilter__option_t::getName() const
242
{
243
  return "relevance-filter";
244
}
245
8997
inline tcMode__option_t::type tcMode__option_t::operator()() const
246
{
247
8997
  return (*Options::current())[*this];
248
}
249
inline bool tcMode__option_t::wasSetByUser() const
250
{
251
  return Options::current()->wasSetByUser(*this);
252
}
253
inline void tcMode__option_t::set(const tcMode__option_t::type& v)
254
{
255
  Options::current()->set(*this, v);
256
}
257
inline const char* tcMode__option_t::getName() const
258
{
259
  return "tc-mode";
260
}
261
158797440
inline theoryOfMode__option_t::type theoryOfMode__option_t::operator()() const
262
{
263
158797440
  return (*Options::current())[*this];
264
}
265
8997
inline bool theoryOfMode__option_t::wasSetByUser() const
266
{
267
8997
  return Options::current()->wasSetByUser(*this);
268
}
269
2102
inline void theoryOfMode__option_t::set(const theoryOfMode__option_t::type& v)
270
{
271
2102
  Options::current()->set(*this, v);
272
2102
}
273
inline const char* theoryOfMode__option_t::getName() const
274
{
275
  return "theoryof-mode";
276
}
277
278
}  // namespace options
279
}  // namespace CVC4
280
281
#endif /* CVC4__OPTIONS__THEORY_H */