1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* 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 |
|
* Contains code for handling command-line options. |
14 |
|
* |
15 |
|
* For each <module>_options.toml configuration file, mkoptions.py |
16 |
|
* expands this template and generates a <module>_options.h file. |
17 |
|
*/ |
18 |
|
|
19 |
|
#include "cvc5_private.h" |
20 |
|
|
21 |
|
#ifndef CVC5__OPTIONS__DATATYPES_H |
22 |
|
#define CVC5__OPTIONS__DATATYPES_H |
23 |
|
|
24 |
|
#include "options/options.h" |
25 |
|
|
26 |
|
// clang-format off |
27 |
|
|
28 |
|
// clang-format on |
29 |
|
|
30 |
|
namespace cvc5 { |
31 |
|
namespace options { |
32 |
|
|
33 |
|
// clang-format off |
34 |
|
|
35 |
|
enum class SygusFairMode |
36 |
|
{ |
37 |
|
DT_SIZE_PRED, |
38 |
|
DT_HEIGHT_PRED, |
39 |
|
NONE, |
40 |
|
DIRECT, |
41 |
|
DT_SIZE |
42 |
|
}; |
43 |
|
|
44 |
|
static constexpr size_t SygusFairMode__numValues = 5; |
45 |
|
|
46 |
|
std::ostream& operator<<(std::ostream& os, SygusFairMode mode); |
47 |
|
SygusFairMode stringToSygusFairMode(const std::string& optarg); |
48 |
|
// clang-format on |
49 |
|
|
50 |
|
#if defined(CVC5_MUZZLED) || defined(CVC5_COMPETITION_MODE) |
51 |
|
# define DO_SEMANTIC_CHECKS_BY_DEFAULT false |
52 |
|
#else /* CVC5_MUZZLED || CVC5_COMPETITION_MODE */ |
53 |
|
# define DO_SEMANTIC_CHECKS_BY_DEFAULT true |
54 |
|
#endif /* CVC5_MUZZLED || CVC5_COMPETITION_MODE */ |
55 |
|
|
56 |
27397 |
struct HolderDATATYPES |
57 |
|
{ |
58 |
|
// clang-format off |
59 |
|
bool cdtBisimilar = true; |
60 |
|
bool cdtBisimilarWasSetByUser = false; |
61 |
|
bool dtBinarySplit = false; |
62 |
|
bool dtBinarySplitWasSetByUser = false; |
63 |
|
bool dtBlastSplits = false; |
64 |
|
bool dtBlastSplitsWasSetByUser = false; |
65 |
|
bool dtCyclic = true; |
66 |
|
bool dtCyclicWasSetByUser = false; |
67 |
|
bool dtForceAssignment = false; |
68 |
|
bool dtForceAssignmentWasSetByUser = false; |
69 |
|
bool dtInferAsLemmas = false; |
70 |
|
bool dtInferAsLemmasWasSetByUser = false; |
71 |
|
bool dtNestedRec = false; |
72 |
|
bool dtNestedRecWasSetByUser = false; |
73 |
|
bool dtPoliteOptimize = true; |
74 |
|
bool dtPoliteOptimizeWasSetByUser = false; |
75 |
|
bool dtRewriteErrorSel = false; |
76 |
|
bool dtRewriteErrorSelWasSetByUser = false; |
77 |
|
bool dtSharedSelectors = true; |
78 |
|
bool dtSharedSelectorsWasSetByUser = false; |
79 |
|
int64_t sygusAbortSize = -1; |
80 |
|
bool sygusAbortSizeWasSetByUser = false; |
81 |
|
bool sygusFairMax = true; |
82 |
|
bool sygusFairMaxWasSetByUser = false; |
83 |
|
SygusFairMode sygusFair = SygusFairMode::DT_SIZE; |
84 |
|
bool sygusFairWasSetByUser = false; |
85 |
|
bool sygusSymBreak = true; |
86 |
|
bool sygusSymBreakWasSetByUser = false; |
87 |
|
bool sygusSymBreakAgg = true; |
88 |
|
bool sygusSymBreakAggWasSetByUser = false; |
89 |
|
bool sygusSymBreakDynamic = true; |
90 |
|
bool sygusSymBreakDynamicWasSetByUser = false; |
91 |
|
bool sygusSymBreakLazy = true; |
92 |
|
bool sygusSymBreakLazyWasSetByUser = false; |
93 |
|
bool sygusSymBreakPbe = true; |
94 |
|
bool sygusSymBreakPbeWasSetByUser = false; |
95 |
|
bool sygusSymBreakRlv = true; |
96 |
|
bool sygusSymBreakRlvWasSetByUser = false; |
97 |
|
// clang-format on |
98 |
|
}; |
99 |
|
|
100 |
|
#undef DO_SEMANTIC_CHECKS_BY_DEFAULT |
101 |
|
|
102 |
|
// clang-format off |
103 |
|
extern struct cdtBisimilar__option_t |
104 |
|
{ |
105 |
|
typedef bool type; |
106 |
|
type operator()() const; |
107 |
|
} thread_local cdtBisimilar; |
108 |
|
extern struct dtBinarySplit__option_t |
109 |
|
{ |
110 |
|
typedef bool type; |
111 |
|
type operator()() const; |
112 |
|
} thread_local dtBinarySplit; |
113 |
|
extern struct dtBlastSplits__option_t |
114 |
|
{ |
115 |
|
typedef bool type; |
116 |
|
type operator()() const; |
117 |
|
} thread_local dtBlastSplits; |
118 |
|
extern struct dtCyclic__option_t |
119 |
|
{ |
120 |
|
typedef bool type; |
121 |
|
type operator()() const; |
122 |
|
} thread_local dtCyclic; |
123 |
|
extern struct dtForceAssignment__option_t |
124 |
|
{ |
125 |
|
typedef bool type; |
126 |
|
type operator()() const; |
127 |
|
} thread_local dtForceAssignment; |
128 |
|
extern struct dtInferAsLemmas__option_t |
129 |
|
{ |
130 |
|
typedef bool type; |
131 |
|
type operator()() const; |
132 |
|
} thread_local dtInferAsLemmas; |
133 |
|
extern struct dtNestedRec__option_t |
134 |
|
{ |
135 |
|
typedef bool type; |
136 |
|
type operator()() const; |
137 |
|
} thread_local dtNestedRec; |
138 |
|
extern struct dtPoliteOptimize__option_t |
139 |
|
{ |
140 |
|
typedef bool type; |
141 |
|
type operator()() const; |
142 |
|
} thread_local dtPoliteOptimize; |
143 |
|
extern struct dtRewriteErrorSel__option_t |
144 |
|
{ |
145 |
|
typedef bool type; |
146 |
|
type operator()() const; |
147 |
|
} thread_local dtRewriteErrorSel; |
148 |
|
extern struct dtSharedSelectors__option_t |
149 |
|
{ |
150 |
|
typedef bool type; |
151 |
|
type operator()() const; |
152 |
|
} thread_local dtSharedSelectors; |
153 |
|
extern struct sygusAbortSize__option_t |
154 |
|
{ |
155 |
|
typedef int64_t type; |
156 |
|
type operator()() const; |
157 |
|
} thread_local sygusAbortSize; |
158 |
|
extern struct sygusFairMax__option_t |
159 |
|
{ |
160 |
|
typedef bool type; |
161 |
|
type operator()() const; |
162 |
|
} thread_local sygusFairMax; |
163 |
|
extern struct sygusFair__option_t |
164 |
|
{ |
165 |
|
typedef SygusFairMode type; |
166 |
|
type operator()() const; |
167 |
|
} thread_local sygusFair; |
168 |
|
extern struct sygusSymBreak__option_t |
169 |
|
{ |
170 |
|
typedef bool type; |
171 |
|
type operator()() const; |
172 |
|
} thread_local sygusSymBreak; |
173 |
|
extern struct sygusSymBreakAgg__option_t |
174 |
|
{ |
175 |
|
typedef bool type; |
176 |
|
type operator()() const; |
177 |
|
} thread_local sygusSymBreakAgg; |
178 |
|
extern struct sygusSymBreakDynamic__option_t |
179 |
|
{ |
180 |
|
typedef bool type; |
181 |
|
type operator()() const; |
182 |
|
} thread_local sygusSymBreakDynamic; |
183 |
|
extern struct sygusSymBreakLazy__option_t |
184 |
|
{ |
185 |
|
typedef bool type; |
186 |
|
type operator()() const; |
187 |
|
} thread_local sygusSymBreakLazy; |
188 |
|
extern struct sygusSymBreakPbe__option_t |
189 |
|
{ |
190 |
|
typedef bool type; |
191 |
|
type operator()() const; |
192 |
|
} thread_local sygusSymBreakPbe; |
193 |
|
extern struct sygusSymBreakRlv__option_t |
194 |
|
{ |
195 |
|
typedef bool type; |
196 |
|
type operator()() const; |
197 |
|
} thread_local sygusSymBreakRlv; |
198 |
|
// clang-format on |
199 |
|
|
200 |
|
namespace datatypes |
201 |
|
{ |
202 |
|
// clang-format off |
203 |
|
static constexpr const char* cdtBisimilar__name = "cdt-bisimilar"; |
204 |
|
static constexpr const char* dtBinarySplit__name = "dt-binary-split"; |
205 |
|
static constexpr const char* dtBlastSplits__name = "dt-blast-splits"; |
206 |
|
static constexpr const char* dtCyclic__name = "dt-cyclic"; |
207 |
|
static constexpr const char* dtForceAssignment__name = "dt-force-assignment"; |
208 |
|
static constexpr const char* dtInferAsLemmas__name = "dt-infer-as-lemmas"; |
209 |
|
static constexpr const char* dtNestedRec__name = "dt-nested-rec"; |
210 |
|
static constexpr const char* dtPoliteOptimize__name = "dt-polite-optimize"; |
211 |
|
static constexpr const char* dtRewriteErrorSel__name = "dt-rewrite-error-sel"; |
212 |
|
static constexpr const char* dtSharedSelectors__name = "dt-share-sel"; |
213 |
|
static constexpr const char* sygusAbortSize__name = "sygus-abort-size"; |
214 |
|
static constexpr const char* sygusFairMax__name = "sygus-fair-max"; |
215 |
|
static constexpr const char* sygusFair__name = "sygus-fair"; |
216 |
|
static constexpr const char* sygusSymBreak__name = "sygus-sym-break"; |
217 |
|
static constexpr const char* sygusSymBreakAgg__name = "sygus-sym-break-agg"; |
218 |
|
static constexpr const char* sygusSymBreakDynamic__name = "sygus-sym-break-dynamic"; |
219 |
|
static constexpr const char* sygusSymBreakLazy__name = "sygus-sym-break-lazy"; |
220 |
|
static constexpr const char* sygusSymBreakPbe__name = "sygus-sym-break-pbe"; |
221 |
|
static constexpr const char* sygusSymBreakRlv__name = "sygus-sym-break-rlv"; |
222 |
|
// clang-format on |
223 |
|
} |
224 |
|
|
225 |
|
} // namespace options |
226 |
|
|
227 |
|
// clang-format off |
228 |
|
|
229 |
|
// clang-format on |
230 |
|
|
231 |
|
namespace options { |
232 |
|
// clang-format off |
233 |
90 |
inline bool cdtBisimilar__option_t::operator()() const |
234 |
90 |
{ return Options::current().datatypes.cdtBisimilar; } |
235 |
1293 |
inline bool dtBinarySplit__option_t::operator()() const |
236 |
1293 |
{ return Options::current().datatypes.dtBinarySplit; } |
237 |
1293 |
inline bool dtBlastSplits__option_t::operator()() const |
238 |
1293 |
{ return Options::current().datatypes.dtBlastSplits; } |
239 |
167658 |
inline bool dtCyclic__option_t::operator()() const |
240 |
167658 |
{ return Options::current().datatypes.dtCyclic; } |
241 |
20732 |
inline bool dtForceAssignment__option_t::operator()() const |
242 |
20732 |
{ return Options::current().datatypes.dtForceAssignment; } |
243 |
296090 |
inline bool dtInferAsLemmas__option_t::operator()() const |
244 |
296090 |
{ return Options::current().datatypes.dtInferAsLemmas; } |
245 |
72382 |
inline bool dtNestedRec__option_t::operator()() const |
246 |
72382 |
{ return Options::current().datatypes.dtNestedRec; } |
247 |
118117 |
inline bool dtPoliteOptimize__option_t::operator()() const |
248 |
118117 |
{ return Options::current().datatypes.dtPoliteOptimize; } |
249 |
4807 |
inline bool dtRewriteErrorSel__option_t::operator()() const |
250 |
4807 |
{ return Options::current().datatypes.dtRewriteErrorSel; } |
251 |
683526 |
inline bool dtSharedSelectors__option_t::operator()() const |
252 |
683526 |
{ return Options::current().datatypes.dtSharedSelectors; } |
253 |
671 |
inline int64_t sygusAbortSize__option_t::operator()() const |
254 |
671 |
{ return Options::current().datatypes.sygusAbortSize; } |
255 |
432 |
inline bool sygusFairMax__option_t::operator()() const |
256 |
432 |
{ return Options::current().datatypes.sygusFairMax; } |
257 |
82481 |
inline SygusFairMode sygusFair__option_t::operator()() const |
258 |
82481 |
{ return Options::current().datatypes.sygusFair; } |
259 |
3120 |
inline bool sygusSymBreak__option_t::operator()() const |
260 |
3120 |
{ return Options::current().datatypes.sygusSymBreak; } |
261 |
180 |
inline bool sygusSymBreakAgg__option_t::operator()() const |
262 |
180 |
{ return Options::current().datatypes.sygusSymBreakAgg; } |
263 |
64489 |
inline bool sygusSymBreakDynamic__option_t::operator()() const |
264 |
64489 |
{ return Options::current().datatypes.sygusSymBreakDynamic; } |
265 |
257296 |
inline bool sygusSymBreakLazy__option_t::operator()() const |
266 |
257296 |
{ return Options::current().datatypes.sygusSymBreakLazy; } |
267 |
5023 |
inline bool sygusSymBreakPbe__option_t::operator()() const |
268 |
5023 |
{ return Options::current().datatypes.sygusSymBreakPbe; } |
269 |
70843 |
inline bool sygusSymBreakRlv__option_t::operator()() const |
270 |
70843 |
{ return Options::current().datatypes.sygusSymBreakRlv; } |
271 |
|
// clang-format on |
272 |
|
|
273 |
|
namespace datatypes |
274 |
|
{ |
275 |
|
// clang-format off |
276 |
|
void setDefaultCdtBisimilar(Options& opts, bool value); |
277 |
|
void setDefaultDtBinarySplit(Options& opts, bool value); |
278 |
|
void setDefaultDtBlastSplits(Options& opts, bool value); |
279 |
|
void setDefaultDtCyclic(Options& opts, bool value); |
280 |
|
void setDefaultDtForceAssignment(Options& opts, bool value); |
281 |
|
void setDefaultDtInferAsLemmas(Options& opts, bool value); |
282 |
|
void setDefaultDtNestedRec(Options& opts, bool value); |
283 |
|
void setDefaultDtPoliteOptimize(Options& opts, bool value); |
284 |
|
void setDefaultDtRewriteErrorSel(Options& opts, bool value); |
285 |
|
void setDefaultDtSharedSelectors(Options& opts, bool value); |
286 |
|
void setDefaultSygusAbortSize(Options& opts, int64_t value); |
287 |
|
void setDefaultSygusFairMax(Options& opts, bool value); |
288 |
|
void setDefaultSygusFair(Options& opts, SygusFairMode value); |
289 |
|
void setDefaultSygusSymBreak(Options& opts, bool value); |
290 |
|
void setDefaultSygusSymBreakAgg(Options& opts, bool value); |
291 |
|
void setDefaultSygusSymBreakDynamic(Options& opts, bool value); |
292 |
|
void setDefaultSygusSymBreakLazy(Options& opts, bool value); |
293 |
|
void setDefaultSygusSymBreakPbe(Options& opts, bool value); |
294 |
|
void setDefaultSygusSymBreakRlv(Options& opts, bool value); |
295 |
|
// clang-format on |
296 |
|
} |
297 |
|
|
298 |
|
} // namespace options |
299 |
|
} // namespace cvc5 |
300 |
|
|
301 |
|
#endif /* CVC5__OPTIONS__DATATYPES_H */ |