Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * The main entry point into the cvc5 library's SMT interface.
11 : : */
12 : :
13 : : #include "smt/solver_engine.h"
14 : :
15 : : #include "base/check.h"
16 : : #include "base/exception.h"
17 : : #include "base/modal_exception.h"
18 : : #include "base/output.h"
19 : : #include "decision/decision_engine.h"
20 : : #include "expr/bound_var_manager.h"
21 : : #include "expr/node.h"
22 : : #include "expr/node_algorithm.h"
23 : : #include "expr/non_closed_node_converter.h"
24 : : #include "expr/plugin.h"
25 : : #include "expr/skolem_manager.h"
26 : : #include "expr/subtype_elim_node_converter.h"
27 : : #include "expr/sygus_term_enumerator.h"
28 : : #include "options/base_options.h"
29 : : #include "options/expr_options.h"
30 : : #include "options/language.h"
31 : : #include "options/main_options.h"
32 : : #include "options/option_exception.h"
33 : : #include "options/options_public.h"
34 : : #include "options/parser_options.h"
35 : : #include "options/printer_options.h"
36 : : #include "options/proof_options.h"
37 : : #include "options/quantifiers_options.h"
38 : : #include "options/smt_options.h"
39 : : #include "options/theory_options.h"
40 : : #include "preprocessing/passes/synth_rew_rules.h"
41 : : #include "printer/printer.h"
42 : : #include "proof/unsat_core.h"
43 : : #include "prop/prop_engine.h"
44 : : #include "smt/abduction_solver.h"
45 : : #include "smt/assertions.h"
46 : : #include "smt/check_models.h"
47 : : #include "smt/context_manager.h"
48 : : #include "smt/env.h"
49 : : #include "smt/expand_definitions.h"
50 : : #include "smt/find_synth_solver.h"
51 : : #include "smt/interpolation_solver.h"
52 : : #include "smt/listeners.h"
53 : : #include "smt/logic_exception.h"
54 : : #include "smt/model.h"
55 : : #include "smt/model_blocker.h"
56 : : #include "smt/model_core_builder.h"
57 : : #include "smt/preprocessor.h"
58 : : #include "smt/proof_manager.h"
59 : : #include "smt/quant_elim_solver.h"
60 : : #include "smt/set_defaults.h"
61 : : #include "smt/smt_driver.h"
62 : : #include "smt/smt_driver_deep_restarts.h"
63 : : #include "smt/smt_solver.h"
64 : : #include "smt/solver_engine_state.h"
65 : : #include "smt/solver_engine_stats.h"
66 : : #include "smt/sygus_solver.h"
67 : : #include "smt/timeout_core_manager.h"
68 : : #include "smt/unsat_core_manager.h"
69 : : #include "theory/datatypes/sygus_datatype_utils.h"
70 : : #include "theory/quantifiers/candidate_rewrite_database.h"
71 : : #include "theory/quantifiers/instantiation_list.h"
72 : : #include "theory/quantifiers/oracle_engine.h"
73 : : #include "theory/quantifiers/quantifiers_attributes.h"
74 : : #include "theory/quantifiers/query_generator.h"
75 : : #include "theory/quantifiers/rewrite_verifier.h"
76 : : #include "theory/quantifiers/sygus/sygus_enumerator.h"
77 : : #include "theory/quantifiers/sygus_sampler.h"
78 : : #include "theory/quantifiers_engine.h"
79 : : #include "theory/rewriter.h"
80 : : #include "theory/smt_engine_subsolver.h"
81 : : #include "theory/theory_engine.h"
82 : : #include "util/random.h"
83 : : #include "util/rational.h"
84 : : #include "util/resource_manager.h"
85 : : #include "util/sexpr.h"
86 : : #include "util/statistics_registry.h"
87 : : #include "util/string.h"
88 : :
89 : : // required for hacks related to old proofs for unsat cores
90 : : #include "base/configuration.h"
91 : : #include "base/configuration_private.h"
92 : :
93 : : using namespace std;
94 : : using namespace cvc5::internal::smt;
95 : : using namespace cvc5::internal::preprocessing;
96 : : using namespace cvc5::internal::prop;
97 : : using namespace cvc5::context;
98 : : using namespace cvc5::internal::theory;
99 : :
100 : : namespace cvc5::internal {
101 : :
102 : 75751 : SolverEngine::SolverEngine(NodeManager* nm, const Options* optr)
103 : 75751 : : d_env(new Env(nm, optr)),
104 : 75751 : d_state(new SolverEngineState(*d_env.get())),
105 : 75751 : d_ctxManager(nullptr),
106 : 75751 : d_routListener(new ResourceOutListener(*this)),
107 : 75751 : d_smtSolver(nullptr),
108 : 75751 : d_smtDriver(nullptr),
109 : 75751 : d_checkModels(nullptr),
110 : 75751 : d_pfManager(nullptr),
111 : 75751 : d_ucManager(nullptr),
112 : 75751 : d_sygusSolver(nullptr),
113 : 75751 : d_abductSolver(nullptr),
114 : 75751 : d_interpolSolver(nullptr),
115 : 75751 : d_quantElimSolver(nullptr),
116 : 75751 : d_userLogicSet(false),
117 : 75751 : d_safeOptsSetRegularOption(false),
118 : 75751 : d_safeOptsSetRegularOptionToDefault(false),
119 : 75751 : d_isInternalSubsolver(false),
120 : 227253 : d_stats(nullptr)
121 : : {
122 : : // listen to resource out
123 : 75751 : getResourceManager()->registerListener(d_routListener.get());
124 : : // make statistics
125 : 75751 : d_stats.reset(new SolverEngineStatistics(d_env->getStatisticsRegistry()));
126 : : // make the SMT solver
127 : 75751 : d_smtSolver.reset(new SmtSolver(*d_env, *d_stats));
128 : : // make the context manager
129 : 75751 : d_ctxManager.reset(new ContextManager(*d_env.get(), *d_state));
130 : : // make the SyGuS solver
131 : 75751 : d_sygusSolver.reset(new SygusSolver(*d_env.get(), *d_smtSolver));
132 : : // make the quantifier elimination solver
133 : 75751 : d_quantElimSolver.reset(
134 : 75751 : new QuantElimSolver(*d_env.get(), *d_smtSolver, d_ctxManager.get()));
135 : 75751 : }
136 : :
137 : 181345 : bool SolverEngine::isFullyInited() const { return d_state->isFullyInited(); }
138 : 34627 : bool SolverEngine::isQueryMade() const { return d_state->isQueryMade(); }
139 : 3657 : size_t SolverEngine::getNumUserLevels() const
140 : : {
141 : 3657 : return d_ctxManager->getNumUserLevels();
142 : : }
143 : 14342 : SmtMode SolverEngine::getSmtMode() const { return d_state->getMode(); }
144 : 4697 : bool SolverEngine::isSmtModeSat() const
145 : : {
146 : 4697 : SmtMode mode = getSmtMode();
147 [ + + ][ + + ]: 4697 : return mode == SmtMode::SAT || mode == SmtMode::SAT_UNKNOWN;
148 : : }
149 : 0 : Result SolverEngine::getStatusOfLastCommand() const
150 : : {
151 : 0 : return d_state->getStatus();
152 : : }
153 : :
154 : 278153 : void SolverEngine::finishInit()
155 : : {
156 [ + + ]: 278153 : if (d_state->isFullyInited())
157 : : {
158 : : // already initialized, return
159 : 227108 : return;
160 : : }
161 : :
162 : : // Notice that finishInit is called when options are finalized. If we are
163 : : // parsing smt2, this occurs at the moment we enter "Assert mode", page 52 of
164 : : // SMT-LIB 2.6 standard.
165 : :
166 : : // set the logic
167 : 51045 : const LogicInfo& logic = getLogicInfo();
168 [ + + ]: 51045 : if (!logic.isLocked())
169 : : {
170 : 16854 : setLogicInternal();
171 : : }
172 : :
173 : : // set the random seed
174 : 51045 : Random::getRandom().setSeed(d_env->getOptions().driver.seed);
175 : :
176 : : // Call finish init on the set defaults module. This inializes the logic
177 : : // and the best default options based on our heuristics.
178 : 51045 : SetDefaults sdefaults(*d_env, d_isInternalSubsolver);
179 : 51045 : sdefaults.setDefaults(d_env->d_logic, getOptions());
180 : :
181 [ + + ]: 51040 : if (d_env->getOptions().smt.produceProofs)
182 : : {
183 : : // make the proof manager
184 : 19794 : d_pfManager.reset(new PfManager(*d_env.get()));
185 : : // start the unsat core manager
186 : 19794 : d_ucManager.reset(new UnsatCoreManager(
187 : 19794 : *d_env.get(), *d_smtSolver.get(), *d_pfManager.get()));
188 : : }
189 : 51040 : if (d_env->isOutputOn(OutputTag::RARE_DB)
190 [ + - ][ - + ]: 51040 : || d_env->isOutputOn(OutputTag::RARE_DB_EXPERT))
[ - + ]
191 : : {
192 : 0 : if (!d_env->getOptions().smt.produceProofs
193 : 0 : || options().proof.proofGranularityMode
194 : : != options::ProofGranularityMode::DSL_REWRITE)
195 : : {
196 [ - - ]: 0 : Warning() << "WARNING: -o rare-db requires --produce-proofs and "
197 : 0 : "--proof-granularity=dsl-rewrite" << std::endl;
198 : : }
199 : : }
200 : : // enable proof support in the environment/rewriter
201 : 51040 : d_env->finishInit(d_pfManager.get());
202 : :
203 [ + - ]: 51040 : Trace("smt-debug") << "SolverEngine::finishInit" << std::endl;
204 : 51040 : d_smtSolver->finishInit();
205 : :
206 : : // make SMT solver driver based on options
207 [ + + ]: 51040 : if (options().smt.deepRestartMode != options::DeepRestartMode::NONE)
208 : : {
209 : 8 : d_smtDriver.reset(new SmtDriverDeepRestarts(
210 : 8 : *d_env.get(), *d_smtSolver.get(), d_ctxManager.get()));
211 : : }
212 : : else
213 : : {
214 : 51032 : ContextManager* ctx = d_ctxManager.get();
215 : : // deep restarts not enabled
216 : 51032 : d_smtDriver.reset(
217 : 51032 : new SmtDriverSingleCall(*d_env.get(), *d_smtSolver.get(), ctx));
218 : : }
219 : :
220 : : // global push/pop around everything, to ensure proper destruction
221 : : // of context-dependent data structures
222 : 51040 : d_ctxManager->setup(d_smtDriver.get());
223 : :
224 : : // subsolvers
225 [ + + ]: 51040 : if (d_env->getOptions().smt.produceAbducts)
226 : : {
227 : 6245 : d_abductSolver.reset(new AbductionSolver(*d_env.get()));
228 : : }
229 [ + + ]: 51040 : if (d_env->getOptions().smt.produceInterpolants)
230 : : {
231 : 1870 : d_interpolSolver.reset(new InterpolationSolver(*d_env));
232 : : }
233 : : // check models utility
234 [ + + ]: 51040 : if (d_env->getOptions().smt.checkModels)
235 : : {
236 : 2432 : d_checkModels.reset(new CheckModels(*d_env.get()));
237 : : }
238 : :
239 [ - + ][ - + ]: 51040 : AlwaysAssert(d_smtSolver->getPropEngine()->getAssertionLevel() == 0)
[ - - ]
240 : : << "The PropEngine has pushed but the SolverEngine "
241 : 0 : "hasn't finished initializing!";
242 : :
243 [ - + ][ - + ]: 51040 : Assert(getLogicInfo().isLocked());
[ - - ]
244 : :
245 : : // store that we are finished initializing
246 : 51040 : d_state->markFinishInit();
247 [ + - ]: 51040 : Trace("smt-debug") << "SolverEngine::finishInit done" << std::endl;
248 : 51045 : }
249 : :
250 : 70731 : void SolverEngine::shutdown()
251 : : {
252 : 70731 : d_ctxManager->shutdown();
253 : 70731 : d_env->shutdown();
254 : 70731 : }
255 : :
256 : 70731 : SolverEngine::~SolverEngine()
257 : : {
258 : :
259 : : try
260 : : {
261 : 70731 : shutdown();
262 : :
263 : : // global push/pop around everything, to ensure proper destruction
264 : : // of context-dependent data structures
265 : 70731 : d_ctxManager->cleanup();
266 : :
267 : : // destroy all passes before destroying things that they refer to
268 : 70731 : d_smtSolver->getPreprocessor()->cleanup();
269 : :
270 : 70731 : d_pfManager.reset(nullptr);
271 : 70731 : d_ucManager.reset(nullptr);
272 : :
273 : 70731 : d_abductSolver.reset(nullptr);
274 : 70731 : d_interpolSolver.reset(nullptr);
275 : 70731 : d_quantElimSolver.reset(nullptr);
276 : 70731 : d_sygusSolver.reset(nullptr);
277 : 70731 : d_smtDriver.reset(nullptr);
278 : 70731 : d_smtSolver.reset(nullptr);
279 : :
280 : 70731 : d_stats.reset(nullptr);
281 : 70731 : d_routListener.reset(nullptr);
282 : : // destroy the state
283 : 70731 : d_state.reset(nullptr);
284 : : // destroy the environment
285 : 70731 : d_env.reset(nullptr);
286 : : }
287 [ - - ]: 0 : catch (Exception& e)
288 : : {
289 : 0 : d_env->warning() << "cvc5 threw an exception during cleanup." << std::endl << e << std::endl;
290 : 0 : }
291 : 70731 : }
292 : :
293 : 43685 : void SolverEngine::setLogic(const LogicInfo& logic)
294 : : {
295 [ - + ]: 43685 : if (d_state->isFullyInited())
296 : : {
297 : 0 : throw ModalException(
298 : : "Cannot set logic in SolverEngine after the engine has "
299 : 0 : "finished initializing.");
300 : : }
301 : 43685 : d_env->d_logic = logic;
302 : 43685 : d_userLogic = logic;
303 : 43685 : d_userLogicSet = true;
304 : 43685 : setLogicInternal();
305 : 43685 : }
306 : :
307 : 0 : void SolverEngine::setLogic(const std::string& s)
308 : : {
309 : : try
310 : : {
311 : 0 : setLogic(LogicInfo(s));
312 : : }
313 [ - - ]: 0 : catch (IllegalArgumentException& e)
314 : : {
315 : 0 : throw LogicException(e.what());
316 : 0 : }
317 : 0 : }
318 : :
319 : 53948 : bool SolverEngine::isLogicSet() const { return d_userLogicSet; }
320 : :
321 : 105297 : const LogicInfo& SolverEngine::getLogicInfo() const
322 : : {
323 : 105297 : return d_env->getLogicInfo();
324 : : }
325 : :
326 : 7758 : LogicInfo SolverEngine::getUserLogicInfo() const
327 : : {
328 : : // Lock the logic to make sure that this logic can be queried. We create a
329 : : // copy of the user logic here to keep this method const.
330 : 7758 : LogicInfo res = d_userLogic;
331 : 7758 : res.lock();
332 : 7758 : return res;
333 : : }
334 : :
335 : 60539 : void SolverEngine::setLogicInternal()
336 : : {
337 [ - + ][ - + ]: 60539 : Assert(!d_state->isFullyInited())
[ - - ]
338 : : << "setting logic in SolverEngine but the engine has already"
339 : 0 : " finished initializing for this run";
340 : 60539 : d_env->d_logic.lock();
341 : 60539 : d_userLogic.lock();
342 : 60539 : }
343 : :
344 : 38834 : void SolverEngine::setInfo(const std::string& key, const std::string& value)
345 : : {
346 [ + - ]: 38834 : Trace("smt") << "SMT setInfo(" << key << ", " << value << ")" << endl;
347 : :
348 [ + + ]: 38834 : if (key == "filename")
349 : : {
350 : 24420 : d_env->d_options.write_driver().filename = value;
351 : 24420 : d_env->getStatisticsRegistry().registerValue<std::string>(
352 : : "driver::filename", value);
353 : : }
354 [ + + ]: 14414 : else if (key == "smt-lib-version")
355 : : {
356 [ + + ][ + + ]: 2580 : if (value != "2" && value != "2.6")
[ + + ]
357 : : {
358 : 308 : d_env->warning() << "SMT-LIB version " << value
359 : : << " unsupported, defaulting to language (and semantics of) "
360 : 308 : "SMT-LIB 2.6\n";
361 : : }
362 : 2580 : getOptions().write_base().inputLanguage = Language::LANG_SMTLIB_V2_6;
363 : : // also update the output language
364 [ + - ]: 2580 : if (!getOptions().printer.outputLanguageWasSetByUser)
365 : : {
366 : 2580 : setOption("output-language", "smtlib2.6");
367 : 2580 : getOptions().write_printer().outputLanguageWasSetByUser = false;
368 : : }
369 : : }
370 [ + + ]: 11834 : else if (key == "status")
371 : : {
372 : 8448 : d_state->notifyExpectedStatus(value);
373 : : }
374 : 38834 : }
375 : :
376 : 284 : bool SolverEngine::isValidGetInfoFlag(const std::string& key) const
377 : : {
378 [ + + ][ + - ]: 566 : if (key == "all-statistics" || key == "error-behavior" || key == "filename"
379 [ + + ][ + + ]: 280 : || key == "name" || key == "version" || key == "authors"
[ + + ]
380 [ + + ][ + - ]: 25 : || key == "status" || key == "time" || key == "reason-unknown"
[ + + ]
381 [ + + ][ + - ]: 566 : || key == "assertion-stack-levels" || key == "all-options")
[ - + ][ + + ]
382 : : {
383 : 276 : return true;
384 : : }
385 : 8 : return false;
386 : : }
387 : :
388 : 276 : std::string SolverEngine::getInfo(const std::string& key) const
389 : : {
390 [ + - ]: 276 : Trace("smt") << "SMT getInfo(" << key << ")" << endl;
391 [ + + ]: 276 : if (key == "all-statistics")
392 : : {
393 : 2 : return toSExpr(d_env->getStatisticsRegistry().begin(),
394 : 4 : d_env->getStatisticsRegistry().end());
395 : : }
396 [ + + ]: 274 : if (key == "error-behavior")
397 : : {
398 : 2 : return "immediate-exit";
399 : : }
400 [ - + ]: 272 : if (key == "filename")
401 : : {
402 : 0 : return d_env->getOptions().driver.filename;
403 : : }
404 [ + + ]: 272 : if (key == "name")
405 : : {
406 : 502 : return toSExpr(Configuration::getName());
407 : : }
408 [ + + ]: 21 : if (key == "version")
409 : : {
410 : 4 : return toSExpr(Configuration::getVersionString());
411 : : }
412 [ + + ]: 19 : if (key == "authors")
413 : : {
414 : 4 : return toSExpr("the " + Configuration::getName() + " authors");
415 : : }
416 [ + + ]: 17 : if (key == "status")
417 : : {
418 : : // sat | unsat | unknown
419 : 3 : Result status = d_state->getStatus();
420 [ - - ][ + ]: 3 : switch (status.getStatus())
421 : : {
422 : 0 : case Result::SAT: return "sat";
423 : 0 : case Result::UNSAT: return "unsat";
424 : 3 : default: return "unknown";
425 : : }
426 : 3 : }
427 [ - + ]: 14 : if (key == "time")
428 : : {
429 : 0 : return toSExpr(std::clock());
430 : : }
431 [ + - ]: 14 : if (key == "reason-unknown")
432 : : {
433 : 14 : Result status = d_state->getStatus();
434 [ + + ][ + - ]: 14 : if (!status.isNull() && status.isUnknown())
[ + + ]
435 : : {
436 : 10 : std::stringstream ss;
437 : 10 : ss << status.getUnknownExplanation();
438 : 10 : std::string s = ss.str();
439 : 10 : transform(s.begin(), s.end(), s.begin(), ::tolower);
440 : 10 : return s;
441 : 10 : }
442 : : else
443 : : {
444 : 4 : throw RecoverableModalException(
445 : : "Can't get-info :reason-unknown when the "
446 : 8 : "last result wasn't unknown!");
447 : : }
448 : 14 : }
449 [ - - ]: 0 : if (key == "assertion-stack-levels")
450 : : {
451 : 0 : size_t ulevel = d_ctxManager->getNumUserLevels();
452 : 0 : AlwaysAssert(ulevel <= std::numeric_limits<unsigned long int>::max());
453 : 0 : return toSExpr(ulevel);
454 : : }
455 : 0 : Assert(key == "all-options");
456 : : // get the options, like all-statistics
457 : 0 : std::vector<std::vector<std::string>> res;
458 [ - - ]: 0 : for (const auto& opt : options::getNames())
459 : : {
460 : 0 : res.emplace_back(
461 : 0 : std::vector<std::string>{opt, options::get(getOptions(), opt)});
462 : 0 : }
463 : 0 : return toSExpr(res);
464 : : }
465 : :
466 : 13715 : void SolverEngine::debugCheckFormals(const std::vector<Node>& formals,
467 : : Node func)
468 : : {
469 : 13715 : std::unordered_set<Node> vars;
470 [ + + ]: 35433 : for (const Node& v : formals)
471 : : {
472 [ - + ]: 21722 : if (v.getKind() != Kind::BOUND_VARIABLE)
473 : : {
474 : 0 : std::stringstream ss;
475 : : ss << "All formal arguments to defined functions must be "
476 : : "BOUND_VARIABLEs, but in the\n"
477 : 0 : << "definition of function " << func << ", formal\n"
478 : 0 : << " " << v << "\n"
479 : 0 : << "has kind " << v.getKind();
480 : 0 : throw TypeCheckingExceptionPrivate(func, ss.str());
481 : 0 : }
482 [ + + ]: 21722 : if (!vars.insert(v).second)
483 : : {
484 : 4 : std::stringstream ss;
485 : : ss << "All formal arguments to defined functions must be "
486 : : "unique, but a duplicate variable was used in the "
487 : 4 : << "definition of function " << func;
488 : 4 : throw TypeCheckingExceptionPrivate(func, ss.str());
489 : 4 : }
490 : : }
491 : 13715 : }
492 : :
493 : 13711 : void SolverEngine::debugCheckFunctionBody(Node formula,
494 : : const std::vector<Node>& formals,
495 : : Node func)
496 : : {
497 : 13711 : TypeNode formulaType = formula.getType(d_env->getOptions().expr.typeChecking);
498 : 13711 : TypeNode funcType = func.getType();
499 : : // We distinguish here between definitions of constants and functions,
500 : : // because the type checking for them is subtly different. Perhaps we
501 : : // should instead have SolverEngine::defineFunction() and
502 : : // SolverEngine::defineConstant() for better clarity, although then that
503 : : // doesn't match the SMT-LIBv2 standard...
504 [ + + ]: 13711 : if (formals.size() > 0)
505 : : {
506 : 9706 : TypeNode rangeType = funcType.getRangeType();
507 [ - + ]: 9706 : if (formulaType != rangeType)
508 : : {
509 : 0 : stringstream ss;
510 : : ss << "Type of defined function does not match its declaration\n"
511 : 0 : << "The function : " << func << "\n"
512 : 0 : << "Declared type : " << rangeType << "\n"
513 : 0 : << "The body : " << formula << "\n"
514 : 0 : << "Body type : " << formulaType;
515 : 0 : throw TypeCheckingExceptionPrivate(func, ss.str());
516 : 0 : }
517 : 9706 : }
518 : : else
519 : : {
520 [ - + ]: 4005 : if (formulaType != funcType)
521 : : {
522 : 0 : stringstream ss;
523 : : ss << "Declared type of defined constant does not match its definition\n"
524 : 0 : << "The constant : " << func << "\n"
525 : 0 : << "Declared type : " << funcType << "\n"
526 : 0 : << "The definition : " << formula << "\n"
527 : 0 : << "Definition type: " << formulaType;
528 : 0 : throw TypeCheckingExceptionPrivate(func, ss.str());
529 : 0 : }
530 : : }
531 : 13711 : }
532 : :
533 : 335440 : void SolverEngine::declareConst(CVC5_UNUSED const Node& c)
534 : : {
535 : 335440 : d_state->notifyDeclaration();
536 : 335440 : }
537 : :
538 : 13904 : void SolverEngine::declareSort(CVC5_UNUSED const TypeNode& tn)
539 : : {
540 : 13904 : d_state->notifyDeclaration();
541 : 13904 : }
542 : :
543 : 9085 : void SolverEngine::defineFunction(Node func,
544 : : const std::vector<Node>& formals,
545 : : Node formula,
546 : : bool global)
547 : : {
548 : 9085 : beginCall();
549 [ + - ]: 9085 : Trace("smt") << "SMT defineFunction(" << func << ")" << endl;
550 : 9088 : debugCheckFormals(formals, func);
551 : :
552 : : // type check body
553 : 9082 : debugCheckFunctionBody(formula, formals, func);
554 : :
555 : 9082 : Node def = formula;
556 [ + + ]: 9082 : if (!formals.empty())
557 : : {
558 : 5664 : NodeManager* nm = d_env->getNodeManager();
559 : 22656 : def = nm->mkNode(
560 : 16992 : Kind::LAMBDA, nm->mkNode(Kind::BOUND_VAR_LIST, formals), def);
561 : : }
562 : 9082 : Node feq = func.eqNode(def);
563 : 9082 : d_smtSolver->getAssertions().addDefineFunDefinition(feq, global);
564 : 9082 : }
565 : :
566 : 629 : void SolverEngine::defineFunction(Node func, Node lambda, bool global)
567 : : {
568 : 629 : beginCall();
569 : : // A define-fun is treated as a (higher-order) assertion. It is provided
570 : : // to the assertions object. It will be added as a top-level substitution
571 : : // within this class, possibly multiple times if global is true.
572 : 629 : Node feq = func.eqNode(lambda);
573 : 629 : d_smtSolver->getAssertions().addDefineFunDefinition(feq, global);
574 : 629 : }
575 : :
576 : 3671 : void SolverEngine::defineFunctionsRec(
577 : : const std::vector<Node>& funcs,
578 : : const std::vector<std::vector<Node>>& formals,
579 : : const std::vector<Node>& formulas,
580 : : bool global)
581 : : {
582 : 3671 : beginCall();
583 [ + - ]: 3671 : Trace("smt") << "SMT defineFunctionsRec(...)" << endl;
584 : :
585 [ - + ][ - - ]: 3671 : if (funcs.size() != formals.size() && funcs.size() != formulas.size())
[ - + ]
586 : : {
587 : 0 : stringstream ss;
588 : : ss << "Number of functions, formals, and function bodies passed to "
589 : : "defineFunctionsRec do not match:"
590 : : << "\n"
591 : 0 : << " #functions : " << funcs.size() << "\n"
592 : 0 : << " #arg lists : " << formals.size() << "\n"
593 : 0 : << " #function bodies : " << formulas.size() << "\n";
594 : 0 : throw ModalException(ss.str());
595 : 0 : }
596 [ + + ]: 8300 : for (unsigned i = 0, size = funcs.size(); i < size; i++)
597 : : {
598 : : // check formal argument list
599 : 4631 : debugCheckFormals(formals[i], funcs[i]);
600 : : // type check body
601 : 4629 : debugCheckFunctionBody(formulas[i], formals[i], funcs[i]);
602 : : }
603 : :
604 : 3670 : NodeManager* nm = d_env->getNodeManager();
605 [ + + ]: 8299 : for (unsigned i = 0, size = funcs.size(); i < size; i++)
606 : : {
607 : : // we assert a quantified formula
608 : 4629 : Node func_app;
609 : : // make the function application
610 [ + + ]: 4629 : if (formals[i].empty())
611 : : {
612 : : // it has no arguments
613 : 587 : func_app = funcs[i];
614 : : }
615 : : else
616 : : {
617 : 4042 : std::vector<Node> children;
618 : 4042 : children.push_back(funcs[i]);
619 : 4042 : children.insert(children.end(), formals[i].begin(), formals[i].end());
620 : 4042 : func_app = nm->mkNode(Kind::APPLY_UF, children);
621 : 4042 : }
622 : 9258 : Node lem = nm->mkNode(Kind::EQUAL, func_app, formulas[i]);
623 [ + + ]: 4629 : if (!formals[i].empty())
624 : : {
625 : : // set the attribute to denote this is a function definition
626 : 4042 : Node aexpr = nm->mkNode(Kind::INST_ATTRIBUTE, func_app);
627 : 4042 : aexpr = nm->mkNode(Kind::INST_PATTERN_LIST, aexpr);
628 : : FunDefAttribute fda;
629 : 4042 : func_app.setAttribute(fda, true);
630 : : // make the quantified formula
631 : 4042 : Node boundVars = nm->mkNode(Kind::BOUND_VAR_LIST, formals[i]);
632 : 4042 : lem = nm->mkNode(Kind::FORALL, boundVars, lem, aexpr);
633 : 4042 : }
634 : : // Assert the quantified formula. Notice we don't call assertFormula
635 : : // directly, since we should call a private member method since we have
636 : : // already ensuring this SolverEngine is initialized above.
637 : : // add define recursive definition to the assertions
638 : 4629 : d_smtSolver->getAssertions().addDefineFunDefinition(lem, global);
639 : 4629 : }
640 : 3670 : }
641 : :
642 : 1941 : void SolverEngine::defineFunctionRec(Node func,
643 : : const std::vector<Node>& formals,
644 : : Node formula,
645 : : bool global)
646 : : {
647 : 1941 : std::vector<Node> funcs;
648 : 1941 : funcs.push_back(func);
649 : 1941 : std::vector<std::vector<Node>> formals_multi;
650 : 1941 : formals_multi.push_back(formals);
651 : 1941 : std::vector<Node> formulas;
652 : 1941 : formulas.push_back(formula);
653 : 1941 : defineFunctionsRec(funcs, formals_multi, formulas, global);
654 : 1941 : }
655 : :
656 : 25459 : TheoryModel* SolverEngine::getAvailableModel(const char* c) const
657 : : {
658 [ - + ]: 25459 : if (!d_env->getOptions().theory.assignFunctionValues)
659 : : {
660 : 0 : std::stringstream ss;
661 : 0 : ss << "Cannot " << c << " when --assign-function-values is false.";
662 : 0 : throw RecoverableModalException(ss.str().c_str());
663 : 0 : }
664 : :
665 : 25459 : if (d_state->getMode() != SmtMode::SAT
666 [ + + ][ - + ]: 25459 : && d_state->getMode() != SmtMode::SAT_UNKNOWN)
[ - + ]
667 : : {
668 : 0 : std::stringstream ss;
669 : : ss << "Cannot " << c
670 : 0 : << " unless immediately preceded by SAT or UNKNOWN response.";
671 : 0 : throw RecoverableModalException(ss.str().c_str());
672 : 0 : }
673 : :
674 [ - + ]: 25459 : if (!d_env->getOptions().smt.produceModels)
675 : : {
676 : 0 : std::stringstream ss;
677 : 0 : ss << "Cannot " << c << " when produce-models options is off.";
678 : 0 : throw ModalException(ss.str().c_str());
679 : 0 : }
680 : :
681 : 25459 : TheoryEngine* te = d_smtSolver->getTheoryEngine();
682 [ - + ][ - + ]: 25459 : Assert(te != nullptr);
[ - - ]
683 : : // If the solver is in UNKNOWN mode, we use the latest available model (e.g.,
684 : : // one that was generated for a last call check). Note that the model is SAT
685 : : // context-independent internally, so this works even if the SAT solver has
686 : : // backtracked since the model was generated. We disable the resource manager
687 : : // while building or getting the model. In general, we should not be spending
688 : : // resources while building a model, but this ensures that we return a model
689 : : // if a problem was solved within the allocated resources.
690 : 25459 : getResourceManager()->setEnabled(false);
691 : 25459 : TheoryModel* m = d_state->getMode() == SmtMode::SAT_UNKNOWN
692 [ + + ]: 25459 : ? te->getModel()
693 : 24469 : : te->getBuiltModel();
694 : 25459 : getResourceManager()->setEnabled(true);
695 : :
696 [ - + ]: 25459 : if (m == nullptr)
697 : : {
698 : 0 : std::stringstream ss;
699 : : ss << "Cannot " << c
700 : : << " since model is not available. Perhaps the most recent call to "
701 : 0 : "check-sat was interrupted?";
702 : 0 : throw RecoverableModalException(ss.str().c_str());
703 : 0 : }
704 : : // compute the model core if necessary and not done so already
705 : 25459 : const Options& opts = d_env->getOptions();
706 : 50918 : if (opts.smt.modelCoresMode != options::ModelCoresMode::NONE
707 [ + + ][ + + ]: 25459 : && !m->isUsingModelCore())
[ + + ]
708 : : {
709 : : // If we enabled model cores, we compute a model core for m based on our
710 : : // (expanded) assertions using the model core builder utility. Notice that
711 : : // we get the assertions using the getAssertionsInternal, which does not
712 : : // impact whether we are in "sat" mode
713 : 202 : std::vector<Node> asserts = getAssertionsInternal();
714 : 202 : d_smtSolver->getPreprocessor()->applySubstitutions(asserts);
715 : 202 : ModelCoreBuilder mcb(*d_env.get());
716 : 202 : mcb.setModelCore(asserts, m, opts.smt.modelCoresMode);
717 : 202 : }
718 : :
719 : 25459 : return m;
720 : : }
721 : :
722 : 8569 : std::shared_ptr<ProofNode> SolverEngine::getAvailableSatProof()
723 : : {
724 [ - + ]: 8569 : if (d_state->getMode() != SmtMode::UNSAT)
725 : : {
726 : 0 : std::stringstream ss;
727 : 0 : ss << "Cannot get proof unless immediately preceded by UNSAT response.";
728 : 0 : throw RecoverableModalException(ss.str().c_str());
729 : 0 : }
730 : 8569 : std::shared_ptr<ProofNode> pePfn;
731 [ + + ]: 8569 : if (d_env->isSatProofProducing())
732 : : {
733 : : // get the proof from the prop engine
734 : 8560 : PropEngine* pe = d_smtSolver->getPropEngine();
735 [ - + ][ - + ]: 8560 : Assert(pe != nullptr);
[ - - ]
736 : 8560 : pePfn = pe->getProof();
737 [ - + ][ - + ]: 8560 : Assert(pePfn != nullptr);
[ - - ]
738 : : }
739 : : else
740 : : {
741 : : const context::CDList<Node>& assertions =
742 : 9 : d_smtSolver->getPreprocessedAssertions();
743 : : // if not SAT proof producing, we construct a trusted step here
744 : 9 : std::vector<std::shared_ptr<ProofNode>> ps;
745 : 9 : ProofNodeManager* pnm = d_pfManager->getProofNodeManager();
746 [ + + ]: 18 : for (const Node& a : assertions)
747 : : {
748 : : // skip true assertions
749 [ + - ][ + - ]: 9 : if (!a.isConst() || !a.getConst<bool>())
[ + - ]
750 : : {
751 : 9 : ps.push_back(pnm->mkAssume(a));
752 : : }
753 : : }
754 : : // since we do not have the theory lemmas, this is an SMT refutation trust
755 : : // step, not a SAT refutation.
756 : 9 : NodeManager* nm = d_env->getNodeManager();
757 : 9 : Node fn = nm->mkConst(false);
758 : 9 : pePfn = pnm->mkTrustedNode(TrustId::SMT_REFUTATION, ps, {}, fn);
759 : 9 : }
760 : 8569 : return pePfn;
761 : 0 : }
762 : :
763 : 1013 : QuantifiersEngine* SolverEngine::getAvailableQuantifiersEngine(
764 : : const char* c) const
765 : : {
766 : 1013 : QuantifiersEngine* qe = d_smtSolver->getQuantifiersEngine();
767 [ - + ]: 1013 : if (qe == nullptr)
768 : : {
769 : 0 : std::stringstream ss;
770 : 0 : ss << "Cannot " << c << " when quantifiers are not present.";
771 : 0 : throw ModalException(ss.str().c_str());
772 : 0 : }
773 : 1013 : return qe;
774 : : }
775 : :
776 : 43326 : Result SolverEngine::checkSat()
777 : : {
778 : 43326 : beginCall(true);
779 : 43373 : Result res = checkSatInternal({});
780 : 43279 : endCall();
781 : 43279 : return res;
782 : 0 : }
783 : :
784 : 287 : Result SolverEngine::checkSat(const Node& assumption)
785 : : {
786 : 287 : beginCall(true);
787 : 286 : std::vector<Node> assump;
788 [ + - ]: 286 : if (!assumption.isNull())
789 : : {
790 : 286 : assump.push_back(assumption);
791 : : }
792 : 286 : Result res = checkSatInternal(assump);
793 : 284 : endCall();
794 : 568 : return res;
795 : 286 : }
796 : :
797 : 5741 : Result SolverEngine::checkSat(const std::vector<Node>& assumptions)
798 : : {
799 : 5741 : beginCall(true);
800 : 5741 : Result res = checkSatInternal(assumptions);
801 : 5735 : endCall();
802 : 5735 : return res;
803 : 0 : }
804 : :
805 : 49353 : Result SolverEngine::checkSatInternal(const std::vector<Node>& assumptions)
806 : : {
807 : 49353 : ensureWellFormedTerms(assumptions, "checkSat");
808 : :
809 [ + - ]: 49353 : Trace("smt") << "SolverEngine::checkSat(" << assumptions << ")" << endl;
810 : : // update the state to indicate we are about to run a check-sat
811 : 49353 : d_state->notifyCheckSat();
812 : :
813 : : // Call the SMT solver driver to check for satisfiability. Note that in the
814 : : // case of options like e.g. deep restarts, this may invokve multiple calls
815 : : // to check satisfiability in the underlying SMT solver
816 : 49353 : Result r = d_smtDriver->checkSat(assumptions);
817 : :
818 [ + - ]: 98604 : Trace("smt") << "SolverEngine::checkSat(" << assumptions << ") => " << r
819 : 49302 : << endl;
820 : : // notify our state of the check-sat result
821 : 49302 : d_state->notifyCheckSatResult(r);
822 : :
823 : : // Check that SAT results generate a model correctly.
824 [ + + ]: 49298 : if (d_env->getOptions().smt.checkModels)
825 : : {
826 [ + + ]: 3768 : if (r.getStatus() == Result::SAT)
827 : : {
828 : 3096 : checkModel();
829 : : }
830 : : }
831 : : // Check that UNSAT results generate a proof correctly.
832 [ + + ]: 49298 : if (d_env->getOptions().smt.checkProofs)
833 : : {
834 [ + + ]: 3601 : if (r.getStatus() == Result::UNSAT)
835 : : {
836 : 2433 : checkProof();
837 : : }
838 : : }
839 : : // Check that UNSAT results generate an unsat core correctly.
840 [ + + ]: 49298 : if (d_env->getOptions().smt.checkUnsatCores)
841 : : {
842 [ + + ]: 3136 : if (r.getStatus() == Result::UNSAT)
843 : : {
844 : 2179 : TimerStat::CodeTimer checkUnsatCoreTimer(d_stats->d_checkUnsatCoreTime);
845 : 2179 : checkUnsatCore();
846 : 2179 : }
847 : : }
848 : :
849 [ - + ]: 49298 : if (d_env->getOptions().base.statisticsEveryQuery)
850 : : {
851 : 0 : printStatisticsDiff();
852 : : }
853 : :
854 : : // set the filename on the result
855 : 49298 : const std::string& filename = d_env->getOptions().driver.filename;
856 : 98596 : return Result(r, filename);
857 : 49302 : }
858 : :
859 : 668 : std::pair<Result, std::vector<Node>> SolverEngine::getTimeoutCore(
860 : : const std::vector<Node>& assumptions)
861 : : {
862 [ + - ]: 668 : Trace("smt") << "SolverEngine::getTimeoutCore()" << std::endl;
863 : 668 : beginCall(true);
864 : : // refresh the assertions, to ensure we have applied preprocessing to
865 : : // all current assertions
866 : 668 : d_smtDriver->refreshAssertions();
867 : 668 : TimeoutCoreManager tcm(*d_env.get());
868 : : // get the preprocessed assertions
869 : : const context::CDList<Node>& assertions =
870 : 668 : d_smtSolver->getPreprocessedAssertions();
871 : 668 : std::vector<Node> passerts(assertions.begin(), assertions.end());
872 : : const context::CDHashMap<size_t, Node>& ppsm =
873 : 668 : d_smtSolver->getPreprocessedSkolemMap();
874 : 668 : std::map<size_t, Node> ppSkolemMap;
875 [ - + ]: 668 : for (auto& pk : ppsm)
876 : : {
877 : 0 : ppSkolemMap[pk.first] = pk.second;
878 : : }
879 : : std::pair<Result, std::vector<Node>> ret =
880 : 668 : tcm.getTimeoutCore(passerts, ppSkolemMap, assumptions);
881 : : // convert the preprocessed assertions to input assertions
882 : 668 : std::vector<Node> core;
883 [ + + ]: 668 : if (assumptions.empty())
884 : : {
885 [ + + ]: 442 : if (!ret.second.empty())
886 : : {
887 : 440 : core = d_ucManager->convertPreprocessedToInput(ret.second, true);
888 : : }
889 : : }
890 : : else
891 : : {
892 : : // not necessary to convert, since we computed the assumptions already
893 : 226 : core = ret.second;
894 : : }
895 : 668 : endCall();
896 : 1336 : return std::pair<Result, std::vector<Node>>(ret.first, core);
897 : 668 : }
898 : :
899 : 250 : std::vector<Node> SolverEngine::getUnsatAssumptions(void)
900 : : {
901 [ + - ]: 250 : Trace("smt") << "SMT getUnsatAssumptions()" << endl;
902 [ - + ]: 250 : if (!d_env->getOptions().smt.unsatAssumptions)
903 : : {
904 : 0 : throw ModalException(
905 : : "Cannot get unsat assumptions when produce-unsat-assumptions option "
906 : 0 : "is off.");
907 : : }
908 [ - + ]: 250 : if (d_state->getMode() != SmtMode::UNSAT)
909 : : {
910 : 0 : throw RecoverableModalException(
911 : : "Cannot get unsat assumptions unless immediately preceded by "
912 : 0 : "UNSAT.");
913 : : }
914 : 250 : UnsatCore core = getUnsatCoreInternal();
915 : 250 : std::vector<Node> res;
916 : 250 : std::vector<Node>& assumps = d_smtSolver->getAssertions().getAssumptions();
917 [ + + ]: 511 : for (const Node& e : assumps)
918 : : {
919 [ + + ]: 261 : if (std::find(core.begin(), core.end(), e) != core.end())
920 : : {
921 : 250 : res.push_back(e);
922 : : }
923 : : }
924 : 500 : return res;
925 : 250 : }
926 : :
927 : 182519 : void SolverEngine::assertFormula(const Node& formula)
928 : : {
929 : 182519 : beginCall();
930 : 182517 : ensureWellFormedTerm(formula, "assertFormula");
931 : 182517 : assertFormulaInternal(formula);
932 : 182517 : }
933 : :
934 : 182848 : void SolverEngine::assertFormulaInternal(const Node& formula)
935 : : {
936 : : // as an optimization we do not check whether formula is well-formed here, and
937 : : // defer this check for certain cases within the assertions module.
938 [ + - ]: 182848 : Trace("smt") << "SolverEngine::assertFormula(" << formula << ")" << endl;
939 : 182848 : Node f = formula;
940 : : // If we are proof producing and don't permit subtypes, we rewrite now.
941 : : // Otherwise we will have an assumption with mixed arithmetic which is
942 : : // not permitted in proofs that cannot be eliminated, and will require a
943 : : // trust step.
944 : : // We don't care if we are an internal subsolver, as this rewriting only
945 : : // impacts having exportable, complete proofs, which is not an issue for
946 : : // internal subsolvers.
947 [ + + ][ + + ]: 182848 : if (d_env->isProofProducing() && !d_isInternalSubsolver)
[ + + ]
948 : : {
949 [ + - ]: 89672 : if (options().proof.proofElimSubtypes)
950 : : {
951 : 89672 : SubtypeElimNodeConverter senc(d_env->getNodeManager());
952 : 89672 : f = senc.convert(formula);
953 : : // note we could throw a warning here if formula and f are different,
954 : : // but currently don't.
955 : 89672 : }
956 : : }
957 : 182848 : d_smtSolver->getAssertions().assertFormula(f);
958 : 182848 : }
959 : :
960 : : /*
961 : : --------------------------------------------------------------------------
962 : : Handling SyGuS commands
963 : : --------------------------------------------------------------------------
964 : : */
965 : :
966 : 2761 : void SolverEngine::declareSygusVar(Node var)
967 : : {
968 : 2761 : beginCall();
969 : 2761 : d_sygusSolver->declareSygusVar(var);
970 : 2761 : }
971 : :
972 : 2635 : void SolverEngine::declareSynthFun(Node func,
973 : : TypeNode sygusType,
974 : : const std::vector<Node>& vars)
975 : : {
976 : 2635 : beginCall();
977 : 2637 : d_sygusSolver->declareSynthFun(func, sygusType, vars);
978 : 2633 : }
979 : 0 : void SolverEngine::declareSynthFun(Node func, const std::vector<Node>& vars)
980 : : {
981 : 0 : beginCall();
982 : : // use a null sygus type
983 : 0 : TypeNode sygusType;
984 : 0 : d_sygusSolver->declareSynthFun(func, sygusType, vars);
985 : 0 : }
986 : :
987 : 2331 : void SolverEngine::assertSygusConstraint(Node n, bool isAssume)
988 : : {
989 : 2331 : beginCall();
990 : 2331 : d_sygusSolver->assertSygusConstraint(n, isAssume);
991 : 2331 : }
992 : :
993 : 63 : std::vector<Node> SolverEngine::getSygusConstraints()
994 : : {
995 : 63 : beginCall();
996 : 63 : return d_sygusSolver->getSygusConstraints();
997 : : }
998 : :
999 : 57 : std::vector<Node> SolverEngine::getSygusAssumptions()
1000 : : {
1001 : 57 : beginCall();
1002 : 57 : return d_sygusSolver->getSygusAssumptions();
1003 : : }
1004 : :
1005 : 123 : void SolverEngine::assertSygusInvConstraint(Node inv,
1006 : : Node pre,
1007 : : Node trans,
1008 : : Node post)
1009 : : {
1010 : 123 : beginCall();
1011 : 123 : d_sygusSolver->assertSygusInvConstraint(inv, pre, trans, post);
1012 : 123 : }
1013 : :
1014 : 1191 : SynthResult SolverEngine::checkSynth(bool isNext)
1015 : : {
1016 : 1191 : beginCall();
1017 [ + + ][ + + ]: 1191 : if (isNext && d_state->getMode() != SmtMode::SYNTH)
[ + + ]
1018 : : {
1019 : 2 : throw RecoverableModalException(
1020 : : "Cannot check-synth-next unless immediately preceded by a successful "
1021 : 4 : "call to check-synth(-next).");
1022 : : }
1023 : 1189 : SynthResult r = d_sygusSolver->checkSynth(isNext);
1024 : 1185 : d_state->notifyCheckSynthResult(r);
1025 : 1185 : return r;
1026 : : }
1027 : :
1028 : 77 : Node SolverEngine::findSynth(modes::FindSynthTarget fst, const TypeNode& gtn)
1029 : : {
1030 [ + - ]: 77 : Trace("smt") << "SolverEngine::findSynth " << fst << std::endl;
1031 : 77 : beginCall(true);
1032 : : // The grammar(s) we will use. This may be more than one if doing rewrite
1033 : : // rule synthesis from input or if no grammar is specified, indicating we
1034 : : // wish to use grammars for each function-to-synthesize.
1035 : 77 : std::vector<TypeNode> gtnu;
1036 [ + + ]: 77 : if (!gtn.isNull())
1037 : : {
1038 : : // Must generalize the free symbols in the grammar to variables. Otherwise,
1039 : : // certain algorithms (e.g. sampling) will fail to treat the free symbols
1040 : : // of the grammar as inputs to the term to find.
1041 : 16 : TypeNode ggtn = theory::datatypes::utils::generalizeSygusType(gtn);
1042 : 16 : gtnu.push_back(ggtn);
1043 : 16 : }
1044 : : // if synthesizing rewrite rules from input, we infer the grammar here
1045 [ + + ]: 77 : if (fst == modes::FindSynthTarget::REWRITE_INPUT)
1046 : : {
1047 [ - + ]: 11 : if (!gtn.isNull())
1048 : : {
1049 [ - - ]: 0 : Warning() << "Ignoring grammar provided to find-synth :rewrite_input"
1050 : 0 : << std::endl;
1051 : : }
1052 : 11 : uint64_t nvars = options().quantifiers.sygusRewSynthInputNVars;
1053 : 11 : std::vector<Node> asserts = getAssertionsInternal();
1054 : 22 : gtnu = preprocessing::passes::SynthRewRulesPass::getGrammarsFrom(
1055 : 22 : *d_env.get(), asserts, nvars);
1056 [ + + ]: 11 : if (gtnu.empty())
1057 : : {
1058 [ + - ]: 1 : Warning() << "Could not find grammar in find-synth :rewrite_input"
1059 : 1 : << std::endl;
1060 : 1 : return Node::null();
1061 : : }
1062 [ + + ]: 11 : }
1063 [ + - ][ + + ]: 76 : if (d_sygusSolver != nullptr && gtnu.empty())
[ + + ]
1064 : : {
1065 : : // if no type provided, and the sygus solver exists,
1066 : : std::vector<std::pair<Node, TypeNode>> funs =
1067 : 50 : d_sygusSolver->getSynthFunctions();
1068 [ + + ]: 100 : for (const std::pair<Node, TypeNode>& f : funs)
1069 : : {
1070 [ + - ]: 50 : if (!f.second.isNull())
1071 : : {
1072 : 50 : gtnu.push_back(f.second);
1073 : : }
1074 : : }
1075 : 50 : }
1076 [ - + ]: 76 : if (gtnu.empty())
1077 : : {
1078 : 0 : throw RecoverableModalException(
1079 : : "No grammar available in call to find-synth. Either provide one or "
1080 : 0 : "ensure synth-fun has been called.");
1081 : : }
1082 : : // initialize find synthesis solver if not done so already
1083 [ + + ]: 76 : if (d_findSynthSolver == nullptr)
1084 : : {
1085 : 64 : d_findSynthSolver.reset(new FindSynthSolver(*d_env.get()));
1086 : : }
1087 : 76 : Node ret = d_findSynthSolver->findSynth(fst, gtnu);
1088 : 69 : d_state->notifyFindSynth(!ret.isNull());
1089 : 69 : endCall();
1090 : 69 : return ret;
1091 : 77 : }
1092 : :
1093 : 16 : Node SolverEngine::findSynthNext()
1094 : : {
1095 : 16 : beginCall();
1096 [ - + ]: 16 : if (d_state->getMode() != SmtMode::FIND_SYNTH)
1097 : : {
1098 : 0 : throw RecoverableModalException(
1099 : : "Cannot find-synth-next unless immediately preceded by a successful "
1100 : 0 : "call to find-synth(-next).");
1101 : : }
1102 : 16 : Node ret = d_findSynthSolver->findSynthNext();
1103 : 16 : d_state->notifyFindSynth(!ret.isNull());
1104 : 16 : return ret;
1105 : 0 : }
1106 : :
1107 : : /*
1108 : : --------------------------------------------------------------------------
1109 : : End of Handling SyGuS commands
1110 : : --------------------------------------------------------------------------
1111 : : */
1112 : :
1113 : 263 : void SolverEngine::declarePool(const Node& p,
1114 : : const std::vector<Node>& initValue)
1115 : : {
1116 : 263 : Assert(p.isVar() && p.getType().isSet());
1117 : 263 : beginCall();
1118 : 263 : QuantifiersEngine* qe = getAvailableQuantifiersEngine("declareTermPool");
1119 : 263 : qe->declarePool(p, initValue);
1120 : 263 : }
1121 : :
1122 : 535 : void SolverEngine::declareOracleFun(
1123 : : Node var, std::function<std::vector<Node>(const std::vector<Node>&)> fn)
1124 : : {
1125 : 535 : beginCall();
1126 : 535 : QuantifiersEngine* qe = getAvailableQuantifiersEngine("declareOracleFun");
1127 : 535 : qe->declareOracleFun(var);
1128 : 535 : NodeManager* nm = d_env->getNodeManager();
1129 : 535 : std::vector<Node> inputs;
1130 : 535 : std::vector<Node> outputs;
1131 : 535 : TypeNode tn = var.getType();
1132 : 535 : Node app;
1133 [ + - ]: 535 : if (tn.isFunction())
1134 : : {
1135 : 535 : const std::vector<TypeNode>& argTypes = tn.getArgTypes();
1136 [ + + ]: 1280 : for (const TypeNode& t : argTypes)
1137 : : {
1138 : 745 : inputs.push_back(NodeManager::mkBoundVar(t));
1139 : : }
1140 : 535 : outputs.push_back(NodeManager::mkBoundVar(tn.getRangeType()));
1141 : 535 : std::vector<Node> appc;
1142 : 535 : appc.push_back(var);
1143 : 535 : appc.insert(appc.end(), inputs.begin(), inputs.end());
1144 : 535 : app = nm->mkNode(Kind::APPLY_UF, appc);
1145 : 535 : }
1146 : : else
1147 : : {
1148 : 0 : outputs.push_back(NodeManager::mkBoundVar(tn.getRangeType()));
1149 : 0 : app = var;
1150 : : }
1151 : : // makes equality assumption
1152 : 1070 : Node assume = nm->mkNode(Kind::EQUAL, app, outputs[0]);
1153 : : // no constraints
1154 : 535 : Node constraint = nm->mkConst(true);
1155 : : // make the oracle constant which carries the method implementation
1156 : 535 : Oracle oracle(fn);
1157 : 535 : Node o = nm->mkOracle(oracle);
1158 : : // set the attribute, which ensures we remember the method implementation for
1159 : : // the oracle function
1160 : 535 : var.setAttribute(theory::OracleInterfaceAttribute(), o);
1161 : : // define the oracle interface
1162 : : Node q = quantifiers::OracleEngine::mkOracleInterface(
1163 : 1070 : inputs, outputs, assume, constraint, o);
1164 : : // assert it
1165 : 535 : assertFormula(q);
1166 : 535 : }
1167 : :
1168 : 28 : void SolverEngine::addPlugin(Plugin* p)
1169 : : {
1170 [ - + ]: 28 : if (d_state->isFullyInited())
1171 : : {
1172 : 0 : throw ModalException(
1173 : 0 : "Cannot add plugin after the solver has been fully initialized.");
1174 : : }
1175 : : // we do not initialize the solver here.
1176 : 28 : d_env->addPlugin(p);
1177 : 28 : }
1178 : :
1179 : 8812 : Node SolverEngine::simplify(const Node& t, bool applySubs)
1180 : : {
1181 : 8812 : beginCall(true);
1182 : 8812 : Node tt = t;
1183 : : // if we are applying substitutions
1184 [ + + ]: 8812 : if (applySubs)
1185 : : {
1186 : : // ensure we've processed assertions
1187 : 325 : d_smtDriver->refreshAssertions();
1188 : : // apply substitutions
1189 : 323 : tt = d_smtSolver->getPreprocessor()->applySubstitutions(tt);
1190 : : }
1191 : : // now rewrite
1192 : 8810 : Node ret = d_env->getRewriter()->rewrite(tt);
1193 : : // make so that the returned term does not involve arithmetic subtyping
1194 : 8810 : SubtypeElimNodeConverter senc(d_env->getNodeManager());
1195 : 8810 : ret = senc.convert(ret);
1196 : 8810 : endCall();
1197 : 17620 : return ret;
1198 : 8812 : }
1199 : :
1200 : 20244 : Node SolverEngine::getValue(const Node& t, bool fromUser)
1201 : : {
1202 : 20244 : ensureWellFormedTerm(t, "get value");
1203 [ + - ]: 20244 : Trace("smt") << "SMT getValue(" << t << ")" << endl;
1204 : 20244 : TypeNode expectedType = t.getType();
1205 : :
1206 : : // We must expand definitions here, which replaces certain subterms of t
1207 : : // by the form that is used internally. This is necessary for some corner
1208 : : // cases of get-value to be accurate, e.g., when getting the value of
1209 : : // a division-by-zero term, we require getting the appropriate skolem
1210 : : // function corresponding to division-by-zero which may have been used during
1211 : : // the previous satisfiability check.
1212 : 20244 : std::unordered_map<Node, Node> cache;
1213 : 20244 : ExpandDefs expDef(*d_env.get());
1214 : : // Must apply substitutions first to ensure we expand definitions in the
1215 : : // solved form of t as well.
1216 : 20244 : Node n = d_smtSolver->getPreprocessor()->applySubstitutions(t);
1217 : 20244 : n = expDef.expandDefinitions(n, cache);
1218 : :
1219 [ + - ]: 20244 : Trace("smt") << "--- getting value of " << n << endl;
1220 : : // There are two ways model values for terms are computed (for historical
1221 : : // reasons). One way is that used in check-model; the other is that
1222 : : // used by the Model classes. It's not clear to me exactly how these
1223 : : // two are different, but they need to be unified. This ugly hack here
1224 : : // is to fix bug 554 until we can revamp boolean-terms and models [MGD]
1225 : :
1226 : : // AJR : necessary?
1227 [ + + ]: 20244 : if (!n.getType().isFunction())
1228 : : {
1229 : 19942 : n = d_env->getRewriter()->rewrite(n);
1230 : : }
1231 : :
1232 [ + - ]: 20244 : Trace("smt") << "--- getting value of " << n << endl;
1233 : 20244 : TheoryModel* m = getAvailableModel("get-value");
1234 [ - + ][ - + ]: 20244 : Assert(m != nullptr);
[ - - ]
1235 : 20244 : Node resultNode = m->getValue(n);
1236 [ + - ]: 20244 : Trace("smt") << "--- got value " << n << " = " << resultNode << endl;
1237 [ + - ][ - + ]: 20244 : Trace("smt") << "--- type " << resultNode.getType() << endl;
[ - - ]
1238 [ + - ]: 20244 : Trace("smt") << "--- expected type " << expectedType << endl;
1239 : :
1240 : : // type-check the result we got
1241 : 20244 : Assert(resultNode.isNull() || resultNode.getType() == expectedType)
1242 : 0 : << "Run with -t smt for details.";
1243 : :
1244 : : // Ensure it's a value (constant or const-ish like real algebraic
1245 : : // numbers), or a lambda (for uninterpreted functions). This assertion only
1246 : : // holds for models that do not have approximate values.
1247 [ + + ]: 20244 : if (!m->isValue(resultNode))
1248 : : {
1249 : 4 : bool subSuccess = false;
1250 [ + - ][ + - ]: 4 : if (fromUser && d_env->getOptions().smt.checkModelSubsolver)
[ + - ]
1251 : : {
1252 : : // invoke satisfiability check
1253 : : // ensure symbols have been substituted
1254 : 4 : resultNode = m->simplify(resultNode);
1255 : : // Note that we must be a "closed" term, i.e. one that can be
1256 : : // given in an assertion.
1257 [ + - ]: 4 : if (NonClosedNodeConverter::isClosed(*d_env.get(), resultNode))
1258 : : {
1259 : : // set up a resource limit
1260 : 4 : ResourceManager* rm = getResourceManager();
1261 : 4 : rm->beginCall();
1262 : 4 : TypeNode rtn = resultNode.getType();
1263 : 4 : SkolemManager* skm = d_env->getNodeManager()->getSkolemManager();
1264 : 4 : Node k = skm->mkInternalSkolemFunction(
1265 : 8 : InternalSkolemId::GET_VALUE_PURIFY, rtn, {resultNode});
1266 : : // the query is (k = resultNode)
1267 : 4 : Node checkQuery = resultNode.eqNode(k);
1268 : 4 : Options subOptions;
1269 : 4 : subOptions.copyValues(d_env->getOptions());
1270 : 4 : smt::SetDefaults::disableChecking(subOptions);
1271 : : // ensure no infinite loop
1272 : 4 : subOptions.write_smt().checkModelSubsolver = false;
1273 : 4 : subOptions.write_smt().modelVarElimUneval = false;
1274 : 4 : subOptions.write_smt().simplificationMode =
1275 : : options::SimplificationMode::NONE;
1276 : : // initialize the subsolver
1277 : 4 : SubsolverSetupInfo ssi(*d_env.get(), subOptions);
1278 : 4 : std::unique_ptr<SolverEngine> getValueChecker;
1279 : 4 : initializeSubsolver(d_env->getNodeManager(), getValueChecker, ssi);
1280 : : // disable all checking options
1281 : 4 : SetDefaults::disableChecking(getValueChecker->getOptions());
1282 : 4 : getValueChecker->assertFormula(checkQuery);
1283 : 4 : Result r = getValueChecker->checkSat();
1284 [ + - ]: 4 : if (r == Result::SAT)
1285 : : {
1286 : : // value is the result of getting the value of k
1287 : 4 : resultNode = getValueChecker->getValue(k);
1288 : 4 : subSuccess = m->isValue(resultNode);
1289 : : }
1290 : : // end resource limit
1291 : 4 : rm->refresh();
1292 : 4 : }
1293 : : }
1294 [ - + ]: 4 : if (!subSuccess)
1295 : : {
1296 : 0 : d_env->warning() << "Could not evaluate " << resultNode << " in getValue."
1297 : 0 : << std::endl;
1298 : : }
1299 : : }
1300 : :
1301 [ + + ]: 20244 : if (d_env->getOptions().smt.abstractValues)
1302 : : {
1303 : 8 : TypeNode rtn = resultNode.getType();
1304 [ + - ]: 8 : if (rtn.isArray())
1305 : : {
1306 : : // construct the skolem function
1307 : 8 : SkolemManager* skm = d_env->getNodeManager()->getSkolemManager();
1308 : 8 : Node a = skm->mkInternalSkolemFunction(
1309 : 16 : InternalSkolemId::ABSTRACT_VALUE, rtn, {resultNode});
1310 : : // add to top-level substitutions if applicable
1311 : 8 : theory::TrustSubstitutionMap& tsm = d_env->getTopLevelSubstitutions();
1312 [ + + ]: 8 : if (!tsm.get().hasSubstitution(resultNode))
1313 : : {
1314 : 6 : tsm.addSubstitution(resultNode, a);
1315 : : }
1316 : 8 : resultNode = a;
1317 [ + - ]: 8 : Trace("smt") << "--- abstract value >> " << resultNode << endl;
1318 : 8 : }
1319 : 8 : }
1320 : 40488 : return resultNode;
1321 : 20244 : }
1322 : :
1323 : 0 : std::vector<Node> SolverEngine::getValues(const std::vector<Node>& exprs,
1324 : : bool fromUser)
1325 : : {
1326 : 0 : std::vector<Node> result;
1327 [ - - ]: 0 : for (const Node& e : exprs)
1328 : : {
1329 : 0 : result.push_back(getValue(e, fromUser));
1330 : : }
1331 : 0 : return result;
1332 : 0 : }
1333 : :
1334 : 619 : std::vector<Node> SolverEngine::getModelDomainElements(TypeNode tn) const
1335 : : {
1336 [ - + ][ - + ]: 619 : Assert(tn.isUninterpretedSort());
[ - - ]
1337 : 619 : TheoryModel* m = getAvailableModel("getModelDomainElements");
1338 : 619 : return m->getDomainElements(tn);
1339 : : }
1340 : :
1341 : 585 : bool SolverEngine::isModelCoreSymbol(Node n)
1342 : : {
1343 [ - + ][ - + ]: 585 : Assert(n.isVar());
[ - - ]
1344 : 585 : const Options& opts = d_env->getOptions();
1345 [ - + ]: 585 : if (opts.smt.modelCoresMode == options::ModelCoresMode::NONE)
1346 : : {
1347 : : // if the model core mode is none, we are always a model core symbol
1348 : 0 : return true;
1349 : : }
1350 : 585 : TheoryModel* tm = getAvailableModel("isModelCoreSymbol");
1351 : 585 : return tm->isModelCoreSymbol(n);
1352 : : }
1353 : :
1354 : 239 : std::string SolverEngine::getModel(const std::vector<TypeNode>& declaredSorts,
1355 : : const std::vector<Node>& declaredFuns)
1356 : : {
1357 : : // !!! Note that all methods called here should have a version at the API
1358 : : // level. This is to ensure that the information associated with a model is
1359 : : // completely accessible by the user. This is currently not rigorously
1360 : : // enforced. An alternative design would be to have this method implemented
1361 : : // at the API level, but this makes exceptions in the text interface less
1362 : : // intuitive.
1363 : 239 : TheoryModel* tm = getAvailableModel("get model");
1364 : : // use the smt::Model model utility for printing
1365 : 239 : const Options& opts = d_env->getOptions();
1366 : 239 : bool isKnownSat = (d_state->getMode() == SmtMode::SAT);
1367 : 239 : Model m(isKnownSat, opts.driver.filename);
1368 : : // set the model declarations, which determines what is printed in the model
1369 [ + + ]: 439 : for (const TypeNode& tn : declaredSorts)
1370 : : {
1371 : 200 : m.addDeclarationSort(tn, getModelDomainElements(tn));
1372 : : }
1373 : 239 : bool usingModelCores =
1374 : 239 : (opts.smt.modelCoresMode != options::ModelCoresMode::NONE);
1375 [ + + ]: 698 : for (const Node& n : declaredFuns)
1376 : : {
1377 [ + + ][ + + ]: 459 : if (usingModelCores && !tm->isModelCoreSymbol(n))
[ + + ][ + + ]
[ - - ]
1378 : : {
1379 : : // skip if not in model core
1380 : 14 : continue;
1381 : : }
1382 : 445 : Node value = tm->getValue(n);
1383 : 445 : m.addDeclarationTerm(n, value);
1384 : 445 : }
1385 : : // for separation logic
1386 : 239 : TypeNode locT, dataT;
1387 [ + + ]: 239 : if (getSepHeapTypes(locT, dataT))
1388 : : {
1389 : 1 : std::pair<Node, Node> sh = getSepHeapAndNilExpr();
1390 : 1 : m.setHeapModel(sh.first, sh.second);
1391 : 1 : }
1392 : : // print the model
1393 : 239 : std::stringstream ssm;
1394 : 239 : ssm << m;
1395 : 478 : return ssm.str();
1396 : 239 : }
1397 : :
1398 : 103 : void SolverEngine::blockModel(modes::BlockModelsMode mode)
1399 : : {
1400 [ + - ]: 103 : Trace("smt") << "SMT blockModel()" << endl;
1401 : 103 : TheoryModel* m = getAvailableModel("block model");
1402 : :
1403 : : // get expanded assertions
1404 : 103 : std::vector<Node> eassertsProc = getSubstitutedAssertions();
1405 : 103 : ModelBlocker mb(*d_env.get());
1406 : 103 : Node eblocker = mb.getModelBlocker(eassertsProc, m, mode);
1407 [ + - ]: 103 : Trace("smt") << "Block formula: " << eblocker << std::endl;
1408 : :
1409 : : // Must begin call now to ensure pops are processed. We cannot call this
1410 : : // above since we are accessing the model.
1411 : 103 : beginCall();
1412 : 103 : assertFormulaInternal(eblocker);
1413 : 103 : }
1414 : :
1415 : 228 : void SolverEngine::blockModelValues(const std::vector<Node>& exprs)
1416 : : {
1417 [ + - ]: 228 : Trace("smt") << "SMT blockModelValues()" << endl;
1418 : 228 : ensureWellFormedTerms(exprs, "block model values");
1419 : :
1420 : 228 : TheoryModel* m = getAvailableModel("block model values");
1421 : :
1422 : : // get expanded assertions
1423 : 228 : std::vector<Node> eassertsProc = getSubstitutedAssertions();
1424 : : // we always do block model values mode here
1425 : 228 : ModelBlocker mb(*d_env.get());
1426 : : Node eblocker = mb.getModelBlocker(
1427 : 228 : eassertsProc, m, modes::BlockModelsMode::VALUES, exprs);
1428 : :
1429 : : // Call begin call here, for same reasons as above.
1430 : 228 : beginCall();
1431 : 228 : assertFormulaInternal(eblocker);
1432 : 228 : }
1433 : :
1434 : 345 : std::pair<Node, Node> SolverEngine::getSepHeapAndNilExpr(void)
1435 : : {
1436 [ - + ]: 345 : if (!getLogicInfo().isTheoryEnabled(THEORY_SEP))
1437 : : {
1438 : 0 : const char* msg =
1439 : : "Cannot obtain separation logic expressions if not using the "
1440 : : "separation logic theory.";
1441 : 0 : throw RecoverableModalException(msg);
1442 : : }
1443 : 345 : Node heap;
1444 : 345 : Node nil;
1445 : 345 : TheoryModel* tm = getAvailableModel("get separation logic heap and nil");
1446 [ + + ]: 345 : if (!tm->getHeapModel(heap, nil))
1447 : : {
1448 : 4 : const char* msg =
1449 : : "Failed to obtain heap/nil "
1450 : : "expressions from theory model.";
1451 : 4 : throw RecoverableModalException(msg);
1452 : : }
1453 : 682 : return std::make_pair(heap, nil);
1454 : 349 : }
1455 : :
1456 : 1632 : std::vector<Node> SolverEngine::getAssertionsInternal() const
1457 : : {
1458 [ - + ][ - + ]: 1632 : Assert(d_state->isFullyInited());
[ - - ]
1459 : : // ensure that global declarations are processed
1460 : 1632 : d_smtSolver->getAssertions().refresh();
1461 : 1632 : const CDList<Node>& al = d_smtSolver->getAssertions().getAssertionList();
1462 : 1632 : std::vector<Node> res;
1463 [ + + ]: 3913 : for (const Node& n : al)
1464 : : {
1465 : 2281 : res.emplace_back(n);
1466 : : }
1467 : 1632 : return res;
1468 : 0 : }
1469 : :
1470 : 303343 : const Options& SolverEngine::options() const { return d_env->getOptions(); }
1471 : :
1472 : 24938 : bool SolverEngine::isWellFormedTerm(const Node& n) const
1473 : : {
1474 : : // Well formed if it does not have free variables. Note that n may have
1475 : : // variable shadowing.
1476 : 24938 : return !expr::hasFreeVar(n);
1477 : : }
1478 : :
1479 : 209246 : void SolverEngine::ensureWellFormedTerm(const Node& n,
1480 : : const std::string& src) const
1481 : : {
1482 [ + - ]: 209246 : if (Configuration::isAssertionBuild())
1483 : : {
1484 : : // Don't check for shadowing here, since shadowing may occur from API
1485 : : // users, including the smt2 parser. We don't need to rewrite since
1486 : : // getFreeVariables is robust to variable shadowing.
1487 : 209246 : std::unordered_set<internal::Node> fvs;
1488 : 209246 : expr::getFreeVariables(n, fvs);
1489 [ - + ]: 209246 : if (!fvs.empty())
1490 : : {
1491 : 0 : std::stringstream se;
1492 : 0 : se << "Cannot process term " << n << " with ";
1493 : 0 : se << "free variables: " << fvs;
1494 : 0 : se << " in context " << src << std::endl;
1495 : 0 : throw ModalException(se.str().c_str());
1496 : 0 : }
1497 : 209246 : }
1498 : 209246 : }
1499 : :
1500 : 49581 : void SolverEngine::ensureWellFormedTerms(const std::vector<Node>& ns,
1501 : : const std::string& src) const
1502 : : {
1503 [ + - ]: 49581 : if (Configuration::isAssertionBuild())
1504 : : {
1505 [ + + ]: 56066 : for (const Node& n : ns)
1506 : : {
1507 : 6485 : ensureWellFormedTerm(n, src);
1508 : : }
1509 : : }
1510 : 49581 : }
1511 : :
1512 : 6091 : void SolverEngine::printProof(std::ostream& out,
1513 : : std::shared_ptr<ProofNode> fp,
1514 : : modes::ProofFormat proofFormat,
1515 : : const std::map<Node, std::string>& assertionNames)
1516 : : {
1517 : 6091 : out << "(" << std::endl;
1518 : : // we print in the format based on the proof mode
1519 : 6091 : options::ProofFormatMode mode = options::ProofFormatMode::NONE;
1520 [ + + ][ - + ]: 6091 : switch (proofFormat)
[ - - ][ - ]
1521 : : {
1522 : 5413 : case modes::ProofFormat::DEFAULT:
1523 : 5413 : mode = options().proof.proofFormatMode;
1524 : 5413 : break;
1525 : 252 : case modes::ProofFormat::NONE: mode = options::ProofFormatMode::NONE; break;
1526 : 0 : case modes::ProofFormat::DOT: mode = options::ProofFormatMode::DOT; break;
1527 : 426 : case modes::ProofFormat::ALETHE:
1528 : 426 : mode = options::ProofFormatMode::ALETHE;
1529 : 426 : break;
1530 : 0 : case modes::ProofFormat::CPC: mode = options::ProofFormatMode::CPC; break;
1531 : 0 : case modes::ProofFormat::LFSC: mode = options::ProofFormatMode::LFSC; break;
1532 : : }
1533 : :
1534 : 6091 : d_pfManager->printProof(out,
1535 : : fp,
1536 : : mode,
1537 : : ProofScopeMode::DEFINITIONS_AND_ASSERTIONS,
1538 : : assertionNames);
1539 : 6091 : out << ")" << std::endl;
1540 : 6091 : }
1541 : :
1542 : 331 : std::vector<Node> SolverEngine::getSubstitutedAssertions()
1543 : : {
1544 : 331 : std::vector<Node> easserts = getAssertions();
1545 : : // must expand definitions
1546 : 331 : d_smtSolver->getPreprocessor()->applySubstitutions(easserts);
1547 : 331 : return easserts;
1548 : 0 : }
1549 : :
1550 : 815428 : Env& SolverEngine::getEnv() { return *d_env.get(); }
1551 : :
1552 : 1072 : void SolverEngine::declareSepHeap(TypeNode locT, TypeNode dataT)
1553 : : {
1554 [ - + ]: 1072 : if (d_state->isFullyInited())
1555 : : {
1556 : 0 : throw ModalException(
1557 : : "Cannot set logic in SolverEngine after the engine has "
1558 : 0 : "finished initializing.");
1559 : : }
1560 [ - + ]: 1072 : if (!getLogicInfo().isTheoryEnabled(THEORY_SEP))
1561 : : {
1562 : 0 : const char* msg =
1563 : : "Cannot declare heap if not using the separation logic theory.";
1564 : 0 : throw RecoverableModalException(msg);
1565 : : }
1566 : 1072 : TypeNode locT2, dataT2;
1567 [ + + ]: 1072 : if (getSepHeapTypes(locT2, dataT2))
1568 : : {
1569 : 3 : std::stringstream ss;
1570 : : ss << "ERROR: cannot declare heap types for separation logic more than "
1571 : 3 : "once. We are declaring heap of type ";
1572 : 3 : ss << locT << " -> " << dataT << ", but we already have ";
1573 : 3 : ss << locT2 << " -> " << dataT2;
1574 : 3 : throw LogicException(ss.str());
1575 : 3 : }
1576 : 1069 : d_env->declareSepHeap(locT, dataT);
1577 : 1075 : }
1578 : :
1579 : 1311 : bool SolverEngine::getSepHeapTypes(TypeNode& locT, TypeNode& dataT)
1580 : : {
1581 [ + + ]: 1311 : if (!d_env->hasSepHeap())
1582 : : {
1583 : 1307 : return false;
1584 : : }
1585 : 4 : locT = d_env->getSepLocType();
1586 : 4 : dataT = d_env->getSepDataType();
1587 : 4 : return true;
1588 : : }
1589 : :
1590 : 346 : Node SolverEngine::getSepHeapExpr() { return getSepHeapAndNilExpr().first; }
1591 : :
1592 : 338 : Node SolverEngine::getSepNilExpr() { return getSepHeapAndNilExpr().second; }
1593 : :
1594 : 648 : std::vector<Node> SolverEngine::getLearnedLiterals(modes::LearnedLitType t)
1595 : : {
1596 [ + - ]: 648 : Trace("smt") << "SMT getLearnedLiterals()" << std::endl;
1597 : : // note that the default mode for learned literals is via the prop engine,
1598 : : // although other modes could use the preprocessor
1599 : 648 : PropEngine* pe = d_smtSolver->getPropEngine();
1600 [ - + ][ - + ]: 648 : Assert(pe != nullptr);
[ - - ]
1601 : 648 : return pe->getLearnedZeroLevelLiterals(t);
1602 : : }
1603 : :
1604 : 2433 : void SolverEngine::checkProof()
1605 : : {
1606 [ - + ][ - + ]: 2433 : Assert(d_env->getOptions().smt.produceProofs);
[ - - ]
1607 [ + + ]: 2433 : if (d_env->isSatProofProducing())
1608 : : {
1609 : : // internal check the proof
1610 : 2427 : PropEngine* pe = d_smtSolver->getPropEngine();
1611 [ - + ][ - + ]: 2427 : Assert(pe != nullptr);
[ - - ]
1612 [ + + ]: 2427 : if (d_env->getOptions().proof.proofCheck == options::ProofCheckMode::EAGER)
1613 : : {
1614 : 7 : pe->checkProof(d_smtSolver->getAssertions().getAssertionList());
1615 : : }
1616 : : }
1617 : 2433 : std::shared_ptr<ProofNode> pePfn = getAvailableSatProof();
1618 [ + - ]: 2433 : if (d_env->getOptions().smt.checkProofs)
1619 : : {
1620 : : // connect proof to assertions, which will fail if the proof is malformed
1621 : 2433 : d_pfManager->connectProofToAssertions(
1622 : : pePfn, d_smtSolver->getAssertions(), ProofScopeMode::UNIFIED);
1623 : : // now check the proof
1624 : 2433 : d_pfManager->checkFinalProof(pePfn);
1625 : : }
1626 : 2433 : }
1627 : :
1628 : 275388 : void SolverEngine::beginCall(bool needsRLlimit)
1629 : : {
1630 : : // ensure this solver engine has been initialized
1631 : 275388 : finishInit();
1632 : : // ensure the context is current
1633 : 275383 : d_ctxManager->doPendingPops();
1634 : : // optionally, ensure the resource manager's state is current
1635 [ + + ]: 275383 : if (needsRLlimit)
1636 : : {
1637 : 60346 : ResourceManager* rm = getResourceManager();
1638 : 60346 : rm->beginCall();
1639 [ + - ]: 120692 : Trace("limit") << "SolverEngine::beginCall(): cumulative millis "
1640 : 0 : << rm->getTimeUsage() << ", resources "
1641 : 60346 : << rm->getResourceUsage() << std::endl;
1642 : : }
1643 : 275383 : }
1644 : :
1645 : 60273 : void SolverEngine::endCall()
1646 : : {
1647 : : // refresh the resource manager (for stats)
1648 : 60273 : ResourceManager* rm = getResourceManager();
1649 : 60273 : rm->refresh();
1650 [ + - ]: 120546 : Trace("limit") << "SolverEngine::endCall(): cumulative millis "
1651 : 0 : << rm->getTimeUsage() << ", resources "
1652 : 60273 : << rm->getResourceUsage() << std::endl;
1653 : 60273 : }
1654 : :
1655 : 286 : StatisticsRegistry& SolverEngine::getStatisticsRegistry()
1656 : : {
1657 : 286 : return d_env->getStatisticsRegistry();
1658 : : }
1659 : :
1660 : 4420 : UnsatCore SolverEngine::getUnsatCoreInternal(bool isInternal)
1661 : : {
1662 [ - + ]: 4420 : if (!d_env->getOptions().smt.produceUnsatCores)
1663 : : {
1664 : 0 : throw ModalException(
1665 : : "Cannot get an unsat core when produce-unsat-cores or produce-proofs "
1666 : 0 : "option is off.");
1667 : : }
1668 [ - + ]: 4420 : if (d_state->getMode() != SmtMode::UNSAT)
1669 : : {
1670 : 0 : throw RecoverableModalException(
1671 : : "Cannot get an unsat core unless immediately preceded by "
1672 : 0 : "UNSAT response.");
1673 : : }
1674 : 4420 : std::vector<Node> core = d_ucManager->getUnsatCore(isInternal);
1675 : 8840 : return UnsatCore(core);
1676 : 4420 : }
1677 : :
1678 : 2179 : void SolverEngine::checkUnsatCore()
1679 : : {
1680 [ - + ][ - + ]: 2179 : Assert(d_env->getOptions().smt.produceUnsatCores)
[ - - ]
1681 : 0 : << "cannot check unsat core if unsat cores are turned off";
1682 : :
1683 : 2179 : d_env->verbose(1) << "SolverEngine::checkUnsatCore(): generating unsat core"
1684 : 2179 : << std::endl;
1685 : 2179 : UnsatCore core = getUnsatCoreInternal();
1686 : :
1687 : : // initialize the core checker
1688 : 2179 : std::unique_ptr<SolverEngine> coreChecker;
1689 : 2179 : initializeSubsolver(coreChecker, *d_env.get());
1690 : : // disable all proof options
1691 : 2179 : SetDefaults::disableChecking(coreChecker->getOptions());
1692 : :
1693 : 2179 : d_env->verbose(1) << "SolverEngine::checkUnsatCore(): pushing core assertions"
1694 : 2179 : << std::endl;
1695 : : // set up the subsolver
1696 : : std::unordered_set<Node> adefs =
1697 : 2179 : d_smtSolver->getAssertions().getCurrentAssertionListDefitions();
1698 : 2179 : std::unordered_set<Node> removed;
1699 : 2179 : assertToSubsolver(*coreChecker.get(), core.getCore(), adefs, removed);
1700 : 2179 : Result r;
1701 : : try
1702 : : {
1703 : 2179 : r = coreChecker->checkSat();
1704 : : }
1705 : 0 : catch (...)
1706 : : {
1707 : 0 : throw;
1708 : 0 : }
1709 : 2179 : d_env->verbose(1) << "SolverEngine::checkUnsatCore(): result is " << r
1710 : 2179 : << std::endl;
1711 [ + + ]: 2179 : if (r.isUnknown())
1712 : : {
1713 : 2 : d_env->warning() << "SolverEngine::checkUnsatCore(): could not check core result "
1714 : 2 : "unknown."
1715 : 2 : << std::endl;
1716 : : }
1717 [ - + ]: 2177 : else if (r.getStatus() == Result::SAT)
1718 : : {
1719 : 0 : InternalError()
1720 : 0 : << "SolverEngine::checkUnsatCore(): produced core was satisfiable.";
1721 : : }
1722 : 2179 : }
1723 : :
1724 : 3096 : void SolverEngine::checkModel(bool hardFailure)
1725 : : {
1726 : 3096 : const CDList<Node>& al = d_smtSolver->getAssertions().getAssertionList();
1727 : : // we always enable the assertion list, so it is able to be checked
1728 : :
1729 : 3096 : TimerStat::CodeTimer checkModelTimer(d_stats->d_checkModelTime);
1730 : :
1731 : 3096 : d_env->verbose(1) << "SolverEngine::checkModel(): generating model"
1732 : 3096 : << std::endl;
1733 : 3096 : TheoryModel* m = getAvailableModel("check model");
1734 [ - + ][ - + ]: 3096 : Assert(m != nullptr);
[ - - ]
1735 : :
1736 : : // check the model with the theory engine for debugging
1737 [ + + ]: 3096 : if (options().smt.debugCheckModels)
1738 : : {
1739 : 2863 : TheoryEngine* te = d_smtSolver->getTheoryEngine();
1740 [ - + ][ - + ]: 2863 : Assert(te != nullptr);
[ - - ]
1741 : 2863 : te->checkTheoryAssertionsWithModel(hardFailure);
1742 : : }
1743 : :
1744 : : // check the model with the check models utility
1745 [ - + ][ - + ]: 3096 : Assert(d_checkModels != nullptr);
[ - - ]
1746 : 3096 : d_checkModels->checkModel(m, al, hardFailure);
1747 : 3096 : }
1748 : :
1749 : 1991 : UnsatCore SolverEngine::getUnsatCore()
1750 : : {
1751 [ + - ]: 1991 : Trace("smt") << "SMT getUnsatCore()" << std::endl;
1752 : 1991 : return getUnsatCoreInternal(false);
1753 : : }
1754 : :
1755 : 458 : std::vector<Node> SolverEngine::getUnsatCoreLemmas()
1756 : : {
1757 [ + - ]: 458 : Trace("smt") << "SMT getUnsatCoreLemmas()" << std::endl;
1758 : 458 : finishInit();
1759 [ - + ]: 458 : if (!d_env->getOptions().smt.produceUnsatCores)
1760 : : {
1761 : 0 : throw ModalException(
1762 : : "Cannot get lemmas used to derive unsat when produce-unsat-cores is "
1763 : 0 : "off.");
1764 : : }
1765 [ - + ]: 458 : if (d_state->getMode() != SmtMode::UNSAT)
1766 : : {
1767 : 0 : throw RecoverableModalException(
1768 : : "Cannot get lemmas used to derive unsat unless immediately preceded by "
1769 : 0 : "UNSAT response.");
1770 : : }
1771 : 458 : return d_ucManager->getUnsatCoreLemmas(false);
1772 : : }
1773 : :
1774 : 11 : void SolverEngine::getRelevantQuantTermVectors(
1775 : : std::map<Node, InstantiationList>& insts,
1776 : : std::map<Node, std::vector<Node>>& sks,
1777 : : bool getDebugInfo)
1778 : : {
1779 [ - + ][ - + ]: 11 : Assert(d_state->getMode() == SmtMode::UNSAT);
[ - - ]
1780 [ - + ][ - + ]: 11 : Assert(d_env->isTheoryProofProducing());
[ - - ]
1781 : : // note that we don't have to connect the SAT proof to the input assertions,
1782 : : // and preprocessing proofs don't impact what instantiations are used
1783 : 11 : d_ucManager->getRelevantQuantTermVectors(insts, sks, getDebugInfo);
1784 : 11 : }
1785 : :
1786 : 6590 : std::vector<std::shared_ptr<ProofNode>> SolverEngine::getProof(
1787 : : modes::ProofComponent c)
1788 : : {
1789 [ + - ]: 6590 : Trace("smt") << "SMT getProof()\n";
1790 : 6590 : const Options& opts = d_env->getOptions();
1791 [ - + ]: 6590 : if (!opts.smt.produceProofs)
1792 : : {
1793 : 0 : throw ModalException("Cannot get a proof when proof option is off.");
1794 : : }
1795 [ + + ]: 6590 : if (c == modes::ProofComponent::SAT
1796 [ + + ]: 6145 : || c == modes::ProofComponent::THEORY_LEMMAS
1797 [ + + ]: 6142 : || c == modes::ProofComponent::PREPROCESS)
1798 : : {
1799 [ + + ]: 451 : if (!d_env->isSatProofProducing())
1800 : : {
1801 : 1 : throw ModalException(
1802 : : "Cannot get a proof for this component when SAT solver is not proof "
1803 : 2 : "producing.");
1804 : : }
1805 : : }
1806 : : // The component modes::ProofComponent::PREPROCESS returns
1807 : : // the proof of all preprocessed assertions. It does not require being in an
1808 : : // unsat state.
1809 : 6589 : if (c != modes::ProofComponent::RAW_PREPROCESS
1810 [ + + ][ - + ]: 6589 : && d_state->getMode() != SmtMode::UNSAT)
[ - + ]
1811 : : {
1812 : 0 : throw RecoverableModalException(
1813 : : "Cannot get a proof unless immediately preceded by "
1814 : 0 : "UNSAT response.");
1815 : : }
1816 : : // determine if we should get the full proof from the SAT solver
1817 : 6589 : PropEngine* pe = d_smtSolver->getPropEngine();
1818 [ - + ][ - + ]: 6589 : Assert(pe != nullptr);
[ - - ]
1819 : 6589 : std::vector<std::shared_ptr<ProofNode>> ps;
1820 : 6589 : bool connectToPreprocess = false;
1821 : 6589 : bool connectMkOuterScope = false;
1822 [ + + ]: 6589 : if (c == modes::ProofComponent::RAW_PREPROCESS)
1823 : : {
1824 : : // use all preprocessed assertions
1825 : : const context::CDList<Node>& assertions =
1826 : 3 : d_smtSolver->getPreprocessedAssertions();
1827 : 3 : connectToPreprocess = true;
1828 : : // We start with (ASSUME a) for each preprocessed assertion a. This
1829 : : // proof will be connected to the proof of preprocessing for a.
1830 : 3 : ProofNodeManager* pnm = d_pfManager->getProofNodeManager();
1831 [ + + ]: 27 : for (const Node& a : assertions)
1832 : : {
1833 : 24 : ps.push_back(pnm->mkAssume(a));
1834 : : }
1835 : : }
1836 [ + + ]: 6586 : else if (c == modes::ProofComponent::SAT)
1837 : : {
1838 : 444 : ps.push_back(pe->getProof(false));
1839 : : }
1840 [ + + ]: 6142 : else if (c == modes::ProofComponent::THEORY_LEMMAS
1841 [ + + ]: 6139 : || c == modes::ProofComponent::PREPROCESS)
1842 : : {
1843 : 6 : ps = pe->getProofLeaves(c);
1844 : : // connect to preprocess proofs for preprocess mode
1845 : 6 : connectToPreprocess = (c == modes::ProofComponent::PREPROCESS);
1846 : : }
1847 [ + - ]: 6136 : else if (c == modes::ProofComponent::FULL)
1848 : : {
1849 : 6136 : ps.push_back(getAvailableSatProof());
1850 : 6136 : connectToPreprocess = true;
1851 : 6136 : connectMkOuterScope = true;
1852 : : }
1853 : : else
1854 : : {
1855 : 0 : std::stringstream ss;
1856 : 0 : ss << "Unknown proof component " << c << std::endl;
1857 : 0 : throw RecoverableModalException(ss.str());
1858 : 0 : }
1859 : :
1860 [ - + ][ - + ]: 6589 : Assert(d_pfManager);
[ - - ]
1861 : : // connect proofs to preprocessing, if specified
1862 [ + + ]: 6589 : if (connectToPreprocess)
1863 : : {
1864 : 6142 : ProofScopeMode scopeMode = connectMkOuterScope
1865 [ + + ]: 6142 : ? ProofScopeMode::DEFINITIONS_AND_ASSERTIONS
1866 : : : ProofScopeMode::NONE;
1867 [ + + ]: 12314 : for (std::shared_ptr<ProofNode>& p : ps)
1868 : : {
1869 [ - + ][ - + ]: 6172 : Assert(p != nullptr);
[ - - ]
1870 : 12344 : p = d_pfManager->connectProofToAssertions(
1871 : 6172 : p, d_smtSolver->getAssertions(), scopeMode);
1872 : : }
1873 : : }
1874 : 6589 : return ps;
1875 : 0 : }
1876 : :
1877 : 0 : void SolverEngine::proofToString(std::ostream& out,
1878 : : std::shared_ptr<ProofNode> fp)
1879 : : {
1880 : : options::ProofFormatMode format_mode =
1881 : 0 : getOptions().proof.proofFormatMode;
1882 : 0 : d_pfManager->printProof(
1883 : : out, fp, format_mode, ProofScopeMode::DEFINITIONS_AND_ASSERTIONS);
1884 : 0 : }
1885 : :
1886 : 79 : void SolverEngine::printInstantiations(std::ostream& out)
1887 : : {
1888 : 79 : QuantifiersEngine* qe = getAvailableQuantifiersEngine("printInstantiations");
1889 : :
1890 : : // First, extract and print the skolemizations
1891 : 79 : bool printed = false;
1892 : 79 : bool reqNames = !d_env->getOptions().quantifiers.printInstFull;
1893 : :
1894 : : // Extract the skolemizations and instantiations
1895 : 79 : std::map<Node, std::vector<Node>> sks;
1896 : 79 : std::map<Node, InstantiationList> rinsts;
1897 [ + + ]: 87 : if ((d_env->getOptions().smt.produceProofs && d_env->isTheoryProofProducing())
1898 [ + + ][ + - ]: 87 : && getSmtMode() == SmtMode::UNSAT)
[ + + ]
1899 : : {
1900 : : // minimize skolemizations and instantiations based on proof manager
1901 : 4 : getRelevantQuantTermVectors(
1902 : 4 : rinsts, sks, options().driver.dumpInstantiationsDebug);
1903 : : }
1904 : : else
1905 : : {
1906 : : // get all skolem term vectors
1907 : 75 : qe->getSkolemTermVectors(sks);
1908 : : // get all instantiations
1909 : 75 : std::map<Node, std::vector<std::vector<Node>>> insts;
1910 : 75 : qe->getInstantiationTermVectors(insts);
1911 [ + + ]: 152 : for (const std::pair<const Node, std::vector<std::vector<Node>>>& i : insts)
1912 : : {
1913 : : // convert to instantiation list
1914 : 77 : Node q = i.first;
1915 : 77 : InstantiationList& ilq = rinsts[q];
1916 : 77 : ilq.initialize(q);
1917 [ + + ]: 166 : for (const std::vector<Node>& ii : i.second)
1918 : : {
1919 : 89 : ilq.d_inst.push_back(InstantiationVec(ii));
1920 : : }
1921 : 77 : }
1922 : 75 : }
1923 : : // only print when in list mode
1924 : 79 : if (d_env->getOptions().quantifiers.printInstMode
1925 [ + + ]: 79 : == options::PrintInstMode::LIST)
1926 : : {
1927 [ + + ]: 82 : for (const std::pair<const Node, std::vector<Node>>& s : sks)
1928 : : {
1929 : 6 : Node name;
1930 [ - + ]: 6 : if (!qe->getNameForQuant(s.first, name, reqNames))
1931 : : {
1932 : : // did not have a name and we are only printing formulas with names
1933 : 0 : continue;
1934 : : }
1935 : 6 : SkolemList slist(name, s.second);
1936 : 6 : out << slist;
1937 : 6 : printed = true;
1938 [ + - ]: 6 : }
1939 : : }
1940 [ + + ]: 164 : for (std::pair<const Node, InstantiationList>& i : rinsts)
1941 : : {
1942 [ - + ]: 85 : if (i.second.d_inst.empty())
1943 : : {
1944 : : // no instantiations, skip
1945 : 0 : continue;
1946 : : }
1947 : 85 : Node name;
1948 [ - + ]: 85 : if (!qe->getNameForQuant(i.first, name, reqNames))
1949 : : {
1950 : : // did not have a name and we are only printing formulas with names
1951 : 0 : continue;
1952 : : }
1953 : : // must have a name
1954 : 85 : if (d_env->getOptions().quantifiers.printInstMode
1955 [ + + ]: 85 : == options::PrintInstMode::NUM)
1956 : : {
1957 : 12 : out << "(num-instantiations " << name << " " << i.second.d_inst.size()
1958 : 6 : << ")" << std::endl;
1959 : : }
1960 : : else
1961 : : {
1962 : : // take the name
1963 : 79 : i.second.d_quant = name;
1964 [ - + ][ - + ]: 79 : Assert(d_env->getOptions().quantifiers.printInstMode
[ - - ]
1965 : : == options::PrintInstMode::LIST);
1966 : 79 : out << i.second;
1967 : : }
1968 : 85 : printed = true;
1969 [ + - ]: 85 : }
1970 : : // if we did not print anything, we indicate this
1971 [ - + ]: 79 : if (!printed)
1972 : : {
1973 : 0 : out << "none" << std::endl;
1974 : : }
1975 : 79 : }
1976 : :
1977 : 0 : void SolverEngine::getInstantiationTermVectors(
1978 : : std::map<Node, std::vector<std::vector<Node>>>& insts)
1979 : : {
1980 : : QuantifiersEngine* qe =
1981 : 0 : getAvailableQuantifiersEngine("getInstantiationTermVectors");
1982 : : // get the list of all instantiations
1983 : 0 : qe->getInstantiationTermVectors(insts);
1984 : 0 : }
1985 : :
1986 : 712 : bool SolverEngine::getSynthSolutions(std::map<Node, Node>& solMap)
1987 : : {
1988 [ - + ]: 712 : if (d_sygusSolver == nullptr)
1989 : : {
1990 : 0 : throw RecoverableModalException(
1991 : 0 : "Cannot get synth solutions in this context.");
1992 : : }
1993 : 712 : bool ret = d_sygusSolver->getSynthSolutions(solMap);
1994 : : // we return false if solMap is empty, that is, when we ask for a solution
1995 : : // when none is available.
1996 [ + + ][ + + ]: 712 : return ret && !solMap.empty();
1997 : : }
1998 : :
1999 : 1320 : bool SolverEngine::getSubsolverSynthSolutions(std::map<Node, Node>& solMap)
2000 : : {
2001 [ - + ]: 1320 : if (d_sygusSolver == nullptr)
2002 : : {
2003 : 0 : throw RecoverableModalException(
2004 : 0 : "Cannot get subsolver synth solutions in this context.");
2005 : : }
2006 : 1320 : bool ret = d_sygusSolver->getSubsolverSynthSolutions(solMap);
2007 : : // we return false if solMap is empty, that is, when we ask for a solution
2008 : : // when none is available.
2009 [ + + ][ + + ]: 1320 : return ret && !solMap.empty();
2010 : : }
2011 : :
2012 : 415 : Node SolverEngine::getQuantifierElimination(Node q, bool doFull)
2013 : : {
2014 : 415 : beginCall(true);
2015 : : Node result = d_quantElimSolver->getQuantifierElimination(
2016 : 419 : q, doFull, d_isInternalSubsolver);
2017 : 411 : endCall();
2018 : 411 : return result;
2019 : 0 : }
2020 : :
2021 : 420 : Node SolverEngine::getInterpolant(const Node& conj, const TypeNode& grammarType)
2022 : : {
2023 : 420 : beginCall(true);
2024 : : // Analogous to getAbduct, ensure that assertions are current.
2025 : 419 : d_smtDriver->refreshAssertions();
2026 : 419 : std::vector<Node> axioms = getAssertions();
2027 : 419 : Node interpol;
2028 : : bool success =
2029 : 419 : d_interpolSolver->getInterpolant(axioms, conj, grammarType, interpol);
2030 : : // notify the state of whether the get-interpolant call was successfuly, which
2031 : : // impacts the SMT mode.
2032 : 419 : d_state->notifyGetInterpol(success);
2033 : 419 : endCall();
2034 [ - + ][ - + ]: 419 : Assert(success == !interpol.isNull());
[ - - ]
2035 : 838 : return interpol;
2036 : 419 : }
2037 : :
2038 : 94 : Node SolverEngine::getInterpolantNext()
2039 : : {
2040 : 94 : beginCall(true);
2041 [ - + ]: 94 : if (d_state->getMode() != SmtMode::INTERPOL)
2042 : : {
2043 : 0 : throw RecoverableModalException(
2044 : : "Cannot get-interpolant-next unless immediately preceded by a "
2045 : : "successful "
2046 : 0 : "call to get-interpolant(-next).");
2047 : : }
2048 : 94 : Node interpol;
2049 : 94 : bool success = d_interpolSolver->getInterpolantNext(interpol);
2050 : : // notify the state of whether the get-interpolantant-next call was successful
2051 : 94 : d_state->notifyGetInterpol(success);
2052 : 94 : endCall();
2053 [ - + ][ - + ]: 94 : Assert(success == !interpol.isNull());
[ - - ]
2054 : 94 : return interpol;
2055 : 0 : }
2056 : :
2057 : 417 : Node SolverEngine::getAbduct(const Node& conj, const TypeNode& grammarType)
2058 : : {
2059 : 417 : beginCall(true);
2060 : : // ensure that assertions are current
2061 : 416 : d_smtDriver->refreshAssertions();
2062 : 416 : std::vector<Node> axioms = getAssertions();
2063 : : // expand definitions in the conjecture as well
2064 : 416 : Node abd;
2065 : 416 : bool success = d_abductSolver->getAbduct(axioms, conj, grammarType, abd);
2066 : : // notify the state of whether the get-abduct call was successful, which
2067 : : // impacts the SMT mode.
2068 : 412 : d_state->notifyGetAbduct(success);
2069 : 412 : endCall();
2070 [ - + ][ - + ]: 412 : Assert(success == !abd.isNull());
[ - - ]
2071 : 824 : return abd;
2072 : 420 : }
2073 : :
2074 : 92 : Node SolverEngine::getAbductNext()
2075 : : {
2076 : 92 : beginCall(true);
2077 [ - + ]: 92 : if (d_state->getMode() != SmtMode::ABDUCT)
2078 : : {
2079 : 0 : throw RecoverableModalException(
2080 : : "Cannot get-abduct-next unless immediately preceded by a successful "
2081 : 0 : "call to get-abduct(-next).");
2082 : : }
2083 : 92 : Node abd;
2084 : 92 : bool success = d_abductSolver->getAbductNext(abd);
2085 : : // notify the state of whether the get-abduct-next call was successful
2086 : 92 : d_state->notifyGetAbduct(success);
2087 : 92 : endCall();
2088 [ - + ][ - + ]: 92 : Assert(success == !abd.isNull());
[ - - ]
2089 : 92 : return abd;
2090 : 0 : }
2091 : :
2092 : 68 : void SolverEngine::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs)
2093 : : {
2094 : : QuantifiersEngine* qe =
2095 : 68 : getAvailableQuantifiersEngine("getInstantiatedQuantifiedFormulas");
2096 : 68 : qe->getInstantiatedQuantifiedFormulas(qs);
2097 : 68 : }
2098 : :
2099 : 68 : void SolverEngine::getInstantiationTermVectors(
2100 : : Node q, std::vector<std::vector<Node>>& tvecs)
2101 : : {
2102 : : QuantifiersEngine* qe =
2103 : 68 : getAvailableQuantifiersEngine("getInstantiationTermVectors");
2104 : 68 : qe->getInstantiationTermVectors(q, tvecs);
2105 : 68 : }
2106 : :
2107 : 1419 : std::vector<Node> SolverEngine::getAssertions()
2108 : : {
2109 : : // ensure this solver engine has been initialized
2110 : 1419 : finishInit();
2111 [ + - ]: 1419 : Trace("smt") << "SMT getAssertions()" << endl;
2112 : : // note we always enable assertions, so it is available here
2113 : 1419 : return getAssertionsInternal();
2114 : : }
2115 : :
2116 : 456 : void SolverEngine::getDifficultyMap(std::map<Node, Node>& dmap)
2117 : : {
2118 [ + - ]: 456 : Trace("smt") << "SMT getDifficultyMap()\n";
2119 : : // ensure this solver engine has been initialized
2120 : 456 : finishInit();
2121 [ + + ]: 456 : if (!d_env->getOptions().smt.produceDifficulty)
2122 : : {
2123 : 2 : throw ModalException(
2124 : 4 : "Cannot get difficulty when difficulty option is off.");
2125 : : }
2126 : : // the prop engine has the proof of false
2127 [ - + ][ - + ]: 454 : Assert(d_pfManager);
[ - - ]
2128 : : // get difficulty map from theory engine first
2129 : 454 : TheoryEngine* te = d_smtSolver->getTheoryEngine();
2130 : : // do not include lemmas
2131 : 454 : te->getDifficultyMap(dmap, false);
2132 : : // then ask proof manager to translate dmap in terms of the input
2133 : 454 : d_pfManager->translateDifficultyMap(dmap, d_smtSolver->getAssertions());
2134 : 454 : }
2135 : :
2136 : 5079 : void SolverEngine::push()
2137 : : {
2138 : 5079 : beginCall();
2139 [ + - ]: 5079 : Trace("smt") << "SMT push()" << endl;
2140 : 5079 : d_smtDriver->refreshAssertions();
2141 : 5079 : d_ctxManager->userPush();
2142 : 5079 : }
2143 : :
2144 : 3750 : void SolverEngine::pop()
2145 : : {
2146 : 3750 : beginCall();
2147 [ + - ]: 3750 : Trace("smt") << "SMT pop()" << endl;
2148 : 3750 : d_ctxManager->userPop();
2149 : :
2150 : : // clear the learned literals from the preprocessor
2151 : 3750 : d_smtSolver->getPreprocessor()->clearLearnedLiterals();
2152 : :
2153 [ + - ]: 7500 : Trace("userpushpop") << "SolverEngine: popped to level "
2154 : 3750 : << d_env->getUserContext()->getLevel() << endl;
2155 : : // should we reset d_status here?
2156 : : // SMT-LIBv2 spec seems to imply no, but it would make sense to..
2157 : 3750 : }
2158 : :
2159 : 691 : void SolverEngine::resetAssertions()
2160 : : {
2161 [ + + ]: 691 : if (!d_state->isFullyInited())
2162 : : {
2163 : : // We're still in Start Mode, nothing asserted yet, do nothing.
2164 : : // (see solver execution modes in the SMT-LIB standard)
2165 [ - + ][ - + ]: 4 : Assert(d_env->getContext()->getLevel() == 0);
[ - - ]
2166 [ - + ][ - + ]: 4 : Assert(d_env->getUserContext()->getLevel() == 0);
[ - - ]
2167 : 4 : return;
2168 : : }
2169 : :
2170 [ + - ]: 687 : Trace("smt") << "SMT resetAssertions()" << endl;
2171 : :
2172 : 687 : d_ctxManager->notifyResetAssertions();
2173 : :
2174 : : // reset SmtSolver, which will construct a new prop engine
2175 : 687 : d_smtSolver->resetAssertions();
2176 : : }
2177 : :
2178 : 155868 : void SolverEngine::interrupt()
2179 : : {
2180 [ - + ]: 155868 : if (!d_state->isFullyInited())
2181 : : {
2182 : 0 : return;
2183 : : }
2184 : 155868 : d_smtSolver->interrupt();
2185 : : }
2186 : :
2187 : 0 : void SolverEngine::setResourceLimit(uint64_t units, bool cumulative)
2188 : : {
2189 [ - - ]: 0 : if (cumulative)
2190 : : {
2191 : 0 : d_env->d_options.write_base().cumulativeResourceLimit = units;
2192 : : }
2193 : : else
2194 : : {
2195 : 0 : d_env->d_options.write_base().perCallResourceLimit = units;
2196 : : }
2197 : 0 : }
2198 : 2651 : void SolverEngine::setTimeLimit(uint64_t millis)
2199 : : {
2200 : 2651 : d_env->d_options.write_base().perCallMillisecondLimit = millis;
2201 : 2651 : }
2202 : :
2203 : 0 : unsigned long SolverEngine::getResourceUsage() const
2204 : : {
2205 : 0 : return getResourceManager()->getResourceUsage();
2206 : : }
2207 : :
2208 : 0 : unsigned long SolverEngine::getTimeUsage() const
2209 : : {
2210 : 0 : return getResourceManager()->getTimeUsage();
2211 : : }
2212 : :
2213 : 0 : unsigned long SolverEngine::getResourceRemaining() const
2214 : : {
2215 : 0 : return getResourceManager()->getResourceRemaining();
2216 : : }
2217 : :
2218 : 13 : void SolverEngine::printStatisticsSafe(int fd) const
2219 : : {
2220 : 13 : d_env->getStatisticsRegistry().printSafe(fd);
2221 : 13 : }
2222 : :
2223 : 0 : void SolverEngine::printStatisticsDiff() const
2224 : : {
2225 : 0 : d_env->getStatisticsRegistry().printDiff(*d_env->getOptions().base.err);
2226 : 0 : d_env->getStatisticsRegistry().storeSnapshot();
2227 : 0 : }
2228 : :
2229 : 256436 : void SolverEngine::setOption(const std::string& key,
2230 : : const std::string& value,
2231 : : bool fromUser)
2232 : : {
2233 [ + + ][ + + ]: 256436 : if (fromUser && options().base.safeMode != options::SafeMode::UNRESTRICTED)
[ + + ]
2234 : : {
2235 : : // Note that the text "in safe mode" must appear in the error messages or
2236 : : // CI will fail, as it searches for this text.
2237 [ - + ]: 74 : if (key == "trace")
2238 : : {
2239 : 0 : throw FatalOptionException("cannot use trace messages in safe mode");
2240 : : }
2241 : : // verify its a regular option
2242 : 74 : options::OptionInfo oinfo = options::getInfo(getOptions(), key);
2243 [ + + ]: 74 : if (oinfo.category == options::OptionInfo::Category::EXPERT)
2244 : : {
2245 : : // option exception
2246 : 4 : std::stringstream ss;
2247 : : ss << "expert option " << key
2248 : 4 : << " cannot be set in safe mode.";
2249 : : // If we are setting to a default value, the exception can be avoided
2250 : : // by omitting the expert option.
2251 [ + + ]: 4 : if (getOption(key) == value)
2252 : : {
2253 : : // note this is not the case for options which safe mode explicitly
2254 : : // disables.
2255 : : ss << " The value for " << key << " is already its current value ("
2256 : 1 : << value << "). Omitting this option may avoid this exception.";
2257 : : }
2258 : 4 : throw FatalOptionException(ss.str());
2259 : 4 : }
2260 [ + + ]: 70 : else if (oinfo.category == options::OptionInfo::Category::REGULAR)
2261 : : {
2262 [ + - ][ - + ]: 2 : if (options().base.safeMode == options::SafeMode::SAFE && !oinfo.noSupports.empty())
[ - + ]
2263 : : {
2264 : 0 : std::stringstream ss;
2265 : : ss << "cannot set option " << key
2266 : 0 : << " in safe mode, as this option does not support ";
2267 : 0 : bool firstTime = true;
2268 [ - - ]: 0 : for (const std::string& s : oinfo.noSupports)
2269 : : {
2270 [ - - ]: 0 : if (!firstTime)
2271 : : {
2272 : 0 : ss << ", ";
2273 : : }
2274 : : else
2275 : : {
2276 : 0 : firstTime = false;
2277 : : }
2278 : 0 : ss << s;
2279 : : }
2280 : 0 : throw FatalOptionException(ss.str());
2281 : 0 : }
2282 [ + - ]: 2 : if (!d_safeOptsSetRegularOption)
2283 : : {
2284 : 2 : d_safeOptsSetRegularOption = true;
2285 : 2 : d_safeOptsRegularOption = key;
2286 : 2 : d_safeOptsRegularOptionValue = value;
2287 : 2 : d_safeOptsSetRegularOptionToDefault = (getOption(key) == value);
2288 : : }
2289 : : else
2290 : : {
2291 : : // option exception
2292 : 0 : std::stringstream ss;
2293 : 0 : ss << "cannot set two regular options (" << d_safeOptsRegularOption
2294 : 0 : << " and " << key << ") in safe mode.";
2295 : : // similar to above, if setting to default value for either of the
2296 : : // regular options.
2297 [ - - ]: 0 : for (size_t i = 0; i < 2; i++)
2298 : : {
2299 [ - - ]: 0 : const std::string& rkey = i == 0 ? d_safeOptsRegularOption : key;
2300 [ - - ]: 0 : const std::string& rvalue = i == 0 ? d_safeOptsRegularOptionValue : value;
2301 [ - - ]: 0 : bool isDefault = i == 0 ? d_safeOptsSetRegularOptionToDefault
2302 : 0 : : (getOption(key) == value);
2303 [ - - ]: 0 : if (isDefault)
2304 : : {
2305 : : // note this is not the case for options which safe mode
2306 : : // explicitly disables.
2307 : : ss << " The value for " << rkey << " is already its current value ("
2308 : 0 : << rvalue << "). Omitting this option may avoid this exception.";
2309 : : }
2310 : : }
2311 : 0 : throw FatalOptionException(ss.str());
2312 : 0 : }
2313 : : }
2314 : 74 : }
2315 [ + - ]: 256432 : Trace("smt") << "SMT setOption(" << key << ", " << value << ")" << endl;
2316 : 256432 : options::set(getOptions(), key, value);
2317 : 245340 : }
2318 : :
2319 : 15352 : void SolverEngine::setIsInternalSubsolver() { d_isInternalSubsolver = true; }
2320 : :
2321 : 0 : bool SolverEngine::isInternalSubsolver() const { return d_isInternalSubsolver; }
2322 : :
2323 : 1263154 : std::string SolverEngine::getOption(const std::string& key) const
2324 : : {
2325 [ + - ]: 1263154 : Trace("smt") << "SMT getOption(" << key << ")" << endl;
2326 : 1263154 : return options::get(getOptions(), key);
2327 : : }
2328 : :
2329 : 2027605 : Options& SolverEngine::getOptions() { return d_env->d_options; }
2330 : :
2331 : 1263154 : const Options& SolverEngine::getOptions() const { return d_env->getOptions(); }
2332 : :
2333 : 247292 : ResourceManager* SolverEngine::getResourceManager() const
2334 : : {
2335 : 247292 : return d_env->getResourceManager();
2336 : : }
2337 : :
2338 : : } // namespace cvc5::internal
|
