1 /********************* */
2 /*! \file smt_engine.cpp
4 ** Top contributors (to current version):
5 ** Morgan Deters, Clark Barrett, Tim King
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2016 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"
21 #include <ext/hash_map>
29 #include "base/configuration.h"
30 #include "base/configuration_private.h"
31 #include "base/exception.h"
32 #include "base/listener.h"
33 #include "base/modal_exception.h"
34 #include "base/output.h"
35 #include "context/cdhashset.h"
36 #include "context/cdlist.h"
37 #include "context/context.h"
38 #include "decision/decision_engine.h"
39 #include "expr/attribute.h"
40 #include "expr/expr.h"
41 #include "expr/kind.h"
42 #include "expr/metakind.h"
43 #include "expr/node.h"
44 #include "expr/node_builder.h"
45 #include "expr/node_self_iterator.h"
46 #include "options/arith_options.h"
47 #include "options/arrays_options.h"
48 #include "options/base_options.h"
49 #include "options/booleans_options.h"
50 #include "options/bv_options.h"
51 #include "options/datatypes_options.h"
52 #include "options/decision_mode.h"
53 #include "options/decision_options.h"
54 #include "options/main_options.h"
55 #include "options/open_ostream.h"
56 #include "options/option_exception.h"
57 #include "options/printer_options.h"
58 #include "options/proof_options.h"
59 #include "options/prop_options.h"
60 #include "options/quantifiers_options.h"
61 #include "options/set_language.h"
62 #include "options/smt_options.h"
63 #include "options/strings_options.h"
64 #include "options/theory_options.h"
65 #include "options/uf_options.h"
66 #include "printer/printer.h"
67 #include "proof/proof.h"
68 #include "proof/proof_manager.h"
69 #include "proof/proof_manager.h"
70 #include "proof/theory_proof.h"
71 #include "proof/unsat_core.h"
72 #include "prop/prop_engine.h"
73 #include "smt/command.h"
74 #include "smt/command_list.h"
75 #include "smt/term_formula_removal.h"
76 #include "smt/logic_request.h"
77 #include "smt/managed_ostreams.h"
78 #include "smt/smt_engine_scope.h"
79 #include "smt/update_ostream.h"
80 #include "smt_util/boolean_simplification.h"
81 #include "smt_util/nary_builder.h"
82 #include "smt_util/node_visitor.h"
83 #include "theory/arith/pseudoboolean_proc.h"
84 #include "theory/booleans/circuit_propagator.h"
85 #include "theory/bv/bvintropow2.h"
86 #include "theory/bv/theory_bv_rewriter.h"
87 #include "theory/logic_info.h"
88 #include "theory/quantifiers/ce_guided_instantiation.h"
89 #include "theory/quantifiers/fun_def_process.h"
90 #include "theory/quantifiers/macros.h"
91 #include "theory/quantifiers/quantifiers_rewriter.h"
92 #include "theory/sort_inference.h"
93 #include "theory/strings/theory_strings.h"
94 #include "theory/substitutions.h"
95 #include "theory/theory_engine.h"
96 #include "theory/theory_model.h"
97 #include "theory/theory_traits.h"
98 #include "util/hash.h"
99 #include "util/proof.h"
100 #include "util/resource_manager.h"
101 #include "options/sep_options.h"
104 using namespace CVC4
;
105 using namespace CVC4::smt
;
106 using namespace CVC4::prop
;
107 using namespace CVC4::context
;
108 using namespace CVC4::theory
;
113 struct DeleteCommandFunction
: public std::unary_function
<const Command
*, void>
115 void operator()(const Command
* command
) { delete command
; }
118 void DeleteAndClearCommandVector(std::vector
<Command
*>& commands
) {
119 std::for_each(commands
.begin(), commands
.end(), DeleteCommandFunction());
123 /** Useful for counting the number of recursive calls. */
128 ScopeCounter(unsigned& d
) : d_depth(d
) {
137 * Representation of a defined function. We keep these around in
138 * SmtEngine to permit expanding definitions late (and lazily), to
139 * support getValue() over defined functions, to support user output
140 * in terms of defined functions, etc.
142 class DefinedFunction
{
144 vector
<Node
> d_formals
;
148 DefinedFunction(Node func
, vector
<Node
> formals
, Node formula
) :
153 Node
getFunction() const { return d_func
; }
154 vector
<Node
> getFormals() const { return d_formals
; }
155 Node
getFormula() const { return d_formula
; }
156 };/* class DefinedFunction */
158 class AssertionPipeline
{
159 vector
<Node
> d_nodes
;
163 size_t size() const { return d_nodes
.size(); }
165 void resize(size_t n
) { d_nodes
.resize(n
); }
166 void clear() { d_nodes
.clear(); }
168 Node
& operator[](size_t i
) { return d_nodes
[i
]; }
169 const Node
& operator[](size_t i
) const { return d_nodes
[i
]; }
170 void push_back(Node n
) { d_nodes
.push_back(n
); }
172 vector
<Node
>& ref() { return d_nodes
; }
173 const vector
<Node
>& ref() const { return d_nodes
; }
175 void replace(size_t i
, Node n
) {
176 PROOF( ProofManager::currentPM()->addDependence(n
, d_nodes
[i
]); );
179 };/* class AssertionPipeline */
181 struct SmtEngineStatistics
{
182 /** time spent in definition-expansion */
183 TimerStat d_definitionExpansionTime
;
184 /** time spent in non-clausal simplification */
185 TimerStat d_nonclausalSimplificationTime
;
186 /** time spent in miplib pass */
187 TimerStat d_miplibPassTime
;
188 /** number of assertions removed by miplib pass */
189 IntStat d_numMiplibAssertionsRemoved
;
190 /** number of constant propagations found during nonclausal simp */
191 IntStat d_numConstantProps
;
192 /** time spent in static learning */
193 TimerStat d_staticLearningTime
;
194 /** time spent in simplifying ITEs */
195 TimerStat d_simpITETime
;
196 /** time spent in simplifying ITEs */
197 TimerStat d_unconstrainedSimpTime
;
198 /** time spent removing ITEs */
199 TimerStat d_iteRemovalTime
;
200 /** time spent in theory preprocessing */
201 TimerStat d_theoryPreprocessTime
;
202 /** time spent in theory preprocessing */
203 TimerStat d_rewriteApplyToConstTime
;
204 /** time spent converting to CNF */
205 TimerStat d_cnfConversionTime
;
206 /** Num of assertions before ite removal */
207 IntStat d_numAssertionsPre
;
208 /** Num of assertions after ite removal */
209 IntStat d_numAssertionsPost
;
210 /** time spent in checkModel() */
211 TimerStat d_checkModelTime
;
212 /** time spent in checkProof() */
213 TimerStat d_checkProofTime
;
214 /** time spent in checkUnsatCore() */
215 TimerStat d_checkUnsatCoreTime
;
216 /** time spent in PropEngine::checkSat() */
217 TimerStat d_solveTime
;
218 /** time spent in pushing/popping */
219 TimerStat d_pushPopTime
;
220 /** time spent in processAssertions() */
221 TimerStat d_processAssertionsTime
;
223 /** Has something simplified to false? */
224 IntStat d_simplifiedToFalse
;
225 /** Number of resource units spent. */
226 ReferenceStat
<uint64_t> d_resourceUnitsUsed
;
228 SmtEngineStatistics() :
229 d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"),
230 d_nonclausalSimplificationTime("smt::SmtEngine::nonclausalSimplificationTime"),
231 d_miplibPassTime("smt::SmtEngine::miplibPassTime"),
232 d_numMiplibAssertionsRemoved("smt::SmtEngine::numMiplibAssertionsRemoved", 0),
233 d_numConstantProps("smt::SmtEngine::numConstantProps", 0),
234 d_staticLearningTime("smt::SmtEngine::staticLearningTime"),
235 d_simpITETime("smt::SmtEngine::simpITETime"),
236 d_unconstrainedSimpTime("smt::SmtEngine::unconstrainedSimpTime"),
237 d_iteRemovalTime("smt::SmtEngine::iteRemovalTime"),
238 d_theoryPreprocessTime("smt::SmtEngine::theoryPreprocessTime"),
239 d_rewriteApplyToConstTime("smt::SmtEngine::rewriteApplyToConstTime"),
240 d_cnfConversionTime("smt::SmtEngine::cnfConversionTime"),
241 d_numAssertionsPre("smt::SmtEngine::numAssertionsPreITERemoval", 0),
242 d_numAssertionsPost("smt::SmtEngine::numAssertionsPostITERemoval", 0),
243 d_checkModelTime("smt::SmtEngine::checkModelTime"),
244 d_checkProofTime("smt::SmtEngine::checkProofTime"),
245 d_checkUnsatCoreTime("smt::SmtEngine::checkUnsatCoreTime"),
246 d_solveTime("smt::SmtEngine::solveTime"),
247 d_pushPopTime("smt::SmtEngine::pushPopTime"),
248 d_processAssertionsTime("smt::SmtEngine::processAssertionsTime"),
249 d_simplifiedToFalse("smt::SmtEngine::simplifiedToFalse", 0),
250 d_resourceUnitsUsed("smt::SmtEngine::resourceUnitsUsed")
253 smtStatisticsRegistry()->registerStat(&d_definitionExpansionTime
);
254 smtStatisticsRegistry()->registerStat(&d_nonclausalSimplificationTime
);
255 smtStatisticsRegistry()->registerStat(&d_miplibPassTime
);
256 smtStatisticsRegistry()->registerStat(&d_numMiplibAssertionsRemoved
);
257 smtStatisticsRegistry()->registerStat(&d_numConstantProps
);
258 smtStatisticsRegistry()->registerStat(&d_staticLearningTime
);
259 smtStatisticsRegistry()->registerStat(&d_simpITETime
);
260 smtStatisticsRegistry()->registerStat(&d_unconstrainedSimpTime
);
261 smtStatisticsRegistry()->registerStat(&d_iteRemovalTime
);
262 smtStatisticsRegistry()->registerStat(&d_theoryPreprocessTime
);
263 smtStatisticsRegistry()->registerStat(&d_rewriteApplyToConstTime
);
264 smtStatisticsRegistry()->registerStat(&d_cnfConversionTime
);
265 smtStatisticsRegistry()->registerStat(&d_numAssertionsPre
);
266 smtStatisticsRegistry()->registerStat(&d_numAssertionsPost
);
267 smtStatisticsRegistry()->registerStat(&d_checkModelTime
);
268 smtStatisticsRegistry()->registerStat(&d_checkProofTime
);
269 smtStatisticsRegistry()->registerStat(&d_checkUnsatCoreTime
);
270 smtStatisticsRegistry()->registerStat(&d_solveTime
);
271 smtStatisticsRegistry()->registerStat(&d_pushPopTime
);
272 smtStatisticsRegistry()->registerStat(&d_processAssertionsTime
);
273 smtStatisticsRegistry()->registerStat(&d_simplifiedToFalse
);
274 smtStatisticsRegistry()->registerStat(&d_resourceUnitsUsed
);
277 ~SmtEngineStatistics() {
278 smtStatisticsRegistry()->unregisterStat(&d_definitionExpansionTime
);
279 smtStatisticsRegistry()->unregisterStat(&d_nonclausalSimplificationTime
);
280 smtStatisticsRegistry()->unregisterStat(&d_miplibPassTime
);
281 smtStatisticsRegistry()->unregisterStat(&d_numMiplibAssertionsRemoved
);
282 smtStatisticsRegistry()->unregisterStat(&d_numConstantProps
);
283 smtStatisticsRegistry()->unregisterStat(&d_staticLearningTime
);
284 smtStatisticsRegistry()->unregisterStat(&d_simpITETime
);
285 smtStatisticsRegistry()->unregisterStat(&d_unconstrainedSimpTime
);
286 smtStatisticsRegistry()->unregisterStat(&d_iteRemovalTime
);
287 smtStatisticsRegistry()->unregisterStat(&d_theoryPreprocessTime
);
288 smtStatisticsRegistry()->unregisterStat(&d_rewriteApplyToConstTime
);
289 smtStatisticsRegistry()->unregisterStat(&d_cnfConversionTime
);
290 smtStatisticsRegistry()->unregisterStat(&d_numAssertionsPre
);
291 smtStatisticsRegistry()->unregisterStat(&d_numAssertionsPost
);
292 smtStatisticsRegistry()->unregisterStat(&d_checkModelTime
);
293 smtStatisticsRegistry()->unregisterStat(&d_checkProofTime
);
294 smtStatisticsRegistry()->unregisterStat(&d_checkUnsatCoreTime
);
295 smtStatisticsRegistry()->unregisterStat(&d_solveTime
);
296 smtStatisticsRegistry()->unregisterStat(&d_pushPopTime
);
297 smtStatisticsRegistry()->unregisterStat(&d_processAssertionsTime
);
298 smtStatisticsRegistry()->unregisterStat(&d_simplifiedToFalse
);
299 smtStatisticsRegistry()->unregisterStat(&d_resourceUnitsUsed
);
301 };/* struct SmtEngineStatistics */
304 class SoftResourceOutListener
: public Listener
{
306 SoftResourceOutListener(SmtEngine
& smt
) : d_smt(&smt
) {}
307 virtual void notify() {
308 SmtScope
scope(d_smt
);
309 Assert(smt::smtEngineInScope());
314 }; /* class SoftResourceOutListener */
317 class HardResourceOutListener
: public Listener
{
319 HardResourceOutListener(SmtEngine
& smt
) : d_smt(&smt
) {}
320 virtual void notify() {
321 SmtScope
scope(d_smt
);
322 theory::Rewriter::clearCaches();
326 }; /* class HardResourceOutListener */
328 class SetLogicListener
: public Listener
{
330 SetLogicListener(SmtEngine
& smt
) : d_smt(&smt
) {}
331 virtual void notify() {
332 LogicInfo
inOptions(options::forceLogicString());
333 d_smt
->setLogic(inOptions
);
337 }; /* class SetLogicListener */
339 class BeforeSearchListener
: public Listener
{
341 BeforeSearchListener(SmtEngine
& smt
) : d_smt(&smt
) {}
342 virtual void notify() {
343 d_smt
->beforeSearch();
347 }; /* class BeforeSearchListener */
349 class UseTheoryListListener
: public Listener
{
351 UseTheoryListListener(TheoryEngine
* theoryEngine
)
352 : d_theoryEngine(theoryEngine
)
356 std::stringstream
commaList(options::useTheoryList());
359 Debug("UseTheoryListListener") << "UseTheoryListListener::notify() "
360 << options::useTheoryList() << std::endl
;
362 while(std::getline(commaList
, token
, ',')){
363 if(token
== "help") {
364 puts(theory::useTheoryHelp
);
367 if(theory::useTheoryValidate(token
)) {
368 d_theoryEngine
->enableTheoryAlternative(token
);
370 throw OptionException(
371 std::string("unknown option for --use-theory : `") + token
+
372 "'. Try --use-theory=help.");
378 TheoryEngine
* d_theoryEngine
;
379 }; /* class UseTheoryListListener */
382 class SetDefaultExprDepthListener
: public Listener
{
384 virtual void notify() {
385 int depth
= options::defaultExprDepth();
386 Debug
.getStream() << expr::ExprSetDepth(depth
);
387 Trace
.getStream() << expr::ExprSetDepth(depth
);
388 Notice
.getStream() << expr::ExprSetDepth(depth
);
389 Chat
.getStream() << expr::ExprSetDepth(depth
);
390 Message
.getStream() << expr::ExprSetDepth(depth
);
391 Warning
.getStream() << expr::ExprSetDepth(depth
);
392 // intentionally exclude Dump stream from this list
396 class SetDefaultExprDagListener
: public Listener
{
398 virtual void notify() {
399 int dag
= options::defaultDagThresh();
400 Debug
.getStream() << expr::ExprDag(dag
);
401 Trace
.getStream() << expr::ExprDag(dag
);
402 Notice
.getStream() << expr::ExprDag(dag
);
403 Chat
.getStream() << expr::ExprDag(dag
);
404 Message
.getStream() << expr::ExprDag(dag
);
405 Warning
.getStream() << expr::ExprDag(dag
);
406 Dump
.getStream() << expr::ExprDag(dag
);
410 class SetPrintExprTypesListener
: public Listener
{
412 virtual void notify() {
413 bool value
= options::printExprTypes();
414 Debug
.getStream() << expr::ExprPrintTypes(value
);
415 Trace
.getStream() << expr::ExprPrintTypes(value
);
416 Notice
.getStream() << expr::ExprPrintTypes(value
);
417 Chat
.getStream() << expr::ExprPrintTypes(value
);
418 Message
.getStream() << expr::ExprPrintTypes(value
);
419 Warning
.getStream() << expr::ExprPrintTypes(value
);
420 // intentionally exclude Dump stream from this list
424 class DumpModeListener
: public Listener
{
426 virtual void notify() {
427 const std::string
& value
= options::dumpModeString();
428 Dump
.setDumpFromString(value
);
432 class PrintSuccessListener
: public Listener
{
434 virtual void notify() {
435 bool value
= options::printSuccess();
436 Debug
.getStream() << Command::printsuccess(value
);
437 Trace
.getStream() << Command::printsuccess(value
);
438 Notice
.getStream() << Command::printsuccess(value
);
439 Chat
.getStream() << Command::printsuccess(value
);
440 Message
.getStream() << Command::printsuccess(value
);
441 Warning
.getStream() << Command::printsuccess(value
);
442 *options::out() << Command::printsuccess(value
);
449 * This is an inelegant solution, but for the present, it will work.
450 * The point of this is to separate the public and private portions of
451 * the SmtEngine class, so that smt_engine.h doesn't
452 * include "expr/node.h", which is a private CVC4 header (and can lead
453 * to linking errors due to the improper inlining of non-visible symbols
456 * The "real" solution (that which is usually implemented) is to move
457 * ALL the implementation to SmtEnginePrivate and maintain a
458 * heap-allocated instance of it in SmtEngine. SmtEngine (the public
459 * one) becomes an "interface shell" which simply acts as a forwarder
462 class SmtEnginePrivate
: public NodeManagerListener
{
465 typedef hash_map
<Node
, Node
, NodeHashFunction
> NodeToNodeHashMap
;
466 typedef hash_map
<Node
, bool, NodeHashFunction
> NodeToBoolHashMap
;
469 * Manager for limiting time and abstract resource usage.
471 ResourceManager
* d_resourceManager
;
473 /** Manager for the memory of regular-output-channel. */
474 ManagedRegularOutputChannel d_managedRegularChannel
;
476 /** Manager for the memory of diagnostic-output-channel. */
477 ManagedDiagnosticOutputChannel d_managedDiagnosticChannel
;
479 /** Manager for the memory of --dump-to. */
480 ManagedDumpOStream d_managedDumpChannel
;
482 /** Manager for --replay-log. */
483 ManagedReplayLogOstream d_managedReplayLog
;
486 * This list contains:
490 * beforeSearchListener
491 * UseTheoryListListener
493 * This needs to be deleted before both NodeManager's Options,
494 * SmtEngine, d_resourceManager, and TheoryEngine.
496 ListenerRegistrationList
* d_listenerRegistrations
;
498 /** Learned literals */
499 vector
<Node
> d_nonClausalLearnedLiterals
;
501 /** Size of assertions array when preprocessing starts */
502 unsigned d_realAssertionsEnd
;
504 /** A circuit propagator for non-clausal propositional deduction */
505 booleans::CircuitPropagator d_propagator
;
506 bool d_propagatorNeedsFinish
;
507 std::vector
<Node
> d_boolVars
;
509 /** Assertions in the preprocessing pipeline */
510 AssertionPipeline d_assertions
;
512 /** Whether any assertions have been processed */
513 CDO
<bool> d_assertionsProcessed
;
515 /** Index for where to store substitutions */
516 CDO
<unsigned> d_substitutionsIndex
;
522 * A context that never pushes/pops, for use by CD structures (like
523 * SubstitutionMaps) that should be "global".
525 context::Context d_fakeContext
;
528 * A map of AbsractValues to their actual constants. Only used if
529 * options::abstractValues() is on.
531 SubstitutionMap d_abstractValueMap
;
534 * A mapping of all abstract values (actual value |-> abstract) that
535 * we've handed out. This is necessary to ensure that we give the
536 * same AbstractValues for the same real constants. Only used if
537 * options::abstractValues() is on.
539 NodeToNodeHashMap d_abstractValues
;
541 /** Number of calls of simplify assertions active.
543 unsigned d_simplifyAssertionsDepth
;
545 /** TODO: whether certain preprocess steps are necessary */
546 //bool d_needsExpandDefs;
547 //bool d_needsRewriteBoolTerms;
548 //bool d_needsConstrainSubTypes;
552 * Map from skolem variables to index in d_assertions containing
553 * corresponding introduced Boolean ite
555 IteSkolemMap d_iteSkolemMap
;
557 /** Instance of the ITE remover */
558 RemoveTermFormulas d_iteRemover
;
562 theory::arith::PseudoBooleanProcessor d_pbsProcessor
;
564 /** The top level substitutions */
565 SubstitutionMap d_topLevelSubstitutions
;
567 static const bool d_doConstantProp
= true;
570 * Runs the nonclausal solver and tries to solve all the assigned
573 * Returns false if the formula simplifies to "false"
575 bool nonClausalSimplify();
578 * Performs static learning on the assertions.
580 void staticLearning();
583 * Remove ITEs from the assertions.
587 Node
intToBV(TNode n
, NodeToNodeHashMap
& cache
);
588 Node
intToBVMakeBinary(TNode n
, NodeToNodeHashMap
& cache
);
591 * Helper function to fix up assertion list to restore invariants needed after
594 void collectSkolems(TNode n
, set
<TNode
>& skolemSet
, NodeToBoolHashMap
& cache
);
597 * Helper function to fix up assertion list to restore invariants needed after
600 bool checkForBadSkolems(TNode n
, TNode skolem
, NodeToBoolHashMap
& cache
);
602 // Lift bit-vectors of size 1 to booleans
605 // Convert booleans to bit-vectors of size 1
608 // Abstract common structure over small domains to UF
609 // return true if changes were made.
610 void bvAbstraction();
612 // Simplify ITE structure
615 // Simplify based on unconstrained values
616 void unconstrainedSimp();
619 * Ensures the assertions asserted after before now effectively come before
620 * d_realAssertionsEnd.
622 void compressBeforeRealAssertions(size_t before
);
625 * Any variable in an assertion that is declared as a subtype type
626 * (predicate subtype or integer subrange type) must be constrained
627 * to be in that type.
629 void constrainSubtypes(TNode n
, AssertionPipeline
& assertions
)
633 * Trace nodes back to their assertions using CircuitPropagator's
636 void traceBackToAssertions(const std::vector
<Node
>& nodes
,
637 std::vector
<TNode
>& assertions
);
640 * Remove conjuncts in toRemove from conjunction n. Return # of removed
643 size_t removeFromConjunction(Node
& n
,
644 const std::hash_set
<unsigned long>& toRemove
);
646 /** Scrub miplib encodings. */
647 void doMiplibTrick();
650 * Perform non-clausal simplification of a Node. This involves
651 * Theory implementations, but does NOT involve the SAT solver in
654 * Returns false if the formula simplifies to "false"
656 bool simplifyAssertions() throw(TypeCheckingException
, LogicException
,
657 UnsafeInterruptException
);
661 SmtEnginePrivate(SmtEngine
& smt
) :
663 d_managedRegularChannel(),
664 d_managedDiagnosticChannel(),
665 d_managedDumpChannel(),
666 d_managedReplayLog(),
667 d_listenerRegistrations(new ListenerRegistrationList()),
668 d_nonClausalLearnedLiterals(),
669 d_realAssertionsEnd(0),
670 d_propagator(d_nonClausalLearnedLiterals
, true, true),
671 d_propagatorNeedsFinish(false),
673 d_assertionsProcessed(smt
.d_userContext
, false),
674 d_substitutionsIndex(smt
.d_userContext
, 0),
676 d_abstractValueMap(&d_fakeContext
),
678 d_simplifyAssertionsDepth(0),
679 //d_needsExpandDefs(true),
680 //d_needsRewriteBoolTerms(true),
681 //d_needsConstrainSubTypes(true), //TODO
683 d_iteRemover(smt
.d_userContext
),
684 d_pbsProcessor(smt
.d_userContext
),
685 d_topLevelSubstitutions(smt
.d_userContext
)
687 d_smt
.d_nodeManager
->subscribeEvents(this);
688 d_true
= NodeManager::currentNM()->mkConst(true);
689 d_resourceManager
= NodeManager::currentResourceManager();
691 d_listenerRegistrations
->add(d_resourceManager
->registerSoftListener(
692 new SoftResourceOutListener(d_smt
)));
694 d_listenerRegistrations
->add(d_resourceManager
->registerHardListener(
695 new HardResourceOutListener(d_smt
)));
697 Options
& nodeManagerOptions
= NodeManager::currentNM()->getOptions();
698 d_listenerRegistrations
->add(
699 nodeManagerOptions
.registerForceLogicListener(
700 new SetLogicListener(d_smt
), true));
702 // Multiple options reuse BeforeSearchListener so registration requires an
703 // extra bit of care.
704 // We can safely not call notify on this before search listener at
705 // registration time. This d_smt cannot be beforeSearch at construction
706 // time. Therefore the BeforeSearchListener is a no-op. Therefore it does
707 // not have to be called.
708 d_listenerRegistrations
->add(
709 nodeManagerOptions
.registerBeforeSearchListener(
710 new BeforeSearchListener(d_smt
)));
712 // These do need registration calls.
713 d_listenerRegistrations
->add(
714 nodeManagerOptions
.registerSetDefaultExprDepthListener(
715 new SetDefaultExprDepthListener(), true));
716 d_listenerRegistrations
->add(
717 nodeManagerOptions
.registerSetDefaultExprDagListener(
718 new SetDefaultExprDagListener(), true));
719 d_listenerRegistrations
->add(
720 nodeManagerOptions
.registerSetPrintExprTypesListener(
721 new SetPrintExprTypesListener(), true));
722 d_listenerRegistrations
->add(
723 nodeManagerOptions
.registerSetDumpModeListener(
724 new DumpModeListener(), true));
725 d_listenerRegistrations
->add(
726 nodeManagerOptions
.registerSetPrintSuccessListener(
727 new PrintSuccessListener(), true));
728 d_listenerRegistrations
->add(
729 nodeManagerOptions
.registerSetRegularOutputChannelListener(
730 new SetToDefaultSourceListener(&d_managedRegularChannel
), true));
731 d_listenerRegistrations
->add(
732 nodeManagerOptions
.registerSetDiagnosticOutputChannelListener(
733 new SetToDefaultSourceListener(&d_managedDiagnosticChannel
), true));
734 d_listenerRegistrations
->add(
735 nodeManagerOptions
.registerDumpToFileNameListener(
736 new SetToDefaultSourceListener(&d_managedDumpChannel
), true));
737 d_listenerRegistrations
->add(
738 nodeManagerOptions
.registerSetReplayLogFilename(
739 new SetToDefaultSourceListener(&d_managedReplayLog
), true));
742 ~SmtEnginePrivate() throw() {
743 delete d_listenerRegistrations
;
745 if(d_propagatorNeedsFinish
) {
746 d_propagator
.finish();
747 d_propagatorNeedsFinish
= false;
749 d_smt
.d_nodeManager
->unsubscribeEvents(this);
752 ResourceManager
* getResourceManager() { return d_resourceManager
; }
753 void spendResource(unsigned ammount
) throw(UnsafeInterruptException
) {
754 d_resourceManager
->spendResource(ammount
);
757 void nmNotifyNewSort(TypeNode tn
, uint32_t flags
) {
758 DeclareTypeCommand
c(tn
.getAttribute(expr::VarNameAttr()),
761 if((flags
& ExprManager::SORT_FLAG_PLACEHOLDER
) == 0) {
762 d_smt
.addToModelCommandAndDump(c
, flags
);
766 void nmNotifyNewSortConstructor(TypeNode tn
) {
767 DeclareTypeCommand
c(tn
.getAttribute(expr::VarNameAttr()),
768 tn
.getAttribute(expr::SortArityAttr()),
770 d_smt
.addToModelCommandAndDump(c
);
773 void nmNotifyNewDatatypes(const std::vector
<DatatypeType
>& dtts
) {
774 DatatypeDeclarationCommand
c(dtts
);
775 d_smt
.addToModelCommandAndDump(c
);
778 void nmNotifyNewVar(TNode n
, uint32_t flags
) {
779 DeclareFunctionCommand
c(n
.getAttribute(expr::VarNameAttr()),
781 n
.getType().toType());
782 if((flags
& ExprManager::VAR_FLAG_DEFINED
) == 0) {
783 d_smt
.addToModelCommandAndDump(c
, flags
);
785 if(n
.getType().isBoolean() && !options::incrementalSolving()) {
786 d_boolVars
.push_back(n
);
790 void nmNotifyNewSkolem(TNode n
, const std::string
& comment
, uint32_t flags
) {
791 string id
= n
.getAttribute(expr::VarNameAttr());
792 DeclareFunctionCommand
c(id
,
794 n
.getType().toType());
795 if(Dump
.isOn("skolems") && comment
!= "") {
796 Dump("skolems") << CommentCommand(id
+ " is " + comment
);
798 if((flags
& ExprManager::VAR_FLAG_DEFINED
) == 0) {
799 d_smt
.addToModelCommandAndDump(c
, flags
, false, "skolems");
801 if(n
.getType().isBoolean() && !options::incrementalSolving()) {
802 d_boolVars
.push_back(n
);
806 void nmNotifyDeleteNode(TNode n
) {
807 d_smt
.d_smtAttributes
->deleteAllAttributes(n
);
810 Node
applySubstitutions(TNode node
) const {
811 return Rewriter::rewrite(d_topLevelSubstitutions
.apply(node
));
815 * Process the assertions that have been asserted.
817 void processAssertions();
820 * Process a user pop. Clears out the non-context-dependent stuff in this
821 * SmtEnginePrivate. Necessary to clear out our assertion vectors in case
822 * someone does a push-assert-pop without a check-sat.
825 d_assertions
.clear();
826 d_nonClausalLearnedLiterals
.clear();
827 d_realAssertionsEnd
= 0;
828 d_iteSkolemMap
.clear();
832 * Adds a formula to the current context. Action here depends on
833 * the SimplificationMode (in the current Options scope); the
834 * formula might be pushed out to the propositional layer
835 * immediately, or it might be simplified and kept, or it might not
836 * even be simplified.
837 * the 2nd and 3rd arguments added for bookkeeping for proofs
839 void addFormula(TNode n
, bool inUnsatCore
, bool inInput
= true)
840 throw(TypeCheckingException
, LogicException
);
842 /** Expand definitions in n. */
843 Node
expandDefinitions(TNode n
, NodeToNodeHashMap
& cache
,
844 bool expandOnly
= false)
845 throw(TypeCheckingException
, LogicException
, UnsafeInterruptException
);
848 * Simplify node "in" by expanding definitions and applying any
849 * substitutions learned from preprocessing.
851 Node
simplify(TNode in
) {
852 // Substitute out any abstract values in ex.
853 // Expand definitions.
854 NodeToNodeHashMap cache
;
855 Node n
= expandDefinitions(in
, cache
).toExpr();
856 // Make sure we've done all preprocessing, etc.
857 Assert(d_assertions
.size() == 0);
858 return applySubstitutions(n
).toExpr();
862 * Substitute away all AbstractValues in a node.
864 Node
substituteAbstractValues(TNode n
) {
865 // We need to do this even if options::abstractValues() is off,
866 // since the setting might have changed after we already gave out
867 // some abstract values.
868 return d_abstractValueMap
.apply(n
);
872 * Make a new (or return an existing) abstract value for a node.
873 * Can only use this if options::abstractValues() is on.
875 Node
mkAbstractValue(TNode n
) {
876 Assert(options::abstractValues());
877 Node
& val
= d_abstractValues
[n
];
879 val
= d_smt
.d_nodeManager
->mkAbstractValue(n
.getType());
880 d_abstractValueMap
.addSubstitution(val
, n
);
882 // We are supposed to ascribe types to all abstract values that go out.
883 NodeManager
* current
= d_smt
.d_nodeManager
;
884 Node ascription
= current
->mkConst(AscriptionType(n
.getType().toType()));
885 Node retval
= current
->mkNode(kind::APPLY_TYPE_ASCRIPTION
, ascription
, val
);
889 NodeToNodeHashMap d_rewriteApplyToConstCache
;
890 Node
rewriteApplyToConst(TNode n
) {
891 Trace("rewriteApplyToConst") << "rewriteApplyToConst :: " << n
<< std::endl
;
893 if(n
.getMetaKind() == kind::metakind::CONSTANT
||
894 n
.getMetaKind() == kind::metakind::VARIABLE
)
899 if(d_rewriteApplyToConstCache
.find(n
) != d_rewriteApplyToConstCache
.end()) {
900 Trace("rewriteApplyToConst") << "in cache :: "
901 << d_rewriteApplyToConstCache
[n
]
903 return d_rewriteApplyToConstCache
[n
];
906 if(n
.getKind() == kind::APPLY_UF
) {
907 if(n
.getNumChildren() == 1 && n
[0].isConst() &&
908 n
[0].getType().isInteger())
911 ss
<< n
.getOperator() << "_";
912 if(n
[0].getConst
<Rational
>() < 0) {
913 ss
<< "m" << -n
[0].getConst
<Rational
>();
917 Node newvar
= NodeManager::currentNM()->mkSkolem(
918 ss
.str(), n
.getType(), "rewriteApplyToConst skolem",
919 NodeManager::SKOLEM_EXACT_NAME
);
920 d_rewriteApplyToConstCache
[n
] = newvar
;
921 Trace("rewriteApplyToConst") << "made :: " << newvar
<< std::endl
;
925 ss
<< "The rewrite-apply-to-const preprocessor is currently limited;"
927 << "it only works if all function symbols are unary and with Integer"
929 << "domain, and all applications are to integer values." << std::endl
930 << "Found application: " << n
;
935 NodeBuilder
<> builder(n
.getKind());
936 if(n
.getMetaKind() == kind::metakind::PARAMETERIZED
) {
937 builder
<< n
.getOperator();
939 for(unsigned i
= 0; i
< n
.getNumChildren(); ++i
) {
940 builder
<< rewriteApplyToConst(n
[i
]);
943 d_rewriteApplyToConstCache
[n
] = rewr
;
944 Trace("rewriteApplyToConst") << "built :: " << rewr
<< std::endl
;
948 void addUseTheoryListListener(TheoryEngine
* theoryEngine
){
949 Options
& nodeManagerOptions
= NodeManager::currentNM()->getOptions();
950 d_listenerRegistrations
->add(
951 nodeManagerOptions
.registerUseTheoryListListener(
952 new UseTheoryListListener(theoryEngine
), true));
955 std::ostream
* getReplayLog() const {
956 return d_managedReplayLog
.getReplayLog();
959 };/* class SmtEnginePrivate */
961 }/* namespace CVC4::smt */
963 SmtEngine::SmtEngine(ExprManager
* em
) throw() :
964 d_context(new Context()),
966 d_userContext(new UserContext()),
968 d_nodeManager(d_exprManager
->getNodeManager()),
969 d_decisionEngine(NULL
),
970 d_theoryEngine(NULL
),
972 d_proofManager(NULL
),
973 d_definedFunctions(NULL
),
974 d_fmfRecFunctionsDefined(NULL
),
975 d_assertionList(NULL
),
977 d_modelGlobalCommands(),
978 d_modelCommands(NULL
),
984 d_fullyInited(false),
985 d_problemExtended(false),
987 d_needPostsolve(false),
988 d_earlyTheoryPP(true),
990 d_replayStream(NULL
),
992 d_smtAttributes(NULL
),
993 d_statisticsRegistry(NULL
),
995 d_channels(new LemmaChannels())
998 d_originalOptions
.copyValues(em
->getOptions());
999 d_smtAttributes
= new expr::attr::SmtAttributes(d_context
);
1000 d_private
= new smt::SmtEnginePrivate(*this);
1001 d_statisticsRegistry
= new StatisticsRegistry();
1002 d_stats
= new SmtEngineStatistics();
1003 d_stats
->d_resourceUnitsUsed
.setData(
1004 d_private
->getResourceManager()->getResourceUsage());
1006 // The ProofManager is constructed before any other proof objects such as
1007 // SatProof and TheoryProofs. The TheoryProofEngine and the SatProof are
1008 // initialized in TheoryEngine and PropEngine respectively.
1009 Assert(d_proofManager
== NULL
);
1011 // d_proofManager must be created before Options has been finished
1012 // being parsed from the input file. Because of this, we cannot trust
1013 // that options::proof() is set correctly yet.
1015 d_proofManager
= new ProofManager(d_userContext
);
1018 // We have mutual dependency here, so we add the prop engine to the theory
1019 // engine later (it is non-essential there)
1020 d_theoryEngine
= new TheoryEngine(d_context
, d_userContext
,
1021 d_private
->d_iteRemover
,
1022 const_cast<const LogicInfo
&>(d_logic
),
1026 for(TheoryId id
= theory::THEORY_FIRST
; id
< theory::THEORY_LAST
; ++id
) {
1027 TheoryConstructor::addTheory(d_theoryEngine
, id
);
1028 //register with proof engine if applicable
1030 ProofManager::currentPM()->getTheoryProofEngine()->registerTheory(d_theoryEngine
->theoryOf(id
));
1034 d_private
->addUseTheoryListListener(d_theoryEngine
);
1036 // global push/pop around everything, to ensure proper destruction
1037 // of context-dependent data structures
1038 d_userContext
->push();
1041 d_definedFunctions
= new(true) DefinedFunctionMap(d_userContext
);
1042 if( options::fmfFunWellDefined() || options::fmfFunWellDefinedRelevant() ){
1043 d_fmfRecFunctionsDefined
= new(true) NodeList(d_userContext
);
1045 d_modelCommands
= new(true) smt::CommandList(d_userContext
);
1048 void SmtEngine::finishInit() {
1049 Trace("smt-debug") << "SmtEngine::finishInit" << std::endl
;
1050 // ensure that our heuristics are properly set up
1053 Trace("smt-debug") << "Making decision engine..." << std::endl
;
1055 d_decisionEngine
= new DecisionEngine(d_context
, d_userContext
);
1056 d_decisionEngine
->init(); // enable appropriate strategies
1058 Trace("smt-debug") << "Making prop engine..." << std::endl
;
1059 d_propEngine
= new PropEngine(d_theoryEngine
, d_decisionEngine
, d_context
,
1060 d_userContext
, d_private
->getReplayLog(),
1061 d_replayStream
, d_channels
);
1063 Trace("smt-debug") << "Setting up theory engine..." << std::endl
;
1064 d_theoryEngine
->setPropEngine(d_propEngine
);
1065 d_theoryEngine
->setDecisionEngine(d_decisionEngine
);
1066 Trace("smt-debug") << "Finishing init for theory engine..." << std::endl
;
1067 d_theoryEngine
->finishInit();
1069 Trace("smt-debug") << "Set up assertion list..." << std::endl
;
1070 // [MGD 10/20/2011] keep around in incremental mode, due to a
1071 // cleanup ordering issue and Nodes/TNodes. If SAT is popped
1072 // first, some user-context-dependent TNodes might still exist
1074 if(options::produceAssertions() ||
1075 options::incrementalSolving()) {
1076 // In the case of incremental solving, we appear to need these to
1077 // ensure the relevant Nodes remain live.
1078 d_assertionList
= new(true) AssertionList(d_userContext
);
1081 // dump out a set-logic command
1082 if(Dump
.isOn("benchmark")) {
1083 if (Dump
.isOn("raw-benchmark")) {
1084 Dump("raw-benchmark") << SetBenchmarkLogicCommand(d_logic
.getLogicString());
1086 LogicInfo everything
;
1088 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.")
1089 << SetBenchmarkLogicCommand(everything
.getLogicString());
1093 Trace("smt-debug") << "Dump declaration commands..." << std::endl
;
1094 // dump out any pending declaration commands
1095 for(unsigned i
= 0; i
< d_dumpCommands
.size(); ++i
) {
1096 Dump("declarations") << *d_dumpCommands
[i
];
1097 delete d_dumpCommands
[i
];
1099 d_dumpCommands
.clear();
1101 PROOF( ProofManager::currentPM()->setLogic(d_logic
); );
1103 for(TheoryId id
= theory::THEORY_FIRST
; id
< theory::THEORY_LAST
; ++id
) {
1104 ProofManager::currentPM()->getTheoryProofEngine()->
1105 finishRegisterTheory(d_theoryEngine
->theoryOf(id
));
1109 Trace("smt-debug") << "SmtEngine::finishInit done" << std::endl
;
1112 void SmtEngine::finalOptionsAreSet() {
1117 if(! d_logic
.isLocked()) {
1121 // finish initialization, create the prop engine, etc.
1124 AlwaysAssert( d_propEngine
->getAssertionLevel() == 0,
1125 "The PropEngine has pushed but the SmtEngine "
1126 "hasn't finished initializing!" );
1128 d_fullyInited
= true;
1129 Assert(d_logic
.isLocked());
1131 d_propEngine
->assertFormula(NodeManager::currentNM()->mkConst
<bool>(true));
1132 d_propEngine
->assertFormula(NodeManager::currentNM()->mkConst
<bool>(false).notNode());
1135 void SmtEngine::shutdown() {
1138 while(options::incrementalSolving() && d_userContext
->getLevel() > 1) {
1142 // check to see if a postsolve() is pending
1143 if(d_needPostsolve
) {
1144 d_theoryEngine
->postsolve();
1145 d_needPostsolve
= false;
1148 if(d_propEngine
!= NULL
) {
1149 d_propEngine
->shutdown();
1151 if(d_theoryEngine
!= NULL
) {
1152 d_theoryEngine
->shutdown();
1154 if(d_decisionEngine
!= NULL
) {
1155 d_decisionEngine
->shutdown();
1159 SmtEngine::~SmtEngine() throw() {
1160 SmtScope
smts(this);
1165 // global push/pop around everything, to ensure proper destruction
1166 // of context-dependent data structures
1167 d_context
->popto(0);
1168 d_userContext
->popto(0);
1170 if(d_assignments
!= NULL
) {
1171 d_assignments
->deleteSelf();
1174 if(d_assertionList
!= NULL
) {
1175 d_assertionList
->deleteSelf();
1178 for(unsigned i
= 0; i
< d_dumpCommands
.size(); ++i
) {
1179 delete d_dumpCommands
[i
];
1180 d_dumpCommands
[i
] = NULL
;
1182 d_dumpCommands
.clear();
1184 DeleteAndClearCommandVector(d_modelGlobalCommands
);
1186 if(d_modelCommands
!= NULL
) {
1187 d_modelCommands
->deleteSelf();
1190 d_definedFunctions
->deleteSelf();
1192 if( d_fmfRecFunctionsDefined
!= NULL
){
1193 d_fmfRecFunctionsDefined
->deleteSelf();
1196 delete d_theoryEngine
;
1197 d_theoryEngine
= NULL
;
1198 delete d_propEngine
;
1199 d_propEngine
= NULL
;
1200 delete d_decisionEngine
;
1201 d_decisionEngine
= NULL
;
1204 // d_proofManager is always created when proofs are enabled at configure time.
1205 // Becuase of this, this code should not be wrapped in PROOF() which
1206 // additionally checks flags such as options::proof().
1208 delete d_proofManager
;
1209 d_proofManager
= NULL
;
1214 delete d_statisticsRegistry
;
1215 d_statisticsRegistry
= NULL
;
1220 delete d_smtAttributes
;
1221 d_smtAttributes
= NULL
;
1223 delete d_userContext
;
1224 d_userContext
= NULL
;
1231 } catch(Exception
& e
) {
1232 Warning() << "CVC4 threw an exception during cleanup." << endl
1237 void SmtEngine::setLogic(const LogicInfo
& logic
) throw(ModalException
) {
1238 SmtScope
smts(this);
1240 throw ModalException("Cannot set logic in SmtEngine after the engine has "
1241 "finished initializing.");
1247 void SmtEngine::setLogic(const std::string
& s
)
1248 throw(ModalException
, LogicException
) {
1249 SmtScope
smts(this);
1251 setLogic(LogicInfo(s
));
1252 } catch(IllegalArgumentException
& e
) {
1253 throw LogicException(e
.what());
1257 void SmtEngine::setLogic(const char* logic
)
1258 throw(ModalException
, LogicException
) {
1259 setLogic(string(logic
));
1262 LogicInfo
SmtEngine::getLogicInfo() const {
1266 void SmtEngine::setLogicInternal() throw() {
1267 Assert(!d_fullyInited
, "setting logic in SmtEngine but the engine has already"
1268 " finished initializing for this run");
1272 void SmtEngine::setDefaults() {
1273 if(options::forceLogicString
.wasSetByUser()) {
1274 d_logic
= LogicInfo(options::forceLogicString());
1276 else if (options::solveIntAsBV() > 0) {
1277 d_logic
= LogicInfo("QF_BV");
1278 } else if ((d_logic
.getLogicString() == "QF_UFBV" ||
1279 d_logic
.getLogicString() == "QF_ABV") &&
1280 options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
) {
1281 d_logic
= LogicInfo("QF_BV");
1285 /* - disabled for 1.4 release [MGD 2014.06.25]
1286 if(!d_logic.hasEverything() && d_logic.isTheoryEnabled(THEORY_STRINGS) ) {
1287 if(! options::stringExp.wasSetByUser()) {
1288 options::stringExp.set( true );
1289 Trace("smt") << "turning on strings-exp, for the theory of strings" << std::endl;
1294 if(options::stringExp()) {
1295 if( !d_logic
.isQuantified() ) {
1296 d_logic
= d_logic
.getUnlockedCopy();
1297 d_logic
.enableQuantifiers();
1299 Trace("smt") << "turning on quantifier logic, for strings-exp"
1302 if(! options::fmfBound
.wasSetByUser()) {
1303 options::fmfBound
.set( true );
1304 Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl
;
1306 if(! options::fmfInstEngine
.wasSetByUser()) {
1307 options::fmfInstEngine
.set( true );
1308 Trace("smt") << "turning on fmf-inst-engine, for strings-exp" << std::endl
;
1311 if(! options::rewriteDivk.wasSetByUser()) {
1312 options::rewriteDivk.set( true );
1313 Trace("smt") << "turning on rewrite-divk, for strings-exp" << std::endl;
1316 if(! options::stringFMF.wasSetByUser()) {
1317 options::stringFMF.set( true );
1318 Trace("smt") << "turning on strings-fmf, for strings-exp" << std::endl;
1323 if(options::checkModels()) {
1324 if(! options::produceAssertions()) {
1325 Notice() << "SmtEngine: turning on produce-assertions to support "
1326 << "check-models." << endl
;
1327 setOption("produce-assertions", SExpr("true"));
1331 if(options::unsatCores()) {
1332 if(options::simplificationMode() != SIMPLIFICATION_MODE_NONE
) {
1333 if(options::simplificationMode
.wasSetByUser()) {
1334 throw OptionException("simplification not supported with unsat cores");
1336 Notice() << "SmtEngine: turning off simplification to support unsat-cores"
1338 options::simplificationMode
.set(SIMPLIFICATION_MODE_NONE
);
1341 if(options::unconstrainedSimp()) {
1342 if(options::unconstrainedSimp
.wasSetByUser()) {
1343 throw OptionException("unconstrained simplification not supported with unsat cores");
1345 Notice() << "SmtEngine: turning off unconstrained simplification to support unsat-cores" << endl
;
1346 options::unconstrainedSimp
.set(false);
1349 if(options::pbRewrites()) {
1350 if(options::pbRewrites
.wasSetByUser()) {
1351 throw OptionException("pseudoboolean rewrites not supported with unsat cores");
1353 Notice() << "SmtEngine: turning off pseudoboolean rewrites to support unsat-cores" << endl
;
1354 setOption("pb-rewrites", false);
1357 if(options::sortInference()) {
1358 if(options::sortInference
.wasSetByUser()) {
1359 throw OptionException("sort inference not supported with unsat cores");
1361 Notice() << "SmtEngine: turning off sort inference to support unsat-cores" << endl
;
1362 options::sortInference
.set(false);
1365 if(options::preSkolemQuant()) {
1366 if(options::preSkolemQuant
.wasSetByUser()) {
1367 throw OptionException("pre-skolemization not supported with unsat cores");
1369 Notice() << "SmtEngine: turning off pre-skolemization to support unsat-cores" << endl
;
1370 options::preSkolemQuant
.set(false);
1373 if(options::bitvectorToBool()) {
1374 if(options::bitvectorToBool
.wasSetByUser()) {
1375 throw OptionException("bv-to-bool not supported with unsat cores");
1377 Notice() << "SmtEngine: turning off bitvector-to-bool to support unsat-cores" << endl
;
1378 options::bitvectorToBool
.set(false);
1381 if(options::boolToBitvector()) {
1382 if(options::boolToBitvector
.wasSetByUser()) {
1383 throw OptionException("bool-to-bv not supported with unsat cores");
1385 Notice() << "SmtEngine: turning off bool-to-bitvector to support unsat-cores" << endl
;
1386 options::boolToBitvector
.set(false);
1389 if(options::bvIntroducePow2()) {
1390 if(options::bvIntroducePow2
.wasSetByUser()) {
1391 throw OptionException("bv-intro-pow2 not supported with unsat cores");
1393 Notice() << "SmtEngine: turning off bv-introduce-pow2 to support unsat-cores" << endl
;
1394 setOption("bv-intro-pow2", false);
1396 if(options::repeatSimp()) {
1397 if(options::repeatSimp
.wasSetByUser()) {
1398 throw OptionException("repeat-simp not supported with unsat cores");
1400 Notice() << "SmtEngine: turning off repeat-simp to support unsat-cores" << endl
;
1401 setOption("repeat-simp", false);
1406 if(options::produceAssignments() && !options::produceModels()) {
1407 Notice() << "SmtEngine: turning on produce-models to support produce-assignments" << endl
;
1408 setOption("produce-models", SExpr("true"));
1411 // Set the options for the theoryOf
1412 if(!options::theoryOfMode
.wasSetByUser()) {
1413 if(d_logic
.isSharingEnabled() &&
1414 !d_logic
.isTheoryEnabled(THEORY_BV
) &&
1415 !d_logic
.isTheoryEnabled(THEORY_STRINGS
) &&
1416 !d_logic
.isTheoryEnabled(THEORY_SETS
) ) {
1417 Trace("smt") << "setting theoryof-mode to term-based" << endl
;
1418 options::theoryOfMode
.set(THEORY_OF_TERM_BASED
);
1422 // strings require LIA, UF; widen the logic
1423 if(d_logic
.isTheoryEnabled(THEORY_STRINGS
)) {
1424 LogicInfo
log(d_logic
.getUnlockedCopy());
1425 // Strings requires arith for length constraints, and also UF
1426 if(!d_logic
.isTheoryEnabled(THEORY_UF
)) {
1427 Trace("smt") << "because strings are enabled, also enabling UF" << endl
;
1428 log
.enableTheory(THEORY_UF
);
1430 if(!d_logic
.isTheoryEnabled(THEORY_ARITH
) || d_logic
.isDifferenceLogic() || !d_logic
.areIntegersUsed()) {
1431 Trace("smt") << "because strings are enabled, also enabling linear integer arithmetic" << endl
;
1432 log
.enableTheory(THEORY_ARITH
);
1433 log
.enableIntegers();
1434 log
.arithOnlyLinear();
1439 if(d_logic
.isTheoryEnabled(THEORY_ARRAY
) || d_logic
.isTheoryEnabled(THEORY_DATATYPES
) || d_logic
.isTheoryEnabled(THEORY_SETS
)) {
1440 if(!d_logic
.isTheoryEnabled(THEORY_UF
)) {
1441 LogicInfo
log(d_logic
.getUnlockedCopy());
1442 Trace("smt") << "because a theory that permits Boolean terms is enabled, also enabling UF" << endl
;
1443 log
.enableTheory(THEORY_UF
);
1449 // by default, symmetry breaker is on only for QF_UF
1450 if(! options::ufSymmetryBreaker
.wasSetByUser()) {
1451 bool qf_uf
= d_logic
.isPure(THEORY_UF
) && !d_logic
.isQuantified() && !options::proof();
1452 Trace("smt") << "setting uf symmetry breaker to " << qf_uf
<< endl
;
1453 options::ufSymmetryBreaker
.set(qf_uf
);
1455 // by default, nonclausal simplification is off for QF_SAT
1456 if(! options::simplificationMode
.wasSetByUser()) {
1457 bool qf_sat
= d_logic
.isPure(THEORY_BOOL
) && !d_logic
.isQuantified();
1458 Trace("smt") << "setting simplification mode to <" << d_logic
.getLogicString() << "> " << (!qf_sat
) << endl
;
1459 //simplification=none works better for SMT LIB benchmarks with quantifiers, not others
1460 //options::simplificationMode.set(qf_sat || quantifiers ? SIMPLIFICATION_MODE_NONE : SIMPLIFICATION_MODE_BATCH);
1461 options::simplificationMode
.set(qf_sat
? SIMPLIFICATION_MODE_NONE
: SIMPLIFICATION_MODE_BATCH
);
1464 // If in arrays, set the UF handler to arrays
1465 if(d_logic
.isTheoryEnabled(THEORY_ARRAY
) && ( !d_logic
.isQuantified() ||
1466 (d_logic
.isQuantified() && !d_logic
.isTheoryEnabled(THEORY_UF
)))) {
1467 Theory::setUninterpretedSortOwner(THEORY_ARRAY
);
1469 Theory::setUninterpretedSortOwner(THEORY_UF
);
1472 // Turn on ite simplification for QF_LIA and QF_AUFBV
1473 // WARNING: These checks match much more than just QF_AUFBV and
1474 // QF_LIA logics. --K [2014/10/15]
1475 if(! options::doITESimp
.wasSetByUser()) {
1476 bool qf_aufbv
= !d_logic
.isQuantified() &&
1477 d_logic
.isTheoryEnabled(THEORY_ARRAY
) &&
1478 d_logic
.isTheoryEnabled(THEORY_UF
) &&
1479 d_logic
.isTheoryEnabled(THEORY_BV
);
1480 bool qf_lia
= !d_logic
.isQuantified() &&
1481 d_logic
.isPure(THEORY_ARITH
) &&
1482 d_logic
.isLinear() &&
1483 !d_logic
.isDifferenceLogic() &&
1484 !d_logic
.areRealsUsed();
1486 bool iteSimp
= (qf_aufbv
|| qf_lia
);
1487 Trace("smt") << "setting ite simplification to " << iteSimp
<< endl
;
1488 options::doITESimp
.set(iteSimp
);
1490 if(! options::compressItes
.wasSetByUser() ){
1491 bool qf_lia
= !d_logic
.isQuantified() &&
1492 d_logic
.isPure(THEORY_ARITH
) &&
1493 d_logic
.isLinear() &&
1494 !d_logic
.isDifferenceLogic() &&
1495 !d_logic
.areRealsUsed();
1497 bool compressIte
= qf_lia
;
1498 Trace("smt") << "setting ite compression to " << compressIte
<< endl
;
1499 options::compressItes
.set(compressIte
);
1501 if(! options::simplifyWithCareEnabled
.wasSetByUser() ){
1502 bool qf_aufbv
= !d_logic
.isQuantified() &&
1503 d_logic
.isTheoryEnabled(THEORY_ARRAY
) &&
1504 d_logic
.isTheoryEnabled(THEORY_UF
) &&
1505 d_logic
.isTheoryEnabled(THEORY_BV
);
1507 bool withCare
= qf_aufbv
;
1508 Trace("smt") << "setting ite simplify with care to " << withCare
<< endl
;
1509 options::simplifyWithCareEnabled
.set(withCare
);
1511 // Turn off array eager index splitting for QF_AUFLIA
1512 if(! options::arraysEagerIndexSplitting
.wasSetByUser()) {
1513 if (not d_logic
.isQuantified() &&
1514 d_logic
.isTheoryEnabled(THEORY_ARRAY
) &&
1515 d_logic
.isTheoryEnabled(THEORY_UF
) &&
1516 d_logic
.isTheoryEnabled(THEORY_ARITH
)) {
1517 Trace("smt") << "setting array eager index splitting to false" << endl
;
1518 options::arraysEagerIndexSplitting
.set(false);
1521 // Turn on model-based arrays for QF_AX (unless models are enabled)
1522 // if(! options::arraysModelBased.wasSetByUser()) {
1523 // if (not d_logic.isQuantified() &&
1524 // d_logic.isTheoryEnabled(THEORY_ARRAY) &&
1525 // d_logic.isPure(THEORY_ARRAY) &&
1526 // !options::produceModels() &&
1527 // !options::checkModels()) {
1528 // Trace("smt") << "turning on model-based array solver" << endl;
1529 // options::arraysModelBased.set(true);
1532 // Turn on multiple-pass non-clausal simplification for QF_AUFBV
1533 if(! options::repeatSimp
.wasSetByUser()) {
1534 bool repeatSimp
= !d_logic
.isQuantified() &&
1535 (d_logic
.isTheoryEnabled(THEORY_ARRAY
) &&
1536 d_logic
.isTheoryEnabled(THEORY_UF
) &&
1537 d_logic
.isTheoryEnabled(THEORY_BV
)) &&
1538 !options::unsatCores();
1539 Trace("smt") << "setting repeat simplification to " << repeatSimp
<< endl
;
1540 options::repeatSimp
.set(repeatSimp
);
1542 // Turn on unconstrained simplification for QF_AUFBV
1543 if(!options::unconstrainedSimp
.wasSetByUser() ||
1544 options::incrementalSolving()) {
1545 // bool qf_sat = d_logic.isPure(THEORY_BOOL) && !d_logic.isQuantified();
1546 // bool uncSimp = false && !qf_sat && !options::incrementalSolving();
1547 bool uncSimp
= !options::incrementalSolving() &&
1548 !d_logic
.isQuantified() &&
1549 !options::produceModels() &&
1550 !options::produceAssignments() &&
1551 !options::checkModels() &&
1552 !options::unsatCores() &&
1553 (d_logic
.isTheoryEnabled(THEORY_ARRAY
) && d_logic
.isTheoryEnabled(THEORY_BV
));
1554 Trace("smt") << "setting unconstrained simplification to " << uncSimp
<< endl
;
1555 options::unconstrainedSimp
.set(uncSimp
);
1557 // Unconstrained simp currently does *not* support model generation
1558 if (options::unconstrainedSimp
.wasSetByUser() && options::unconstrainedSimp()) {
1559 if (options::produceModels()) {
1560 if (options::produceModels
.wasSetByUser()) {
1561 throw OptionException("Cannot use unconstrained-simp with model generation.");
1563 Notice() << "SmtEngine: turning off produce-models to support unconstrainedSimp" << endl
;
1564 setOption("produce-models", SExpr("false"));
1566 if (options::produceAssignments()) {
1567 if (options::produceAssignments
.wasSetByUser()) {
1568 throw OptionException("Cannot use unconstrained-simp with model generation (produce-assignments).");
1570 Notice() << "SmtEngine: turning off produce-assignments to support unconstrainedSimp" << endl
;
1571 setOption("produce-assignments", SExpr("false"));
1573 if (options::checkModels()) {
1574 if (options::checkModels
.wasSetByUser()) {
1575 throw OptionException("Cannot use unconstrained-simp with model generation (check-models).");
1577 Notice() << "SmtEngine: turning off check-models to support unconstrainedSimp" << endl
;
1578 setOption("check-models", SExpr("false"));
1583 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
&&
1584 options::incrementalSolving()) {
1585 if (options::incrementalSolving
.wasSetByUser()) {
1586 throw OptionException(std::string("Eager bit-blasting does not currently support incremental mode. \n\
1587 Try --bitblast=lazy"));
1589 Notice() << "SmtEngine: turning off incremental to support eager bit-blasting" << endl
;
1590 setOption("incremental", SExpr("false"));
1593 if (! options::bvEagerExplanations
.wasSetByUser() &&
1594 d_logic
.isTheoryEnabled(THEORY_ARRAY
) &&
1595 d_logic
.isTheoryEnabled(THEORY_BV
)) {
1596 Trace("smt") << "enabling eager bit-vector explanations " << endl
;
1597 options::bvEagerExplanations
.set(true);
1600 if( !options::bitvectorEqualitySolver() ){
1601 Trace("smt") << "disabling bvLazyRewriteExtf since equality solver is disabled" << endl
;
1602 options::bvLazyRewriteExtf
.set(false);
1605 // Turn on arith rewrite equalities only for pure arithmetic
1606 if(! options::arithRewriteEq
.wasSetByUser()) {
1607 bool arithRewriteEq
= d_logic
.isPure(THEORY_ARITH
) && !d_logic
.isQuantified();
1608 Trace("smt") << "setting arith rewrite equalities " << arithRewriteEq
<< endl
;
1609 options::arithRewriteEq
.set(arithRewriteEq
);
1611 if(! options::arithHeuristicPivots
.wasSetByUser()) {
1612 int16_t heuristicPivots
= 5;
1613 if(d_logic
.isPure(THEORY_ARITH
) && !d_logic
.isQuantified()) {
1614 if(d_logic
.isDifferenceLogic()) {
1615 heuristicPivots
= -1;
1616 } else if(!d_logic
.areIntegersUsed()) {
1617 heuristicPivots
= 0;
1620 Trace("smt") << "setting arithHeuristicPivots " << heuristicPivots
<< endl
;
1621 options::arithHeuristicPivots
.set(heuristicPivots
);
1623 if(! options::arithPivotThreshold
.wasSetByUser()){
1624 uint16_t pivotThreshold
= 2;
1625 if(d_logic
.isPure(THEORY_ARITH
) && !d_logic
.isQuantified()){
1626 if(d_logic
.isDifferenceLogic()){
1627 pivotThreshold
= 16;
1630 Trace("smt") << "setting arith arithPivotThreshold " << pivotThreshold
<< endl
;
1631 options::arithPivotThreshold
.set(pivotThreshold
);
1633 if(! options::arithStandardCheckVarOrderPivots
.wasSetByUser()){
1634 int16_t varOrderPivots
= -1;
1635 if(d_logic
.isPure(THEORY_ARITH
) && !d_logic
.isQuantified()){
1636 varOrderPivots
= 200;
1638 Trace("smt") << "setting arithStandardCheckVarOrderPivots " << varOrderPivots
<< endl
;
1639 options::arithStandardCheckVarOrderPivots
.set(varOrderPivots
);
1641 // Turn off early theory preprocessing if arithRewriteEq is on
1642 if (options::arithRewriteEq()) {
1643 d_earlyTheoryPP
= false;
1646 // Set decision mode based on logic (if not set by user)
1647 if(!options::decisionMode
.wasSetByUser()) {
1648 decision::DecisionMode decMode
=
1650 d_logic
.hasEverything() ? decision::DECISION_STRATEGY_JUSTIFICATION
:
1652 (not d_logic
.isQuantified() &&
1653 d_logic
.isPure(THEORY_BV
)
1655 // QF_AUFBV or QF_ABV or QF_UFBV
1656 (not d_logic
.isQuantified() &&
1657 (d_logic
.isTheoryEnabled(THEORY_ARRAY
) ||
1658 d_logic
.isTheoryEnabled(THEORY_UF
)) &&
1659 d_logic
.isTheoryEnabled(THEORY_BV
)
1661 // QF_AUFLIA (and may be ends up enabling QF_AUFLRA?)
1662 (not d_logic
.isQuantified() &&
1663 d_logic
.isTheoryEnabled(THEORY_ARRAY
) &&
1664 d_logic
.isTheoryEnabled(THEORY_UF
) &&
1665 d_logic
.isTheoryEnabled(THEORY_ARITH
)
1668 (not d_logic
.isQuantified() &&
1669 d_logic
.isPure(THEORY_ARITH
) && d_logic
.isLinear() && !d_logic
.isDifferenceLogic() && !d_logic
.areIntegersUsed()
1672 d_logic
.isQuantified() ||
1674 d_logic
.isTheoryEnabled(THEORY_STRINGS
)
1675 ? decision::DECISION_STRATEGY_JUSTIFICATION
1676 : decision::DECISION_STRATEGY_INTERNAL
1681 d_logic
.hasEverything() || d_logic
.isTheoryEnabled(THEORY_STRINGS
) ? false :
1683 (not d_logic
.isQuantified() &&
1684 d_logic
.isTheoryEnabled(THEORY_ARRAY
) &&
1685 d_logic
.isTheoryEnabled(THEORY_UF
) &&
1686 d_logic
.isTheoryEnabled(THEORY_ARITH
)
1689 (not d_logic
.isQuantified() &&
1690 d_logic
.isPure(THEORY_ARITH
) && d_logic
.isLinear() && !d_logic
.isDifferenceLogic() && !d_logic
.areIntegersUsed()
1695 Trace("smt") << "setting decision mode to " << decMode
<< endl
;
1696 options::decisionMode
.set(decMode
);
1697 options::decisionStopOnly
.set(stoponly
);
1699 if( options::incrementalSolving() ){
1700 //disable modes not supported by incremental
1701 options::sortInference
.set( false );
1702 options::ufssFairnessMonotone
.set( false );
1703 options::quantEpr
.set( false );
1705 if( d_logic
.hasCardinalityConstraints() ){
1706 //must have finite model finding on
1707 options::finiteModelFind
.set( true );
1710 //if it contains a theory with non-termination, do not strictly enforce that quantifiers and theory combination must be interleaved
1711 if( d_logic
.isTheoryEnabled(THEORY_STRINGS
) || (d_logic
.isTheoryEnabled(THEORY_ARITH
) && !d_logic
.isLinear()) ){
1712 if( !options::instWhenStrictInterleave
.wasSetByUser() ){
1713 options::instWhenStrictInterleave
.set( false );
1717 //local theory extensions
1718 if( options::localTheoryExt() ){
1719 if( !options::instMaxLevel
.wasSetByUser() ){
1720 options::instMaxLevel
.set( 0 );
1723 if( options::instMaxLevel()!=-1 ){
1724 Notice() << "SmtEngine: turning off cbqi to support instMaxLevel" << endl
;
1725 options::cbqi
.set(false);
1727 //track instantiations?
1728 if( options::cbqiNestedQE() || ( options::proof() && !options::trackInstLemmas
.wasSetByUser() ) ){
1729 options::trackInstLemmas
.set( true );
1732 if( ( options::fmfBoundLazy
.wasSetByUser() && options::fmfBoundLazy() ) ||
1733 ( options::fmfBoundInt
.wasSetByUser() && options::fmfBoundInt() ) ) {
1734 options::fmfBound
.set( true );
1736 //now have determined whether fmfBoundInt is on/off
1737 //apply fmfBoundInt options
1738 if( options::fmfBound() ){
1739 //must have finite model finding on
1740 options::finiteModelFind
.set( true );
1741 if( ! options::mbqiMode
.wasSetByUser() ||
1742 ( options::mbqiMode()!=quantifiers::MBQI_NONE
&&
1743 options::mbqiMode()!=quantifiers::MBQI_FMC
&&
1744 options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL
) ){
1745 //if bounded integers are set, use no MBQI by default
1746 options::mbqiMode
.set( quantifiers::MBQI_NONE
);
1748 if( ! options::prenexQuant
.wasSetByUser() ){
1749 options::prenexQuant
.set( quantifiers::PRENEX_QUANT_NONE
);
1752 if( options::mbqiMode()==quantifiers::MBQI_ABS
){
1753 if( !d_logic
.isPure(THEORY_UF
) ){
1754 //MBQI_ABS is only supported in pure quantified UF
1755 options::mbqiMode
.set( quantifiers::MBQI_FMC
);
1758 if( options::ufssSymBreak() ){
1759 options::sortInference
.set( true );
1761 if( options::fmfFunWellDefinedRelevant() ){
1762 if( !options::fmfFunWellDefined
.wasSetByUser() ){
1763 options::fmfFunWellDefined
.set( true );
1766 if( options::fmfFunWellDefined() ){
1767 if( !options::finiteModelFind
.wasSetByUser() ){
1768 options::finiteModelFind
.set( true );
1772 if( options::quantEpr() ){
1773 if( !options::preSkolemQuant
.wasSetByUser() ){
1774 options::preSkolemQuant
.set( true );
1778 //now, have determined whether finite model find is on/off
1779 //apply finite model finding options
1780 if( options::finiteModelFind() ){
1781 //apply conservative quantifiers splitting
1782 if( !options::quantDynamicSplit
.wasSetByUser() ){
1783 options::quantDynamicSplit
.set( quantifiers::QUANT_DSPLIT_MODE_DEFAULT
);
1785 if( !options::eMatching
.wasSetByUser() ){
1786 options::eMatching
.set( options::fmfInstEngine() );
1788 if( !options::instWhenMode
.wasSetByUser() ){
1789 //instantiate only on last call FIXME: remove?
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( options::cegqiSingleInvMode()!=quantifiers::CEGQI_SI_MODE_NONE
){
1809 if( !options::ceGuidedInst
.wasSetByUser() ){
1810 options::ceGuidedInst
.set( true );
1813 if( options::ceGuidedInst() ){
1814 //counterexample-guided instantiation for sygus
1815 if( !options::cegqiSingleInvMode
.wasSetByUser() ){
1816 options::cegqiSingleInvMode
.set( quantifiers::CEGQI_SI_MODE_USE
);
1818 if( !options::quantConflictFind
.wasSetByUser() ){
1819 options::quantConflictFind
.set( false );
1821 if( !options::instNoEntail
.wasSetByUser() ){
1822 options::instNoEntail
.set( false );
1824 //do not allow partial functions
1825 if( !options::bitvectorDivByZeroConst
.wasSetByUser() ){
1826 options::bitvectorDivByZeroConst
.set( true );
1828 if( !options::dtRewriteErrorSel
.wasSetByUser() ){
1829 options::dtRewriteErrorSel
.set( true );
1832 if( !options::miniscopeQuant
.wasSetByUser() ){
1833 options::miniscopeQuant
.set( false );
1835 if( !options::miniscopeQuantFreeVar
.wasSetByUser() ){
1836 options::miniscopeQuantFreeVar
.set( false );
1839 if( !options::rewriteDivk
.wasSetByUser()) {
1840 options::rewriteDivk
.set( true );
1843 if( !options::macrosQuant
.wasSetByUser()) {
1844 options::macrosQuant
.set( false );
1846 if( !options::cbqiPreRegInst
.wasSetByUser()) {
1847 options::cbqiPreRegInst
.set( true );
1850 //counterexample-guided instantiation for non-sygus
1851 // enable if any possible quantifiers with arithmetic, datatypes or bitvectors
1852 if( ( d_logic
.isQuantified() && ( d_logic
.isTheoryEnabled(THEORY_ARITH
) || d_logic
.isTheoryEnabled(THEORY_DATATYPES
) || d_logic
.isTheoryEnabled(THEORY_BV
) ) ) ||
1853 options::cbqiAll() ){
1854 if( !options::cbqi
.wasSetByUser() ){
1855 options::cbqi
.set( true );
1858 if( options::cbqi() ){
1860 if( !options::rewriteDivk
.wasSetByUser()) {
1861 options::rewriteDivk
.set( true );
1863 if( d_logic
.isPure(THEORY_ARITH
) ){
1864 options::cbqiAll
.set( false );
1865 if( !options::quantConflictFind
.wasSetByUser() ){
1866 options::quantConflictFind
.set( false );
1868 if( !options::instNoEntail
.wasSetByUser() ){
1869 options::instNoEntail
.set( false );
1871 if( !options::instWhenMode
.wasSetByUser() && options::cbqiModel() ){
1872 //only instantiation should happen at last call when model is avaiable
1873 options::instWhenMode
.set( quantifiers::INST_WHEN_LAST_CALL
);
1877 //implied options...
1878 if( options::strictTriggers() ){
1879 if( !options::userPatternsQuant
.wasSetByUser() ){
1880 options::userPatternsQuant
.set( quantifiers::USER_PAT_MODE_TRUST
);
1883 if( options::qcfMode
.wasSetByUser() || options::qcfTConstraint() ){
1884 options::quantConflictFind
.set( true );
1886 if( options::cbqiNestedQE() ){
1887 //only sound with prenex = disj_normal or normal
1888 if( options::prenexQuant()<=quantifiers::PRENEX_QUANT_DISJ_NORMAL
){
1889 options::prenexQuant
.set( quantifiers::PRENEX_QUANT_DISJ_NORMAL
);
1891 options::prenexQuantUser
.set( true );
1892 if( !options::preSkolemQuant
.wasSetByUser() ){
1893 options::preSkolemQuant
.set( true );
1896 //for induction techniques
1897 if( options::quantInduction() ){
1898 if( !options::dtStcInduction
.wasSetByUser() ){
1899 options::dtStcInduction
.set( true );
1901 if( !options::intWfInduction
.wasSetByUser() ){
1902 options::intWfInduction
.set( true );
1905 if( options::dtStcInduction() ){
1906 //leads to unfairness FIXME
1907 if( !options::dtForceAssignment
.wasSetByUser() ){
1908 options::dtForceAssignment
.set( true );
1910 //try to remove ITEs from quantified formulas
1911 if( !options::iteDtTesterSplitQuant
.wasSetByUser() ){
1912 options::iteDtTesterSplitQuant
.set( true );
1914 if( !options::iteLiftQuant
.wasSetByUser() ){
1915 options::iteLiftQuant
.set( quantifiers::ITE_LIFT_QUANT_MODE_ALL
);
1918 if( options::intWfInduction() ){
1919 if( !options::purifyTriggers
.wasSetByUser() ){
1920 options::purifyTriggers
.set( true );
1923 if( options::conjectureNoFilter() ){
1924 if( !options::conjectureFilterActiveTerms
.wasSetByUser() ){
1925 options::conjectureFilterActiveTerms
.set( false );
1927 if( !options::conjectureFilterCanonical
.wasSetByUser() ){
1928 options::conjectureFilterCanonical
.set( false );
1930 if( !options::conjectureFilterModel
.wasSetByUser() ){
1931 options::conjectureFilterModel
.set( false );
1934 if( options::conjectureGenPerRound
.wasSetByUser() ){
1935 if( options::conjectureGenPerRound()>0 ){
1936 options::conjectureGen
.set( true );
1938 options::conjectureGen
.set( false );
1941 //can't pre-skolemize nested quantifiers without UF theory
1942 if( !d_logic
.isTheoryEnabled(THEORY_UF
) && options::preSkolemQuant() ){
1943 if( !options::preSkolemQuantNested
.wasSetByUser() ){
1944 options::preSkolemQuantNested
.set( false );
1947 if( !d_logic
.isTheoryEnabled(THEORY_DATATYPES
) ){
1948 options::quantDynamicSplit
.set( quantifiers::QUANT_DSPLIT_MODE_NONE
);
1951 //until bugs 371,431 are fixed
1952 if( ! options::minisatUseElim
.wasSetByUser()){
1953 //AJR: cannot use minisat elim for new implementation of sets TODO: why?
1954 if( d_logic
.isTheoryEnabled(THEORY_SETS
) || d_logic
.isQuantified() || options::produceModels() || options::produceAssignments() || options::checkModels() ){
1955 options::minisatUseElim
.set( false );
1958 else if (options::minisatUseElim()) {
1959 if (options::produceModels()) {
1960 Notice() << "SmtEngine: turning off produce-models to support minisatUseElim" << endl
;
1961 setOption("produce-models", SExpr("false"));
1963 if (options::produceAssignments()) {
1964 Notice() << "SmtEngine: turning off produce-assignments to support minisatUseElim" << endl
;
1965 setOption("produce-assignments", SExpr("false"));
1967 if (options::checkModels()) {
1968 Notice() << "SmtEngine: turning off check-models to support minisatUseElim" << endl
;
1969 setOption("check-models", SExpr("false"));
1973 // For now, these array theory optimizations do not support model-building
1974 if (options::produceModels() || options::produceAssignments() || options::checkModels()) {
1975 options::arraysOptimizeLinear
.set(false);
1976 options::arraysLazyRIntro1
.set(false);
1979 // Non-linear arithmetic does not support models
1980 if (d_logic
.isTheoryEnabled(THEORY_ARITH
) &&
1981 !d_logic
.isLinear()) {
1982 if (options::produceModels()) {
1983 if(options::produceModels
.wasSetByUser()) {
1984 throw OptionException("produce-model not supported with nonlinear arith");
1986 Warning() << "SmtEngine: turning off produce-models because unsupported for nonlinear arith" << endl
;
1987 setOption("produce-models", SExpr("false"));
1989 if (options::produceAssignments()) {
1990 if(options::produceAssignments
.wasSetByUser()) {
1991 throw OptionException("produce-assignments not supported with nonlinear arith");
1993 Warning() << "SmtEngine: turning off produce-assignments because unsupported for nonlinear arith" << endl
;
1994 setOption("produce-assignments", SExpr("false"));
1996 if (options::checkModels()) {
1997 if(options::checkModels
.wasSetByUser()) {
1998 throw OptionException("check-models not supported with nonlinear arith");
2000 Warning() << "SmtEngine: turning off check-models because unsupported for nonlinear arith" << endl
;
2001 setOption("check-models", SExpr("false"));
2005 if(options::incrementalSolving() && options::proof()) {
2006 Warning() << "SmtEngine: turning off incremental solving mode (not yet supported with --proof, try --tear-down-incremental instead)" << endl
;
2007 setOption("incremental", SExpr("false"));
2011 void SmtEngine::setInfo(const std::string
& key
, const CVC4::SExpr
& value
)
2012 throw(OptionException
, ModalException
) {
2014 SmtScope
smts(this);
2016 Trace("smt") << "SMT setInfo(" << key
<< ", " << value
<< ")" << endl
;
2018 if(Dump
.isOn("benchmark")) {
2019 if(key
== "status") {
2020 string s
= value
.getValue();
2021 BenchmarkStatus status
=
2022 (s
== "sat") ? SMT_SATISFIABLE
:
2023 ((s
== "unsat") ? SMT_UNSATISFIABLE
: SMT_UNKNOWN
);
2024 Dump("benchmark") << SetBenchmarkStatusCommand(status
);
2026 Dump("benchmark") << SetInfoCommand(key
, value
);
2030 // Check for CVC4-specific info keys (prefixed with "cvc4-" or "cvc4_")
2031 if(key
.length() > 5) {
2032 string prefix
= key
.substr(0, 5);
2033 if(prefix
== "cvc4-" || prefix
== "cvc4_") {
2034 string cvc4key
= key
.substr(5);
2035 if(cvc4key
== "logic") {
2036 if(! value
.isAtom()) {
2037 throw OptionException("argument to (set-info :cvc4-logic ..) must be a string");
2039 SmtScope
smts(this);
2040 d_logic
= value
.getValue();
2044 throw UnrecognizedOptionException();
2049 // Check for standard info keys (SMT-LIB v1, SMT-LIB v2, ...)
2050 if(key
== "source" ||
2051 key
== "category" ||
2052 key
== "difficulty" ||
2056 } else if(key
== "name") {
2057 d_filename
= value
.getValue();
2059 } else if(key
== "smt-lib-version") {
2060 if( (value
.isInteger() && value
.getIntegerValue() == Integer(2)) ||
2061 (value
.isRational() && value
.getRationalValue() == Rational(2)) ||
2062 value
.getValue() == "2" ||
2063 value
.getValue() == "2.0" ) {
2064 // supported SMT-LIB version
2065 if(!options::outputLanguage
.wasSetByUser() &&
2066 ( options::outputLanguage() == language::output::LANG_SMTLIB_V2_5
|| options::outputLanguage() == language::output::LANG_SMTLIB_V2_6
)) {
2067 options::outputLanguage
.set(language::output::LANG_SMTLIB_V2_0
);
2068 *options::out() << language::SetLanguage(language::output::LANG_SMTLIB_V2_0
);
2071 } else if( (value
.isRational() && value
.getRationalValue() == Rational(5, 2)) ||
2072 value
.getValue() == "2.5" ) {
2073 // supported SMT-LIB version
2074 if(!options::outputLanguage
.wasSetByUser() &&
2075 options::outputLanguage() == language::output::LANG_SMTLIB_V2_0
) {
2076 options::outputLanguage
.set(language::output::LANG_SMTLIB_V2_5
);
2077 *options::out() << language::SetLanguage(language::output::LANG_SMTLIB_V2_5
);
2080 } else if( (value
.isRational() && value
.getRationalValue() == Rational(13, 5)) ||
2081 value
.getValue() == "2.6" ) {
2082 // supported SMT-LIB version
2083 if(!options::outputLanguage
.wasSetByUser() &&
2084 options::outputLanguage() == language::output::LANG_SMTLIB_V2_0
) {
2085 options::outputLanguage
.set(language::output::LANG_SMTLIB_V2_6
);
2086 *options::out() << language::SetLanguage(language::output::LANG_SMTLIB_V2_6
);
2090 Warning() << "Warning: unsupported smt-lib-version: " << value
<< endl
;
2091 throw UnrecognizedOptionException();
2092 } else if(key
== "status") {
2094 if(value
.isAtom()) {
2095 s
= value
.getValue();
2097 if(s
!= "sat" && s
!= "unsat" && s
!= "unknown") {
2098 throw OptionException("argument to (set-info :status ..) must be "
2099 "`sat' or `unsat' or `unknown'");
2101 d_status
= Result(s
, d_filename
);
2104 throw UnrecognizedOptionException();
2107 CVC4::SExpr
SmtEngine::getInfo(const std::string
& key
) const
2108 throw(OptionException
, ModalException
) {
2110 SmtScope
smts(this);
2112 Trace("smt") << "SMT getInfo(" << key
<< ")" << endl
;
2113 if(key
== "all-statistics") {
2114 vector
<SExpr
> stats
;
2115 for(StatisticsRegistry::const_iterator i
= NodeManager::fromExprManager(d_exprManager
)->getStatisticsRegistry()->begin();
2116 i
!= NodeManager::fromExprManager(d_exprManager
)->getStatisticsRegistry()->end();
2119 v
.push_back((*i
).first
);
2120 v
.push_back((*i
).second
);
2123 for(StatisticsRegistry::const_iterator i
= d_statisticsRegistry
->begin();
2124 i
!= d_statisticsRegistry
->end();
2127 v
.push_back((*i
).first
);
2128 v
.push_back((*i
).second
);
2131 return SExpr(stats
);
2132 } else if(key
== "error-behavior") {
2133 // immediate-exit | continued-execution
2134 if( options::continuedExecution() || options::interactive() ) {
2135 return SExpr(SExpr::Keyword("continued-execution"));
2137 return SExpr(SExpr::Keyword("immediate-exit"));
2139 } else if(key
== "name") {
2140 return SExpr(Configuration::getName());
2141 } else if(key
== "version") {
2142 return SExpr(Configuration::getVersionString());
2143 } else if(key
== "authors") {
2144 return SExpr(Configuration::about());
2145 } else if(key
== "status") {
2146 // sat | unsat | unknown
2147 switch(d_status
.asSatisfiabilityResult().isSat()) {
2149 return SExpr(SExpr::Keyword("sat"));
2151 return SExpr(SExpr::Keyword("unsat"));
2153 return SExpr(SExpr::Keyword("unknown"));
2155 } else if(key
== "reason-unknown") {
2156 if(!d_status
.isNull() && d_status
.isUnknown()) {
2158 ss
<< d_status
.whyUnknown();
2159 string s
= ss
.str();
2160 transform(s
.begin(), s
.end(), s
.begin(), ::tolower
);
2161 return SExpr(SExpr::Keyword(s
));
2163 throw ModalException("Can't get-info :reason-unknown when the "
2164 "last result wasn't unknown!");
2166 } else if(key
== "assertion-stack-levels") {
2167 AlwaysAssert(d_userLevels
.size() <=
2168 std::numeric_limits
<unsigned long int>::max());
2169 return SExpr(static_cast<unsigned long int>(d_userLevels
.size()));
2170 } else if(key
== "all-options") {
2171 // get the options, like all-statistics
2172 std::vector
< std::vector
<std::string
> > current_options
=
2173 Options::current()->getOptions();
2174 return SExpr::parseListOfListOfAtoms(current_options
);
2176 throw UnrecognizedOptionException();
2180 void SmtEngine::defineFunction(Expr func
,
2181 const std::vector
<Expr
>& formals
,
2183 SmtScope
smts(this);
2185 Trace("smt") << "SMT defineFunction(" << func
<< ")" << endl
;
2186 for(std::vector
<Expr
>::const_iterator i
= formals
.begin(); i
!= formals
.end(); ++i
) {
2187 if((*i
).getKind() != kind::BOUND_VARIABLE
) {
2189 ss
<< "All formal arguments to defined functions must be BOUND_VARIABLEs, but in the\n"
2190 << "definition of function " << func
<< ", formal\n"
2191 << " " << *i
<< "\n"
2192 << "has kind " << (*i
).getKind();
2193 throw TypeCheckingException(func
, ss
.str());
2198 ss
<< language::SetLanguage(language::SetLanguage::getLanguage(Dump
.getStream()))
2200 DefineFunctionCommand
c(ss
.str(), func
, formals
, formula
);
2201 addToModelCommandAndDump(c
, ExprManager::VAR_FLAG_DEFINED
, true, "declarations");
2204 PROOF( if (options::checkUnsatCores()) {
2205 d_defineCommands
.push_back(c
.clone());
2209 // Substitute out any abstract values in formula
2210 Expr form
= d_private
->substituteAbstractValues(Node::fromExpr(formula
)).toExpr();
2213 Type formulaType
= form
.getType(options::typeChecking());
2215 Type funcType
= func
.getType();
2216 // We distinguish here between definitions of constants and functions,
2217 // because the type checking for them is subtly different. Perhaps we
2218 // should instead have SmtEngine::defineFunction() and
2219 // SmtEngine::defineConstant() for better clarity, although then that
2220 // doesn't match the SMT-LIBv2 standard...
2221 if(formals
.size() > 0) {
2222 Type rangeType
= FunctionType(funcType
).getRangeType();
2223 if(! formulaType
.isComparableTo(rangeType
)) {
2225 ss
<< "Type of defined function does not match its declaration\n"
2226 << "The function : " << func
<< "\n"
2227 << "Declared type : " << rangeType
<< "\n"
2228 << "The body : " << formula
<< "\n"
2229 << "Body type : " << formulaType
;
2230 throw TypeCheckingException(func
, ss
.str());
2233 if(! formulaType
.isComparableTo(funcType
)) {
2235 ss
<< "Declared type of defined constant does not match its definition\n"
2236 << "The constant : " << func
<< "\n"
2237 << "Declared type : " << funcType
<< " " << Type::getTypeNode(funcType
)->getId() << "\n"
2238 << "The definition : " << formula
<< "\n"
2239 << "Definition type: " << formulaType
<< " " << Type::getTypeNode(formulaType
)->getId();
2240 throw TypeCheckingException(func
, ss
.str());
2243 TNode funcNode
= func
.getTNode();
2244 vector
<Node
> formalsNodes
;
2245 for(vector
<Expr
>::const_iterator i
= formals
.begin(),
2246 iend
= formals
.end();
2249 formalsNodes
.push_back((*i
).getNode());
2251 TNode formNode
= form
.getTNode();
2252 DefinedFunction
def(funcNode
, formalsNodes
, formNode
);
2253 // Permit (check-sat) (define-fun ...) (get-value ...) sequences.
2254 // Otherwise, (check-sat) (get-value ((! foo :named bar))) breaks
2255 // d_haveAdditions = true;
2256 Debug("smt") << "definedFunctions insert " << funcNode
<< " " << formNode
<< endl
;
2257 d_definedFunctions
->insert(funcNode
, def
);
2260 bool SmtEngine::isDefinedFunction( Expr func
){
2261 Node nf
= Node::fromExpr( func
);
2262 Debug("smt") << "isDefined function " << nf
<< "?" << std::endl
;
2263 return d_definedFunctions
->find(nf
) != d_definedFunctions
->end();
2266 Node
SmtEnginePrivate::expandDefinitions(TNode n
, hash_map
<Node
, Node
, NodeHashFunction
>& cache
, bool expandOnly
)
2267 throw(TypeCheckingException
, LogicException
, UnsafeInterruptException
) {
2269 stack
< triple
<Node
, Node
, bool> > worklist
;
2271 worklist
.push(make_triple(Node(n
), Node(n
), false));
2272 // The worklist is made of triples, each is input / original node then the output / rewritten node
2273 // and finally a flag tracking whether the children have been explored (i.e. if this is a downward
2277 spendResource(options::preprocessStep());
2278 n
= worklist
.top().first
; // n is the input / original
2279 Node node
= worklist
.top().second
; // node is the output / result
2280 bool childrenPushed
= worklist
.top().third
;
2283 // Working downwards
2284 if(!childrenPushed
) {
2285 Kind k
= n
.getKind();
2287 // Apart from apply, we can short circuit leaves
2288 if(k
!= kind::APPLY
&& n
.getNumChildren() == 0) {
2289 SmtEngine::DefinedFunctionMap::const_iterator i
= d_smt
.d_definedFunctions
->find(n
);
2290 if(i
!= d_smt
.d_definedFunctions
->end()) {
2291 // replacement must be closed
2292 if((*i
).second
.getFormals().size() > 0) {
2293 result
.push(d_smt
.d_nodeManager
->mkNode(kind::LAMBDA
, d_smt
.d_nodeManager
->mkNode(kind::BOUND_VAR_LIST
, (*i
).second
.getFormals()), (*i
).second
.getFormula()));
2296 // don't bother putting in the cache
2297 result
.push((*i
).second
.getFormula());
2300 // don't bother putting in the cache
2305 // maybe it's in the cache
2306 hash_map
<Node
, Node
, NodeHashFunction
>::iterator cacheHit
= cache
.find(n
);
2307 if(cacheHit
!= cache
.end()) {
2308 TNode ret
= (*cacheHit
).second
;
2309 result
.push(ret
.isNull() ? n
: ret
);
2313 // otherwise expand it
2314 bool doExpand
= k
== kind::APPLY
;
2316 if( options::macrosQuant() ){
2317 //expand if we have inferred an operator corresponds to a defined function
2318 doExpand
= k
==kind::APPLY_UF
&& d_smt
.isDefinedFunction( n
.getOperator().toExpr() );
2322 vector
<Node
> formals
;
2324 if( n
.getOperator().getKind() == kind::LAMBDA
){
2325 TNode op
= n
.getOperator();
2327 for( unsigned i
=0; i
<op
[0].getNumChildren(); i
++ ){
2328 formals
.push_back( op
[0][i
] );
2332 // application of a user-defined symbol
2333 TNode func
= n
.getOperator();
2334 SmtEngine::DefinedFunctionMap::const_iterator i
= d_smt
.d_definedFunctions
->find(func
);
2335 if(i
== d_smt
.d_definedFunctions
->end()) {
2336 throw TypeCheckingException(n
.toExpr(), string("Undefined function: `") + func
.toString() + "'");
2338 DefinedFunction def
= (*i
).second
;
2339 formals
= def
.getFormals();
2341 if(Debug
.isOn("expand")) {
2342 Debug("expand") << "found: " << n
<< endl
;
2343 Debug("expand") << " func: " << func
<< endl
;
2344 string name
= func
.getAttribute(expr::VarNameAttr());
2345 Debug("expand") << " : \"" << name
<< "\"" << endl
;
2347 if(Debug
.isOn("expand")) {
2348 Debug("expand") << " defn: " << def
.getFunction() << endl
2350 if(formals
.size() > 0) {
2351 copy( formals
.begin(), formals
.end() - 1,
2352 ostream_iterator
<Node
>(Debug("expand"), ", ") );
2353 Debug("expand") << formals
.back();
2355 Debug("expand") << "]" << endl
2356 << " " << def
.getFunction().getType() << endl
2357 << " " << def
.getFormula() << endl
;
2360 fm
= def
.getFormula();
2363 Node instance
= fm
.substitute(formals
.begin(), formals
.end(),
2364 n
.begin(), n
.end());
2365 Debug("expand") << "made : " << instance
<< endl
;
2367 Node expanded
= expandDefinitions(instance
, cache
, expandOnly
);
2368 cache
[n
] = (n
== expanded
? Node::null() : expanded
);
2369 result
.push(expanded
);
2372 } else if(! expandOnly
) {
2373 // do not do any theory stuff if expandOnly is true
2375 theory::Theory
* t
= d_smt
.d_theoryEngine
->theoryOf(node
);
2378 LogicRequest
req(d_smt
);
2379 node
= t
->expandDefinition(req
, n
);
2382 // there should be children here, otherwise we short-circuited a result-push/continue, above
2383 if (node
.getNumChildren() == 0) {
2384 Debug("expand") << "Unexpectedly no children..." << node
<< endl
;
2386 // This invariant holds at the moment but it is concievable that a new theory
2387 // might introduce a kind which can have children before definition expansion but doesn't
2388 // afterwards. If this happens, remove this assertion.
2389 Assert(node
.getNumChildren() > 0);
2391 // the partial functions can fall through, in which case we still
2392 // consider their children
2393 worklist
.push(make_triple(Node(n
), node
, true)); // Original and rewritten result
2395 for(size_t i
= 0; i
< node
.getNumChildren(); ++i
) {
2396 worklist
.push(make_triple(node
[i
], node
[i
], false)); // Rewrite the children of the result only
2401 // Reconstruct the node from it's (now rewritten) children on the stack
2403 Debug("expand") << "cons : " << node
<< endl
;
2404 //cout << "cons : " << node << endl;
2405 NodeBuilder
<> nb(node
.getKind());
2406 if(node
.getMetaKind() == kind::metakind::PARAMETERIZED
) {
2407 Debug("expand") << "op : " << node
.getOperator() << endl
;
2408 //cout << "op : " << node.getOperator() << endl;
2409 nb
<< node
.getOperator();
2411 for(size_t i
= 0; i
< node
.getNumChildren(); ++i
) {
2412 Assert(!result
.empty());
2413 Node expanded
= result
.top();
2415 //cout << "exchld : " << expanded << endl;
2416 Debug("expand") << "exchld : " << expanded
<< endl
;
2420 cache
[n
] = n
== node
? Node::null() : node
; // Only cache once all subterms are expanded
2423 } while(!worklist
.empty());
2425 AlwaysAssert(result
.size() == 1);
2427 return result
.top();
2430 //TODO: clean this up
2431 struct intToBV_stack_element
{
2433 bool children_added
;
2434 intToBV_stack_element(TNode node
)
2435 : node(node
), children_added(false) {}
2436 };/* struct intToBV_stack_element */
2438 typedef std::hash_map
<Node
, Node
, NodeHashFunction
> NodeMap
;
2440 Node
SmtEnginePrivate::intToBVMakeBinary(TNode n
, NodeMap
& cache
) {
2441 // Do a topological sort of the subexpressions and substitute them
2442 vector
<intToBV_stack_element
> toVisit
;
2443 toVisit
.push_back(n
);
2445 while (!toVisit
.empty())
2447 // The current node we are processing
2448 intToBV_stack_element
& stackHead
= toVisit
.back();
2449 TNode current
= stackHead
.node
;
2451 NodeMap::iterator find
= cache
.find(current
);
2452 if (find
!= cache
.end()) {
2456 if (stackHead
.children_added
) {
2457 // Children have been processed, so rebuild this node
2459 NodeManager
* nm
= NodeManager::currentNM();
2460 if (current
.getNumChildren() > 2 && (current
.getKind() == kind::PLUS
|| current
.getKind() == kind::MULT
)) {
2461 Assert(cache
.find(current
[0]) != cache
.end());
2462 result
= cache
[current
[0]];
2463 for (unsigned i
= 1; i
< current
.getNumChildren(); ++ i
) {
2464 Assert(cache
.find(current
[i
]) != cache
.end());
2465 Node child
= current
[i
];
2466 Node childRes
= cache
[current
[i
]];
2467 result
= nm
->mkNode(current
.getKind(), result
, childRes
);
2471 NodeBuilder
<> builder(current
.getKind());
2472 for (unsigned i
= 0; i
< current
.getNumChildren(); ++ i
) {
2473 Assert(cache
.find(current
[i
]) != cache
.end());
2474 builder
<< cache
[current
[i
]];
2478 cache
[current
] = result
;
2481 // Mark that we have added the children if any
2482 if (current
.getNumChildren() > 0) {
2483 stackHead
.children_added
= true;
2484 // We need to add the children
2485 for(TNode::iterator child_it
= current
.begin(); child_it
!= current
.end(); ++ child_it
) {
2486 TNode childNode
= *child_it
;
2487 NodeMap::iterator childFind
= cache
.find(childNode
);
2488 if (childFind
== cache
.end()) {
2489 toVisit
.push_back(childNode
);
2493 cache
[current
] = current
;
2501 Node
SmtEnginePrivate::intToBV(TNode n
, NodeMap
& cache
) {
2502 int size
= options::solveIntAsBV();
2503 AlwaysAssert(size
> 0);
2504 AlwaysAssert(!options::incrementalSolving());
2506 vector
<intToBV_stack_element
> toVisit
;
2507 NodeMap binaryCache
;
2508 Node n_binary
= intToBVMakeBinary(n
, binaryCache
);
2509 toVisit
.push_back(TNode(n_binary
));
2511 while (!toVisit
.empty())
2513 // The current node we are processing
2514 intToBV_stack_element
& stackHead
= toVisit
.back();
2515 TNode current
= stackHead
.node
;
2517 // If node is already in the cache we're done, pop from the stack
2518 NodeMap::iterator find
= cache
.find(current
);
2519 if (find
!= cache
.end()) {
2524 // Not yet substituted, so process
2525 NodeManager
* nm
= NodeManager::currentNM();
2526 if (stackHead
.children_added
) {
2527 // Children have been processed, so rebuild this node
2528 vector
<Node
> children
;
2530 for (unsigned i
= 0; i
< current
.getNumChildren(); ++ i
) {
2531 Assert(cache
.find(current
[i
]) != cache
.end());
2532 TNode childRes
= cache
[current
[i
]];
2533 TypeNode type
= childRes
.getType();
2534 if (type
.isBitVector()) {
2535 unsigned bvsize
= type
.getBitVectorSize();
2540 children
.push_back(childRes
);
2543 kind::Kind_t newKind
= current
.getKind();
2547 Assert(children
.size() == 2);
2548 newKind
= kind::BITVECTOR_PLUS
;
2552 Assert(children
.size() == 2);
2553 newKind
= kind::BITVECTOR_MULT
;
2557 Assert(children
.size() == 2);
2558 newKind
= kind::BITVECTOR_SUB
;
2562 Assert(children
.size() == 1);
2563 newKind
= kind::BITVECTOR_NEG
;
2567 newKind
= kind::BITVECTOR_SLT
;
2570 newKind
= kind::BITVECTOR_SLE
;
2573 newKind
= kind::BITVECTOR_SGT
;
2576 newKind
= kind::BITVECTOR_SGE
;
2582 if (Theory::theoryOf(current
) == THEORY_BOOL
) {
2585 throw TypeCheckingException(current
.toExpr(), string("Cannot translate to BV: ") + current
.toString());
2587 for (unsigned i
= 0; i
< children
.size(); ++i
) {
2588 TypeNode type
= children
[i
].getType();
2589 if (!type
.isBitVector()) {
2592 unsigned bvsize
= type
.getBitVectorSize();
2595 Node signExtendOp
= nm
->mkConst
<BitVectorSignExtend
>(BitVectorSignExtend(max
- bvsize
));
2596 children
[i
] = nm
->mkNode(signExtendOp
, children
[i
]);
2600 NodeBuilder
<> builder(newKind
);
2601 for (unsigned i
= 0; i
< children
.size(); ++i
) {
2602 builder
<< children
[i
];
2604 // Mark the substitution and continue
2605 Node result
= builder
;
2607 result
= Rewriter::rewrite(result
);
2608 cache
[current
] = result
;
2611 // Mark that we have added the children if any
2612 if (current
.getNumChildren() > 0) {
2613 stackHead
.children_added
= true;
2614 // We need to add the children
2615 for(TNode::iterator child_it
= current
.begin(); child_it
!= current
.end(); ++ child_it
) {
2616 TNode childNode
= *child_it
;
2617 NodeMap::iterator childFind
= cache
.find(childNode
);
2618 if (childFind
== cache
.end()) {
2619 toVisit
.push_back(childNode
);
2623 // It's a leaf: could be a variable or a numeral
2624 Node result
= current
;
2625 if (current
.isVar()) {
2626 if (current
.getType() == nm
->integerType()) {
2627 result
= nm
->mkSkolem("__intToBV_var", nm
->mkBitVectorType(size
),
2628 "Variable introduced in intToBV pass");
2631 AlwaysAssert(current
.getType() == nm
->booleanType());
2634 else if (current
.isConst()) {
2635 switch (current
.getKind()) {
2636 case kind::CONST_RATIONAL
: {
2637 Rational constant
= current
.getConst
<Rational
>();
2638 AlwaysAssert(constant
.isIntegral());
2639 AlwaysAssert(constant
>= 0);
2640 BitVector
bv(size
, constant
.getNumerator());
2641 if (bv
.toSignedInt() != constant
.getNumerator()) {
2642 throw TypeCheckingException(current
.toExpr(), string("Not enough bits for constant in intToBV: ") + current
.toString());
2644 result
= nm
->mkConst(bv
);
2647 case kind::CONST_BOOLEAN
:
2650 throw TypeCheckingException(current
.toExpr(), string("Cannot translate const to BV: ") + current
.toString());
2654 throw TypeCheckingException(current
.toExpr(), string("Cannot translate to BV: ") + current
.toString());
2656 cache
[current
] = result
;
2661 return cache
[n_binary
];
2664 void SmtEnginePrivate::removeITEs() {
2665 d_smt
.finalOptionsAreSet();
2666 spendResource(options::preprocessStep());
2667 Trace("simplify") << "SmtEnginePrivate::removeITEs()" << endl
;
2669 // Remove all of the ITE occurrences and normalize
2670 d_iteRemover
.run(d_assertions
.ref(), d_iteSkolemMap
, true);
2671 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
2672 d_assertions
.replace(i
, Rewriter::rewrite(d_assertions
[i
]));
2676 void SmtEnginePrivate::staticLearning() {
2677 d_smt
.finalOptionsAreSet();
2678 spendResource(options::preprocessStep());
2680 TimerStat::CodeTimer
staticLearningTimer(d_smt
.d_stats
->d_staticLearningTime
);
2682 Trace("simplify") << "SmtEnginePrivate::staticLearning()" << endl
;
2684 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
2686 NodeBuilder
<> learned(kind::AND
);
2687 learned
<< d_assertions
[i
];
2688 d_smt
.d_theoryEngine
->ppStaticLearn(d_assertions
[i
], learned
);
2689 if(learned
.getNumChildren() == 1) {
2692 d_assertions
.replace(i
, learned
);
2697 // do dumping (before/after any preprocessing pass)
2698 static void dumpAssertions(const char* key
, const AssertionPipeline
& assertionList
) {
2699 if( Dump
.isOn("assertions") &&
2700 Dump
.isOn(string("assertions:") + key
) ) {
2701 // Push the simplified assertions to the dump output stream
2702 for(unsigned i
= 0; i
< assertionList
.size(); ++ i
) {
2703 TNode n
= assertionList
[i
];
2704 Dump("assertions") << AssertCommand(Expr(n
.toExpr()));
2709 // returns false if it learns a conflict
2710 bool SmtEnginePrivate::nonClausalSimplify() {
2711 spendResource(options::preprocessStep());
2712 d_smt
.finalOptionsAreSet();
2714 if(options::unsatCores() || options::fewerPreprocessingHoles()) {
2718 TimerStat::CodeTimer
nonclausalTimer(d_smt
.d_stats
->d_nonclausalSimplificationTime
);
2720 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify()" << endl
;
2721 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
2722 Trace("simplify") << "Assertion #" << i
<< " : " << d_assertions
[i
] << std::endl
;
2725 if(d_propagatorNeedsFinish
) {
2726 d_propagator
.finish();
2727 d_propagatorNeedsFinish
= false;
2729 d_propagator
.initialize();
2731 // Assert all the assertions to the propagator
2732 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
2733 << "asserting to propagator" << endl
;
2734 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
2735 Assert(Rewriter::rewrite(d_assertions
[i
]) == d_assertions
[i
]);
2736 // Don't reprocess substitutions
2737 if (d_substitutionsIndex
> 0 && i
== d_substitutionsIndex
) {
2740 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): asserting " << d_assertions
[i
] << endl
;
2741 Debug("cores") << "d_propagator assertTrue: " << d_assertions
[i
] << std::endl
;
2742 d_propagator
.assertTrue(d_assertions
[i
]);
2745 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
2746 << "propagating" << endl
;
2747 if (d_propagator
.propagate()) {
2748 // If in conflict, just return false
2749 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
2750 << "conflict in non-clausal propagation" << endl
;
2751 Node falseNode
= NodeManager::currentNM()->mkConst
<bool>(false);
2752 Assert(!options::unsatCores() && !options::fewerPreprocessingHoles());
2753 d_assertions
.clear();
2754 addFormula(falseNode
, false, false);
2755 d_propagatorNeedsFinish
= true;
2760 Trace("simplify") << "Iterate through " << d_nonClausalLearnedLiterals
.size() << " learned literals." << std::endl
;
2761 // No conflict, go through the literals and solve them
2762 SubstitutionMap
constantPropagations(d_smt
.d_context
);
2763 SubstitutionMap
newSubstitutions(d_smt
.d_context
);
2764 SubstitutionMap::iterator pos
;
2766 for(unsigned i
= 0, i_end
= d_nonClausalLearnedLiterals
.size(); i
< i_end
; ++ i
) {
2767 // Simplify the literal we learned wrt previous substitutions
2768 Node learnedLiteral
= d_nonClausalLearnedLiterals
[i
];
2769 Assert(Rewriter::rewrite(learnedLiteral
) == learnedLiteral
);
2770 Assert(d_topLevelSubstitutions
.apply(learnedLiteral
) == learnedLiteral
);
2771 Trace("simplify") << "Process learnedLiteral : " << learnedLiteral
<< std::endl
;
2772 Node learnedLiteralNew
= newSubstitutions
.apply(learnedLiteral
);
2773 if (learnedLiteral
!= learnedLiteralNew
) {
2774 learnedLiteral
= Rewriter::rewrite(learnedLiteralNew
);
2776 Trace("simplify") << "Process learnedLiteral, after newSubs : " << learnedLiteral
<< std::endl
;
2778 learnedLiteralNew
= constantPropagations
.apply(learnedLiteral
);
2779 if (learnedLiteralNew
== learnedLiteral
) {
2782 ++d_smt
.d_stats
->d_numConstantProps
;
2783 learnedLiteral
= Rewriter::rewrite(learnedLiteralNew
);
2785 Trace("simplify") << "Process learnedLiteral, after constProp : " << learnedLiteral
<< std::endl
;
2786 // It might just simplify to a constant
2787 if (learnedLiteral
.isConst()) {
2788 if (learnedLiteral
.getConst
<bool>()) {
2789 // If the learned literal simplifies to true, it's redundant
2792 // If the learned literal simplifies to false, we're in conflict
2793 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
2795 << d_nonClausalLearnedLiterals
[i
] << endl
;
2796 Assert(!options::unsatCores());
2797 d_assertions
.clear();
2798 addFormula(NodeManager::currentNM()->mkConst
<bool>(false), false, false);
2799 d_propagatorNeedsFinish
= true;
2804 // Solve it with the corresponding theory, possibly adding new
2805 // substitutions to newSubstitutions
2806 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
2807 << "solving " << learnedLiteral
<< endl
;
2809 Theory::PPAssertStatus solveStatus
=
2810 d_smt
.d_theoryEngine
->solve(learnedLiteral
, newSubstitutions
);
2812 switch (solveStatus
) {
2813 case Theory::PP_ASSERT_STATUS_SOLVED
: {
2814 // The literal should rewrite to true
2815 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
2816 << "solved " << learnedLiteral
<< endl
;
2817 Assert(Rewriter::rewrite(newSubstitutions
.apply(learnedLiteral
)).isConst());
2818 // vector<pair<Node, Node> > equations;
2819 // constantPropagations.simplifyLHS(d_topLevelSubstitutions, equations, true);
2820 // if (equations.empty()) {
2823 // Assert(equations[0].first.isConst() && equations[0].second.isConst() && equations[0].first != equations[0].second);
2824 // else fall through
2827 case Theory::PP_ASSERT_STATUS_CONFLICT
:
2828 // If in conflict, we return false
2829 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
2830 << "conflict while solving "
2831 << learnedLiteral
<< endl
;
2832 Assert(!options::unsatCores());
2833 d_assertions
.clear();
2834 addFormula(NodeManager::currentNM()->mkConst
<bool>(false), false, false);
2835 d_propagatorNeedsFinish
= true;
2838 if (d_doConstantProp
&& learnedLiteral
.getKind() == kind::EQUAL
&& (learnedLiteral
[0].isConst() || learnedLiteral
[1].isConst())) {
2839 // constant propagation
2842 if (learnedLiteral
[0].isConst()) {
2843 t
= learnedLiteral
[1];
2844 c
= learnedLiteral
[0];
2847 t
= learnedLiteral
[0];
2848 c
= learnedLiteral
[1];
2850 Assert(!t
.isConst());
2851 Assert(constantPropagations
.apply(t
) == t
);
2852 Assert(d_topLevelSubstitutions
.apply(t
) == t
);
2853 Assert(newSubstitutions
.apply(t
) == t
);
2854 constantPropagations
.addSubstitution(t
, c
);
2855 // vector<pair<Node,Node> > equations;
2856 // constantPropagations.simplifyLHS(t, c, equations, true);
2857 // if (!equations.empty()) {
2858 // Assert(equations[0].first.isConst() && equations[0].second.isConst() && equations[0].first != equations[0].second);
2859 // d_assertions.clear();
2860 // addFormula(NodeManager::currentNM()->mkConst<bool>(false), false, false);
2863 // d_topLevelSubstitutions.simplifyRHS(constantPropagations);
2867 d_nonClausalLearnedLiterals
[j
++] = d_nonClausalLearnedLiterals
[i
];
2872 #ifdef CVC4_ASSERTIONS
2873 // Check data structure invariants:
2874 // 1. for each lhs of d_topLevelSubstitutions, does not appear anywhere in rhs of d_topLevelSubstitutions or anywhere in constantPropagations
2875 // 2. each lhs of constantPropagations rewrites to itself
2876 // 3. if l -> r is a constant propagation and l is a subterm of l' with l' -> r' another constant propagation, then l'[l/r] -> r' should be a
2877 // constant propagation too
2878 // 4. each lhs of constantPropagations is different from each rhs
2879 for (pos
= newSubstitutions
.begin(); pos
!= newSubstitutions
.end(); ++pos
) {
2880 Assert((*pos
).first
.isVar());
2881 Assert(d_topLevelSubstitutions
.apply((*pos
).first
) == (*pos
).first
);
2882 Assert(d_topLevelSubstitutions
.apply((*pos
).second
) == (*pos
).second
);
2883 Assert(newSubstitutions
.apply(newSubstitutions
.apply((*pos
).second
)) == newSubstitutions
.apply((*pos
).second
));
2885 for (pos
= constantPropagations
.begin(); pos
!= constantPropagations
.end(); ++pos
) {
2886 Assert((*pos
).second
.isConst());
2887 Assert(Rewriter::rewrite((*pos
).first
) == (*pos
).first
);
2888 // Node newLeft = d_topLevelSubstitutions.apply((*pos).first);
2889 // if (newLeft != (*pos).first) {
2890 // newLeft = Rewriter::rewrite(newLeft);
2891 // Assert(newLeft == (*pos).second ||
2892 // (constantPropagations.hasSubstitution(newLeft) && constantPropagations.apply(newLeft) == (*pos).second));
2894 // newLeft = constantPropagations.apply((*pos).first);
2895 // if (newLeft != (*pos).first) {
2896 // newLeft = Rewriter::rewrite(newLeft);
2897 // Assert(newLeft == (*pos).second ||
2898 // (constantPropagations.hasSubstitution(newLeft) && constantPropagations.apply(newLeft) == (*pos).second));
2900 Assert(constantPropagations
.apply((*pos
).second
) == (*pos
).second
);
2902 #endif /* CVC4_ASSERTIONS */
2904 // Resize the learnt
2905 Trace("simplify") << "Resize non-clausal learned literals to " << j
<< std::endl
;
2906 d_nonClausalLearnedLiterals
.resize(j
);
2908 hash_set
<TNode
, TNodeHashFunction
> s
;
2909 Trace("debugging") << "NonClausal simplify pre-preprocess\n";
2910 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
2911 Node assertion
= d_assertions
[i
];
2912 Node assertionNew
= newSubstitutions
.apply(assertion
);
2913 Trace("debugging") << "assertion = " << assertion
<< endl
;
2914 Trace("debugging") << "assertionNew = " << assertionNew
<< endl
;
2915 if (assertion
!= assertionNew
) {
2916 assertion
= Rewriter::rewrite(assertionNew
);
2917 Trace("debugging") << "rewrite(assertion) = " << assertion
<< endl
;
2919 Assert(Rewriter::rewrite(assertion
) == assertion
);
2921 assertionNew
= constantPropagations
.apply(assertion
);
2922 if (assertionNew
== assertion
) {
2925 ++d_smt
.d_stats
->d_numConstantProps
;
2926 Trace("debugging") << "assertionNew = " << assertionNew
<< endl
;
2927 assertion
= Rewriter::rewrite(assertionNew
);
2928 Trace("debugging") << "assertionNew = " << assertionNew
<< endl
;
2930 Trace("debugging") << "\n";
2931 s
.insert(assertion
);
2932 d_assertions
.replace(i
, assertion
);
2933 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
2934 << "non-clausal preprocessed: "
2935 << assertion
<< endl
;
2938 // If in incremental mode, add substitutions to the list of assertions
2939 if (d_substitutionsIndex
> 0) {
2940 NodeBuilder
<> substitutionsBuilder(kind::AND
);
2941 substitutionsBuilder
<< d_assertions
[d_substitutionsIndex
];
2942 pos
= newSubstitutions
.begin();
2943 for (; pos
!= newSubstitutions
.end(); ++pos
) {
2944 // Add back this substitution as an assertion
2945 TNode lhs
= (*pos
).first
, rhs
= newSubstitutions
.apply((*pos
).second
);
2946 Node n
= NodeManager::currentNM()->mkNode(kind::EQUAL
, lhs
, rhs
);
2947 substitutionsBuilder
<< n
;
2948 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): will notify SAT layer of substitution: " << n
<< endl
;
2950 if (substitutionsBuilder
.getNumChildren() > 1) {
2951 d_assertions
.replace(d_substitutionsIndex
,
2952 Rewriter::rewrite(Node(substitutionsBuilder
)));
2955 // If not in incremental mode, must add substitutions to model
2956 TheoryModel
* m
= d_smt
.d_theoryEngine
->getModel();
2958 for(pos
= newSubstitutions
.begin(); pos
!= newSubstitutions
.end(); ++pos
) {
2959 Node n
= (*pos
).first
;
2960 Node v
= newSubstitutions
.apply((*pos
).second
);
2961 Trace("model") << "Add substitution : " << n
<< " " << v
<< endl
;
2962 m
->addSubstitution( n
, v
);
2967 NodeBuilder
<> learnedBuilder(kind::AND
);
2968 Assert(d_realAssertionsEnd
<= d_assertions
.size());
2969 learnedBuilder
<< d_assertions
[d_realAssertionsEnd
- 1];
2971 for (unsigned i
= 0; i
< d_nonClausalLearnedLiterals
.size(); ++ i
) {
2972 Node learned
= d_nonClausalLearnedLiterals
[i
];
2973 Assert(d_topLevelSubstitutions
.apply(learned
) == learned
);
2974 Node learnedNew
= newSubstitutions
.apply(learned
);
2975 if (learned
!= learnedNew
) {
2976 learned
= Rewriter::rewrite(learnedNew
);
2978 Assert(Rewriter::rewrite(learned
) == learned
);
2980 learnedNew
= constantPropagations
.apply(learned
);
2981 if (learnedNew
== learned
) {
2984 ++d_smt
.d_stats
->d_numConstantProps
;
2985 learned
= Rewriter::rewrite(learnedNew
);
2987 if (s
.find(learned
) != s
.end()) {
2991 learnedBuilder
<< learned
;
2992 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
2993 << "non-clausal learned : "
2996 d_nonClausalLearnedLiterals
.clear();
2998 for (pos
= constantPropagations
.begin(); pos
!= constantPropagations
.end(); ++pos
) {
2999 Node cProp
= (*pos
).first
.eqNode((*pos
).second
);
3000 Assert(d_topLevelSubstitutions
.apply(cProp
) == cProp
);
3001 Node cPropNew
= newSubstitutions
.apply(cProp
);
3002 if (cProp
!= cPropNew
) {
3003 cProp
= Rewriter::rewrite(cPropNew
);
3004 Assert(Rewriter::rewrite(cProp
) == cProp
);
3006 if (s
.find(cProp
) != s
.end()) {
3010 learnedBuilder
<< cProp
;
3011 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
3012 << "non-clausal constant propagation : "
3016 // Add new substitutions to topLevelSubstitutions
3017 // Note that we don't have to keep rhs's in full solved form
3018 // because SubstitutionMap::apply does a fixed-point iteration when substituting
3019 d_topLevelSubstitutions
.addSubstitutions(newSubstitutions
);
3021 if(learnedBuilder
.getNumChildren() > 1) {
3022 d_assertions
.replace(d_realAssertionsEnd
- 1,
3023 Rewriter::rewrite(Node(learnedBuilder
)));
3026 d_propagatorNeedsFinish
= true;
3030 void SmtEnginePrivate::bvAbstraction() {
3031 Trace("bv-abstraction") << "SmtEnginePrivate::bvAbstraction()" << endl
;
3032 std::vector
<Node
> new_assertions
;
3033 bool changed
= d_smt
.d_theoryEngine
->ppBvAbstraction(d_assertions
.ref(), new_assertions
);
3034 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
3035 d_assertions
.replace(i
, Rewriter::rewrite(new_assertions
[i
]));
3037 // if we are using the lazy solver and the abstraction
3038 // applies, then UF symbols were introduced
3039 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY
&&
3041 LogicRequest
req(d_smt
);
3042 req
.widenLogic(THEORY_UF
);
3047 void SmtEnginePrivate::bvToBool() {
3048 Trace("bv-to-bool") << "SmtEnginePrivate::bvToBool()" << endl
;
3049 spendResource(options::preprocessStep());
3050 std::vector
<Node
> new_assertions
;
3051 d_smt
.d_theoryEngine
->ppBvToBool(d_assertions
.ref(), new_assertions
);
3052 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
3053 d_assertions
.replace(i
, Rewriter::rewrite(new_assertions
[i
]));
3057 void SmtEnginePrivate::boolToBv() {
3058 Trace("bool-to-bv") << "SmtEnginePrivate::boolToBv()" << endl
;
3059 spendResource(options::preprocessStep());
3060 std::vector
<Node
> new_assertions
;
3061 d_smt
.d_theoryEngine
->ppBoolToBv(d_assertions
.ref(), new_assertions
);
3062 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
3063 d_assertions
.replace(i
, Rewriter::rewrite(new_assertions
[i
]));
3067 bool SmtEnginePrivate::simpITE() {
3068 TimerStat::CodeTimer
simpITETimer(d_smt
.d_stats
->d_simpITETime
);
3070 spendResource(options::preprocessStep());
3072 Trace("simplify") << "SmtEnginePrivate::simpITE()" << endl
;
3074 unsigned numAssertionOnEntry
= d_assertions
.size();
3075 for (unsigned i
= 0; i
< d_assertions
.size(); ++i
) {
3076 spendResource(options::preprocessStep());
3077 Node result
= d_smt
.d_theoryEngine
->ppSimpITE(d_assertions
[i
]);
3078 d_assertions
.replace(i
, result
);
3079 if(result
.isConst() && !result
.getConst
<bool>()){
3083 bool result
= d_smt
.d_theoryEngine
->donePPSimpITE(d_assertions
.ref());
3084 if(numAssertionOnEntry
< d_assertions
.size()){
3085 compressBeforeRealAssertions(numAssertionOnEntry
);
3090 void SmtEnginePrivate::compressBeforeRealAssertions(size_t before
){
3091 size_t curr
= d_assertions
.size();
3092 if(before
>= curr
||
3093 d_realAssertionsEnd
<= 0 ||
3094 d_realAssertionsEnd
>= curr
){
3099 // original: [0 ... d_realAssertionsEnd)
3101 // ites skolems [d_realAssertionsEnd, before)
3103 // added [before, curr)
3105 Assert(0 < d_realAssertionsEnd
);
3106 Assert(d_realAssertionsEnd
<= before
);
3107 Assert(before
< curr
);
3109 std::vector
<Node
> intoConjunction
;
3110 for(size_t i
= before
; i
<curr
; ++i
){
3111 intoConjunction
.push_back(d_assertions
[i
]);
3113 d_assertions
.resize(before
);
3114 size_t lastBeforeItes
= d_realAssertionsEnd
- 1;
3115 intoConjunction
.push_back(d_assertions
[lastBeforeItes
]);
3116 Node newLast
= util::NaryBuilder::mkAssoc(kind::AND
, intoConjunction
);
3117 d_assertions
.replace(lastBeforeItes
, newLast
);
3118 Assert(d_assertions
.size() == before
);
3121 void SmtEnginePrivate::unconstrainedSimp() {
3122 TimerStat::CodeTimer
unconstrainedSimpTimer(d_smt
.d_stats
->d_unconstrainedSimpTime
);
3123 spendResource(options::preprocessStep());
3124 Trace("simplify") << "SmtEnginePrivate::unconstrainedSimp()" << endl
;
3125 d_smt
.d_theoryEngine
->ppUnconstrainedSimp(d_assertions
.ref());
3129 void SmtEnginePrivate::constrainSubtypes(TNode top
, AssertionPipeline
& assertions
)
3132 Trace("constrainSubtypes") << "constrainSubtypes(): looking at " << top
<< endl
;
3135 stack
<TNode
> worklist
;
3140 TNode n
= worklist
.top();
3143 TypeNode t
= n
.getType();
3144 if(t
.isPredicateSubtype()) {
3145 WarningOnce() << "Warning: CVC4 doesn't yet do checking that predicate subtypes are nonempty domains" << endl
;
3146 Node pred
= t
.getSubtypePredicate();
3148 // pred can be a LAMBDA, a function constant, or a datatype tester
3149 Trace("constrainSubtypes") << "constrainSubtypes(): pred.getType() == " << pred
.getType() << endl
;
3150 if(d_smt
.d_definedFunctions
->find(pred
) != d_smt
.d_definedFunctions
->end()) {
3152 } else if(pred
.getType().isTester()) {
3153 k
= kind::APPLY_TESTER
;
3157 Node app
= NodeManager::currentNM()->mkNode(k
, pred
, n
);
3158 Trace("constrainSubtypes") << "constrainSubtypes(): assert(" << k
<< ") " << app
<< endl
;
3159 assertions
.push_back(app
);
3160 } else if(t
.isSubrange()) {
3161 SubrangeBounds bounds
= t
.getSubrangeBounds();
3162 Trace("constrainSubtypes") << "constrainSubtypes(): got bounds " << bounds
<< endl
;
3163 if(bounds
.lower
.hasBound()) {
3164 Node c
= NodeManager::currentNM()->mkConst(Rational(bounds
.lower
.getBound()));
3165 Node lb
= NodeManager::currentNM()->mkNode(kind::LEQ
, c
, n
);
3166 Trace("constrainSubtypes") << "constrainSubtypes(): assert " << lb
<< endl
;
3167 assertions
.push_back(lb
);
3169 if(bounds
.upper
.hasBound()) {
3170 Node c
= NodeManager::currentNM()->mkConst(Rational(bounds
.upper
.getBound()));
3171 Node ub
= NodeManager::currentNM()->mkNode(kind::LEQ
, n
, c
);
3172 Trace("constrainSubtypes") << "constrainSubtypes(): assert " << ub
<< endl
;
3173 assertions
.push_back(ub
);
3177 for(TNode::iterator i
= n
.begin(); i
!= n
.end(); ++i
) {
3178 if(done
.find(*i
) == done
.end()) {
3183 } while(! worklist
.empty());
3186 void SmtEnginePrivate::traceBackToAssertions(const std::vector
<Node
>& nodes
, std::vector
<TNode
>& assertions
) {
3187 const booleans::CircuitPropagator::BackEdgesMap
& backEdges
= d_propagator
.getBackEdges();
3188 for(vector
<Node
>::const_iterator i
= nodes
.begin(); i
!= nodes
.end(); ++i
) {
3189 booleans::CircuitPropagator::BackEdgesMap::const_iterator j
= backEdges
.find(*i
);
3190 // term must appear in map, otherwise how did we get here?!
3191 Assert(j
!= backEdges
.end());
3192 // if term maps to empty, that means it's a top-level assertion
3193 if(!(*j
).second
.empty()) {
3194 traceBackToAssertions((*j
).second
, assertions
);
3196 assertions
.push_back(*i
);
3201 size_t SmtEnginePrivate::removeFromConjunction(Node
& n
, const std::hash_set
<unsigned long>& toRemove
) {
3202 Assert(n
.getKind() == kind::AND
);
3203 size_t removals
= 0;
3204 for(Node::iterator j
= n
.begin(); j
!= n
.end(); ++j
) {
3205 size_t subremovals
= 0;
3207 if(toRemove
.find(sub
.getId()) != toRemove
.end() ||
3208 (sub
.getKind() == kind::AND
&& (subremovals
= removeFromConjunction(sub
, toRemove
)) > 0)) {
3209 NodeBuilder
<> b(kind::AND
);
3210 b
.append(n
.begin(), j
);
3211 if(subremovals
> 0) {
3212 removals
+= subremovals
;
3217 for(++j
; j
!= n
.end(); ++j
) {
3218 if(toRemove
.find((*j
).getId()) != toRemove
.end()) {
3220 } else if((*j
).getKind() == kind::AND
) {
3222 if((subremovals
= removeFromConjunction(sub
, toRemove
)) > 0) {
3223 removals
+= subremovals
;
3232 if(b
.getNumChildren() == 0) {
3235 } else if(b
.getNumChildren() == 1) {
3241 n
= Rewriter::rewrite(n
);
3246 Assert(removals
== 0);
3250 void SmtEnginePrivate::doMiplibTrick() {
3251 Assert(d_realAssertionsEnd
== d_assertions
.size());
3252 Assert(!options::incrementalSolving());
3254 const booleans::CircuitPropagator::BackEdgesMap
& backEdges
= d_propagator
.getBackEdges();
3255 hash_set
<unsigned long> removeAssertions
;
3257 NodeManager
* nm
= NodeManager::currentNM();
3258 Node zero
= nm
->mkConst(Rational(0)), one
= nm
->mkConst(Rational(1));
3260 hash_map
<TNode
, Node
, TNodeHashFunction
> intVars
;
3261 for(vector
<Node
>::const_iterator i
= d_boolVars
.begin(); i
!= d_boolVars
.end(); ++i
) {
3262 if(d_propagator
.isAssigned(*i
)) {
3263 Debug("miplib") << "ineligible: " << *i
<< " because assigned " << d_propagator
.getAssignment(*i
) << endl
;
3267 vector
<TNode
> assertions
;
3268 booleans::CircuitPropagator::BackEdgesMap::const_iterator j
= backEdges
.find(*i
);
3269 // if not in back edges map, the bool var is unconstrained, showing up in no assertions.
3270 // if maps to an empty vector, that means the bool var was asserted itself.
3271 if(j
!= backEdges
.end()) {
3272 if(!(*j
).second
.empty()) {
3273 traceBackToAssertions((*j
).second
, assertions
);
3275 assertions
.push_back(*i
);
3278 Debug("miplib") << "for " << *i
<< endl
;
3279 bool eligible
= true;
3280 map
<pair
<Node
, Node
>, uint64_t> marks
;
3281 map
<pair
<Node
, Node
>, vector
<Rational
> > coef
;
3282 map
<pair
<Node
, Node
>, vector
<Rational
> > checks
;
3283 map
<pair
<Node
, Node
>, vector
<TNode
> > asserts
;
3284 for(vector
<TNode
>::const_iterator j
= assertions
.begin(); j
!= assertions
.end(); ++j
) {
3285 Debug("miplib") << " found: " << *j
<< endl
;
3286 if((*j
).getKind() != kind::IMPLIES
) {
3288 Debug("miplib") << " -- INELIGIBLE -- (not =>)" << endl
;
3291 Node conj
= BooleanSimplification::simplify((*j
)[0]);
3292 if(conj
.getKind() == kind::AND
&& conj
.getNumChildren() > 6) {
3294 Debug("miplib") << " -- INELIGIBLE -- (N-ary /\\ too big)" << endl
;
3297 if(conj
.getKind() != kind::AND
&& !conj
.isVar() && !(conj
.getKind() == kind::NOT
&& conj
[0].isVar())) {
3299 Debug("miplib") << " -- INELIGIBLE -- (not /\\ or literal)" << endl
;
3302 if((*j
)[1].getKind() != kind::EQUAL
||
3303 !( ( (*j
)[1][0].isVar() &&
3304 (*j
)[1][1].getKind() == kind::CONST_RATIONAL
) ||
3305 ( (*j
)[1][0].getKind() == kind::CONST_RATIONAL
&&
3306 (*j
)[1][1].isVar() ) )) {
3308 Debug("miplib") << " -- INELIGIBLE -- (=> (and X X) X)" << endl
;
3311 if(conj
.getKind() == kind::AND
) {
3313 bool found_x
= false;
3314 map
<TNode
, bool> neg
;
3315 for(Node::iterator ii
= conj
.begin(); ii
!= conj
.end(); ++ii
) {
3317 posv
.push_back(*ii
);
3319 found_x
= found_x
|| *i
== *ii
;
3320 } else if((*ii
).getKind() == kind::NOT
&& (*ii
)[0].isVar()) {
3321 posv
.push_back((*ii
)[0]);
3322 neg
[(*ii
)[0]] = true;
3323 found_x
= found_x
|| *i
== (*ii
)[0];
3326 Debug("miplib") << " -- INELIGIBLE -- (non-var: " << *ii
<< ")" << endl
;
3329 if(d_propagator
.isAssigned(posv
.back())) {
3331 Debug("miplib") << " -- INELIGIBLE -- (" << posv
.back() << " asserted)" << endl
;
3340 Debug("miplib") << " --INELIGIBLE -- (couldn't find " << *i
<< " in conjunction)" << endl
;
3343 sort(posv
.begin(), posv
.end());
3344 const Node pos
= NodeManager::currentNM()->mkNode(kind::AND
, posv
);
3345 const TNode var
= ((*j
)[1][0].getKind() == kind::CONST_RATIONAL
) ? (*j
)[1][1] : (*j
)[1][0];
3346 const pair
<Node
, Node
> pos_var(pos
, var
);
3347 const Rational
& constant
= ((*j
)[1][0].getKind() == kind::CONST_RATIONAL
) ? (*j
)[1][0].getConst
<Rational
>() : (*j
)[1][1].getConst
<Rational
>();
3349 unsigned countneg
= 0, thepos
= 0;
3350 for(unsigned ii
= 0; ii
< pos
.getNumChildren(); ++ii
) {
3355 mark
|= (0x1 << ii
);
3358 if((marks
[pos_var
] & (1lu << mark
)) != 0) {
3360 Debug("miplib") << " -- INELIGIBLE -- (remarked)" << endl
;
3363 Debug("miplib") << "mark is " << mark
<< " -- " << (1lu << mark
) << endl
;
3364 marks
[pos_var
] |= (1lu << mark
);
3365 Debug("miplib") << "marks[" << pos
<< "," << var
<< "] now " << marks
[pos_var
] << endl
;
3366 if(countneg
== pos
.getNumChildren()) {
3369 Debug("miplib") << " -- INELIGIBLE -- (nonzero constant)" << endl
;
3372 } else if(countneg
== pos
.getNumChildren() - 1) {
3373 Assert(coef
[pos_var
].size() <= 6 && thepos
< 6);
3374 if(coef
[pos_var
].size() <= thepos
) {
3375 coef
[pos_var
].resize(thepos
+ 1);
3377 coef
[pos_var
][thepos
] = constant
;
3379 if(checks
[pos_var
].size() <= mark
) {
3380 checks
[pos_var
].resize(mark
+ 1);
3382 checks
[pos_var
][mark
] = constant
;
3384 asserts
[pos_var
].push_back(*j
);
3387 if(x
!= *i
&& x
!= (*i
).notNode()) {
3389 Debug("miplib") << " -- INELIGIBLE -- (x not present where I expect it)" << endl
;
3392 const bool xneg
= (x
.getKind() == kind::NOT
);
3393 x
= xneg
? x
[0] : x
;
3394 Debug("miplib") << " x:" << x
<< " " << xneg
<< endl
;
3395 const TNode var
= ((*j
)[1][0].getKind() == kind::CONST_RATIONAL
) ? (*j
)[1][1] : (*j
)[1][0];
3396 const pair
<Node
, Node
> x_var(x
, var
);
3397 const Rational
& constant
= ((*j
)[1][0].getKind() == kind::CONST_RATIONAL
) ? (*j
)[1][0].getConst
<Rational
>() : (*j
)[1][1].getConst
<Rational
>();
3398 unsigned mark
= (xneg
? 0 : 1);
3399 if((marks
[x_var
] & (1u << mark
)) != 0) {
3401 Debug("miplib") << " -- INELIGIBLE -- (remarked)" << endl
;
3404 marks
[x_var
] |= (1u << mark
);
3408 Debug("miplib") << " -- INELIGIBLE -- (nonzero constant)" << endl
;
3412 Assert(coef
[x_var
].size() <= 6);
3413 coef
[x_var
].resize(6);
3414 coef
[x_var
][0] = constant
;
3416 asserts
[x_var
].push_back(*j
);
3420 for(map
<pair
<Node
, Node
>, uint64_t>::const_iterator j
= marks
.begin(); j
!= marks
.end(); ++j
) {
3421 const TNode pos
= (*j
).first
.first
;
3422 const TNode var
= (*j
).first
.second
;
3423 const pair
<Node
, Node
>& pos_var
= (*j
).first
;
3424 const uint64_t mark
= (*j
).second
;
3425 const unsigned numVars
= pos
.getKind() == kind::AND
? pos
.getNumChildren() : 1;
3426 uint64_t expected
= (uint64_t(1) << (1 << numVars
)) - 1;
3427 expected
= (expected
== 0) ? -1 : expected
; // fix for overflow
3428 Debug("miplib") << "[" << pos
<< "] => " << hex
<< mark
<< " expect " << expected
<< dec
<< endl
;
3429 Assert(pos
.getKind() == kind::AND
|| pos
.isVar());
3430 if(mark
!= expected
) {
3431 Debug("miplib") << " -- INELIGIBLE " << pos
<< " -- (insufficiently marked, got " << mark
<< " for " << numVars
<< " vars, expected " << expected
<< endl
;
3433 if(mark
!= 3) { // exclude single-var case; nothing to check there
3434 uint64_t sz
= (uint64_t(1) << checks
[pos_var
].size()) - 1;
3435 sz
= (sz
== 0) ? -1 : sz
; // fix for overflow
3436 Assert(sz
== mark
, "expected size %u == mark %u", sz
, mark
);
3437 for(size_t k
= 0; k
< checks
[pos_var
].size(); ++k
) {
3438 if((k
& (k
- 1)) != 0) {
3440 Debug("miplib") << k
<< " => " << checks
[pos_var
][k
] << endl
;
3441 for(size_t v
= 1, kk
= k
; kk
!= 0; ++v
, kk
>>= 1) {
3442 if((kk
& 0x1) == 1) {
3443 Assert(pos
.getKind() == kind::AND
);
3444 Debug("miplib") << "var " << v
<< " : " << pos
[v
- 1] << " coef:" << coef
[pos_var
][v
- 1] << endl
;
3445 sum
+= coef
[pos_var
][v
- 1];
3448 Debug("miplib") << "checkSum is " << sum
<< " input says " << checks
[pos_var
][k
] << endl
;
3449 if(sum
!= checks
[pos_var
][k
]) {
3451 Debug("miplib") << " -- INELIGIBLE " << pos
<< " -- (nonlinear combination)" << endl
;
3455 Assert(checks
[pos_var
][k
] == 0, "checks[(%s,%s)][%u] should be 0, but it's %s", pos
.toString().c_str(), var
.toString().c_str(), k
, checks
[pos_var
][k
].toString().c_str()); // we never set for single-positive-var
3460 eligible
= true; // next is still eligible
3464 Debug("miplib") << " -- ELIGIBLE " << *i
<< " , " << pos
<< " --" << endl
;
3465 vector
<Node
> newVars
;
3466 expr::NodeSelfIterator ii
, iiend
;
3467 if(pos
.getKind() == kind::AND
) {
3471 ii
= expr::NodeSelfIterator::self(pos
);
3472 iiend
= expr::NodeSelfIterator::selfEnd(pos
);
3474 for(; ii
!= iiend
; ++ii
) {
3475 Node
& varRef
= intVars
[*ii
];
3476 if(varRef
.isNull()) {
3478 ss
<< "mipvar_" << *ii
;
3479 Node newVar
= nm
->mkSkolem(ss
.str(), nm
->integerType(), "a variable introduced due to scrubbing a miplib encoding", NodeManager::SKOLEM_EXACT_NAME
);
3480 Node geq
= Rewriter::rewrite(nm
->mkNode(kind::GEQ
, newVar
, zero
));
3481 Node leq
= Rewriter::rewrite(nm
->mkNode(kind::LEQ
, newVar
, one
));
3482 addFormula(Rewriter::rewrite(geq
.andNode(leq
)), false, false);
3483 SubstitutionMap
nullMap(&d_fakeContext
);
3484 Theory::PPAssertStatus status CVC4_UNUSED
; // just for assertions
3485 status
= d_smt
.d_theoryEngine
->solve(geq
, nullMap
);
3486 Assert(status
== Theory::PP_ASSERT_STATUS_UNSOLVED
,
3487 "unexpected solution from arith's ppAssert()");
3488 Assert(nullMap
.empty(),
3489 "unexpected substitution from arith's ppAssert()");
3490 status
= d_smt
.d_theoryEngine
->solve(leq
, nullMap
);
3491 Assert(status
== Theory::PP_ASSERT_STATUS_UNSOLVED
,
3492 "unexpected solution from arith's ppAssert()");
3493 Assert(nullMap
.empty(),
3494 "unexpected substitution from arith's ppAssert()");
3495 d_smt
.d_theoryEngine
->getModel()->addSubstitution(*ii
, newVar
.eqNode(one
));
3496 newVars
.push_back(newVar
);
3499 newVars
.push_back(varRef
);
3501 if(!d_smt
.d_logic
.areIntegersUsed()) {
3502 d_smt
.d_logic
= d_smt
.d_logic
.getUnlockedCopy();
3503 d_smt
.d_logic
.enableIntegers();
3504 d_smt
.d_logic
.lock();
3508 if(pos
.getKind() == kind::AND
) {
3509 NodeBuilder
<> sumb(kind::PLUS
);
3510 for(size_t ii
= 0; ii
< pos
.getNumChildren(); ++ii
) {
3511 sumb
<< nm
->mkNode(kind::MULT
, nm
->mkConst(coef
[pos_var
][ii
]), newVars
[ii
]);
3515 sum
= nm
->mkNode(kind::MULT
, nm
->mkConst(coef
[pos_var
][0]), newVars
[0]);
3517 Debug("miplib") << "vars[] " << var
<< endl
3518 << " eq " << Rewriter::rewrite(sum
) << endl
;
3519 Node newAssertion
= var
.eqNode(Rewriter::rewrite(sum
));
3520 if(d_topLevelSubstitutions
.hasSubstitution(newAssertion
[0])) {
3521 //Warning() << "RE-SUBSTITUTION " << newAssertion[0] << endl;
3522 //Warning() << "REPLACE " << newAssertion[1] << endl;
3523 //Warning() << "ORIG " << d_topLevelSubstitutions.getSubstitution(newAssertion[0]) << endl;
3524 Assert(d_topLevelSubstitutions
.getSubstitution(newAssertion
[0]) == newAssertion
[1]);
3525 } else if(pos
.getNumChildren() <= options::arithMLTrickSubstitutions()) {
3526 d_topLevelSubstitutions
.addSubstitution(newAssertion
[0], newAssertion
[1]);
3527 Debug("miplib") << "addSubs: " << newAssertion
[0] << " to " << newAssertion
[1] << endl
;
3529 Debug("miplib") << "skipSubs: " << newAssertion
[0] << " to " << newAssertion
[1] << " (threshold is " << options::arithMLTrickSubstitutions() << ")" << endl
;
3531 newAssertion
= Rewriter::rewrite(newAssertion
);
3532 Debug("miplib") << " " << newAssertion
<< endl
;
3533 addFormula(newAssertion
, false, false);
3534 Debug("miplib") << " assertions to remove: " << endl
;
3535 for(vector
<TNode
>::const_iterator k
= asserts
[pos_var
].begin(), k_end
= asserts
[pos_var
].end(); k
!= k_end
; ++k
) {
3536 Debug("miplib") << " " << *k
<< endl
;
3537 removeAssertions
.insert((*k
).getId());
3543 if(!removeAssertions
.empty()) {
3544 Debug("miplib") << "SmtEnginePrivate::simplify(): scrubbing miplib encoding..." << endl
;
3545 for(size_t i
= 0; i
< d_realAssertionsEnd
; ++i
) {
3546 if(removeAssertions
.find(d_assertions
[i
].getId()) != removeAssertions
.end()) {
3547 Debug("miplib") << "SmtEnginePrivate::simplify(): - removing " << d_assertions
[i
] << endl
;
3548 d_assertions
[i
] = d_true
;
3549 ++d_smt
.d_stats
->d_numMiplibAssertionsRemoved
;
3550 } else if(d_assertions
[i
].getKind() == kind::AND
) {
3551 size_t removals
= removeFromConjunction(d_assertions
[i
], removeAssertions
);
3553 Debug("miplib") << "SmtEnginePrivate::simplify(): - reduced " << d_assertions
[i
] << endl
;
3554 Debug("miplib") << "SmtEnginePrivate::simplify(): - by " << removals
<< " conjuncts" << endl
;
3555 d_smt
.d_stats
->d_numMiplibAssertionsRemoved
+= removals
;
3558 Debug("miplib") << "had: " << d_assertions
[i
] << endl
;
3559 d_assertions
[i
] = Rewriter::rewrite(d_topLevelSubstitutions
.apply(d_assertions
[i
]));
3560 Debug("miplib") << "now: " << d_assertions
[i
] << endl
;
3563 Debug("miplib") << "SmtEnginePrivate::simplify(): miplib pass found nothing." << endl
;
3565 d_realAssertionsEnd
= d_assertions
.size();
3569 // returns false if simplification led to "false"
3570 bool SmtEnginePrivate::simplifyAssertions()
3571 throw(TypeCheckingException
, LogicException
, UnsafeInterruptException
) {
3572 spendResource(options::preprocessStep());
3573 Assert(d_smt
.d_pendingPops
== 0);
3575 ScopeCounter
depth(d_simplifyAssertionsDepth
);
3577 Trace("simplify") << "SmtEnginePrivate::simplify()" << endl
;
3579 dumpAssertions("pre-nonclausal", d_assertions
);
3581 if(options::simplificationMode() != SIMPLIFICATION_MODE_NONE
) {
3582 // Perform non-clausal simplification
3583 Chat() << "...performing nonclausal simplification..." << endl
;
3584 Trace("simplify") << "SmtEnginePrivate::simplify(): "
3585 << "performing non-clausal simplification" << endl
;
3586 bool noConflict
= nonClausalSimplify();
3591 // We piggy-back off of the BackEdgesMap in the CircuitPropagator to
3592 // do the miplib trick.
3593 if( // check that option is on
3594 options::arithMLTrick() &&
3595 // miplib rewrites aren't safe in incremental mode
3596 ! options::incrementalSolving() &&
3597 // only useful in arith
3598 d_smt
.d_logic
.isTheoryEnabled(THEORY_ARITH
) &&
3599 // we add new assertions and need this (in practice, this
3600 // restriction only disables miplib processing during
3601 // re-simplification, which we don't expect to be useful anyway)
3602 d_realAssertionsEnd
== d_assertions
.size() ) {
3603 Chat() << "...fixing miplib encodings..." << endl
;
3604 Trace("simplify") << "SmtEnginePrivate::simplify(): "
3605 << "looking for miplib pseudobooleans..." << endl
;
3607 TimerStat::CodeTimer
miplibTimer(d_smt
.d_stats
->d_miplibPassTime
);
3611 Trace("simplify") << "SmtEnginePrivate::simplify(): "
3612 << "skipping miplib pseudobooleans pass (either incrementalSolving is on, or miplib pbs are turned off)..." << endl
;
3616 dumpAssertions("post-nonclausal", d_assertions
);
3617 Trace("smt") << "POST nonClausalSimplify" << endl
;
3618 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
3620 // before ppRewrite check if only core theory for BV theory
3621 d_smt
.d_theoryEngine
->staticInitializeBVOptions(d_assertions
.ref());
3623 dumpAssertions("pre-theorypp", d_assertions
);
3625 // Theory preprocessing
3626 if (d_smt
.d_earlyTheoryPP
) {
3627 Chat() << "...doing early theory preprocessing..." << endl
;
3628 TimerStat::CodeTimer
codeTimer(d_smt
.d_stats
->d_theoryPreprocessTime
);
3629 // Call the theory preprocessors
3630 d_smt
.d_theoryEngine
->preprocessStart();
3631 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
3632 Assert(Rewriter::rewrite(d_assertions
[i
]) == d_assertions
[i
]);
3633 d_assertions
.replace(i
, d_smt
.d_theoryEngine
->preprocess(d_assertions
[i
]));
3634 Assert(Rewriter::rewrite(d_assertions
[i
]) == d_assertions
[i
]);
3638 dumpAssertions("post-theorypp", d_assertions
);
3639 Trace("smt") << "POST theoryPP" << endl
;
3640 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
3642 // ITE simplification
3643 if(options::doITESimp() &&
3644 (d_simplifyAssertionsDepth
<= 1 || options::doITESimpOnRepeat())) {
3645 Chat() << "...doing ITE simplification..." << endl
;
3646 bool noConflict
= simpITE();
3648 Chat() << "...ITE simplification found unsat..." << endl
;
3653 dumpAssertions("post-itesimp", d_assertions
);
3654 Trace("smt") << "POST iteSimp" << endl
;
3655 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
3657 // Unconstrained simplification
3658 if(options::unconstrainedSimp()) {
3659 Chat() << "...doing unconstrained simplification..." << endl
;
3660 unconstrainedSimp();
3663 dumpAssertions("post-unconstrained", d_assertions
);
3664 Trace("smt") << "POST unconstrainedSimp" << endl
;
3665 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
3667 if(options::repeatSimp() && options::simplificationMode() != SIMPLIFICATION_MODE_NONE
) {
3668 Chat() << "...doing another round of nonclausal simplification..." << endl
;
3669 Trace("simplify") << "SmtEnginePrivate::simplify(): "
3670 << " doing repeated simplification" << endl
;
3671 bool noConflict
= nonClausalSimplify();
3677 dumpAssertions("post-repeatsimp", d_assertions
);
3678 Trace("smt") << "POST repeatSimp" << endl
;
3679 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
3681 } catch(TypeCheckingExceptionPrivate
& tcep
) {
3682 // Calls to this function should have already weeded out any
3683 // typechecking exceptions via (e.g.) ensureBoolean(). But a
3684 // theory could still create a new expression that isn't
3685 // well-typed, and we don't want the C++ runtime to abort our
3686 // process without any error notice.
3688 ss
<< "A bad expression was produced. Original exception follows:\n"
3690 InternalError(ss
.str().c_str());
3695 Result
SmtEngine::check() {
3696 Assert(d_fullyInited
);
3697 Assert(d_pendingPops
== 0);
3699 Trace("smt") << "SmtEngine::check()" << endl
;
3701 ResourceManager
* resourceManager
= d_private
->getResourceManager();
3703 resourceManager
->beginCall();
3705 // Only way we can be out of resource is if cumulative budget is on
3706 if (resourceManager
->cumulativeLimitOn() &&
3707 resourceManager
->out()) {
3708 Result::UnknownExplanation why
= resourceManager
->outOfResources() ?
3709 Result::RESOURCEOUT
: Result::TIMEOUT
;
3710 return Result(Result::VALIDITY_UNKNOWN
, why
, d_filename
);
3713 // Make sure the prop layer has all of the assertions
3714 Trace("smt") << "SmtEngine::check(): processing assertions" << endl
;
3715 d_private
->processAssertions();
3716 Trace("smt") << "SmtEngine::check(): done processing assertions" << endl
;
3718 // Turn off stop only for QF_LRA
3719 // TODO: Bring up in a meeting where to put this
3720 if(options::decisionStopOnly() && !options::decisionMode
.wasSetByUser() ){
3722 (not d_logic
.isQuantified() &&
3723 d_logic
.isPure(THEORY_ARITH
) && d_logic
.isLinear() && !d_logic
.isDifferenceLogic() && !d_logic
.areIntegersUsed()
3725 if(d_private
->d_iteSkolemMap
.empty()){
3726 options::decisionStopOnly
.set(false);
3727 d_decisionEngine
->clearStrategies();
3728 Trace("smt") << "SmtEngine::check(): turning off stop only" << endl
;
3733 TimerStat::CodeTimer
solveTimer(d_stats
->d_solveTime
);
3735 Chat() << "solving..." << endl
;
3736 Trace("smt") << "SmtEngine::check(): running check" << endl
;
3737 Result result
= d_propEngine
->checkSat();
3739 resourceManager
->endCall();
3740 Trace("limit") << "SmtEngine::check(): cumulative millis " << resourceManager
->getTimeUsage()
3741 << ", resources " << resourceManager
->getResourceUsage() << endl
;
3744 return Result(result
, d_filename
);
3747 Result
SmtEngine::quickCheck() {
3748 Assert(d_fullyInited
);
3749 Trace("smt") << "SMT quickCheck()" << endl
;
3750 return Result(Result::VALIDITY_UNKNOWN
, Result::REQUIRES_FULL_CHECK
, d_filename
);
3754 void SmtEnginePrivate::collectSkolems(TNode n
, set
<TNode
>& skolemSet
, hash_map
<Node
, bool, NodeHashFunction
>& cache
)
3756 hash_map
<Node
, bool, NodeHashFunction
>::iterator it
;
3758 if (it
!= cache
.end()) {
3762 size_t sz
= n
.getNumChildren();
3764 IteSkolemMap::iterator it
= d_iteSkolemMap
.find(n
);
3765 if (it
!= d_iteSkolemMap
.end()) {
3766 skolemSet
.insert(n
);
3773 for (; k
< sz
; ++k
) {
3774 collectSkolems(n
[k
], skolemSet
, cache
);
3780 bool SmtEnginePrivate::checkForBadSkolems(TNode n
, TNode skolem
, hash_map
<Node
, bool, NodeHashFunction
>& cache
)
3782 hash_map
<Node
, bool, NodeHashFunction
>::iterator it
;
3784 if (it
!= cache
.end()) {
3785 return (*it
).second
;
3788 size_t sz
= n
.getNumChildren();
3790 IteSkolemMap::iterator it
= d_iteSkolemMap
.find(n
);
3792 if (it
!= d_iteSkolemMap
.end()) {
3793 if (!((*it
).first
< n
)) {
3802 for (; k
< sz
; ++k
) {
3803 if (checkForBadSkolems(n
[k
], skolem
, cache
)) {
3813 void SmtEnginePrivate::processAssertions() {
3814 TimerStat::CodeTimer
paTimer(d_smt
.d_stats
->d_processAssertionsTime
);
3815 spendResource(options::preprocessStep());
3816 Assert(d_smt
.d_fullyInited
);
3817 Assert(d_smt
.d_pendingPops
== 0);
3819 // Dump the assertions
3820 dumpAssertions("pre-everything", d_assertions
);
3822 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() begin" << endl
;
3823 Trace("smt") << "SmtEnginePrivate::processAssertions()" << endl
;
3825 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
3827 if (d_assertions
.size() == 0) {
3832 if (d_assertionsProcessed
&& options::incrementalSolving()) {
3833 // Placeholder for storing substitutions
3834 d_substitutionsIndex
= d_assertions
.size();
3835 d_assertions
.push_back(NodeManager::currentNM()->mkConst
<bool>(true));
3838 // Add dummy assertion in last position - to be used as a
3839 // placeholder for any new assertions to get added
3840 d_assertions
.push_back(NodeManager::currentNM()->mkConst
<bool>(true));
3841 // any assertions added beyond realAssertionsEnd must NOT affect the
3842 // equisatisfiability
3843 d_realAssertionsEnd
= d_assertions
.size();
3845 // Assertions are NOT guaranteed to be rewritten by this point
3847 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-definition-expansion" << endl
;
3848 dumpAssertions("pre-definition-expansion", d_assertions
);
3850 Chat() << "expanding definitions..." << endl
;
3851 Trace("simplify") << "SmtEnginePrivate::simplify(): expanding definitions" << endl
;
3852 TimerStat::CodeTimer
codeTimer(d_smt
.d_stats
->d_definitionExpansionTime
);
3853 hash_map
<Node
, Node
, NodeHashFunction
> cache
;
3854 for(unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
3855 d_assertions
.replace(i
, expandDefinitions(d_assertions
[i
], cache
));
3858 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-definition-expansion" << endl
;
3859 dumpAssertions("post-definition-expansion", d_assertions
);
3861 // save the assertions now
3864 for (unsigned i
= 0; i
< d_assertions
.size(); ++i
) {
3865 ProofManager::currentPM()->addAssertion(d_assertions
[i
].toExpr());
3869 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
3871 if( options::ceGuidedInst() ){
3872 //register sygus conjecture pre-rewrite (motivated by solution reconstruction)
3873 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
3874 d_smt
.d_theoryEngine
->getQuantifiersEngine()->getCegInstantiation()->preregisterAssertion( d_assertions
[i
] );
3878 if (options::solveIntAsBV() > 0) {
3879 Chat() << "converting ints to bit-vectors..." << endl
;
3880 hash_map
<Node
, Node
, NodeHashFunction
> cache
;
3881 for(unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
3882 d_assertions
.replace(i
, intToBV(d_assertions
[i
], cache
));
3886 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
&&
3887 !d_smt
.d_logic
.isPure(THEORY_BV
) &&
3888 d_smt
.d_logic
.getLogicString() != "QF_UFBV" &&
3889 d_smt
.d_logic
.getLogicString() != "QF_ABV") {
3890 throw ModalException("Eager bit-blasting does not currently support theory combination. "
3891 "Note that in a QF_BV problem UF symbols can be introduced for division. "
3892 "Try --bv-div-zero-const to interpret division by zero as a constant.");
3895 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
) {
3896 d_smt
.d_theoryEngine
->mkAckermanizationAsssertions(d_assertions
.ref());
3899 if ( options::bvAbstraction() &&
3900 !options::incrementalSolving()) {
3901 dumpAssertions("pre-bv-abstraction", d_assertions
);
3903 dumpAssertions("post-bv-abstraction", d_assertions
);
3906 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
3908 dumpAssertions("pre-constrain-subtypes", d_assertions
);
3910 // Any variables of subtype types need to be constrained properly.
3911 // Careful, here: constrainSubtypes() adds to the back of
3912 // d_assertions, but we don't need to reprocess those.
3913 // We also can't use an iterator, because the vector may be moved in
3914 // memory during this loop.
3915 Chat() << "constraining subtypes..." << endl
;
3916 for(unsigned i
= 0, i_end
= d_assertions
.size(); i
!= i_end
; ++i
) {
3917 constrainSubtypes(d_assertions
[i
], d_assertions
);
3920 dumpAssertions("post-constrain-subtypes", d_assertions
);
3922 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
3924 bool noConflict
= true;
3926 // Unconstrained simplification
3927 if(options::unconstrainedSimp()) {
3928 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-unconstrained-simp" << endl
;
3929 dumpAssertions("pre-unconstrained-simp", d_assertions
);
3930 Chat() << "...doing unconstrained simplification..." << endl
;
3931 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
3932 d_assertions
.replace(i
, Rewriter::rewrite(d_assertions
[i
]));
3934 unconstrainedSimp();
3935 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-unconstrained-simp" << endl
;
3936 dumpAssertions("post-unconstrained-simp", d_assertions
);
3939 if(options::bvIntroducePow2()){
3940 theory::bv::BVIntroducePow2::pow2Rewrite(d_assertions
.ref());
3943 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-substitution" << endl
;
3944 dumpAssertions("pre-substitution", d_assertions
);
3946 if(options::unsatCores()) {
3947 // special rewriting pass for unsat cores, since many of the passes below are skipped
3948 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
3949 d_assertions
.replace(i
, Rewriter::rewrite(d_assertions
[i
]));
3952 // Apply the substitutions we already have, and normalize
3953 if(!options::unsatCores()) {
3954 Chat() << "applying substitutions..." << endl
;
3955 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
3956 << "applying substitutions" << endl
;
3957 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
3958 Trace("simplify") << "applying to " << d_assertions
[i
] << endl
;
3959 spendResource(options::preprocessStep());
3960 d_assertions
.replace(i
, Rewriter::rewrite(d_topLevelSubstitutions
.apply(d_assertions
[i
])));
3961 Trace("simplify") << " got " << d_assertions
[i
] << endl
;
3965 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-substitution" << endl
;
3966 dumpAssertions("post-substitution", d_assertions
);
3968 // Assertions ARE guaranteed to be rewritten by this point
3970 // Lift bit-vectors of size 1 to bool
3971 if(options::bitvectorToBool()) {
3972 dumpAssertions("pre-bv-to-bool", d_assertions
);
3973 Chat() << "...doing bvToBool..." << endl
;
3975 dumpAssertions("post-bv-to-bool", d_assertions
);
3976 Trace("smt") << "POST bvToBool" << endl
;
3978 // Convert non-top-level Booleans to bit-vectors of size 1
3979 if(options::boolToBitvector()) {
3980 dumpAssertions("pre-bool-to-bv", d_assertions
);
3981 Chat() << "...doing boolToBv..." << endl
;
3983 dumpAssertions("post-bool-to-bv", d_assertions
);
3984 Trace("smt") << "POST boolToBv" << endl
;
3986 if(options::sepPreSkolemEmp()) {
3987 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
3988 Node prev
= d_assertions
[i
];
3989 Node next
= sep::TheorySepRewriter::preprocess( prev
);
3991 d_assertions
.replace( i
, Rewriter::rewrite( next
) );
3992 Trace("sep-preprocess") << "*** Preprocess sep " << prev
<< endl
;
3993 Trace("sep-preprocess") << " ...got " << d_assertions
[i
] << endl
;
3998 if( d_smt
.d_logic
.isQuantified() ){
3999 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-quant-preprocess" << endl
;
4001 dumpAssertions("pre-skolem-quant", d_assertions
);
4002 //remove rewrite rules, apply pre-skolemization to existential quantifiers
4003 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
4004 Node prev
= d_assertions
[i
];
4005 Node next
= quantifiers::QuantifiersRewriter::preprocess( prev
);
4007 d_assertions
.replace( i
, Rewriter::rewrite( next
) );
4008 Trace("quantifiers-preprocess") << "*** Pre-skolemize " << prev
<< endl
;
4009 Trace("quantifiers-preprocess") << " ...got " << d_assertions
[i
] << endl
;
4012 dumpAssertions("post-skolem-quant", d_assertions
);
4013 if( options::macrosQuant() ){
4014 //quantifiers macro expansion
4015 quantifiers::QuantifierMacros
qm( d_smt
.d_theoryEngine
->getQuantifiersEngine() );
4018 success
= qm
.simplify( d_assertions
.ref(), true );
4020 //finalize the definitions
4021 qm
.finalizeDefinitions();
4024 //fmf-fun : assume admissible functions, applying preprocessing reduction to FMF
4025 if( options::fmfFunWellDefined() ){
4026 quantifiers::FunDefFmf fdf
;
4027 //must carry over current definitions (for incremental)
4028 for( context::CDList
<Node
>::const_iterator fit
= d_smt
.d_fmfRecFunctionsDefined
->begin();
4029 fit
!= d_smt
.d_fmfRecFunctionsDefined
->end(); ++fit
) {
4031 Assert( d_smt
.d_fmfRecFunctionsAbs
.find( f
)!=d_smt
.d_fmfRecFunctionsAbs
.end() );
4032 TypeNode ft
= d_smt
.d_fmfRecFunctionsAbs
[f
];
4033 fdf
.d_sorts
[f
] = ft
;
4034 std::map
< Node
, std::vector
< Node
> >::iterator fcit
= d_smt
.d_fmfRecFunctionsConcrete
.find( f
);
4035 Assert( fcit
!=d_smt
.d_fmfRecFunctionsConcrete
.end() );
4036 for( unsigned j
=0; j
<fcit
->second
.size(); j
++ ){
4037 fdf
.d_input_arg_inj
[f
].push_back( fcit
->second
[j
] );
4040 fdf
.simplify( d_assertions
.ref() );
4041 //must store new definitions (for incremental)
4042 for( unsigned i
=0; i
<fdf
.d_funcs
.size(); i
++ ){
4043 Node f
= fdf
.d_funcs
[i
];
4044 d_smt
.d_fmfRecFunctionsAbs
[f
] = fdf
.d_sorts
[f
];
4045 d_smt
.d_fmfRecFunctionsConcrete
[f
].clear();
4046 for( unsigned j
=0; j
<fdf
.d_input_arg_inj
[f
].size(); j
++ ){
4047 d_smt
.d_fmfRecFunctionsConcrete
[f
].push_back( fdf
.d_input_arg_inj
[f
][j
] );
4049 d_smt
.d_fmfRecFunctionsDefined
->push_back( f
);
4052 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-quant-preprocess" << endl
;
4055 if( options::sortInference() || options::ufssFairnessMonotone() ){
4056 //sort inference technique
4057 SortInference
* si
= d_smt
.d_theoryEngine
->getSortInference();
4058 si
->simplify( d_assertions
.ref(), options::sortInference(), options::ufssFairnessMonotone() );
4059 for( std::map
< Node
, Node
>::iterator it
= si
->d_model_replace_f
.begin(); it
!= si
->d_model_replace_f
.end(); ++it
){
4060 d_smt
.setPrintFuncInModel( it
->first
.toExpr(), false );
4061 d_smt
.setPrintFuncInModel( it
->second
.toExpr(), true );
4065 if( options::pbRewrites() ){
4066 d_pbsProcessor
.learn(d_assertions
.ref());
4067 if(d_pbsProcessor
.likelyToHelp()){
4068 d_pbsProcessor
.applyReplacements(d_assertions
.ref());
4072 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-simplify" << endl
;
4073 dumpAssertions("pre-simplify", d_assertions
);
4074 Chat() << "simplifying assertions..." << endl
;
4075 noConflict
= simplifyAssertions();
4077 ++(d_smt
.d_stats
->d_simplifiedToFalse
);
4079 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-simplify" << endl
;
4080 dumpAssertions("post-simplify", d_assertions
);
4082 dumpAssertions("pre-static-learning", d_assertions
);
4083 if(options::doStaticLearning()) {
4084 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-static-learning" << endl
;
4085 // Perform static learning
4086 Chat() << "doing static learning..." << endl
;
4087 Trace("simplify") << "SmtEnginePrivate::simplify(): "
4088 << "performing static learning" << endl
;
4090 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-static-learning" << endl
;
4092 dumpAssertions("post-static-learning", d_assertions
);
4094 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
4097 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-ite-removal" << endl
;
4098 dumpAssertions("pre-ite-removal", d_assertions
);
4100 Chat() << "removing term ITEs..." << endl
;
4101 TimerStat::CodeTimer
codeTimer(d_smt
.d_stats
->d_iteRemovalTime
);
4102 // Remove ITEs, updating d_iteSkolemMap
4103 d_smt
.d_stats
->d_numAssertionsPre
+= d_assertions
.size();
4105 d_smt
.d_stats
->d_numAssertionsPost
+= d_assertions
.size();
4107 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-ite-removal" << endl
;
4108 dumpAssertions("post-ite-removal", d_assertions
);
4110 dumpAssertions("pre-repeat-simplify", d_assertions
);
4111 if(options::repeatSimp()) {
4112 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-repeat-simplify" << endl
;
4113 Chat() << "re-simplifying assertions..." << endl
;
4114 ScopeCounter
depth(d_simplifyAssertionsDepth
);
4115 noConflict
&= simplifyAssertions();
4117 // Need to fix up assertion list to maintain invariants:
4118 // Let Sk be the set of Skolem variables introduced by ITE's. Let <_sk be the order in which these variables were introduced
4119 // during ite removal.
4120 // For each skolem variable sk, let iteExpr = iteMap(sk) be the ite expr mapped to by sk.
4122 // cache for expression traversal
4123 hash_map
<Node
, bool, NodeHashFunction
> cache
;
4125 // First, find all skolems that appear in the substitution map - their associated iteExpr will need
4126 // to be moved to the main assertion set
4127 set
<TNode
> skolemSet
;
4128 SubstitutionMap::iterator pos
= d_topLevelSubstitutions
.begin();
4129 for (; pos
!= d_topLevelSubstitutions
.end(); ++pos
) {
4130 collectSkolems((*pos
).first
, skolemSet
, cache
);
4131 collectSkolems((*pos
).second
, skolemSet
, cache
);
4134 // We need to ensure:
4135 // 1. iteExpr has the form (ite cond (sk = t) (sk = e))
4136 // 2. if some sk' in Sk appears in cond, t, or e, then sk' <_sk sk
4137 // If either of these is violated, we must add iteExpr as a proper assertion
4138 IteSkolemMap::iterator it
= d_iteSkolemMap
.begin();
4139 IteSkolemMap::iterator iend
= d_iteSkolemMap
.end();
4140 NodeBuilder
<> builder(kind::AND
);
4141 builder
<< d_assertions
[d_realAssertionsEnd
- 1];
4142 vector
<TNode
> toErase
;
4143 for (; it
!= iend
; ++it
) {
4144 if (skolemSet
.find((*it
).first
) == skolemSet
.end()) {
4145 TNode iteExpr
= d_assertions
[(*it
).second
];
4146 if (iteExpr
.getKind() == kind::ITE
&&
4147 iteExpr
[1].getKind() == kind::EQUAL
&&
4148 iteExpr
[1][0] == (*it
).first
&&
4149 iteExpr
[2].getKind() == kind::EQUAL
&&
4150 iteExpr
[2][0] == (*it
).first
) {
4152 bool bad
= checkForBadSkolems(iteExpr
[0], (*it
).first
, cache
);
4153 bad
= bad
|| checkForBadSkolems(iteExpr
[1][1], (*it
).first
, cache
);
4154 bad
= bad
|| checkForBadSkolems(iteExpr
[2][1], (*it
).first
, cache
);
4160 // Move this iteExpr into the main assertions
4161 builder
<< d_assertions
[(*it
).second
];
4162 d_assertions
[(*it
).second
] = NodeManager::currentNM()->mkConst
<bool>(true);
4163 toErase
.push_back((*it
).first
);
4165 if(builder
.getNumChildren() > 1) {
4166 while (!toErase
.empty()) {
4167 d_iteSkolemMap
.erase(toErase
.back());
4170 d_assertions
[d_realAssertionsEnd
- 1] = Rewriter::rewrite(Node(builder
));
4172 // For some reason this is needed for some benchmarks, such as
4173 // http://cvc4.cs.nyu.edu/benchmarks/smtlib2/QF_AUFBV/dwp_formulas/try5_small_difret_functions_dwp_tac.re_node_set_remove_at.il.dwp.smt2
4174 // Figure it out later
4176 // Assert(iteRewriteAssertionsEnd == d_assertions.size());
4178 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-repeat-simplify" << endl
;
4180 dumpAssertions("post-repeat-simplify", d_assertions
);
4182 dumpAssertions("pre-rewrite-apply-to-const", d_assertions
);
4183 if(options::rewriteApplyToConst()) {
4184 Chat() << "Rewriting applies to constants..." << endl
;
4185 TimerStat::CodeTimer
codeTimer(d_smt
.d_stats
->d_rewriteApplyToConstTime
);
4186 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
4187 d_assertions
[i
] = Rewriter::rewrite(rewriteApplyToConst(d_assertions
[i
]));
4190 dumpAssertions("post-rewrite-apply-to-const", d_assertions
);
4192 // begin: INVARIANT to maintain: no reordering of assertions or
4193 // introducing new ones
4194 #ifdef CVC4_ASSERTIONS
4195 unsigned iteRewriteAssertionsEnd
= d_assertions
.size();
4198 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
4200 Debug("smt") << "SmtEnginePrivate::processAssertions() POST SIMPLIFICATION" << endl
;
4201 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
4203 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-theory-preprocessing" << endl
;
4204 dumpAssertions("pre-theory-preprocessing", d_assertions
);
4206 Chat() << "theory preprocessing..." << endl
;
4207 TimerStat::CodeTimer
codeTimer(d_smt
.d_stats
->d_theoryPreprocessTime
);
4208 // Call the theory preprocessors
4209 d_smt
.d_theoryEngine
->preprocessStart();
4210 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
4211 d_assertions
.replace(i
, d_smt
.d_theoryEngine
->preprocess(d_assertions
[i
]));
4214 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-theory-preprocessing" << endl
;
4215 dumpAssertions("post-theory-preprocessing", d_assertions
);
4217 // If we are using eager bit-blasting wrap assertions in fake atom so that
4218 // everything gets bit-blasted to internal SAT solver
4219 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
) {
4220 for (unsigned i
= 0; i
< d_assertions
.size(); ++i
) {
4221 TNode atom
= d_assertions
[i
];
4222 Node eager_atom
= NodeManager::currentNM()->mkNode(kind::BITVECTOR_EAGER_ATOM
, atom
);
4223 d_assertions
.replace(i
, eager_atom
);
4224 TheoryModel
* m
= d_smt
.d_theoryEngine
->getModel();
4225 m
->addSubstitution(eager_atom
, atom
);
4229 //notify theory engine new preprocessed assertions
4230 d_smt
.d_theoryEngine
->notifyPreprocessedAssertions( d_assertions
.ref() );
4232 // Push the formula to decision engine
4234 Chat() << "pushing to decision engine..." << endl
;
4235 Assert(iteRewriteAssertionsEnd
== d_assertions
.size());
4236 d_smt
.d_decisionEngine
->addAssertions
4237 (d_assertions
.ref(), d_realAssertionsEnd
, d_iteSkolemMap
);
4240 // end: INVARIANT to maintain: no reordering of assertions or
4241 // introducing new ones
4243 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() end" << endl
;
4244 dumpAssertions("post-everything", d_assertions
);
4246 // Push the formula to SAT
4248 Chat() << "converting to CNF..." << endl
;
4249 TimerStat::CodeTimer
codeTimer(d_smt
.d_stats
->d_cnfConversionTime
);
4250 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
4251 Chat() << "+ " << d_assertions
[i
] << std::endl
;
4252 d_smt
.d_propEngine
->assertFormula(d_assertions
[i
]);
4256 d_assertionsProcessed
= true;
4258 d_assertions
.clear();
4259 d_iteSkolemMap
.clear();
4262 void SmtEnginePrivate::addFormula(TNode n
, bool inUnsatCore
, bool inInput
)
4263 throw(TypeCheckingException
, LogicException
) {
4270 Trace("smt") << "SmtEnginePrivate::addFormula(" << n
<< "), inUnsatCore = " << inUnsatCore
<< ", inInput = " << inInput
<< endl
;
4271 // Give it to proof manager
4274 // n is an input assertion
4275 if (inUnsatCore
|| options::dumpUnsatCores() || options::checkUnsatCores() || options::fewerPreprocessingHoles()) {
4277 ProofManager::currentPM()->addCoreAssertion(n
.toExpr());
4280 // n is the result of an unknown preprocessing step, add it to dependency map to null
4281 ProofManager::currentPM()->addDependence(n
, Node::null());
4283 // rewrite rules are by default in the unsat core because
4284 // they need to be applied until saturation
4285 if(options::unsatCores() &&
4286 n
.getKind() == kind::REWRITE_RULE
){
4287 ProofManager::currentPM()->addUnsatCore(n
.toExpr());
4291 // Add the normalized formula to the queue
4292 d_assertions
.push_back(n
);
4293 //d_assertions.push_back(Rewriter::rewrite(n));
4296 void SmtEngine::ensureBoolean(const Expr
& e
) throw(TypeCheckingException
) {
4297 Type type
= e
.getType(options::typeChecking());
4298 Type boolType
= d_exprManager
->booleanType();
4299 if(type
!= boolType
) {
4301 ss
<< "Expected " << boolType
<< "\n"
4302 << "The assertion : " << e
<< "\n"
4303 << "Its type : " << type
;
4304 throw TypeCheckingException(e
, ss
.str());
4308 Result
SmtEngine::checkSat(const Expr
& ex
, bool inUnsatCore
) throw(TypeCheckingException
, ModalException
, LogicException
) {
4309 return checkSatisfiability( ex
, inUnsatCore
, false );
4310 }/* SmtEngine::checkSat() */
4312 Result
SmtEngine::query(const Expr
& ex
, bool inUnsatCore
) throw(TypeCheckingException
, ModalException
, LogicException
) {
4313 Assert(!ex
.isNull());
4314 return checkSatisfiability( ex
, inUnsatCore
, true );
4315 }/* SmtEngine::query() */
4317 Result
SmtEngine::checkSatisfiability(const Expr
& ex
, bool inUnsatCore
, bool isQuery
) {
4319 Assert(ex
.isNull() || ex
.getExprManager() == d_exprManager
);
4320 SmtScope
smts(this);
4321 finalOptionsAreSet();
4324 Trace("smt") << "SmtEngine::" << (isQuery
? "query" : "checkSat") << "(" << ex
<< ")" << endl
;
4326 if(d_queryMade
&& !options::incrementalSolving()) {
4327 throw ModalException("Cannot make multiple queries unless "
4328 "incremental solving is enabled "
4329 "(try --incremental)");
4334 // Substitute out any abstract values in ex.
4335 e
= d_private
->substituteAbstractValues(Node::fromExpr(ex
)).toExpr();
4336 // Ensure expr is type-checked at this point.
4340 // check to see if a postsolve() is pending
4341 if(d_needPostsolve
) {
4342 d_theoryEngine
->postsolve();
4343 d_needPostsolve
= false;
4349 // Note that a query has been made
4354 d_problemExtended
= true;
4355 Expr ea
= isQuery
? e
.notExpr() : e
;
4356 if(d_assertionList
!= NULL
) {
4357 d_assertionList
->push_back(ea
);
4359 d_private
->addFormula(ea
.getNode(), inUnsatCore
);
4362 Result
r(Result::SAT_UNKNOWN
, Result::UNKNOWN_REASON
);
4363 r
= isQuery
? check().asValidityResult() : check().asSatisfiabilityResult();
4365 if (options::solveIntAsBV() > 0 &&r
.asSatisfiabilityResult().isSat() == Result::UNSAT
) {
4366 r
= Result(Result::SAT_UNKNOWN
, Result::UNKNOWN_REASON
);
4369 d_needPostsolve
= true;
4371 // Dump the query if requested
4372 if(Dump
.isOn("benchmark")) {
4373 // the expr already got dumped out if assertion-dumping is on
4375 Dump("benchmark") << QueryCommand(ex
);
4377 Dump("benchmark") << CheckSatCommand(ex
);
4384 // Remember the status
4387 d_problemExtended
= false;
4389 Trace("smt") << "SmtEngine::" << (isQuery
? "query" : "checkSat") << "(" << e
<< ") => " << r
<< endl
;
4391 // Check that SAT results generate a model correctly.
4392 if(options::checkModels()) {
4393 if(r
.asSatisfiabilityResult().isSat() == Result::SAT
||
4394 (r
.isUnknown() && r
.whyUnknown() == Result::INCOMPLETE
) ){
4395 checkModel(/* hard failure iff */ ! r
.isUnknown());
4398 // Check that UNSAT results generate a proof correctly.
4399 if(options::checkProofs()) {
4400 if(r
.asSatisfiabilityResult().isSat() == Result::UNSAT
) {
4401 TimerStat::CodeTimer
checkProofTimer(d_stats
->d_checkProofTime
);
4405 // Check that UNSAT results generate an unsat core correctly.
4406 if(options::checkUnsatCores()) {
4407 if(r
.asSatisfiabilityResult().isSat() == Result::UNSAT
) {
4408 TimerStat::CodeTimer
checkUnsatCoreTimer(d_stats
->d_checkUnsatCoreTime
);
4414 } catch (UnsafeInterruptException
& e
) {
4415 AlwaysAssert(d_private
->getResourceManager()->out());
4416 Result::UnknownExplanation why
= d_private
->getResourceManager()->outOfResources() ?
4417 Result::RESOURCEOUT
: Result::TIMEOUT
;
4418 return Result(Result::SAT_UNKNOWN
, why
, d_filename
);
4423 Result
SmtEngine::checkSynth(const Expr
& e
) throw(TypeCheckingException
, ModalException
, LogicException
) {
4424 SmtScope
smts(this);
4425 Trace("smt") << "Check synth: " << e
<< std::endl
;
4426 Trace("smt-synth") << "Check synthesis conjecture: " << e
<< std::endl
;
4428 Node conj
= Node::fromExpr( e
);
4429 if( conj
.getKind()==kind::FORALL
){
4430 //possibly run quantifier elimination to make formula into single invocation
4431 if( conj
[1].getKind()==kind::EXISTS
){
4432 Node conj_se
= conj
[1][1];
4434 Trace("smt-synth") << "Compute single invocation for " << conj_se
<< "..." << std::endl
;
4435 quantifiers::SingleInvocationPartition
sip( kind::APPLY
);
4436 sip
.init( conj_se
);
4437 Trace("smt-synth") << "...finished, got:" << std::endl
;
4438 sip
.debugPrint("smt-synth");
4440 if( !sip
.isPurelySingleInvocation() && sip
.isNonGroundSingleInvocation() ){
4441 //We are in the case where our synthesis conjecture is exists f. forall xy. P( f( x ), x, y ), P does not contain f.
4442 //The following will run QE on (exists z x.) exists y. P( z, x, y ) to obtain Q( z, x ),
4443 // and then constructs exists f. forall x. Q( f( x ), x ), where Q does not contain f. We invoke synthesis solver on this result.
4445 //create new smt engine to do quantifier elimination
4446 SmtEngine
smt_qe( d_exprManager
);
4447 smt_qe
.setLogic(getLogicInfo());
4448 Trace("smt-synth") << "Property is non-ground single invocation, run QE to obtain single invocation." << std::endl
;
4449 //partition variables
4450 std::vector
< Node
> qe_vars
;
4451 std::vector
< Node
> nqe_vars
;
4452 for( unsigned i
=0; i
<sip
.d_all_vars
.size(); i
++ ){
4453 Node v
= sip
.d_all_vars
[i
];
4454 if( std::find( sip
.d_si_vars
.begin(), sip
.d_si_vars
.end(), v
)==sip
.d_si_vars
.end() ){
4455 qe_vars
.push_back( v
);
4457 nqe_vars
.push_back( v
);
4460 std::vector
< Node
> orig
;
4461 std::vector
< Node
> subs
;
4462 //skolemize non-qe variables
4463 for( unsigned i
=0; i
<nqe_vars
.size(); i
++ ){
4464 Node k
= NodeManager::currentNM()->mkSkolem( "k", nqe_vars
[i
].getType(), "qe for non-ground single invocation" );
4465 orig
.push_back( nqe_vars
[i
] );
4466 subs
.push_back( k
);
4467 Trace("smt-synth") << " subs : " << nqe_vars
[i
] << " -> " << k
<< std::endl
;
4469 for( std::map
< Node
, bool >::iterator it
= sip
.d_funcs
.begin(); it
!= sip
.d_funcs
.end(); ++it
){
4470 orig
.push_back( sip
.d_func_inv
[it
->first
] );
4471 Node k
= NodeManager::currentNM()->mkSkolem( "k", sip
.d_func_fo_var
[it
->first
].getType(), "qe for function in non-ground single invocation" );
4472 subs
.push_back( k
);
4473 Trace("smt-synth") << " subs : " << sip
.d_func_inv
[it
->first
] << " -> " << k
<< std::endl
;
4475 Node conj_se_ngsi
= sip
.getFullSpecification();
4476 Node conj_se_ngsi_subs
= conj_se_ngsi
.substitute( orig
.begin(), orig
.end(), subs
.begin(), subs
.end() );
4477 Assert( !qe_vars
.empty() );
4478 conj_se_ngsi_subs
= NodeManager::currentNM()->mkNode( kind::EXISTS
, NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST
, qe_vars
), conj_se_ngsi_subs
);
4480 Trace("smt-synth") << "Run quantifier elimination on " << conj_se_ngsi_subs
<< std::endl
;
4481 Expr qe_res
= smt_qe
.doQuantifierElimination( conj_se_ngsi_subs
.toExpr(), true, false );
4482 Trace("smt-synth") << "Result : " << qe_res
<< std::endl
;
4484 //create single invocation conjecture
4485 Node qe_res_n
= Node::fromExpr( qe_res
);
4486 qe_res_n
= qe_res_n
.substitute( subs
.begin(), subs
.end(), orig
.begin(), orig
.end() );
4487 if( !nqe_vars
.empty() ){
4488 qe_res_n
= NodeManager::currentNM()->mkNode( kind::EXISTS
, NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST
, nqe_vars
), qe_res_n
);
4490 Assert( conj
.getNumChildren()==3 );
4491 qe_res_n
= NodeManager::currentNM()->mkNode( kind::FORALL
, conj
[0], qe_res_n
, conj
[2] );
4492 Trace("smt-synth") << "Converted conjecture after QE : " << qe_res_n
<< std::endl
;
4493 e_check
= qe_res_n
.toExpr();
4498 return checkSatisfiability( e_check
, true, false );
4501 Result
SmtEngine::assertFormula(const Expr
& ex
, bool inUnsatCore
) throw(TypeCheckingException
, LogicException
, UnsafeInterruptException
) {
4502 Assert(ex
.getExprManager() == d_exprManager
);
4503 SmtScope
smts(this);
4504 finalOptionsAreSet();
4507 Trace("smt") << "SmtEngine::assertFormula(" << ex
<< ")" << endl
;
4509 if (Dump
.isOn("raw-benchmark")) {
4510 Dump("raw-benchmark") << AssertCommand(ex
);
4513 // Substitute out any abstract values in ex
4514 Expr e
= d_private
->substituteAbstractValues(Node::fromExpr(ex
)).toExpr();
4517 if(d_assertionList
!= NULL
) {
4518 d_assertionList
->push_back(e
);
4520 d_private
->addFormula(e
.getNode(), inUnsatCore
);
4521 return quickCheck().asValidityResult();
4522 }/* SmtEngine::assertFormula() */
4524 Node
SmtEngine::postprocess(TNode node
, TypeNode expectedType
) const {
4528 Expr
SmtEngine::simplify(const Expr
& ex
) throw(TypeCheckingException
, LogicException
, UnsafeInterruptException
) {
4529 Assert(ex
.getExprManager() == d_exprManager
);
4530 SmtScope
smts(this);
4531 finalOptionsAreSet();
4533 Trace("smt") << "SMT simplify(" << ex
<< ")" << endl
;
4535 if(Dump
.isOn("benchmark")) {
4536 Dump("benchmark") << SimplifyCommand(ex
);
4539 Expr e
= d_private
->substituteAbstractValues(Node::fromExpr(ex
)).toExpr();
4540 if( options::typeChecking() ) {
4541 e
.getType(true); // ensure expr is type-checked at this point
4544 // Make sure all preprocessing is done
4545 d_private
->processAssertions();
4546 Node n
= d_private
->simplify(Node::fromExpr(e
));
4547 n
= postprocess(n
, TypeNode::fromType(e
.getType()));
4551 Expr
SmtEngine::expandDefinitions(const Expr
& ex
) throw(TypeCheckingException
, LogicException
, UnsafeInterruptException
) {
4552 d_private
->spendResource(options::preprocessStep());
4554 Assert(ex
.getExprManager() == d_exprManager
);
4555 SmtScope
smts(this);
4556 finalOptionsAreSet();
4558 Trace("smt") << "SMT expandDefinitions(" << ex
<< ")" << endl
;
4560 // Substitute out any abstract values in ex.
4561 Expr e
= d_private
->substituteAbstractValues(Node::fromExpr(ex
)).toExpr();
4562 if(options::typeChecking()) {
4563 // Ensure expr is type-checked at this point.
4566 if(Dump
.isOn("benchmark")) {
4567 Dump("benchmark") << ExpandDefinitionsCommand(e
);
4569 hash_map
<Node
, Node
, NodeHashFunction
> cache
;
4570 Node n
= d_private
->expandDefinitions(Node::fromExpr(e
), cache
, /* expandOnly = */ true);
4571 n
= postprocess(n
, TypeNode::fromType(e
.getType()));
4576 Expr
SmtEngine::getValue(const Expr
& ex
) const throw(ModalException
, TypeCheckingException
, LogicException
, UnsafeInterruptException
) {
4577 Assert(ex
.getExprManager() == d_exprManager
);
4578 SmtScope
smts(this);
4580 Trace("smt") << "SMT getValue(" << ex
<< ")" << endl
;
4581 if(Dump
.isOn("benchmark")) {
4582 Dump("benchmark") << GetValueCommand(ex
);
4585 if(!options::produceModels()) {
4587 "Cannot get value when produce-models options is off.";
4588 throw ModalException(msg
);
4590 if(d_status
.isNull() ||
4591 d_status
.asSatisfiabilityResult() == Result::UNSAT
||
4592 d_problemExtended
) {
4594 "Cannot get value unless immediately preceded by SAT/INVALID or UNKNOWN response.";
4595 throw ModalException(msg
);
4598 // Substitute out any abstract values in ex.
4599 Expr e
= d_private
->substituteAbstractValues(Node::fromExpr(ex
)).toExpr();
4601 // Ensure expr is type-checked at this point.
4602 e
.getType(options::typeChecking());
4604 // do not need to apply preprocessing substitutions (should be recorded
4605 // in model already)
4607 Node n
= Node::fromExpr(e
);
4608 Trace("smt") << "--- getting value of " << n
<< endl
;
4609 TypeNode expectedType
= n
.getType();
4611 // Expand, then normalize
4612 hash_map
<Node
, Node
, NodeHashFunction
> cache
;
4613 n
= d_private
->expandDefinitions(n
, cache
);
4614 // There are two ways model values for terms are computed (for historical
4615 // reasons). One way is that used in check-model; the other is that
4616 // used by the Model classes. It's not clear to me exactly how these
4617 // two are different, but they need to be unified. This ugly hack here
4618 // is to fix bug 554 until we can revamp boolean-terms and models [MGD]
4621 if(!n
.getType().isFunction()) {
4622 n
= Rewriter::rewrite(n
);
4625 Trace("smt") << "--- getting value of " << n
<< endl
;
4626 TheoryModel
* m
= d_theoryEngine
->getModel();
4629 resultNode
= m
->getValue(n
);
4631 Trace("smt") << "--- got value " << n
<< " = " << resultNode
<< endl
;
4632 resultNode
= postprocess(resultNode
, expectedType
);
4633 Trace("smt") << "--- model-post returned " << resultNode
<< endl
;
4634 Trace("smt") << "--- model-post returned " << resultNode
.getType() << endl
;
4635 Trace("smt") << "--- model-post expected " << expectedType
<< endl
;
4637 // type-check the result we got
4638 Assert(resultNode
.isNull() || resultNode
.getType().isSubtypeOf(expectedType
),
4639 "Run with -t smt for details.");
4641 // ensure it's a constant
4642 Assert(resultNode
.getKind() == kind::LAMBDA
|| resultNode
.isConst());
4644 if(options::abstractValues() && resultNode
.getType().isArray()) {
4645 resultNode
= d_private
->mkAbstractValue(resultNode
);
4646 Trace("smt") << "--- abstract value >> " << resultNode
<< endl
;
4649 return resultNode
.toExpr();
4652 bool SmtEngine::addToAssignment(const Expr
& ex
) throw() {
4653 SmtScope
smts(this);
4654 finalOptionsAreSet();
4656 // Substitute out any abstract values in ex
4657 Expr e
= d_private
->substituteAbstractValues(Node::fromExpr(ex
)).toExpr();
4658 Type type
= e
.getType(options::typeChecking());
4660 PrettyCheckArgument(
4661 type
.isBoolean(), e
,
4662 "expected Boolean-typed variable or function application "
4663 "in addToAssignment()" );
4664 Node n
= e
.getNode();
4665 // must be an APPLY of a zero-ary defined function, or a variable
4666 PrettyCheckArgument(
4667 ( ( n
.getKind() == kind::APPLY
&&
4668 ( d_definedFunctions
->find(n
.getOperator()) !=
4669 d_definedFunctions
->end() ) &&
4670 n
.getNumChildren() == 0 ) ||
4672 "expected variable or defined-function application "
4673 "in addToAssignment(),\ngot %s", e
.toString().c_str() );
4674 if(!options::produceAssignments()) {
4677 if(d_assignments
== NULL
) {
4678 d_assignments
= new(true) AssignmentSet(d_context
);
4680 d_assignments
->insert(n
);
4685 CVC4::SExpr
SmtEngine::getAssignment() throw(ModalException
, UnsafeInterruptException
) {
4686 Trace("smt") << "SMT getAssignment()" << endl
;
4687 SmtScope
smts(this);
4688 finalOptionsAreSet();
4689 if(Dump
.isOn("benchmark")) {
4690 Dump("benchmark") << GetAssignmentCommand();
4692 if(!options::produceAssignments()) {
4694 "Cannot get the current assignment when "
4695 "produce-assignments option is off.";
4696 throw ModalException(msg
);
4698 if(d_status
.isNull() ||
4699 d_status
.asSatisfiabilityResult() == Result::UNSAT
||
4700 d_problemExtended
) {
4702 "Cannot get the current assignment unless immediately "
4703 "preceded by SAT/INVALID or UNKNOWN response.";
4704 throw ModalException(msg
);
4707 if(d_assignments
== NULL
) {
4708 return SExpr(vector
<SExpr
>());
4711 vector
<SExpr
> sexprs
;
4712 TypeNode boolType
= d_nodeManager
->booleanType();
4713 TheoryModel
* m
= d_theoryEngine
->getModel();
4714 for(AssignmentSet::key_iterator i
= d_assignments
->key_begin(),
4715 iend
= d_assignments
->key_end();
4718 Assert((*i
).getType() == boolType
);
4720 Trace("smt") << "--- getting value of " << *i
<< endl
;
4722 // Expand, then normalize
4723 hash_map
<Node
, Node
, NodeHashFunction
> cache
;
4724 Node n
= d_private
->expandDefinitions(*i
, cache
);
4725 n
= Rewriter::rewrite(n
);
4727 Trace("smt") << "--- getting value of " << n
<< endl
;
4730 resultNode
= m
->getValue(n
);
4733 // type-check the result we got
4734 Assert(resultNode
.isNull() || resultNode
.getType() == boolType
);
4736 // ensure it's a constant
4737 Assert(resultNode
.isConst());
4740 if((*i
).getKind() == kind::APPLY
) {
4741 Assert((*i
).getNumChildren() == 0);
4742 v
.push_back(SExpr(SExpr::Keyword((*i
).getOperator().toString())));
4744 Assert((*i
).isVar());
4745 v
.push_back(SExpr(SExpr::Keyword((*i
).toString())));
4747 v
.push_back(SExpr(SExpr::Keyword(resultNode
.toString())));
4748 sexprs
.push_back(SExpr(v
));
4750 return SExpr(sexprs
);
4753 void SmtEngine::addToModelCommandAndDump(const Command
& c
, uint32_t flags
, bool userVisible
, const char* dumpTag
) {
4754 Trace("smt") << "SMT addToModelCommandAndDump(" << c
<< ")" << endl
;
4755 SmtScope
smts(this);
4756 // If we aren't yet fully inited, the user might still turn on
4757 // produce-models. So let's keep any commands around just in
4758 // case. This is useful in two cases: (1) SMT-LIBv1 auto-declares
4759 // sort "U" in QF_UF before setLogic() is run and we still want to
4760 // support finding card(U) with --finite-model-find, and (2) to
4761 // decouple SmtEngine and ExprManager if the user does a few
4762 // ExprManager::mkSort() before SmtEngine::setOption("produce-models")
4763 // and expects to find their cardinalities in the model.
4764 if(/* userVisible && */
4765 (!d_fullyInited
|| options::produceModels()) &&
4766 (flags
& ExprManager::VAR_FLAG_DEFINED
) == 0) {
4768 if(flags
& ExprManager::VAR_FLAG_GLOBAL
) {
4769 d_modelGlobalCommands
.push_back(c
.clone());
4771 d_modelCommands
->push_back(c
.clone());
4774 if(Dump
.isOn(dumpTag
)) {
4778 d_dumpCommands
.push_back(c
.clone());
4783 Model
* SmtEngine::getModel() throw(ModalException
, UnsafeInterruptException
) {
4784 Trace("smt") << "SMT getModel()" << endl
;
4785 SmtScope
smts(this);
4787 finalOptionsAreSet();
4789 if(Dump
.isOn("benchmark")) {
4790 Dump("benchmark") << GetModelCommand();
4793 if(d_status
.isNull() ||
4794 d_status
.asSatisfiabilityResult() == Result::UNSAT
||
4795 d_problemExtended
) {
4797 "Cannot get the current model unless immediately "
4798 "preceded by SAT/INVALID or UNKNOWN response.";
4799 throw ModalException(msg
);
4801 if(!options::produceModels()) {
4803 "Cannot get model when produce-models options is off.";
4804 throw ModalException(msg
);
4806 TheoryModel
* m
= d_theoryEngine
->getModel();
4807 m
->d_inputName
= d_filename
;
4811 void SmtEngine::checkUnsatCore() {
4812 Assert(options::unsatCores(), "cannot check unsat core if unsat cores are turned off");
4814 Notice() << "SmtEngine::checkUnsatCore(): generating unsat core" << endl
;
4815 UnsatCore core
= getUnsatCore();
4817 SmtEngine
coreChecker(d_exprManager
);
4818 coreChecker
.setLogic(getLogicInfo());
4821 std::vector
<Command
*>::const_iterator itg
= d_defineCommands
.begin();
4822 for (; itg
!= d_defineCommands
.end(); ++itg
) {
4823 (*itg
)->invoke(&coreChecker
);
4827 Notice() << "SmtEngine::checkUnsatCore(): pushing core assertions (size == " << core
.size() << ")" << endl
;
4828 for(UnsatCore::iterator i
= core
.begin(); i
!= core
.end(); ++i
) {
4829 Notice() << "SmtEngine::checkUnsatCore(): pushing core member " << *i
<< endl
;
4830 coreChecker
.assertFormula(*i
);
4832 const bool checkUnsatCores
= options::checkUnsatCores();
4835 options::checkUnsatCores
.set(false);
4836 options::checkProofs
.set(false);
4837 r
= coreChecker
.checkSat();
4839 options::checkUnsatCores
.set(checkUnsatCores
);
4842 Notice() << "SmtEngine::checkUnsatCore(): result is " << r
<< endl
;
4843 if(r
.asSatisfiabilityResult().isUnknown()) {
4844 InternalError("SmtEngine::checkUnsatCore(): could not check core result unknown.");
4847 if(r
.asSatisfiabilityResult().isSat()) {
4848 InternalError("SmtEngine::checkUnsatCore(): produced core was satisfiable.");
4852 void SmtEngine::checkModel(bool hardFailure
) {
4853 // --check-model implies --produce-assertions, which enables the
4854 // assertion list, so we should be ok.
4855 Assert(d_assertionList
!= NULL
, "don't have an assertion list to check in SmtEngine::checkModel()");
4857 TimerStat::CodeTimer
checkModelTimer(d_stats
->d_checkModelTime
);
4859 // Throughout, we use Notice() to give diagnostic output.
4861 // If this function is running, the user gave --check-model (or equivalent),
4862 // and if Notice() is on, the user gave --verbose (or equivalent).
4864 Notice() << "SmtEngine::checkModel(): generating model" << endl
;
4865 TheoryModel
* m
= d_theoryEngine
->getModel();
4867 // Check individual theory assertions
4868 d_theoryEngine
->checkTheoryAssertionsWithModel();
4873 // We have a "fake context" for the substitution map (we don't need it
4874 // to be context-dependent)
4875 context::Context fakeContext
;
4876 SubstitutionMap
substitutions(&fakeContext
, /* substituteUnderQuantifiers = */ false);
4878 for(size_t k
= 0; k
< m
->getNumCommands(); ++k
) {
4879 const DeclareFunctionCommand
* c
= dynamic_cast<const DeclareFunctionCommand
*>(m
->getCommand(k
));
4880 Notice() << "SmtEngine::checkModel(): model command " << k
<< " : " << m
->getCommand(k
) << endl
;
4882 // we don't care about DECLARE-DATATYPES, DECLARE-SORT, ...
4883 Notice() << "SmtEngine::checkModel(): skipping..." << endl
;
4885 // We have a DECLARE-FUN:
4887 // We'll first do some checks, then add to our substitution map
4888 // the mapping: function symbol |-> value
4890 Expr func
= c
->getFunction();
4891 Node val
= m
->getValue(func
);
4893 Notice() << "SmtEngine::checkModel(): adding substitution: " << func
<< " |-> " << val
<< endl
;
4895 // (1) if the value is a lambda, ensure the lambda doesn't contain the
4896 // function symbol (since then the definition is recursive)
4897 if (val
.getKind() == kind::LAMBDA
) {
4898 // first apply the model substitutions we have so far
4899 Debug("boolean-terms") << "applying subses to " << val
[1] << endl
;
4900 Node n
= substitutions
.apply(val
[1]);
4901 Debug("boolean-terms") << "++ got " << n
<< endl
;
4902 // now check if n contains func by doing a substitution
4903 // [func->func2] and checking equality of the Nodes.
4904 // (this just a way to check if func is in n.)
4905 SubstitutionMap
subs(&fakeContext
);
4906 Node func2
= NodeManager::currentNM()->mkSkolem("", TypeNode::fromType(func
.getType()), "", NodeManager::SKOLEM_NO_NOTIFY
);
4907 subs
.addSubstitution(func
, func2
);
4908 if(subs
.apply(n
) != n
) {
4909 Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE DEFINED IN TERMS OF ITSELF ***" << endl
;
4911 ss
<< "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
4912 << "considering model value for " << func
<< endl
4913 << "body of lambda is: " << val
<< endl
;
4915 ss
<< "body substitutes to: " << n
<< endl
;
4917 ss
<< "so " << func
<< " is defined in terms of itself." << endl
4918 << "Run with `--check-models -v' for additional diagnostics.";
4919 InternalError(ss
.str());
4923 // (2) check that the value is actually a value
4924 else if (!val
.isConst()) {
4925 Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE NOT A CONSTANT ***" << endl
;
4927 ss
<< "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
4928 << "model value for " << func
<< endl
4929 << " is " << val
<< endl
4930 << "and that is not a constant (.isConst() == false)." << endl
4931 << "Run with `--check-models -v' for additional diagnostics.";
4932 InternalError(ss
.str());
4935 // (3) check that it's the correct (sub)type
4936 // This was intended to be a more general check, but for now we can't do that because
4937 // e.g. "1" is an INT, which isn't a subrange type [1..10] (etc.).
4938 else if(func
.getType().isInteger() && !val
.getType().isInteger()) {
4939 Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE NOT CORRECT TYPE ***" << endl
;
4941 ss
<< "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
4942 << "model value for " << func
<< endl
4943 << " is " << val
<< endl
4944 << "value type is " << val
.getType() << endl
4945 << "should be of type " << func
.getType() << endl
4946 << "Run with `--check-models -v' for additional diagnostics.";
4947 InternalError(ss
.str());
4950 // (4) checks complete, add the substitution
4951 Debug("boolean-terms") << "cm: adding subs " << func
<< " :=> " << val
<< endl
;
4952 substitutions
.addSubstitution(func
, val
);
4956 // Now go through all our user assertions checking if they're satisfied.
4957 for(AssertionList::const_iterator i
= d_assertionList
->begin(); i
!= d_assertionList
->end(); ++i
) {
4958 Notice() << "SmtEngine::checkModel(): checking assertion " << *i
<< endl
;
4959 Node n
= Node::fromExpr(*i
);
4961 // Apply any define-funs from the problem.
4963 hash_map
<Node
, Node
, NodeHashFunction
> cache
;
4964 n
= d_private
->expandDefinitions(n
, cache
);
4966 Notice() << "SmtEngine::checkModel(): -- expands to " << n
<< endl
;
4968 // Apply our model value substitutions.
4969 Debug("boolean-terms") << "applying subses to " << n
<< endl
;
4970 n
= substitutions
.apply(n
);
4971 Debug("boolean-terms") << "++ got " << n
<< endl
;
4972 Notice() << "SmtEngine::checkModel(): -- substitutes to " << n
<< endl
;
4974 if( n
.getKind() != kind::REWRITE_RULE
){
4975 // In case it's a quantifier (or contains one), look up its value before
4976 // simplifying, or the quantifier might be irreparably altered.
4978 Notice() << "SmtEngine::checkModel(): -- get value : " << n
<< std::endl
;
4980 // Note this "skip" is done here, rather than above. This is
4981 // because (1) the quantifier could in principle simplify to false,
4982 // which should be reported, and (2) checking for the quantifier
4983 // above, before simplification, doesn't catch buried quantifiers
4984 // anyway (those not at the top-level).
4985 Notice() << "SmtEngine::checkModel(): -- skipping rewrite-rules assertion"
4990 // Simplify the result.
4991 n
= d_private
->simplify(n
);
4992 Notice() << "SmtEngine::checkModel(): -- simplifies to " << n
<< endl
;
4994 // Replace the already-known ITEs (this is important for ground ITEs under quantifiers).
4995 n
= d_private
->d_iteRemover
.replace(n
);
4996 Notice() << "SmtEngine::checkModel(): -- ite replacement gives " << n
<< endl
;
4998 // Apply our model value substitutions (again), as things may have been simplified.
4999 Debug("boolean-terms") << "applying subses to " << n
<< endl
;
5000 n
= substitutions
.apply(n
);
5001 Debug("boolean-terms") << "++ got " << n
<< endl
;
5002 Notice() << "SmtEngine::checkModel(): -- re-substitutes to " << n
<< endl
;
5004 // As a last-ditch effort, ask model to simplify it.
5005 // Presently, this is only an issue for quantifiers, which can have a value
5006 // but don't show up in our substitution map above.
5008 Notice() << "SmtEngine::checkModel(): -- model-substitutes to " << n
<< endl
;
5010 if( d_logic
.isQuantified() ){
5011 // AJR: since quantified formulas are not checkable, we assign them to true/false based on the satisfying assignment.
5012 // however, quantified formulas can be modified during preprocess, so they may not correspond to those in the satisfying assignment.
5013 // hence we use a relaxed version of check model here.
5014 // this is necessary until preprocessing passes explicitly record how they rewrite quantified formulas
5015 if( hardFailure
&& !n
.isConst() && n
.getKind() != kind::LAMBDA
){
5016 Notice() << "SmtEngine::checkModel(): -- relax check model wrt quantified formulas..." << endl
;
5017 AlwaysAssert( quantifiers::QuantifiersRewriter::containsQuantifiers( n
) );
5018 Warning() << "Warning : SmtEngine::checkModel(): cannot check simplified assertion : " << n
<< endl
;
5022 AlwaysAssert(!hardFailure
|| n
.isConst() || n
.getKind() == kind::LAMBDA
);
5024 // The result should be == true.
5025 if(n
!= NodeManager::currentNM()->mkConst(true)) {
5026 Notice() << "SmtEngine::checkModel(): *** PROBLEM: EXPECTED `TRUE' ***"
5029 ss
<< "SmtEngine::checkModel(): "
5030 << "ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
5031 << "assertion: " << *i
<< endl
5032 << "simplifies to: " << n
<< endl
5033 << "expected `true'." << endl
5034 << "Run with `--check-models -v' for additional diagnostics.";
5036 InternalError(ss
.str());
5038 Warning() << ss
.str() << endl
;
5042 Notice() << "SmtEngine::checkModel(): all assertions checked out OK !" << endl
;
5045 UnsatCore
SmtEngine::getUnsatCore() throw(ModalException
, UnsafeInterruptException
) {
5046 Trace("smt") << "SMT getUnsatCore()" << endl
;
5047 SmtScope
smts(this);
5048 finalOptionsAreSet();
5049 if(Dump
.isOn("benchmark")) {
5050 Dump("benchmark") << GetUnsatCoreCommand();
5053 if(!options::unsatCores()) {
5054 throw ModalException("Cannot get an unsat core when produce-unsat-cores option is off.");
5056 if(d_status
.isNull() ||
5057 d_status
.asSatisfiabilityResult() != Result::UNSAT
||
5058 d_problemExtended
) {
5059 throw ModalException("Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.");
5062 d_proofManager
->traceUnsatCore();// just to trigger core creation
5063 return UnsatCore(this, d_proofManager
->extractUnsatCore());
5064 #else /* IS_PROOFS_BUILD */
5065 throw ModalException("This build of CVC4 doesn't have proof support (required for unsat cores).");
5066 #endif /* IS_PROOFS_BUILD */
5069 Proof
* SmtEngine::getProof() throw(ModalException
, UnsafeInterruptException
) {
5070 Trace("smt") << "SMT getProof()" << endl
;
5071 SmtScope
smts(this);
5072 finalOptionsAreSet();
5073 if(Dump
.isOn("benchmark")) {
5074 Dump("benchmark") << GetProofCommand();
5077 if(!options::proof()) {
5078 throw ModalException("Cannot get a proof when produce-proofs option is off.");
5080 if(d_status
.isNull() ||
5081 d_status
.asSatisfiabilityResult() != Result::UNSAT
||
5082 d_problemExtended
) {
5083 throw ModalException("Cannot get a proof unless immediately preceded by UNSAT/VALID response.");
5086 return ProofManager::getProof(this);
5087 #else /* IS_PROOFS_BUILD */
5088 throw ModalException("This build of CVC4 doesn't have proof support.");
5089 #endif /* IS_PROOFS_BUILD */
5092 void SmtEngine::printInstantiations( std::ostream
& out
) {
5093 SmtScope
smts(this);
5094 if( options::instFormatMode()==INST_FORMAT_MODE_SZS
){
5095 out
<< "% SZS output start Proof for " << d_filename
.c_str() << std::endl
;
5097 if( d_theoryEngine
){
5098 d_theoryEngine
->printInstantiations( out
);
5102 if( options::instFormatMode()==INST_FORMAT_MODE_SZS
){
5103 out
<< "% SZS output end Proof for " << d_filename
.c_str() << std::endl
;
5107 void SmtEngine::printSynthSolution( std::ostream
& out
) {
5108 SmtScope
smts(this);
5109 if( d_theoryEngine
){
5110 d_theoryEngine
->printSynthSolution( out
);
5116 Expr
SmtEngine::doQuantifierElimination(const Expr
& e
, bool doFull
, bool strict
) throw(TypeCheckingException
, ModalException
, LogicException
) {
5117 SmtScope
smts(this);
5118 if(!d_logic
.isPure(THEORY_ARITH
) && strict
){
5119 Warning() << "Unexpected logic for quantifier elimination " << d_logic
<< endl
;
5121 Trace("smt-qe") << "Do quantifier elimination " << e
<< std::endl
;
5122 Node n_e
= Node::fromExpr( e
);
5123 if( n_e
.getKind()!=kind::EXISTS
){
5124 throw ModalException("Expecting an existentially quantified formula as argument to get-qe.");
5126 //tag the quantified formula with the quant-elim attribute
5127 TypeNode t
= NodeManager::currentNM()->booleanType();
5128 Node n_attr
= NodeManager::currentNM()->mkSkolem("qe", t
, "Auxiliary variable for qe attr.");
5129 std::vector
< Node
> node_values
;
5130 d_theoryEngine
->setUserAttribute( doFull
? "quant-elim" : "quant-elim-partial", n_attr
, node_values
, "");
5131 n_attr
= NodeManager::currentNM()->mkNode(kind::INST_ATTRIBUTE
, n_attr
);
5132 n_attr
= NodeManager::currentNM()->mkNode(kind::INST_PATTERN_LIST
, n_attr
);
5133 std::vector
< Node
> e_children
;
5134 e_children
.push_back( n_e
[0] );
5135 e_children
.push_back( n_e
[1] );
5136 e_children
.push_back( n_attr
);
5137 Node nn_e
= NodeManager::currentNM()->mkNode( kind::EXISTS
, e_children
);
5138 Trace("smt-qe-debug") << "Query for quantifier elimination : " << nn_e
<< std::endl
;
5139 Assert( nn_e
.getNumChildren()==3 );
5140 Result r
= checkSatisfiability(nn_e
.toExpr(), true, true);
5141 Trace("smt-qe") << "Query returned " << r
<< std::endl
;
5142 if(r
.asSatisfiabilityResult().isSat() != Result::UNSAT
) {
5143 if( r
.asSatisfiabilityResult().isSat() != Result::SAT
&& doFull
){
5145 ss
<< "While performing quantifier elimination, unexpected result : " << r
<< " for query.";
5146 InternalError(ss
.str().c_str());
5149 Node top_q
= Rewriter::rewrite( nn_e
).negate();
5150 Assert( top_q
.getKind()==kind::FORALL
);
5151 Trace("smt-qe") << "Get qe for " << top_q
<< std::endl
;
5152 Node ret_n
= d_theoryEngine
->getInstantiatedConjunction( top_q
);
5153 Trace("smt-qe") << "Returned : " << ret_n
<< std::endl
;
5154 ret_n
= Rewriter::rewrite( ret_n
.negate() );
5155 return ret_n
.toExpr();
5157 return NodeManager::currentNM()->mkConst(true).toExpr();
5161 void SmtEngine::getInstantiatedQuantifiedFormulas( std::vector
< Expr
>& qs
) {
5162 SmtScope
smts(this);
5163 if( d_theoryEngine
){
5164 std::vector
< Node
> qs_n
;
5165 d_theoryEngine
->getInstantiatedQuantifiedFormulas( qs_n
);
5166 for( unsigned i
=0; i
<qs_n
.size(); i
++ ){
5167 qs
.push_back( qs_n
[i
].toExpr() );
5174 void SmtEngine::getInstantiations( Expr q
, std::vector
< Expr
>& insts
) {
5175 SmtScope
smts(this);
5176 if( d_theoryEngine
){
5177 std::vector
< Node
> insts_n
;
5178 d_theoryEngine
->getInstantiations( Node::fromExpr( q
), insts_n
);
5179 for( unsigned i
=0; i
<insts_n
.size(); i
++ ){
5180 insts
.push_back( insts_n
[i
].toExpr() );
5187 void SmtEngine::getInstantiationTermVectors( Expr q
, std::vector
< std::vector
< Expr
> >& tvecs
) {
5188 SmtScope
smts(this);
5189 Assert(options::trackInstLemmas());
5190 if( d_theoryEngine
){
5191 std::vector
< std::vector
< Node
> > tvecs_n
;
5192 d_theoryEngine
->getInstantiationTermVectors( Node::fromExpr( q
), tvecs_n
);
5193 for( unsigned i
=0; i
<tvecs_n
.size(); i
++ ){
5194 std::vector
< Expr
> tvec
;
5195 for( unsigned j
=0; j
<tvecs_n
[i
].size(); j
++ ){
5196 tvec
.push_back( tvecs_n
[i
][j
].toExpr() );
5198 tvecs
.push_back( tvec
);
5205 vector
<Expr
> SmtEngine::getAssertions() throw(ModalException
) {
5206 SmtScope
smts(this);
5207 finalOptionsAreSet();
5209 if(Dump
.isOn("benchmark")) {
5210 Dump("benchmark") << GetAssertionsCommand();
5212 Trace("smt") << "SMT getAssertions()" << endl
;
5213 if(!options::produceAssertions()) {
5215 "Cannot query the current assertion list when not in produce-assertions mode.";
5216 throw ModalException(msg
);
5218 Assert(d_assertionList
!= NULL
);
5219 // copy the result out
5220 return vector
<Expr
>(d_assertionList
->begin(), d_assertionList
->end());
5223 void SmtEngine::push() throw(ModalException
, LogicException
, UnsafeInterruptException
) {
5224 SmtScope
smts(this);
5225 finalOptionsAreSet();
5227 Trace("smt") << "SMT push()" << endl
;
5228 d_private
->processAssertions();
5229 if(Dump
.isOn("benchmark")) {
5230 Dump("benchmark") << PushCommand();
5232 if(!options::incrementalSolving()) {
5233 throw ModalException("Cannot push when not solving incrementally (use --incremental)");
5236 // check to see if a postsolve() is pending
5237 if(d_needPostsolve
) {
5238 d_theoryEngine
->postsolve();
5239 d_needPostsolve
= false;
5242 // The problem isn't really "extended" yet, but this disallows
5243 // get-model after a push, simplifying our lives somewhat and
5244 // staying symmtric with pop.
5245 d_problemExtended
= true;
5247 d_userLevels
.push_back(d_userContext
->getLevel());
5249 Trace("userpushpop") << "SmtEngine: pushed to level "
5250 << d_userContext
->getLevel() << endl
;
5253 void SmtEngine::pop() throw(ModalException
, UnsafeInterruptException
) {
5254 SmtScope
smts(this);
5255 finalOptionsAreSet();
5256 Trace("smt") << "SMT pop()" << endl
;
5257 if(Dump
.isOn("benchmark")) {
5258 Dump("benchmark") << PopCommand();
5260 if(!options::incrementalSolving()) {
5261 throw ModalException("Cannot pop when not solving incrementally (use --incremental)");
5263 if(d_userLevels
.size() == 0) {
5264 throw ModalException("Cannot pop beyond the first user frame");
5267 // check to see if a postsolve() is pending
5268 if(d_needPostsolve
) {
5269 d_theoryEngine
->postsolve();
5270 d_needPostsolve
= false;
5273 // The problem isn't really "extended" yet, but this disallows
5274 // get-model after a pop, simplifying our lives somewhat. It might
5275 // not be strictly necessary to do so, since the pops occur lazily,
5276 // but also it would be weird to have a legally-executed (get-model)
5277 // that only returns a subset of the assignment (because the rest
5278 // is no longer in scope!).
5279 d_problemExtended
= true;
5281 AlwaysAssert(d_userContext
->getLevel() > 0);
5282 AlwaysAssert(d_userLevels
.back() < d_userContext
->getLevel());
5283 while (d_userLevels
.back() < d_userContext
->getLevel()) {
5286 d_userLevels
.pop_back();
5288 // Clear out assertion queues etc., in case anything is still in there
5289 d_private
->notifyPop();
5291 Trace("userpushpop") << "SmtEngine: popped to level "
5292 << d_userContext
->getLevel() << endl
;
5293 // FIXME: should we reset d_status here?
5294 // SMT-LIBv2 spec seems to imply no, but it would make sense to..
5297 void SmtEngine::internalPush() {
5298 Assert(d_fullyInited
);
5299 Trace("smt") << "SmtEngine::internalPush()" << endl
;
5301 if(options::incrementalSolving()) {
5302 d_private
->processAssertions();
5303 TimerStat::CodeTimer
pushPopTimer(d_stats
->d_pushPopTime
);
5304 d_userContext
->push();
5305 // the d_context push is done inside of the SAT solver
5306 d_propEngine
->push();
5310 void SmtEngine::internalPop(bool immediate
) {
5311 Assert(d_fullyInited
);
5312 Trace("smt") << "SmtEngine::internalPop()" << endl
;
5313 if(options::incrementalSolving()) {
5321 void SmtEngine::doPendingPops() {
5322 Assert(d_pendingPops
== 0 || options::incrementalSolving());
5323 while(d_pendingPops
> 0) {
5324 TimerStat::CodeTimer
pushPopTimer(d_stats
->d_pushPopTime
);
5325 d_propEngine
->pop();
5326 // the d_context pop is done inside of the SAT solver
5327 d_userContext
->pop();
5332 void SmtEngine::reset() throw() {
5333 SmtScope
smts(this);
5334 ExprManager
*em
= d_exprManager
;
5335 Trace("smt") << "SMT reset()" << endl
;
5336 if(Dump
.isOn("benchmark")) {
5337 Dump("benchmark") << ResetCommand();
5340 opts
.copyValues(d_originalOptions
);
5342 NodeManager::fromExprManager(em
)->getOptions().copyValues(opts
);
5343 new(this) SmtEngine(em
);
5346 void SmtEngine::resetAssertions() throw() {
5347 SmtScope
smts(this);
5349 Trace("smt") << "SMT resetAssertions()" << endl
;
5350 if(Dump
.isOn("benchmark")) {
5351 Dump("benchmark") << ResetAssertionsCommand();
5354 while(!d_userLevels
.empty()) {
5358 // Also remember the global push/pop around everything.
5359 Assert(d_userLevels
.size() == 0 && d_userContext
->getLevel() == 1);
5360 d_context
->popto(0);
5361 d_userContext
->popto(0);
5362 DeleteAndClearCommandVector(d_modelGlobalCommands
);
5363 d_userContext
->push();
5367 void SmtEngine::interrupt() throw(ModalException
) {
5368 if(!d_fullyInited
) {
5371 d_propEngine
->interrupt();
5372 d_theoryEngine
->interrupt();
5375 void SmtEngine::setResourceLimit(unsigned long units
, bool cumulative
) {
5376 d_private
->getResourceManager()->setResourceLimit(units
, cumulative
);
5378 void SmtEngine::setTimeLimit(unsigned long milis
, bool cumulative
) {
5379 d_private
->getResourceManager()->setTimeLimit(milis
, cumulative
);
5382 unsigned long SmtEngine::getResourceUsage() const {
5383 return d_private
->getResourceManager()->getResourceUsage();
5386 unsigned long SmtEngine::getTimeUsage() const {
5387 return d_private
->getResourceManager()->getTimeUsage();
5390 unsigned long SmtEngine::getResourceRemaining() const throw(ModalException
) {
5391 return d_private
->getResourceManager()->getResourceRemaining();
5394 unsigned long SmtEngine::getTimeRemaining() const throw(ModalException
) {
5395 return d_private
->getResourceManager()->getTimeRemaining();
5398 Statistics
SmtEngine::getStatistics() const throw() {
5399 return Statistics(*d_statisticsRegistry
);
5402 SExpr
SmtEngine::getStatistic(std::string name
) const throw() {
5403 return d_statisticsRegistry
->getStatistic(name
);
5406 void SmtEngine::setUserAttribute(const std::string
& attr
, Expr expr
, std::vector
<Expr
> expr_values
, std::string str_value
) {
5407 SmtScope
smts(this);
5408 std::vector
<Node
> node_values
;
5409 for( unsigned i
=0; i
<expr_values
.size(); i
++ ){
5410 node_values
.push_back( expr_values
[i
].getNode() );
5412 d_theoryEngine
->setUserAttribute(attr
, expr
.getNode(), node_values
, str_value
);
5415 void SmtEngine::setPrintFuncInModel(Expr f
, bool p
) {
5416 Trace("setp-model") << "Set printInModel " << f
<< " to " << p
<< std::endl
;
5417 for( unsigned i
=0; i
<d_modelGlobalCommands
.size(); i
++ ){
5418 Command
* c
= d_modelGlobalCommands
[i
];
5419 DeclareFunctionCommand
* dfc
= dynamic_cast<DeclareFunctionCommand
*>(c
);
5421 if( dfc
->getFunction()==f
){
5422 dfc
->setPrintInModel( p
);
5426 for( unsigned i
=0; i
<d_modelCommands
->size(); i
++ ){
5427 Command
* c
= (*d_modelCommands
)[i
];
5428 DeclareFunctionCommand
* dfc
= dynamic_cast<DeclareFunctionCommand
*>(c
);
5430 if( dfc
->getFunction()==f
){
5431 dfc
->setPrintInModel( p
);
5439 void SmtEngine::beforeSearch() throw(ModalException
) {
5441 throw ModalException(
5442 "SmtEngine::beforeSearch called after initialization.");
5447 void SmtEngine::setOption(const std::string
& key
, const CVC4::SExpr
& value
)
5448 throw(OptionException
, ModalException
) {
5450 NodeManagerScope
nms(d_nodeManager
);
5451 Trace("smt") << "SMT setOption(" << key
<< ", " << value
<< ")" << endl
;
5453 if(Dump
.isOn("benchmark")) {
5454 Dump("benchmark") << SetOptionCommand(key
, value
);
5457 if(key
== "command-verbosity") {
5458 if(!value
.isAtom()) {
5459 const vector
<SExpr
>& cs
= value
.getChildren();
5460 if(cs
.size() == 2 &&
5461 (cs
[0].isKeyword() || cs
[0].isString()) &&
5462 cs
[1].isInteger()) {
5463 string c
= cs
[0].getValue();
5464 const Integer
& v
= cs
[1].getIntegerValue();
5465 if(v
< 0 || v
> 2) {
5466 throw OptionException("command-verbosity must be 0, 1, or 2");
5468 d_commandVerbosity
[c
] = v
;
5472 throw OptionException("command-verbosity value must be a tuple (command-name, integer)");
5475 if(!value
.isAtom()) {
5476 throw OptionException("bad value for :" + key
);
5479 string optionarg
= value
.getValue();
5480 Options
& nodeManagerOptions
= NodeManager::currentNM()->getOptions();
5481 nodeManagerOptions
.setOption(key
, optionarg
);
5484 CVC4::SExpr
SmtEngine::getOption(const std::string
& key
) const
5485 throw(OptionException
) {
5487 NodeManagerScope
nms(d_nodeManager
);
5489 Trace("smt") << "SMT getOption(" << key
<< ")" << endl
;
5491 if(key
.length() >= 18 &&
5492 key
.compare(0, 18, "command-verbosity:") == 0) {
5493 map
<string
, Integer
>::const_iterator i
= d_commandVerbosity
.find(key
.c_str() + 18);
5494 if(i
!= d_commandVerbosity
.end()) {
5495 return SExpr((*i
).second
);
5497 i
= d_commandVerbosity
.find("*");
5498 if(i
!= d_commandVerbosity
.end()) {
5499 return SExpr((*i
).second
);
5501 return SExpr(Integer(2));
5504 if(Dump
.isOn("benchmark")) {
5505 Dump("benchmark") << GetOptionCommand(key
);
5508 if(key
== "command-verbosity") {
5509 vector
<SExpr
> result
;
5510 SExpr defaultVerbosity
;
5511 for(map
<string
, Integer
>::const_iterator i
= d_commandVerbosity
.begin();
5512 i
!= d_commandVerbosity
.end();
5515 v
.push_back(SExpr((*i
).first
));
5516 v
.push_back(SExpr((*i
).second
));
5517 if((*i
).first
== "*") {
5518 // put the default at the end of the SExpr
5519 defaultVerbosity
= SExpr(v
);
5521 result
.push_back(SExpr(v
));
5524 // put the default at the end of the SExpr
5525 if(!defaultVerbosity
.isAtom()) {
5526 result
.push_back(defaultVerbosity
);
5528 // ensure the default is always listed
5530 v
.push_back(SExpr("*"));
5531 v
.push_back(SExpr(Integer(2)));
5532 result
.push_back(SExpr(v
));
5534 return SExpr(result
);
5537 Options
& nodeManagerOptions
= NodeManager::currentNM()->getOptions();
5538 return SExpr::parseAtom(nodeManagerOptions
.getOption(key
));
5541 void SmtEngine::setReplayStream(ExprStream
* replayStream
) {
5542 AlwaysAssert(!d_fullyInited
,
5543 "Cannot set replay stream once fully initialized");
5544 d_replayStream
= replayStream
;
5547 }/* CVC4 namespace */