1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Morgan Deters, Abdalrhman Mohamed |
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 |
|
* The main entry point into the cvc5 library's SMT interface. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "smt/smt_engine.h" |
17 |
|
|
18 |
|
#include "base/check.h" |
19 |
|
#include "base/exception.h" |
20 |
|
#include "base/modal_exception.h" |
21 |
|
#include "base/output.h" |
22 |
|
#include "decision/decision_engine.h" |
23 |
|
#include "expr/bound_var_manager.h" |
24 |
|
#include "expr/node.h" |
25 |
|
#include "options/base_options.h" |
26 |
|
#include "options/expr_options.h" |
27 |
|
#include "options/language.h" |
28 |
|
#include "options/main_options.h" |
29 |
|
#include "options/option_exception.h" |
30 |
|
#include "options/options_public.h" |
31 |
|
#include "options/parser_options.h" |
32 |
|
#include "options/printer_options.h" |
33 |
|
#include "options/proof_options.h" |
34 |
|
#include "options/smt_options.h" |
35 |
|
#include "options/theory_options.h" |
36 |
|
#include "printer/printer.h" |
37 |
|
#include "proof/unsat_core.h" |
38 |
|
#include "prop/prop_engine.h" |
39 |
|
#include "smt/abduction_solver.h" |
40 |
|
#include "smt/abstract_values.h" |
41 |
|
#include "smt/assertions.h" |
42 |
|
#include "smt/check_models.h" |
43 |
|
#include "smt/dump.h" |
44 |
|
#include "smt/dump_manager.h" |
45 |
|
#include "smt/env.h" |
46 |
|
#include "smt/interpolation_solver.h" |
47 |
|
#include "smt/listeners.h" |
48 |
|
#include "smt/logic_exception.h" |
49 |
|
#include "smt/model_blocker.h" |
50 |
|
#include "smt/model_core_builder.h" |
51 |
|
#include "smt/node_command.h" |
52 |
|
#include "smt/options_manager.h" |
53 |
|
#include "smt/preprocessor.h" |
54 |
|
#include "smt/proof_manager.h" |
55 |
|
#include "smt/quant_elim_solver.h" |
56 |
|
#include "smt/smt_engine_scope.h" |
57 |
|
#include "smt/smt_engine_state.h" |
58 |
|
#include "smt/smt_engine_stats.h" |
59 |
|
#include "smt/smt_solver.h" |
60 |
|
#include "smt/sygus_solver.h" |
61 |
|
#include "smt/unsat_core_manager.h" |
62 |
|
#include "theory/quantifiers/instantiation_list.h" |
63 |
|
#include "theory/quantifiers/quantifiers_attributes.h" |
64 |
|
#include "theory/quantifiers_engine.h" |
65 |
|
#include "theory/rewriter.h" |
66 |
|
#include "theory/smt_engine_subsolver.h" |
67 |
|
#include "theory/theory_engine.h" |
68 |
|
#include "util/random.h" |
69 |
|
#include "util/rational.h" |
70 |
|
#include "util/resource_manager.h" |
71 |
|
#include "util/sexpr.h" |
72 |
|
#include "util/statistics_registry.h" |
73 |
|
|
74 |
|
// required for hacks related to old proofs for unsat cores |
75 |
|
#include "base/configuration.h" |
76 |
|
#include "base/configuration_private.h" |
77 |
|
|
78 |
|
using namespace std; |
79 |
|
using namespace cvc5::smt; |
80 |
|
using namespace cvc5::preprocessing; |
81 |
|
using namespace cvc5::prop; |
82 |
|
using namespace cvc5::context; |
83 |
|
using namespace cvc5::theory; |
84 |
|
|
85 |
|
namespace cvc5 { |
86 |
|
|
87 |
10484 |
SmtEngine::SmtEngine(NodeManager* nm, Options* optr) |
88 |
10484 |
: d_env(new Env(nm, optr)), |
89 |
10484 |
d_state(new SmtEngineState(getContext(), getUserContext(), *this)), |
90 |
10484 |
d_absValues(new AbstractValues(getNodeManager())), |
91 |
10484 |
d_asserts(new Assertions(*d_env.get(), *d_absValues.get())), |
92 |
10484 |
d_routListener(new ResourceOutListener(*this)), |
93 |
10484 |
d_snmListener(new SmtNodeManagerListener(*getDumpManager(), d_outMgr)), |
94 |
|
d_smtSolver(nullptr), |
95 |
|
d_model(nullptr), |
96 |
|
d_checkModels(nullptr), |
97 |
|
d_pfManager(nullptr), |
98 |
|
d_ucManager(nullptr), |
99 |
|
d_sygusSolver(nullptr), |
100 |
|
d_abductSolver(nullptr), |
101 |
|
d_interpolSolver(nullptr), |
102 |
|
d_quantElimSolver(nullptr), |
103 |
|
d_isInternalSubsolver(false), |
104 |
|
d_stats(nullptr), |
105 |
|
d_outMgr(this), |
106 |
|
d_optm(nullptr), |
107 |
|
d_pp(nullptr), |
108 |
73389 |
d_scope(nullptr) |
109 |
|
{ |
110 |
|
// !!!!!!!!!!!!!!!!!!!!!! temporary hack: this makes the current SmtEngine |
111 |
|
// we are constructing the current SmtEngine in scope for the lifetime of |
112 |
|
// this SmtEngine, or until another SmtEngine is constructed (that SmtEngine |
113 |
|
// is then in scope during its lifetime). This is mostly to ensure that |
114 |
|
// options are always in scope, for e.g. printing expressions, which rely |
115 |
|
// on knowing the output language. |
116 |
|
// Notice that the SmtEngine may spawn new SmtEngine "subsolvers" internally. |
117 |
|
// These are created, used, and deleted in a modular fashion while not |
118 |
|
// interleaving calls to the master SmtEngine. Thus the hack here does not |
119 |
|
// break this use case. |
120 |
|
// On the other hand, this hack breaks use cases where multiple SmtEngine |
121 |
|
// objects are created by the user. |
122 |
10484 |
d_scope.reset(new SmtScope(this)); |
123 |
|
// set the options manager |
124 |
10485 |
d_optm.reset(new smt::OptionsManager(&getOptions())); |
125 |
|
// listen to node manager events |
126 |
10483 |
getNodeManager()->subscribeEvents(d_snmListener.get()); |
127 |
|
// listen to resource out |
128 |
10483 |
getResourceManager()->registerListener(d_routListener.get()); |
129 |
|
// make statistics |
130 |
10483 |
d_stats.reset(new SmtEngineStatistics()); |
131 |
|
// reset the preprocessor |
132 |
31449 |
d_pp.reset( |
133 |
20966 |
new smt::Preprocessor(*this, *d_env.get(), *d_absValues.get(), *d_stats)); |
134 |
|
// make the SMT solver |
135 |
52415 |
d_smtSolver.reset( |
136 |
41932 |
new SmtSolver(*this, *d_env.get(), *d_state, *d_pp, *d_stats)); |
137 |
|
// make the SyGuS solver |
138 |
41932 |
d_sygusSolver.reset( |
139 |
31449 |
new SygusSolver(*d_smtSolver, *d_pp, getUserContext(), d_outMgr)); |
140 |
|
// make the quantifier elimination solver |
141 |
10483 |
d_quantElimSolver.reset(new QuantElimSolver(*d_smtSolver)); |
142 |
|
|
143 |
10483 |
} |
144 |
|
|
145 |
28380 |
bool SmtEngine::isFullyInited() const { return d_state->isFullyInited(); } |
146 |
10943 |
bool SmtEngine::isQueryMade() const { return d_state->isQueryMade(); } |
147 |
2825 |
size_t SmtEngine::getNumUserLevels() const |
148 |
|
{ |
149 |
2825 |
return d_state->getNumUserLevels(); |
150 |
|
} |
151 |
166 |
SmtMode SmtEngine::getSmtMode() const { return d_state->getMode(); } |
152 |
128 |
bool SmtEngine::isSmtModeSat() const |
153 |
|
{ |
154 |
128 |
SmtMode mode = getSmtMode(); |
155 |
128 |
return mode == SmtMode::SAT || mode == SmtMode::SAT_UNKNOWN; |
156 |
|
} |
157 |
|
Result SmtEngine::getStatusOfLastCommand() const |
158 |
|
{ |
159 |
|
return d_state->getStatus(); |
160 |
|
} |
161 |
28265 |
context::UserContext* SmtEngine::getUserContext() |
162 |
|
{ |
163 |
28265 |
return d_env->getUserContext(); |
164 |
|
} |
165 |
10502 |
context::Context* SmtEngine::getContext() { return d_env->getContext(); } |
166 |
|
|
167 |
344683 |
TheoryEngine* SmtEngine::getTheoryEngine() |
168 |
|
{ |
169 |
344683 |
return d_smtSolver->getTheoryEngine(); |
170 |
|
} |
171 |
|
|
172 |
56155 |
prop::PropEngine* SmtEngine::getPropEngine() |
173 |
|
{ |
174 |
56155 |
return d_smtSolver->getPropEngine(); |
175 |
|
} |
176 |
|
|
177 |
121624 |
void SmtEngine::finishInit() |
178 |
|
{ |
179 |
121624 |
if (d_state->isFullyInited()) |
180 |
|
{ |
181 |
|
// already initialized, return |
182 |
111782 |
return; |
183 |
|
} |
184 |
|
|
185 |
|
// Notice that finishInitInternal is called when options are finalized. If we |
186 |
|
// are parsing smt2, this occurs at the moment we enter "Assert mode", page 52 |
187 |
|
// of SMT-LIB 2.6 standard. |
188 |
|
|
189 |
|
// set the logic |
190 |
9842 |
const LogicInfo& logic = getLogicInfo(); |
191 |
9842 |
if (!logic.isLocked()) |
192 |
|
{ |
193 |
1570 |
setLogicInternal(); |
194 |
|
} |
195 |
|
|
196 |
|
// set the random seed |
197 |
9842 |
Random::getRandom().setSeed(d_env->getOptions().driver.seed); |
198 |
|
|
199 |
|
// Call finish init on the options manager. This inializes the resource |
200 |
|
// manager based on the options, and sets up the best default options |
201 |
|
// based on our heuristics. |
202 |
9842 |
d_optm->finishInit(d_env->d_logic, d_isInternalSubsolver); |
203 |
|
|
204 |
9841 |
ProofNodeManager* pnm = nullptr; |
205 |
9841 |
if (d_env->getOptions().smt.produceProofs) |
206 |
|
{ |
207 |
|
// ensure bound variable uses canonical bound variables |
208 |
3759 |
getNodeManager()->getBoundVarManager()->enableKeepCacheValues(); |
209 |
|
// make the proof manager |
210 |
3759 |
d_pfManager.reset(new PfManager(getUserContext(), this)); |
211 |
3759 |
PreprocessProofGenerator* pppg = d_pfManager->getPreprocessProofGenerator(); |
212 |
|
// start the unsat core manager |
213 |
3759 |
d_ucManager.reset(new UnsatCoreManager()); |
214 |
|
// use this proof node manager |
215 |
3759 |
pnm = d_pfManager->getProofNodeManager(); |
216 |
|
// enable proof support in the environment/rewriter |
217 |
3759 |
d_env->setProofNodeManager(pnm); |
218 |
|
// enable it in the assertions pipeline |
219 |
3759 |
d_asserts->setProofGenerator(pppg); |
220 |
|
// enable it in the SmtSolver |
221 |
3759 |
d_smtSolver->setProofNodeManager(pnm); |
222 |
|
// enabled proofs in the preprocessor |
223 |
3759 |
d_pp->setProofGenerator(pppg); |
224 |
|
} |
225 |
|
|
226 |
9841 |
Trace("smt-debug") << "SmtEngine::finishInit" << std::endl; |
227 |
9841 |
d_smtSolver->finishInit(logic); |
228 |
|
|
229 |
|
// now can construct the SMT-level model object |
230 |
9841 |
TheoryEngine* te = d_smtSolver->getTheoryEngine(); |
231 |
9841 |
Assert(te != nullptr); |
232 |
9841 |
TheoryModel* tm = te->getModel(); |
233 |
9841 |
if (tm != nullptr) |
234 |
|
{ |
235 |
9841 |
d_model.reset(new Model(tm)); |
236 |
|
// make the check models utility |
237 |
9841 |
d_checkModels.reset(new CheckModels(*d_env.get())); |
238 |
|
} |
239 |
|
|
240 |
|
// global push/pop around everything, to ensure proper destruction |
241 |
|
// of context-dependent data structures |
242 |
9841 |
d_state->setup(); |
243 |
|
|
244 |
9841 |
Trace("smt-debug") << "Set up assertions..." << std::endl; |
245 |
9841 |
d_asserts->finishInit(); |
246 |
|
|
247 |
|
// dump out a set-logic command only when raw-benchmark is disabled to avoid |
248 |
|
// dumping the command twice. |
249 |
9841 |
if (Dump.isOn("benchmark") && !Dump.isOn("raw-benchmark")) |
250 |
|
{ |
251 |
2 |
LogicInfo everything; |
252 |
1 |
everything.lock(); |
253 |
3 |
getPrinter().toStreamCmdComment( |
254 |
1 |
getOutputManager().getDumpOut(), |
255 |
|
"cvc5 always dumps the most general, all-supported logic (below), as " |
256 |
|
"some internals might require the use of a logic more general than " |
257 |
1 |
"the input."); |
258 |
2 |
getPrinter().toStreamCmdSetBenchmarkLogic(getOutputManager().getDumpOut(), |
259 |
2 |
everything.getLogicString()); |
260 |
|
} |
261 |
|
|
262 |
|
// initialize the dump manager |
263 |
9841 |
getDumpManager()->finishInit(); |
264 |
|
|
265 |
|
// subsolvers |
266 |
9841 |
if (d_env->getOptions().smt.produceAbducts) |
267 |
|
{ |
268 |
326 |
d_abductSolver.reset(new AbductionSolver(this)); |
269 |
|
} |
270 |
19682 |
if (d_env->getOptions().smt.produceInterpols |
271 |
9841 |
!= options::ProduceInterpols::NONE) |
272 |
|
{ |
273 |
114 |
d_interpolSolver.reset(new InterpolationSolver(this)); |
274 |
|
} |
275 |
|
|
276 |
9841 |
d_pp->finishInit(); |
277 |
|
|
278 |
9841 |
AlwaysAssert(getPropEngine()->getAssertionLevel() == 0) |
279 |
|
<< "The PropEngine has pushed but the SmtEngine " |
280 |
|
"hasn't finished initializing!"; |
281 |
|
|
282 |
9841 |
Assert(getLogicInfo().isLocked()); |
283 |
|
|
284 |
|
// store that we are finished initializing |
285 |
9841 |
d_state->finishInit(); |
286 |
9841 |
Trace("smt-debug") << "SmtEngine::finishInit done" << std::endl; |
287 |
|
} |
288 |
|
|
289 |
10483 |
void SmtEngine::shutdown() { |
290 |
10483 |
d_state->shutdown(); |
291 |
|
|
292 |
10483 |
d_smtSolver->shutdown(); |
293 |
|
|
294 |
10483 |
d_env->shutdown(); |
295 |
10483 |
} |
296 |
|
|
297 |
20966 |
SmtEngine::~SmtEngine() |
298 |
|
{ |
299 |
20966 |
SmtScope smts(this); |
300 |
|
|
301 |
|
try { |
302 |
10483 |
shutdown(); |
303 |
|
|
304 |
|
// global push/pop around everything, to ensure proper destruction |
305 |
|
// of context-dependent data structures |
306 |
10483 |
d_state->cleanup(); |
307 |
|
|
308 |
|
//destroy all passes before destroying things that they refer to |
309 |
10483 |
d_pp->cleanup(); |
310 |
|
|
311 |
10483 |
d_pfManager.reset(nullptr); |
312 |
10483 |
d_ucManager.reset(nullptr); |
313 |
|
|
314 |
10483 |
d_absValues.reset(nullptr); |
315 |
10483 |
d_asserts.reset(nullptr); |
316 |
10483 |
d_model.reset(nullptr); |
317 |
|
|
318 |
10483 |
d_abductSolver.reset(nullptr); |
319 |
10483 |
d_interpolSolver.reset(nullptr); |
320 |
10483 |
d_quantElimSolver.reset(nullptr); |
321 |
10483 |
d_sygusSolver.reset(nullptr); |
322 |
10483 |
d_smtSolver.reset(nullptr); |
323 |
|
|
324 |
10483 |
d_stats.reset(nullptr); |
325 |
10483 |
getNodeManager()->unsubscribeEvents(d_snmListener.get()); |
326 |
10483 |
d_snmListener.reset(nullptr); |
327 |
10483 |
d_routListener.reset(nullptr); |
328 |
10483 |
d_optm.reset(nullptr); |
329 |
10483 |
d_pp.reset(nullptr); |
330 |
|
// destroy the state |
331 |
10483 |
d_state.reset(nullptr); |
332 |
|
// destroy the environment |
333 |
10483 |
d_env.reset(nullptr); |
334 |
|
} catch(Exception& e) { |
335 |
|
Warning() << "cvc5 threw an exception during cleanup." << endl << e << endl; |
336 |
|
} |
337 |
10483 |
} |
338 |
|
|
339 |
8350 |
void SmtEngine::setLogic(const LogicInfo& logic) |
340 |
|
{ |
341 |
16700 |
SmtScope smts(this); |
342 |
8350 |
if (d_state->isFullyInited()) |
343 |
|
{ |
344 |
|
throw ModalException("Cannot set logic in SmtEngine after the engine has " |
345 |
|
"finished initializing."); |
346 |
|
} |
347 |
8350 |
d_env->d_logic = logic; |
348 |
8350 |
d_userLogic = logic; |
349 |
8350 |
setLogicInternal(); |
350 |
8350 |
} |
351 |
|
|
352 |
2 |
void SmtEngine::setLogic(const std::string& s) |
353 |
|
{ |
354 |
4 |
SmtScope smts(this); |
355 |
|
try |
356 |
|
{ |
357 |
2 |
setLogic(LogicInfo(s)); |
358 |
|
// dump out a set-logic command |
359 |
2 |
if (Dump.isOn("raw-benchmark")) |
360 |
|
{ |
361 |
|
getPrinter().toStreamCmdSetBenchmarkLogic( |
362 |
|
getOutputManager().getDumpOut(), getLogicInfo().getLogicString()); |
363 |
|
} |
364 |
|
} |
365 |
|
catch (IllegalArgumentException& e) |
366 |
|
{ |
367 |
|
throw LogicException(e.what()); |
368 |
|
} |
369 |
2 |
} |
370 |
|
|
371 |
2 |
void SmtEngine::setLogic(const char* logic) { setLogic(string(logic)); } |
372 |
|
|
373 |
46441 |
const LogicInfo& SmtEngine::getLogicInfo() const |
374 |
|
{ |
375 |
46441 |
return d_env->getLogicInfo(); |
376 |
|
} |
377 |
|
|
378 |
395 |
LogicInfo SmtEngine::getUserLogicInfo() const |
379 |
|
{ |
380 |
|
// Lock the logic to make sure that this logic can be queried. We create a |
381 |
|
// copy of the user logic here to keep this method const. |
382 |
395 |
LogicInfo res = d_userLogic; |
383 |
395 |
res.lock(); |
384 |
395 |
return res; |
385 |
|
} |
386 |
|
|
387 |
6121 |
void SmtEngine::notifyStartParsing(const std::string& filename) |
388 |
|
{ |
389 |
6121 |
d_state->setFilename(filename); |
390 |
12242 |
d_env->getStatisticsRegistry().registerValue<std::string>("driver::filename", |
391 |
12242 |
filename); |
392 |
|
// Copy the original options. This is called prior to beginning parsing. |
393 |
|
// Hence reset should revert to these options, which note is after reading |
394 |
|
// the command line. |
395 |
6121 |
} |
396 |
|
|
397 |
|
const std::string& SmtEngine::getFilename() const |
398 |
|
{ |
399 |
|
return d_state->getFilename(); |
400 |
|
} |
401 |
|
|
402 |
|
void SmtEngine::setResultStatistic(const std::string& result) { |
403 |
|
d_env->getStatisticsRegistry().registerValue<std::string>("driver::sat/unsat", |
404 |
|
result); |
405 |
|
} |
406 |
6121 |
void SmtEngine::setTotalTimeStatistic(double seconds) { |
407 |
12242 |
d_env->getStatisticsRegistry().registerValue<double>("driver::totalTime", |
408 |
12242 |
seconds); |
409 |
6121 |
} |
410 |
|
|
411 |
9920 |
void SmtEngine::setLogicInternal() |
412 |
|
{ |
413 |
9920 |
Assert(!d_state->isFullyInited()) |
414 |
|
<< "setting logic in SmtEngine but the engine has already" |
415 |
|
" finished initializing for this run"; |
416 |
9920 |
d_env->d_logic.lock(); |
417 |
9920 |
d_userLogic.lock(); |
418 |
9920 |
} |
419 |
|
|
420 |
5703 |
void SmtEngine::setInfo(const std::string& key, const std::string& value) |
421 |
|
{ |
422 |
11406 |
SmtScope smts(this); |
423 |
|
|
424 |
5703 |
Trace("smt") << "SMT setInfo(" << key << ", " << value << ")" << endl; |
425 |
|
|
426 |
5703 |
if (Dump.isOn("benchmark")) |
427 |
|
{ |
428 |
|
if (key == "status") |
429 |
|
{ |
430 |
|
Result::Sat status = |
431 |
|
(value == "sat") |
432 |
|
? Result::SAT |
433 |
|
: ((value == "unsat") ? Result::UNSAT : Result::SAT_UNKNOWN); |
434 |
|
getPrinter().toStreamCmdSetBenchmarkStatus( |
435 |
|
getOutputManager().getDumpOut(), status); |
436 |
|
} |
437 |
|
else |
438 |
|
{ |
439 |
|
getPrinter().toStreamCmdSetInfo( |
440 |
|
getOutputManager().getDumpOut(), key, value); |
441 |
|
} |
442 |
|
} |
443 |
|
|
444 |
5703 |
if (key == "filename") |
445 |
|
{ |
446 |
52 |
d_state->setFilename(value); |
447 |
|
} |
448 |
5651 |
else if (key == "smt-lib-version" && !getOptions().base.inputLanguageWasSetByUser) |
449 |
|
{ |
450 |
699 |
language::input::Language ilang = language::input::LANG_SMTLIB_V2_6; |
451 |
|
|
452 |
699 |
if (value != "2" && value != "2.6") |
453 |
|
{ |
454 |
8 |
Warning() << "SMT-LIB version " << value |
455 |
|
<< " unsupported, defaulting to language (and semantics of) " |
456 |
4 |
"SMT-LIB 2.6\n"; |
457 |
|
} |
458 |
699 |
getOptions().base.inputLanguage = ilang; |
459 |
|
// also update the output language |
460 |
699 |
if (!getOptions().base.outputLanguageWasSetByUser) |
461 |
|
{ |
462 |
699 |
language::output::Language olang = language::toOutputLanguage(ilang); |
463 |
699 |
if (d_env->getOptions().base.outputLanguage != olang) |
464 |
|
{ |
465 |
2 |
getOptions().base.outputLanguage = olang; |
466 |
2 |
*d_env->getOptions().base.out << language::SetLanguage(olang); |
467 |
|
} |
468 |
|
} |
469 |
|
} |
470 |
4952 |
else if (key == "status") |
471 |
|
{ |
472 |
3661 |
d_state->notifyExpectedStatus(value); |
473 |
|
} |
474 |
5703 |
} |
475 |
|
|
476 |
24 |
bool SmtEngine::isValidGetInfoFlag(const std::string& key) const |
477 |
|
{ |
478 |
71 |
if (key == "all-statistics" || key == "error-behavior" || key == "name" |
479 |
19 |
|| key == "version" || key == "authors" || key == "status" |
480 |
15 |
|| key == "reason-unknown" || key == "assertion-stack-levels" |
481 |
30 |
|| key == "all-options" || key == "time") |
482 |
|
{ |
483 |
18 |
return true; |
484 |
|
} |
485 |
6 |
return false; |
486 |
|
} |
487 |
|
|
488 |
18 |
std::string SmtEngine::getInfo(const std::string& key) const |
489 |
|
{ |
490 |
36 |
SmtScope smts(this); |
491 |
|
|
492 |
18 |
Trace("smt") << "SMT getInfo(" << key << ")" << endl; |
493 |
18 |
if (key == "all-statistics") |
494 |
|
{ |
495 |
1 |
return toSExpr(d_env->getStatisticsRegistry().begin(), d_env->getStatisticsRegistry().end()); |
496 |
|
} |
497 |
17 |
if (key == "error-behavior") |
498 |
|
{ |
499 |
1 |
return "immediate-exit"; |
500 |
|
} |
501 |
16 |
if (key == "name") |
502 |
|
{ |
503 |
3 |
return toSExpr(Configuration::getName()); |
504 |
|
} |
505 |
13 |
if (key == "version") |
506 |
|
{ |
507 |
1 |
return toSExpr(Configuration::getVersionString()); |
508 |
|
} |
509 |
12 |
if (key == "authors") |
510 |
|
{ |
511 |
1 |
return toSExpr(Configuration::about()); |
512 |
|
} |
513 |
11 |
if (key == "status") |
514 |
|
{ |
515 |
|
// sat | unsat | unknown |
516 |
4 |
Result status = d_state->getStatus(); |
517 |
2 |
switch (status.asSatisfiabilityResult().isSat()) |
518 |
|
{ |
519 |
|
case Result::SAT: return "sat"; |
520 |
|
case Result::UNSAT: return "unsat"; |
521 |
2 |
default: return "unknown"; |
522 |
|
} |
523 |
|
} |
524 |
9 |
if (key == "time") |
525 |
|
{ |
526 |
|
return toSExpr(std::clock()); |
527 |
|
} |
528 |
9 |
if (key == "reason-unknown") |
529 |
|
{ |
530 |
18 |
Result status = d_state->getStatus(); |
531 |
9 |
if (!status.isNull() && status.isUnknown()) |
532 |
|
{ |
533 |
12 |
std::stringstream ss; |
534 |
6 |
ss << status.whyUnknown(); |
535 |
12 |
std::string s = ss.str(); |
536 |
6 |
transform(s.begin(), s.end(), s.begin(), ::tolower); |
537 |
6 |
return s; |
538 |
|
} |
539 |
|
else |
540 |
|
{ |
541 |
|
throw RecoverableModalException( |
542 |
|
"Can't get-info :reason-unknown when the " |
543 |
3 |
"last result wasn't unknown!"); |
544 |
|
} |
545 |
|
} |
546 |
|
if (key == "assertion-stack-levels") |
547 |
|
{ |
548 |
|
size_t ulevel = d_state->getNumUserLevels(); |
549 |
|
AlwaysAssert(ulevel <= std::numeric_limits<unsigned long int>::max()); |
550 |
|
return toSExpr(ulevel); |
551 |
|
} |
552 |
|
Assert(key == "all-options"); |
553 |
|
// get the options, like all-statistics |
554 |
|
return toSExpr(options::getAll(getOptions())); |
555 |
|
} |
556 |
|
|
557 |
2461 |
void SmtEngine::debugCheckFormals(const std::vector<Node>& formals, Node func) |
558 |
|
{ |
559 |
5739 |
for (std::vector<Node>::const_iterator i = formals.begin(); |
560 |
5739 |
i != formals.end(); |
561 |
|
++i) |
562 |
|
{ |
563 |
3278 |
if((*i).getKind() != kind::BOUND_VARIABLE) { |
564 |
|
stringstream ss; |
565 |
|
ss << "All formal arguments to defined functions must be BOUND_VARIABLEs, but in the\n" |
566 |
|
<< "definition of function " << func << ", formal\n" |
567 |
|
<< " " << *i << "\n" |
568 |
|
<< "has kind " << (*i).getKind(); |
569 |
|
throw TypeCheckingExceptionPrivate(func, ss.str()); |
570 |
|
} |
571 |
|
} |
572 |
2461 |
} |
573 |
|
|
574 |
2461 |
void SmtEngine::debugCheckFunctionBody(Node formula, |
575 |
|
const std::vector<Node>& formals, |
576 |
|
Node func) |
577 |
|
{ |
578 |
|
TypeNode formulaType = |
579 |
4922 |
formula.getType(d_env->getOptions().expr.typeChecking); |
580 |
4922 |
TypeNode funcType = func.getType(); |
581 |
|
// We distinguish here between definitions of constants and functions, |
582 |
|
// because the type checking for them is subtly different. Perhaps we |
583 |
|
// should instead have SmtEngine::defineFunction() and |
584 |
|
// SmtEngine::defineConstant() for better clarity, although then that |
585 |
|
// doesn't match the SMT-LIBv2 standard... |
586 |
2461 |
if(formals.size() > 0) { |
587 |
2764 |
TypeNode rangeType = funcType.getRangeType(); |
588 |
1382 |
if(! formulaType.isComparableTo(rangeType)) { |
589 |
|
stringstream ss; |
590 |
|
ss << "Type of defined function does not match its declaration\n" |
591 |
|
<< "The function : " << func << "\n" |
592 |
|
<< "Declared type : " << rangeType << "\n" |
593 |
|
<< "The body : " << formula << "\n" |
594 |
|
<< "Body type : " << formulaType; |
595 |
|
throw TypeCheckingExceptionPrivate(func, ss.str()); |
596 |
|
} |
597 |
|
} else { |
598 |
1079 |
if(! formulaType.isComparableTo(funcType)) { |
599 |
|
stringstream ss; |
600 |
|
ss << "Declared type of defined constant does not match its definition\n" |
601 |
|
<< "The constant : " << func << "\n" |
602 |
|
<< "Declared type : " << funcType << "\n" |
603 |
|
<< "The definition : " << formula << "\n" |
604 |
|
<< "Definition type: " << formulaType; |
605 |
|
throw TypeCheckingExceptionPrivate(func, ss.str()); |
606 |
|
} |
607 |
|
} |
608 |
2461 |
} |
609 |
|
|
610 |
2269 |
void SmtEngine::defineFunction(Node func, |
611 |
|
const std::vector<Node>& formals, |
612 |
|
Node formula, |
613 |
|
bool global) |
614 |
|
{ |
615 |
4538 |
SmtScope smts(this); |
616 |
2269 |
finishInit(); |
617 |
2269 |
d_state->doPendingPops(); |
618 |
2269 |
Trace("smt") << "SMT defineFunction(" << func << ")" << endl; |
619 |
2269 |
debugCheckFormals(formals, func); |
620 |
|
|
621 |
4538 |
stringstream ss; |
622 |
|
ss << language::SetLanguage( |
623 |
|
language::SetLanguage::getLanguage(Dump.getStream())) |
624 |
2269 |
<< func; |
625 |
|
|
626 |
4538 |
DefineFunctionNodeCommand nc(ss.str(), func, formals, formula); |
627 |
2269 |
getDumpManager()->addToDump(nc, "declarations"); |
628 |
|
|
629 |
|
// type check body |
630 |
2269 |
debugCheckFunctionBody(formula, formals, func); |
631 |
|
|
632 |
|
// Substitute out any abstract values in formula |
633 |
4538 |
Node def = d_absValues->substituteAbstractValues(formula); |
634 |
2269 |
if (!formals.empty()) |
635 |
|
{ |
636 |
1211 |
NodeManager* nm = NodeManager::currentNM(); |
637 |
3633 |
def = nm->mkNode( |
638 |
2422 |
kind::LAMBDA, nm->mkNode(kind::BOUND_VAR_LIST, formals), def); |
639 |
|
} |
640 |
|
// A define-fun is treated as a (higher-order) assertion. It is provided |
641 |
|
// to the assertions object. It will be added as a top-level substitution |
642 |
|
// within this class, possibly multiple times if global is true. |
643 |
4538 |
Node feq = func.eqNode(def); |
644 |
2269 |
d_asserts->addDefineFunDefinition(feq, global); |
645 |
2269 |
} |
646 |
|
|
647 |
141 |
void SmtEngine::defineFunctionsRec( |
648 |
|
const std::vector<Node>& funcs, |
649 |
|
const std::vector<std::vector<Node>>& formals, |
650 |
|
const std::vector<Node>& formulas, |
651 |
|
bool global) |
652 |
|
{ |
653 |
282 |
SmtScope smts(this); |
654 |
141 |
finishInit(); |
655 |
141 |
d_state->doPendingPops(); |
656 |
141 |
Trace("smt") << "SMT defineFunctionsRec(...)" << endl; |
657 |
|
|
658 |
141 |
if (funcs.size() != formals.size() && funcs.size() != formulas.size()) |
659 |
|
{ |
660 |
|
stringstream ss; |
661 |
|
ss << "Number of functions, formals, and function bodies passed to " |
662 |
|
"defineFunctionsRec do not match:" |
663 |
|
<< "\n" |
664 |
|
<< " #functions : " << funcs.size() << "\n" |
665 |
|
<< " #arg lists : " << formals.size() << "\n" |
666 |
|
<< " #function bodies : " << formulas.size() << "\n"; |
667 |
|
throw ModalException(ss.str()); |
668 |
|
} |
669 |
333 |
for (unsigned i = 0, size = funcs.size(); i < size; i++) |
670 |
|
{ |
671 |
|
// check formal argument list |
672 |
192 |
debugCheckFormals(formals[i], funcs[i]); |
673 |
|
// type check body |
674 |
192 |
debugCheckFunctionBody(formulas[i], formals[i], funcs[i]); |
675 |
|
} |
676 |
|
|
677 |
141 |
if (Dump.isOn("raw-benchmark")) |
678 |
|
{ |
679 |
|
getPrinter().toStreamCmdDefineFunctionRec( |
680 |
|
getOutputManager().getDumpOut(), funcs, formals, formulas); |
681 |
|
} |
682 |
|
|
683 |
141 |
NodeManager* nm = getNodeManager(); |
684 |
333 |
for (unsigned i = 0, size = funcs.size(); i < size; i++) |
685 |
|
{ |
686 |
|
// we assert a quantified formula |
687 |
384 |
Node func_app; |
688 |
|
// make the function application |
689 |
192 |
if (formals[i].empty()) |
690 |
|
{ |
691 |
|
// it has no arguments |
692 |
21 |
func_app = funcs[i]; |
693 |
|
} |
694 |
|
else |
695 |
|
{ |
696 |
342 |
std::vector<Node> children; |
697 |
171 |
children.push_back(funcs[i]); |
698 |
171 |
children.insert(children.end(), formals[i].begin(), formals[i].end()); |
699 |
171 |
func_app = nm->mkNode(kind::APPLY_UF, children); |
700 |
|
} |
701 |
384 |
Node lem = nm->mkNode(kind::EQUAL, func_app, formulas[i]); |
702 |
192 |
if (!formals[i].empty()) |
703 |
|
{ |
704 |
|
// set the attribute to denote this is a function definition |
705 |
342 |
Node aexpr = nm->mkNode(kind::INST_ATTRIBUTE, func_app); |
706 |
171 |
aexpr = nm->mkNode(kind::INST_PATTERN_LIST, aexpr); |
707 |
|
FunDefAttribute fda; |
708 |
171 |
func_app.setAttribute(fda, true); |
709 |
|
// make the quantified formula |
710 |
342 |
Node boundVars = nm->mkNode(kind::BOUND_VAR_LIST, formals[i]); |
711 |
171 |
lem = nm->mkNode(kind::FORALL, boundVars, lem, aexpr); |
712 |
|
} |
713 |
|
// assert the quantified formula |
714 |
|
// notice we don't call assertFormula directly, since this would |
715 |
|
// duplicate the output on raw-benchmark. |
716 |
|
// add define recursive definition to the assertions |
717 |
192 |
d_asserts->addDefineFunDefinition(lem, global); |
718 |
|
} |
719 |
141 |
} |
720 |
|
|
721 |
16 |
void SmtEngine::defineFunctionRec(Node func, |
722 |
|
const std::vector<Node>& formals, |
723 |
|
Node formula, |
724 |
|
bool global) |
725 |
|
{ |
726 |
32 |
std::vector<Node> funcs; |
727 |
16 |
funcs.push_back(func); |
728 |
32 |
std::vector<std::vector<Node>> formals_multi; |
729 |
16 |
formals_multi.push_back(formals); |
730 |
32 |
std::vector<Node> formulas; |
731 |
16 |
formulas.push_back(formula); |
732 |
16 |
defineFunctionsRec(funcs, formals_multi, formulas, global); |
733 |
16 |
} |
734 |
|
|
735 |
89574 |
Result SmtEngine::quickCheck() { |
736 |
89574 |
Assert(d_state->isFullyInited()); |
737 |
89574 |
Trace("smt") << "SMT quickCheck()" << endl; |
738 |
89574 |
const std::string& filename = d_state->getFilename(); |
739 |
|
return Result( |
740 |
89574 |
Result::ENTAILMENT_UNKNOWN, Result::REQUIRES_FULL_CHECK, filename); |
741 |
|
} |
742 |
|
|
743 |
5135 |
Model* SmtEngine::getAvailableModel(const char* c) const |
744 |
|
{ |
745 |
5135 |
if (!d_env->getOptions().theory.assignFunctionValues) |
746 |
|
{ |
747 |
|
std::stringstream ss; |
748 |
|
ss << "Cannot " << c << " when --assign-function-values is false."; |
749 |
|
throw RecoverableModalException(ss.str().c_str()); |
750 |
|
} |
751 |
|
|
752 |
10270 |
if (d_state->getMode() != SmtMode::SAT |
753 |
5135 |
&& d_state->getMode() != SmtMode::SAT_UNKNOWN) |
754 |
|
{ |
755 |
18 |
std::stringstream ss; |
756 |
|
ss << "Cannot " << c |
757 |
9 |
<< " unless immediately preceded by SAT/NOT_ENTAILED or UNKNOWN " |
758 |
9 |
"response."; |
759 |
9 |
throw RecoverableModalException(ss.str().c_str()); |
760 |
|
} |
761 |
|
|
762 |
5126 |
if (!d_env->getOptions().smt.produceModels) |
763 |
|
{ |
764 |
4 |
std::stringstream ss; |
765 |
2 |
ss << "Cannot " << c << " when produce-models options is off."; |
766 |
2 |
throw ModalException(ss.str().c_str()); |
767 |
|
} |
768 |
|
|
769 |
5124 |
TheoryEngine* te = d_smtSolver->getTheoryEngine(); |
770 |
5124 |
Assert(te != nullptr); |
771 |
5124 |
TheoryModel* m = te->getBuiltModel(); |
772 |
|
|
773 |
5123 |
if (m == nullptr) |
774 |
|
{ |
775 |
|
std::stringstream ss; |
776 |
|
ss << "Cannot " << c |
777 |
|
<< " since model is not available. Perhaps the most recent call to " |
778 |
|
"check-sat was interrupted?"; |
779 |
|
throw RecoverableModalException(ss.str().c_str()); |
780 |
|
} |
781 |
|
|
782 |
5123 |
return d_model.get(); |
783 |
|
} |
784 |
|
|
785 |
117 |
QuantifiersEngine* SmtEngine::getAvailableQuantifiersEngine(const char* c) const |
786 |
|
{ |
787 |
117 |
QuantifiersEngine* qe = d_smtSolver->getQuantifiersEngine(); |
788 |
117 |
if (qe == nullptr) |
789 |
|
{ |
790 |
|
std::stringstream ss; |
791 |
|
ss << "Cannot " << c << " when quantifiers are not present."; |
792 |
|
throw ModalException(ss.str().c_str()); |
793 |
|
} |
794 |
117 |
return qe; |
795 |
|
} |
796 |
|
|
797 |
4869 |
void SmtEngine::notifyPushPre() { d_smtSolver->processAssertions(*d_asserts); } |
798 |
|
|
799 |
4869 |
void SmtEngine::notifyPushPost() |
800 |
|
{ |
801 |
9738 |
TimerStat::CodeTimer pushPopTimer(d_stats->d_pushPopTime); |
802 |
4869 |
Assert(getPropEngine() != nullptr); |
803 |
4869 |
getPropEngine()->push(); |
804 |
4869 |
} |
805 |
|
|
806 |
4869 |
void SmtEngine::notifyPopPre() |
807 |
|
{ |
808 |
9738 |
TimerStat::CodeTimer pushPopTimer(d_stats->d_pushPopTime); |
809 |
4869 |
PropEngine* pe = getPropEngine(); |
810 |
4869 |
Assert(pe != nullptr); |
811 |
4869 |
pe->pop(); |
812 |
4869 |
} |
813 |
|
|
814 |
15176 |
void SmtEngine::notifyPostSolvePre() |
815 |
|
{ |
816 |
15176 |
PropEngine* pe = getPropEngine(); |
817 |
15176 |
Assert(pe != nullptr); |
818 |
15176 |
pe->resetTrail(); |
819 |
15176 |
} |
820 |
|
|
821 |
15176 |
void SmtEngine::notifyPostSolvePost() |
822 |
|
{ |
823 |
15176 |
TheoryEngine* te = getTheoryEngine(); |
824 |
15176 |
Assert(te != nullptr); |
825 |
15176 |
te->postsolve(); |
826 |
15176 |
} |
827 |
|
|
828 |
12754 |
Result SmtEngine::checkSat() |
829 |
|
{ |
830 |
25508 |
Node nullNode; |
831 |
25490 |
return checkSat(nullNode); |
832 |
|
} |
833 |
|
|
834 |
13341 |
Result SmtEngine::checkSat(const Node& assumption) |
835 |
|
{ |
836 |
13341 |
if (Dump.isOn("benchmark")) |
837 |
|
{ |
838 |
4 |
getPrinter().toStreamCmdCheckSat(getOutputManager().getDumpOut(), |
839 |
2 |
assumption); |
840 |
|
} |
841 |
26682 |
std::vector<Node> assump; |
842 |
13341 |
if (!assumption.isNull()) |
843 |
|
{ |
844 |
587 |
assump.push_back(assumption); |
845 |
|
} |
846 |
26663 |
return checkSatInternal(assump, false); |
847 |
|
} |
848 |
|
|
849 |
996 |
Result SmtEngine::checkSat(const std::vector<Node>& assumptions) |
850 |
|
{ |
851 |
996 |
if (Dump.isOn("benchmark")) |
852 |
|
{ |
853 |
|
if (assumptions.empty()) |
854 |
|
{ |
855 |
|
getPrinter().toStreamCmdCheckSat(getOutputManager().getDumpOut()); |
856 |
|
} |
857 |
|
else |
858 |
|
{ |
859 |
|
getPrinter().toStreamCmdCheckSatAssuming(getOutputManager().getDumpOut(), |
860 |
|
assumptions); |
861 |
|
} |
862 |
|
} |
863 |
996 |
return checkSatInternal(assumptions, false); |
864 |
|
} |
865 |
|
|
866 |
631 |
Result SmtEngine::checkEntailed(const Node& node) |
867 |
|
{ |
868 |
631 |
if (Dump.isOn("benchmark")) |
869 |
|
{ |
870 |
|
getPrinter().toStreamCmdQuery(getOutputManager().getDumpOut(), node); |
871 |
|
} |
872 |
1258 |
return checkSatInternal( |
873 |
1262 |
node.isNull() ? std::vector<Node>() : std::vector<Node>{node}, |
874 |
|
true) |
875 |
1254 |
.asEntailmentResult(); |
876 |
|
} |
877 |
|
|
878 |
2 |
Result SmtEngine::checkEntailed(const std::vector<Node>& nodes) |
879 |
|
{ |
880 |
2 |
return checkSatInternal(nodes, true).asEntailmentResult(); |
881 |
|
} |
882 |
|
|
883 |
14970 |
Result SmtEngine::checkSatInternal(const std::vector<Node>& assumptions, |
884 |
|
bool isEntailmentCheck) |
885 |
|
{ |
886 |
|
try |
887 |
|
{ |
888 |
29940 |
SmtScope smts(this); |
889 |
14970 |
finishInit(); |
890 |
|
|
891 |
29940 |
Trace("smt") << "SmtEngine::" |
892 |
29940 |
<< (isEntailmentCheck ? "checkEntailed" : "checkSat") << "(" |
893 |
14970 |
<< assumptions << ")" << endl; |
894 |
|
// check the satisfiability with the solver object |
895 |
|
Result r = d_smtSolver->checkSatisfiability( |
896 |
29919 |
*d_asserts.get(), assumptions, isEntailmentCheck); |
897 |
|
|
898 |
29898 |
Trace("smt") << "SmtEngine::" << (isEntailmentCheck ? "query" : "checkSat") |
899 |
14949 |
<< "(" << assumptions << ") => " << r << endl; |
900 |
|
|
901 |
|
// Check that SAT results generate a model correctly. |
902 |
14949 |
if (d_env->getOptions().smt.checkModels) |
903 |
|
{ |
904 |
2551 |
if (r.asSatisfiabilityResult().isSat() == Result::SAT) |
905 |
|
{ |
906 |
2152 |
checkModel(); |
907 |
|
} |
908 |
|
} |
909 |
|
// Check that UNSAT results generate a proof correctly. |
910 |
29894 |
if (d_env->getOptions().smt.checkProofs |
911 |
14947 |
|| d_env->getOptions().proof.proofEagerChecking) |
912 |
|
{ |
913 |
2256 |
if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) |
914 |
|
{ |
915 |
2732 |
if ((d_env->getOptions().smt.checkProofs |
916 |
|
|| d_env->getOptions().proof.proofEagerChecking) |
917 |
2732 |
&& !d_env->getOptions().smt.produceProofs) |
918 |
|
{ |
919 |
|
throw ModalException( |
920 |
|
"Cannot check-proofs because proofs were disabled."); |
921 |
|
} |
922 |
1366 |
checkProof(); |
923 |
|
} |
924 |
|
} |
925 |
|
// Check that UNSAT results generate an unsat core correctly. |
926 |
14947 |
if (d_env->getOptions().smt.checkUnsatCores) |
927 |
|
{ |
928 |
2366 |
if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) |
929 |
|
{ |
930 |
2728 |
TimerStat::CodeTimer checkUnsatCoreTimer(d_stats->d_checkUnsatCoreTime); |
931 |
1364 |
checkUnsatCore(); |
932 |
|
} |
933 |
|
} |
934 |
14947 |
if (d_env->getOptions().base.statisticsEveryQuery) |
935 |
|
{ |
936 |
|
printStatisticsDiff(); |
937 |
|
} |
938 |
14947 |
return r; |
939 |
|
} |
940 |
|
catch (UnsafeInterruptException& e) |
941 |
|
{ |
942 |
|
AlwaysAssert(getResourceManager()->out()); |
943 |
|
// Notice that we do not notify the state of this result. If we wanted to |
944 |
|
// make the solver resume a working state after an interupt, then we would |
945 |
|
// implement a different callback and use it here, e.g. |
946 |
|
// d_state.notifyCheckSatInterupt. |
947 |
|
Result::UnknownExplanation why = getResourceManager()->outOfResources() |
948 |
|
? Result::RESOURCEOUT |
949 |
|
: Result::TIMEOUT; |
950 |
|
|
951 |
|
if (d_env->getOptions().base.statisticsEveryQuery) |
952 |
|
{ |
953 |
|
printStatisticsDiff(); |
954 |
|
} |
955 |
|
return Result(Result::SAT_UNKNOWN, why, d_state->getFilename()); |
956 |
|
} |
957 |
|
} |
958 |
|
|
959 |
13 |
std::vector<Node> SmtEngine::getUnsatAssumptions(void) |
960 |
|
{ |
961 |
13 |
Trace("smt") << "SMT getUnsatAssumptions()" << endl; |
962 |
26 |
SmtScope smts(this); |
963 |
13 |
if (!d_env->getOptions().smt.unsatAssumptions) |
964 |
|
{ |
965 |
|
throw ModalException( |
966 |
|
"Cannot get unsat assumptions when produce-unsat-assumptions option " |
967 |
|
"is off."); |
968 |
|
} |
969 |
13 |
if (d_state->getMode() != SmtMode::UNSAT) |
970 |
|
{ |
971 |
|
throw RecoverableModalException( |
972 |
|
"Cannot get unsat assumptions unless immediately preceded by " |
973 |
|
"UNSAT/ENTAILED."); |
974 |
|
} |
975 |
13 |
finishInit(); |
976 |
13 |
if (Dump.isOn("benchmark")) |
977 |
|
{ |
978 |
|
getPrinter().toStreamCmdGetUnsatAssumptions( |
979 |
|
getOutputManager().getDumpOut()); |
980 |
|
} |
981 |
26 |
UnsatCore core = getUnsatCoreInternal(); |
982 |
13 |
std::vector<Node> res; |
983 |
13 |
std::vector<Node>& assumps = d_asserts->getAssumptions(); |
984 |
37 |
for (const Node& e : assumps) |
985 |
|
{ |
986 |
24 |
if (std::find(core.begin(), core.end(), e) != core.end()) |
987 |
|
{ |
988 |
16 |
res.push_back(e); |
989 |
|
} |
990 |
|
} |
991 |
26 |
return res; |
992 |
|
} |
993 |
|
|
994 |
89575 |
Result SmtEngine::assertFormula(const Node& formula) |
995 |
|
{ |
996 |
179150 |
SmtScope smts(this); |
997 |
89575 |
finishInit(); |
998 |
89574 |
d_state->doPendingPops(); |
999 |
|
|
1000 |
89574 |
Trace("smt") << "SmtEngine::assertFormula(" << formula << ")" << endl; |
1001 |
|
|
1002 |
89574 |
if (Dump.isOn("raw-benchmark")) |
1003 |
|
{ |
1004 |
3 |
getPrinter().toStreamCmdAssert(getOutputManager().getDumpOut(), formula); |
1005 |
|
} |
1006 |
|
|
1007 |
|
// Substitute out any abstract values in ex |
1008 |
179148 |
Node n = d_absValues->substituteAbstractValues(formula); |
1009 |
|
|
1010 |
89574 |
d_asserts->assertFormula(n); |
1011 |
179148 |
return quickCheck().asEntailmentResult(); |
1012 |
|
}/* SmtEngine::assertFormula() */ |
1013 |
|
|
1014 |
|
/* |
1015 |
|
-------------------------------------------------------------------------- |
1016 |
|
Handling SyGuS commands |
1017 |
|
-------------------------------------------------------------------------- |
1018 |
|
*/ |
1019 |
|
|
1020 |
413 |
void SmtEngine::declareSygusVar(Node var) |
1021 |
|
{ |
1022 |
826 |
SmtScope smts(this); |
1023 |
413 |
d_sygusSolver->declareSygusVar(var); |
1024 |
413 |
if (Dump.isOn("raw-benchmark")) |
1025 |
|
{ |
1026 |
|
getPrinter().toStreamCmdDeclareVar( |
1027 |
|
getOutputManager().getDumpOut(), var, var.getType()); |
1028 |
|
} |
1029 |
|
// don't need to set that the conjecture is stale |
1030 |
413 |
} |
1031 |
|
|
1032 |
321 |
void SmtEngine::declareSynthFun(Node func, |
1033 |
|
TypeNode sygusType, |
1034 |
|
bool isInv, |
1035 |
|
const std::vector<Node>& vars) |
1036 |
|
{ |
1037 |
642 |
SmtScope smts(this); |
1038 |
321 |
d_state->doPendingPops(); |
1039 |
321 |
d_sygusSolver->declareSynthFun(func, sygusType, isInv, vars); |
1040 |
|
|
1041 |
|
// !!! TEMPORARY: We cannot construct a SynthFunCommand since we cannot |
1042 |
|
// construct a Term-level Grammar from a Node-level sygus TypeNode. Thus we |
1043 |
|
// must print the command using the Node-level utility method for now. |
1044 |
|
|
1045 |
321 |
if (Dump.isOn("raw-benchmark")) |
1046 |
|
{ |
1047 |
|
getPrinter().toStreamCmdSynthFun( |
1048 |
|
getOutputManager().getDumpOut(), func, vars, isInv, sygusType); |
1049 |
|
} |
1050 |
321 |
} |
1051 |
|
void SmtEngine::declareSynthFun(Node func, |
1052 |
|
bool isInv, |
1053 |
|
const std::vector<Node>& vars) |
1054 |
|
{ |
1055 |
|
// use a null sygus type |
1056 |
|
TypeNode sygusType; |
1057 |
|
declareSynthFun(func, sygusType, isInv, vars); |
1058 |
|
} |
1059 |
|
|
1060 |
616 |
void SmtEngine::assertSygusConstraint(Node constraint) |
1061 |
|
{ |
1062 |
1232 |
SmtScope smts(this); |
1063 |
616 |
finishInit(); |
1064 |
616 |
d_sygusSolver->assertSygusConstraint(constraint); |
1065 |
616 |
if (Dump.isOn("raw-benchmark")) |
1066 |
|
{ |
1067 |
|
getPrinter().toStreamCmdConstraint(getOutputManager().getDumpOut(), |
1068 |
|
constraint); |
1069 |
|
} |
1070 |
616 |
} |
1071 |
|
|
1072 |
18 |
void SmtEngine::assertSygusInvConstraint(Node inv, |
1073 |
|
Node pre, |
1074 |
|
Node trans, |
1075 |
|
Node post) |
1076 |
|
{ |
1077 |
36 |
SmtScope smts(this); |
1078 |
18 |
finishInit(); |
1079 |
18 |
d_sygusSolver->assertSygusInvConstraint(inv, pre, trans, post); |
1080 |
18 |
if (Dump.isOn("raw-benchmark")) |
1081 |
|
{ |
1082 |
|
getPrinter().toStreamCmdInvConstraint( |
1083 |
|
getOutputManager().getDumpOut(), inv, pre, trans, post); |
1084 |
|
} |
1085 |
18 |
} |
1086 |
|
|
1087 |
206 |
Result SmtEngine::checkSynth() |
1088 |
|
{ |
1089 |
412 |
SmtScope smts(this); |
1090 |
206 |
finishInit(); |
1091 |
403 |
return d_sygusSolver->checkSynth(*d_asserts); |
1092 |
|
} |
1093 |
|
|
1094 |
|
/* |
1095 |
|
-------------------------------------------------------------------------- |
1096 |
|
End of Handling SyGuS commands |
1097 |
|
-------------------------------------------------------------------------- |
1098 |
|
*/ |
1099 |
|
|
1100 |
5 |
void SmtEngine::declarePool(const Node& p, const std::vector<Node>& initValue) |
1101 |
|
{ |
1102 |
5 |
Assert(p.isVar() && p.getType().isSet()); |
1103 |
5 |
finishInit(); |
1104 |
5 |
QuantifiersEngine* qe = getAvailableQuantifiersEngine("declareTermPool"); |
1105 |
5 |
qe->declarePool(p, initValue); |
1106 |
5 |
} |
1107 |
|
|
1108 |
68 |
Node SmtEngine::simplify(const Node& ex) |
1109 |
|
{ |
1110 |
136 |
SmtScope smts(this); |
1111 |
68 |
finishInit(); |
1112 |
68 |
d_state->doPendingPops(); |
1113 |
|
// ensure we've processed assertions |
1114 |
68 |
d_smtSolver->processAssertions(*d_asserts); |
1115 |
136 |
return d_pp->simplify(ex); |
1116 |
|
} |
1117 |
|
|
1118 |
1913 |
Node SmtEngine::expandDefinitions(const Node& ex) |
1119 |
|
{ |
1120 |
1913 |
getResourceManager()->spendResource(Resource::PreprocessStep); |
1121 |
3826 |
SmtScope smts(this); |
1122 |
1913 |
finishInit(); |
1123 |
1913 |
d_state->doPendingPops(); |
1124 |
3826 |
return d_pp->expandDefinitions(ex); |
1125 |
|
} |
1126 |
|
|
1127 |
|
// TODO(#1108): Simplify the error reporting of this method. |
1128 |
2913 |
Node SmtEngine::getValue(const Node& ex) const |
1129 |
|
{ |
1130 |
5826 |
SmtScope smts(this); |
1131 |
|
|
1132 |
2913 |
Trace("smt") << "SMT getValue(" << ex << ")" << endl; |
1133 |
2913 |
if (Dump.isOn("benchmark")) |
1134 |
|
{ |
1135 |
|
getPrinter().toStreamCmdGetValue(d_outMgr.getDumpOut(), {ex}); |
1136 |
|
} |
1137 |
5826 |
TypeNode expectedType = ex.getType(); |
1138 |
|
|
1139 |
|
// Substitute out any abstract values in ex and expand |
1140 |
5826 |
Node n = d_pp->expandDefinitions(ex); |
1141 |
|
|
1142 |
2913 |
Trace("smt") << "--- getting value of " << n << endl; |
1143 |
|
// There are two ways model values for terms are computed (for historical |
1144 |
|
// reasons). One way is that used in check-model; the other is that |
1145 |
|
// used by the Model classes. It's not clear to me exactly how these |
1146 |
|
// two are different, but they need to be unified. This ugly hack here |
1147 |
|
// is to fix bug 554 until we can revamp boolean-terms and models [MGD] |
1148 |
|
|
1149 |
|
//AJR : necessary? |
1150 |
2913 |
if(!n.getType().isFunction()) { |
1151 |
2906 |
n = Rewriter::rewrite(n); |
1152 |
|
} |
1153 |
|
|
1154 |
2913 |
Trace("smt") << "--- getting value of " << n << endl; |
1155 |
2913 |
Model* m = getAvailableModel("get-value"); |
1156 |
2907 |
Assert(m != nullptr); |
1157 |
2907 |
Node resultNode = m->getValue(n); |
1158 |
2907 |
Trace("smt") << "--- got value " << n << " = " << resultNode << endl; |
1159 |
2907 |
Trace("smt") << "--- type " << resultNode.getType() << endl; |
1160 |
2907 |
Trace("smt") << "--- expected type " << expectedType << endl; |
1161 |
|
|
1162 |
|
// type-check the result we got |
1163 |
|
// Notice that lambdas have function type, which does not respect the subtype |
1164 |
|
// relation, so we ignore them here. |
1165 |
2907 |
Assert(resultNode.isNull() || resultNode.getKind() == kind::LAMBDA |
1166 |
|
|| resultNode.getType().isSubtypeOf(expectedType)) |
1167 |
|
<< "Run with -t smt for details."; |
1168 |
|
|
1169 |
|
// Ensure it's a constant, or a lambda (for uninterpreted functions). This |
1170 |
|
// assertion only holds for models that do not have approximate values. |
1171 |
2907 |
Assert(m->hasApproximations() || resultNode.getKind() == kind::LAMBDA |
1172 |
|
|| resultNode.isConst()); |
1173 |
|
|
1174 |
5814 |
if (d_env->getOptions().smt.abstractValues |
1175 |
5814 |
&& resultNode.getType().isArray()) |
1176 |
|
{ |
1177 |
8 |
resultNode = d_absValues->mkAbstractValue(resultNode); |
1178 |
8 |
Trace("smt") << "--- abstract value >> " << resultNode << endl; |
1179 |
|
} |
1180 |
|
|
1181 |
5814 |
return resultNode; |
1182 |
|
} |
1183 |
|
|
1184 |
|
std::vector<Node> SmtEngine::getValues(const std::vector<Node>& exprs) |
1185 |
|
{ |
1186 |
|
std::vector<Node> result; |
1187 |
|
for (const Node& e : exprs) |
1188 |
|
{ |
1189 |
|
result.push_back(getValue(e)); |
1190 |
|
} |
1191 |
|
return result; |
1192 |
|
} |
1193 |
|
|
1194 |
|
// TODO(#1108): Simplify the error reporting of this method. |
1195 |
30 |
Model* SmtEngine::getModel() { |
1196 |
30 |
Trace("smt") << "SMT getModel()" << endl; |
1197 |
60 |
SmtScope smts(this); |
1198 |
|
|
1199 |
30 |
finishInit(); |
1200 |
|
|
1201 |
30 |
if (Dump.isOn("benchmark")) |
1202 |
|
{ |
1203 |
|
getPrinter().toStreamCmdGetModel(getOutputManager().getDumpOut()); |
1204 |
|
} |
1205 |
|
|
1206 |
30 |
Model* m = getAvailableModel("get model"); |
1207 |
|
|
1208 |
|
// Since model m is being returned to the user, we must ensure that this |
1209 |
|
// model object remains valid with future check-sat calls. Hence, we set |
1210 |
|
// the theory engine into "eager model building" mode. TODO #2648: revisit. |
1211 |
25 |
TheoryEngine* te = getTheoryEngine(); |
1212 |
25 |
Assert(te != nullptr); |
1213 |
25 |
te->setEagerModelBuilding(); |
1214 |
|
|
1215 |
50 |
if (d_env->getOptions().smt.modelCoresMode |
1216 |
25 |
!= options::ModelCoresMode::NONE) |
1217 |
|
{ |
1218 |
|
// If we enabled model cores, we compute a model core for m based on our |
1219 |
|
// (expanded) assertions using the model core builder utility |
1220 |
|
std::vector<Node> eassertsProc = getExpandedAssertions(); |
1221 |
|
ModelCoreBuilder::setModelCore(eassertsProc, |
1222 |
|
m->getTheoryModel(), |
1223 |
|
d_env->getOptions().smt.modelCoresMode); |
1224 |
|
} |
1225 |
|
// set the information on the SMT-level model |
1226 |
25 |
Assert(m != nullptr); |
1227 |
25 |
m->d_inputName = d_state->getFilename(); |
1228 |
25 |
m->d_isKnownSat = (d_state->getMode() == SmtMode::SAT); |
1229 |
50 |
return m; |
1230 |
|
} |
1231 |
|
|
1232 |
18 |
Result SmtEngine::blockModel() |
1233 |
|
{ |
1234 |
18 |
Trace("smt") << "SMT blockModel()" << endl; |
1235 |
36 |
SmtScope smts(this); |
1236 |
|
|
1237 |
18 |
finishInit(); |
1238 |
|
|
1239 |
18 |
if (Dump.isOn("benchmark")) |
1240 |
|
{ |
1241 |
|
getPrinter().toStreamCmdBlockModel(getOutputManager().getDumpOut()); |
1242 |
|
} |
1243 |
|
|
1244 |
18 |
Model* m = getAvailableModel("block model"); |
1245 |
|
|
1246 |
36 |
if (d_env->getOptions().smt.blockModelsMode |
1247 |
18 |
== options::BlockModelsMode::NONE) |
1248 |
|
{ |
1249 |
4 |
std::stringstream ss; |
1250 |
2 |
ss << "Cannot block model when block-models is set to none."; |
1251 |
2 |
throw RecoverableModalException(ss.str().c_str()); |
1252 |
|
} |
1253 |
|
|
1254 |
|
// get expanded assertions |
1255 |
32 |
std::vector<Node> eassertsProc = getExpandedAssertions(); |
1256 |
|
Node eblocker = |
1257 |
|
ModelBlocker::getModelBlocker(eassertsProc, |
1258 |
|
m->getTheoryModel(), |
1259 |
32 |
d_env->getOptions().smt.blockModelsMode); |
1260 |
16 |
Trace("smt") << "Block formula: " << eblocker << std::endl; |
1261 |
32 |
return assertFormula(eblocker); |
1262 |
|
} |
1263 |
|
|
1264 |
12 |
Result SmtEngine::blockModelValues(const std::vector<Node>& exprs) |
1265 |
|
{ |
1266 |
12 |
Trace("smt") << "SMT blockModelValues()" << endl; |
1267 |
24 |
SmtScope smts(this); |
1268 |
|
|
1269 |
12 |
finishInit(); |
1270 |
|
|
1271 |
12 |
if (Dump.isOn("benchmark")) |
1272 |
|
{ |
1273 |
|
getPrinter().toStreamCmdBlockModelValues(getOutputManager().getDumpOut(), |
1274 |
|
exprs); |
1275 |
|
} |
1276 |
|
|
1277 |
12 |
Model* m = getAvailableModel("block model values"); |
1278 |
|
|
1279 |
|
// get expanded assertions |
1280 |
22 |
std::vector<Node> eassertsProc = getExpandedAssertions(); |
1281 |
|
// we always do block model values mode here |
1282 |
|
Node eblocker = |
1283 |
|
ModelBlocker::getModelBlocker(eassertsProc, |
1284 |
|
m->getTheoryModel(), |
1285 |
|
options::BlockModelsMode::VALUES, |
1286 |
20 |
exprs); |
1287 |
20 |
return assertFormula(eblocker); |
1288 |
|
} |
1289 |
|
|
1290 |
10 |
std::pair<Node, Node> SmtEngine::getSepHeapAndNilExpr(void) |
1291 |
|
{ |
1292 |
10 |
if (!getLogicInfo().isTheoryEnabled(THEORY_SEP)) |
1293 |
|
{ |
1294 |
|
const char* msg = |
1295 |
|
"Cannot obtain separation logic expressions if not using the " |
1296 |
|
"separation logic theory."; |
1297 |
|
throw RecoverableModalException(msg); |
1298 |
|
} |
1299 |
20 |
NodeManagerScope nms(getNodeManager()); |
1300 |
20 |
Node heap; |
1301 |
20 |
Node nil; |
1302 |
10 |
Model* m = getAvailableModel("get separation logic heap and nil"); |
1303 |
10 |
TheoryModel* tm = m->getTheoryModel(); |
1304 |
10 |
if (!tm->getHeapModel(heap, nil)) |
1305 |
|
{ |
1306 |
4 |
const char* msg = |
1307 |
|
"Failed to obtain heap/nil " |
1308 |
|
"expressions from theory model."; |
1309 |
4 |
throw RecoverableModalException(msg); |
1310 |
|
} |
1311 |
12 |
return std::make_pair(heap, nil); |
1312 |
|
} |
1313 |
|
|
1314 |
94 |
std::vector<Node> SmtEngine::getExpandedAssertions() |
1315 |
|
{ |
1316 |
186 |
std::vector<Node> easserts = getAssertions(); |
1317 |
|
// must expand definitions |
1318 |
92 |
std::vector<Node> eassertsProc; |
1319 |
184 |
std::unordered_map<Node, Node> cache; |
1320 |
382 |
for (const Node& e : easserts) |
1321 |
|
{ |
1322 |
580 |
Node eae = d_pp->expandDefinitions(e, cache); |
1323 |
290 |
eassertsProc.push_back(eae); |
1324 |
|
} |
1325 |
184 |
return eassertsProc; |
1326 |
|
} |
1327 |
26 |
Env& SmtEngine::getEnv() { return *d_env.get(); } |
1328 |
|
|
1329 |
121 |
void SmtEngine::declareSepHeap(TypeNode locT, TypeNode dataT) |
1330 |
|
{ |
1331 |
121 |
if (!getLogicInfo().isTheoryEnabled(THEORY_SEP)) |
1332 |
|
{ |
1333 |
|
const char* msg = |
1334 |
|
"Cannot declare heap if not using the separation logic theory."; |
1335 |
|
throw RecoverableModalException(msg); |
1336 |
|
} |
1337 |
242 |
SmtScope smts(this); |
1338 |
121 |
finishInit(); |
1339 |
121 |
TheoryEngine* te = getTheoryEngine(); |
1340 |
123 |
te->declareSepHeap(locT, dataT); |
1341 |
119 |
} |
1342 |
|
|
1343 |
1364 |
bool SmtEngine::getSepHeapTypes(TypeNode& locT, TypeNode& dataT) |
1344 |
|
{ |
1345 |
2728 |
SmtScope smts(this); |
1346 |
1364 |
finishInit(); |
1347 |
1364 |
TheoryEngine* te = getTheoryEngine(); |
1348 |
2728 |
return te->getSepHeapTypes(locT, dataT); |
1349 |
|
} |
1350 |
|
|
1351 |
5 |
Node SmtEngine::getSepHeapExpr() { return getSepHeapAndNilExpr().first; } |
1352 |
|
|
1353 |
5 |
Node SmtEngine::getSepNilExpr() { return getSepHeapAndNilExpr().second; } |
1354 |
|
|
1355 |
1366 |
void SmtEngine::checkProof() |
1356 |
|
{ |
1357 |
1366 |
Assert(d_env->getOptions().smt.produceProofs); |
1358 |
|
// internal check the proof |
1359 |
1366 |
PropEngine* pe = getPropEngine(); |
1360 |
1366 |
Assert(pe != nullptr); |
1361 |
1366 |
if (d_env->getOptions().proof.proofEagerChecking) |
1362 |
|
{ |
1363 |
|
pe->checkProof(d_asserts->getAssertionList()); |
1364 |
|
} |
1365 |
1366 |
Assert(pe->getProof() != nullptr); |
1366 |
2732 |
std::shared_ptr<ProofNode> pePfn = pe->getProof(); |
1367 |
1366 |
if (d_env->getOptions().smt.checkProofs) |
1368 |
|
{ |
1369 |
1366 |
d_pfManager->checkProof(pePfn, *d_asserts); |
1370 |
|
} |
1371 |
1366 |
} |
1372 |
|
|
1373 |
4643740 |
StatisticsRegistry& SmtEngine::getStatisticsRegistry() |
1374 |
|
{ |
1375 |
4643740 |
return d_env->getStatisticsRegistry(); |
1376 |
|
} |
1377 |
|
|
1378 |
1420 |
UnsatCore SmtEngine::getUnsatCoreInternal() |
1379 |
|
{ |
1380 |
1420 |
if (!d_env->getOptions().smt.unsatCores) |
1381 |
|
{ |
1382 |
|
throw ModalException( |
1383 |
|
"Cannot get an unsat core when produce-unsat-cores or produce-proofs " |
1384 |
|
"option is off."); |
1385 |
|
} |
1386 |
1420 |
if (d_state->getMode() != SmtMode::UNSAT) |
1387 |
|
{ |
1388 |
|
throw RecoverableModalException( |
1389 |
|
"Cannot get an unsat core unless immediately preceded by " |
1390 |
|
"UNSAT/ENTAILED response."); |
1391 |
|
} |
1392 |
|
// generate with new proofs |
1393 |
1420 |
PropEngine* pe = getPropEngine(); |
1394 |
1420 |
Assert(pe != nullptr); |
1395 |
|
|
1396 |
2840 |
std::shared_ptr<ProofNode> pepf; |
1397 |
1420 |
if (options::unsatCoresMode() == options::UnsatCoresMode::ASSUMPTIONS) |
1398 |
|
{ |
1399 |
1369 |
pepf = pe->getRefutation(); |
1400 |
|
} |
1401 |
|
else |
1402 |
|
{ |
1403 |
51 |
pepf = pe->getProof(); |
1404 |
|
} |
1405 |
1420 |
Assert(pepf != nullptr); |
1406 |
2840 |
std::shared_ptr<ProofNode> pfn = d_pfManager->getFinalProof(pepf, *d_asserts); |
1407 |
2840 |
std::vector<Node> core; |
1408 |
1420 |
d_ucManager->getUnsatCore(pfn, *d_asserts, core); |
1409 |
1420 |
if (options::minimalUnsatCores()) |
1410 |
|
{ |
1411 |
1 |
core = reduceUnsatCore(core); |
1412 |
|
} |
1413 |
2840 |
return UnsatCore(core); |
1414 |
|
} |
1415 |
|
|
1416 |
1 |
std::vector<Node> SmtEngine::reduceUnsatCore(const std::vector<Node>& core) |
1417 |
|
{ |
1418 |
1 |
Assert(options::unsatCores()) |
1419 |
|
<< "cannot reduce unsat core if unsat cores are turned off"; |
1420 |
|
|
1421 |
1 |
Notice() << "SmtEngine::reduceUnsatCore(): reducing unsat core" << endl; |
1422 |
2 |
std::unordered_set<Node> removed; |
1423 |
4 |
for (const Node& skip : core) |
1424 |
|
{ |
1425 |
6 |
std::unique_ptr<SmtEngine> coreChecker; |
1426 |
3 |
initializeSubsolver(coreChecker); |
1427 |
3 |
coreChecker->setLogic(getLogicInfo()); |
1428 |
3 |
coreChecker->getOptions().smt.checkUnsatCores = false; |
1429 |
|
// disable all proof options |
1430 |
3 |
coreChecker->getOptions().smt.produceProofs = false; |
1431 |
3 |
coreChecker->getOptions().smt.checkProofs = false; |
1432 |
3 |
coreChecker->getOptions().proof.proofEagerChecking = false; |
1433 |
|
|
1434 |
12 |
for (const Node& ucAssertion : core) |
1435 |
|
{ |
1436 |
9 |
if (ucAssertion != skip && removed.find(ucAssertion) == removed.end()) |
1437 |
|
{ |
1438 |
8 |
Node assertionAfterExpansion = expandDefinitions(ucAssertion); |
1439 |
4 |
coreChecker->assertFormula(assertionAfterExpansion); |
1440 |
|
} |
1441 |
|
} |
1442 |
6 |
Result r; |
1443 |
|
try |
1444 |
|
{ |
1445 |
3 |
r = coreChecker->checkSat(); |
1446 |
|
} |
1447 |
|
catch (...) |
1448 |
|
{ |
1449 |
|
throw; |
1450 |
|
} |
1451 |
|
|
1452 |
3 |
if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) |
1453 |
|
{ |
1454 |
1 |
removed.insert(skip); |
1455 |
|
} |
1456 |
2 |
else if (r.asSatisfiabilityResult().isUnknown()) |
1457 |
|
{ |
1458 |
|
Warning() << "SmtEngine::reduceUnsatCore(): could not reduce unsat core " |
1459 |
|
"due to " |
1460 |
|
"unknown result."; |
1461 |
|
} |
1462 |
|
} |
1463 |
|
|
1464 |
1 |
if (removed.empty()) |
1465 |
|
{ |
1466 |
|
return core; |
1467 |
|
} |
1468 |
|
else |
1469 |
|
{ |
1470 |
2 |
std::vector<Node> newUcAssertions; |
1471 |
4 |
for (const Node& n : core) |
1472 |
|
{ |
1473 |
3 |
if (removed.find(n) == removed.end()) |
1474 |
|
{ |
1475 |
2 |
newUcAssertions.push_back(n); |
1476 |
|
} |
1477 |
|
} |
1478 |
|
|
1479 |
1 |
return newUcAssertions; |
1480 |
|
} |
1481 |
|
} |
1482 |
|
|
1483 |
1364 |
void SmtEngine::checkUnsatCore() { |
1484 |
1364 |
Assert(d_env->getOptions().smt.unsatCores) |
1485 |
|
<< "cannot check unsat core if unsat cores are turned off"; |
1486 |
|
|
1487 |
1364 |
Notice() << "SmtEngine::checkUnsatCore(): generating unsat core" << endl; |
1488 |
2728 |
UnsatCore core = getUnsatCore(); |
1489 |
|
|
1490 |
|
// initialize the core checker |
1491 |
2728 |
std::unique_ptr<SmtEngine> coreChecker; |
1492 |
1364 |
initializeSubsolver(coreChecker); |
1493 |
1364 |
coreChecker->getOptions().smt.checkUnsatCores = false; |
1494 |
|
// disable all proof options |
1495 |
1364 |
coreChecker->getOptions().smt.produceProofs = false; |
1496 |
1364 |
coreChecker->getOptions().smt.checkProofs = false; |
1497 |
1364 |
coreChecker->getOptions().proof.proofEagerChecking = false; |
1498 |
|
|
1499 |
|
// set up separation logic heap if necessary |
1500 |
2728 |
TypeNode sepLocType, sepDataType; |
1501 |
1364 |
if (getSepHeapTypes(sepLocType, sepDataType)) |
1502 |
|
{ |
1503 |
21 |
coreChecker->declareSepHeap(sepLocType, sepDataType); |
1504 |
|
} |
1505 |
|
|
1506 |
1364 |
Notice() << "SmtEngine::checkUnsatCore(): pushing core assertions" |
1507 |
|
<< std::endl; |
1508 |
1364 |
theory::TrustSubstitutionMap& tls = d_env->getTopLevelSubstitutions(); |
1509 |
7316 |
for(UnsatCore::iterator i = core.begin(); i != core.end(); ++i) { |
1510 |
11904 |
Node assertionAfterExpansion = tls.apply(*i, false); |
1511 |
5952 |
Notice() << "SmtEngine::checkUnsatCore(): pushing core member " << *i |
1512 |
|
<< ", expanded to " << assertionAfterExpansion << "\n"; |
1513 |
5952 |
coreChecker->assertFormula(assertionAfterExpansion); |
1514 |
|
} |
1515 |
2728 |
Result r; |
1516 |
|
try { |
1517 |
1364 |
r = coreChecker->checkSat(); |
1518 |
|
} catch(...) { |
1519 |
|
throw; |
1520 |
|
} |
1521 |
1364 |
Notice() << "SmtEngine::checkUnsatCore(): result is " << r << endl; |
1522 |
1364 |
if(r.asSatisfiabilityResult().isUnknown()) { |
1523 |
1 |
Warning() |
1524 |
|
<< "SmtEngine::checkUnsatCore(): could not check core result unknown." |
1525 |
|
<< std::endl; |
1526 |
|
} |
1527 |
1363 |
else if (r.asSatisfiabilityResult().isSat()) |
1528 |
|
{ |
1529 |
|
InternalError() |
1530 |
|
<< "SmtEngine::checkUnsatCore(): produced core was satisfiable."; |
1531 |
|
} |
1532 |
1364 |
} |
1533 |
|
|
1534 |
2152 |
void SmtEngine::checkModel(bool hardFailure) { |
1535 |
2152 |
context::CDList<Node>* al = d_asserts->getAssertionList(); |
1536 |
|
// --check-model implies --produce-assertions, which enables the |
1537 |
|
// assertion list, so we should be ok. |
1538 |
2152 |
Assert(al != nullptr) |
1539 |
|
<< "don't have an assertion list to check in SmtEngine::checkModel()"; |
1540 |
|
|
1541 |
4304 |
TimerStat::CodeTimer checkModelTimer(d_stats->d_checkModelTime); |
1542 |
|
|
1543 |
2152 |
Notice() << "SmtEngine::checkModel(): generating model" << endl; |
1544 |
2152 |
Model* m = getAvailableModel("check model"); |
1545 |
2151 |
Assert(m != nullptr); |
1546 |
|
|
1547 |
|
// check the model with the theory engine for debugging |
1548 |
2151 |
if (options::debugCheckModels()) |
1549 |
|
{ |
1550 |
2137 |
TheoryEngine* te = getTheoryEngine(); |
1551 |
2137 |
Assert(te != nullptr); |
1552 |
2137 |
te->checkTheoryAssertionsWithModel(hardFailure); |
1553 |
|
} |
1554 |
|
|
1555 |
|
// check the model with the check models utility |
1556 |
2151 |
Assert(d_checkModels != nullptr); |
1557 |
2151 |
d_checkModels->checkModel(m, al, hardFailure); |
1558 |
2150 |
} |
1559 |
|
|
1560 |
1407 |
UnsatCore SmtEngine::getUnsatCore() { |
1561 |
1407 |
Trace("smt") << "SMT getUnsatCore()" << std::endl; |
1562 |
2814 |
SmtScope smts(this); |
1563 |
1407 |
finishInit(); |
1564 |
1407 |
if (Dump.isOn("benchmark")) |
1565 |
|
{ |
1566 |
|
getPrinter().toStreamCmdGetUnsatCore(getOutputManager().getDumpOut()); |
1567 |
|
} |
1568 |
2814 |
return getUnsatCoreInternal(); |
1569 |
|
} |
1570 |
|
|
1571 |
7 |
void SmtEngine::getRelevantInstantiationTermVectors( |
1572 |
|
std::map<Node, std::vector<std::vector<Node>>>& insts) |
1573 |
|
{ |
1574 |
7 |
Assert(d_state->getMode() == SmtMode::UNSAT); |
1575 |
|
// generate with new proofs |
1576 |
7 |
PropEngine* pe = getPropEngine(); |
1577 |
7 |
Assert(pe != nullptr); |
1578 |
7 |
Assert(pe->getProof() != nullptr); |
1579 |
|
std::shared_ptr<ProofNode> pfn = |
1580 |
14 |
d_pfManager->getFinalProof(pe->getProof(), *d_asserts); |
1581 |
7 |
d_ucManager->getRelevantInstantiations(pfn, insts); |
1582 |
7 |
} |
1583 |
|
|
1584 |
1 |
std::string SmtEngine::getProof() |
1585 |
|
{ |
1586 |
1 |
Trace("smt") << "SMT getProof()\n"; |
1587 |
2 |
SmtScope smts(this); |
1588 |
1 |
finishInit(); |
1589 |
1 |
if (Dump.isOn("benchmark")) |
1590 |
|
{ |
1591 |
|
getPrinter().toStreamCmdGetProof(getOutputManager().getDumpOut()); |
1592 |
|
} |
1593 |
1 |
if (!d_env->getOptions().smt.produceProofs) |
1594 |
|
{ |
1595 |
|
throw ModalException("Cannot get a proof when proof option is off."); |
1596 |
|
} |
1597 |
1 |
if (d_state->getMode() != SmtMode::UNSAT) |
1598 |
|
{ |
1599 |
|
throw RecoverableModalException( |
1600 |
|
"Cannot get a proof unless immediately preceded by " |
1601 |
|
"UNSAT/ENTAILED response."); |
1602 |
|
} |
1603 |
|
// the prop engine has the proof of false |
1604 |
1 |
PropEngine* pe = getPropEngine(); |
1605 |
1 |
Assert(pe != nullptr); |
1606 |
1 |
Assert(pe->getProof() != nullptr); |
1607 |
1 |
Assert(d_pfManager); |
1608 |
2 |
std::ostringstream ss; |
1609 |
1 |
d_pfManager->printProof(ss, pe->getProof(), *d_asserts); |
1610 |
2 |
return ss.str(); |
1611 |
|
} |
1612 |
|
|
1613 |
15 |
void SmtEngine::printInstantiations( std::ostream& out ) { |
1614 |
30 |
SmtScope smts(this); |
1615 |
15 |
finishInit(); |
1616 |
15 |
if (d_env->getOptions().printer.instFormatMode == options::InstFormatMode::SZS) |
1617 |
|
{ |
1618 |
|
out << "% SZS output start Proof for " << d_state->getFilename() |
1619 |
|
<< std::endl; |
1620 |
|
} |
1621 |
15 |
QuantifiersEngine* qe = getAvailableQuantifiersEngine("printInstantiations"); |
1622 |
|
|
1623 |
|
// First, extract and print the skolemizations |
1624 |
15 |
bool printed = false; |
1625 |
15 |
bool reqNames = !d_env->getOptions().printer.printInstFull; |
1626 |
|
// only print when in list mode |
1627 |
15 |
if (d_env->getOptions().printer.printInstMode == options::PrintInstMode::LIST) |
1628 |
|
{ |
1629 |
24 |
std::map<Node, std::vector<Node>> sks; |
1630 |
12 |
qe->getSkolemTermVectors(sks); |
1631 |
21 |
for (const std::pair<const Node, std::vector<Node>>& s : sks) |
1632 |
|
{ |
1633 |
18 |
Node name; |
1634 |
9 |
if (!qe->getNameForQuant(s.first, name, reqNames)) |
1635 |
|
{ |
1636 |
|
// did not have a name and we are only printing formulas with names |
1637 |
|
continue; |
1638 |
|
} |
1639 |
18 |
SkolemList slist(name, s.second); |
1640 |
9 |
out << slist; |
1641 |
9 |
printed = true; |
1642 |
|
} |
1643 |
|
} |
1644 |
|
|
1645 |
|
// Second, extract and print the instantiations |
1646 |
30 |
std::map<Node, std::vector<std::vector<Node>>> insts; |
1647 |
15 |
getInstantiationTermVectors(insts); |
1648 |
36 |
for (const std::pair<const Node, std::vector<std::vector<Node>>>& i : insts) |
1649 |
|
{ |
1650 |
21 |
if (i.second.empty()) |
1651 |
|
{ |
1652 |
|
// no instantiations, skip |
1653 |
|
continue; |
1654 |
|
} |
1655 |
42 |
Node name; |
1656 |
21 |
if (!qe->getNameForQuant(i.first, name, reqNames)) |
1657 |
|
{ |
1658 |
|
// did not have a name and we are only printing formulas with names |
1659 |
|
continue; |
1660 |
|
} |
1661 |
|
// must have a name |
1662 |
21 |
if (d_env->getOptions().printer.printInstMode == options::PrintInstMode::NUM) |
1663 |
|
{ |
1664 |
12 |
out << "(num-instantiations " << name << " " << i.second.size() << ")" |
1665 |
6 |
<< std::endl; |
1666 |
|
} |
1667 |
|
else |
1668 |
|
{ |
1669 |
15 |
Assert(d_env->getOptions().printer.printInstMode |
1670 |
|
== options::PrintInstMode::LIST); |
1671 |
30 |
InstantiationList ilist(name, i.second); |
1672 |
15 |
out << ilist; |
1673 |
|
} |
1674 |
21 |
printed = true; |
1675 |
|
} |
1676 |
|
// if we did not print anything, we indicate this |
1677 |
15 |
if (!printed) |
1678 |
|
{ |
1679 |
|
out << "No instantiations" << std::endl; |
1680 |
|
} |
1681 |
15 |
if (d_env->getOptions().printer.instFormatMode == options::InstFormatMode::SZS) |
1682 |
|
{ |
1683 |
|
out << "% SZS output end Proof for " << d_state->getFilename() << std::endl; |
1684 |
|
} |
1685 |
15 |
} |
1686 |
|
|
1687 |
15 |
void SmtEngine::getInstantiationTermVectors( |
1688 |
|
std::map<Node, std::vector<std::vector<Node>>>& insts) |
1689 |
|
{ |
1690 |
30 |
SmtScope smts(this); |
1691 |
15 |
finishInit(); |
1692 |
30 |
if (d_env->getOptions().smt.produceProofs |
1693 |
11 |
&& (!d_env->getOptions().smt.unsatCores |
1694 |
11 |
|| d_env->getOptions().smt.unsatCoresMode == options::UnsatCoresMode::FULL_PROOF) |
1695 |
22 |
&& getSmtMode() == SmtMode::UNSAT) |
1696 |
|
{ |
1697 |
|
// minimize instantiations based on proof manager |
1698 |
7 |
getRelevantInstantiationTermVectors(insts); |
1699 |
|
} |
1700 |
|
else |
1701 |
|
{ |
1702 |
|
QuantifiersEngine* qe = |
1703 |
8 |
getAvailableQuantifiersEngine("getInstantiationTermVectors"); |
1704 |
|
// otherwise, just get the list of all instantiations |
1705 |
8 |
qe->getInstantiationTermVectors(insts); |
1706 |
|
} |
1707 |
15 |
} |
1708 |
|
|
1709 |
86 |
bool SmtEngine::getSynthSolutions(std::map<Node, Node>& solMap) |
1710 |
|
{ |
1711 |
172 |
SmtScope smts(this); |
1712 |
86 |
finishInit(); |
1713 |
172 |
return d_sygusSolver->getSynthSolutions(solMap); |
1714 |
|
} |
1715 |
|
|
1716 |
30 |
Node SmtEngine::getQuantifierElimination(Node q, bool doFull, bool strict) |
1717 |
|
{ |
1718 |
60 |
SmtScope smts(this); |
1719 |
30 |
finishInit(); |
1720 |
30 |
const LogicInfo& logic = getLogicInfo(); |
1721 |
30 |
if (!logic.isPure(THEORY_ARITH) && strict) |
1722 |
|
{ |
1723 |
10 |
Warning() << "Unexpected logic for quantifier elimination " << logic |
1724 |
4 |
<< endl; |
1725 |
|
} |
1726 |
|
return d_quantElimSolver->getQuantifierElimination( |
1727 |
60 |
*d_asserts, q, doFull, d_isInternalSubsolver); |
1728 |
|
} |
1729 |
|
|
1730 |
10 |
bool SmtEngine::getInterpol(const Node& conj, |
1731 |
|
const TypeNode& grammarType, |
1732 |
|
Node& interpol) |
1733 |
|
{ |
1734 |
20 |
SmtScope smts(this); |
1735 |
10 |
finishInit(); |
1736 |
10 |
bool success = d_interpolSolver->getInterpol(conj, grammarType, interpol); |
1737 |
|
// notify the state of whether the get-interpol call was successfuly, which |
1738 |
|
// impacts the SMT mode. |
1739 |
10 |
d_state->notifyGetInterpol(success); |
1740 |
20 |
return success; |
1741 |
|
} |
1742 |
|
|
1743 |
9 |
bool SmtEngine::getInterpol(const Node& conj, Node& interpol) |
1744 |
|
{ |
1745 |
18 |
TypeNode grammarType; |
1746 |
18 |
return getInterpol(conj, grammarType, interpol); |
1747 |
|
} |
1748 |
|
|
1749 |
16 |
bool SmtEngine::getAbduct(const Node& conj, |
1750 |
|
const TypeNode& grammarType, |
1751 |
|
Node& abd) |
1752 |
|
{ |
1753 |
32 |
SmtScope smts(this); |
1754 |
16 |
finishInit(); |
1755 |
16 |
bool success = d_abductSolver->getAbduct(conj, grammarType, abd); |
1756 |
|
// notify the state of whether the get-abduct call was successfuly, which |
1757 |
|
// impacts the SMT mode. |
1758 |
14 |
d_state->notifyGetAbduct(success); |
1759 |
28 |
return success; |
1760 |
|
} |
1761 |
|
|
1762 |
10 |
bool SmtEngine::getAbduct(const Node& conj, Node& abd) |
1763 |
|
{ |
1764 |
20 |
TypeNode grammarType; |
1765 |
19 |
return getAbduct(conj, grammarType, abd); |
1766 |
|
} |
1767 |
|
|
1768 |
47 |
void SmtEngine::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs) |
1769 |
|
{ |
1770 |
94 |
SmtScope smts(this); |
1771 |
|
QuantifiersEngine* qe = |
1772 |
47 |
getAvailableQuantifiersEngine("getInstantiatedQuantifiedFormulas"); |
1773 |
47 |
qe->getInstantiatedQuantifiedFormulas(qs); |
1774 |
47 |
} |
1775 |
|
|
1776 |
42 |
void SmtEngine::getInstantiationTermVectors( |
1777 |
|
Node q, std::vector<std::vector<Node>>& tvecs) |
1778 |
|
{ |
1779 |
84 |
SmtScope smts(this); |
1780 |
|
QuantifiersEngine* qe = |
1781 |
42 |
getAvailableQuantifiersEngine("getInstantiationTermVectors"); |
1782 |
42 |
qe->getInstantiationTermVectors(q, tvecs); |
1783 |
42 |
} |
1784 |
|
|
1785 |
94 |
std::vector<Node> SmtEngine::getAssertions() |
1786 |
|
{ |
1787 |
188 |
SmtScope smts(this); |
1788 |
94 |
finishInit(); |
1789 |
94 |
d_state->doPendingPops(); |
1790 |
94 |
if (Dump.isOn("benchmark")) |
1791 |
|
{ |
1792 |
|
getPrinter().toStreamCmdGetAssertions(getOutputManager().getDumpOut()); |
1793 |
|
} |
1794 |
94 |
Trace("smt") << "SMT getAssertions()" << endl; |
1795 |
94 |
if (!d_env->getOptions().smt.produceAssertions) |
1796 |
|
{ |
1797 |
2 |
const char* msg = |
1798 |
|
"Cannot query the current assertion list when not in produce-assertions mode."; |
1799 |
2 |
throw ModalException(msg); |
1800 |
|
} |
1801 |
92 |
context::CDList<Node>* al = d_asserts->getAssertionList(); |
1802 |
92 |
Assert(al != nullptr); |
1803 |
92 |
std::vector<Node> res; |
1804 |
382 |
for (const Node& n : *al) |
1805 |
|
{ |
1806 |
290 |
res.emplace_back(n); |
1807 |
|
} |
1808 |
|
// copy the result out |
1809 |
184 |
return res; |
1810 |
|
} |
1811 |
|
|
1812 |
4036 |
void SmtEngine::push() |
1813 |
|
{ |
1814 |
8072 |
SmtScope smts(this); |
1815 |
4036 |
finishInit(); |
1816 |
4036 |
d_state->doPendingPops(); |
1817 |
4036 |
Trace("smt") << "SMT push()" << endl; |
1818 |
4036 |
d_smtSolver->processAssertions(*d_asserts); |
1819 |
4036 |
if(Dump.isOn("benchmark")) { |
1820 |
|
getPrinter().toStreamCmdPush(getOutputManager().getDumpOut()); |
1821 |
|
} |
1822 |
4036 |
d_state->userPush(); |
1823 |
4036 |
} |
1824 |
|
|
1825 |
3497 |
void SmtEngine::pop() { |
1826 |
6994 |
SmtScope smts(this); |
1827 |
3497 |
finishInit(); |
1828 |
3497 |
Trace("smt") << "SMT pop()" << endl; |
1829 |
3497 |
if (Dump.isOn("benchmark")) |
1830 |
|
{ |
1831 |
|
getPrinter().toStreamCmdPop(getOutputManager().getDumpOut()); |
1832 |
|
} |
1833 |
3497 |
d_state->userPop(); |
1834 |
|
|
1835 |
|
// Clear out assertion queues etc., in case anything is still in there |
1836 |
3497 |
d_asserts->clearCurrent(); |
1837 |
|
// clear the learned literals from the preprocessor |
1838 |
3497 |
d_pp->clearLearnedLiterals(); |
1839 |
|
|
1840 |
6994 |
Trace("userpushpop") << "SmtEngine: popped to level " |
1841 |
3497 |
<< getUserContext()->getLevel() << endl; |
1842 |
|
// should we reset d_status here? |
1843 |
|
// SMT-LIBv2 spec seems to imply no, but it would make sense to.. |
1844 |
3497 |
} |
1845 |
|
|
1846 |
71 |
void SmtEngine::resetAssertions() |
1847 |
|
{ |
1848 |
138 |
SmtScope smts(this); |
1849 |
|
|
1850 |
71 |
if (!d_state->isFullyInited()) |
1851 |
|
{ |
1852 |
|
// We're still in Start Mode, nothing asserted yet, do nothing. |
1853 |
|
// (see solver execution modes in the SMT-LIB standard) |
1854 |
4 |
Assert(getContext()->getLevel() == 0); |
1855 |
4 |
Assert(getUserContext()->getLevel() == 0); |
1856 |
4 |
getDumpManager()->resetAssertions(); |
1857 |
4 |
return; |
1858 |
|
} |
1859 |
|
|
1860 |
|
|
1861 |
67 |
Trace("smt") << "SMT resetAssertions()" << endl; |
1862 |
67 |
if (Dump.isOn("benchmark")) |
1863 |
|
{ |
1864 |
|
getPrinter().toStreamCmdResetAssertions(getOutputManager().getDumpOut()); |
1865 |
|
} |
1866 |
|
|
1867 |
67 |
d_asserts->clearCurrent(); |
1868 |
67 |
d_state->notifyResetAssertions(); |
1869 |
67 |
getDumpManager()->resetAssertions(); |
1870 |
|
// push the state to maintain global context around everything |
1871 |
67 |
d_state->setup(); |
1872 |
|
|
1873 |
|
// reset SmtSolver, which will construct a new prop engine |
1874 |
67 |
d_smtSolver->resetAssertions(); |
1875 |
|
} |
1876 |
|
|
1877 |
|
void SmtEngine::interrupt() |
1878 |
|
{ |
1879 |
|
if (!d_state->isFullyInited()) |
1880 |
|
{ |
1881 |
|
return; |
1882 |
|
} |
1883 |
|
d_smtSolver->interrupt(); |
1884 |
|
} |
1885 |
|
|
1886 |
|
void SmtEngine::setResourceLimit(uint64_t units, bool cumulative) |
1887 |
|
{ |
1888 |
|
if (cumulative) |
1889 |
|
{ |
1890 |
|
d_env->d_options.base.cumulativeResourceLimit = units; |
1891 |
|
} |
1892 |
|
else |
1893 |
|
{ |
1894 |
|
d_env->d_options.base.perCallResourceLimit = units; |
1895 |
|
} |
1896 |
|
} |
1897 |
|
void SmtEngine::setTimeLimit(uint64_t millis) |
1898 |
|
{ |
1899 |
|
d_env->d_options.base.perCallMillisecondLimit = millis; |
1900 |
|
} |
1901 |
|
|
1902 |
|
unsigned long SmtEngine::getResourceUsage() const |
1903 |
|
{ |
1904 |
|
return getResourceManager()->getResourceUsage(); |
1905 |
|
} |
1906 |
|
|
1907 |
|
unsigned long SmtEngine::getTimeUsage() const |
1908 |
|
{ |
1909 |
|
return getResourceManager()->getTimeUsage(); |
1910 |
|
} |
1911 |
|
|
1912 |
|
unsigned long SmtEngine::getResourceRemaining() const |
1913 |
|
{ |
1914 |
|
return getResourceManager()->getResourceRemaining(); |
1915 |
|
} |
1916 |
|
|
1917 |
801782 |
NodeManager* SmtEngine::getNodeManager() const |
1918 |
|
{ |
1919 |
801782 |
return d_env->getNodeManager(); |
1920 |
|
} |
1921 |
|
|
1922 |
|
void SmtEngine::printStatisticsSafe(int fd) const |
1923 |
|
{ |
1924 |
|
d_env->getStatisticsRegistry().printSafe(fd); |
1925 |
|
} |
1926 |
|
|
1927 |
|
void SmtEngine::printStatisticsDiff() const |
1928 |
|
{ |
1929 |
|
d_env->getStatisticsRegistry().printDiff(*d_env->getOptions().base.err); |
1930 |
|
d_env->getStatisticsRegistry().storeSnapshot(); |
1931 |
|
} |
1932 |
|
|
1933 |
208 |
void SmtEngine::setUserAttribute(const std::string& attr, |
1934 |
|
Node expr, |
1935 |
|
const std::vector<Node>& expr_values, |
1936 |
|
const std::string& str_value) |
1937 |
|
{ |
1938 |
416 |
SmtScope smts(this); |
1939 |
208 |
finishInit(); |
1940 |
208 |
TheoryEngine* te = getTheoryEngine(); |
1941 |
208 |
Assert(te != nullptr); |
1942 |
208 |
te->setUserAttribute(attr, expr, expr_values, str_value); |
1943 |
208 |
} |
1944 |
|
|
1945 |
9534 |
void SmtEngine::setOption(const std::string& key, const std::string& value) |
1946 |
|
{ |
1947 |
19064 |
NodeManagerScope nms(getNodeManager()); |
1948 |
9534 |
Trace("smt") << "SMT setOption(" << key << ", " << value << ")" << endl; |
1949 |
|
|
1950 |
9534 |
if (Dump.isOn("benchmark")) |
1951 |
|
{ |
1952 |
4 |
getPrinter().toStreamCmdSetOption( |
1953 |
2 |
getOutputManager().getDumpOut(), key, value); |
1954 |
|
} |
1955 |
|
|
1956 |
9534 |
if (key == "command-verbosity") |
1957 |
|
{ |
1958 |
4 |
size_t fstIndex = value.find(" "); |
1959 |
4 |
size_t sndIndex = value.find(" ", fstIndex + 1); |
1960 |
4 |
if (sndIndex == std::string::npos) |
1961 |
|
{ |
1962 |
8 |
string c = value.substr(1, fstIndex - 1); |
1963 |
|
int v = |
1964 |
4 |
std::stoi(value.substr(fstIndex + 1, value.length() - fstIndex - 1)); |
1965 |
4 |
if (v < 0 || v > 2) |
1966 |
|
{ |
1967 |
|
throw OptionException("command-verbosity must be 0, 1, or 2"); |
1968 |
|
} |
1969 |
4 |
d_commandVerbosity[c] = v; |
1970 |
4 |
return; |
1971 |
|
} |
1972 |
|
throw OptionException( |
1973 |
|
"command-verbosity value must be a tuple (command-name integer)"); |
1974 |
|
} |
1975 |
|
|
1976 |
9530 |
if (value.find(" ") != std::string::npos) |
1977 |
|
{ |
1978 |
|
throw OptionException("bad value for :" + key); |
1979 |
|
} |
1980 |
|
|
1981 |
19060 |
std::string optionarg = value; |
1982 |
9530 |
options::set(getOptions(), key, optionarg); |
1983 |
|
} |
1984 |
|
|
1985 |
2681 |
void SmtEngine::setIsInternalSubsolver() { d_isInternalSubsolver = true; } |
1986 |
|
|
1987 |
13735 |
bool SmtEngine::isInternalSubsolver() const { return d_isInternalSubsolver; } |
1988 |
|
|
1989 |
597216 |
std::string SmtEngine::getOption(const std::string& key) const |
1990 |
|
{ |
1991 |
1194432 |
NodeManagerScope nms(getNodeManager()); |
1992 |
597216 |
NodeManager* nm = d_env->getNodeManager(); |
1993 |
|
|
1994 |
597216 |
Trace("smt") << "SMT getOption(" << key << ")" << endl; |
1995 |
|
|
1996 |
597216 |
if (key.find("command-verbosity:") == 0) |
1997 |
|
{ |
1998 |
597154 |
auto it = d_commandVerbosity.find(key.substr(std::strlen("command-verbosity:"))); |
1999 |
597154 |
if (it != d_commandVerbosity.end()) |
2000 |
|
{ |
2001 |
|
return std::to_string(it->second); |
2002 |
|
} |
2003 |
597154 |
it = d_commandVerbosity.find("*"); |
2004 |
597154 |
if (it != d_commandVerbosity.end()) |
2005 |
|
{ |
2006 |
32 |
return std::to_string(it->second); |
2007 |
|
} |
2008 |
597122 |
return "2"; |
2009 |
|
} |
2010 |
|
|
2011 |
62 |
if (Dump.isOn("benchmark")) |
2012 |
|
{ |
2013 |
|
getPrinter().toStreamCmdGetOption(d_outMgr.getDumpOut(), key); |
2014 |
|
} |
2015 |
|
|
2016 |
62 |
if (key == "command-verbosity") |
2017 |
|
{ |
2018 |
6 |
vector<Node> result; |
2019 |
6 |
Node defaultVerbosity; |
2020 |
7 |
for (const auto& verb: d_commandVerbosity) |
2021 |
|
{ |
2022 |
|
// treat the command name as a variable name as opposed to a string |
2023 |
|
// constant to avoid printing double quotes around the name |
2024 |
8 |
Node name = nm->mkBoundVar(verb.first, nm->integerType()); |
2025 |
8 |
Node value = nm->mkConst(Rational(verb.second)); |
2026 |
4 |
if (verb.first == "*") |
2027 |
|
{ |
2028 |
|
// put the default at the end of the SExpr |
2029 |
2 |
defaultVerbosity = nm->mkNode(Kind::SEXPR, name, value); |
2030 |
|
} |
2031 |
|
else |
2032 |
|
{ |
2033 |
2 |
result.push_back(nm->mkNode(Kind::SEXPR, name, value)); |
2034 |
|
} |
2035 |
|
} |
2036 |
|
// ensure the default is always listed |
2037 |
3 |
if (defaultVerbosity.isNull()) |
2038 |
|
{ |
2039 |
3 |
defaultVerbosity = nm->mkNode(Kind::SEXPR, |
2040 |
2 |
nm->mkBoundVar("*", nm->integerType()), |
2041 |
2 |
nm->mkConst(Rational(2))); |
2042 |
|
} |
2043 |
3 |
result.push_back(defaultVerbosity); |
2044 |
3 |
return nm->mkNode(Kind::SEXPR, result).toString(); |
2045 |
|
} |
2046 |
|
|
2047 |
116 |
std::string atom = options::get(getOptions(), key); |
2048 |
|
|
2049 |
57 |
if (atom != "true" && atom != "false") |
2050 |
|
{ |
2051 |
|
try |
2052 |
|
{ |
2053 |
13 |
Integer z(atom); |
2054 |
|
} |
2055 |
4 |
catch (std::invalid_argument&) |
2056 |
|
{ |
2057 |
2 |
atom = "\"" + atom + "\""; |
2058 |
|
} |
2059 |
|
} |
2060 |
|
|
2061 |
57 |
return atom; |
2062 |
|
} |
2063 |
|
|
2064 |
3752172 |
Options& SmtEngine::getOptions() { return d_env->d_options; } |
2065 |
|
|
2066 |
59 |
const Options& SmtEngine::getOptions() const { return d_env->getOptions(); } |
2067 |
|
|
2068 |
7247982 |
ResourceManager* SmtEngine::getResourceManager() const |
2069 |
|
{ |
2070 |
7247982 |
return d_env->getResourceManager(); |
2071 |
|
} |
2072 |
|
|
2073 |
22685 |
DumpManager* SmtEngine::getDumpManager() { return d_env->getDumpManager(); } |
2074 |
|
|
2075 |
10 |
const Printer& SmtEngine::getPrinter() const { return d_env->getPrinter(); } |
2076 |
|
|
2077 |
19781 |
OutputManager& SmtEngine::getOutputManager() { return d_outMgr; } |
2078 |
|
|
2079 |
32202603 |
theory::Rewriter* SmtEngine::getRewriter() { return d_env->getRewriter(); } |
2080 |
|
|
2081 |
29286 |
} // namespace cvc5 |