1 /********************* */
2 /*! \file smt_engine.cpp
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Morgan Deters, Aina Niemetz
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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.\endverbatim
12 ** \brief The main entry point into the CVC4 library's SMT interface
14 ** The main entry point into the CVC4 library's SMT interface.
17 #include "smt/smt_engine.h"
27 #include <unordered_map>
28 #include <unordered_set>
32 #include "api/cvc4cpp.h"
33 #include "base/check.h"
34 #include "base/configuration.h"
35 #include "base/configuration_private.h"
36 #include "base/exception.h"
37 #include "base/modal_exception.h"
38 #include "base/output.h"
39 #include "context/cdhashmap.h"
40 #include "context/cdhashset.h"
41 #include "context/cdlist.h"
42 #include "context/context.h"
43 #include "decision/decision_engine.h"
44 #include "expr/attribute.h"
45 #include "expr/expr.h"
46 #include "expr/kind.h"
47 #include "expr/metakind.h"
48 #include "expr/node.h"
49 #include "expr/node_algorithm.h"
50 #include "expr/node_builder.h"
51 #include "expr/node_self_iterator.h"
52 #include "expr/node_visitor.h"
53 #include "options/arith_options.h"
54 #include "options/arrays_options.h"
55 #include "options/base_options.h"
56 #include "options/booleans_options.h"
57 #include "options/bv_options.h"
58 #include "options/datatypes_options.h"
59 #include "options/decision_options.h"
60 #include "options/language.h"
61 #include "options/main_options.h"
62 #include "options/open_ostream.h"
63 #include "options/option_exception.h"
64 #include "options/printer_options.h"
65 #include "options/proof_options.h"
66 #include "options/prop_options.h"
67 #include "options/quantifiers_options.h"
68 #include "options/sep_options.h"
69 #include "options/set_language.h"
70 #include "options/smt_options.h"
71 #include "options/strings_options.h"
72 #include "options/theory_options.h"
73 #include "options/uf_options.h"
74 #include "preprocessing/preprocessing_pass.h"
75 #include "preprocessing/preprocessing_pass_context.h"
76 #include "preprocessing/preprocessing_pass_registry.h"
77 #include "printer/printer.h"
78 #include "proof/proof.h"
79 #include "proof/proof_manager.h"
80 #include "proof/theory_proof.h"
81 #include "proof/unsat_core.h"
82 #include "prop/prop_engine.h"
83 #include "smt/abduction_solver.h"
84 #include "smt/abstract_values.h"
85 #include "smt/expr_names.h"
86 #include "smt/command.h"
87 #include "smt/defined_function.h"
88 #include "smt/dump_manager.h"
89 #include "smt/listeners.h"
90 #include "smt/logic_request.h"
91 #include "smt/model_blocker.h"
92 #include "smt/model_core_builder.h"
93 #include "smt/options_manager.h"
94 #include "smt/process_assertions.h"
95 #include "smt/smt_engine_scope.h"
96 #include "smt/smt_engine_stats.h"
97 #include "smt/term_formula_removal.h"
98 #include "smt/update_ostream.h"
99 #include "smt_util/boolean_simplification.h"
100 #include "smt_util/nary_builder.h"
101 #include "theory/booleans/circuit_propagator.h"
102 #include "theory/bv/theory_bv_rewriter.h"
103 #include "theory/logic_info.h"
104 #include "theory/quantifiers/fun_def_process.h"
105 #include "theory/quantifiers/single_inv_partition.h"
106 #include "theory/quantifiers/sygus/synth_engine.h"
107 #include "theory/quantifiers/term_util.h"
108 #include "theory/quantifiers_engine.h"
109 #include "theory/rewriter.h"
110 #include "theory/sort_inference.h"
111 #include "theory/strings/theory_strings.h"
112 #include "theory/substitutions.h"
113 #include "theory/theory_engine.h"
114 #include "theory/theory_model.h"
115 #include "theory/theory_traits.h"
116 #include "util/hash.h"
117 #include "util/proof.h"
118 #include "util/random.h"
119 #include "util/resource_manager.h"
121 #if (IS_LFSC_BUILD && IS_PROOFS_BUILD)
126 using namespace CVC4
;
127 using namespace CVC4::smt
;
128 using namespace CVC4::preprocessing
;
129 using namespace CVC4::prop
;
130 using namespace CVC4::context
;
131 using namespace CVC4::theory
;
136 extern const char* const plf_signatures
;
142 * This is an inelegant solution, but for the present, it will work.
143 * The point of this is to separate the public and private portions of
144 * the SmtEngine class, so that smt_engine.h doesn't
145 * include "expr/node.h", which is a private CVC4 header (and can lead
146 * to linking errors due to the improper inlining of non-visible symbols
149 * The "real" solution (that which is usually implemented) is to move
150 * ALL the implementation to SmtEnginePrivate and maintain a
151 * heap-allocated instance of it in SmtEngine. SmtEngine (the public
152 * one) becomes an "interface shell" which simply acts as a forwarder
155 class SmtEnginePrivate
159 typedef unordered_map
<Node
, Node
, NodeHashFunction
> NodeToNodeHashMap
;
160 typedef unordered_map
<Node
, bool, NodeHashFunction
> NodeToBoolHashMap
;
162 /** A circuit propagator for non-clausal propositional deduction */
163 booleans::CircuitPropagator d_propagator
;
165 /** Assertions in the preprocessing pipeline */
166 AssertionPipeline d_assertions
;
168 /** Whether any assertions have been processed */
169 CDO
<bool> d_assertionsProcessed
;
174 /** The preprocessing pass context */
175 std::unique_ptr
<PreprocessingPassContext
> d_preprocessingPassContext
;
177 /** Process assertions module */
178 ProcessAssertions d_processor
;
181 IteSkolemMap
& getIteSkolemMap() { return d_assertions
.getIteSkolemMap(); }
183 /** Instance of the ITE remover */
184 RemoveTermFormulas d_iteRemover
;
186 /* Finishes the initialization of the private portion of SMTEngine. */
189 /*------------------- sygus utils ------------------*/
191 * sygus variables declared (from "declare-var" and "declare-fun" commands)
193 * The SyGuS semantics for declared variables is that they are implicitly
194 * universally quantified in the constraints.
196 std::vector
<Node
> d_sygusVars
;
197 /** sygus constraints */
198 std::vector
<Node
> d_sygusConstraints
;
199 /** functions-to-synthesize */
200 std::vector
<Node
> d_sygusFunSymbols
;
202 * Whether we need to reconstruct the sygus conjecture.
204 CDO
<bool> d_sygusConjectureStale
;
205 /*------------------- end of sygus utils ------------------*/
208 SmtEnginePrivate(SmtEngine
& smt
)
210 d_propagator(true, true),
212 d_assertionsProcessed(smt
.getUserContext(), false),
213 d_processor(smt
, *smt
.getResourceManager()),
214 d_iteRemover(smt
.getUserContext()),
215 d_sygusConjectureStale(smt
.getUserContext(), true)
217 d_true
= NodeManager::currentNM()->mkConst(true);
222 if(d_propagator
.getNeedsFinish()) {
223 d_propagator
.finish();
224 d_propagator
.setNeedsFinish(false);
228 void spendResource(ResourceManager::Resource r
)
230 d_smt
.getResourceManager()->spendResource(r
);
233 ProcessAssertions
* getProcessAssertions() { return &d_processor
; }
235 Node
applySubstitutions(TNode node
)
237 return Rewriter::rewrite(
238 d_preprocessingPassContext
->getTopLevelSubstitutions().apply(node
));
242 * Process the assertions that have been asserted.
244 void processAssertions();
246 /** Process a user push.
253 * Process a user pop. Clears out the non-context-dependent stuff in this
254 * SmtEnginePrivate. Necessary to clear out our assertion vectors in case
255 * someone does a push-assert-pop without a check-sat. It also pops the
256 * last map of expression names from notifyPush.
259 d_assertions
.clear();
260 d_propagator
.getLearnedLiterals().clear();
261 getIteSkolemMap().clear();
265 * Adds a formula to the current context. Action here depends on
266 * the SimplificationMode (in the current Options scope); the
267 * formula might be pushed out to the propositional layer
268 * immediately, or it might be simplified and kept, or it might not
269 * even be simplified.
270 * The arguments isInput and isAssumption are used for bookkeeping for proofs.
271 * The argument maybeHasFv should be set to true if the assertion may have
272 * free variables. By construction, assertions from the smt2 parser are
273 * guaranteed not to have free variables. However, other cases such as
274 * assertions from the SyGuS parser may have free variables (say if the
275 * input contains an assert or define-fun-rec command).
277 * @param isAssumption If true, the formula is considered to be an assumption
278 * (this is used to distinguish assertions and assumptions)
280 void addFormula(TNode n
,
283 bool isAssumption
= false,
284 bool maybeHasFv
= false);
286 * Simplify node "in" by expanding definitions and applying any
287 * substitutions learned from preprocessing.
289 Node
simplify(TNode in
) {
290 // Substitute out any abstract values in ex.
291 // Expand definitions.
292 NodeToNodeHashMap cache
;
293 Node n
= d_processor
.expandDefinitions(in
, cache
).toExpr();
294 // Make sure we've done all preprocessing, etc.
295 Assert(d_assertions
.size() == 0);
296 return applySubstitutions(n
).toExpr();
298 };/* class SmtEnginePrivate */
300 }/* namespace CVC4::smt */
302 SmtEngine::SmtEngine(ExprManager
* em
, Options
* optr
)
303 : d_context(new Context()),
304 d_userContext(new UserContext()),
307 d_nodeManager(d_exprManager
->getNodeManager()),
308 d_absValues(new AbstractValues(d_nodeManager
)),
309 d_exprNames(new ExprNames(d_userContext
.get())),
310 d_dumpm(new DumpManager(d_userContext
.get())),
311 d_routListener(new ResourceOutListener(*this)),
312 d_snmListener(new SmtNodeManagerListener(*d_dumpm
.get())),
313 d_theoryEngine(nullptr),
314 d_propEngine(nullptr),
315 d_proofManager(nullptr),
316 d_rewriter(new theory::Rewriter()),
317 d_definedFunctions(nullptr),
318 d_abductSolver(nullptr),
319 d_assertionList(nullptr),
320 d_assignments(nullptr),
324 d_isInternalSubsolver(false),
326 d_fullyInited(false),
328 d_needPostsolve(false),
329 d_globalNegation(false),
332 d_smtMode(SMT_MODE_START
),
334 d_statisticsRegistry(nullptr),
336 d_resourceManager(nullptr),
339 // !!!!!!!!!!!!!!!!!!!!!! temporary hack: this makes the current SmtEngine
340 // we are constructing the current SmtEngine in scope for the lifetime of
341 // this SmtEngine, or until another SmtEngine is constructed (that SmtEngine
342 // is then in scope during its lifetime). This is mostly to ensure that
343 // options are always in scope, for e.g. printing expressions, which rely
344 // on knowing the output language.
345 // Notice that the SmtEngine may spawn new SmtEngine "subsolvers" internally.
346 // These are created, used, and deleted in a modular fashion while not
347 // interleaving calls to the master SmtEngine. Thus the hack here does not
348 // break this use case.
349 // On the other hand, this hack breaks use cases where multiple SmtEngine
350 // objects are created by the user.
351 d_scope
.reset(new SmtScope(this));
354 // if we provided a set of options, copy their values to the options
355 // owned by this SmtEngine.
356 d_options
.copyValues(*optr
);
358 d_statisticsRegistry
.reset(new StatisticsRegistry());
359 d_resourceManager
.reset(
360 new ResourceManager(*d_statisticsRegistry
.get(), d_options
));
361 d_optm
.reset(new smt::OptionsManager(&d_options
, d_resourceManager
.get()));
362 d_private
.reset(new smt::SmtEnginePrivate(*this));
363 // listen to node manager events
364 d_nodeManager
->subscribeEvents(d_snmListener
.get());
365 // listen to resource out
366 d_resourceManager
->registerListener(d_routListener
.get());
368 d_stats
.reset(new SmtEngineStatistics());
370 // The ProofManager is constructed before any other proof objects such as
371 // SatProof and TheoryProofs. The TheoryProofEngine and the SatProof are
372 // initialized in TheoryEngine and PropEngine respectively.
373 Assert(d_proofManager
== nullptr);
375 // d_proofManager must be created before Options has been finished
376 // being parsed from the input file. Because of this, we cannot trust
377 // that options::proof() is set correctly yet.
379 d_proofManager
.reset(new ProofManager(getUserContext()));
382 d_definedFunctions
= new (true) DefinedFunctionMap(getUserContext());
385 void SmtEngine::finishInit()
387 // Notice that finishInit is called when options are finalized. If we are
388 // parsing smt2, this occurs at the moment we enter "Assert mode", page 52
389 // of SMT-LIB 2.6 standard.
391 // set the random seed
392 Random::getRandom().setSeed(options::seed());
394 // Call finish init on the options manager. This inializes the resource
395 // manager based on the options, and sets up the best default options
396 // based on our heuristics.
397 d_optm
->finishInit(d_logic
, d_isInternalSubsolver
);
399 Trace("smt-debug") << "SmtEngine::finishInit" << std::endl
;
400 // We have mutual dependency here, so we add the prop engine to the theory
401 // engine later (it is non-essential there)
402 d_theoryEngine
.reset(new TheoryEngine(getContext(),
404 getResourceManager(),
405 d_private
->d_iteRemover
,
406 const_cast<const LogicInfo
&>(d_logic
)));
409 for(TheoryId id
= theory::THEORY_FIRST
; id
< theory::THEORY_LAST
; ++id
) {
410 TheoryConstructor::addTheory(getTheoryEngine(), id
);
411 //register with proof engine if applicable
413 ProofManager::currentPM()->getTheoryProofEngine()->registerTheory(d_theoryEngine
->theoryOf(id
));
417 Trace("smt-debug") << "Making decision engine..." << std::endl
;
419 Trace("smt-debug") << "Making prop engine..." << std::endl
;
420 /* force destruction of referenced PropEngine to enforce that statistics
421 * are unregistered by the obsolete PropEngine object before registered
422 * again by the new PropEngine object */
423 d_propEngine
.reset(nullptr);
424 d_propEngine
.reset(new PropEngine(
425 getTheoryEngine(), getContext(), getUserContext(), getResourceManager()));
427 Trace("smt-debug") << "Setting up theory engine..." << std::endl
;
428 d_theoryEngine
->setPropEngine(getPropEngine());
429 Trace("smt-debug") << "Finishing init for theory engine..." << std::endl
;
430 d_theoryEngine
->finishInit();
432 // global push/pop around everything, to ensure proper destruction
433 // of context-dependent data structures
434 d_userContext
->push();
437 Trace("smt-debug") << "Set up assertion list..." << std::endl
;
438 // [MGD 10/20/2011] keep around in incremental mode, due to a
439 // cleanup ordering issue and Nodes/TNodes. If SAT is popped
440 // first, some user-context-dependent TNodes might still exist
442 if(options::produceAssertions() ||
443 options::incrementalSolving()) {
444 // In the case of incremental solving, we appear to need these to
445 // ensure the relevant Nodes remain live.
446 d_assertionList
= new (true) AssertionList(getUserContext());
447 d_globalDefineFunRecLemmas
.reset(new std::vector
<Node
>());
450 // dump out a set-logic command only when raw-benchmark is disabled to avoid
451 // dumping the command twice.
452 if (Dump
.isOn("benchmark") && !Dump
.isOn("raw-benchmark"))
454 LogicInfo everything
;
456 Dump("benchmark") << CommentCommand(
457 "CVC4 always dumps the most general, all-supported logic (below), as "
458 "some internals might require the use of a logic more general than "
460 << SetBenchmarkLogicCommand(
461 everything
.getLogicString());
464 // initialize the dump manager
465 d_dumpm
->finishInit();
468 if (options::produceAbducts())
470 d_abductSolver
.reset(new AbductionSolver(this));
473 PROOF( ProofManager::currentPM()->setLogic(d_logic
); );
475 for(TheoryId id
= theory::THEORY_FIRST
; id
< theory::THEORY_LAST
; ++id
) {
476 ProofManager::currentPM()->getTheoryProofEngine()->
477 finishRegisterTheory(d_theoryEngine
->theoryOf(id
));
480 d_private
->finishInit();
481 Trace("smt-debug") << "SmtEngine::finishInit done" << std::endl
;
484 void SmtEngine::finalOptionsAreSet() {
489 if(! d_logic
.isLocked()) {
493 // finish initialization, create the prop engine, etc.
496 AlwaysAssert(d_propEngine
->getAssertionLevel() == 0)
497 << "The PropEngine has pushed but the SmtEngine "
498 "hasn't finished initializing!";
500 d_fullyInited
= true;
501 Assert(d_logic
.isLocked());
504 void SmtEngine::shutdown() {
507 while(options::incrementalSolving() && d_userContext
->getLevel() > 1) {
511 if (d_propEngine
!= nullptr)
513 d_propEngine
->shutdown();
515 if (d_theoryEngine
!= nullptr)
517 d_theoryEngine
->shutdown();
521 SmtEngine::~SmtEngine()
528 // global push/pop around everything, to ensure proper destruction
529 // of context-dependent data structures
531 d_userContext
->popto(0);
533 if(d_assignments
!= NULL
) {
534 d_assignments
->deleteSelf();
537 d_globalDefineFunRecLemmas
.reset();
539 if(d_assertionList
!= NULL
) {
540 d_assertionList
->deleteSelf();
543 d_definedFunctions
->deleteSelf();
545 //destroy all passes before destroying things that they refer to
546 d_private
->getProcessAssertions()->cleanup();
548 // d_proofManager is always created when proofs are enabled at configure
549 // time. Because of this, this code should not be wrapped in PROOF() which
550 // additionally checks flags such as options::proof().
552 // Note: the proof manager must be destroyed before the theory engine.
553 // Because the destruction of the proofs depends on contexts owned be the
556 d_proofManager
.reset(nullptr);
559 d_absValues
.reset(nullptr);
560 d_exprNames
.reset(nullptr);
561 d_dumpm
.reset(nullptr);
563 d_theoryEngine
.reset(nullptr);
564 d_propEngine
.reset(nullptr);
566 d_stats
.reset(nullptr);
567 d_private
.reset(nullptr);
568 d_nodeManager
->unsubscribeEvents(d_snmListener
.get());
569 d_snmListener
.reset(nullptr);
570 d_routListener
.reset(nullptr);
571 d_optm
.reset(nullptr);
572 // d_resourceManager must be destroyed before d_statisticsRegistry
573 d_resourceManager
.reset(nullptr);
574 d_statisticsRegistry
.reset(nullptr);
577 d_userContext
.reset(nullptr);
578 d_context
.reset(nullptr);
579 } catch(Exception
& e
) {
580 Warning() << "CVC4 threw an exception during cleanup." << endl
585 void SmtEngine::setLogic(const LogicInfo
& logic
)
589 throw ModalException("Cannot set logic in SmtEngine after the engine has "
590 "finished initializing.");
597 void SmtEngine::setLogic(const std::string
& s
)
602 setLogic(LogicInfo(s
));
603 // dump out a set-logic command
604 if (Dump
.isOn("raw-benchmark"))
606 Dump("raw-benchmark")
607 << SetBenchmarkLogicCommand(d_logic
.getLogicString());
610 catch (IllegalArgumentException
& e
)
612 throw LogicException(e
.what());
616 void SmtEngine::setLogic(const char* logic
) { setLogic(string(logic
)); }
617 LogicInfo
SmtEngine::getLogicInfo() const {
621 LogicInfo
SmtEngine::getUserLogicInfo() const
623 // Lock the logic to make sure that this logic can be queried. We create a
624 // copy of the user logic here to keep this method const.
625 LogicInfo res
= d_userLogic
;
630 void SmtEngine::notifyStartParsing(std::string filename
)
632 d_filename
= filename
;
634 // Copy the original options. This is called prior to beginning parsing.
635 // Hence reset should revert to these options, which note is after reading
637 d_originalOptions
.copyValues(d_options
);
640 std::string
SmtEngine::getFilename() const { return d_filename
; }
641 void SmtEngine::setLogicInternal()
643 Assert(!d_fullyInited
)
644 << "setting logic in SmtEngine but the engine has already"
645 " finished initializing for this run";
650 void SmtEngine::setProblemExtended()
652 d_smtMode
= SMT_MODE_ASSERT
;
653 d_assumptions
.clear();
656 void SmtEngine::setInfo(const std::string
& key
, const CVC4::SExpr
& value
)
660 Trace("smt") << "SMT setInfo(" << key
<< ", " << value
<< ")" << endl
;
662 if(Dump
.isOn("benchmark")) {
663 if(key
== "status") {
664 string s
= value
.getValue();
665 BenchmarkStatus status
=
666 (s
== "sat") ? SMT_SATISFIABLE
:
667 ((s
== "unsat") ? SMT_UNSATISFIABLE
: SMT_UNKNOWN
);
668 Dump("benchmark") << SetBenchmarkStatusCommand(status
);
670 Dump("benchmark") << SetInfoCommand(key
, value
);
674 // Check for standard info keys (SMT-LIB v1, SMT-LIB v2, ...)
675 if (key
== "source" || key
== "category" || key
== "difficulty"
676 || key
== "notes" || key
== "name" || key
== "license")
681 else if (key
== "filename")
683 d_filename
= value
.getValue();
686 else if (key
== "smt-lib-version" && !options::inputLanguage
.wasSetByUser())
688 language::input::Language ilang
= language::input::LANG_AUTO
;
689 if( (value
.isInteger() && value
.getIntegerValue() == Integer(2)) ||
690 (value
.isRational() && value
.getRationalValue() == Rational(2)) ||
691 value
.getValue() == "2" ||
692 value
.getValue() == "2.0" ) {
693 ilang
= language::input::LANG_SMTLIB_V2_0
;
694 } else if( (value
.isRational() && value
.getRationalValue() == Rational(5, 2)) ||
695 value
.getValue() == "2.5" ) {
696 ilang
= language::input::LANG_SMTLIB_V2_5
;
697 } else if( (value
.isRational() && value
.getRationalValue() == Rational(13, 5)) ||
698 value
.getValue() == "2.6" ) {
699 ilang
= language::input::LANG_SMTLIB_V2_6
;
703 Warning() << "Warning: unsupported smt-lib-version: " << value
<< endl
;
704 throw UnrecognizedOptionException();
706 options::inputLanguage
.set(ilang
);
707 // also update the output language
708 if (!options::outputLanguage
.wasSetByUser())
710 language::output::Language olang
= language::toOutputLanguage(ilang
);
711 if (options::outputLanguage() != olang
)
713 options::outputLanguage
.set(olang
);
714 *options::out() << language::SetLanguage(olang
);
718 } else if(key
== "status") {
721 s
= value
.getValue();
723 if(s
!= "sat" && s
!= "unsat" && s
!= "unknown") {
724 throw OptionException("argument to (set-info :status ..) must be "
725 "`sat' or `unsat' or `unknown'");
727 d_expectedStatus
= Result(s
, d_filename
);
730 throw UnrecognizedOptionException();
733 bool SmtEngine::isValidGetInfoFlag(const std::string
& key
) const
735 if (key
== "all-statistics" || key
== "error-behavior" || key
== "name"
736 || key
== "version" || key
== "authors" || key
== "status"
737 || key
== "reason-unknown" || key
== "assertion-stack-levels"
738 || key
== "all-options")
745 CVC4::SExpr
SmtEngine::getInfo(const std::string
& key
) const
749 Trace("smt") << "SMT getInfo(" << key
<< ")" << endl
;
750 if (!isValidGetInfoFlag(key
))
752 throw UnrecognizedOptionException();
754 if (key
== "all-statistics")
757 for (StatisticsRegistry::const_iterator i
=
758 NodeManager::fromExprManager(d_exprManager
)
759 ->getStatisticsRegistry()
762 != NodeManager::fromExprManager(d_exprManager
)
763 ->getStatisticsRegistry()
768 v
.push_back((*i
).first
);
769 v
.push_back((*i
).second
);
772 for (StatisticsRegistry::const_iterator i
= d_statisticsRegistry
->begin();
773 i
!= d_statisticsRegistry
->end();
777 v
.push_back((*i
).first
);
778 v
.push_back((*i
).second
);
783 if (key
== "error-behavior")
785 return SExpr(SExpr::Keyword("immediate-exit"));
789 return SExpr(Configuration::getName());
791 if (key
== "version")
793 return SExpr(Configuration::getVersionString());
795 if (key
== "authors")
797 return SExpr(Configuration::about());
801 // sat | unsat | unknown
802 switch (d_status
.asSatisfiabilityResult().isSat())
804 case Result::SAT
: return SExpr(SExpr::Keyword("sat"));
805 case Result::UNSAT
: return SExpr(SExpr::Keyword("unsat"));
806 default: return SExpr(SExpr::Keyword("unknown"));
809 if (key
== "reason-unknown")
811 if (!d_status
.isNull() && d_status
.isUnknown())
814 ss
<< d_status
.whyUnknown();
816 transform(s
.begin(), s
.end(), s
.begin(), ::tolower
);
817 return SExpr(SExpr::Keyword(s
));
821 throw RecoverableModalException(
822 "Can't get-info :reason-unknown when the "
823 "last result wasn't unknown!");
826 if (key
== "assertion-stack-levels")
828 AlwaysAssert(d_userLevels
.size()
829 <= std::numeric_limits
<unsigned long int>::max());
830 return SExpr(static_cast<unsigned long int>(d_userLevels
.size()));
832 Assert(key
== "all-options");
833 // get the options, like all-statistics
834 std::vector
<std::vector
<std::string
>> current_options
=
835 Options::current()->getOptions();
836 return SExpr::parseListOfListOfAtoms(current_options
);
839 void SmtEngine::debugCheckFormals(const std::vector
<Expr
>& formals
, Expr func
)
841 for(std::vector
<Expr
>::const_iterator i
= formals
.begin(); i
!= formals
.end(); ++i
) {
842 if((*i
).getKind() != kind::BOUND_VARIABLE
) {
844 ss
<< "All formal arguments to defined functions must be BOUND_VARIABLEs, but in the\n"
845 << "definition of function " << func
<< ", formal\n"
847 << "has kind " << (*i
).getKind();
848 throw TypeCheckingException(func
, ss
.str());
853 void SmtEngine::debugCheckFunctionBody(Expr formula
,
854 const std::vector
<Expr
>& formals
,
857 Type formulaType
= formula
.getType(options::typeChecking());
858 Type funcType
= func
.getType();
859 // We distinguish here between definitions of constants and functions,
860 // because the type checking for them is subtly different. Perhaps we
861 // should instead have SmtEngine::defineFunction() and
862 // SmtEngine::defineConstant() for better clarity, although then that
863 // doesn't match the SMT-LIBv2 standard...
864 if(formals
.size() > 0) {
865 Type rangeType
= FunctionType(funcType
).getRangeType();
866 if(! formulaType
.isComparableTo(rangeType
)) {
868 ss
<< "Type of defined function does not match its declaration\n"
869 << "The function : " << func
<< "\n"
870 << "Declared type : " << rangeType
<< "\n"
871 << "The body : " << formula
<< "\n"
872 << "Body type : " << formulaType
;
873 throw TypeCheckingException(func
, ss
.str());
876 if(! formulaType
.isComparableTo(funcType
)) {
878 ss
<< "Declared type of defined constant does not match its definition\n"
879 << "The constant : " << func
<< "\n"
880 << "Declared type : " << funcType
<< " " << Type::getTypeNode(funcType
)->getId() << "\n"
881 << "The definition : " << formula
<< "\n"
882 << "Definition type: " << formulaType
<< " " << Type::getTypeNode(formulaType
)->getId();
883 throw TypeCheckingException(func
, ss
.str());
888 void SmtEngine::defineFunction(Expr func
,
889 const std::vector
<Expr
>& formals
,
894 finalOptionsAreSet();
896 Trace("smt") << "SMT defineFunction(" << func
<< ")" << endl
;
897 debugCheckFormals(formals
, func
);
900 ss
<< language::SetLanguage(
901 language::SetLanguage::getLanguage(Dump
.getStream()))
903 DefineFunctionCommand
c(ss
.str(), func
, formals
, formula
, global
);
904 d_dumpm
->addToModelCommandAndDump(
905 c
, ExprManager::VAR_FLAG_DEFINED
, true, "declarations");
907 PROOF(if (options::checkUnsatCores()) {
908 d_defineCommands
.push_back(c
.clone());
912 debugCheckFunctionBody(formula
, formals
, func
);
914 // Substitute out any abstract values in formula
915 Node formNode
= d_absValues
->substituteAbstractValues(Node::fromExpr(formula
));
917 TNode funcNode
= func
.getTNode();
918 vector
<Node
> formalsNodes
;
919 for(vector
<Expr
>::const_iterator i
= formals
.begin(),
920 iend
= formals
.end();
923 formalsNodes
.push_back((*i
).getNode());
925 DefinedFunction
def(funcNode
, formalsNodes
, formNode
);
926 // Permit (check-sat) (define-fun ...) (get-value ...) sequences.
927 // Otherwise, (check-sat) (get-value ((! foo :named bar))) breaks
928 // d_haveAdditions = true;
929 Debug("smt") << "definedFunctions insert " << funcNode
<< " " << formNode
<< endl
;
933 d_definedFunctions
->insertAtContextLevelZero(funcNode
, def
);
937 d_definedFunctions
->insert(funcNode
, def
);
941 void SmtEngine::defineFunctionsRec(
942 const std::vector
<Expr
>& funcs
,
943 const std::vector
<std::vector
<Expr
>>& formals
,
944 const std::vector
<Expr
>& formulas
,
948 finalOptionsAreSet();
950 Trace("smt") << "SMT defineFunctionsRec(...)" << endl
;
952 if (funcs
.size() != formals
.size() && funcs
.size() != formulas
.size())
955 ss
<< "Number of functions, formals, and function bodies passed to "
956 "defineFunctionsRec do not match:"
958 << " #functions : " << funcs
.size() << "\n"
959 << " #arg lists : " << formals
.size() << "\n"
960 << " #function bodies : " << formulas
.size() << "\n";
961 throw ModalException(ss
.str());
963 for (unsigned i
= 0, size
= funcs
.size(); i
< size
; i
++)
965 // check formal argument list
966 debugCheckFormals(formals
[i
], funcs
[i
]);
968 debugCheckFunctionBody(formulas
[i
], formals
[i
], funcs
[i
]);
971 if (Dump
.isOn("raw-benchmark"))
973 std::vector
<api::Term
> tFuncs
= api::exprVectorToTerms(d_solver
, funcs
);
974 std::vector
<std::vector
<api::Term
>> tFormals
;
975 for (const std::vector
<Expr
>& formal
: formals
)
977 tFormals
.emplace_back(api::exprVectorToTerms(d_solver
, formal
));
979 std::vector
<api::Term
> tFormulas
=
980 api::exprVectorToTerms(d_solver
, formulas
);
981 Dump("raw-benchmark") << DefineFunctionRecCommand(
982 d_solver
, tFuncs
, tFormals
, tFormulas
, global
);
985 ExprManager
* em
= getExprManager();
986 bool maybeHasFv
= language::isInputLangSygus(options::inputLanguage());
987 for (unsigned i
= 0, size
= funcs
.size(); i
< size
; i
++)
989 // we assert a quantified formula
991 // make the function application
992 if (formals
[i
].empty())
994 // it has no arguments
999 std::vector
<Expr
> children
;
1000 children
.push_back(funcs
[i
]);
1001 children
.insert(children
.end(), formals
[i
].begin(), formals
[i
].end());
1002 func_app
= em
->mkExpr(kind::APPLY_UF
, children
);
1004 Expr lem
= em
->mkExpr(kind::EQUAL
, func_app
, formulas
[i
]);
1005 if (!formals
[i
].empty())
1007 // set the attribute to denote this is a function definition
1008 std::string
attr_name("fun-def");
1009 Expr aexpr
= em
->mkExpr(kind::INST_ATTRIBUTE
, func_app
);
1010 aexpr
= em
->mkExpr(kind::INST_PATTERN_LIST
, aexpr
);
1011 std::vector
<Expr
> expr_values
;
1012 std::string str_value
;
1013 setUserAttribute(attr_name
, func_app
, expr_values
, str_value
);
1014 // make the quantified formula
1015 Expr boundVars
= em
->mkExpr(kind::BOUND_VAR_LIST
, formals
[i
]);
1016 lem
= em
->mkExpr(kind::FORALL
, boundVars
, lem
, aexpr
);
1018 // assert the quantified formula
1019 // notice we don't call assertFormula directly, since this would
1020 // duplicate the output on raw-benchmark.
1021 Node n
= d_absValues
->substituteAbstractValues(Node::fromExpr(lem
));
1022 if (d_assertionList
!= nullptr)
1024 d_assertionList
->push_back(n
);
1026 if (global
&& d_globalDefineFunRecLemmas
!= nullptr)
1028 // Global definitions are asserted at check-sat-time because we have to
1029 // make sure that they are always present
1030 Assert(!language::isInputLangSygus(options::inputLanguage()));
1031 d_globalDefineFunRecLemmas
->emplace_back(n
);
1035 d_private
->addFormula(n
, false, true, false, maybeHasFv
);
1040 void SmtEngine::defineFunctionRec(Expr func
,
1041 const std::vector
<Expr
>& formals
,
1045 std::vector
<Expr
> funcs
;
1046 funcs
.push_back(func
);
1047 std::vector
<std::vector
<Expr
> > formals_multi
;
1048 formals_multi
.push_back(formals
);
1049 std::vector
<Expr
> formulas
;
1050 formulas
.push_back(formula
);
1051 defineFunctionsRec(funcs
, formals_multi
, formulas
, global
);
1054 bool SmtEngine::isDefinedFunction( Expr func
){
1055 Node nf
= Node::fromExpr( func
);
1056 Debug("smt") << "isDefined function " << nf
<< "?" << std::endl
;
1057 return d_definedFunctions
->find(nf
) != d_definedFunctions
->end();
1060 void SmtEnginePrivate::finishInit()
1062 d_preprocessingPassContext
.reset(
1063 new PreprocessingPassContext(&d_smt
, &d_iteRemover
, &d_propagator
));
1065 // initialize the preprocessing passes
1066 d_processor
.finishInit(d_preprocessingPassContext
.get());
1069 Result
SmtEngine::check() {
1070 Assert(d_fullyInited
);
1071 Assert(d_pendingPops
== 0);
1073 Trace("smt") << "SmtEngine::check()" << endl
;
1076 if (d_resourceManager
->out())
1078 Result::UnknownExplanation why
= d_resourceManager
->outOfResources()
1079 ? Result::RESOURCEOUT
1081 return Result(Result::ENTAILMENT_UNKNOWN
, why
, d_filename
);
1083 d_resourceManager
->beginCall();
1085 // Make sure the prop layer has all of the assertions
1086 Trace("smt") << "SmtEngine::check(): processing assertions" << endl
;
1087 d_private
->processAssertions();
1088 Trace("smt") << "SmtEngine::check(): done processing assertions" << endl
;
1090 TimerStat::CodeTimer
solveTimer(d_stats
->d_solveTime
);
1092 Chat() << "solving..." << endl
;
1093 Trace("smt") << "SmtEngine::check(): running check" << endl
;
1094 Result result
= d_propEngine
->checkSat();
1096 d_resourceManager
->endCall();
1097 Trace("limit") << "SmtEngine::check(): cumulative millis "
1098 << d_resourceManager
->getTimeUsage() << ", resources "
1099 << d_resourceManager
->getResourceUsage() << endl
;
1101 return Result(result
, d_filename
);
1104 Result
SmtEngine::quickCheck() {
1105 Assert(d_fullyInited
);
1106 Trace("smt") << "SMT quickCheck()" << endl
;
1108 Result::ENTAILMENT_UNKNOWN
, Result::REQUIRES_FULL_CHECK
, d_filename
);
1111 theory::TheoryModel
* SmtEngine::getAvailableModel(const char* c
) const
1113 if (!options::assignFunctionValues())
1115 std::stringstream ss
;
1116 ss
<< "Cannot " << c
<< " when --assign-function-values is false.";
1117 throw RecoverableModalException(ss
.str().c_str());
1120 if (d_smtMode
!= SMT_MODE_SAT
&& d_smtMode
!= SMT_MODE_SAT_UNKNOWN
)
1122 std::stringstream ss
;
1123 ss
<< "Cannot " << c
1124 << " unless immediately preceded by SAT/NOT_ENTAILED or UNKNOWN "
1126 throw RecoverableModalException(ss
.str().c_str());
1129 if (!options::produceModels())
1131 std::stringstream ss
;
1132 ss
<< "Cannot " << c
<< " when produce-models options is off.";
1133 throw ModalException(ss
.str().c_str());
1136 TheoryModel
* m
= d_theoryEngine
->getBuiltModel();
1140 std::stringstream ss
;
1141 ss
<< "Cannot " << c
1142 << " since model is not available. Perhaps the most recent call to "
1143 "check-sat was interupted?";
1144 throw RecoverableModalException(ss
.str().c_str());
1150 void SmtEnginePrivate::processAssertions() {
1151 TimerStat::CodeTimer
paTimer(d_smt
.d_stats
->d_processAssertionsTime
);
1152 spendResource(ResourceManager::Resource::PreprocessStep
);
1153 Assert(d_smt
.d_fullyInited
);
1154 Assert(d_smt
.d_pendingPops
== 0);
1156 if (d_assertions
.size() == 0) {
1160 if (d_assertionsProcessed
&& options::incrementalSolving()) {
1161 // TODO(b/1255): Substitutions in incremental mode should be managed with a
1162 // proper data structure.
1164 d_assertions
.enableStoreSubstsInAsserts();
1168 d_assertions
.disableStoreSubstsInAsserts();
1171 // process the assertions
1172 bool noConflict
= d_processor
.apply(d_assertions
);
1174 //notify theory engine new preprocessed assertions
1175 d_smt
.d_theoryEngine
->notifyPreprocessedAssertions( d_assertions
.ref() );
1177 // Push the formula to decision engine
1180 Chat() << "pushing to decision engine..." << endl
;
1181 d_smt
.d_propEngine
->addAssertionsToDecisionEngine(d_assertions
);
1184 // end: INVARIANT to maintain: no reordering of assertions or
1185 // introducing new ones
1187 // if incremental, compute which variables are assigned
1188 if (options::incrementalSolving())
1190 d_preprocessingPassContext
->recordSymbolsInAssertions(d_assertions
.ref());
1193 // Push the formula to SAT
1195 Chat() << "converting to CNF..." << endl
;
1196 TimerStat::CodeTimer
codeTimer(d_smt
.d_stats
->d_cnfConversionTime
);
1197 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
1198 Chat() << "+ " << d_assertions
[i
] << std::endl
;
1199 d_smt
.d_propEngine
->assertFormula(d_assertions
[i
]);
1203 d_assertionsProcessed
= true;
1205 d_assertions
.clear();
1206 getIteSkolemMap().clear();
1209 void SmtEnginePrivate::addFormula(
1210 TNode n
, bool inUnsatCore
, bool inInput
, bool isAssumption
, bool maybeHasFv
)
1217 Trace("smt") << "SmtEnginePrivate::addFormula(" << n
1218 << "), inUnsatCore = " << inUnsatCore
1219 << ", inInput = " << inInput
1220 << ", isAssumption = " << isAssumption
<< endl
;
1222 // Ensure that it does not contain free variables
1225 if (expr::hasFreeVar(n
))
1227 std::stringstream se
;
1228 se
<< "Cannot process assertion with free variable.";
1229 if (language::isInputLangSygus(options::inputLanguage()))
1231 // Common misuse of SyGuS is to use top-level assert instead of
1232 // constraint when defining the synthesis conjecture.
1233 se
<< " Perhaps you meant `constraint` instead of `assert`?";
1235 throw ModalException(se
.str().c_str());
1239 // Give it to proof manager
1242 // n is an input assertion
1243 if (inUnsatCore
|| options::unsatCores() || options::dumpUnsatCores() || options::checkUnsatCores() || options::fewerPreprocessingHoles()) {
1245 ProofManager::currentPM()->addCoreAssertion(n
.toExpr());
1248 // n is the result of an unknown preprocessing step, add it to dependency map to null
1249 ProofManager::currentPM()->addDependence(n
, Node::null());
1253 // Add the normalized formula to the queue
1254 d_assertions
.push_back(n
, isAssumption
);
1255 //d_assertions.push_back(Rewriter::rewrite(n));
1258 void SmtEngine::ensureBoolean(const Node
& n
)
1260 TypeNode type
= n
.getType(options::typeChecking());
1261 TypeNode boolType
= NodeManager::currentNM()->booleanType();
1262 if(type
!= boolType
) {
1264 ss
<< "Expected " << boolType
<< "\n"
1265 << "The assertion : " << n
<< "\n"
1266 << "Its type : " << type
;
1267 throw TypeCheckingException(n
.toExpr(), ss
.str());
1271 Result
SmtEngine::checkSat(const Expr
& assumption
, bool inUnsatCore
)
1273 Dump("benchmark") << CheckSatCommand(assumption
);
1274 return checkSatisfiability(assumption
, inUnsatCore
, false);
1277 Result
SmtEngine::checkSat(const vector
<Expr
>& assumptions
, bool inUnsatCore
)
1279 if (assumptions
.empty())
1281 Dump("benchmark") << CheckSatCommand();
1285 Dump("benchmark") << CheckSatAssumingCommand(assumptions
);
1288 return checkSatisfiability(assumptions
, inUnsatCore
, false);
1291 Result
SmtEngine::checkEntailed(const Expr
& expr
, bool inUnsatCore
)
1293 Dump("benchmark") << QueryCommand(expr
, inUnsatCore
);
1294 return checkSatisfiability(
1295 expr
.isNull() ? std::vector
<Expr
>() : std::vector
<Expr
>{expr
},
1298 .asEntailmentResult();
1301 Result
SmtEngine::checkEntailed(const vector
<Expr
>& exprs
, bool inUnsatCore
)
1303 return checkSatisfiability(exprs
, inUnsatCore
, true).asEntailmentResult();
1306 Result
SmtEngine::checkSatisfiability(const Expr
& expr
,
1308 bool isEntailmentCheck
)
1310 return checkSatisfiability(
1311 expr
.isNull() ? std::vector
<Expr
>() : std::vector
<Expr
>{expr
},
1316 Result
SmtEngine::checkSatisfiability(const vector
<Expr
>& assumptions
,
1318 bool isEntailmentCheck
)
1322 SmtScope
smts(this);
1323 finalOptionsAreSet();
1326 Trace("smt") << "SmtEngine::"
1327 << (isEntailmentCheck
? "checkEntailed" : "checkSat") << "("
1328 << assumptions
<< ")" << endl
;
1330 if(d_queryMade
&& !options::incrementalSolving()) {
1331 throw ModalException("Cannot make multiple queries unless "
1332 "incremental solving is enabled "
1333 "(try --incremental)");
1336 // Note that a query has been made
1338 // reset global negation
1339 d_globalNegation
= false;
1341 bool didInternalPush
= false;
1343 setProblemExtended();
1345 if (isEntailmentCheck
)
1347 size_t size
= assumptions
.size();
1350 /* Assume: not (BIGAND assumptions) */
1351 d_assumptions
.push_back(
1352 d_exprManager
->mkExpr(kind::AND
, assumptions
).notExpr());
1356 /* Assume: not expr */
1357 d_assumptions
.push_back(assumptions
[0].notExpr());
1362 /* Assume: BIGAND assumptions */
1363 d_assumptions
= assumptions
;
1366 if (!d_assumptions
.empty())
1369 didInternalPush
= true;
1372 Result
r(Result::SAT_UNKNOWN
, Result::UNKNOWN_REASON
);
1373 for (Expr e
: d_assumptions
)
1375 // Substitute out any abstract values in ex.
1376 Node n
= d_absValues
->substituteAbstractValues(Node::fromExpr(e
));
1377 // Ensure expr is type-checked at this point.
1380 /* Add assumption */
1381 if (d_assertionList
!= NULL
)
1383 d_assertionList
->push_back(n
);
1385 d_private
->addFormula(n
, inUnsatCore
, true, true);
1388 if (d_globalDefineFunRecLemmas
!= nullptr)
1390 // Global definitions are asserted at check-sat-time because we have to
1391 // make sure that they are always present (they are essentially level
1393 for (const Node
& lemma
: *d_globalDefineFunRecLemmas
)
1395 d_private
->addFormula(lemma
, false, true, false, false);
1401 if ((options::solveRealAsInt() || options::solveIntAsBV() > 0)
1402 && r
.asSatisfiabilityResult().isSat() == Result::UNSAT
)
1404 r
= Result(Result::SAT_UNKNOWN
, Result::UNKNOWN_REASON
);
1406 // flipped if we did a global negation
1407 if (d_globalNegation
)
1409 Trace("smt") << "SmtEngine::process global negate " << r
<< std::endl
;
1410 if (r
.asSatisfiabilityResult().isSat() == Result::UNSAT
)
1412 r
= Result(Result::SAT
);
1414 else if (r
.asSatisfiabilityResult().isSat() == Result::SAT
)
1416 // only if satisfaction complete
1417 if (d_logic
.isPure(THEORY_ARITH
) || d_logic
.isPure(THEORY_BV
))
1419 r
= Result(Result::UNSAT
);
1423 r
= Result(Result::SAT_UNKNOWN
, Result::UNKNOWN_REASON
);
1426 Trace("smt") << "SmtEngine::global negate returned " << r
<< std::endl
;
1429 d_needPostsolve
= true;
1432 if (didInternalPush
)
1437 // Remember the status
1439 // Check against expected status
1440 if (!d_expectedStatus
.isUnknown() && !d_status
.isUnknown()
1441 && d_status
!= d_expectedStatus
)
1443 CVC4_FATAL() << "Expected result " << d_expectedStatus
<< " but got "
1446 d_expectedStatus
= Result();
1447 // Update the SMT mode
1448 if (d_status
.asSatisfiabilityResult().isSat() == Result::UNSAT
)
1450 d_smtMode
= SMT_MODE_UNSAT
;
1452 else if (d_status
.asSatisfiabilityResult().isSat() == Result::SAT
)
1454 d_smtMode
= SMT_MODE_SAT
;
1458 d_smtMode
= SMT_MODE_SAT_UNKNOWN
;
1461 Trace("smt") << "SmtEngine::" << (isEntailmentCheck
? "query" : "checkSat")
1462 << "(" << assumptions
<< ") => " << r
<< endl
;
1464 // Check that SAT results generate a model correctly.
1465 if(options::checkModels()) {
1466 if (r
.asSatisfiabilityResult().isSat() == Result::SAT
)
1471 // Check that UNSAT results generate a proof correctly.
1472 if(options::checkProofs()) {
1473 if(r
.asSatisfiabilityResult().isSat() == Result::UNSAT
) {
1477 // Check that UNSAT results generate an unsat core correctly.
1478 if(options::checkUnsatCores()) {
1479 if(r
.asSatisfiabilityResult().isSat() == Result::UNSAT
) {
1480 TimerStat::CodeTimer
checkUnsatCoreTimer(d_stats
->d_checkUnsatCoreTime
);
1486 } catch (UnsafeInterruptException
& e
) {
1487 AlwaysAssert(d_resourceManager
->out());
1488 Result::UnknownExplanation why
= d_resourceManager
->outOfResources()
1489 ? Result::RESOURCEOUT
1491 return Result(Result::SAT_UNKNOWN
, why
, d_filename
);
1495 vector
<Expr
> SmtEngine::getUnsatAssumptions(void)
1497 Trace("smt") << "SMT getUnsatAssumptions()" << endl
;
1498 SmtScope
smts(this);
1499 if (!options::unsatAssumptions())
1501 throw ModalException(
1502 "Cannot get unsat assumptions when produce-unsat-assumptions option "
1505 if (d_smtMode
!= SMT_MODE_UNSAT
)
1507 throw RecoverableModalException(
1508 "Cannot get unsat assumptions unless immediately preceded by "
1511 finalOptionsAreSet();
1512 if (Dump
.isOn("benchmark"))
1514 Dump("benchmark") << GetUnsatAssumptionsCommand();
1516 UnsatCore core
= getUnsatCoreInternal();
1518 for (const Expr
& e
: d_assumptions
)
1520 if (find(core
.begin(), core
.end(), e
) != core
.end()) { res
.push_back(e
); }
1525 Result
SmtEngine::assertFormula(const Node
& formula
, bool inUnsatCore
)
1527 SmtScope
smts(this);
1528 finalOptionsAreSet();
1531 Trace("smt") << "SmtEngine::assertFormula(" << formula
<< ")" << endl
;
1533 if (Dump
.isOn("raw-benchmark")) {
1534 Dump("raw-benchmark") << AssertCommand(formula
.toExpr());
1537 // Substitute out any abstract values in ex
1538 Node n
= d_absValues
->substituteAbstractValues(formula
);
1541 if(d_assertionList
!= NULL
) {
1542 d_assertionList
->push_back(n
);
1544 bool maybeHasFv
= language::isInputLangSygus(options::inputLanguage());
1545 d_private
->addFormula(n
, inUnsatCore
, true, false, maybeHasFv
);
1546 return quickCheck().asEntailmentResult();
1547 }/* SmtEngine::assertFormula() */
1550 --------------------------------------------------------------------------
1551 Handling SyGuS commands
1552 --------------------------------------------------------------------------
1555 void SmtEngine::declareSygusVar(const std::string
& id
, Expr var
, Type type
)
1557 SmtScope
smts(this);
1558 finalOptionsAreSet();
1559 d_private
->d_sygusVars
.push_back(Node::fromExpr(var
));
1560 Trace("smt") << "SmtEngine::declareSygusVar: " << var
<< "\n";
1561 Dump("raw-benchmark") << DeclareSygusVarCommand(id
, var
, type
);
1562 // don't need to set that the conjecture is stale
1565 void SmtEngine::declareSygusFunctionVar(const std::string
& id
,
1569 SmtScope
smts(this);
1570 finalOptionsAreSet();
1571 d_private
->d_sygusVars
.push_back(Node::fromExpr(var
));
1572 Trace("smt") << "SmtEngine::declareSygusFunctionVar: " << var
<< "\n";
1573 Dump("raw-benchmark") << DeclareSygusVarCommand(id
, var
, type
);
1575 // don't need to set that the conjecture is stale
1578 void SmtEngine::declareSynthFun(const std::string
& id
,
1582 const std::vector
<Expr
>& vars
)
1584 SmtScope
smts(this);
1585 finalOptionsAreSet();
1587 Node fn
= Node::fromExpr(func
);
1588 d_private
->d_sygusFunSymbols
.push_back(fn
);
1591 Expr bvl
= d_exprManager
->mkExpr(kind::BOUND_VAR_LIST
, vars
);
1592 std::vector
<Expr
> attr_val_bvl
;
1593 attr_val_bvl
.push_back(bvl
);
1594 setUserAttribute("sygus-synth-fun-var-list", func
, attr_val_bvl
, "");
1596 // whether sygus type encodes syntax restrictions
1597 if (sygusType
.isDatatype()
1598 && static_cast<DatatypeType
>(sygusType
).getDatatype().isSygus())
1600 TypeNode stn
= TypeNode::fromType(sygusType
);
1601 Node sym
= d_nodeManager
->mkBoundVar("sfproxy", stn
);
1602 std::vector
<Expr
> attr_value
;
1603 attr_value
.push_back(sym
.toExpr());
1604 setUserAttribute("sygus-synth-grammar", func
, attr_value
, "");
1606 Trace("smt") << "SmtEngine::declareSynthFun: " << func
<< "\n";
1607 Dump("raw-benchmark") << SynthFunCommand(id
, func
, sygusType
, isInv
, vars
);
1608 // sygus conjecture is now stale
1609 setSygusConjectureStale();
1612 void SmtEngine::assertSygusConstraint(const Node
& constraint
)
1614 SmtScope
smts(this);
1615 finalOptionsAreSet();
1616 d_private
->d_sygusConstraints
.push_back(constraint
);
1618 Trace("smt") << "SmtEngine::assertSygusConstrant: " << constraint
<< "\n";
1619 Dump("raw-benchmark") << SygusConstraintCommand(constraint
.toExpr());
1620 // sygus conjecture is now stale
1621 setSygusConjectureStale();
1624 void SmtEngine::assertSygusInvConstraint(const Expr
& inv
,
1629 SmtScope
smts(this);
1630 finalOptionsAreSet();
1631 // build invariant constraint
1633 // get variables (regular and their respective primed versions)
1634 std::vector
<Node
> terms
, vars
, primed_vars
;
1635 terms
.push_back(Node::fromExpr(inv
));
1636 terms
.push_back(Node::fromExpr(pre
));
1637 terms
.push_back(Node::fromExpr(trans
));
1638 terms
.push_back(Node::fromExpr(post
));
1639 // variables are built based on the invariant type
1640 FunctionType t
= static_cast<FunctionType
>(inv
.getType());
1641 std::vector
<Type
> argTypes
= t
.getArgTypes();
1642 for (const Type
& ti
: argTypes
)
1644 TypeNode tn
= TypeNode::fromType(ti
);
1645 vars
.push_back(d_nodeManager
->mkBoundVar(tn
));
1646 d_private
->d_sygusVars
.push_back(vars
.back());
1647 std::stringstream ss
;
1648 ss
<< vars
.back() << "'";
1649 primed_vars
.push_back(d_nodeManager
->mkBoundVar(ss
.str(), tn
));
1650 d_private
->d_sygusVars
.push_back(primed_vars
.back());
1653 // make relevant terms; 0 -> Inv, 1 -> Pre, 2 -> Trans, 3 -> Post
1654 for (unsigned i
= 0; i
< 4; ++i
)
1657 Trace("smt-debug") << "Make inv-constraint term #" << i
<< " : " << op
1658 << " with type " << op
.getType() << "...\n";
1659 std::vector
<Node
> children
;
1660 children
.push_back(op
);
1661 // transition relation applied over both variable lists
1664 children
.insert(children
.end(), vars
.begin(), vars
.end());
1665 children
.insert(children
.end(), primed_vars
.begin(), primed_vars
.end());
1669 children
.insert(children
.end(), vars
.begin(), vars
.end());
1671 terms
[i
] = d_nodeManager
->mkNode(kind::APPLY_UF
, children
);
1672 // make application of Inv on primed variables
1676 children
.push_back(op
);
1677 children
.insert(children
.end(), primed_vars
.begin(), primed_vars
.end());
1678 terms
.push_back(d_nodeManager
->mkNode(kind::APPLY_UF
, children
));
1682 std::vector
<Node
> conj
;
1683 conj
.push_back(d_nodeManager
->mkNode(kind::IMPLIES
, terms
[1], terms
[0]));
1684 Node term0_and_2
= d_nodeManager
->mkNode(kind::AND
, terms
[0], terms
[2]);
1685 conj
.push_back(d_nodeManager
->mkNode(kind::IMPLIES
, term0_and_2
, terms
[4]));
1686 conj
.push_back(d_nodeManager
->mkNode(kind::IMPLIES
, terms
[0], terms
[3]));
1687 Node constraint
= d_nodeManager
->mkNode(kind::AND
, conj
);
1689 d_private
->d_sygusConstraints
.push_back(constraint
);
1691 Trace("smt") << "SmtEngine::assertSygusInvConstrant: " << constraint
<< "\n";
1692 Dump("raw-benchmark") << SygusInvConstraintCommand(inv
, pre
, trans
, post
);
1693 // sygus conjecture is now stale
1694 setSygusConjectureStale();
1697 Result
SmtEngine::checkSynth()
1699 SmtScope
smts(this);
1701 if (options::incrementalSolving())
1703 // TODO (project #7)
1704 throw ModalException(
1705 "Cannot make check-synth commands when incremental solving is enabled");
1708 if (d_private
->d_sygusConjectureStale
)
1710 // build synthesis conjecture from asserted constraints and declared
1711 // variables/functions
1713 d_nodeManager
->mkSkolem("sygus", d_nodeManager
->booleanType());
1714 Node inst_attr
= d_nodeManager
->mkNode(kind::INST_ATTRIBUTE
, sygusVar
);
1715 Node sygusAttr
= d_nodeManager
->mkNode(kind::INST_PATTERN_LIST
, inst_attr
);
1716 std::vector
<Node
> bodyv
;
1717 Trace("smt") << "Sygus : Constructing sygus constraint...\n";
1718 unsigned n_constraints
= d_private
->d_sygusConstraints
.size();
1719 Node body
= n_constraints
== 0
1720 ? d_nodeManager
->mkConst(true)
1721 : (n_constraints
== 1
1722 ? d_private
->d_sygusConstraints
[0]
1723 : d_nodeManager
->mkNode(
1724 kind::AND
, d_private
->d_sygusConstraints
));
1725 body
= body
.notNode();
1726 Trace("smt") << "...constructed sygus constraint " << body
<< std::endl
;
1727 if (!d_private
->d_sygusVars
.empty())
1730 d_nodeManager
->mkNode(kind::BOUND_VAR_LIST
, d_private
->d_sygusVars
);
1731 body
= d_nodeManager
->mkNode(kind::EXISTS
, boundVars
, body
);
1732 Trace("smt") << "...constructed exists " << body
<< std::endl
;
1734 if (!d_private
->d_sygusFunSymbols
.empty())
1736 Node boundVars
= d_nodeManager
->mkNode(kind::BOUND_VAR_LIST
,
1737 d_private
->d_sygusFunSymbols
);
1738 body
= d_nodeManager
->mkNode(kind::FORALL
, boundVars
, body
, sygusAttr
);
1740 Trace("smt") << "...constructed forall " << body
<< std::endl
;
1742 // set attribute for synthesis conjecture
1743 setUserAttribute("sygus", sygusVar
.toExpr(), {}, "");
1745 Trace("smt") << "Check synthesis conjecture: " << body
<< std::endl
;
1746 Dump("raw-benchmark") << CheckSynthCommand();
1748 d_private
->d_sygusConjectureStale
= false;
1750 if (options::incrementalSolving())
1752 // we push a context so that this conjecture is removed if we modify it
1755 assertFormula(body
, true);
1759 query
= body
.toExpr();
1763 Result r
= checkSatisfiability(query
, true, false);
1765 // Check that synthesis solutions satisfy the conjecture
1766 if (options::checkSynthSol()
1767 && r
.asSatisfiabilityResult().isSat() == Result::UNSAT
)
1769 checkSynthSolution();
1775 --------------------------------------------------------------------------
1776 End of Handling SyGuS commands
1777 --------------------------------------------------------------------------
1780 Node
SmtEngine::postprocess(TNode node
, TypeNode expectedType
) const {
1784 Expr
SmtEngine::simplify(const Expr
& ex
)
1786 Assert(ex
.getExprManager() == d_exprManager
);
1787 SmtScope
smts(this);
1788 finalOptionsAreSet();
1790 Trace("smt") << "SMT simplify(" << ex
<< ")" << endl
;
1792 if(Dump
.isOn("benchmark")) {
1793 Dump("benchmark") << SimplifyCommand(ex
);
1796 Expr e
= d_absValues
->substituteAbstractValues(Node::fromExpr(ex
)).toExpr();
1797 if( options::typeChecking() ) {
1798 e
.getType(true); // ensure expr is type-checked at this point
1801 // Make sure all preprocessing is done
1802 d_private
->processAssertions();
1803 Node n
= d_private
->simplify(Node::fromExpr(e
));
1804 n
= postprocess(n
, TypeNode::fromType(e
.getType()));
1808 Node
SmtEngine::expandDefinitions(const Node
& ex
)
1810 d_private
->spendResource(ResourceManager::Resource::PreprocessStep
);
1812 SmtScope
smts(this);
1813 finalOptionsAreSet();
1815 Trace("smt") << "SMT expandDefinitions(" << ex
<< ")" << endl
;
1817 // Substitute out any abstract values in ex.
1818 Node e
= d_absValues
->substituteAbstractValues(ex
);
1819 if(options::typeChecking()) {
1820 // Ensure expr is type-checked at this point.
1824 unordered_map
<Node
, Node
, NodeHashFunction
> cache
;
1825 Node n
= d_private
->getProcessAssertions()->expandDefinitions(
1826 e
, cache
, /* expandOnly = */ true);
1827 n
= postprocess(n
, e
.getType());
1832 // TODO(#1108): Simplify the error reporting of this method.
1833 Expr
SmtEngine::getValue(const Expr
& ex
) const
1835 Assert(ex
.getExprManager() == d_exprManager
);
1836 SmtScope
smts(this);
1838 Trace("smt") << "SMT getValue(" << ex
<< ")" << endl
;
1839 if(Dump
.isOn("benchmark")) {
1840 Dump("benchmark") << GetValueCommand(ex
);
1843 // Substitute out any abstract values in ex.
1844 Expr e
= d_absValues
->substituteAbstractValues(Node::fromExpr(ex
)).toExpr();
1846 // Ensure expr is type-checked at this point.
1847 e
.getType(options::typeChecking());
1849 // do not need to apply preprocessing substitutions (should be recorded
1850 // in model already)
1852 Node n
= Node::fromExpr(e
);
1853 Trace("smt") << "--- getting value of " << n
<< endl
;
1854 TypeNode expectedType
= n
.getType();
1856 // Expand, then normalize
1857 unordered_map
<Node
, Node
, NodeHashFunction
> cache
;
1858 n
= d_private
->getProcessAssertions()->expandDefinitions(n
, cache
);
1859 // There are two ways model values for terms are computed (for historical
1860 // reasons). One way is that used in check-model; the other is that
1861 // used by the Model classes. It's not clear to me exactly how these
1862 // two are different, but they need to be unified. This ugly hack here
1863 // is to fix bug 554 until we can revamp boolean-terms and models [MGD]
1866 if(!n
.getType().isFunction()) {
1867 n
= Rewriter::rewrite(n
);
1870 Trace("smt") << "--- getting value of " << n
<< endl
;
1871 TheoryModel
* m
= getAvailableModel("get-value");
1874 resultNode
= m
->getValue(n
);
1876 Trace("smt") << "--- got value " << n
<< " = " << resultNode
<< endl
;
1877 resultNode
= postprocess(resultNode
, expectedType
);
1878 Trace("smt") << "--- model-post returned " << resultNode
<< endl
;
1879 Trace("smt") << "--- model-post returned " << resultNode
.getType() << endl
;
1880 Trace("smt") << "--- model-post expected " << expectedType
<< endl
;
1882 // type-check the result we got
1883 // Notice that lambdas have function type, which does not respect the subtype
1884 // relation, so we ignore them here.
1885 Assert(resultNode
.isNull() || resultNode
.getKind() == kind::LAMBDA
1886 || resultNode
.getType().isSubtypeOf(expectedType
))
1887 << "Run with -t smt for details.";
1889 // Ensure it's a constant, or a lambda (for uninterpreted functions). This
1890 // assertion only holds for models that do not have approximate values.
1891 Assert(m
->hasApproximations() || resultNode
.getKind() == kind::LAMBDA
1892 || resultNode
.isConst());
1894 if(options::abstractValues() && resultNode
.getType().isArray()) {
1895 resultNode
= d_absValues
->mkAbstractValue(resultNode
);
1896 Trace("smt") << "--- abstract value >> " << resultNode
<< endl
;
1899 return resultNode
.toExpr();
1902 vector
<Expr
> SmtEngine::getValues(const vector
<Expr
>& exprs
)
1904 vector
<Expr
> result
;
1905 for (const Expr
& e
: exprs
)
1907 result
.push_back(getValue(e
));
1912 bool SmtEngine::addToAssignment(const Expr
& ex
) {
1913 SmtScope
smts(this);
1914 finalOptionsAreSet();
1916 // Substitute out any abstract values in ex
1917 Node n
= d_absValues
->substituteAbstractValues(Node::fromExpr(ex
));
1918 TypeNode type
= n
.getType(options::typeChecking());
1920 PrettyCheckArgument(type
.isBoolean(),
1922 "expected Boolean-typed variable or function application "
1923 "in addToAssignment()");
1924 // must be a defined constant, or a variable
1925 PrettyCheckArgument(
1926 (((d_definedFunctions
->find(n
) != d_definedFunctions
->end())
1927 && n
.getNumChildren() == 0)
1930 "expected variable or defined-function application "
1931 "in addToAssignment(),\ngot %s",
1932 n
.toString().c_str());
1933 if(!options::produceAssignments()) {
1936 if(d_assignments
== NULL
) {
1937 d_assignments
= new (true) AssignmentSet(getContext());
1939 d_assignments
->insert(n
);
1944 // TODO(#1108): Simplify the error reporting of this method.
1945 vector
<pair
<Expr
, Expr
>> SmtEngine::getAssignment()
1947 Trace("smt") << "SMT getAssignment()" << endl
;
1948 SmtScope
smts(this);
1949 finalOptionsAreSet();
1950 if(Dump
.isOn("benchmark")) {
1951 Dump("benchmark") << GetAssignmentCommand();
1953 if(!options::produceAssignments()) {
1955 "Cannot get the current assignment when "
1956 "produce-assignments option is off.";
1957 throw ModalException(msg
);
1960 // Get the model here, regardless of whether d_assignments is null, since
1961 // we should throw errors related to model availability whether or not
1962 // assignments is null.
1963 TheoryModel
* m
= getAvailableModel("get assignment");
1965 vector
<pair
<Expr
,Expr
>> res
;
1966 if (d_assignments
!= nullptr)
1968 TypeNode boolType
= d_nodeManager
->booleanType();
1969 for (AssignmentSet::key_iterator i
= d_assignments
->key_begin(),
1970 iend
= d_assignments
->key_end();
1975 Assert(as
.getType() == boolType
);
1977 Trace("smt") << "--- getting value of " << as
<< endl
;
1979 // Expand, then normalize
1980 unordered_map
<Node
, Node
, NodeHashFunction
> cache
;
1981 Node n
= d_private
->getProcessAssertions()->expandDefinitions(as
, cache
);
1982 n
= Rewriter::rewrite(n
);
1984 Trace("smt") << "--- getting value of " << n
<< endl
;
1988 resultNode
= m
->getValue(n
);
1991 // type-check the result we got
1992 Assert(resultNode
.isNull() || resultNode
.getType() == boolType
);
1994 // ensure it's a constant
1995 Assert(resultNode
.isConst());
1998 res
.emplace_back(as
.toExpr(), resultNode
.toExpr());
2004 // TODO(#1108): Simplify the error reporting of this method.
2005 Model
* SmtEngine::getModel() {
2006 Trace("smt") << "SMT getModel()" << endl
;
2007 SmtScope
smts(this);
2009 finalOptionsAreSet();
2011 if(Dump
.isOn("benchmark")) {
2012 Dump("benchmark") << GetModelCommand();
2015 TheoryModel
* m
= getAvailableModel("get model");
2017 // Since model m is being returned to the user, we must ensure that this
2018 // model object remains valid with future check-sat calls. Hence, we set
2019 // the theory engine into "eager model building" mode. TODO #2648: revisit.
2020 d_theoryEngine
->setEagerModelBuilding();
2022 if (options::modelCoresMode() != options::ModelCoresMode::NONE
)
2024 // If we enabled model cores, we compute a model core for m based on our
2025 // (expanded) assertions using the model core builder utility
2026 std::vector
<Expr
> eassertsProc
= getExpandedAssertions();
2027 ModelCoreBuilder::setModelCore(eassertsProc
, m
, options::modelCoresMode());
2029 m
->d_inputName
= d_filename
;
2030 m
->d_isKnownSat
= (d_smtMode
== SMT_MODE_SAT
);
2034 Result
SmtEngine::blockModel()
2036 Trace("smt") << "SMT blockModel()" << endl
;
2037 SmtScope
smts(this);
2039 finalOptionsAreSet();
2041 if (Dump
.isOn("benchmark"))
2043 Dump("benchmark") << BlockModelCommand();
2046 TheoryModel
* m
= getAvailableModel("block model");
2048 if (options::blockModelsMode() == options::BlockModelsMode::NONE
)
2050 std::stringstream ss
;
2051 ss
<< "Cannot block model when block-models is set to none.";
2052 throw ModalException(ss
.str().c_str());
2055 // get expanded assertions
2056 std::vector
<Expr
> eassertsProc
= getExpandedAssertions();
2057 Expr eblocker
= ModelBlocker::getModelBlocker(
2058 eassertsProc
, m
, options::blockModelsMode());
2059 return assertFormula(Node::fromExpr(eblocker
));
2062 Result
SmtEngine::blockModelValues(const std::vector
<Expr
>& exprs
)
2064 Trace("smt") << "SMT blockModelValues()" << endl
;
2065 SmtScope
smts(this);
2067 finalOptionsAreSet();
2069 PrettyCheckArgument(
2071 "block model values must be called on non-empty set of terms");
2072 if (Dump
.isOn("benchmark"))
2074 Dump("benchmark") << BlockModelValuesCommand(exprs
);
2077 TheoryModel
* m
= getAvailableModel("block model values");
2079 // get expanded assertions
2080 std::vector
<Expr
> eassertsProc
= getExpandedAssertions();
2081 // we always do block model values mode here
2082 Expr eblocker
= ModelBlocker::getModelBlocker(
2083 eassertsProc
, m
, options::BlockModelsMode::VALUES
, exprs
);
2084 return assertFormula(Node::fromExpr(eblocker
));
2087 std::pair
<Expr
, Expr
> SmtEngine::getSepHeapAndNilExpr(void)
2089 if (!d_logic
.isTheoryEnabled(THEORY_SEP
))
2092 "Cannot obtain separation logic expressions if not using the "
2093 "separation logic theory.";
2094 throw RecoverableModalException(msg
);
2096 NodeManagerScope
nms(d_nodeManager
);
2099 Model
* m
= getAvailableModel("get separation logic heap and nil");
2100 if (!m
->getHeapModel(heap
, nil
))
2103 << "SmtEngine::getSepHeapAndNilExpr(): failed to obtain heap/nil "
2104 "expressions from theory model.";
2106 return std::make_pair(heap
, nil
);
2109 std::vector
<Expr
> SmtEngine::getExpandedAssertions()
2111 std::vector
<Expr
> easserts
= getAssertions();
2112 // must expand definitions
2113 std::vector
<Expr
> eassertsProc
;
2114 std::unordered_map
<Node
, Node
, NodeHashFunction
> cache
;
2115 for (const Expr
& e
: easserts
)
2117 Node ea
= Node::fromExpr(e
);
2118 Node eae
= d_private
->getProcessAssertions()->expandDefinitions(ea
, cache
);
2119 eassertsProc
.push_back(eae
.toExpr());
2121 return eassertsProc
;
2124 Expr
SmtEngine::getSepHeapExpr() { return getSepHeapAndNilExpr().first
; }
2126 Expr
SmtEngine::getSepNilExpr() { return getSepHeapAndNilExpr().second
; }
2128 void SmtEngine::checkProof()
2130 #if (IS_LFSC_BUILD && IS_PROOFS_BUILD)
2132 Chat() << "generating proof..." << endl
;
2134 const Proof
& pf
= getProof();
2136 Chat() << "checking proof..." << endl
;
2138 std::string logicString
= d_logic
.getLogicString();
2140 std::stringstream pfStream
;
2142 pfStream
<< proof::plf_signatures
<< endl
;
2143 int64_t sizeBeforeProof
= static_cast<int64_t>(pfStream
.tellp());
2145 pf
.toStream(pfStream
);
2146 d_stats
->d_proofsSize
+=
2147 static_cast<int64_t>(pfStream
.tellp()) - sizeBeforeProof
;
2150 TimerStat::CodeTimer
checkProofTimer(d_stats
->d_lfscCheckProofTime
);
2152 lfscc_check_file(pfStream
, false, false, false, false, false, false, false);
2154 // FIXME: we should actually call lfscc_cleanup here, but lfscc_cleanup
2155 // segfaults on regress0/bv/core/bitvec7.smt
2158 #else /* (IS_LFSC_BUILD && IS_PROOFS_BUILD) */
2160 << "This version of CVC4 was built without proof support; cannot check "
2162 #endif /* (IS_LFSC_BUILD && IS_PROOFS_BUILD) */
2165 UnsatCore
SmtEngine::getUnsatCoreInternal()
2168 if (!options::unsatCores())
2170 throw ModalException(
2171 "Cannot get an unsat core when produce-unsat-cores option is off.");
2173 if (d_smtMode
!= SMT_MODE_UNSAT
)
2175 throw RecoverableModalException(
2176 "Cannot get an unsat core unless immediately preceded by "
2177 "UNSAT/ENTAILED response.");
2180 d_proofManager
->traceUnsatCore(); // just to trigger core creation
2181 return UnsatCore(this, d_proofManager
->extractUnsatCore());
2182 #else /* IS_PROOFS_BUILD */
2183 throw ModalException(
2184 "This build of CVC4 doesn't have proof support (required for unsat "
2186 #endif /* IS_PROOFS_BUILD */
2189 void SmtEngine::checkUnsatCore() {
2190 Assert(options::unsatCores())
2191 << "cannot check unsat core if unsat cores are turned off";
2193 Notice() << "SmtEngine::checkUnsatCore(): generating unsat core" << endl
;
2194 UnsatCore core
= getUnsatCore();
2196 SmtEngine
coreChecker(d_exprManager
, &d_options
);
2197 coreChecker
.setIsInternalSubsolver();
2198 coreChecker
.setLogic(getLogicInfo());
2199 coreChecker
.getOptions().set(options::checkUnsatCores
, false);
2200 coreChecker
.getOptions().set(options::checkProofs
, false);
2203 std::vector
<Command
*>::const_iterator itg
= d_defineCommands
.begin();
2204 for (; itg
!= d_defineCommands
.end(); ++itg
) {
2205 (*itg
)->invoke(&coreChecker
);
2209 Notice() << "SmtEngine::checkUnsatCore(): pushing core assertions (size == " << core
.size() << ")" << endl
;
2210 for(UnsatCore::iterator i
= core
.begin(); i
!= core
.end(); ++i
) {
2211 Notice() << "SmtEngine::checkUnsatCore(): pushing core member " << *i
<< endl
;
2212 coreChecker
.assertFormula(Node::fromExpr(*i
));
2216 r
= coreChecker
.checkSat();
2220 Notice() << "SmtEngine::checkUnsatCore(): result is " << r
<< endl
;
2221 if(r
.asSatisfiabilityResult().isUnknown()) {
2223 << "SmtEngine::checkUnsatCore(): could not check core result unknown."
2226 else if (r
.asSatisfiabilityResult().isSat())
2229 << "SmtEngine::checkUnsatCore(): produced core was satisfiable.";
2233 void SmtEngine::checkModel(bool hardFailure
) {
2234 // --check-model implies --produce-assertions, which enables the
2235 // assertion list, so we should be ok.
2236 Assert(d_assertionList
!= NULL
)
2237 << "don't have an assertion list to check in SmtEngine::checkModel()";
2239 TimerStat::CodeTimer
checkModelTimer(d_stats
->d_checkModelTime
);
2241 // Throughout, we use Notice() to give diagnostic output.
2243 // If this function is running, the user gave --check-model (or equivalent),
2244 // and if Notice() is on, the user gave --verbose (or equivalent).
2246 Notice() << "SmtEngine::checkModel(): generating model" << endl
;
2247 TheoryModel
* m
= getAvailableModel("check model");
2249 // check-model is not guaranteed to succeed if approximate values were used.
2250 // Thus, we intentionally abort here.
2251 if (m
->hasApproximations())
2253 throw RecoverableModalException(
2254 "Cannot run check-model on a model with approximate values.");
2257 // Check individual theory assertions
2258 if (options::debugCheckModels())
2260 d_theoryEngine
->checkTheoryAssertionsWithModel(hardFailure
);
2266 // We have a "fake context" for the substitution map (we don't need it
2267 // to be context-dependent)
2268 context::Context fakeContext
;
2269 SubstitutionMap
substitutions(&fakeContext
, /* substituteUnderQuantifiers = */ false);
2271 for(size_t k
= 0; k
< m
->getNumCommands(); ++k
) {
2272 const DeclareFunctionCommand
* c
= dynamic_cast<const DeclareFunctionCommand
*>(m
->getCommand(k
));
2273 Notice() << "SmtEngine::checkModel(): model command " << k
<< " : " << m
->getCommand(k
) << endl
;
2275 // we don't care about DECLARE-DATATYPES, DECLARE-SORT, ...
2276 Notice() << "SmtEngine::checkModel(): skipping..." << endl
;
2278 // We have a DECLARE-FUN:
2280 // We'll first do some checks, then add to our substitution map
2281 // the mapping: function symbol |-> value
2283 Expr func
= c
->getFunction();
2284 Node val
= m
->getValue(func
);
2286 Notice() << "SmtEngine::checkModel(): adding substitution: " << func
<< " |-> " << val
<< endl
;
2288 // (1) if the value is a lambda, ensure the lambda doesn't contain the
2289 // function symbol (since then the definition is recursive)
2290 if (val
.getKind() == kind::LAMBDA
) {
2291 // first apply the model substitutions we have so far
2292 Debug("boolean-terms") << "applying subses to " << val
[1] << endl
;
2293 Node n
= substitutions
.apply(val
[1]);
2294 Debug("boolean-terms") << "++ got " << n
<< endl
;
2295 // now check if n contains func by doing a substitution
2296 // [func->func2] and checking equality of the Nodes.
2297 // (this just a way to check if func is in n.)
2298 SubstitutionMap
subs(&fakeContext
);
2299 Node func2
= NodeManager::currentNM()->mkSkolem("", TypeNode::fromType(func
.getType()), "", NodeManager::SKOLEM_NO_NOTIFY
);
2300 subs
.addSubstitution(func
, func2
);
2301 if(subs
.apply(n
) != n
) {
2302 Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE DEFINED IN TERMS OF ITSELF ***" << endl
;
2304 ss
<< "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
2305 << "considering model value for " << func
<< endl
2306 << "body of lambda is: " << val
<< endl
;
2308 ss
<< "body substitutes to: " << n
<< endl
;
2310 ss
<< "so " << func
<< " is defined in terms of itself." << endl
2311 << "Run with `--check-models -v' for additional diagnostics.";
2312 InternalError() << ss
.str();
2316 // (2) check that the value is actually a value
2317 else if (!val
.isConst())
2319 // This is only a warning since it could have been assigned an
2320 // unevaluable term (e.g. an application of a transcendental function).
2321 // This parallels the behavior (warnings for non-constant expressions)
2322 // when checking whether assertions are satisfied below.
2323 Warning() << "Warning : SmtEngine::checkModel(): "
2324 << "model value for " << func
<< endl
2325 << " is " << val
<< endl
2326 << "and that is not a constant (.isConst() == false)."
2328 << "Run with `--check-models -v' for additional diagnostics."
2332 // (3) check that it's the correct (sub)type
2333 // This was intended to be a more general check, but for now we can't do that because
2334 // e.g. "1" is an INT, which isn't a subrange type [1..10] (etc.).
2335 else if(func
.getType().isInteger() && !val
.getType().isInteger()) {
2336 Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE NOT CORRECT TYPE ***" << endl
;
2338 << "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH "
2341 << "model value for " << func
<< endl
2342 << " is " << val
<< endl
2343 << "value type is " << val
.getType() << endl
2344 << "should be of type " << func
.getType() << endl
2345 << "Run with `--check-models -v' for additional diagnostics.";
2348 // (4) checks complete, add the substitution
2349 Debug("boolean-terms") << "cm: adding subs " << func
<< " :=> " << val
<< endl
;
2350 substitutions
.addSubstitution(func
, val
);
2354 // Now go through all our user assertions checking if they're satisfied.
2355 for (const Node
& assertion
: *d_assertionList
)
2357 Notice() << "SmtEngine::checkModel(): checking assertion " << assertion
2360 Node nr
= Rewriter::rewrite(substitutions
.apply(n
));
2361 Trace("boolean-terms") << "n: " << n
<< endl
;
2362 Trace("boolean-terms") << "nr: " << nr
<< endl
;
2363 if (nr
.isConst() && nr
.getConst
<bool>())
2367 // Apply any define-funs from the problem.
2369 unordered_map
<Node
, Node
, NodeHashFunction
> cache
;
2370 n
= d_private
->getProcessAssertions()->expandDefinitions(n
, cache
);
2372 Notice() << "SmtEngine::checkModel(): -- expands to " << n
<< endl
;
2374 // Apply our model value substitutions.
2375 Debug("boolean-terms") << "applying subses to " << n
<< endl
;
2376 n
= substitutions
.apply(n
);
2377 Debug("boolean-terms") << "++ got " << n
<< endl
;
2378 Notice() << "SmtEngine::checkModel(): -- substitutes to " << n
<< endl
;
2380 // We look up the value before simplifying. If n contains quantifiers,
2381 // this may increases the chance of finding its value before the node is
2382 // altered by simplification below.
2384 Notice() << "SmtEngine::checkModel(): -- get value : " << n
<< std::endl
;
2386 // Simplify the result.
2387 n
= d_private
->simplify(n
);
2388 Notice() << "SmtEngine::checkModel(): -- simplifies to " << n
<< endl
;
2390 // Replace the already-known ITEs (this is important for ground ITEs under quantifiers).
2391 n
= d_private
->d_iteRemover
.replace(n
);
2392 Notice() << "SmtEngine::checkModel(): -- ite replacement gives " << n
<< endl
;
2394 // Apply our model value substitutions (again), as things may have been simplified.
2395 Debug("boolean-terms") << "applying subses to " << n
<< endl
;
2396 n
= substitutions
.apply(n
);
2397 Debug("boolean-terms") << "++ got " << n
<< endl
;
2398 Notice() << "SmtEngine::checkModel(): -- re-substitutes to " << n
<< endl
;
2400 // As a last-ditch effort, ask model to simplify it.
2401 // Presently, this is only an issue for quantifiers, which can have a value
2402 // but don't show up in our substitution map above.
2404 Notice() << "SmtEngine::checkModel(): -- model-substitutes to " << n
<< endl
;
2408 if (n
.getConst
<bool>())
2410 // assertion is true, everything is fine
2415 // Otherwise, we did not succeed in showing the current assertion to be
2416 // true. This may either indicate that our model is wrong, or that we cannot
2417 // check it. The latter may be the case for several reasons.
2418 // For example, quantified formulas are not checkable, although we assign
2419 // them to true/false based on the satisfying assignment. However,
2420 // quantified formulas can be modified during preprocess, so they may not
2421 // correspond to those in the satisfying assignment. Hence we throw
2422 // warnings for assertions that do not simplify to either true or false.
2423 // Other theories such as non-linear arithmetic (in particular,
2424 // transcendental functions) also have the property of not being able to
2425 // be checked precisely here.
2426 // Note that warnings like these can be avoided for quantified formulas
2427 // by making preprocessing passes explicitly record how they
2428 // rewrite quantified formulas (see cvc4-wishues#43).
2431 // Not constant, print a less severe warning message here.
2432 Warning() << "Warning : SmtEngine::checkModel(): cannot check simplified "
2437 // Assertions that simplify to false result in an InternalError or
2438 // Warning being thrown below (when hardFailure is false).
2439 Notice() << "SmtEngine::checkModel(): *** PROBLEM: EXPECTED `TRUE' ***"
2442 ss
<< "SmtEngine::checkModel(): "
2443 << "ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
2444 << "assertion: " << assertion
<< endl
2445 << "simplifies to: " << n
<< endl
2446 << "expected `true'." << endl
2447 << "Run with `--check-models -v' for additional diagnostics.";
2450 // internal error if hardFailure is true
2451 InternalError() << ss
.str();
2455 Warning() << ss
.str() << endl
;
2458 Notice() << "SmtEngine::checkModel(): all assertions checked out OK !" << endl
;
2461 void SmtEngine::checkSynthSolution()
2463 NodeManager
* nm
= NodeManager::currentNM();
2464 Notice() << "SmtEngine::checkSynthSolution(): checking synthesis solution" << endl
;
2465 std::map
<Node
, std::map
<Node
, Node
>> sol_map
;
2466 /* Get solutions and build auxiliary vectors for substituting */
2467 if (!d_theoryEngine
->getSynthSolutions(sol_map
))
2469 InternalError() << "SmtEngine::checkSynthSolution(): No solution to check!";
2472 if (sol_map
.empty())
2474 InternalError() << "SmtEngine::checkSynthSolution(): Got empty solution!";
2477 Trace("check-synth-sol") << "Got solution map:\n";
2478 // the set of synthesis conjectures in our assertions
2479 std::unordered_set
<Node
, NodeHashFunction
> conjs
;
2480 // For each of the above conjectures, the functions-to-synthesis and their
2481 // solutions. This is used as a substitution below.
2482 std::map
<Node
, std::vector
<Node
>> fvarMap
;
2483 std::map
<Node
, std::vector
<Node
>> fsolMap
;
2484 for (const std::pair
<const Node
, std::map
<Node
, Node
>>& cmap
: sol_map
)
2486 Trace("check-synth-sol") << "For conjecture " << cmap
.first
<< ":\n";
2487 conjs
.insert(cmap
.first
);
2488 std::vector
<Node
>& fvars
= fvarMap
[cmap
.first
];
2489 std::vector
<Node
>& fsols
= fsolMap
[cmap
.first
];
2490 for (const std::pair
<const Node
, Node
>& pair
: cmap
.second
)
2492 Trace("check-synth-sol")
2493 << " " << pair
.first
<< " --> " << pair
.second
<< "\n";
2494 fvars
.push_back(pair
.first
);
2495 fsols
.push_back(pair
.second
);
2498 Trace("check-synth-sol") << "Starting new SMT Engine\n";
2499 /* Start new SMT engine to check solutions */
2500 SmtEngine
solChecker(d_exprManager
, &d_options
);
2501 solChecker
.setIsInternalSubsolver();
2502 solChecker
.setLogic(getLogicInfo());
2503 solChecker
.getOptions().set(options::checkSynthSol
, false);
2504 solChecker
.getOptions().set(options::sygusRecFun
, false);
2506 Trace("check-synth-sol") << "Retrieving assertions\n";
2507 // Build conjecture from original assertions
2508 if (d_assertionList
== NULL
)
2510 Trace("check-synth-sol") << "No assertions to check\n";
2513 // auxiliary assertions
2514 std::vector
<Node
> auxAssertions
;
2515 // expand definitions cache
2516 std::unordered_map
<Node
, Node
, NodeHashFunction
> cache
;
2517 for (const Node
& assertion
: *d_assertionList
)
2519 Notice() << "SmtEngine::checkSynthSolution(): checking assertion "
2520 << assertion
<< endl
;
2521 Trace("check-synth-sol") << "Retrieving assertion " << assertion
<< "\n";
2522 // Apply any define-funs from the problem.
2524 d_private
->getProcessAssertions()->expandDefinitions(assertion
, cache
);
2525 Notice() << "SmtEngine::checkSynthSolution(): -- expands to " << n
<< endl
;
2526 Trace("check-synth-sol") << "Expanded assertion " << n
<< "\n";
2527 if (conjs
.find(n
) == conjs
.end())
2529 Trace("check-synth-sol") << "It is an auxiliary assertion\n";
2530 auxAssertions
.push_back(n
);
2534 Trace("check-synth-sol") << "It is a synthesis conjecture\n";
2537 // check all conjectures
2538 for (const Node
& conj
: conjs
)
2540 // get the solution for this conjecture
2541 std::vector
<Node
>& fvars
= fvarMap
[conj
];
2542 std::vector
<Node
>& fsols
= fsolMap
[conj
];
2543 // Apply solution map to conjecture body
2545 /* Whether property is quantifier free */
2546 if (conj
[1].getKind() != kind::EXISTS
)
2548 conjBody
= conj
[1].substitute(
2549 fvars
.begin(), fvars
.end(), fsols
.begin(), fsols
.end());
2553 conjBody
= conj
[1][1].substitute(
2554 fvars
.begin(), fvars
.end(), fsols
.begin(), fsols
.end());
2556 /* Skolemize property */
2557 std::vector
<Node
> vars
, skos
;
2558 for (unsigned j
= 0, size
= conj
[1][0].getNumChildren(); j
< size
; ++j
)
2560 vars
.push_back(conj
[1][0][j
]);
2561 std::stringstream ss
;
2563 skos
.push_back(nm
->mkSkolem(ss
.str(), conj
[1][0][j
].getType()));
2564 Trace("check-synth-sol") << "\tSkolemizing " << conj
[1][0][j
] << " to "
2565 << skos
.back() << "\n";
2567 conjBody
= conjBody
.substitute(
2568 vars
.begin(), vars
.end(), skos
.begin(), skos
.end());
2570 Notice() << "SmtEngine::checkSynthSolution(): -- body substitutes to "
2571 << conjBody
<< endl
;
2572 Trace("check-synth-sol") << "Substituted body of assertion to " << conjBody
2574 solChecker
.assertFormula(conjBody
);
2575 // Assert all auxiliary assertions. This may include recursive function
2576 // definitions that were added as assertions to the sygus problem.
2577 for (const Node
& a
: auxAssertions
)
2579 solChecker
.assertFormula(a
);
2581 Result r
= solChecker
.checkSat();
2582 Notice() << "SmtEngine::checkSynthSolution(): result is " << r
<< endl
;
2583 Trace("check-synth-sol") << "Satsifiability check: " << r
<< "\n";
2584 if (r
.asSatisfiabilityResult().isUnknown())
2586 InternalError() << "SmtEngine::checkSynthSolution(): could not check "
2590 else if (r
.asSatisfiabilityResult().isSat())
2593 << "SmtEngine::checkSynthSolution(): produced solution leads to "
2594 "satisfiable negated conjecture.";
2596 solChecker
.resetAssertions();
2600 void SmtEngine::checkInterpol(Expr interpol
,
2601 const std::vector
<Expr
>& easserts
,
2606 void SmtEngine::checkAbduct(Node a
)
2608 Assert(a
.getType().isBoolean());
2609 // check it with the abduction solver
2610 return d_abductSolver
->checkAbduct(a
);
2613 // TODO(#1108): Simplify the error reporting of this method.
2614 UnsatCore
SmtEngine::getUnsatCore() {
2615 Trace("smt") << "SMT getUnsatCore()" << endl
;
2616 SmtScope
smts(this);
2617 finalOptionsAreSet();
2618 if(Dump
.isOn("benchmark")) {
2619 Dump("benchmark") << GetUnsatCoreCommand();
2621 return getUnsatCoreInternal();
2624 // TODO(#1108): Simplify the error reporting of this method.
2625 const Proof
& SmtEngine::getProof()
2627 Trace("smt") << "SMT getProof()" << endl
;
2628 SmtScope
smts(this);
2629 finalOptionsAreSet();
2630 if(Dump
.isOn("benchmark")) {
2631 Dump("benchmark") << GetProofCommand();
2634 if(!options::proof()) {
2635 throw ModalException("Cannot get a proof when produce-proofs option is off.");
2637 if (d_smtMode
!= SMT_MODE_UNSAT
)
2639 throw RecoverableModalException(
2640 "Cannot get a proof unless immediately preceded by UNSAT/ENTAILED "
2644 return ProofManager::getProof(this);
2645 #else /* IS_PROOFS_BUILD */
2646 throw ModalException("This build of CVC4 doesn't have proof support.");
2647 #endif /* IS_PROOFS_BUILD */
2650 void SmtEngine::printInstantiations( std::ostream
& out
) {
2651 SmtScope
smts(this);
2652 finalOptionsAreSet();
2653 if (options::instFormatMode() == options::InstFormatMode::SZS
)
2655 out
<< "% SZS output start Proof for " << d_filename
.c_str() << std::endl
;
2657 if( d_theoryEngine
){
2658 d_theoryEngine
->printInstantiations( out
);
2662 if (options::instFormatMode() == options::InstFormatMode::SZS
)
2664 out
<< "% SZS output end Proof for " << d_filename
.c_str() << std::endl
;
2668 void SmtEngine::printSynthSolution( std::ostream
& out
) {
2669 SmtScope
smts(this);
2670 finalOptionsAreSet();
2671 if( d_theoryEngine
){
2672 d_theoryEngine
->printSynthSolution( out
);
2678 bool SmtEngine::getSynthSolutions(std::map
<Expr
, Expr
>& sol_map
)
2680 SmtScope
smts(this);
2681 finalOptionsAreSet();
2682 std::map
<Node
, std::map
<Node
, Node
>> sol_mapn
;
2683 Assert(d_theoryEngine
!= nullptr);
2684 // fail if the theory engine does not have synthesis solutions
2685 if (!d_theoryEngine
->getSynthSolutions(sol_mapn
))
2689 for (std::pair
<const Node
, std::map
<Node
, Node
>>& cs
: sol_mapn
)
2691 for (std::pair
<const Node
, Node
>& s
: cs
.second
)
2693 sol_map
[s
.first
.toExpr()] = s
.second
.toExpr();
2699 Expr
SmtEngine::doQuantifierElimination(const Expr
& e
, bool doFull
, bool strict
)
2701 SmtScope
smts(this);
2702 finalOptionsAreSet();
2703 if(!d_logic
.isPure(THEORY_ARITH
) && strict
){
2704 Warning() << "Unexpected logic for quantifier elimination " << d_logic
<< endl
;
2706 Trace("smt-qe") << "Do quantifier elimination " << e
<< std::endl
;
2707 Node n_e
= Node::fromExpr( e
);
2708 if (n_e
.getKind() != kind::EXISTS
&& n_e
.getKind() != kind::FORALL
)
2710 throw ModalException(
2711 "Expecting a quantified formula as argument to get-qe.");
2713 //tag the quantified formula with the quant-elim attribute
2714 TypeNode t
= NodeManager::currentNM()->booleanType();
2715 Node n_attr
= NodeManager::currentNM()->mkSkolem("qe", t
, "Auxiliary variable for qe attr.");
2716 std::vector
< Node
> node_values
;
2717 d_theoryEngine
->setUserAttribute( doFull
? "quant-elim" : "quant-elim-partial", n_attr
, node_values
, "");
2718 n_attr
= NodeManager::currentNM()->mkNode(kind::INST_ATTRIBUTE
, n_attr
);
2719 n_attr
= NodeManager::currentNM()->mkNode(kind::INST_PATTERN_LIST
, n_attr
);
2720 std::vector
< Node
> e_children
;
2721 e_children
.push_back( n_e
[0] );
2722 e_children
.push_back(n_e
.getKind() == kind::EXISTS
? n_e
[1]
2724 e_children
.push_back( n_attr
);
2725 Node nn_e
= NodeManager::currentNM()->mkNode( kind::EXISTS
, e_children
);
2726 Trace("smt-qe-debug") << "Query for quantifier elimination : " << nn_e
<< std::endl
;
2727 Assert(nn_e
.getNumChildren() == 3);
2728 Result r
= checkSatisfiability(nn_e
.toExpr(), true, true);
2729 Trace("smt-qe") << "Query returned " << r
<< std::endl
;
2730 if(r
.asSatisfiabilityResult().isSat() != Result::UNSAT
) {
2731 if( r
.asSatisfiabilityResult().isSat() != Result::SAT
&& doFull
){
2733 << "While performing quantifier elimination, unexpected result : "
2734 << r
<< " for query.";
2735 // failed, return original
2738 std::vector
< Node
> inst_qs
;
2739 d_theoryEngine
->getInstantiatedQuantifiedFormulas( inst_qs
);
2740 Assert(inst_qs
.size() <= 1);
2742 if( inst_qs
.size()==1 ){
2743 Node top_q
= inst_qs
[0];
2744 //Node top_q = Rewriter::rewrite( nn_e ).negate();
2745 Assert(top_q
.getKind() == kind::FORALL
);
2746 Trace("smt-qe") << "Get qe for " << top_q
<< std::endl
;
2747 ret_n
= d_theoryEngine
->getInstantiatedConjunction( top_q
);
2748 Trace("smt-qe") << "Returned : " << ret_n
<< std::endl
;
2749 if (n_e
.getKind() == kind::EXISTS
)
2751 ret_n
= Rewriter::rewrite(ret_n
.negate());
2754 ret_n
= NodeManager::currentNM()->mkConst(n_e
.getKind() != kind::EXISTS
);
2756 // do extended rewrite to minimize the size of the formula aggressively
2757 theory::quantifiers::ExtendedRewriter
extr(true);
2758 ret_n
= extr
.extendedRewrite(ret_n
);
2759 return ret_n
.toExpr();
2761 return NodeManager::currentNM()
2762 ->mkConst(n_e
.getKind() == kind::EXISTS
)
2767 bool SmtEngine::getInterpol(const Expr
& conj
,
2768 const Type
& grammarType
,
2774 bool SmtEngine::getInterpol(const Expr
& conj
, Expr
& interpol
)
2777 return getInterpol(conj
, grammarType
, interpol
);
2780 bool SmtEngine::getAbduct(const Node
& conj
,
2781 const TypeNode
& grammarType
,
2784 if (d_abductSolver
->getAbduct(conj
, grammarType
, abd
))
2786 // successfully generated an abduct, update to abduct state
2787 d_smtMode
= SMT_MODE_ABDUCT
;
2790 // failed, we revert to the assert state
2791 d_smtMode
= SMT_MODE_ASSERT
;
2795 bool SmtEngine::getAbduct(const Node
& conj
, Node
& abd
)
2797 TypeNode grammarType
;
2798 return getAbduct(conj
, grammarType
, abd
);
2801 void SmtEngine::getInstantiatedQuantifiedFormulas( std::vector
< Expr
>& qs
) {
2802 SmtScope
smts(this);
2803 if( d_theoryEngine
){
2804 std::vector
< Node
> qs_n
;
2805 d_theoryEngine
->getInstantiatedQuantifiedFormulas( qs_n
);
2806 for( unsigned i
=0; i
<qs_n
.size(); i
++ ){
2807 qs
.push_back( qs_n
[i
].toExpr() );
2814 void SmtEngine::getInstantiations( Expr q
, std::vector
< Expr
>& insts
) {
2815 SmtScope
smts(this);
2816 if( d_theoryEngine
){
2817 std::vector
< Node
> insts_n
;
2818 d_theoryEngine
->getInstantiations( Node::fromExpr( q
), insts_n
);
2819 for( unsigned i
=0; i
<insts_n
.size(); i
++ ){
2820 insts
.push_back( insts_n
[i
].toExpr() );
2827 void SmtEngine::getInstantiationTermVectors( Expr q
, std::vector
< std::vector
< Expr
> >& tvecs
) {
2828 SmtScope
smts(this);
2829 Assert(options::trackInstLemmas());
2830 if( d_theoryEngine
){
2831 std::vector
< std::vector
< Node
> > tvecs_n
;
2832 d_theoryEngine
->getInstantiationTermVectors( Node::fromExpr( q
), tvecs_n
);
2833 for( unsigned i
=0; i
<tvecs_n
.size(); i
++ ){
2834 std::vector
< Expr
> tvec
;
2835 for( unsigned j
=0; j
<tvecs_n
[i
].size(); j
++ ){
2836 tvec
.push_back( tvecs_n
[i
][j
].toExpr() );
2838 tvecs
.push_back( tvec
);
2845 vector
<Expr
> SmtEngine::getAssertions() {
2846 SmtScope
smts(this);
2847 finalOptionsAreSet();
2849 if(Dump
.isOn("benchmark")) {
2850 Dump("benchmark") << GetAssertionsCommand();
2852 Trace("smt") << "SMT getAssertions()" << endl
;
2853 if(!options::produceAssertions()) {
2855 "Cannot query the current assertion list when not in produce-assertions mode.";
2856 throw ModalException(msg
);
2858 Assert(d_assertionList
!= NULL
);
2859 std::vector
<Expr
> res
;
2860 for (const Node
& n
: *d_assertionList
)
2862 res
.emplace_back(n
.toExpr());
2864 // copy the result out
2868 void SmtEngine::push()
2870 SmtScope
smts(this);
2871 finalOptionsAreSet();
2873 Trace("smt") << "SMT push()" << endl
;
2874 d_private
->notifyPush();
2875 d_private
->processAssertions();
2876 if(Dump
.isOn("benchmark")) {
2877 Dump("benchmark") << PushCommand();
2879 if(!options::incrementalSolving()) {
2880 throw ModalException("Cannot push when not solving incrementally (use --incremental)");
2884 // The problem isn't really "extended" yet, but this disallows
2885 // get-model after a push, simplifying our lives somewhat and
2886 // staying symmetric with pop.
2887 setProblemExtended();
2889 d_userLevels
.push_back(d_userContext
->getLevel());
2891 Trace("userpushpop") << "SmtEngine: pushed to level "
2892 << d_userContext
->getLevel() << endl
;
2895 void SmtEngine::pop() {
2896 SmtScope
smts(this);
2897 finalOptionsAreSet();
2898 Trace("smt") << "SMT pop()" << endl
;
2899 if(Dump
.isOn("benchmark")) {
2900 Dump("benchmark") << PopCommand();
2902 if(!options::incrementalSolving()) {
2903 throw ModalException("Cannot pop when not solving incrementally (use --incremental)");
2905 if(d_userLevels
.size() == 0) {
2906 throw ModalException("Cannot pop beyond the first user frame");
2909 // The problem isn't really "extended" yet, but this disallows
2910 // get-model after a pop, simplifying our lives somewhat. It might
2911 // not be strictly necessary to do so, since the pops occur lazily,
2912 // but also it would be weird to have a legally-executed (get-model)
2913 // that only returns a subset of the assignment (because the rest
2914 // is no longer in scope!).
2915 setProblemExtended();
2917 AlwaysAssert(d_userContext
->getLevel() > 0);
2918 AlwaysAssert(d_userLevels
.back() < d_userContext
->getLevel());
2919 while (d_userLevels
.back() < d_userContext
->getLevel()) {
2922 d_userLevels
.pop_back();
2924 // Clear out assertion queues etc., in case anything is still in there
2925 d_private
->notifyPop();
2927 Trace("userpushpop") << "SmtEngine: popped to level "
2928 << d_userContext
->getLevel() << endl
;
2929 // FIXME: should we reset d_status here?
2930 // SMT-LIBv2 spec seems to imply no, but it would make sense to..
2933 void SmtEngine::internalPush() {
2934 Assert(d_fullyInited
);
2935 Trace("smt") << "SmtEngine::internalPush()" << endl
;
2937 if(options::incrementalSolving()) {
2938 d_private
->processAssertions();
2939 TimerStat::CodeTimer
pushPopTimer(d_stats
->d_pushPopTime
);
2940 d_userContext
->push();
2941 // the d_context push is done inside of the SAT solver
2942 d_propEngine
->push();
2946 void SmtEngine::internalPop(bool immediate
) {
2947 Assert(d_fullyInited
);
2948 Trace("smt") << "SmtEngine::internalPop()" << endl
;
2949 if(options::incrementalSolving()) {
2957 void SmtEngine::doPendingPops() {
2958 Trace("smt") << "SmtEngine::doPendingPops()" << endl
;
2959 Assert(d_pendingPops
== 0 || options::incrementalSolving());
2960 // check to see if a postsolve() is pending
2961 if (d_needPostsolve
)
2963 d_propEngine
->resetTrail();
2965 while(d_pendingPops
> 0) {
2966 TimerStat::CodeTimer
pushPopTimer(d_stats
->d_pushPopTime
);
2967 d_propEngine
->pop();
2968 // the d_context pop is done inside of the SAT solver
2969 d_userContext
->pop();
2972 if (d_needPostsolve
)
2974 d_theoryEngine
->postsolve();
2975 d_needPostsolve
= false;
2979 void SmtEngine::reset()
2981 SmtScope
smts(this);
2982 ExprManager
*em
= d_exprManager
;
2983 Trace("smt") << "SMT reset()" << endl
;
2984 if(Dump
.isOn("benchmark")) {
2985 Dump("benchmark") << ResetCommand();
2988 opts
.copyValues(d_originalOptions
);
2990 new (this) SmtEngine(em
, &opts
);
2993 void SmtEngine::resetAssertions()
2995 SmtScope
smts(this);
2999 // We're still in Start Mode, nothing asserted yet, do nothing.
3000 // (see solver execution modes in the SMT-LIB standard)
3001 Assert(d_context
->getLevel() == 0);
3002 Assert(d_userContext
->getLevel() == 0);
3003 d_dumpm
->resetAssertions();
3009 Trace("smt") << "SMT resetAssertions()" << endl
;
3010 if (Dump
.isOn("benchmark"))
3012 Dump("benchmark") << ResetAssertionsCommand();
3015 while (!d_userLevels
.empty())
3020 // Remember the global push/pop around everything when beyond Start mode
3021 // (see solver execution modes in the SMT-LIB standard)
3022 Assert(d_userLevels
.size() == 0 && d_userContext
->getLevel() == 1);
3023 d_context
->popto(0);
3024 d_userContext
->popto(0);
3025 d_dumpm
->resetAssertions();
3026 d_userContext
->push();
3029 /* Create new PropEngine.
3030 * First force destruction of referenced PropEngine to enforce that
3031 * statistics are unregistered by the obsolete PropEngine object before
3032 * registered again by the new PropEngine object */
3033 d_propEngine
.reset(nullptr);
3034 d_propEngine
.reset(new PropEngine(
3035 getTheoryEngine(), getContext(), getUserContext(), getResourceManager()));
3036 d_theoryEngine
->setPropEngine(getPropEngine());
3039 void SmtEngine::interrupt()
3041 if(!d_fullyInited
) {
3044 d_propEngine
->interrupt();
3045 d_theoryEngine
->interrupt();
3048 void SmtEngine::setResourceLimit(unsigned long units
, bool cumulative
) {
3049 d_resourceManager
->setResourceLimit(units
, cumulative
);
3051 void SmtEngine::setTimeLimit(unsigned long milis
)
3053 d_resourceManager
->setTimeLimit(milis
);
3056 unsigned long SmtEngine::getResourceUsage() const {
3057 return d_resourceManager
->getResourceUsage();
3060 unsigned long SmtEngine::getTimeUsage() const {
3061 return d_resourceManager
->getTimeUsage();
3064 unsigned long SmtEngine::getResourceRemaining() const
3066 return d_resourceManager
->getResourceRemaining();
3069 NodeManager
* SmtEngine::getNodeManager() const
3071 return d_exprManager
->getNodeManager();
3074 Statistics
SmtEngine::getStatistics() const
3076 return Statistics(*d_statisticsRegistry
);
3079 SExpr
SmtEngine::getStatistic(std::string name
) const
3081 return d_statisticsRegistry
->getStatistic(name
);
3084 void SmtEngine::safeFlushStatistics(int fd
) const {
3085 d_statisticsRegistry
->safeFlushInformation(fd
);
3088 void SmtEngine::setUserAttribute(const std::string
& attr
,
3090 const std::vector
<Expr
>& expr_values
,
3091 const std::string
& str_value
)
3093 SmtScope
smts(this);
3094 finalOptionsAreSet();
3095 std::vector
<Node
> node_values
;
3096 for( unsigned i
=0; i
<expr_values
.size(); i
++ ){
3097 node_values
.push_back( expr_values
[i
].getNode() );
3099 d_theoryEngine
->setUserAttribute(attr
, expr
.getNode(), node_values
, str_value
);
3102 void SmtEngine::setOption(const std::string
& key
, const CVC4::SExpr
& value
)
3104 // Always check whether the SmtEngine has been initialized (which is done
3105 // upon entering Assert mode the first time). No option can be set after
3108 throw ModalException("SmtEngine::setOption called after initialization.");
3110 NodeManagerScope
nms(d_nodeManager
);
3111 Trace("smt") << "SMT setOption(" << key
<< ", " << value
<< ")" << endl
;
3113 if(Dump
.isOn("benchmark")) {
3114 Dump("benchmark") << SetOptionCommand(key
, value
);
3117 if(key
== "command-verbosity") {
3118 if(!value
.isAtom()) {
3119 const vector
<SExpr
>& cs
= value
.getChildren();
3120 if(cs
.size() == 2 &&
3121 (cs
[0].isKeyword() || cs
[0].isString()) &&
3122 cs
[1].isInteger()) {
3123 string c
= cs
[0].getValue();
3124 const Integer
& v
= cs
[1].getIntegerValue();
3125 if(v
< 0 || v
> 2) {
3126 throw OptionException("command-verbosity must be 0, 1, or 2");
3128 d_commandVerbosity
[c
] = v
;
3132 throw OptionException("command-verbosity value must be a tuple (command-name, integer)");
3135 if(!value
.isAtom()) {
3136 throw OptionException("bad value for :" + key
);
3139 string optionarg
= value
.getValue();
3140 d_options
.setOption(key
, optionarg
);
3143 void SmtEngine::setIsInternalSubsolver() { d_isInternalSubsolver
= true; }
3145 bool SmtEngine::isInternalSubsolver() const { return d_isInternalSubsolver
; }
3147 CVC4::SExpr
SmtEngine::getOption(const std::string
& key
) const
3149 NodeManagerScope
nms(d_nodeManager
);
3151 Trace("smt") << "SMT getOption(" << key
<< ")" << endl
;
3153 if(key
.length() >= 18 &&
3154 key
.compare(0, 18, "command-verbosity:") == 0) {
3155 map
<string
, Integer
>::const_iterator i
= d_commandVerbosity
.find(key
.c_str() + 18);
3156 if(i
!= d_commandVerbosity
.end()) {
3157 return SExpr((*i
).second
);
3159 i
= d_commandVerbosity
.find("*");
3160 if(i
!= d_commandVerbosity
.end()) {
3161 return SExpr((*i
).second
);
3163 return SExpr(Integer(2));
3166 if(Dump
.isOn("benchmark")) {
3167 Dump("benchmark") << GetOptionCommand(key
);
3170 if(key
== "command-verbosity") {
3171 vector
<SExpr
> result
;
3172 SExpr defaultVerbosity
;
3173 for(map
<string
, Integer
>::const_iterator i
= d_commandVerbosity
.begin();
3174 i
!= d_commandVerbosity
.end();
3177 v
.push_back(SExpr((*i
).first
));
3178 v
.push_back(SExpr((*i
).second
));
3179 if((*i
).first
== "*") {
3180 // put the default at the end of the SExpr
3181 defaultVerbosity
= SExpr(v
);
3183 result
.push_back(SExpr(v
));
3186 // put the default at the end of the SExpr
3187 if(!defaultVerbosity
.isAtom()) {
3188 result
.push_back(defaultVerbosity
);
3190 // ensure the default is always listed
3192 v
.push_back(SExpr("*"));
3193 v
.push_back(SExpr(Integer(2)));
3194 result
.push_back(SExpr(v
));
3196 return SExpr(result
);
3199 return SExpr::parseAtom(d_options
.getOption(key
));
3202 bool SmtEngine::getExpressionName(const Node
& e
, std::string
& name
) const {
3203 return d_exprNames
->getExpressionName(e
, name
);
3206 void SmtEngine::setExpressionName(const Node
& e
, const std::string
& name
) {
3207 Trace("smt-debug") << "Set expression name " << e
<< " to " << name
<< std::endl
;
3208 d_exprNames
->setExpressionName(e
,name
);
3211 Options
& SmtEngine::getOptions() { return d_options
; }
3213 const Options
& SmtEngine::getOptions() const { return d_options
; }
3215 ResourceManager
* SmtEngine::getResourceManager()
3217 return d_resourceManager
.get();
3220 DumpManager
* SmtEngine::getDumpManager() { return d_dumpm
.get(); }
3222 void SmtEngine::setSygusConjectureStale()
3224 if (d_private
->d_sygusConjectureStale
)
3229 d_private
->d_sygusConjectureStale
= true;
3230 if (options::incrementalSolving())
3236 }/* CVC4 namespace */