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