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