1 /********************* */
2 /*! \file smt_engine.cpp
4 ** Top contributors (to current version):
5 ** Morgan Deters, Andrew Reynolds, Tim King
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
8 ** in the top-level source directory) and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
12 ** \brief The main entry point into the CVC4 library's SMT interface
14 ** The main entry point into the CVC4 library's SMT interface.
17 #include "smt/smt_engine.h"
27 #include <unordered_map>
28 #include <unordered_set>
32 #include "base/configuration.h"
33 #include "base/configuration_private.h"
34 #include "base/exception.h"
35 #include "base/listener.h"
36 #include "base/modal_exception.h"
37 #include "base/output.h"
38 #include "context/cdhashmap.h"
39 #include "context/cdhashset.h"
40 #include "context/cdlist.h"
41 #include "context/context.h"
42 #include "decision/decision_engine.h"
43 #include "expr/attribute.h"
44 #include "expr/expr.h"
45 #include "expr/kind.h"
46 #include "expr/metakind.h"
47 #include "expr/node.h"
48 #include "expr/node_builder.h"
49 #include "expr/node_self_iterator.h"
50 #include "options/arith_options.h"
51 #include "options/arrays_options.h"
52 #include "options/base_options.h"
53 #include "options/booleans_options.h"
54 #include "options/bv_options.h"
55 #include "options/datatypes_options.h"
56 #include "options/decision_mode.h"
57 #include "options/decision_options.h"
58 #include "options/language.h"
59 #include "options/main_options.h"
60 #include "options/open_ostream.h"
61 #include "options/option_exception.h"
62 #include "options/printer_options.h"
63 #include "options/proof_options.h"
64 #include "options/prop_options.h"
65 #include "options/quantifiers_options.h"
66 #include "options/sep_options.h"
67 #include "options/set_language.h"
68 #include "options/smt_options.h"
69 #include "options/strings_options.h"
70 #include "options/theory_options.h"
71 #include "options/uf_options.h"
72 #include "preprocessing/passes/apply_substs.h"
73 #include "preprocessing/passes/apply_to_const.h"
74 #include "preprocessing/passes/bool_to_bv.h"
75 #include "preprocessing/passes/bv_abstraction.h"
76 #include "preprocessing/passes/bv_ackermann.h"
77 #include "preprocessing/passes/bv_eager_atoms.h"
78 #include "preprocessing/passes/bv_gauss.h"
79 #include "preprocessing/passes/bv_intro_pow2.h"
80 #include "preprocessing/passes/bv_to_bool.h"
81 #include "preprocessing/passes/extended_rewriter_pass.h"
82 #include "preprocessing/passes/int_to_bv.h"
83 #include "preprocessing/passes/ite_removal.h"
84 #include "preprocessing/passes/pseudo_boolean_processor.h"
85 #include "preprocessing/passes/quantifiers_preprocess.h"
86 #include "preprocessing/passes/real_to_int.h"
87 #include "preprocessing/passes/rewrite.h"
88 #include "preprocessing/passes/sep_skolem_emp.h"
89 #include "preprocessing/passes/sort_infer.h"
90 #include "preprocessing/passes/static_learning.h"
91 #include "preprocessing/passes/sygus_inference.h"
92 #include "preprocessing/passes/symmetry_breaker.h"
93 #include "preprocessing/passes/symmetry_detect.h"
94 #include "preprocessing/passes/synth_rew_rules.h"
95 #include "preprocessing/preprocessing_pass.h"
96 #include "preprocessing/preprocessing_pass_context.h"
97 #include "preprocessing/preprocessing_pass_registry.h"
98 #include "printer/printer.h"
99 #include "proof/proof.h"
100 #include "proof/proof_manager.h"
101 #include "proof/theory_proof.h"
102 #include "proof/unsat_core.h"
103 #include "prop/prop_engine.h"
104 #include "smt/command.h"
105 #include "smt/command_list.h"
106 #include "smt/logic_request.h"
107 #include "smt/managed_ostreams.h"
108 #include "smt/smt_engine_scope.h"
109 #include "smt/term_formula_removal.h"
110 #include "smt/update_ostream.h"
111 #include "smt_util/boolean_simplification.h"
112 #include "smt_util/nary_builder.h"
113 #include "smt_util/node_visitor.h"
114 #include "theory/booleans/circuit_propagator.h"
115 #include "theory/bv/theory_bv_rewriter.h"
116 #include "theory/logic_info.h"
117 #include "theory/quantifiers/fun_def_process.h"
118 #include "theory/quantifiers/global_negate.h"
119 #include "theory/quantifiers/macros.h"
120 #include "theory/quantifiers/quantifiers_rewriter.h"
121 #include "theory/quantifiers/single_inv_partition.h"
122 #include "theory/quantifiers/sygus/ce_guided_instantiation.h"
123 #include "theory/quantifiers/term_util.h"
124 #include "theory/rewriter.h"
125 #include "theory/sort_inference.h"
126 #include "theory/strings/theory_strings.h"
127 #include "theory/substitutions.h"
128 #include "theory/theory_engine.h"
129 #include "theory/theory_model.h"
130 #include "theory/theory_traits.h"
131 #include "util/hash.h"
132 #include "util/proof.h"
133 #include "util/random.h"
134 #include "util/resource_manager.h"
137 using namespace CVC4
;
138 using namespace CVC4::smt
;
139 using namespace CVC4::preprocessing
;
140 using namespace CVC4::preprocessing::passes
;
141 using namespace CVC4::prop
;
142 using namespace CVC4::context
;
143 using namespace CVC4::theory
;
148 struct DeleteCommandFunction
: public std::unary_function
<const Command
*, void>
150 void operator()(const Command
* command
) { delete command
; }
153 void DeleteAndClearCommandVector(std::vector
<Command
*>& commands
) {
154 std::for_each(commands
.begin(), commands
.end(), DeleteCommandFunction());
158 /** Useful for counting the number of recursive calls. */
163 ScopeCounter(unsigned& d
) : d_depth(d
) {
172 * Representation of a defined function. We keep these around in
173 * SmtEngine to permit expanding definitions late (and lazily), to
174 * support getValue() over defined functions, to support user output
175 * in terms of defined functions, etc.
177 class DefinedFunction
{
179 vector
<Node
> d_formals
;
183 DefinedFunction(Node func
, vector
<Node
> formals
, Node formula
) :
188 Node
getFunction() const { return d_func
; }
189 vector
<Node
> getFormals() const { return d_formals
; }
190 Node
getFormula() const { return d_formula
; }
191 };/* class DefinedFunction */
193 struct SmtEngineStatistics
{
194 /** time spent in definition-expansion */
195 TimerStat d_definitionExpansionTime
;
196 /** time spent in non-clausal simplification */
197 TimerStat d_nonclausalSimplificationTime
;
198 /** time spent in miplib pass */
199 TimerStat d_miplibPassTime
;
200 /** number of assertions removed by miplib pass */
201 IntStat d_numMiplibAssertionsRemoved
;
202 /** number of constant propagations found during nonclausal simp */
203 IntStat d_numConstantProps
;
204 /** time spent in simplifying ITEs */
205 TimerStat d_simpITETime
;
206 /** time spent in simplifying ITEs */
207 TimerStat d_unconstrainedSimpTime
;
208 /** time spent in theory preprocessing */
209 TimerStat d_theoryPreprocessTime
;
210 /** time spent converting to CNF */
211 TimerStat d_cnfConversionTime
;
212 /** Num of assertions before ite removal */
213 IntStat d_numAssertionsPre
;
214 /** Num of assertions after ite removal */
215 IntStat d_numAssertionsPost
;
216 /** time spent in checkModel() */
217 TimerStat d_checkModelTime
;
218 /** time spent in checkProof() */
219 TimerStat d_checkProofTime
;
220 /** time spent in checkUnsatCore() */
221 TimerStat d_checkUnsatCoreTime
;
222 /** time spent in PropEngine::checkSat() */
223 TimerStat d_solveTime
;
224 /** time spent in pushing/popping */
225 TimerStat d_pushPopTime
;
226 /** time spent in processAssertions() */
227 TimerStat d_processAssertionsTime
;
229 /** Has something simplified to false? */
230 IntStat d_simplifiedToFalse
;
231 /** Number of resource units spent. */
232 ReferenceStat
<uint64_t> d_resourceUnitsUsed
;
234 SmtEngineStatistics() :
235 d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"),
236 d_nonclausalSimplificationTime("smt::SmtEngine::nonclausalSimplificationTime"),
237 d_miplibPassTime("smt::SmtEngine::miplibPassTime"),
238 d_numMiplibAssertionsRemoved("smt::SmtEngine::numMiplibAssertionsRemoved", 0),
239 d_numConstantProps("smt::SmtEngine::numConstantProps", 0),
240 d_simpITETime("smt::SmtEngine::simpITETime"),
241 d_unconstrainedSimpTime("smt::SmtEngine::unconstrainedSimpTime"),
242 d_theoryPreprocessTime("smt::SmtEngine::theoryPreprocessTime"),
243 d_cnfConversionTime("smt::SmtEngine::cnfConversionTime"),
244 d_numAssertionsPre("smt::SmtEngine::numAssertionsPreITERemoval", 0),
245 d_numAssertionsPost("smt::SmtEngine::numAssertionsPostITERemoval", 0),
246 d_checkModelTime("smt::SmtEngine::checkModelTime"),
247 d_checkProofTime("smt::SmtEngine::checkProofTime"),
248 d_checkUnsatCoreTime("smt::SmtEngine::checkUnsatCoreTime"),
249 d_solveTime("smt::SmtEngine::solveTime"),
250 d_pushPopTime("smt::SmtEngine::pushPopTime"),
251 d_processAssertionsTime("smt::SmtEngine::processAssertionsTime"),
252 d_simplifiedToFalse("smt::SmtEngine::simplifiedToFalse", 0),
253 d_resourceUnitsUsed("smt::SmtEngine::resourceUnitsUsed")
255 smtStatisticsRegistry()->registerStat(&d_definitionExpansionTime
);
256 smtStatisticsRegistry()->registerStat(&d_nonclausalSimplificationTime
);
257 smtStatisticsRegistry()->registerStat(&d_miplibPassTime
);
258 smtStatisticsRegistry()->registerStat(&d_numMiplibAssertionsRemoved
);
259 smtStatisticsRegistry()->registerStat(&d_numConstantProps
);
260 smtStatisticsRegistry()->registerStat(&d_simpITETime
);
261 smtStatisticsRegistry()->registerStat(&d_unconstrainedSimpTime
);
262 smtStatisticsRegistry()->registerStat(&d_theoryPreprocessTime
);
263 smtStatisticsRegistry()->registerStat(&d_cnfConversionTime
);
264 smtStatisticsRegistry()->registerStat(&d_numAssertionsPre
);
265 smtStatisticsRegistry()->registerStat(&d_numAssertionsPost
);
266 smtStatisticsRegistry()->registerStat(&d_checkModelTime
);
267 smtStatisticsRegistry()->registerStat(&d_checkProofTime
);
268 smtStatisticsRegistry()->registerStat(&d_checkUnsatCoreTime
);
269 smtStatisticsRegistry()->registerStat(&d_solveTime
);
270 smtStatisticsRegistry()->registerStat(&d_pushPopTime
);
271 smtStatisticsRegistry()->registerStat(&d_processAssertionsTime
);
272 smtStatisticsRegistry()->registerStat(&d_simplifiedToFalse
);
273 smtStatisticsRegistry()->registerStat(&d_resourceUnitsUsed
);
276 ~SmtEngineStatistics() {
277 smtStatisticsRegistry()->unregisterStat(&d_definitionExpansionTime
);
278 smtStatisticsRegistry()->unregisterStat(&d_nonclausalSimplificationTime
);
279 smtStatisticsRegistry()->unregisterStat(&d_miplibPassTime
);
280 smtStatisticsRegistry()->unregisterStat(&d_numMiplibAssertionsRemoved
);
281 smtStatisticsRegistry()->unregisterStat(&d_numConstantProps
);
282 smtStatisticsRegistry()->unregisterStat(&d_simpITETime
);
283 smtStatisticsRegistry()->unregisterStat(&d_unconstrainedSimpTime
);
284 smtStatisticsRegistry()->unregisterStat(&d_theoryPreprocessTime
);
285 smtStatisticsRegistry()->unregisterStat(&d_cnfConversionTime
);
286 smtStatisticsRegistry()->unregisterStat(&d_numAssertionsPre
);
287 smtStatisticsRegistry()->unregisterStat(&d_numAssertionsPost
);
288 smtStatisticsRegistry()->unregisterStat(&d_checkModelTime
);
289 smtStatisticsRegistry()->unregisterStat(&d_checkProofTime
);
290 smtStatisticsRegistry()->unregisterStat(&d_checkUnsatCoreTime
);
291 smtStatisticsRegistry()->unregisterStat(&d_solveTime
);
292 smtStatisticsRegistry()->unregisterStat(&d_pushPopTime
);
293 smtStatisticsRegistry()->unregisterStat(&d_processAssertionsTime
);
294 smtStatisticsRegistry()->unregisterStat(&d_simplifiedToFalse
);
295 smtStatisticsRegistry()->unregisterStat(&d_resourceUnitsUsed
);
297 };/* struct SmtEngineStatistics */
300 class SoftResourceOutListener
: public Listener
{
302 SoftResourceOutListener(SmtEngine
& smt
) : d_smt(&smt
) {}
303 void notify() override
305 SmtScope
scope(d_smt
);
306 Assert(smt::smtEngineInScope());
311 }; /* class SoftResourceOutListener */
314 class HardResourceOutListener
: public Listener
{
316 HardResourceOutListener(SmtEngine
& smt
) : d_smt(&smt
) {}
317 void notify() override
319 SmtScope
scope(d_smt
);
320 theory::Rewriter::clearCaches();
324 }; /* class HardResourceOutListener */
326 class SetLogicListener
: public Listener
{
328 SetLogicListener(SmtEngine
& smt
) : d_smt(&smt
) {}
329 void notify() override
331 LogicInfo
inOptions(options::forceLogicString());
332 d_smt
->setLogic(inOptions
);
336 }; /* class SetLogicListener */
338 class BeforeSearchListener
: public Listener
{
340 BeforeSearchListener(SmtEngine
& smt
) : d_smt(&smt
) {}
341 void notify() override
{ d_smt
->beforeSearch(); }
345 }; /* class BeforeSearchListener */
347 class UseTheoryListListener
: public Listener
{
349 UseTheoryListListener(TheoryEngine
* theoryEngine
)
350 : d_theoryEngine(theoryEngine
)
353 void notify() override
355 std::stringstream
commaList(options::useTheoryList());
358 Debug("UseTheoryListListener") << "UseTheoryListListener::notify() "
359 << options::useTheoryList() << std::endl
;
361 while(std::getline(commaList
, token
, ',')){
362 if(token
== "help") {
363 puts(theory::useTheoryHelp
);
366 if(theory::useTheoryValidate(token
)) {
367 d_theoryEngine
->enableTheoryAlternative(token
);
369 throw OptionException(
370 std::string("unknown option for --use-theory : `") + token
+
371 "'. Try --use-theory=help.");
377 TheoryEngine
* d_theoryEngine
;
378 }; /* class UseTheoryListListener */
381 class SetDefaultExprDepthListener
: public Listener
{
383 void notify() override
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 void notify() override
400 int dag
= options::defaultDagThresh();
401 Debug
.getStream() << expr::ExprDag(dag
);
402 Trace
.getStream() << expr::ExprDag(dag
);
403 Notice
.getStream() << expr::ExprDag(dag
);
404 Chat
.getStream() << expr::ExprDag(dag
);
405 Message
.getStream() << expr::ExprDag(dag
);
406 Warning
.getStream() << expr::ExprDag(dag
);
407 Dump
.getStream() << expr::ExprDag(dag
);
411 class SetPrintExprTypesListener
: public Listener
{
413 void notify() override
415 bool value
= options::printExprTypes();
416 Debug
.getStream() << expr::ExprPrintTypes(value
);
417 Trace
.getStream() << expr::ExprPrintTypes(value
);
418 Notice
.getStream() << expr::ExprPrintTypes(value
);
419 Chat
.getStream() << expr::ExprPrintTypes(value
);
420 Message
.getStream() << expr::ExprPrintTypes(value
);
421 Warning
.getStream() << expr::ExprPrintTypes(value
);
422 // intentionally exclude Dump stream from this list
426 class DumpModeListener
: public Listener
{
428 void notify() override
430 const std::string
& value
= options::dumpModeString();
431 Dump
.setDumpFromString(value
);
435 class PrintSuccessListener
: public Listener
{
437 void notify() override
439 bool value
= options::printSuccess();
440 Debug
.getStream() << Command::printsuccess(value
);
441 Trace
.getStream() << Command::printsuccess(value
);
442 Notice
.getStream() << Command::printsuccess(value
);
443 Chat
.getStream() << Command::printsuccess(value
);
444 Message
.getStream() << Command::printsuccess(value
);
445 Warning
.getStream() << Command::printsuccess(value
);
446 *options::out() << Command::printsuccess(value
);
453 * This is an inelegant solution, but for the present, it will work.
454 * The point of this is to separate the public and private portions of
455 * the SmtEngine class, so that smt_engine.h doesn't
456 * include "expr/node.h", which is a private CVC4 header (and can lead
457 * to linking errors due to the improper inlining of non-visible symbols
460 * The "real" solution (that which is usually implemented) is to move
461 * ALL the implementation to SmtEnginePrivate and maintain a
462 * heap-allocated instance of it in SmtEngine. SmtEngine (the public
463 * one) becomes an "interface shell" which simply acts as a forwarder
466 class SmtEnginePrivate
: public NodeManagerListener
{
469 typedef unordered_map
<Node
, Node
, NodeHashFunction
> NodeToNodeHashMap
;
470 typedef unordered_map
<Node
, bool, NodeHashFunction
> NodeToBoolHashMap
;
473 * Manager for limiting time and abstract resource usage.
475 ResourceManager
* d_resourceManager
;
477 /** Manager for the memory of regular-output-channel. */
478 ManagedRegularOutputChannel d_managedRegularChannel
;
480 /** Manager for the memory of diagnostic-output-channel. */
481 ManagedDiagnosticOutputChannel d_managedDiagnosticChannel
;
483 /** Manager for the memory of --dump-to. */
484 ManagedDumpOStream d_managedDumpChannel
;
486 /** Manager for --replay-log. */
487 ManagedReplayLogOstream d_managedReplayLog
;
490 * This list contains:
494 * beforeSearchListener
495 * UseTheoryListListener
497 * This needs to be deleted before both NodeManager's Options,
498 * SmtEngine, d_resourceManager, and TheoryEngine.
500 ListenerRegistrationList
* d_listenerRegistrations
;
502 /** Learned literals */
503 vector
<Node
> d_nonClausalLearnedLiterals
;
505 /** A circuit propagator for non-clausal propositional deduction */
506 booleans::CircuitPropagator d_propagator
;
507 bool d_propagatorNeedsFinish
;
508 std::vector
<Node
> d_boolVars
;
510 /** Assertions in the preprocessing pipeline */
511 AssertionPipeline d_assertions
;
513 /** Whether any assertions have been processed */
514 CDO
<bool> d_assertionsProcessed
;
520 * A context that never pushes/pops, for use by CD structures (like
521 * SubstitutionMaps) that should be "global".
523 context::Context d_fakeContext
;
526 * A map of AbsractValues to their actual constants. Only used if
527 * options::abstractValues() is on.
529 SubstitutionMap d_abstractValueMap
;
532 * A mapping of all abstract values (actual value |-> abstract) that
533 * we've handed out. This is necessary to ensure that we give the
534 * same AbstractValues for the same real constants. Only used if
535 * options::abstractValues() is on.
537 NodeToNodeHashMap d_abstractValues
;
539 /** Number of calls of simplify assertions active.
541 unsigned d_simplifyAssertionsDepth
;
543 /** TODO: whether certain preprocess steps are necessary */
544 //bool d_needsExpandDefs;
546 //------------------------------- expression names
547 /** mapping from expressions to name */
548 context::CDHashMap
< Node
, std::string
, NodeHashFunction
> d_exprNames
;
549 //------------------------------- end expression names
551 IteSkolemMap
& getIteSkolemMap() { return d_assertions
.getIteSkolemMap(); }
553 /** Instance of the ITE remover */
554 RemoveTermFormulas d_iteRemover
;
556 /* Finishes the initialization of the private portion of SMTEngine. */
560 std::unique_ptr
<PreprocessingPassContext
> d_preprocessingPassContext
;
561 PreprocessingPassRegistry d_preprocessingPassRegistry
;
563 static const bool d_doConstantProp
= true;
566 * Runs the nonclausal solver and tries to solve all the assigned
569 * Returns false if the formula simplifies to "false"
571 bool nonClausalSimplify();
574 * Performs static learning on the assertions.
576 void staticLearning();
578 Node
realToInt(TNode n
, NodeToNodeHashMap
& cache
, std::vector
< Node
>& var_eq
);
579 Node
purifyNlTerms(TNode n
, NodeToNodeHashMap
& cache
, NodeToNodeHashMap
& bcache
, std::vector
< Node
>& var_eq
, bool beneathMult
= false);
582 * Helper function to fix up assertion list to restore invariants needed after
585 void collectSkolems(TNode n
, set
<TNode
>& skolemSet
, NodeToBoolHashMap
& cache
);
588 * Helper function to fix up assertion list to restore invariants needed after
591 bool checkForBadSkolems(TNode n
, TNode skolem
, NodeToBoolHashMap
& cache
);
593 // Simplify ITE structure
596 // Simplify based on unconstrained values
597 void unconstrainedSimp();
600 * Ensures the assertions asserted after before now effectively come before
601 * d_realAssertionsEnd.
603 void compressBeforeRealAssertions(size_t before
);
606 * Trace nodes back to their assertions using CircuitPropagator's
609 void traceBackToAssertions(const std::vector
<Node
>& nodes
,
610 std::vector
<TNode
>& assertions
);
613 * Remove conjuncts in toRemove from conjunction n. Return # of removed
616 size_t removeFromConjunction(
617 Node
& n
, const std::unordered_set
<unsigned long>& toRemove
);
619 /** Scrub miplib encodings. */
620 void doMiplibTrick();
623 * Perform non-clausal simplification of a Node. This involves
624 * Theory implementations, but does NOT involve the SAT solver in
627 * Returns false if the formula simplifies to "false"
629 bool simplifyAssertions();
632 SmtEnginePrivate(SmtEngine
& smt
)
634 d_managedRegularChannel(),
635 d_managedDiagnosticChannel(),
636 d_managedDumpChannel(),
637 d_managedReplayLog(),
638 d_listenerRegistrations(new ListenerRegistrationList()),
639 d_nonClausalLearnedLiterals(),
640 d_propagator(d_nonClausalLearnedLiterals
, true, true),
641 d_propagatorNeedsFinish(false),
642 d_assertions(d_smt
.d_userContext
),
643 d_assertionsProcessed(smt
.d_userContext
, false),
645 d_abstractValueMap(&d_fakeContext
),
647 d_simplifyAssertionsDepth(0),
648 // d_needsExpandDefs(true), //TODO?
649 d_exprNames(smt
.d_userContext
),
650 d_iteRemover(smt
.d_userContext
)
652 d_smt
.d_nodeManager
->subscribeEvents(this);
653 d_true
= NodeManager::currentNM()->mkConst(true);
654 d_resourceManager
= NodeManager::currentResourceManager();
656 d_listenerRegistrations
->add(d_resourceManager
->registerSoftListener(
657 new SoftResourceOutListener(d_smt
)));
659 d_listenerRegistrations
->add(d_resourceManager
->registerHardListener(
660 new HardResourceOutListener(d_smt
)));
662 Options
& nodeManagerOptions
= NodeManager::currentNM()->getOptions();
663 d_listenerRegistrations
->add(
664 nodeManagerOptions
.registerForceLogicListener(
665 new SetLogicListener(d_smt
), true));
667 // Multiple options reuse BeforeSearchListener so registration requires an
668 // extra bit of care.
669 // We can safely not call notify on this before search listener at
670 // registration time. This d_smt cannot be beforeSearch at construction
671 // time. Therefore the BeforeSearchListener is a no-op. Therefore it does
672 // not have to be called.
673 d_listenerRegistrations
->add(
674 nodeManagerOptions
.registerBeforeSearchListener(
675 new BeforeSearchListener(d_smt
)));
677 // These do need registration calls.
678 d_listenerRegistrations
->add(
679 nodeManagerOptions
.registerSetDefaultExprDepthListener(
680 new SetDefaultExprDepthListener(), true));
681 d_listenerRegistrations
->add(
682 nodeManagerOptions
.registerSetDefaultExprDagListener(
683 new SetDefaultExprDagListener(), true));
684 d_listenerRegistrations
->add(
685 nodeManagerOptions
.registerSetPrintExprTypesListener(
686 new SetPrintExprTypesListener(), true));
687 d_listenerRegistrations
->add(
688 nodeManagerOptions
.registerSetDumpModeListener(
689 new DumpModeListener(), true));
690 d_listenerRegistrations
->add(
691 nodeManagerOptions
.registerSetPrintSuccessListener(
692 new PrintSuccessListener(), true));
693 d_listenerRegistrations
->add(
694 nodeManagerOptions
.registerSetRegularOutputChannelListener(
695 new SetToDefaultSourceListener(&d_managedRegularChannel
), true));
696 d_listenerRegistrations
->add(
697 nodeManagerOptions
.registerSetDiagnosticOutputChannelListener(
698 new SetToDefaultSourceListener(&d_managedDiagnosticChannel
), true));
699 d_listenerRegistrations
->add(
700 nodeManagerOptions
.registerDumpToFileNameListener(
701 new SetToDefaultSourceListener(&d_managedDumpChannel
), true));
702 d_listenerRegistrations
->add(
703 nodeManagerOptions
.registerSetReplayLogFilename(
704 new SetToDefaultSourceListener(&d_managedReplayLog
), true));
709 delete d_listenerRegistrations
;
711 if(d_propagatorNeedsFinish
) {
712 d_propagator
.finish();
713 d_propagatorNeedsFinish
= false;
715 d_smt
.d_nodeManager
->unsubscribeEvents(this);
718 void unregisterPreprocessingPasses()
720 d_preprocessingPassRegistry
.unregisterPasses();
723 ResourceManager
* getResourceManager() { return d_resourceManager
; }
724 void spendResource(unsigned amount
)
726 d_resourceManager
->spendResource(amount
);
729 void nmNotifyNewSort(TypeNode tn
, uint32_t flags
) override
731 DeclareTypeCommand
c(tn
.getAttribute(expr::VarNameAttr()),
734 if((flags
& ExprManager::SORT_FLAG_PLACEHOLDER
) == 0) {
735 d_smt
.addToModelCommandAndDump(c
, flags
);
739 void nmNotifyNewSortConstructor(TypeNode tn
, uint32_t flags
) override
741 DeclareTypeCommand
c(tn
.getAttribute(expr::VarNameAttr()),
742 tn
.getAttribute(expr::SortArityAttr()),
744 if ((flags
& ExprManager::SORT_FLAG_PLACEHOLDER
) == 0)
746 d_smt
.addToModelCommandAndDump(c
);
750 void nmNotifyNewDatatypes(const std::vector
<DatatypeType
>& dtts
) override
752 DatatypeDeclarationCommand
c(dtts
);
753 d_smt
.addToModelCommandAndDump(c
);
756 void nmNotifyNewVar(TNode n
, uint32_t flags
) override
758 DeclareFunctionCommand
c(n
.getAttribute(expr::VarNameAttr()),
760 n
.getType().toType());
761 if((flags
& ExprManager::VAR_FLAG_DEFINED
) == 0) {
762 d_smt
.addToModelCommandAndDump(c
, flags
);
764 if(n
.getType().isBoolean() && !options::incrementalSolving()) {
765 d_boolVars
.push_back(n
);
769 void nmNotifyNewSkolem(TNode n
,
770 const std::string
& comment
,
771 uint32_t flags
) override
773 string id
= n
.getAttribute(expr::VarNameAttr());
774 DeclareFunctionCommand
c(id
, n
.toExpr(), n
.getType().toType());
775 if(Dump
.isOn("skolems") && comment
!= "") {
776 Dump("skolems") << CommentCommand(id
+ " is " + comment
);
778 if((flags
& ExprManager::VAR_FLAG_DEFINED
) == 0) {
779 d_smt
.addToModelCommandAndDump(c
, flags
, false, "skolems");
781 if(n
.getType().isBoolean() && !options::incrementalSolving()) {
782 d_boolVars
.push_back(n
);
786 void nmNotifyDeleteNode(TNode n
) override
{}
788 Node
applySubstitutions(TNode node
)
790 return Rewriter::rewrite(
791 d_assertions
.getTopLevelSubstitutions().apply(node
));
795 * Process the assertions that have been asserted.
797 void processAssertions();
799 /** Process a user push.
806 * Process a user pop. Clears out the non-context-dependent stuff in this
807 * SmtEnginePrivate. Necessary to clear out our assertion vectors in case
808 * someone does a push-assert-pop without a check-sat. It also pops the
809 * last map of expression names from notifyPush.
812 d_assertions
.clear();
813 d_nonClausalLearnedLiterals
.clear();
814 getIteSkolemMap().clear();
818 * Adds a formula to the current context. Action here depends on
819 * the SimplificationMode (in the current Options scope); the
820 * formula might be pushed out to the propositional layer
821 * immediately, or it might be simplified and kept, or it might not
822 * even be simplified.
823 * the 2nd and 3rd arguments added for bookkeeping for proofs
825 void addFormula(TNode n
, bool inUnsatCore
, bool inInput
= true);
827 /** Expand definitions in n. */
828 Node
expandDefinitions(TNode n
,
829 NodeToNodeHashMap
& cache
,
830 bool expandOnly
= false);
833 * Simplify node "in" by expanding definitions and applying any
834 * substitutions learned from preprocessing.
836 Node
simplify(TNode in
) {
837 // Substitute out any abstract values in ex.
838 // Expand definitions.
839 NodeToNodeHashMap cache
;
840 Node n
= expandDefinitions(in
, cache
).toExpr();
841 // Make sure we've done all preprocessing, etc.
842 Assert(d_assertions
.size() == 0);
843 return applySubstitutions(n
).toExpr();
847 * Substitute away all AbstractValues in a node.
849 Node
substituteAbstractValues(TNode n
) {
850 // We need to do this even if options::abstractValues() is off,
851 // since the setting might have changed after we already gave out
852 // some abstract values.
853 return d_abstractValueMap
.apply(n
);
857 * Make a new (or return an existing) abstract value for a node.
858 * Can only use this if options::abstractValues() is on.
860 Node
mkAbstractValue(TNode n
) {
861 Assert(options::abstractValues());
862 Node
& val
= d_abstractValues
[n
];
864 val
= d_smt
.d_nodeManager
->mkAbstractValue(n
.getType());
865 d_abstractValueMap
.addSubstitution(val
, n
);
867 // We are supposed to ascribe types to all abstract values that go out.
868 NodeManager
* current
= d_smt
.d_nodeManager
;
869 Node ascription
= current
->mkConst(AscriptionType(n
.getType().toType()));
870 Node retval
= current
->mkNode(kind::APPLY_TYPE_ASCRIPTION
, ascription
, val
);
874 void addUseTheoryListListener(TheoryEngine
* theoryEngine
){
875 Options
& nodeManagerOptions
= NodeManager::currentNM()->getOptions();
876 d_listenerRegistrations
->add(
877 nodeManagerOptions
.registerUseTheoryListListener(
878 new UseTheoryListListener(theoryEngine
), true));
881 std::ostream
* getReplayLog() const {
882 return d_managedReplayLog
.getReplayLog();
885 //------------------------------- expression names
886 // implements setExpressionName, as described in smt_engine.h
887 void setExpressionName(Expr e
, std::string name
) {
888 d_exprNames
[Node::fromExpr(e
)] = name
;
891 // implements getExpressionName, as described in smt_engine.h
892 bool getExpressionName(Expr e
, std::string
& name
) const {
893 context::CDHashMap
< Node
, std::string
, NodeHashFunction
>::const_iterator it
= d_exprNames
.find(e
);
894 if(it
!=d_exprNames
.end()) {
901 //------------------------------- end expression names
903 };/* class SmtEnginePrivate */
905 }/* namespace CVC4::smt */
907 SmtEngine::SmtEngine(ExprManager
* em
)
908 : d_context(new Context()),
910 d_userContext(new UserContext()),
912 d_nodeManager(d_exprManager
->getNodeManager()),
913 d_decisionEngine(NULL
),
914 d_theoryEngine(NULL
),
916 d_proofManager(NULL
),
917 d_definedFunctions(NULL
),
918 d_fmfRecFunctionsDefined(NULL
),
919 d_assertionList(NULL
),
921 d_modelGlobalCommands(),
922 d_modelCommands(NULL
),
928 d_fullyInited(false),
929 d_problemExtended(false),
931 d_needPostsolve(false),
932 d_earlyTheoryPP(true),
933 d_globalNegation(false),
935 d_replayStream(NULL
),
937 d_statisticsRegistry(NULL
),
939 d_channels(new LemmaChannels())
942 d_originalOptions
.copyValues(em
->getOptions());
943 d_private
= new smt::SmtEnginePrivate(*this);
944 d_statisticsRegistry
= new StatisticsRegistry();
945 d_stats
= new SmtEngineStatistics();
946 d_stats
->d_resourceUnitsUsed
.setData(
947 d_private
->getResourceManager()->getResourceUsage());
949 // The ProofManager is constructed before any other proof objects such as
950 // SatProof and TheoryProofs. The TheoryProofEngine and the SatProof are
951 // initialized in TheoryEngine and PropEngine respectively.
952 Assert(d_proofManager
== NULL
);
954 // d_proofManager must be created before Options has been finished
955 // being parsed from the input file. Because of this, we cannot trust
956 // that options::proof() is set correctly yet.
958 d_proofManager
= new ProofManager(d_userContext
);
961 // We have mutual dependency here, so we add the prop engine to the theory
962 // engine later (it is non-essential there)
963 d_theoryEngine
= new TheoryEngine(d_context
,
965 d_private
->d_iteRemover
,
966 const_cast<const LogicInfo
&>(d_logic
),
970 for(TheoryId id
= theory::THEORY_FIRST
; id
< theory::THEORY_LAST
; ++id
) {
971 TheoryConstructor::addTheory(d_theoryEngine
, id
);
972 //register with proof engine if applicable
974 ProofManager::currentPM()->getTheoryProofEngine()->registerTheory(d_theoryEngine
->theoryOf(id
));
978 d_private
->addUseTheoryListListener(d_theoryEngine
);
980 // global push/pop around everything, to ensure proper destruction
981 // of context-dependent data structures
982 d_userContext
->push();
985 d_definedFunctions
= new(true) DefinedFunctionMap(d_userContext
);
986 d_fmfRecFunctionsDefined
= new(true) NodeList(d_userContext
);
987 d_modelCommands
= new(true) smt::CommandList(d_userContext
);
990 void SmtEngine::finishInit() {
991 Trace("smt-debug") << "SmtEngine::finishInit" << std::endl
;
992 // ensure that our heuristics are properly set up
995 Trace("smt-debug") << "Making decision engine..." << std::endl
;
997 d_decisionEngine
= new DecisionEngine(d_context
, d_userContext
);
998 d_decisionEngine
->init(); // enable appropriate strategies
1000 Trace("smt-debug") << "Making prop engine..." << std::endl
;
1001 d_propEngine
= new PropEngine(d_theoryEngine
, d_decisionEngine
, d_context
,
1002 d_userContext
, d_private
->getReplayLog(),
1003 d_replayStream
, d_channels
);
1005 Trace("smt-debug") << "Setting up theory engine..." << std::endl
;
1006 d_theoryEngine
->setPropEngine(d_propEngine
);
1007 d_theoryEngine
->setDecisionEngine(d_decisionEngine
);
1008 Trace("smt-debug") << "Finishing init for theory engine..." << std::endl
;
1009 d_theoryEngine
->finishInit();
1011 Trace("smt-debug") << "Set up assertion list..." << std::endl
;
1012 // [MGD 10/20/2011] keep around in incremental mode, due to a
1013 // cleanup ordering issue and Nodes/TNodes. If SAT is popped
1014 // first, some user-context-dependent TNodes might still exist
1016 if(options::produceAssertions() ||
1017 options::incrementalSolving()) {
1018 // In the case of incremental solving, we appear to need these to
1019 // ensure the relevant Nodes remain live.
1020 d_assertionList
= new(true) AssertionList(d_userContext
);
1023 // dump out a set-logic command
1024 if(Dump
.isOn("benchmark")) {
1025 if (Dump
.isOn("raw-benchmark")) {
1026 Dump("raw-benchmark") << SetBenchmarkLogicCommand(d_logic
.getLogicString());
1028 LogicInfo everything
;
1030 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.")
1031 << SetBenchmarkLogicCommand(everything
.getLogicString());
1035 Trace("smt-debug") << "Dump declaration commands..." << std::endl
;
1036 // dump out any pending declaration commands
1037 for(unsigned i
= 0; i
< d_dumpCommands
.size(); ++i
) {
1038 Dump("declarations") << *d_dumpCommands
[i
];
1039 delete d_dumpCommands
[i
];
1041 d_dumpCommands
.clear();
1043 PROOF( ProofManager::currentPM()->setLogic(d_logic
); );
1045 for(TheoryId id
= theory::THEORY_FIRST
; id
< theory::THEORY_LAST
; ++id
) {
1046 ProofManager::currentPM()->getTheoryProofEngine()->
1047 finishRegisterTheory(d_theoryEngine
->theoryOf(id
));
1050 d_private
->finishInit();
1051 Trace("smt-debug") << "SmtEngine::finishInit done" << std::endl
;
1054 void SmtEngine::finalOptionsAreSet() {
1059 if(! d_logic
.isLocked()) {
1063 // finish initialization, create the prop engine, etc.
1066 AlwaysAssert( d_propEngine
->getAssertionLevel() == 0,
1067 "The PropEngine has pushed but the SmtEngine "
1068 "hasn't finished initializing!" );
1070 d_fullyInited
= true;
1071 Assert(d_logic
.isLocked());
1073 d_propEngine
->assertFormula(NodeManager::currentNM()->mkConst
<bool>(true));
1074 d_propEngine
->assertFormula(NodeManager::currentNM()->mkConst
<bool>(false).notNode());
1077 void SmtEngine::shutdown() {
1080 while(options::incrementalSolving() && d_userContext
->getLevel() > 1) {
1084 // check to see if a postsolve() is pending
1085 if(d_needPostsolve
) {
1086 d_theoryEngine
->postsolve();
1087 d_needPostsolve
= false;
1090 if(d_propEngine
!= NULL
) {
1091 d_propEngine
->shutdown();
1093 if(d_theoryEngine
!= NULL
) {
1094 d_theoryEngine
->shutdown();
1096 if(d_decisionEngine
!= NULL
) {
1097 d_decisionEngine
->shutdown();
1101 SmtEngine::~SmtEngine()
1103 SmtScope
smts(this);
1108 // global push/pop around everything, to ensure proper destruction
1109 // of context-dependent data structures
1110 d_context
->popto(0);
1111 d_userContext
->popto(0);
1113 if(d_assignments
!= NULL
) {
1114 d_assignments
->deleteSelf();
1117 if(d_assertionList
!= NULL
) {
1118 d_assertionList
->deleteSelf();
1121 for(unsigned i
= 0; i
< d_dumpCommands
.size(); ++i
) {
1122 delete d_dumpCommands
[i
];
1123 d_dumpCommands
[i
] = NULL
;
1125 d_dumpCommands
.clear();
1127 DeleteAndClearCommandVector(d_modelGlobalCommands
);
1129 if(d_modelCommands
!= NULL
) {
1130 d_modelCommands
->deleteSelf();
1133 d_definedFunctions
->deleteSelf();
1134 d_fmfRecFunctionsDefined
->deleteSelf();
1136 //destroy all passes before destroying things that they refer to
1137 d_private
->unregisterPreprocessingPasses();
1139 delete d_theoryEngine
;
1140 d_theoryEngine
= NULL
;
1141 delete d_propEngine
;
1142 d_propEngine
= NULL
;
1143 delete d_decisionEngine
;
1144 d_decisionEngine
= NULL
;
1147 // d_proofManager is always created when proofs are enabled at configure time.
1148 // Becuase of this, this code should not be wrapped in PROOF() which
1149 // additionally checks flags such as options::proof().
1151 delete d_proofManager
;
1152 d_proofManager
= NULL
;
1157 delete d_statisticsRegistry
;
1158 d_statisticsRegistry
= NULL
;
1163 delete d_userContext
;
1164 d_userContext
= NULL
;
1171 } catch(Exception
& e
) {
1172 Warning() << "CVC4 threw an exception during cleanup." << endl
1177 void SmtEngine::setLogic(const LogicInfo
& logic
)
1179 SmtScope
smts(this);
1181 throw ModalException("Cannot set logic in SmtEngine after the engine has "
1182 "finished initializing.");
1188 void SmtEngine::setLogic(const std::string
& s
)
1190 SmtScope
smts(this);
1192 setLogic(LogicInfo(s
));
1193 } catch(IllegalArgumentException
& e
) {
1194 throw LogicException(e
.what());
1198 void SmtEngine::setLogic(const char* logic
) { setLogic(string(logic
)); }
1199 LogicInfo
SmtEngine::getLogicInfo() const {
1202 void SmtEngine::setLogicInternal()
1204 Assert(!d_fullyInited
, "setting logic in SmtEngine but the engine has already"
1205 " finished initializing for this run");
1209 void SmtEngine::setDefaults() {
1210 Random::getRandom().setSeed(options::seed());
1211 // Language-based defaults
1212 if (!options::bitvectorDivByZeroConst
.wasSetByUser())
1214 // Bitvector-divide-by-zero changed semantics in SMT LIB 2.6, thus we
1215 // set this option if the input format is SMT LIB 2.6. We also set this
1216 // option if we are sygus, since we assume SMT LIB 2.6 semantics for sygus.
1217 options::bitvectorDivByZeroConst
.set(
1218 language::isInputLang_smt2_6(options::inputLanguage())
1219 || options::inputLanguage() == language::input::LANG_SYGUS
);
1221 bool is_sygus
= false;
1222 if (options::inputLanguage() == language::input::LANG_SYGUS
)
1225 if (!options::ceGuidedInst
.wasSetByUser())
1227 options::ceGuidedInst
.set(true);
1229 // must use Ferrante/Rackoff for real arithmetic
1230 if (!options::cbqiMidpoint
.wasSetByUser())
1232 options::cbqiMidpoint
.set(true);
1234 if (options::sygusRepairConst())
1236 if (!options::cbqi
.wasSetByUser())
1238 options::cbqi
.set(true);
1243 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
)
1245 if (options::produceModels()
1246 && (d_logic
.isTheoryEnabled(THEORY_ARRAYS
)
1247 || d_logic
.isTheoryEnabled(THEORY_UF
)))
1249 if (options::bitblastMode
.wasSetByUser()
1250 || options::produceModels
.wasSetByUser())
1252 throw OptionException(std::string(
1253 "Eager bit-blasting currently does not support model generation "
1254 "for the combination of bit-vectors with arrays or uinterpreted "
1255 "functions. Try --bitblast=lazy"));
1257 Notice() << "SmtEngine: setting bit-blast mode to lazy to support model"
1258 << "generation" << endl
;
1259 setOption("bitblastMode", SExpr("lazy"));
1262 if (options::incrementalSolving() && !d_logic
.isPure(THEORY_BV
))
1264 throw OptionException(
1265 "Incremental eager bit-blasting is currently "
1266 "only supported for QF_BV. Try --bitblast=lazy.");
1270 if(options::forceLogicString
.wasSetByUser()) {
1271 d_logic
= LogicInfo(options::forceLogicString());
1272 }else if (options::solveIntAsBV() > 0) {
1273 d_logic
= LogicInfo("QF_BV");
1274 }else if (d_logic
.getLogicString() == "QF_NRA" && options::solveRealAsInt()) {
1275 d_logic
= LogicInfo("QF_NIA");
1276 } else if ((d_logic
.getLogicString() == "QF_UFBV" ||
1277 d_logic
.getLogicString() == "QF_ABV") &&
1278 options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
) {
1279 d_logic
= LogicInfo("QF_BV");
1283 /* - disabled for 1.4 release [MGD 2014.06.25]
1284 if(!d_logic.hasEverything() && d_logic.isTheoryEnabled(THEORY_STRINGS) ) {
1285 if(! options::stringExp.wasSetByUser()) {
1286 options::stringExp.set( true );
1287 Trace("smt") << "turning on strings-exp, for the theory of strings" << std::endl;
1292 if(options::stringExp()) {
1293 if( !d_logic
.isQuantified() ) {
1294 d_logic
= d_logic
.getUnlockedCopy();
1295 d_logic
.enableQuantifiers();
1297 Trace("smt") << "turning on quantifier logic, for strings-exp"
1300 if(! options::fmfBound
.wasSetByUser()) {
1301 options::fmfBound
.set( true );
1302 Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl
;
1304 if(! options::fmfInstEngine
.wasSetByUser()) {
1305 options::fmfInstEngine
.set( true );
1306 Trace("smt") << "turning on fmf-inst-engine, for strings-exp" << std::endl
;
1309 if(! options::rewriteDivk.wasSetByUser()) {
1310 options::rewriteDivk.set( true );
1311 Trace("smt") << "turning on rewrite-divk, for strings-exp" << std::endl;
1314 if(! options::stringFMF.wasSetByUser()) {
1315 options::stringFMF.set( true );
1316 Trace("smt") << "turning on strings-fmf, for strings-exp" << std::endl;
1321 // sygus inference may require datatypes
1322 if (options::sygusInference())
1324 d_logic
= d_logic
.getUnlockedCopy();
1325 d_logic
.enableTheory(THEORY_DATATYPES
);
1327 // since we are trying to recast as sygus, we assume the input is sygus
1331 if ((options::checkModels() || options::checkSynthSol())
1332 && !options::produceAssertions())
1334 Notice() << "SmtEngine: turning on produce-assertions to support "
1335 << "check-models or check-synth-sol." << endl
;
1336 setOption("produce-assertions", SExpr("true"));
1339 // Disable options incompatible with incremental solving, unsat cores, and
1340 // proofs or output an error if enabled explicitly
1341 if (options::incrementalSolving() || options::unsatCores()
1342 || options::proof())
1344 if (options::unconstrainedSimp())
1346 if (options::unconstrainedSimp
.wasSetByUser())
1348 throw OptionException(
1349 "unconstrained simplification not supported with unsat "
1350 "cores/proofs/incremental solving");
1352 Notice() << "SmtEngine: turning off unconstrained simplification to "
1353 "support unsat cores/proofs/incremental solving"
1355 options::unconstrainedSimp
.set(false);
1360 // Turn on unconstrained simplification for QF_AUFBV
1361 if (!options::unconstrainedSimp
.wasSetByUser())
1363 // bool qf_sat = d_logic.isPure(THEORY_BOOL) &&
1364 // !d_logic.isQuantified(); bool uncSimp = false && !qf_sat &&
1365 // !options::incrementalSolving();
1366 bool uncSimp
= !d_logic
.isQuantified() && !options::produceModels()
1367 && !options::produceAssignments()
1368 && !options::checkModels()
1369 && (d_logic
.isTheoryEnabled(THEORY_ARRAYS
)
1370 && d_logic
.isTheoryEnabled(THEORY_BV
));
1371 Trace("smt") << "setting unconstrained simplification to " << uncSimp
1373 options::unconstrainedSimp
.set(uncSimp
);
1377 // Disable options incompatible with unsat cores and proofs or output an
1378 // error if enabled explicitly
1379 if (options::unsatCores() || options::proof())
1381 if (options::simplificationMode() != SIMPLIFICATION_MODE_NONE
)
1383 if (options::simplificationMode
.wasSetByUser())
1385 throw OptionException(
1386 "simplification not supported with unsat cores/proofs");
1388 Notice() << "SmtEngine: turning off simplification to support unsat "
1391 options::simplificationMode
.set(SIMPLIFICATION_MODE_NONE
);
1394 if (options::pbRewrites())
1396 if (options::pbRewrites
.wasSetByUser())
1398 throw OptionException(
1399 "pseudoboolean rewrites not supported with unsat cores/proofs");
1401 Notice() << "SmtEngine: turning off pseudoboolean rewrites to support "
1402 "unsat cores/proofs"
1404 setOption("pb-rewrites", false);
1407 if (options::sortInference())
1409 if (options::sortInference
.wasSetByUser())
1411 throw OptionException(
1412 "sort inference not supported with unsat cores/proofs");
1414 Notice() << "SmtEngine: turning off sort inference to support unsat "
1417 options::sortInference
.set(false);
1420 if (options::preSkolemQuant())
1422 if (options::preSkolemQuant
.wasSetByUser())
1424 throw OptionException(
1425 "pre-skolemization not supported with unsat cores/proofs");
1427 Notice() << "SmtEngine: turning off pre-skolemization to support unsat "
1430 options::preSkolemQuant
.set(false);
1433 if (options::bitvectorToBool())
1435 if (options::bitvectorToBool
.wasSetByUser())
1437 throw OptionException(
1438 "bv-to-bool not supported with unsat cores/proofs");
1440 Notice() << "SmtEngine: turning off bitvector-to-bool to support unsat "
1443 options::bitvectorToBool
.set(false);
1446 if (options::boolToBitvector())
1448 if (options::boolToBitvector
.wasSetByUser())
1450 throw OptionException(
1451 "bool-to-bv not supported with unsat cores/proofs");
1453 Notice() << "SmtEngine: turning off bool-to-bitvector to support unsat "
1456 options::boolToBitvector
.set(false);
1459 if (options::bvIntroducePow2())
1461 if (options::bvIntroducePow2
.wasSetByUser())
1463 throw OptionException(
1464 "bv-intro-pow2 not supported with unsat cores/proofs");
1466 Notice() << "SmtEngine: turning off bv-intro-pow2 to support "
1467 "unsat-cores/proofs"
1469 setOption("bv-intro-pow2", false);
1472 if (options::repeatSimp())
1474 if (options::repeatSimp
.wasSetByUser())
1476 throw OptionException(
1477 "repeat-simp not supported with unsat cores/proofs");
1479 Notice() << "SmtEngine: turning off repeat-simp to support unsat "
1482 setOption("repeat-simp", false);
1485 if (options::globalNegate())
1487 if (options::globalNegate
.wasSetByUser())
1489 throw OptionException(
1490 "global-negate not supported with unsat cores/proofs");
1492 Notice() << "SmtEngine: turning off global-negate to support unsat "
1495 setOption("global-negate", false);
1500 // by default, nonclausal simplification is off for QF_SAT
1501 if (!options::simplificationMode
.wasSetByUser())
1503 bool qf_sat
= d_logic
.isPure(THEORY_BOOL
) && !d_logic
.isQuantified();
1504 Trace("smt") << "setting simplification mode to <"
1505 << d_logic
.getLogicString() << "> " << (!qf_sat
) << endl
;
1506 // simplification=none works better for SMT LIB benchmarks with
1507 // quantifiers, not others options::simplificationMode.set(qf_sat ||
1508 // quantifiers ? SIMPLIFICATION_MODE_NONE : SIMPLIFICATION_MODE_BATCH);
1509 options::simplificationMode
.set(qf_sat
? SIMPLIFICATION_MODE_NONE
1510 : SIMPLIFICATION_MODE_BATCH
);
1514 if (options::cbqiBv() && d_logic
.isQuantified())
1516 if(options::boolToBitvector
.wasSetByUser()) {
1517 throw OptionException(
1518 "bool-to-bv not supported with CBQI BV for quantified logics");
1520 Notice() << "SmtEngine: turning off bool-to-bitvector to support CBQI BV"
1522 options::boolToBitvector
.set(false);
1525 // cases where we need produce models
1526 if (!options::produceModels()
1527 && (options::produceAssignments() || options::sygusRewSynthCheck()
1530 Notice() << "SmtEngine: turning on produce-models" << endl
;
1531 setOption("produce-models", SExpr("true"));
1534 // Set the options for the theoryOf
1535 if(!options::theoryOfMode
.wasSetByUser()) {
1536 if(d_logic
.isSharingEnabled() &&
1537 !d_logic
.isTheoryEnabled(THEORY_BV
) &&
1538 !d_logic
.isTheoryEnabled(THEORY_STRINGS
) &&
1539 !d_logic
.isTheoryEnabled(THEORY_SETS
) ) {
1540 Trace("smt") << "setting theoryof-mode to term-based" << endl
;
1541 options::theoryOfMode
.set(THEORY_OF_TERM_BASED
);
1545 // strings require LIA, UF; widen the logic
1546 if(d_logic
.isTheoryEnabled(THEORY_STRINGS
)) {
1547 LogicInfo
log(d_logic
.getUnlockedCopy());
1548 // Strings requires arith for length constraints, and also UF
1549 if(!d_logic
.isTheoryEnabled(THEORY_UF
)) {
1550 Trace("smt") << "because strings are enabled, also enabling UF" << endl
;
1551 log
.enableTheory(THEORY_UF
);
1553 if(!d_logic
.isTheoryEnabled(THEORY_ARITH
) || d_logic
.isDifferenceLogic() || !d_logic
.areIntegersUsed()) {
1554 Trace("smt") << "because strings are enabled, also enabling linear integer arithmetic" << endl
;
1555 log
.enableTheory(THEORY_ARITH
);
1556 log
.enableIntegers();
1557 log
.arithOnlyLinear();
1562 if(d_logic
.isTheoryEnabled(THEORY_ARRAYS
) || d_logic
.isTheoryEnabled(THEORY_DATATYPES
) || d_logic
.isTheoryEnabled(THEORY_SETS
)) {
1563 if(!d_logic
.isTheoryEnabled(THEORY_UF
)) {
1564 LogicInfo
log(d_logic
.getUnlockedCopy());
1565 Trace("smt") << "because a theory that permits Boolean terms is enabled, also enabling UF" << endl
;
1566 log
.enableTheory(THEORY_UF
);
1572 // by default, symmetry breaker is on only for non-incremental QF_UF
1573 if(! options::ufSymmetryBreaker
.wasSetByUser()) {
1574 bool qf_uf_noinc
= d_logic
.isPure(THEORY_UF
) && !d_logic
.isQuantified()
1575 && !options::incrementalSolving() && !options::proof()
1576 && !options::unsatCores();
1577 Trace("smt") << "setting uf symmetry breaker to " << qf_uf_noinc
<< endl
;
1578 options::ufSymmetryBreaker
.set(qf_uf_noinc
);
1581 // If in arrays, set the UF handler to arrays
1582 if(d_logic
.isTheoryEnabled(THEORY_ARRAYS
) && ( !d_logic
.isQuantified() ||
1583 (d_logic
.isQuantified() && !d_logic
.isTheoryEnabled(THEORY_UF
)))) {
1584 Theory::setUninterpretedSortOwner(THEORY_ARRAYS
);
1586 Theory::setUninterpretedSortOwner(THEORY_UF
);
1589 // Turn on ite simplification for QF_LIA and QF_AUFBV
1590 // WARNING: These checks match much more than just QF_AUFBV and
1591 // QF_LIA logics. --K [2014/10/15]
1592 if(! options::doITESimp
.wasSetByUser()) {
1593 bool qf_aufbv
= !d_logic
.isQuantified() &&
1594 d_logic
.isTheoryEnabled(THEORY_ARRAYS
) &&
1595 d_logic
.isTheoryEnabled(THEORY_UF
) &&
1596 d_logic
.isTheoryEnabled(THEORY_BV
);
1597 bool qf_lia
= !d_logic
.isQuantified() &&
1598 d_logic
.isPure(THEORY_ARITH
) &&
1599 d_logic
.isLinear() &&
1600 !d_logic
.isDifferenceLogic() &&
1601 !d_logic
.areRealsUsed();
1603 bool iteSimp
= (qf_aufbv
|| qf_lia
);
1604 Trace("smt") << "setting ite simplification to " << iteSimp
<< endl
;
1605 options::doITESimp
.set(iteSimp
);
1607 if(! options::compressItes
.wasSetByUser() ){
1608 bool qf_lia
= !d_logic
.isQuantified() &&
1609 d_logic
.isPure(THEORY_ARITH
) &&
1610 d_logic
.isLinear() &&
1611 !d_logic
.isDifferenceLogic() &&
1612 !d_logic
.areRealsUsed();
1614 bool compressIte
= qf_lia
;
1615 Trace("smt") << "setting ite compression to " << compressIte
<< endl
;
1616 options::compressItes
.set(compressIte
);
1618 if(! options::simplifyWithCareEnabled
.wasSetByUser() ){
1619 bool qf_aufbv
= !d_logic
.isQuantified() &&
1620 d_logic
.isTheoryEnabled(THEORY_ARRAYS
) &&
1621 d_logic
.isTheoryEnabled(THEORY_UF
) &&
1622 d_logic
.isTheoryEnabled(THEORY_BV
);
1624 bool withCare
= qf_aufbv
;
1625 Trace("smt") << "setting ite simplify with care to " << withCare
<< endl
;
1626 options::simplifyWithCareEnabled
.set(withCare
);
1628 // Turn off array eager index splitting for QF_AUFLIA
1629 if(! options::arraysEagerIndexSplitting
.wasSetByUser()) {
1630 if (not d_logic
.isQuantified() &&
1631 d_logic
.isTheoryEnabled(THEORY_ARRAYS
) &&
1632 d_logic
.isTheoryEnabled(THEORY_UF
) &&
1633 d_logic
.isTheoryEnabled(THEORY_ARITH
)) {
1634 Trace("smt") << "setting array eager index splitting to false" << endl
;
1635 options::arraysEagerIndexSplitting
.set(false);
1638 // Turn on model-based arrays for QF_AX (unless models are enabled)
1639 // if(! options::arraysModelBased.wasSetByUser()) {
1640 // if (not d_logic.isQuantified() &&
1641 // d_logic.isTheoryEnabled(THEORY_ARRAYS) &&
1642 // d_logic.isPure(THEORY_ARRAYS) &&
1643 // !options::produceModels() &&
1644 // !options::checkModels()) {
1645 // Trace("smt") << "turning on model-based array solver" << endl;
1646 // options::arraysModelBased.set(true);
1649 // Turn on multiple-pass non-clausal simplification for QF_AUFBV
1650 if(! options::repeatSimp
.wasSetByUser()) {
1651 bool repeatSimp
= !d_logic
.isQuantified() &&
1652 (d_logic
.isTheoryEnabled(THEORY_ARRAYS
) &&
1653 d_logic
.isTheoryEnabled(THEORY_UF
) &&
1654 d_logic
.isTheoryEnabled(THEORY_BV
)) &&
1655 !options::unsatCores();
1656 Trace("smt") << "setting repeat simplification to " << repeatSimp
<< endl
;
1657 options::repeatSimp
.set(repeatSimp
);
1659 // Unconstrained simp currently does *not* support model generation
1660 if (options::unconstrainedSimp
.wasSetByUser() && options::unconstrainedSimp()) {
1661 if (options::produceModels()) {
1662 if (options::produceModels
.wasSetByUser()) {
1663 throw OptionException("Cannot use unconstrained-simp with model generation.");
1665 Notice() << "SmtEngine: turning off produce-models to support unconstrainedSimp" << endl
;
1666 setOption("produce-models", SExpr("false"));
1668 if (options::produceAssignments()) {
1669 if (options::produceAssignments
.wasSetByUser()) {
1670 throw OptionException("Cannot use unconstrained-simp with model generation (produce-assignments).");
1672 Notice() << "SmtEngine: turning off produce-assignments to support unconstrainedSimp" << endl
;
1673 setOption("produce-assignments", SExpr("false"));
1675 if (options::checkModels()) {
1676 if (options::checkModels
.wasSetByUser()) {
1677 throw OptionException("Cannot use unconstrained-simp with model generation (check-models).");
1679 Notice() << "SmtEngine: turning off check-models to support unconstrainedSimp" << endl
;
1680 setOption("check-models", SExpr("false"));
1684 if (! options::bvEagerExplanations
.wasSetByUser() &&
1685 d_logic
.isTheoryEnabled(THEORY_ARRAYS
) &&
1686 d_logic
.isTheoryEnabled(THEORY_BV
)) {
1687 Trace("smt") << "enabling eager bit-vector explanations " << endl
;
1688 options::bvEagerExplanations
.set(true);
1691 // Turn on arith rewrite equalities only for pure arithmetic
1692 if(! options::arithRewriteEq
.wasSetByUser()) {
1693 bool arithRewriteEq
= d_logic
.isPure(THEORY_ARITH
) && d_logic
.isLinear() && !d_logic
.isQuantified();
1694 Trace("smt") << "setting arith rewrite equalities " << arithRewriteEq
<< endl
;
1695 options::arithRewriteEq
.set(arithRewriteEq
);
1697 if(! options::arithHeuristicPivots
.wasSetByUser()) {
1698 int16_t heuristicPivots
= 5;
1699 if(d_logic
.isPure(THEORY_ARITH
) && !d_logic
.isQuantified()) {
1700 if(d_logic
.isDifferenceLogic()) {
1701 heuristicPivots
= -1;
1702 } else if(!d_logic
.areIntegersUsed()) {
1703 heuristicPivots
= 0;
1706 Trace("smt") << "setting arithHeuristicPivots " << heuristicPivots
<< endl
;
1707 options::arithHeuristicPivots
.set(heuristicPivots
);
1709 if(! options::arithPivotThreshold
.wasSetByUser()){
1710 uint16_t pivotThreshold
= 2;
1711 if(d_logic
.isPure(THEORY_ARITH
) && !d_logic
.isQuantified()){
1712 if(d_logic
.isDifferenceLogic()){
1713 pivotThreshold
= 16;
1716 Trace("smt") << "setting arith arithPivotThreshold " << pivotThreshold
<< endl
;
1717 options::arithPivotThreshold
.set(pivotThreshold
);
1719 if(! options::arithStandardCheckVarOrderPivots
.wasSetByUser()){
1720 int16_t varOrderPivots
= -1;
1721 if(d_logic
.isPure(THEORY_ARITH
) && !d_logic
.isQuantified()){
1722 varOrderPivots
= 200;
1724 Trace("smt") << "setting arithStandardCheckVarOrderPivots " << varOrderPivots
<< endl
;
1725 options::arithStandardCheckVarOrderPivots
.set(varOrderPivots
);
1727 // Turn off early theory preprocessing if arithRewriteEq is on
1728 if (options::arithRewriteEq()) {
1729 d_earlyTheoryPP
= false;
1731 if (d_logic
.isPure(THEORY_ARITH
) && !d_logic
.areRealsUsed())
1733 if (!options::nlExtTangentPlanesInterleave
.wasSetByUser())
1735 Trace("smt") << "setting nlExtTangentPlanesInterleave to true" << endl
;
1736 options::nlExtTangentPlanesInterleave
.set(true);
1740 // Set decision mode based on logic (if not set by user)
1741 if(!options::decisionMode
.wasSetByUser()) {
1742 decision::DecisionMode decMode
=
1744 d_logic
.hasEverything() ? decision::DECISION_STRATEGY_JUSTIFICATION
:
1746 (not d_logic
.isQuantified() &&
1747 d_logic
.isPure(THEORY_BV
)
1749 // QF_AUFBV or QF_ABV or QF_UFBV
1750 (not d_logic
.isQuantified() &&
1751 (d_logic
.isTheoryEnabled(THEORY_ARRAYS
) ||
1752 d_logic
.isTheoryEnabled(THEORY_UF
)) &&
1753 d_logic
.isTheoryEnabled(THEORY_BV
)
1755 // QF_AUFLIA (and may be ends up enabling QF_AUFLRA?)
1756 (not d_logic
.isQuantified() &&
1757 d_logic
.isTheoryEnabled(THEORY_ARRAYS
) &&
1758 d_logic
.isTheoryEnabled(THEORY_UF
) &&
1759 d_logic
.isTheoryEnabled(THEORY_ARITH
)
1762 (not d_logic
.isQuantified() &&
1763 d_logic
.isPure(THEORY_ARITH
) && d_logic
.isLinear() && !d_logic
.isDifferenceLogic() && !d_logic
.areIntegersUsed()
1766 d_logic
.isQuantified() ||
1768 d_logic
.isTheoryEnabled(THEORY_STRINGS
)
1769 ? decision::DECISION_STRATEGY_JUSTIFICATION
1770 : decision::DECISION_STRATEGY_INTERNAL
1775 d_logic
.hasEverything() || d_logic
.isTheoryEnabled(THEORY_STRINGS
) ? false :
1777 (not d_logic
.isQuantified() &&
1778 d_logic
.isTheoryEnabled(THEORY_ARRAYS
) &&
1779 d_logic
.isTheoryEnabled(THEORY_UF
) &&
1780 d_logic
.isTheoryEnabled(THEORY_ARITH
)
1783 (not d_logic
.isQuantified() &&
1784 d_logic
.isPure(THEORY_ARITH
) && d_logic
.isLinear() && !d_logic
.isDifferenceLogic() && !d_logic
.areIntegersUsed()
1789 Trace("smt") << "setting decision mode to " << decMode
<< endl
;
1790 options::decisionMode
.set(decMode
);
1791 options::decisionStopOnly
.set(stoponly
);
1793 if( options::incrementalSolving() ){
1794 //disable modes not supported by incremental
1795 options::sortInference
.set( false );
1796 options::ufssFairnessMonotone
.set( false );
1797 options::quantEpr
.set( false );
1798 options::globalNegate
.set(false);
1800 if( d_logic
.hasCardinalityConstraints() ){
1801 //must have finite model finding on
1802 options::finiteModelFind
.set( true );
1805 //if it contains a theory with non-termination, do not strictly enforce that quantifiers and theory combination must be interleaved
1806 if( d_logic
.isTheoryEnabled(THEORY_STRINGS
) || (d_logic
.isTheoryEnabled(THEORY_ARITH
) && !d_logic
.isLinear()) ){
1807 if( !options::instWhenStrictInterleave
.wasSetByUser() ){
1808 options::instWhenStrictInterleave
.set( false );
1812 //local theory extensions
1813 if( options::localTheoryExt() ){
1814 if( !options::instMaxLevel
.wasSetByUser() ){
1815 options::instMaxLevel
.set( 0 );
1818 if( options::instMaxLevel()!=-1 ){
1819 Notice() << "SmtEngine: turning off cbqi to support instMaxLevel" << endl
;
1820 options::cbqi
.set(false);
1822 //track instantiations?
1823 if( options::cbqiNestedQE() || ( options::proof() && !options::trackInstLemmas
.wasSetByUser() ) ){
1824 options::trackInstLemmas
.set( true );
1827 if( ( options::fmfBoundLazy
.wasSetByUser() && options::fmfBoundLazy() ) ||
1828 ( options::fmfBoundInt
.wasSetByUser() && options::fmfBoundInt() ) ) {
1829 options::fmfBound
.set( true );
1831 //now have determined whether fmfBoundInt is on/off
1832 //apply fmfBoundInt options
1833 if( options::fmfBound() ){
1834 //must have finite model finding on
1835 options::finiteModelFind
.set( true );
1836 if (!options::mbqiMode
.wasSetByUser()
1837 || (options::mbqiMode() != quantifiers::MBQI_NONE
1838 && options::mbqiMode() != quantifiers::MBQI_FMC
))
1840 //if bounded integers are set, use no MBQI by default
1841 options::mbqiMode
.set( quantifiers::MBQI_NONE
);
1843 if( ! options::prenexQuant
.wasSetByUser() ){
1844 options::prenexQuant
.set( quantifiers::PRENEX_QUANT_NONE
);
1847 if( options::ufHo() ){
1848 //if higher-order, then current variants of model-based instantiation cannot be used
1849 if( options::mbqiMode()!=quantifiers::MBQI_NONE
){
1850 options::mbqiMode
.set( quantifiers::MBQI_NONE
);
1853 if( options::mbqiMode()==quantifiers::MBQI_ABS
){
1854 if( !d_logic
.isPure(THEORY_UF
) ){
1855 //MBQI_ABS is only supported in pure quantified UF
1856 options::mbqiMode
.set( quantifiers::MBQI_FMC
);
1859 if( options::fmfFunWellDefinedRelevant() ){
1860 if( !options::fmfFunWellDefined
.wasSetByUser() ){
1861 options::fmfFunWellDefined
.set( true );
1864 if( options::fmfFunWellDefined() ){
1865 if( !options::finiteModelFind
.wasSetByUser() ){
1866 options::finiteModelFind
.set( true );
1870 if( options::quantEpr() ){
1871 if( !options::preSkolemQuant
.wasSetByUser() ){
1872 options::preSkolemQuant
.set( true );
1876 //now, have determined whether finite model find is on/off
1877 //apply finite model finding options
1878 if( options::finiteModelFind() ){
1879 //apply conservative quantifiers splitting
1880 if( !options::quantDynamicSplit
.wasSetByUser() ){
1881 options::quantDynamicSplit
.set( quantifiers::QUANT_DSPLIT_MODE_DEFAULT
);
1883 //do not eliminate extended arithmetic symbols from quantified formulas
1884 if( !options::elimExtArithQuant
.wasSetByUser() ){
1885 options::elimExtArithQuant
.set( false );
1887 if( !options::eMatching
.wasSetByUser() ){
1888 options::eMatching
.set( options::fmfInstEngine() );
1890 if( !options::instWhenMode
.wasSetByUser() ){
1891 //instantiate only on last call
1892 if( options::eMatching() ){
1893 options::instWhenMode
.set( quantifiers::INST_WHEN_LAST_CALL
);
1896 if( options::mbqiMode()==quantifiers::MBQI_ABS
){
1897 if( !options::preSkolemQuant
.wasSetByUser() ){
1898 options::preSkolemQuant
.set( true );
1900 if( !options::preSkolemQuantNested
.wasSetByUser() ){
1901 options::preSkolemQuantNested
.set( true );
1903 if( !options::fmfOneInstPerRound
.wasSetByUser() ){
1904 options::fmfOneInstPerRound
.set( true );
1909 //apply counterexample guided instantiation options
1910 // if we are attempting to rewrite everything to SyGuS, use ceGuidedInst
1911 if (options::sygusInference())
1913 if (!options::ceGuidedInst
.wasSetByUser())
1915 options::ceGuidedInst
.set(true);
1917 // optimization: apply preskolemization, makes it succeed more often
1918 if (!options::preSkolemQuant
.wasSetByUser())
1920 options::preSkolemQuant
.set(true);
1922 if (!options::preSkolemQuantNested
.wasSetByUser())
1924 options::preSkolemQuantNested
.set(true);
1927 if( options::cegqiSingleInvMode()!=quantifiers::CEGQI_SI_MODE_NONE
){
1928 if( !options::ceGuidedInst
.wasSetByUser() ){
1929 options::ceGuidedInst
.set( true );
1932 // if sygus is enabled, set the defaults for sygus
1933 if( options::ceGuidedInst() ){
1934 //counterexample-guided instantiation for sygus
1935 if( !options::cegqiSingleInvMode
.wasSetByUser() ){
1936 options::cegqiSingleInvMode
.set( quantifiers::CEGQI_SI_MODE_USE
);
1938 if( !options::quantConflictFind
.wasSetByUser() ){
1939 options::quantConflictFind
.set( false );
1941 if( !options::instNoEntail
.wasSetByUser() ){
1942 options::instNoEntail
.set( false );
1944 if (!options::cbqiFullEffort
.wasSetByUser())
1946 // should use full effort cbqi for single invocation and repair const
1947 options::cbqiFullEffort
.set(true);
1949 if (options::sygusRew())
1951 options::sygusRewSynth
.set(true);
1952 options::sygusRewVerify
.set(true);
1954 if (options::sygusRewSynth() || options::sygusRewVerify())
1956 // rewrite rule synthesis implies that sygus stream must be true
1957 options::sygusStream
.set(true);
1959 if (options::sygusStream())
1961 // PBE and streaming modes are incompatible
1962 if (!options::sygusSymBreakPbe
.wasSetByUser())
1964 options::sygusSymBreakPbe
.set(false);
1966 if (!options::sygusUnifPbe
.wasSetByUser())
1968 options::sygusUnifPbe
.set(false);
1971 //do not allow partial functions
1972 if( !options::bitvectorDivByZeroConst
.wasSetByUser() ){
1973 options::bitvectorDivByZeroConst
.set( true );
1975 if( !options::dtRewriteErrorSel
.wasSetByUser() ){
1976 options::dtRewriteErrorSel
.set( true );
1979 if( !options::miniscopeQuant
.wasSetByUser() ){
1980 options::miniscopeQuant
.set( false );
1982 if( !options::miniscopeQuantFreeVar
.wasSetByUser() ){
1983 options::miniscopeQuantFreeVar
.set( false );
1985 if (!options::quantSplit
.wasSetByUser())
1987 options::quantSplit
.set(false);
1990 if( !options::rewriteDivk
.wasSetByUser()) {
1991 options::rewriteDivk
.set( true );
1994 if( !options::macrosQuant
.wasSetByUser()) {
1995 options::macrosQuant
.set( false );
1997 if( !options::cbqiPreRegInst
.wasSetByUser()) {
1998 options::cbqiPreRegInst
.set( true );
2001 //counterexample-guided instantiation for non-sygus
2002 // enable if any possible quantifiers with arithmetic, datatypes or bitvectors
2003 if (d_logic
.isQuantified()
2004 && ((options::decisionMode() != decision::DECISION_STRATEGY_INTERNAL
2005 && (d_logic
.isTheoryEnabled(THEORY_ARITH
)
2006 || d_logic
.isTheoryEnabled(THEORY_DATATYPES
)
2007 || d_logic
.isTheoryEnabled(THEORY_BV
)
2008 || d_logic
.isTheoryEnabled(THEORY_FP
)))
2009 || d_logic
.isPure(THEORY_ARITH
) || d_logic
.isPure(THEORY_BV
)
2010 || options::cbqiAll()))
2012 if( !options::cbqi
.wasSetByUser() ){
2013 options::cbqi
.set( true );
2015 // check whether we should apply full cbqi
2016 if (d_logic
.isPure(THEORY_BV
))
2018 if (!options::cbqiFullEffort
.wasSetByUser())
2020 options::cbqiFullEffort
.set(true);
2024 if( options::cbqi() ){
2026 if( !options::rewriteDivk
.wasSetByUser()) {
2027 options::rewriteDivk
.set( true );
2029 if (options::incrementalSolving())
2031 // cannot do nested quantifier elimination in incremental mode
2032 options::cbqiNestedQE
.set(false);
2034 if (d_logic
.isPure(THEORY_ARITH
) || d_logic
.isPure(THEORY_BV
))
2036 options::cbqiAll
.set( false );
2037 if( !options::quantConflictFind
.wasSetByUser() ){
2038 options::quantConflictFind
.set( false );
2040 if( !options::instNoEntail
.wasSetByUser() ){
2041 options::instNoEntail
.set( false );
2043 if( !options::instWhenMode
.wasSetByUser() && options::cbqiModel() ){
2044 //only instantiation should happen at last call when model is avaiable
2045 options::instWhenMode
.set( quantifiers::INST_WHEN_LAST_CALL
);
2048 // only supported in pure arithmetic or pure BV
2049 options::cbqiNestedQE
.set(false);
2052 if (options::cbqiNestedQE()
2053 || options::decisionMode() == decision::DECISION_STRATEGY_INTERNAL
)
2055 // only complete with prenex = disj_normal or normal
2056 if (options::prenexQuant() <= quantifiers::PRENEX_QUANT_DISJ_NORMAL
)
2058 options::prenexQuant
.set(quantifiers::PRENEX_QUANT_DISJ_NORMAL
);
2061 else if (options::globalNegate())
2063 if (!options::prenexQuant
.wasSetByUser())
2065 options::prenexQuant
.set(quantifiers::PRENEX_QUANT_NONE
);
2069 //implied options...
2070 if( options::strictTriggers() ){
2071 if( !options::userPatternsQuant
.wasSetByUser() ){
2072 options::userPatternsQuant
.set( quantifiers::USER_PAT_MODE_TRUST
);
2075 if( options::qcfMode
.wasSetByUser() || options::qcfTConstraint() ){
2076 options::quantConflictFind
.set( true );
2078 if( options::cbqiNestedQE() ){
2079 options::prenexQuantUser
.set( true );
2080 if( !options::preSkolemQuant
.wasSetByUser() ){
2081 options::preSkolemQuant
.set( true );
2084 //for induction techniques
2085 if( options::quantInduction() ){
2086 if( !options::dtStcInduction
.wasSetByUser() ){
2087 options::dtStcInduction
.set( true );
2089 if( !options::intWfInduction
.wasSetByUser() ){
2090 options::intWfInduction
.set( true );
2093 if( options::dtStcInduction() ){
2094 //try to remove ITEs from quantified formulas
2095 if( !options::iteDtTesterSplitQuant
.wasSetByUser() ){
2096 options::iteDtTesterSplitQuant
.set( true );
2098 if( !options::iteLiftQuant
.wasSetByUser() ){
2099 options::iteLiftQuant
.set( quantifiers::ITE_LIFT_QUANT_MODE_ALL
);
2102 if( options::intWfInduction() ){
2103 if( !options::purifyTriggers
.wasSetByUser() ){
2104 options::purifyTriggers
.set( true );
2107 if( options::conjectureNoFilter() ){
2108 if( !options::conjectureFilterActiveTerms
.wasSetByUser() ){
2109 options::conjectureFilterActiveTerms
.set( false );
2111 if( !options::conjectureFilterCanonical
.wasSetByUser() ){
2112 options::conjectureFilterCanonical
.set( false );
2114 if( !options::conjectureFilterModel
.wasSetByUser() ){
2115 options::conjectureFilterModel
.set( false );
2118 if( options::conjectureGenPerRound
.wasSetByUser() ){
2119 if( options::conjectureGenPerRound()>0 ){
2120 options::conjectureGen
.set( true );
2122 options::conjectureGen
.set( false );
2125 //can't pre-skolemize nested quantifiers without UF theory
2126 if( !d_logic
.isTheoryEnabled(THEORY_UF
) && options::preSkolemQuant() ){
2127 if( !options::preSkolemQuantNested
.wasSetByUser() ){
2128 options::preSkolemQuantNested
.set( false );
2131 if( !d_logic
.isTheoryEnabled(THEORY_DATATYPES
) ){
2132 options::quantDynamicSplit
.set( quantifiers::QUANT_DSPLIT_MODE_NONE
);
2135 //until bugs 371,431 are fixed
2136 if( ! options::minisatUseElim
.wasSetByUser()){
2137 // cannot use minisat elimination for logics where a theory solver
2138 // introduces new literals into the search. This includes quantifiers
2139 // (quantifier instantiation), and the lemma schemas used in non-linear
2140 // and sets. We also can't use it if models are enabled.
2141 if (d_logic
.isTheoryEnabled(THEORY_SETS
) || d_logic
.isQuantified()
2142 || options::produceModels() || options::produceAssignments()
2143 || options::checkModels()
2144 || (d_logic
.isTheoryEnabled(THEORY_ARITH
) && !d_logic
.isLinear()))
2146 options::minisatUseElim
.set( false );
2149 else if (options::minisatUseElim()) {
2150 if (options::produceModels()) {
2151 Notice() << "SmtEngine: turning off produce-models to support minisatUseElim" << endl
;
2152 setOption("produce-models", SExpr("false"));
2154 if (options::produceAssignments()) {
2155 Notice() << "SmtEngine: turning off produce-assignments to support minisatUseElim" << endl
;
2156 setOption("produce-assignments", SExpr("false"));
2158 if (options::checkModels()) {
2159 Notice() << "SmtEngine: turning off check-models to support minisatUseElim" << endl
;
2160 setOption("check-models", SExpr("false"));
2164 // For now, these array theory optimizations do not support model-building
2165 if (options::produceModels() || options::produceAssignments() || options::checkModels()) {
2166 options::arraysOptimizeLinear
.set(false);
2167 options::arraysLazyRIntro1
.set(false);
2170 // Non-linear arithmetic does not support models unless nlExt is enabled
2171 if ((d_logic
.isTheoryEnabled(THEORY_ARITH
) && !d_logic
.isLinear()
2172 && !options::nlExt())
2173 || options::globalNegate())
2175 std::string reason
=
2176 options::globalNegate() ? "--global-negate" : "nonlinear arithmetic";
2177 if (options::produceModels()) {
2178 if(options::produceModels
.wasSetByUser()) {
2179 throw OptionException(
2180 std::string("produce-model not supported with " + reason
));
2183 << "SmtEngine: turning off produce-models because unsupported for "
2185 setOption("produce-models", SExpr("false"));
2187 if (options::produceAssignments()) {
2188 if(options::produceAssignments
.wasSetByUser()) {
2189 throw OptionException(
2190 std::string("produce-assignments not supported with " + reason
));
2192 Warning() << "SmtEngine: turning off produce-assignments because "
2195 setOption("produce-assignments", SExpr("false"));
2197 if (options::checkModels()) {
2198 if(options::checkModels
.wasSetByUser()) {
2199 throw OptionException(
2200 std::string("check-models not supported with " + reason
));
2203 << "SmtEngine: turning off check-models because unsupported for "
2205 setOption("check-models", SExpr("false"));
2209 if(options::incrementalSolving() && options::proof()) {
2210 Warning() << "SmtEngine: turning off incremental solving mode (not yet supported with --proof, try --tear-down-incremental instead)" << endl
;
2211 setOption("incremental", SExpr("false"));
2214 if (options::proof())
2216 if (options::bitvectorAlgebraicSolver())
2218 if (options::bitvectorAlgebraicSolver
.wasSetByUser())
2220 throw OptionException(
2221 "--bv-algebraic-solver is not supported with proofs");
2223 Notice() << "SmtEngine: turning off bv algebraic solver to support proofs"
2225 options::bitvectorAlgebraicSolver
.set(false);
2227 if (options::bitvectorEqualitySolver())
2229 if (options::bitvectorEqualitySolver
.wasSetByUser())
2231 throw OptionException("--bv-eq-solver is not supported with proofs");
2233 Notice() << "SmtEngine: turning off bv eq solver to support proofs"
2235 options::bitvectorEqualitySolver
.set(false);
2237 if (options::bitvectorInequalitySolver())
2239 if (options::bitvectorInequalitySolver
.wasSetByUser())
2241 throw OptionException(
2242 "--bv-inequality-solver is not supported with proofs");
2244 Notice() << "SmtEngine: turning off bv ineq solver to support proofs"
2246 options::bitvectorInequalitySolver
.set(false);
2250 if (!options::bitvectorEqualitySolver())
2252 if (options::bvLazyRewriteExtf())
2254 if (options::bvLazyRewriteExtf
.wasSetByUser())
2256 throw OptionException(
2257 "--bv-lazy-rewrite-extf requires --bv-eq-solver to be set");
2261 << "disabling bvLazyRewriteExtf since equality solver is disabled"
2263 options::bvLazyRewriteExtf
.set(false);
2267 void SmtEngine::setProblemExtended(bool value
)
2269 d_problemExtended
= value
;
2270 if (value
) { d_assumptions
.clear(); }
2273 void SmtEngine::setInfo(const std::string
& key
, const CVC4::SExpr
& value
)
2275 SmtScope
smts(this);
2277 Trace("smt") << "SMT setInfo(" << key
<< ", " << value
<< ")" << endl
;
2279 if(Dump
.isOn("benchmark")) {
2280 if(key
== "status") {
2281 string s
= value
.getValue();
2282 BenchmarkStatus status
=
2283 (s
== "sat") ? SMT_SATISFIABLE
:
2284 ((s
== "unsat") ? SMT_UNSATISFIABLE
: SMT_UNKNOWN
);
2285 Dump("benchmark") << SetBenchmarkStatusCommand(status
);
2287 Dump("benchmark") << SetInfoCommand(key
, value
);
2291 // Check for CVC4-specific info keys (prefixed with "cvc4-" or "cvc4_")
2292 if(key
.length() > 5) {
2293 string prefix
= key
.substr(0, 5);
2294 if(prefix
== "cvc4-" || prefix
== "cvc4_") {
2295 string cvc4key
= key
.substr(5);
2296 if(cvc4key
== "logic") {
2297 if(! value
.isAtom()) {
2298 throw OptionException("argument to (set-info :cvc4-logic ..) must be a string");
2300 SmtScope
smts(this);
2301 d_logic
= value
.getValue();
2305 throw UnrecognizedOptionException();
2310 // Check for standard info keys (SMT-LIB v1, SMT-LIB v2, ...)
2312 || key
== "category"
2313 || key
== "difficulty"
2315 || key
== "license")
2319 } else if(key
== "name") {
2320 d_filename
= value
.getValue();
2323 else if (key
== "smt-lib-version" && !options::inputLanguage
.wasSetByUser())
2325 language::input::Language ilang
= language::input::LANG_AUTO
;
2326 if( (value
.isInteger() && value
.getIntegerValue() == Integer(2)) ||
2327 (value
.isRational() && value
.getRationalValue() == Rational(2)) ||
2328 value
.getValue() == "2" ||
2329 value
.getValue() == "2.0" ) {
2330 ilang
= language::input::LANG_SMTLIB_V2_0
;
2331 } else if( (value
.isRational() && value
.getRationalValue() == Rational(5, 2)) ||
2332 value
.getValue() == "2.5" ) {
2333 ilang
= language::input::LANG_SMTLIB_V2_5
;
2334 } else if( (value
.isRational() && value
.getRationalValue() == Rational(13, 5)) ||
2335 value
.getValue() == "2.6" ) {
2336 ilang
= language::input::LANG_SMTLIB_V2_6
;
2338 else if (value
.getValue() == "2.6.1")
2340 ilang
= language::input::LANG_SMTLIB_V2_6_1
;
2344 Warning() << "Warning: unsupported smt-lib-version: " << value
<< endl
;
2345 throw UnrecognizedOptionException();
2347 options::inputLanguage
.set(ilang
);
2348 // also update the output language
2349 if (!options::outputLanguage
.wasSetByUser())
2351 language::output::Language olang
= language::toOutputLanguage(ilang
);
2352 if (options::outputLanguage() != olang
)
2354 options::outputLanguage
.set(olang
);
2355 *options::out() << language::SetLanguage(olang
);
2359 } else if(key
== "status") {
2361 if(value
.isAtom()) {
2362 s
= value
.getValue();
2364 if(s
!= "sat" && s
!= "unsat" && s
!= "unknown") {
2365 throw OptionException("argument to (set-info :status ..) must be "
2366 "`sat' or `unsat' or `unknown'");
2368 d_status
= Result(s
, d_filename
);
2371 throw UnrecognizedOptionException();
2374 CVC4::SExpr
SmtEngine::getInfo(const std::string
& key
) const {
2376 SmtScope
smts(this);
2378 Trace("smt") << "SMT getInfo(" << key
<< ")" << endl
;
2379 if(key
== "all-statistics") {
2380 vector
<SExpr
> stats
;
2381 for(StatisticsRegistry::const_iterator i
= NodeManager::fromExprManager(d_exprManager
)->getStatisticsRegistry()->begin();
2382 i
!= NodeManager::fromExprManager(d_exprManager
)->getStatisticsRegistry()->end();
2385 v
.push_back((*i
).first
);
2386 v
.push_back((*i
).second
);
2389 for(StatisticsRegistry::const_iterator i
= d_statisticsRegistry
->begin();
2390 i
!= d_statisticsRegistry
->end();
2393 v
.push_back((*i
).first
);
2394 v
.push_back((*i
).second
);
2397 return SExpr(stats
);
2398 } else if(key
== "error-behavior") {
2399 // immediate-exit | continued-execution
2400 if( options::continuedExecution() || options::interactive() ) {
2401 return SExpr(SExpr::Keyword("continued-execution"));
2403 return SExpr(SExpr::Keyword("immediate-exit"));
2405 } else if(key
== "name") {
2406 return SExpr(Configuration::getName());
2407 } else if(key
== "version") {
2408 return SExpr(Configuration::getVersionString());
2409 } else if(key
== "authors") {
2410 return SExpr(Configuration::about());
2411 } else if(key
== "status") {
2412 // sat | unsat | unknown
2413 switch(d_status
.asSatisfiabilityResult().isSat()) {
2415 return SExpr(SExpr::Keyword("sat"));
2417 return SExpr(SExpr::Keyword("unsat"));
2419 return SExpr(SExpr::Keyword("unknown"));
2421 } else if(key
== "reason-unknown") {
2422 if(!d_status
.isNull() && d_status
.isUnknown()) {
2424 ss
<< d_status
.whyUnknown();
2425 string s
= ss
.str();
2426 transform(s
.begin(), s
.end(), s
.begin(), ::tolower
);
2427 return SExpr(SExpr::Keyword(s
));
2429 throw ModalException("Can't get-info :reason-unknown when the "
2430 "last result wasn't unknown!");
2432 } else if(key
== "assertion-stack-levels") {
2433 AlwaysAssert(d_userLevels
.size() <=
2434 std::numeric_limits
<unsigned long int>::max());
2435 return SExpr(static_cast<unsigned long int>(d_userLevels
.size()));
2436 } else if(key
== "all-options") {
2437 // get the options, like all-statistics
2438 std::vector
< std::vector
<std::string
> > current_options
=
2439 Options::current()->getOptions();
2440 return SExpr::parseListOfListOfAtoms(current_options
);
2442 throw UnrecognizedOptionException();
2446 void SmtEngine::debugCheckFormals(const std::vector
<Expr
>& formals
, Expr func
)
2448 for(std::vector
<Expr
>::const_iterator i
= formals
.begin(); i
!= formals
.end(); ++i
) {
2449 if((*i
).getKind() != kind::BOUND_VARIABLE
) {
2451 ss
<< "All formal arguments to defined functions must be BOUND_VARIABLEs, but in the\n"
2452 << "definition of function " << func
<< ", formal\n"
2453 << " " << *i
<< "\n"
2454 << "has kind " << (*i
).getKind();
2455 throw TypeCheckingException(func
, ss
.str());
2460 void SmtEngine::debugCheckFunctionBody(Expr formula
,
2461 const std::vector
<Expr
>& formals
,
2464 Type formulaType
= formula
.getType(options::typeChecking());
2465 Type funcType
= func
.getType();
2466 // We distinguish here between definitions of constants and functions,
2467 // because the type checking for them is subtly different. Perhaps we
2468 // should instead have SmtEngine::defineFunction() and
2469 // SmtEngine::defineConstant() for better clarity, although then that
2470 // doesn't match the SMT-LIBv2 standard...
2471 if(formals
.size() > 0) {
2472 Type rangeType
= FunctionType(funcType
).getRangeType();
2473 if(! formulaType
.isComparableTo(rangeType
)) {
2475 ss
<< "Type of defined function does not match its declaration\n"
2476 << "The function : " << func
<< "\n"
2477 << "Declared type : " << rangeType
<< "\n"
2478 << "The body : " << formula
<< "\n"
2479 << "Body type : " << formulaType
;
2480 throw TypeCheckingException(func
, ss
.str());
2483 if(! formulaType
.isComparableTo(funcType
)) {
2485 ss
<< "Declared type of defined constant does not match its definition\n"
2486 << "The constant : " << func
<< "\n"
2487 << "Declared type : " << funcType
<< " " << Type::getTypeNode(funcType
)->getId() << "\n"
2488 << "The definition : " << formula
<< "\n"
2489 << "Definition type: " << formulaType
<< " " << Type::getTypeNode(formulaType
)->getId();
2490 throw TypeCheckingException(func
, ss
.str());
2495 void SmtEngine::defineFunction(Expr func
,
2496 const std::vector
<Expr
>& formals
,
2499 SmtScope
smts(this);
2501 Trace("smt") << "SMT defineFunction(" << func
<< ")" << endl
;
2502 debugCheckFormals(formals
, func
);
2505 ss
<< language::SetLanguage(
2506 language::SetLanguage::getLanguage(Dump
.getStream()))
2508 DefineFunctionCommand
c(ss
.str(), func
, formals
, formula
);
2509 addToModelCommandAndDump(
2510 c
, ExprManager::VAR_FLAG_DEFINED
, true, "declarations");
2512 PROOF(if (options::checkUnsatCores()) {
2513 d_defineCommands
.push_back(c
.clone());
2517 debugCheckFunctionBody(formula
, formals
, func
);
2519 // Substitute out any abstract values in formula
2521 d_private
->substituteAbstractValues(Node::fromExpr(formula
)).toExpr();
2523 TNode funcNode
= func
.getTNode();
2524 vector
<Node
> formalsNodes
;
2525 for(vector
<Expr
>::const_iterator i
= formals
.begin(),
2526 iend
= formals
.end();
2529 formalsNodes
.push_back((*i
).getNode());
2531 TNode formNode
= form
.getTNode();
2532 DefinedFunction
def(funcNode
, formalsNodes
, formNode
);
2533 // Permit (check-sat) (define-fun ...) (get-value ...) sequences.
2534 // Otherwise, (check-sat) (get-value ((! foo :named bar))) breaks
2535 // d_haveAdditions = true;
2536 Debug("smt") << "definedFunctions insert " << funcNode
<< " " << formNode
<< endl
;
2537 d_definedFunctions
->insert(funcNode
, def
);
2540 void SmtEngine::defineFunctionsRec(
2541 const std::vector
<Expr
>& funcs
,
2542 const std::vector
<std::vector
<Expr
> >& formals
,
2543 const std::vector
<Expr
>& formulas
)
2545 SmtScope
smts(this);
2546 finalOptionsAreSet();
2548 Trace("smt") << "SMT defineFunctionsRec(...)" << endl
;
2550 if (funcs
.size() != formals
.size() && funcs
.size() != formulas
.size())
2553 ss
<< "Number of functions, formals, and function bodies passed to "
2554 "defineFunctionsRec do not match:"
2556 << " #functions : " << funcs
.size() << "\n"
2557 << " #arg lists : " << formals
.size() << "\n"
2558 << " #function bodies : " << formulas
.size() << "\n";
2559 throw ModalException(ss
.str());
2561 for (unsigned i
= 0, size
= funcs
.size(); i
< size
; i
++)
2563 // check formal argument list
2564 debugCheckFormals(formals
[i
], funcs
[i
]);
2566 debugCheckFunctionBody(formulas
[i
], formals
[i
], funcs
[i
]);
2569 if (Dump
.isOn("raw-benchmark"))
2571 Dump("raw-benchmark") << DefineFunctionRecCommand(funcs
, formals
, formulas
);
2574 ExprManager
* em
= getExprManager();
2575 for (unsigned i
= 0, size
= funcs
.size(); i
< size
; i
++)
2577 // we assert a quantified formula
2579 // make the function application
2580 if (formals
[i
].empty())
2582 // it has no arguments
2583 func_app
= funcs
[i
];
2587 std::vector
<Expr
> children
;
2588 children
.push_back(funcs
[i
]);
2589 children
.insert(children
.end(), formals
[i
].begin(), formals
[i
].end());
2590 func_app
= em
->mkExpr(kind::APPLY_UF
, children
);
2592 Expr lem
= em
->mkExpr(kind::EQUAL
, func_app
, formulas
[i
]);
2593 if (!formals
[i
].empty())
2595 // set the attribute to denote this is a function definition
2596 std::string
attr_name("fun-def");
2597 Expr aexpr
= em
->mkExpr(kind::INST_ATTRIBUTE
, func_app
);
2598 aexpr
= em
->mkExpr(kind::INST_PATTERN_LIST
, aexpr
);
2599 std::vector
<Expr
> expr_values
;
2600 std::string str_value
;
2601 setUserAttribute(attr_name
, func_app
, expr_values
, str_value
);
2602 // make the quantified formula
2603 Expr boundVars
= em
->mkExpr(kind::BOUND_VAR_LIST
, formals
[i
]);
2604 lem
= em
->mkExpr(kind::FORALL
, boundVars
, lem
, aexpr
);
2606 // assert the quantified formula
2607 // notice we don't call assertFormula directly, since this would
2608 // duplicate the output on raw-benchmark.
2609 Expr e
= d_private
->substituteAbstractValues(Node::fromExpr(lem
)).toExpr();
2610 if (d_assertionList
!= NULL
)
2612 d_assertionList
->push_back(e
);
2614 d_private
->addFormula(e
.getNode(), false);
2618 void SmtEngine::defineFunctionRec(Expr func
,
2619 const std::vector
<Expr
>& formals
,
2622 std::vector
<Expr
> funcs
;
2623 funcs
.push_back(func
);
2624 std::vector
<std::vector
<Expr
> > formals_multi
;
2625 formals_multi
.push_back(formals
);
2626 std::vector
<Expr
> formulas
;
2627 formulas
.push_back(formula
);
2628 defineFunctionsRec(funcs
, formals_multi
, formulas
);
2631 bool SmtEngine::isDefinedFunction( Expr func
){
2632 Node nf
= Node::fromExpr( func
);
2633 Debug("smt") << "isDefined function " << nf
<< "?" << std::endl
;
2634 return d_definedFunctions
->find(nf
) != d_definedFunctions
->end();
2637 void SmtEnginePrivate::finishInit()
2639 d_preprocessingPassContext
.reset(
2640 new PreprocessingPassContext(&d_smt
, d_resourceManager
, &d_iteRemover
));
2641 // TODO: register passes here (this will likely change when we add support for
2642 // actually assembling preprocessing pipelines).
2643 std::unique_ptr
<ApplySubsts
> applySubsts(
2644 new ApplySubsts(d_preprocessingPassContext
.get()));
2645 std::unique_ptr
<ApplyToConst
> applyToConst(
2646 new ApplyToConst(d_preprocessingPassContext
.get()));
2647 std::unique_ptr
<BoolToBV
> boolToBv(
2648 new BoolToBV(d_preprocessingPassContext
.get()));
2649 std::unique_ptr
<BvAbstraction
> bvAbstract(
2650 new BvAbstraction(d_preprocessingPassContext
.get()));
2651 std::unique_ptr
<BvEagerAtoms
> bvEagerAtoms(
2652 new BvEagerAtoms(d_preprocessingPassContext
.get()));
2653 std::unique_ptr
<BVAckermann
> bvAckermann(
2654 new BVAckermann(d_preprocessingPassContext
.get()));
2655 std::unique_ptr
<BVGauss
> bvGauss(
2656 new BVGauss(d_preprocessingPassContext
.get()));
2657 std::unique_ptr
<BvIntroPow2
> bvIntroPow2(
2658 new BvIntroPow2(d_preprocessingPassContext
.get()));
2659 std::unique_ptr
<BVToBool
> bvToBool(
2660 new BVToBool(d_preprocessingPassContext
.get()));
2661 std::unique_ptr
<ExtRewPre
> extRewPre(
2662 new ExtRewPre(d_preprocessingPassContext
.get()));
2663 std::unique_ptr
<IntToBV
> intToBV(
2664 new IntToBV(d_preprocessingPassContext
.get()));
2665 std::unique_ptr
<QuantifiersPreprocess
> quantifiersPreprocess(
2666 new QuantifiersPreprocess(d_preprocessingPassContext
.get()));
2667 std::unique_ptr
<PseudoBooleanProcessor
> pbProc(
2668 new PseudoBooleanProcessor(d_preprocessingPassContext
.get()));
2669 std::unique_ptr
<IteRemoval
> iteRemoval(
2670 new IteRemoval(d_preprocessingPassContext
.get()));
2671 std::unique_ptr
<RealToInt
> realToInt(
2672 new RealToInt(d_preprocessingPassContext
.get()));
2673 std::unique_ptr
<Rewrite
> rewrite(
2674 new Rewrite(d_preprocessingPassContext
.get()));
2675 std::unique_ptr
<SortInferencePass
> sortInfer(
2676 new SortInferencePass(d_preprocessingPassContext
.get(),
2677 d_smt
.d_theoryEngine
->getSortInference()));
2678 std::unique_ptr
<StaticLearning
> staticLearning(
2679 new StaticLearning(d_preprocessingPassContext
.get()));
2680 std::unique_ptr
<SygusInference
> sygusInfer(
2681 new SygusInference(d_preprocessingPassContext
.get()));
2682 std::unique_ptr
<SymBreakerPass
> sbProc(
2683 new SymBreakerPass(d_preprocessingPassContext
.get()));
2684 std::unique_ptr
<SynthRewRulesPass
> srrProc(
2685 new SynthRewRulesPass(d_preprocessingPassContext
.get()));
2686 std::unique_ptr
<SepSkolemEmp
> sepSkolemEmp(
2687 new SepSkolemEmp(d_preprocessingPassContext
.get()));
2688 d_preprocessingPassRegistry
.registerPass("apply-substs",
2689 std::move(applySubsts
));
2690 d_preprocessingPassRegistry
.registerPass("apply-to-const",
2691 std::move(applyToConst
));
2692 d_preprocessingPassRegistry
.registerPass("bool-to-bv", std::move(boolToBv
));
2693 d_preprocessingPassRegistry
.registerPass("bv-abstraction",
2694 std::move(bvAbstract
));
2695 d_preprocessingPassRegistry
.registerPass("bv-ackermann",
2696 std::move(bvAckermann
));
2697 d_preprocessingPassRegistry
.registerPass("bv-eager-atoms",
2698 std::move(bvEagerAtoms
));
2699 d_preprocessingPassRegistry
.registerPass("bv-gauss", std::move(bvGauss
));
2700 d_preprocessingPassRegistry
.registerPass("bv-intro-pow2",
2701 std::move(bvIntroPow2
));
2702 d_preprocessingPassRegistry
.registerPass("bv-to-bool", std::move(bvToBool
));
2703 d_preprocessingPassRegistry
.registerPass("ext-rew-pre", std::move(extRewPre
));
2704 d_preprocessingPassRegistry
.registerPass("int-to-bv", std::move(intToBV
));
2705 d_preprocessingPassRegistry
.registerPass("quantifiers-preprocess",
2706 std::move(quantifiersPreprocess
));
2707 d_preprocessingPassRegistry
.registerPass("pseudo-boolean-processor",
2709 d_preprocessingPassRegistry
.registerPass("ite-removal",
2710 std::move(iteRemoval
));
2711 d_preprocessingPassRegistry
.registerPass("real-to-int", std::move(realToInt
));
2712 d_preprocessingPassRegistry
.registerPass("rewrite", std::move(rewrite
));
2713 d_preprocessingPassRegistry
.registerPass("sep-skolem-emp",
2714 std::move(sepSkolemEmp
));
2715 d_preprocessingPassRegistry
.registerPass("sort-inference",
2716 std::move(sortInfer
));
2717 d_preprocessingPassRegistry
.registerPass("static-learning",
2718 std::move(staticLearning
));
2719 d_preprocessingPassRegistry
.registerPass("sygus-infer",
2720 std::move(sygusInfer
));
2721 d_preprocessingPassRegistry
.registerPass("sym-break", std::move(sbProc
));
2722 d_preprocessingPassRegistry
.registerPass("synth-rr", std::move(srrProc
));
2725 Node
SmtEnginePrivate::expandDefinitions(TNode n
, unordered_map
<Node
, Node
, NodeHashFunction
>& cache
, bool expandOnly
)
2727 stack
<std::tuple
<Node
, Node
, bool>> worklist
;
2729 worklist
.push(std::make_tuple(Node(n
), Node(n
), false));
2730 // The worklist is made of triples, each is input / original node then the output / rewritten node
2731 // and finally a flag tracking whether the children have been explored (i.e. if this is a downward
2735 spendResource(options::preprocessStep());
2737 // n is the input / original
2738 // node is the output / result
2740 bool childrenPushed
;
2741 std::tie(n
, node
, childrenPushed
) = worklist
.top();
2744 // Working downwards
2745 if(!childrenPushed
) {
2746 Kind k
= n
.getKind();
2748 // we can short circuit (variable) leaves
2750 SmtEngine::DefinedFunctionMap::const_iterator i
= d_smt
.d_definedFunctions
->find(n
);
2751 if(i
!= d_smt
.d_definedFunctions
->end()) {
2752 // replacement must be closed
2753 if((*i
).second
.getFormals().size() > 0) {
2754 result
.push(d_smt
.d_nodeManager
->mkNode(kind::LAMBDA
, d_smt
.d_nodeManager
->mkNode(kind::BOUND_VAR_LIST
, (*i
).second
.getFormals()), (*i
).second
.getFormula()));
2757 // don't bother putting in the cache
2758 result
.push((*i
).second
.getFormula());
2761 // don't bother putting in the cache
2766 // maybe it's in the cache
2767 unordered_map
<Node
, Node
, NodeHashFunction
>::iterator cacheHit
= cache
.find(n
);
2768 if(cacheHit
!= cache
.end()) {
2769 TNode ret
= (*cacheHit
).second
;
2770 result
.push(ret
.isNull() ? n
: ret
);
2774 // otherwise expand it
2775 bool doExpand
= false;
2776 if (k
== kind::APPLY
)
2780 else if (k
== kind::APPLY_UF
)
2782 // Always do beta-reduction here. The reason is that there may be
2783 // operators such as INTS_MODULUS in the body of the lambda that would
2784 // otherwise be introduced by beta-reduction via the rewriter, but are
2785 // not expanded here since the traversal in this function does not
2786 // traverse the operators of nodes. Hence, we beta-reduce here to
2787 // ensure terms in the body of the lambda are expanded during this
2789 if (n
.getOperator().getKind() == kind::LAMBDA
)
2793 else if (options::macrosQuant() || options::sygusInference())
2795 // The above options assign substitutions to APPLY_UF, thus we check
2796 // here and expand if this operator corresponds to a defined function.
2797 doExpand
= d_smt
.isDefinedFunction(n
.getOperator().toExpr());
2801 vector
<Node
> formals
;
2803 if( n
.getOperator().getKind() == kind::LAMBDA
){
2804 TNode op
= n
.getOperator();
2806 for( unsigned i
=0; i
<op
[0].getNumChildren(); i
++ ){
2807 formals
.push_back( op
[0][i
] );
2811 // application of a user-defined symbol
2812 TNode func
= n
.getOperator();
2813 SmtEngine::DefinedFunctionMap::const_iterator i
= d_smt
.d_definedFunctions
->find(func
);
2814 if(i
== d_smt
.d_definedFunctions
->end()) {
2815 throw TypeCheckingException(n
.toExpr(), string("Undefined function: `") + func
.toString() + "'");
2817 DefinedFunction def
= (*i
).second
;
2818 formals
= def
.getFormals();
2820 if(Debug
.isOn("expand")) {
2821 Debug("expand") << "found: " << n
<< endl
;
2822 Debug("expand") << " func: " << func
<< endl
;
2823 string name
= func
.getAttribute(expr::VarNameAttr());
2824 Debug("expand") << " : \"" << name
<< "\"" << endl
;
2826 if(Debug
.isOn("expand")) {
2827 Debug("expand") << " defn: " << def
.getFunction() << endl
2829 if(formals
.size() > 0) {
2830 copy( formals
.begin(), formals
.end() - 1,
2831 ostream_iterator
<Node
>(Debug("expand"), ", ") );
2832 Debug("expand") << formals
.back();
2834 Debug("expand") << "]" << endl
2835 << " " << def
.getFunction().getType() << endl
2836 << " " << def
.getFormula() << endl
;
2839 fm
= def
.getFormula();
2842 Node instance
= fm
.substitute(formals
.begin(),
2845 n
.begin() + formals
.size());
2846 Debug("expand") << "made : " << instance
<< endl
;
2848 Node expanded
= expandDefinitions(instance
, cache
, expandOnly
);
2849 cache
[n
] = (n
== expanded
? Node::null() : expanded
);
2850 result
.push(expanded
);
2853 } else if(! expandOnly
) {
2854 // do not do any theory stuff if expandOnly is true
2856 theory::Theory
* t
= d_smt
.d_theoryEngine
->theoryOf(node
);
2859 LogicRequest
req(d_smt
);
2860 node
= t
->expandDefinition(req
, n
);
2863 // the partial functions can fall through, in which case we still
2864 // consider their children
2865 worklist
.push(std::make_tuple(
2866 Node(n
), node
, true)); // Original and rewritten result
2868 for(size_t i
= 0; i
< node
.getNumChildren(); ++i
) {
2870 std::make_tuple(node
[i
],
2872 false)); // Rewrite the children of the result only
2877 // Reconstruct the node from it's (now rewritten) children on the stack
2879 Debug("expand") << "cons : " << node
<< endl
;
2880 if(node
.getNumChildren()>0) {
2881 //cout << "cons : " << node << endl;
2882 NodeBuilder
<> nb(node
.getKind());
2883 if(node
.getMetaKind() == kind::metakind::PARAMETERIZED
) {
2884 Debug("expand") << "op : " << node
.getOperator() << endl
;
2885 //cout << "op : " << node.getOperator() << endl;
2886 nb
<< node
.getOperator();
2888 for(size_t i
= 0; i
< node
.getNumChildren(); ++i
) {
2889 Assert(!result
.empty());
2890 Node expanded
= result
.top();
2892 //cout << "exchld : " << expanded << endl;
2893 Debug("expand") << "exchld : " << expanded
<< endl
;
2898 cache
[n
] = n
== node
? Node::null() : node
; // Only cache once all subterms are expanded
2901 } while(!worklist
.empty());
2903 AlwaysAssert(result
.size() == 1);
2905 return result
.top();
2908 typedef std::unordered_map
<Node
, Node
, NodeHashFunction
> NodeMap
;
2910 Node
SmtEnginePrivate::purifyNlTerms(TNode n
, NodeMap
& cache
, NodeMap
& bcache
, std::vector
< Node
>& var_eq
, bool beneathMult
) {
2912 NodeMap::iterator find
= bcache
.find(n
);
2913 if (find
!= bcache
.end()) {
2914 return (*find
).second
;
2917 NodeMap::iterator find
= cache
.find(n
);
2918 if (find
!= cache
.end()) {
2919 return (*find
).second
;
2923 if( n
.getNumChildren()>0 ){
2925 && (n
.getKind() == kind::PLUS
|| n
.getKind() == kind::MINUS
))
2927 // don't do it if it rewrites to a constant
2928 Node nr
= Rewriter::rewrite(n
);
2931 // return the rewritten constant
2937 ret
= NodeManager::currentNM()->mkSkolem(
2940 "Variable introduced in purifyNl pass");
2941 Node np
= purifyNlTerms(n
, cache
, bcache
, var_eq
, false);
2942 var_eq
.push_back(np
.eqNode(ret
));
2943 Trace("nl-ext-purify")
2944 << "Purify : " << ret
<< " -> " << np
<< std::endl
;
2949 bool beneathMultNew
= beneathMult
|| n
.getKind()==kind::MULT
;
2950 bool childChanged
= false;
2951 std::vector
< Node
> children
;
2952 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
2953 Node nc
= purifyNlTerms( n
[i
], cache
, bcache
, var_eq
, beneathMultNew
);
2954 childChanged
= childChanged
|| nc
!=n
[i
];
2955 children
.push_back( nc
);
2958 ret
= NodeManager::currentNM()->mkNode( n
.getKind(), children
);
2970 // do dumping (before/after any preprocessing pass)
2971 static void dumpAssertions(const char* key
,
2972 const AssertionPipeline
& assertionList
) {
2973 if( Dump
.isOn("assertions") &&
2974 Dump
.isOn(string("assertions:") + key
) ) {
2975 // Push the simplified assertions to the dump output stream
2976 for(unsigned i
= 0; i
< assertionList
.size(); ++ i
) {
2977 TNode n
= assertionList
[i
];
2978 Dump("assertions") << AssertCommand(Expr(n
.toExpr()));
2983 // returns false if it learns a conflict
2984 bool SmtEnginePrivate::nonClausalSimplify() {
2985 spendResource(options::preprocessStep());
2986 d_smt
.finalOptionsAreSet();
2988 if(options::unsatCores() || options::fewerPreprocessingHoles()) {
2992 TimerStat::CodeTimer
nonclausalTimer(d_smt
.d_stats
->d_nonclausalSimplificationTime
);
2994 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify()" << endl
;
2995 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
2996 Trace("simplify") << "Assertion #" << i
<< " : " << d_assertions
[i
] << std::endl
;
2999 if(d_propagatorNeedsFinish
) {
3000 d_propagator
.finish();
3001 d_propagatorNeedsFinish
= false;
3003 d_propagator
.initialize();
3005 // Assert all the assertions to the propagator
3006 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
3007 << "asserting to propagator" << endl
;
3008 CDO
<unsigned>& substs_index
= d_assertions
.getSubstitutionsIndex();
3009 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
3010 Assert(Rewriter::rewrite(d_assertions
[i
]) == d_assertions
[i
]);
3011 // Don't reprocess substitutions
3012 if (substs_index
> 0 && i
== substs_index
)
3016 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): asserting " << d_assertions
[i
] << endl
;
3017 Debug("cores") << "d_propagator assertTrue: " << d_assertions
[i
] << std::endl
;
3018 d_propagator
.assertTrue(d_assertions
[i
]);
3021 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
3022 << "propagating" << endl
;
3023 if (d_propagator
.propagate()) {
3024 // If in conflict, just return false
3025 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
3026 << "conflict in non-clausal propagation" << endl
;
3027 Node falseNode
= NodeManager::currentNM()->mkConst
<bool>(false);
3028 Assert(!options::unsatCores() && !options::fewerPreprocessingHoles());
3029 d_assertions
.clear();
3030 addFormula(falseNode
, false, false);
3031 d_propagatorNeedsFinish
= true;
3036 Trace("simplify") << "Iterate through " << d_nonClausalLearnedLiterals
.size() << " learned literals." << std::endl
;
3037 // No conflict, go through the literals and solve them
3038 SubstitutionMap
& top_level_substs
= d_assertions
.getTopLevelSubstitutions();
3039 SubstitutionMap
constantPropagations(d_smt
.d_context
);
3040 SubstitutionMap
newSubstitutions(d_smt
.d_context
);
3041 SubstitutionMap::iterator pos
;
3043 for(unsigned i
= 0, i_end
= d_nonClausalLearnedLiterals
.size(); i
< i_end
; ++ i
) {
3044 // Simplify the literal we learned wrt previous substitutions
3045 Node learnedLiteral
= d_nonClausalLearnedLiterals
[i
];
3046 Assert(Rewriter::rewrite(learnedLiteral
) == learnedLiteral
);
3047 Assert(top_level_substs
.apply(learnedLiteral
) == learnedLiteral
);
3048 Trace("simplify") << "Process learnedLiteral : " << learnedLiteral
<< std::endl
;
3049 Node learnedLiteralNew
= newSubstitutions
.apply(learnedLiteral
);
3050 if (learnedLiteral
!= learnedLiteralNew
) {
3051 learnedLiteral
= Rewriter::rewrite(learnedLiteralNew
);
3053 Trace("simplify") << "Process learnedLiteral, after newSubs : " << learnedLiteral
<< std::endl
;
3055 learnedLiteralNew
= constantPropagations
.apply(learnedLiteral
);
3056 if (learnedLiteralNew
== learnedLiteral
) {
3059 ++d_smt
.d_stats
->d_numConstantProps
;
3060 learnedLiteral
= Rewriter::rewrite(learnedLiteralNew
);
3062 Trace("simplify") << "Process learnedLiteral, after constProp : " << learnedLiteral
<< std::endl
;
3063 // It might just simplify to a constant
3064 if (learnedLiteral
.isConst()) {
3065 if (learnedLiteral
.getConst
<bool>()) {
3066 // If the learned literal simplifies to true, it's redundant
3069 // If the learned literal simplifies to false, we're in conflict
3070 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
3072 << d_nonClausalLearnedLiterals
[i
] << endl
;
3073 Assert(!options::unsatCores());
3074 d_assertions
.clear();
3075 addFormula(NodeManager::currentNM()->mkConst
<bool>(false), false, false);
3076 d_propagatorNeedsFinish
= true;
3081 // Solve it with the corresponding theory, possibly adding new
3082 // substitutions to newSubstitutions
3083 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
3084 << "solving " << learnedLiteral
<< endl
;
3086 Theory::PPAssertStatus solveStatus
=
3087 d_smt
.d_theoryEngine
->solve(learnedLiteral
, newSubstitutions
);
3089 switch (solveStatus
) {
3090 case Theory::PP_ASSERT_STATUS_SOLVED
: {
3091 // The literal should rewrite to true
3092 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
3093 << "solved " << learnedLiteral
<< endl
;
3094 Assert(Rewriter::rewrite(newSubstitutions
.apply(learnedLiteral
)).isConst());
3095 // vector<pair<Node, Node> > equations;
3096 // constantPropagations.simplifyLHS(top_level_substs, equations,
3097 // true); if (equations.empty()) {
3100 // Assert(equations[0].first.isConst() &&
3101 // equations[0].second.isConst() && equations[0].first !=
3102 // equations[0].second);
3103 // else fall through
3106 case Theory::PP_ASSERT_STATUS_CONFLICT
:
3107 // If in conflict, we return false
3108 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
3109 << "conflict while solving "
3110 << learnedLiteral
<< endl
;
3111 Assert(!options::unsatCores());
3112 d_assertions
.clear();
3113 addFormula(NodeManager::currentNM()->mkConst
<bool>(false), false, false);
3114 d_propagatorNeedsFinish
= true;
3117 if (d_doConstantProp
&& learnedLiteral
.getKind() == kind::EQUAL
&& (learnedLiteral
[0].isConst() || learnedLiteral
[1].isConst())) {
3118 // constant propagation
3121 if (learnedLiteral
[0].isConst()) {
3122 t
= learnedLiteral
[1];
3123 c
= learnedLiteral
[0];
3126 t
= learnedLiteral
[0];
3127 c
= learnedLiteral
[1];
3129 Assert(!t
.isConst());
3130 Assert(constantPropagations
.apply(t
) == t
);
3131 Assert(top_level_substs
.apply(t
) == t
);
3132 Assert(newSubstitutions
.apply(t
) == t
);
3133 constantPropagations
.addSubstitution(t
, c
);
3134 // vector<pair<Node,Node> > equations;
3135 // constantPropagations.simplifyLHS(t, c, equations, true);
3136 // if (!equations.empty()) {
3137 // Assert(equations[0].first.isConst() &&
3138 // equations[0].second.isConst() && equations[0].first !=
3139 // equations[0].second); d_assertions.clear();
3140 // addFormula(NodeManager::currentNM()->mkConst<bool>(false), false,
3143 // top_level_substs.simplifyRHS(constantPropagations);
3147 d_nonClausalLearnedLiterals
[j
++] = d_nonClausalLearnedLiterals
[i
];
3153 #ifdef CVC4_ASSERTIONS
3154 // NOTE: When debugging this code, consider moving this check inside of the
3155 // loop over d_nonClausalLearnedLiterals. This check has been moved outside
3156 // because it is costly for certain inputs (see bug 508).
3158 // Check data structure invariants:
3159 // 1. for each lhs of top_level_substs, does not appear anywhere in rhs of
3160 // top_level_substs or anywhere in constantPropagations
3161 // 2. each lhs of constantPropagations rewrites to itself
3162 // 3. if l -> r is a constant propagation and l is a subterm of l' with l' ->
3163 // r' another constant propagation, then l'[l/r] -> r' should be a
3164 // constant propagation too
3165 // 4. each lhs of constantPropagations is different from each rhs
3166 for (pos
= newSubstitutions
.begin(); pos
!= newSubstitutions
.end(); ++pos
) {
3167 Assert((*pos
).first
.isVar());
3168 Assert(top_level_substs
.apply((*pos
).first
) == (*pos
).first
);
3169 Assert(top_level_substs
.apply((*pos
).second
) == (*pos
).second
);
3170 Assert(newSubstitutions
.apply(newSubstitutions
.apply((*pos
).second
)) == newSubstitutions
.apply((*pos
).second
));
3172 for (pos
= constantPropagations
.begin(); pos
!= constantPropagations
.end(); ++pos
) {
3173 Assert((*pos
).second
.isConst());
3174 Assert(Rewriter::rewrite((*pos
).first
) == (*pos
).first
);
3175 // Node newLeft = top_level_substs.apply((*pos).first);
3176 // if (newLeft != (*pos).first) {
3177 // newLeft = Rewriter::rewrite(newLeft);
3178 // Assert(newLeft == (*pos).second ||
3179 // (constantPropagations.hasSubstitution(newLeft) &&
3180 // constantPropagations.apply(newLeft) == (*pos).second));
3182 // newLeft = constantPropagations.apply((*pos).first);
3183 // if (newLeft != (*pos).first) {
3184 // newLeft = Rewriter::rewrite(newLeft);
3185 // Assert(newLeft == (*pos).second ||
3186 // (constantPropagations.hasSubstitution(newLeft) &&
3187 // constantPropagations.apply(newLeft) == (*pos).second));
3189 Assert(constantPropagations
.apply((*pos
).second
) == (*pos
).second
);
3191 #endif /* CVC4_ASSERTIONS */
3193 // Resize the learnt
3194 Trace("simplify") << "Resize non-clausal learned literals to " << j
<< std::endl
;
3195 d_nonClausalLearnedLiterals
.resize(j
);
3197 unordered_set
<TNode
, TNodeHashFunction
> s
;
3198 Trace("debugging") << "NonClausal simplify pre-preprocess\n";
3199 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
3200 Node assertion
= d_assertions
[i
];
3201 Node assertionNew
= newSubstitutions
.apply(assertion
);
3202 Trace("debugging") << "assertion = " << assertion
<< endl
;
3203 Trace("debugging") << "assertionNew = " << assertionNew
<< endl
;
3204 if (assertion
!= assertionNew
) {
3205 assertion
= Rewriter::rewrite(assertionNew
);
3206 Trace("debugging") << "rewrite(assertion) = " << assertion
<< endl
;
3208 Assert(Rewriter::rewrite(assertion
) == assertion
);
3210 assertionNew
= constantPropagations
.apply(assertion
);
3211 if (assertionNew
== assertion
) {
3214 ++d_smt
.d_stats
->d_numConstantProps
;
3215 Trace("debugging") << "assertionNew = " << assertionNew
<< endl
;
3216 assertion
= Rewriter::rewrite(assertionNew
);
3217 Trace("debugging") << "assertionNew = " << assertionNew
<< endl
;
3219 Trace("debugging") << "\n";
3220 s
.insert(assertion
);
3221 d_assertions
.replace(i
, assertion
);
3222 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
3223 << "non-clausal preprocessed: "
3224 << assertion
<< endl
;
3227 // If in incremental mode, add substitutions to the list of assertions
3228 if (substs_index
> 0)
3230 NodeBuilder
<> substitutionsBuilder(kind::AND
);
3231 substitutionsBuilder
<< d_assertions
[substs_index
];
3232 pos
= newSubstitutions
.begin();
3233 for (; pos
!= newSubstitutions
.end(); ++pos
) {
3234 // Add back this substitution as an assertion
3235 TNode lhs
= (*pos
).first
, rhs
= newSubstitutions
.apply((*pos
).second
);
3236 Node n
= NodeManager::currentNM()->mkNode(kind::EQUAL
, lhs
, rhs
);
3237 substitutionsBuilder
<< n
;
3238 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): will notify SAT layer of substitution: " << n
<< endl
;
3240 if (substitutionsBuilder
.getNumChildren() > 1) {
3241 d_assertions
.replace(substs_index
,
3242 Rewriter::rewrite(Node(substitutionsBuilder
)));
3245 // If not in incremental mode, must add substitutions to model
3246 TheoryModel
* m
= d_smt
.d_theoryEngine
->getModel();
3248 for(pos
= newSubstitutions
.begin(); pos
!= newSubstitutions
.end(); ++pos
) {
3249 Node n
= (*pos
).first
;
3250 Node v
= newSubstitutions
.apply((*pos
).second
);
3251 Trace("model") << "Add substitution : " << n
<< " " << v
<< endl
;
3252 m
->addSubstitution( n
, v
);
3257 NodeBuilder
<> learnedBuilder(kind::AND
);
3258 Assert(d_assertions
.getRealAssertionsEnd() <= d_assertions
.size());
3259 learnedBuilder
<< d_assertions
[d_assertions
.getRealAssertionsEnd() - 1];
3261 for (unsigned i
= 0; i
< d_nonClausalLearnedLiterals
.size(); ++ i
) {
3262 Node learned
= d_nonClausalLearnedLiterals
[i
];
3263 Assert(top_level_substs
.apply(learned
) == learned
);
3264 Node learnedNew
= newSubstitutions
.apply(learned
);
3265 if (learned
!= learnedNew
) {
3266 learned
= Rewriter::rewrite(learnedNew
);
3268 Assert(Rewriter::rewrite(learned
) == learned
);
3270 learnedNew
= constantPropagations
.apply(learned
);
3271 if (learnedNew
== learned
) {
3274 ++d_smt
.d_stats
->d_numConstantProps
;
3275 learned
= Rewriter::rewrite(learnedNew
);
3277 if (s
.find(learned
) != s
.end()) {
3281 learnedBuilder
<< learned
;
3282 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
3283 << "non-clausal learned : "
3286 d_nonClausalLearnedLiterals
.clear();
3288 for (pos
= constantPropagations
.begin(); pos
!= constantPropagations
.end(); ++pos
) {
3289 Node cProp
= (*pos
).first
.eqNode((*pos
).second
);
3290 Assert(top_level_substs
.apply(cProp
) == cProp
);
3291 Node cPropNew
= newSubstitutions
.apply(cProp
);
3292 if (cProp
!= cPropNew
) {
3293 cProp
= Rewriter::rewrite(cPropNew
);
3294 Assert(Rewriter::rewrite(cProp
) == cProp
);
3296 if (s
.find(cProp
) != s
.end()) {
3300 learnedBuilder
<< cProp
;
3301 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
3302 << "non-clausal constant propagation : "
3306 // Add new substitutions to topLevelSubstitutions
3307 // Note that we don't have to keep rhs's in full solved form
3308 // because SubstitutionMap::apply does a fixed-point iteration when substituting
3309 top_level_substs
.addSubstitutions(newSubstitutions
);
3311 if(learnedBuilder
.getNumChildren() > 1) {
3312 d_assertions
.replace(d_assertions
.getRealAssertionsEnd() - 1,
3313 Rewriter::rewrite(Node(learnedBuilder
)));
3316 d_propagatorNeedsFinish
= true;
3320 bool SmtEnginePrivate::simpITE() {
3321 TimerStat::CodeTimer
simpITETimer(d_smt
.d_stats
->d_simpITETime
);
3323 spendResource(options::preprocessStep());
3325 Trace("simplify") << "SmtEnginePrivate::simpITE()" << endl
;
3327 unsigned numAssertionOnEntry
= d_assertions
.size();
3328 for (unsigned i
= 0; i
< d_assertions
.size(); ++i
) {
3329 spendResource(options::preprocessStep());
3330 Node result
= d_smt
.d_theoryEngine
->ppSimpITE(d_assertions
[i
]);
3331 d_assertions
.replace(i
, result
);
3332 if(result
.isConst() && !result
.getConst
<bool>()){
3336 bool result
= d_smt
.d_theoryEngine
->donePPSimpITE(d_assertions
.ref());
3337 if(numAssertionOnEntry
< d_assertions
.size()){
3338 compressBeforeRealAssertions(numAssertionOnEntry
);
3343 void SmtEnginePrivate::compressBeforeRealAssertions(size_t before
){
3344 size_t curr
= d_assertions
.size();
3345 if (before
>= curr
|| d_assertions
.getRealAssertionsEnd() <= 0
3346 || d_assertions
.getRealAssertionsEnd() >= curr
)
3352 // original: [0 ... d_assertions.getRealAssertionsEnd())
3354 // ites skolems [d_assertions.getRealAssertionsEnd(), before)
3356 // added [before, curr)
3358 Assert(0 < d_assertions
.getRealAssertionsEnd());
3359 Assert(d_assertions
.getRealAssertionsEnd() <= before
);
3360 Assert(before
< curr
);
3362 std::vector
<Node
> intoConjunction
;
3363 for(size_t i
= before
; i
<curr
; ++i
){
3364 intoConjunction
.push_back(d_assertions
[i
]);
3366 d_assertions
.resize(before
);
3367 size_t lastBeforeItes
= d_assertions
.getRealAssertionsEnd() - 1;
3368 intoConjunction
.push_back(d_assertions
[lastBeforeItes
]);
3369 Node newLast
= util::NaryBuilder::mkAssoc(kind::AND
, intoConjunction
);
3370 d_assertions
.replace(lastBeforeItes
, newLast
);
3371 Assert(d_assertions
.size() == before
);
3374 void SmtEnginePrivate::unconstrainedSimp() {
3375 TimerStat::CodeTimer
unconstrainedSimpTimer(d_smt
.d_stats
->d_unconstrainedSimpTime
);
3376 spendResource(options::preprocessStep());
3377 Trace("simplify") << "SmtEnginePrivate::unconstrainedSimp()" << endl
;
3378 d_smt
.d_theoryEngine
->ppUnconstrainedSimp(d_assertions
.ref());
3381 void SmtEnginePrivate::traceBackToAssertions(const std::vector
<Node
>& nodes
, std::vector
<TNode
>& assertions
) {
3382 const booleans::CircuitPropagator::BackEdgesMap
& backEdges
= d_propagator
.getBackEdges();
3383 for(vector
<Node
>::const_iterator i
= nodes
.begin(); i
!= nodes
.end(); ++i
) {
3384 booleans::CircuitPropagator::BackEdgesMap::const_iterator j
= backEdges
.find(*i
);
3385 // term must appear in map, otherwise how did we get here?!
3386 Assert(j
!= backEdges
.end());
3387 // if term maps to empty, that means it's a top-level assertion
3388 if(!(*j
).second
.empty()) {
3389 traceBackToAssertions((*j
).second
, assertions
);
3391 assertions
.push_back(*i
);
3396 size_t SmtEnginePrivate::removeFromConjunction(Node
& n
, const std::unordered_set
<unsigned long>& toRemove
) {
3397 Assert(n
.getKind() == kind::AND
);
3398 size_t removals
= 0;
3399 for(Node::iterator j
= n
.begin(); j
!= n
.end(); ++j
) {
3400 size_t subremovals
= 0;
3402 if(toRemove
.find(sub
.getId()) != toRemove
.end() ||
3403 (sub
.getKind() == kind::AND
&& (subremovals
= removeFromConjunction(sub
, toRemove
)) > 0)) {
3404 NodeBuilder
<> b(kind::AND
);
3405 b
.append(n
.begin(), j
);
3406 if(subremovals
> 0) {
3407 removals
+= subremovals
;
3412 for(++j
; j
!= n
.end(); ++j
) {
3413 if(toRemove
.find((*j
).getId()) != toRemove
.end()) {
3415 } else if((*j
).getKind() == kind::AND
) {
3417 if((subremovals
= removeFromConjunction(sub
, toRemove
)) > 0) {
3418 removals
+= subremovals
;
3427 if(b
.getNumChildren() == 0) {
3430 } else if(b
.getNumChildren() == 1) {
3436 n
= Rewriter::rewrite(n
);
3441 Assert(removals
== 0);
3445 void SmtEnginePrivate::doMiplibTrick() {
3446 Assert(d_assertions
.getRealAssertionsEnd() == d_assertions
.size());
3447 Assert(!options::incrementalSolving());
3449 const booleans::CircuitPropagator::BackEdgesMap
& backEdges
= d_propagator
.getBackEdges();
3450 unordered_set
<unsigned long> removeAssertions
;
3452 NodeManager
* nm
= NodeManager::currentNM();
3453 Node zero
= nm
->mkConst(Rational(0)), one
= nm
->mkConst(Rational(1));
3455 SubstitutionMap
& top_level_substs
= d_assertions
.getTopLevelSubstitutions();
3456 unordered_map
<TNode
, Node
, TNodeHashFunction
> intVars
;
3457 for(vector
<Node
>::const_iterator i
= d_boolVars
.begin(); i
!= d_boolVars
.end(); ++i
) {
3458 if(d_propagator
.isAssigned(*i
)) {
3459 Debug("miplib") << "ineligible: " << *i
<< " because assigned " << d_propagator
.getAssignment(*i
) << endl
;
3463 vector
<TNode
> assertions
;
3464 booleans::CircuitPropagator::BackEdgesMap::const_iterator j
= backEdges
.find(*i
);
3465 // if not in back edges map, the bool var is unconstrained, showing up in no assertions.
3466 // if maps to an empty vector, that means the bool var was asserted itself.
3467 if(j
!= backEdges
.end()) {
3468 if(!(*j
).second
.empty()) {
3469 traceBackToAssertions((*j
).second
, assertions
);
3471 assertions
.push_back(*i
);
3474 Debug("miplib") << "for " << *i
<< endl
;
3475 bool eligible
= true;
3476 map
<pair
<Node
, Node
>, uint64_t> marks
;
3477 map
<pair
<Node
, Node
>, vector
<Rational
> > coef
;
3478 map
<pair
<Node
, Node
>, vector
<Rational
> > checks
;
3479 map
<pair
<Node
, Node
>, vector
<TNode
> > asserts
;
3480 for(vector
<TNode
>::const_iterator j
= assertions
.begin(); j
!= assertions
.end(); ++j
) {
3481 Debug("miplib") << " found: " << *j
<< endl
;
3482 if((*j
).getKind() != kind::IMPLIES
) {
3484 Debug("miplib") << " -- INELIGIBLE -- (not =>)" << endl
;
3487 Node conj
= BooleanSimplification::simplify((*j
)[0]);
3488 if(conj
.getKind() == kind::AND
&& conj
.getNumChildren() > 6) {
3490 Debug("miplib") << " -- INELIGIBLE -- (N-ary /\\ too big)" << endl
;
3493 if(conj
.getKind() != kind::AND
&& !conj
.isVar() && !(conj
.getKind() == kind::NOT
&& conj
[0].isVar())) {
3495 Debug("miplib") << " -- INELIGIBLE -- (not /\\ or literal)" << endl
;
3498 if((*j
)[1].getKind() != kind::EQUAL
||
3499 !( ( (*j
)[1][0].isVar() &&
3500 (*j
)[1][1].getKind() == kind::CONST_RATIONAL
) ||
3501 ( (*j
)[1][0].getKind() == kind::CONST_RATIONAL
&&
3502 (*j
)[1][1].isVar() ) )) {
3504 Debug("miplib") << " -- INELIGIBLE -- (=> (and X X) X)" << endl
;
3507 if(conj
.getKind() == kind::AND
) {
3509 bool found_x
= false;
3510 map
<TNode
, bool> neg
;
3511 for(Node::iterator ii
= conj
.begin(); ii
!= conj
.end(); ++ii
) {
3513 posv
.push_back(*ii
);
3515 found_x
= found_x
|| *i
== *ii
;
3516 } else if((*ii
).getKind() == kind::NOT
&& (*ii
)[0].isVar()) {
3517 posv
.push_back((*ii
)[0]);
3518 neg
[(*ii
)[0]] = true;
3519 found_x
= found_x
|| *i
== (*ii
)[0];
3522 Debug("miplib") << " -- INELIGIBLE -- (non-var: " << *ii
<< ")" << endl
;
3525 if(d_propagator
.isAssigned(posv
.back())) {
3527 Debug("miplib") << " -- INELIGIBLE -- (" << posv
.back() << " asserted)" << endl
;
3536 Debug("miplib") << " --INELIGIBLE -- (couldn't find " << *i
<< " in conjunction)" << endl
;
3539 sort(posv
.begin(), posv
.end());
3540 const Node pos
= NodeManager::currentNM()->mkNode(kind::AND
, posv
);
3541 const TNode var
= ((*j
)[1][0].getKind() == kind::CONST_RATIONAL
) ? (*j
)[1][1] : (*j
)[1][0];
3542 const pair
<Node
, Node
> pos_var(pos
, var
);
3543 const Rational
& constant
= ((*j
)[1][0].getKind() == kind::CONST_RATIONAL
) ? (*j
)[1][0].getConst
<Rational
>() : (*j
)[1][1].getConst
<Rational
>();
3545 unsigned countneg
= 0, thepos
= 0;
3546 for(unsigned ii
= 0; ii
< pos
.getNumChildren(); ++ii
) {
3551 mark
|= (0x1 << ii
);
3554 if((marks
[pos_var
] & (1lu << mark
)) != 0) {
3556 Debug("miplib") << " -- INELIGIBLE -- (remarked)" << endl
;
3559 Debug("miplib") << "mark is " << mark
<< " -- " << (1lu << mark
) << endl
;
3560 marks
[pos_var
] |= (1lu << mark
);
3561 Debug("miplib") << "marks[" << pos
<< "," << var
<< "] now " << marks
[pos_var
] << endl
;
3562 if(countneg
== pos
.getNumChildren()) {
3565 Debug("miplib") << " -- INELIGIBLE -- (nonzero constant)" << endl
;
3568 } else if(countneg
== pos
.getNumChildren() - 1) {
3569 Assert(coef
[pos_var
].size() <= 6 && thepos
< 6);
3570 if(coef
[pos_var
].size() <= thepos
) {
3571 coef
[pos_var
].resize(thepos
+ 1);
3573 coef
[pos_var
][thepos
] = constant
;
3575 if(checks
[pos_var
].size() <= mark
) {
3576 checks
[pos_var
].resize(mark
+ 1);
3578 checks
[pos_var
][mark
] = constant
;
3580 asserts
[pos_var
].push_back(*j
);
3583 if(x
!= *i
&& x
!= (*i
).notNode()) {
3585 Debug("miplib") << " -- INELIGIBLE -- (x not present where I expect it)" << endl
;
3588 const bool xneg
= (x
.getKind() == kind::NOT
);
3589 x
= xneg
? x
[0] : x
;
3590 Debug("miplib") << " x:" << x
<< " " << xneg
<< endl
;
3591 const TNode var
= ((*j
)[1][0].getKind() == kind::CONST_RATIONAL
) ? (*j
)[1][1] : (*j
)[1][0];
3592 const pair
<Node
, Node
> x_var(x
, var
);
3593 const Rational
& constant
= ((*j
)[1][0].getKind() == kind::CONST_RATIONAL
) ? (*j
)[1][0].getConst
<Rational
>() : (*j
)[1][1].getConst
<Rational
>();
3594 unsigned mark
= (xneg
? 0 : 1);
3595 if((marks
[x_var
] & (1u << mark
)) != 0) {
3597 Debug("miplib") << " -- INELIGIBLE -- (remarked)" << endl
;
3600 marks
[x_var
] |= (1u << mark
);
3604 Debug("miplib") << " -- INELIGIBLE -- (nonzero constant)" << endl
;
3608 Assert(coef
[x_var
].size() <= 6);
3609 coef
[x_var
].resize(6);
3610 coef
[x_var
][0] = constant
;
3612 asserts
[x_var
].push_back(*j
);
3616 for(map
<pair
<Node
, Node
>, uint64_t>::const_iterator j
= marks
.begin(); j
!= marks
.end(); ++j
) {
3617 const TNode pos
= (*j
).first
.first
;
3618 const TNode var
= (*j
).first
.second
;
3619 const pair
<Node
, Node
>& pos_var
= (*j
).first
;
3620 const uint64_t mark
= (*j
).second
;
3621 const unsigned numVars
= pos
.getKind() == kind::AND
? pos
.getNumChildren() : 1;
3622 uint64_t expected
= (uint64_t(1) << (1 << numVars
)) - 1;
3623 expected
= (expected
== 0) ? -1 : expected
; // fix for overflow
3624 Debug("miplib") << "[" << pos
<< "] => " << hex
<< mark
<< " expect " << expected
<< dec
<< endl
;
3625 Assert(pos
.getKind() == kind::AND
|| pos
.isVar());
3626 if(mark
!= expected
) {
3627 Debug("miplib") << " -- INELIGIBLE " << pos
<< " -- (insufficiently marked, got " << mark
<< " for " << numVars
<< " vars, expected " << expected
<< endl
;
3629 if(mark
!= 3) { // exclude single-var case; nothing to check there
3630 uint64_t sz
= (uint64_t(1) << checks
[pos_var
].size()) - 1;
3631 sz
= (sz
== 0) ? -1 : sz
; // fix for overflow
3632 Assert(sz
== mark
, "expected size %u == mark %u", sz
, mark
);
3633 for(size_t k
= 0; k
< checks
[pos_var
].size(); ++k
) {
3634 if((k
& (k
- 1)) != 0) {
3636 Debug("miplib") << k
<< " => " << checks
[pos_var
][k
] << endl
;
3637 for(size_t v
= 1, kk
= k
; kk
!= 0; ++v
, kk
>>= 1) {
3638 if((kk
& 0x1) == 1) {
3639 Assert(pos
.getKind() == kind::AND
);
3640 Debug("miplib") << "var " << v
<< " : " << pos
[v
- 1] << " coef:" << coef
[pos_var
][v
- 1] << endl
;
3641 sum
+= coef
[pos_var
][v
- 1];
3644 Debug("miplib") << "checkSum is " << sum
<< " input says " << checks
[pos_var
][k
] << endl
;
3645 if(sum
!= checks
[pos_var
][k
]) {
3647 Debug("miplib") << " -- INELIGIBLE " << pos
<< " -- (nonlinear combination)" << endl
;
3651 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
3656 eligible
= true; // next is still eligible
3660 Debug("miplib") << " -- ELIGIBLE " << *i
<< " , " << pos
<< " --" << endl
;
3661 vector
<Node
> newVars
;
3662 expr::NodeSelfIterator ii
, iiend
;
3663 if(pos
.getKind() == kind::AND
) {
3667 ii
= expr::NodeSelfIterator::self(pos
);
3668 iiend
= expr::NodeSelfIterator::selfEnd(pos
);
3670 for(; ii
!= iiend
; ++ii
) {
3671 Node
& varRef
= intVars
[*ii
];
3672 if(varRef
.isNull()) {
3674 ss
<< "mipvar_" << *ii
;
3675 Node newVar
= nm
->mkSkolem(ss
.str(), nm
->integerType(), "a variable introduced due to scrubbing a miplib encoding", NodeManager::SKOLEM_EXACT_NAME
);
3676 Node geq
= Rewriter::rewrite(nm
->mkNode(kind::GEQ
, newVar
, zero
));
3677 Node leq
= Rewriter::rewrite(nm
->mkNode(kind::LEQ
, newVar
, one
));
3678 addFormula(Rewriter::rewrite(geq
.andNode(leq
)), false, false);
3679 SubstitutionMap
nullMap(&d_fakeContext
);
3680 Theory::PPAssertStatus status CVC4_UNUSED
; // just for assertions
3681 status
= d_smt
.d_theoryEngine
->solve(geq
, nullMap
);
3682 Assert(status
== Theory::PP_ASSERT_STATUS_UNSOLVED
,
3683 "unexpected solution from arith's ppAssert()");
3684 Assert(nullMap
.empty(),
3685 "unexpected substitution from arith's ppAssert()");
3686 status
= d_smt
.d_theoryEngine
->solve(leq
, nullMap
);
3687 Assert(status
== Theory::PP_ASSERT_STATUS_UNSOLVED
,
3688 "unexpected solution from arith's ppAssert()");
3689 Assert(nullMap
.empty(),
3690 "unexpected substitution from arith's ppAssert()");
3691 d_smt
.d_theoryEngine
->getModel()->addSubstitution(*ii
, newVar
.eqNode(one
));
3692 newVars
.push_back(newVar
);
3695 newVars
.push_back(varRef
);
3697 if(!d_smt
.d_logic
.areIntegersUsed()) {
3698 d_smt
.d_logic
= d_smt
.d_logic
.getUnlockedCopy();
3699 d_smt
.d_logic
.enableIntegers();
3700 d_smt
.d_logic
.lock();
3704 if(pos
.getKind() == kind::AND
) {
3705 NodeBuilder
<> sumb(kind::PLUS
);
3706 for(size_t ii
= 0; ii
< pos
.getNumChildren(); ++ii
) {
3707 sumb
<< nm
->mkNode(kind::MULT
, nm
->mkConst(coef
[pos_var
][ii
]), newVars
[ii
]);
3711 sum
= nm
->mkNode(kind::MULT
, nm
->mkConst(coef
[pos_var
][0]), newVars
[0]);
3713 Debug("miplib") << "vars[] " << var
<< endl
3714 << " eq " << Rewriter::rewrite(sum
) << endl
;
3715 Node newAssertion
= var
.eqNode(Rewriter::rewrite(sum
));
3716 if (top_level_substs
.hasSubstitution(newAssertion
[0]))
3718 // Warning() << "RE-SUBSTITUTION " << newAssertion[0] << endl;
3719 // Warning() << "REPLACE " << newAssertion[1] << endl;
3720 // Warning() << "ORIG " <<
3721 // top_level_substs.getSubstitution(newAssertion[0]) << endl;
3722 Assert(top_level_substs
.getSubstitution(newAssertion
[0])
3723 == newAssertion
[1]);
3724 } else if(pos
.getNumChildren() <= options::arithMLTrickSubstitutions()) {
3725 top_level_substs
.addSubstitution(newAssertion
[0], newAssertion
[1]);
3726 Debug("miplib") << "addSubs: " << newAssertion
[0] << " to " << newAssertion
[1] << endl
;
3728 Debug("miplib") << "skipSubs: " << newAssertion
[0] << " to " << newAssertion
[1] << " (threshold is " << options::arithMLTrickSubstitutions() << ")" << endl
;
3730 newAssertion
= Rewriter::rewrite(newAssertion
);
3731 Debug("miplib") << " " << newAssertion
<< endl
;
3732 addFormula(newAssertion
, false, false);
3733 Debug("miplib") << " assertions to remove: " << endl
;
3734 for(vector
<TNode
>::const_iterator k
= asserts
[pos_var
].begin(), k_end
= asserts
[pos_var
].end(); k
!= k_end
; ++k
) {
3735 Debug("miplib") << " " << *k
<< endl
;
3736 removeAssertions
.insert((*k
).getId());
3742 if(!removeAssertions
.empty()) {
3743 Debug("miplib") << "SmtEnginePrivate::simplify(): scrubbing miplib encoding..." << endl
;
3744 for (size_t i
= 0; i
< d_assertions
.getRealAssertionsEnd(); ++i
)
3746 if(removeAssertions
.find(d_assertions
[i
].getId()) != removeAssertions
.end()) {
3747 Debug("miplib") << "SmtEnginePrivate::simplify(): - removing " << d_assertions
[i
] << endl
;
3748 d_assertions
[i
] = d_true
;
3749 ++d_smt
.d_stats
->d_numMiplibAssertionsRemoved
;
3750 } else if(d_assertions
[i
].getKind() == kind::AND
) {
3751 size_t removals
= removeFromConjunction(d_assertions
[i
], removeAssertions
);
3753 Debug("miplib") << "SmtEnginePrivate::simplify(): - reduced " << d_assertions
[i
] << endl
;
3754 Debug("miplib") << "SmtEnginePrivate::simplify(): - by " << removals
<< " conjuncts" << endl
;
3755 d_smt
.d_stats
->d_numMiplibAssertionsRemoved
+= removals
;
3758 Debug("miplib") << "had: " << d_assertions
[i
] << endl
;
3760 Rewriter::rewrite(top_level_substs
.apply(d_assertions
[i
]));
3761 Debug("miplib") << "now: " << d_assertions
[i
] << endl
;
3764 Debug("miplib") << "SmtEnginePrivate::simplify(): miplib pass found nothing." << endl
;
3766 d_assertions
.updateRealAssertionsEnd();
3770 // returns false if simplification led to "false"
3771 bool SmtEnginePrivate::simplifyAssertions()
3773 spendResource(options::preprocessStep());
3774 Assert(d_smt
.d_pendingPops
== 0);
3776 ScopeCounter
depth(d_simplifyAssertionsDepth
);
3778 Trace("simplify") << "SmtEnginePrivate::simplify()" << endl
;
3780 dumpAssertions("pre-nonclausal", d_assertions
);
3782 if(options::simplificationMode() != SIMPLIFICATION_MODE_NONE
) {
3783 // Perform non-clausal simplification
3784 Chat() << "...performing nonclausal simplification..." << endl
;
3785 Trace("simplify") << "SmtEnginePrivate::simplify(): "
3786 << "performing non-clausal simplification" << endl
;
3787 bool noConflict
= nonClausalSimplify();
3792 // We piggy-back off of the BackEdgesMap in the CircuitPropagator to
3793 // do the miplib trick.
3794 if ( // check that option is on
3795 options::arithMLTrick() &&
3796 // miplib rewrites aren't safe in incremental mode
3797 !options::incrementalSolving() &&
3798 // only useful in arith
3799 d_smt
.d_logic
.isTheoryEnabled(THEORY_ARITH
) &&
3800 // we add new assertions and need this (in practice, this
3801 // restriction only disables miplib processing during
3802 // re-simplification, which we don't expect to be useful anyway)
3803 d_assertions
.getRealAssertionsEnd() == d_assertions
.size())
3805 Chat() << "...fixing miplib encodings..." << endl
;
3806 Trace("simplify") << "SmtEnginePrivate::simplify(): "
3807 << "looking for miplib pseudobooleans..." << endl
;
3809 TimerStat::CodeTimer
miplibTimer(d_smt
.d_stats
->d_miplibPassTime
);
3813 Trace("simplify") << "SmtEnginePrivate::simplify(): "
3814 << "skipping miplib pseudobooleans pass (either incrementalSolving is on, or miplib pbs are turned off)..." << endl
;
3818 dumpAssertions("post-nonclausal", d_assertions
);
3819 Trace("smt") << "POST nonClausalSimplify" << endl
;
3820 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
3822 // before ppRewrite check if only core theory for BV theory
3823 d_smt
.d_theoryEngine
->staticInitializeBVOptions(d_assertions
.ref());
3825 dumpAssertions("pre-theorypp", d_assertions
);
3827 // Theory preprocessing
3828 if (d_smt
.d_earlyTheoryPP
) {
3829 Chat() << "...doing early theory preprocessing..." << endl
;
3830 TimerStat::CodeTimer
codeTimer(d_smt
.d_stats
->d_theoryPreprocessTime
);
3831 // Call the theory preprocessors
3832 d_smt
.d_theoryEngine
->preprocessStart();
3833 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
3834 Assert(Rewriter::rewrite(d_assertions
[i
]) == d_assertions
[i
]);
3835 d_assertions
.replace(i
, d_smt
.d_theoryEngine
->preprocess(d_assertions
[i
]));
3836 Assert(Rewriter::rewrite(d_assertions
[i
]) == d_assertions
[i
]);
3840 dumpAssertions("post-theorypp", d_assertions
);
3841 Trace("smt") << "POST theoryPP" << endl
;
3842 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
3844 // ITE simplification
3845 if(options::doITESimp() &&
3846 (d_simplifyAssertionsDepth
<= 1 || options::doITESimpOnRepeat())) {
3847 Chat() << "...doing ITE simplification..." << endl
;
3848 bool noConflict
= simpITE();
3850 Chat() << "...ITE simplification found unsat..." << endl
;
3855 dumpAssertions("post-itesimp", d_assertions
);
3856 Trace("smt") << "POST iteSimp" << endl
;
3857 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
3859 // Unconstrained simplification
3860 if(options::unconstrainedSimp()) {
3861 Chat() << "...doing unconstrained simplification..." << endl
;
3862 unconstrainedSimp();
3865 dumpAssertions("post-unconstrained", d_assertions
);
3866 Trace("smt") << "POST unconstrainedSimp" << endl
;
3867 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
3869 if(options::repeatSimp() && options::simplificationMode() != SIMPLIFICATION_MODE_NONE
) {
3870 Chat() << "...doing another round of nonclausal simplification..." << endl
;
3871 Trace("simplify") << "SmtEnginePrivate::simplify(): "
3872 << " doing repeated simplification" << endl
;
3873 bool noConflict
= nonClausalSimplify();
3879 dumpAssertions("post-repeatsimp", d_assertions
);
3880 Trace("smt") << "POST repeatSimp" << endl
;
3881 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
3883 } catch(TypeCheckingExceptionPrivate
& tcep
) {
3884 // Calls to this function should have already weeded out any
3885 // typechecking exceptions via (e.g.) ensureBoolean(). But a
3886 // theory could still create a new expression that isn't
3887 // well-typed, and we don't want the C++ runtime to abort our
3888 // process without any error notice.
3890 ss
<< "A bad expression was produced. Original exception follows:\n"
3892 InternalError(ss
.str().c_str());
3897 Result
SmtEngine::check() {
3898 Assert(d_fullyInited
);
3899 Assert(d_pendingPops
== 0);
3901 Trace("smt") << "SmtEngine::check()" << endl
;
3903 ResourceManager
* resourceManager
= d_private
->getResourceManager();
3905 resourceManager
->beginCall();
3907 // Only way we can be out of resource is if cumulative budget is on
3908 if (resourceManager
->cumulativeLimitOn() &&
3909 resourceManager
->out()) {
3910 Result::UnknownExplanation why
= resourceManager
->outOfResources() ?
3911 Result::RESOURCEOUT
: Result::TIMEOUT
;
3912 return Result(Result::VALIDITY_UNKNOWN
, why
, d_filename
);
3915 // Make sure the prop layer has all of the assertions
3916 Trace("smt") << "SmtEngine::check(): processing assertions" << endl
;
3917 d_private
->processAssertions();
3918 Trace("smt") << "SmtEngine::check(): done processing assertions" << endl
;
3920 // Turn off stop only for QF_LRA
3921 // TODO: Bring up in a meeting where to put this
3922 if(options::decisionStopOnly() && !options::decisionMode
.wasSetByUser() ){
3924 (not d_logic
.isQuantified() &&
3925 d_logic
.isPure(THEORY_ARITH
) && d_logic
.isLinear() && !d_logic
.isDifferenceLogic() && !d_logic
.areIntegersUsed()
3927 if (d_private
->getIteSkolemMap().empty())
3929 options::decisionStopOnly
.set(false);
3930 d_decisionEngine
->clearStrategies();
3931 Trace("smt") << "SmtEngine::check(): turning off stop only" << endl
;
3936 TimerStat::CodeTimer
solveTimer(d_stats
->d_solveTime
);
3938 Chat() << "solving..." << endl
;
3939 Trace("smt") << "SmtEngine::check(): running check" << endl
;
3940 Result result
= d_propEngine
->checkSat();
3942 resourceManager
->endCall();
3943 Trace("limit") << "SmtEngine::check(): cumulative millis " << resourceManager
->getTimeUsage()
3944 << ", resources " << resourceManager
->getResourceUsage() << endl
;
3947 return Result(result
, d_filename
);
3950 Result
SmtEngine::quickCheck() {
3951 Assert(d_fullyInited
);
3952 Trace("smt") << "SMT quickCheck()" << endl
;
3953 return Result(Result::VALIDITY_UNKNOWN
, Result::REQUIRES_FULL_CHECK
, d_filename
);
3957 void SmtEnginePrivate::collectSkolems(TNode n
, set
<TNode
>& skolemSet
, unordered_map
<Node
, bool, NodeHashFunction
>& cache
)
3959 unordered_map
<Node
, bool, NodeHashFunction
>::iterator it
;
3961 if (it
!= cache
.end()) {
3965 size_t sz
= n
.getNumChildren();
3967 IteSkolemMap::iterator it
= getIteSkolemMap().find(n
);
3968 if (it
!= getIteSkolemMap().end())
3970 skolemSet
.insert(n
);
3977 for (; k
< sz
; ++k
) {
3978 collectSkolems(n
[k
], skolemSet
, cache
);
3984 bool SmtEnginePrivate::checkForBadSkolems(TNode n
, TNode skolem
, unordered_map
<Node
, bool, NodeHashFunction
>& cache
)
3986 unordered_map
<Node
, bool, NodeHashFunction
>::iterator it
;
3988 if (it
!= cache
.end()) {
3989 return (*it
).second
;
3992 size_t sz
= n
.getNumChildren();
3994 IteSkolemMap::iterator it
= getIteSkolemMap().find(n
);
3996 if (it
!= getIteSkolemMap().end())
3998 if (!((*it
).first
< n
)) {
4007 for (; k
< sz
; ++k
) {
4008 if (checkForBadSkolems(n
[k
], skolem
, cache
)) {
4018 void SmtEnginePrivate::processAssertions() {
4019 TimerStat::CodeTimer
paTimer(d_smt
.d_stats
->d_processAssertionsTime
);
4020 spendResource(options::preprocessStep());
4021 Assert(d_smt
.d_fullyInited
);
4022 Assert(d_smt
.d_pendingPops
== 0);
4023 SubstitutionMap
& top_level_substs
= d_assertions
.getTopLevelSubstitutions();
4025 // Dump the assertions
4026 dumpAssertions("pre-everything", d_assertions
);
4028 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() begin" << endl
;
4029 Trace("smt") << "SmtEnginePrivate::processAssertions()" << endl
;
4031 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
4033 if (d_assertions
.size() == 0) {
4038 if (options::bvGaussElim())
4040 d_preprocessingPassRegistry
.getPass("bv-gauss")->apply(&d_assertions
);
4043 if (d_assertionsProcessed
&& options::incrementalSolving()) {
4044 // TODO(b/1255): Substitutions in incremental mode should be managed with a
4045 // proper data structure.
4047 // Placeholder for storing substitutions
4048 d_assertions
.getSubstitutionsIndex() = d_assertions
.size();
4049 d_assertions
.push_back(NodeManager::currentNM()->mkConst
<bool>(true));
4052 // Add dummy assertion in last position - to be used as a
4053 // placeholder for any new assertions to get added
4054 d_assertions
.push_back(NodeManager::currentNM()->mkConst
<bool>(true));
4055 // any assertions added beyond realAssertionsEnd must NOT affect the
4056 // equisatisfiability
4057 d_assertions
.updateRealAssertionsEnd();
4059 // Assertions are NOT guaranteed to be rewritten by this point
4061 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-definition-expansion" << endl
;
4062 dumpAssertions("pre-definition-expansion", d_assertions
);
4064 Chat() << "expanding definitions..." << endl
;
4065 Trace("simplify") << "SmtEnginePrivate::simplify(): expanding definitions" << endl
;
4066 TimerStat::CodeTimer
codeTimer(d_smt
.d_stats
->d_definitionExpansionTime
);
4067 unordered_map
<Node
, Node
, NodeHashFunction
> cache
;
4068 for(unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
4069 d_assertions
.replace(i
, expandDefinitions(d_assertions
[i
], cache
));
4072 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-definition-expansion" << endl
;
4073 dumpAssertions("post-definition-expansion", d_assertions
);
4075 // save the assertions now
4078 for (unsigned i
= 0; i
< d_assertions
.size(); ++i
) {
4079 ProofManager::currentPM()->addAssertion(d_assertions
[i
].toExpr());
4083 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
4085 if (options::globalNegate())
4087 // global negation of the formula
4088 quantifiers::GlobalNegate gn
;
4089 gn
.simplify(d_assertions
.ref());
4090 d_smt
.d_globalNegation
= !d_smt
.d_globalNegation
;
4093 if( options::nlExtPurify() ){
4094 unordered_map
<Node
, Node
, NodeHashFunction
> cache
;
4095 unordered_map
<Node
, Node
, NodeHashFunction
> bcache
;
4096 std::vector
< Node
> var_eq
;
4097 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
4098 Node a
= d_assertions
[i
];
4099 d_assertions
.replace(i
, purifyNlTerms(a
, cache
, bcache
, var_eq
));
4100 Trace("nl-ext-purify")
4101 << "Purify : " << a
<< " -> " << d_assertions
[i
] << std::endl
;
4103 if( !var_eq
.empty() ){
4104 unsigned lastIndex
= d_assertions
.size()-1;
4105 var_eq
.insert( var_eq
.begin(), d_assertions
[lastIndex
] );
4106 d_assertions
.replace(lastIndex
, NodeManager::currentNM()->mkNode( kind::AND
, var_eq
) );
4110 if( options::ceGuidedInst() ){
4111 //register sygus conjecture pre-rewrite (motivated by solution reconstruction)
4112 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
4113 d_smt
.d_theoryEngine
->getQuantifiersEngine()->getCegInstantiation()->preregisterAssertion( d_assertions
[i
] );
4117 if (options::solveRealAsInt()) {
4118 d_preprocessingPassRegistry
.getPass("real-to-int")->apply(&d_assertions
);
4121 if (options::solveIntAsBV() > 0)
4123 d_preprocessingPassRegistry
.getPass("int-to-bv")->apply(&d_assertions
);
4126 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
&&
4127 !d_smt
.d_logic
.isPure(THEORY_BV
) &&
4128 d_smt
.d_logic
.getLogicString() != "QF_UFBV" &&
4129 d_smt
.d_logic
.getLogicString() != "QF_ABV") {
4130 throw ModalException("Eager bit-blasting does not currently support theory combination. "
4131 "Note that in a QF_BV problem UF symbols can be introduced for division. "
4132 "Try --bv-div-zero-const to interpret division by zero as a constant.");
4135 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
4136 && !options::incrementalSolving())
4138 d_preprocessingPassRegistry
.getPass("bv-ackermann")->apply(&d_assertions
);
4141 if (options::bvAbstraction() && !options::incrementalSolving())
4143 d_preprocessingPassRegistry
.getPass("bv-abstraction")->apply(&d_assertions
);
4146 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
4148 bool noConflict
= true;
4150 if (options::extRewPrep())
4152 d_preprocessingPassRegistry
.getPass("ext-rew-pre")->apply(&d_assertions
);
4155 // Unconstrained simplification
4156 if(options::unconstrainedSimp()) {
4157 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-unconstrained-simp" << endl
;
4158 dumpAssertions("pre-unconstrained-simp", d_assertions
);
4159 d_preprocessingPassRegistry
.getPass("rewrite")->apply(&d_assertions
);
4160 unconstrainedSimp();
4161 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-unconstrained-simp" << endl
;
4162 dumpAssertions("post-unconstrained-simp", d_assertions
);
4165 if(options::bvIntroducePow2())
4167 d_preprocessingPassRegistry
.getPass("bv-intro-pow2")->apply(&d_assertions
);
4170 if (options::unsatCores())
4172 // special rewriting pass for unsat cores, since many of the passes below
4174 d_preprocessingPassRegistry
.getPass("rewrite")->apply(&d_assertions
);
4178 d_preprocessingPassRegistry
.getPass("apply-substs")->apply(&d_assertions
);
4181 // Assertions ARE guaranteed to be rewritten by this point
4182 #ifdef CVC4_ASSERTIONS
4183 for (unsigned i
= 0; i
< d_assertions
.size(); ++i
)
4185 Assert(Rewriter::rewrite(d_assertions
[i
]) == d_assertions
[i
]);
4189 // Lift bit-vectors of size 1 to bool
4190 if (options::bitvectorToBool())
4192 d_preprocessingPassRegistry
.getPass("bv-to-bool")->apply(&d_assertions
);
4194 // Convert non-top-level Booleans to bit-vectors of size 1
4195 if (options::boolToBitvector())
4197 d_preprocessingPassRegistry
.getPass("bool-to-bv")->apply(&d_assertions
);
4199 if(options::sepPreSkolemEmp()) {
4200 d_preprocessingPassRegistry
.getPass("sep-skolem-emp")->apply(&d_assertions
);
4203 if( d_smt
.d_logic
.isQuantified() ){
4204 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-quant-preprocess" << endl
;
4206 dumpAssertions("pre-skolem-quant", d_assertions
);
4207 //remove rewrite rules, apply pre-skolemization to existential quantifiers
4208 d_preprocessingPassRegistry
.getPass("quantifiers-preprocess")
4209 ->apply(&d_assertions
);
4210 dumpAssertions("post-skolem-quant", d_assertions
);
4211 if( options::macrosQuant() ){
4212 //quantifiers macro expansion
4213 quantifiers::QuantifierMacros
qm( d_smt
.d_theoryEngine
->getQuantifiersEngine() );
4216 success
= qm
.simplify( d_assertions
.ref(), true );
4218 //finalize the definitions
4219 qm
.finalizeDefinitions();
4222 //fmf-fun : assume admissible functions, applying preprocessing reduction to FMF
4223 if( options::fmfFunWellDefined() ){
4224 quantifiers::FunDefFmf fdf
;
4225 Assert( d_smt
.d_fmfRecFunctionsDefined
!=NULL
);
4226 //must carry over current definitions (for incremental)
4227 for( context::CDList
<Node
>::const_iterator fit
= d_smt
.d_fmfRecFunctionsDefined
->begin();
4228 fit
!= d_smt
.d_fmfRecFunctionsDefined
->end(); ++fit
) {
4230 Assert( d_smt
.d_fmfRecFunctionsAbs
.find( f
)!=d_smt
.d_fmfRecFunctionsAbs
.end() );
4231 TypeNode ft
= d_smt
.d_fmfRecFunctionsAbs
[f
];
4232 fdf
.d_sorts
[f
] = ft
;
4233 std::map
< Node
, std::vector
< Node
> >::iterator fcit
= d_smt
.d_fmfRecFunctionsConcrete
.find( f
);
4234 Assert( fcit
!=d_smt
.d_fmfRecFunctionsConcrete
.end() );
4235 for( unsigned j
=0; j
<fcit
->second
.size(); j
++ ){
4236 fdf
.d_input_arg_inj
[f
].push_back( fcit
->second
[j
] );
4239 fdf
.simplify( d_assertions
.ref() );
4240 //must store new definitions (for incremental)
4241 for( unsigned i
=0; i
<fdf
.d_funcs
.size(); i
++ ){
4242 Node f
= fdf
.d_funcs
[i
];
4243 d_smt
.d_fmfRecFunctionsAbs
[f
] = fdf
.d_sorts
[f
];
4244 d_smt
.d_fmfRecFunctionsConcrete
[f
].clear();
4245 for( unsigned j
=0; j
<fdf
.d_input_arg_inj
[f
].size(); j
++ ){
4246 d_smt
.d_fmfRecFunctionsConcrete
[f
].push_back( fdf
.d_input_arg_inj
[f
][j
] );
4248 d_smt
.d_fmfRecFunctionsDefined
->push_back( f
);
4251 if (options::sygusInference())
4253 d_preprocessingPassRegistry
.getPass("sygus-infer")->apply(&d_assertions
);
4255 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-quant-preprocess" << endl
;
4258 if( options::sortInference() || options::ufssFairnessMonotone() ){
4259 d_preprocessingPassRegistry
.getPass("sort-inference")->apply(&d_assertions
);
4262 if( options::pbRewrites() ){
4263 d_preprocessingPassRegistry
.getPass("pseudo-boolean-processor")
4264 ->apply(&d_assertions
);
4267 if (options::synthRrPrep())
4269 // do candidate rewrite rule synthesis
4270 d_preprocessingPassRegistry
.getPass("synth-rr")->apply(&d_assertions
);
4273 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-simplify" << endl
;
4274 dumpAssertions("pre-simplify", d_assertions
);
4275 Chat() << "simplifying assertions..." << endl
;
4276 noConflict
= simplifyAssertions();
4278 ++(d_smt
.d_stats
->d_simplifiedToFalse
);
4280 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-simplify" << endl
;
4281 dumpAssertions("post-simplify", d_assertions
);
4283 if (options::symmetryBreakerExp() && !options::incrementalSolving())
4285 // apply symmetry breaking if not in incremental mode
4286 d_preprocessingPassRegistry
.getPass("sym-break")->apply(&d_assertions
);
4289 if(options::doStaticLearning()) {
4290 d_preprocessingPassRegistry
.getPass("static-learning")
4291 ->apply(&d_assertions
);
4293 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
4296 d_smt
.d_stats
->d_numAssertionsPre
+= d_assertions
.size();
4297 d_preprocessingPassRegistry
.getPass("ite-removal")->apply(&d_assertions
);
4298 // This is needed because when solving incrementally, removeITEs may introduce
4299 // skolems that were solved for earlier and thus appear in the substitution
4301 d_preprocessingPassRegistry
.getPass("apply-substs")->apply(&d_assertions
);
4302 d_smt
.d_stats
->d_numAssertionsPost
+= d_assertions
.size();
4305 dumpAssertions("pre-repeat-simplify", d_assertions
);
4306 if(options::repeatSimp()) {
4307 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-repeat-simplify" << endl
;
4308 Chat() << "re-simplifying assertions..." << endl
;
4309 ScopeCounter
depth(d_simplifyAssertionsDepth
);
4310 noConflict
&= simplifyAssertions();
4312 // Need to fix up assertion list to maintain invariants:
4313 // Let Sk be the set of Skolem variables introduced by ITE's. Let <_sk be the order in which these variables were introduced
4314 // during ite removal.
4315 // For each skolem variable sk, let iteExpr = iteMap(sk) be the ite expr mapped to by sk.
4317 // cache for expression traversal
4318 unordered_map
<Node
, bool, NodeHashFunction
> cache
;
4320 // First, find all skolems that appear in the substitution map - their associated iteExpr will need
4321 // to be moved to the main assertion set
4322 set
<TNode
> skolemSet
;
4323 SubstitutionMap::iterator pos
= top_level_substs
.begin();
4324 for (; pos
!= top_level_substs
.end(); ++pos
)
4326 collectSkolems((*pos
).first
, skolemSet
, cache
);
4327 collectSkolems((*pos
).second
, skolemSet
, cache
);
4330 // We need to ensure:
4331 // 1. iteExpr has the form (ite cond (sk = t) (sk = e))
4332 // 2. if some sk' in Sk appears in cond, t, or e, then sk' <_sk sk
4333 // If either of these is violated, we must add iteExpr as a proper assertion
4334 IteSkolemMap::iterator it
= getIteSkolemMap().begin();
4335 IteSkolemMap::iterator iend
= getIteSkolemMap().end();
4336 NodeBuilder
<> builder(kind::AND
);
4337 builder
<< d_assertions
[d_assertions
.getRealAssertionsEnd() - 1];
4338 vector
<TNode
> toErase
;
4339 for (; it
!= iend
; ++it
) {
4340 if (skolemSet
.find((*it
).first
) == skolemSet
.end()) {
4341 TNode iteExpr
= d_assertions
[(*it
).second
];
4342 if (iteExpr
.getKind() == kind::ITE
&&
4343 iteExpr
[1].getKind() == kind::EQUAL
&&
4344 iteExpr
[1][0] == (*it
).first
&&
4345 iteExpr
[2].getKind() == kind::EQUAL
&&
4346 iteExpr
[2][0] == (*it
).first
) {
4348 bool bad
= checkForBadSkolems(iteExpr
[0], (*it
).first
, cache
);
4349 bad
= bad
|| checkForBadSkolems(iteExpr
[1][1], (*it
).first
, cache
);
4350 bad
= bad
|| checkForBadSkolems(iteExpr
[2][1], (*it
).first
, cache
);
4356 // Move this iteExpr into the main assertions
4357 builder
<< d_assertions
[(*it
).second
];
4358 d_assertions
[(*it
).second
] = NodeManager::currentNM()->mkConst
<bool>(true);
4359 toErase
.push_back((*it
).first
);
4361 if(builder
.getNumChildren() > 1) {
4362 while (!toErase
.empty()) {
4363 getIteSkolemMap().erase(toErase
.back());
4366 d_assertions
[d_assertions
.getRealAssertionsEnd() - 1] =
4367 Rewriter::rewrite(Node(builder
));
4369 // TODO(b/1256): For some reason this is needed for some benchmarks, such as
4370 // QF_AUFBV/dwp_formulas/try5_small_difret_functions_dwp_tac.re_node_set_remove_at.il.dwp.smt2
4371 d_preprocessingPassRegistry
.getPass("ite-removal")->apply(&d_assertions
);
4372 d_preprocessingPassRegistry
.getPass("apply-substs")->apply(&d_assertions
);
4373 // Assert(iteRewriteAssertionsEnd == d_assertions.size());
4375 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-repeat-simplify" << endl
;
4377 dumpAssertions("post-repeat-simplify", d_assertions
);
4379 if (options::rewriteApplyToConst())
4381 d_preprocessingPassRegistry
.getPass("apply-to-const")->apply(&d_assertions
);
4384 // begin: INVARIANT to maintain: no reordering of assertions or
4385 // introducing new ones
4386 #ifdef CVC4_ASSERTIONS
4387 unsigned iteRewriteAssertionsEnd
= d_assertions
.size();
4390 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
4392 Debug("smt") << "SmtEnginePrivate::processAssertions() POST SIMPLIFICATION" << endl
;
4393 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
4395 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-theory-preprocessing" << endl
;
4396 dumpAssertions("pre-theory-preprocessing", d_assertions
);
4398 Chat() << "theory preprocessing..." << endl
;
4399 TimerStat::CodeTimer
codeTimer(d_smt
.d_stats
->d_theoryPreprocessTime
);
4400 // Call the theory preprocessors
4401 d_smt
.d_theoryEngine
->preprocessStart();
4402 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
4403 d_assertions
.replace(i
, d_smt
.d_theoryEngine
->preprocess(d_assertions
[i
]));
4406 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-theory-preprocessing" << endl
;
4407 dumpAssertions("post-theory-preprocessing", d_assertions
);
4409 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
)
4411 d_preprocessingPassRegistry
.getPass("bv-eager-atoms")->apply(&d_assertions
);
4414 //notify theory engine new preprocessed assertions
4415 d_smt
.d_theoryEngine
->notifyPreprocessedAssertions( d_assertions
.ref() );
4417 // Push the formula to decision engine
4419 Chat() << "pushing to decision engine..." << endl
;
4420 Assert(iteRewriteAssertionsEnd
== d_assertions
.size());
4421 d_smt
.d_decisionEngine
->addAssertions(d_assertions
.ref(),
4422 d_assertions
.getRealAssertionsEnd(),
4426 // end: INVARIANT to maintain: no reordering of assertions or
4427 // introducing new ones
4429 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() end" << endl
;
4430 dumpAssertions("post-everything", d_assertions
);
4432 // Push the formula to SAT
4434 Chat() << "converting to CNF..." << endl
;
4435 TimerStat::CodeTimer
codeTimer(d_smt
.d_stats
->d_cnfConversionTime
);
4436 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
4437 Chat() << "+ " << d_assertions
[i
] << std::endl
;
4438 d_smt
.d_propEngine
->assertFormula(d_assertions
[i
]);
4442 d_assertionsProcessed
= true;
4444 d_assertions
.clear();
4445 getIteSkolemMap().clear();
4448 void SmtEnginePrivate::addFormula(TNode n
, bool inUnsatCore
, bool inInput
)
4455 Trace("smt") << "SmtEnginePrivate::addFormula(" << n
<< "), inUnsatCore = " << inUnsatCore
<< ", inInput = " << inInput
<< endl
;
4457 // Give it to proof manager
4460 // n is an input assertion
4461 if (inUnsatCore
|| options::unsatCores() || options::dumpUnsatCores() || options::checkUnsatCores() || options::fewerPreprocessingHoles()) {
4463 ProofManager::currentPM()->addCoreAssertion(n
.toExpr());
4466 // n is the result of an unknown preprocessing step, add it to dependency map to null
4467 ProofManager::currentPM()->addDependence(n
, Node::null());
4469 // rewrite rules are by default in the unsat core because
4470 // they need to be applied until saturation
4471 if(options::unsatCores() &&
4472 n
.getKind() == kind::REWRITE_RULE
){
4473 ProofManager::currentPM()->addUnsatCore(n
.toExpr());
4477 // Add the normalized formula to the queue
4478 d_assertions
.push_back(n
);
4479 //d_assertions.push_back(Rewriter::rewrite(n));
4482 void SmtEngine::ensureBoolean(const Expr
& e
)
4484 Type type
= e
.getType(options::typeChecking());
4485 Type boolType
= d_exprManager
->booleanType();
4486 if(type
!= boolType
) {
4488 ss
<< "Expected " << boolType
<< "\n"
4489 << "The assertion : " << e
<< "\n"
4490 << "Its type : " << type
;
4491 throw TypeCheckingException(e
, ss
.str());
4495 Result
SmtEngine::checkSat(const Expr
& assumption
, bool inUnsatCore
)
4497 return checkSatisfiability(assumption
, inUnsatCore
, false);
4500 Result
SmtEngine::checkSat(const vector
<Expr
>& assumptions
, bool inUnsatCore
)
4502 return checkSatisfiability(assumptions
, inUnsatCore
, false);
4505 Result
SmtEngine::query(const Expr
& assumption
, bool inUnsatCore
)
4507 Assert(!assumption
.isNull());
4508 return checkSatisfiability(assumption
, inUnsatCore
, true);
4511 Result
SmtEngine::query(const vector
<Expr
>& assumptions
, bool inUnsatCore
)
4513 return checkSatisfiability(assumptions
, inUnsatCore
, true);
4516 Result
SmtEngine::checkSatisfiability(const Expr
& expr
,
4520 return checkSatisfiability(
4521 expr
.isNull() ? vector
<Expr
>() : vector
<Expr
>{expr
},
4526 Result
SmtEngine::checkSatisfiability(const vector
<Expr
>& assumptions
,
4532 SmtScope
smts(this);
4533 finalOptionsAreSet();
4536 Trace("smt") << "SmtEngine::" << (isQuery
? "query" : "checkSat") << "("
4537 << assumptions
<< ")" << endl
;
4539 if(d_queryMade
&& !options::incrementalSolving()) {
4540 throw ModalException("Cannot make multiple queries unless "
4541 "incremental solving is enabled "
4542 "(try --incremental)");
4545 // check to see if a postsolve() is pending
4546 if(d_needPostsolve
) {
4547 d_theoryEngine
->postsolve();
4548 d_needPostsolve
= false;
4550 // Note that a query has been made
4552 // reset global negation
4553 d_globalNegation
= false;
4555 bool didInternalPush
= false;
4557 setProblemExtended(true);
4561 size_t size
= assumptions
.size();
4564 /* Assume: not (BIGAND assumptions) */
4565 d_assumptions
.push_back(
4566 d_exprManager
->mkExpr(kind::AND
, assumptions
).notExpr());
4570 /* Assume: not expr */
4571 d_assumptions
.push_back(assumptions
[0].notExpr());
4576 /* Assume: BIGAND assumptions */
4577 d_assumptions
= assumptions
;
4580 if (!d_assumptions
.empty())
4583 didInternalPush
= true;
4586 Result
r(Result::SAT_UNKNOWN
, Result::UNKNOWN_REASON
);
4587 for (Expr e
: d_assumptions
)
4589 // Substitute out any abstract values in ex.
4590 e
= d_private
->substituteAbstractValues(Node::fromExpr(e
)).toExpr();
4591 Assert(e
.getExprManager() == d_exprManager
);
4592 // Ensure expr is type-checked at this point.
4595 /* Add assumption */
4596 if (d_assertionList
!= NULL
)
4598 d_assertionList
->push_back(e
);
4600 d_private
->addFormula(e
.getNode(), inUnsatCore
);
4603 r
= isQuery
? check().asValidityResult() : check().asSatisfiabilityResult();
4605 if ((options::solveRealAsInt() || options::solveIntAsBV() > 0)
4606 && r
.asSatisfiabilityResult().isSat() == Result::UNSAT
)
4608 r
= Result(Result::SAT_UNKNOWN
, Result::UNKNOWN_REASON
);
4610 // flipped if we did a global negation
4611 if (d_globalNegation
)
4613 Trace("smt") << "SmtEngine::process global negate " << r
<< std::endl
;
4614 if (r
.asSatisfiabilityResult().isSat() == Result::UNSAT
)
4616 r
= Result(Result::SAT
);
4618 else if (r
.asSatisfiabilityResult().isSat() == Result::SAT
)
4620 // only if satisfaction complete
4621 if (d_logic
.isPure(THEORY_ARITH
) || d_logic
.isPure(THEORY_BV
))
4623 r
= Result(Result::UNSAT
);
4627 r
= Result(Result::SAT_UNKNOWN
, Result::UNKNOWN_REASON
);
4630 Trace("smt") << "SmtEngine::global negate returned " << r
<< std::endl
;
4633 d_needPostsolve
= true;
4635 // Dump the query if requested
4636 if (Dump
.isOn("benchmark"))
4638 size_t size
= assumptions
.size();
4639 // the expr already got dumped out if assertion-dumping is on
4640 if (isQuery
&& size
== 1)
4642 Dump("benchmark") << QueryCommand(assumptions
[0]);
4646 Dump("benchmark") << CheckSatCommand();
4650 Dump("benchmark") << CheckSatAssumingCommand(d_assumptions
);
4654 d_propEngine
->resetTrail();
4657 if (didInternalPush
)
4662 // Remember the status
4665 setProblemExtended(false);
4667 Trace("smt") << "SmtEngine::" << (isQuery
? "query" : "checkSat") << "("
4668 << assumptions
<< ") => " << r
<< endl
;
4670 // Check that SAT results generate a model correctly.
4671 if(options::checkModels()) {
4672 // TODO (#1693) check model when unknown result?
4673 if (r
.asSatisfiabilityResult().isSat() == Result::SAT
)
4678 // Check that UNSAT results generate a proof correctly.
4679 if(options::checkProofs()) {
4680 if(r
.asSatisfiabilityResult().isSat() == Result::UNSAT
) {
4681 TimerStat::CodeTimer
checkProofTimer(d_stats
->d_checkProofTime
);
4685 // Check that UNSAT results generate an unsat core correctly.
4686 if(options::checkUnsatCores()) {
4687 if(r
.asSatisfiabilityResult().isSat() == Result::UNSAT
) {
4688 TimerStat::CodeTimer
checkUnsatCoreTimer(d_stats
->d_checkUnsatCoreTime
);
4692 // Check that synthesis solutions satisfy the conjecture
4693 if (options::checkSynthSol()
4694 && r
.asSatisfiabilityResult().isSat() == Result::UNSAT
)
4696 checkSynthSolution();
4700 } catch (UnsafeInterruptException
& e
) {
4701 AlwaysAssert(d_private
->getResourceManager()->out());
4702 Result::UnknownExplanation why
= d_private
->getResourceManager()->outOfResources() ?
4703 Result::RESOURCEOUT
: Result::TIMEOUT
;
4704 return Result(Result::SAT_UNKNOWN
, why
, d_filename
);
4708 vector
<Expr
> SmtEngine::getUnsatAssumptions(void)
4710 Trace("smt") << "SMT getUnsatAssumptions()" << endl
;
4711 SmtScope
smts(this);
4712 if (!options::unsatAssumptions())
4714 throw ModalException(
4715 "Cannot get unsat assumptions when produce-unsat-assumptions option "
4718 if (d_status
.isNull()
4719 || d_status
.asSatisfiabilityResult() != Result::UNSAT
4720 || d_problemExtended
)
4722 throw RecoverableModalException(
4723 "Cannot get unsat assumptions unless immediately preceded by "
4724 "UNSAT/VALID response.");
4726 finalOptionsAreSet();
4727 if (Dump
.isOn("benchmark"))
4729 Dump("benchmark") << GetUnsatAssumptionsCommand();
4731 UnsatCore core
= getUnsatCoreInternal();
4733 for (const Expr
& e
: d_assumptions
)
4735 if (find(core
.begin(), core
.end(), e
) != core
.end()) { res
.push_back(e
); }
4740 Result
SmtEngine::checkSynth(const Expr
& e
)
4742 SmtScope
smts(this);
4743 Trace("smt") << "Check synth: " << e
<< std::endl
;
4744 Trace("smt-synth") << "Check synthesis conjecture: " << e
<< std::endl
;
4745 return checkSatisfiability(e
, true, false);
4748 Result
SmtEngine::assertFormula(const Expr
& ex
, bool inUnsatCore
)
4750 Assert(ex
.getExprManager() == d_exprManager
);
4751 SmtScope
smts(this);
4752 finalOptionsAreSet();
4755 Trace("smt") << "SmtEngine::assertFormula(" << ex
<< ")" << endl
;
4757 if (Dump
.isOn("raw-benchmark")) {
4758 Dump("raw-benchmark") << AssertCommand(ex
);
4761 // Substitute out any abstract values in ex
4762 Expr e
= d_private
->substituteAbstractValues(Node::fromExpr(ex
)).toExpr();
4765 if(d_assertionList
!= NULL
) {
4766 d_assertionList
->push_back(e
);
4768 d_private
->addFormula(e
.getNode(), inUnsatCore
);
4769 return quickCheck().asValidityResult();
4770 }/* SmtEngine::assertFormula() */
4772 Node
SmtEngine::postprocess(TNode node
, TypeNode expectedType
) const {
4776 Expr
SmtEngine::simplify(const Expr
& ex
)
4778 Assert(ex
.getExprManager() == d_exprManager
);
4779 SmtScope
smts(this);
4780 finalOptionsAreSet();
4782 Trace("smt") << "SMT simplify(" << ex
<< ")" << endl
;
4784 if(Dump
.isOn("benchmark")) {
4785 Dump("benchmark") << SimplifyCommand(ex
);
4788 Expr e
= d_private
->substituteAbstractValues(Node::fromExpr(ex
)).toExpr();
4789 if( options::typeChecking() ) {
4790 e
.getType(true); // ensure expr is type-checked at this point
4793 // Make sure all preprocessing is done
4794 d_private
->processAssertions();
4795 Node n
= d_private
->simplify(Node::fromExpr(e
));
4796 n
= postprocess(n
, TypeNode::fromType(e
.getType()));
4800 Expr
SmtEngine::expandDefinitions(const Expr
& ex
)
4802 d_private
->spendResource(options::preprocessStep());
4804 Assert(ex
.getExprManager() == d_exprManager
);
4805 SmtScope
smts(this);
4806 finalOptionsAreSet();
4808 Trace("smt") << "SMT expandDefinitions(" << ex
<< ")" << endl
;
4810 // Substitute out any abstract values in ex.
4811 Expr e
= d_private
->substituteAbstractValues(Node::fromExpr(ex
)).toExpr();
4812 if(options::typeChecking()) {
4813 // Ensure expr is type-checked at this point.
4816 if(Dump
.isOn("benchmark")) {
4817 Dump("benchmark") << ExpandDefinitionsCommand(e
);
4819 unordered_map
<Node
, Node
, NodeHashFunction
> cache
;
4820 Node n
= d_private
->expandDefinitions(Node::fromExpr(e
), cache
, /* expandOnly = */ true);
4821 n
= postprocess(n
, TypeNode::fromType(e
.getType()));
4826 // TODO(#1108): Simplify the error reporting of this method.
4827 Expr
SmtEngine::getValue(const Expr
& ex
) const
4829 Assert(ex
.getExprManager() == d_exprManager
);
4830 SmtScope
smts(this);
4832 Trace("smt") << "SMT getValue(" << ex
<< ")" << endl
;
4833 if(Dump
.isOn("benchmark")) {
4834 Dump("benchmark") << GetValueCommand(ex
);
4837 if(!options::produceModels()) {
4839 "Cannot get value when produce-models options is off.";
4840 throw ModalException(msg
);
4842 if(d_status
.isNull() ||
4843 d_status
.asSatisfiabilityResult() == Result::UNSAT
||
4844 d_problemExtended
) {
4846 "Cannot get value unless immediately preceded by SAT/INVALID or UNKNOWN response.";
4847 throw RecoverableModalException(msg
);
4850 // Substitute out any abstract values in ex.
4851 Expr e
= d_private
->substituteAbstractValues(Node::fromExpr(ex
)).toExpr();
4853 // Ensure expr is type-checked at this point.
4854 e
.getType(options::typeChecking());
4856 // do not need to apply preprocessing substitutions (should be recorded
4857 // in model already)
4859 Node n
= Node::fromExpr(e
);
4860 Trace("smt") << "--- getting value of " << n
<< endl
;
4861 TypeNode expectedType
= n
.getType();
4863 // Expand, then normalize
4864 unordered_map
<Node
, Node
, NodeHashFunction
> cache
;
4865 n
= d_private
->expandDefinitions(n
, cache
);
4866 // There are two ways model values for terms are computed (for historical
4867 // reasons). One way is that used in check-model; the other is that
4868 // used by the Model classes. It's not clear to me exactly how these
4869 // two are different, but they need to be unified. This ugly hack here
4870 // is to fix bug 554 until we can revamp boolean-terms and models [MGD]
4873 if(!n
.getType().isFunction()) {
4874 n
= Rewriter::rewrite(n
);
4877 Trace("smt") << "--- getting value of " << n
<< endl
;
4878 TheoryModel
* m
= d_theoryEngine
->getModel();
4881 resultNode
= m
->getValue(n
);
4883 Trace("smt") << "--- got value " << n
<< " = " << resultNode
<< endl
;
4884 resultNode
= postprocess(resultNode
, expectedType
);
4885 Trace("smt") << "--- model-post returned " << resultNode
<< endl
;
4886 Trace("smt") << "--- model-post returned " << resultNode
.getType() << endl
;
4887 Trace("smt") << "--- model-post expected " << expectedType
<< endl
;
4889 // type-check the result we got
4890 Assert(resultNode
.isNull() || resultNode
.getType().isSubtypeOf(expectedType
),
4891 "Run with -t smt for details.");
4893 // ensure it's a constant
4894 Assert(resultNode
.getKind() == kind::LAMBDA
|| resultNode
.isConst());
4896 if(options::abstractValues() && resultNode
.getType().isArray()) {
4897 resultNode
= d_private
->mkAbstractValue(resultNode
);
4898 Trace("smt") << "--- abstract value >> " << resultNode
<< endl
;
4901 return resultNode
.toExpr();
4904 bool SmtEngine::addToAssignment(const Expr
& ex
) {
4905 SmtScope
smts(this);
4906 finalOptionsAreSet();
4908 // Substitute out any abstract values in ex
4909 Expr e
= d_private
->substituteAbstractValues(Node::fromExpr(ex
)).toExpr();
4910 Type type
= e
.getType(options::typeChecking());
4912 PrettyCheckArgument(
4913 type
.isBoolean(), e
,
4914 "expected Boolean-typed variable or function application "
4915 "in addToAssignment()" );
4916 Node n
= e
.getNode();
4917 // must be an APPLY of a zero-ary defined function, or a variable
4918 PrettyCheckArgument(
4919 ( ( n
.getKind() == kind::APPLY
&&
4920 ( d_definedFunctions
->find(n
.getOperator()) !=
4921 d_definedFunctions
->end() ) &&
4922 n
.getNumChildren() == 0 ) ||
4924 "expected variable or defined-function application "
4925 "in addToAssignment(),\ngot %s", e
.toString().c_str() );
4926 if(!options::produceAssignments()) {
4929 if(d_assignments
== NULL
) {
4930 d_assignments
= new(true) AssignmentSet(d_context
);
4932 d_assignments
->insert(n
);
4937 // TODO(#1108): Simplify the error reporting of this method.
4938 vector
<pair
<Expr
, Expr
>> SmtEngine::getAssignment()
4940 Trace("smt") << "SMT getAssignment()" << endl
;
4941 SmtScope
smts(this);
4942 finalOptionsAreSet();
4943 if(Dump
.isOn("benchmark")) {
4944 Dump("benchmark") << GetAssignmentCommand();
4946 if(!options::produceAssignments()) {
4948 "Cannot get the current assignment when "
4949 "produce-assignments option is off.";
4950 throw ModalException(msg
);
4952 if(d_status
.isNull() ||
4953 d_status
.asSatisfiabilityResult() == Result::UNSAT
||
4954 d_problemExtended
) {
4956 "Cannot get the current assignment unless immediately "
4957 "preceded by SAT/INVALID or UNKNOWN response.";
4958 throw RecoverableModalException(msg
);
4961 vector
<pair
<Expr
,Expr
>> res
;
4962 if (d_assignments
!= nullptr)
4964 TypeNode boolType
= d_nodeManager
->booleanType();
4965 TheoryModel
* m
= d_theoryEngine
->getModel();
4966 for (AssignmentSet::key_iterator i
= d_assignments
->key_begin(),
4967 iend
= d_assignments
->key_end();
4972 Assert(as
.getType() == boolType
);
4974 Trace("smt") << "--- getting value of " << as
<< endl
;
4976 // Expand, then normalize
4977 unordered_map
<Node
, Node
, NodeHashFunction
> cache
;
4978 Node n
= d_private
->expandDefinitions(as
, cache
);
4979 n
= Rewriter::rewrite(n
);
4981 Trace("smt") << "--- getting value of " << n
<< endl
;
4985 resultNode
= m
->getValue(n
);
4988 // type-check the result we got
4989 Assert(resultNode
.isNull() || resultNode
.getType() == boolType
);
4991 // ensure it's a constant
4992 Assert(resultNode
.isConst());
4994 Assert(as
.getKind() == kind::APPLY
|| as
.isVar());
4995 Assert(as
.getKind() != kind::APPLY
|| as
.getNumChildren() == 0);
4996 res
.emplace_back(as
.toExpr(), resultNode
.toExpr());
5002 void SmtEngine::addToModelCommandAndDump(const Command
& c
, uint32_t flags
, bool userVisible
, const char* dumpTag
) {
5003 Trace("smt") << "SMT addToModelCommandAndDump(" << c
<< ")" << endl
;
5004 SmtScope
smts(this);
5005 // If we aren't yet fully inited, the user might still turn on
5006 // produce-models. So let's keep any commands around just in
5007 // case. This is useful in two cases: (1) SMT-LIBv1 auto-declares
5008 // sort "U" in QF_UF before setLogic() is run and we still want to
5009 // support finding card(U) with --finite-model-find, and (2) to
5010 // decouple SmtEngine and ExprManager if the user does a few
5011 // ExprManager::mkSort() before SmtEngine::setOption("produce-models")
5012 // and expects to find their cardinalities in the model.
5013 if(/* userVisible && */
5014 (!d_fullyInited
|| options::produceModels()) &&
5015 (flags
& ExprManager::VAR_FLAG_DEFINED
) == 0) {
5017 if(flags
& ExprManager::VAR_FLAG_GLOBAL
) {
5018 d_modelGlobalCommands
.push_back(c
.clone());
5020 d_modelCommands
->push_back(c
.clone());
5023 if(Dump
.isOn(dumpTag
)) {
5027 d_dumpCommands
.push_back(c
.clone());
5032 // TODO(#1108): Simplify the error reporting of this method.
5033 Model
* SmtEngine::getModel() {
5034 Trace("smt") << "SMT getModel()" << endl
;
5035 SmtScope
smts(this);
5037 finalOptionsAreSet();
5039 if(Dump
.isOn("benchmark")) {
5040 Dump("benchmark") << GetModelCommand();
5043 if (!options::assignFunctionValues())
5046 "Cannot get the model when --assign-function-values is false.";
5047 throw RecoverableModalException(msg
);
5050 if(d_status
.isNull() ||
5051 d_status
.asSatisfiabilityResult() == Result::UNSAT
||
5052 d_problemExtended
) {
5054 "Cannot get the current model unless immediately "
5055 "preceded by SAT/INVALID or UNKNOWN response.";
5056 throw RecoverableModalException(msg
);
5058 if(!options::produceModels()) {
5060 "Cannot get model when produce-models options is off.";
5061 throw ModalException(msg
);
5063 TheoryModel
* m
= d_theoryEngine
->getModel();
5064 m
->d_inputName
= d_filename
;
5068 std::pair
<Expr
, Expr
> SmtEngine::getSepHeapAndNilExpr(void)
5070 if (!d_logic
.isTheoryEnabled(THEORY_SEP
))
5073 "Cannot obtain separation logic expressions if not using the "
5074 "separation logic theory.";
5075 throw RecoverableModalException(msg
);
5077 NodeManagerScope
nms(d_nodeManager
);
5080 Model
* m
= getModel();
5081 if (m
->getHeapModel(heap
, nil
))
5083 return std::make_pair(heap
, nil
);
5086 "SmtEngine::getSepHeapAndNilExpr(): failed to obtain heap/nil "
5087 "expressions from theory model.");
5090 Expr
SmtEngine::getSepHeapExpr() { return getSepHeapAndNilExpr().first
; }
5092 Expr
SmtEngine::getSepNilExpr() { return getSepHeapAndNilExpr().second
; }
5094 UnsatCore
SmtEngine::getUnsatCoreInternal()
5097 if (!options::unsatCores())
5099 throw ModalException(
5100 "Cannot get an unsat core when produce-unsat-cores option is off.");
5102 if (d_status
.isNull() || d_status
.asSatisfiabilityResult() != Result::UNSAT
5103 || d_problemExtended
)
5105 throw RecoverableModalException(
5106 "Cannot get an unsat core unless immediately preceded by UNSAT/VALID "
5110 d_proofManager
->traceUnsatCore(); // just to trigger core creation
5111 return UnsatCore(this, d_proofManager
->extractUnsatCore());
5112 #else /* IS_PROOFS_BUILD */
5113 throw ModalException(
5114 "This build of CVC4 doesn't have proof support (required for unsat "
5116 #endif /* IS_PROOFS_BUILD */
5119 void SmtEngine::checkUnsatCore() {
5120 Assert(options::unsatCores(), "cannot check unsat core if unsat cores are turned off");
5122 Notice() << "SmtEngine::checkUnsatCore(): generating unsat core" << endl
;
5123 UnsatCore core
= getUnsatCore();
5125 SmtEngine
coreChecker(d_exprManager
);
5126 coreChecker
.setLogic(getLogicInfo());
5129 std::vector
<Command
*>::const_iterator itg
= d_defineCommands
.begin();
5130 for (; itg
!= d_defineCommands
.end(); ++itg
) {
5131 (*itg
)->invoke(&coreChecker
);
5135 Notice() << "SmtEngine::checkUnsatCore(): pushing core assertions (size == " << core
.size() << ")" << endl
;
5136 for(UnsatCore::iterator i
= core
.begin(); i
!= core
.end(); ++i
) {
5137 Notice() << "SmtEngine::checkUnsatCore(): pushing core member " << *i
<< endl
;
5138 coreChecker
.assertFormula(*i
);
5140 const bool checkUnsatCores
= options::checkUnsatCores();
5143 options::checkUnsatCores
.set(false);
5144 options::checkProofs
.set(false);
5145 r
= coreChecker
.checkSat();
5147 options::checkUnsatCores
.set(checkUnsatCores
);
5150 Notice() << "SmtEngine::checkUnsatCore(): result is " << r
<< endl
;
5151 if(r
.asSatisfiabilityResult().isUnknown()) {
5152 InternalError("SmtEngine::checkUnsatCore(): could not check core result unknown.");
5155 if(r
.asSatisfiabilityResult().isSat()) {
5156 InternalError("SmtEngine::checkUnsatCore(): produced core was satisfiable.");
5160 void SmtEngine::checkModel(bool hardFailure
) {
5161 // --check-model implies --produce-assertions, which enables the
5162 // assertion list, so we should be ok.
5163 Assert(d_assertionList
!= NULL
, "don't have an assertion list to check in SmtEngine::checkModel()");
5165 TimerStat::CodeTimer
checkModelTimer(d_stats
->d_checkModelTime
);
5167 // Throughout, we use Notice() to give diagnostic output.
5169 // If this function is running, the user gave --check-model (or equivalent),
5170 // and if Notice() is on, the user gave --verbose (or equivalent).
5172 Notice() << "SmtEngine::checkModel(): generating model" << endl
;
5173 TheoryModel
* m
= d_theoryEngine
->getModel();
5175 // check-model is not guaranteed to succeed if approximate values were used
5176 if (m
->hasApproximations())
5179 << "WARNING: running check-model on a model with approximate values..."
5183 // Check individual theory assertions
5184 d_theoryEngine
->checkTheoryAssertionsWithModel(hardFailure
);
5189 // We have a "fake context" for the substitution map (we don't need it
5190 // to be context-dependent)
5191 context::Context fakeContext
;
5192 SubstitutionMap
substitutions(&fakeContext
, /* substituteUnderQuantifiers = */ false);
5194 for(size_t k
= 0; k
< m
->getNumCommands(); ++k
) {
5195 const DeclareFunctionCommand
* c
= dynamic_cast<const DeclareFunctionCommand
*>(m
->getCommand(k
));
5196 Notice() << "SmtEngine::checkModel(): model command " << k
<< " : " << m
->getCommand(k
) << endl
;
5198 // we don't care about DECLARE-DATATYPES, DECLARE-SORT, ...
5199 Notice() << "SmtEngine::checkModel(): skipping..." << endl
;
5201 // We have a DECLARE-FUN:
5203 // We'll first do some checks, then add to our substitution map
5204 // the mapping: function symbol |-> value
5206 Expr func
= c
->getFunction();
5207 Node val
= m
->getValue(func
);
5209 Notice() << "SmtEngine::checkModel(): adding substitution: " << func
<< " |-> " << val
<< endl
;
5211 // (1) if the value is a lambda, ensure the lambda doesn't contain the
5212 // function symbol (since then the definition is recursive)
5213 if (val
.getKind() == kind::LAMBDA
) {
5214 // first apply the model substitutions we have so far
5215 Debug("boolean-terms") << "applying subses to " << val
[1] << endl
;
5216 Node n
= substitutions
.apply(val
[1]);
5217 Debug("boolean-terms") << "++ got " << n
<< endl
;
5218 // now check if n contains func by doing a substitution
5219 // [func->func2] and checking equality of the Nodes.
5220 // (this just a way to check if func is in n.)
5221 SubstitutionMap
subs(&fakeContext
);
5222 Node func2
= NodeManager::currentNM()->mkSkolem("", TypeNode::fromType(func
.getType()), "", NodeManager::SKOLEM_NO_NOTIFY
);
5223 subs
.addSubstitution(func
, func2
);
5224 if(subs
.apply(n
) != n
) {
5225 Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE DEFINED IN TERMS OF ITSELF ***" << endl
;
5227 ss
<< "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
5228 << "considering model value for " << func
<< endl
5229 << "body of lambda is: " << val
<< endl
;
5231 ss
<< "body substitutes to: " << n
<< endl
;
5233 ss
<< "so " << func
<< " is defined in terms of itself." << endl
5234 << "Run with `--check-models -v' for additional diagnostics.";
5235 InternalError(ss
.str());
5239 // (2) check that the value is actually a value
5240 else if (!val
.isConst()) {
5241 Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE NOT A CONSTANT ***" << endl
;
5243 ss
<< "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
5244 << "model value for " << func
<< endl
5245 << " is " << val
<< endl
5246 << "and that is not a constant (.isConst() == false)." << endl
5247 << "Run with `--check-models -v' for additional diagnostics.";
5248 InternalError(ss
.str());
5251 // (3) check that it's the correct (sub)type
5252 // This was intended to be a more general check, but for now we can't do that because
5253 // e.g. "1" is an INT, which isn't a subrange type [1..10] (etc.).
5254 else if(func
.getType().isInteger() && !val
.getType().isInteger()) {
5255 Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE NOT CORRECT TYPE ***" << endl
;
5257 ss
<< "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
5258 << "model value for " << func
<< endl
5259 << " is " << val
<< endl
5260 << "value type is " << val
.getType() << endl
5261 << "should be of type " << func
.getType() << endl
5262 << "Run with `--check-models -v' for additional diagnostics.";
5263 InternalError(ss
.str());
5266 // (4) checks complete, add the substitution
5267 Debug("boolean-terms") << "cm: adding subs " << func
<< " :=> " << val
<< endl
;
5268 substitutions
.addSubstitution(func
, val
);
5272 // Now go through all our user assertions checking if they're satisfied.
5273 for(AssertionList::const_iterator i
= d_assertionList
->begin(); i
!= d_assertionList
->end(); ++i
) {
5274 Notice() << "SmtEngine::checkModel(): checking assertion " << *i
<< endl
;
5275 Node n
= Node::fromExpr(*i
);
5277 // Apply any define-funs from the problem.
5279 unordered_map
<Node
, Node
, NodeHashFunction
> cache
;
5280 n
= d_private
->expandDefinitions(n
, cache
);
5282 Notice() << "SmtEngine::checkModel(): -- expands to " << n
<< endl
;
5284 // Apply our model value substitutions.
5285 Debug("boolean-terms") << "applying subses to " << n
<< endl
;
5286 n
= substitutions
.apply(n
);
5287 Debug("boolean-terms") << "++ got " << n
<< endl
;
5288 Notice() << "SmtEngine::checkModel(): -- substitutes to " << n
<< endl
;
5290 if( n
.getKind() != kind::REWRITE_RULE
){
5291 // In case it's a quantifier (or contains one), look up its value before
5292 // simplifying, or the quantifier might be irreparably altered.
5294 Notice() << "SmtEngine::checkModel(): -- get value : " << n
<< std::endl
;
5296 // Note this "skip" is done here, rather than above. This is
5297 // because (1) the quantifier could in principle simplify to false,
5298 // which should be reported, and (2) checking for the quantifier
5299 // above, before simplification, doesn't catch buried quantifiers
5300 // anyway (those not at the top-level).
5301 Notice() << "SmtEngine::checkModel(): -- skipping rewrite-rules assertion"
5306 // Simplify the result.
5307 n
= d_private
->simplify(n
);
5308 Notice() << "SmtEngine::checkModel(): -- simplifies to " << n
<< endl
;
5310 // Replace the already-known ITEs (this is important for ground ITEs under quantifiers).
5311 n
= d_private
->d_iteRemover
.replace(n
);
5312 Notice() << "SmtEngine::checkModel(): -- ite replacement gives " << n
<< endl
;
5314 // Apply our model value substitutions (again), as things may have been simplified.
5315 Debug("boolean-terms") << "applying subses to " << n
<< endl
;
5316 n
= substitutions
.apply(n
);
5317 Debug("boolean-terms") << "++ got " << n
<< endl
;
5318 Notice() << "SmtEngine::checkModel(): -- re-substitutes to " << n
<< endl
;
5320 // As a last-ditch effort, ask model to simplify it.
5321 // Presently, this is only an issue for quantifiers, which can have a value
5322 // but don't show up in our substitution map above.
5324 Notice() << "SmtEngine::checkModel(): -- model-substitutes to " << n
<< endl
;
5326 if( d_logic
.isQuantified() ){
5327 // AJR: since quantified formulas are not checkable, we assign them to true/false based on the satisfying assignment.
5328 // however, quantified formulas can be modified during preprocess, so they may not correspond to those in the satisfying assignment.
5329 // hence we use a relaxed version of check model here.
5330 // this is necessary until preprocessing passes explicitly record how they rewrite quantified formulas
5331 if( hardFailure
&& !n
.isConst() && n
.getKind() != kind::LAMBDA
){
5332 Notice() << "SmtEngine::checkModel(): -- relax check model wrt quantified formulas..." << endl
;
5333 AlwaysAssert( quantifiers::QuantifiersRewriter::containsQuantifiers( n
) );
5334 Warning() << "Warning : SmtEngine::checkModel(): cannot check simplified assertion : " << n
<< endl
;
5338 AlwaysAssert(!hardFailure
|| n
.isConst() || n
.getKind() == kind::LAMBDA
);
5340 // The result should be == true.
5341 if(n
!= NodeManager::currentNM()->mkConst(true)) {
5342 Notice() << "SmtEngine::checkModel(): *** PROBLEM: EXPECTED `TRUE' ***"
5345 ss
<< "SmtEngine::checkModel(): "
5346 << "ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
5347 << "assertion: " << *i
<< endl
5348 << "simplifies to: " << n
<< endl
5349 << "expected `true'." << endl
5350 << "Run with `--check-models -v' for additional diagnostics.";
5352 InternalError(ss
.str());
5354 Warning() << ss
.str() << endl
;
5358 Notice() << "SmtEngine::checkModel(): all assertions checked out OK !" << endl
;
5361 void SmtEngine::checkSynthSolution()
5363 NodeManager
* nm
= NodeManager::currentNM();
5364 Notice() << "SmtEngine::checkSynthSolution(): checking synthesis solution" << endl
;
5365 map
<Node
, Node
> sol_map
;
5366 /* Get solutions and build auxiliary vectors for substituting */
5367 d_theoryEngine
->getSynthSolutions(sol_map
);
5368 if (sol_map
.empty())
5370 Trace("check-synth-sol") << "No solution to check!\n";
5373 Trace("check-synth-sol") << "Got solution map:\n";
5374 std::vector
<Node
> function_vars
, function_sols
;
5375 for (const auto& pair
: sol_map
)
5377 Trace("check-synth-sol") << pair
.first
<< " --> " << pair
.second
<< "\n";
5378 function_vars
.push_back(pair
.first
);
5379 function_sols
.push_back(pair
.second
);
5381 Trace("check-synth-sol") << "Starting new SMT Engine\n";
5382 /* Start new SMT engine to check solutions */
5383 SmtEngine
solChecker(d_exprManager
);
5384 solChecker
.setLogic(getLogicInfo());
5385 setOption("check-synth-sol", SExpr("false"));
5387 Trace("check-synth-sol") << "Retrieving assertions\n";
5388 // Build conjecture from original assertions
5389 if (d_assertionList
== NULL
)
5391 Trace("check-synth-sol") << "No assertions to check\n";
5394 for (AssertionList::const_iterator i
= d_assertionList
->begin();
5395 i
!= d_assertionList
->end();
5398 Notice() << "SmtEngine::checkSynthSolution(): checking assertion " << *i
<< endl
;
5399 Trace("check-synth-sol") << "Retrieving assertion " << *i
<< "\n";
5400 Node conj
= Node::fromExpr(*i
);
5401 // Apply any define-funs from the problem.
5403 unordered_map
<Node
, Node
, NodeHashFunction
> cache
;
5404 conj
= d_private
->expandDefinitions(conj
, cache
);
5406 Notice() << "SmtEngine::checkSynthSolution(): -- expands to " << conj
<< endl
;
5407 Trace("check-synth-sol") << "Expanded assertion " << conj
<< "\n";
5408 if (conj
.getKind() != kind::FORALL
)
5410 Trace("check-synth-sol") << "Not a checkable assertion.\n";
5414 // Apply solution map to conjecture body
5416 /* Whether property is quantifier free */
5417 if (conj
[1].getKind() != kind::EXISTS
)
5419 conjBody
= conj
[1].substitute(function_vars
.begin(),
5420 function_vars
.end(),
5421 function_sols
.begin(),
5422 function_sols
.end());
5426 conjBody
= conj
[1][1].substitute(function_vars
.begin(),
5427 function_vars
.end(),
5428 function_sols
.begin(),
5429 function_sols
.end());
5431 /* Skolemize property */
5432 std::vector
<Node
> vars
, skos
;
5433 for (unsigned j
= 0, size
= conj
[1][0].getNumChildren(); j
< size
; ++j
)
5435 vars
.push_back(conj
[1][0][j
]);
5436 std::stringstream ss
;
5438 skos
.push_back(nm
->mkSkolem(ss
.str(), conj
[1][0][j
].getType()));
5439 Trace("check-synth-sol") << "\tSkolemizing " << conj
[1][0][j
] << " to "
5440 << skos
.back() << "\n";
5442 conjBody
= conjBody
.substitute(
5443 vars
.begin(), vars
.end(), skos
.begin(), skos
.end());
5445 Notice() << "SmtEngine::checkSynthSolution(): -- body substitutes to "
5446 << conjBody
<< endl
;
5447 Trace("check-synth-sol") << "Substituted body of assertion to " << conjBody
5449 solChecker
.assertFormula(conjBody
.toExpr());
5450 Result r
= solChecker
.checkSat();
5451 Notice() << "SmtEngine::checkSynthSolution(): result is " << r
<< endl
;
5452 Trace("check-synth-sol") << "Satsifiability check: " << r
<< "\n";
5453 if (r
.asSatisfiabilityResult().isUnknown())
5456 "SmtEngine::checkSynthSolution(): could not check solution, result "
5459 else if (r
.asSatisfiabilityResult().isSat())
5462 "SmtEngine::checkSynthSolution(): produced solution leads to "
5463 "satisfiable negated conjecture.");
5465 solChecker
.resetAssertions();
5469 // TODO(#1108): Simplify the error reporting of this method.
5470 UnsatCore
SmtEngine::getUnsatCore() {
5471 Trace("smt") << "SMT getUnsatCore()" << endl
;
5472 SmtScope
smts(this);
5473 finalOptionsAreSet();
5474 if(Dump
.isOn("benchmark")) {
5475 Dump("benchmark") << GetUnsatCoreCommand();
5477 return getUnsatCoreInternal();
5480 // TODO(#1108): Simplify the error reporting of this method.
5481 const Proof
& SmtEngine::getProof()
5483 Trace("smt") << "SMT getProof()" << endl
;
5484 SmtScope
smts(this);
5485 finalOptionsAreSet();
5486 if(Dump
.isOn("benchmark")) {
5487 Dump("benchmark") << GetProofCommand();
5490 if(!options::proof()) {
5491 throw ModalException("Cannot get a proof when produce-proofs option is off.");
5493 if(d_status
.isNull() ||
5494 d_status
.asSatisfiabilityResult() != Result::UNSAT
||
5495 d_problemExtended
) {
5496 throw RecoverableModalException(
5497 "Cannot get a proof unless immediately preceded by UNSAT/VALID "
5501 return ProofManager::getProof(this);
5502 #else /* IS_PROOFS_BUILD */
5503 throw ModalException("This build of CVC4 doesn't have proof support.");
5504 #endif /* IS_PROOFS_BUILD */
5507 void SmtEngine::printInstantiations( std::ostream
& out
) {
5508 SmtScope
smts(this);
5509 if( options::instFormatMode()==INST_FORMAT_MODE_SZS
){
5510 out
<< "% SZS output start Proof for " << d_filename
.c_str() << std::endl
;
5512 if( d_theoryEngine
){
5513 d_theoryEngine
->printInstantiations( out
);
5517 if( options::instFormatMode()==INST_FORMAT_MODE_SZS
){
5518 out
<< "% SZS output end Proof for " << d_filename
.c_str() << std::endl
;
5522 void SmtEngine::printSynthSolution( std::ostream
& out
) {
5523 SmtScope
smts(this);
5524 if( d_theoryEngine
){
5525 d_theoryEngine
->printSynthSolution( out
);
5531 void SmtEngine::getSynthSolutions(std::map
<Expr
, Expr
>& sol_map
)
5533 SmtScope
smts(this);
5534 map
<Node
, Node
> sol_mapn
;
5535 Assert(d_theoryEngine
!= nullptr);
5536 d_theoryEngine
->getSynthSolutions(sol_mapn
);
5537 for (std::pair
<const Node
, Node
>& s
: sol_mapn
)
5539 sol_map
[s
.first
.toExpr()] = s
.second
.toExpr();
5543 Expr
SmtEngine::doQuantifierElimination(const Expr
& e
, bool doFull
, bool strict
)
5545 SmtScope
smts(this);
5546 if(!d_logic
.isPure(THEORY_ARITH
) && strict
){
5547 Warning() << "Unexpected logic for quantifier elimination " << d_logic
<< endl
;
5549 Trace("smt-qe") << "Do quantifier elimination " << e
<< std::endl
;
5550 Node n_e
= Node::fromExpr( e
);
5551 if (n_e
.getKind() != kind::EXISTS
&& n_e
.getKind() != kind::FORALL
)
5553 throw ModalException(
5554 "Expecting a quantified formula as argument to get-qe.");
5556 //tag the quantified formula with the quant-elim attribute
5557 TypeNode t
= NodeManager::currentNM()->booleanType();
5558 Node n_attr
= NodeManager::currentNM()->mkSkolem("qe", t
, "Auxiliary variable for qe attr.");
5559 std::vector
< Node
> node_values
;
5560 d_theoryEngine
->setUserAttribute( doFull
? "quant-elim" : "quant-elim-partial", n_attr
, node_values
, "");
5561 n_attr
= NodeManager::currentNM()->mkNode(kind::INST_ATTRIBUTE
, n_attr
);
5562 n_attr
= NodeManager::currentNM()->mkNode(kind::INST_PATTERN_LIST
, n_attr
);
5563 std::vector
< Node
> e_children
;
5564 e_children
.push_back( n_e
[0] );
5565 e_children
.push_back(n_e
.getKind() == kind::EXISTS
? n_e
[1]
5567 e_children
.push_back( n_attr
);
5568 Node nn_e
= NodeManager::currentNM()->mkNode( kind::EXISTS
, e_children
);
5569 Trace("smt-qe-debug") << "Query for quantifier elimination : " << nn_e
<< std::endl
;
5570 Assert( nn_e
.getNumChildren()==3 );
5571 Result r
= checkSatisfiability(nn_e
.toExpr(), true, true);
5572 Trace("smt-qe") << "Query returned " << r
<< std::endl
;
5573 if(r
.asSatisfiabilityResult().isSat() != Result::UNSAT
) {
5574 if( r
.asSatisfiabilityResult().isSat() != Result::SAT
&& doFull
){
5576 ss
<< "While performing quantifier elimination, unexpected result : " << r
<< " for query.";
5577 InternalError(ss
.str().c_str());
5579 std::vector
< Node
> inst_qs
;
5580 d_theoryEngine
->getInstantiatedQuantifiedFormulas( inst_qs
);
5581 Assert( inst_qs
.size()<=1 );
5583 if( inst_qs
.size()==1 ){
5584 Node top_q
= inst_qs
[0];
5585 //Node top_q = Rewriter::rewrite( nn_e ).negate();
5586 Assert( top_q
.getKind()==kind::FORALL
);
5587 Trace("smt-qe") << "Get qe for " << top_q
<< std::endl
;
5588 ret_n
= d_theoryEngine
->getInstantiatedConjunction( top_q
);
5589 Trace("smt-qe") << "Returned : " << ret_n
<< std::endl
;
5590 if (n_e
.getKind() == kind::EXISTS
)
5592 ret_n
= Rewriter::rewrite(ret_n
.negate());
5595 ret_n
= NodeManager::currentNM()->mkConst(n_e
.getKind() != kind::EXISTS
);
5597 // do extended rewrite to minimize the size of the formula aggressively
5598 theory::quantifiers::ExtendedRewriter
extr(true);
5599 ret_n
= extr
.extendedRewrite(ret_n
);
5600 return ret_n
.toExpr();
5602 return NodeManager::currentNM()
5603 ->mkConst(n_e
.getKind() == kind::EXISTS
)
5608 void SmtEngine::getInstantiatedQuantifiedFormulas( std::vector
< Expr
>& qs
) {
5609 SmtScope
smts(this);
5610 if( d_theoryEngine
){
5611 std::vector
< Node
> qs_n
;
5612 d_theoryEngine
->getInstantiatedQuantifiedFormulas( qs_n
);
5613 for( unsigned i
=0; i
<qs_n
.size(); i
++ ){
5614 qs
.push_back( qs_n
[i
].toExpr() );
5621 void SmtEngine::getInstantiations( Expr q
, std::vector
< Expr
>& insts
) {
5622 SmtScope
smts(this);
5623 if( d_theoryEngine
){
5624 std::vector
< Node
> insts_n
;
5625 d_theoryEngine
->getInstantiations( Node::fromExpr( q
), insts_n
);
5626 for( unsigned i
=0; i
<insts_n
.size(); i
++ ){
5627 insts
.push_back( insts_n
[i
].toExpr() );
5634 void SmtEngine::getInstantiationTermVectors( Expr q
, std::vector
< std::vector
< Expr
> >& tvecs
) {
5635 SmtScope
smts(this);
5636 Assert(options::trackInstLemmas());
5637 if( d_theoryEngine
){
5638 std::vector
< std::vector
< Node
> > tvecs_n
;
5639 d_theoryEngine
->getInstantiationTermVectors( Node::fromExpr( q
), tvecs_n
);
5640 for( unsigned i
=0; i
<tvecs_n
.size(); i
++ ){
5641 std::vector
< Expr
> tvec
;
5642 for( unsigned j
=0; j
<tvecs_n
[i
].size(); j
++ ){
5643 tvec
.push_back( tvecs_n
[i
][j
].toExpr() );
5645 tvecs
.push_back( tvec
);
5652 vector
<Expr
> SmtEngine::getAssertions() {
5653 SmtScope
smts(this);
5654 finalOptionsAreSet();
5656 if(Dump
.isOn("benchmark")) {
5657 Dump("benchmark") << GetAssertionsCommand();
5659 Trace("smt") << "SMT getAssertions()" << endl
;
5660 if(!options::produceAssertions()) {
5662 "Cannot query the current assertion list when not in produce-assertions mode.";
5663 throw ModalException(msg
);
5665 Assert(d_assertionList
!= NULL
);
5666 // copy the result out
5667 return vector
<Expr
>(d_assertionList
->begin(), d_assertionList
->end());
5670 void SmtEngine::push()
5672 SmtScope
smts(this);
5673 finalOptionsAreSet();
5675 Trace("smt") << "SMT push()" << endl
;
5676 d_private
->notifyPush();
5677 d_private
->processAssertions();
5678 if(Dump
.isOn("benchmark")) {
5679 Dump("benchmark") << PushCommand();
5681 if(!options::incrementalSolving()) {
5682 throw ModalException("Cannot push when not solving incrementally (use --incremental)");
5685 // check to see if a postsolve() is pending
5686 if(d_needPostsolve
) {
5687 d_theoryEngine
->postsolve();
5688 d_needPostsolve
= false;
5691 // The problem isn't really "extended" yet, but this disallows
5692 // get-model after a push, simplifying our lives somewhat and
5693 // staying symmtric with pop.
5694 setProblemExtended(true);
5696 d_userLevels
.push_back(d_userContext
->getLevel());
5698 Trace("userpushpop") << "SmtEngine: pushed to level "
5699 << d_userContext
->getLevel() << endl
;
5702 void SmtEngine::pop() {
5703 SmtScope
smts(this);
5704 finalOptionsAreSet();
5705 Trace("smt") << "SMT pop()" << endl
;
5706 if(Dump
.isOn("benchmark")) {
5707 Dump("benchmark") << PopCommand();
5709 if(!options::incrementalSolving()) {
5710 throw ModalException("Cannot pop when not solving incrementally (use --incremental)");
5712 if(d_userLevels
.size() == 0) {
5713 throw ModalException("Cannot pop beyond the first user frame");
5716 // check to see if a postsolve() is pending
5717 if(d_needPostsolve
) {
5718 d_theoryEngine
->postsolve();
5719 d_needPostsolve
= false;
5722 // The problem isn't really "extended" yet, but this disallows
5723 // get-model after a pop, simplifying our lives somewhat. It might
5724 // not be strictly necessary to do so, since the pops occur lazily,
5725 // but also it would be weird to have a legally-executed (get-model)
5726 // that only returns a subset of the assignment (because the rest
5727 // is no longer in scope!).
5728 setProblemExtended(true);
5730 AlwaysAssert(d_userContext
->getLevel() > 0);
5731 AlwaysAssert(d_userLevels
.back() < d_userContext
->getLevel());
5732 while (d_userLevels
.back() < d_userContext
->getLevel()) {
5735 d_userLevels
.pop_back();
5737 // Clear out assertion queues etc., in case anything is still in there
5738 d_private
->notifyPop();
5740 Trace("userpushpop") << "SmtEngine: popped to level "
5741 << d_userContext
->getLevel() << endl
;
5742 // FIXME: should we reset d_status here?
5743 // SMT-LIBv2 spec seems to imply no, but it would make sense to..
5746 void SmtEngine::internalPush() {
5747 Assert(d_fullyInited
);
5748 Trace("smt") << "SmtEngine::internalPush()" << endl
;
5750 if(options::incrementalSolving()) {
5751 d_private
->processAssertions();
5752 TimerStat::CodeTimer
pushPopTimer(d_stats
->d_pushPopTime
);
5753 d_userContext
->push();
5754 // the d_context push is done inside of the SAT solver
5755 d_propEngine
->push();
5759 void SmtEngine::internalPop(bool immediate
) {
5760 Assert(d_fullyInited
);
5761 Trace("smt") << "SmtEngine::internalPop()" << endl
;
5762 if(options::incrementalSolving()) {
5770 void SmtEngine::doPendingPops() {
5771 Assert(d_pendingPops
== 0 || options::incrementalSolving());
5772 while(d_pendingPops
> 0) {
5773 TimerStat::CodeTimer
pushPopTimer(d_stats
->d_pushPopTime
);
5774 d_propEngine
->pop();
5775 // the d_context pop is done inside of the SAT solver
5776 d_userContext
->pop();
5781 void SmtEngine::reset()
5783 SmtScope
smts(this);
5784 ExprManager
*em
= d_exprManager
;
5785 Trace("smt") << "SMT reset()" << endl
;
5786 if(Dump
.isOn("benchmark")) {
5787 Dump("benchmark") << ResetCommand();
5790 opts
.copyValues(d_originalOptions
);
5792 NodeManager::fromExprManager(em
)->getOptions().copyValues(opts
);
5793 new(this) SmtEngine(em
);
5796 void SmtEngine::resetAssertions()
5798 SmtScope
smts(this);
5801 Trace("smt") << "SMT resetAssertions()" << endl
;
5802 if(Dump
.isOn("benchmark")) {
5803 Dump("benchmark") << ResetAssertionsCommand();
5806 while(!d_userLevels
.empty()) {
5810 // Also remember the global push/pop around everything.
5811 Assert(d_userLevels
.size() == 0 && d_userContext
->getLevel() == 1);
5812 d_context
->popto(0);
5813 d_userContext
->popto(0);
5814 DeleteAndClearCommandVector(d_modelGlobalCommands
);
5815 d_userContext
->push();
5819 void SmtEngine::interrupt()
5821 if(!d_fullyInited
) {
5824 d_propEngine
->interrupt();
5825 d_theoryEngine
->interrupt();
5828 void SmtEngine::setResourceLimit(unsigned long units
, bool cumulative
) {
5829 d_private
->getResourceManager()->setResourceLimit(units
, cumulative
);
5831 void SmtEngine::setTimeLimit(unsigned long milis
, bool cumulative
) {
5832 d_private
->getResourceManager()->setTimeLimit(milis
, cumulative
);
5835 unsigned long SmtEngine::getResourceUsage() const {
5836 return d_private
->getResourceManager()->getResourceUsage();
5839 unsigned long SmtEngine::getTimeUsage() const {
5840 return d_private
->getResourceManager()->getTimeUsage();
5843 unsigned long SmtEngine::getResourceRemaining() const
5845 return d_private
->getResourceManager()->getResourceRemaining();
5848 unsigned long SmtEngine::getTimeRemaining() const
5850 return d_private
->getResourceManager()->getTimeRemaining();
5853 Statistics
SmtEngine::getStatistics() const
5855 return Statistics(*d_statisticsRegistry
);
5858 SExpr
SmtEngine::getStatistic(std::string name
) const
5860 return d_statisticsRegistry
->getStatistic(name
);
5863 void SmtEngine::safeFlushStatistics(int fd
) const {
5864 d_statisticsRegistry
->safeFlushInformation(fd
);
5867 void SmtEngine::setUserAttribute(const std::string
& attr
,
5869 const std::vector
<Expr
>& expr_values
,
5870 const std::string
& str_value
)
5872 SmtScope
smts(this);
5873 std::vector
<Node
> node_values
;
5874 for( unsigned i
=0; i
<expr_values
.size(); i
++ ){
5875 node_values
.push_back( expr_values
[i
].getNode() );
5877 d_theoryEngine
->setUserAttribute(attr
, expr
.getNode(), node_values
, str_value
);
5880 void SmtEngine::setPrintFuncInModel(Expr f
, bool p
) {
5881 Trace("setp-model") << "Set printInModel " << f
<< " to " << p
<< std::endl
;
5882 for( unsigned i
=0; i
<d_modelGlobalCommands
.size(); i
++ ){
5883 Command
* c
= d_modelGlobalCommands
[i
];
5884 DeclareFunctionCommand
* dfc
= dynamic_cast<DeclareFunctionCommand
*>(c
);
5886 if( dfc
->getFunction()==f
){
5887 dfc
->setPrintInModel( p
);
5891 for( unsigned i
=0; i
<d_modelCommands
->size(); i
++ ){
5892 Command
* c
= (*d_modelCommands
)[i
];
5893 DeclareFunctionCommand
* dfc
= dynamic_cast<DeclareFunctionCommand
*>(c
);
5895 if( dfc
->getFunction()==f
){
5896 dfc
->setPrintInModel( p
);
5902 void SmtEngine::beforeSearch()
5905 throw ModalException(
5906 "SmtEngine::beforeSearch called after initialization.");
5911 void SmtEngine::setOption(const std::string
& key
, const CVC4::SExpr
& value
)
5913 NodeManagerScope
nms(d_nodeManager
);
5914 Trace("smt") << "SMT setOption(" << key
<< ", " << value
<< ")" << endl
;
5916 if(Dump
.isOn("benchmark")) {
5917 Dump("benchmark") << SetOptionCommand(key
, value
);
5920 if(key
== "command-verbosity") {
5921 if(!value
.isAtom()) {
5922 const vector
<SExpr
>& cs
= value
.getChildren();
5923 if(cs
.size() == 2 &&
5924 (cs
[0].isKeyword() || cs
[0].isString()) &&
5925 cs
[1].isInteger()) {
5926 string c
= cs
[0].getValue();
5927 const Integer
& v
= cs
[1].getIntegerValue();
5928 if(v
< 0 || v
> 2) {
5929 throw OptionException("command-verbosity must be 0, 1, or 2");
5931 d_commandVerbosity
[c
] = v
;
5935 throw OptionException("command-verbosity value must be a tuple (command-name, integer)");
5938 if(!value
.isAtom()) {
5939 throw OptionException("bad value for :" + key
);
5942 string optionarg
= value
.getValue();
5943 Options
& nodeManagerOptions
= NodeManager::currentNM()->getOptions();
5944 nodeManagerOptions
.setOption(key
, optionarg
);
5947 CVC4::SExpr
SmtEngine::getOption(const std::string
& key
) const
5949 NodeManagerScope
nms(d_nodeManager
);
5951 Trace("smt") << "SMT getOption(" << key
<< ")" << endl
;
5953 if(key
.length() >= 18 &&
5954 key
.compare(0, 18, "command-verbosity:") == 0) {
5955 map
<string
, Integer
>::const_iterator i
= d_commandVerbosity
.find(key
.c_str() + 18);
5956 if(i
!= d_commandVerbosity
.end()) {
5957 return SExpr((*i
).second
);
5959 i
= d_commandVerbosity
.find("*");
5960 if(i
!= d_commandVerbosity
.end()) {
5961 return SExpr((*i
).second
);
5963 return SExpr(Integer(2));
5966 if(Dump
.isOn("benchmark")) {
5967 Dump("benchmark") << GetOptionCommand(key
);
5970 if(key
== "command-verbosity") {
5971 vector
<SExpr
> result
;
5972 SExpr defaultVerbosity
;
5973 for(map
<string
, Integer
>::const_iterator i
= d_commandVerbosity
.begin();
5974 i
!= d_commandVerbosity
.end();
5977 v
.push_back(SExpr((*i
).first
));
5978 v
.push_back(SExpr((*i
).second
));
5979 if((*i
).first
== "*") {
5980 // put the default at the end of the SExpr
5981 defaultVerbosity
= SExpr(v
);
5983 result
.push_back(SExpr(v
));
5986 // put the default at the end of the SExpr
5987 if(!defaultVerbosity
.isAtom()) {
5988 result
.push_back(defaultVerbosity
);
5990 // ensure the default is always listed
5992 v
.push_back(SExpr("*"));
5993 v
.push_back(SExpr(Integer(2)));
5994 result
.push_back(SExpr(v
));
5996 return SExpr(result
);
5999 Options
& nodeManagerOptions
= NodeManager::currentNM()->getOptions();
6000 return SExpr::parseAtom(nodeManagerOptions
.getOption(key
));
6003 void SmtEngine::setReplayStream(ExprStream
* replayStream
) {
6004 AlwaysAssert(!d_fullyInited
,
6005 "Cannot set replay stream once fully initialized");
6006 d_replayStream
= replayStream
;
6009 bool SmtEngine::getExpressionName(Expr e
, std::string
& name
) const {
6010 return d_private
->getExpressionName(e
, name
);
6013 void SmtEngine::setExpressionName(Expr e
, const std::string
& name
) {
6014 Trace("smt-debug") << "Set expression name " << e
<< " to " << name
<< std::endl
;
6015 d_private
->setExpressionName(e
,name
);
6018 }/* CVC4 namespace */