GCC Code Coverage Report
Directory: . Exec Total Coverage
File: build-coverage/src/options/base_options.cpp Lines: 7 111 6.3 %
Date: 2021-08-01 Branches: 6 72 8.3 %

Line Exec Source
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
 * Option template for option modules.
14
 *
15
 * For each <module>_options.toml configuration file, mkoptions.py
16
 * expands this template and generates a <module>_options.cpp file.
17
 */
18
#include "options/base_options.h"
19
20
#include <iostream>
21
22
#include "base/check.h"
23
#include "options/option_exception.h"
24
25
// clang-format off
26
namespace cvc5 {
27
28
29
30
namespace options {
31
32
thread_local struct err__option_t err;
33
thread_local struct in__option_t in;
34
thread_local struct incrementalSolving__option_t incrementalSolving;
35
thread_local struct inputLanguage__option_t inputLanguage;
36
thread_local struct languageHelp__option_t languageHelp;
37
thread_local struct out__option_t out;
38
thread_local struct outputLanguage__option_t outputLanguage;
39
thread_local struct outputTag__option_t outputTag;
40
thread_local struct outputTagHolder__option_t outputTagHolder;
41
thread_local struct parseOnly__option_t parseOnly;
42
thread_local struct preprocessOnly__option_t preprocessOnly;
43
thread_local struct printSuccess__option_t printSuccess;
44
thread_local struct resourceWeightHolder__option_t resourceWeightHolder;
45
thread_local struct perCallResourceLimit__option_t perCallResourceLimit;
46
thread_local struct cumulativeResourceLimit__option_t cumulativeResourceLimit;
47
thread_local struct statistics__option_t statistics;
48
thread_local struct statisticsAll__option_t statisticsAll;
49
thread_local struct statisticsEveryQuery__option_t statisticsEveryQuery;
50
thread_local struct statisticsExpert__option_t statisticsExpert;
51
thread_local struct perCallMillisecondLimit__option_t perCallMillisecondLimit;
52
thread_local struct cumulativeMillisecondLimit__option_t cumulativeMillisecondLimit;
53
thread_local struct verbosity__option_t verbosity;
54
55
56
std::ostream& operator<<(std::ostream& os, OutputTag mode)
57
{
58
  switch(mode) {
59
    case OutputTag::SYGUS:
60
      return os << "OutputTag::SYGUS";
61
    case OutputTag::TRIGGER:
62
      return os << "OutputTag::TRIGGER";
63
    case OutputTag::INST:
64
      return os << "OutputTag::INST";
65
    default:
66
      Unreachable();
67
  }
68
  return os;
69
}
70
71
3
OutputTag stringToOutputTag(const std::string& optarg)
72
{
73
3
  if (optarg == "sygus")
74
  {
75
1
    return OutputTag::SYGUS;
76
  }
77
2
  else if (optarg == "trigger")
78
  {
79
    return OutputTag::TRIGGER;
80
  }
81
2
  else if (optarg == "inst")
82
  {
83
2
    return OutputTag::INST;
84
  }
85
  else if (optarg == "help")
86
  {
87
    std::cerr << "Output tags.\n"
88
         "Available tags for --output are:\n"
89
         "+ sygus\n"
90
         "  print enumerated terms and candidates generated by the sygus solver\n"
91
         "+ trigger\n"
92
         "  print selected triggers for quantified formulas\n"
93
         "+ inst\n"
94
         "  print instantiations during solving\n";
95
    std::exit(1);
96
  }
97
  throw OptionException(std::string("unknown option for --output: `") +
98
                        optarg + "'.  Try --output=help.");
99
}
100
101
102
103
namespace base
104
{
105
// clang-format off
106
void setDefaultErr(Options& opts, std::ostream* value)
107
{
108
    if (!opts.base.errWasSetByUser) {
109
        opts.base.err = value;
110
    }
111
}
112
void setDefaultIn(Options& opts, std::istream* value)
113
{
114
    if (!opts.base.inWasSetByUser) {
115
        opts.base.in = value;
116
    }
117
}
118
void setDefaultIncrementalSolving(Options& opts, bool value)
119
{
120
    if (!opts.base.incrementalSolvingWasSetByUser) {
121
        opts.base.incrementalSolving = value;
122
    }
123
}
124
void setDefaultInputLanguage(Options& opts, InputLanguage value)
125
{
126
    if (!opts.base.inputLanguageWasSetByUser) {
127
        opts.base.inputLanguage = value;
128
    }
129
}
130
void setDefaultLanguageHelp(Options& opts, bool value)
131
{
132
    if (!opts.base.languageHelpWasSetByUser) {
133
        opts.base.languageHelp = value;
134
    }
135
}
136
void setDefaultOut(Options& opts, std::ostream* value)
137
{
138
    if (!opts.base.outWasSetByUser) {
139
        opts.base.out = value;
140
    }
141
}
142
void setDefaultOutputLanguage(Options& opts, OutputLanguage value)
143
{
144
    if (!opts.base.outputLanguageWasSetByUser) {
145
        opts.base.outputLanguage = value;
146
    }
147
}
148
void setDefaultOutputTag(Options& opts, OutputTag value)
149
{
150
    if (!opts.base.outputTagWasSetByUser) {
151
        opts.base.outputTag = value;
152
    }
153
}
154
void setDefaultOutputTagHolder(Options& opts, std::bitset<OutputTag__numValues> value)
155
{
156
    if (!opts.base.outputTagHolderWasSetByUser) {
157
        opts.base.outputTagHolder = value;
158
    }
159
}
160
void setDefaultParseOnly(Options& opts, bool value)
161
{
162
    if (!opts.base.parseOnlyWasSetByUser) {
163
        opts.base.parseOnly = value;
164
    }
165
}
166
void setDefaultPreprocessOnly(Options& opts, bool value)
167
{
168
    if (!opts.base.preprocessOnlyWasSetByUser) {
169
        opts.base.preprocessOnly = value;
170
    }
171
}
172
void setDefaultPrintSuccess(Options& opts, bool value)
173
{
174
    if (!opts.base.printSuccessWasSetByUser) {
175
        opts.base.printSuccess = value;
176
    }
177
}
178
void setDefaultResourceWeightHolder(Options& opts, std::vector<std::string> value)
179
{
180
    if (!opts.base.resourceWeightHolderWasSetByUser) {
181
        opts.base.resourceWeightHolder = value;
182
    }
183
}
184
void setDefaultPerCallResourceLimit(Options& opts, uint64_t value)
185
{
186
    if (!opts.base.perCallResourceLimitWasSetByUser) {
187
        opts.base.perCallResourceLimit = value;
188
    }
189
}
190
void setDefaultCumulativeResourceLimit(Options& opts, uint64_t value)
191
{
192
    if (!opts.base.cumulativeResourceLimitWasSetByUser) {
193
        opts.base.cumulativeResourceLimit = value;
194
    }
195
}
196
void setDefaultStatistics(Options& opts, bool value)
197
{
198
    if (!opts.base.statisticsWasSetByUser) {
199
        opts.base.statistics = value;
200
    }
201
}
202
void setDefaultStatisticsAll(Options& opts, bool value)
203
{
204
    if (!opts.base.statisticsAllWasSetByUser) {
205
        opts.base.statisticsAll = value;
206
    }
207
}
208
void setDefaultStatisticsEveryQuery(Options& opts, bool value)
209
{
210
    if (!opts.base.statisticsEveryQueryWasSetByUser) {
211
        opts.base.statisticsEveryQuery = value;
212
    }
213
}
214
void setDefaultStatisticsExpert(Options& opts, bool value)
215
{
216
    if (!opts.base.statisticsExpertWasSetByUser) {
217
        opts.base.statisticsExpert = value;
218
    }
219
}
220
void setDefaultPerCallMillisecondLimit(Options& opts, uint64_t value)
221
{
222
    if (!opts.base.perCallMillisecondLimitWasSetByUser) {
223
        opts.base.perCallMillisecondLimit = value;
224
    }
225
}
226
void setDefaultCumulativeMillisecondLimit(Options& opts, uint64_t value)
227
{
228
    if (!opts.base.cumulativeMillisecondLimitWasSetByUser) {
229
        opts.base.cumulativeMillisecondLimit = value;
230
    }
231
}
232
void setDefaultVerbosity(Options& opts, int value)
233
{
234
    if (!opts.base.verbosityWasSetByUser) {
235
        opts.base.verbosity = value;
236
    }
237
}
238
// clang-format on
239
}
240
241
}  // namespace options
242
29280
}  // namespace cvc5
243
// clang-format on