GCC Code Coverage Report
Directory: . Exec Total Coverage
File: build-coverage/src/options/datatypes_options.cpp Lines: 51 123 41.5 %
Date: 2021-03-23 Branches: 7 34 20.6 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file module_template.cpp
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 Option template for option modules.
13
 **
14
 ** For each <module>_options.toml configuration file, mkoptions.py
15
 ** expands this template and generates a <module>_options.cpp file.
16
 **/
17
18
#include "options/options_holder.h"
19
#include "base/check.h"
20
21
namespace CVC4 {
22
23
85
template <> const options::cdtBisimilar__option_t::type& Options::operator[](
24
    options::cdtBisimilar__option_t) const
25
{
26
85
  return d_holder->cdtBisimilar;
27
}
28
template <> bool Options::wasSetByUser(options::cdtBisimilar__option_t) const
29
{
30
  return d_holder->cdtBisimilar__setByUser__;
31
}
32
1549
template <> const options::dtBinarySplit__option_t::type& Options::operator[](
33
    options::dtBinarySplit__option_t) const
34
{
35
1549
  return d_holder->dtBinarySplit;
36
}
37
template <> bool Options::wasSetByUser(options::dtBinarySplit__option_t) const
38
{
39
  return d_holder->dtBinarySplit__setByUser__;
40
}
41
1549
template <> const options::dtBlastSplits__option_t::type& Options::operator[](
42
    options::dtBlastSplits__option_t) const
43
{
44
1549
  return d_holder->dtBlastSplits;
45
}
46
template <> bool Options::wasSetByUser(options::dtBlastSplits__option_t) const
47
{
48
  return d_holder->dtBlastSplits__setByUser__;
49
}
50
225561
template <> const options::dtCyclic__option_t::type& Options::operator[](
51
    options::dtCyclic__option_t) const
52
{
53
225561
  return d_holder->dtCyclic;
54
}
55
template <> bool Options::wasSetByUser(options::dtCyclic__option_t) const
56
{
57
  return d_holder->dtCyclic__setByUser__;
58
}
59
template <> void Options::set(
60
    options::dtForceAssignment__option_t,
61
    const options::dtForceAssignment__option_t::type& x)
62
{
63
  d_holder->dtForceAssignment = x;
64
}
65
26978
template <> const options::dtForceAssignment__option_t::type& Options::operator[](
66
    options::dtForceAssignment__option_t) const
67
{
68
26978
  return d_holder->dtForceAssignment;
69
}
70
template <> bool Options::wasSetByUser(options::dtForceAssignment__option_t) const
71
{
72
  return d_holder->dtForceAssignment__setByUser__;
73
}
74
411653
template <> const options::dtInferAsLemmas__option_t::type& Options::operator[](
75
    options::dtInferAsLemmas__option_t) const
76
{
77
411653
  return d_holder->dtInferAsLemmas;
78
}
79
template <> bool Options::wasSetByUser(options::dtInferAsLemmas__option_t) const
80
{
81
  return d_holder->dtInferAsLemmas__setByUser__;
82
}
83
47442
template <> const options::dtNestedRec__option_t::type& Options::operator[](
84
    options::dtNestedRec__option_t) const
85
{
86
47442
  return d_holder->dtNestedRec;
87
}
88
template <> bool Options::wasSetByUser(options::dtNestedRec__option_t) const
89
{
90
  return d_holder->dtNestedRec__setByUser__;
91
}
92
148165
template <> const options::dtPoliteOptimize__option_t::type& Options::operator[](
93
    options::dtPoliteOptimize__option_t) const
94
{
95
148165
  return d_holder->dtPoliteOptimize;
96
}
97
template <> bool Options::wasSetByUser(options::dtPoliteOptimize__option_t) const
98
{
99
  return d_holder->dtPoliteOptimize__setByUser__;
100
}
101
1319
template <> void Options::set(
102
    options::dtRewriteErrorSel__option_t,
103
    const options::dtRewriteErrorSel__option_t::type& x)
104
{
105
1319
  d_holder->dtRewriteErrorSel = x;
106
1319
}
107
3140
template <> const options::dtRewriteErrorSel__option_t::type& Options::operator[](
108
    options::dtRewriteErrorSel__option_t) const
109
{
110
3140
  return d_holder->dtRewriteErrorSel;
111
}
112
1319
template <> bool Options::wasSetByUser(options::dtRewriteErrorSel__option_t) const
113
{
114
1319
  return d_holder->dtRewriteErrorSel__setByUser__;
115
}
116
943868
template <> const options::dtSharedSelectors__option_t::type& Options::operator[](
117
    options::dtSharedSelectors__option_t) const
118
{
119
943868
  return d_holder->dtSharedSelectors;
120
}
121
template <> bool Options::wasSetByUser(options::dtSharedSelectors__option_t) const
122
{
123
  return d_holder->dtSharedSelectors__setByUser__;
124
}
125
1001
template <> const options::sygusAbortSize__option_t::type& Options::operator[](
126
    options::sygusAbortSize__option_t) const
127
{
128
1001
  return d_holder->sygusAbortSize;
129
}
130
template <> bool Options::wasSetByUser(options::sygusAbortSize__option_t) const
131
{
132
  return d_holder->sygusAbortSize__setByUser__;
133
}
134
626
template <> const options::sygusFairMax__option_t::type& Options::operator[](
135
    options::sygusFairMax__option_t) const
136
{
137
626
  return d_holder->sygusFairMax;
138
}
139
template <> bool Options::wasSetByUser(options::sygusFairMax__option_t) const
140
{
141
  return d_holder->sygusFairMax__setByUser__;
142
}
143
146134
template <> const options::sygusFair__option_t::type& Options::operator[](
144
    options::sygusFair__option_t) const
145
{
146
146134
  return d_holder->sygusFair;
147
}
148
template <> bool Options::wasSetByUser(options::sygusFair__option_t) const
149
{
150
  return d_holder->sygusFair__setByUser__;
151
}
152
4794
template <> const options::sygusSymBreak__option_t::type& Options::operator[](
153
    options::sygusSymBreak__option_t) const
154
{
155
4794
  return d_holder->sygusSymBreak;
156
}
157
template <> bool Options::wasSetByUser(options::sygusSymBreak__option_t) const
158
{
159
  return d_holder->sygusSymBreak__setByUser__;
160
}
161
301
template <> const options::sygusSymBreakAgg__option_t::type& Options::operator[](
162
    options::sygusSymBreakAgg__option_t) const
163
{
164
301
  return d_holder->sygusSymBreakAgg;
165
}
166
template <> bool Options::wasSetByUser(options::sygusSymBreakAgg__option_t) const
167
{
168
  return d_holder->sygusSymBreakAgg__setByUser__;
169
}
170
81536
template <> const options::sygusSymBreakDynamic__option_t::type& Options::operator[](
171
    options::sygusSymBreakDynamic__option_t) const
172
{
173
81536
  return d_holder->sygusSymBreakDynamic;
174
}
175
template <> bool Options::wasSetByUser(options::sygusSymBreakDynamic__option_t) const
176
{
177
  return d_holder->sygusSymBreakDynamic__setByUser__;
178
}
179
475840
template <> const options::sygusSymBreakLazy__option_t::type& Options::operator[](
180
    options::sygusSymBreakLazy__option_t) const
181
{
182
475840
  return d_holder->sygusSymBreakLazy;
183
}
184
template <> bool Options::wasSetByUser(options::sygusSymBreakLazy__option_t) const
185
{
186
  return d_holder->sygusSymBreakLazy__setByUser__;
187
}
188
template <> void Options::set(
189
    options::sygusSymBreakPbe__option_t,
190
    const options::sygusSymBreakPbe__option_t::type& x)
191
{
192
  d_holder->sygusSymBreakPbe = x;
193
}
194
8027
template <> const options::sygusSymBreakPbe__option_t::type& Options::operator[](
195
    options::sygusSymBreakPbe__option_t) const
196
{
197
8027
  return d_holder->sygusSymBreakPbe;
198
}
199
template <> bool Options::wasSetByUser(options::sygusSymBreakPbe__option_t) const
200
{
201
  return d_holder->sygusSymBreakPbe__setByUser__;
202
}
203
123130
template <> const options::sygusSymBreakRlv__option_t::type& Options::operator[](
204
    options::sygusSymBreakRlv__option_t) const
205
{
206
123130
  return d_holder->sygusSymBreakRlv;
207
}
208
template <> bool Options::wasSetByUser(options::sygusSymBreakRlv__option_t) const
209
{
210
  return d_holder->sygusSymBreakRlv__setByUser__;
211
}
212
213
214
namespace options {
215
216
thread_local struct cdtBisimilar__option_t cdtBisimilar;
217
thread_local struct dtBinarySplit__option_t dtBinarySplit;
218
thread_local struct dtBlastSplits__option_t dtBlastSplits;
219
thread_local struct dtCyclic__option_t dtCyclic;
220
thread_local struct dtForceAssignment__option_t dtForceAssignment;
221
thread_local struct dtInferAsLemmas__option_t dtInferAsLemmas;
222
thread_local struct dtNestedRec__option_t dtNestedRec;
223
thread_local struct dtPoliteOptimize__option_t dtPoliteOptimize;
224
thread_local struct dtRewriteErrorSel__option_t dtRewriteErrorSel;
225
thread_local struct dtSharedSelectors__option_t dtSharedSelectors;
226
thread_local struct sygusAbortSize__option_t sygusAbortSize;
227
thread_local struct sygusFairMax__option_t sygusFairMax;
228
thread_local struct sygusFair__option_t sygusFair;
229
thread_local struct sygusSymBreak__option_t sygusSymBreak;
230
thread_local struct sygusSymBreakAgg__option_t sygusSymBreakAgg;
231
thread_local struct sygusSymBreakDynamic__option_t sygusSymBreakDynamic;
232
thread_local struct sygusSymBreakLazy__option_t sygusSymBreakLazy;
233
thread_local struct sygusSymBreakPbe__option_t sygusSymBreakPbe;
234
thread_local struct sygusSymBreakRlv__option_t sygusSymBreakRlv;
235
236
237
std::ostream&
238
operator<<(std::ostream& os, SygusFairMode mode)
239
{
240
  os << "SygusFairMode::";
241
  switch(mode) {
242
    case SygusFairMode::DT_SIZE_PRED:
243
      os << "DT_SIZE_PRED";
244
      break;
245
    case SygusFairMode::DT_SIZE:
246
      os << "DT_SIZE";
247
      break;
248
    case SygusFairMode::DT_HEIGHT_PRED:
249
      os << "DT_HEIGHT_PRED";
250
      break;
251
    case SygusFairMode::NONE:
252
      os << "NONE";
253
      break;
254
    case SygusFairMode::DIRECT:
255
      os << "DIRECT";
256
      break;
257
    default:
258
        Unreachable();
259
  }
260
  return os;
261
}
262
263
SygusFairMode
264
4
stringToSygusFairMode(const std::string& option, const std::string& optarg)
265
{
266
4
  if (optarg == "dt-size-bound")
267
  {
268
    return SygusFairMode::DT_SIZE_PRED;
269
  }
270
4
  else if (optarg == "dt-size")
271
  {
272
    return SygusFairMode::DT_SIZE;
273
  }
274
4
  else if (optarg == "dt-height-bound")
275
  {
276
    return SygusFairMode::DT_HEIGHT_PRED;
277
  }
278
4
  else if (optarg == "none")
279
  {
280
    return SygusFairMode::NONE;
281
  }
282
4
  else if (optarg == "direct")
283
  {
284
4
    return SygusFairMode::DIRECT;
285
  }
286
  else if (optarg == "help")
287
  {
288
    puts("Modes for enforcing fairness for counterexample guided quantifier instantion.\n"
289
         "Available modes for --sygus-fair are:\n"
290
         "+ dt-size-bound\n"
291
         "  Enforce fairness by size bound predicate.\n"
292
         "+ dt-size (default)\n"
293
         "  Enforce fairness using size operator.\n"
294
         "+ dt-height-bound\n"
295
         "  Enforce fairness by height bound predicate.\n"
296
         "+ none\n"
297
         "  Do not enforce fairness.\n"
298
         "+ direct\n"
299
         "  Enforce fairness using direct conflict lemmas.\n");
300
    exit(1);
301
  }
302
  else
303
  {
304
    throw OptionException(std::string("unknown option for --sygus-fair: `") +
305
                          optarg + "'.  Try --sygus-fair=help.");
306
  }
307
}
308
309
310
}  // namespace options
311
26685
}  // namespace CVC4