1 /********************* */
2 /*! \file smt_engine.cpp
4 ** Top contributors (to current version):
5 ** Morgan Deters, Andrew Reynolds, Tim King
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2018 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 "base/configuration.h"
33 #include "base/configuration_private.h"
34 #include "base/exception.h"
35 #include "base/listener.h"
36 #include "base/modal_exception.h"
37 #include "base/output.h"
38 #include "context/cdhashmap.h"
39 #include "context/cdhashset.h"
40 #include "context/cdlist.h"
41 #include "context/context.h"
42 #include "decision/decision_engine.h"
43 #include "expr/attribute.h"
44 #include "expr/expr.h"
45 #include "expr/kind.h"
46 #include "expr/metakind.h"
47 #include "expr/node.h"
48 #include "expr/node_algorithm.h"
49 #include "expr/node_builder.h"
50 #include "expr/node_self_iterator.h"
51 #include "options/arith_options.h"
52 #include "options/arrays_options.h"
53 #include "options/base_options.h"
54 #include "options/booleans_options.h"
55 #include "options/bv_options.h"
56 #include "options/datatypes_options.h"
57 #include "options/decision_mode.h"
58 #include "options/decision_options.h"
59 #include "options/language.h"
60 #include "options/main_options.h"
61 #include "options/open_ostream.h"
62 #include "options/option_exception.h"
63 #include "options/printer_options.h"
64 #include "options/proof_options.h"
65 #include "options/prop_options.h"
66 #include "options/quantifiers_options.h"
67 #include "options/sep_options.h"
68 #include "options/set_language.h"
69 #include "options/smt_options.h"
70 #include "options/strings_options.h"
71 #include "options/theory_options.h"
72 #include "options/uf_options.h"
73 #include "preprocessing/preprocessing_pass.h"
74 #include "preprocessing/preprocessing_pass_context.h"
75 #include "preprocessing/preprocessing_pass_registry.h"
76 #include "printer/printer.h"
77 #include "proof/proof.h"
78 #include "proof/proof_manager.h"
79 #include "proof/theory_proof.h"
80 #include "proof/unsat_core.h"
81 #include "prop/prop_engine.h"
82 #include "smt/command.h"
83 #include "smt/command_list.h"
84 #include "smt/logic_request.h"
85 #include "smt/managed_ostreams.h"
86 #include "smt/model_core_builder.h"
87 #include "smt/smt_engine_scope.h"
88 #include "smt/term_formula_removal.h"
89 #include "smt/update_ostream.h"
90 #include "smt_util/boolean_simplification.h"
91 #include "smt_util/nary_builder.h"
92 #include "smt_util/node_visitor.h"
93 #include "theory/booleans/circuit_propagator.h"
94 #include "theory/bv/theory_bv_rewriter.h"
95 #include "theory/logic_info.h"
96 #include "theory/quantifiers/fun_def_process.h"
97 #include "theory/quantifiers/quantifiers_rewriter.h"
98 #include "theory/quantifiers/single_inv_partition.h"
99 #include "theory/quantifiers/sygus/synth_engine.h"
100 #include "theory/quantifiers/term_util.h"
101 #include "theory/rewriter.h"
102 #include "theory/sort_inference.h"
103 #include "theory/strings/theory_strings.h"
104 #include "theory/substitutions.h"
105 #include "theory/theory_engine.h"
106 #include "theory/theory_model.h"
107 #include "theory/theory_traits.h"
108 #include "util/hash.h"
109 #include "util/proof.h"
110 #include "util/random.h"
111 #include "util/resource_manager.h"
114 using namespace CVC4
;
115 using namespace CVC4::smt
;
116 using namespace CVC4::preprocessing
;
117 using namespace CVC4::prop
;
118 using namespace CVC4::context
;
119 using namespace CVC4::theory
;
124 struct DeleteCommandFunction
: public std::unary_function
<const Command
*, void>
126 void operator()(const Command
* command
) { delete command
; }
129 void DeleteAndClearCommandVector(std::vector
<Command
*>& commands
) {
130 std::for_each(commands
.begin(), commands
.end(), DeleteCommandFunction());
134 /** Useful for counting the number of recursive calls. */
139 ScopeCounter(unsigned& d
) : d_depth(d
) {
148 * Representation of a defined function. We keep these around in
149 * SmtEngine to permit expanding definitions late (and lazily), to
150 * support getValue() over defined functions, to support user output
151 * in terms of defined functions, etc.
153 class DefinedFunction
{
155 vector
<Node
> d_formals
;
159 DefinedFunction(Node func
, vector
<Node
> formals
, Node formula
) :
164 Node
getFunction() const { return d_func
; }
165 vector
<Node
> getFormals() const { return d_formals
; }
166 Node
getFormula() const { return d_formula
; }
167 };/* class DefinedFunction */
169 struct SmtEngineStatistics
{
170 /** time spent in definition-expansion */
171 TimerStat d_definitionExpansionTime
;
172 /** number of constant propagations found during nonclausal simp */
173 IntStat d_numConstantProps
;
174 /** time spent converting to CNF */
175 TimerStat d_cnfConversionTime
;
176 /** Num of assertions before ite removal */
177 IntStat d_numAssertionsPre
;
178 /** Num of assertions after ite removal */
179 IntStat d_numAssertionsPost
;
180 /** time spent in checkModel() */
181 TimerStat d_checkModelTime
;
182 /** time spent in checkProof() */
183 TimerStat d_checkProofTime
;
184 /** time spent in checkUnsatCore() */
185 TimerStat d_checkUnsatCoreTime
;
186 /** time spent in PropEngine::checkSat() */
187 TimerStat d_solveTime
;
188 /** time spent in pushing/popping */
189 TimerStat d_pushPopTime
;
190 /** time spent in processAssertions() */
191 TimerStat d_processAssertionsTime
;
193 /** Has something simplified to false? */
194 IntStat d_simplifiedToFalse
;
195 /** Number of resource units spent. */
196 ReferenceStat
<uint64_t> d_resourceUnitsUsed
;
198 SmtEngineStatistics() :
199 d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"),
200 d_numConstantProps("smt::SmtEngine::numConstantProps", 0),
201 d_cnfConversionTime("smt::SmtEngine::cnfConversionTime"),
202 d_numAssertionsPre("smt::SmtEngine::numAssertionsPreITERemoval", 0),
203 d_numAssertionsPost("smt::SmtEngine::numAssertionsPostITERemoval", 0),
204 d_checkModelTime("smt::SmtEngine::checkModelTime"),
205 d_checkProofTime("smt::SmtEngine::checkProofTime"),
206 d_checkUnsatCoreTime("smt::SmtEngine::checkUnsatCoreTime"),
207 d_solveTime("smt::SmtEngine::solveTime"),
208 d_pushPopTime("smt::SmtEngine::pushPopTime"),
209 d_processAssertionsTime("smt::SmtEngine::processAssertionsTime"),
210 d_simplifiedToFalse("smt::SmtEngine::simplifiedToFalse", 0),
211 d_resourceUnitsUsed("smt::SmtEngine::resourceUnitsUsed")
213 smtStatisticsRegistry()->registerStat(&d_definitionExpansionTime
);
214 smtStatisticsRegistry()->registerStat(&d_numConstantProps
);
215 smtStatisticsRegistry()->registerStat(&d_cnfConversionTime
);
216 smtStatisticsRegistry()->registerStat(&d_numAssertionsPre
);
217 smtStatisticsRegistry()->registerStat(&d_numAssertionsPost
);
218 smtStatisticsRegistry()->registerStat(&d_checkModelTime
);
219 smtStatisticsRegistry()->registerStat(&d_checkProofTime
);
220 smtStatisticsRegistry()->registerStat(&d_checkUnsatCoreTime
);
221 smtStatisticsRegistry()->registerStat(&d_solveTime
);
222 smtStatisticsRegistry()->registerStat(&d_pushPopTime
);
223 smtStatisticsRegistry()->registerStat(&d_processAssertionsTime
);
224 smtStatisticsRegistry()->registerStat(&d_simplifiedToFalse
);
225 smtStatisticsRegistry()->registerStat(&d_resourceUnitsUsed
);
228 ~SmtEngineStatistics() {
229 smtStatisticsRegistry()->unregisterStat(&d_definitionExpansionTime
);
230 smtStatisticsRegistry()->unregisterStat(&d_numConstantProps
);
231 smtStatisticsRegistry()->unregisterStat(&d_cnfConversionTime
);
232 smtStatisticsRegistry()->unregisterStat(&d_numAssertionsPre
);
233 smtStatisticsRegistry()->unregisterStat(&d_numAssertionsPost
);
234 smtStatisticsRegistry()->unregisterStat(&d_checkModelTime
);
235 smtStatisticsRegistry()->unregisterStat(&d_checkProofTime
);
236 smtStatisticsRegistry()->unregisterStat(&d_checkUnsatCoreTime
);
237 smtStatisticsRegistry()->unregisterStat(&d_solveTime
);
238 smtStatisticsRegistry()->unregisterStat(&d_pushPopTime
);
239 smtStatisticsRegistry()->unregisterStat(&d_processAssertionsTime
);
240 smtStatisticsRegistry()->unregisterStat(&d_simplifiedToFalse
);
241 smtStatisticsRegistry()->unregisterStat(&d_resourceUnitsUsed
);
243 };/* struct SmtEngineStatistics */
246 class SoftResourceOutListener
: public Listener
{
248 SoftResourceOutListener(SmtEngine
& smt
) : d_smt(&smt
) {}
249 void notify() override
251 SmtScope
scope(d_smt
);
252 Assert(smt::smtEngineInScope());
257 }; /* class SoftResourceOutListener */
260 class HardResourceOutListener
: public Listener
{
262 HardResourceOutListener(SmtEngine
& smt
) : d_smt(&smt
) {}
263 void notify() override
265 SmtScope
scope(d_smt
);
266 theory::Rewriter::clearCaches();
270 }; /* class HardResourceOutListener */
272 class SetLogicListener
: public Listener
{
274 SetLogicListener(SmtEngine
& smt
) : d_smt(&smt
) {}
275 void notify() override
277 LogicInfo
inOptions(options::forceLogicString());
278 d_smt
->setLogic(inOptions
);
282 }; /* class SetLogicListener */
284 class BeforeSearchListener
: public Listener
{
286 BeforeSearchListener(SmtEngine
& smt
) : d_smt(&smt
) {}
287 void notify() override
{ d_smt
->beforeSearch(); }
291 }; /* class BeforeSearchListener */
293 class UseTheoryListListener
: public Listener
{
295 UseTheoryListListener(TheoryEngine
* theoryEngine
)
296 : d_theoryEngine(theoryEngine
)
299 void notify() override
301 std::stringstream
commaList(options::useTheoryList());
304 Debug("UseTheoryListListener") << "UseTheoryListListener::notify() "
305 << options::useTheoryList() << std::endl
;
307 while(std::getline(commaList
, token
, ',')){
308 if(token
== "help") {
309 puts(theory::useTheoryHelp
);
312 if(theory::useTheoryValidate(token
)) {
313 d_theoryEngine
->enableTheoryAlternative(token
);
315 throw OptionException(
316 std::string("unknown option for --use-theory : `") + token
+
317 "'. Try --use-theory=help.");
323 TheoryEngine
* d_theoryEngine
;
324 }; /* class UseTheoryListListener */
327 class SetDefaultExprDepthListener
: public Listener
{
329 void notify() override
331 int depth
= options::defaultExprDepth();
332 Debug
.getStream() << expr::ExprSetDepth(depth
);
333 Trace
.getStream() << expr::ExprSetDepth(depth
);
334 Notice
.getStream() << expr::ExprSetDepth(depth
);
335 Chat
.getStream() << expr::ExprSetDepth(depth
);
336 Message
.getStream() << expr::ExprSetDepth(depth
);
337 Warning
.getStream() << expr::ExprSetDepth(depth
);
338 // intentionally exclude Dump stream from this list
342 class SetDefaultExprDagListener
: public Listener
{
344 void notify() override
346 int dag
= options::defaultDagThresh();
347 Debug
.getStream() << expr::ExprDag(dag
);
348 Trace
.getStream() << expr::ExprDag(dag
);
349 Notice
.getStream() << expr::ExprDag(dag
);
350 Chat
.getStream() << expr::ExprDag(dag
);
351 Message
.getStream() << expr::ExprDag(dag
);
352 Warning
.getStream() << expr::ExprDag(dag
);
353 Dump
.getStream() << expr::ExprDag(dag
);
357 class SetPrintExprTypesListener
: public Listener
{
359 void notify() override
361 bool value
= options::printExprTypes();
362 Debug
.getStream() << expr::ExprPrintTypes(value
);
363 Trace
.getStream() << expr::ExprPrintTypes(value
);
364 Notice
.getStream() << expr::ExprPrintTypes(value
);
365 Chat
.getStream() << expr::ExprPrintTypes(value
);
366 Message
.getStream() << expr::ExprPrintTypes(value
);
367 Warning
.getStream() << expr::ExprPrintTypes(value
);
368 // intentionally exclude Dump stream from this list
372 class DumpModeListener
: public Listener
{
374 void notify() override
376 const std::string
& value
= options::dumpModeString();
377 Dump
.setDumpFromString(value
);
381 class PrintSuccessListener
: public Listener
{
383 void notify() override
385 bool value
= options::printSuccess();
386 Debug
.getStream() << Command::printsuccess(value
);
387 Trace
.getStream() << Command::printsuccess(value
);
388 Notice
.getStream() << Command::printsuccess(value
);
389 Chat
.getStream() << Command::printsuccess(value
);
390 Message
.getStream() << Command::printsuccess(value
);
391 Warning
.getStream() << Command::printsuccess(value
);
392 *options::out() << Command::printsuccess(value
);
399 * This is an inelegant solution, but for the present, it will work.
400 * The point of this is to separate the public and private portions of
401 * the SmtEngine class, so that smt_engine.h doesn't
402 * include "expr/node.h", which is a private CVC4 header (and can lead
403 * to linking errors due to the improper inlining of non-visible symbols
406 * The "real" solution (that which is usually implemented) is to move
407 * ALL the implementation to SmtEnginePrivate and maintain a
408 * heap-allocated instance of it in SmtEngine. SmtEngine (the public
409 * one) becomes an "interface shell" which simply acts as a forwarder
412 class SmtEnginePrivate
: public NodeManagerListener
{
415 typedef unordered_map
<Node
, Node
, NodeHashFunction
> NodeToNodeHashMap
;
416 typedef unordered_map
<Node
, bool, NodeHashFunction
> NodeToBoolHashMap
;
419 * Manager for limiting time and abstract resource usage.
421 ResourceManager
* d_resourceManager
;
423 /** Manager for the memory of regular-output-channel. */
424 ManagedRegularOutputChannel d_managedRegularChannel
;
426 /** Manager for the memory of diagnostic-output-channel. */
427 ManagedDiagnosticOutputChannel d_managedDiagnosticChannel
;
429 /** Manager for the memory of --dump-to. */
430 ManagedDumpOStream d_managedDumpChannel
;
432 /** Manager for --replay-log. */
433 ManagedReplayLogOstream d_managedReplayLog
;
436 * This list contains:
440 * beforeSearchListener
441 * UseTheoryListListener
443 * This needs to be deleted before both NodeManager's Options,
444 * SmtEngine, d_resourceManager, and TheoryEngine.
446 ListenerRegistrationList
* d_listenerRegistrations
;
448 /** A circuit propagator for non-clausal propositional deduction */
449 booleans::CircuitPropagator d_propagator
;
451 /** Assertions in the preprocessing pipeline */
452 AssertionPipeline d_assertions
;
454 /** Whether any assertions have been processed */
455 CDO
<bool> d_assertionsProcessed
;
461 * A context that never pushes/pops, for use by CD structures (like
462 * SubstitutionMaps) that should be "global".
464 context::Context d_fakeContext
;
467 * A map of AbsractValues to their actual constants. Only used if
468 * options::abstractValues() is on.
470 SubstitutionMap d_abstractValueMap
;
473 * A mapping of all abstract values (actual value |-> abstract) that
474 * we've handed out. This is necessary to ensure that we give the
475 * same AbstractValues for the same real constants. Only used if
476 * options::abstractValues() is on.
478 NodeToNodeHashMap d_abstractValues
;
480 /** Number of calls of simplify assertions active.
482 unsigned d_simplifyAssertionsDepth
;
484 /** TODO: whether certain preprocess steps are necessary */
485 //bool d_needsExpandDefs;
487 //------------------------------- expression names
488 /** mapping from expressions to name */
489 context::CDHashMap
< Node
, std::string
, NodeHashFunction
> d_exprNames
;
490 //------------------------------- end expression names
492 IteSkolemMap
& getIteSkolemMap() { return d_assertions
.getIteSkolemMap(); }
494 /** Instance of the ITE remover */
495 RemoveTermFormulas d_iteRemover
;
497 /* Finishes the initialization of the private portion of SMTEngine. */
501 std::unique_ptr
<PreprocessingPassContext
> d_preprocessingPassContext
;
504 * Map of preprocessing pass instances, mapping from names to preprocessing
507 std::unordered_map
<std::string
, std::unique_ptr
<PreprocessingPass
>> d_passes
;
510 * Helper function to fix up assertion list to restore invariants needed after
513 void collectSkolems(TNode n
, set
<TNode
>& skolemSet
, NodeToBoolHashMap
& cache
);
516 * Helper function to fix up assertion list to restore invariants needed after
519 bool checkForBadSkolems(TNode n
, TNode skolem
, NodeToBoolHashMap
& cache
);
522 * Perform non-clausal simplification of a Node. This involves
523 * Theory implementations, but does NOT involve the SAT solver in
526 * Returns false if the formula simplifies to "false"
528 bool simplifyAssertions();
531 SmtEnginePrivate(SmtEngine
& smt
)
533 d_managedRegularChannel(),
534 d_managedDiagnosticChannel(),
535 d_managedDumpChannel(),
536 d_managedReplayLog(),
537 d_listenerRegistrations(new ListenerRegistrationList()),
538 d_propagator(true, true),
540 d_assertionsProcessed(smt
.d_userContext
, false),
542 d_abstractValueMap(&d_fakeContext
),
544 d_simplifyAssertionsDepth(0),
545 // d_needsExpandDefs(true), //TODO?
546 d_exprNames(smt
.d_userContext
),
547 d_iteRemover(smt
.d_userContext
)
549 d_smt
.d_nodeManager
->subscribeEvents(this);
550 d_true
= NodeManager::currentNM()->mkConst(true);
551 d_resourceManager
= NodeManager::currentResourceManager();
553 d_listenerRegistrations
->add(d_resourceManager
->registerSoftListener(
554 new SoftResourceOutListener(d_smt
)));
556 d_listenerRegistrations
->add(d_resourceManager
->registerHardListener(
557 new HardResourceOutListener(d_smt
)));
559 Options
& nodeManagerOptions
= NodeManager::currentNM()->getOptions();
560 d_listenerRegistrations
->add(
561 nodeManagerOptions
.registerForceLogicListener(
562 new SetLogicListener(d_smt
), true));
564 // Multiple options reuse BeforeSearchListener so registration requires an
565 // extra bit of care.
566 // We can safely not call notify on this before search listener at
567 // registration time. This d_smt cannot be beforeSearch at construction
568 // time. Therefore the BeforeSearchListener is a no-op. Therefore it does
569 // not have to be called.
570 d_listenerRegistrations
->add(
571 nodeManagerOptions
.registerBeforeSearchListener(
572 new BeforeSearchListener(d_smt
)));
574 // These do need registration calls.
575 d_listenerRegistrations
->add(
576 nodeManagerOptions
.registerSetDefaultExprDepthListener(
577 new SetDefaultExprDepthListener(), true));
578 d_listenerRegistrations
->add(
579 nodeManagerOptions
.registerSetDefaultExprDagListener(
580 new SetDefaultExprDagListener(), true));
581 d_listenerRegistrations
->add(
582 nodeManagerOptions
.registerSetPrintExprTypesListener(
583 new SetPrintExprTypesListener(), true));
584 d_listenerRegistrations
->add(
585 nodeManagerOptions
.registerSetDumpModeListener(
586 new DumpModeListener(), true));
587 d_listenerRegistrations
->add(
588 nodeManagerOptions
.registerSetPrintSuccessListener(
589 new PrintSuccessListener(), true));
590 d_listenerRegistrations
->add(
591 nodeManagerOptions
.registerSetRegularOutputChannelListener(
592 new SetToDefaultSourceListener(&d_managedRegularChannel
), true));
593 d_listenerRegistrations
->add(
594 nodeManagerOptions
.registerSetDiagnosticOutputChannelListener(
595 new SetToDefaultSourceListener(&d_managedDiagnosticChannel
), true));
596 d_listenerRegistrations
->add(
597 nodeManagerOptions
.registerDumpToFileNameListener(
598 new SetToDefaultSourceListener(&d_managedDumpChannel
), true));
599 d_listenerRegistrations
->add(
600 nodeManagerOptions
.registerSetReplayLogFilename(
601 new SetToDefaultSourceListener(&d_managedReplayLog
), true));
606 delete d_listenerRegistrations
;
608 if(d_propagator
.getNeedsFinish()) {
609 d_propagator
.finish();
610 d_propagator
.setNeedsFinish(false);
612 d_smt
.d_nodeManager
->unsubscribeEvents(this);
615 void cleanupPreprocessingPasses() { d_passes
.clear(); }
617 ResourceManager
* getResourceManager() { return d_resourceManager
; }
618 void spendResource(unsigned amount
)
620 d_resourceManager
->spendResource(amount
);
623 void nmNotifyNewSort(TypeNode tn
, uint32_t flags
) override
625 DeclareTypeCommand
c(tn
.getAttribute(expr::VarNameAttr()),
628 if((flags
& ExprManager::SORT_FLAG_PLACEHOLDER
) == 0) {
629 d_smt
.addToModelCommandAndDump(c
, flags
);
633 void nmNotifyNewSortConstructor(TypeNode tn
, uint32_t flags
) override
635 DeclareTypeCommand
c(tn
.getAttribute(expr::VarNameAttr()),
636 tn
.getAttribute(expr::SortArityAttr()),
638 if ((flags
& ExprManager::SORT_FLAG_PLACEHOLDER
) == 0)
640 d_smt
.addToModelCommandAndDump(c
);
644 void nmNotifyNewDatatypes(const std::vector
<DatatypeType
>& dtts
,
645 uint32_t flags
) override
647 if ((flags
& ExprManager::DATATYPE_FLAG_PLACEHOLDER
) == 0)
649 DatatypeDeclarationCommand
c(dtts
);
650 d_smt
.addToModelCommandAndDump(c
);
654 void nmNotifyNewVar(TNode n
, uint32_t flags
) override
656 DeclareFunctionCommand
c(n
.getAttribute(expr::VarNameAttr()),
658 n
.getType().toType());
659 if((flags
& ExprManager::VAR_FLAG_DEFINED
) == 0) {
660 d_smt
.addToModelCommandAndDump(c
, flags
);
664 void nmNotifyNewSkolem(TNode n
,
665 const std::string
& comment
,
666 uint32_t flags
) override
668 string id
= n
.getAttribute(expr::VarNameAttr());
669 DeclareFunctionCommand
c(id
, n
.toExpr(), n
.getType().toType());
670 if(Dump
.isOn("skolems") && comment
!= "") {
671 Dump("skolems") << CommentCommand(id
+ " is " + comment
);
673 if((flags
& ExprManager::VAR_FLAG_DEFINED
) == 0) {
674 d_smt
.addToModelCommandAndDump(c
, flags
, false, "skolems");
678 void nmNotifyDeleteNode(TNode n
) override
{}
680 Node
applySubstitutions(TNode node
)
682 return Rewriter::rewrite(
683 d_preprocessingPassContext
->getTopLevelSubstitutions().apply(node
));
687 * Process the assertions that have been asserted.
689 void processAssertions();
691 /** Process a user push.
698 * Process a user pop. Clears out the non-context-dependent stuff in this
699 * SmtEnginePrivate. Necessary to clear out our assertion vectors in case
700 * someone does a push-assert-pop without a check-sat. It also pops the
701 * last map of expression names from notifyPush.
704 d_assertions
.clear();
705 d_propagator
.getLearnedLiterals().clear();
706 getIteSkolemMap().clear();
710 * Adds a formula to the current context. Action here depends on
711 * the SimplificationMode (in the current Options scope); the
712 * formula might be pushed out to the propositional layer
713 * immediately, or it might be simplified and kept, or it might not
714 * even be simplified.
715 * the 2nd and 3rd arguments added for bookkeeping for proofs
717 void addFormula(TNode n
, bool inUnsatCore
, bool inInput
= true);
719 /** Expand definitions in n. */
720 Node
expandDefinitions(TNode n
,
721 NodeToNodeHashMap
& cache
,
722 bool expandOnly
= false);
725 * Simplify node "in" by expanding definitions and applying any
726 * substitutions learned from preprocessing.
728 Node
simplify(TNode in
) {
729 // Substitute out any abstract values in ex.
730 // Expand definitions.
731 NodeToNodeHashMap cache
;
732 Node n
= expandDefinitions(in
, cache
).toExpr();
733 // Make sure we've done all preprocessing, etc.
734 Assert(d_assertions
.size() == 0);
735 return applySubstitutions(n
).toExpr();
739 * Substitute away all AbstractValues in a node.
741 Node
substituteAbstractValues(TNode n
) {
742 // We need to do this even if options::abstractValues() is off,
743 // since the setting might have changed after we already gave out
744 // some abstract values.
745 return d_abstractValueMap
.apply(n
);
749 * Make a new (or return an existing) abstract value for a node.
750 * Can only use this if options::abstractValues() is on.
752 Node
mkAbstractValue(TNode n
) {
753 Assert(options::abstractValues());
754 Node
& val
= d_abstractValues
[n
];
756 val
= d_smt
.d_nodeManager
->mkAbstractValue(n
.getType());
757 d_abstractValueMap
.addSubstitution(val
, n
);
759 // We are supposed to ascribe types to all abstract values that go out.
760 NodeManager
* current
= d_smt
.d_nodeManager
;
761 Node ascription
= current
->mkConst(AscriptionType(n
.getType().toType()));
762 Node retval
= current
->mkNode(kind::APPLY_TYPE_ASCRIPTION
, ascription
, val
);
766 void addUseTheoryListListener(TheoryEngine
* theoryEngine
){
767 Options
& nodeManagerOptions
= NodeManager::currentNM()->getOptions();
768 d_listenerRegistrations
->add(
769 nodeManagerOptions
.registerUseTheoryListListener(
770 new UseTheoryListListener(theoryEngine
), true));
773 std::ostream
* getReplayLog() const {
774 return d_managedReplayLog
.getReplayLog();
777 //------------------------------- expression names
778 // implements setExpressionName, as described in smt_engine.h
779 void setExpressionName(Expr e
, std::string name
) {
780 d_exprNames
[Node::fromExpr(e
)] = name
;
783 // implements getExpressionName, as described in smt_engine.h
784 bool getExpressionName(Expr e
, std::string
& name
) const {
785 context::CDHashMap
< Node
, std::string
, NodeHashFunction
>::const_iterator it
= d_exprNames
.find(e
);
786 if(it
!=d_exprNames
.end()) {
793 //------------------------------- end expression names
794 };/* class SmtEnginePrivate */
796 }/* namespace CVC4::smt */
798 SmtEngine::SmtEngine(ExprManager
* em
)
799 : d_context(new Context()),
801 d_userContext(new UserContext()),
803 d_nodeManager(d_exprManager
->getNodeManager()),
804 d_decisionEngine(NULL
),
805 d_theoryEngine(NULL
),
807 d_proofManager(NULL
),
808 d_definedFunctions(NULL
),
809 d_fmfRecFunctionsDefined(NULL
),
810 d_assertionList(NULL
),
812 d_modelGlobalCommands(),
813 d_modelCommands(NULL
),
819 d_fullyInited(false),
820 d_problemExtended(false),
822 d_needPostsolve(false),
823 d_earlyTheoryPP(true),
824 d_globalNegation(false),
826 d_replayStream(NULL
),
828 d_statisticsRegistry(NULL
),
830 d_channels(new LemmaChannels())
833 d_originalOptions
.copyValues(em
->getOptions());
834 d_private
= new smt::SmtEnginePrivate(*this);
835 d_statisticsRegistry
= new StatisticsRegistry();
836 d_stats
= new SmtEngineStatistics();
837 d_stats
->d_resourceUnitsUsed
.setData(
838 d_private
->getResourceManager()->getResourceUsage());
840 // The ProofManager is constructed before any other proof objects such as
841 // SatProof and TheoryProofs. The TheoryProofEngine and the SatProof are
842 // initialized in TheoryEngine and PropEngine respectively.
843 Assert(d_proofManager
== NULL
);
845 // d_proofManager must be created before Options has been finished
846 // being parsed from the input file. Because of this, we cannot trust
847 // that options::proof() is set correctly yet.
849 d_proofManager
= new ProofManager(d_userContext
);
852 // We have mutual dependency here, so we add the prop engine to the theory
853 // engine later (it is non-essential there)
854 d_theoryEngine
= new TheoryEngine(d_context
,
856 d_private
->d_iteRemover
,
857 const_cast<const LogicInfo
&>(d_logic
),
861 for(TheoryId id
= theory::THEORY_FIRST
; id
< theory::THEORY_LAST
; ++id
) {
862 TheoryConstructor::addTheory(d_theoryEngine
, id
);
863 //register with proof engine if applicable
865 ProofManager::currentPM()->getTheoryProofEngine()->registerTheory(d_theoryEngine
->theoryOf(id
));
869 d_private
->addUseTheoryListListener(d_theoryEngine
);
871 // global push/pop around everything, to ensure proper destruction
872 // of context-dependent data structures
873 d_userContext
->push();
876 d_definedFunctions
= new(true) DefinedFunctionMap(d_userContext
);
877 d_fmfRecFunctionsDefined
= new(true) NodeList(d_userContext
);
878 d_modelCommands
= new(true) smt::CommandList(d_userContext
);
881 void SmtEngine::finishInit() {
882 Trace("smt-debug") << "SmtEngine::finishInit" << std::endl
;
883 // ensure that our heuristics are properly set up
886 Trace("smt-debug") << "Making decision engine..." << std::endl
;
888 d_decisionEngine
= new DecisionEngine(d_context
, d_userContext
);
889 d_decisionEngine
->init(); // enable appropriate strategies
891 Trace("smt-debug") << "Making prop engine..." << std::endl
;
892 d_propEngine
= new PropEngine(d_theoryEngine
, d_decisionEngine
, d_context
,
893 d_userContext
, d_private
->getReplayLog(),
894 d_replayStream
, d_channels
);
896 Trace("smt-debug") << "Setting up theory engine..." << std::endl
;
897 d_theoryEngine
->setPropEngine(d_propEngine
);
898 d_theoryEngine
->setDecisionEngine(d_decisionEngine
);
899 Trace("smt-debug") << "Finishing init for theory engine..." << std::endl
;
900 d_theoryEngine
->finishInit();
902 Trace("smt-debug") << "Set up assertion list..." << std::endl
;
903 // [MGD 10/20/2011] keep around in incremental mode, due to a
904 // cleanup ordering issue and Nodes/TNodes. If SAT is popped
905 // first, some user-context-dependent TNodes might still exist
907 if(options::produceAssertions() ||
908 options::incrementalSolving()) {
909 // In the case of incremental solving, we appear to need these to
910 // ensure the relevant Nodes remain live.
911 d_assertionList
= new(true) AssertionList(d_userContext
);
914 // dump out a set-logic command
915 if(Dump
.isOn("benchmark")) {
916 if (Dump
.isOn("raw-benchmark")) {
917 Dump("raw-benchmark") << SetBenchmarkLogicCommand(d_logic
.getLogicString());
919 LogicInfo everything
;
921 Dump("benchmark") << CommentCommand("CVC4 always dumps the most general, all-supported logic (below), as some internals might require the use of a logic more general than the input.")
922 << SetBenchmarkLogicCommand(everything
.getLogicString());
926 Trace("smt-debug") << "Dump declaration commands..." << std::endl
;
927 // dump out any pending declaration commands
928 for(unsigned i
= 0; i
< d_dumpCommands
.size(); ++i
) {
929 Dump("declarations") << *d_dumpCommands
[i
];
930 delete d_dumpCommands
[i
];
932 d_dumpCommands
.clear();
934 PROOF( ProofManager::currentPM()->setLogic(d_logic
); );
936 for(TheoryId id
= theory::THEORY_FIRST
; id
< theory::THEORY_LAST
; ++id
) {
937 ProofManager::currentPM()->getTheoryProofEngine()->
938 finishRegisterTheory(d_theoryEngine
->theoryOf(id
));
941 d_private
->finishInit();
942 Trace("smt-debug") << "SmtEngine::finishInit done" << std::endl
;
945 void SmtEngine::finalOptionsAreSet() {
950 if(! d_logic
.isLocked()) {
954 // finish initialization, create the prop engine, etc.
957 AlwaysAssert( d_propEngine
->getAssertionLevel() == 0,
958 "The PropEngine has pushed but the SmtEngine "
959 "hasn't finished initializing!" );
961 d_fullyInited
= true;
962 Assert(d_logic
.isLocked());
964 d_propEngine
->assertFormula(NodeManager::currentNM()->mkConst
<bool>(true));
965 d_propEngine
->assertFormula(NodeManager::currentNM()->mkConst
<bool>(false).notNode());
968 void SmtEngine::shutdown() {
971 while(options::incrementalSolving() && d_userContext
->getLevel() > 1) {
975 // check to see if a postsolve() is pending
976 if(d_needPostsolve
) {
977 d_theoryEngine
->postsolve();
978 d_needPostsolve
= false;
981 if(d_propEngine
!= NULL
) {
982 d_propEngine
->shutdown();
984 if(d_theoryEngine
!= NULL
) {
985 d_theoryEngine
->shutdown();
987 if(d_decisionEngine
!= NULL
) {
988 d_decisionEngine
->shutdown();
992 SmtEngine::~SmtEngine()
999 // global push/pop around everything, to ensure proper destruction
1000 // of context-dependent data structures
1001 d_context
->popto(0);
1002 d_userContext
->popto(0);
1004 if(d_assignments
!= NULL
) {
1005 d_assignments
->deleteSelf();
1008 if(d_assertionList
!= NULL
) {
1009 d_assertionList
->deleteSelf();
1012 for(unsigned i
= 0; i
< d_dumpCommands
.size(); ++i
) {
1013 delete d_dumpCommands
[i
];
1014 d_dumpCommands
[i
] = NULL
;
1016 d_dumpCommands
.clear();
1018 DeleteAndClearCommandVector(d_modelGlobalCommands
);
1020 if(d_modelCommands
!= NULL
) {
1021 d_modelCommands
->deleteSelf();
1024 d_definedFunctions
->deleteSelf();
1025 d_fmfRecFunctionsDefined
->deleteSelf();
1027 //destroy all passes before destroying things that they refer to
1028 d_private
->cleanupPreprocessingPasses();
1030 delete d_theoryEngine
;
1031 d_theoryEngine
= NULL
;
1032 delete d_propEngine
;
1033 d_propEngine
= NULL
;
1034 delete d_decisionEngine
;
1035 d_decisionEngine
= NULL
;
1038 // d_proofManager is always created when proofs are enabled at configure time.
1039 // Becuase of this, this code should not be wrapped in PROOF() which
1040 // additionally checks flags such as options::proof().
1042 delete d_proofManager
;
1043 d_proofManager
= NULL
;
1048 delete d_statisticsRegistry
;
1049 d_statisticsRegistry
= NULL
;
1054 delete d_userContext
;
1055 d_userContext
= NULL
;
1062 } catch(Exception
& e
) {
1063 Warning() << "CVC4 threw an exception during cleanup." << endl
1068 void SmtEngine::setLogic(const LogicInfo
& logic
)
1070 SmtScope
smts(this);
1072 throw ModalException("Cannot set logic in SmtEngine after the engine has "
1073 "finished initializing.");
1079 void SmtEngine::setLogic(const std::string
& s
)
1081 SmtScope
smts(this);
1083 setLogic(LogicInfo(s
));
1084 } catch(IllegalArgumentException
& e
) {
1085 throw LogicException(e
.what());
1089 void SmtEngine::setLogic(const char* logic
) { setLogic(string(logic
)); }
1090 LogicInfo
SmtEngine::getLogicInfo() const {
1093 void SmtEngine::setFilename(std::string filename
) { d_filename
= filename
; }
1094 std::string
SmtEngine::getFilename() const { return d_filename
; }
1095 void SmtEngine::setLogicInternal()
1097 Assert(!d_fullyInited
, "setting logic in SmtEngine but the engine has already"
1098 " finished initializing for this run");
1102 void SmtEngine::setDefaults() {
1103 Random::getRandom().setSeed(options::seed());
1104 // Language-based defaults
1105 if (!options::bitvectorDivByZeroConst
.wasSetByUser())
1107 // Bitvector-divide-by-zero changed semantics in SMT LIB 2.6, thus we
1108 // set this option if the input format is SMT LIB 2.6. We also set this
1109 // option if we are sygus, since we assume SMT LIB 2.6 semantics for sygus.
1110 options::bitvectorDivByZeroConst
.set(
1111 language::isInputLang_smt2_6(options::inputLanguage())
1112 || options::inputLanguage() == language::input::LANG_SYGUS
);
1114 bool is_sygus
= false;
1115 if (options::inputLanguage() == language::input::LANG_SYGUS
)
1118 // must use Ferrante/Rackoff for real arithmetic
1119 if (!options::cbqiMidpoint
.wasSetByUser())
1121 options::cbqiMidpoint
.set(true);
1123 if (options::sygusRepairConst())
1125 if (!options::cbqi
.wasSetByUser())
1127 options::cbqi
.set(true);
1132 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
)
1134 if (options::produceModels()
1135 && (d_logic
.isTheoryEnabled(THEORY_ARRAYS
)
1136 || d_logic
.isTheoryEnabled(THEORY_UF
)))
1138 if (options::bitblastMode
.wasSetByUser()
1139 || options::produceModels
.wasSetByUser())
1141 throw OptionException(std::string(
1142 "Eager bit-blasting currently does not support model generation "
1143 "for the combination of bit-vectors with arrays or uinterpreted "
1144 "functions. Try --bitblast=lazy"));
1146 Notice() << "SmtEngine: setting bit-blast mode to lazy to support model"
1147 << "generation" << endl
;
1148 setOption("bitblastMode", SExpr("lazy"));
1151 if (options::incrementalSolving() && !d_logic
.isPure(THEORY_BV
))
1153 throw OptionException(
1154 "Incremental eager bit-blasting is currently "
1155 "only supported for QF_BV. Try --bitblast=lazy.");
1159 if(options::forceLogicString
.wasSetByUser()) {
1160 d_logic
= LogicInfo(options::forceLogicString());
1161 }else if (options::solveIntAsBV() > 0) {
1162 d_logic
= LogicInfo("QF_BV");
1163 }else if (d_logic
.getLogicString() == "QF_NRA" && options::solveRealAsInt()) {
1164 d_logic
= LogicInfo("QF_NIA");
1165 } else if ((d_logic
.getLogicString() == "QF_UFBV" ||
1166 d_logic
.getLogicString() == "QF_ABV") &&
1167 options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
) {
1168 d_logic
= LogicInfo("QF_BV");
1172 /* - disabled for 1.4 release [MGD 2014.06.25]
1173 if(!d_logic.hasEverything() && d_logic.isTheoryEnabled(THEORY_STRINGS) ) {
1174 if(! options::stringExp.wasSetByUser()) {
1175 options::stringExp.set( true );
1176 Trace("smt") << "turning on strings-exp, for the theory of strings" << std::endl;
1181 if(options::stringExp()) {
1182 if( !d_logic
.isQuantified() ) {
1183 d_logic
= d_logic
.getUnlockedCopy();
1184 d_logic
.enableQuantifiers();
1186 Trace("smt") << "turning on quantifier logic, for strings-exp"
1189 if(! options::fmfBound
.wasSetByUser()) {
1190 options::fmfBound
.set( true );
1191 Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl
;
1193 if(! options::fmfInstEngine
.wasSetByUser()) {
1194 options::fmfInstEngine
.set( true );
1195 Trace("smt") << "turning on fmf-inst-engine, for strings-exp" << std::endl
;
1198 if(! options::rewriteDivk.wasSetByUser()) {
1199 options::rewriteDivk.set( true );
1200 Trace("smt") << "turning on rewrite-divk, for strings-exp" << std::endl;
1203 if(! options::stringFMF.wasSetByUser()) {
1204 options::stringFMF.set( true );
1205 Trace("smt") << "turning on strings-fmf, for strings-exp" << std::endl;
1210 // sygus inference may require datatypes
1211 if (options::sygusInference() || options::sygusRewSynthInput())
1213 d_logic
= d_logic
.getUnlockedCopy();
1214 // sygus requires arithmetic, datatypes and quantifiers
1215 d_logic
.enableTheory(THEORY_ARITH
);
1216 d_logic
.enableTheory(THEORY_DATATYPES
);
1217 d_logic
.enableTheory(THEORY_QUANTIFIERS
);
1219 // since we are trying to recast as sygus, we assume the input is sygus
1223 if ((options::checkModels() || options::checkSynthSol()
1224 || options::produceModelCores())
1225 && !options::produceAssertions())
1227 Notice() << "SmtEngine: turning on produce-assertions to support "
1228 << "check-models, check-synth-sol or produce-model-cores." << endl
;
1229 setOption("produce-assertions", SExpr("true"));
1232 // Disable options incompatible with incremental solving, unsat cores, and
1233 // proofs or output an error if enabled explicitly
1234 if (options::incrementalSolving() || options::unsatCores()
1235 || options::proof())
1237 if (options::unconstrainedSimp())
1239 if (options::unconstrainedSimp
.wasSetByUser())
1241 throw OptionException(
1242 "unconstrained simplification not supported with unsat "
1243 "cores/proofs/incremental solving");
1245 Notice() << "SmtEngine: turning off unconstrained simplification to "
1246 "support unsat cores/proofs/incremental solving"
1248 options::unconstrainedSimp
.set(false);
1253 // Turn on unconstrained simplification for QF_AUFBV
1254 if (!options::unconstrainedSimp
.wasSetByUser())
1256 // bool qf_sat = d_logic.isPure(THEORY_BOOL) &&
1257 // !d_logic.isQuantified(); bool uncSimp = false && !qf_sat &&
1258 // !options::incrementalSolving();
1259 bool uncSimp
= !d_logic
.isQuantified() && !options::produceModels()
1260 && !options::produceAssignments()
1261 && !options::checkModels()
1262 && (d_logic
.isTheoryEnabled(THEORY_ARRAYS
)
1263 && d_logic
.isTheoryEnabled(THEORY_BV
));
1264 Trace("smt") << "setting unconstrained simplification to " << uncSimp
1266 options::unconstrainedSimp
.set(uncSimp
);
1270 // Disable options incompatible with unsat cores and proofs or output an
1271 // error if enabled explicitly
1272 if (options::unsatCores() || options::proof())
1274 if (options::simplificationMode() != SIMPLIFICATION_MODE_NONE
)
1276 if (options::simplificationMode
.wasSetByUser())
1278 throw OptionException(
1279 "simplification not supported with unsat cores/proofs");
1281 Notice() << "SmtEngine: turning off simplification to support unsat "
1284 options::simplificationMode
.set(SIMPLIFICATION_MODE_NONE
);
1287 if (options::pbRewrites())
1289 if (options::pbRewrites
.wasSetByUser())
1291 throw OptionException(
1292 "pseudoboolean rewrites not supported with unsat cores/proofs");
1294 Notice() << "SmtEngine: turning off pseudoboolean rewrites to support "
1295 "unsat cores/proofs"
1297 setOption("pb-rewrites", false);
1300 if (options::sortInference())
1302 if (options::sortInference
.wasSetByUser())
1304 throw OptionException(
1305 "sort inference not supported with unsat cores/proofs");
1307 Notice() << "SmtEngine: turning off sort inference to support unsat "
1310 options::sortInference
.set(false);
1313 if (options::preSkolemQuant())
1315 if (options::preSkolemQuant
.wasSetByUser())
1317 throw OptionException(
1318 "pre-skolemization not supported with unsat cores/proofs");
1320 Notice() << "SmtEngine: turning off pre-skolemization to support unsat "
1323 options::preSkolemQuant
.set(false);
1326 if (options::bitvectorToBool())
1328 if (options::bitvectorToBool
.wasSetByUser())
1330 throw OptionException(
1331 "bv-to-bool not supported with unsat cores/proofs");
1333 Notice() << "SmtEngine: turning off bitvector-to-bool to support unsat "
1336 options::bitvectorToBool
.set(false);
1339 if (options::boolToBitvector())
1341 if (options::boolToBitvector
.wasSetByUser())
1343 throw OptionException(
1344 "bool-to-bv not supported with unsat cores/proofs");
1346 Notice() << "SmtEngine: turning off bool-to-bitvector to support unsat "
1349 options::boolToBitvector
.set(false);
1352 if (options::bvIntroducePow2())
1354 if (options::bvIntroducePow2
.wasSetByUser())
1356 throw OptionException(
1357 "bv-intro-pow2 not supported with unsat cores/proofs");
1359 Notice() << "SmtEngine: turning off bv-intro-pow2 to support "
1360 "unsat-cores/proofs"
1362 setOption("bv-intro-pow2", false);
1365 if (options::repeatSimp())
1367 if (options::repeatSimp
.wasSetByUser())
1369 throw OptionException(
1370 "repeat-simp not supported with unsat cores/proofs");
1372 Notice() << "SmtEngine: turning off repeat-simp to support unsat "
1375 setOption("repeat-simp", false);
1378 if (options::globalNegate())
1380 if (options::globalNegate
.wasSetByUser())
1382 throw OptionException(
1383 "global-negate not supported with unsat cores/proofs");
1385 Notice() << "SmtEngine: turning off global-negate to support unsat "
1388 setOption("global-negate", false);
1393 // by default, nonclausal simplification is off for QF_SAT
1394 if (!options::simplificationMode
.wasSetByUser())
1396 bool qf_sat
= d_logic
.isPure(THEORY_BOOL
) && !d_logic
.isQuantified();
1397 Trace("smt") << "setting simplification mode to <"
1398 << d_logic
.getLogicString() << "> " << (!qf_sat
) << endl
;
1399 // simplification=none works better for SMT LIB benchmarks with
1400 // quantifiers, not others options::simplificationMode.set(qf_sat ||
1401 // quantifiers ? SIMPLIFICATION_MODE_NONE : SIMPLIFICATION_MODE_BATCH);
1402 options::simplificationMode
.set(qf_sat
? SIMPLIFICATION_MODE_NONE
1403 : SIMPLIFICATION_MODE_BATCH
);
1407 if (options::cbqiBv() && d_logic
.isQuantified())
1409 if(options::boolToBitvector
.wasSetByUser()) {
1410 throw OptionException(
1411 "bool-to-bv not supported with CBQI BV for quantified logics");
1413 Notice() << "SmtEngine: turning off bool-to-bitvector to support CBQI BV"
1415 options::boolToBitvector
.set(false);
1418 // cases where we need produce models
1419 if (!options::produceModels()
1420 && (options::produceAssignments() || options::sygusRewSynthCheck()
1421 || options::produceModelCores() || is_sygus
))
1423 Notice() << "SmtEngine: turning on produce-models" << endl
;
1424 setOption("produce-models", SExpr("true"));
1427 // Set the options for the theoryOf
1428 if(!options::theoryOfMode
.wasSetByUser()) {
1429 if(d_logic
.isSharingEnabled() &&
1430 !d_logic
.isTheoryEnabled(THEORY_BV
) &&
1431 !d_logic
.isTheoryEnabled(THEORY_STRINGS
) &&
1432 !d_logic
.isTheoryEnabled(THEORY_SETS
) ) {
1433 Trace("smt") << "setting theoryof-mode to term-based" << endl
;
1434 options::theoryOfMode
.set(THEORY_OF_TERM_BASED
);
1438 // strings require LIA, UF; widen the logic
1439 if(d_logic
.isTheoryEnabled(THEORY_STRINGS
)) {
1440 LogicInfo
log(d_logic
.getUnlockedCopy());
1441 // Strings requires arith for length constraints, and also UF
1442 if(!d_logic
.isTheoryEnabled(THEORY_UF
)) {
1443 Trace("smt") << "because strings are enabled, also enabling UF" << endl
;
1444 log
.enableTheory(THEORY_UF
);
1446 if(!d_logic
.isTheoryEnabled(THEORY_ARITH
) || d_logic
.isDifferenceLogic() || !d_logic
.areIntegersUsed()) {
1447 Trace("smt") << "because strings are enabled, also enabling linear integer arithmetic" << endl
;
1448 log
.enableTheory(THEORY_ARITH
);
1449 log
.enableIntegers();
1450 log
.arithOnlyLinear();
1455 if(d_logic
.isTheoryEnabled(THEORY_ARRAYS
) || d_logic
.isTheoryEnabled(THEORY_DATATYPES
) || d_logic
.isTheoryEnabled(THEORY_SETS
)) {
1456 if(!d_logic
.isTheoryEnabled(THEORY_UF
)) {
1457 LogicInfo
log(d_logic
.getUnlockedCopy());
1458 Trace("smt") << "because a theory that permits Boolean terms is enabled, also enabling UF" << endl
;
1459 log
.enableTheory(THEORY_UF
);
1465 // by default, symmetry breaker is on only for non-incremental QF_UF
1466 if(! options::ufSymmetryBreaker
.wasSetByUser()) {
1467 bool qf_uf_noinc
= d_logic
.isPure(THEORY_UF
) && !d_logic
.isQuantified()
1468 && !options::incrementalSolving() && !options::proof()
1469 && !options::unsatCores();
1470 Trace("smt") << "setting uf symmetry breaker to " << qf_uf_noinc
<< endl
;
1471 options::ufSymmetryBreaker
.set(qf_uf_noinc
);
1474 // If in arrays, set the UF handler to arrays
1475 if(d_logic
.isTheoryEnabled(THEORY_ARRAYS
) && ( !d_logic
.isQuantified() ||
1476 (d_logic
.isQuantified() && !d_logic
.isTheoryEnabled(THEORY_UF
)))) {
1477 Theory::setUninterpretedSortOwner(THEORY_ARRAYS
);
1479 Theory::setUninterpretedSortOwner(THEORY_UF
);
1482 // Turn on ite simplification for QF_LIA and QF_AUFBV
1483 // WARNING: These checks match much more than just QF_AUFBV and
1484 // QF_LIA logics. --K [2014/10/15]
1485 if(! options::doITESimp
.wasSetByUser()) {
1486 bool qf_aufbv
= !d_logic
.isQuantified() &&
1487 d_logic
.isTheoryEnabled(THEORY_ARRAYS
) &&
1488 d_logic
.isTheoryEnabled(THEORY_UF
) &&
1489 d_logic
.isTheoryEnabled(THEORY_BV
);
1490 bool qf_lia
= !d_logic
.isQuantified() &&
1491 d_logic
.isPure(THEORY_ARITH
) &&
1492 d_logic
.isLinear() &&
1493 !d_logic
.isDifferenceLogic() &&
1494 !d_logic
.areRealsUsed();
1496 bool iteSimp
= (qf_aufbv
|| qf_lia
);
1497 Trace("smt") << "setting ite simplification to " << iteSimp
<< endl
;
1498 options::doITESimp
.set(iteSimp
);
1500 if(! options::compressItes
.wasSetByUser() ){
1501 bool qf_lia
= !d_logic
.isQuantified() &&
1502 d_logic
.isPure(THEORY_ARITH
) &&
1503 d_logic
.isLinear() &&
1504 !d_logic
.isDifferenceLogic() &&
1505 !d_logic
.areRealsUsed();
1507 bool compressIte
= qf_lia
;
1508 Trace("smt") << "setting ite compression to " << compressIte
<< endl
;
1509 options::compressItes
.set(compressIte
);
1511 if(! options::simplifyWithCareEnabled
.wasSetByUser() ){
1512 bool qf_aufbv
= !d_logic
.isQuantified() &&
1513 d_logic
.isTheoryEnabled(THEORY_ARRAYS
) &&
1514 d_logic
.isTheoryEnabled(THEORY_UF
) &&
1515 d_logic
.isTheoryEnabled(THEORY_BV
);
1517 bool withCare
= qf_aufbv
;
1518 Trace("smt") << "setting ite simplify with care to " << withCare
<< endl
;
1519 options::simplifyWithCareEnabled
.set(withCare
);
1521 // Turn off array eager index splitting for QF_AUFLIA
1522 if(! options::arraysEagerIndexSplitting
.wasSetByUser()) {
1523 if (not d_logic
.isQuantified() &&
1524 d_logic
.isTheoryEnabled(THEORY_ARRAYS
) &&
1525 d_logic
.isTheoryEnabled(THEORY_UF
) &&
1526 d_logic
.isTheoryEnabled(THEORY_ARITH
)) {
1527 Trace("smt") << "setting array eager index splitting to false" << endl
;
1528 options::arraysEagerIndexSplitting
.set(false);
1531 // Turn on model-based arrays for QF_AX (unless models are enabled)
1532 // if(! options::arraysModelBased.wasSetByUser()) {
1533 // if (not d_logic.isQuantified() &&
1534 // d_logic.isTheoryEnabled(THEORY_ARRAYS) &&
1535 // d_logic.isPure(THEORY_ARRAYS) &&
1536 // !options::produceModels() &&
1537 // !options::checkModels()) {
1538 // Trace("smt") << "turning on model-based array solver" << endl;
1539 // options::arraysModelBased.set(true);
1542 // Turn on multiple-pass non-clausal simplification for QF_AUFBV
1543 if(! options::repeatSimp
.wasSetByUser()) {
1544 bool repeatSimp
= !d_logic
.isQuantified() &&
1545 (d_logic
.isTheoryEnabled(THEORY_ARRAYS
) &&
1546 d_logic
.isTheoryEnabled(THEORY_UF
) &&
1547 d_logic
.isTheoryEnabled(THEORY_BV
)) &&
1548 !options::unsatCores();
1549 Trace("smt") << "setting repeat simplification to " << repeatSimp
<< endl
;
1550 options::repeatSimp
.set(repeatSimp
);
1552 // Unconstrained simp currently does *not* support model generation
1553 if (options::unconstrainedSimp
.wasSetByUser() && options::unconstrainedSimp()) {
1554 if (options::produceModels()) {
1555 if (options::produceModels
.wasSetByUser()) {
1556 throw OptionException("Cannot use unconstrained-simp with model generation.");
1558 Notice() << "SmtEngine: turning off produce-models to support unconstrainedSimp" << endl
;
1559 setOption("produce-models", SExpr("false"));
1561 if (options::produceAssignments()) {
1562 if (options::produceAssignments
.wasSetByUser()) {
1563 throw OptionException("Cannot use unconstrained-simp with model generation (produce-assignments).");
1565 Notice() << "SmtEngine: turning off produce-assignments to support unconstrainedSimp" << endl
;
1566 setOption("produce-assignments", SExpr("false"));
1568 if (options::checkModels()) {
1569 if (options::checkModels
.wasSetByUser()) {
1570 throw OptionException("Cannot use unconstrained-simp with model generation (check-models).");
1572 Notice() << "SmtEngine: turning off check-models to support unconstrainedSimp" << endl
;
1573 setOption("check-models", SExpr("false"));
1577 if (! options::bvEagerExplanations
.wasSetByUser() &&
1578 d_logic
.isTheoryEnabled(THEORY_ARRAYS
) &&
1579 d_logic
.isTheoryEnabled(THEORY_BV
)) {
1580 Trace("smt") << "enabling eager bit-vector explanations " << endl
;
1581 options::bvEagerExplanations
.set(true);
1584 // Turn on arith rewrite equalities only for pure arithmetic
1585 if(! options::arithRewriteEq
.wasSetByUser()) {
1586 bool arithRewriteEq
= d_logic
.isPure(THEORY_ARITH
) && d_logic
.isLinear() && !d_logic
.isQuantified();
1587 Trace("smt") << "setting arith rewrite equalities " << arithRewriteEq
<< endl
;
1588 options::arithRewriteEq
.set(arithRewriteEq
);
1590 if(! options::arithHeuristicPivots
.wasSetByUser()) {
1591 int16_t heuristicPivots
= 5;
1592 if(d_logic
.isPure(THEORY_ARITH
) && !d_logic
.isQuantified()) {
1593 if(d_logic
.isDifferenceLogic()) {
1594 heuristicPivots
= -1;
1595 } else if(!d_logic
.areIntegersUsed()) {
1596 heuristicPivots
= 0;
1599 Trace("smt") << "setting arithHeuristicPivots " << heuristicPivots
<< endl
;
1600 options::arithHeuristicPivots
.set(heuristicPivots
);
1602 if(! options::arithPivotThreshold
.wasSetByUser()){
1603 uint16_t pivotThreshold
= 2;
1604 if(d_logic
.isPure(THEORY_ARITH
) && !d_logic
.isQuantified()){
1605 if(d_logic
.isDifferenceLogic()){
1606 pivotThreshold
= 16;
1609 Trace("smt") << "setting arith arithPivotThreshold " << pivotThreshold
<< endl
;
1610 options::arithPivotThreshold
.set(pivotThreshold
);
1612 if(! options::arithStandardCheckVarOrderPivots
.wasSetByUser()){
1613 int16_t varOrderPivots
= -1;
1614 if(d_logic
.isPure(THEORY_ARITH
) && !d_logic
.isQuantified()){
1615 varOrderPivots
= 200;
1617 Trace("smt") << "setting arithStandardCheckVarOrderPivots " << varOrderPivots
<< endl
;
1618 options::arithStandardCheckVarOrderPivots
.set(varOrderPivots
);
1620 // Turn off early theory preprocessing if arithRewriteEq is on
1621 if (options::arithRewriteEq()) {
1622 d_earlyTheoryPP
= false;
1624 if (d_logic
.isPure(THEORY_ARITH
) && !d_logic
.areRealsUsed())
1626 if (!options::nlExtTangentPlanesInterleave
.wasSetByUser())
1628 Trace("smt") << "setting nlExtTangentPlanesInterleave to true" << endl
;
1629 options::nlExtTangentPlanesInterleave
.set(true);
1633 // Set decision mode based on logic (if not set by user)
1634 if(!options::decisionMode
.wasSetByUser()) {
1635 decision::DecisionMode decMode
=
1636 // sygus uses internal
1637 is_sygus
? decision::DECISION_STRATEGY_INTERNAL
:
1639 d_logic
.hasEverything()
1640 ? decision::DECISION_STRATEGY_JUSTIFICATION
1642 (not d_logic
.isQuantified() && d_logic
.isPure(THEORY_BV
))
1644 // QF_AUFBV or QF_ABV or QF_UFBV
1645 (not d_logic
.isQuantified()
1646 && (d_logic
.isTheoryEnabled(THEORY_ARRAYS
)
1647 || d_logic
.isTheoryEnabled(THEORY_UF
))
1648 && d_logic
.isTheoryEnabled(THEORY_BV
))
1650 // QF_AUFLIA (and may be ends up enabling
1652 (not d_logic
.isQuantified()
1653 && d_logic
.isTheoryEnabled(THEORY_ARRAYS
)
1654 && d_logic
.isTheoryEnabled(THEORY_UF
)
1655 && d_logic
.isTheoryEnabled(THEORY_ARITH
))
1658 (not d_logic
.isQuantified()
1659 && d_logic
.isPure(THEORY_ARITH
)
1660 && d_logic
.isLinear()
1661 && !d_logic
.isDifferenceLogic()
1662 && !d_logic
.areIntegersUsed())
1665 d_logic
.isQuantified() ||
1667 d_logic
.isTheoryEnabled(THEORY_STRINGS
)
1668 ? decision::DECISION_STRATEGY_JUSTIFICATION
1669 : decision::DECISION_STRATEGY_INTERNAL
);
1673 d_logic
.hasEverything() || d_logic
.isTheoryEnabled(THEORY_STRINGS
) ? false :
1675 (not d_logic
.isQuantified() &&
1676 d_logic
.isTheoryEnabled(THEORY_ARRAYS
) &&
1677 d_logic
.isTheoryEnabled(THEORY_UF
) &&
1678 d_logic
.isTheoryEnabled(THEORY_ARITH
)
1681 (not d_logic
.isQuantified() &&
1682 d_logic
.isPure(THEORY_ARITH
) && d_logic
.isLinear() && !d_logic
.isDifferenceLogic() && !d_logic
.areIntegersUsed()
1687 Trace("smt") << "setting decision mode to " << decMode
<< endl
;
1688 options::decisionMode
.set(decMode
);
1689 options::decisionStopOnly
.set(stoponly
);
1691 if( options::incrementalSolving() ){
1692 //disable modes not supported by incremental
1693 options::sortInference
.set( false );
1694 options::ufssFairnessMonotone
.set( false );
1695 options::quantEpr
.set( false );
1696 options::globalNegate
.set(false);
1698 if( d_logic
.hasCardinalityConstraints() ){
1699 //must have finite model finding on
1700 options::finiteModelFind
.set( true );
1703 //if it contains a theory with non-termination, do not strictly enforce that quantifiers and theory combination must be interleaved
1704 if( d_logic
.isTheoryEnabled(THEORY_STRINGS
) || (d_logic
.isTheoryEnabled(THEORY_ARITH
) && !d_logic
.isLinear()) ){
1705 if( !options::instWhenStrictInterleave
.wasSetByUser() ){
1706 options::instWhenStrictInterleave
.set( false );
1710 //local theory extensions
1711 if( options::localTheoryExt() ){
1712 if( !options::instMaxLevel
.wasSetByUser() ){
1713 options::instMaxLevel
.set( 0 );
1716 if( options::instMaxLevel()!=-1 ){
1717 Notice() << "SmtEngine: turning off cbqi to support instMaxLevel" << endl
;
1718 options::cbqi
.set(false);
1720 //track instantiations?
1721 if( options::cbqiNestedQE() || ( options::proof() && !options::trackInstLemmas
.wasSetByUser() ) ){
1722 options::trackInstLemmas
.set( true );
1725 if( ( options::fmfBoundLazy
.wasSetByUser() && options::fmfBoundLazy() ) ||
1726 ( options::fmfBoundInt
.wasSetByUser() && options::fmfBoundInt() ) ) {
1727 options::fmfBound
.set( true );
1729 //now have determined whether fmfBoundInt is on/off
1730 //apply fmfBoundInt options
1731 if( options::fmfBound() ){
1732 //must have finite model finding on
1733 options::finiteModelFind
.set( true );
1734 if (!options::mbqiMode
.wasSetByUser()
1735 || (options::mbqiMode() != quantifiers::MBQI_NONE
1736 && options::mbqiMode() != quantifiers::MBQI_FMC
))
1738 //if bounded integers are set, use no MBQI by default
1739 options::mbqiMode
.set( quantifiers::MBQI_NONE
);
1741 if( ! options::prenexQuant
.wasSetByUser() ){
1742 options::prenexQuant
.set( quantifiers::PRENEX_QUANT_NONE
);
1745 if( options::ufHo() ){
1746 //if higher-order, then current variants of model-based instantiation cannot be used
1747 if( options::mbqiMode()!=quantifiers::MBQI_NONE
){
1748 options::mbqiMode
.set( quantifiers::MBQI_NONE
);
1751 if( options::mbqiMode()==quantifiers::MBQI_ABS
){
1752 if( !d_logic
.isPure(THEORY_UF
) ){
1753 //MBQI_ABS is only supported in pure quantified UF
1754 options::mbqiMode
.set( quantifiers::MBQI_FMC
);
1757 if( options::fmfFunWellDefinedRelevant() ){
1758 if( !options::fmfFunWellDefined
.wasSetByUser() ){
1759 options::fmfFunWellDefined
.set( true );
1762 if( options::fmfFunWellDefined() ){
1763 if( !options::finiteModelFind
.wasSetByUser() ){
1764 options::finiteModelFind
.set( true );
1768 if( options::quantEpr() ){
1769 if( !options::preSkolemQuant
.wasSetByUser() ){
1770 options::preSkolemQuant
.set( true );
1774 //now, have determined whether finite model find is on/off
1775 //apply finite model finding options
1776 if( options::finiteModelFind() ){
1777 //apply conservative quantifiers splitting
1778 if( !options::quantDynamicSplit
.wasSetByUser() ){
1779 options::quantDynamicSplit
.set( quantifiers::QUANT_DSPLIT_MODE_DEFAULT
);
1781 //do not eliminate extended arithmetic symbols from quantified formulas
1782 if( !options::elimExtArithQuant
.wasSetByUser() ){
1783 options::elimExtArithQuant
.set( false );
1785 if( !options::eMatching
.wasSetByUser() ){
1786 options::eMatching
.set( options::fmfInstEngine() );
1788 if( !options::instWhenMode
.wasSetByUser() ){
1789 //instantiate only on last call
1790 if( options::eMatching() ){
1791 options::instWhenMode
.set( quantifiers::INST_WHEN_LAST_CALL
);
1794 if( options::mbqiMode()==quantifiers::MBQI_ABS
){
1795 if( !options::preSkolemQuant
.wasSetByUser() ){
1796 options::preSkolemQuant
.set( true );
1798 if( !options::preSkolemQuantNested
.wasSetByUser() ){
1799 options::preSkolemQuantNested
.set( true );
1801 if( !options::fmfOneInstPerRound
.wasSetByUser() ){
1802 options::fmfOneInstPerRound
.set( true );
1807 //apply counterexample guided instantiation options
1808 // if we are attempting to rewrite everything to SyGuS, use ceGuidedInst
1811 if (!options::ceGuidedInst
.wasSetByUser())
1813 options::ceGuidedInst
.set(true);
1816 if (options::sygusInference())
1818 // optimization: apply preskolemization, makes it succeed more often
1819 if (!options::preSkolemQuant
.wasSetByUser())
1821 options::preSkolemQuant
.set(true);
1823 if (!options::preSkolemQuantNested
.wasSetByUser())
1825 options::preSkolemQuantNested
.set(true);
1828 if( options::cegqiSingleInvMode()!=quantifiers::CEGQI_SI_MODE_NONE
){
1829 if( !options::ceGuidedInst
.wasSetByUser() ){
1830 options::ceGuidedInst
.set( true );
1833 // if sygus is enabled, set the defaults for sygus
1834 if( options::ceGuidedInst() ){
1835 //counterexample-guided instantiation for sygus
1836 if( !options::cegqiSingleInvMode
.wasSetByUser() ){
1837 options::cegqiSingleInvMode
.set( quantifiers::CEGQI_SI_MODE_USE
);
1839 if( !options::quantConflictFind
.wasSetByUser() ){
1840 options::quantConflictFind
.set( false );
1842 if( !options::instNoEntail
.wasSetByUser() ){
1843 options::instNoEntail
.set( false );
1845 if (!options::cbqiFullEffort
.wasSetByUser())
1847 // should use full effort cbqi for single invocation and repair const
1848 options::cbqiFullEffort
.set(true);
1850 if (options::sygusRew())
1852 options::sygusRewSynth
.set(true);
1853 options::sygusRewVerify
.set(true);
1855 if (options::sygusRewSynthInput())
1857 // If we are using synthesis rewrite rules from input, we use
1858 // sygusRewSynth after preprocessing. See passes/synth_rew_rules.h for
1859 // details on this technique.
1860 options::sygusRewSynth
.set(true);
1861 // we should not use the extended rewriter, since we are interested
1862 // in rewrites that are not in the main rewriter
1863 if (!options::sygusExtRew
.wasSetByUser())
1865 options::sygusExtRew
.set(false);
1868 if (options::sygusRewSynth() || options::sygusRewVerify())
1870 // rewrite rule synthesis implies that sygus stream must be true
1871 options::sygusStream
.set(true);
1873 if (options::sygusStream())
1875 // PBE and streaming modes are incompatible
1876 if (!options::sygusSymBreakPbe
.wasSetByUser())
1878 options::sygusSymBreakPbe
.set(false);
1880 if (!options::sygusUnifPbe
.wasSetByUser())
1882 options::sygusUnifPbe
.set(false);
1885 //do not allow partial functions
1886 if( !options::bitvectorDivByZeroConst
.wasSetByUser() ){
1887 options::bitvectorDivByZeroConst
.set( true );
1889 if( !options::dtRewriteErrorSel
.wasSetByUser() ){
1890 options::dtRewriteErrorSel
.set( true );
1893 if( !options::miniscopeQuant
.wasSetByUser() ){
1894 options::miniscopeQuant
.set( false );
1896 if( !options::miniscopeQuantFreeVar
.wasSetByUser() ){
1897 options::miniscopeQuantFreeVar
.set( false );
1899 if (!options::quantSplit
.wasSetByUser())
1901 options::quantSplit
.set(false);
1904 if( !options::rewriteDivk
.wasSetByUser()) {
1905 options::rewriteDivk
.set( true );
1908 if( !options::macrosQuant
.wasSetByUser()) {
1909 options::macrosQuant
.set( false );
1911 if( !options::cbqiPreRegInst
.wasSetByUser()) {
1912 options::cbqiPreRegInst
.set( true );
1915 //counterexample-guided instantiation for non-sygus
1916 // enable if any possible quantifiers with arithmetic, datatypes or bitvectors
1917 if ((d_logic
.isQuantified()
1918 && (d_logic
.isTheoryEnabled(THEORY_ARITH
)
1919 || d_logic
.isTheoryEnabled(THEORY_DATATYPES
)
1920 || d_logic
.isTheoryEnabled(THEORY_BV
)
1921 || d_logic
.isTheoryEnabled(THEORY_FP
)))
1922 || options::cbqiAll())
1924 if( !options::cbqi
.wasSetByUser() ){
1925 options::cbqi
.set( true );
1927 // check whether we should apply full cbqi
1928 if (d_logic
.isPure(THEORY_BV
))
1930 if (!options::cbqiFullEffort
.wasSetByUser())
1932 options::cbqiFullEffort
.set(true);
1936 if( options::cbqi() ){
1938 if( !options::rewriteDivk
.wasSetByUser()) {
1939 options::rewriteDivk
.set( true );
1941 if (options::incrementalSolving())
1943 // cannot do nested quantifier elimination in incremental mode
1944 options::cbqiNestedQE
.set(false);
1946 if (d_logic
.isPure(THEORY_ARITH
) || d_logic
.isPure(THEORY_BV
))
1948 if( !options::quantConflictFind
.wasSetByUser() ){
1949 options::quantConflictFind
.set( false );
1951 if( !options::instNoEntail
.wasSetByUser() ){
1952 options::instNoEntail
.set( false );
1954 if( !options::instWhenMode
.wasSetByUser() && options::cbqiModel() ){
1955 //only instantiation should happen at last call when model is avaiable
1956 options::instWhenMode
.set( quantifiers::INST_WHEN_LAST_CALL
);
1959 // only supported in pure arithmetic or pure BV
1960 options::cbqiNestedQE
.set(false);
1963 if (options::cbqiNestedQE())
1965 // only complete with prenex = disj_normal or normal
1966 if (options::prenexQuant() <= quantifiers::PRENEX_QUANT_DISJ_NORMAL
)
1968 options::prenexQuant
.set(quantifiers::PRENEX_QUANT_DISJ_NORMAL
);
1971 else if (options::globalNegate())
1973 if (!options::prenexQuant
.wasSetByUser())
1975 options::prenexQuant
.set(quantifiers::PRENEX_QUANT_NONE
);
1979 //implied options...
1980 if( options::strictTriggers() ){
1981 if( !options::userPatternsQuant
.wasSetByUser() ){
1982 options::userPatternsQuant
.set( quantifiers::USER_PAT_MODE_TRUST
);
1985 if( options::qcfMode
.wasSetByUser() || options::qcfTConstraint() ){
1986 options::quantConflictFind
.set( true );
1988 if( options::cbqiNestedQE() ){
1989 options::prenexQuantUser
.set( true );
1990 if( !options::preSkolemQuant
.wasSetByUser() ){
1991 options::preSkolemQuant
.set( true );
1994 //for induction techniques
1995 if( options::quantInduction() ){
1996 if( !options::dtStcInduction
.wasSetByUser() ){
1997 options::dtStcInduction
.set( true );
1999 if( !options::intWfInduction
.wasSetByUser() ){
2000 options::intWfInduction
.set( true );
2003 if( options::dtStcInduction() ){
2004 //try to remove ITEs from quantified formulas
2005 if( !options::iteDtTesterSplitQuant
.wasSetByUser() ){
2006 options::iteDtTesterSplitQuant
.set( true );
2008 if( !options::iteLiftQuant
.wasSetByUser() ){
2009 options::iteLiftQuant
.set( quantifiers::ITE_LIFT_QUANT_MODE_ALL
);
2012 if( options::intWfInduction() ){
2013 if( !options::purifyTriggers
.wasSetByUser() ){
2014 options::purifyTriggers
.set( true );
2017 if( options::conjectureNoFilter() ){
2018 if( !options::conjectureFilterActiveTerms
.wasSetByUser() ){
2019 options::conjectureFilterActiveTerms
.set( false );
2021 if( !options::conjectureFilterCanonical
.wasSetByUser() ){
2022 options::conjectureFilterCanonical
.set( false );
2024 if( !options::conjectureFilterModel
.wasSetByUser() ){
2025 options::conjectureFilterModel
.set( false );
2028 if( options::conjectureGenPerRound
.wasSetByUser() ){
2029 if( options::conjectureGenPerRound()>0 ){
2030 options::conjectureGen
.set( true );
2032 options::conjectureGen
.set( false );
2035 //can't pre-skolemize nested quantifiers without UF theory
2036 if( !d_logic
.isTheoryEnabled(THEORY_UF
) && options::preSkolemQuant() ){
2037 if( !options::preSkolemQuantNested
.wasSetByUser() ){
2038 options::preSkolemQuantNested
.set( false );
2041 if( !d_logic
.isTheoryEnabled(THEORY_DATATYPES
) ){
2042 options::quantDynamicSplit
.set( quantifiers::QUANT_DSPLIT_MODE_NONE
);
2045 //until bugs 371,431 are fixed
2046 if( ! options::minisatUseElim
.wasSetByUser()){
2047 // cannot use minisat elimination for logics where a theory solver
2048 // introduces new literals into the search. This includes quantifiers
2049 // (quantifier instantiation), and the lemma schemas used in non-linear
2050 // and sets. We also can't use it if models are enabled.
2051 if (d_logic
.isTheoryEnabled(THEORY_SETS
) || d_logic
.isQuantified()
2052 || options::produceModels() || options::produceAssignments()
2053 || options::checkModels()
2054 || (d_logic
.isTheoryEnabled(THEORY_ARITH
) && !d_logic
.isLinear()))
2056 options::minisatUseElim
.set( false );
2059 else if (options::minisatUseElim()) {
2060 if (options::produceModels()) {
2061 Notice() << "SmtEngine: turning off produce-models to support minisatUseElim" << endl
;
2062 setOption("produce-models", SExpr("false"));
2064 if (options::produceAssignments()) {
2065 Notice() << "SmtEngine: turning off produce-assignments to support minisatUseElim" << endl
;
2066 setOption("produce-assignments", SExpr("false"));
2068 if (options::checkModels()) {
2069 Notice() << "SmtEngine: turning off check-models to support minisatUseElim" << endl
;
2070 setOption("check-models", SExpr("false"));
2074 // For now, these array theory optimizations do not support model-building
2075 if (options::produceModels() || options::produceAssignments() || options::checkModels()) {
2076 options::arraysOptimizeLinear
.set(false);
2077 options::arraysLazyRIntro1
.set(false);
2080 // Non-linear arithmetic does not support models unless nlExt is enabled
2081 if ((d_logic
.isTheoryEnabled(THEORY_ARITH
) && !d_logic
.isLinear()
2082 && !options::nlExt())
2083 || options::globalNegate())
2085 std::string reason
=
2086 options::globalNegate() ? "--global-negate" : "nonlinear arithmetic";
2087 if (options::produceModels()) {
2088 if(options::produceModels
.wasSetByUser()) {
2089 throw OptionException(
2090 std::string("produce-model not supported with " + reason
));
2093 << "SmtEngine: turning off produce-models because unsupported for "
2095 setOption("produce-models", SExpr("false"));
2097 if (options::produceAssignments()) {
2098 if(options::produceAssignments
.wasSetByUser()) {
2099 throw OptionException(
2100 std::string("produce-assignments not supported with " + reason
));
2102 Warning() << "SmtEngine: turning off produce-assignments because "
2105 setOption("produce-assignments", SExpr("false"));
2107 if (options::checkModels()) {
2108 if(options::checkModels
.wasSetByUser()) {
2109 throw OptionException(
2110 std::string("check-models not supported with " + reason
));
2113 << "SmtEngine: turning off check-models because unsupported for "
2115 setOption("check-models", SExpr("false"));
2119 if(options::incrementalSolving() && options::proof()) {
2120 Warning() << "SmtEngine: turning off incremental solving mode (not yet supported with --proof, try --tear-down-incremental instead)" << endl
;
2121 setOption("incremental", SExpr("false"));
2124 if (options::proof())
2126 if (options::bitvectorAlgebraicSolver())
2128 if (options::bitvectorAlgebraicSolver
.wasSetByUser())
2130 throw OptionException(
2131 "--bv-algebraic-solver is not supported with proofs");
2133 Notice() << "SmtEngine: turning off bv algebraic solver to support proofs"
2135 options::bitvectorAlgebraicSolver
.set(false);
2137 if (options::bitvectorEqualitySolver())
2139 if (options::bitvectorEqualitySolver
.wasSetByUser())
2141 throw OptionException("--bv-eq-solver is not supported with proofs");
2143 Notice() << "SmtEngine: turning off bv eq solver to support proofs"
2145 options::bitvectorEqualitySolver
.set(false);
2147 if (options::bitvectorInequalitySolver())
2149 if (options::bitvectorInequalitySolver
.wasSetByUser())
2151 throw OptionException(
2152 "--bv-inequality-solver is not supported with proofs");
2154 Notice() << "SmtEngine: turning off bv ineq solver to support proofs"
2156 options::bitvectorInequalitySolver
.set(false);
2160 if (!options::bitvectorEqualitySolver())
2162 if (options::bvLazyRewriteExtf())
2164 if (options::bvLazyRewriteExtf
.wasSetByUser())
2166 throw OptionException(
2167 "--bv-lazy-rewrite-extf requires --bv-eq-solver to be set");
2171 << "disabling bvLazyRewriteExtf since equality solver is disabled"
2173 options::bvLazyRewriteExtf
.set(false);
2177 void SmtEngine::setProblemExtended(bool value
)
2179 d_problemExtended
= value
;
2180 if (value
) { d_assumptions
.clear(); }
2183 void SmtEngine::setInfo(const std::string
& key
, const CVC4::SExpr
& value
)
2185 SmtScope
smts(this);
2187 Trace("smt") << "SMT setInfo(" << key
<< ", " << value
<< ")" << endl
;
2189 if(Dump
.isOn("benchmark")) {
2190 if(key
== "status") {
2191 string s
= value
.getValue();
2192 BenchmarkStatus status
=
2193 (s
== "sat") ? SMT_SATISFIABLE
:
2194 ((s
== "unsat") ? SMT_UNSATISFIABLE
: SMT_UNKNOWN
);
2195 Dump("benchmark") << SetBenchmarkStatusCommand(status
);
2197 Dump("benchmark") << SetInfoCommand(key
, value
);
2201 // Check for CVC4-specific info keys (prefixed with "cvc4-" or "cvc4_")
2202 if(key
.length() > 5) {
2203 string prefix
= key
.substr(0, 5);
2204 if(prefix
== "cvc4-" || prefix
== "cvc4_") {
2205 string cvc4key
= key
.substr(5);
2206 if(cvc4key
== "logic") {
2207 if(! value
.isAtom()) {
2208 throw OptionException("argument to (set-info :cvc4-logic ..) must be a string");
2210 SmtScope
smts(this);
2211 d_logic
= value
.getValue();
2215 throw UnrecognizedOptionException();
2220 // Check for standard info keys (SMT-LIB v1, SMT-LIB v2, ...)
2221 if (key
== "source" || key
== "category" || key
== "difficulty"
2222 || key
== "notes" || key
== "name" || key
== "license")
2227 else if (key
== "filename")
2229 d_filename
= value
.getValue();
2232 else if (key
== "smt-lib-version" && !options::inputLanguage
.wasSetByUser())
2234 language::input::Language ilang
= language::input::LANG_AUTO
;
2235 if( (value
.isInteger() && value
.getIntegerValue() == Integer(2)) ||
2236 (value
.isRational() && value
.getRationalValue() == Rational(2)) ||
2237 value
.getValue() == "2" ||
2238 value
.getValue() == "2.0" ) {
2239 ilang
= language::input::LANG_SMTLIB_V2_0
;
2240 } else if( (value
.isRational() && value
.getRationalValue() == Rational(5, 2)) ||
2241 value
.getValue() == "2.5" ) {
2242 ilang
= language::input::LANG_SMTLIB_V2_5
;
2243 } else if( (value
.isRational() && value
.getRationalValue() == Rational(13, 5)) ||
2244 value
.getValue() == "2.6" ) {
2245 ilang
= language::input::LANG_SMTLIB_V2_6
;
2247 else if (value
.getValue() == "2.6.1")
2249 ilang
= language::input::LANG_SMTLIB_V2_6_1
;
2253 Warning() << "Warning: unsupported smt-lib-version: " << value
<< endl
;
2254 throw UnrecognizedOptionException();
2256 options::inputLanguage
.set(ilang
);
2257 // also update the output language
2258 if (!options::outputLanguage
.wasSetByUser())
2260 language::output::Language olang
= language::toOutputLanguage(ilang
);
2261 if (options::outputLanguage() != olang
)
2263 options::outputLanguage
.set(olang
);
2264 *options::out() << language::SetLanguage(olang
);
2268 } else if(key
== "status") {
2270 if(value
.isAtom()) {
2271 s
= value
.getValue();
2273 if(s
!= "sat" && s
!= "unsat" && s
!= "unknown") {
2274 throw OptionException("argument to (set-info :status ..) must be "
2275 "`sat' or `unsat' or `unknown'");
2277 d_status
= Result(s
, d_filename
);
2280 throw UnrecognizedOptionException();
2283 CVC4::SExpr
SmtEngine::getInfo(const std::string
& key
) const {
2285 SmtScope
smts(this);
2287 Trace("smt") << "SMT getInfo(" << key
<< ")" << endl
;
2288 if(key
== "all-statistics") {
2289 vector
<SExpr
> stats
;
2290 for(StatisticsRegistry::const_iterator i
= NodeManager::fromExprManager(d_exprManager
)->getStatisticsRegistry()->begin();
2291 i
!= NodeManager::fromExprManager(d_exprManager
)->getStatisticsRegistry()->end();
2294 v
.push_back((*i
).first
);
2295 v
.push_back((*i
).second
);
2298 for(StatisticsRegistry::const_iterator i
= d_statisticsRegistry
->begin();
2299 i
!= d_statisticsRegistry
->end();
2302 v
.push_back((*i
).first
);
2303 v
.push_back((*i
).second
);
2306 return SExpr(stats
);
2307 } else if(key
== "error-behavior") {
2308 // immediate-exit | continued-execution
2309 if( options::continuedExecution() || options::interactive() ) {
2310 return SExpr(SExpr::Keyword("continued-execution"));
2312 return SExpr(SExpr::Keyword("immediate-exit"));
2314 } else if(key
== "name") {
2315 return SExpr(Configuration::getName());
2316 } else if(key
== "version") {
2317 return SExpr(Configuration::getVersionString());
2318 } else if(key
== "authors") {
2319 return SExpr(Configuration::about());
2320 } else if(key
== "status") {
2321 // sat | unsat | unknown
2322 switch(d_status
.asSatisfiabilityResult().isSat()) {
2324 return SExpr(SExpr::Keyword("sat"));
2326 return SExpr(SExpr::Keyword("unsat"));
2328 return SExpr(SExpr::Keyword("unknown"));
2330 } else if(key
== "reason-unknown") {
2331 if(!d_status
.isNull() && d_status
.isUnknown()) {
2333 ss
<< d_status
.whyUnknown();
2334 string s
= ss
.str();
2335 transform(s
.begin(), s
.end(), s
.begin(), ::tolower
);
2336 return SExpr(SExpr::Keyword(s
));
2338 throw ModalException("Can't get-info :reason-unknown when the "
2339 "last result wasn't unknown!");
2341 } else if(key
== "assertion-stack-levels") {
2342 AlwaysAssert(d_userLevels
.size() <=
2343 std::numeric_limits
<unsigned long int>::max());
2344 return SExpr(static_cast<unsigned long int>(d_userLevels
.size()));
2345 } else if(key
== "all-options") {
2346 // get the options, like all-statistics
2347 std::vector
< std::vector
<std::string
> > current_options
=
2348 Options::current()->getOptions();
2349 return SExpr::parseListOfListOfAtoms(current_options
);
2351 throw UnrecognizedOptionException();
2355 void SmtEngine::debugCheckFormals(const std::vector
<Expr
>& formals
, Expr func
)
2357 for(std::vector
<Expr
>::const_iterator i
= formals
.begin(); i
!= formals
.end(); ++i
) {
2358 if((*i
).getKind() != kind::BOUND_VARIABLE
) {
2360 ss
<< "All formal arguments to defined functions must be BOUND_VARIABLEs, but in the\n"
2361 << "definition of function " << func
<< ", formal\n"
2362 << " " << *i
<< "\n"
2363 << "has kind " << (*i
).getKind();
2364 throw TypeCheckingException(func
, ss
.str());
2369 void SmtEngine::debugCheckFunctionBody(Expr formula
,
2370 const std::vector
<Expr
>& formals
,
2373 Type formulaType
= formula
.getType(options::typeChecking());
2374 Type funcType
= func
.getType();
2375 // We distinguish here between definitions of constants and functions,
2376 // because the type checking for them is subtly different. Perhaps we
2377 // should instead have SmtEngine::defineFunction() and
2378 // SmtEngine::defineConstant() for better clarity, although then that
2379 // doesn't match the SMT-LIBv2 standard...
2380 if(formals
.size() > 0) {
2381 Type rangeType
= FunctionType(funcType
).getRangeType();
2382 if(! formulaType
.isComparableTo(rangeType
)) {
2384 ss
<< "Type of defined function does not match its declaration\n"
2385 << "The function : " << func
<< "\n"
2386 << "Declared type : " << rangeType
<< "\n"
2387 << "The body : " << formula
<< "\n"
2388 << "Body type : " << formulaType
;
2389 throw TypeCheckingException(func
, ss
.str());
2392 if(! formulaType
.isComparableTo(funcType
)) {
2394 ss
<< "Declared type of defined constant does not match its definition\n"
2395 << "The constant : " << func
<< "\n"
2396 << "Declared type : " << funcType
<< " " << Type::getTypeNode(funcType
)->getId() << "\n"
2397 << "The definition : " << formula
<< "\n"
2398 << "Definition type: " << formulaType
<< " " << Type::getTypeNode(formulaType
)->getId();
2399 throw TypeCheckingException(func
, ss
.str());
2404 void SmtEngine::defineFunction(Expr func
,
2405 const std::vector
<Expr
>& formals
,
2408 SmtScope
smts(this);
2410 Trace("smt") << "SMT defineFunction(" << func
<< ")" << endl
;
2411 debugCheckFormals(formals
, func
);
2414 ss
<< language::SetLanguage(
2415 language::SetLanguage::getLanguage(Dump
.getStream()))
2417 DefineFunctionCommand
c(ss
.str(), func
, formals
, formula
);
2418 addToModelCommandAndDump(
2419 c
, ExprManager::VAR_FLAG_DEFINED
, true, "declarations");
2421 PROOF(if (options::checkUnsatCores()) {
2422 d_defineCommands
.push_back(c
.clone());
2426 debugCheckFunctionBody(formula
, formals
, func
);
2428 // Substitute out any abstract values in formula
2430 d_private
->substituteAbstractValues(Node::fromExpr(formula
)).toExpr();
2432 TNode funcNode
= func
.getTNode();
2433 vector
<Node
> formalsNodes
;
2434 for(vector
<Expr
>::const_iterator i
= formals
.begin(),
2435 iend
= formals
.end();
2438 formalsNodes
.push_back((*i
).getNode());
2440 TNode formNode
= form
.getTNode();
2441 DefinedFunction
def(funcNode
, formalsNodes
, formNode
);
2442 // Permit (check-sat) (define-fun ...) (get-value ...) sequences.
2443 // Otherwise, (check-sat) (get-value ((! foo :named bar))) breaks
2444 // d_haveAdditions = true;
2445 Debug("smt") << "definedFunctions insert " << funcNode
<< " " << formNode
<< endl
;
2446 d_definedFunctions
->insert(funcNode
, def
);
2449 void SmtEngine::defineFunctionsRec(
2450 const std::vector
<Expr
>& funcs
,
2451 const std::vector
<std::vector
<Expr
> >& formals
,
2452 const std::vector
<Expr
>& formulas
)
2454 SmtScope
smts(this);
2455 finalOptionsAreSet();
2457 Trace("smt") << "SMT defineFunctionsRec(...)" << endl
;
2459 if (funcs
.size() != formals
.size() && funcs
.size() != formulas
.size())
2462 ss
<< "Number of functions, formals, and function bodies passed to "
2463 "defineFunctionsRec do not match:"
2465 << " #functions : " << funcs
.size() << "\n"
2466 << " #arg lists : " << formals
.size() << "\n"
2467 << " #function bodies : " << formulas
.size() << "\n";
2468 throw ModalException(ss
.str());
2470 for (unsigned i
= 0, size
= funcs
.size(); i
< size
; i
++)
2472 // check formal argument list
2473 debugCheckFormals(formals
[i
], funcs
[i
]);
2475 debugCheckFunctionBody(formulas
[i
], formals
[i
], funcs
[i
]);
2478 if (Dump
.isOn("raw-benchmark"))
2480 Dump("raw-benchmark") << DefineFunctionRecCommand(funcs
, formals
, formulas
);
2483 ExprManager
* em
= getExprManager();
2484 for (unsigned i
= 0, size
= funcs
.size(); i
< size
; i
++)
2486 // we assert a quantified formula
2488 // make the function application
2489 if (formals
[i
].empty())
2491 // it has no arguments
2492 func_app
= funcs
[i
];
2496 std::vector
<Expr
> children
;
2497 children
.push_back(funcs
[i
]);
2498 children
.insert(children
.end(), formals
[i
].begin(), formals
[i
].end());
2499 func_app
= em
->mkExpr(kind::APPLY_UF
, children
);
2501 Expr lem
= em
->mkExpr(kind::EQUAL
, func_app
, formulas
[i
]);
2502 if (!formals
[i
].empty())
2504 // set the attribute to denote this is a function definition
2505 std::string
attr_name("fun-def");
2506 Expr aexpr
= em
->mkExpr(kind::INST_ATTRIBUTE
, func_app
);
2507 aexpr
= em
->mkExpr(kind::INST_PATTERN_LIST
, aexpr
);
2508 std::vector
<Expr
> expr_values
;
2509 std::string str_value
;
2510 setUserAttribute(attr_name
, func_app
, expr_values
, str_value
);
2511 // make the quantified formula
2512 Expr boundVars
= em
->mkExpr(kind::BOUND_VAR_LIST
, formals
[i
]);
2513 lem
= em
->mkExpr(kind::FORALL
, boundVars
, lem
, aexpr
);
2515 // assert the quantified formula
2516 // notice we don't call assertFormula directly, since this would
2517 // duplicate the output on raw-benchmark.
2518 Expr e
= d_private
->substituteAbstractValues(Node::fromExpr(lem
)).toExpr();
2519 if (d_assertionList
!= NULL
)
2521 d_assertionList
->push_back(e
);
2523 d_private
->addFormula(e
.getNode(), false);
2527 void SmtEngine::defineFunctionRec(Expr func
,
2528 const std::vector
<Expr
>& formals
,
2531 std::vector
<Expr
> funcs
;
2532 funcs
.push_back(func
);
2533 std::vector
<std::vector
<Expr
> > formals_multi
;
2534 formals_multi
.push_back(formals
);
2535 std::vector
<Expr
> formulas
;
2536 formulas
.push_back(formula
);
2537 defineFunctionsRec(funcs
, formals_multi
, formulas
);
2540 bool SmtEngine::isDefinedFunction( Expr func
){
2541 Node nf
= Node::fromExpr( func
);
2542 Debug("smt") << "isDefined function " << nf
<< "?" << std::endl
;
2543 return d_definedFunctions
->find(nf
) != d_definedFunctions
->end();
2546 void SmtEnginePrivate::finishInit()
2548 PreprocessingPassRegistry
& ppReg
= PreprocessingPassRegistry::getInstance();
2549 d_preprocessingPassContext
.reset(new PreprocessingPassContext(
2550 &d_smt
, d_resourceManager
, &d_iteRemover
, &d_propagator
));
2552 // TODO: this will likely change when we add support for actually assembling
2553 // preprocessing pipelines. For now, we just create an instance of each
2554 // available preprocessing pass.
2555 std::vector
<std::string
> passNames
= ppReg
.getAvailablePasses();
2556 for (const std::string
& passName
: passNames
)
2558 d_passes
[passName
].reset(
2559 ppReg
.createPass(d_preprocessingPassContext
.get(), passName
));
2563 Node
SmtEnginePrivate::expandDefinitions(TNode n
, unordered_map
<Node
, Node
, NodeHashFunction
>& cache
, bool expandOnly
)
2565 stack
<std::tuple
<Node
, Node
, bool>> worklist
;
2567 worklist
.push(std::make_tuple(Node(n
), Node(n
), false));
2568 // The worklist is made of triples, each is input / original node then the output / rewritten node
2569 // and finally a flag tracking whether the children have been explored (i.e. if this is a downward
2573 spendResource(options::preprocessStep());
2575 // n is the input / original
2576 // node is the output / result
2578 bool childrenPushed
;
2579 std::tie(n
, node
, childrenPushed
) = worklist
.top();
2582 // Working downwards
2583 if(!childrenPushed
) {
2584 Kind k
= n
.getKind();
2586 // we can short circuit (variable) leaves
2588 SmtEngine::DefinedFunctionMap::const_iterator i
= d_smt
.d_definedFunctions
->find(n
);
2589 if(i
!= d_smt
.d_definedFunctions
->end()) {
2590 // replacement must be closed
2591 if((*i
).second
.getFormals().size() > 0) {
2592 result
.push(d_smt
.d_nodeManager
->mkNode(kind::LAMBDA
, d_smt
.d_nodeManager
->mkNode(kind::BOUND_VAR_LIST
, (*i
).second
.getFormals()), (*i
).second
.getFormula()));
2595 // don't bother putting in the cache
2596 result
.push((*i
).second
.getFormula());
2599 // don't bother putting in the cache
2604 // maybe it's in the cache
2605 unordered_map
<Node
, Node
, NodeHashFunction
>::iterator cacheHit
= cache
.find(n
);
2606 if(cacheHit
!= cache
.end()) {
2607 TNode ret
= (*cacheHit
).second
;
2608 result
.push(ret
.isNull() ? n
: ret
);
2612 // otherwise expand it
2613 bool doExpand
= false;
2614 if (k
== kind::APPLY
)
2618 else if (k
== kind::APPLY_UF
)
2620 // Always do beta-reduction here. The reason is that there may be
2621 // operators such as INTS_MODULUS in the body of the lambda that would
2622 // otherwise be introduced by beta-reduction via the rewriter, but are
2623 // not expanded here since the traversal in this function does not
2624 // traverse the operators of nodes. Hence, we beta-reduce here to
2625 // ensure terms in the body of the lambda are expanded during this
2627 if (n
.getOperator().getKind() == kind::LAMBDA
)
2631 else if (options::macrosQuant() || options::sygusInference())
2633 // The above options assign substitutions to APPLY_UF, thus we check
2634 // here and expand if this operator corresponds to a defined function.
2635 doExpand
= d_smt
.isDefinedFunction(n
.getOperator().toExpr());
2639 vector
<Node
> formals
;
2641 if( n
.getOperator().getKind() == kind::LAMBDA
){
2642 TNode op
= n
.getOperator();
2644 for( unsigned i
=0; i
<op
[0].getNumChildren(); i
++ ){
2645 formals
.push_back( op
[0][i
] );
2649 // application of a user-defined symbol
2650 TNode func
= n
.getOperator();
2651 SmtEngine::DefinedFunctionMap::const_iterator i
= d_smt
.d_definedFunctions
->find(func
);
2652 if(i
== d_smt
.d_definedFunctions
->end()) {
2653 throw TypeCheckingException(n
.toExpr(), string("Undefined function: `") + func
.toString() + "'");
2655 DefinedFunction def
= (*i
).second
;
2656 formals
= def
.getFormals();
2658 if(Debug
.isOn("expand")) {
2659 Debug("expand") << "found: " << n
<< endl
;
2660 Debug("expand") << " func: " << func
<< endl
;
2661 string name
= func
.getAttribute(expr::VarNameAttr());
2662 Debug("expand") << " : \"" << name
<< "\"" << endl
;
2664 if(Debug
.isOn("expand")) {
2665 Debug("expand") << " defn: " << def
.getFunction() << endl
2667 if(formals
.size() > 0) {
2668 copy( formals
.begin(), formals
.end() - 1,
2669 ostream_iterator
<Node
>(Debug("expand"), ", ") );
2670 Debug("expand") << formals
.back();
2672 Debug("expand") << "]" << endl
2673 << " " << def
.getFunction().getType() << endl
2674 << " " << def
.getFormula() << endl
;
2677 fm
= def
.getFormula();
2680 Node instance
= fm
.substitute(formals
.begin(),
2683 n
.begin() + formals
.size());
2684 Debug("expand") << "made : " << instance
<< endl
;
2686 Node expanded
= expandDefinitions(instance
, cache
, expandOnly
);
2687 cache
[n
] = (n
== expanded
? Node::null() : expanded
);
2688 result
.push(expanded
);
2691 } else if(! expandOnly
) {
2692 // do not do any theory stuff if expandOnly is true
2694 theory::Theory
* t
= d_smt
.d_theoryEngine
->theoryOf(node
);
2697 LogicRequest
req(d_smt
);
2698 node
= t
->expandDefinition(req
, n
);
2701 // the partial functions can fall through, in which case we still
2702 // consider their children
2703 worklist
.push(std::make_tuple(
2704 Node(n
), node
, true)); // Original and rewritten result
2706 for(size_t i
= 0; i
< node
.getNumChildren(); ++i
) {
2708 std::make_tuple(node
[i
],
2710 false)); // Rewrite the children of the result only
2715 // Reconstruct the node from it's (now rewritten) children on the stack
2717 Debug("expand") << "cons : " << node
<< endl
;
2718 if(node
.getNumChildren()>0) {
2719 //cout << "cons : " << node << endl;
2720 NodeBuilder
<> nb(node
.getKind());
2721 if(node
.getMetaKind() == kind::metakind::PARAMETERIZED
) {
2722 Debug("expand") << "op : " << node
.getOperator() << endl
;
2723 //cout << "op : " << node.getOperator() << endl;
2724 nb
<< node
.getOperator();
2726 for(size_t i
= 0; i
< node
.getNumChildren(); ++i
) {
2727 Assert(!result
.empty());
2728 Node expanded
= result
.top();
2730 //cout << "exchld : " << expanded << endl;
2731 Debug("expand") << "exchld : " << expanded
<< endl
;
2736 cache
[n
] = n
== node
? Node::null() : node
; // Only cache once all subterms are expanded
2739 } while(!worklist
.empty());
2741 AlwaysAssert(result
.size() == 1);
2743 return result
.top();
2746 // do dumping (before/after any preprocessing pass)
2747 static void dumpAssertions(const char* key
,
2748 const AssertionPipeline
& assertionList
) {
2749 if( Dump
.isOn("assertions") &&
2750 Dump
.isOn(string("assertions:") + key
) ) {
2751 // Push the simplified assertions to the dump output stream
2752 for(unsigned i
= 0; i
< assertionList
.size(); ++ i
) {
2753 TNode n
= assertionList
[i
];
2754 Dump("assertions") << AssertCommand(Expr(n
.toExpr()));
2759 // returns false if simplification led to "false"
2760 bool SmtEnginePrivate::simplifyAssertions()
2762 spendResource(options::preprocessStep());
2763 Assert(d_smt
.d_pendingPops
== 0);
2765 ScopeCounter
depth(d_simplifyAssertionsDepth
);
2767 Trace("simplify") << "SmtEnginePrivate::simplify()" << endl
;
2769 if (options::simplificationMode() != SIMPLIFICATION_MODE_NONE
)
2771 if (!options::unsatCores() && !options::fewerPreprocessingHoles())
2773 // Perform non-clausal simplification
2774 PreprocessingPassResult res
=
2775 d_passes
["non-clausal-simp"]->apply(&d_assertions
);
2776 if (res
== PreprocessingPassResult::CONFLICT
)
2782 // We piggy-back off of the BackEdgesMap in the CircuitPropagator to
2783 // do the miplib trick.
2784 if ( // check that option is on
2785 options::arithMLTrick() &&
2786 // miplib rewrites aren't safe in incremental mode
2787 !options::incrementalSolving() &&
2788 // only useful in arith
2789 d_smt
.d_logic
.isTheoryEnabled(THEORY_ARITH
) &&
2790 // we add new assertions and need this (in practice, this
2791 // restriction only disables miplib processing during
2792 // re-simplification, which we don't expect to be useful anyway)
2793 d_assertions
.getRealAssertionsEnd() == d_assertions
.size())
2795 d_passes
["miplib-trick"]->apply(&d_assertions
);
2797 Trace("simplify") << "SmtEnginePrivate::simplify(): "
2798 << "skipping miplib pseudobooleans pass (either incrementalSolving is on, or miplib pbs are turned off)..." << endl
;
2802 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
2804 // before ppRewrite check if only core theory for BV theory
2805 d_smt
.d_theoryEngine
->staticInitializeBVOptions(d_assertions
.ref());
2807 // Theory preprocessing
2808 if (d_smt
.d_earlyTheoryPP
)
2810 d_passes
["theory-preprocess"]->apply(&d_assertions
);
2813 // ITE simplification
2814 if (options::doITESimp()
2815 && (d_simplifyAssertionsDepth
<= 1 || options::doITESimpOnRepeat()))
2817 PreprocessingPassResult res
= d_passes
["ite-simp"]->apply(&d_assertions
);
2818 if (res
== PreprocessingPassResult::CONFLICT
)
2820 Chat() << "...ITE simplification found unsat..." << endl
;
2825 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
2827 // Unconstrained simplification
2828 if(options::unconstrainedSimp()) {
2829 d_passes
["unconstrained-simplifier"]->apply(&d_assertions
);
2832 if (options::repeatSimp()
2833 && options::simplificationMode() != SIMPLIFICATION_MODE_NONE
2834 && !options::unsatCores() && !options::fewerPreprocessingHoles())
2836 PreprocessingPassResult res
=
2837 d_passes
["non-clausal-simp"]->apply(&d_assertions
);
2838 if (res
== PreprocessingPassResult::CONFLICT
)
2844 dumpAssertions("post-repeatsimp", d_assertions
);
2845 Trace("smt") << "POST repeatSimp" << endl
;
2846 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
2848 } catch(TypeCheckingExceptionPrivate
& tcep
) {
2849 // Calls to this function should have already weeded out any
2850 // typechecking exceptions via (e.g.) ensureBoolean(). But a
2851 // theory could still create a new expression that isn't
2852 // well-typed, and we don't want the C++ runtime to abort our
2853 // process without any error notice.
2855 ss
<< "A bad expression was produced. Original exception follows:\n"
2857 InternalError(ss
.str().c_str());
2862 Result
SmtEngine::check() {
2863 Assert(d_fullyInited
);
2864 Assert(d_pendingPops
== 0);
2866 Trace("smt") << "SmtEngine::check()" << endl
;
2868 ResourceManager
* resourceManager
= d_private
->getResourceManager();
2870 resourceManager
->beginCall();
2872 // Only way we can be out of resource is if cumulative budget is on
2873 if (resourceManager
->cumulativeLimitOn() &&
2874 resourceManager
->out()) {
2875 Result::UnknownExplanation why
= resourceManager
->outOfResources() ?
2876 Result::RESOURCEOUT
: Result::TIMEOUT
;
2877 return Result(Result::VALIDITY_UNKNOWN
, why
, d_filename
);
2880 // Make sure the prop layer has all of the assertions
2881 Trace("smt") << "SmtEngine::check(): processing assertions" << endl
;
2882 d_private
->processAssertions();
2883 Trace("smt") << "SmtEngine::check(): done processing assertions" << endl
;
2885 // Turn off stop only for QF_LRA
2886 // TODO: Bring up in a meeting where to put this
2887 if(options::decisionStopOnly() && !options::decisionMode
.wasSetByUser() ){
2889 (not d_logic
.isQuantified() &&
2890 d_logic
.isPure(THEORY_ARITH
) && d_logic
.isLinear() && !d_logic
.isDifferenceLogic() && !d_logic
.areIntegersUsed()
2892 if (d_private
->getIteSkolemMap().empty())
2894 options::decisionStopOnly
.set(false);
2895 d_decisionEngine
->clearStrategies();
2896 Trace("smt") << "SmtEngine::check(): turning off stop only" << endl
;
2901 TimerStat::CodeTimer
solveTimer(d_stats
->d_solveTime
);
2903 Chat() << "solving..." << endl
;
2904 Trace("smt") << "SmtEngine::check(): running check" << endl
;
2905 Result result
= d_propEngine
->checkSat();
2907 resourceManager
->endCall();
2908 Trace("limit") << "SmtEngine::check(): cumulative millis " << resourceManager
->getTimeUsage()
2909 << ", resources " << resourceManager
->getResourceUsage() << endl
;
2912 return Result(result
, d_filename
);
2915 Result
SmtEngine::quickCheck() {
2916 Assert(d_fullyInited
);
2917 Trace("smt") << "SMT quickCheck()" << endl
;
2918 return Result(Result::VALIDITY_UNKNOWN
, Result::REQUIRES_FULL_CHECK
, d_filename
);
2922 void SmtEnginePrivate::collectSkolems(TNode n
, set
<TNode
>& skolemSet
, unordered_map
<Node
, bool, NodeHashFunction
>& cache
)
2924 unordered_map
<Node
, bool, NodeHashFunction
>::iterator it
;
2926 if (it
!= cache
.end()) {
2930 size_t sz
= n
.getNumChildren();
2932 IteSkolemMap::iterator it
= getIteSkolemMap().find(n
);
2933 if (it
!= getIteSkolemMap().end())
2935 skolemSet
.insert(n
);
2942 for (; k
< sz
; ++k
) {
2943 collectSkolems(n
[k
], skolemSet
, cache
);
2948 bool SmtEnginePrivate::checkForBadSkolems(TNode n
, TNode skolem
, unordered_map
<Node
, bool, NodeHashFunction
>& cache
)
2950 unordered_map
<Node
, bool, NodeHashFunction
>::iterator it
;
2952 if (it
!= cache
.end()) {
2953 return (*it
).second
;
2956 size_t sz
= n
.getNumChildren();
2958 IteSkolemMap::iterator it
= getIteSkolemMap().find(n
);
2960 if (it
!= getIteSkolemMap().end())
2962 if (!((*it
).first
< n
)) {
2971 for (; k
< sz
; ++k
) {
2972 if (checkForBadSkolems(n
[k
], skolem
, cache
)) {
2982 void SmtEnginePrivate::processAssertions() {
2983 TimerStat::CodeTimer
paTimer(d_smt
.d_stats
->d_processAssertionsTime
);
2984 spendResource(options::preprocessStep());
2985 Assert(d_smt
.d_fullyInited
);
2986 Assert(d_smt
.d_pendingPops
== 0);
2987 SubstitutionMap
& top_level_substs
=
2988 d_preprocessingPassContext
->getTopLevelSubstitutions();
2990 // Dump the assertions
2991 dumpAssertions("pre-everything", d_assertions
);
2993 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() begin" << endl
;
2994 Trace("smt") << "SmtEnginePrivate::processAssertions()" << endl
;
2996 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
2998 if (d_assertions
.size() == 0) {
3003 if (options::bvGaussElim())
3005 d_passes
["bv-gauss"]->apply(&d_assertions
);
3008 if (d_assertionsProcessed
&& options::incrementalSolving()) {
3009 // TODO(b/1255): Substitutions in incremental mode should be managed with a
3010 // proper data structure.
3012 // Placeholder for storing substitutions
3013 d_preprocessingPassContext
->setSubstitutionsIndex(d_assertions
.size());
3014 d_assertions
.push_back(NodeManager::currentNM()->mkConst
<bool>(true));
3017 // Add dummy assertion in last position - to be used as a
3018 // placeholder for any new assertions to get added
3019 d_assertions
.push_back(NodeManager::currentNM()->mkConst
<bool>(true));
3020 // any assertions added beyond realAssertionsEnd must NOT affect the
3021 // equisatisfiability
3022 d_assertions
.updateRealAssertionsEnd();
3024 // Assertions are NOT guaranteed to be rewritten by this point
3026 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-definition-expansion" << endl
;
3027 dumpAssertions("pre-definition-expansion", d_assertions
);
3029 Chat() << "expanding definitions..." << endl
;
3030 Trace("simplify") << "SmtEnginePrivate::simplify(): expanding definitions" << endl
;
3031 TimerStat::CodeTimer
codeTimer(d_smt
.d_stats
->d_definitionExpansionTime
);
3032 unordered_map
<Node
, Node
, NodeHashFunction
> cache
;
3033 for(unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
3034 d_assertions
.replace(i
, expandDefinitions(d_assertions
[i
], cache
));
3037 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-definition-expansion" << endl
;
3038 dumpAssertions("post-definition-expansion", d_assertions
);
3040 // save the assertions now
3043 for (unsigned i
= 0; i
< d_assertions
.size(); ++i
) {
3044 ProofManager::currentPM()->addAssertion(d_assertions
[i
].toExpr());
3048 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
3050 if (options::globalNegate())
3052 // global negation of the formula
3053 d_passes
["global-negate"]->apply(&d_assertions
);
3054 d_smt
.d_globalNegation
= !d_smt
.d_globalNegation
;
3057 if( options::nlExtPurify() ){
3058 d_passes
["nl-ext-purify"]->apply(&d_assertions
);
3061 if( options::ceGuidedInst() ){
3062 //register sygus conjecture pre-rewrite (motivated by solution reconstruction)
3063 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
3064 d_smt
.d_theoryEngine
->getQuantifiersEngine()
3066 ->preregisterAssertion(d_assertions
[i
]);
3070 if (options::solveRealAsInt()) {
3071 d_passes
["real-to-int"]->apply(&d_assertions
);
3074 if (options::solveIntAsBV() > 0)
3076 d_passes
["int-to-bv"]->apply(&d_assertions
);
3079 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
&&
3080 !d_smt
.d_logic
.isPure(THEORY_BV
) &&
3081 d_smt
.d_logic
.getLogicString() != "QF_UFBV" &&
3082 d_smt
.d_logic
.getLogicString() != "QF_ABV") {
3083 throw ModalException("Eager bit-blasting does not currently support theory combination. "
3084 "Note that in a QF_BV problem UF symbols can be introduced for division. "
3085 "Try --bv-div-zero-const to interpret division by zero as a constant.");
3088 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
3089 && !options::incrementalSolving())
3091 d_passes
["bv-ackermann"]->apply(&d_assertions
);
3094 if (options::bvAbstraction() && !options::incrementalSolving())
3096 d_passes
["bv-abstraction"]->apply(&d_assertions
);
3099 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
3101 bool noConflict
= true;
3103 if (options::extRewPrep())
3105 d_passes
["ext-rew-pre"]->apply(&d_assertions
);
3108 // Unconstrained simplification
3109 if(options::unconstrainedSimp()) {
3110 d_passes
["rewrite"]->apply(&d_assertions
);
3111 d_passes
["unconstrained-simplifier"]->apply(&d_assertions
);
3114 if(options::bvIntroducePow2())
3116 d_passes
["bv-intro-pow2"]->apply(&d_assertions
);
3119 if (options::unsatCores())
3121 // special rewriting pass for unsat cores, since many of the passes below
3123 d_passes
["rewrite"]->apply(&d_assertions
);
3127 d_passes
["apply-substs"]->apply(&d_assertions
);
3130 // Assertions ARE guaranteed to be rewritten by this point
3131 #ifdef CVC4_ASSERTIONS
3132 for (unsigned i
= 0; i
< d_assertions
.size(); ++i
)
3134 Assert(Rewriter::rewrite(d_assertions
[i
]) == d_assertions
[i
]);
3138 // Lift bit-vectors of size 1 to bool
3139 if (options::bitvectorToBool())
3141 d_passes
["bv-to-bool"]->apply(&d_assertions
);
3143 // Convert non-top-level Booleans to bit-vectors of size 1
3144 if (options::boolToBitvector())
3146 d_passes
["bool-to-bv"]->apply(&d_assertions
);
3148 if(options::sepPreSkolemEmp()) {
3149 d_passes
["sep-skolem-emp"]->apply(&d_assertions
);
3152 if( d_smt
.d_logic
.isQuantified() ){
3153 //remove rewrite rules, apply pre-skolemization to existential quantifiers
3154 d_passes
["quantifiers-preprocess"]->apply(&d_assertions
);
3155 if( options::macrosQuant() ){
3156 //quantifiers macro expansion
3157 d_passes
["quantifier-macros"]->apply(&d_assertions
);
3160 //fmf-fun : assume admissible functions, applying preprocessing reduction to FMF
3161 if( options::fmfFunWellDefined() ){
3162 quantifiers::FunDefFmf fdf
;
3163 Assert( d_smt
.d_fmfRecFunctionsDefined
!=NULL
);
3164 //must carry over current definitions (for incremental)
3165 for( context::CDList
<Node
>::const_iterator fit
= d_smt
.d_fmfRecFunctionsDefined
->begin();
3166 fit
!= d_smt
.d_fmfRecFunctionsDefined
->end(); ++fit
) {
3168 Assert( d_smt
.d_fmfRecFunctionsAbs
.find( f
)!=d_smt
.d_fmfRecFunctionsAbs
.end() );
3169 TypeNode ft
= d_smt
.d_fmfRecFunctionsAbs
[f
];
3170 fdf
.d_sorts
[f
] = ft
;
3171 std::map
< Node
, std::vector
< Node
> >::iterator fcit
= d_smt
.d_fmfRecFunctionsConcrete
.find( f
);
3172 Assert( fcit
!=d_smt
.d_fmfRecFunctionsConcrete
.end() );
3173 for( unsigned j
=0; j
<fcit
->second
.size(); j
++ ){
3174 fdf
.d_input_arg_inj
[f
].push_back( fcit
->second
[j
] );
3177 fdf
.simplify( d_assertions
.ref() );
3178 //must store new definitions (for incremental)
3179 for( unsigned i
=0; i
<fdf
.d_funcs
.size(); i
++ ){
3180 Node f
= fdf
.d_funcs
[i
];
3181 d_smt
.d_fmfRecFunctionsAbs
[f
] = fdf
.d_sorts
[f
];
3182 d_smt
.d_fmfRecFunctionsConcrete
[f
].clear();
3183 for( unsigned j
=0; j
<fdf
.d_input_arg_inj
[f
].size(); j
++ ){
3184 d_smt
.d_fmfRecFunctionsConcrete
[f
].push_back( fdf
.d_input_arg_inj
[f
][j
] );
3186 d_smt
.d_fmfRecFunctionsDefined
->push_back( f
);
3189 if (options::sygusInference())
3191 d_passes
["sygus-infer"]->apply(&d_assertions
);
3195 if( options::sortInference() || options::ufssFairnessMonotone() ){
3196 d_passes
["sort-inference"]->apply(&d_assertions
);
3199 if( options::pbRewrites() ){
3200 d_passes
["pseudo-boolean-processor"]->apply(&d_assertions
);
3203 if (options::sygusRewSynthInput())
3205 // do candidate rewrite rule synthesis
3206 d_passes
["synth-rr"]->apply(&d_assertions
);
3209 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-simplify" << endl
;
3210 dumpAssertions("pre-simplify", d_assertions
);
3211 Chat() << "simplifying assertions..." << endl
;
3212 noConflict
= simplifyAssertions();
3214 ++(d_smt
.d_stats
->d_simplifiedToFalse
);
3216 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-simplify" << endl
;
3217 dumpAssertions("post-simplify", d_assertions
);
3219 if (options::symmetryBreakerExp() && !options::incrementalSolving())
3221 // apply symmetry breaking if not in incremental mode
3222 d_passes
["sym-break"]->apply(&d_assertions
);
3225 if(options::doStaticLearning()) {
3226 d_passes
["static-learning"]->apply(&d_assertions
);
3228 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
3231 d_smt
.d_stats
->d_numAssertionsPre
+= d_assertions
.size();
3232 d_passes
["ite-removal"]->apply(&d_assertions
);
3233 // This is needed because when solving incrementally, removeITEs may introduce
3234 // skolems that were solved for earlier and thus appear in the substitution
3236 d_passes
["apply-substs"]->apply(&d_assertions
);
3237 d_smt
.d_stats
->d_numAssertionsPost
+= d_assertions
.size();
3240 dumpAssertions("pre-repeat-simplify", d_assertions
);
3241 if(options::repeatSimp()) {
3242 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-repeat-simplify" << endl
;
3243 Chat() << "re-simplifying assertions..." << endl
;
3244 ScopeCounter
depth(d_simplifyAssertionsDepth
);
3245 noConflict
&= simplifyAssertions();
3247 // Need to fix up assertion list to maintain invariants:
3248 // Let Sk be the set of Skolem variables introduced by ITE's. Let <_sk be the order in which these variables were introduced
3249 // during ite removal.
3250 // For each skolem variable sk, let iteExpr = iteMap(sk) be the ite expr mapped to by sk.
3252 // cache for expression traversal
3253 unordered_map
<Node
, bool, NodeHashFunction
> cache
;
3255 // First, find all skolems that appear in the substitution map - their associated iteExpr will need
3256 // to be moved to the main assertion set
3257 set
<TNode
> skolemSet
;
3258 SubstitutionMap::iterator pos
= top_level_substs
.begin();
3259 for (; pos
!= top_level_substs
.end(); ++pos
)
3261 collectSkolems((*pos
).first
, skolemSet
, cache
);
3262 collectSkolems((*pos
).second
, skolemSet
, cache
);
3265 // We need to ensure:
3266 // 1. iteExpr has the form (ite cond (sk = t) (sk = e))
3267 // 2. if some sk' in Sk appears in cond, t, or e, then sk' <_sk sk
3268 // If either of these is violated, we must add iteExpr as a proper assertion
3269 IteSkolemMap::iterator it
= getIteSkolemMap().begin();
3270 IteSkolemMap::iterator iend
= getIteSkolemMap().end();
3271 NodeBuilder
<> builder(kind::AND
);
3272 builder
<< d_assertions
[d_assertions
.getRealAssertionsEnd() - 1];
3273 vector
<TNode
> toErase
;
3274 for (; it
!= iend
; ++it
) {
3275 if (skolemSet
.find((*it
).first
) == skolemSet
.end()) {
3276 TNode iteExpr
= d_assertions
[(*it
).second
];
3277 if (iteExpr
.getKind() == kind::ITE
&&
3278 iteExpr
[1].getKind() == kind::EQUAL
&&
3279 iteExpr
[1][0] == (*it
).first
&&
3280 iteExpr
[2].getKind() == kind::EQUAL
&&
3281 iteExpr
[2][0] == (*it
).first
) {
3283 bool bad
= checkForBadSkolems(iteExpr
[0], (*it
).first
, cache
);
3284 bad
= bad
|| checkForBadSkolems(iteExpr
[1][1], (*it
).first
, cache
);
3285 bad
= bad
|| checkForBadSkolems(iteExpr
[2][1], (*it
).first
, cache
);
3291 // Move this iteExpr into the main assertions
3292 builder
<< d_assertions
[(*it
).second
];
3293 d_assertions
[(*it
).second
] = NodeManager::currentNM()->mkConst
<bool>(true);
3294 toErase
.push_back((*it
).first
);
3296 if(builder
.getNumChildren() > 1) {
3297 while (!toErase
.empty()) {
3298 getIteSkolemMap().erase(toErase
.back());
3301 d_assertions
[d_assertions
.getRealAssertionsEnd() - 1] =
3302 Rewriter::rewrite(Node(builder
));
3304 // TODO(b/1256): For some reason this is needed for some benchmarks, such as
3305 // QF_AUFBV/dwp_formulas/try5_small_difret_functions_dwp_tac.re_node_set_remove_at.il.dwp.smt2
3306 d_passes
["ite-removal"]->apply(&d_assertions
);
3307 d_passes
["apply-substs"]->apply(&d_assertions
);
3308 // Assert(iteRewriteAssertionsEnd == d_assertions.size());
3310 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-repeat-simplify" << endl
;
3312 dumpAssertions("post-repeat-simplify", d_assertions
);
3314 if (options::rewriteApplyToConst())
3316 d_passes
["apply-to-const"]->apply(&d_assertions
);
3319 // begin: INVARIANT to maintain: no reordering of assertions or
3320 // introducing new ones
3321 #ifdef CVC4_ASSERTIONS
3322 unsigned iteRewriteAssertionsEnd
= d_assertions
.size();
3325 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
3327 Debug("smt") << "SmtEnginePrivate::processAssertions() POST SIMPLIFICATION" << endl
;
3328 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
3330 d_passes
["theory-preprocess"]->apply(&d_assertions
);
3332 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
)
3334 d_passes
["bv-eager-atoms"]->apply(&d_assertions
);
3337 //notify theory engine new preprocessed assertions
3338 d_smt
.d_theoryEngine
->notifyPreprocessedAssertions( d_assertions
.ref() );
3340 // Push the formula to decision engine
3342 Chat() << "pushing to decision engine..." << endl
;
3343 Assert(iteRewriteAssertionsEnd
== d_assertions
.size());
3344 d_smt
.d_decisionEngine
->addAssertions(d_assertions
);
3347 // end: INVARIANT to maintain: no reordering of assertions or
3348 // introducing new ones
3350 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() end" << endl
;
3351 dumpAssertions("post-everything", d_assertions
);
3353 // if incremental, compute which variables are assigned
3354 if (options::incrementalSolving())
3356 d_preprocessingPassContext
->recordSymbolsInAssertions(d_assertions
.ref());
3359 // Push the formula to SAT
3361 Chat() << "converting to CNF..." << endl
;
3362 TimerStat::CodeTimer
codeTimer(d_smt
.d_stats
->d_cnfConversionTime
);
3363 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
3364 Chat() << "+ " << d_assertions
[i
] << std::endl
;
3365 d_smt
.d_propEngine
->assertFormula(d_assertions
[i
]);
3369 d_assertionsProcessed
= true;
3371 d_assertions
.clear();
3372 getIteSkolemMap().clear();
3375 void SmtEnginePrivate::addFormula(TNode n
, bool inUnsatCore
, bool inInput
)
3382 Trace("smt") << "SmtEnginePrivate::addFormula(" << n
<< "), inUnsatCore = " << inUnsatCore
<< ", inInput = " << inInput
<< endl
;
3384 // Give it to proof manager
3387 // n is an input assertion
3388 if (inUnsatCore
|| options::unsatCores() || options::dumpUnsatCores() || options::checkUnsatCores() || options::fewerPreprocessingHoles()) {
3390 ProofManager::currentPM()->addCoreAssertion(n
.toExpr());
3393 // n is the result of an unknown preprocessing step, add it to dependency map to null
3394 ProofManager::currentPM()->addDependence(n
, Node::null());
3396 // rewrite rules are by default in the unsat core because
3397 // they need to be applied until saturation
3398 if(options::unsatCores() &&
3399 n
.getKind() == kind::REWRITE_RULE
){
3400 ProofManager::currentPM()->addUnsatCore(n
.toExpr());
3404 // Add the normalized formula to the queue
3405 d_assertions
.push_back(n
);
3406 //d_assertions.push_back(Rewriter::rewrite(n));
3409 void SmtEngine::ensureBoolean(const Expr
& e
)
3411 Type type
= e
.getType(options::typeChecking());
3412 Type boolType
= d_exprManager
->booleanType();
3413 if(type
!= boolType
) {
3415 ss
<< "Expected " << boolType
<< "\n"
3416 << "The assertion : " << e
<< "\n"
3417 << "Its type : " << type
;
3418 throw TypeCheckingException(e
, ss
.str());
3422 Result
SmtEngine::checkSat(const Expr
& assumption
, bool inUnsatCore
)
3424 return checkSatisfiability(assumption
, inUnsatCore
, false);
3427 Result
SmtEngine::checkSat(const vector
<Expr
>& assumptions
, bool inUnsatCore
)
3429 return checkSatisfiability(assumptions
, inUnsatCore
, false);
3432 Result
SmtEngine::query(const Expr
& assumption
, bool inUnsatCore
)
3434 Assert(!assumption
.isNull());
3435 return checkSatisfiability(assumption
, inUnsatCore
, true);
3438 Result
SmtEngine::query(const vector
<Expr
>& assumptions
, bool inUnsatCore
)
3440 return checkSatisfiability(assumptions
, inUnsatCore
, true);
3443 Result
SmtEngine::checkSatisfiability(const Expr
& expr
,
3447 return checkSatisfiability(
3448 expr
.isNull() ? vector
<Expr
>() : vector
<Expr
>{expr
},
3453 Result
SmtEngine::checkSatisfiability(const vector
<Expr
>& assumptions
,
3459 SmtScope
smts(this);
3460 finalOptionsAreSet();
3463 Trace("smt") << "SmtEngine::" << (isQuery
? "query" : "checkSat") << "("
3464 << assumptions
<< ")" << endl
;
3466 if(d_queryMade
&& !options::incrementalSolving()) {
3467 throw ModalException("Cannot make multiple queries unless "
3468 "incremental solving is enabled "
3469 "(try --incremental)");
3472 // check to see if a postsolve() is pending
3473 if(d_needPostsolve
) {
3474 d_theoryEngine
->postsolve();
3475 d_needPostsolve
= false;
3477 // Note that a query has been made
3479 // reset global negation
3480 d_globalNegation
= false;
3482 bool didInternalPush
= false;
3484 setProblemExtended(true);
3488 size_t size
= assumptions
.size();
3491 /* Assume: not (BIGAND assumptions) */
3492 d_assumptions
.push_back(
3493 d_exprManager
->mkExpr(kind::AND
, assumptions
).notExpr());
3497 /* Assume: not expr */
3498 d_assumptions
.push_back(assumptions
[0].notExpr());
3503 /* Assume: BIGAND assumptions */
3504 d_assumptions
= assumptions
;
3507 if (!d_assumptions
.empty())
3510 didInternalPush
= true;
3513 Result
r(Result::SAT_UNKNOWN
, Result::UNKNOWN_REASON
);
3514 for (Expr e
: d_assumptions
)
3516 // Substitute out any abstract values in ex.
3517 e
= d_private
->substituteAbstractValues(Node::fromExpr(e
)).toExpr();
3518 Assert(e
.getExprManager() == d_exprManager
);
3519 // Ensure expr is type-checked at this point.
3522 /* Add assumption */
3523 if (d_assertionList
!= NULL
)
3525 d_assertionList
->push_back(e
);
3527 d_private
->addFormula(e
.getNode(), inUnsatCore
);
3530 r
= isQuery
? check().asValidityResult() : check().asSatisfiabilityResult();
3532 if ((options::solveRealAsInt() || options::solveIntAsBV() > 0)
3533 && r
.asSatisfiabilityResult().isSat() == Result::UNSAT
)
3535 r
= Result(Result::SAT_UNKNOWN
, Result::UNKNOWN_REASON
);
3537 // flipped if we did a global negation
3538 if (d_globalNegation
)
3540 Trace("smt") << "SmtEngine::process global negate " << r
<< std::endl
;
3541 if (r
.asSatisfiabilityResult().isSat() == Result::UNSAT
)
3543 r
= Result(Result::SAT
);
3545 else if (r
.asSatisfiabilityResult().isSat() == Result::SAT
)
3547 // only if satisfaction complete
3548 if (d_logic
.isPure(THEORY_ARITH
) || d_logic
.isPure(THEORY_BV
))
3550 r
= Result(Result::UNSAT
);
3554 r
= Result(Result::SAT_UNKNOWN
, Result::UNKNOWN_REASON
);
3557 Trace("smt") << "SmtEngine::global negate returned " << r
<< std::endl
;
3560 d_needPostsolve
= true;
3562 // Dump the query if requested
3563 if (Dump
.isOn("benchmark"))
3565 size_t size
= assumptions
.size();
3566 // the expr already got dumped out if assertion-dumping is on
3567 if (isQuery
&& size
== 1)
3569 Dump("benchmark") << QueryCommand(assumptions
[0]);
3573 Dump("benchmark") << CheckSatCommand();
3577 Dump("benchmark") << CheckSatAssumingCommand(d_assumptions
);
3581 d_propEngine
->resetTrail();
3584 if (didInternalPush
)
3589 // Remember the status
3592 setProblemExtended(false);
3594 Trace("smt") << "SmtEngine::" << (isQuery
? "query" : "checkSat") << "("
3595 << assumptions
<< ") => " << r
<< endl
;
3597 // Check that SAT results generate a model correctly.
3598 if(options::checkModels()) {
3599 // TODO (#1693) check model when unknown result?
3600 if (r
.asSatisfiabilityResult().isSat() == Result::SAT
)
3605 // Check that UNSAT results generate a proof correctly.
3606 if(options::checkProofs()) {
3607 if(r
.asSatisfiabilityResult().isSat() == Result::UNSAT
) {
3608 TimerStat::CodeTimer
checkProofTimer(d_stats
->d_checkProofTime
);
3612 // Check that UNSAT results generate an unsat core correctly.
3613 if(options::checkUnsatCores()) {
3614 if(r
.asSatisfiabilityResult().isSat() == Result::UNSAT
) {
3615 TimerStat::CodeTimer
checkUnsatCoreTimer(d_stats
->d_checkUnsatCoreTime
);
3619 // Check that synthesis solutions satisfy the conjecture
3620 if (options::checkSynthSol()
3621 && r
.asSatisfiabilityResult().isSat() == Result::UNSAT
)
3623 checkSynthSolution();
3627 } catch (UnsafeInterruptException
& e
) {
3628 AlwaysAssert(d_private
->getResourceManager()->out());
3629 Result::UnknownExplanation why
= d_private
->getResourceManager()->outOfResources() ?
3630 Result::RESOURCEOUT
: Result::TIMEOUT
;
3631 return Result(Result::SAT_UNKNOWN
, why
, d_filename
);
3635 vector
<Expr
> SmtEngine::getUnsatAssumptions(void)
3637 Trace("smt") << "SMT getUnsatAssumptions()" << endl
;
3638 SmtScope
smts(this);
3639 if (!options::unsatAssumptions())
3641 throw ModalException(
3642 "Cannot get unsat assumptions when produce-unsat-assumptions option "
3645 if (d_status
.isNull()
3646 || d_status
.asSatisfiabilityResult() != Result::UNSAT
3647 || d_problemExtended
)
3649 throw RecoverableModalException(
3650 "Cannot get unsat assumptions unless immediately preceded by "
3651 "UNSAT/VALID response.");
3653 finalOptionsAreSet();
3654 if (Dump
.isOn("benchmark"))
3656 Dump("benchmark") << GetUnsatAssumptionsCommand();
3658 UnsatCore core
= getUnsatCoreInternal();
3660 for (const Expr
& e
: d_assumptions
)
3662 if (find(core
.begin(), core
.end(), e
) != core
.end()) { res
.push_back(e
); }
3667 Result
SmtEngine::checkSynth(const Expr
& e
)
3669 SmtScope
smts(this);
3670 Trace("smt") << "Check synth: " << e
<< std::endl
;
3671 Trace("smt-synth") << "Check synthesis conjecture: " << e
<< std::endl
;
3672 return checkSatisfiability(e
, true, false);
3675 Result
SmtEngine::assertFormula(const Expr
& ex
, bool inUnsatCore
)
3677 Assert(ex
.getExprManager() == d_exprManager
);
3678 SmtScope
smts(this);
3679 finalOptionsAreSet();
3682 Trace("smt") << "SmtEngine::assertFormula(" << ex
<< ")" << endl
;
3684 if (Dump
.isOn("raw-benchmark")) {
3685 Dump("raw-benchmark") << AssertCommand(ex
);
3688 // Substitute out any abstract values in ex
3689 Expr e
= d_private
->substituteAbstractValues(Node::fromExpr(ex
)).toExpr();
3692 if(d_assertionList
!= NULL
) {
3693 d_assertionList
->push_back(e
);
3695 d_private
->addFormula(e
.getNode(), inUnsatCore
);
3696 return quickCheck().asValidityResult();
3697 }/* SmtEngine::assertFormula() */
3699 Node
SmtEngine::postprocess(TNode node
, TypeNode expectedType
) const {
3703 Expr
SmtEngine::simplify(const Expr
& ex
)
3705 Assert(ex
.getExprManager() == d_exprManager
);
3706 SmtScope
smts(this);
3707 finalOptionsAreSet();
3709 Trace("smt") << "SMT simplify(" << ex
<< ")" << endl
;
3711 if(Dump
.isOn("benchmark")) {
3712 Dump("benchmark") << SimplifyCommand(ex
);
3715 Expr e
= d_private
->substituteAbstractValues(Node::fromExpr(ex
)).toExpr();
3716 if( options::typeChecking() ) {
3717 e
.getType(true); // ensure expr is type-checked at this point
3720 // Make sure all preprocessing is done
3721 d_private
->processAssertions();
3722 Node n
= d_private
->simplify(Node::fromExpr(e
));
3723 n
= postprocess(n
, TypeNode::fromType(e
.getType()));
3727 Expr
SmtEngine::expandDefinitions(const Expr
& ex
)
3729 d_private
->spendResource(options::preprocessStep());
3731 Assert(ex
.getExprManager() == d_exprManager
);
3732 SmtScope
smts(this);
3733 finalOptionsAreSet();
3735 Trace("smt") << "SMT expandDefinitions(" << ex
<< ")" << endl
;
3737 // Substitute out any abstract values in ex.
3738 Expr e
= d_private
->substituteAbstractValues(Node::fromExpr(ex
)).toExpr();
3739 if(options::typeChecking()) {
3740 // Ensure expr is type-checked at this point.
3743 if(Dump
.isOn("benchmark")) {
3744 Dump("benchmark") << ExpandDefinitionsCommand(e
);
3746 unordered_map
<Node
, Node
, NodeHashFunction
> cache
;
3747 Node n
= d_private
->expandDefinitions(Node::fromExpr(e
), cache
, /* expandOnly = */ true);
3748 n
= postprocess(n
, TypeNode::fromType(e
.getType()));
3753 // TODO(#1108): Simplify the error reporting of this method.
3754 Expr
SmtEngine::getValue(const Expr
& ex
) const
3756 Assert(ex
.getExprManager() == d_exprManager
);
3757 SmtScope
smts(this);
3759 Trace("smt") << "SMT getValue(" << ex
<< ")" << endl
;
3760 if(Dump
.isOn("benchmark")) {
3761 Dump("benchmark") << GetValueCommand(ex
);
3764 if(!options::produceModels()) {
3766 "Cannot get value when produce-models options is off.";
3767 throw ModalException(msg
);
3769 if(d_status
.isNull() ||
3770 d_status
.asSatisfiabilityResult() == Result::UNSAT
||
3771 d_problemExtended
) {
3773 "Cannot get value unless immediately preceded by SAT/INVALID or UNKNOWN response.";
3774 throw RecoverableModalException(msg
);
3777 // Substitute out any abstract values in ex.
3778 Expr e
= d_private
->substituteAbstractValues(Node::fromExpr(ex
)).toExpr();
3780 // Ensure expr is type-checked at this point.
3781 e
.getType(options::typeChecking());
3783 // do not need to apply preprocessing substitutions (should be recorded
3784 // in model already)
3786 Node n
= Node::fromExpr(e
);
3787 Trace("smt") << "--- getting value of " << n
<< endl
;
3788 TypeNode expectedType
= n
.getType();
3790 // Expand, then normalize
3791 unordered_map
<Node
, Node
, NodeHashFunction
> cache
;
3792 n
= d_private
->expandDefinitions(n
, cache
);
3793 // There are two ways model values for terms are computed (for historical
3794 // reasons). One way is that used in check-model; the other is that
3795 // used by the Model classes. It's not clear to me exactly how these
3796 // two are different, but they need to be unified. This ugly hack here
3797 // is to fix bug 554 until we can revamp boolean-terms and models [MGD]
3800 if(!n
.getType().isFunction()) {
3801 n
= Rewriter::rewrite(n
);
3804 Trace("smt") << "--- getting value of " << n
<< endl
;
3805 TheoryModel
* m
= d_theoryEngine
->getModel();
3808 resultNode
= m
->getValue(n
);
3810 Trace("smt") << "--- got value " << n
<< " = " << resultNode
<< endl
;
3811 resultNode
= postprocess(resultNode
, expectedType
);
3812 Trace("smt") << "--- model-post returned " << resultNode
<< endl
;
3813 Trace("smt") << "--- model-post returned " << resultNode
.getType() << endl
;
3814 Trace("smt") << "--- model-post expected " << expectedType
<< endl
;
3816 // type-check the result we got
3817 Assert(resultNode
.isNull() || resultNode
.getType().isSubtypeOf(expectedType
),
3818 "Run with -t smt for details.");
3820 // ensure it's a constant
3821 Assert(resultNode
.getKind() == kind::LAMBDA
|| resultNode
.isConst());
3823 if(options::abstractValues() && resultNode
.getType().isArray()) {
3824 resultNode
= d_private
->mkAbstractValue(resultNode
);
3825 Trace("smt") << "--- abstract value >> " << resultNode
<< endl
;
3828 return resultNode
.toExpr();
3831 bool SmtEngine::addToAssignment(const Expr
& ex
) {
3832 SmtScope
smts(this);
3833 finalOptionsAreSet();
3835 // Substitute out any abstract values in ex
3836 Expr e
= d_private
->substituteAbstractValues(Node::fromExpr(ex
)).toExpr();
3837 Type type
= e
.getType(options::typeChecking());
3839 PrettyCheckArgument(
3840 type
.isBoolean(), e
,
3841 "expected Boolean-typed variable or function application "
3842 "in addToAssignment()" );
3843 Node n
= e
.getNode();
3844 // must be an APPLY of a zero-ary defined function, or a variable
3845 PrettyCheckArgument(
3846 ( ( n
.getKind() == kind::APPLY
&&
3847 ( d_definedFunctions
->find(n
.getOperator()) !=
3848 d_definedFunctions
->end() ) &&
3849 n
.getNumChildren() == 0 ) ||
3851 "expected variable or defined-function application "
3852 "in addToAssignment(),\ngot %s", e
.toString().c_str() );
3853 if(!options::produceAssignments()) {
3856 if(d_assignments
== NULL
) {
3857 d_assignments
= new(true) AssignmentSet(d_context
);
3859 d_assignments
->insert(n
);
3864 // TODO(#1108): Simplify the error reporting of this method.
3865 vector
<pair
<Expr
, Expr
>> SmtEngine::getAssignment()
3867 Trace("smt") << "SMT getAssignment()" << endl
;
3868 SmtScope
smts(this);
3869 finalOptionsAreSet();
3870 if(Dump
.isOn("benchmark")) {
3871 Dump("benchmark") << GetAssignmentCommand();
3873 if(!options::produceAssignments()) {
3875 "Cannot get the current assignment when "
3876 "produce-assignments option is off.";
3877 throw ModalException(msg
);
3879 if(d_status
.isNull() ||
3880 d_status
.asSatisfiabilityResult() == Result::UNSAT
||
3881 d_problemExtended
) {
3883 "Cannot get the current assignment unless immediately "
3884 "preceded by SAT/INVALID or UNKNOWN response.";
3885 throw RecoverableModalException(msg
);
3888 vector
<pair
<Expr
,Expr
>> res
;
3889 if (d_assignments
!= nullptr)
3891 TypeNode boolType
= d_nodeManager
->booleanType();
3892 TheoryModel
* m
= d_theoryEngine
->getModel();
3893 for (AssignmentSet::key_iterator i
= d_assignments
->key_begin(),
3894 iend
= d_assignments
->key_end();
3899 Assert(as
.getType() == boolType
);
3901 Trace("smt") << "--- getting value of " << as
<< endl
;
3903 // Expand, then normalize
3904 unordered_map
<Node
, Node
, NodeHashFunction
> cache
;
3905 Node n
= d_private
->expandDefinitions(as
, cache
);
3906 n
= Rewriter::rewrite(n
);
3908 Trace("smt") << "--- getting value of " << n
<< endl
;
3912 resultNode
= m
->getValue(n
);
3915 // type-check the result we got
3916 Assert(resultNode
.isNull() || resultNode
.getType() == boolType
);
3918 // ensure it's a constant
3919 Assert(resultNode
.isConst());
3921 Assert(as
.getKind() == kind::APPLY
|| as
.isVar());
3922 Assert(as
.getKind() != kind::APPLY
|| as
.getNumChildren() == 0);
3923 res
.emplace_back(as
.toExpr(), resultNode
.toExpr());
3929 void SmtEngine::addToModelCommandAndDump(const Command
& c
, uint32_t flags
, bool userVisible
, const char* dumpTag
) {
3930 Trace("smt") << "SMT addToModelCommandAndDump(" << c
<< ")" << endl
;
3931 SmtScope
smts(this);
3932 // If we aren't yet fully inited, the user might still turn on
3933 // produce-models. So let's keep any commands around just in
3934 // case. This is useful in two cases: (1) SMT-LIBv1 auto-declares
3935 // sort "U" in QF_UF before setLogic() is run and we still want to
3936 // support finding card(U) with --finite-model-find, and (2) to
3937 // decouple SmtEngine and ExprManager if the user does a few
3938 // ExprManager::mkSort() before SmtEngine::setOption("produce-models")
3939 // and expects to find their cardinalities in the model.
3940 if(/* userVisible && */
3941 (!d_fullyInited
|| options::produceModels()) &&
3942 (flags
& ExprManager::VAR_FLAG_DEFINED
) == 0) {
3944 if(flags
& ExprManager::VAR_FLAG_GLOBAL
) {
3945 d_modelGlobalCommands
.push_back(c
.clone());
3947 d_modelCommands
->push_back(c
.clone());
3950 if(Dump
.isOn(dumpTag
)) {
3954 d_dumpCommands
.push_back(c
.clone());
3959 // TODO(#1108): Simplify the error reporting of this method.
3960 Model
* SmtEngine::getModel() {
3961 Trace("smt") << "SMT getModel()" << endl
;
3962 SmtScope
smts(this);
3964 finalOptionsAreSet();
3966 if(Dump
.isOn("benchmark")) {
3967 Dump("benchmark") << GetModelCommand();
3970 if (!options::assignFunctionValues())
3973 "Cannot get the model when --assign-function-values is false.";
3974 throw RecoverableModalException(msg
);
3977 if(d_status
.isNull() ||
3978 d_status
.asSatisfiabilityResult() == Result::UNSAT
||
3979 d_problemExtended
) {
3981 "Cannot get the current model unless immediately "
3982 "preceded by SAT/INVALID or UNKNOWN response.";
3983 throw RecoverableModalException(msg
);
3985 if(!options::produceModels()) {
3987 "Cannot get model when produce-models options is off.";
3988 throw ModalException(msg
);
3990 TheoryModel
* m
= d_theoryEngine
->getModel();
3992 if (options::produceModelCores())
3994 // If we enabled model cores, we compute a model core for m based on our
3995 // assertions using the model core builder utility
3996 std::vector
<Expr
> easserts
= getAssertions();
3997 ModelCoreBuilder::setModelCore(easserts
, m
);
3999 m
->d_inputName
= d_filename
;
4003 std::pair
<Expr
, Expr
> SmtEngine::getSepHeapAndNilExpr(void)
4005 if (!d_logic
.isTheoryEnabled(THEORY_SEP
))
4008 "Cannot obtain separation logic expressions if not using the "
4009 "separation logic theory.";
4010 throw RecoverableModalException(msg
);
4012 NodeManagerScope
nms(d_nodeManager
);
4015 Model
* m
= getModel();
4016 if (m
->getHeapModel(heap
, nil
))
4018 return std::make_pair(heap
, nil
);
4021 "SmtEngine::getSepHeapAndNilExpr(): failed to obtain heap/nil "
4022 "expressions from theory model.");
4025 Expr
SmtEngine::getSepHeapExpr() { return getSepHeapAndNilExpr().first
; }
4027 Expr
SmtEngine::getSepNilExpr() { return getSepHeapAndNilExpr().second
; }
4029 UnsatCore
SmtEngine::getUnsatCoreInternal()
4032 if (!options::unsatCores())
4034 throw ModalException(
4035 "Cannot get an unsat core when produce-unsat-cores option is off.");
4037 if (d_status
.isNull() || d_status
.asSatisfiabilityResult() != Result::UNSAT
4038 || d_problemExtended
)
4040 throw RecoverableModalException(
4041 "Cannot get an unsat core unless immediately preceded by UNSAT/VALID "
4045 d_proofManager
->traceUnsatCore(); // just to trigger core creation
4046 return UnsatCore(this, d_proofManager
->extractUnsatCore());
4047 #else /* IS_PROOFS_BUILD */
4048 throw ModalException(
4049 "This build of CVC4 doesn't have proof support (required for unsat "
4051 #endif /* IS_PROOFS_BUILD */
4054 void SmtEngine::checkUnsatCore() {
4055 Assert(options::unsatCores(), "cannot check unsat core if unsat cores are turned off");
4057 Notice() << "SmtEngine::checkUnsatCore(): generating unsat core" << endl
;
4058 UnsatCore core
= getUnsatCore();
4060 SmtEngine
coreChecker(d_exprManager
);
4061 coreChecker
.setLogic(getLogicInfo());
4064 std::vector
<Command
*>::const_iterator itg
= d_defineCommands
.begin();
4065 for (; itg
!= d_defineCommands
.end(); ++itg
) {
4066 (*itg
)->invoke(&coreChecker
);
4070 Notice() << "SmtEngine::checkUnsatCore(): pushing core assertions (size == " << core
.size() << ")" << endl
;
4071 for(UnsatCore::iterator i
= core
.begin(); i
!= core
.end(); ++i
) {
4072 Notice() << "SmtEngine::checkUnsatCore(): pushing core member " << *i
<< endl
;
4073 coreChecker
.assertFormula(*i
);
4075 const bool checkUnsatCores
= options::checkUnsatCores();
4078 options::checkUnsatCores
.set(false);
4079 options::checkProofs
.set(false);
4080 r
= coreChecker
.checkSat();
4082 options::checkUnsatCores
.set(checkUnsatCores
);
4085 Notice() << "SmtEngine::checkUnsatCore(): result is " << r
<< endl
;
4086 if(r
.asSatisfiabilityResult().isUnknown()) {
4087 InternalError("SmtEngine::checkUnsatCore(): could not check core result unknown.");
4090 if(r
.asSatisfiabilityResult().isSat()) {
4091 InternalError("SmtEngine::checkUnsatCore(): produced core was satisfiable.");
4095 void SmtEngine::checkModel(bool hardFailure
) {
4096 // --check-model implies --produce-assertions, which enables the
4097 // assertion list, so we should be ok.
4098 Assert(d_assertionList
!= NULL
, "don't have an assertion list to check in SmtEngine::checkModel()");
4100 TimerStat::CodeTimer
checkModelTimer(d_stats
->d_checkModelTime
);
4102 // Throughout, we use Notice() to give diagnostic output.
4104 // If this function is running, the user gave --check-model (or equivalent),
4105 // and if Notice() is on, the user gave --verbose (or equivalent).
4107 Notice() << "SmtEngine::checkModel(): generating model" << endl
;
4108 TheoryModel
* m
= d_theoryEngine
->getModel();
4110 // check-model is not guaranteed to succeed if approximate values were used
4111 if (m
->hasApproximations())
4114 << "WARNING: running check-model on a model with approximate values..."
4118 // Check individual theory assertions
4119 d_theoryEngine
->checkTheoryAssertionsWithModel(hardFailure
);
4124 // We have a "fake context" for the substitution map (we don't need it
4125 // to be context-dependent)
4126 context::Context fakeContext
;
4127 SubstitutionMap
substitutions(&fakeContext
, /* substituteUnderQuantifiers = */ false);
4129 for(size_t k
= 0; k
< m
->getNumCommands(); ++k
) {
4130 const DeclareFunctionCommand
* c
= dynamic_cast<const DeclareFunctionCommand
*>(m
->getCommand(k
));
4131 Notice() << "SmtEngine::checkModel(): model command " << k
<< " : " << m
->getCommand(k
) << endl
;
4133 // we don't care about DECLARE-DATATYPES, DECLARE-SORT, ...
4134 Notice() << "SmtEngine::checkModel(): skipping..." << endl
;
4136 // We have a DECLARE-FUN:
4138 // We'll first do some checks, then add to our substitution map
4139 // the mapping: function symbol |-> value
4141 Expr func
= c
->getFunction();
4142 Node val
= m
->getValue(func
);
4144 Notice() << "SmtEngine::checkModel(): adding substitution: " << func
<< " |-> " << val
<< endl
;
4146 // (1) if the value is a lambda, ensure the lambda doesn't contain the
4147 // function symbol (since then the definition is recursive)
4148 if (val
.getKind() == kind::LAMBDA
) {
4149 // first apply the model substitutions we have so far
4150 Debug("boolean-terms") << "applying subses to " << val
[1] << endl
;
4151 Node n
= substitutions
.apply(val
[1]);
4152 Debug("boolean-terms") << "++ got " << n
<< endl
;
4153 // now check if n contains func by doing a substitution
4154 // [func->func2] and checking equality of the Nodes.
4155 // (this just a way to check if func is in n.)
4156 SubstitutionMap
subs(&fakeContext
);
4157 Node func2
= NodeManager::currentNM()->mkSkolem("", TypeNode::fromType(func
.getType()), "", NodeManager::SKOLEM_NO_NOTIFY
);
4158 subs
.addSubstitution(func
, func2
);
4159 if(subs
.apply(n
) != n
) {
4160 Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE DEFINED IN TERMS OF ITSELF ***" << endl
;
4162 ss
<< "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
4163 << "considering model value for " << func
<< endl
4164 << "body of lambda is: " << val
<< endl
;
4166 ss
<< "body substitutes to: " << n
<< endl
;
4168 ss
<< "so " << func
<< " is defined in terms of itself." << endl
4169 << "Run with `--check-models -v' for additional diagnostics.";
4170 InternalError(ss
.str());
4174 // (2) check that the value is actually a value
4175 else if (!val
.isConst()) {
4176 Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE NOT A CONSTANT ***" << endl
;
4178 ss
<< "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
4179 << "model value for " << func
<< endl
4180 << " is " << val
<< endl
4181 << "and that is not a constant (.isConst() == false)." << endl
4182 << "Run with `--check-models -v' for additional diagnostics.";
4183 InternalError(ss
.str());
4186 // (3) check that it's the correct (sub)type
4187 // This was intended to be a more general check, but for now we can't do that because
4188 // e.g. "1" is an INT, which isn't a subrange type [1..10] (etc.).
4189 else if(func
.getType().isInteger() && !val
.getType().isInteger()) {
4190 Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE NOT CORRECT TYPE ***" << endl
;
4192 ss
<< "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
4193 << "model value for " << func
<< endl
4194 << " is " << val
<< endl
4195 << "value type is " << val
.getType() << endl
4196 << "should be of type " << func
.getType() << endl
4197 << "Run with `--check-models -v' for additional diagnostics.";
4198 InternalError(ss
.str());
4201 // (4) checks complete, add the substitution
4202 Debug("boolean-terms") << "cm: adding subs " << func
<< " :=> " << val
<< endl
;
4203 substitutions
.addSubstitution(func
, val
);
4207 // Now go through all our user assertions checking if they're satisfied.
4208 for(AssertionList::const_iterator i
= d_assertionList
->begin(); i
!= d_assertionList
->end(); ++i
) {
4209 Notice() << "SmtEngine::checkModel(): checking assertion " << *i
<< endl
;
4210 Node n
= Node::fromExpr(*i
);
4212 // Apply any define-funs from the problem.
4214 unordered_map
<Node
, Node
, NodeHashFunction
> cache
;
4215 n
= d_private
->expandDefinitions(n
, cache
);
4217 Notice() << "SmtEngine::checkModel(): -- expands to " << n
<< endl
;
4219 // Apply our model value substitutions.
4220 Debug("boolean-terms") << "applying subses to " << n
<< endl
;
4221 n
= substitutions
.apply(n
);
4222 Debug("boolean-terms") << "++ got " << n
<< endl
;
4223 Notice() << "SmtEngine::checkModel(): -- substitutes to " << n
<< endl
;
4225 if( n
.getKind() != kind::REWRITE_RULE
){
4226 // In case it's a quantifier (or contains one), look up its value before
4227 // simplifying, or the quantifier might be irreparably altered.
4229 Notice() << "SmtEngine::checkModel(): -- get value : " << n
<< std::endl
;
4231 // Note this "skip" is done here, rather than above. This is
4232 // because (1) the quantifier could in principle simplify to false,
4233 // which should be reported, and (2) checking for the quantifier
4234 // above, before simplification, doesn't catch buried quantifiers
4235 // anyway (those not at the top-level).
4236 Notice() << "SmtEngine::checkModel(): -- skipping rewrite-rules assertion"
4241 // Simplify the result.
4242 n
= d_private
->simplify(n
);
4243 Notice() << "SmtEngine::checkModel(): -- simplifies to " << n
<< endl
;
4245 // Replace the already-known ITEs (this is important for ground ITEs under quantifiers).
4246 n
= d_private
->d_iteRemover
.replace(n
);
4247 Notice() << "SmtEngine::checkModel(): -- ite replacement gives " << n
<< endl
;
4249 // Apply our model value substitutions (again), as things may have been simplified.
4250 Debug("boolean-terms") << "applying subses to " << n
<< endl
;
4251 n
= substitutions
.apply(n
);
4252 Debug("boolean-terms") << "++ got " << n
<< endl
;
4253 Notice() << "SmtEngine::checkModel(): -- re-substitutes to " << n
<< endl
;
4255 // As a last-ditch effort, ask model to simplify it.
4256 // Presently, this is only an issue for quantifiers, which can have a value
4257 // but don't show up in our substitution map above.
4259 Notice() << "SmtEngine::checkModel(): -- model-substitutes to " << n
<< endl
;
4261 if( d_logic
.isQuantified() ){
4262 // AJR: since quantified formulas are not checkable, we assign them to true/false based on the satisfying assignment.
4263 // however, quantified formulas can be modified during preprocess, so they may not correspond to those in the satisfying assignment.
4264 // hence we use a relaxed version of check model here.
4265 // this is necessary until preprocessing passes explicitly record how they rewrite quantified formulas
4266 if( hardFailure
&& !n
.isConst() && n
.getKind() != kind::LAMBDA
){
4267 Notice() << "SmtEngine::checkModel(): -- relax check model wrt quantified formulas..." << endl
;
4268 AlwaysAssert( quantifiers::QuantifiersRewriter::containsQuantifiers( n
) );
4269 Warning() << "Warning : SmtEngine::checkModel(): cannot check simplified assertion : " << n
<< endl
;
4273 AlwaysAssert(!hardFailure
|| n
.isConst() || n
.getKind() == kind::LAMBDA
);
4275 // The result should be == true.
4276 if(n
!= NodeManager::currentNM()->mkConst(true)) {
4277 Notice() << "SmtEngine::checkModel(): *** PROBLEM: EXPECTED `TRUE' ***"
4280 ss
<< "SmtEngine::checkModel(): "
4281 << "ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
4282 << "assertion: " << *i
<< endl
4283 << "simplifies to: " << n
<< endl
4284 << "expected `true'." << endl
4285 << "Run with `--check-models -v' for additional diagnostics.";
4287 InternalError(ss
.str());
4289 Warning() << ss
.str() << endl
;
4293 Notice() << "SmtEngine::checkModel(): all assertions checked out OK !" << endl
;
4296 void SmtEngine::checkSynthSolution()
4298 NodeManager
* nm
= NodeManager::currentNM();
4299 Notice() << "SmtEngine::checkSynthSolution(): checking synthesis solution" << endl
;
4300 map
<Node
, Node
> sol_map
;
4301 /* Get solutions and build auxiliary vectors for substituting */
4302 d_theoryEngine
->getSynthSolutions(sol_map
);
4303 if (sol_map
.empty())
4305 Trace("check-synth-sol") << "No solution to check!\n";
4308 Trace("check-synth-sol") << "Got solution map:\n";
4309 std::vector
<Node
> function_vars
, function_sols
;
4310 for (const auto& pair
: sol_map
)
4312 Trace("check-synth-sol") << pair
.first
<< " --> " << pair
.second
<< "\n";
4313 function_vars
.push_back(pair
.first
);
4314 function_sols
.push_back(pair
.second
);
4316 Trace("check-synth-sol") << "Starting new SMT Engine\n";
4317 /* Start new SMT engine to check solutions */
4318 SmtEngine
solChecker(d_exprManager
);
4319 solChecker
.setLogic(getLogicInfo());
4320 setOption("check-synth-sol", SExpr("false"));
4322 Trace("check-synth-sol") << "Retrieving assertions\n";
4323 // Build conjecture from original assertions
4324 if (d_assertionList
== NULL
)
4326 Trace("check-synth-sol") << "No assertions to check\n";
4329 for (AssertionList::const_iterator i
= d_assertionList
->begin();
4330 i
!= d_assertionList
->end();
4333 Notice() << "SmtEngine::checkSynthSolution(): checking assertion " << *i
<< endl
;
4334 Trace("check-synth-sol") << "Retrieving assertion " << *i
<< "\n";
4335 Node conj
= Node::fromExpr(*i
);
4336 // Apply any define-funs from the problem.
4338 unordered_map
<Node
, Node
, NodeHashFunction
> cache
;
4339 conj
= d_private
->expandDefinitions(conj
, cache
);
4341 Notice() << "SmtEngine::checkSynthSolution(): -- expands to " << conj
<< endl
;
4342 Trace("check-synth-sol") << "Expanded assertion " << conj
<< "\n";
4343 if (conj
.getKind() != kind::FORALL
)
4345 Trace("check-synth-sol") << "Not a checkable assertion.\n";
4349 // Apply solution map to conjecture body
4351 /* Whether property is quantifier free */
4352 if (conj
[1].getKind() != kind::EXISTS
)
4354 conjBody
= conj
[1].substitute(function_vars
.begin(),
4355 function_vars
.end(),
4356 function_sols
.begin(),
4357 function_sols
.end());
4361 conjBody
= conj
[1][1].substitute(function_vars
.begin(),
4362 function_vars
.end(),
4363 function_sols
.begin(),
4364 function_sols
.end());
4366 /* Skolemize property */
4367 std::vector
<Node
> vars
, skos
;
4368 for (unsigned j
= 0, size
= conj
[1][0].getNumChildren(); j
< size
; ++j
)
4370 vars
.push_back(conj
[1][0][j
]);
4371 std::stringstream ss
;
4373 skos
.push_back(nm
->mkSkolem(ss
.str(), conj
[1][0][j
].getType()));
4374 Trace("check-synth-sol") << "\tSkolemizing " << conj
[1][0][j
] << " to "
4375 << skos
.back() << "\n";
4377 conjBody
= conjBody
.substitute(
4378 vars
.begin(), vars
.end(), skos
.begin(), skos
.end());
4380 Notice() << "SmtEngine::checkSynthSolution(): -- body substitutes to "
4381 << conjBody
<< endl
;
4382 Trace("check-synth-sol") << "Substituted body of assertion to " << conjBody
4384 solChecker
.assertFormula(conjBody
.toExpr());
4385 Result r
= solChecker
.checkSat();
4386 Notice() << "SmtEngine::checkSynthSolution(): result is " << r
<< endl
;
4387 Trace("check-synth-sol") << "Satsifiability check: " << r
<< "\n";
4388 if (r
.asSatisfiabilityResult().isUnknown())
4391 "SmtEngine::checkSynthSolution(): could not check solution, result "
4394 else if (r
.asSatisfiabilityResult().isSat())
4397 "SmtEngine::checkSynthSolution(): produced solution leads to "
4398 "satisfiable negated conjecture.");
4400 solChecker
.resetAssertions();
4404 // TODO(#1108): Simplify the error reporting of this method.
4405 UnsatCore
SmtEngine::getUnsatCore() {
4406 Trace("smt") << "SMT getUnsatCore()" << endl
;
4407 SmtScope
smts(this);
4408 finalOptionsAreSet();
4409 if(Dump
.isOn("benchmark")) {
4410 Dump("benchmark") << GetUnsatCoreCommand();
4412 return getUnsatCoreInternal();
4415 // TODO(#1108): Simplify the error reporting of this method.
4416 const Proof
& SmtEngine::getProof()
4418 Trace("smt") << "SMT getProof()" << endl
;
4419 SmtScope
smts(this);
4420 finalOptionsAreSet();
4421 if(Dump
.isOn("benchmark")) {
4422 Dump("benchmark") << GetProofCommand();
4425 if(!options::proof()) {
4426 throw ModalException("Cannot get a proof when produce-proofs option is off.");
4428 if(d_status
.isNull() ||
4429 d_status
.asSatisfiabilityResult() != Result::UNSAT
||
4430 d_problemExtended
) {
4431 throw RecoverableModalException(
4432 "Cannot get a proof unless immediately preceded by UNSAT/VALID "
4436 return ProofManager::getProof(this);
4437 #else /* IS_PROOFS_BUILD */
4438 throw ModalException("This build of CVC4 doesn't have proof support.");
4439 #endif /* IS_PROOFS_BUILD */
4442 void SmtEngine::printInstantiations( std::ostream
& out
) {
4443 SmtScope
smts(this);
4444 if( options::instFormatMode()==INST_FORMAT_MODE_SZS
){
4445 out
<< "% SZS output start Proof for " << d_filename
.c_str() << std::endl
;
4447 if( d_theoryEngine
){
4448 d_theoryEngine
->printInstantiations( out
);
4452 if( options::instFormatMode()==INST_FORMAT_MODE_SZS
){
4453 out
<< "% SZS output end Proof for " << d_filename
.c_str() << std::endl
;
4457 void SmtEngine::printSynthSolution( std::ostream
& out
) {
4458 SmtScope
smts(this);
4459 if( d_theoryEngine
){
4460 d_theoryEngine
->printSynthSolution( out
);
4466 void SmtEngine::getSynthSolutions(std::map
<Expr
, Expr
>& sol_map
)
4468 SmtScope
smts(this);
4469 map
<Node
, Node
> sol_mapn
;
4470 Assert(d_theoryEngine
!= nullptr);
4471 d_theoryEngine
->getSynthSolutions(sol_mapn
);
4472 for (std::pair
<const Node
, Node
>& s
: sol_mapn
)
4474 sol_map
[s
.first
.toExpr()] = s
.second
.toExpr();
4478 Expr
SmtEngine::doQuantifierElimination(const Expr
& e
, bool doFull
, bool strict
)
4480 SmtScope
smts(this);
4481 if(!d_logic
.isPure(THEORY_ARITH
) && strict
){
4482 Warning() << "Unexpected logic for quantifier elimination " << d_logic
<< endl
;
4484 Trace("smt-qe") << "Do quantifier elimination " << e
<< std::endl
;
4485 Node n_e
= Node::fromExpr( e
);
4486 if (n_e
.getKind() != kind::EXISTS
&& n_e
.getKind() != kind::FORALL
)
4488 throw ModalException(
4489 "Expecting a quantified formula as argument to get-qe.");
4491 //tag the quantified formula with the quant-elim attribute
4492 TypeNode t
= NodeManager::currentNM()->booleanType();
4493 Node n_attr
= NodeManager::currentNM()->mkSkolem("qe", t
, "Auxiliary variable for qe attr.");
4494 std::vector
< Node
> node_values
;
4495 d_theoryEngine
->setUserAttribute( doFull
? "quant-elim" : "quant-elim-partial", n_attr
, node_values
, "");
4496 n_attr
= NodeManager::currentNM()->mkNode(kind::INST_ATTRIBUTE
, n_attr
);
4497 n_attr
= NodeManager::currentNM()->mkNode(kind::INST_PATTERN_LIST
, n_attr
);
4498 std::vector
< Node
> e_children
;
4499 e_children
.push_back( n_e
[0] );
4500 e_children
.push_back(n_e
.getKind() == kind::EXISTS
? n_e
[1]
4502 e_children
.push_back( n_attr
);
4503 Node nn_e
= NodeManager::currentNM()->mkNode( kind::EXISTS
, e_children
);
4504 Trace("smt-qe-debug") << "Query for quantifier elimination : " << nn_e
<< std::endl
;
4505 Assert( nn_e
.getNumChildren()==3 );
4506 Result r
= checkSatisfiability(nn_e
.toExpr(), true, true);
4507 Trace("smt-qe") << "Query returned " << r
<< std::endl
;
4508 if(r
.asSatisfiabilityResult().isSat() != Result::UNSAT
) {
4509 if( r
.asSatisfiabilityResult().isSat() != Result::SAT
&& doFull
){
4511 ss
<< "While performing quantifier elimination, unexpected result : " << r
<< " for query.";
4512 InternalError(ss
.str().c_str());
4514 std::vector
< Node
> inst_qs
;
4515 d_theoryEngine
->getInstantiatedQuantifiedFormulas( inst_qs
);
4516 Assert( inst_qs
.size()<=1 );
4518 if( inst_qs
.size()==1 ){
4519 Node top_q
= inst_qs
[0];
4520 //Node top_q = Rewriter::rewrite( nn_e ).negate();
4521 Assert( top_q
.getKind()==kind::FORALL
);
4522 Trace("smt-qe") << "Get qe for " << top_q
<< std::endl
;
4523 ret_n
= d_theoryEngine
->getInstantiatedConjunction( top_q
);
4524 Trace("smt-qe") << "Returned : " << ret_n
<< std::endl
;
4525 if (n_e
.getKind() == kind::EXISTS
)
4527 ret_n
= Rewriter::rewrite(ret_n
.negate());
4530 ret_n
= NodeManager::currentNM()->mkConst(n_e
.getKind() != kind::EXISTS
);
4532 // do extended rewrite to minimize the size of the formula aggressively
4533 theory::quantifiers::ExtendedRewriter
extr(true);
4534 ret_n
= extr
.extendedRewrite(ret_n
);
4535 return ret_n
.toExpr();
4537 return NodeManager::currentNM()
4538 ->mkConst(n_e
.getKind() == kind::EXISTS
)
4543 void SmtEngine::getInstantiatedQuantifiedFormulas( std::vector
< Expr
>& qs
) {
4544 SmtScope
smts(this);
4545 if( d_theoryEngine
){
4546 std::vector
< Node
> qs_n
;
4547 d_theoryEngine
->getInstantiatedQuantifiedFormulas( qs_n
);
4548 for( unsigned i
=0; i
<qs_n
.size(); i
++ ){
4549 qs
.push_back( qs_n
[i
].toExpr() );
4556 void SmtEngine::getInstantiations( Expr q
, std::vector
< Expr
>& insts
) {
4557 SmtScope
smts(this);
4558 if( d_theoryEngine
){
4559 std::vector
< Node
> insts_n
;
4560 d_theoryEngine
->getInstantiations( Node::fromExpr( q
), insts_n
);
4561 for( unsigned i
=0; i
<insts_n
.size(); i
++ ){
4562 insts
.push_back( insts_n
[i
].toExpr() );
4569 void SmtEngine::getInstantiationTermVectors( Expr q
, std::vector
< std::vector
< Expr
> >& tvecs
) {
4570 SmtScope
smts(this);
4571 Assert(options::trackInstLemmas());
4572 if( d_theoryEngine
){
4573 std::vector
< std::vector
< Node
> > tvecs_n
;
4574 d_theoryEngine
->getInstantiationTermVectors( Node::fromExpr( q
), tvecs_n
);
4575 for( unsigned i
=0; i
<tvecs_n
.size(); i
++ ){
4576 std::vector
< Expr
> tvec
;
4577 for( unsigned j
=0; j
<tvecs_n
[i
].size(); j
++ ){
4578 tvec
.push_back( tvecs_n
[i
][j
].toExpr() );
4580 tvecs
.push_back( tvec
);
4587 vector
<Expr
> SmtEngine::getAssertions() {
4588 SmtScope
smts(this);
4589 finalOptionsAreSet();
4591 if(Dump
.isOn("benchmark")) {
4592 Dump("benchmark") << GetAssertionsCommand();
4594 Trace("smt") << "SMT getAssertions()" << endl
;
4595 if(!options::produceAssertions()) {
4597 "Cannot query the current assertion list when not in produce-assertions mode.";
4598 throw ModalException(msg
);
4600 Assert(d_assertionList
!= NULL
);
4601 // copy the result out
4602 return vector
<Expr
>(d_assertionList
->begin(), d_assertionList
->end());
4605 void SmtEngine::push()
4607 SmtScope
smts(this);
4608 finalOptionsAreSet();
4610 Trace("smt") << "SMT push()" << endl
;
4611 d_private
->notifyPush();
4612 d_private
->processAssertions();
4613 if(Dump
.isOn("benchmark")) {
4614 Dump("benchmark") << PushCommand();
4616 if(!options::incrementalSolving()) {
4617 throw ModalException("Cannot push when not solving incrementally (use --incremental)");
4620 // check to see if a postsolve() is pending
4621 if(d_needPostsolve
) {
4622 d_theoryEngine
->postsolve();
4623 d_needPostsolve
= false;
4626 // The problem isn't really "extended" yet, but this disallows
4627 // get-model after a push, simplifying our lives somewhat and
4628 // staying symmtric with pop.
4629 setProblemExtended(true);
4631 d_userLevels
.push_back(d_userContext
->getLevel());
4633 Trace("userpushpop") << "SmtEngine: pushed to level "
4634 << d_userContext
->getLevel() << endl
;
4637 void SmtEngine::pop() {
4638 SmtScope
smts(this);
4639 finalOptionsAreSet();
4640 Trace("smt") << "SMT pop()" << endl
;
4641 if(Dump
.isOn("benchmark")) {
4642 Dump("benchmark") << PopCommand();
4644 if(!options::incrementalSolving()) {
4645 throw ModalException("Cannot pop when not solving incrementally (use --incremental)");
4647 if(d_userLevels
.size() == 0) {
4648 throw ModalException("Cannot pop beyond the first user frame");
4651 // check to see if a postsolve() is pending
4652 if(d_needPostsolve
) {
4653 d_theoryEngine
->postsolve();
4654 d_needPostsolve
= false;
4657 // The problem isn't really "extended" yet, but this disallows
4658 // get-model after a pop, simplifying our lives somewhat. It might
4659 // not be strictly necessary to do so, since the pops occur lazily,
4660 // but also it would be weird to have a legally-executed (get-model)
4661 // that only returns a subset of the assignment (because the rest
4662 // is no longer in scope!).
4663 setProblemExtended(true);
4665 AlwaysAssert(d_userContext
->getLevel() > 0);
4666 AlwaysAssert(d_userLevels
.back() < d_userContext
->getLevel());
4667 while (d_userLevels
.back() < d_userContext
->getLevel()) {
4670 d_userLevels
.pop_back();
4672 // Clear out assertion queues etc., in case anything is still in there
4673 d_private
->notifyPop();
4675 Trace("userpushpop") << "SmtEngine: popped to level "
4676 << d_userContext
->getLevel() << endl
;
4677 // FIXME: should we reset d_status here?
4678 // SMT-LIBv2 spec seems to imply no, but it would make sense to..
4681 void SmtEngine::internalPush() {
4682 Assert(d_fullyInited
);
4683 Trace("smt") << "SmtEngine::internalPush()" << endl
;
4685 if(options::incrementalSolving()) {
4686 d_private
->processAssertions();
4687 TimerStat::CodeTimer
pushPopTimer(d_stats
->d_pushPopTime
);
4688 d_userContext
->push();
4689 // the d_context push is done inside of the SAT solver
4690 d_propEngine
->push();
4694 void SmtEngine::internalPop(bool immediate
) {
4695 Assert(d_fullyInited
);
4696 Trace("smt") << "SmtEngine::internalPop()" << endl
;
4697 if(options::incrementalSolving()) {
4705 void SmtEngine::doPendingPops() {
4706 Assert(d_pendingPops
== 0 || options::incrementalSolving());
4707 while(d_pendingPops
> 0) {
4708 TimerStat::CodeTimer
pushPopTimer(d_stats
->d_pushPopTime
);
4709 d_propEngine
->pop();
4710 // the d_context pop is done inside of the SAT solver
4711 d_userContext
->pop();
4716 void SmtEngine::reset()
4718 SmtScope
smts(this);
4719 ExprManager
*em
= d_exprManager
;
4720 Trace("smt") << "SMT reset()" << endl
;
4721 if(Dump
.isOn("benchmark")) {
4722 Dump("benchmark") << ResetCommand();
4725 opts
.copyValues(d_originalOptions
);
4727 NodeManager::fromExprManager(em
)->getOptions().copyValues(opts
);
4728 new(this) SmtEngine(em
);
4731 void SmtEngine::resetAssertions()
4733 SmtScope
smts(this);
4736 Trace("smt") << "SMT resetAssertions()" << endl
;
4737 if(Dump
.isOn("benchmark")) {
4738 Dump("benchmark") << ResetAssertionsCommand();
4741 while(!d_userLevels
.empty()) {
4745 // Also remember the global push/pop around everything.
4746 Assert(d_userLevels
.size() == 0 && d_userContext
->getLevel() == 1);
4747 d_context
->popto(0);
4748 d_userContext
->popto(0);
4749 DeleteAndClearCommandVector(d_modelGlobalCommands
);
4750 d_userContext
->push();
4754 void SmtEngine::interrupt()
4756 if(!d_fullyInited
) {
4759 d_propEngine
->interrupt();
4760 d_theoryEngine
->interrupt();
4763 void SmtEngine::setResourceLimit(unsigned long units
, bool cumulative
) {
4764 d_private
->getResourceManager()->setResourceLimit(units
, cumulative
);
4766 void SmtEngine::setTimeLimit(unsigned long milis
, bool cumulative
) {
4767 d_private
->getResourceManager()->setTimeLimit(milis
, cumulative
);
4770 unsigned long SmtEngine::getResourceUsage() const {
4771 return d_private
->getResourceManager()->getResourceUsage();
4774 unsigned long SmtEngine::getTimeUsage() const {
4775 return d_private
->getResourceManager()->getTimeUsage();
4778 unsigned long SmtEngine::getResourceRemaining() const
4780 return d_private
->getResourceManager()->getResourceRemaining();
4783 unsigned long SmtEngine::getTimeRemaining() const
4785 return d_private
->getResourceManager()->getTimeRemaining();
4788 Statistics
SmtEngine::getStatistics() const
4790 return Statistics(*d_statisticsRegistry
);
4793 SExpr
SmtEngine::getStatistic(std::string name
) const
4795 return d_statisticsRegistry
->getStatistic(name
);
4798 void SmtEngine::safeFlushStatistics(int fd
) const {
4799 d_statisticsRegistry
->safeFlushInformation(fd
);
4802 void SmtEngine::setUserAttribute(const std::string
& attr
,
4804 const std::vector
<Expr
>& expr_values
,
4805 const std::string
& str_value
)
4807 SmtScope
smts(this);
4808 std::vector
<Node
> node_values
;
4809 for( unsigned i
=0; i
<expr_values
.size(); i
++ ){
4810 node_values
.push_back( expr_values
[i
].getNode() );
4812 d_theoryEngine
->setUserAttribute(attr
, expr
.getNode(), node_values
, str_value
);
4815 void SmtEngine::setPrintFuncInModel(Expr f
, bool p
) {
4816 Trace("setp-model") << "Set printInModel " << f
<< " to " << p
<< std::endl
;
4817 for( unsigned i
=0; i
<d_modelGlobalCommands
.size(); i
++ ){
4818 Command
* c
= d_modelGlobalCommands
[i
];
4819 DeclareFunctionCommand
* dfc
= dynamic_cast<DeclareFunctionCommand
*>(c
);
4821 if( dfc
->getFunction()==f
){
4822 dfc
->setPrintInModel( p
);
4826 for( unsigned i
=0; i
<d_modelCommands
->size(); i
++ ){
4827 Command
* c
= (*d_modelCommands
)[i
];
4828 DeclareFunctionCommand
* dfc
= dynamic_cast<DeclareFunctionCommand
*>(c
);
4830 if( dfc
->getFunction()==f
){
4831 dfc
->setPrintInModel( p
);
4837 void SmtEngine::beforeSearch()
4840 throw ModalException(
4841 "SmtEngine::beforeSearch called after initialization.");
4846 void SmtEngine::setOption(const std::string
& key
, const CVC4::SExpr
& value
)
4848 NodeManagerScope
nms(d_nodeManager
);
4849 Trace("smt") << "SMT setOption(" << key
<< ", " << value
<< ")" << endl
;
4851 if(Dump
.isOn("benchmark")) {
4852 Dump("benchmark") << SetOptionCommand(key
, value
);
4855 if(key
== "command-verbosity") {
4856 if(!value
.isAtom()) {
4857 const vector
<SExpr
>& cs
= value
.getChildren();
4858 if(cs
.size() == 2 &&
4859 (cs
[0].isKeyword() || cs
[0].isString()) &&
4860 cs
[1].isInteger()) {
4861 string c
= cs
[0].getValue();
4862 const Integer
& v
= cs
[1].getIntegerValue();
4863 if(v
< 0 || v
> 2) {
4864 throw OptionException("command-verbosity must be 0, 1, or 2");
4866 d_commandVerbosity
[c
] = v
;
4870 throw OptionException("command-verbosity value must be a tuple (command-name, integer)");
4873 if(!value
.isAtom()) {
4874 throw OptionException("bad value for :" + key
);
4877 string optionarg
= value
.getValue();
4878 Options
& nodeManagerOptions
= NodeManager::currentNM()->getOptions();
4879 nodeManagerOptions
.setOption(key
, optionarg
);
4882 CVC4::SExpr
SmtEngine::getOption(const std::string
& key
) const
4884 NodeManagerScope
nms(d_nodeManager
);
4886 Trace("smt") << "SMT getOption(" << key
<< ")" << endl
;
4888 if(key
.length() >= 18 &&
4889 key
.compare(0, 18, "command-verbosity:") == 0) {
4890 map
<string
, Integer
>::const_iterator i
= d_commandVerbosity
.find(key
.c_str() + 18);
4891 if(i
!= d_commandVerbosity
.end()) {
4892 return SExpr((*i
).second
);
4894 i
= d_commandVerbosity
.find("*");
4895 if(i
!= d_commandVerbosity
.end()) {
4896 return SExpr((*i
).second
);
4898 return SExpr(Integer(2));
4901 if(Dump
.isOn("benchmark")) {
4902 Dump("benchmark") << GetOptionCommand(key
);
4905 if(key
== "command-verbosity") {
4906 vector
<SExpr
> result
;
4907 SExpr defaultVerbosity
;
4908 for(map
<string
, Integer
>::const_iterator i
= d_commandVerbosity
.begin();
4909 i
!= d_commandVerbosity
.end();
4912 v
.push_back(SExpr((*i
).first
));
4913 v
.push_back(SExpr((*i
).second
));
4914 if((*i
).first
== "*") {
4915 // put the default at the end of the SExpr
4916 defaultVerbosity
= SExpr(v
);
4918 result
.push_back(SExpr(v
));
4921 // put the default at the end of the SExpr
4922 if(!defaultVerbosity
.isAtom()) {
4923 result
.push_back(defaultVerbosity
);
4925 // ensure the default is always listed
4927 v
.push_back(SExpr("*"));
4928 v
.push_back(SExpr(Integer(2)));
4929 result
.push_back(SExpr(v
));
4931 return SExpr(result
);
4934 Options
& nodeManagerOptions
= NodeManager::currentNM()->getOptions();
4935 return SExpr::parseAtom(nodeManagerOptions
.getOption(key
));
4938 void SmtEngine::setReplayStream(ExprStream
* replayStream
) {
4939 AlwaysAssert(!d_fullyInited
,
4940 "Cannot set replay stream once fully initialized");
4941 d_replayStream
= replayStream
;
4944 bool SmtEngine::getExpressionName(Expr e
, std::string
& name
) const {
4945 return d_private
->getExpressionName(e
, name
);
4948 void SmtEngine::setExpressionName(Expr e
, const std::string
& name
) {
4949 Trace("smt-debug") << "Set expression name " << e
<< " to " << name
<< std::endl
;
4950 d_private
->setExpressionName(e
,name
);
4953 }/* CVC4 namespace */