1 /******************************************************************************
2 * Top contributors (to current version):
3 * Andrew Reynolds, Morgan Deters, Abdalrhman Mohamed
5 * This file is part of the cvc5 project.
7 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8 * in the top-level source directory and their institutional affiliations.
9 * All rights reserved. See the file COPYING in the top-level source
10 * directory for licensing information.
11 * ****************************************************************************
13 * The main entry point into the cvc5 library's SMT interface.
16 #include "smt/smt_engine.h"
18 #include "base/check.h"
19 #include "base/exception.h"
20 #include "base/modal_exception.h"
21 #include "base/output.h"
22 #include "decision/decision_engine.h"
23 #include "expr/bound_var_manager.h"
24 #include "expr/node.h"
25 #include "options/base_options.h"
26 #include "options/expr_options.h"
27 #include "options/language.h"
28 #include "options/main_options.h"
29 #include "options/option_exception.h"
30 #include "options/options_public.h"
31 #include "options/parser_options.h"
32 #include "options/printer_options.h"
33 #include "options/proof_options.h"
34 #include "options/smt_options.h"
35 #include "options/theory_options.h"
36 #include "printer/printer.h"
37 #include "proof/unsat_core.h"
38 #include "prop/prop_engine.h"
39 #include "smt/abduction_solver.h"
40 #include "smt/abstract_values.h"
41 #include "smt/assertions.h"
42 #include "smt/check_models.h"
44 #include "smt/dump_manager.h"
46 #include "smt/interpolation_solver.h"
47 #include "smt/listeners.h"
48 #include "smt/logic_exception.h"
49 #include "smt/model_blocker.h"
50 #include "smt/model_core_builder.h"
51 #include "smt/node_command.h"
52 #include "smt/preprocessor.h"
53 #include "smt/proof_manager.h"
54 #include "smt/quant_elim_solver.h"
55 #include "smt/set_defaults.h"
56 #include "smt/smt_engine_scope.h"
57 #include "smt/smt_engine_state.h"
58 #include "smt/smt_engine_stats.h"
59 #include "smt/smt_solver.h"
60 #include "smt/sygus_solver.h"
61 #include "smt/unsat_core_manager.h"
62 #include "theory/quantifiers/instantiation_list.h"
63 #include "theory/quantifiers/quantifiers_attributes.h"
64 #include "theory/quantifiers_engine.h"
65 #include "theory/rewriter.h"
66 #include "theory/smt_engine_subsolver.h"
67 #include "theory/theory_engine.h"
68 #include "util/random.h"
69 #include "util/rational.h"
70 #include "util/resource_manager.h"
71 #include "util/sexpr.h"
72 #include "util/statistics_registry.h"
74 // required for hacks related to old proofs for unsat cores
75 #include "base/configuration.h"
76 #include "base/configuration_private.h"
79 using namespace cvc5::smt
;
80 using namespace cvc5::preprocessing
;
81 using namespace cvc5::prop
;
82 using namespace cvc5::context
;
83 using namespace cvc5::theory
;
87 SmtEngine::SmtEngine(NodeManager
* nm
, const Options
* optr
)
88 : d_env(new Env(nm
, optr
)),
89 d_state(new SmtEngineState(*d_env
.get(), *this)),
90 d_absValues(new AbstractValues(getNodeManager())),
91 d_asserts(new Assertions(*d_env
.get(), *d_absValues
.get())),
92 d_routListener(new ResourceOutListener(*this)),
93 d_snmListener(new SmtNodeManagerListener(*getDumpManager(), d_outMgr
)),
95 d_checkModels(nullptr),
98 d_sygusSolver(nullptr),
99 d_abductSolver(nullptr),
100 d_interpolSolver(nullptr),
101 d_quantElimSolver(nullptr),
102 d_isInternalSubsolver(false),
108 // !!!!!!!!!!!!!!!!!!!!!! temporary hack: this makes the current SmtEngine
109 // we are constructing the current SmtEngine in scope for the lifetime of
110 // this SmtEngine, or until another SmtEngine is constructed (that SmtEngine
111 // is then in scope during its lifetime). This is mostly to ensure that
112 // options are always in scope, for e.g. printing expressions, which rely
113 // on knowing the output language.
114 // Notice that the SmtEngine may spawn new SmtEngine "subsolvers" internally.
115 // These are created, used, and deleted in a modular fashion while not
116 // interleaving calls to the master SmtEngine. Thus the hack here does not
117 // break this use case.
118 // On the other hand, this hack breaks use cases where multiple SmtEngine
119 // objects are created by the user.
120 d_scope
.reset(new SmtScope(this));
121 // listen to node manager events
122 getNodeManager()->subscribeEvents(d_snmListener
.get());
123 // listen to resource out
124 getResourceManager()->registerListener(d_routListener
.get());
126 d_stats
.reset(new SmtEngineStatistics());
127 // reset the preprocessor
129 new smt::Preprocessor(*this, *d_env
.get(), *d_absValues
.get(), *d_stats
));
130 // make the SMT solver
131 d_smtSolver
.reset(new SmtSolver(*d_env
.get(), *d_state
, *d_pp
, *d_stats
));
132 // make the SyGuS solver
133 d_sygusSolver
.reset(new SygusSolver(*d_env
.get(), *d_smtSolver
, *d_pp
));
134 // make the quantifier elimination solver
135 d_quantElimSolver
.reset(new QuantElimSolver(*d_env
.get(), *d_smtSolver
));
138 bool SmtEngine::isFullyInited() const { return d_state
->isFullyInited(); }
139 bool SmtEngine::isQueryMade() const { return d_state
->isQueryMade(); }
140 size_t SmtEngine::getNumUserLevels() const
142 return d_state
->getNumUserLevels();
144 SmtMode
SmtEngine::getSmtMode() const { return d_state
->getMode(); }
145 bool SmtEngine::isSmtModeSat() const
147 SmtMode mode
= getSmtMode();
148 return mode
== SmtMode::SAT
|| mode
== SmtMode::SAT_UNKNOWN
;
150 Result
SmtEngine::getStatusOfLastCommand() const
152 return d_state
->getStatus();
154 context::UserContext
* SmtEngine::getUserContext()
156 return d_env
->getUserContext();
158 context::Context
* SmtEngine::getContext() { return d_env
->getContext(); }
160 TheoryEngine
* SmtEngine::getTheoryEngine()
162 return d_smtSolver
->getTheoryEngine();
165 prop::PropEngine
* SmtEngine::getPropEngine()
167 return d_smtSolver
->getPropEngine();
170 void SmtEngine::finishInit()
172 if (d_state
->isFullyInited())
174 // already initialized, return
178 // Notice that finishInitInternal is called when options are finalized. If we
179 // are parsing smt2, this occurs at the moment we enter "Assert mode", page 52
180 // of SMT-LIB 2.6 standard.
183 const LogicInfo
& logic
= getLogicInfo();
184 if (!logic
.isLocked())
189 // set the random seed
190 Random::getRandom().setSeed(d_env
->getOptions().driver
.seed
);
192 // Call finish init on the set defaults module. This inializes the logic
193 // and the best default options based on our heuristics.
194 SetDefaults
sdefaults(d_isInternalSubsolver
);
195 sdefaults
.setDefaults(d_env
->d_logic
, getOptions());
197 ProofNodeManager
* pnm
= nullptr;
198 if (d_env
->getOptions().smt
.produceProofs
)
200 // ensure bound variable uses canonical bound variables
201 getNodeManager()->getBoundVarManager()->enableKeepCacheValues();
202 // make the proof manager
203 d_pfManager
.reset(new PfManager(*d_env
.get(), this));
204 PreprocessProofGenerator
* pppg
= d_pfManager
->getPreprocessProofGenerator();
205 // start the unsat core manager
206 d_ucManager
.reset(new UnsatCoreManager());
207 // use this proof node manager
208 pnm
= d_pfManager
->getProofNodeManager();
209 // enable proof support in the environment/rewriter
210 d_env
->setProofNodeManager(pnm
);
211 // enable it in the assertions pipeline
212 d_asserts
->setProofGenerator(pppg
);
213 // enabled proofs in the preprocessor
214 d_pp
->setProofGenerator(pppg
);
217 Trace("smt-debug") << "SmtEngine::finishInit" << std::endl
;
218 d_smtSolver
->finishInit(logic
);
220 // now can construct the SMT-level model object
221 TheoryEngine
* te
= d_smtSolver
->getTheoryEngine();
222 Assert(te
!= nullptr);
223 TheoryModel
* tm
= te
->getModel();
226 // make the check models utility
227 d_checkModels
.reset(new CheckModels(*d_env
.get()));
230 // global push/pop around everything, to ensure proper destruction
231 // of context-dependent data structures
234 Trace("smt-debug") << "Set up assertions..." << std::endl
;
235 d_asserts
->finishInit();
237 // dump out a set-logic command only when raw-benchmark is disabled to avoid
238 // dumping the command twice.
239 if (Dump
.isOn("benchmark") && !Dump
.isOn("raw-benchmark"))
241 LogicInfo everything
;
243 getPrinter().toStreamCmdComment(
245 "cvc5 always dumps the most general, all-supported logic (below), as "
246 "some internals might require the use of a logic more general than "
248 getPrinter().toStreamCmdSetBenchmarkLogic(d_env
->getDumpOut(),
249 everything
.getLogicString());
252 // initialize the dump manager
253 getDumpManager()->finishInit();
256 if (d_env
->getOptions().smt
.produceAbducts
)
258 d_abductSolver
.reset(new AbductionSolver(*d_env
.get()));
260 if (d_env
->getOptions().smt
.produceInterpols
261 != options::ProduceInterpols::NONE
)
263 d_interpolSolver
.reset(new InterpolationSolver(*d_env
.get()));
268 AlwaysAssert(getPropEngine()->getAssertionLevel() == 0)
269 << "The PropEngine has pushed but the SmtEngine "
270 "hasn't finished initializing!";
272 Assert(getLogicInfo().isLocked());
274 // store that we are finished initializing
275 d_state
->finishInit();
276 Trace("smt-debug") << "SmtEngine::finishInit done" << std::endl
;
279 void SmtEngine::shutdown() {
282 d_smtSolver
->shutdown();
287 SmtEngine::~SmtEngine()
294 // global push/pop around everything, to ensure proper destruction
295 // of context-dependent data structures
298 //destroy all passes before destroying things that they refer to
301 d_pfManager
.reset(nullptr);
302 d_ucManager
.reset(nullptr);
304 d_absValues
.reset(nullptr);
305 d_asserts
.reset(nullptr);
307 d_abductSolver
.reset(nullptr);
308 d_interpolSolver
.reset(nullptr);
309 d_quantElimSolver
.reset(nullptr);
310 d_sygusSolver
.reset(nullptr);
311 d_smtSolver
.reset(nullptr);
313 d_stats
.reset(nullptr);
314 getNodeManager()->unsubscribeEvents(d_snmListener
.get());
315 d_snmListener
.reset(nullptr);
316 d_routListener
.reset(nullptr);
319 d_state
.reset(nullptr);
320 // destroy the environment
321 d_env
.reset(nullptr);
322 } catch(Exception
& e
) {
323 Warning() << "cvc5 threw an exception during cleanup." << endl
<< e
<< endl
;
327 void SmtEngine::setLogic(const LogicInfo
& logic
)
330 if (d_state
->isFullyInited())
332 throw ModalException("Cannot set logic in SmtEngine after the engine has "
333 "finished initializing.");
335 d_env
->d_logic
= logic
;
340 void SmtEngine::setLogic(const std::string
& s
)
345 setLogic(LogicInfo(s
));
346 // dump out a set-logic command
347 if (Dump
.isOn("raw-benchmark"))
349 getPrinter().toStreamCmdSetBenchmarkLogic(
350 d_env
->getDumpOut(), getLogicInfo().getLogicString());
353 catch (IllegalArgumentException
& e
)
355 throw LogicException(e
.what());
359 void SmtEngine::setLogic(const char* logic
) { setLogic(string(logic
)); }
361 const LogicInfo
& SmtEngine::getLogicInfo() const
363 return d_env
->getLogicInfo();
366 LogicInfo
SmtEngine::getUserLogicInfo() const
368 // Lock the logic to make sure that this logic can be queried. We create a
369 // copy of the user logic here to keep this method const.
370 LogicInfo res
= d_userLogic
;
375 void SmtEngine::setLogicInternal()
377 Assert(!d_state
->isFullyInited())
378 << "setting logic in SmtEngine but the engine has already"
379 " finished initializing for this run";
380 d_env
->d_logic
.lock();
384 void SmtEngine::setInfo(const std::string
& key
, const std::string
& value
)
388 Trace("smt") << "SMT setInfo(" << key
<< ", " << value
<< ")" << endl
;
390 if (Dump
.isOn("benchmark"))
397 : ((value
== "unsat") ? Result::UNSAT
: Result::SAT_UNKNOWN
);
398 getPrinter().toStreamCmdSetBenchmarkStatus(d_env
->getDumpOut(), status
);
402 getPrinter().toStreamCmdSetInfo(d_env
->getDumpOut(), key
, value
);
406 if (key
== "filename")
408 d_env
->d_options
.driver
.filename
= value
;
409 d_env
->d_originalOptions
->driver
.filename
= value
;
410 d_env
->getStatisticsRegistry().registerValue
<std::string
>(
411 "driver::filename", value
);
413 else if (key
== "smt-lib-version" && !getOptions().base
.inputLanguageWasSetByUser
)
415 Language ilang
= Language::LANG_SMTLIB_V2_6
;
417 if (value
!= "2" && value
!= "2.6")
419 Warning() << "SMT-LIB version " << value
420 << " unsupported, defaulting to language (and semantics of) "
423 getOptions().base
.inputLanguage
= ilang
;
424 // also update the output language
425 if (!getOptions().base
.outputLanguageWasSetByUser
)
427 Language olang
= ilang
;
428 if (d_env
->getOptions().base
.outputLanguage
!= olang
)
430 getOptions().base
.outputLanguage
= olang
;
431 *d_env
->getOptions().base
.out
<< language::SetLanguage(olang
);
435 else if (key
== "status")
437 d_state
->notifyExpectedStatus(value
);
441 bool SmtEngine::isValidGetInfoFlag(const std::string
& key
) const
443 if (key
== "all-statistics" || key
== "error-behavior" || key
== "name"
444 || key
== "version" || key
== "authors" || key
== "status"
445 || key
== "reason-unknown" || key
== "assertion-stack-levels"
446 || key
== "all-options" || key
== "time")
453 std::string
SmtEngine::getInfo(const std::string
& key
) const
457 Trace("smt") << "SMT getInfo(" << key
<< ")" << endl
;
458 if (key
== "all-statistics")
460 return toSExpr(d_env
->getStatisticsRegistry().begin(), d_env
->getStatisticsRegistry().end());
462 if (key
== "error-behavior")
464 return "immediate-exit";
466 if (key
== "filename")
468 return d_env
->getOptions().driver
.filename
;
472 return toSExpr(Configuration::getName());
474 if (key
== "version")
476 return toSExpr(Configuration::getVersionString());
478 if (key
== "authors")
480 return toSExpr(Configuration::about());
484 // sat | unsat | unknown
485 Result status
= d_state
->getStatus();
486 switch (status
.asSatisfiabilityResult().isSat())
488 case Result::SAT
: return "sat";
489 case Result::UNSAT
: return "unsat";
490 default: return "unknown";
495 return toSExpr(std::clock());
497 if (key
== "reason-unknown")
499 Result status
= d_state
->getStatus();
500 if (!status
.isNull() && status
.isUnknown())
502 std::stringstream ss
;
503 ss
<< status
.whyUnknown();
504 std::string s
= ss
.str();
505 transform(s
.begin(), s
.end(), s
.begin(), ::tolower
);
510 throw RecoverableModalException(
511 "Can't get-info :reason-unknown when the "
512 "last result wasn't unknown!");
515 if (key
== "assertion-stack-levels")
517 size_t ulevel
= d_state
->getNumUserLevels();
518 AlwaysAssert(ulevel
<= std::numeric_limits
<unsigned long int>::max());
519 return toSExpr(ulevel
);
521 Assert(key
== "all-options");
522 // get the options, like all-statistics
523 std::vector
<std::vector
<std::string
>> res
;
524 for (const auto& opt
: options::getNames())
526 res
.emplace_back(std::vector
<std::string
>{opt
, options::get(getOptions(), opt
)});
531 void SmtEngine::debugCheckFormals(const std::vector
<Node
>& formals
, Node func
)
533 for (std::vector
<Node
>::const_iterator i
= formals
.begin();
537 if((*i
).getKind() != kind::BOUND_VARIABLE
) {
539 ss
<< "All formal arguments to defined functions must be BOUND_VARIABLEs, but in the\n"
540 << "definition of function " << func
<< ", formal\n"
542 << "has kind " << (*i
).getKind();
543 throw TypeCheckingExceptionPrivate(func
, ss
.str());
548 void SmtEngine::debugCheckFunctionBody(Node formula
,
549 const std::vector
<Node
>& formals
,
552 TypeNode formulaType
=
553 formula
.getType(d_env
->getOptions().expr
.typeChecking
);
554 TypeNode funcType
= func
.getType();
555 // We distinguish here between definitions of constants and functions,
556 // because the type checking for them is subtly different. Perhaps we
557 // should instead have SmtEngine::defineFunction() and
558 // SmtEngine::defineConstant() for better clarity, although then that
559 // doesn't match the SMT-LIBv2 standard...
560 if(formals
.size() > 0) {
561 TypeNode rangeType
= funcType
.getRangeType();
562 if(! formulaType
.isComparableTo(rangeType
)) {
564 ss
<< "Type of defined function does not match its declaration\n"
565 << "The function : " << func
<< "\n"
566 << "Declared type : " << rangeType
<< "\n"
567 << "The body : " << formula
<< "\n"
568 << "Body type : " << formulaType
;
569 throw TypeCheckingExceptionPrivate(func
, ss
.str());
572 if(! formulaType
.isComparableTo(funcType
)) {
574 ss
<< "Declared type of defined constant does not match its definition\n"
575 << "The constant : " << func
<< "\n"
576 << "Declared type : " << funcType
<< "\n"
577 << "The definition : " << formula
<< "\n"
578 << "Definition type: " << formulaType
;
579 throw TypeCheckingExceptionPrivate(func
, ss
.str());
584 void SmtEngine::defineFunction(Node func
,
585 const std::vector
<Node
>& formals
,
591 d_state
->doPendingPops();
592 Trace("smt") << "SMT defineFunction(" << func
<< ")" << endl
;
593 debugCheckFormals(formals
, func
);
596 ss
<< language::SetLanguage(
597 language::SetLanguage::getLanguage(Dump
.getStream()))
600 DefineFunctionNodeCommand
nc(ss
.str(), func
, formals
, formula
);
601 getDumpManager()->addToDump(nc
, "declarations");
604 debugCheckFunctionBody(formula
, formals
, func
);
606 // Substitute out any abstract values in formula
607 Node def
= d_absValues
->substituteAbstractValues(formula
);
608 if (!formals
.empty())
610 NodeManager
* nm
= NodeManager::currentNM();
612 kind::LAMBDA
, nm
->mkNode(kind::BOUND_VAR_LIST
, formals
), def
);
614 // A define-fun is treated as a (higher-order) assertion. It is provided
615 // to the assertions object. It will be added as a top-level substitution
616 // within this class, possibly multiple times if global is true.
617 Node feq
= func
.eqNode(def
);
618 d_asserts
->addDefineFunDefinition(feq
, global
);
621 void SmtEngine::defineFunctionsRec(
622 const std::vector
<Node
>& funcs
,
623 const std::vector
<std::vector
<Node
>>& formals
,
624 const std::vector
<Node
>& formulas
,
629 d_state
->doPendingPops();
630 Trace("smt") << "SMT defineFunctionsRec(...)" << endl
;
632 if (funcs
.size() != formals
.size() && funcs
.size() != formulas
.size())
635 ss
<< "Number of functions, formals, and function bodies passed to "
636 "defineFunctionsRec do not match:"
638 << " #functions : " << funcs
.size() << "\n"
639 << " #arg lists : " << formals
.size() << "\n"
640 << " #function bodies : " << formulas
.size() << "\n";
641 throw ModalException(ss
.str());
643 for (unsigned i
= 0, size
= funcs
.size(); i
< size
; i
++)
645 // check formal argument list
646 debugCheckFormals(formals
[i
], funcs
[i
]);
648 debugCheckFunctionBody(formulas
[i
], formals
[i
], funcs
[i
]);
651 if (Dump
.isOn("raw-benchmark"))
653 getPrinter().toStreamCmdDefineFunctionRec(
654 d_env
->getDumpOut(), funcs
, formals
, formulas
);
657 NodeManager
* nm
= getNodeManager();
658 for (unsigned i
= 0, size
= funcs
.size(); i
< size
; i
++)
660 // we assert a quantified formula
662 // make the function application
663 if (formals
[i
].empty())
665 // it has no arguments
670 std::vector
<Node
> children
;
671 children
.push_back(funcs
[i
]);
672 children
.insert(children
.end(), formals
[i
].begin(), formals
[i
].end());
673 func_app
= nm
->mkNode(kind::APPLY_UF
, children
);
675 Node lem
= nm
->mkNode(kind::EQUAL
, func_app
, formulas
[i
]);
676 if (!formals
[i
].empty())
678 // set the attribute to denote this is a function definition
679 Node aexpr
= nm
->mkNode(kind::INST_ATTRIBUTE
, func_app
);
680 aexpr
= nm
->mkNode(kind::INST_PATTERN_LIST
, aexpr
);
682 func_app
.setAttribute(fda
, true);
683 // make the quantified formula
684 Node boundVars
= nm
->mkNode(kind::BOUND_VAR_LIST
, formals
[i
]);
685 lem
= nm
->mkNode(kind::FORALL
, boundVars
, lem
, aexpr
);
687 // assert the quantified formula
688 // notice we don't call assertFormula directly, since this would
689 // duplicate the output on raw-benchmark.
690 // add define recursive definition to the assertions
691 d_asserts
->addDefineFunDefinition(lem
, global
);
695 void SmtEngine::defineFunctionRec(Node func
,
696 const std::vector
<Node
>& formals
,
700 std::vector
<Node
> funcs
;
701 funcs
.push_back(func
);
702 std::vector
<std::vector
<Node
>> formals_multi
;
703 formals_multi
.push_back(formals
);
704 std::vector
<Node
> formulas
;
705 formulas
.push_back(formula
);
706 defineFunctionsRec(funcs
, formals_multi
, formulas
, global
);
709 Result
SmtEngine::quickCheck() {
710 Assert(d_state
->isFullyInited());
711 Trace("smt") << "SMT quickCheck()" << endl
;
712 const std::string
& filename
= d_env
->getOptions().driver
.filename
;
714 Result::ENTAILMENT_UNKNOWN
, Result::REQUIRES_FULL_CHECK
, filename
);
717 TheoryModel
* SmtEngine::getAvailableModel(const char* c
) const
719 if (!d_env
->getOptions().theory
.assignFunctionValues
)
721 std::stringstream ss
;
722 ss
<< "Cannot " << c
<< " when --assign-function-values is false.";
723 throw RecoverableModalException(ss
.str().c_str());
726 if (d_state
->getMode() != SmtMode::SAT
727 && d_state
->getMode() != SmtMode::SAT_UNKNOWN
)
729 std::stringstream ss
;
731 << " unless immediately preceded by SAT/NOT_ENTAILED or UNKNOWN "
733 throw RecoverableModalException(ss
.str().c_str());
736 if (!d_env
->getOptions().smt
.produceModels
)
738 std::stringstream ss
;
739 ss
<< "Cannot " << c
<< " when produce-models options is off.";
740 throw ModalException(ss
.str().c_str());
743 TheoryEngine
* te
= d_smtSolver
->getTheoryEngine();
744 Assert(te
!= nullptr);
745 TheoryModel
* m
= te
->getBuiltModel();
749 std::stringstream ss
;
751 << " since model is not available. Perhaps the most recent call to "
752 "check-sat was interrupted?";
753 throw RecoverableModalException(ss
.str().c_str());
759 QuantifiersEngine
* SmtEngine::getAvailableQuantifiersEngine(const char* c
) const
761 QuantifiersEngine
* qe
= d_smtSolver
->getQuantifiersEngine();
764 std::stringstream ss
;
765 ss
<< "Cannot " << c
<< " when quantifiers are not present.";
766 throw ModalException(ss
.str().c_str());
771 void SmtEngine::notifyPushPre() { d_smtSolver
->processAssertions(*d_asserts
); }
773 void SmtEngine::notifyPushPost()
775 TimerStat::CodeTimer
pushPopTimer(d_stats
->d_pushPopTime
);
776 Assert(getPropEngine() != nullptr);
777 getPropEngine()->push();
780 void SmtEngine::notifyPopPre()
782 TimerStat::CodeTimer
pushPopTimer(d_stats
->d_pushPopTime
);
783 PropEngine
* pe
= getPropEngine();
784 Assert(pe
!= nullptr);
788 void SmtEngine::notifyPostSolvePre()
790 PropEngine
* pe
= getPropEngine();
791 Assert(pe
!= nullptr);
795 void SmtEngine::notifyPostSolvePost()
797 TheoryEngine
* te
= getTheoryEngine();
798 Assert(te
!= nullptr);
802 Result
SmtEngine::checkSat()
805 return checkSat(nullNode
);
808 Result
SmtEngine::checkSat(const Node
& assumption
)
810 if (Dump
.isOn("benchmark"))
812 getPrinter().toStreamCmdCheckSat(d_env
->getDumpOut(), assumption
);
814 std::vector
<Node
> assump
;
815 if (!assumption
.isNull())
817 assump
.push_back(assumption
);
819 return checkSatInternal(assump
, false);
822 Result
SmtEngine::checkSat(const std::vector
<Node
>& assumptions
)
824 if (Dump
.isOn("benchmark"))
826 if (assumptions
.empty())
828 getPrinter().toStreamCmdCheckSat(d_env
->getDumpOut());
832 getPrinter().toStreamCmdCheckSatAssuming(d_env
->getDumpOut(),
836 return checkSatInternal(assumptions
, false);
839 Result
SmtEngine::checkEntailed(const Node
& node
)
841 if (Dump
.isOn("benchmark"))
843 getPrinter().toStreamCmdQuery(d_env
->getDumpOut(), node
);
845 return checkSatInternal(
846 node
.isNull() ? std::vector
<Node
>() : std::vector
<Node
>{node
},
848 .asEntailmentResult();
851 Result
SmtEngine::checkEntailed(const std::vector
<Node
>& nodes
)
853 return checkSatInternal(nodes
, true).asEntailmentResult();
856 Result
SmtEngine::checkSatInternal(const std::vector
<Node
>& assumptions
,
857 bool isEntailmentCheck
)
864 Trace("smt") << "SmtEngine::"
865 << (isEntailmentCheck
? "checkEntailed" : "checkSat") << "("
866 << assumptions
<< ")" << endl
;
867 // check the satisfiability with the solver object
868 Result r
= d_smtSolver
->checkSatisfiability(
869 *d_asserts
.get(), assumptions
, isEntailmentCheck
);
871 Trace("smt") << "SmtEngine::" << (isEntailmentCheck
? "query" : "checkSat")
872 << "(" << assumptions
<< ") => " << r
<< endl
;
874 // Check that SAT results generate a model correctly.
875 if (d_env
->getOptions().smt
.checkModels
)
877 if (r
.asSatisfiabilityResult().isSat() == Result::SAT
)
882 // Check that UNSAT results generate a proof correctly.
883 if (d_env
->getOptions().smt
.checkProofs
884 || d_env
->getOptions().proof
.proofCheck
885 == options::ProofCheckMode::EAGER
)
887 if (r
.asSatisfiabilityResult().isSat() == Result::UNSAT
)
889 if ((d_env
->getOptions().smt
.checkProofs
890 || d_env
->getOptions().proof
.proofCheck
891 == options::ProofCheckMode::EAGER
)
892 && !d_env
->getOptions().smt
.produceProofs
)
894 throw ModalException(
895 "Cannot check-proofs because proofs were disabled.");
900 // Check that UNSAT results generate an unsat core correctly.
901 if (d_env
->getOptions().smt
.checkUnsatCores
)
903 if (r
.asSatisfiabilityResult().isSat() == Result::UNSAT
)
905 TimerStat::CodeTimer
checkUnsatCoreTimer(d_stats
->d_checkUnsatCoreTime
);
909 if (d_env
->getOptions().base
.statisticsEveryQuery
)
911 printStatisticsDiff();
915 catch (UnsafeInterruptException
& e
)
917 AlwaysAssert(getResourceManager()->out());
918 // Notice that we do not notify the state of this result. If we wanted to
919 // make the solver resume a working state after an interupt, then we would
920 // implement a different callback and use it here, e.g.
921 // d_state.notifyCheckSatInterupt.
922 Result::UnknownExplanation why
= getResourceManager()->outOfResources()
923 ? Result::RESOURCEOUT
926 if (d_env
->getOptions().base
.statisticsEveryQuery
)
928 printStatisticsDiff();
930 return Result(Result::SAT_UNKNOWN
, why
, d_env
->getOptions().driver
.filename
);
934 std::vector
<Node
> SmtEngine::getUnsatAssumptions(void)
936 Trace("smt") << "SMT getUnsatAssumptions()" << endl
;
938 if (!d_env
->getOptions().smt
.unsatAssumptions
)
940 throw ModalException(
941 "Cannot get unsat assumptions when produce-unsat-assumptions option "
944 if (d_state
->getMode() != SmtMode::UNSAT
)
946 throw RecoverableModalException(
947 "Cannot get unsat assumptions unless immediately preceded by "
951 if (Dump
.isOn("benchmark"))
953 getPrinter().toStreamCmdGetUnsatAssumptions(d_env
->getDumpOut());
955 UnsatCore core
= getUnsatCoreInternal();
956 std::vector
<Node
> res
;
957 std::vector
<Node
>& assumps
= d_asserts
->getAssumptions();
958 for (const Node
& e
: assumps
)
960 if (std::find(core
.begin(), core
.end(), e
) != core
.end())
968 Result
SmtEngine::assertFormula(const Node
& formula
)
972 d_state
->doPendingPops();
974 Trace("smt") << "SmtEngine::assertFormula(" << formula
<< ")" << endl
;
976 if (Dump
.isOn("raw-benchmark"))
978 getPrinter().toStreamCmdAssert(d_env
->getDumpOut(), formula
);
981 // Substitute out any abstract values in ex
982 Node n
= d_absValues
->substituteAbstractValues(formula
);
984 d_asserts
->assertFormula(n
);
985 return quickCheck().asEntailmentResult();
986 }/* SmtEngine::assertFormula() */
989 --------------------------------------------------------------------------
990 Handling SyGuS commands
991 --------------------------------------------------------------------------
994 void SmtEngine::declareSygusVar(Node var
)
997 d_sygusSolver
->declareSygusVar(var
);
998 if (Dump
.isOn("raw-benchmark"))
1000 getPrinter().toStreamCmdDeclareVar(d_env
->getDumpOut(), var
, var
.getType());
1002 // don't need to set that the conjecture is stale
1005 void SmtEngine::declareSynthFun(Node func
,
1008 const std::vector
<Node
>& vars
)
1010 SmtScope
smts(this);
1012 d_state
->doPendingPops();
1013 d_sygusSolver
->declareSynthFun(func
, sygusType
, isInv
, vars
);
1015 // !!! TEMPORARY: We cannot construct a SynthFunCommand since we cannot
1016 // construct a Term-level Grammar from a Node-level sygus TypeNode. Thus we
1017 // must print the command using the Node-level utility method for now.
1019 if (Dump
.isOn("raw-benchmark"))
1021 getPrinter().toStreamCmdSynthFun(
1022 d_env
->getDumpOut(), func
, vars
, isInv
, sygusType
);
1025 void SmtEngine::declareSynthFun(Node func
,
1027 const std::vector
<Node
>& vars
)
1029 // use a null sygus type
1031 declareSynthFun(func
, sygusType
, isInv
, vars
);
1034 void SmtEngine::assertSygusConstraint(Node constraint
)
1036 SmtScope
smts(this);
1038 d_sygusSolver
->assertSygusConstraint(constraint
);
1039 if (Dump
.isOn("raw-benchmark"))
1041 getPrinter().toStreamCmdConstraint(d_env
->getDumpOut(), constraint
);
1045 void SmtEngine::assertSygusInvConstraint(Node inv
,
1050 SmtScope
smts(this);
1052 d_sygusSolver
->assertSygusInvConstraint(inv
, pre
, trans
, post
);
1053 if (Dump
.isOn("raw-benchmark"))
1055 getPrinter().toStreamCmdInvConstraint(
1056 d_env
->getDumpOut(), inv
, pre
, trans
, post
);
1060 Result
SmtEngine::checkSynth()
1062 SmtScope
smts(this);
1064 return d_sygusSolver
->checkSynth(*d_asserts
);
1068 --------------------------------------------------------------------------
1069 End of Handling SyGuS commands
1070 --------------------------------------------------------------------------
1073 void SmtEngine::declarePool(const Node
& p
, const std::vector
<Node
>& initValue
)
1075 Assert(p
.isVar() && p
.getType().isSet());
1077 QuantifiersEngine
* qe
= getAvailableQuantifiersEngine("declareTermPool");
1078 qe
->declarePool(p
, initValue
);
1081 Node
SmtEngine::simplify(const Node
& ex
)
1083 SmtScope
smts(this);
1085 d_state
->doPendingPops();
1086 // ensure we've processed assertions
1087 d_smtSolver
->processAssertions(*d_asserts
);
1088 return d_pp
->simplify(ex
);
1091 Node
SmtEngine::expandDefinitions(const Node
& ex
)
1093 getResourceManager()->spendResource(Resource::PreprocessStep
);
1094 SmtScope
smts(this);
1096 d_state
->doPendingPops();
1097 return d_pp
->expandDefinitions(ex
);
1100 // TODO(#1108): Simplify the error reporting of this method.
1101 Node
SmtEngine::getValue(const Node
& ex
) const
1103 SmtScope
smts(this);
1105 Trace("smt") << "SMT getValue(" << ex
<< ")" << endl
;
1106 if (Dump
.isOn("benchmark"))
1108 getPrinter().toStreamCmdGetValue(d_env
->getDumpOut(), {ex
});
1110 TypeNode expectedType
= ex
.getType();
1112 // Substitute out any abstract values in ex and expand
1113 Node n
= d_pp
->expandDefinitions(ex
);
1115 Trace("smt") << "--- getting value of " << n
<< endl
;
1116 // There are two ways model values for terms are computed (for historical
1117 // reasons). One way is that used in check-model; the other is that
1118 // used by the Model classes. It's not clear to me exactly how these
1119 // two are different, but they need to be unified. This ugly hack here
1120 // is to fix bug 554 until we can revamp boolean-terms and models [MGD]
1123 if(!n
.getType().isFunction()) {
1124 n
= Rewriter::rewrite(n
);
1127 Trace("smt") << "--- getting value of " << n
<< endl
;
1128 TheoryModel
* m
= getAvailableModel("get-value");
1129 Assert(m
!= nullptr);
1130 Node resultNode
= m
->getValue(n
);
1131 Trace("smt") << "--- got value " << n
<< " = " << resultNode
<< endl
;
1132 Trace("smt") << "--- type " << resultNode
.getType() << endl
;
1133 Trace("smt") << "--- expected type " << expectedType
<< endl
;
1135 // type-check the result we got
1136 // Notice that lambdas have function type, which does not respect the subtype
1137 // relation, so we ignore them here.
1138 Assert(resultNode
.isNull() || resultNode
.getKind() == kind::LAMBDA
1139 || resultNode
.getType().isSubtypeOf(expectedType
))
1140 << "Run with -t smt for details.";
1142 // Ensure it's a constant, or a lambda (for uninterpreted functions). This
1143 // assertion only holds for models that do not have approximate values.
1144 Assert(m
->hasApproximations() || resultNode
.getKind() == kind::LAMBDA
1145 || resultNode
.isConst());
1147 if (d_env
->getOptions().smt
.abstractValues
1148 && resultNode
.getType().isArray())
1150 resultNode
= d_absValues
->mkAbstractValue(resultNode
);
1151 Trace("smt") << "--- abstract value >> " << resultNode
<< endl
;
1157 std::vector
<Node
> SmtEngine::getValues(const std::vector
<Node
>& exprs
) const
1159 std::vector
<Node
> result
;
1160 for (const Node
& e
: exprs
)
1162 result
.push_back(getValue(e
));
1167 std::vector
<Node
> SmtEngine::getModelDomainElements(TypeNode tn
) const
1169 Assert(tn
.isSort());
1170 TheoryModel
* m
= getAvailableModel("getModelDomainElements");
1171 return m
->getDomainElements(tn
);
1174 bool SmtEngine::isModelCoreSymbol(Node n
)
1176 SmtScope
smts(this);
1178 const Options
& opts
= d_env
->getOptions();
1179 if (opts
.smt
.modelCoresMode
== options::ModelCoresMode::NONE
)
1181 // if the model core mode is none, we are always a model core symbol
1184 TheoryModel
* tm
= getAvailableModel("isModelCoreSymbol");
1185 // compute the model core if not done so already
1186 if (!tm
->isUsingModelCore())
1188 // If we enabled model cores, we compute a model core for m based on our
1189 // (expanded) assertions using the model core builder utility. Notice that
1190 // we get the assertions using the getAssertionsInternal, which does not
1191 // impact whether we are in "sat" mode
1192 std::vector
<Node
> asserts
= getAssertionsInternal();
1193 d_pp
->expandDefinitions(asserts
);
1194 ModelCoreBuilder::setModelCore(asserts
, tm
, opts
.smt
.modelCoresMode
);
1196 return tm
->isModelCoreSymbol(n
);
1199 std::string
SmtEngine::getModel(const std::vector
<TypeNode
>& declaredSorts
,
1200 const std::vector
<Node
>& declaredFuns
)
1202 SmtScope
smts(this);
1203 // !!! Note that all methods called here should have a version at the API
1204 // level. This is to ensure that the information associated with a model is
1205 // completely accessible by the user. This is currently not rigorously
1206 // enforced. An alternative design would be to have this method implemented
1207 // at the API level, but this makes exceptions in the text interface less
1208 // intuitive and makes it impossible to implement raw-benchmark at the
1210 if (Dump
.isOn("raw-benchmark"))
1212 getPrinter().toStreamCmdGetModel(d_env
->getDumpOut());
1214 TheoryModel
* tm
= getAvailableModel("get model");
1215 // use the smt::Model model utility for printing
1216 const Options
& opts
= d_env
->getOptions();
1217 bool isKnownSat
= (d_state
->getMode() == SmtMode::SAT
);
1218 Model
m(isKnownSat
, opts
.driver
.filename
);
1219 // set the model declarations, which determines what is printed in the model
1220 for (const TypeNode
& tn
: declaredSorts
)
1222 m
.addDeclarationSort(tn
, getModelDomainElements(tn
));
1224 bool usingModelCores
=
1225 (opts
.smt
.modelCoresMode
!= options::ModelCoresMode::NONE
);
1226 for (const Node
& n
: declaredFuns
)
1228 if (usingModelCores
&& !tm
->isModelCoreSymbol(n
))
1230 // skip if not in model core
1233 Node value
= tm
->getValue(n
);
1234 m
.addDeclarationTerm(n
, value
);
1236 // for separation logic
1237 TypeNode locT
, dataT
;
1238 if (getSepHeapTypes(locT
, dataT
))
1240 std::pair
<Node
, Node
> sh
= getSepHeapAndNilExpr();
1241 m
.setHeapModel(sh
.first
, sh
.second
);
1244 std::stringstream ssm
;
1249 Result
SmtEngine::blockModel()
1251 Trace("smt") << "SMT blockModel()" << endl
;
1252 SmtScope
smts(this);
1256 if (Dump
.isOn("benchmark"))
1258 getPrinter().toStreamCmdBlockModel(d_env
->getDumpOut());
1261 TheoryModel
* m
= getAvailableModel("block model");
1263 if (d_env
->getOptions().smt
.blockModelsMode
1264 == options::BlockModelsMode::NONE
)
1266 std::stringstream ss
;
1267 ss
<< "Cannot block model when block-models is set to none.";
1268 throw RecoverableModalException(ss
.str().c_str());
1271 // get expanded assertions
1272 std::vector
<Node
> eassertsProc
= getExpandedAssertions();
1273 Node eblocker
= ModelBlocker::getModelBlocker(
1274 eassertsProc
, m
, d_env
->getOptions().smt
.blockModelsMode
);
1275 Trace("smt") << "Block formula: " << eblocker
<< std::endl
;
1276 return assertFormula(eblocker
);
1279 Result
SmtEngine::blockModelValues(const std::vector
<Node
>& exprs
)
1281 Trace("smt") << "SMT blockModelValues()" << endl
;
1282 SmtScope
smts(this);
1286 if (Dump
.isOn("benchmark"))
1288 getPrinter().toStreamCmdBlockModelValues(d_env
->getDumpOut(), exprs
);
1291 TheoryModel
* m
= getAvailableModel("block model values");
1293 // get expanded assertions
1294 std::vector
<Node
> eassertsProc
= getExpandedAssertions();
1295 // we always do block model values mode here
1296 Node eblocker
= ModelBlocker::getModelBlocker(
1297 eassertsProc
, m
, options::BlockModelsMode::VALUES
, exprs
);
1298 return assertFormula(eblocker
);
1301 std::pair
<Node
, Node
> SmtEngine::getSepHeapAndNilExpr(void)
1303 if (!getLogicInfo().isTheoryEnabled(THEORY_SEP
))
1306 "Cannot obtain separation logic expressions if not using the "
1307 "separation logic theory.";
1308 throw RecoverableModalException(msg
);
1310 NodeManagerScope
nms(getNodeManager());
1313 TheoryModel
* tm
= getAvailableModel("get separation logic heap and nil");
1314 if (!tm
->getHeapModel(heap
, nil
))
1317 "Failed to obtain heap/nil "
1318 "expressions from theory model.";
1319 throw RecoverableModalException(msg
);
1321 return std::make_pair(heap
, nil
);
1324 std::vector
<Node
> SmtEngine::getAssertionsInternal()
1326 Assert(d_state
->isFullyInited());
1327 context::CDList
<Node
>* al
= d_asserts
->getAssertionList();
1328 Assert(al
!= nullptr);
1329 std::vector
<Node
> res
;
1330 for (const Node
& n
: *al
)
1332 res
.emplace_back(n
);
1337 std::vector
<Node
> SmtEngine::getExpandedAssertions()
1339 std::vector
<Node
> easserts
= getAssertions();
1340 // must expand definitions
1341 d_pp
->expandDefinitions(easserts
);
1344 Env
& SmtEngine::getEnv() { return *d_env
.get(); }
1346 void SmtEngine::declareSepHeap(TypeNode locT
, TypeNode dataT
)
1348 if (!getLogicInfo().isTheoryEnabled(THEORY_SEP
))
1351 "Cannot declare heap if not using the separation logic theory.";
1352 throw RecoverableModalException(msg
);
1354 SmtScope
smts(this);
1356 TheoryEngine
* te
= getTheoryEngine();
1357 te
->declareSepHeap(locT
, dataT
);
1360 bool SmtEngine::getSepHeapTypes(TypeNode
& locT
, TypeNode
& dataT
)
1362 SmtScope
smts(this);
1364 TheoryEngine
* te
= getTheoryEngine();
1365 return te
->getSepHeapTypes(locT
, dataT
);
1368 Node
SmtEngine::getSepHeapExpr() { return getSepHeapAndNilExpr().first
; }
1370 Node
SmtEngine::getSepNilExpr() { return getSepHeapAndNilExpr().second
; }
1372 void SmtEngine::checkProof()
1374 Assert(d_env
->getOptions().smt
.produceProofs
);
1375 // internal check the proof
1376 PropEngine
* pe
= getPropEngine();
1377 Assert(pe
!= nullptr);
1378 if (d_env
->getOptions().proof
.proofCheck
== options::ProofCheckMode::EAGER
)
1380 pe
->checkProof(d_asserts
->getAssertionList());
1382 Assert(pe
->getProof() != nullptr);
1383 std::shared_ptr
<ProofNode
> pePfn
= pe
->getProof();
1384 if (d_env
->getOptions().smt
.checkProofs
)
1386 d_pfManager
->checkProof(pePfn
, *d_asserts
);
1390 StatisticsRegistry
& SmtEngine::getStatisticsRegistry()
1392 return d_env
->getStatisticsRegistry();
1395 UnsatCore
SmtEngine::getUnsatCoreInternal()
1397 if (!d_env
->getOptions().smt
.unsatCores
)
1399 throw ModalException(
1400 "Cannot get an unsat core when produce-unsat-cores or produce-proofs "
1403 if (d_state
->getMode() != SmtMode::UNSAT
)
1405 throw RecoverableModalException(
1406 "Cannot get an unsat core unless immediately preceded by "
1407 "UNSAT/ENTAILED response.");
1409 // generate with new proofs
1410 PropEngine
* pe
= getPropEngine();
1411 Assert(pe
!= nullptr);
1413 std::shared_ptr
<ProofNode
> pepf
;
1414 if (options::unsatCoresMode() == options::UnsatCoresMode::ASSUMPTIONS
)
1416 pepf
= pe
->getRefutation();
1420 pepf
= pe
->getProof();
1422 Assert(pepf
!= nullptr);
1423 std::shared_ptr
<ProofNode
> pfn
= d_pfManager
->getFinalProof(pepf
, *d_asserts
);
1424 std::vector
<Node
> core
;
1425 d_ucManager
->getUnsatCore(pfn
, *d_asserts
, core
);
1426 if (options::minimalUnsatCores())
1428 core
= reduceUnsatCore(core
);
1430 return UnsatCore(core
);
1433 std::vector
<Node
> SmtEngine::reduceUnsatCore(const std::vector
<Node
>& core
)
1435 Assert(options::unsatCores())
1436 << "cannot reduce unsat core if unsat cores are turned off";
1438 Notice() << "SmtEngine::reduceUnsatCore(): reducing unsat core" << endl
;
1439 std::unordered_set
<Node
> removed
;
1440 for (const Node
& skip
: core
)
1442 std::unique_ptr
<SmtEngine
> coreChecker
;
1443 initializeSubsolver(coreChecker
, *d_env
.get());
1444 coreChecker
->setLogic(getLogicInfo());
1445 coreChecker
->getOptions().smt
.checkUnsatCores
= false;
1446 // disable all proof options
1447 coreChecker
->getOptions().smt
.produceProofs
= false;
1448 coreChecker
->getOptions().smt
.checkProofs
= false;
1450 for (const Node
& ucAssertion
: core
)
1452 if (ucAssertion
!= skip
&& removed
.find(ucAssertion
) == removed
.end())
1454 Node assertionAfterExpansion
= expandDefinitions(ucAssertion
);
1455 coreChecker
->assertFormula(assertionAfterExpansion
);
1461 r
= coreChecker
->checkSat();
1468 if (r
.asSatisfiabilityResult().isSat() == Result::UNSAT
)
1470 removed
.insert(skip
);
1472 else if (r
.asSatisfiabilityResult().isUnknown())
1474 Warning() << "SmtEngine::reduceUnsatCore(): could not reduce unsat core "
1480 if (removed
.empty())
1486 std::vector
<Node
> newUcAssertions
;
1487 for (const Node
& n
: core
)
1489 if (removed
.find(n
) == removed
.end())
1491 newUcAssertions
.push_back(n
);
1495 return newUcAssertions
;
1499 void SmtEngine::checkUnsatCore() {
1500 Assert(d_env
->getOptions().smt
.unsatCores
)
1501 << "cannot check unsat core if unsat cores are turned off";
1503 Notice() << "SmtEngine::checkUnsatCore(): generating unsat core" << endl
;
1504 UnsatCore core
= getUnsatCore();
1506 // initialize the core checker
1507 std::unique_ptr
<SmtEngine
> coreChecker
;
1508 initializeSubsolver(coreChecker
, *d_env
.get());
1509 coreChecker
->getOptions().smt
.checkUnsatCores
= false;
1510 // disable all proof options
1511 coreChecker
->getOptions().smt
.produceProofs
= false;
1512 coreChecker
->getOptions().smt
.checkProofs
= false;
1514 // set up separation logic heap if necessary
1515 TypeNode sepLocType
, sepDataType
;
1516 if (getSepHeapTypes(sepLocType
, sepDataType
))
1518 coreChecker
->declareSepHeap(sepLocType
, sepDataType
);
1521 Notice() << "SmtEngine::checkUnsatCore(): pushing core assertions"
1523 theory::TrustSubstitutionMap
& tls
= d_env
->getTopLevelSubstitutions();
1524 for(UnsatCore::iterator i
= core
.begin(); i
!= core
.end(); ++i
) {
1525 Node assertionAfterExpansion
= tls
.apply(*i
, false);
1526 Notice() << "SmtEngine::checkUnsatCore(): pushing core member " << *i
1527 << ", expanded to " << assertionAfterExpansion
<< "\n";
1528 coreChecker
->assertFormula(assertionAfterExpansion
);
1532 r
= coreChecker
->checkSat();
1536 Notice() << "SmtEngine::checkUnsatCore(): result is " << r
<< endl
;
1537 if(r
.asSatisfiabilityResult().isUnknown()) {
1539 << "SmtEngine::checkUnsatCore(): could not check core result unknown."
1542 else if (r
.asSatisfiabilityResult().isSat())
1545 << "SmtEngine::checkUnsatCore(): produced core was satisfiable.";
1549 void SmtEngine::checkModel(bool hardFailure
) {
1550 context::CDList
<Node
>* al
= d_asserts
->getAssertionList();
1551 // --check-model implies --produce-assertions, which enables the
1552 // assertion list, so we should be ok.
1553 Assert(al
!= nullptr)
1554 << "don't have an assertion list to check in SmtEngine::checkModel()";
1556 TimerStat::CodeTimer
checkModelTimer(d_stats
->d_checkModelTime
);
1558 Notice() << "SmtEngine::checkModel(): generating model" << endl
;
1559 TheoryModel
* m
= getAvailableModel("check model");
1560 Assert(m
!= nullptr);
1562 // check the model with the theory engine for debugging
1563 if (options::debugCheckModels())
1565 TheoryEngine
* te
= getTheoryEngine();
1566 Assert(te
!= nullptr);
1567 te
->checkTheoryAssertionsWithModel(hardFailure
);
1570 // check the model with the check models utility
1571 Assert(d_checkModels
!= nullptr);
1572 d_checkModels
->checkModel(m
, al
, hardFailure
);
1575 UnsatCore
SmtEngine::getUnsatCore() {
1576 Trace("smt") << "SMT getUnsatCore()" << std::endl
;
1577 SmtScope
smts(this);
1579 if (Dump
.isOn("benchmark"))
1581 getPrinter().toStreamCmdGetUnsatCore(d_env
->getDumpOut());
1583 return getUnsatCoreInternal();
1586 void SmtEngine::getRelevantInstantiationTermVectors(
1587 std::map
<Node
, InstantiationList
>& insts
, bool getDebugInfo
)
1589 Assert(d_state
->getMode() == SmtMode::UNSAT
);
1590 // generate with new proofs
1591 PropEngine
* pe
= getPropEngine();
1592 Assert(pe
!= nullptr);
1593 Assert(pe
->getProof() != nullptr);
1594 std::shared_ptr
<ProofNode
> pfn
=
1595 d_pfManager
->getFinalProof(pe
->getProof(), *d_asserts
);
1596 d_ucManager
->getRelevantInstantiations(pfn
, insts
, getDebugInfo
);
1599 std::string
SmtEngine::getProof()
1601 Trace("smt") << "SMT getProof()\n";
1602 SmtScope
smts(this);
1604 if (Dump
.isOn("benchmark"))
1606 getPrinter().toStreamCmdGetProof(d_env
->getDumpOut());
1608 if (!d_env
->getOptions().smt
.produceProofs
)
1610 throw ModalException("Cannot get a proof when proof option is off.");
1612 if (d_state
->getMode() != SmtMode::UNSAT
)
1614 throw RecoverableModalException(
1615 "Cannot get a proof unless immediately preceded by "
1616 "UNSAT/ENTAILED response.");
1618 // the prop engine has the proof of false
1619 PropEngine
* pe
= getPropEngine();
1620 Assert(pe
!= nullptr);
1621 Assert(pe
->getProof() != nullptr);
1622 Assert(d_pfManager
);
1623 std::ostringstream ss
;
1624 d_pfManager
->printProof(ss
, pe
->getProof(), *d_asserts
);
1628 void SmtEngine::printInstantiations( std::ostream
& out
) {
1629 SmtScope
smts(this);
1631 QuantifiersEngine
* qe
= getAvailableQuantifiersEngine("printInstantiations");
1633 // First, extract and print the skolemizations
1634 bool printed
= false;
1635 bool reqNames
= !d_env
->getOptions().printer
.printInstFull
;
1636 // only print when in list mode
1637 if (d_env
->getOptions().printer
.printInstMode
== options::PrintInstMode::LIST
)
1639 std::map
<Node
, std::vector
<Node
>> sks
;
1640 qe
->getSkolemTermVectors(sks
);
1641 for (const std::pair
<const Node
, std::vector
<Node
>>& s
: sks
)
1644 if (!qe
->getNameForQuant(s
.first
, name
, reqNames
))
1646 // did not have a name and we are only printing formulas with names
1649 SkolemList
slist(name
, s
.second
);
1655 // Second, extract and print the instantiations
1656 std::map
<Node
, InstantiationList
> rinsts
;
1657 if (d_env
->getOptions().smt
.produceProofs
1658 && (!d_env
->getOptions().smt
.unsatCores
1659 || d_env
->getOptions().smt
.unsatCoresMode
1660 == options::UnsatCoresMode::FULL_PROOF
)
1661 && getSmtMode() == SmtMode::UNSAT
)
1663 // minimize instantiations based on proof manager
1664 getRelevantInstantiationTermVectors(rinsts
,
1665 options::dumpInstantiationsDebug());
1669 std::map
<Node
, std::vector
<std::vector
<Node
>>> insts
;
1670 getInstantiationTermVectors(insts
);
1671 for (const std::pair
<const Node
, std::vector
<std::vector
<Node
>>>& i
: insts
)
1673 // convert to instantiation list
1675 InstantiationList
& ilq
= rinsts
[q
];
1677 for (const std::vector
<Node
>& ii
: i
.second
)
1679 ilq
.d_inst
.push_back(InstantiationVec(ii
));
1683 for (std::pair
<const Node
, InstantiationList
>& i
: rinsts
)
1685 if (i
.second
.d_inst
.empty())
1687 // no instantiations, skip
1691 if (!qe
->getNameForQuant(i
.first
, name
, reqNames
))
1693 // did not have a name and we are only printing formulas with names
1697 if (d_env
->getOptions().printer
.printInstMode
== options::PrintInstMode::NUM
)
1699 out
<< "(num-instantiations " << name
<< " " << i
.second
.d_inst
.size()
1700 << ")" << std::endl
;
1705 i
.second
.d_quant
= name
;
1706 Assert(d_env
->getOptions().printer
.printInstMode
1707 == options::PrintInstMode::LIST
);
1712 // if we did not print anything, we indicate this
1715 out
<< "none" << std::endl
;
1719 void SmtEngine::getInstantiationTermVectors(
1720 std::map
<Node
, std::vector
<std::vector
<Node
>>>& insts
)
1722 SmtScope
smts(this);
1724 QuantifiersEngine
* qe
=
1725 getAvailableQuantifiersEngine("getInstantiationTermVectors");
1726 // get the list of all instantiations
1727 qe
->getInstantiationTermVectors(insts
);
1730 bool SmtEngine::getSynthSolutions(std::map
<Node
, Node
>& solMap
)
1732 SmtScope
smts(this);
1734 return d_sygusSolver
->getSynthSolutions(solMap
);
1737 Node
SmtEngine::getQuantifierElimination(Node q
, bool doFull
, bool strict
)
1739 SmtScope
smts(this);
1741 const LogicInfo
& logic
= getLogicInfo();
1742 if (!logic
.isPure(THEORY_ARITH
) && strict
)
1744 Warning() << "Unexpected logic for quantifier elimination " << logic
1747 return d_quantElimSolver
->getQuantifierElimination(
1748 *d_asserts
, q
, doFull
, d_isInternalSubsolver
);
1751 bool SmtEngine::getInterpol(const Node
& conj
,
1752 const TypeNode
& grammarType
,
1755 SmtScope
smts(this);
1757 std::vector
<Node
> axioms
= getExpandedAssertions();
1759 d_interpolSolver
->getInterpol(axioms
, conj
, grammarType
, interpol
);
1760 // notify the state of whether the get-interpol call was successfuly, which
1761 // impacts the SMT mode.
1762 d_state
->notifyGetInterpol(success
);
1766 bool SmtEngine::getInterpol(const Node
& conj
, Node
& interpol
)
1768 TypeNode grammarType
;
1769 return getInterpol(conj
, grammarType
, interpol
);
1772 bool SmtEngine::getAbduct(const Node
& conj
,
1773 const TypeNode
& grammarType
,
1776 SmtScope
smts(this);
1778 std::vector
<Node
> axioms
= getExpandedAssertions();
1779 bool success
= d_abductSolver
->getAbduct(axioms
, conj
, grammarType
, abd
);
1780 // notify the state of whether the get-abduct call was successfuly, which
1781 // impacts the SMT mode.
1782 d_state
->notifyGetAbduct(success
);
1786 bool SmtEngine::getAbduct(const Node
& conj
, Node
& abd
)
1788 TypeNode grammarType
;
1789 return getAbduct(conj
, grammarType
, abd
);
1792 void SmtEngine::getInstantiatedQuantifiedFormulas(std::vector
<Node
>& qs
)
1794 SmtScope
smts(this);
1795 QuantifiersEngine
* qe
=
1796 getAvailableQuantifiersEngine("getInstantiatedQuantifiedFormulas");
1797 qe
->getInstantiatedQuantifiedFormulas(qs
);
1800 void SmtEngine::getInstantiationTermVectors(
1801 Node q
, std::vector
<std::vector
<Node
>>& tvecs
)
1803 SmtScope
smts(this);
1804 QuantifiersEngine
* qe
=
1805 getAvailableQuantifiersEngine("getInstantiationTermVectors");
1806 qe
->getInstantiationTermVectors(q
, tvecs
);
1809 std::vector
<Node
> SmtEngine::getAssertions()
1811 SmtScope
smts(this);
1813 d_state
->doPendingPops();
1814 if (Dump
.isOn("benchmark"))
1816 getPrinter().toStreamCmdGetAssertions(d_env
->getDumpOut());
1818 Trace("smt") << "SMT getAssertions()" << endl
;
1819 if (!d_env
->getOptions().smt
.produceAssertions
)
1822 "Cannot query the current assertion list when not in produce-assertions mode.";
1823 throw ModalException(msg
);
1825 return getAssertionsInternal();
1828 void SmtEngine::push()
1830 SmtScope
smts(this);
1832 d_state
->doPendingPops();
1833 Trace("smt") << "SMT push()" << endl
;
1834 d_smtSolver
->processAssertions(*d_asserts
);
1835 if(Dump
.isOn("benchmark")) {
1836 getPrinter().toStreamCmdPush(d_env
->getDumpOut());
1838 d_state
->userPush();
1841 void SmtEngine::pop() {
1842 SmtScope
smts(this);
1844 Trace("smt") << "SMT pop()" << endl
;
1845 if (Dump
.isOn("benchmark"))
1847 getPrinter().toStreamCmdPop(d_env
->getDumpOut());
1851 // Clear out assertion queues etc., in case anything is still in there
1852 d_asserts
->clearCurrent();
1853 // clear the learned literals from the preprocessor
1854 d_pp
->clearLearnedLiterals();
1856 Trace("userpushpop") << "SmtEngine: popped to level "
1857 << getUserContext()->getLevel() << endl
;
1858 // should we reset d_status here?
1859 // SMT-LIBv2 spec seems to imply no, but it would make sense to..
1862 void SmtEngine::resetAssertions()
1864 SmtScope
smts(this);
1866 if (!d_state
->isFullyInited())
1868 // We're still in Start Mode, nothing asserted yet, do nothing.
1869 // (see solver execution modes in the SMT-LIB standard)
1870 Assert(getContext()->getLevel() == 0);
1871 Assert(getUserContext()->getLevel() == 0);
1872 getDumpManager()->resetAssertions();
1877 Trace("smt") << "SMT resetAssertions()" << endl
;
1878 if (Dump
.isOn("benchmark"))
1880 getPrinter().toStreamCmdResetAssertions(d_env
->getDumpOut());
1883 d_asserts
->clearCurrent();
1884 d_state
->notifyResetAssertions();
1885 getDumpManager()->resetAssertions();
1886 // push the state to maintain global context around everything
1889 // reset SmtSolver, which will construct a new prop engine
1890 d_smtSolver
->resetAssertions();
1893 void SmtEngine::interrupt()
1895 if (!d_state
->isFullyInited())
1899 d_smtSolver
->interrupt();
1902 void SmtEngine::setResourceLimit(uint64_t units
, bool cumulative
)
1906 d_env
->d_options
.base
.cumulativeResourceLimit
= units
;
1910 d_env
->d_options
.base
.perCallResourceLimit
= units
;
1913 void SmtEngine::setTimeLimit(uint64_t millis
)
1915 d_env
->d_options
.base
.perCallMillisecondLimit
= millis
;
1918 unsigned long SmtEngine::getResourceUsage() const
1920 return getResourceManager()->getResourceUsage();
1923 unsigned long SmtEngine::getTimeUsage() const
1925 return getResourceManager()->getTimeUsage();
1928 unsigned long SmtEngine::getResourceRemaining() const
1930 return getResourceManager()->getResourceRemaining();
1933 NodeManager
* SmtEngine::getNodeManager() const
1935 return d_env
->getNodeManager();
1938 void SmtEngine::printStatisticsSafe(int fd
) const
1940 d_env
->getStatisticsRegistry().printSafe(fd
);
1943 void SmtEngine::printStatisticsDiff() const
1945 d_env
->getStatisticsRegistry().printDiff(*d_env
->getOptions().base
.err
);
1946 d_env
->getStatisticsRegistry().storeSnapshot();
1949 void SmtEngine::setOption(const std::string
& key
, const std::string
& value
)
1951 NodeManagerScope
nms(getNodeManager());
1952 Trace("smt") << "SMT setOption(" << key
<< ", " << value
<< ")" << endl
;
1954 if (Dump
.isOn("benchmark"))
1956 getPrinter().toStreamCmdSetOption(d_env
->getDumpOut(), key
, value
);
1959 if (key
== "command-verbosity")
1961 size_t fstIndex
= value
.find(" ");
1962 size_t sndIndex
= value
.find(" ", fstIndex
+ 1);
1963 if (sndIndex
== std::string::npos
)
1965 string c
= value
.substr(1, fstIndex
- 1);
1967 std::stoi(value
.substr(fstIndex
+ 1, value
.length() - fstIndex
- 1));
1970 throw OptionException("command-verbosity must be 0, 1, or 2");
1972 d_commandVerbosity
[c
] = v
;
1975 throw OptionException(
1976 "command-verbosity value must be a tuple (command-name integer)");
1979 if (value
.find(" ") != std::string::npos
)
1981 throw OptionException("bad value for :" + key
);
1984 std::string optionarg
= value
;
1985 options::set(getOptions(), key
, optionarg
);
1988 void SmtEngine::setIsInternalSubsolver() { d_isInternalSubsolver
= true; }
1990 bool SmtEngine::isInternalSubsolver() const { return d_isInternalSubsolver
; }
1992 std::string
SmtEngine::getOption(const std::string
& key
) const
1994 NodeManagerScope
nms(getNodeManager());
1995 NodeManager
* nm
= d_env
->getNodeManager();
1997 Trace("smt") << "SMT getOption(" << key
<< ")" << endl
;
1999 if (key
.find("command-verbosity:") == 0)
2001 auto it
= d_commandVerbosity
.find(key
.substr(std::strlen("command-verbosity:")));
2002 if (it
!= d_commandVerbosity
.end())
2004 return std::to_string(it
->second
);
2006 it
= d_commandVerbosity
.find("*");
2007 if (it
!= d_commandVerbosity
.end())
2009 return std::to_string(it
->second
);
2014 if (Dump
.isOn("benchmark"))
2016 getPrinter().toStreamCmdGetOption(d_env
->getDumpOut(), key
);
2019 if (key
== "command-verbosity")
2021 vector
<Node
> result
;
2022 Node defaultVerbosity
;
2023 for (const auto& verb
: d_commandVerbosity
)
2025 // treat the command name as a variable name as opposed to a string
2026 // constant to avoid printing double quotes around the name
2027 Node name
= nm
->mkBoundVar(verb
.first
, nm
->integerType());
2028 Node value
= nm
->mkConst(Rational(verb
.second
));
2029 if (verb
.first
== "*")
2031 // put the default at the end of the SExpr
2032 defaultVerbosity
= nm
->mkNode(Kind::SEXPR
, name
, value
);
2036 result
.push_back(nm
->mkNode(Kind::SEXPR
, name
, value
));
2039 // ensure the default is always listed
2040 if (defaultVerbosity
.isNull())
2042 defaultVerbosity
= nm
->mkNode(Kind::SEXPR
,
2043 nm
->mkBoundVar("*", nm
->integerType()),
2044 nm
->mkConst(Rational(2)));
2046 result
.push_back(defaultVerbosity
);
2047 return nm
->mkNode(Kind::SEXPR
, result
).toString();
2050 return options::get(getOptions(), key
);
2053 Options
& SmtEngine::getOptions() { return d_env
->d_options
; }
2055 const Options
& SmtEngine::getOptions() const { return d_env
->getOptions(); }
2057 ResourceManager
* SmtEngine::getResourceManager() const
2059 return d_env
->getResourceManager();
2062 DumpManager
* SmtEngine::getDumpManager() { return d_env
->getDumpManager(); }
2064 const Printer
& SmtEngine::getPrinter() const { return d_env
->getPrinter(); }
2066 OutputManager
& SmtEngine::getOutputManager() { return d_outMgr
; }
2068 theory::Rewriter
* SmtEngine::getRewriter() { return d_env
->getRewriter(); }