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/command.h"
86 #include "smt/command_list.h"
87 #include "smt/defined_function.h"
88 #include "smt/listeners.h"
89 #include "smt/logic_request.h"
90 #include "smt/model_blocker.h"
91 #include "smt/model_core_builder.h"
92 #include "smt/options_manager.h"
93 #include "smt/process_assertions.h"
94 #include "smt/smt_engine_scope.h"
95 #include "smt/smt_engine_stats.h"
96 #include "smt/term_formula_removal.h"
97 #include "smt/update_ostream.h"
98 #include "smt_util/boolean_simplification.h"
99 #include "smt_util/nary_builder.h"
100 #include "theory/booleans/circuit_propagator.h"
101 #include "theory/bv/theory_bv_rewriter.h"
102 #include "theory/logic_info.h"
103 #include "theory/quantifiers/fun_def_process.h"
104 #include "theory/quantifiers/single_inv_partition.h"
105 #include "theory/quantifiers/sygus/synth_engine.h"
106 #include "theory/quantifiers/term_util.h"
107 #include "theory/quantifiers_engine.h"
108 #include "theory/rewriter.h"
109 #include "theory/sort_inference.h"
110 #include "theory/strings/theory_strings.h"
111 #include "theory/substitutions.h"
112 #include "theory/theory_engine.h"
113 #include "theory/theory_model.h"
114 #include "theory/theory_traits.h"
115 #include "util/hash.h"
116 #include "util/proof.h"
117 #include "util/random.h"
118 #include "util/resource_manager.h"
120 #if (IS_LFSC_BUILD && IS_PROOFS_BUILD)
125 using namespace CVC4
;
126 using namespace CVC4::smt
;
127 using namespace CVC4::preprocessing
;
128 using namespace CVC4::prop
;
129 using namespace CVC4::context
;
130 using namespace CVC4::theory
;
135 extern const char* const plf_signatures
;
140 struct DeleteCommandFunction
: public std::unary_function
<const Command
*, void>
142 void operator()(const Command
* command
) { delete command
; }
145 void DeleteAndClearCommandVector(std::vector
<Command
*>& commands
) {
146 std::for_each(commands
.begin(), commands
.end(), DeleteCommandFunction());
151 * This is an inelegant solution, but for the present, it will work.
152 * The point of this is to separate the public and private portions of
153 * the SmtEngine class, so that smt_engine.h doesn't
154 * include "expr/node.h", which is a private CVC4 header (and can lead
155 * to linking errors due to the improper inlining of non-visible symbols
158 * The "real" solution (that which is usually implemented) is to move
159 * ALL the implementation to SmtEnginePrivate and maintain a
160 * heap-allocated instance of it in SmtEngine. SmtEngine (the public
161 * one) becomes an "interface shell" which simply acts as a forwarder
164 class SmtEnginePrivate
168 typedef unordered_map
<Node
, Node
, NodeHashFunction
> NodeToNodeHashMap
;
169 typedef unordered_map
<Node
, bool, NodeHashFunction
> NodeToBoolHashMap
;
171 /** A circuit propagator for non-clausal propositional deduction */
172 booleans::CircuitPropagator d_propagator
;
174 /** Assertions in the preprocessing pipeline */
175 AssertionPipeline d_assertions
;
177 /** Whether any assertions have been processed */
178 CDO
<bool> d_assertionsProcessed
;
183 /** The preprocessing pass context */
184 std::unique_ptr
<PreprocessingPassContext
> d_preprocessingPassContext
;
186 /** Process assertions module */
187 ProcessAssertions d_processor
;
189 //------------------------------- expression names
190 /** mapping from expressions to name */
191 context::CDHashMap
< Node
, std::string
, NodeHashFunction
> d_exprNames
;
192 //------------------------------- end expression names
194 IteSkolemMap
& getIteSkolemMap() { return d_assertions
.getIteSkolemMap(); }
196 /** Instance of the ITE remover */
197 RemoveTermFormulas d_iteRemover
;
199 /* Finishes the initialization of the private portion of SMTEngine. */
202 /*------------------- sygus utils ------------------*/
204 * sygus variables declared (from "declare-var" and "declare-fun" commands)
206 * The SyGuS semantics for declared variables is that they are implicitly
207 * universally quantified in the constraints.
209 std::vector
<Node
> d_sygusVars
;
210 /** sygus constraints */
211 std::vector
<Node
> d_sygusConstraints
;
212 /** functions-to-synthesize */
213 std::vector
<Node
> d_sygusFunSymbols
;
215 * Whether we need to reconstruct the sygus conjecture.
217 CDO
<bool> d_sygusConjectureStale
;
218 /*------------------- end of sygus utils ------------------*/
221 SmtEnginePrivate(SmtEngine
& smt
)
223 d_propagator(true, true),
225 d_assertionsProcessed(smt
.getUserContext(), false),
226 d_processor(smt
, *smt
.getResourceManager()),
227 d_exprNames(smt
.getUserContext()),
228 d_iteRemover(smt
.getUserContext()),
229 d_sygusConjectureStale(smt
.getUserContext(), true)
231 d_true
= NodeManager::currentNM()->mkConst(true);
236 if(d_propagator
.getNeedsFinish()) {
237 d_propagator
.finish();
238 d_propagator
.setNeedsFinish(false);
242 void spendResource(ResourceManager::Resource r
)
244 d_smt
.getResourceManager()->spendResource(r
);
247 ProcessAssertions
* getProcessAssertions() { return &d_processor
; }
249 Node
applySubstitutions(TNode node
)
251 return Rewriter::rewrite(
252 d_preprocessingPassContext
->getTopLevelSubstitutions().apply(node
));
256 * Process the assertions that have been asserted.
258 void processAssertions();
260 /** Process a user push.
267 * Process a user pop. Clears out the non-context-dependent stuff in this
268 * SmtEnginePrivate. Necessary to clear out our assertion vectors in case
269 * someone does a push-assert-pop without a check-sat. It also pops the
270 * last map of expression names from notifyPush.
273 d_assertions
.clear();
274 d_propagator
.getLearnedLiterals().clear();
275 getIteSkolemMap().clear();
279 * Adds a formula to the current context. Action here depends on
280 * the SimplificationMode (in the current Options scope); the
281 * formula might be pushed out to the propositional layer
282 * immediately, or it might be simplified and kept, or it might not
283 * even be simplified.
284 * The arguments isInput and isAssumption are used for bookkeeping for proofs.
285 * The argument maybeHasFv should be set to true if the assertion may have
286 * free variables. By construction, assertions from the smt2 parser are
287 * guaranteed not to have free variables. However, other cases such as
288 * assertions from the SyGuS parser may have free variables (say if the
289 * input contains an assert or define-fun-rec command).
291 * @param isAssumption If true, the formula is considered to be an assumption
292 * (this is used to distinguish assertions and assumptions)
294 void addFormula(TNode n
,
297 bool isAssumption
= false,
298 bool maybeHasFv
= false);
300 * Simplify node "in" by expanding definitions and applying any
301 * substitutions learned from preprocessing.
303 Node
simplify(TNode in
) {
304 // Substitute out any abstract values in ex.
305 // Expand definitions.
306 NodeToNodeHashMap cache
;
307 Node n
= d_processor
.expandDefinitions(in
, cache
).toExpr();
308 // Make sure we've done all preprocessing, etc.
309 Assert(d_assertions
.size() == 0);
310 return applySubstitutions(n
).toExpr();
313 //------------------------------- expression names
314 // implements setExpressionName, as described in smt_engine.h
315 void setExpressionName(Expr e
, std::string name
) {
316 d_exprNames
[Node::fromExpr(e
)] = name
;
319 // implements getExpressionName, as described in smt_engine.h
320 bool getExpressionName(Expr e
, std::string
& name
) const {
321 context::CDHashMap
< Node
, std::string
, NodeHashFunction
>::const_iterator it
= d_exprNames
.find(e
);
322 if(it
!=d_exprNames
.end()) {
329 //------------------------------- end expression names
330 };/* class SmtEnginePrivate */
332 }/* namespace CVC4::smt */
334 SmtEngine::SmtEngine(ExprManager
* em
, Options
* optr
)
335 : d_context(new Context()),
336 d_userContext(new UserContext()),
339 d_nodeManager(d_exprManager
->getNodeManager()),
340 d_absValues(new AbstractValues(d_nodeManager
)),
341 d_routListener(new ResourceOutListener(*this)),
342 d_snmListener(new SmtNodeManagerListener(*this)),
343 d_theoryEngine(nullptr),
344 d_propEngine(nullptr),
345 d_proofManager(nullptr),
346 d_rewriter(new theory::Rewriter()),
347 d_definedFunctions(nullptr),
348 d_abductSolver(nullptr),
349 d_assertionList(nullptr),
350 d_assignments(nullptr),
351 d_modelGlobalCommands(),
352 d_modelCommands(nullptr),
357 d_isInternalSubsolver(false),
359 d_fullyInited(false),
361 d_needPostsolve(false),
362 d_globalNegation(false),
365 d_smtMode(SMT_MODE_START
),
367 d_statisticsRegistry(nullptr),
369 d_resourceManager(nullptr),
372 // !!!!!!!!!!!!!!!!!!!!!! temporary hack: this makes the current SmtEngine
373 // we are constructing the current SmtEngine in scope for the lifetime of
374 // this SmtEngine, or until another SmtEngine is constructed (that SmtEngine
375 // is then in scope during its lifetime). This is mostly to ensure that
376 // options are always in scope, for e.g. printing expressions, which rely
377 // on knowing the output language.
378 // Notice that the SmtEngine may spawn new SmtEngine "subsolvers" internally.
379 // These are created, used, and deleted in a modular fashion while not
380 // interleaving calls to the master SmtEngine. Thus the hack here does not
381 // break this use case.
382 // On the other hand, this hack breaks use cases where multiple SmtEngine
383 // objects are created by the user.
384 d_scope
.reset(new SmtScope(this));
387 // if we provided a set of options, copy their values to the options
388 // owned by this SmtEngine.
389 d_options
.copyValues(*optr
);
391 d_statisticsRegistry
.reset(new StatisticsRegistry());
392 d_resourceManager
.reset(
393 new ResourceManager(*d_statisticsRegistry
.get(), d_options
));
394 d_optm
.reset(new smt::OptionsManager(&d_options
, d_resourceManager
.get()));
395 d_private
.reset(new smt::SmtEnginePrivate(*this));
396 // listen to node manager events
397 d_nodeManager
->subscribeEvents(d_snmListener
.get());
398 // listen to resource out
399 d_resourceManager
->registerListener(d_routListener
.get());
401 d_stats
.reset(new SmtEngineStatistics());
403 // The ProofManager is constructed before any other proof objects such as
404 // SatProof and TheoryProofs. The TheoryProofEngine and the SatProof are
405 // initialized in TheoryEngine and PropEngine respectively.
406 Assert(d_proofManager
== nullptr);
408 // d_proofManager must be created before Options has been finished
409 // being parsed from the input file. Because of this, we cannot trust
410 // that options::proof() is set correctly yet.
412 d_proofManager
.reset(new ProofManager(getUserContext()));
415 d_definedFunctions
= new (true) DefinedFunctionMap(getUserContext());
416 d_modelCommands
= new (true) smt::CommandList(getUserContext());
419 void SmtEngine::finishInit()
421 // Notice that finishInit is called when options are finalized. If we are
422 // parsing smt2, this occurs at the moment we enter "Assert mode", page 52
423 // of SMT-LIB 2.6 standard.
425 // set the random seed
426 Random::getRandom().setSeed(options::seed());
428 // Call finish init on the options manager. This inializes the resource
429 // manager based on the options, and sets up the best default options
430 // based on our heuristics.
431 d_optm
->finishInit(d_logic
, d_isInternalSubsolver
);
433 Trace("smt-debug") << "SmtEngine::finishInit" << std::endl
;
434 // We have mutual dependency here, so we add the prop engine to the theory
435 // engine later (it is non-essential there)
436 d_theoryEngine
.reset(new TheoryEngine(getContext(),
438 getResourceManager(),
439 d_private
->d_iteRemover
,
440 const_cast<const LogicInfo
&>(d_logic
)));
443 for(TheoryId id
= theory::THEORY_FIRST
; id
< theory::THEORY_LAST
; ++id
) {
444 TheoryConstructor::addTheory(getTheoryEngine(), id
);
445 //register with proof engine if applicable
447 ProofManager::currentPM()->getTheoryProofEngine()->registerTheory(d_theoryEngine
->theoryOf(id
));
451 Trace("smt-debug") << "Making decision engine..." << std::endl
;
453 Trace("smt-debug") << "Making prop engine..." << std::endl
;
454 /* force destruction of referenced PropEngine to enforce that statistics
455 * are unregistered by the obsolete PropEngine object before registered
456 * again by the new PropEngine object */
457 d_propEngine
.reset(nullptr);
458 d_propEngine
.reset(new PropEngine(
459 getTheoryEngine(), getContext(), getUserContext(), getResourceManager()));
461 Trace("smt-debug") << "Setting up theory engine..." << std::endl
;
462 d_theoryEngine
->setPropEngine(getPropEngine());
463 Trace("smt-debug") << "Finishing init for theory engine..." << std::endl
;
464 d_theoryEngine
->finishInit();
466 // global push/pop around everything, to ensure proper destruction
467 // of context-dependent data structures
468 d_userContext
->push();
471 Trace("smt-debug") << "Set up assertion list..." << std::endl
;
472 // [MGD 10/20/2011] keep around in incremental mode, due to a
473 // cleanup ordering issue and Nodes/TNodes. If SAT is popped
474 // first, some user-context-dependent TNodes might still exist
476 if(options::produceAssertions() ||
477 options::incrementalSolving()) {
478 // In the case of incremental solving, we appear to need these to
479 // ensure the relevant Nodes remain live.
480 d_assertionList
= new (true) AssertionList(getUserContext());
481 d_globalDefineFunRecLemmas
.reset(new std::vector
<Node
>());
484 // dump out a set-logic command only when raw-benchmark is disabled to avoid
485 // dumping the command twice.
486 if (Dump
.isOn("benchmark") && !Dump
.isOn("raw-benchmark"))
488 LogicInfo everything
;
490 Dump("benchmark") << CommentCommand(
491 "CVC4 always dumps the most general, all-supported logic (below), as "
492 "some internals might require the use of a logic more general than "
494 << SetBenchmarkLogicCommand(
495 everything
.getLogicString());
498 Trace("smt-debug") << "Dump declaration commands..." << std::endl
;
499 // dump out any pending declaration commands
500 for(unsigned i
= 0; i
< d_dumpCommands
.size(); ++i
) {
501 Dump("declarations") << *d_dumpCommands
[i
];
502 delete d_dumpCommands
[i
];
504 d_dumpCommands
.clear();
507 if (options::produceAbducts())
509 d_abductSolver
.reset(new AbductionSolver(this));
512 PROOF( ProofManager::currentPM()->setLogic(d_logic
); );
514 for(TheoryId id
= theory::THEORY_FIRST
; id
< theory::THEORY_LAST
; ++id
) {
515 ProofManager::currentPM()->getTheoryProofEngine()->
516 finishRegisterTheory(d_theoryEngine
->theoryOf(id
));
519 d_private
->finishInit();
520 Trace("smt-debug") << "SmtEngine::finishInit done" << std::endl
;
523 void SmtEngine::finalOptionsAreSet() {
528 if(! d_logic
.isLocked()) {
532 // finish initialization, create the prop engine, etc.
535 AlwaysAssert(d_propEngine
->getAssertionLevel() == 0)
536 << "The PropEngine has pushed but the SmtEngine "
537 "hasn't finished initializing!";
539 d_fullyInited
= true;
540 Assert(d_logic
.isLocked());
543 void SmtEngine::shutdown() {
546 while(options::incrementalSolving() && d_userContext
->getLevel() > 1) {
550 if (d_propEngine
!= nullptr)
552 d_propEngine
->shutdown();
554 if (d_theoryEngine
!= nullptr)
556 d_theoryEngine
->shutdown();
560 SmtEngine::~SmtEngine()
567 // global push/pop around everything, to ensure proper destruction
568 // of context-dependent data structures
570 d_userContext
->popto(0);
572 if(d_assignments
!= NULL
) {
573 d_assignments
->deleteSelf();
576 d_globalDefineFunRecLemmas
.reset();
578 if(d_assertionList
!= NULL
) {
579 d_assertionList
->deleteSelf();
582 for(unsigned i
= 0; i
< d_dumpCommands
.size(); ++i
) {
583 delete d_dumpCommands
[i
];
584 d_dumpCommands
[i
] = NULL
;
586 d_dumpCommands
.clear();
588 DeleteAndClearCommandVector(d_modelGlobalCommands
);
590 if(d_modelCommands
!= NULL
) {
591 d_modelCommands
->deleteSelf();
594 d_definedFunctions
->deleteSelf();
596 //destroy all passes before destroying things that they refer to
597 d_private
->getProcessAssertions()->cleanup();
599 // d_proofManager is always created when proofs are enabled at configure
600 // time. Because of this, this code should not be wrapped in PROOF() which
601 // additionally checks flags such as options::proof().
603 // Note: the proof manager must be destroyed before the theory engine.
604 // Because the destruction of the proofs depends on contexts owned be the
607 d_proofManager
.reset(nullptr);
610 d_absValues
.reset(nullptr);
612 d_theoryEngine
.reset(nullptr);
613 d_propEngine
.reset(nullptr);
615 d_stats
.reset(nullptr);
616 d_private
.reset(nullptr);
617 d_nodeManager
->unsubscribeEvents(d_snmListener
.get());
618 d_snmListener
.reset(nullptr);
619 d_routListener
.reset(nullptr);
620 d_optm
.reset(nullptr);
621 // d_resourceManager must be destroyed before d_statisticsRegistry
622 d_resourceManager
.reset(nullptr);
623 d_statisticsRegistry
.reset(nullptr);
626 d_userContext
.reset(nullptr);
627 d_context
.reset(nullptr);
628 } catch(Exception
& e
) {
629 Warning() << "CVC4 threw an exception during cleanup." << endl
634 void SmtEngine::setLogic(const LogicInfo
& logic
)
638 throw ModalException("Cannot set logic in SmtEngine after the engine has "
639 "finished initializing.");
646 void SmtEngine::setLogic(const std::string
& s
)
651 setLogic(LogicInfo(s
));
652 // dump out a set-logic command
653 if (Dump
.isOn("raw-benchmark"))
655 Dump("raw-benchmark")
656 << SetBenchmarkLogicCommand(d_logic
.getLogicString());
659 catch (IllegalArgumentException
& e
)
661 throw LogicException(e
.what());
665 void SmtEngine::setLogic(const char* logic
) { setLogic(string(logic
)); }
666 LogicInfo
SmtEngine::getLogicInfo() const {
670 LogicInfo
SmtEngine::getUserLogicInfo() const
672 // Lock the logic to make sure that this logic can be queried. We create a
673 // copy of the user logic here to keep this method const.
674 LogicInfo res
= d_userLogic
;
679 void SmtEngine::notifyStartParsing(std::string filename
)
681 d_filename
= filename
;
683 // Copy the original options. This is called prior to beginning parsing.
684 // Hence reset should revert to these options, which note is after reading
686 d_originalOptions
.copyValues(d_options
);
689 std::string
SmtEngine::getFilename() const { return d_filename
; }
690 void SmtEngine::setLogicInternal()
692 Assert(!d_fullyInited
)
693 << "setting logic in SmtEngine but the engine has already"
694 " finished initializing for this run";
699 void SmtEngine::setProblemExtended()
701 d_smtMode
= SMT_MODE_ASSERT
;
702 d_assumptions
.clear();
705 void SmtEngine::setInfo(const std::string
& key
, const CVC4::SExpr
& value
)
709 Trace("smt") << "SMT setInfo(" << key
<< ", " << value
<< ")" << endl
;
711 if(Dump
.isOn("benchmark")) {
712 if(key
== "status") {
713 string s
= value
.getValue();
714 BenchmarkStatus status
=
715 (s
== "sat") ? SMT_SATISFIABLE
:
716 ((s
== "unsat") ? SMT_UNSATISFIABLE
: SMT_UNKNOWN
);
717 Dump("benchmark") << SetBenchmarkStatusCommand(status
);
719 Dump("benchmark") << SetInfoCommand(key
, value
);
723 // Check for standard info keys (SMT-LIB v1, SMT-LIB v2, ...)
724 if (key
== "source" || key
== "category" || key
== "difficulty"
725 || key
== "notes" || key
== "name" || key
== "license")
730 else if (key
== "filename")
732 d_filename
= value
.getValue();
735 else if (key
== "smt-lib-version" && !options::inputLanguage
.wasSetByUser())
737 language::input::Language ilang
= language::input::LANG_AUTO
;
738 if( (value
.isInteger() && value
.getIntegerValue() == Integer(2)) ||
739 (value
.isRational() && value
.getRationalValue() == Rational(2)) ||
740 value
.getValue() == "2" ||
741 value
.getValue() == "2.0" ) {
742 ilang
= language::input::LANG_SMTLIB_V2_0
;
743 } else if( (value
.isRational() && value
.getRationalValue() == Rational(5, 2)) ||
744 value
.getValue() == "2.5" ) {
745 ilang
= language::input::LANG_SMTLIB_V2_5
;
746 } else if( (value
.isRational() && value
.getRationalValue() == Rational(13, 5)) ||
747 value
.getValue() == "2.6" ) {
748 ilang
= language::input::LANG_SMTLIB_V2_6
;
752 Warning() << "Warning: unsupported smt-lib-version: " << value
<< endl
;
753 throw UnrecognizedOptionException();
755 options::inputLanguage
.set(ilang
);
756 // also update the output language
757 if (!options::outputLanguage
.wasSetByUser())
759 language::output::Language olang
= language::toOutputLanguage(ilang
);
760 if (options::outputLanguage() != olang
)
762 options::outputLanguage
.set(olang
);
763 *options::out() << language::SetLanguage(olang
);
767 } else if(key
== "status") {
770 s
= value
.getValue();
772 if(s
!= "sat" && s
!= "unsat" && s
!= "unknown") {
773 throw OptionException("argument to (set-info :status ..) must be "
774 "`sat' or `unsat' or `unknown'");
776 d_expectedStatus
= Result(s
, d_filename
);
779 throw UnrecognizedOptionException();
782 bool SmtEngine::isValidGetInfoFlag(const std::string
& key
) const
784 if (key
== "all-statistics" || key
== "error-behavior" || key
== "name"
785 || key
== "version" || key
== "authors" || key
== "status"
786 || key
== "reason-unknown" || key
== "assertion-stack-levels"
787 || key
== "all-options")
794 CVC4::SExpr
SmtEngine::getInfo(const std::string
& key
) const
798 Trace("smt") << "SMT getInfo(" << key
<< ")" << endl
;
799 if (!isValidGetInfoFlag(key
))
801 throw UnrecognizedOptionException();
803 if (key
== "all-statistics")
806 for (StatisticsRegistry::const_iterator i
=
807 NodeManager::fromExprManager(d_exprManager
)
808 ->getStatisticsRegistry()
811 != NodeManager::fromExprManager(d_exprManager
)
812 ->getStatisticsRegistry()
817 v
.push_back((*i
).first
);
818 v
.push_back((*i
).second
);
821 for (StatisticsRegistry::const_iterator i
= d_statisticsRegistry
->begin();
822 i
!= d_statisticsRegistry
->end();
826 v
.push_back((*i
).first
);
827 v
.push_back((*i
).second
);
832 if (key
== "error-behavior")
834 return SExpr(SExpr::Keyword("immediate-exit"));
838 return SExpr(Configuration::getName());
840 if (key
== "version")
842 return SExpr(Configuration::getVersionString());
844 if (key
== "authors")
846 return SExpr(Configuration::about());
850 // sat | unsat | unknown
851 switch (d_status
.asSatisfiabilityResult().isSat())
853 case Result::SAT
: return SExpr(SExpr::Keyword("sat"));
854 case Result::UNSAT
: return SExpr(SExpr::Keyword("unsat"));
855 default: return SExpr(SExpr::Keyword("unknown"));
858 if (key
== "reason-unknown")
860 if (!d_status
.isNull() && d_status
.isUnknown())
863 ss
<< d_status
.whyUnknown();
865 transform(s
.begin(), s
.end(), s
.begin(), ::tolower
);
866 return SExpr(SExpr::Keyword(s
));
870 throw RecoverableModalException(
871 "Can't get-info :reason-unknown when the "
872 "last result wasn't unknown!");
875 if (key
== "assertion-stack-levels")
877 AlwaysAssert(d_userLevels
.size()
878 <= std::numeric_limits
<unsigned long int>::max());
879 return SExpr(static_cast<unsigned long int>(d_userLevels
.size()));
881 Assert(key
== "all-options");
882 // get the options, like all-statistics
883 std::vector
<std::vector
<std::string
>> current_options
=
884 Options::current()->getOptions();
885 return SExpr::parseListOfListOfAtoms(current_options
);
888 void SmtEngine::debugCheckFormals(const std::vector
<Expr
>& formals
, Expr func
)
890 for(std::vector
<Expr
>::const_iterator i
= formals
.begin(); i
!= formals
.end(); ++i
) {
891 if((*i
).getKind() != kind::BOUND_VARIABLE
) {
893 ss
<< "All formal arguments to defined functions must be BOUND_VARIABLEs, but in the\n"
894 << "definition of function " << func
<< ", formal\n"
896 << "has kind " << (*i
).getKind();
897 throw TypeCheckingException(func
, ss
.str());
902 void SmtEngine::debugCheckFunctionBody(Expr formula
,
903 const std::vector
<Expr
>& formals
,
906 Type formulaType
= formula
.getType(options::typeChecking());
907 Type funcType
= func
.getType();
908 // We distinguish here between definitions of constants and functions,
909 // because the type checking for them is subtly different. Perhaps we
910 // should instead have SmtEngine::defineFunction() and
911 // SmtEngine::defineConstant() for better clarity, although then that
912 // doesn't match the SMT-LIBv2 standard...
913 if(formals
.size() > 0) {
914 Type rangeType
= FunctionType(funcType
).getRangeType();
915 if(! formulaType
.isComparableTo(rangeType
)) {
917 ss
<< "Type of defined function does not match its declaration\n"
918 << "The function : " << func
<< "\n"
919 << "Declared type : " << rangeType
<< "\n"
920 << "The body : " << formula
<< "\n"
921 << "Body type : " << formulaType
;
922 throw TypeCheckingException(func
, ss
.str());
925 if(! formulaType
.isComparableTo(funcType
)) {
927 ss
<< "Declared type of defined constant does not match its definition\n"
928 << "The constant : " << func
<< "\n"
929 << "Declared type : " << funcType
<< " " << Type::getTypeNode(funcType
)->getId() << "\n"
930 << "The definition : " << formula
<< "\n"
931 << "Definition type: " << formulaType
<< " " << Type::getTypeNode(formulaType
)->getId();
932 throw TypeCheckingException(func
, ss
.str());
937 void SmtEngine::defineFunction(Expr func
,
938 const std::vector
<Expr
>& formals
,
943 finalOptionsAreSet();
945 Trace("smt") << "SMT defineFunction(" << func
<< ")" << endl
;
946 debugCheckFormals(formals
, func
);
949 ss
<< language::SetLanguage(
950 language::SetLanguage::getLanguage(Dump
.getStream()))
952 DefineFunctionCommand
c(ss
.str(), func
, formals
, formula
, global
);
953 addToModelCommandAndDump(
954 c
, ExprManager::VAR_FLAG_DEFINED
, true, "declarations");
956 PROOF(if (options::checkUnsatCores()) {
957 d_defineCommands
.push_back(c
.clone());
961 debugCheckFunctionBody(formula
, formals
, func
);
963 // Substitute out any abstract values in formula
964 Node formNode
= d_absValues
->substituteAbstractValues(Node::fromExpr(formula
));
966 TNode funcNode
= func
.getTNode();
967 vector
<Node
> formalsNodes
;
968 for(vector
<Expr
>::const_iterator i
= formals
.begin(),
969 iend
= formals
.end();
972 formalsNodes
.push_back((*i
).getNode());
974 DefinedFunction
def(funcNode
, formalsNodes
, formNode
);
975 // Permit (check-sat) (define-fun ...) (get-value ...) sequences.
976 // Otherwise, (check-sat) (get-value ((! foo :named bar))) breaks
977 // d_haveAdditions = true;
978 Debug("smt") << "definedFunctions insert " << funcNode
<< " " << formNode
<< endl
;
982 d_definedFunctions
->insertAtContextLevelZero(funcNode
, def
);
986 d_definedFunctions
->insert(funcNode
, def
);
990 void SmtEngine::defineFunctionsRec(
991 const std::vector
<Expr
>& funcs
,
992 const std::vector
<std::vector
<Expr
>>& formals
,
993 const std::vector
<Expr
>& formulas
,
997 finalOptionsAreSet();
999 Trace("smt") << "SMT defineFunctionsRec(...)" << endl
;
1001 if (funcs
.size() != formals
.size() && funcs
.size() != formulas
.size())
1004 ss
<< "Number of functions, formals, and function bodies passed to "
1005 "defineFunctionsRec do not match:"
1007 << " #functions : " << funcs
.size() << "\n"
1008 << " #arg lists : " << formals
.size() << "\n"
1009 << " #function bodies : " << formulas
.size() << "\n";
1010 throw ModalException(ss
.str());
1012 for (unsigned i
= 0, size
= funcs
.size(); i
< size
; i
++)
1014 // check formal argument list
1015 debugCheckFormals(formals
[i
], funcs
[i
]);
1017 debugCheckFunctionBody(formulas
[i
], formals
[i
], funcs
[i
]);
1020 if (Dump
.isOn("raw-benchmark"))
1022 std::vector
<api::Term
> tFuncs
= api::exprVectorToTerms(d_solver
, funcs
);
1023 std::vector
<std::vector
<api::Term
>> tFormals
;
1024 for (const std::vector
<Expr
>& formal
: formals
)
1026 tFormals
.emplace_back(api::exprVectorToTerms(d_solver
, formal
));
1028 std::vector
<api::Term
> tFormulas
=
1029 api::exprVectorToTerms(d_solver
, formulas
);
1030 Dump("raw-benchmark") << DefineFunctionRecCommand(
1031 d_solver
, tFuncs
, tFormals
, tFormulas
, global
);
1034 ExprManager
* em
= getExprManager();
1035 bool maybeHasFv
= language::isInputLangSygus(options::inputLanguage());
1036 for (unsigned i
= 0, size
= funcs
.size(); i
< size
; i
++)
1038 // we assert a quantified formula
1040 // make the function application
1041 if (formals
[i
].empty())
1043 // it has no arguments
1044 func_app
= funcs
[i
];
1048 std::vector
<Expr
> children
;
1049 children
.push_back(funcs
[i
]);
1050 children
.insert(children
.end(), formals
[i
].begin(), formals
[i
].end());
1051 func_app
= em
->mkExpr(kind::APPLY_UF
, children
);
1053 Expr lem
= em
->mkExpr(kind::EQUAL
, func_app
, formulas
[i
]);
1054 if (!formals
[i
].empty())
1056 // set the attribute to denote this is a function definition
1057 std::string
attr_name("fun-def");
1058 Expr aexpr
= em
->mkExpr(kind::INST_ATTRIBUTE
, func_app
);
1059 aexpr
= em
->mkExpr(kind::INST_PATTERN_LIST
, aexpr
);
1060 std::vector
<Expr
> expr_values
;
1061 std::string str_value
;
1062 setUserAttribute(attr_name
, func_app
, expr_values
, str_value
);
1063 // make the quantified formula
1064 Expr boundVars
= em
->mkExpr(kind::BOUND_VAR_LIST
, formals
[i
]);
1065 lem
= em
->mkExpr(kind::FORALL
, boundVars
, lem
, aexpr
);
1067 // assert the quantified formula
1068 // notice we don't call assertFormula directly, since this would
1069 // duplicate the output on raw-benchmark.
1070 Node n
= d_absValues
->substituteAbstractValues(Node::fromExpr(lem
));
1071 if (d_assertionList
!= nullptr)
1073 d_assertionList
->push_back(n
);
1075 if (global
&& d_globalDefineFunRecLemmas
!= nullptr)
1077 // Global definitions are asserted at check-sat-time because we have to
1078 // make sure that they are always present
1079 Assert(!language::isInputLangSygus(options::inputLanguage()));
1080 d_globalDefineFunRecLemmas
->emplace_back(n
);
1084 d_private
->addFormula(n
, false, true, false, maybeHasFv
);
1089 void SmtEngine::defineFunctionRec(Expr func
,
1090 const std::vector
<Expr
>& formals
,
1094 std::vector
<Expr
> funcs
;
1095 funcs
.push_back(func
);
1096 std::vector
<std::vector
<Expr
> > formals_multi
;
1097 formals_multi
.push_back(formals
);
1098 std::vector
<Expr
> formulas
;
1099 formulas
.push_back(formula
);
1100 defineFunctionsRec(funcs
, formals_multi
, formulas
, global
);
1103 bool SmtEngine::isDefinedFunction( Expr func
){
1104 Node nf
= Node::fromExpr( func
);
1105 Debug("smt") << "isDefined function " << nf
<< "?" << std::endl
;
1106 return d_definedFunctions
->find(nf
) != d_definedFunctions
->end();
1109 void SmtEnginePrivate::finishInit()
1111 d_preprocessingPassContext
.reset(
1112 new PreprocessingPassContext(&d_smt
, &d_iteRemover
, &d_propagator
));
1114 // initialize the preprocessing passes
1115 d_processor
.finishInit(d_preprocessingPassContext
.get());
1118 Result
SmtEngine::check() {
1119 Assert(d_fullyInited
);
1120 Assert(d_pendingPops
== 0);
1122 Trace("smt") << "SmtEngine::check()" << endl
;
1125 if (d_resourceManager
->out())
1127 Result::UnknownExplanation why
= d_resourceManager
->outOfResources()
1128 ? Result::RESOURCEOUT
1130 return Result(Result::ENTAILMENT_UNKNOWN
, why
, d_filename
);
1132 d_resourceManager
->beginCall();
1134 // Make sure the prop layer has all of the assertions
1135 Trace("smt") << "SmtEngine::check(): processing assertions" << endl
;
1136 d_private
->processAssertions();
1137 Trace("smt") << "SmtEngine::check(): done processing assertions" << endl
;
1139 TimerStat::CodeTimer
solveTimer(d_stats
->d_solveTime
);
1141 Chat() << "solving..." << endl
;
1142 Trace("smt") << "SmtEngine::check(): running check" << endl
;
1143 Result result
= d_propEngine
->checkSat();
1145 d_resourceManager
->endCall();
1146 Trace("limit") << "SmtEngine::check(): cumulative millis "
1147 << d_resourceManager
->getTimeUsage() << ", resources "
1148 << d_resourceManager
->getResourceUsage() << endl
;
1150 return Result(result
, d_filename
);
1153 Result
SmtEngine::quickCheck() {
1154 Assert(d_fullyInited
);
1155 Trace("smt") << "SMT quickCheck()" << endl
;
1157 Result::ENTAILMENT_UNKNOWN
, Result::REQUIRES_FULL_CHECK
, d_filename
);
1160 theory::TheoryModel
* SmtEngine::getAvailableModel(const char* c
) const
1162 if (!options::assignFunctionValues())
1164 std::stringstream ss
;
1165 ss
<< "Cannot " << c
<< " when --assign-function-values is false.";
1166 throw RecoverableModalException(ss
.str().c_str());
1169 if (d_smtMode
!= SMT_MODE_SAT
&& d_smtMode
!= SMT_MODE_SAT_UNKNOWN
)
1171 std::stringstream ss
;
1172 ss
<< "Cannot " << c
1173 << " unless immediately preceded by SAT/NOT_ENTAILED or UNKNOWN "
1175 throw RecoverableModalException(ss
.str().c_str());
1178 if (!options::produceModels())
1180 std::stringstream ss
;
1181 ss
<< "Cannot " << c
<< " when produce-models options is off.";
1182 throw ModalException(ss
.str().c_str());
1185 TheoryModel
* m
= d_theoryEngine
->getBuiltModel();
1189 std::stringstream ss
;
1190 ss
<< "Cannot " << c
1191 << " since model is not available. Perhaps the most recent call to "
1192 "check-sat was interupted?";
1193 throw RecoverableModalException(ss
.str().c_str());
1199 void SmtEnginePrivate::processAssertions() {
1200 TimerStat::CodeTimer
paTimer(d_smt
.d_stats
->d_processAssertionsTime
);
1201 spendResource(ResourceManager::Resource::PreprocessStep
);
1202 Assert(d_smt
.d_fullyInited
);
1203 Assert(d_smt
.d_pendingPops
== 0);
1205 if (d_assertions
.size() == 0) {
1209 if (d_assertionsProcessed
&& options::incrementalSolving()) {
1210 // TODO(b/1255): Substitutions in incremental mode should be managed with a
1211 // proper data structure.
1213 d_assertions
.enableStoreSubstsInAsserts();
1217 d_assertions
.disableStoreSubstsInAsserts();
1220 // process the assertions
1221 bool noConflict
= d_processor
.apply(d_assertions
);
1223 //notify theory engine new preprocessed assertions
1224 d_smt
.d_theoryEngine
->notifyPreprocessedAssertions( d_assertions
.ref() );
1226 // Push the formula to decision engine
1229 Chat() << "pushing to decision engine..." << endl
;
1230 d_smt
.d_propEngine
->addAssertionsToDecisionEngine(d_assertions
);
1233 // end: INVARIANT to maintain: no reordering of assertions or
1234 // introducing new ones
1236 // if incremental, compute which variables are assigned
1237 if (options::incrementalSolving())
1239 d_preprocessingPassContext
->recordSymbolsInAssertions(d_assertions
.ref());
1242 // Push the formula to SAT
1244 Chat() << "converting to CNF..." << endl
;
1245 TimerStat::CodeTimer
codeTimer(d_smt
.d_stats
->d_cnfConversionTime
);
1246 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
1247 Chat() << "+ " << d_assertions
[i
] << std::endl
;
1248 d_smt
.d_propEngine
->assertFormula(d_assertions
[i
]);
1252 d_assertionsProcessed
= true;
1254 d_assertions
.clear();
1255 getIteSkolemMap().clear();
1258 void SmtEnginePrivate::addFormula(
1259 TNode n
, bool inUnsatCore
, bool inInput
, bool isAssumption
, bool maybeHasFv
)
1266 Trace("smt") << "SmtEnginePrivate::addFormula(" << n
1267 << "), inUnsatCore = " << inUnsatCore
1268 << ", inInput = " << inInput
1269 << ", isAssumption = " << isAssumption
<< endl
;
1271 // Ensure that it does not contain free variables
1274 if (expr::hasFreeVar(n
))
1276 std::stringstream se
;
1277 se
<< "Cannot process assertion with free variable.";
1278 if (language::isInputLangSygus(options::inputLanguage()))
1280 // Common misuse of SyGuS is to use top-level assert instead of
1281 // constraint when defining the synthesis conjecture.
1282 se
<< " Perhaps you meant `constraint` instead of `assert`?";
1284 throw ModalException(se
.str().c_str());
1288 // Give it to proof manager
1291 // n is an input assertion
1292 if (inUnsatCore
|| options::unsatCores() || options::dumpUnsatCores() || options::checkUnsatCores() || options::fewerPreprocessingHoles()) {
1294 ProofManager::currentPM()->addCoreAssertion(n
.toExpr());
1297 // n is the result of an unknown preprocessing step, add it to dependency map to null
1298 ProofManager::currentPM()->addDependence(n
, Node::null());
1302 // Add the normalized formula to the queue
1303 d_assertions
.push_back(n
, isAssumption
);
1304 //d_assertions.push_back(Rewriter::rewrite(n));
1307 void SmtEngine::ensureBoolean(const Node
& n
)
1309 TypeNode type
= n
.getType(options::typeChecking());
1310 TypeNode boolType
= NodeManager::currentNM()->booleanType();
1311 if(type
!= boolType
) {
1313 ss
<< "Expected " << boolType
<< "\n"
1314 << "The assertion : " << n
<< "\n"
1315 << "Its type : " << type
;
1316 throw TypeCheckingException(n
.toExpr(), ss
.str());
1320 Result
SmtEngine::checkSat(const Expr
& assumption
, bool inUnsatCore
)
1322 Dump("benchmark") << CheckSatCommand(assumption
);
1323 return checkSatisfiability(assumption
, inUnsatCore
, false);
1326 Result
SmtEngine::checkSat(const vector
<Expr
>& assumptions
, bool inUnsatCore
)
1328 if (assumptions
.empty())
1330 Dump("benchmark") << CheckSatCommand();
1334 Dump("benchmark") << CheckSatAssumingCommand(assumptions
);
1337 return checkSatisfiability(assumptions
, inUnsatCore
, false);
1340 Result
SmtEngine::checkEntailed(const Expr
& expr
, bool inUnsatCore
)
1342 Dump("benchmark") << QueryCommand(expr
, inUnsatCore
);
1343 return checkSatisfiability(
1344 expr
.isNull() ? std::vector
<Expr
>() : std::vector
<Expr
>{expr
},
1347 .asEntailmentResult();
1350 Result
SmtEngine::checkEntailed(const vector
<Expr
>& exprs
, bool inUnsatCore
)
1352 return checkSatisfiability(exprs
, inUnsatCore
, true).asEntailmentResult();
1355 Result
SmtEngine::checkSatisfiability(const Expr
& expr
,
1357 bool isEntailmentCheck
)
1359 return checkSatisfiability(
1360 expr
.isNull() ? std::vector
<Expr
>() : std::vector
<Expr
>{expr
},
1365 Result
SmtEngine::checkSatisfiability(const vector
<Expr
>& assumptions
,
1367 bool isEntailmentCheck
)
1371 SmtScope
smts(this);
1372 finalOptionsAreSet();
1375 Trace("smt") << "SmtEngine::"
1376 << (isEntailmentCheck
? "checkEntailed" : "checkSat") << "("
1377 << assumptions
<< ")" << endl
;
1379 if(d_queryMade
&& !options::incrementalSolving()) {
1380 throw ModalException("Cannot make multiple queries unless "
1381 "incremental solving is enabled "
1382 "(try --incremental)");
1385 // Note that a query has been made
1387 // reset global negation
1388 d_globalNegation
= false;
1390 bool didInternalPush
= false;
1392 setProblemExtended();
1394 if (isEntailmentCheck
)
1396 size_t size
= assumptions
.size();
1399 /* Assume: not (BIGAND assumptions) */
1400 d_assumptions
.push_back(
1401 d_exprManager
->mkExpr(kind::AND
, assumptions
).notExpr());
1405 /* Assume: not expr */
1406 d_assumptions
.push_back(assumptions
[0].notExpr());
1411 /* Assume: BIGAND assumptions */
1412 d_assumptions
= assumptions
;
1415 if (!d_assumptions
.empty())
1418 didInternalPush
= true;
1421 Result
r(Result::SAT_UNKNOWN
, Result::UNKNOWN_REASON
);
1422 for (Expr e
: d_assumptions
)
1424 // Substitute out any abstract values in ex.
1425 Node n
= d_absValues
->substituteAbstractValues(Node::fromExpr(e
));
1426 // Ensure expr is type-checked at this point.
1429 /* Add assumption */
1430 if (d_assertionList
!= NULL
)
1432 d_assertionList
->push_back(n
);
1434 d_private
->addFormula(n
, inUnsatCore
, true, true);
1437 if (d_globalDefineFunRecLemmas
!= nullptr)
1439 // Global definitions are asserted at check-sat-time because we have to
1440 // make sure that they are always present (they are essentially level
1442 for (const Node
& lemma
: *d_globalDefineFunRecLemmas
)
1444 d_private
->addFormula(lemma
, false, true, false, false);
1450 if ((options::solveRealAsInt() || options::solveIntAsBV() > 0)
1451 && r
.asSatisfiabilityResult().isSat() == Result::UNSAT
)
1453 r
= Result(Result::SAT_UNKNOWN
, Result::UNKNOWN_REASON
);
1455 // flipped if we did a global negation
1456 if (d_globalNegation
)
1458 Trace("smt") << "SmtEngine::process global negate " << r
<< std::endl
;
1459 if (r
.asSatisfiabilityResult().isSat() == Result::UNSAT
)
1461 r
= Result(Result::SAT
);
1463 else if (r
.asSatisfiabilityResult().isSat() == Result::SAT
)
1465 // only if satisfaction complete
1466 if (d_logic
.isPure(THEORY_ARITH
) || d_logic
.isPure(THEORY_BV
))
1468 r
= Result(Result::UNSAT
);
1472 r
= Result(Result::SAT_UNKNOWN
, Result::UNKNOWN_REASON
);
1475 Trace("smt") << "SmtEngine::global negate returned " << r
<< std::endl
;
1478 d_needPostsolve
= true;
1481 if (didInternalPush
)
1486 // Remember the status
1488 // Check against expected status
1489 if (!d_expectedStatus
.isUnknown() && !d_status
.isUnknown()
1490 && d_status
!= d_expectedStatus
)
1492 CVC4_FATAL() << "Expected result " << d_expectedStatus
<< " but got "
1495 d_expectedStatus
= Result();
1496 // Update the SMT mode
1497 if (d_status
.asSatisfiabilityResult().isSat() == Result::UNSAT
)
1499 d_smtMode
= SMT_MODE_UNSAT
;
1501 else if (d_status
.asSatisfiabilityResult().isSat() == Result::SAT
)
1503 d_smtMode
= SMT_MODE_SAT
;
1507 d_smtMode
= SMT_MODE_SAT_UNKNOWN
;
1510 Trace("smt") << "SmtEngine::" << (isEntailmentCheck
? "query" : "checkSat")
1511 << "(" << assumptions
<< ") => " << r
<< endl
;
1513 // Check that SAT results generate a model correctly.
1514 if(options::checkModels()) {
1515 if (r
.asSatisfiabilityResult().isSat() == Result::SAT
)
1520 // Check that UNSAT results generate a proof correctly.
1521 if(options::checkProofs()) {
1522 if(r
.asSatisfiabilityResult().isSat() == Result::UNSAT
) {
1526 // Check that UNSAT results generate an unsat core correctly.
1527 if(options::checkUnsatCores()) {
1528 if(r
.asSatisfiabilityResult().isSat() == Result::UNSAT
) {
1529 TimerStat::CodeTimer
checkUnsatCoreTimer(d_stats
->d_checkUnsatCoreTime
);
1535 } catch (UnsafeInterruptException
& e
) {
1536 AlwaysAssert(d_resourceManager
->out());
1537 Result::UnknownExplanation why
= d_resourceManager
->outOfResources()
1538 ? Result::RESOURCEOUT
1540 return Result(Result::SAT_UNKNOWN
, why
, d_filename
);
1544 vector
<Expr
> SmtEngine::getUnsatAssumptions(void)
1546 Trace("smt") << "SMT getUnsatAssumptions()" << endl
;
1547 SmtScope
smts(this);
1548 if (!options::unsatAssumptions())
1550 throw ModalException(
1551 "Cannot get unsat assumptions when produce-unsat-assumptions option "
1554 if (d_smtMode
!= SMT_MODE_UNSAT
)
1556 throw RecoverableModalException(
1557 "Cannot get unsat assumptions unless immediately preceded by "
1560 finalOptionsAreSet();
1561 if (Dump
.isOn("benchmark"))
1563 Dump("benchmark") << GetUnsatAssumptionsCommand();
1565 UnsatCore core
= getUnsatCoreInternal();
1567 for (const Expr
& e
: d_assumptions
)
1569 if (find(core
.begin(), core
.end(), e
) != core
.end()) { res
.push_back(e
); }
1574 Result
SmtEngine::assertFormula(const Node
& formula
, bool inUnsatCore
)
1576 SmtScope
smts(this);
1577 finalOptionsAreSet();
1580 Trace("smt") << "SmtEngine::assertFormula(" << formula
<< ")" << endl
;
1582 if (Dump
.isOn("raw-benchmark")) {
1583 Dump("raw-benchmark") << AssertCommand(formula
.toExpr());
1586 // Substitute out any abstract values in ex
1587 Node n
= d_absValues
->substituteAbstractValues(formula
);
1590 if(d_assertionList
!= NULL
) {
1591 d_assertionList
->push_back(n
);
1593 bool maybeHasFv
= language::isInputLangSygus(options::inputLanguage());
1594 d_private
->addFormula(n
, inUnsatCore
, true, false, maybeHasFv
);
1595 return quickCheck().asEntailmentResult();
1596 }/* SmtEngine::assertFormula() */
1599 --------------------------------------------------------------------------
1600 Handling SyGuS commands
1601 --------------------------------------------------------------------------
1604 void SmtEngine::declareSygusVar(const std::string
& id
, Expr var
, Type type
)
1606 SmtScope
smts(this);
1607 finalOptionsAreSet();
1608 d_private
->d_sygusVars
.push_back(Node::fromExpr(var
));
1609 Trace("smt") << "SmtEngine::declareSygusVar: " << var
<< "\n";
1610 Dump("raw-benchmark") << DeclareSygusVarCommand(id
, var
, type
);
1611 // don't need to set that the conjecture is stale
1614 void SmtEngine::declareSygusFunctionVar(const std::string
& id
,
1618 SmtScope
smts(this);
1619 finalOptionsAreSet();
1620 d_private
->d_sygusVars
.push_back(Node::fromExpr(var
));
1621 Trace("smt") << "SmtEngine::declareSygusFunctionVar: " << var
<< "\n";
1622 Dump("raw-benchmark") << DeclareSygusVarCommand(id
, var
, type
);
1624 // don't need to set that the conjecture is stale
1627 void SmtEngine::declareSynthFun(const std::string
& id
,
1631 const std::vector
<Expr
>& vars
)
1633 SmtScope
smts(this);
1634 finalOptionsAreSet();
1636 Node fn
= Node::fromExpr(func
);
1637 d_private
->d_sygusFunSymbols
.push_back(fn
);
1640 Expr bvl
= d_exprManager
->mkExpr(kind::BOUND_VAR_LIST
, vars
);
1641 std::vector
<Expr
> attr_val_bvl
;
1642 attr_val_bvl
.push_back(bvl
);
1643 setUserAttribute("sygus-synth-fun-var-list", func
, attr_val_bvl
, "");
1645 // whether sygus type encodes syntax restrictions
1646 if (sygusType
.isDatatype()
1647 && static_cast<DatatypeType
>(sygusType
).getDatatype().isSygus())
1649 TypeNode stn
= TypeNode::fromType(sygusType
);
1650 Node sym
= d_nodeManager
->mkBoundVar("sfproxy", stn
);
1651 std::vector
<Expr
> attr_value
;
1652 attr_value
.push_back(sym
.toExpr());
1653 setUserAttribute("sygus-synth-grammar", func
, attr_value
, "");
1655 Trace("smt") << "SmtEngine::declareSynthFun: " << func
<< "\n";
1656 Dump("raw-benchmark") << SynthFunCommand(id
, func
, sygusType
, isInv
, vars
);
1657 // sygus conjecture is now stale
1658 setSygusConjectureStale();
1661 void SmtEngine::assertSygusConstraint(const Node
& constraint
)
1663 SmtScope
smts(this);
1664 finalOptionsAreSet();
1665 d_private
->d_sygusConstraints
.push_back(constraint
);
1667 Trace("smt") << "SmtEngine::assertSygusConstrant: " << constraint
<< "\n";
1668 Dump("raw-benchmark") << SygusConstraintCommand(constraint
.toExpr());
1669 // sygus conjecture is now stale
1670 setSygusConjectureStale();
1673 void SmtEngine::assertSygusInvConstraint(const Expr
& inv
,
1678 SmtScope
smts(this);
1679 finalOptionsAreSet();
1680 // build invariant constraint
1682 // get variables (regular and their respective primed versions)
1683 std::vector
<Node
> terms
, vars
, primed_vars
;
1684 terms
.push_back(Node::fromExpr(inv
));
1685 terms
.push_back(Node::fromExpr(pre
));
1686 terms
.push_back(Node::fromExpr(trans
));
1687 terms
.push_back(Node::fromExpr(post
));
1688 // variables are built based on the invariant type
1689 FunctionType t
= static_cast<FunctionType
>(inv
.getType());
1690 std::vector
<Type
> argTypes
= t
.getArgTypes();
1691 for (const Type
& ti
: argTypes
)
1693 TypeNode tn
= TypeNode::fromType(ti
);
1694 vars
.push_back(d_nodeManager
->mkBoundVar(tn
));
1695 d_private
->d_sygusVars
.push_back(vars
.back());
1696 std::stringstream ss
;
1697 ss
<< vars
.back() << "'";
1698 primed_vars
.push_back(d_nodeManager
->mkBoundVar(ss
.str(), tn
));
1699 d_private
->d_sygusVars
.push_back(primed_vars
.back());
1702 // make relevant terms; 0 -> Inv, 1 -> Pre, 2 -> Trans, 3 -> Post
1703 for (unsigned i
= 0; i
< 4; ++i
)
1706 Trace("smt-debug") << "Make inv-constraint term #" << i
<< " : " << op
1707 << " with type " << op
.getType() << "...\n";
1708 std::vector
<Node
> children
;
1709 children
.push_back(op
);
1710 // transition relation applied over both variable lists
1713 children
.insert(children
.end(), vars
.begin(), vars
.end());
1714 children
.insert(children
.end(), primed_vars
.begin(), primed_vars
.end());
1718 children
.insert(children
.end(), vars
.begin(), vars
.end());
1720 terms
[i
] = d_nodeManager
->mkNode(kind::APPLY_UF
, children
);
1721 // make application of Inv on primed variables
1725 children
.push_back(op
);
1726 children
.insert(children
.end(), primed_vars
.begin(), primed_vars
.end());
1727 terms
.push_back(d_nodeManager
->mkNode(kind::APPLY_UF
, children
));
1731 std::vector
<Node
> conj
;
1732 conj
.push_back(d_nodeManager
->mkNode(kind::IMPLIES
, terms
[1], terms
[0]));
1733 Node term0_and_2
= d_nodeManager
->mkNode(kind::AND
, terms
[0], terms
[2]);
1734 conj
.push_back(d_nodeManager
->mkNode(kind::IMPLIES
, term0_and_2
, terms
[4]));
1735 conj
.push_back(d_nodeManager
->mkNode(kind::IMPLIES
, terms
[0], terms
[3]));
1736 Node constraint
= d_nodeManager
->mkNode(kind::AND
, conj
);
1738 d_private
->d_sygusConstraints
.push_back(constraint
);
1740 Trace("smt") << "SmtEngine::assertSygusInvConstrant: " << constraint
<< "\n";
1741 Dump("raw-benchmark") << SygusInvConstraintCommand(inv
, pre
, trans
, post
);
1742 // sygus conjecture is now stale
1743 setSygusConjectureStale();
1746 Result
SmtEngine::checkSynth()
1748 SmtScope
smts(this);
1750 if (options::incrementalSolving())
1752 // TODO (project #7)
1753 throw ModalException(
1754 "Cannot make check-synth commands when incremental solving is enabled");
1757 if (d_private
->d_sygusConjectureStale
)
1759 // build synthesis conjecture from asserted constraints and declared
1760 // variables/functions
1762 d_nodeManager
->mkSkolem("sygus", d_nodeManager
->booleanType());
1763 Node inst_attr
= d_nodeManager
->mkNode(kind::INST_ATTRIBUTE
, sygusVar
);
1764 Node sygusAttr
= d_nodeManager
->mkNode(kind::INST_PATTERN_LIST
, inst_attr
);
1765 std::vector
<Node
> bodyv
;
1766 Trace("smt") << "Sygus : Constructing sygus constraint...\n";
1767 unsigned n_constraints
= d_private
->d_sygusConstraints
.size();
1768 Node body
= n_constraints
== 0
1769 ? d_nodeManager
->mkConst(true)
1770 : (n_constraints
== 1
1771 ? d_private
->d_sygusConstraints
[0]
1772 : d_nodeManager
->mkNode(
1773 kind::AND
, d_private
->d_sygusConstraints
));
1774 body
= body
.notNode();
1775 Trace("smt") << "...constructed sygus constraint " << body
<< std::endl
;
1776 if (!d_private
->d_sygusVars
.empty())
1779 d_nodeManager
->mkNode(kind::BOUND_VAR_LIST
, d_private
->d_sygusVars
);
1780 body
= d_nodeManager
->mkNode(kind::EXISTS
, boundVars
, body
);
1781 Trace("smt") << "...constructed exists " << body
<< std::endl
;
1783 if (!d_private
->d_sygusFunSymbols
.empty())
1785 Node boundVars
= d_nodeManager
->mkNode(kind::BOUND_VAR_LIST
,
1786 d_private
->d_sygusFunSymbols
);
1787 body
= d_nodeManager
->mkNode(kind::FORALL
, boundVars
, body
, sygusAttr
);
1789 Trace("smt") << "...constructed forall " << body
<< std::endl
;
1791 // set attribute for synthesis conjecture
1792 setUserAttribute("sygus", sygusVar
.toExpr(), {}, "");
1794 Trace("smt") << "Check synthesis conjecture: " << body
<< std::endl
;
1795 Dump("raw-benchmark") << CheckSynthCommand();
1797 d_private
->d_sygusConjectureStale
= false;
1799 if (options::incrementalSolving())
1801 // we push a context so that this conjecture is removed if we modify it
1804 assertFormula(body
, true);
1808 query
= body
.toExpr();
1812 Result r
= checkSatisfiability(query
, true, false);
1814 // Check that synthesis solutions satisfy the conjecture
1815 if (options::checkSynthSol()
1816 && r
.asSatisfiabilityResult().isSat() == Result::UNSAT
)
1818 checkSynthSolution();
1824 --------------------------------------------------------------------------
1825 End of Handling SyGuS commands
1826 --------------------------------------------------------------------------
1829 Node
SmtEngine::postprocess(TNode node
, TypeNode expectedType
) const {
1833 Expr
SmtEngine::simplify(const Expr
& ex
)
1835 Assert(ex
.getExprManager() == d_exprManager
);
1836 SmtScope
smts(this);
1837 finalOptionsAreSet();
1839 Trace("smt") << "SMT simplify(" << ex
<< ")" << endl
;
1841 if(Dump
.isOn("benchmark")) {
1842 Dump("benchmark") << SimplifyCommand(ex
);
1845 Expr e
= d_absValues
->substituteAbstractValues(Node::fromExpr(ex
)).toExpr();
1846 if( options::typeChecking() ) {
1847 e
.getType(true); // ensure expr is type-checked at this point
1850 // Make sure all preprocessing is done
1851 d_private
->processAssertions();
1852 Node n
= d_private
->simplify(Node::fromExpr(e
));
1853 n
= postprocess(n
, TypeNode::fromType(e
.getType()));
1857 Node
SmtEngine::expandDefinitions(const Node
& ex
)
1859 d_private
->spendResource(ResourceManager::Resource::PreprocessStep
);
1861 SmtScope
smts(this);
1862 finalOptionsAreSet();
1864 Trace("smt") << "SMT expandDefinitions(" << ex
<< ")" << endl
;
1866 // Substitute out any abstract values in ex.
1867 Node e
= d_absValues
->substituteAbstractValues(ex
);
1868 if(options::typeChecking()) {
1869 // Ensure expr is type-checked at this point.
1873 unordered_map
<Node
, Node
, NodeHashFunction
> cache
;
1874 Node n
= d_private
->getProcessAssertions()->expandDefinitions(
1875 e
, cache
, /* expandOnly = */ true);
1876 n
= postprocess(n
, e
.getType());
1881 // TODO(#1108): Simplify the error reporting of this method.
1882 Expr
SmtEngine::getValue(const Expr
& ex
) const
1884 Assert(ex
.getExprManager() == d_exprManager
);
1885 SmtScope
smts(this);
1887 Trace("smt") << "SMT getValue(" << ex
<< ")" << endl
;
1888 if(Dump
.isOn("benchmark")) {
1889 Dump("benchmark") << GetValueCommand(ex
);
1892 // Substitute out any abstract values in ex.
1893 Expr e
= d_absValues
->substituteAbstractValues(Node::fromExpr(ex
)).toExpr();
1895 // Ensure expr is type-checked at this point.
1896 e
.getType(options::typeChecking());
1898 // do not need to apply preprocessing substitutions (should be recorded
1899 // in model already)
1901 Node n
= Node::fromExpr(e
);
1902 Trace("smt") << "--- getting value of " << n
<< endl
;
1903 TypeNode expectedType
= n
.getType();
1905 // Expand, then normalize
1906 unordered_map
<Node
, Node
, NodeHashFunction
> cache
;
1907 n
= d_private
->getProcessAssertions()->expandDefinitions(n
, cache
);
1908 // There are two ways model values for terms are computed (for historical
1909 // reasons). One way is that used in check-model; the other is that
1910 // used by the Model classes. It's not clear to me exactly how these
1911 // two are different, but they need to be unified. This ugly hack here
1912 // is to fix bug 554 until we can revamp boolean-terms and models [MGD]
1915 if(!n
.getType().isFunction()) {
1916 n
= Rewriter::rewrite(n
);
1919 Trace("smt") << "--- getting value of " << n
<< endl
;
1920 TheoryModel
* m
= getAvailableModel("get-value");
1923 resultNode
= m
->getValue(n
);
1925 Trace("smt") << "--- got value " << n
<< " = " << resultNode
<< endl
;
1926 resultNode
= postprocess(resultNode
, expectedType
);
1927 Trace("smt") << "--- model-post returned " << resultNode
<< endl
;
1928 Trace("smt") << "--- model-post returned " << resultNode
.getType() << endl
;
1929 Trace("smt") << "--- model-post expected " << expectedType
<< endl
;
1931 // type-check the result we got
1932 // Notice that lambdas have function type, which does not respect the subtype
1933 // relation, so we ignore them here.
1934 Assert(resultNode
.isNull() || resultNode
.getKind() == kind::LAMBDA
1935 || resultNode
.getType().isSubtypeOf(expectedType
))
1936 << "Run with -t smt for details.";
1938 // Ensure it's a constant, or a lambda (for uninterpreted functions). This
1939 // assertion only holds for models that do not have approximate values.
1940 Assert(m
->hasApproximations() || resultNode
.getKind() == kind::LAMBDA
1941 || resultNode
.isConst());
1943 if(options::abstractValues() && resultNode
.getType().isArray()) {
1944 resultNode
= d_absValues
->mkAbstractValue(resultNode
);
1945 Trace("smt") << "--- abstract value >> " << resultNode
<< endl
;
1948 return resultNode
.toExpr();
1951 vector
<Expr
> SmtEngine::getValues(const vector
<Expr
>& exprs
)
1953 vector
<Expr
> result
;
1954 for (const Expr
& e
: exprs
)
1956 result
.push_back(getValue(e
));
1961 bool SmtEngine::addToAssignment(const Expr
& ex
) {
1962 SmtScope
smts(this);
1963 finalOptionsAreSet();
1965 // Substitute out any abstract values in ex
1966 Node n
= d_absValues
->substituteAbstractValues(Node::fromExpr(ex
));
1967 TypeNode type
= n
.getType(options::typeChecking());
1969 PrettyCheckArgument(type
.isBoolean(),
1971 "expected Boolean-typed variable or function application "
1972 "in addToAssignment()");
1973 // must be a defined constant, or a variable
1974 PrettyCheckArgument(
1975 (((d_definedFunctions
->find(n
) != d_definedFunctions
->end())
1976 && n
.getNumChildren() == 0)
1979 "expected variable or defined-function application "
1980 "in addToAssignment(),\ngot %s",
1981 n
.toString().c_str());
1982 if(!options::produceAssignments()) {
1985 if(d_assignments
== NULL
) {
1986 d_assignments
= new (true) AssignmentSet(getContext());
1988 d_assignments
->insert(n
);
1993 // TODO(#1108): Simplify the error reporting of this method.
1994 vector
<pair
<Expr
, Expr
>> SmtEngine::getAssignment()
1996 Trace("smt") << "SMT getAssignment()" << endl
;
1997 SmtScope
smts(this);
1998 finalOptionsAreSet();
1999 if(Dump
.isOn("benchmark")) {
2000 Dump("benchmark") << GetAssignmentCommand();
2002 if(!options::produceAssignments()) {
2004 "Cannot get the current assignment when "
2005 "produce-assignments option is off.";
2006 throw ModalException(msg
);
2009 // Get the model here, regardless of whether d_assignments is null, since
2010 // we should throw errors related to model availability whether or not
2011 // assignments is null.
2012 TheoryModel
* m
= getAvailableModel("get assignment");
2014 vector
<pair
<Expr
,Expr
>> res
;
2015 if (d_assignments
!= nullptr)
2017 TypeNode boolType
= d_nodeManager
->booleanType();
2018 for (AssignmentSet::key_iterator i
= d_assignments
->key_begin(),
2019 iend
= d_assignments
->key_end();
2024 Assert(as
.getType() == boolType
);
2026 Trace("smt") << "--- getting value of " << as
<< endl
;
2028 // Expand, then normalize
2029 unordered_map
<Node
, Node
, NodeHashFunction
> cache
;
2030 Node n
= d_private
->getProcessAssertions()->expandDefinitions(as
, cache
);
2031 n
= Rewriter::rewrite(n
);
2033 Trace("smt") << "--- getting value of " << n
<< endl
;
2037 resultNode
= m
->getValue(n
);
2040 // type-check the result we got
2041 Assert(resultNode
.isNull() || resultNode
.getType() == boolType
);
2043 // ensure it's a constant
2044 Assert(resultNode
.isConst());
2047 res
.emplace_back(as
.toExpr(), resultNode
.toExpr());
2053 void SmtEngine::addToModelCommandAndDump(const Command
& c
, uint32_t flags
, bool userVisible
, const char* dumpTag
) {
2054 Trace("smt") << "SMT addToModelCommandAndDump(" << c
<< ")" << endl
;
2055 SmtScope
smts(this);
2056 // If we aren't yet fully inited, the user might still turn on
2057 // produce-models. So let's keep any commands around just in
2058 // case. This is useful in two cases: (1) SMT-LIBv1 auto-declares
2059 // sort "U" in QF_UF before setLogic() is run and we still want to
2060 // support finding card(U) with --finite-model-find, and (2) to
2061 // decouple SmtEngine and ExprManager if the user does a few
2062 // ExprManager::mkSort() before SmtEngine::setOption("produce-models")
2063 // and expects to find their cardinalities in the model.
2064 if(/* userVisible && */
2065 (!d_fullyInited
|| options::produceModels()) &&
2066 (flags
& ExprManager::VAR_FLAG_DEFINED
) == 0) {
2067 if(flags
& ExprManager::VAR_FLAG_GLOBAL
) {
2068 d_modelGlobalCommands
.push_back(c
.clone());
2070 d_modelCommands
->push_back(c
.clone());
2073 if(Dump
.isOn(dumpTag
)) {
2077 d_dumpCommands
.push_back(c
.clone());
2082 // TODO(#1108): Simplify the error reporting of this method.
2083 Model
* SmtEngine::getModel() {
2084 Trace("smt") << "SMT getModel()" << endl
;
2085 SmtScope
smts(this);
2087 finalOptionsAreSet();
2089 if(Dump
.isOn("benchmark")) {
2090 Dump("benchmark") << GetModelCommand();
2093 TheoryModel
* m
= getAvailableModel("get model");
2095 // Since model m is being returned to the user, we must ensure that this
2096 // model object remains valid with future check-sat calls. Hence, we set
2097 // the theory engine into "eager model building" mode. TODO #2648: revisit.
2098 d_theoryEngine
->setEagerModelBuilding();
2100 if (options::modelCoresMode() != options::ModelCoresMode::NONE
)
2102 // If we enabled model cores, we compute a model core for m based on our
2103 // (expanded) assertions using the model core builder utility
2104 std::vector
<Expr
> eassertsProc
= getExpandedAssertions();
2105 ModelCoreBuilder::setModelCore(eassertsProc
, m
, options::modelCoresMode());
2107 m
->d_inputName
= d_filename
;
2108 m
->d_isKnownSat
= (d_smtMode
== SMT_MODE_SAT
);
2112 Result
SmtEngine::blockModel()
2114 Trace("smt") << "SMT blockModel()" << endl
;
2115 SmtScope
smts(this);
2117 finalOptionsAreSet();
2119 if (Dump
.isOn("benchmark"))
2121 Dump("benchmark") << BlockModelCommand();
2124 TheoryModel
* m
= getAvailableModel("block model");
2126 if (options::blockModelsMode() == options::BlockModelsMode::NONE
)
2128 std::stringstream ss
;
2129 ss
<< "Cannot block model when block-models is set to none.";
2130 throw ModalException(ss
.str().c_str());
2133 // get expanded assertions
2134 std::vector
<Expr
> eassertsProc
= getExpandedAssertions();
2135 Expr eblocker
= ModelBlocker::getModelBlocker(
2136 eassertsProc
, m
, options::blockModelsMode());
2137 return assertFormula(Node::fromExpr(eblocker
));
2140 Result
SmtEngine::blockModelValues(const std::vector
<Expr
>& exprs
)
2142 Trace("smt") << "SMT blockModelValues()" << endl
;
2143 SmtScope
smts(this);
2145 finalOptionsAreSet();
2147 PrettyCheckArgument(
2149 "block model values must be called on non-empty set of terms");
2150 if (Dump
.isOn("benchmark"))
2152 Dump("benchmark") << BlockModelValuesCommand(exprs
);
2155 TheoryModel
* m
= getAvailableModel("block model values");
2157 // get expanded assertions
2158 std::vector
<Expr
> eassertsProc
= getExpandedAssertions();
2159 // we always do block model values mode here
2160 Expr eblocker
= ModelBlocker::getModelBlocker(
2161 eassertsProc
, m
, options::BlockModelsMode::VALUES
, exprs
);
2162 return assertFormula(Node::fromExpr(eblocker
));
2165 std::pair
<Expr
, Expr
> SmtEngine::getSepHeapAndNilExpr(void)
2167 if (!d_logic
.isTheoryEnabled(THEORY_SEP
))
2170 "Cannot obtain separation logic expressions if not using the "
2171 "separation logic theory.";
2172 throw RecoverableModalException(msg
);
2174 NodeManagerScope
nms(d_nodeManager
);
2177 Model
* m
= getAvailableModel("get separation logic heap and nil");
2178 if (!m
->getHeapModel(heap
, nil
))
2181 << "SmtEngine::getSepHeapAndNilExpr(): failed to obtain heap/nil "
2182 "expressions from theory model.";
2184 return std::make_pair(heap
, nil
);
2187 std::vector
<Expr
> SmtEngine::getExpandedAssertions()
2189 std::vector
<Expr
> easserts
= getAssertions();
2190 // must expand definitions
2191 std::vector
<Expr
> eassertsProc
;
2192 std::unordered_map
<Node
, Node
, NodeHashFunction
> cache
;
2193 for (const Expr
& e
: easserts
)
2195 Node ea
= Node::fromExpr(e
);
2196 Node eae
= d_private
->getProcessAssertions()->expandDefinitions(ea
, cache
);
2197 eassertsProc
.push_back(eae
.toExpr());
2199 return eassertsProc
;
2202 Expr
SmtEngine::getSepHeapExpr() { return getSepHeapAndNilExpr().first
; }
2204 Expr
SmtEngine::getSepNilExpr() { return getSepHeapAndNilExpr().second
; }
2206 void SmtEngine::checkProof()
2208 #if (IS_LFSC_BUILD && IS_PROOFS_BUILD)
2210 Chat() << "generating proof..." << endl
;
2212 const Proof
& pf
= getProof();
2214 Chat() << "checking proof..." << endl
;
2216 std::string logicString
= d_logic
.getLogicString();
2218 std::stringstream pfStream
;
2220 pfStream
<< proof::plf_signatures
<< endl
;
2221 int64_t sizeBeforeProof
= static_cast<int64_t>(pfStream
.tellp());
2223 pf
.toStream(pfStream
);
2224 d_stats
->d_proofsSize
+=
2225 static_cast<int64_t>(pfStream
.tellp()) - sizeBeforeProof
;
2228 TimerStat::CodeTimer
checkProofTimer(d_stats
->d_lfscCheckProofTime
);
2230 lfscc_check_file(pfStream
, false, false, false, false, false, false, false);
2232 // FIXME: we should actually call lfscc_cleanup here, but lfscc_cleanup
2233 // segfaults on regress0/bv/core/bitvec7.smt
2236 #else /* (IS_LFSC_BUILD && IS_PROOFS_BUILD) */
2238 << "This version of CVC4 was built without proof support; cannot check "
2240 #endif /* (IS_LFSC_BUILD && IS_PROOFS_BUILD) */
2243 UnsatCore
SmtEngine::getUnsatCoreInternal()
2246 if (!options::unsatCores())
2248 throw ModalException(
2249 "Cannot get an unsat core when produce-unsat-cores option is off.");
2251 if (d_smtMode
!= SMT_MODE_UNSAT
)
2253 throw RecoverableModalException(
2254 "Cannot get an unsat core unless immediately preceded by "
2255 "UNSAT/ENTAILED response.");
2258 d_proofManager
->traceUnsatCore(); // just to trigger core creation
2259 return UnsatCore(this, d_proofManager
->extractUnsatCore());
2260 #else /* IS_PROOFS_BUILD */
2261 throw ModalException(
2262 "This build of CVC4 doesn't have proof support (required for unsat "
2264 #endif /* IS_PROOFS_BUILD */
2267 void SmtEngine::checkUnsatCore() {
2268 Assert(options::unsatCores())
2269 << "cannot check unsat core if unsat cores are turned off";
2271 Notice() << "SmtEngine::checkUnsatCore(): generating unsat core" << endl
;
2272 UnsatCore core
= getUnsatCore();
2274 SmtEngine
coreChecker(d_exprManager
, &d_options
);
2275 coreChecker
.setIsInternalSubsolver();
2276 coreChecker
.setLogic(getLogicInfo());
2277 coreChecker
.getOptions().set(options::checkUnsatCores
, false);
2278 coreChecker
.getOptions().set(options::checkProofs
, false);
2281 std::vector
<Command
*>::const_iterator itg
= d_defineCommands
.begin();
2282 for (; itg
!= d_defineCommands
.end(); ++itg
) {
2283 (*itg
)->invoke(&coreChecker
);
2287 Notice() << "SmtEngine::checkUnsatCore(): pushing core assertions (size == " << core
.size() << ")" << endl
;
2288 for(UnsatCore::iterator i
= core
.begin(); i
!= core
.end(); ++i
) {
2289 Notice() << "SmtEngine::checkUnsatCore(): pushing core member " << *i
<< endl
;
2290 coreChecker
.assertFormula(Node::fromExpr(*i
));
2294 r
= coreChecker
.checkSat();
2298 Notice() << "SmtEngine::checkUnsatCore(): result is " << r
<< endl
;
2299 if(r
.asSatisfiabilityResult().isUnknown()) {
2301 << "SmtEngine::checkUnsatCore(): could not check core result unknown."
2304 else if (r
.asSatisfiabilityResult().isSat())
2307 << "SmtEngine::checkUnsatCore(): produced core was satisfiable.";
2311 void SmtEngine::checkModel(bool hardFailure
) {
2312 // --check-model implies --produce-assertions, which enables the
2313 // assertion list, so we should be ok.
2314 Assert(d_assertionList
!= NULL
)
2315 << "don't have an assertion list to check in SmtEngine::checkModel()";
2317 TimerStat::CodeTimer
checkModelTimer(d_stats
->d_checkModelTime
);
2319 // Throughout, we use Notice() to give diagnostic output.
2321 // If this function is running, the user gave --check-model (or equivalent),
2322 // and if Notice() is on, the user gave --verbose (or equivalent).
2324 Notice() << "SmtEngine::checkModel(): generating model" << endl
;
2325 TheoryModel
* m
= getAvailableModel("check model");
2327 // check-model is not guaranteed to succeed if approximate values were used.
2328 // Thus, we intentionally abort here.
2329 if (m
->hasApproximations())
2331 throw RecoverableModalException(
2332 "Cannot run check-model on a model with approximate values.");
2335 // Check individual theory assertions
2336 if (options::debugCheckModels())
2338 d_theoryEngine
->checkTheoryAssertionsWithModel(hardFailure
);
2344 // We have a "fake context" for the substitution map (we don't need it
2345 // to be context-dependent)
2346 context::Context fakeContext
;
2347 SubstitutionMap
substitutions(&fakeContext
, /* substituteUnderQuantifiers = */ false);
2349 for(size_t k
= 0; k
< m
->getNumCommands(); ++k
) {
2350 const DeclareFunctionCommand
* c
= dynamic_cast<const DeclareFunctionCommand
*>(m
->getCommand(k
));
2351 Notice() << "SmtEngine::checkModel(): model command " << k
<< " : " << m
->getCommand(k
) << endl
;
2353 // we don't care about DECLARE-DATATYPES, DECLARE-SORT, ...
2354 Notice() << "SmtEngine::checkModel(): skipping..." << endl
;
2356 // We have a DECLARE-FUN:
2358 // We'll first do some checks, then add to our substitution map
2359 // the mapping: function symbol |-> value
2361 Expr func
= c
->getFunction();
2362 Node val
= m
->getValue(func
);
2364 Notice() << "SmtEngine::checkModel(): adding substitution: " << func
<< " |-> " << val
<< endl
;
2366 // (1) if the value is a lambda, ensure the lambda doesn't contain the
2367 // function symbol (since then the definition is recursive)
2368 if (val
.getKind() == kind::LAMBDA
) {
2369 // first apply the model substitutions we have so far
2370 Debug("boolean-terms") << "applying subses to " << val
[1] << endl
;
2371 Node n
= substitutions
.apply(val
[1]);
2372 Debug("boolean-terms") << "++ got " << n
<< endl
;
2373 // now check if n contains func by doing a substitution
2374 // [func->func2] and checking equality of the Nodes.
2375 // (this just a way to check if func is in n.)
2376 SubstitutionMap
subs(&fakeContext
);
2377 Node func2
= NodeManager::currentNM()->mkSkolem("", TypeNode::fromType(func
.getType()), "", NodeManager::SKOLEM_NO_NOTIFY
);
2378 subs
.addSubstitution(func
, func2
);
2379 if(subs
.apply(n
) != n
) {
2380 Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE DEFINED IN TERMS OF ITSELF ***" << endl
;
2382 ss
<< "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
2383 << "considering model value for " << func
<< endl
2384 << "body of lambda is: " << val
<< endl
;
2386 ss
<< "body substitutes to: " << n
<< endl
;
2388 ss
<< "so " << func
<< " is defined in terms of itself." << endl
2389 << "Run with `--check-models -v' for additional diagnostics.";
2390 InternalError() << ss
.str();
2394 // (2) check that the value is actually a value
2395 else if (!val
.isConst())
2397 // This is only a warning since it could have been assigned an
2398 // unevaluable term (e.g. an application of a transcendental function).
2399 // This parallels the behavior (warnings for non-constant expressions)
2400 // when checking whether assertions are satisfied below.
2401 Warning() << "Warning : SmtEngine::checkModel(): "
2402 << "model value for " << func
<< endl
2403 << " is " << val
<< endl
2404 << "and that is not a constant (.isConst() == false)."
2406 << "Run with `--check-models -v' for additional diagnostics."
2410 // (3) check that it's the correct (sub)type
2411 // This was intended to be a more general check, but for now we can't do that because
2412 // e.g. "1" is an INT, which isn't a subrange type [1..10] (etc.).
2413 else if(func
.getType().isInteger() && !val
.getType().isInteger()) {
2414 Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE NOT CORRECT TYPE ***" << endl
;
2416 << "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH "
2419 << "model value for " << func
<< endl
2420 << " is " << val
<< endl
2421 << "value type is " << val
.getType() << endl
2422 << "should be of type " << func
.getType() << endl
2423 << "Run with `--check-models -v' for additional diagnostics.";
2426 // (4) checks complete, add the substitution
2427 Debug("boolean-terms") << "cm: adding subs " << func
<< " :=> " << val
<< endl
;
2428 substitutions
.addSubstitution(func
, val
);
2432 // Now go through all our user assertions checking if they're satisfied.
2433 for (const Node
& assertion
: *d_assertionList
)
2435 Notice() << "SmtEngine::checkModel(): checking assertion " << assertion
2438 Node nr
= Rewriter::rewrite(substitutions
.apply(n
));
2439 Trace("boolean-terms") << "n: " << n
<< endl
;
2440 Trace("boolean-terms") << "nr: " << nr
<< endl
;
2441 if (nr
.isConst() && nr
.getConst
<bool>())
2445 // Apply any define-funs from the problem.
2447 unordered_map
<Node
, Node
, NodeHashFunction
> cache
;
2448 n
= d_private
->getProcessAssertions()->expandDefinitions(n
, cache
);
2450 Notice() << "SmtEngine::checkModel(): -- expands to " << n
<< endl
;
2452 // Apply our model value substitutions.
2453 Debug("boolean-terms") << "applying subses to " << n
<< endl
;
2454 n
= substitutions
.apply(n
);
2455 Debug("boolean-terms") << "++ got " << n
<< endl
;
2456 Notice() << "SmtEngine::checkModel(): -- substitutes to " << n
<< endl
;
2458 // We look up the value before simplifying. If n contains quantifiers,
2459 // this may increases the chance of finding its value before the node is
2460 // altered by simplification below.
2462 Notice() << "SmtEngine::checkModel(): -- get value : " << n
<< std::endl
;
2464 // Simplify the result.
2465 n
= d_private
->simplify(n
);
2466 Notice() << "SmtEngine::checkModel(): -- simplifies to " << n
<< endl
;
2468 // Replace the already-known ITEs (this is important for ground ITEs under quantifiers).
2469 n
= d_private
->d_iteRemover
.replace(n
);
2470 Notice() << "SmtEngine::checkModel(): -- ite replacement gives " << n
<< endl
;
2472 // Apply our model value substitutions (again), as things may have been simplified.
2473 Debug("boolean-terms") << "applying subses to " << n
<< endl
;
2474 n
= substitutions
.apply(n
);
2475 Debug("boolean-terms") << "++ got " << n
<< endl
;
2476 Notice() << "SmtEngine::checkModel(): -- re-substitutes to " << n
<< endl
;
2478 // As a last-ditch effort, ask model to simplify it.
2479 // Presently, this is only an issue for quantifiers, which can have a value
2480 // but don't show up in our substitution map above.
2482 Notice() << "SmtEngine::checkModel(): -- model-substitutes to " << n
<< endl
;
2486 if (n
.getConst
<bool>())
2488 // assertion is true, everything is fine
2493 // Otherwise, we did not succeed in showing the current assertion to be
2494 // true. This may either indicate that our model is wrong, or that we cannot
2495 // check it. The latter may be the case for several reasons.
2496 // For example, quantified formulas are not checkable, although we assign
2497 // them to true/false based on the satisfying assignment. However,
2498 // quantified formulas can be modified during preprocess, so they may not
2499 // correspond to those in the satisfying assignment. Hence we throw
2500 // warnings for assertions that do not simplify to either true or false.
2501 // Other theories such as non-linear arithmetic (in particular,
2502 // transcendental functions) also have the property of not being able to
2503 // be checked precisely here.
2504 // Note that warnings like these can be avoided for quantified formulas
2505 // by making preprocessing passes explicitly record how they
2506 // rewrite quantified formulas (see cvc4-wishues#43).
2509 // Not constant, print a less severe warning message here.
2510 Warning() << "Warning : SmtEngine::checkModel(): cannot check simplified "
2515 // Assertions that simplify to false result in an InternalError or
2516 // Warning being thrown below (when hardFailure is false).
2517 Notice() << "SmtEngine::checkModel(): *** PROBLEM: EXPECTED `TRUE' ***"
2520 ss
<< "SmtEngine::checkModel(): "
2521 << "ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
2522 << "assertion: " << assertion
<< endl
2523 << "simplifies to: " << n
<< endl
2524 << "expected `true'." << endl
2525 << "Run with `--check-models -v' for additional diagnostics.";
2528 // internal error if hardFailure is true
2529 InternalError() << ss
.str();
2533 Warning() << ss
.str() << endl
;
2536 Notice() << "SmtEngine::checkModel(): all assertions checked out OK !" << endl
;
2539 void SmtEngine::checkSynthSolution()
2541 NodeManager
* nm
= NodeManager::currentNM();
2542 Notice() << "SmtEngine::checkSynthSolution(): checking synthesis solution" << endl
;
2543 std::map
<Node
, std::map
<Node
, Node
>> sol_map
;
2544 /* Get solutions and build auxiliary vectors for substituting */
2545 if (!d_theoryEngine
->getSynthSolutions(sol_map
))
2547 InternalError() << "SmtEngine::checkSynthSolution(): No solution to check!";
2550 if (sol_map
.empty())
2552 InternalError() << "SmtEngine::checkSynthSolution(): Got empty solution!";
2555 Trace("check-synth-sol") << "Got solution map:\n";
2556 // the set of synthesis conjectures in our assertions
2557 std::unordered_set
<Node
, NodeHashFunction
> conjs
;
2558 // For each of the above conjectures, the functions-to-synthesis and their
2559 // solutions. This is used as a substitution below.
2560 std::map
<Node
, std::vector
<Node
>> fvarMap
;
2561 std::map
<Node
, std::vector
<Node
>> fsolMap
;
2562 for (const std::pair
<const Node
, std::map
<Node
, Node
>>& cmap
: sol_map
)
2564 Trace("check-synth-sol") << "For conjecture " << cmap
.first
<< ":\n";
2565 conjs
.insert(cmap
.first
);
2566 std::vector
<Node
>& fvars
= fvarMap
[cmap
.first
];
2567 std::vector
<Node
>& fsols
= fsolMap
[cmap
.first
];
2568 for (const std::pair
<const Node
, Node
>& pair
: cmap
.second
)
2570 Trace("check-synth-sol")
2571 << " " << pair
.first
<< " --> " << pair
.second
<< "\n";
2572 fvars
.push_back(pair
.first
);
2573 fsols
.push_back(pair
.second
);
2576 Trace("check-synth-sol") << "Starting new SMT Engine\n";
2577 /* Start new SMT engine to check solutions */
2578 SmtEngine
solChecker(d_exprManager
, &d_options
);
2579 solChecker
.setIsInternalSubsolver();
2580 solChecker
.setLogic(getLogicInfo());
2581 solChecker
.getOptions().set(options::checkSynthSol
, false);
2582 solChecker
.getOptions().set(options::sygusRecFun
, false);
2584 Trace("check-synth-sol") << "Retrieving assertions\n";
2585 // Build conjecture from original assertions
2586 if (d_assertionList
== NULL
)
2588 Trace("check-synth-sol") << "No assertions to check\n";
2591 // auxiliary assertions
2592 std::vector
<Node
> auxAssertions
;
2593 // expand definitions cache
2594 std::unordered_map
<Node
, Node
, NodeHashFunction
> cache
;
2595 for (const Node
& assertion
: *d_assertionList
)
2597 Notice() << "SmtEngine::checkSynthSolution(): checking assertion "
2598 << assertion
<< endl
;
2599 Trace("check-synth-sol") << "Retrieving assertion " << assertion
<< "\n";
2600 // Apply any define-funs from the problem.
2602 d_private
->getProcessAssertions()->expandDefinitions(assertion
, cache
);
2603 Notice() << "SmtEngine::checkSynthSolution(): -- expands to " << n
<< endl
;
2604 Trace("check-synth-sol") << "Expanded assertion " << n
<< "\n";
2605 if (conjs
.find(n
) == conjs
.end())
2607 Trace("check-synth-sol") << "It is an auxiliary assertion\n";
2608 auxAssertions
.push_back(n
);
2612 Trace("check-synth-sol") << "It is a synthesis conjecture\n";
2615 // check all conjectures
2616 for (const Node
& conj
: conjs
)
2618 // get the solution for this conjecture
2619 std::vector
<Node
>& fvars
= fvarMap
[conj
];
2620 std::vector
<Node
>& fsols
= fsolMap
[conj
];
2621 // Apply solution map to conjecture body
2623 /* Whether property is quantifier free */
2624 if (conj
[1].getKind() != kind::EXISTS
)
2626 conjBody
= conj
[1].substitute(
2627 fvars
.begin(), fvars
.end(), fsols
.begin(), fsols
.end());
2631 conjBody
= conj
[1][1].substitute(
2632 fvars
.begin(), fvars
.end(), fsols
.begin(), fsols
.end());
2634 /* Skolemize property */
2635 std::vector
<Node
> vars
, skos
;
2636 for (unsigned j
= 0, size
= conj
[1][0].getNumChildren(); j
< size
; ++j
)
2638 vars
.push_back(conj
[1][0][j
]);
2639 std::stringstream ss
;
2641 skos
.push_back(nm
->mkSkolem(ss
.str(), conj
[1][0][j
].getType()));
2642 Trace("check-synth-sol") << "\tSkolemizing " << conj
[1][0][j
] << " to "
2643 << skos
.back() << "\n";
2645 conjBody
= conjBody
.substitute(
2646 vars
.begin(), vars
.end(), skos
.begin(), skos
.end());
2648 Notice() << "SmtEngine::checkSynthSolution(): -- body substitutes to "
2649 << conjBody
<< endl
;
2650 Trace("check-synth-sol") << "Substituted body of assertion to " << conjBody
2652 solChecker
.assertFormula(conjBody
);
2653 // Assert all auxiliary assertions. This may include recursive function
2654 // definitions that were added as assertions to the sygus problem.
2655 for (const Node
& a
: auxAssertions
)
2657 solChecker
.assertFormula(a
);
2659 Result r
= solChecker
.checkSat();
2660 Notice() << "SmtEngine::checkSynthSolution(): result is " << r
<< endl
;
2661 Trace("check-synth-sol") << "Satsifiability check: " << r
<< "\n";
2662 if (r
.asSatisfiabilityResult().isUnknown())
2664 InternalError() << "SmtEngine::checkSynthSolution(): could not check "
2668 else if (r
.asSatisfiabilityResult().isSat())
2671 << "SmtEngine::checkSynthSolution(): produced solution leads to "
2672 "satisfiable negated conjecture.";
2674 solChecker
.resetAssertions();
2678 void SmtEngine::checkInterpol(Expr interpol
,
2679 const std::vector
<Expr
>& easserts
,
2684 void SmtEngine::checkAbduct(Node a
)
2686 Assert(a
.getType().isBoolean());
2687 // check it with the abduction solver
2688 return d_abductSolver
->checkAbduct(a
);
2691 // TODO(#1108): Simplify the error reporting of this method.
2692 UnsatCore
SmtEngine::getUnsatCore() {
2693 Trace("smt") << "SMT getUnsatCore()" << endl
;
2694 SmtScope
smts(this);
2695 finalOptionsAreSet();
2696 if(Dump
.isOn("benchmark")) {
2697 Dump("benchmark") << GetUnsatCoreCommand();
2699 return getUnsatCoreInternal();
2702 // TODO(#1108): Simplify the error reporting of this method.
2703 const Proof
& SmtEngine::getProof()
2705 Trace("smt") << "SMT getProof()" << endl
;
2706 SmtScope
smts(this);
2707 finalOptionsAreSet();
2708 if(Dump
.isOn("benchmark")) {
2709 Dump("benchmark") << GetProofCommand();
2712 if(!options::proof()) {
2713 throw ModalException("Cannot get a proof when produce-proofs option is off.");
2715 if (d_smtMode
!= SMT_MODE_UNSAT
)
2717 throw RecoverableModalException(
2718 "Cannot get a proof unless immediately preceded by UNSAT/ENTAILED "
2722 return ProofManager::getProof(this);
2723 #else /* IS_PROOFS_BUILD */
2724 throw ModalException("This build of CVC4 doesn't have proof support.");
2725 #endif /* IS_PROOFS_BUILD */
2728 void SmtEngine::printInstantiations( std::ostream
& out
) {
2729 SmtScope
smts(this);
2730 finalOptionsAreSet();
2731 if (options::instFormatMode() == options::InstFormatMode::SZS
)
2733 out
<< "% SZS output start Proof for " << d_filename
.c_str() << std::endl
;
2735 if( d_theoryEngine
){
2736 d_theoryEngine
->printInstantiations( out
);
2740 if (options::instFormatMode() == options::InstFormatMode::SZS
)
2742 out
<< "% SZS output end Proof for " << d_filename
.c_str() << std::endl
;
2746 void SmtEngine::printSynthSolution( std::ostream
& out
) {
2747 SmtScope
smts(this);
2748 finalOptionsAreSet();
2749 if( d_theoryEngine
){
2750 d_theoryEngine
->printSynthSolution( out
);
2756 bool SmtEngine::getSynthSolutions(std::map
<Expr
, Expr
>& sol_map
)
2758 SmtScope
smts(this);
2759 finalOptionsAreSet();
2760 std::map
<Node
, std::map
<Node
, Node
>> sol_mapn
;
2761 Assert(d_theoryEngine
!= nullptr);
2762 // fail if the theory engine does not have synthesis solutions
2763 if (!d_theoryEngine
->getSynthSolutions(sol_mapn
))
2767 for (std::pair
<const Node
, std::map
<Node
, Node
>>& cs
: sol_mapn
)
2769 for (std::pair
<const Node
, Node
>& s
: cs
.second
)
2771 sol_map
[s
.first
.toExpr()] = s
.second
.toExpr();
2777 Expr
SmtEngine::doQuantifierElimination(const Expr
& e
, bool doFull
, bool strict
)
2779 SmtScope
smts(this);
2780 finalOptionsAreSet();
2781 if(!d_logic
.isPure(THEORY_ARITH
) && strict
){
2782 Warning() << "Unexpected logic for quantifier elimination " << d_logic
<< endl
;
2784 Trace("smt-qe") << "Do quantifier elimination " << e
<< std::endl
;
2785 Node n_e
= Node::fromExpr( e
);
2786 if (n_e
.getKind() != kind::EXISTS
&& n_e
.getKind() != kind::FORALL
)
2788 throw ModalException(
2789 "Expecting a quantified formula as argument to get-qe.");
2791 //tag the quantified formula with the quant-elim attribute
2792 TypeNode t
= NodeManager::currentNM()->booleanType();
2793 Node n_attr
= NodeManager::currentNM()->mkSkolem("qe", t
, "Auxiliary variable for qe attr.");
2794 std::vector
< Node
> node_values
;
2795 d_theoryEngine
->setUserAttribute( doFull
? "quant-elim" : "quant-elim-partial", n_attr
, node_values
, "");
2796 n_attr
= NodeManager::currentNM()->mkNode(kind::INST_ATTRIBUTE
, n_attr
);
2797 n_attr
= NodeManager::currentNM()->mkNode(kind::INST_PATTERN_LIST
, n_attr
);
2798 std::vector
< Node
> e_children
;
2799 e_children
.push_back( n_e
[0] );
2800 e_children
.push_back(n_e
.getKind() == kind::EXISTS
? n_e
[1]
2802 e_children
.push_back( n_attr
);
2803 Node nn_e
= NodeManager::currentNM()->mkNode( kind::EXISTS
, e_children
);
2804 Trace("smt-qe-debug") << "Query for quantifier elimination : " << nn_e
<< std::endl
;
2805 Assert(nn_e
.getNumChildren() == 3);
2806 Result r
= checkSatisfiability(nn_e
.toExpr(), true, true);
2807 Trace("smt-qe") << "Query returned " << r
<< std::endl
;
2808 if(r
.asSatisfiabilityResult().isSat() != Result::UNSAT
) {
2809 if( r
.asSatisfiabilityResult().isSat() != Result::SAT
&& doFull
){
2811 << "While performing quantifier elimination, unexpected result : "
2812 << r
<< " for query.";
2813 // failed, return original
2816 std::vector
< Node
> inst_qs
;
2817 d_theoryEngine
->getInstantiatedQuantifiedFormulas( inst_qs
);
2818 Assert(inst_qs
.size() <= 1);
2820 if( inst_qs
.size()==1 ){
2821 Node top_q
= inst_qs
[0];
2822 //Node top_q = Rewriter::rewrite( nn_e ).negate();
2823 Assert(top_q
.getKind() == kind::FORALL
);
2824 Trace("smt-qe") << "Get qe for " << top_q
<< std::endl
;
2825 ret_n
= d_theoryEngine
->getInstantiatedConjunction( top_q
);
2826 Trace("smt-qe") << "Returned : " << ret_n
<< std::endl
;
2827 if (n_e
.getKind() == kind::EXISTS
)
2829 ret_n
= Rewriter::rewrite(ret_n
.negate());
2832 ret_n
= NodeManager::currentNM()->mkConst(n_e
.getKind() != kind::EXISTS
);
2834 // do extended rewrite to minimize the size of the formula aggressively
2835 theory::quantifiers::ExtendedRewriter
extr(true);
2836 ret_n
= extr
.extendedRewrite(ret_n
);
2837 return ret_n
.toExpr();
2839 return NodeManager::currentNM()
2840 ->mkConst(n_e
.getKind() == kind::EXISTS
)
2845 bool SmtEngine::getInterpol(const Expr
& conj
,
2846 const Type
& grammarType
,
2852 bool SmtEngine::getInterpol(const Expr
& conj
, Expr
& interpol
)
2855 return getInterpol(conj
, grammarType
, interpol
);
2858 bool SmtEngine::getAbduct(const Node
& conj
,
2859 const TypeNode
& grammarType
,
2862 if (d_abductSolver
->getAbduct(conj
, grammarType
, abd
))
2864 // successfully generated an abduct, update to abduct state
2865 d_smtMode
= SMT_MODE_ABDUCT
;
2868 // failed, we revert to the assert state
2869 d_smtMode
= SMT_MODE_ASSERT
;
2873 bool SmtEngine::getAbduct(const Node
& conj
, Node
& abd
)
2875 TypeNode grammarType
;
2876 return getAbduct(conj
, grammarType
, abd
);
2879 void SmtEngine::getInstantiatedQuantifiedFormulas( std::vector
< Expr
>& qs
) {
2880 SmtScope
smts(this);
2881 if( d_theoryEngine
){
2882 std::vector
< Node
> qs_n
;
2883 d_theoryEngine
->getInstantiatedQuantifiedFormulas( qs_n
);
2884 for( unsigned i
=0; i
<qs_n
.size(); i
++ ){
2885 qs
.push_back( qs_n
[i
].toExpr() );
2892 void SmtEngine::getInstantiations( Expr q
, std::vector
< Expr
>& insts
) {
2893 SmtScope
smts(this);
2894 if( d_theoryEngine
){
2895 std::vector
< Node
> insts_n
;
2896 d_theoryEngine
->getInstantiations( Node::fromExpr( q
), insts_n
);
2897 for( unsigned i
=0; i
<insts_n
.size(); i
++ ){
2898 insts
.push_back( insts_n
[i
].toExpr() );
2905 void SmtEngine::getInstantiationTermVectors( Expr q
, std::vector
< std::vector
< Expr
> >& tvecs
) {
2906 SmtScope
smts(this);
2907 Assert(options::trackInstLemmas());
2908 if( d_theoryEngine
){
2909 std::vector
< std::vector
< Node
> > tvecs_n
;
2910 d_theoryEngine
->getInstantiationTermVectors( Node::fromExpr( q
), tvecs_n
);
2911 for( unsigned i
=0; i
<tvecs_n
.size(); i
++ ){
2912 std::vector
< Expr
> tvec
;
2913 for( unsigned j
=0; j
<tvecs_n
[i
].size(); j
++ ){
2914 tvec
.push_back( tvecs_n
[i
][j
].toExpr() );
2916 tvecs
.push_back( tvec
);
2923 vector
<Expr
> SmtEngine::getAssertions() {
2924 SmtScope
smts(this);
2925 finalOptionsAreSet();
2927 if(Dump
.isOn("benchmark")) {
2928 Dump("benchmark") << GetAssertionsCommand();
2930 Trace("smt") << "SMT getAssertions()" << endl
;
2931 if(!options::produceAssertions()) {
2933 "Cannot query the current assertion list when not in produce-assertions mode.";
2934 throw ModalException(msg
);
2936 Assert(d_assertionList
!= NULL
);
2937 std::vector
<Expr
> res
;
2938 for (const Node
& n
: *d_assertionList
)
2940 res
.emplace_back(n
.toExpr());
2942 // copy the result out
2946 void SmtEngine::push()
2948 SmtScope
smts(this);
2949 finalOptionsAreSet();
2951 Trace("smt") << "SMT push()" << endl
;
2952 d_private
->notifyPush();
2953 d_private
->processAssertions();
2954 if(Dump
.isOn("benchmark")) {
2955 Dump("benchmark") << PushCommand();
2957 if(!options::incrementalSolving()) {
2958 throw ModalException("Cannot push when not solving incrementally (use --incremental)");
2962 // The problem isn't really "extended" yet, but this disallows
2963 // get-model after a push, simplifying our lives somewhat and
2964 // staying symmetric with pop.
2965 setProblemExtended();
2967 d_userLevels
.push_back(d_userContext
->getLevel());
2969 Trace("userpushpop") << "SmtEngine: pushed to level "
2970 << d_userContext
->getLevel() << endl
;
2973 void SmtEngine::pop() {
2974 SmtScope
smts(this);
2975 finalOptionsAreSet();
2976 Trace("smt") << "SMT pop()" << endl
;
2977 if(Dump
.isOn("benchmark")) {
2978 Dump("benchmark") << PopCommand();
2980 if(!options::incrementalSolving()) {
2981 throw ModalException("Cannot pop when not solving incrementally (use --incremental)");
2983 if(d_userLevels
.size() == 0) {
2984 throw ModalException("Cannot pop beyond the first user frame");
2987 // The problem isn't really "extended" yet, but this disallows
2988 // get-model after a pop, simplifying our lives somewhat. It might
2989 // not be strictly necessary to do so, since the pops occur lazily,
2990 // but also it would be weird to have a legally-executed (get-model)
2991 // that only returns a subset of the assignment (because the rest
2992 // is no longer in scope!).
2993 setProblemExtended();
2995 AlwaysAssert(d_userContext
->getLevel() > 0);
2996 AlwaysAssert(d_userLevels
.back() < d_userContext
->getLevel());
2997 while (d_userLevels
.back() < d_userContext
->getLevel()) {
3000 d_userLevels
.pop_back();
3002 // Clear out assertion queues etc., in case anything is still in there
3003 d_private
->notifyPop();
3005 Trace("userpushpop") << "SmtEngine: popped to level "
3006 << d_userContext
->getLevel() << endl
;
3007 // FIXME: should we reset d_status here?
3008 // SMT-LIBv2 spec seems to imply no, but it would make sense to..
3011 void SmtEngine::internalPush() {
3012 Assert(d_fullyInited
);
3013 Trace("smt") << "SmtEngine::internalPush()" << endl
;
3015 if(options::incrementalSolving()) {
3016 d_private
->processAssertions();
3017 TimerStat::CodeTimer
pushPopTimer(d_stats
->d_pushPopTime
);
3018 d_userContext
->push();
3019 // the d_context push is done inside of the SAT solver
3020 d_propEngine
->push();
3024 void SmtEngine::internalPop(bool immediate
) {
3025 Assert(d_fullyInited
);
3026 Trace("smt") << "SmtEngine::internalPop()" << endl
;
3027 if(options::incrementalSolving()) {
3035 void SmtEngine::doPendingPops() {
3036 Trace("smt") << "SmtEngine::doPendingPops()" << endl
;
3037 Assert(d_pendingPops
== 0 || options::incrementalSolving());
3038 // check to see if a postsolve() is pending
3039 if (d_needPostsolve
)
3041 d_propEngine
->resetTrail();
3043 while(d_pendingPops
> 0) {
3044 TimerStat::CodeTimer
pushPopTimer(d_stats
->d_pushPopTime
);
3045 d_propEngine
->pop();
3046 // the d_context pop is done inside of the SAT solver
3047 d_userContext
->pop();
3050 if (d_needPostsolve
)
3052 d_theoryEngine
->postsolve();
3053 d_needPostsolve
= false;
3057 void SmtEngine::reset()
3059 SmtScope
smts(this);
3060 ExprManager
*em
= d_exprManager
;
3061 Trace("smt") << "SMT reset()" << endl
;
3062 if(Dump
.isOn("benchmark")) {
3063 Dump("benchmark") << ResetCommand();
3066 opts
.copyValues(d_originalOptions
);
3068 new (this) SmtEngine(em
, &opts
);
3071 void SmtEngine::resetAssertions()
3073 SmtScope
smts(this);
3077 // We're still in Start Mode, nothing asserted yet, do nothing.
3078 // (see solver execution modes in the SMT-LIB standard)
3079 Assert(d_context
->getLevel() == 0);
3080 Assert(d_userContext
->getLevel() == 0);
3081 DeleteAndClearCommandVector(d_modelGlobalCommands
);
3087 Trace("smt") << "SMT resetAssertions()" << endl
;
3088 if (Dump
.isOn("benchmark"))
3090 Dump("benchmark") << ResetAssertionsCommand();
3093 while (!d_userLevels
.empty())
3098 // Remember the global push/pop around everything when beyond Start mode
3099 // (see solver execution modes in the SMT-LIB standard)
3100 Assert(d_userLevels
.size() == 0 && d_userContext
->getLevel() == 1);
3101 d_context
->popto(0);
3102 d_userContext
->popto(0);
3103 DeleteAndClearCommandVector(d_modelGlobalCommands
);
3104 d_userContext
->push();
3107 /* Create new PropEngine.
3108 * First force destruction of referenced PropEngine to enforce that
3109 * statistics are unregistered by the obsolete PropEngine object before
3110 * registered again by the new PropEngine object */
3111 d_propEngine
.reset(nullptr);
3112 d_propEngine
.reset(new PropEngine(
3113 getTheoryEngine(), getContext(), getUserContext(), getResourceManager()));
3114 d_theoryEngine
->setPropEngine(getPropEngine());
3117 void SmtEngine::interrupt()
3119 if(!d_fullyInited
) {
3122 d_propEngine
->interrupt();
3123 d_theoryEngine
->interrupt();
3126 void SmtEngine::setResourceLimit(unsigned long units
, bool cumulative
) {
3127 d_resourceManager
->setResourceLimit(units
, cumulative
);
3129 void SmtEngine::setTimeLimit(unsigned long milis
)
3131 d_resourceManager
->setTimeLimit(milis
);
3134 unsigned long SmtEngine::getResourceUsage() const {
3135 return d_resourceManager
->getResourceUsage();
3138 unsigned long SmtEngine::getTimeUsage() const {
3139 return d_resourceManager
->getTimeUsage();
3142 unsigned long SmtEngine::getResourceRemaining() const
3144 return d_resourceManager
->getResourceRemaining();
3147 NodeManager
* SmtEngine::getNodeManager() const
3149 return d_exprManager
->getNodeManager();
3152 Statistics
SmtEngine::getStatistics() const
3154 return Statistics(*d_statisticsRegistry
);
3157 SExpr
SmtEngine::getStatistic(std::string name
) const
3159 return d_statisticsRegistry
->getStatistic(name
);
3162 void SmtEngine::safeFlushStatistics(int fd
) const {
3163 d_statisticsRegistry
->safeFlushInformation(fd
);
3166 void SmtEngine::setUserAttribute(const std::string
& attr
,
3168 const std::vector
<Expr
>& expr_values
,
3169 const std::string
& str_value
)
3171 SmtScope
smts(this);
3172 finalOptionsAreSet();
3173 std::vector
<Node
> node_values
;
3174 for( unsigned i
=0; i
<expr_values
.size(); i
++ ){
3175 node_values
.push_back( expr_values
[i
].getNode() );
3177 d_theoryEngine
->setUserAttribute(attr
, expr
.getNode(), node_values
, str_value
);
3180 void SmtEngine::setPrintFuncInModel(Expr f
, bool p
) {
3181 Trace("setp-model") << "Set printInModel " << f
<< " to " << p
<< std::endl
;
3182 for( unsigned i
=0; i
<d_modelGlobalCommands
.size(); i
++ ){
3183 Command
* c
= d_modelGlobalCommands
[i
];
3184 DeclareFunctionCommand
* dfc
= dynamic_cast<DeclareFunctionCommand
*>(c
);
3186 if( dfc
->getFunction()==f
){
3187 dfc
->setPrintInModel( p
);
3191 for( unsigned i
=0; i
<d_modelCommands
->size(); i
++ ){
3192 Command
* c
= (*d_modelCommands
)[i
];
3193 DeclareFunctionCommand
* dfc
= dynamic_cast<DeclareFunctionCommand
*>(c
);
3195 if( dfc
->getFunction()==f
){
3196 dfc
->setPrintInModel( p
);
3202 void SmtEngine::setOption(const std::string
& key
, const CVC4::SExpr
& value
)
3204 // Always check whether the SmtEngine has been initialized (which is done
3205 // upon entering Assert mode the first time). No option can be set after
3208 throw ModalException("SmtEngine::setOption called after initialization.");
3210 NodeManagerScope
nms(d_nodeManager
);
3211 Trace("smt") << "SMT setOption(" << key
<< ", " << value
<< ")" << endl
;
3213 if(Dump
.isOn("benchmark")) {
3214 Dump("benchmark") << SetOptionCommand(key
, value
);
3217 if(key
== "command-verbosity") {
3218 if(!value
.isAtom()) {
3219 const vector
<SExpr
>& cs
= value
.getChildren();
3220 if(cs
.size() == 2 &&
3221 (cs
[0].isKeyword() || cs
[0].isString()) &&
3222 cs
[1].isInteger()) {
3223 string c
= cs
[0].getValue();
3224 const Integer
& v
= cs
[1].getIntegerValue();
3225 if(v
< 0 || v
> 2) {
3226 throw OptionException("command-verbosity must be 0, 1, or 2");
3228 d_commandVerbosity
[c
] = v
;
3232 throw OptionException("command-verbosity value must be a tuple (command-name, integer)");
3235 if(!value
.isAtom()) {
3236 throw OptionException("bad value for :" + key
);
3239 string optionarg
= value
.getValue();
3240 d_options
.setOption(key
, optionarg
);
3243 void SmtEngine::setIsInternalSubsolver() { d_isInternalSubsolver
= true; }
3245 bool SmtEngine::isInternalSubsolver() const { return d_isInternalSubsolver
; }
3247 CVC4::SExpr
SmtEngine::getOption(const std::string
& key
) const
3249 NodeManagerScope
nms(d_nodeManager
);
3251 Trace("smt") << "SMT getOption(" << key
<< ")" << endl
;
3253 if(key
.length() >= 18 &&
3254 key
.compare(0, 18, "command-verbosity:") == 0) {
3255 map
<string
, Integer
>::const_iterator i
= d_commandVerbosity
.find(key
.c_str() + 18);
3256 if(i
!= d_commandVerbosity
.end()) {
3257 return SExpr((*i
).second
);
3259 i
= d_commandVerbosity
.find("*");
3260 if(i
!= d_commandVerbosity
.end()) {
3261 return SExpr((*i
).second
);
3263 return SExpr(Integer(2));
3266 if(Dump
.isOn("benchmark")) {
3267 Dump("benchmark") << GetOptionCommand(key
);
3270 if(key
== "command-verbosity") {
3271 vector
<SExpr
> result
;
3272 SExpr defaultVerbosity
;
3273 for(map
<string
, Integer
>::const_iterator i
= d_commandVerbosity
.begin();
3274 i
!= d_commandVerbosity
.end();
3277 v
.push_back(SExpr((*i
).first
));
3278 v
.push_back(SExpr((*i
).second
));
3279 if((*i
).first
== "*") {
3280 // put the default at the end of the SExpr
3281 defaultVerbosity
= SExpr(v
);
3283 result
.push_back(SExpr(v
));
3286 // put the default at the end of the SExpr
3287 if(!defaultVerbosity
.isAtom()) {
3288 result
.push_back(defaultVerbosity
);
3290 // ensure the default is always listed
3292 v
.push_back(SExpr("*"));
3293 v
.push_back(SExpr(Integer(2)));
3294 result
.push_back(SExpr(v
));
3296 return SExpr(result
);
3299 return SExpr::parseAtom(d_options
.getOption(key
));
3302 bool SmtEngine::getExpressionName(Expr e
, std::string
& name
) const {
3303 return d_private
->getExpressionName(e
, name
);
3306 void SmtEngine::setExpressionName(Expr e
, const std::string
& name
) {
3307 Trace("smt-debug") << "Set expression name " << e
<< " to " << name
<< std::endl
;
3308 d_private
->setExpressionName(e
,name
);
3311 Options
& SmtEngine::getOptions() { return d_options
; }
3313 const Options
& SmtEngine::getOptions() const { return d_options
; }
3315 ResourceManager
* SmtEngine::getResourceManager()
3317 return d_resourceManager
.get();
3320 void SmtEngine::setSygusConjectureStale()
3322 if (d_private
->d_sygusConjectureStale
)
3327 d_private
->d_sygusConjectureStale
= true;
3328 if (options::incrementalSolving())
3334 }/* CVC4 namespace */