1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Tim King, Gereon Kremer, Andrew Reynolds |
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 |
|
* Definitions of public facing interface functions for Options. |
14 |
|
* |
15 |
|
* These are all 1 line wrappers for Options::get<T>, Options::set<T>, and |
16 |
|
* Options::wasSetByUser<T> for different option types T. |
17 |
|
*/ |
18 |
|
|
19 |
|
#include <fstream> |
20 |
|
#include <ostream> |
21 |
|
#include <string> |
22 |
|
#include <vector> |
23 |
|
|
24 |
|
#include "base/listener.h" |
25 |
|
#include "base/modal_exception.h" |
26 |
|
#include "options/options.h" |
27 |
|
#include "options/base_options.h" |
28 |
|
#include "options/language.h" |
29 |
|
#include "options/main_options.h" |
30 |
|
#include "options/option_exception.h" |
31 |
|
#include "options/parser_options.h" |
32 |
|
#include "options/printer_modes.h" |
33 |
|
#include "options/printer_options.h" |
34 |
|
#include "options/quantifiers_options.h" |
35 |
|
#include "options/resource_manager_options.h" |
36 |
|
#include "options/smt_options.h" |
37 |
|
#include "options/uf_options.h" |
38 |
|
|
39 |
|
namespace cvc5 { |
40 |
|
|
41 |
|
// Get accessor functions. |
42 |
791545 |
InputLanguage Options::getInputLanguage() const { |
43 |
791545 |
return (*this)[options::inputLanguage]; |
44 |
|
} |
45 |
|
|
46 |
153 |
options::InstFormatMode Options::getInstFormatMode() const |
47 |
|
{ |
48 |
153 |
return (*this)[options::instFormatMode]; |
49 |
|
} |
50 |
|
|
51 |
11778 |
OutputLanguage Options::getOutputLanguage() const { |
52 |
11778 |
return (*this)[options::outputLanguage]; |
53 |
|
} |
54 |
|
|
55 |
2954721 |
bool Options::getUfHo() const { return (*this)[options::ufHo]; } |
56 |
|
|
57 |
301200 |
bool Options::getDumpInstantiations() const{ |
58 |
602412 |
return (*this)[options::dumpInstantiations]; |
59 |
|
} |
60 |
|
|
61 |
301200 |
bool Options::getDumpModels() const{ |
62 |
301200 |
return (*this)[options::dumpModels]; |
63 |
|
} |
64 |
|
|
65 |
301200 |
bool Options::getDumpProofs() const{ |
66 |
301200 |
return (*this)[options::dumpProofs]; |
67 |
|
} |
68 |
|
|
69 |
301200 |
bool Options::getDumpUnsatCores() const{ |
70 |
|
// dump unsat cores full enables dumpUnsatCores |
71 |
301200 |
return (*this)[options::dumpUnsatCores] |
72 |
301200 |
|| (*this)[options::dumpUnsatCoresFull]; |
73 |
|
} |
74 |
|
|
75 |
5858 |
bool Options::getEarlyExit() const{ |
76 |
17574 |
return (*this)[options::earlyExit]; |
77 |
|
} |
78 |
|
|
79 |
6109 |
bool Options::getFilesystemAccess() const{ |
80 |
6109 |
return (*this)[options::filesystemAccess]; |
81 |
|
} |
82 |
|
|
83 |
28 |
bool Options::getForceNoLimitCpuWhileDump() const{ |
84 |
56 |
return (*this)[options::forceNoLimitCpuWhileDump]; |
85 |
|
} |
86 |
|
|
87 |
5879 |
bool Options::getHelp() const{ |
88 |
11758 |
return (*this)[options::help]; |
89 |
|
} |
90 |
|
|
91 |
|
bool Options::getIncrementalSolving() const{ |
92 |
|
return (*this)[options::incrementalSolving]; |
93 |
|
} |
94 |
|
|
95 |
5878 |
bool Options::getInteractive() const{ |
96 |
23514 |
return (*this)[options::interactive]; |
97 |
|
} |
98 |
|
|
99 |
28 |
bool Options::getInteractivePrompt() const{ |
100 |
56 |
return (*this)[options::interactivePrompt]; |
101 |
|
} |
102 |
|
|
103 |
5879 |
bool Options::getLanguageHelp() const{ |
104 |
5879 |
return (*this)[options::languageHelp]; |
105 |
|
} |
106 |
|
|
107 |
5878 |
bool Options::getMemoryMap() const{ |
108 |
11756 |
return (*this)[options::memoryMap]; |
109 |
|
} |
110 |
|
|
111 |
312440 |
bool Options::getParseOnly() const{ |
112 |
624880 |
return (*this)[options::parseOnly]; |
113 |
|
} |
114 |
|
|
115 |
|
bool Options::getProduceModels() const{ |
116 |
|
return (*this)[options::produceModels]; |
117 |
|
} |
118 |
|
|
119 |
5879 |
bool Options::getSegvSpin() const{ |
120 |
11758 |
return (*this)[options::segvSpin]; |
121 |
|
} |
122 |
|
|
123 |
6109 |
bool Options::getSemanticChecks() const{ |
124 |
12218 |
return (*this)[options::semanticChecks]; |
125 |
|
} |
126 |
|
|
127 |
5878 |
bool Options::getStatistics() const{ |
128 |
|
// statsEveryQuery enables stats |
129 |
27098 |
return (*this)[options::statistics] || (*this)[options::statisticsEveryQuery]; |
130 |
|
} |
131 |
|
|
132 |
9464 |
bool Options::getStatsEveryQuery() const{ |
133 |
9464 |
return (*this)[options::statisticsEveryQuery]; |
134 |
|
} |
135 |
|
|
136 |
6109 |
bool Options::getStrictParsing() const{ |
137 |
12227 |
return (*this)[options::strictParsing]; |
138 |
|
} |
139 |
|
|
140 |
5878 |
int Options::getTearDownIncremental() const{ |
141 |
11756 |
return (*this)[options::tearDownIncremental]; |
142 |
|
} |
143 |
|
|
144 |
5879 |
uint64_t Options::getCumulativeTimeLimit() const |
145 |
|
{ |
146 |
11758 |
return (*this)[options::cumulativeMillisecondLimit]; |
147 |
|
} |
148 |
|
|
149 |
5879 |
bool Options::getVersion() const{ |
150 |
11758 |
return (*this)[options::version]; |
151 |
|
} |
152 |
|
|
153 |
9 |
const std::string& Options::getForceLogicString() const{ |
154 |
6148 |
return (*this)[options::forceLogicString]; |
155 |
|
} |
156 |
|
|
157 |
602442 |
int Options::getVerbosity() const{ |
158 |
602442 |
return (*this)[options::verbosity]; |
159 |
|
} |
160 |
|
|
161 |
12 |
std::istream* Options::getIn() const{ |
162 |
24 |
return (*this)[options::in]; |
163 |
|
} |
164 |
|
|
165 |
17578 |
std::ostream* Options::getErr(){ |
166 |
17578 |
return (*this)[options::err]; |
167 |
|
} |
168 |
|
|
169 |
319941 |
std::ostream* Options::getOut(){ |
170 |
319941 |
return (*this)[options::out]; |
171 |
|
} |
172 |
|
|
173 |
12 |
std::ostream* Options::getOutConst() const{ |
174 |
|
// #warning "Remove Options::getOutConst" |
175 |
12 |
return (*this)[options::out]; |
176 |
|
} |
177 |
|
|
178 |
5879 |
std::string Options::getBinaryName() const{ |
179 |
11758 |
return (*this)[options::binary_name]; |
180 |
|
} |
181 |
|
|
182 |
|
std::ostream* Options::currentGetOut() { |
183 |
|
return current().getOut(); |
184 |
|
} |
185 |
|
|
186 |
|
|
187 |
|
// TODO: Document these. |
188 |
|
|
189 |
5656 |
void Options::setInputLanguage(InputLanguage value) { |
190 |
5656 |
set(options::inputLanguage, value); |
191 |
5656 |
} |
192 |
|
|
193 |
5879 |
void Options::setInteractive(bool value) { |
194 |
5879 |
set(options::interactive, value); |
195 |
5879 |
} |
196 |
|
|
197 |
|
void Options::setOut(std::ostream* value) { |
198 |
|
set(options::out, value); |
199 |
|
} |
200 |
|
|
201 |
5880 |
void Options::setOutputLanguage(OutputLanguage value) { |
202 |
5880 |
set(options::outputLanguage, value); |
203 |
5880 |
} |
204 |
|
|
205 |
5858 |
bool Options::wasSetByUserEarlyExit() const { |
206 |
5858 |
return wasSetByUser(options::earlyExit); |
207 |
|
} |
208 |
|
|
209 |
6121 |
bool Options::wasSetByUserForceLogicString() const { |
210 |
6121 |
return wasSetByUser(options::forceLogicString); |
211 |
|
} |
212 |
|
|
213 |
5878 |
bool Options::wasSetByUserIncrementalSolving() const { |
214 |
5878 |
return wasSetByUser(options::incrementalSolving); |
215 |
|
} |
216 |
|
|
217 |
5879 |
bool Options::wasSetByUserInteractive() const { |
218 |
5879 |
return wasSetByUser(options::interactive); |
219 |
|
} |
220 |
|
|
221 |
|
|
222 |
5858 |
void Options::flushErr() { |
223 |
5858 |
if(getErr() != NULL) { |
224 |
5858 |
*(getErr()) << std::flush; |
225 |
|
} |
226 |
5858 |
} |
227 |
|
|
228 |
5858 |
void Options::flushOut() { |
229 |
5858 |
if(getOut() != NULL) { |
230 |
5858 |
*(getOut()) << std::flush; |
231 |
|
} |
232 |
5858 |
} |
233 |
|
|
234 |
752003 |
} // namespace cvc5 |