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/listener.h"
38 #include "base/modal_exception.h"
39 #include "base/output.h"
40 #include "context/cdhashmap.h"
41 #include "context/cdhashset.h"
42 #include "context/cdlist.h"
43 #include "context/context.h"
44 #include "decision/decision_engine.h"
45 #include "expr/attribute.h"
46 #include "expr/expr.h"
47 #include "expr/kind.h"
48 #include "expr/metakind.h"
49 #include "expr/node.h"
50 #include "expr/node_algorithm.h"
51 #include "expr/node_builder.h"
52 #include "expr/node_self_iterator.h"
53 #include "expr/node_visitor.h"
54 #include "options/arith_options.h"
55 #include "options/arrays_options.h"
56 #include "options/base_options.h"
57 #include "options/booleans_options.h"
58 #include "options/bv_options.h"
59 #include "options/datatypes_options.h"
60 #include "options/decision_options.h"
61 #include "options/language.h"
62 #include "options/main_options.h"
63 #include "options/open_ostream.h"
64 #include "options/option_exception.h"
65 #include "options/printer_options.h"
66 #include "options/proof_options.h"
67 #include "options/prop_options.h"
68 #include "options/quantifiers_options.h"
69 #include "options/sep_options.h"
70 #include "options/set_language.h"
71 #include "options/smt_options.h"
72 #include "options/strings_options.h"
73 #include "options/theory_options.h"
74 #include "options/uf_options.h"
75 #include "preprocessing/preprocessing_pass.h"
76 #include "preprocessing/preprocessing_pass_context.h"
77 #include "preprocessing/preprocessing_pass_registry.h"
78 #include "printer/printer.h"
79 #include "proof/proof.h"
80 #include "proof/proof_manager.h"
81 #include "proof/theory_proof.h"
82 #include "proof/unsat_core.h"
83 #include "prop/prop_engine.h"
84 #include "smt/abduction_solver.h"
85 #include "smt/command.h"
86 #include "smt/command_list.h"
87 #include "smt/defined_function.h"
88 #include "smt/logic_request.h"
89 #include "smt/managed_ostreams.h"
90 #include "smt/model_blocker.h"
91 #include "smt/model_core_builder.h"
92 #include "smt/process_assertions.h"
93 #include "smt/set_defaults.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());
150 class SoftResourceOutListener
: public Listener
{
152 SoftResourceOutListener(SmtEngine
& smt
) : d_smt(&smt
) {}
153 void notify() override
155 SmtScope
scope(d_smt
);
156 Assert(smt::smtEngineInScope());
161 }; /* class SoftResourceOutListener */
164 class HardResourceOutListener
: public Listener
{
166 HardResourceOutListener(SmtEngine
& smt
) : d_smt(&smt
) {}
167 void notify() override
169 SmtScope
scope(d_smt
);
170 theory::Rewriter::clearCaches();
174 }; /* class HardResourceOutListener */
176 class BeforeSearchListener
: public Listener
{
178 BeforeSearchListener(SmtEngine
& smt
) : d_smt(&smt
) {}
179 void notify() override
{ d_smt
->beforeSearch(); }
183 }; /* class BeforeSearchListener */
185 class SetDefaultExprDepthListener
: public Listener
{
187 void notify() override
189 int depth
= options::defaultExprDepth();
190 Debug
.getStream() << expr::ExprSetDepth(depth
);
191 Trace
.getStream() << expr::ExprSetDepth(depth
);
192 Notice
.getStream() << expr::ExprSetDepth(depth
);
193 Chat
.getStream() << expr::ExprSetDepth(depth
);
194 Message
.getStream() << expr::ExprSetDepth(depth
);
195 Warning
.getStream() << expr::ExprSetDepth(depth
);
196 // intentionally exclude Dump stream from this list
200 class SetDefaultExprDagListener
: public Listener
{
202 void notify() override
204 int dag
= options::defaultDagThresh();
205 Debug
.getStream() << expr::ExprDag(dag
);
206 Trace
.getStream() << expr::ExprDag(dag
);
207 Notice
.getStream() << expr::ExprDag(dag
);
208 Chat
.getStream() << expr::ExprDag(dag
);
209 Message
.getStream() << expr::ExprDag(dag
);
210 Warning
.getStream() << expr::ExprDag(dag
);
211 Dump
.getStream() << expr::ExprDag(dag
);
215 class SetPrintExprTypesListener
: public Listener
{
217 void notify() override
219 bool value
= options::printExprTypes();
220 Debug
.getStream() << expr::ExprPrintTypes(value
);
221 Trace
.getStream() << expr::ExprPrintTypes(value
);
222 Notice
.getStream() << expr::ExprPrintTypes(value
);
223 Chat
.getStream() << expr::ExprPrintTypes(value
);
224 Message
.getStream() << expr::ExprPrintTypes(value
);
225 Warning
.getStream() << expr::ExprPrintTypes(value
);
226 // intentionally exclude Dump stream from this list
230 class DumpModeListener
: public Listener
{
232 void notify() override
234 const std::string
& value
= options::dumpModeString();
235 Dump
.setDumpFromString(value
);
239 class PrintSuccessListener
: public Listener
{
241 void notify() override
243 bool value
= options::printSuccess();
244 Debug
.getStream() << Command::printsuccess(value
);
245 Trace
.getStream() << Command::printsuccess(value
);
246 Notice
.getStream() << Command::printsuccess(value
);
247 Chat
.getStream() << Command::printsuccess(value
);
248 Message
.getStream() << Command::printsuccess(value
);
249 Warning
.getStream() << Command::printsuccess(value
);
250 *options::out() << Command::printsuccess(value
);
257 * This is an inelegant solution, but for the present, it will work.
258 * The point of this is to separate the public and private portions of
259 * the SmtEngine class, so that smt_engine.h doesn't
260 * include "expr/node.h", which is a private CVC4 header (and can lead
261 * to linking errors due to the improper inlining of non-visible symbols
264 * The "real" solution (that which is usually implemented) is to move
265 * ALL the implementation to SmtEnginePrivate and maintain a
266 * heap-allocated instance of it in SmtEngine. SmtEngine (the public
267 * one) becomes an "interface shell" which simply acts as a forwarder
270 class SmtEnginePrivate
: public NodeManagerListener
{
273 typedef unordered_map
<Node
, Node
, NodeHashFunction
> NodeToNodeHashMap
;
274 typedef unordered_map
<Node
, bool, NodeHashFunction
> NodeToBoolHashMap
;
276 /** Manager for the memory of regular-output-channel. */
277 ManagedRegularOutputChannel d_managedRegularChannel
;
279 /** Manager for the memory of diagnostic-output-channel. */
280 ManagedDiagnosticOutputChannel d_managedDiagnosticChannel
;
282 /** Manager for the memory of --dump-to. */
283 ManagedDumpOStream d_managedDumpChannel
;
286 * This list contains:
289 * beforeSearchListener
291 * This needs to be deleted before both NodeManager's Options,
292 * SmtEngine, d_resourceManager, and TheoryEngine.
294 ListenerRegistrationList
* d_listenerRegistrations
;
296 /** A circuit propagator for non-clausal propositional deduction */
297 booleans::CircuitPropagator d_propagator
;
299 /** Assertions in the preprocessing pipeline */
300 AssertionPipeline d_assertions
;
302 /** Whether any assertions have been processed */
303 CDO
<bool> d_assertionsProcessed
;
309 * A context that never pushes/pops, for use by CD structures (like
310 * SubstitutionMaps) that should be "global".
312 context::Context d_fakeContext
;
315 * A map of AbsractValues to their actual constants. Only used if
316 * options::abstractValues() is on.
318 SubstitutionMap d_abstractValueMap
;
321 * A mapping of all abstract values (actual value |-> abstract) that
322 * we've handed out. This is necessary to ensure that we give the
323 * same AbstractValues for the same real constants. Only used if
324 * options::abstractValues() is on.
326 NodeToNodeHashMap d_abstractValues
;
328 /** TODO: whether certain preprocess steps are necessary */
329 //bool d_needsExpandDefs;
331 /** The preprocessing pass context */
332 std::unique_ptr
<PreprocessingPassContext
> d_preprocessingPassContext
;
334 /** Process assertions module */
335 ProcessAssertions d_processor
;
337 //------------------------------- expression names
338 /** mapping from expressions to name */
339 context::CDHashMap
< Node
, std::string
, NodeHashFunction
> d_exprNames
;
340 //------------------------------- end expression names
342 IteSkolemMap
& getIteSkolemMap() { return d_assertions
.getIteSkolemMap(); }
344 /** Instance of the ITE remover */
345 RemoveTermFormulas d_iteRemover
;
347 /* Finishes the initialization of the private portion of SMTEngine. */
350 /*------------------- sygus utils ------------------*/
352 * sygus variables declared (from "declare-var" and "declare-fun" commands)
354 * The SyGuS semantics for declared variables is that they are implicitly
355 * universally quantified in the constraints.
357 std::vector
<Node
> d_sygusVars
;
358 /** sygus constraints */
359 std::vector
<Node
> d_sygusConstraints
;
360 /** functions-to-synthesize */
361 std::vector
<Node
> d_sygusFunSymbols
;
363 * Whether we need to reconstruct the sygus conjecture.
365 CDO
<bool> d_sygusConjectureStale
;
366 /*------------------- end of sygus utils ------------------*/
369 SmtEnginePrivate(SmtEngine
& smt
)
371 d_managedRegularChannel(),
372 d_managedDiagnosticChannel(),
373 d_managedDumpChannel(),
374 d_listenerRegistrations(new ListenerRegistrationList()),
375 d_propagator(true, true),
377 d_assertionsProcessed(smt
.getUserContext(), false),
379 d_abstractValueMap(&d_fakeContext
),
381 d_processor(smt
, *smt
.getResourceManager()),
382 // d_needsExpandDefs(true), //TODO?
383 d_exprNames(smt
.getUserContext()),
384 d_iteRemover(smt
.getUserContext()),
385 d_sygusConjectureStale(smt
.getUserContext(), true)
387 d_smt
.d_nodeManager
->subscribeEvents(this);
388 d_true
= NodeManager::currentNM()->mkConst(true);
389 ResourceManager
* rm
= d_smt
.getResourceManager();
391 d_listenerRegistrations
->add(
392 rm
->registerSoftListener(new SoftResourceOutListener(d_smt
)));
394 d_listenerRegistrations
->add(
395 rm
->registerHardListener(new HardResourceOutListener(d_smt
)));
399 Options
& opts
= d_smt
.getOptions();
400 // Multiple options reuse BeforeSearchListener so registration requires an
401 // extra bit of care.
402 // We can safely not call notify on this before search listener at
403 // registration time. This d_smt cannot be beforeSearch at construction
404 // time. Therefore the BeforeSearchListener is a no-op. Therefore it does
405 // not have to be called.
406 d_listenerRegistrations
->add(
407 opts
.registerBeforeSearchListener(new BeforeSearchListener(d_smt
)));
409 // These do need registration calls.
410 d_listenerRegistrations
->add(opts
.registerSetDefaultExprDepthListener(
411 new SetDefaultExprDepthListener(), true));
412 d_listenerRegistrations
->add(opts
.registerSetDefaultExprDagListener(
413 new SetDefaultExprDagListener(), true));
414 d_listenerRegistrations
->add(opts
.registerSetPrintExprTypesListener(
415 new SetPrintExprTypesListener(), true));
416 d_listenerRegistrations
->add(
417 opts
.registerSetDumpModeListener(new DumpModeListener(), true));
418 d_listenerRegistrations
->add(opts
.registerSetPrintSuccessListener(
419 new PrintSuccessListener(), true));
420 d_listenerRegistrations
->add(opts
.registerSetRegularOutputChannelListener(
421 new SetToDefaultSourceListener(&d_managedRegularChannel
), true));
422 d_listenerRegistrations
->add(
423 opts
.registerSetDiagnosticOutputChannelListener(
424 new SetToDefaultSourceListener(&d_managedDiagnosticChannel
),
426 d_listenerRegistrations
->add(opts
.registerDumpToFileNameListener(
427 new SetToDefaultSourceListener(&d_managedDumpChannel
), true));
429 catch (OptionException
& e
)
431 // Registering the option listeners can lead to OptionExceptions, e.g.
432 // when the user chooses a dump tag that does not exist. In that case, we
433 // have to make sure that we delete existing listener registrations and
434 // that we unsubscribe from NodeManager events. Otherwise we will have
435 // errors in the deconstructors of the NodeManager (because the
436 // NodeManager tries to notify an SmtEnginePrivate that does not exist)
437 // and the ListenerCollection (because not all registrations have been
438 // removed before calling the deconstructor).
439 delete d_listenerRegistrations
;
440 d_smt
.d_nodeManager
->unsubscribeEvents(this);
441 throw OptionException(e
.getRawMessage());
447 delete d_listenerRegistrations
;
449 if(d_propagator
.getNeedsFinish()) {
450 d_propagator
.finish();
451 d_propagator
.setNeedsFinish(false);
453 d_smt
.d_nodeManager
->unsubscribeEvents(this);
456 void spendResource(ResourceManager::Resource r
)
458 d_smt
.getResourceManager()->spendResource(r
);
461 ProcessAssertions
* getProcessAssertions() { return &d_processor
; }
463 void nmNotifyNewSort(TypeNode tn
, uint32_t flags
) override
465 DeclareTypeCommand
c(tn
.getAttribute(expr::VarNameAttr()),
468 if((flags
& ExprManager::SORT_FLAG_PLACEHOLDER
) == 0) {
469 d_smt
.addToModelCommandAndDump(c
, flags
);
473 void nmNotifyNewSortConstructor(TypeNode tn
, uint32_t flags
) override
475 DeclareTypeCommand
c(tn
.getAttribute(expr::VarNameAttr()),
476 tn
.getAttribute(expr::SortArityAttr()),
478 if ((flags
& ExprManager::SORT_FLAG_PLACEHOLDER
) == 0)
480 d_smt
.addToModelCommandAndDump(c
);
484 void nmNotifyNewDatatypes(const std::vector
<DatatypeType
>& dtts
,
485 uint32_t flags
) override
487 if ((flags
& ExprManager::DATATYPE_FLAG_PLACEHOLDER
) == 0)
489 std::vector
<Type
> types(dtts
.begin(), dtts
.end());
490 DatatypeDeclarationCommand
c(types
);
491 d_smt
.addToModelCommandAndDump(c
);
495 void nmNotifyNewVar(TNode n
, uint32_t flags
) override
497 DeclareFunctionCommand
c(n
.getAttribute(expr::VarNameAttr()),
499 n
.getType().toType());
500 if((flags
& ExprManager::VAR_FLAG_DEFINED
) == 0) {
501 d_smt
.addToModelCommandAndDump(c
, flags
);
505 void nmNotifyNewSkolem(TNode n
,
506 const std::string
& comment
,
507 uint32_t flags
) override
509 string id
= n
.getAttribute(expr::VarNameAttr());
510 DeclareFunctionCommand
c(id
, n
.toExpr(), n
.getType().toType());
511 if(Dump
.isOn("skolems") && comment
!= "") {
512 Dump("skolems") << CommentCommand(id
+ " is " + comment
);
514 if((flags
& ExprManager::VAR_FLAG_DEFINED
) == 0) {
515 d_smt
.addToModelCommandAndDump(c
, flags
, false, "skolems");
519 void nmNotifyDeleteNode(TNode n
) override
{}
521 Node
applySubstitutions(TNode node
)
523 return Rewriter::rewrite(
524 d_preprocessingPassContext
->getTopLevelSubstitutions().apply(node
));
528 * Process the assertions that have been asserted.
530 void processAssertions();
532 /** Process a user push.
539 * Process a user pop. Clears out the non-context-dependent stuff in this
540 * SmtEnginePrivate. Necessary to clear out our assertion vectors in case
541 * someone does a push-assert-pop without a check-sat. It also pops the
542 * last map of expression names from notifyPush.
545 d_assertions
.clear();
546 d_propagator
.getLearnedLiterals().clear();
547 getIteSkolemMap().clear();
551 * Adds a formula to the current context. Action here depends on
552 * the SimplificationMode (in the current Options scope); the
553 * formula might be pushed out to the propositional layer
554 * immediately, or it might be simplified and kept, or it might not
555 * even be simplified.
556 * The arguments isInput and isAssumption are used for bookkeeping for proofs.
557 * The argument maybeHasFv should be set to true if the assertion may have
558 * free variables. By construction, assertions from the smt2 parser are
559 * guaranteed not to have free variables. However, other cases such as
560 * assertions from the SyGuS parser may have free variables (say if the
561 * input contains an assert or define-fun-rec command).
563 * @param isAssumption If true, the formula is considered to be an assumption
564 * (this is used to distinguish assertions and assumptions)
566 void addFormula(TNode n
,
569 bool isAssumption
= false,
570 bool maybeHasFv
= false);
572 * Simplify node "in" by expanding definitions and applying any
573 * substitutions learned from preprocessing.
575 Node
simplify(TNode in
) {
576 // Substitute out any abstract values in ex.
577 // Expand definitions.
578 NodeToNodeHashMap cache
;
579 Node n
= d_processor
.expandDefinitions(in
, cache
).toExpr();
580 // Make sure we've done all preprocessing, etc.
581 Assert(d_assertions
.size() == 0);
582 return applySubstitutions(n
).toExpr();
586 * Substitute away all AbstractValues in a node.
588 Node
substituteAbstractValues(TNode n
) {
589 // We need to do this even if options::abstractValues() is off,
590 // since the setting might have changed after we already gave out
591 // some abstract values.
592 return d_abstractValueMap
.apply(n
);
596 * Make a new (or return an existing) abstract value for a node.
597 * Can only use this if options::abstractValues() is on.
599 Node
mkAbstractValue(TNode n
) {
600 Assert(options::abstractValues());
601 Node
& val
= d_abstractValues
[n
];
603 val
= d_smt
.d_nodeManager
->mkAbstractValue(n
.getType());
604 d_abstractValueMap
.addSubstitution(val
, n
);
606 // We are supposed to ascribe types to all abstract values that go out.
607 NodeManager
* current
= d_smt
.d_nodeManager
;
608 Node ascription
= current
->mkConst(AscriptionType(n
.getType().toType()));
609 Node retval
= current
->mkNode(kind::APPLY_TYPE_ASCRIPTION
, ascription
, val
);
613 //------------------------------- expression names
614 // implements setExpressionName, as described in smt_engine.h
615 void setExpressionName(Expr e
, std::string name
) {
616 d_exprNames
[Node::fromExpr(e
)] = name
;
619 // implements getExpressionName, as described in smt_engine.h
620 bool getExpressionName(Expr e
, std::string
& name
) const {
621 context::CDHashMap
< Node
, std::string
, NodeHashFunction
>::const_iterator it
= d_exprNames
.find(e
);
622 if(it
!=d_exprNames
.end()) {
629 //------------------------------- end expression names
630 };/* class SmtEnginePrivate */
632 }/* namespace CVC4::smt */
634 SmtEngine::SmtEngine(ExprManager
* em
, Options
* optr
)
635 : d_context(new Context()),
636 d_userContext(new UserContext()),
639 d_nodeManager(d_exprManager
->getNodeManager()),
640 d_theoryEngine(nullptr),
641 d_propEngine(nullptr),
642 d_proofManager(nullptr),
643 d_rewriter(new theory::Rewriter()),
644 d_definedFunctions(nullptr),
645 d_abductSolver(nullptr),
646 d_assertionList(nullptr),
647 d_assignments(nullptr),
648 d_modelGlobalCommands(),
649 d_modelCommands(nullptr),
654 d_isInternalSubsolver(false),
656 d_fullyInited(false),
658 d_needPostsolve(false),
659 d_globalNegation(false),
662 d_smtMode(SMT_MODE_START
),
664 d_statisticsRegistry(nullptr),
666 d_resourceManager(nullptr),
669 // !!!!!!!!!!!!!!!!!!!!!! temporary hack: this makes the current SmtEngine
670 // we are constructing the current SmtEngine in scope for the lifetime of
671 // this SmtEngine, or until another SmtEngine is constructed (that SmtEngine
672 // is then in scope during its lifetime). This is mostly to ensure that
673 // options are always in scope, for e.g. printing expressions, which rely
674 // on knowing the output language.
675 // Notice that the SmtEngine may spawn new SmtEngine "subsolvers" internally.
676 // These are created, used, and deleted in a modular fashion while not
677 // interleaving calls to the master SmtEngine. Thus the hack here does not
678 // break this use case.
679 // On the other hand, this hack breaks use cases where multiple SmtEngine
680 // objects are created by the user.
681 d_scope
.reset(new SmtScope(this));
684 // if we provided a set of options, copy their values to the options
685 // owned by this SmtEngine.
686 d_options
.copyValues(*optr
);
688 d_statisticsRegistry
.reset(new StatisticsRegistry());
689 d_resourceManager
.reset(
690 new ResourceManager(*d_statisticsRegistry
.get(), d_options
));
691 d_private
.reset(new smt::SmtEnginePrivate(*this));
692 d_stats
.reset(new SmtEngineStatistics());
693 d_stats
->d_resourceUnitsUsed
.setData(d_resourceManager
->getResourceUsage());
695 // The ProofManager is constructed before any other proof objects such as
696 // SatProof and TheoryProofs. The TheoryProofEngine and the SatProof are
697 // initialized in TheoryEngine and PropEngine respectively.
698 Assert(d_proofManager
== nullptr);
700 // d_proofManager must be created before Options has been finished
701 // being parsed from the input file. Because of this, we cannot trust
702 // that options::proof() is set correctly yet.
704 d_proofManager
.reset(new ProofManager(getUserContext()));
707 d_definedFunctions
= new (true) DefinedFunctionMap(getUserContext());
708 d_modelCommands
= new (true) smt::CommandList(getUserContext());
711 void SmtEngine::finishInit()
713 // Notice that finishInit is called when options are finalized. If we are
714 // parsing smt2, this occurs at the moment we enter "Assert mode", page 52
715 // of SMT-LIB 2.6 standard.
717 // Inialize the resource manager based on the options.
718 d_resourceManager
->setHardLimit(options::hardLimit());
719 if (options::perCallResourceLimit() != 0)
721 d_resourceManager
->setResourceLimit(options::perCallResourceLimit(), false);
723 if (options::cumulativeResourceLimit() != 0)
725 d_resourceManager
->setResourceLimit(options::cumulativeResourceLimit(),
728 if (options::perCallMillisecondLimit() != 0)
730 d_resourceManager
->setTimeLimit(options::perCallMillisecondLimit(), false);
732 if (options::cumulativeMillisecondLimit() != 0)
734 d_resourceManager
->setTimeLimit(options::cumulativeMillisecondLimit(),
737 if (options::cpuTime())
739 d_resourceManager
->useCPUTime(true);
742 // set the random seed
743 Random::getRandom().setSeed(options::seed());
745 // ensure that our heuristics are properly set up
746 setDefaults(d_logic
, d_isInternalSubsolver
);
748 Trace("smt-debug") << "SmtEngine::finishInit" << std::endl
;
749 // We have mutual dependency here, so we add the prop engine to the theory
750 // engine later (it is non-essential there)
751 d_theoryEngine
.reset(new TheoryEngine(getContext(),
753 getResourceManager(),
754 d_private
->d_iteRemover
,
755 const_cast<const LogicInfo
&>(d_logic
)));
758 for(TheoryId id
= theory::THEORY_FIRST
; id
< theory::THEORY_LAST
; ++id
) {
759 TheoryConstructor::addTheory(getTheoryEngine(), id
);
760 //register with proof engine if applicable
762 ProofManager::currentPM()->getTheoryProofEngine()->registerTheory(d_theoryEngine
->theoryOf(id
));
766 Trace("smt-debug") << "Making decision engine..." << std::endl
;
768 Trace("smt-debug") << "Making prop engine..." << std::endl
;
769 /* force destruction of referenced PropEngine to enforce that statistics
770 * are unregistered by the obsolete PropEngine object before registered
771 * again by the new PropEngine object */
772 d_propEngine
.reset(nullptr);
773 d_propEngine
.reset(new PropEngine(
774 getTheoryEngine(), getContext(), getUserContext(), getResourceManager()));
776 Trace("smt-debug") << "Setting up theory engine..." << std::endl
;
777 d_theoryEngine
->setPropEngine(getPropEngine());
778 Trace("smt-debug") << "Finishing init for theory engine..." << std::endl
;
779 d_theoryEngine
->finishInit();
781 // global push/pop around everything, to ensure proper destruction
782 // of context-dependent data structures
783 d_userContext
->push();
786 Trace("smt-debug") << "Set up assertion list..." << std::endl
;
787 // [MGD 10/20/2011] keep around in incremental mode, due to a
788 // cleanup ordering issue and Nodes/TNodes. If SAT is popped
789 // first, some user-context-dependent TNodes might still exist
791 if(options::produceAssertions() ||
792 options::incrementalSolving()) {
793 // In the case of incremental solving, we appear to need these to
794 // ensure the relevant Nodes remain live.
795 d_assertionList
= new (true) AssertionList(getUserContext());
796 d_globalDefineFunRecLemmas
.reset(new std::vector
<Node
>());
799 // dump out a set-logic command only when raw-benchmark is disabled to avoid
800 // dumping the command twice.
801 if (Dump
.isOn("benchmark") && !Dump
.isOn("raw-benchmark"))
803 LogicInfo everything
;
805 Dump("benchmark") << CommentCommand(
806 "CVC4 always dumps the most general, all-supported logic (below), as "
807 "some internals might require the use of a logic more general than "
809 << SetBenchmarkLogicCommand(
810 everything
.getLogicString());
813 Trace("smt-debug") << "Dump declaration commands..." << std::endl
;
814 // dump out any pending declaration commands
815 for(unsigned i
= 0; i
< d_dumpCommands
.size(); ++i
) {
816 Dump("declarations") << *d_dumpCommands
[i
];
817 delete d_dumpCommands
[i
];
819 d_dumpCommands
.clear();
822 if (options::produceAbducts())
824 d_abductSolver
.reset(new AbductionSolver(this));
827 PROOF( ProofManager::currentPM()->setLogic(d_logic
); );
829 for(TheoryId id
= theory::THEORY_FIRST
; id
< theory::THEORY_LAST
; ++id
) {
830 ProofManager::currentPM()->getTheoryProofEngine()->
831 finishRegisterTheory(d_theoryEngine
->theoryOf(id
));
834 d_private
->finishInit();
835 Trace("smt-debug") << "SmtEngine::finishInit done" << std::endl
;
838 void SmtEngine::finalOptionsAreSet() {
843 if(! d_logic
.isLocked()) {
847 // finish initialization, create the prop engine, etc.
850 AlwaysAssert(d_propEngine
->getAssertionLevel() == 0)
851 << "The PropEngine has pushed but the SmtEngine "
852 "hasn't finished initializing!";
854 d_fullyInited
= true;
855 Assert(d_logic
.isLocked());
858 void SmtEngine::shutdown() {
861 while(options::incrementalSolving() && d_userContext
->getLevel() > 1) {
865 if (d_propEngine
!= nullptr)
867 d_propEngine
->shutdown();
869 if (d_theoryEngine
!= nullptr)
871 d_theoryEngine
->shutdown();
875 SmtEngine::~SmtEngine()
882 // global push/pop around everything, to ensure proper destruction
883 // of context-dependent data structures
885 d_userContext
->popto(0);
887 if(d_assignments
!= NULL
) {
888 d_assignments
->deleteSelf();
891 d_globalDefineFunRecLemmas
.reset();
893 if(d_assertionList
!= NULL
) {
894 d_assertionList
->deleteSelf();
897 for(unsigned i
= 0; i
< d_dumpCommands
.size(); ++i
) {
898 delete d_dumpCommands
[i
];
899 d_dumpCommands
[i
] = NULL
;
901 d_dumpCommands
.clear();
903 DeleteAndClearCommandVector(d_modelGlobalCommands
);
905 if(d_modelCommands
!= NULL
) {
906 d_modelCommands
->deleteSelf();
909 d_definedFunctions
->deleteSelf();
911 //destroy all passes before destroying things that they refer to
912 d_private
->getProcessAssertions()->cleanup();
914 // d_proofManager is always created when proofs are enabled at configure
915 // time. Because of this, this code should not be wrapped in PROOF() which
916 // additionally checks flags such as options::proof().
918 // Note: the proof manager must be destroyed before the theory engine.
919 // Because the destruction of the proofs depends on contexts owned be the
922 d_proofManager
.reset(nullptr);
925 d_theoryEngine
.reset(nullptr);
926 d_propEngine
.reset(nullptr);
928 d_stats
.reset(nullptr);
929 d_private
.reset(nullptr);
930 // d_resourceManager must be destroyed before d_statisticsRegistry
931 d_resourceManager
.reset(nullptr);
932 d_statisticsRegistry
.reset(nullptr);
935 d_userContext
.reset(nullptr);
936 d_context
.reset(nullptr);
937 } catch(Exception
& e
) {
938 Warning() << "CVC4 threw an exception during cleanup." << endl
943 void SmtEngine::setLogic(const LogicInfo
& logic
)
947 throw ModalException("Cannot set logic in SmtEngine after the engine has "
948 "finished initializing.");
955 void SmtEngine::setLogic(const std::string
& s
)
960 setLogic(LogicInfo(s
));
961 // dump out a set-logic command
962 if (Dump
.isOn("raw-benchmark"))
964 Dump("raw-benchmark")
965 << SetBenchmarkLogicCommand(d_logic
.getLogicString());
968 catch (IllegalArgumentException
& e
)
970 throw LogicException(e
.what());
974 void SmtEngine::setLogic(const char* logic
) { setLogic(string(logic
)); }
975 LogicInfo
SmtEngine::getLogicInfo() const {
979 LogicInfo
SmtEngine::getUserLogicInfo() const
981 // Lock the logic to make sure that this logic can be queried. We create a
982 // copy of the user logic here to keep this method const.
983 LogicInfo res
= d_userLogic
;
988 void SmtEngine::notifyStartParsing(std::string filename
)
990 d_filename
= filename
;
992 // Copy the original options. This is called prior to beginning parsing.
993 // Hence reset should revert to these options, which note is after reading
995 d_originalOptions
.copyValues(d_options
);
998 std::string
SmtEngine::getFilename() const { return d_filename
; }
999 void SmtEngine::setLogicInternal()
1001 Assert(!d_fullyInited
)
1002 << "setting logic in SmtEngine but the engine has already"
1003 " finished initializing for this run";
1008 void SmtEngine::setProblemExtended()
1010 d_smtMode
= SMT_MODE_ASSERT
;
1011 d_assumptions
.clear();
1014 void SmtEngine::setInfo(const std::string
& key
, const CVC4::SExpr
& value
)
1016 SmtScope
smts(this);
1018 Trace("smt") << "SMT setInfo(" << key
<< ", " << value
<< ")" << endl
;
1020 if(Dump
.isOn("benchmark")) {
1021 if(key
== "status") {
1022 string s
= value
.getValue();
1023 BenchmarkStatus status
=
1024 (s
== "sat") ? SMT_SATISFIABLE
:
1025 ((s
== "unsat") ? SMT_UNSATISFIABLE
: SMT_UNKNOWN
);
1026 Dump("benchmark") << SetBenchmarkStatusCommand(status
);
1028 Dump("benchmark") << SetInfoCommand(key
, value
);
1032 // Check for standard info keys (SMT-LIB v1, SMT-LIB v2, ...)
1033 if (key
== "source" || key
== "category" || key
== "difficulty"
1034 || key
== "notes" || key
== "name" || key
== "license")
1039 else if (key
== "filename")
1041 d_filename
= value
.getValue();
1044 else if (key
== "smt-lib-version" && !options::inputLanguage
.wasSetByUser())
1046 language::input::Language ilang
= language::input::LANG_AUTO
;
1047 if( (value
.isInteger() && value
.getIntegerValue() == Integer(2)) ||
1048 (value
.isRational() && value
.getRationalValue() == Rational(2)) ||
1049 value
.getValue() == "2" ||
1050 value
.getValue() == "2.0" ) {
1051 ilang
= language::input::LANG_SMTLIB_V2_0
;
1052 } else if( (value
.isRational() && value
.getRationalValue() == Rational(5, 2)) ||
1053 value
.getValue() == "2.5" ) {
1054 ilang
= language::input::LANG_SMTLIB_V2_5
;
1055 } else if( (value
.isRational() && value
.getRationalValue() == Rational(13, 5)) ||
1056 value
.getValue() == "2.6" ) {
1057 ilang
= language::input::LANG_SMTLIB_V2_6
;
1061 Warning() << "Warning: unsupported smt-lib-version: " << value
<< endl
;
1062 throw UnrecognizedOptionException();
1064 options::inputLanguage
.set(ilang
);
1065 // also update the output language
1066 if (!options::outputLanguage
.wasSetByUser())
1068 language::output::Language olang
= language::toOutputLanguage(ilang
);
1069 if (options::outputLanguage() != olang
)
1071 options::outputLanguage
.set(olang
);
1072 *options::out() << language::SetLanguage(olang
);
1076 } else if(key
== "status") {
1078 if(value
.isAtom()) {
1079 s
= value
.getValue();
1081 if(s
!= "sat" && s
!= "unsat" && s
!= "unknown") {
1082 throw OptionException("argument to (set-info :status ..) must be "
1083 "`sat' or `unsat' or `unknown'");
1085 d_expectedStatus
= Result(s
, d_filename
);
1088 throw UnrecognizedOptionException();
1091 bool SmtEngine::isValidGetInfoFlag(const std::string
& key
) const
1093 if (key
== "all-statistics" || key
== "error-behavior" || key
== "name"
1094 || key
== "version" || key
== "authors" || key
== "status"
1095 || key
== "reason-unknown" || key
== "assertion-stack-levels"
1096 || key
== "all-options")
1103 CVC4::SExpr
SmtEngine::getInfo(const std::string
& key
) const
1105 SmtScope
smts(this);
1107 Trace("smt") << "SMT getInfo(" << key
<< ")" << endl
;
1108 if (!isValidGetInfoFlag(key
))
1110 throw UnrecognizedOptionException();
1112 if (key
== "all-statistics")
1114 vector
<SExpr
> stats
;
1115 for (StatisticsRegistry::const_iterator i
=
1116 NodeManager::fromExprManager(d_exprManager
)
1117 ->getStatisticsRegistry()
1120 != NodeManager::fromExprManager(d_exprManager
)
1121 ->getStatisticsRegistry()
1126 v
.push_back((*i
).first
);
1127 v
.push_back((*i
).second
);
1130 for (StatisticsRegistry::const_iterator i
= d_statisticsRegistry
->begin();
1131 i
!= d_statisticsRegistry
->end();
1135 v
.push_back((*i
).first
);
1136 v
.push_back((*i
).second
);
1139 return SExpr(stats
);
1141 if (key
== "error-behavior")
1143 return SExpr(SExpr::Keyword("immediate-exit"));
1147 return SExpr(Configuration::getName());
1149 if (key
== "version")
1151 return SExpr(Configuration::getVersionString());
1153 if (key
== "authors")
1155 return SExpr(Configuration::about());
1157 if (key
== "status")
1159 // sat | unsat | unknown
1160 switch (d_status
.asSatisfiabilityResult().isSat())
1162 case Result::SAT
: return SExpr(SExpr::Keyword("sat"));
1163 case Result::UNSAT
: return SExpr(SExpr::Keyword("unsat"));
1164 default: return SExpr(SExpr::Keyword("unknown"));
1167 if (key
== "reason-unknown")
1169 if (!d_status
.isNull() && d_status
.isUnknown())
1172 ss
<< d_status
.whyUnknown();
1173 string s
= ss
.str();
1174 transform(s
.begin(), s
.end(), s
.begin(), ::tolower
);
1175 return SExpr(SExpr::Keyword(s
));
1179 throw RecoverableModalException(
1180 "Can't get-info :reason-unknown when the "
1181 "last result wasn't unknown!");
1184 if (key
== "assertion-stack-levels")
1186 AlwaysAssert(d_userLevels
.size()
1187 <= std::numeric_limits
<unsigned long int>::max());
1188 return SExpr(static_cast<unsigned long int>(d_userLevels
.size()));
1190 Assert(key
== "all-options");
1191 // get the options, like all-statistics
1192 std::vector
<std::vector
<std::string
>> current_options
=
1193 Options::current()->getOptions();
1194 return SExpr::parseListOfListOfAtoms(current_options
);
1197 void SmtEngine::debugCheckFormals(const std::vector
<Expr
>& formals
, Expr func
)
1199 for(std::vector
<Expr
>::const_iterator i
= formals
.begin(); i
!= formals
.end(); ++i
) {
1200 if((*i
).getKind() != kind::BOUND_VARIABLE
) {
1202 ss
<< "All formal arguments to defined functions must be BOUND_VARIABLEs, but in the\n"
1203 << "definition of function " << func
<< ", formal\n"
1204 << " " << *i
<< "\n"
1205 << "has kind " << (*i
).getKind();
1206 throw TypeCheckingException(func
, ss
.str());
1211 void SmtEngine::debugCheckFunctionBody(Expr formula
,
1212 const std::vector
<Expr
>& formals
,
1215 Type formulaType
= formula
.getType(options::typeChecking());
1216 Type funcType
= func
.getType();
1217 // We distinguish here between definitions of constants and functions,
1218 // because the type checking for them is subtly different. Perhaps we
1219 // should instead have SmtEngine::defineFunction() and
1220 // SmtEngine::defineConstant() for better clarity, although then that
1221 // doesn't match the SMT-LIBv2 standard...
1222 if(formals
.size() > 0) {
1223 Type rangeType
= FunctionType(funcType
).getRangeType();
1224 if(! formulaType
.isComparableTo(rangeType
)) {
1226 ss
<< "Type of defined function does not match its declaration\n"
1227 << "The function : " << func
<< "\n"
1228 << "Declared type : " << rangeType
<< "\n"
1229 << "The body : " << formula
<< "\n"
1230 << "Body type : " << formulaType
;
1231 throw TypeCheckingException(func
, ss
.str());
1234 if(! formulaType
.isComparableTo(funcType
)) {
1236 ss
<< "Declared type of defined constant does not match its definition\n"
1237 << "The constant : " << func
<< "\n"
1238 << "Declared type : " << funcType
<< " " << Type::getTypeNode(funcType
)->getId() << "\n"
1239 << "The definition : " << formula
<< "\n"
1240 << "Definition type: " << formulaType
<< " " << Type::getTypeNode(formulaType
)->getId();
1241 throw TypeCheckingException(func
, ss
.str());
1246 void SmtEngine::defineFunction(Expr func
,
1247 const std::vector
<Expr
>& formals
,
1251 SmtScope
smts(this);
1252 finalOptionsAreSet();
1254 Trace("smt") << "SMT defineFunction(" << func
<< ")" << endl
;
1255 debugCheckFormals(formals
, func
);
1258 ss
<< language::SetLanguage(
1259 language::SetLanguage::getLanguage(Dump
.getStream()))
1261 DefineFunctionCommand
c(ss
.str(), func
, formals
, formula
, global
);
1262 addToModelCommandAndDump(
1263 c
, ExprManager::VAR_FLAG_DEFINED
, true, "declarations");
1265 PROOF(if (options::checkUnsatCores()) {
1266 d_defineCommands
.push_back(c
.clone());
1270 debugCheckFunctionBody(formula
, formals
, func
);
1272 // Substitute out any abstract values in formula
1274 d_private
->substituteAbstractValues(Node::fromExpr(formula
)).toExpr();
1276 TNode funcNode
= func
.getTNode();
1277 vector
<Node
> formalsNodes
;
1278 for(vector
<Expr
>::const_iterator i
= formals
.begin(),
1279 iend
= formals
.end();
1282 formalsNodes
.push_back((*i
).getNode());
1284 TNode formNode
= form
.getTNode();
1285 DefinedFunction
def(funcNode
, formalsNodes
, formNode
);
1286 // Permit (check-sat) (define-fun ...) (get-value ...) sequences.
1287 // Otherwise, (check-sat) (get-value ((! foo :named bar))) breaks
1288 // d_haveAdditions = true;
1289 Debug("smt") << "definedFunctions insert " << funcNode
<< " " << formNode
<< endl
;
1293 d_definedFunctions
->insertAtContextLevelZero(funcNode
, def
);
1297 d_definedFunctions
->insert(funcNode
, def
);
1301 void SmtEngine::defineFunctionsRec(
1302 const std::vector
<Expr
>& funcs
,
1303 const std::vector
<std::vector
<Expr
>>& formals
,
1304 const std::vector
<Expr
>& formulas
,
1307 SmtScope
smts(this);
1308 finalOptionsAreSet();
1310 Trace("smt") << "SMT defineFunctionsRec(...)" << endl
;
1312 if (funcs
.size() != formals
.size() && funcs
.size() != formulas
.size())
1315 ss
<< "Number of functions, formals, and function bodies passed to "
1316 "defineFunctionsRec do not match:"
1318 << " #functions : " << funcs
.size() << "\n"
1319 << " #arg lists : " << formals
.size() << "\n"
1320 << " #function bodies : " << formulas
.size() << "\n";
1321 throw ModalException(ss
.str());
1323 for (unsigned i
= 0, size
= funcs
.size(); i
< size
; i
++)
1325 // check formal argument list
1326 debugCheckFormals(formals
[i
], funcs
[i
]);
1328 debugCheckFunctionBody(formulas
[i
], formals
[i
], funcs
[i
]);
1331 if (Dump
.isOn("raw-benchmark"))
1333 std::vector
<api::Term
> tFuncs
= api::exprVectorToTerms(d_solver
, funcs
);
1334 std::vector
<std::vector
<api::Term
>> tFormals
;
1335 for (const std::vector
<Expr
>& formal
: formals
)
1337 tFormals
.emplace_back(api::exprVectorToTerms(d_solver
, formal
));
1339 std::vector
<api::Term
> tFormulas
=
1340 api::exprVectorToTerms(d_solver
, formulas
);
1341 Dump("raw-benchmark") << DefineFunctionRecCommand(
1342 d_solver
, tFuncs
, tFormals
, tFormulas
, global
);
1345 ExprManager
* em
= getExprManager();
1346 bool maybeHasFv
= language::isInputLangSygus(options::inputLanguage());
1347 for (unsigned i
= 0, size
= funcs
.size(); i
< size
; i
++)
1349 // we assert a quantified formula
1351 // make the function application
1352 if (formals
[i
].empty())
1354 // it has no arguments
1355 func_app
= funcs
[i
];
1359 std::vector
<Expr
> children
;
1360 children
.push_back(funcs
[i
]);
1361 children
.insert(children
.end(), formals
[i
].begin(), formals
[i
].end());
1362 func_app
= em
->mkExpr(kind::APPLY_UF
, children
);
1364 Expr lem
= em
->mkExpr(kind::EQUAL
, func_app
, formulas
[i
]);
1365 if (!formals
[i
].empty())
1367 // set the attribute to denote this is a function definition
1368 std::string
attr_name("fun-def");
1369 Expr aexpr
= em
->mkExpr(kind::INST_ATTRIBUTE
, func_app
);
1370 aexpr
= em
->mkExpr(kind::INST_PATTERN_LIST
, aexpr
);
1371 std::vector
<Expr
> expr_values
;
1372 std::string str_value
;
1373 setUserAttribute(attr_name
, func_app
, expr_values
, str_value
);
1374 // make the quantified formula
1375 Expr boundVars
= em
->mkExpr(kind::BOUND_VAR_LIST
, formals
[i
]);
1376 lem
= em
->mkExpr(kind::FORALL
, boundVars
, lem
, aexpr
);
1378 // assert the quantified formula
1379 // notice we don't call assertFormula directly, since this would
1380 // duplicate the output on raw-benchmark.
1381 Expr e
= d_private
->substituteAbstractValues(Node::fromExpr(lem
)).toExpr();
1382 if (d_assertionList
!= nullptr)
1384 d_assertionList
->push_back(e
);
1386 if (global
&& d_globalDefineFunRecLemmas
!= nullptr)
1388 // Global definitions are asserted at check-sat-time because we have to
1389 // make sure that they are always present
1390 Assert(!language::isInputLangSygus(options::inputLanguage()));
1391 d_globalDefineFunRecLemmas
->emplace_back(Node::fromExpr(e
));
1395 d_private
->addFormula(e
.getNode(), false, true, false, maybeHasFv
);
1400 void SmtEngine::defineFunctionRec(Expr func
,
1401 const std::vector
<Expr
>& formals
,
1405 std::vector
<Expr
> funcs
;
1406 funcs
.push_back(func
);
1407 std::vector
<std::vector
<Expr
> > formals_multi
;
1408 formals_multi
.push_back(formals
);
1409 std::vector
<Expr
> formulas
;
1410 formulas
.push_back(formula
);
1411 defineFunctionsRec(funcs
, formals_multi
, formulas
, global
);
1414 bool SmtEngine::isDefinedFunction( Expr func
){
1415 Node nf
= Node::fromExpr( func
);
1416 Debug("smt") << "isDefined function " << nf
<< "?" << std::endl
;
1417 return d_definedFunctions
->find(nf
) != d_definedFunctions
->end();
1420 void SmtEnginePrivate::finishInit()
1422 d_preprocessingPassContext
.reset(
1423 new PreprocessingPassContext(&d_smt
, &d_iteRemover
, &d_propagator
));
1425 // initialize the preprocessing passes
1426 d_processor
.finishInit(d_preprocessingPassContext
.get());
1429 Result
SmtEngine::check() {
1430 Assert(d_fullyInited
);
1431 Assert(d_pendingPops
== 0);
1433 Trace("smt") << "SmtEngine::check()" << endl
;
1435 d_resourceManager
->beginCall();
1437 // Only way we can be out of resource is if cumulative budget is on
1438 if (d_resourceManager
->cumulativeLimitOn() && d_resourceManager
->out())
1440 Result::UnknownExplanation why
= d_resourceManager
->outOfResources()
1441 ? Result::RESOURCEOUT
1443 return Result(Result::ENTAILMENT_UNKNOWN
, why
, d_filename
);
1446 // Make sure the prop layer has all of the assertions
1447 Trace("smt") << "SmtEngine::check(): processing assertions" << endl
;
1448 d_private
->processAssertions();
1449 Trace("smt") << "SmtEngine::check(): done processing assertions" << endl
;
1451 TimerStat::CodeTimer
solveTimer(d_stats
->d_solveTime
);
1453 Chat() << "solving..." << endl
;
1454 Trace("smt") << "SmtEngine::check(): running check" << endl
;
1455 Result result
= d_propEngine
->checkSat();
1457 d_resourceManager
->endCall();
1458 Trace("limit") << "SmtEngine::check(): cumulative millis "
1459 << d_resourceManager
->getTimeUsage() << ", resources "
1460 << d_resourceManager
->getResourceUsage() << endl
;
1462 return Result(result
, d_filename
);
1465 Result
SmtEngine::quickCheck() {
1466 Assert(d_fullyInited
);
1467 Trace("smt") << "SMT quickCheck()" << endl
;
1469 Result::ENTAILMENT_UNKNOWN
, Result::REQUIRES_FULL_CHECK
, d_filename
);
1472 theory::TheoryModel
* SmtEngine::getAvailableModel(const char* c
) const
1474 if (!options::assignFunctionValues())
1476 std::stringstream ss
;
1477 ss
<< "Cannot " << c
<< " when --assign-function-values is false.";
1478 throw RecoverableModalException(ss
.str().c_str());
1481 if (d_smtMode
!= SMT_MODE_SAT
&& d_smtMode
!= SMT_MODE_SAT_UNKNOWN
)
1483 std::stringstream ss
;
1484 ss
<< "Cannot " << c
1485 << " unless immediately preceded by SAT/NOT_ENTAILED or UNKNOWN "
1487 throw RecoverableModalException(ss
.str().c_str());
1490 if (!options::produceModels())
1492 std::stringstream ss
;
1493 ss
<< "Cannot " << c
<< " when produce-models options is off.";
1494 throw ModalException(ss
.str().c_str());
1497 TheoryModel
* m
= d_theoryEngine
->getBuiltModel();
1501 std::stringstream ss
;
1502 ss
<< "Cannot " << c
1503 << " since model is not available. Perhaps the most recent call to "
1504 "check-sat was interupted?";
1505 throw RecoverableModalException(ss
.str().c_str());
1511 void SmtEnginePrivate::processAssertions() {
1512 TimerStat::CodeTimer
paTimer(d_smt
.d_stats
->d_processAssertionsTime
);
1513 spendResource(ResourceManager::Resource::PreprocessStep
);
1514 Assert(d_smt
.d_fullyInited
);
1515 Assert(d_smt
.d_pendingPops
== 0);
1517 if (d_assertions
.size() == 0) {
1521 if (d_assertionsProcessed
&& options::incrementalSolving()) {
1522 // TODO(b/1255): Substitutions in incremental mode should be managed with a
1523 // proper data structure.
1525 d_assertions
.enableStoreSubstsInAsserts();
1529 d_assertions
.disableStoreSubstsInAsserts();
1532 // process the assertions
1533 bool noConflict
= d_processor
.apply(d_assertions
);
1535 //notify theory engine new preprocessed assertions
1536 d_smt
.d_theoryEngine
->notifyPreprocessedAssertions( d_assertions
.ref() );
1538 // Push the formula to decision engine
1541 Chat() << "pushing to decision engine..." << endl
;
1542 d_smt
.d_propEngine
->addAssertionsToDecisionEngine(d_assertions
);
1545 // end: INVARIANT to maintain: no reordering of assertions or
1546 // introducing new ones
1548 // if incremental, compute which variables are assigned
1549 if (options::incrementalSolving())
1551 d_preprocessingPassContext
->recordSymbolsInAssertions(d_assertions
.ref());
1554 // Push the formula to SAT
1556 Chat() << "converting to CNF..." << endl
;
1557 TimerStat::CodeTimer
codeTimer(d_smt
.d_stats
->d_cnfConversionTime
);
1558 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
1559 Chat() << "+ " << d_assertions
[i
] << std::endl
;
1560 d_smt
.d_propEngine
->assertFormula(d_assertions
[i
]);
1564 d_assertionsProcessed
= true;
1566 d_assertions
.clear();
1567 getIteSkolemMap().clear();
1570 void SmtEnginePrivate::addFormula(
1571 TNode n
, bool inUnsatCore
, bool inInput
, bool isAssumption
, bool maybeHasFv
)
1578 Trace("smt") << "SmtEnginePrivate::addFormula(" << n
1579 << "), inUnsatCore = " << inUnsatCore
1580 << ", inInput = " << inInput
1581 << ", isAssumption = " << isAssumption
<< endl
;
1583 // Ensure that it does not contain free variables
1586 if (expr::hasFreeVar(n
))
1588 std::stringstream se
;
1589 se
<< "Cannot process assertion with free variable.";
1590 if (language::isInputLangSygus(options::inputLanguage()))
1592 // Common misuse of SyGuS is to use top-level assert instead of
1593 // constraint when defining the synthesis conjecture.
1594 se
<< " Perhaps you meant `constraint` instead of `assert`?";
1596 throw ModalException(se
.str().c_str());
1600 // Give it to proof manager
1603 // n is an input assertion
1604 if (inUnsatCore
|| options::unsatCores() || options::dumpUnsatCores() || options::checkUnsatCores() || options::fewerPreprocessingHoles()) {
1606 ProofManager::currentPM()->addCoreAssertion(n
.toExpr());
1609 // n is the result of an unknown preprocessing step, add it to dependency map to null
1610 ProofManager::currentPM()->addDependence(n
, Node::null());
1614 // Add the normalized formula to the queue
1615 d_assertions
.push_back(n
, isAssumption
);
1616 //d_assertions.push_back(Rewriter::rewrite(n));
1619 void SmtEngine::ensureBoolean(const Expr
& e
)
1621 Type type
= e
.getType(options::typeChecking());
1622 Type boolType
= d_exprManager
->booleanType();
1623 if(type
!= boolType
) {
1625 ss
<< "Expected " << boolType
<< "\n"
1626 << "The assertion : " << e
<< "\n"
1627 << "Its type : " << type
;
1628 throw TypeCheckingException(e
, ss
.str());
1632 Result
SmtEngine::checkSat(const Expr
& assumption
, bool inUnsatCore
)
1634 Dump("benchmark") << CheckSatCommand(assumption
);
1635 return checkSatisfiability(assumption
, inUnsatCore
, false);
1638 Result
SmtEngine::checkSat(const vector
<Expr
>& assumptions
, bool inUnsatCore
)
1640 if (assumptions
.empty())
1642 Dump("benchmark") << CheckSatCommand();
1646 Dump("benchmark") << CheckSatAssumingCommand(assumptions
);
1649 return checkSatisfiability(assumptions
, inUnsatCore
, false);
1652 Result
SmtEngine::checkEntailed(const Expr
& expr
, bool inUnsatCore
)
1654 Dump("benchmark") << QueryCommand(expr
, inUnsatCore
);
1655 return checkSatisfiability(
1656 expr
.isNull() ? std::vector
<Expr
>() : std::vector
<Expr
>{expr
},
1659 .asEntailmentResult();
1662 Result
SmtEngine::checkEntailed(const vector
<Expr
>& exprs
, bool inUnsatCore
)
1664 return checkSatisfiability(exprs
, inUnsatCore
, true).asEntailmentResult();
1667 Result
SmtEngine::checkSatisfiability(const Expr
& expr
,
1669 bool isEntailmentCheck
)
1671 return checkSatisfiability(
1672 expr
.isNull() ? std::vector
<Expr
>() : std::vector
<Expr
>{expr
},
1677 Result
SmtEngine::checkSatisfiability(const vector
<Expr
>& assumptions
,
1679 bool isEntailmentCheck
)
1683 SmtScope
smts(this);
1684 finalOptionsAreSet();
1687 Trace("smt") << "SmtEngine::"
1688 << (isEntailmentCheck
? "checkEntailed" : "checkSat") << "("
1689 << assumptions
<< ")" << endl
;
1691 if(d_queryMade
&& !options::incrementalSolving()) {
1692 throw ModalException("Cannot make multiple queries unless "
1693 "incremental solving is enabled "
1694 "(try --incremental)");
1697 // Note that a query has been made
1699 // reset global negation
1700 d_globalNegation
= false;
1702 bool didInternalPush
= false;
1704 setProblemExtended();
1706 if (isEntailmentCheck
)
1708 size_t size
= assumptions
.size();
1711 /* Assume: not (BIGAND assumptions) */
1712 d_assumptions
.push_back(
1713 d_exprManager
->mkExpr(kind::AND
, assumptions
).notExpr());
1717 /* Assume: not expr */
1718 d_assumptions
.push_back(assumptions
[0].notExpr());
1723 /* Assume: BIGAND assumptions */
1724 d_assumptions
= assumptions
;
1727 if (!d_assumptions
.empty())
1730 didInternalPush
= true;
1733 Result
r(Result::SAT_UNKNOWN
, Result::UNKNOWN_REASON
);
1734 for (Expr e
: d_assumptions
)
1736 // Substitute out any abstract values in ex.
1737 e
= d_private
->substituteAbstractValues(Node::fromExpr(e
)).toExpr();
1738 Assert(e
.getExprManager() == d_exprManager
);
1739 // Ensure expr is type-checked at this point.
1742 /* Add assumption */
1743 if (d_assertionList
!= NULL
)
1745 d_assertionList
->push_back(e
);
1747 d_private
->addFormula(e
.getNode(), inUnsatCore
, true, true);
1750 if (d_globalDefineFunRecLemmas
!= nullptr)
1752 // Global definitions are asserted at check-sat-time because we have to
1753 // make sure that they are always present (they are essentially level
1755 for (const Node
& lemma
: *d_globalDefineFunRecLemmas
)
1757 d_private
->addFormula(lemma
, false, true, false, false);
1763 if ((options::solveRealAsInt() || options::solveIntAsBV() > 0)
1764 && r
.asSatisfiabilityResult().isSat() == Result::UNSAT
)
1766 r
= Result(Result::SAT_UNKNOWN
, Result::UNKNOWN_REASON
);
1768 // flipped if we did a global negation
1769 if (d_globalNegation
)
1771 Trace("smt") << "SmtEngine::process global negate " << r
<< std::endl
;
1772 if (r
.asSatisfiabilityResult().isSat() == Result::UNSAT
)
1774 r
= Result(Result::SAT
);
1776 else if (r
.asSatisfiabilityResult().isSat() == Result::SAT
)
1778 // only if satisfaction complete
1779 if (d_logic
.isPure(THEORY_ARITH
) || d_logic
.isPure(THEORY_BV
))
1781 r
= Result(Result::UNSAT
);
1785 r
= Result(Result::SAT_UNKNOWN
, Result::UNKNOWN_REASON
);
1788 Trace("smt") << "SmtEngine::global negate returned " << r
<< std::endl
;
1791 d_needPostsolve
= true;
1794 if (didInternalPush
)
1799 // Remember the status
1801 // Check against expected status
1802 if (!d_expectedStatus
.isUnknown() && !d_status
.isUnknown()
1803 && d_status
!= d_expectedStatus
)
1805 CVC4_FATAL() << "Expected result " << d_expectedStatus
<< " but got "
1808 d_expectedStatus
= Result();
1809 // Update the SMT mode
1810 if (d_status
.asSatisfiabilityResult().isSat() == Result::UNSAT
)
1812 d_smtMode
= SMT_MODE_UNSAT
;
1814 else if (d_status
.asSatisfiabilityResult().isSat() == Result::SAT
)
1816 d_smtMode
= SMT_MODE_SAT
;
1820 d_smtMode
= SMT_MODE_SAT_UNKNOWN
;
1823 Trace("smt") << "SmtEngine::" << (isEntailmentCheck
? "query" : "checkSat")
1824 << "(" << assumptions
<< ") => " << r
<< endl
;
1826 // Check that SAT results generate a model correctly.
1827 if(options::checkModels()) {
1828 if (r
.asSatisfiabilityResult().isSat() == Result::SAT
)
1833 // Check that UNSAT results generate a proof correctly.
1834 if(options::checkProofs()) {
1835 if(r
.asSatisfiabilityResult().isSat() == Result::UNSAT
) {
1839 // Check that UNSAT results generate an unsat core correctly.
1840 if(options::checkUnsatCores()) {
1841 if(r
.asSatisfiabilityResult().isSat() == Result::UNSAT
) {
1842 TimerStat::CodeTimer
checkUnsatCoreTimer(d_stats
->d_checkUnsatCoreTime
);
1848 } catch (UnsafeInterruptException
& e
) {
1849 AlwaysAssert(d_resourceManager
->out());
1850 Result::UnknownExplanation why
= d_resourceManager
->outOfResources()
1851 ? Result::RESOURCEOUT
1853 return Result(Result::SAT_UNKNOWN
, why
, d_filename
);
1857 vector
<Expr
> SmtEngine::getUnsatAssumptions(void)
1859 Trace("smt") << "SMT getUnsatAssumptions()" << endl
;
1860 SmtScope
smts(this);
1861 if (!options::unsatAssumptions())
1863 throw ModalException(
1864 "Cannot get unsat assumptions when produce-unsat-assumptions option "
1867 if (d_smtMode
!= SMT_MODE_UNSAT
)
1869 throw RecoverableModalException(
1870 "Cannot get unsat assumptions unless immediately preceded by "
1873 finalOptionsAreSet();
1874 if (Dump
.isOn("benchmark"))
1876 Dump("benchmark") << GetUnsatAssumptionsCommand();
1878 UnsatCore core
= getUnsatCoreInternal();
1880 for (const Expr
& e
: d_assumptions
)
1882 if (find(core
.begin(), core
.end(), e
) != core
.end()) { res
.push_back(e
); }
1887 Result
SmtEngine::assertFormula(const Expr
& ex
, bool inUnsatCore
)
1889 Assert(ex
.getExprManager() == d_exprManager
);
1890 SmtScope
smts(this);
1891 finalOptionsAreSet();
1894 Trace("smt") << "SmtEngine::assertFormula(" << ex
<< ")" << endl
;
1896 if (Dump
.isOn("raw-benchmark")) {
1897 Dump("raw-benchmark") << AssertCommand(ex
);
1900 // Substitute out any abstract values in ex
1901 Expr e
= d_private
->substituteAbstractValues(Node::fromExpr(ex
)).toExpr();
1904 if(d_assertionList
!= NULL
) {
1905 d_assertionList
->push_back(e
);
1907 bool maybeHasFv
= language::isInputLangSygus(options::inputLanguage());
1908 d_private
->addFormula(e
.getNode(), inUnsatCore
, true, false, maybeHasFv
);
1909 return quickCheck().asEntailmentResult();
1910 }/* SmtEngine::assertFormula() */
1913 --------------------------------------------------------------------------
1914 Handling SyGuS commands
1915 --------------------------------------------------------------------------
1918 void SmtEngine::declareSygusVar(const std::string
& id
, Expr var
, Type type
)
1920 SmtScope
smts(this);
1921 finalOptionsAreSet();
1922 d_private
->d_sygusVars
.push_back(Node::fromExpr(var
));
1923 Trace("smt") << "SmtEngine::declareSygusVar: " << var
<< "\n";
1924 Dump("raw-benchmark") << DeclareSygusVarCommand(id
, var
, type
);
1925 // don't need to set that the conjecture is stale
1928 void SmtEngine::declareSygusFunctionVar(const std::string
& id
,
1932 SmtScope
smts(this);
1933 finalOptionsAreSet();
1934 d_private
->d_sygusVars
.push_back(Node::fromExpr(var
));
1935 Trace("smt") << "SmtEngine::declareSygusFunctionVar: " << var
<< "\n";
1936 Dump("raw-benchmark") << DeclareSygusVarCommand(id
, var
, type
);
1938 // don't need to set that the conjecture is stale
1941 void SmtEngine::declareSynthFun(const std::string
& id
,
1945 const std::vector
<Expr
>& vars
)
1947 SmtScope
smts(this);
1948 finalOptionsAreSet();
1950 Node fn
= Node::fromExpr(func
);
1951 d_private
->d_sygusFunSymbols
.push_back(fn
);
1954 Expr bvl
= d_exprManager
->mkExpr(kind::BOUND_VAR_LIST
, vars
);
1955 std::vector
<Expr
> attr_val_bvl
;
1956 attr_val_bvl
.push_back(bvl
);
1957 setUserAttribute("sygus-synth-fun-var-list", func
, attr_val_bvl
, "");
1959 // whether sygus type encodes syntax restrictions
1960 if (sygusType
.isDatatype()
1961 && static_cast<DatatypeType
>(sygusType
).getDatatype().isSygus())
1963 TypeNode stn
= TypeNode::fromType(sygusType
);
1964 Node sym
= d_nodeManager
->mkBoundVar("sfproxy", stn
);
1965 std::vector
<Expr
> attr_value
;
1966 attr_value
.push_back(sym
.toExpr());
1967 setUserAttribute("sygus-synth-grammar", func
, attr_value
, "");
1969 Trace("smt") << "SmtEngine::declareSynthFun: " << func
<< "\n";
1970 Dump("raw-benchmark") << SynthFunCommand(id
, func
, sygusType
, isInv
, vars
);
1971 // sygus conjecture is now stale
1972 setSygusConjectureStale();
1975 void SmtEngine::assertSygusConstraint(Expr constraint
)
1977 SmtScope
smts(this);
1978 finalOptionsAreSet();
1979 d_private
->d_sygusConstraints
.push_back(constraint
);
1981 Trace("smt") << "SmtEngine::assertSygusConstrant: " << constraint
<< "\n";
1982 Dump("raw-benchmark") << SygusConstraintCommand(constraint
);
1983 // sygus conjecture is now stale
1984 setSygusConjectureStale();
1987 void SmtEngine::assertSygusInvConstraint(const Expr
& inv
,
1992 SmtScope
smts(this);
1993 finalOptionsAreSet();
1994 // build invariant constraint
1996 // get variables (regular and their respective primed versions)
1997 std::vector
<Node
> terms
, vars
, primed_vars
;
1998 terms
.push_back(Node::fromExpr(inv
));
1999 terms
.push_back(Node::fromExpr(pre
));
2000 terms
.push_back(Node::fromExpr(trans
));
2001 terms
.push_back(Node::fromExpr(post
));
2002 // variables are built based on the invariant type
2003 FunctionType t
= static_cast<FunctionType
>(inv
.getType());
2004 std::vector
<Type
> argTypes
= t
.getArgTypes();
2005 for (const Type
& ti
: argTypes
)
2007 TypeNode tn
= TypeNode::fromType(ti
);
2008 vars
.push_back(d_nodeManager
->mkBoundVar(tn
));
2009 d_private
->d_sygusVars
.push_back(vars
.back());
2010 std::stringstream ss
;
2011 ss
<< vars
.back() << "'";
2012 primed_vars
.push_back(d_nodeManager
->mkBoundVar(ss
.str(), tn
));
2013 d_private
->d_sygusVars
.push_back(primed_vars
.back());
2016 // make relevant terms; 0 -> Inv, 1 -> Pre, 2 -> Trans, 3 -> Post
2017 for (unsigned i
= 0; i
< 4; ++i
)
2020 Trace("smt-debug") << "Make inv-constraint term #" << i
<< " : " << op
2021 << " with type " << op
.getType() << "...\n";
2022 std::vector
<Node
> children
;
2023 children
.push_back(op
);
2024 // transition relation applied over both variable lists
2027 children
.insert(children
.end(), vars
.begin(), vars
.end());
2028 children
.insert(children
.end(), primed_vars
.begin(), primed_vars
.end());
2032 children
.insert(children
.end(), vars
.begin(), vars
.end());
2034 terms
[i
] = d_nodeManager
->mkNode(kind::APPLY_UF
, children
);
2035 // make application of Inv on primed variables
2039 children
.push_back(op
);
2040 children
.insert(children
.end(), primed_vars
.begin(), primed_vars
.end());
2041 terms
.push_back(d_nodeManager
->mkNode(kind::APPLY_UF
, children
));
2045 std::vector
<Node
> conj
;
2046 conj
.push_back(d_nodeManager
->mkNode(kind::IMPLIES
, terms
[1], terms
[0]));
2047 Node term0_and_2
= d_nodeManager
->mkNode(kind::AND
, terms
[0], terms
[2]);
2048 conj
.push_back(d_nodeManager
->mkNode(kind::IMPLIES
, term0_and_2
, terms
[4]));
2049 conj
.push_back(d_nodeManager
->mkNode(kind::IMPLIES
, terms
[0], terms
[3]));
2050 Node constraint
= d_nodeManager
->mkNode(kind::AND
, conj
);
2052 d_private
->d_sygusConstraints
.push_back(constraint
);
2054 Trace("smt") << "SmtEngine::assertSygusInvConstrant: " << constraint
<< "\n";
2055 Dump("raw-benchmark") << SygusInvConstraintCommand(inv
, pre
, trans
, post
);
2056 // sygus conjecture is now stale
2057 setSygusConjectureStale();
2060 Result
SmtEngine::checkSynth()
2062 SmtScope
smts(this);
2064 if (options::incrementalSolving())
2066 // TODO (project #7)
2067 throw ModalException(
2068 "Cannot make check-synth commands when incremental solving is enabled");
2071 if (d_private
->d_sygusConjectureStale
)
2073 // build synthesis conjecture from asserted constraints and declared
2074 // variables/functions
2076 d_nodeManager
->mkSkolem("sygus", d_nodeManager
->booleanType());
2077 Node inst_attr
= d_nodeManager
->mkNode(kind::INST_ATTRIBUTE
, sygusVar
);
2078 Node sygusAttr
= d_nodeManager
->mkNode(kind::INST_PATTERN_LIST
, inst_attr
);
2079 std::vector
<Node
> bodyv
;
2080 Trace("smt") << "Sygus : Constructing sygus constraint...\n";
2081 unsigned n_constraints
= d_private
->d_sygusConstraints
.size();
2082 Node body
= n_constraints
== 0
2083 ? d_nodeManager
->mkConst(true)
2084 : (n_constraints
== 1
2085 ? d_private
->d_sygusConstraints
[0]
2086 : d_nodeManager
->mkNode(
2087 kind::AND
, d_private
->d_sygusConstraints
));
2088 body
= body
.notNode();
2089 Trace("smt") << "...constructed sygus constraint " << body
<< std::endl
;
2090 if (!d_private
->d_sygusVars
.empty())
2093 d_nodeManager
->mkNode(kind::BOUND_VAR_LIST
, d_private
->d_sygusVars
);
2094 body
= d_nodeManager
->mkNode(kind::EXISTS
, boundVars
, body
);
2095 Trace("smt") << "...constructed exists " << body
<< std::endl
;
2097 if (!d_private
->d_sygusFunSymbols
.empty())
2099 Node boundVars
= d_nodeManager
->mkNode(kind::BOUND_VAR_LIST
,
2100 d_private
->d_sygusFunSymbols
);
2101 body
= d_nodeManager
->mkNode(kind::FORALL
, boundVars
, body
, sygusAttr
);
2103 Trace("smt") << "...constructed forall " << body
<< std::endl
;
2105 // set attribute for synthesis conjecture
2106 setUserAttribute("sygus", sygusVar
.toExpr(), {}, "");
2108 Trace("smt") << "Check synthesis conjecture: " << body
<< std::endl
;
2109 Dump("raw-benchmark") << CheckSynthCommand();
2111 d_private
->d_sygusConjectureStale
= false;
2113 if (options::incrementalSolving())
2115 // we push a context so that this conjecture is removed if we modify it
2118 assertFormula(body
.toExpr(), true);
2122 query
= body
.toExpr();
2126 Result r
= checkSatisfiability(query
, true, false);
2128 // Check that synthesis solutions satisfy the conjecture
2129 if (options::checkSynthSol()
2130 && r
.asSatisfiabilityResult().isSat() == Result::UNSAT
)
2132 checkSynthSolution();
2138 --------------------------------------------------------------------------
2139 End of Handling SyGuS commands
2140 --------------------------------------------------------------------------
2143 Node
SmtEngine::postprocess(TNode node
, TypeNode expectedType
) const {
2147 Expr
SmtEngine::simplify(const Expr
& ex
)
2149 Assert(ex
.getExprManager() == d_exprManager
);
2150 SmtScope
smts(this);
2151 finalOptionsAreSet();
2153 Trace("smt") << "SMT simplify(" << ex
<< ")" << endl
;
2155 if(Dump
.isOn("benchmark")) {
2156 Dump("benchmark") << SimplifyCommand(ex
);
2159 Expr e
= d_private
->substituteAbstractValues(Node::fromExpr(ex
)).toExpr();
2160 if( options::typeChecking() ) {
2161 e
.getType(true); // ensure expr is type-checked at this point
2164 // Make sure all preprocessing is done
2165 d_private
->processAssertions();
2166 Node n
= d_private
->simplify(Node::fromExpr(e
));
2167 n
= postprocess(n
, TypeNode::fromType(e
.getType()));
2171 Node
SmtEngine::expandDefinitions(const Node
& ex
)
2173 d_private
->spendResource(ResourceManager::Resource::PreprocessStep
);
2175 SmtScope
smts(this);
2176 finalOptionsAreSet();
2178 Trace("smt") << "SMT expandDefinitions(" << ex
<< ")" << endl
;
2180 // Substitute out any abstract values in ex.
2181 Node e
= d_private
->substituteAbstractValues(ex
);
2182 if(options::typeChecking()) {
2183 // Ensure expr is type-checked at this point.
2187 unordered_map
<Node
, Node
, NodeHashFunction
> cache
;
2188 Node n
= d_private
->getProcessAssertions()->expandDefinitions(
2189 e
, cache
, /* expandOnly = */ true);
2190 n
= postprocess(n
, e
.getType());
2195 // TODO(#1108): Simplify the error reporting of this method.
2196 Expr
SmtEngine::getValue(const Expr
& ex
) const
2198 Assert(ex
.getExprManager() == d_exprManager
);
2199 SmtScope
smts(this);
2201 Trace("smt") << "SMT getValue(" << ex
<< ")" << endl
;
2202 if(Dump
.isOn("benchmark")) {
2203 Dump("benchmark") << GetValueCommand(ex
);
2206 // Substitute out any abstract values in ex.
2207 Expr e
= d_private
->substituteAbstractValues(Node::fromExpr(ex
)).toExpr();
2209 // Ensure expr is type-checked at this point.
2210 e
.getType(options::typeChecking());
2212 // do not need to apply preprocessing substitutions (should be recorded
2213 // in model already)
2215 Node n
= Node::fromExpr(e
);
2216 Trace("smt") << "--- getting value of " << n
<< endl
;
2217 TypeNode expectedType
= n
.getType();
2219 // Expand, then normalize
2220 unordered_map
<Node
, Node
, NodeHashFunction
> cache
;
2221 n
= d_private
->getProcessAssertions()->expandDefinitions(n
, cache
);
2222 // There are two ways model values for terms are computed (for historical
2223 // reasons). One way is that used in check-model; the other is that
2224 // used by the Model classes. It's not clear to me exactly how these
2225 // two are different, but they need to be unified. This ugly hack here
2226 // is to fix bug 554 until we can revamp boolean-terms and models [MGD]
2229 if(!n
.getType().isFunction()) {
2230 n
= Rewriter::rewrite(n
);
2233 Trace("smt") << "--- getting value of " << n
<< endl
;
2234 TheoryModel
* m
= getAvailableModel("get-value");
2237 resultNode
= m
->getValue(n
);
2239 Trace("smt") << "--- got value " << n
<< " = " << resultNode
<< endl
;
2240 resultNode
= postprocess(resultNode
, expectedType
);
2241 Trace("smt") << "--- model-post returned " << resultNode
<< endl
;
2242 Trace("smt") << "--- model-post returned " << resultNode
.getType() << endl
;
2243 Trace("smt") << "--- model-post expected " << expectedType
<< endl
;
2245 // type-check the result we got
2246 // Notice that lambdas have function type, which does not respect the subtype
2247 // relation, so we ignore them here.
2248 Assert(resultNode
.isNull() || resultNode
.getKind() == kind::LAMBDA
2249 || resultNode
.getType().isSubtypeOf(expectedType
))
2250 << "Run with -t smt for details.";
2252 // Ensure it's a constant, or a lambda (for uninterpreted functions). This
2253 // assertion only holds for models that do not have approximate values.
2254 Assert(m
->hasApproximations() || resultNode
.getKind() == kind::LAMBDA
2255 || resultNode
.isConst());
2257 if(options::abstractValues() && resultNode
.getType().isArray()) {
2258 resultNode
= d_private
->mkAbstractValue(resultNode
);
2259 Trace("smt") << "--- abstract value >> " << resultNode
<< endl
;
2262 return resultNode
.toExpr();
2265 vector
<Expr
> SmtEngine::getValues(const vector
<Expr
>& exprs
)
2267 vector
<Expr
> result
;
2268 for (const Expr
& e
: exprs
)
2270 result
.push_back(getValue(e
));
2275 bool SmtEngine::addToAssignment(const Expr
& ex
) {
2276 SmtScope
smts(this);
2277 finalOptionsAreSet();
2279 // Substitute out any abstract values in ex
2280 Expr e
= d_private
->substituteAbstractValues(Node::fromExpr(ex
)).toExpr();
2281 Type type
= e
.getType(options::typeChecking());
2283 PrettyCheckArgument(
2284 type
.isBoolean(), e
,
2285 "expected Boolean-typed variable or function application "
2286 "in addToAssignment()" );
2287 Node n
= e
.getNode();
2288 // must be a defined constant, or a variable
2289 PrettyCheckArgument(
2290 (((d_definedFunctions
->find(n
) != d_definedFunctions
->end())
2291 && n
.getNumChildren() == 0)
2294 "expected variable or defined-function application "
2295 "in addToAssignment(),\ngot %s",
2296 e
.toString().c_str());
2297 if(!options::produceAssignments()) {
2300 if(d_assignments
== NULL
) {
2301 d_assignments
= new (true) AssignmentSet(getContext());
2303 d_assignments
->insert(n
);
2308 // TODO(#1108): Simplify the error reporting of this method.
2309 vector
<pair
<Expr
, Expr
>> SmtEngine::getAssignment()
2311 Trace("smt") << "SMT getAssignment()" << endl
;
2312 SmtScope
smts(this);
2313 finalOptionsAreSet();
2314 if(Dump
.isOn("benchmark")) {
2315 Dump("benchmark") << GetAssignmentCommand();
2317 if(!options::produceAssignments()) {
2319 "Cannot get the current assignment when "
2320 "produce-assignments option is off.";
2321 throw ModalException(msg
);
2324 // Get the model here, regardless of whether d_assignments is null, since
2325 // we should throw errors related to model availability whether or not
2326 // assignments is null.
2327 TheoryModel
* m
= getAvailableModel("get assignment");
2329 vector
<pair
<Expr
,Expr
>> res
;
2330 if (d_assignments
!= nullptr)
2332 TypeNode boolType
= d_nodeManager
->booleanType();
2333 for (AssignmentSet::key_iterator i
= d_assignments
->key_begin(),
2334 iend
= d_assignments
->key_end();
2339 Assert(as
.getType() == boolType
);
2341 Trace("smt") << "--- getting value of " << as
<< endl
;
2343 // Expand, then normalize
2344 unordered_map
<Node
, Node
, NodeHashFunction
> cache
;
2345 Node n
= d_private
->getProcessAssertions()->expandDefinitions(as
, cache
);
2346 n
= Rewriter::rewrite(n
);
2348 Trace("smt") << "--- getting value of " << n
<< endl
;
2352 resultNode
= m
->getValue(n
);
2355 // type-check the result we got
2356 Assert(resultNode
.isNull() || resultNode
.getType() == boolType
);
2358 // ensure it's a constant
2359 Assert(resultNode
.isConst());
2362 res
.emplace_back(as
.toExpr(), resultNode
.toExpr());
2368 void SmtEngine::addToModelCommandAndDump(const Command
& c
, uint32_t flags
, bool userVisible
, const char* dumpTag
) {
2369 Trace("smt") << "SMT addToModelCommandAndDump(" << c
<< ")" << endl
;
2370 SmtScope
smts(this);
2371 // If we aren't yet fully inited, the user might still turn on
2372 // produce-models. So let's keep any commands around just in
2373 // case. This is useful in two cases: (1) SMT-LIBv1 auto-declares
2374 // sort "U" in QF_UF before setLogic() is run and we still want to
2375 // support finding card(U) with --finite-model-find, and (2) to
2376 // decouple SmtEngine and ExprManager if the user does a few
2377 // ExprManager::mkSort() before SmtEngine::setOption("produce-models")
2378 // and expects to find their cardinalities in the model.
2379 if(/* userVisible && */
2380 (!d_fullyInited
|| options::produceModels()) &&
2381 (flags
& ExprManager::VAR_FLAG_DEFINED
) == 0) {
2382 if(flags
& ExprManager::VAR_FLAG_GLOBAL
) {
2383 d_modelGlobalCommands
.push_back(c
.clone());
2385 d_modelCommands
->push_back(c
.clone());
2388 if(Dump
.isOn(dumpTag
)) {
2392 d_dumpCommands
.push_back(c
.clone());
2397 // TODO(#1108): Simplify the error reporting of this method.
2398 Model
* SmtEngine::getModel() {
2399 Trace("smt") << "SMT getModel()" << endl
;
2400 SmtScope
smts(this);
2402 finalOptionsAreSet();
2404 if(Dump
.isOn("benchmark")) {
2405 Dump("benchmark") << GetModelCommand();
2408 TheoryModel
* m
= getAvailableModel("get model");
2410 // Since model m is being returned to the user, we must ensure that this
2411 // model object remains valid with future check-sat calls. Hence, we set
2412 // the theory engine into "eager model building" mode. TODO #2648: revisit.
2413 d_theoryEngine
->setEagerModelBuilding();
2415 if (options::modelCoresMode() != options::ModelCoresMode::NONE
)
2417 // If we enabled model cores, we compute a model core for m based on our
2418 // (expanded) assertions using the model core builder utility
2419 std::vector
<Expr
> eassertsProc
= getExpandedAssertions();
2420 ModelCoreBuilder::setModelCore(eassertsProc
, m
, options::modelCoresMode());
2422 m
->d_inputName
= d_filename
;
2423 m
->d_isKnownSat
= (d_smtMode
== SMT_MODE_SAT
);
2427 Result
SmtEngine::blockModel()
2429 Trace("smt") << "SMT blockModel()" << endl
;
2430 SmtScope
smts(this);
2432 finalOptionsAreSet();
2434 if (Dump
.isOn("benchmark"))
2436 Dump("benchmark") << BlockModelCommand();
2439 TheoryModel
* m
= getAvailableModel("block model");
2441 if (options::blockModelsMode() == options::BlockModelsMode::NONE
)
2443 std::stringstream ss
;
2444 ss
<< "Cannot block model when block-models is set to none.";
2445 throw ModalException(ss
.str().c_str());
2448 // get expanded assertions
2449 std::vector
<Expr
> eassertsProc
= getExpandedAssertions();
2450 Expr eblocker
= ModelBlocker::getModelBlocker(
2451 eassertsProc
, m
, options::blockModelsMode());
2452 return assertFormula(eblocker
);
2455 Result
SmtEngine::blockModelValues(const std::vector
<Expr
>& exprs
)
2457 Trace("smt") << "SMT blockModelValues()" << endl
;
2458 SmtScope
smts(this);
2460 finalOptionsAreSet();
2462 PrettyCheckArgument(
2464 "block model values must be called on non-empty set of terms");
2465 if (Dump
.isOn("benchmark"))
2467 Dump("benchmark") << BlockModelValuesCommand(exprs
);
2470 TheoryModel
* m
= getAvailableModel("block model values");
2472 // get expanded assertions
2473 std::vector
<Expr
> eassertsProc
= getExpandedAssertions();
2474 // we always do block model values mode here
2475 Expr eblocker
= ModelBlocker::getModelBlocker(
2476 eassertsProc
, m
, options::BlockModelsMode::VALUES
, exprs
);
2477 return assertFormula(eblocker
);
2480 std::pair
<Expr
, Expr
> SmtEngine::getSepHeapAndNilExpr(void)
2482 if (!d_logic
.isTheoryEnabled(THEORY_SEP
))
2485 "Cannot obtain separation logic expressions if not using the "
2486 "separation logic theory.";
2487 throw RecoverableModalException(msg
);
2489 NodeManagerScope
nms(d_nodeManager
);
2492 Model
* m
= getAvailableModel("get separation logic heap and nil");
2493 if (!m
->getHeapModel(heap
, nil
))
2496 << "SmtEngine::getSepHeapAndNilExpr(): failed to obtain heap/nil "
2497 "expressions from theory model.";
2499 return std::make_pair(heap
, nil
);
2502 std::vector
<Expr
> SmtEngine::getExpandedAssertions()
2504 std::vector
<Expr
> easserts
= getAssertions();
2505 // must expand definitions
2506 std::vector
<Expr
> eassertsProc
;
2507 std::unordered_map
<Node
, Node
, NodeHashFunction
> cache
;
2508 for (const Expr
& e
: easserts
)
2510 Node ea
= Node::fromExpr(e
);
2511 Node eae
= d_private
->getProcessAssertions()->expandDefinitions(ea
, cache
);
2512 eassertsProc
.push_back(eae
.toExpr());
2514 return eassertsProc
;
2517 Expr
SmtEngine::getSepHeapExpr() { return getSepHeapAndNilExpr().first
; }
2519 Expr
SmtEngine::getSepNilExpr() { return getSepHeapAndNilExpr().second
; }
2521 void SmtEngine::checkProof()
2523 #if (IS_LFSC_BUILD && IS_PROOFS_BUILD)
2525 Chat() << "generating proof..." << endl
;
2527 const Proof
& pf
= getProof();
2529 Chat() << "checking proof..." << endl
;
2531 std::string logicString
= d_logic
.getLogicString();
2533 std::stringstream pfStream
;
2535 pfStream
<< proof::plf_signatures
<< endl
;
2536 int64_t sizeBeforeProof
= static_cast<int64_t>(pfStream
.tellp());
2538 pf
.toStream(pfStream
);
2539 d_stats
->d_proofsSize
+=
2540 static_cast<int64_t>(pfStream
.tellp()) - sizeBeforeProof
;
2543 TimerStat::CodeTimer
checkProofTimer(d_stats
->d_lfscCheckProofTime
);
2545 lfscc_check_file(pfStream
, false, false, false, false, false, false, false);
2547 // FIXME: we should actually call lfscc_cleanup here, but lfscc_cleanup
2548 // segfaults on regress0/bv/core/bitvec7.smt
2551 #else /* (IS_LFSC_BUILD && IS_PROOFS_BUILD) */
2553 << "This version of CVC4 was built without proof support; cannot check "
2555 #endif /* (IS_LFSC_BUILD && IS_PROOFS_BUILD) */
2558 UnsatCore
SmtEngine::getUnsatCoreInternal()
2561 if (!options::unsatCores())
2563 throw ModalException(
2564 "Cannot get an unsat core when produce-unsat-cores option is off.");
2566 if (d_smtMode
!= SMT_MODE_UNSAT
)
2568 throw RecoverableModalException(
2569 "Cannot get an unsat core unless immediately preceded by "
2570 "UNSAT/ENTAILED response.");
2573 d_proofManager
->traceUnsatCore(); // just to trigger core creation
2574 return UnsatCore(this, d_proofManager
->extractUnsatCore());
2575 #else /* IS_PROOFS_BUILD */
2576 throw ModalException(
2577 "This build of CVC4 doesn't have proof support (required for unsat "
2579 #endif /* IS_PROOFS_BUILD */
2582 void SmtEngine::checkUnsatCore() {
2583 Assert(options::unsatCores())
2584 << "cannot check unsat core if unsat cores are turned off";
2586 Notice() << "SmtEngine::checkUnsatCore(): generating unsat core" << endl
;
2587 UnsatCore core
= getUnsatCore();
2589 SmtEngine
coreChecker(d_exprManager
, &d_options
);
2590 coreChecker
.setIsInternalSubsolver();
2591 coreChecker
.setLogic(getLogicInfo());
2592 coreChecker
.getOptions().set(options::checkUnsatCores
, false);
2593 coreChecker
.getOptions().set(options::checkProofs
, false);
2596 std::vector
<Command
*>::const_iterator itg
= d_defineCommands
.begin();
2597 for (; itg
!= d_defineCommands
.end(); ++itg
) {
2598 (*itg
)->invoke(&coreChecker
);
2602 Notice() << "SmtEngine::checkUnsatCore(): pushing core assertions (size == " << core
.size() << ")" << endl
;
2603 for(UnsatCore::iterator i
= core
.begin(); i
!= core
.end(); ++i
) {
2604 Notice() << "SmtEngine::checkUnsatCore(): pushing core member " << *i
<< endl
;
2605 coreChecker
.assertFormula(*i
);
2609 r
= coreChecker
.checkSat();
2613 Notice() << "SmtEngine::checkUnsatCore(): result is " << r
<< endl
;
2614 if(r
.asSatisfiabilityResult().isUnknown()) {
2616 << "SmtEngine::checkUnsatCore(): could not check core result unknown."
2619 else if (r
.asSatisfiabilityResult().isSat())
2622 << "SmtEngine::checkUnsatCore(): produced core was satisfiable.";
2626 void SmtEngine::checkModel(bool hardFailure
) {
2627 // --check-model implies --produce-assertions, which enables the
2628 // assertion list, so we should be ok.
2629 Assert(d_assertionList
!= NULL
)
2630 << "don't have an assertion list to check in SmtEngine::checkModel()";
2632 TimerStat::CodeTimer
checkModelTimer(d_stats
->d_checkModelTime
);
2634 // Throughout, we use Notice() to give diagnostic output.
2636 // If this function is running, the user gave --check-model (or equivalent),
2637 // and if Notice() is on, the user gave --verbose (or equivalent).
2639 Notice() << "SmtEngine::checkModel(): generating model" << endl
;
2640 TheoryModel
* m
= getAvailableModel("check model");
2642 // check-model is not guaranteed to succeed if approximate values were used.
2643 // Thus, we intentionally abort here.
2644 if (m
->hasApproximations())
2646 throw RecoverableModalException(
2647 "Cannot run check-model on a model with approximate values.");
2650 // Check individual theory assertions
2651 if (options::debugCheckModels())
2653 d_theoryEngine
->checkTheoryAssertionsWithModel(hardFailure
);
2659 // We have a "fake context" for the substitution map (we don't need it
2660 // to be context-dependent)
2661 context::Context fakeContext
;
2662 SubstitutionMap
substitutions(&fakeContext
, /* substituteUnderQuantifiers = */ false);
2664 for(size_t k
= 0; k
< m
->getNumCommands(); ++k
) {
2665 const DeclareFunctionCommand
* c
= dynamic_cast<const DeclareFunctionCommand
*>(m
->getCommand(k
));
2666 Notice() << "SmtEngine::checkModel(): model command " << k
<< " : " << m
->getCommand(k
) << endl
;
2668 // we don't care about DECLARE-DATATYPES, DECLARE-SORT, ...
2669 Notice() << "SmtEngine::checkModel(): skipping..." << endl
;
2671 // We have a DECLARE-FUN:
2673 // We'll first do some checks, then add to our substitution map
2674 // the mapping: function symbol |-> value
2676 Expr func
= c
->getFunction();
2677 Node val
= m
->getValue(func
);
2679 Notice() << "SmtEngine::checkModel(): adding substitution: " << func
<< " |-> " << val
<< endl
;
2681 // (1) if the value is a lambda, ensure the lambda doesn't contain the
2682 // function symbol (since then the definition is recursive)
2683 if (val
.getKind() == kind::LAMBDA
) {
2684 // first apply the model substitutions we have so far
2685 Debug("boolean-terms") << "applying subses to " << val
[1] << endl
;
2686 Node n
= substitutions
.apply(val
[1]);
2687 Debug("boolean-terms") << "++ got " << n
<< endl
;
2688 // now check if n contains func by doing a substitution
2689 // [func->func2] and checking equality of the Nodes.
2690 // (this just a way to check if func is in n.)
2691 SubstitutionMap
subs(&fakeContext
);
2692 Node func2
= NodeManager::currentNM()->mkSkolem("", TypeNode::fromType(func
.getType()), "", NodeManager::SKOLEM_NO_NOTIFY
);
2693 subs
.addSubstitution(func
, func2
);
2694 if(subs
.apply(n
) != n
) {
2695 Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE DEFINED IN TERMS OF ITSELF ***" << endl
;
2697 ss
<< "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
2698 << "considering model value for " << func
<< endl
2699 << "body of lambda is: " << val
<< endl
;
2701 ss
<< "body substitutes to: " << n
<< endl
;
2703 ss
<< "so " << func
<< " is defined in terms of itself." << endl
2704 << "Run with `--check-models -v' for additional diagnostics.";
2705 InternalError() << ss
.str();
2709 // (2) check that the value is actually a value
2710 else if (!val
.isConst())
2712 // This is only a warning since it could have been assigned an
2713 // unevaluable term (e.g. an application of a transcendental function).
2714 // This parallels the behavior (warnings for non-constant expressions)
2715 // when checking whether assertions are satisfied below.
2716 Warning() << "Warning : SmtEngine::checkModel(): "
2717 << "model value for " << func
<< endl
2718 << " is " << val
<< endl
2719 << "and that is not a constant (.isConst() == false)."
2721 << "Run with `--check-models -v' for additional diagnostics."
2725 // (3) check that it's the correct (sub)type
2726 // This was intended to be a more general check, but for now we can't do that because
2727 // e.g. "1" is an INT, which isn't a subrange type [1..10] (etc.).
2728 else if(func
.getType().isInteger() && !val
.getType().isInteger()) {
2729 Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE NOT CORRECT TYPE ***" << endl
;
2731 << "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH "
2734 << "model value for " << func
<< endl
2735 << " is " << val
<< endl
2736 << "value type is " << val
.getType() << endl
2737 << "should be of type " << func
.getType() << endl
2738 << "Run with `--check-models -v' for additional diagnostics.";
2741 // (4) checks complete, add the substitution
2742 Debug("boolean-terms") << "cm: adding subs " << func
<< " :=> " << val
<< endl
;
2743 substitutions
.addSubstitution(func
, val
);
2747 // Now go through all our user assertions checking if they're satisfied.
2748 for(AssertionList::const_iterator i
= d_assertionList
->begin(); i
!= d_assertionList
->end(); ++i
) {
2749 Notice() << "SmtEngine::checkModel(): checking assertion " << *i
<< endl
;
2750 Node n
= Node::fromExpr(*i
);
2752 // Apply any define-funs from the problem.
2754 unordered_map
<Node
, Node
, NodeHashFunction
> cache
;
2755 n
= d_private
->getProcessAssertions()->expandDefinitions(n
, cache
);
2757 Notice() << "SmtEngine::checkModel(): -- expands to " << n
<< endl
;
2759 // Apply our model value substitutions.
2760 Debug("boolean-terms") << "applying subses to " << n
<< endl
;
2761 n
= substitutions
.apply(n
);
2762 Debug("boolean-terms") << "++ got " << n
<< endl
;
2763 Notice() << "SmtEngine::checkModel(): -- substitutes to " << n
<< endl
;
2765 // We look up the value before simplifying. If n contains quantifiers,
2766 // this may increases the chance of finding its value before the node is
2767 // altered by simplification below.
2769 Notice() << "SmtEngine::checkModel(): -- get value : " << n
<< std::endl
;
2771 // Simplify the result.
2772 n
= d_private
->simplify(n
);
2773 Notice() << "SmtEngine::checkModel(): -- simplifies to " << n
<< endl
;
2775 // Replace the already-known ITEs (this is important for ground ITEs under quantifiers).
2776 n
= d_private
->d_iteRemover
.replace(n
);
2777 Notice() << "SmtEngine::checkModel(): -- ite replacement gives " << n
<< endl
;
2779 // Apply our model value substitutions (again), as things may have been simplified.
2780 Debug("boolean-terms") << "applying subses to " << n
<< endl
;
2781 n
= substitutions
.apply(n
);
2782 Debug("boolean-terms") << "++ got " << n
<< endl
;
2783 Notice() << "SmtEngine::checkModel(): -- re-substitutes to " << n
<< endl
;
2785 // As a last-ditch effort, ask model to simplify it.
2786 // Presently, this is only an issue for quantifiers, which can have a value
2787 // but don't show up in our substitution map above.
2789 Notice() << "SmtEngine::checkModel(): -- model-substitutes to " << n
<< endl
;
2793 if (n
.getConst
<bool>())
2795 // assertion is true, everything is fine
2800 // Otherwise, we did not succeed in showing the current assertion to be
2801 // true. This may either indicate that our model is wrong, or that we cannot
2802 // check it. The latter may be the case for several reasons.
2803 // For example, quantified formulas are not checkable, although we assign
2804 // them to true/false based on the satisfying assignment. However,
2805 // quantified formulas can be modified during preprocess, so they may not
2806 // correspond to those in the satisfying assignment. Hence we throw
2807 // warnings for assertions that do not simplify to either true or false.
2808 // Other theories such as non-linear arithmetic (in particular,
2809 // transcendental functions) also have the property of not being able to
2810 // be checked precisely here.
2811 // Note that warnings like these can be avoided for quantified formulas
2812 // by making preprocessing passes explicitly record how they
2813 // rewrite quantified formulas (see cvc4-wishues#43).
2816 // Not constant, print a less severe warning message here.
2817 Warning() << "Warning : SmtEngine::checkModel(): cannot check simplified "
2822 // Assertions that simplify to false result in an InternalError or
2823 // Warning being thrown below (when hardFailure is false).
2824 Notice() << "SmtEngine::checkModel(): *** PROBLEM: EXPECTED `TRUE' ***"
2827 ss
<< "SmtEngine::checkModel(): "
2828 << "ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
2829 << "assertion: " << *i
<< endl
2830 << "simplifies to: " << n
<< endl
2831 << "expected `true'." << endl
2832 << "Run with `--check-models -v' for additional diagnostics.";
2835 // internal error if hardFailure is true
2836 InternalError() << ss
.str();
2840 Warning() << ss
.str() << endl
;
2843 Notice() << "SmtEngine::checkModel(): all assertions checked out OK !" << endl
;
2846 void SmtEngine::checkSynthSolution()
2848 NodeManager
* nm
= NodeManager::currentNM();
2849 Notice() << "SmtEngine::checkSynthSolution(): checking synthesis solution" << endl
;
2850 std::map
<Node
, std::map
<Node
, Node
>> sol_map
;
2851 /* Get solutions and build auxiliary vectors for substituting */
2852 if (!d_theoryEngine
->getSynthSolutions(sol_map
))
2854 InternalError() << "SmtEngine::checkSynthSolution(): No solution to check!";
2857 if (sol_map
.empty())
2859 InternalError() << "SmtEngine::checkSynthSolution(): Got empty solution!";
2862 Trace("check-synth-sol") << "Got solution map:\n";
2863 // the set of synthesis conjectures in our assertions
2864 std::unordered_set
<Node
, NodeHashFunction
> conjs
;
2865 // For each of the above conjectures, the functions-to-synthesis and their
2866 // solutions. This is used as a substitution below.
2867 std::map
<Node
, std::vector
<Node
>> fvarMap
;
2868 std::map
<Node
, std::vector
<Node
>> fsolMap
;
2869 for (const std::pair
<const Node
, std::map
<Node
, Node
>>& cmap
: sol_map
)
2871 Trace("check-synth-sol") << "For conjecture " << cmap
.first
<< ":\n";
2872 conjs
.insert(cmap
.first
);
2873 std::vector
<Node
>& fvars
= fvarMap
[cmap
.first
];
2874 std::vector
<Node
>& fsols
= fsolMap
[cmap
.first
];
2875 for (const std::pair
<const Node
, Node
>& pair
: cmap
.second
)
2877 Trace("check-synth-sol")
2878 << " " << pair
.first
<< " --> " << pair
.second
<< "\n";
2879 fvars
.push_back(pair
.first
);
2880 fsols
.push_back(pair
.second
);
2883 Trace("check-synth-sol") << "Starting new SMT Engine\n";
2884 /* Start new SMT engine to check solutions */
2885 SmtEngine
solChecker(d_exprManager
, &d_options
);
2886 solChecker
.setIsInternalSubsolver();
2887 solChecker
.setLogic(getLogicInfo());
2888 solChecker
.getOptions().set(options::checkSynthSol
, false);
2889 solChecker
.getOptions().set(options::sygusRecFun
, false);
2891 Trace("check-synth-sol") << "Retrieving assertions\n";
2892 // Build conjecture from original assertions
2893 if (d_assertionList
== NULL
)
2895 Trace("check-synth-sol") << "No assertions to check\n";
2898 // auxiliary assertions
2899 std::vector
<Node
> auxAssertions
;
2900 // expand definitions cache
2901 std::unordered_map
<Node
, Node
, NodeHashFunction
> cache
;
2902 for (AssertionList::const_iterator i
= d_assertionList
->begin();
2903 i
!= d_assertionList
->end();
2906 Notice() << "SmtEngine::checkSynthSolution(): checking assertion " << *i
<< endl
;
2907 Trace("check-synth-sol") << "Retrieving assertion " << *i
<< "\n";
2908 Node assertion
= Node::fromExpr(*i
);
2909 // Apply any define-funs from the problem.
2911 d_private
->getProcessAssertions()->expandDefinitions(assertion
, cache
);
2912 Notice() << "SmtEngine::checkSynthSolution(): -- expands to " << assertion
2914 Trace("check-synth-sol") << "Expanded assertion " << assertion
<< "\n";
2915 if (conjs
.find(assertion
) == conjs
.end())
2917 Trace("check-synth-sol") << "It is an auxiliary assertion\n";
2918 auxAssertions
.push_back(assertion
);
2922 Trace("check-synth-sol") << "It is a synthesis conjecture\n";
2925 // check all conjectures
2926 for (const Node
& conj
: conjs
)
2928 // get the solution for this conjecture
2929 std::vector
<Node
>& fvars
= fvarMap
[conj
];
2930 std::vector
<Node
>& fsols
= fsolMap
[conj
];
2931 // Apply solution map to conjecture body
2933 /* Whether property is quantifier free */
2934 if (conj
[1].getKind() != kind::EXISTS
)
2936 conjBody
= conj
[1].substitute(
2937 fvars
.begin(), fvars
.end(), fsols
.begin(), fsols
.end());
2941 conjBody
= conj
[1][1].substitute(
2942 fvars
.begin(), fvars
.end(), fsols
.begin(), fsols
.end());
2944 /* Skolemize property */
2945 std::vector
<Node
> vars
, skos
;
2946 for (unsigned j
= 0, size
= conj
[1][0].getNumChildren(); j
< size
; ++j
)
2948 vars
.push_back(conj
[1][0][j
]);
2949 std::stringstream ss
;
2951 skos
.push_back(nm
->mkSkolem(ss
.str(), conj
[1][0][j
].getType()));
2952 Trace("check-synth-sol") << "\tSkolemizing " << conj
[1][0][j
] << " to "
2953 << skos
.back() << "\n";
2955 conjBody
= conjBody
.substitute(
2956 vars
.begin(), vars
.end(), skos
.begin(), skos
.end());
2958 Notice() << "SmtEngine::checkSynthSolution(): -- body substitutes to "
2959 << conjBody
<< endl
;
2960 Trace("check-synth-sol") << "Substituted body of assertion to " << conjBody
2962 solChecker
.assertFormula(conjBody
.toExpr());
2963 // Assert all auxiliary assertions. This may include recursive function
2964 // definitions that were added as assertions to the sygus problem.
2965 for (const Node
& a
: auxAssertions
)
2967 solChecker
.assertFormula(a
.toExpr());
2969 Result r
= solChecker
.checkSat();
2970 Notice() << "SmtEngine::checkSynthSolution(): result is " << r
<< endl
;
2971 Trace("check-synth-sol") << "Satsifiability check: " << r
<< "\n";
2972 if (r
.asSatisfiabilityResult().isUnknown())
2974 InternalError() << "SmtEngine::checkSynthSolution(): could not check "
2978 else if (r
.asSatisfiabilityResult().isSat())
2981 << "SmtEngine::checkSynthSolution(): produced solution leads to "
2982 "satisfiable negated conjecture.";
2984 solChecker
.resetAssertions();
2988 void SmtEngine::checkInterpol(Expr interpol
,
2989 const std::vector
<Expr
>& easserts
,
2994 void SmtEngine::checkAbduct(Node a
)
2996 Assert(a
.getType().isBoolean());
2997 // check it with the abduction solver
2998 return d_abductSolver
->checkAbduct(a
);
3001 // TODO(#1108): Simplify the error reporting of this method.
3002 UnsatCore
SmtEngine::getUnsatCore() {
3003 Trace("smt") << "SMT getUnsatCore()" << endl
;
3004 SmtScope
smts(this);
3005 finalOptionsAreSet();
3006 if(Dump
.isOn("benchmark")) {
3007 Dump("benchmark") << GetUnsatCoreCommand();
3009 return getUnsatCoreInternal();
3012 // TODO(#1108): Simplify the error reporting of this method.
3013 const Proof
& SmtEngine::getProof()
3015 Trace("smt") << "SMT getProof()" << endl
;
3016 SmtScope
smts(this);
3017 finalOptionsAreSet();
3018 if(Dump
.isOn("benchmark")) {
3019 Dump("benchmark") << GetProofCommand();
3022 if(!options::proof()) {
3023 throw ModalException("Cannot get a proof when produce-proofs option is off.");
3025 if (d_smtMode
!= SMT_MODE_UNSAT
)
3027 throw RecoverableModalException(
3028 "Cannot get a proof unless immediately preceded by UNSAT/ENTAILED "
3032 return ProofManager::getProof(this);
3033 #else /* IS_PROOFS_BUILD */
3034 throw ModalException("This build of CVC4 doesn't have proof support.");
3035 #endif /* IS_PROOFS_BUILD */
3038 void SmtEngine::printInstantiations( std::ostream
& out
) {
3039 SmtScope
smts(this);
3040 finalOptionsAreSet();
3041 if (options::instFormatMode() == options::InstFormatMode::SZS
)
3043 out
<< "% SZS output start Proof for " << d_filename
.c_str() << std::endl
;
3045 if( d_theoryEngine
){
3046 d_theoryEngine
->printInstantiations( out
);
3050 if (options::instFormatMode() == options::InstFormatMode::SZS
)
3052 out
<< "% SZS output end Proof for " << d_filename
.c_str() << std::endl
;
3056 void SmtEngine::printSynthSolution( std::ostream
& out
) {
3057 SmtScope
smts(this);
3058 finalOptionsAreSet();
3059 if( d_theoryEngine
){
3060 d_theoryEngine
->printSynthSolution( out
);
3066 bool SmtEngine::getSynthSolutions(std::map
<Expr
, Expr
>& sol_map
)
3068 SmtScope
smts(this);
3069 finalOptionsAreSet();
3070 std::map
<Node
, std::map
<Node
, Node
>> sol_mapn
;
3071 Assert(d_theoryEngine
!= nullptr);
3072 // fail if the theory engine does not have synthesis solutions
3073 if (!d_theoryEngine
->getSynthSolutions(sol_mapn
))
3077 for (std::pair
<const Node
, std::map
<Node
, Node
>>& cs
: sol_mapn
)
3079 for (std::pair
<const Node
, Node
>& s
: cs
.second
)
3081 sol_map
[s
.first
.toExpr()] = s
.second
.toExpr();
3087 Expr
SmtEngine::doQuantifierElimination(const Expr
& e
, bool doFull
, bool strict
)
3089 SmtScope
smts(this);
3090 finalOptionsAreSet();
3091 if(!d_logic
.isPure(THEORY_ARITH
) && strict
){
3092 Warning() << "Unexpected logic for quantifier elimination " << d_logic
<< endl
;
3094 Trace("smt-qe") << "Do quantifier elimination " << e
<< std::endl
;
3095 Node n_e
= Node::fromExpr( e
);
3096 if (n_e
.getKind() != kind::EXISTS
&& n_e
.getKind() != kind::FORALL
)
3098 throw ModalException(
3099 "Expecting a quantified formula as argument to get-qe.");
3101 //tag the quantified formula with the quant-elim attribute
3102 TypeNode t
= NodeManager::currentNM()->booleanType();
3103 Node n_attr
= NodeManager::currentNM()->mkSkolem("qe", t
, "Auxiliary variable for qe attr.");
3104 std::vector
< Node
> node_values
;
3105 d_theoryEngine
->setUserAttribute( doFull
? "quant-elim" : "quant-elim-partial", n_attr
, node_values
, "");
3106 n_attr
= NodeManager::currentNM()->mkNode(kind::INST_ATTRIBUTE
, n_attr
);
3107 n_attr
= NodeManager::currentNM()->mkNode(kind::INST_PATTERN_LIST
, n_attr
);
3108 std::vector
< Node
> e_children
;
3109 e_children
.push_back( n_e
[0] );
3110 e_children
.push_back(n_e
.getKind() == kind::EXISTS
? n_e
[1]
3112 e_children
.push_back( n_attr
);
3113 Node nn_e
= NodeManager::currentNM()->mkNode( kind::EXISTS
, e_children
);
3114 Trace("smt-qe-debug") << "Query for quantifier elimination : " << nn_e
<< std::endl
;
3115 Assert(nn_e
.getNumChildren() == 3);
3116 Result r
= checkSatisfiability(nn_e
.toExpr(), true, true);
3117 Trace("smt-qe") << "Query returned " << r
<< std::endl
;
3118 if(r
.asSatisfiabilityResult().isSat() != Result::UNSAT
) {
3119 if( r
.asSatisfiabilityResult().isSat() != Result::SAT
&& doFull
){
3121 << "While performing quantifier elimination, unexpected result : "
3122 << r
<< " for query.";
3123 // failed, return original
3126 std::vector
< Node
> inst_qs
;
3127 d_theoryEngine
->getInstantiatedQuantifiedFormulas( inst_qs
);
3128 Assert(inst_qs
.size() <= 1);
3130 if( inst_qs
.size()==1 ){
3131 Node top_q
= inst_qs
[0];
3132 //Node top_q = Rewriter::rewrite( nn_e ).negate();
3133 Assert(top_q
.getKind() == kind::FORALL
);
3134 Trace("smt-qe") << "Get qe for " << top_q
<< std::endl
;
3135 ret_n
= d_theoryEngine
->getInstantiatedConjunction( top_q
);
3136 Trace("smt-qe") << "Returned : " << ret_n
<< std::endl
;
3137 if (n_e
.getKind() == kind::EXISTS
)
3139 ret_n
= Rewriter::rewrite(ret_n
.negate());
3142 ret_n
= NodeManager::currentNM()->mkConst(n_e
.getKind() != kind::EXISTS
);
3144 // do extended rewrite to minimize the size of the formula aggressively
3145 theory::quantifiers::ExtendedRewriter
extr(true);
3146 ret_n
= extr
.extendedRewrite(ret_n
);
3147 return ret_n
.toExpr();
3149 return NodeManager::currentNM()
3150 ->mkConst(n_e
.getKind() == kind::EXISTS
)
3155 bool SmtEngine::getInterpol(const Expr
& conj
,
3156 const Type
& grammarType
,
3162 bool SmtEngine::getInterpol(const Expr
& conj
, Expr
& interpol
)
3165 return getInterpol(conj
, grammarType
, interpol
);
3168 bool SmtEngine::getAbduct(const Node
& conj
,
3169 const TypeNode
& grammarType
,
3172 if (d_abductSolver
->getAbduct(conj
, grammarType
, abd
))
3174 // successfully generated an abduct, update to abduct state
3175 d_smtMode
= SMT_MODE_ABDUCT
;
3178 // failed, we revert to the assert state
3179 d_smtMode
= SMT_MODE_ASSERT
;
3183 bool SmtEngine::getAbduct(const Node
& conj
, Node
& abd
)
3185 TypeNode grammarType
;
3186 return getAbduct(conj
, grammarType
, abd
);
3189 void SmtEngine::getInstantiatedQuantifiedFormulas( std::vector
< Expr
>& qs
) {
3190 SmtScope
smts(this);
3191 if( d_theoryEngine
){
3192 std::vector
< Node
> qs_n
;
3193 d_theoryEngine
->getInstantiatedQuantifiedFormulas( qs_n
);
3194 for( unsigned i
=0; i
<qs_n
.size(); i
++ ){
3195 qs
.push_back( qs_n
[i
].toExpr() );
3202 void SmtEngine::getInstantiations( Expr q
, std::vector
< Expr
>& insts
) {
3203 SmtScope
smts(this);
3204 if( d_theoryEngine
){
3205 std::vector
< Node
> insts_n
;
3206 d_theoryEngine
->getInstantiations( Node::fromExpr( q
), insts_n
);
3207 for( unsigned i
=0; i
<insts_n
.size(); i
++ ){
3208 insts
.push_back( insts_n
[i
].toExpr() );
3215 void SmtEngine::getInstantiationTermVectors( Expr q
, std::vector
< std::vector
< Expr
> >& tvecs
) {
3216 SmtScope
smts(this);
3217 Assert(options::trackInstLemmas());
3218 if( d_theoryEngine
){
3219 std::vector
< std::vector
< Node
> > tvecs_n
;
3220 d_theoryEngine
->getInstantiationTermVectors( Node::fromExpr( q
), tvecs_n
);
3221 for( unsigned i
=0; i
<tvecs_n
.size(); i
++ ){
3222 std::vector
< Expr
> tvec
;
3223 for( unsigned j
=0; j
<tvecs_n
[i
].size(); j
++ ){
3224 tvec
.push_back( tvecs_n
[i
][j
].toExpr() );
3226 tvecs
.push_back( tvec
);
3233 vector
<Expr
> SmtEngine::getAssertions() {
3234 SmtScope
smts(this);
3235 finalOptionsAreSet();
3237 if(Dump
.isOn("benchmark")) {
3238 Dump("benchmark") << GetAssertionsCommand();
3240 Trace("smt") << "SMT getAssertions()" << endl
;
3241 if(!options::produceAssertions()) {
3243 "Cannot query the current assertion list when not in produce-assertions mode.";
3244 throw ModalException(msg
);
3246 Assert(d_assertionList
!= NULL
);
3247 // copy the result out
3248 return vector
<Expr
>(d_assertionList
->begin(), d_assertionList
->end());
3251 void SmtEngine::push()
3253 SmtScope
smts(this);
3254 finalOptionsAreSet();
3256 Trace("smt") << "SMT push()" << endl
;
3257 d_private
->notifyPush();
3258 d_private
->processAssertions();
3259 if(Dump
.isOn("benchmark")) {
3260 Dump("benchmark") << PushCommand();
3262 if(!options::incrementalSolving()) {
3263 throw ModalException("Cannot push when not solving incrementally (use --incremental)");
3267 // The problem isn't really "extended" yet, but this disallows
3268 // get-model after a push, simplifying our lives somewhat and
3269 // staying symmetric with pop.
3270 setProblemExtended();
3272 d_userLevels
.push_back(d_userContext
->getLevel());
3274 Trace("userpushpop") << "SmtEngine: pushed to level "
3275 << d_userContext
->getLevel() << endl
;
3278 void SmtEngine::pop() {
3279 SmtScope
smts(this);
3280 finalOptionsAreSet();
3281 Trace("smt") << "SMT pop()" << endl
;
3282 if(Dump
.isOn("benchmark")) {
3283 Dump("benchmark") << PopCommand();
3285 if(!options::incrementalSolving()) {
3286 throw ModalException("Cannot pop when not solving incrementally (use --incremental)");
3288 if(d_userLevels
.size() == 0) {
3289 throw ModalException("Cannot pop beyond the first user frame");
3292 // The problem isn't really "extended" yet, but this disallows
3293 // get-model after a pop, simplifying our lives somewhat. It might
3294 // not be strictly necessary to do so, since the pops occur lazily,
3295 // but also it would be weird to have a legally-executed (get-model)
3296 // that only returns a subset of the assignment (because the rest
3297 // is no longer in scope!).
3298 setProblemExtended();
3300 AlwaysAssert(d_userContext
->getLevel() > 0);
3301 AlwaysAssert(d_userLevels
.back() < d_userContext
->getLevel());
3302 while (d_userLevels
.back() < d_userContext
->getLevel()) {
3305 d_userLevels
.pop_back();
3307 // Clear out assertion queues etc., in case anything is still in there
3308 d_private
->notifyPop();
3310 Trace("userpushpop") << "SmtEngine: popped to level "
3311 << d_userContext
->getLevel() << endl
;
3312 // FIXME: should we reset d_status here?
3313 // SMT-LIBv2 spec seems to imply no, but it would make sense to..
3316 void SmtEngine::internalPush() {
3317 Assert(d_fullyInited
);
3318 Trace("smt") << "SmtEngine::internalPush()" << endl
;
3320 if(options::incrementalSolving()) {
3321 d_private
->processAssertions();
3322 TimerStat::CodeTimer
pushPopTimer(d_stats
->d_pushPopTime
);
3323 d_userContext
->push();
3324 // the d_context push is done inside of the SAT solver
3325 d_propEngine
->push();
3329 void SmtEngine::internalPop(bool immediate
) {
3330 Assert(d_fullyInited
);
3331 Trace("smt") << "SmtEngine::internalPop()" << endl
;
3332 if(options::incrementalSolving()) {
3340 void SmtEngine::doPendingPops() {
3341 Trace("smt") << "SmtEngine::doPendingPops()" << endl
;
3342 Assert(d_pendingPops
== 0 || options::incrementalSolving());
3343 // check to see if a postsolve() is pending
3344 if (d_needPostsolve
)
3346 d_propEngine
->resetTrail();
3348 while(d_pendingPops
> 0) {
3349 TimerStat::CodeTimer
pushPopTimer(d_stats
->d_pushPopTime
);
3350 d_propEngine
->pop();
3351 // the d_context pop is done inside of the SAT solver
3352 d_userContext
->pop();
3355 if (d_needPostsolve
)
3357 d_theoryEngine
->postsolve();
3358 d_needPostsolve
= false;
3362 void SmtEngine::reset()
3364 SmtScope
smts(this);
3365 ExprManager
*em
= d_exprManager
;
3366 Trace("smt") << "SMT reset()" << endl
;
3367 if(Dump
.isOn("benchmark")) {
3368 Dump("benchmark") << ResetCommand();
3371 opts
.copyValues(d_originalOptions
);
3373 new (this) SmtEngine(em
, &opts
);
3376 void SmtEngine::resetAssertions()
3378 SmtScope
smts(this);
3382 // We're still in Start Mode, nothing asserted yet, do nothing.
3383 // (see solver execution modes in the SMT-LIB standard)
3384 Assert(d_context
->getLevel() == 0);
3385 Assert(d_userContext
->getLevel() == 0);
3386 DeleteAndClearCommandVector(d_modelGlobalCommands
);
3392 Trace("smt") << "SMT resetAssertions()" << endl
;
3393 if (Dump
.isOn("benchmark"))
3395 Dump("benchmark") << ResetAssertionsCommand();
3398 while (!d_userLevels
.empty())
3403 // Remember the global push/pop around everything when beyond Start mode
3404 // (see solver execution modes in the SMT-LIB standard)
3405 Assert(d_userLevels
.size() == 0 && d_userContext
->getLevel() == 1);
3406 d_context
->popto(0);
3407 d_userContext
->popto(0);
3408 DeleteAndClearCommandVector(d_modelGlobalCommands
);
3409 d_userContext
->push();
3412 /* Create new PropEngine.
3413 * First force destruction of referenced PropEngine to enforce that
3414 * statistics are unregistered by the obsolete PropEngine object before
3415 * registered again by the new PropEngine object */
3416 d_propEngine
.reset(nullptr);
3417 d_propEngine
.reset(new PropEngine(
3418 getTheoryEngine(), getContext(), getUserContext(), getResourceManager()));
3419 d_theoryEngine
->setPropEngine(getPropEngine());
3422 void SmtEngine::interrupt()
3424 if(!d_fullyInited
) {
3427 d_propEngine
->interrupt();
3428 d_theoryEngine
->interrupt();
3431 void SmtEngine::setResourceLimit(unsigned long units
, bool cumulative
) {
3432 d_resourceManager
->setResourceLimit(units
, cumulative
);
3434 void SmtEngine::setTimeLimit(unsigned long milis
, bool cumulative
) {
3435 d_resourceManager
->setTimeLimit(milis
, cumulative
);
3438 unsigned long SmtEngine::getResourceUsage() const {
3439 return d_resourceManager
->getResourceUsage();
3442 unsigned long SmtEngine::getTimeUsage() const {
3443 return d_resourceManager
->getTimeUsage();
3446 unsigned long SmtEngine::getResourceRemaining() const
3448 return d_resourceManager
->getResourceRemaining();
3451 unsigned long SmtEngine::getTimeRemaining() const
3453 return d_resourceManager
->getTimeRemaining();
3456 NodeManager
* SmtEngine::getNodeManager() const
3458 return d_exprManager
->getNodeManager();
3461 Statistics
SmtEngine::getStatistics() const
3463 return Statistics(*d_statisticsRegistry
);
3466 SExpr
SmtEngine::getStatistic(std::string name
) const
3468 return d_statisticsRegistry
->getStatistic(name
);
3471 void SmtEngine::safeFlushStatistics(int fd
) const {
3472 d_statisticsRegistry
->safeFlushInformation(fd
);
3475 void SmtEngine::setUserAttribute(const std::string
& attr
,
3477 const std::vector
<Expr
>& expr_values
,
3478 const std::string
& str_value
)
3480 SmtScope
smts(this);
3481 finalOptionsAreSet();
3482 std::vector
<Node
> node_values
;
3483 for( unsigned i
=0; i
<expr_values
.size(); i
++ ){
3484 node_values
.push_back( expr_values
[i
].getNode() );
3486 d_theoryEngine
->setUserAttribute(attr
, expr
.getNode(), node_values
, str_value
);
3489 void SmtEngine::setPrintFuncInModel(Expr f
, bool p
) {
3490 Trace("setp-model") << "Set printInModel " << f
<< " to " << p
<< std::endl
;
3491 for( unsigned i
=0; i
<d_modelGlobalCommands
.size(); i
++ ){
3492 Command
* c
= d_modelGlobalCommands
[i
];
3493 DeclareFunctionCommand
* dfc
= dynamic_cast<DeclareFunctionCommand
*>(c
);
3495 if( dfc
->getFunction()==f
){
3496 dfc
->setPrintInModel( p
);
3500 for( unsigned i
=0; i
<d_modelCommands
->size(); i
++ ){
3501 Command
* c
= (*d_modelCommands
)[i
];
3502 DeclareFunctionCommand
* dfc
= dynamic_cast<DeclareFunctionCommand
*>(c
);
3504 if( dfc
->getFunction()==f
){
3505 dfc
->setPrintInModel( p
);
3511 void SmtEngine::beforeSearch()
3514 throw ModalException(
3515 "SmtEngine::beforeSearch called after initialization.");
3520 void SmtEngine::setOption(const std::string
& key
, const CVC4::SExpr
& value
)
3522 NodeManagerScope
nms(d_nodeManager
);
3523 Trace("smt") << "SMT setOption(" << key
<< ", " << value
<< ")" << endl
;
3525 if(Dump
.isOn("benchmark")) {
3526 Dump("benchmark") << SetOptionCommand(key
, value
);
3529 if(key
== "command-verbosity") {
3530 if(!value
.isAtom()) {
3531 const vector
<SExpr
>& cs
= value
.getChildren();
3532 if(cs
.size() == 2 &&
3533 (cs
[0].isKeyword() || cs
[0].isString()) &&
3534 cs
[1].isInteger()) {
3535 string c
= cs
[0].getValue();
3536 const Integer
& v
= cs
[1].getIntegerValue();
3537 if(v
< 0 || v
> 2) {
3538 throw OptionException("command-verbosity must be 0, 1, or 2");
3540 d_commandVerbosity
[c
] = v
;
3544 throw OptionException("command-verbosity value must be a tuple (command-name, integer)");
3547 if(!value
.isAtom()) {
3548 throw OptionException("bad value for :" + key
);
3551 string optionarg
= value
.getValue();
3552 d_options
.setOption(key
, optionarg
);
3555 void SmtEngine::setIsInternalSubsolver() { d_isInternalSubsolver
= true; }
3557 bool SmtEngine::isInternalSubsolver() const { return d_isInternalSubsolver
; }
3559 CVC4::SExpr
SmtEngine::getOption(const std::string
& key
) const
3561 NodeManagerScope
nms(d_nodeManager
);
3563 Trace("smt") << "SMT getOption(" << key
<< ")" << endl
;
3565 if(key
.length() >= 18 &&
3566 key
.compare(0, 18, "command-verbosity:") == 0) {
3567 map
<string
, Integer
>::const_iterator i
= d_commandVerbosity
.find(key
.c_str() + 18);
3568 if(i
!= d_commandVerbosity
.end()) {
3569 return SExpr((*i
).second
);
3571 i
= d_commandVerbosity
.find("*");
3572 if(i
!= d_commandVerbosity
.end()) {
3573 return SExpr((*i
).second
);
3575 return SExpr(Integer(2));
3578 if(Dump
.isOn("benchmark")) {
3579 Dump("benchmark") << GetOptionCommand(key
);
3582 if(key
== "command-verbosity") {
3583 vector
<SExpr
> result
;
3584 SExpr defaultVerbosity
;
3585 for(map
<string
, Integer
>::const_iterator i
= d_commandVerbosity
.begin();
3586 i
!= d_commandVerbosity
.end();
3589 v
.push_back(SExpr((*i
).first
));
3590 v
.push_back(SExpr((*i
).second
));
3591 if((*i
).first
== "*") {
3592 // put the default at the end of the SExpr
3593 defaultVerbosity
= SExpr(v
);
3595 result
.push_back(SExpr(v
));
3598 // put the default at the end of the SExpr
3599 if(!defaultVerbosity
.isAtom()) {
3600 result
.push_back(defaultVerbosity
);
3602 // ensure the default is always listed
3604 v
.push_back(SExpr("*"));
3605 v
.push_back(SExpr(Integer(2)));
3606 result
.push_back(SExpr(v
));
3608 return SExpr(result
);
3611 return SExpr::parseAtom(d_options
.getOption(key
));
3614 bool SmtEngine::getExpressionName(Expr e
, std::string
& name
) const {
3615 return d_private
->getExpressionName(e
, name
);
3618 void SmtEngine::setExpressionName(Expr e
, const std::string
& name
) {
3619 Trace("smt-debug") << "Set expression name " << e
<< " to " << name
<< std::endl
;
3620 d_private
->setExpressionName(e
,name
);
3623 Options
& SmtEngine::getOptions() { return d_options
; }
3625 const Options
& SmtEngine::getOptions() const { return d_options
; }
3627 ResourceManager
* SmtEngine::getResourceManager()
3629 return d_resourceManager
.get();
3632 void SmtEngine::setSygusConjectureStale()
3634 if (d_private
->d_sygusConjectureStale
)
3639 d_private
->d_sygusConjectureStale
= true;
3640 if (options::incrementalSolving())
3646 }/* CVC4 namespace */