1 /********************* */
2 /*! \file smt_engine.cpp
4 ** Top contributors (to current version):
5 ** Morgan Deters, Tim King, Andrew Reynolds
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
8 ** in the top-level source directory) and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
12 ** \brief The main entry point into the CVC4 library's SMT interface
14 ** The main entry point into the CVC4 library's SMT interface.
17 #include "smt/smt_engine.h"
21 #include <unordered_map>
22 #include <unordered_set>
30 #include "base/configuration.h"
31 #include "base/configuration_private.h"
32 #include "base/exception.h"
33 #include "base/listener.h"
34 #include "base/modal_exception.h"
35 #include "base/output.h"
36 #include "context/cdhashmap.h"
37 #include "context/cdhashset.h"
38 #include "context/cdlist.h"
39 #include "context/context.h"
40 #include "decision/decision_engine.h"
41 #include "expr/attribute.h"
42 #include "expr/expr.h"
43 #include "expr/kind.h"
44 #include "expr/metakind.h"
45 #include "expr/node.h"
46 #include "expr/node_builder.h"
47 #include "expr/node_self_iterator.h"
48 #include "options/arith_options.h"
49 #include "options/arrays_options.h"
50 #include "options/base_options.h"
51 #include "options/booleans_options.h"
52 #include "options/bv_options.h"
53 #include "options/datatypes_options.h"
54 #include "options/decision_mode.h"
55 #include "options/decision_options.h"
56 #include "options/language.h"
57 #include "options/main_options.h"
58 #include "options/open_ostream.h"
59 #include "options/option_exception.h"
60 #include "options/printer_options.h"
61 #include "options/proof_options.h"
62 #include "options/prop_options.h"
63 #include "options/quantifiers_options.h"
64 #include "options/sep_options.h"
65 #include "options/set_language.h"
66 #include "options/smt_options.h"
67 #include "options/strings_options.h"
68 #include "options/theory_options.h"
69 #include "options/uf_options.h"
70 #include "printer/printer.h"
71 #include "proof/proof.h"
72 #include "proof/proof_manager.h"
73 #include "proof/theory_proof.h"
74 #include "proof/unsat_core.h"
75 #include "prop/prop_engine.h"
76 #include "smt/command.h"
77 #include "smt/command_list.h"
78 #include "smt/logic_request.h"
79 #include "smt/managed_ostreams.h"
80 #include "smt/smt_engine_scope.h"
81 #include "smt/term_formula_removal.h"
82 #include "smt/update_ostream.h"
83 #include "smt_util/boolean_simplification.h"
84 #include "smt_util/nary_builder.h"
85 #include "smt_util/node_visitor.h"
86 #include "theory/arith/pseudoboolean_proc.h"
87 #include "theory/booleans/circuit_propagator.h"
88 #include "theory/bv/bvintropow2.h"
89 #include "theory/bv/theory_bv_rewriter.h"
90 #include "theory/logic_info.h"
91 #include "theory/quantifiers/ce_guided_instantiation.h"
92 #include "theory/quantifiers/fun_def_process.h"
93 #include "theory/quantifiers/macros.h"
94 #include "theory/quantifiers/quantifiers_rewriter.h"
95 #include "theory/quantifiers/term_util.h"
96 #include "theory/sort_inference.h"
97 #include "theory/strings/theory_strings.h"
98 #include "theory/substitutions.h"
99 #include "theory/theory_engine.h"
100 #include "theory/theory_model.h"
101 #include "theory/theory_traits.h"
102 #include "util/hash.h"
103 #include "util/proof.h"
104 #include "util/resource_manager.h"
107 using namespace CVC4
;
108 using namespace CVC4::smt
;
109 using namespace CVC4::prop
;
110 using namespace CVC4::context
;
111 using namespace CVC4::theory
;
116 struct DeleteCommandFunction
: public std::unary_function
<const Command
*, void>
118 void operator()(const Command
* command
) { delete command
; }
121 void DeleteAndClearCommandVector(std::vector
<Command
*>& commands
) {
122 std::for_each(commands
.begin(), commands
.end(), DeleteCommandFunction());
126 /** Useful for counting the number of recursive calls. */
131 ScopeCounter(unsigned& d
) : d_depth(d
) {
140 * Representation of a defined function. We keep these around in
141 * SmtEngine to permit expanding definitions late (and lazily), to
142 * support getValue() over defined functions, to support user output
143 * in terms of defined functions, etc.
145 class DefinedFunction
{
147 vector
<Node
> d_formals
;
151 DefinedFunction(Node func
, vector
<Node
> formals
, Node formula
) :
156 Node
getFunction() const { return d_func
; }
157 vector
<Node
> getFormals() const { return d_formals
; }
158 Node
getFormula() const { return d_formula
; }
159 };/* class DefinedFunction */
161 class AssertionPipeline
{
162 vector
<Node
> d_nodes
;
166 size_t size() const { return d_nodes
.size(); }
168 void resize(size_t n
) { d_nodes
.resize(n
); }
169 void clear() { d_nodes
.clear(); }
171 Node
& operator[](size_t i
) { return d_nodes
[i
]; }
172 const Node
& operator[](size_t i
) const { return d_nodes
[i
]; }
173 void push_back(Node n
) { d_nodes
.push_back(n
); }
175 vector
<Node
>& ref() { return d_nodes
; }
176 const vector
<Node
>& ref() const { return d_nodes
; }
178 void replace(size_t i
, Node n
) {
179 PROOF( ProofManager::currentPM()->addDependence(n
, d_nodes
[i
]); );
182 };/* class AssertionPipeline */
184 struct SmtEngineStatistics
{
185 /** time spent in definition-expansion */
186 TimerStat d_definitionExpansionTime
;
187 /** time spent in non-clausal simplification */
188 TimerStat d_nonclausalSimplificationTime
;
189 /** time spent in miplib pass */
190 TimerStat d_miplibPassTime
;
191 /** number of assertions removed by miplib pass */
192 IntStat d_numMiplibAssertionsRemoved
;
193 /** number of constant propagations found during nonclausal simp */
194 IntStat d_numConstantProps
;
195 /** time spent in static learning */
196 TimerStat d_staticLearningTime
;
197 /** time spent in simplifying ITEs */
198 TimerStat d_simpITETime
;
199 /** time spent in simplifying ITEs */
200 TimerStat d_unconstrainedSimpTime
;
201 /** time spent removing ITEs */
202 TimerStat d_iteRemovalTime
;
203 /** time spent in theory preprocessing */
204 TimerStat d_theoryPreprocessTime
;
205 /** time spent in theory preprocessing */
206 TimerStat d_rewriteApplyToConstTime
;
207 /** time spent converting to CNF */
208 TimerStat d_cnfConversionTime
;
209 /** Num of assertions before ite removal */
210 IntStat d_numAssertionsPre
;
211 /** Num of assertions after ite removal */
212 IntStat d_numAssertionsPost
;
213 /** time spent in checkModel() */
214 TimerStat d_checkModelTime
;
215 /** time spent in checkProof() */
216 TimerStat d_checkProofTime
;
217 /** time spent in checkUnsatCore() */
218 TimerStat d_checkUnsatCoreTime
;
219 /** time spent in PropEngine::checkSat() */
220 TimerStat d_solveTime
;
221 /** time spent in pushing/popping */
222 TimerStat d_pushPopTime
;
223 /** time spent in processAssertions() */
224 TimerStat d_processAssertionsTime
;
226 /** Has something simplified to false? */
227 IntStat d_simplifiedToFalse
;
228 /** Number of resource units spent. */
229 ReferenceStat
<uint64_t> d_resourceUnitsUsed
;
231 SmtEngineStatistics() :
232 d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"),
233 d_nonclausalSimplificationTime("smt::SmtEngine::nonclausalSimplificationTime"),
234 d_miplibPassTime("smt::SmtEngine::miplibPassTime"),
235 d_numMiplibAssertionsRemoved("smt::SmtEngine::numMiplibAssertionsRemoved", 0),
236 d_numConstantProps("smt::SmtEngine::numConstantProps", 0),
237 d_staticLearningTime("smt::SmtEngine::staticLearningTime"),
238 d_simpITETime("smt::SmtEngine::simpITETime"),
239 d_unconstrainedSimpTime("smt::SmtEngine::unconstrainedSimpTime"),
240 d_iteRemovalTime("smt::SmtEngine::iteRemovalTime"),
241 d_theoryPreprocessTime("smt::SmtEngine::theoryPreprocessTime"),
242 d_rewriteApplyToConstTime("smt::SmtEngine::rewriteApplyToConstTime"),
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")
256 smtStatisticsRegistry()->registerStat(&d_definitionExpansionTime
);
257 smtStatisticsRegistry()->registerStat(&d_nonclausalSimplificationTime
);
258 smtStatisticsRegistry()->registerStat(&d_miplibPassTime
);
259 smtStatisticsRegistry()->registerStat(&d_numMiplibAssertionsRemoved
);
260 smtStatisticsRegistry()->registerStat(&d_numConstantProps
);
261 smtStatisticsRegistry()->registerStat(&d_staticLearningTime
);
262 smtStatisticsRegistry()->registerStat(&d_simpITETime
);
263 smtStatisticsRegistry()->registerStat(&d_unconstrainedSimpTime
);
264 smtStatisticsRegistry()->registerStat(&d_iteRemovalTime
);
265 smtStatisticsRegistry()->registerStat(&d_theoryPreprocessTime
);
266 smtStatisticsRegistry()->registerStat(&d_rewriteApplyToConstTime
);
267 smtStatisticsRegistry()->registerStat(&d_cnfConversionTime
);
268 smtStatisticsRegistry()->registerStat(&d_numAssertionsPre
);
269 smtStatisticsRegistry()->registerStat(&d_numAssertionsPost
);
270 smtStatisticsRegistry()->registerStat(&d_checkModelTime
);
271 smtStatisticsRegistry()->registerStat(&d_checkProofTime
);
272 smtStatisticsRegistry()->registerStat(&d_checkUnsatCoreTime
);
273 smtStatisticsRegistry()->registerStat(&d_solveTime
);
274 smtStatisticsRegistry()->registerStat(&d_pushPopTime
);
275 smtStatisticsRegistry()->registerStat(&d_processAssertionsTime
);
276 smtStatisticsRegistry()->registerStat(&d_simplifiedToFalse
);
277 smtStatisticsRegistry()->registerStat(&d_resourceUnitsUsed
);
280 ~SmtEngineStatistics() {
281 smtStatisticsRegistry()->unregisterStat(&d_definitionExpansionTime
);
282 smtStatisticsRegistry()->unregisterStat(&d_nonclausalSimplificationTime
);
283 smtStatisticsRegistry()->unregisterStat(&d_miplibPassTime
);
284 smtStatisticsRegistry()->unregisterStat(&d_numMiplibAssertionsRemoved
);
285 smtStatisticsRegistry()->unregisterStat(&d_numConstantProps
);
286 smtStatisticsRegistry()->unregisterStat(&d_staticLearningTime
);
287 smtStatisticsRegistry()->unregisterStat(&d_simpITETime
);
288 smtStatisticsRegistry()->unregisterStat(&d_unconstrainedSimpTime
);
289 smtStatisticsRegistry()->unregisterStat(&d_iteRemovalTime
);
290 smtStatisticsRegistry()->unregisterStat(&d_theoryPreprocessTime
);
291 smtStatisticsRegistry()->unregisterStat(&d_rewriteApplyToConstTime
);
292 smtStatisticsRegistry()->unregisterStat(&d_cnfConversionTime
);
293 smtStatisticsRegistry()->unregisterStat(&d_numAssertionsPre
);
294 smtStatisticsRegistry()->unregisterStat(&d_numAssertionsPost
);
295 smtStatisticsRegistry()->unregisterStat(&d_checkModelTime
);
296 smtStatisticsRegistry()->unregisterStat(&d_checkProofTime
);
297 smtStatisticsRegistry()->unregisterStat(&d_checkUnsatCoreTime
);
298 smtStatisticsRegistry()->unregisterStat(&d_solveTime
);
299 smtStatisticsRegistry()->unregisterStat(&d_pushPopTime
);
300 smtStatisticsRegistry()->unregisterStat(&d_processAssertionsTime
);
301 smtStatisticsRegistry()->unregisterStat(&d_simplifiedToFalse
);
302 smtStatisticsRegistry()->unregisterStat(&d_resourceUnitsUsed
);
304 };/* struct SmtEngineStatistics */
307 class SoftResourceOutListener
: public Listener
{
309 SoftResourceOutListener(SmtEngine
& smt
) : d_smt(&smt
) {}
310 virtual void notify() {
311 SmtScope
scope(d_smt
);
312 Assert(smt::smtEngineInScope());
317 }; /* class SoftResourceOutListener */
320 class HardResourceOutListener
: public Listener
{
322 HardResourceOutListener(SmtEngine
& smt
) : d_smt(&smt
) {}
323 virtual void notify() {
324 SmtScope
scope(d_smt
);
325 theory::Rewriter::clearCaches();
329 }; /* class HardResourceOutListener */
331 class SetLogicListener
: public Listener
{
333 SetLogicListener(SmtEngine
& smt
) : d_smt(&smt
) {}
334 virtual void notify() {
335 LogicInfo
inOptions(options::forceLogicString());
336 d_smt
->setLogic(inOptions
);
340 }; /* class SetLogicListener */
342 class BeforeSearchListener
: public Listener
{
344 BeforeSearchListener(SmtEngine
& smt
) : d_smt(&smt
) {}
345 virtual void notify() {
346 d_smt
->beforeSearch();
350 }; /* class BeforeSearchListener */
352 class UseTheoryListListener
: public Listener
{
354 UseTheoryListListener(TheoryEngine
* theoryEngine
)
355 : d_theoryEngine(theoryEngine
)
359 std::stringstream
commaList(options::useTheoryList());
362 Debug("UseTheoryListListener") << "UseTheoryListListener::notify() "
363 << options::useTheoryList() << std::endl
;
365 while(std::getline(commaList
, token
, ',')){
366 if(token
== "help") {
367 puts(theory::useTheoryHelp
);
370 if(theory::useTheoryValidate(token
)) {
371 d_theoryEngine
->enableTheoryAlternative(token
);
373 throw OptionException(
374 std::string("unknown option for --use-theory : `") + token
+
375 "'. Try --use-theory=help.");
381 TheoryEngine
* d_theoryEngine
;
382 }; /* class UseTheoryListListener */
385 class SetDefaultExprDepthListener
: public Listener
{
387 virtual void notify() {
388 int depth
= options::defaultExprDepth();
389 Debug
.getStream() << expr::ExprSetDepth(depth
);
390 Trace
.getStream() << expr::ExprSetDepth(depth
);
391 Notice
.getStream() << expr::ExprSetDepth(depth
);
392 Chat
.getStream() << expr::ExprSetDepth(depth
);
393 Message
.getStream() << expr::ExprSetDepth(depth
);
394 Warning
.getStream() << expr::ExprSetDepth(depth
);
395 // intentionally exclude Dump stream from this list
399 class SetDefaultExprDagListener
: public Listener
{
401 virtual void notify() {
402 int dag
= options::defaultDagThresh();
403 Debug
.getStream() << expr::ExprDag(dag
);
404 Trace
.getStream() << expr::ExprDag(dag
);
405 Notice
.getStream() << expr::ExprDag(dag
);
406 Chat
.getStream() << expr::ExprDag(dag
);
407 Message
.getStream() << expr::ExprDag(dag
);
408 Warning
.getStream() << expr::ExprDag(dag
);
409 Dump
.getStream() << expr::ExprDag(dag
);
413 class SetPrintExprTypesListener
: public Listener
{
415 virtual void notify() {
416 bool value
= options::printExprTypes();
417 Debug
.getStream() << expr::ExprPrintTypes(value
);
418 Trace
.getStream() << expr::ExprPrintTypes(value
);
419 Notice
.getStream() << expr::ExprPrintTypes(value
);
420 Chat
.getStream() << expr::ExprPrintTypes(value
);
421 Message
.getStream() << expr::ExprPrintTypes(value
);
422 Warning
.getStream() << expr::ExprPrintTypes(value
);
423 // intentionally exclude Dump stream from this list
427 class DumpModeListener
: public Listener
{
429 virtual void notify() {
430 const std::string
& value
= options::dumpModeString();
431 Dump
.setDumpFromString(value
);
435 class PrintSuccessListener
: public Listener
{
437 virtual void notify() {
438 bool value
= options::printSuccess();
439 Debug
.getStream() << Command::printsuccess(value
);
440 Trace
.getStream() << Command::printsuccess(value
);
441 Notice
.getStream() << Command::printsuccess(value
);
442 Chat
.getStream() << Command::printsuccess(value
);
443 Message
.getStream() << Command::printsuccess(value
);
444 Warning
.getStream() << Command::printsuccess(value
);
445 *options::out() << Command::printsuccess(value
);
452 * This is an inelegant solution, but for the present, it will work.
453 * The point of this is to separate the public and private portions of
454 * the SmtEngine class, so that smt_engine.h doesn't
455 * include "expr/node.h", which is a private CVC4 header (and can lead
456 * to linking errors due to the improper inlining of non-visible symbols
459 * The "real" solution (that which is usually implemented) is to move
460 * ALL the implementation to SmtEnginePrivate and maintain a
461 * heap-allocated instance of it in SmtEngine. SmtEngine (the public
462 * one) becomes an "interface shell" which simply acts as a forwarder
465 class SmtEnginePrivate
: public NodeManagerListener
{
468 typedef unordered_map
<Node
, Node
, NodeHashFunction
> NodeToNodeHashMap
;
469 typedef unordered_map
<Node
, bool, NodeHashFunction
> NodeToBoolHashMap
;
472 * Manager for limiting time and abstract resource usage.
474 ResourceManager
* d_resourceManager
;
476 /** Manager for the memory of regular-output-channel. */
477 ManagedRegularOutputChannel d_managedRegularChannel
;
479 /** Manager for the memory of diagnostic-output-channel. */
480 ManagedDiagnosticOutputChannel d_managedDiagnosticChannel
;
482 /** Manager for the memory of --dump-to. */
483 ManagedDumpOStream d_managedDumpChannel
;
485 /** Manager for --replay-log. */
486 ManagedReplayLogOstream d_managedReplayLog
;
489 * This list contains:
493 * beforeSearchListener
494 * UseTheoryListListener
496 * This needs to be deleted before both NodeManager's Options,
497 * SmtEngine, d_resourceManager, and TheoryEngine.
499 ListenerRegistrationList
* d_listenerRegistrations
;
501 /** Learned literals */
502 vector
<Node
> d_nonClausalLearnedLiterals
;
504 /** Size of assertions array when preprocessing starts */
505 unsigned d_realAssertionsEnd
;
507 /** A circuit propagator for non-clausal propositional deduction */
508 booleans::CircuitPropagator d_propagator
;
509 bool d_propagatorNeedsFinish
;
510 std::vector
<Node
> d_boolVars
;
512 /** Assertions in the preprocessing pipeline */
513 AssertionPipeline d_assertions
;
515 /** Whether any assertions have been processed */
516 CDO
<bool> d_assertionsProcessed
;
518 /** Index for where to store substitutions */
519 CDO
<unsigned> d_substitutionsIndex
;
525 * A context that never pushes/pops, for use by CD structures (like
526 * SubstitutionMaps) that should be "global".
528 context::Context d_fakeContext
;
531 * A map of AbsractValues to their actual constants. Only used if
532 * options::abstractValues() is on.
534 SubstitutionMap d_abstractValueMap
;
537 * A mapping of all abstract values (actual value |-> abstract) that
538 * we've handed out. This is necessary to ensure that we give the
539 * same AbstractValues for the same real constants. Only used if
540 * options::abstractValues() is on.
542 NodeToNodeHashMap d_abstractValues
;
544 /** Number of calls of simplify assertions active.
546 unsigned d_simplifyAssertionsDepth
;
548 /** TODO: whether certain preprocess steps are necessary */
549 //bool d_needsExpandDefs;
551 //------------------------------- expression names
552 /** mapping from expressions to name */
553 context::CDHashMap
< Node
, std::string
, NodeHashFunction
> d_exprNames
;
554 //------------------------------- end expression names
557 * Map from skolem variables to index in d_assertions containing
558 * corresponding introduced Boolean ite
560 IteSkolemMap d_iteSkolemMap
;
562 /** Instance of the ITE remover */
563 RemoveTermFormulas d_iteRemover
;
567 theory::arith::PseudoBooleanProcessor d_pbsProcessor
;
569 /** The top level substitutions */
570 SubstitutionMap d_topLevelSubstitutions
;
572 static const bool d_doConstantProp
= true;
575 * Runs the nonclausal solver and tries to solve all the assigned
578 * Returns false if the formula simplifies to "false"
580 bool nonClausalSimplify();
583 * Performs static learning on the assertions.
585 void staticLearning();
588 * Remove ITEs from the assertions.
592 Node
realToInt(TNode n
, NodeToNodeHashMap
& cache
, std::vector
< Node
>& var_eq
);
593 Node
intToBV(TNode n
, NodeToNodeHashMap
& cache
);
594 Node
intToBVMakeBinary(TNode n
, NodeToNodeHashMap
& cache
);
595 Node
purifyNlTerms(TNode n
, NodeToNodeHashMap
& cache
, NodeToNodeHashMap
& bcache
, std::vector
< Node
>& var_eq
, bool beneathMult
= false);
598 * Helper function to fix up assertion list to restore invariants needed after
601 void collectSkolems(TNode n
, set
<TNode
>& skolemSet
, NodeToBoolHashMap
& cache
);
604 * Helper function to fix up assertion list to restore invariants needed after
607 bool checkForBadSkolems(TNode n
, TNode skolem
, NodeToBoolHashMap
& cache
);
609 // Lift bit-vectors of size 1 to booleans
612 // Convert booleans to bit-vectors of size 1
615 // Abstract common structure over small domains to UF
616 // return true if changes were made.
617 void bvAbstraction();
619 // Simplify ITE structure
622 // Simplify based on unconstrained values
623 void unconstrainedSimp();
626 * Ensures the assertions asserted after before now effectively come before
627 * d_realAssertionsEnd.
629 void compressBeforeRealAssertions(size_t before
);
632 * Trace nodes back to their assertions using CircuitPropagator's
635 void traceBackToAssertions(const std::vector
<Node
>& nodes
,
636 std::vector
<TNode
>& assertions
);
639 * Remove conjuncts in toRemove from conjunction n. Return # of removed
642 size_t removeFromConjunction(Node
& n
,
643 const std::unordered_set
<unsigned long>& toRemove
);
645 /** Scrub miplib encodings. */
646 void doMiplibTrick();
649 * Perform non-clausal simplification of a Node. This involves
650 * Theory implementations, but does NOT involve the SAT solver in
653 * Returns false if the formula simplifies to "false"
655 bool simplifyAssertions() throw(TypeCheckingException
, LogicException
,
656 UnsafeInterruptException
);
660 SmtEnginePrivate(SmtEngine
& smt
) :
662 d_managedRegularChannel(),
663 d_managedDiagnosticChannel(),
664 d_managedDumpChannel(),
665 d_managedReplayLog(),
666 d_listenerRegistrations(new ListenerRegistrationList()),
667 d_nonClausalLearnedLiterals(),
668 d_realAssertionsEnd(0),
669 d_propagator(d_nonClausalLearnedLiterals
, true, true),
670 d_propagatorNeedsFinish(false),
672 d_assertionsProcessed(smt
.d_userContext
, false),
673 d_substitutionsIndex(smt
.d_userContext
, 0),
675 d_abstractValueMap(&d_fakeContext
),
677 d_simplifyAssertionsDepth(0),
678 //d_needsExpandDefs(true), //TODO?
679 d_exprNames(smt
.d_userContext
),
681 d_iteRemover(smt
.d_userContext
),
682 d_pbsProcessor(smt
.d_userContext
),
683 d_topLevelSubstitutions(smt
.d_userContext
)
685 d_smt
.d_nodeManager
->subscribeEvents(this);
686 d_true
= NodeManager::currentNM()->mkConst(true);
687 d_resourceManager
= NodeManager::currentResourceManager();
689 d_listenerRegistrations
->add(d_resourceManager
->registerSoftListener(
690 new SoftResourceOutListener(d_smt
)));
692 d_listenerRegistrations
->add(d_resourceManager
->registerHardListener(
693 new HardResourceOutListener(d_smt
)));
695 Options
& nodeManagerOptions
= NodeManager::currentNM()->getOptions();
696 d_listenerRegistrations
->add(
697 nodeManagerOptions
.registerForceLogicListener(
698 new SetLogicListener(d_smt
), true));
700 // Multiple options reuse BeforeSearchListener so registration requires an
701 // extra bit of care.
702 // We can safely not call notify on this before search listener at
703 // registration time. This d_smt cannot be beforeSearch at construction
704 // time. Therefore the BeforeSearchListener is a no-op. Therefore it does
705 // not have to be called.
706 d_listenerRegistrations
->add(
707 nodeManagerOptions
.registerBeforeSearchListener(
708 new BeforeSearchListener(d_smt
)));
710 // These do need registration calls.
711 d_listenerRegistrations
->add(
712 nodeManagerOptions
.registerSetDefaultExprDepthListener(
713 new SetDefaultExprDepthListener(), true));
714 d_listenerRegistrations
->add(
715 nodeManagerOptions
.registerSetDefaultExprDagListener(
716 new SetDefaultExprDagListener(), true));
717 d_listenerRegistrations
->add(
718 nodeManagerOptions
.registerSetPrintExprTypesListener(
719 new SetPrintExprTypesListener(), true));
720 d_listenerRegistrations
->add(
721 nodeManagerOptions
.registerSetDumpModeListener(
722 new DumpModeListener(), true));
723 d_listenerRegistrations
->add(
724 nodeManagerOptions
.registerSetPrintSuccessListener(
725 new PrintSuccessListener(), true));
726 d_listenerRegistrations
->add(
727 nodeManagerOptions
.registerSetRegularOutputChannelListener(
728 new SetToDefaultSourceListener(&d_managedRegularChannel
), true));
729 d_listenerRegistrations
->add(
730 nodeManagerOptions
.registerSetDiagnosticOutputChannelListener(
731 new SetToDefaultSourceListener(&d_managedDiagnosticChannel
), true));
732 d_listenerRegistrations
->add(
733 nodeManagerOptions
.registerDumpToFileNameListener(
734 new SetToDefaultSourceListener(&d_managedDumpChannel
), true));
735 d_listenerRegistrations
->add(
736 nodeManagerOptions
.registerSetReplayLogFilename(
737 new SetToDefaultSourceListener(&d_managedReplayLog
), true));
740 ~SmtEnginePrivate() throw() {
741 delete d_listenerRegistrations
;
743 if(d_propagatorNeedsFinish
) {
744 d_propagator
.finish();
745 d_propagatorNeedsFinish
= false;
747 d_smt
.d_nodeManager
->unsubscribeEvents(this);
750 ResourceManager
* getResourceManager() { return d_resourceManager
; }
751 void spendResource(unsigned amount
) throw(UnsafeInterruptException
) {
752 d_resourceManager
->spendResource(amount
);
755 void nmNotifyNewSort(TypeNode tn
, uint32_t flags
) {
756 DeclareTypeCommand
c(tn
.getAttribute(expr::VarNameAttr()),
759 if((flags
& ExprManager::SORT_FLAG_PLACEHOLDER
) == 0) {
760 d_smt
.addToModelCommandAndDump(c
, flags
);
764 void nmNotifyNewSortConstructor(TypeNode tn
) {
765 DeclareTypeCommand
c(tn
.getAttribute(expr::VarNameAttr()),
766 tn
.getAttribute(expr::SortArityAttr()),
768 d_smt
.addToModelCommandAndDump(c
);
771 void nmNotifyNewDatatypes(const std::vector
<DatatypeType
>& dtts
) {
772 DatatypeDeclarationCommand
c(dtts
);
773 d_smt
.addToModelCommandAndDump(c
);
776 void nmNotifyNewVar(TNode n
, uint32_t flags
) {
777 DeclareFunctionCommand
c(n
.getAttribute(expr::VarNameAttr()),
779 n
.getType().toType());
780 if((flags
& ExprManager::VAR_FLAG_DEFINED
) == 0) {
781 d_smt
.addToModelCommandAndDump(c
, flags
);
783 if(n
.getType().isBoolean() && !options::incrementalSolving()) {
784 d_boolVars
.push_back(n
);
788 void nmNotifyNewSkolem(TNode n
, const std::string
& comment
, uint32_t flags
) {
789 string id
= n
.getAttribute(expr::VarNameAttr());
790 DeclareFunctionCommand
c(id
,
792 n
.getType().toType());
793 if(Dump
.isOn("skolems") && comment
!= "") {
794 Dump("skolems") << CommentCommand(id
+ " is " + comment
);
796 if((flags
& ExprManager::VAR_FLAG_DEFINED
) == 0) {
797 d_smt
.addToModelCommandAndDump(c
, flags
, false, "skolems");
799 if(n
.getType().isBoolean() && !options::incrementalSolving()) {
800 d_boolVars
.push_back(n
);
804 void nmNotifyDeleteNode(TNode n
) {}
806 Node
applySubstitutions(TNode node
) const {
807 return Rewriter::rewrite(d_topLevelSubstitutions
.apply(node
));
811 * Apply the substitutions in d_topLevelAssertions and the rewriter to each of
812 * the assertions in d_assertions, and store the result back in d_assertions.
814 void applySubstitutionsToAssertions();
817 * Process the assertions that have been asserted.
819 void processAssertions();
821 /** Process a user push.
828 * Process a user pop. Clears out the non-context-dependent stuff in this
829 * SmtEnginePrivate. Necessary to clear out our assertion vectors in case
830 * someone does a push-assert-pop without a check-sat. It also pops the
831 * last map of expression names from notifyPush.
834 d_assertions
.clear();
835 d_nonClausalLearnedLiterals
.clear();
836 d_realAssertionsEnd
= 0;
837 d_iteSkolemMap
.clear();
841 * Adds a formula to the current context. Action here depends on
842 * the SimplificationMode (in the current Options scope); the
843 * formula might be pushed out to the propositional layer
844 * immediately, or it might be simplified and kept, or it might not
845 * even be simplified.
846 * the 2nd and 3rd arguments added for bookkeeping for proofs
848 void addFormula(TNode n
, bool inUnsatCore
, bool inInput
= true)
849 throw(TypeCheckingException
, LogicException
);
851 /** Expand definitions in n. */
852 Node
expandDefinitions(TNode n
, NodeToNodeHashMap
& cache
,
853 bool expandOnly
= false)
854 throw(TypeCheckingException
, LogicException
, UnsafeInterruptException
);
857 * Simplify node "in" by expanding definitions and applying any
858 * substitutions learned from preprocessing.
860 Node
simplify(TNode in
) {
861 // Substitute out any abstract values in ex.
862 // Expand definitions.
863 NodeToNodeHashMap cache
;
864 Node n
= expandDefinitions(in
, cache
).toExpr();
865 // Make sure we've done all preprocessing, etc.
866 Assert(d_assertions
.size() == 0);
867 return applySubstitutions(n
).toExpr();
871 * Substitute away all AbstractValues in a node.
873 Node
substituteAbstractValues(TNode n
) {
874 // We need to do this even if options::abstractValues() is off,
875 // since the setting might have changed after we already gave out
876 // some abstract values.
877 return d_abstractValueMap
.apply(n
);
881 * Make a new (or return an existing) abstract value for a node.
882 * Can only use this if options::abstractValues() is on.
884 Node
mkAbstractValue(TNode n
) {
885 Assert(options::abstractValues());
886 Node
& val
= d_abstractValues
[n
];
888 val
= d_smt
.d_nodeManager
->mkAbstractValue(n
.getType());
889 d_abstractValueMap
.addSubstitution(val
, n
);
891 // We are supposed to ascribe types to all abstract values that go out.
892 NodeManager
* current
= d_smt
.d_nodeManager
;
893 Node ascription
= current
->mkConst(AscriptionType(n
.getType().toType()));
894 Node retval
= current
->mkNode(kind::APPLY_TYPE_ASCRIPTION
, ascription
, val
);
898 NodeToNodeHashMap d_rewriteApplyToConstCache
;
899 Node
rewriteApplyToConst(TNode n
) {
900 Trace("rewriteApplyToConst") << "rewriteApplyToConst :: " << n
<< std::endl
;
902 if(n
.getMetaKind() == kind::metakind::CONSTANT
||
903 n
.getMetaKind() == kind::metakind::VARIABLE
||
904 n
.getMetaKind() == kind::metakind::NULLARY_OPERATOR
)
909 if(d_rewriteApplyToConstCache
.find(n
) != d_rewriteApplyToConstCache
.end()) {
910 Trace("rewriteApplyToConst") << "in cache :: "
911 << d_rewriteApplyToConstCache
[n
]
913 return d_rewriteApplyToConstCache
[n
];
916 if(n
.getKind() == kind::APPLY_UF
) {
917 if(n
.getNumChildren() == 1 && n
[0].isConst() &&
918 n
[0].getType().isInteger())
921 ss
<< n
.getOperator() << "_";
922 if(n
[0].getConst
<Rational
>() < 0) {
923 ss
<< "m" << -n
[0].getConst
<Rational
>();
927 Node newvar
= NodeManager::currentNM()->mkSkolem(
928 ss
.str(), n
.getType(), "rewriteApplyToConst skolem",
929 NodeManager::SKOLEM_EXACT_NAME
);
930 d_rewriteApplyToConstCache
[n
] = newvar
;
931 Trace("rewriteApplyToConst") << "made :: " << newvar
<< std::endl
;
935 ss
<< "The rewrite-apply-to-const preprocessor is currently limited;"
937 << "it only works if all function symbols are unary and with Integer"
939 << "domain, and all applications are to integer values." << std::endl
940 << "Found application: " << n
;
945 NodeBuilder
<> builder(n
.getKind());
946 if(n
.getMetaKind() == kind::metakind::PARAMETERIZED
) {
947 builder
<< n
.getOperator();
949 for(unsigned i
= 0; i
< n
.getNumChildren(); ++i
) {
950 builder
<< rewriteApplyToConst(n
[i
]);
953 d_rewriteApplyToConstCache
[n
] = rewr
;
954 Trace("rewriteApplyToConst") << "built :: " << rewr
<< std::endl
;
958 void addUseTheoryListListener(TheoryEngine
* theoryEngine
){
959 Options
& nodeManagerOptions
= NodeManager::currentNM()->getOptions();
960 d_listenerRegistrations
->add(
961 nodeManagerOptions
.registerUseTheoryListListener(
962 new UseTheoryListListener(theoryEngine
), true));
965 std::ostream
* getReplayLog() const {
966 return d_managedReplayLog
.getReplayLog();
969 //------------------------------- expression names
970 // implements setExpressionName, as described in smt_engine.h
971 void setExpressionName(Expr e
, std::string name
) {
972 d_exprNames
[Node::fromExpr(e
)] = name
;
975 // implements getExpressionName, as described in smt_engine.h
976 bool getExpressionName(Expr e
, std::string
& name
) const {
977 context::CDHashMap
< Node
, std::string
, NodeHashFunction
>::const_iterator it
= d_exprNames
.find(e
);
978 if(it
!=d_exprNames
.end()) {
985 //------------------------------- end expression names
987 };/* class SmtEnginePrivate */
989 }/* namespace CVC4::smt */
991 SmtEngine::SmtEngine(ExprManager
* em
) throw() :
992 d_context(new Context()),
994 d_userContext(new UserContext()),
996 d_nodeManager(d_exprManager
->getNodeManager()),
997 d_decisionEngine(NULL
),
998 d_theoryEngine(NULL
),
1000 d_proofManager(NULL
),
1001 d_definedFunctions(NULL
),
1002 d_fmfRecFunctionsDefined(NULL
),
1003 d_assertionList(NULL
),
1004 d_assignments(NULL
),
1005 d_modelGlobalCommands(),
1006 d_modelCommands(NULL
),
1010 d_originalOptions(),
1012 d_fullyInited(false),
1013 d_problemExtended(false),
1015 d_needPostsolve(false),
1016 d_earlyTheoryPP(true),
1018 d_replayStream(NULL
),
1020 d_statisticsRegistry(NULL
),
1022 d_channels(new LemmaChannels())
1024 SmtScope
smts(this);
1025 d_originalOptions
.copyValues(em
->getOptions());
1026 d_private
= new smt::SmtEnginePrivate(*this);
1027 d_statisticsRegistry
= new StatisticsRegistry();
1028 d_stats
= new SmtEngineStatistics();
1029 d_stats
->d_resourceUnitsUsed
.setData(
1030 d_private
->getResourceManager()->getResourceUsage());
1032 // The ProofManager is constructed before any other proof objects such as
1033 // SatProof and TheoryProofs. The TheoryProofEngine and the SatProof are
1034 // initialized in TheoryEngine and PropEngine respectively.
1035 Assert(d_proofManager
== NULL
);
1037 // d_proofManager must be created before Options has been finished
1038 // being parsed from the input file. Because of this, we cannot trust
1039 // that options::proof() is set correctly yet.
1041 d_proofManager
= new ProofManager(d_userContext
);
1044 // We have mutual dependency here, so we add the prop engine to the theory
1045 // engine later (it is non-essential there)
1046 d_theoryEngine
= new TheoryEngine(d_context
, d_userContext
,
1047 d_private
->d_iteRemover
,
1048 const_cast<const LogicInfo
&>(d_logic
),
1052 for(TheoryId id
= theory::THEORY_FIRST
; id
< theory::THEORY_LAST
; ++id
) {
1053 TheoryConstructor::addTheory(d_theoryEngine
, id
);
1054 //register with proof engine if applicable
1056 ProofManager::currentPM()->getTheoryProofEngine()->registerTheory(d_theoryEngine
->theoryOf(id
));
1060 d_private
->addUseTheoryListListener(d_theoryEngine
);
1062 // global push/pop around everything, to ensure proper destruction
1063 // of context-dependent data structures
1064 d_userContext
->push();
1067 d_definedFunctions
= new(true) DefinedFunctionMap(d_userContext
);
1068 d_fmfRecFunctionsDefined
= new(true) NodeList(d_userContext
);
1069 d_modelCommands
= new(true) smt::CommandList(d_userContext
);
1072 void SmtEngine::finishInit() {
1073 Trace("smt-debug") << "SmtEngine::finishInit" << std::endl
;
1074 // ensure that our heuristics are properly set up
1077 Trace("smt-debug") << "Making decision engine..." << std::endl
;
1079 d_decisionEngine
= new DecisionEngine(d_context
, d_userContext
);
1080 d_decisionEngine
->init(); // enable appropriate strategies
1082 Trace("smt-debug") << "Making prop engine..." << std::endl
;
1083 d_propEngine
= new PropEngine(d_theoryEngine
, d_decisionEngine
, d_context
,
1084 d_userContext
, d_private
->getReplayLog(),
1085 d_replayStream
, d_channels
);
1087 Trace("smt-debug") << "Setting up theory engine..." << std::endl
;
1088 d_theoryEngine
->setPropEngine(d_propEngine
);
1089 d_theoryEngine
->setDecisionEngine(d_decisionEngine
);
1090 Trace("smt-debug") << "Finishing init for theory engine..." << std::endl
;
1091 d_theoryEngine
->finishInit();
1093 Trace("smt-debug") << "Set up assertion list..." << std::endl
;
1094 // [MGD 10/20/2011] keep around in incremental mode, due to a
1095 // cleanup ordering issue and Nodes/TNodes. If SAT is popped
1096 // first, some user-context-dependent TNodes might still exist
1098 if(options::produceAssertions() ||
1099 options::incrementalSolving()) {
1100 // In the case of incremental solving, we appear to need these to
1101 // ensure the relevant Nodes remain live.
1102 d_assertionList
= new(true) AssertionList(d_userContext
);
1105 // dump out a set-logic command
1106 if(Dump
.isOn("benchmark")) {
1107 if (Dump
.isOn("raw-benchmark")) {
1108 Dump("raw-benchmark") << SetBenchmarkLogicCommand(d_logic
.getLogicString());
1110 LogicInfo everything
;
1112 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.")
1113 << SetBenchmarkLogicCommand(everything
.getLogicString());
1117 Trace("smt-debug") << "Dump declaration commands..." << std::endl
;
1118 // dump out any pending declaration commands
1119 for(unsigned i
= 0; i
< d_dumpCommands
.size(); ++i
) {
1120 Dump("declarations") << *d_dumpCommands
[i
];
1121 delete d_dumpCommands
[i
];
1123 d_dumpCommands
.clear();
1125 PROOF( ProofManager::currentPM()->setLogic(d_logic
); );
1127 for(TheoryId id
= theory::THEORY_FIRST
; id
< theory::THEORY_LAST
; ++id
) {
1128 ProofManager::currentPM()->getTheoryProofEngine()->
1129 finishRegisterTheory(d_theoryEngine
->theoryOf(id
));
1133 Trace("smt-debug") << "SmtEngine::finishInit done" << std::endl
;
1136 void SmtEngine::finalOptionsAreSet() {
1141 if(! d_logic
.isLocked()) {
1145 // finish initialization, create the prop engine, etc.
1148 AlwaysAssert( d_propEngine
->getAssertionLevel() == 0,
1149 "The PropEngine has pushed but the SmtEngine "
1150 "hasn't finished initializing!" );
1152 d_fullyInited
= true;
1153 Assert(d_logic
.isLocked());
1155 d_propEngine
->assertFormula(NodeManager::currentNM()->mkConst
<bool>(true));
1156 d_propEngine
->assertFormula(NodeManager::currentNM()->mkConst
<bool>(false).notNode());
1159 void SmtEngine::shutdown() {
1162 while(options::incrementalSolving() && d_userContext
->getLevel() > 1) {
1166 // check to see if a postsolve() is pending
1167 if(d_needPostsolve
) {
1168 d_theoryEngine
->postsolve();
1169 d_needPostsolve
= false;
1172 if(d_propEngine
!= NULL
) {
1173 d_propEngine
->shutdown();
1175 if(d_theoryEngine
!= NULL
) {
1176 d_theoryEngine
->shutdown();
1178 if(d_decisionEngine
!= NULL
) {
1179 d_decisionEngine
->shutdown();
1183 SmtEngine::~SmtEngine() throw() {
1184 SmtScope
smts(this);
1189 // global push/pop around everything, to ensure proper destruction
1190 // of context-dependent data structures
1191 d_context
->popto(0);
1192 d_userContext
->popto(0);
1194 if(d_assignments
!= NULL
) {
1195 d_assignments
->deleteSelf();
1198 if(d_assertionList
!= NULL
) {
1199 d_assertionList
->deleteSelf();
1202 for(unsigned i
= 0; i
< d_dumpCommands
.size(); ++i
) {
1203 delete d_dumpCommands
[i
];
1204 d_dumpCommands
[i
] = NULL
;
1206 d_dumpCommands
.clear();
1208 DeleteAndClearCommandVector(d_modelGlobalCommands
);
1210 if(d_modelCommands
!= NULL
) {
1211 d_modelCommands
->deleteSelf();
1214 d_definedFunctions
->deleteSelf();
1215 d_fmfRecFunctionsDefined
->deleteSelf();
1217 delete d_theoryEngine
;
1218 d_theoryEngine
= NULL
;
1219 delete d_propEngine
;
1220 d_propEngine
= NULL
;
1221 delete d_decisionEngine
;
1222 d_decisionEngine
= NULL
;
1225 // d_proofManager is always created when proofs are enabled at configure time.
1226 // Becuase of this, this code should not be wrapped in PROOF() which
1227 // additionally checks flags such as options::proof().
1229 delete d_proofManager
;
1230 d_proofManager
= NULL
;
1235 delete d_statisticsRegistry
;
1236 d_statisticsRegistry
= NULL
;
1241 delete d_userContext
;
1242 d_userContext
= NULL
;
1249 } catch(Exception
& e
) {
1250 Warning() << "CVC4 threw an exception during cleanup." << endl
1255 void SmtEngine::setLogic(const LogicInfo
& logic
) throw(ModalException
) {
1256 SmtScope
smts(this);
1258 throw ModalException("Cannot set logic in SmtEngine after the engine has "
1259 "finished initializing.");
1265 void SmtEngine::setLogic(const std::string
& s
)
1266 throw(ModalException
, LogicException
) {
1267 SmtScope
smts(this);
1269 setLogic(LogicInfo(s
));
1270 } catch(IllegalArgumentException
& e
) {
1271 throw LogicException(e
.what());
1275 void SmtEngine::setLogic(const char* logic
)
1276 throw(ModalException
, LogicException
) {
1277 setLogic(string(logic
));
1280 LogicInfo
SmtEngine::getLogicInfo() const {
1284 void SmtEngine::setLogicInternal() throw() {
1285 Assert(!d_fullyInited
, "setting logic in SmtEngine but the engine has already"
1286 " finished initializing for this run");
1290 void SmtEngine::setDefaults() {
1291 // Language-based defaults
1292 if (!options::bitvectorDivByZeroConst
.wasSetByUser())
1294 options::bitvectorDivByZeroConst
.set(options::inputLanguage()
1295 == language::input::LANG_SMTLIB_V2_6
);
1297 if (options::inputLanguage() == language::input::LANG_SYGUS
)
1299 if (!options::ceGuidedInst
.wasSetByUser())
1301 options::ceGuidedInst
.set(true);
1305 if(options::forceLogicString
.wasSetByUser()) {
1306 d_logic
= LogicInfo(options::forceLogicString());
1307 }else if (options::solveIntAsBV() > 0) {
1308 d_logic
= LogicInfo("QF_BV");
1309 }else if (d_logic
.getLogicString() == "QF_NRA" && options::solveRealAsInt()) {
1310 d_logic
= LogicInfo("QF_NIA");
1311 } else if ((d_logic
.getLogicString() == "QF_UFBV" ||
1312 d_logic
.getLogicString() == "QF_ABV") &&
1313 options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
) {
1314 d_logic
= LogicInfo("QF_BV");
1318 /* - disabled for 1.4 release [MGD 2014.06.25]
1319 if(!d_logic.hasEverything() && d_logic.isTheoryEnabled(THEORY_STRINGS) ) {
1320 if(! options::stringExp.wasSetByUser()) {
1321 options::stringExp.set( true );
1322 Trace("smt") << "turning on strings-exp, for the theory of strings" << std::endl;
1327 if(options::stringExp()) {
1328 if( !d_logic
.isQuantified() ) {
1329 d_logic
= d_logic
.getUnlockedCopy();
1330 d_logic
.enableQuantifiers();
1332 Trace("smt") << "turning on quantifier logic, for strings-exp"
1335 if(! options::fmfBound
.wasSetByUser()) {
1336 options::fmfBound
.set( true );
1337 Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl
;
1339 if(! options::fmfInstEngine
.wasSetByUser()) {
1340 options::fmfInstEngine
.set( true );
1341 Trace("smt") << "turning on fmf-inst-engine, for strings-exp" << std::endl
;
1344 if(! options::rewriteDivk.wasSetByUser()) {
1345 options::rewriteDivk.set( true );
1346 Trace("smt") << "turning on rewrite-divk, for strings-exp" << std::endl;
1349 if(! options::stringFMF.wasSetByUser()) {
1350 options::stringFMF.set( true );
1351 Trace("smt") << "turning on strings-fmf, for strings-exp" << std::endl;
1356 if(options::checkModels()) {
1357 if(! options::produceAssertions()) {
1358 Notice() << "SmtEngine: turning on produce-assertions to support "
1359 << "check-models." << endl
;
1360 setOption("produce-assertions", SExpr("true"));
1364 if(options::unsatCores()) {
1365 if(options::simplificationMode() != SIMPLIFICATION_MODE_NONE
) {
1366 if(options::simplificationMode
.wasSetByUser()) {
1367 throw OptionException("simplification not supported with unsat cores");
1369 Notice() << "SmtEngine: turning off simplification to support unsat-cores"
1371 options::simplificationMode
.set(SIMPLIFICATION_MODE_NONE
);
1374 if(options::unconstrainedSimp()) {
1375 if(options::unconstrainedSimp
.wasSetByUser()) {
1376 throw OptionException("unconstrained simplification not supported with unsat cores");
1378 Notice() << "SmtEngine: turning off unconstrained simplification to support unsat-cores" << endl
;
1379 options::unconstrainedSimp
.set(false);
1382 if(options::pbRewrites()) {
1383 if(options::pbRewrites
.wasSetByUser()) {
1384 throw OptionException("pseudoboolean rewrites not supported with unsat cores");
1386 Notice() << "SmtEngine: turning off pseudoboolean rewrites to support unsat-cores" << endl
;
1387 setOption("pb-rewrites", false);
1390 if(options::sortInference()) {
1391 if(options::sortInference
.wasSetByUser()) {
1392 throw OptionException("sort inference not supported with unsat cores");
1394 Notice() << "SmtEngine: turning off sort inference to support unsat-cores" << endl
;
1395 options::sortInference
.set(false);
1398 if(options::preSkolemQuant()) {
1399 if(options::preSkolemQuant
.wasSetByUser()) {
1400 throw OptionException("pre-skolemization not supported with unsat cores");
1402 Notice() << "SmtEngine: turning off pre-skolemization to support unsat-cores" << endl
;
1403 options::preSkolemQuant
.set(false);
1406 if(options::bitvectorToBool()) {
1407 if(options::bitvectorToBool
.wasSetByUser()) {
1408 throw OptionException("bv-to-bool not supported with unsat cores");
1410 Notice() << "SmtEngine: turning off bitvector-to-bool to support unsat-cores" << endl
;
1411 options::bitvectorToBool
.set(false);
1414 if(options::boolToBitvector()) {
1415 if(options::boolToBitvector
.wasSetByUser()) {
1416 throw OptionException("bool-to-bv not supported with unsat cores");
1418 Notice() << "SmtEngine: turning off bool-to-bitvector to support unsat-cores" << endl
;
1419 options::boolToBitvector
.set(false);
1422 if(options::bvIntroducePow2()) {
1423 if(options::bvIntroducePow2
.wasSetByUser()) {
1424 throw OptionException("bv-intro-pow2 not supported with unsat cores");
1426 Notice() << "SmtEngine: turning off bv-introduce-pow2 to support unsat-cores" << endl
;
1427 setOption("bv-intro-pow2", false);
1429 if(options::repeatSimp()) {
1430 if(options::repeatSimp
.wasSetByUser()) {
1431 throw OptionException("repeat-simp not supported with unsat cores");
1433 Notice() << "SmtEngine: turning off repeat-simp to support unsat-cores" << endl
;
1434 setOption("repeat-simp", false);
1438 if (options::cbqiBv()) {
1439 if(options::boolToBitvector
.wasSetByUser()) {
1440 throw OptionException("bool-to-bv not supported with CBQI BV");
1442 Notice() << "SmtEngine: turning off bool-to-bitvector to support CBQI BV"
1444 options::boolToBitvector
.set(false);
1447 if(options::produceAssignments() && !options::produceModels()) {
1448 Notice() << "SmtEngine: turning on produce-models to support produce-assignments" << endl
;
1449 setOption("produce-models", SExpr("true"));
1452 // Set the options for the theoryOf
1453 if(!options::theoryOfMode
.wasSetByUser()) {
1454 if(d_logic
.isSharingEnabled() &&
1455 !d_logic
.isTheoryEnabled(THEORY_BV
) &&
1456 !d_logic
.isTheoryEnabled(THEORY_STRINGS
) &&
1457 !d_logic
.isTheoryEnabled(THEORY_SETS
) ) {
1458 Trace("smt") << "setting theoryof-mode to term-based" << endl
;
1459 options::theoryOfMode
.set(THEORY_OF_TERM_BASED
);
1463 // strings require LIA, UF; widen the logic
1464 if(d_logic
.isTheoryEnabled(THEORY_STRINGS
)) {
1465 LogicInfo
log(d_logic
.getUnlockedCopy());
1466 // Strings requires arith for length constraints, and also UF
1467 if(!d_logic
.isTheoryEnabled(THEORY_UF
)) {
1468 Trace("smt") << "because strings are enabled, also enabling UF" << endl
;
1469 log
.enableTheory(THEORY_UF
);
1471 if(!d_logic
.isTheoryEnabled(THEORY_ARITH
) || d_logic
.isDifferenceLogic() || !d_logic
.areIntegersUsed()) {
1472 Trace("smt") << "because strings are enabled, also enabling linear integer arithmetic" << endl
;
1473 log
.enableTheory(THEORY_ARITH
);
1474 log
.enableIntegers();
1475 log
.arithOnlyLinear();
1480 if(d_logic
.isTheoryEnabled(THEORY_ARRAY
) || d_logic
.isTheoryEnabled(THEORY_DATATYPES
) || d_logic
.isTheoryEnabled(THEORY_SETS
)) {
1481 if(!d_logic
.isTheoryEnabled(THEORY_UF
)) {
1482 LogicInfo
log(d_logic
.getUnlockedCopy());
1483 Trace("smt") << "because a theory that permits Boolean terms is enabled, also enabling UF" << endl
;
1484 log
.enableTheory(THEORY_UF
);
1490 // by default, symmetry breaker is on only for QF_UF
1491 if(! options::ufSymmetryBreaker
.wasSetByUser()) {
1492 bool qf_uf
= d_logic
.isPure(THEORY_UF
) && !d_logic
.isQuantified() && !options::proof();
1493 Trace("smt") << "setting uf symmetry breaker to " << qf_uf
<< endl
;
1494 options::ufSymmetryBreaker
.set(qf_uf
);
1496 // by default, nonclausal simplification is off for QF_SAT
1497 if(! options::simplificationMode
.wasSetByUser()) {
1498 bool qf_sat
= d_logic
.isPure(THEORY_BOOL
) && !d_logic
.isQuantified();
1499 Trace("smt") << "setting simplification mode to <" << d_logic
.getLogicString() << "> " << (!qf_sat
) << endl
;
1500 //simplification=none works better for SMT LIB benchmarks with quantifiers, not others
1501 //options::simplificationMode.set(qf_sat || quantifiers ? SIMPLIFICATION_MODE_NONE : SIMPLIFICATION_MODE_BATCH);
1502 options::simplificationMode
.set(qf_sat
? SIMPLIFICATION_MODE_NONE
: SIMPLIFICATION_MODE_BATCH
);
1505 // If in arrays, set the UF handler to arrays
1506 if(d_logic
.isTheoryEnabled(THEORY_ARRAY
) && ( !d_logic
.isQuantified() ||
1507 (d_logic
.isQuantified() && !d_logic
.isTheoryEnabled(THEORY_UF
)))) {
1508 Theory::setUninterpretedSortOwner(THEORY_ARRAY
);
1510 Theory::setUninterpretedSortOwner(THEORY_UF
);
1513 // Turn on ite simplification for QF_LIA and QF_AUFBV
1514 // WARNING: These checks match much more than just QF_AUFBV and
1515 // QF_LIA logics. --K [2014/10/15]
1516 if(! options::doITESimp
.wasSetByUser()) {
1517 bool qf_aufbv
= !d_logic
.isQuantified() &&
1518 d_logic
.isTheoryEnabled(THEORY_ARRAY
) &&
1519 d_logic
.isTheoryEnabled(THEORY_UF
) &&
1520 d_logic
.isTheoryEnabled(THEORY_BV
);
1521 bool qf_lia
= !d_logic
.isQuantified() &&
1522 d_logic
.isPure(THEORY_ARITH
) &&
1523 d_logic
.isLinear() &&
1524 !d_logic
.isDifferenceLogic() &&
1525 !d_logic
.areRealsUsed();
1527 bool iteSimp
= (qf_aufbv
|| qf_lia
);
1528 Trace("smt") << "setting ite simplification to " << iteSimp
<< endl
;
1529 options::doITESimp
.set(iteSimp
);
1531 if(! options::compressItes
.wasSetByUser() ){
1532 bool qf_lia
= !d_logic
.isQuantified() &&
1533 d_logic
.isPure(THEORY_ARITH
) &&
1534 d_logic
.isLinear() &&
1535 !d_logic
.isDifferenceLogic() &&
1536 !d_logic
.areRealsUsed();
1538 bool compressIte
= qf_lia
;
1539 Trace("smt") << "setting ite compression to " << compressIte
<< endl
;
1540 options::compressItes
.set(compressIte
);
1542 if(! options::simplifyWithCareEnabled
.wasSetByUser() ){
1543 bool qf_aufbv
= !d_logic
.isQuantified() &&
1544 d_logic
.isTheoryEnabled(THEORY_ARRAY
) &&
1545 d_logic
.isTheoryEnabled(THEORY_UF
) &&
1546 d_logic
.isTheoryEnabled(THEORY_BV
);
1548 bool withCare
= qf_aufbv
;
1549 Trace("smt") << "setting ite simplify with care to " << withCare
<< endl
;
1550 options::simplifyWithCareEnabled
.set(withCare
);
1552 // Turn off array eager index splitting for QF_AUFLIA
1553 if(! options::arraysEagerIndexSplitting
.wasSetByUser()) {
1554 if (not d_logic
.isQuantified() &&
1555 d_logic
.isTheoryEnabled(THEORY_ARRAY
) &&
1556 d_logic
.isTheoryEnabled(THEORY_UF
) &&
1557 d_logic
.isTheoryEnabled(THEORY_ARITH
)) {
1558 Trace("smt") << "setting array eager index splitting to false" << endl
;
1559 options::arraysEagerIndexSplitting
.set(false);
1562 // Turn on model-based arrays for QF_AX (unless models are enabled)
1563 // if(! options::arraysModelBased.wasSetByUser()) {
1564 // if (not d_logic.isQuantified() &&
1565 // d_logic.isTheoryEnabled(THEORY_ARRAY) &&
1566 // d_logic.isPure(THEORY_ARRAY) &&
1567 // !options::produceModels() &&
1568 // !options::checkModels()) {
1569 // Trace("smt") << "turning on model-based array solver" << endl;
1570 // options::arraysModelBased.set(true);
1573 // Turn on multiple-pass non-clausal simplification for QF_AUFBV
1574 if(! options::repeatSimp
.wasSetByUser()) {
1575 bool repeatSimp
= !d_logic
.isQuantified() &&
1576 (d_logic
.isTheoryEnabled(THEORY_ARRAY
) &&
1577 d_logic
.isTheoryEnabled(THEORY_UF
) &&
1578 d_logic
.isTheoryEnabled(THEORY_BV
)) &&
1579 !options::unsatCores();
1580 Trace("smt") << "setting repeat simplification to " << repeatSimp
<< endl
;
1581 options::repeatSimp
.set(repeatSimp
);
1583 // Turn on unconstrained simplification for QF_AUFBV
1584 if(!options::unconstrainedSimp
.wasSetByUser() ||
1585 options::incrementalSolving()) {
1586 // bool qf_sat = d_logic.isPure(THEORY_BOOL) && !d_logic.isQuantified();
1587 // bool uncSimp = false && !qf_sat && !options::incrementalSolving();
1588 bool uncSimp
= !options::incrementalSolving() &&
1589 !d_logic
.isQuantified() &&
1590 !options::produceModels() &&
1591 !options::produceAssignments() &&
1592 !options::checkModels() &&
1593 !options::unsatCores() &&
1594 (d_logic
.isTheoryEnabled(THEORY_ARRAY
) && d_logic
.isTheoryEnabled(THEORY_BV
));
1595 Trace("smt") << "setting unconstrained simplification to " << uncSimp
<< endl
;
1596 options::unconstrainedSimp
.set(uncSimp
);
1598 // Unconstrained simp currently does *not* support model generation
1599 if (options::unconstrainedSimp
.wasSetByUser() && options::unconstrainedSimp()) {
1600 if (options::produceModels()) {
1601 if (options::produceModels
.wasSetByUser()) {
1602 throw OptionException("Cannot use unconstrained-simp with model generation.");
1604 Notice() << "SmtEngine: turning off produce-models to support unconstrainedSimp" << endl
;
1605 setOption("produce-models", SExpr("false"));
1607 if (options::produceAssignments()) {
1608 if (options::produceAssignments
.wasSetByUser()) {
1609 throw OptionException("Cannot use unconstrained-simp with model generation (produce-assignments).");
1611 Notice() << "SmtEngine: turning off produce-assignments to support unconstrainedSimp" << endl
;
1612 setOption("produce-assignments", SExpr("false"));
1614 if (options::checkModels()) {
1615 if (options::checkModels
.wasSetByUser()) {
1616 throw OptionException("Cannot use unconstrained-simp with model generation (check-models).");
1618 Notice() << "SmtEngine: turning off check-models to support unconstrainedSimp" << endl
;
1619 setOption("check-models", SExpr("false"));
1624 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
&&
1625 options::incrementalSolving()) {
1626 if (options::incrementalSolving
.wasSetByUser()) {
1627 throw OptionException(std::string("Eager bit-blasting does not currently support incremental mode. \n\
1628 Try --bitblast=lazy"));
1630 Notice() << "SmtEngine: turning off incremental to support eager bit-blasting" << endl
;
1631 setOption("incremental", SExpr("false"));
1634 if (! options::bvEagerExplanations
.wasSetByUser() &&
1635 d_logic
.isTheoryEnabled(THEORY_ARRAY
) &&
1636 d_logic
.isTheoryEnabled(THEORY_BV
)) {
1637 Trace("smt") << "enabling eager bit-vector explanations " << endl
;
1638 options::bvEagerExplanations
.set(true);
1641 if( !options::bitvectorEqualitySolver() ){
1642 Trace("smt") << "disabling bvLazyRewriteExtf since equality solver is disabled" << endl
;
1643 options::bvLazyRewriteExtf
.set(false);
1646 // Turn on arith rewrite equalities only for pure arithmetic
1647 if(! options::arithRewriteEq
.wasSetByUser()) {
1648 bool arithRewriteEq
= d_logic
.isPure(THEORY_ARITH
) && d_logic
.isLinear() && !d_logic
.isQuantified();
1649 Trace("smt") << "setting arith rewrite equalities " << arithRewriteEq
<< endl
;
1650 options::arithRewriteEq
.set(arithRewriteEq
);
1652 if(! options::arithHeuristicPivots
.wasSetByUser()) {
1653 int16_t heuristicPivots
= 5;
1654 if(d_logic
.isPure(THEORY_ARITH
) && !d_logic
.isQuantified()) {
1655 if(d_logic
.isDifferenceLogic()) {
1656 heuristicPivots
= -1;
1657 } else if(!d_logic
.areIntegersUsed()) {
1658 heuristicPivots
= 0;
1661 Trace("smt") << "setting arithHeuristicPivots " << heuristicPivots
<< endl
;
1662 options::arithHeuristicPivots
.set(heuristicPivots
);
1664 if(! options::arithPivotThreshold
.wasSetByUser()){
1665 uint16_t pivotThreshold
= 2;
1666 if(d_logic
.isPure(THEORY_ARITH
) && !d_logic
.isQuantified()){
1667 if(d_logic
.isDifferenceLogic()){
1668 pivotThreshold
= 16;
1671 Trace("smt") << "setting arith arithPivotThreshold " << pivotThreshold
<< endl
;
1672 options::arithPivotThreshold
.set(pivotThreshold
);
1674 if(! options::arithStandardCheckVarOrderPivots
.wasSetByUser()){
1675 int16_t varOrderPivots
= -1;
1676 if(d_logic
.isPure(THEORY_ARITH
) && !d_logic
.isQuantified()){
1677 varOrderPivots
= 200;
1679 Trace("smt") << "setting arithStandardCheckVarOrderPivots " << varOrderPivots
<< endl
;
1680 options::arithStandardCheckVarOrderPivots
.set(varOrderPivots
);
1682 // Turn off early theory preprocessing if arithRewriteEq is on
1683 if (options::arithRewriteEq()) {
1684 d_earlyTheoryPP
= false;
1687 // Set decision mode based on logic (if not set by user)
1688 if(!options::decisionMode
.wasSetByUser()) {
1689 decision::DecisionMode decMode
=
1691 d_logic
.hasEverything() ? decision::DECISION_STRATEGY_JUSTIFICATION
:
1693 (not d_logic
.isQuantified() &&
1694 d_logic
.isPure(THEORY_BV
)
1696 // QF_AUFBV or QF_ABV or QF_UFBV
1697 (not d_logic
.isQuantified() &&
1698 (d_logic
.isTheoryEnabled(THEORY_ARRAY
) ||
1699 d_logic
.isTheoryEnabled(THEORY_UF
)) &&
1700 d_logic
.isTheoryEnabled(THEORY_BV
)
1702 // QF_AUFLIA (and may be ends up enabling QF_AUFLRA?)
1703 (not d_logic
.isQuantified() &&
1704 d_logic
.isTheoryEnabled(THEORY_ARRAY
) &&
1705 d_logic
.isTheoryEnabled(THEORY_UF
) &&
1706 d_logic
.isTheoryEnabled(THEORY_ARITH
)
1709 (not d_logic
.isQuantified() &&
1710 d_logic
.isPure(THEORY_ARITH
) && d_logic
.isLinear() && !d_logic
.isDifferenceLogic() && !d_logic
.areIntegersUsed()
1713 d_logic
.isQuantified() ||
1715 d_logic
.isTheoryEnabled(THEORY_STRINGS
)
1716 ? decision::DECISION_STRATEGY_JUSTIFICATION
1717 : decision::DECISION_STRATEGY_INTERNAL
1722 d_logic
.hasEverything() || d_logic
.isTheoryEnabled(THEORY_STRINGS
) ? false :
1724 (not d_logic
.isQuantified() &&
1725 d_logic
.isTheoryEnabled(THEORY_ARRAY
) &&
1726 d_logic
.isTheoryEnabled(THEORY_UF
) &&
1727 d_logic
.isTheoryEnabled(THEORY_ARITH
)
1730 (not d_logic
.isQuantified() &&
1731 d_logic
.isPure(THEORY_ARITH
) && d_logic
.isLinear() && !d_logic
.isDifferenceLogic() && !d_logic
.areIntegersUsed()
1736 Trace("smt") << "setting decision mode to " << decMode
<< endl
;
1737 options::decisionMode
.set(decMode
);
1738 options::decisionStopOnly
.set(stoponly
);
1740 if( options::incrementalSolving() ){
1741 //disable modes not supported by incremental
1742 options::sortInference
.set( false );
1743 options::ufssFairnessMonotone
.set( false );
1744 options::quantEpr
.set( false );
1746 if( d_logic
.hasCardinalityConstraints() ){
1747 //must have finite model finding on
1748 options::finiteModelFind
.set( true );
1751 //if it contains a theory with non-termination, do not strictly enforce that quantifiers and theory combination must be interleaved
1752 if( d_logic
.isTheoryEnabled(THEORY_STRINGS
) || (d_logic
.isTheoryEnabled(THEORY_ARITH
) && !d_logic
.isLinear()) ){
1753 if( !options::instWhenStrictInterleave
.wasSetByUser() ){
1754 options::instWhenStrictInterleave
.set( false );
1758 //local theory extensions
1759 if( options::localTheoryExt() ){
1760 if( !options::instMaxLevel
.wasSetByUser() ){
1761 options::instMaxLevel
.set( 0 );
1764 if( options::instMaxLevel()!=-1 ){
1765 Notice() << "SmtEngine: turning off cbqi to support instMaxLevel" << endl
;
1766 options::cbqi
.set(false);
1768 //track instantiations?
1769 if( options::cbqiNestedQE() || ( options::proof() && !options::trackInstLemmas
.wasSetByUser() ) ){
1770 options::trackInstLemmas
.set( true );
1773 if( ( options::fmfBoundLazy
.wasSetByUser() && options::fmfBoundLazy() ) ||
1774 ( options::fmfBoundInt
.wasSetByUser() && options::fmfBoundInt() ) ) {
1775 options::fmfBound
.set( true );
1777 //now have determined whether fmfBoundInt is on/off
1778 //apply fmfBoundInt options
1779 if( options::fmfBound() ){
1780 //must have finite model finding on
1781 options::finiteModelFind
.set( true );
1782 if( ! options::mbqiMode
.wasSetByUser() ||
1783 ( options::mbqiMode()!=quantifiers::MBQI_NONE
&&
1784 options::mbqiMode()!=quantifiers::MBQI_FMC
&&
1785 options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL
) ){
1786 //if bounded integers are set, use no MBQI by default
1787 options::mbqiMode
.set( quantifiers::MBQI_NONE
);
1789 if( ! options::prenexQuant
.wasSetByUser() ){
1790 options::prenexQuant
.set( quantifiers::PRENEX_QUANT_NONE
);
1793 if( options::ufHo() ){
1794 //if higher-order, then current variants of model-based instantiation cannot be used
1795 if( options::mbqiMode()!=quantifiers::MBQI_NONE
){
1796 options::mbqiMode
.set( quantifiers::MBQI_NONE
);
1799 if( options::mbqiMode()==quantifiers::MBQI_ABS
){
1800 if( !d_logic
.isPure(THEORY_UF
) ){
1801 //MBQI_ABS is only supported in pure quantified UF
1802 options::mbqiMode
.set( quantifiers::MBQI_FMC
);
1805 if( options::ufssSymBreak() ){
1806 options::sortInference
.set( true );
1808 if( options::fmfFunWellDefinedRelevant() ){
1809 if( !options::fmfFunWellDefined
.wasSetByUser() ){
1810 options::fmfFunWellDefined
.set( true );
1813 if( options::fmfFunWellDefined() ){
1814 if( !options::finiteModelFind
.wasSetByUser() ){
1815 options::finiteModelFind
.set( true );
1819 if( options::quantEpr() ){
1820 if( !options::preSkolemQuant
.wasSetByUser() ){
1821 options::preSkolemQuant
.set( true );
1825 //now, have determined whether finite model find is on/off
1826 //apply finite model finding options
1827 if( options::finiteModelFind() ){
1828 //apply conservative quantifiers splitting
1829 if( !options::quantDynamicSplit
.wasSetByUser() ){
1830 options::quantDynamicSplit
.set( quantifiers::QUANT_DSPLIT_MODE_DEFAULT
);
1832 //do not eliminate extended arithmetic symbols from quantified formulas
1833 if( !options::elimExtArithQuant
.wasSetByUser() ){
1834 options::elimExtArithQuant
.set( false );
1836 if( !options::eMatching
.wasSetByUser() ){
1837 options::eMatching
.set( options::fmfInstEngine() );
1839 if( !options::instWhenMode
.wasSetByUser() ){
1840 //instantiate only on last call
1841 if( options::eMatching() ){
1842 options::instWhenMode
.set( quantifiers::INST_WHEN_LAST_CALL
);
1845 if( options::mbqiMode()==quantifiers::MBQI_ABS
){
1846 if( !options::preSkolemQuant
.wasSetByUser() ){
1847 options::preSkolemQuant
.set( true );
1849 if( !options::preSkolemQuantNested
.wasSetByUser() ){
1850 options::preSkolemQuantNested
.set( true );
1852 if( !options::fmfOneInstPerRound
.wasSetByUser() ){
1853 options::fmfOneInstPerRound
.set( true );
1858 //apply counterexample guided instantiation options
1859 if( options::cegqiSingleInvMode()!=quantifiers::CEGQI_SI_MODE_NONE
){
1860 if( !options::ceGuidedInst
.wasSetByUser() ){
1861 options::ceGuidedInst
.set( true );
1864 if( options::ceGuidedInst() ){
1865 //counterexample-guided instantiation for sygus
1866 if( !options::cegqiSingleInvMode
.wasSetByUser() ){
1867 options::cegqiSingleInvMode
.set( quantifiers::CEGQI_SI_MODE_USE
);
1869 if( !options::quantConflictFind
.wasSetByUser() ){
1870 options::quantConflictFind
.set( false );
1872 if( !options::instNoEntail
.wasSetByUser() ){
1873 options::instNoEntail
.set( false );
1875 //do not allow partial functions
1876 if( !options::bitvectorDivByZeroConst
.wasSetByUser() ){
1877 options::bitvectorDivByZeroConst
.set( true );
1879 if( !options::dtRewriteErrorSel
.wasSetByUser() ){
1880 options::dtRewriteErrorSel
.set( true );
1883 if( !options::miniscopeQuant
.wasSetByUser() ){
1884 options::miniscopeQuant
.set( false );
1886 if( !options::miniscopeQuantFreeVar
.wasSetByUser() ){
1887 options::miniscopeQuantFreeVar
.set( false );
1890 if( !options::rewriteDivk
.wasSetByUser()) {
1891 options::rewriteDivk
.set( true );
1894 if( !options::macrosQuant
.wasSetByUser()) {
1895 options::macrosQuant
.set( false );
1897 if( !options::cbqiPreRegInst
.wasSetByUser()) {
1898 options::cbqiPreRegInst
.set( true );
1901 //counterexample-guided instantiation for non-sygus
1902 // enable if any possible quantifiers with arithmetic, datatypes or bitvectors
1903 if( d_logic
.isQuantified() &&
1904 ( ( options::decisionMode()!=decision::DECISION_STRATEGY_INTERNAL
&&
1905 ( d_logic
.isTheoryEnabled(THEORY_ARITH
) || d_logic
.isTheoryEnabled(THEORY_DATATYPES
) || d_logic
.isTheoryEnabled(THEORY_BV
) ) ) ||
1906 d_logic
.isPure(THEORY_ARITH
) || d_logic
.isPure(THEORY_BV
) ||
1907 options::cbqiAll() ) ){
1908 if( !options::cbqi
.wasSetByUser() ){
1909 options::cbqi
.set( true );
1912 if( options::cbqi() ){
1914 if( !options::rewriteDivk
.wasSetByUser()) {
1915 options::rewriteDivk
.set( true );
1917 if( d_logic
.isPure(THEORY_ARITH
) ){
1918 options::cbqiAll
.set( false );
1919 if( !options::quantConflictFind
.wasSetByUser() ){
1920 options::quantConflictFind
.set( false );
1922 if( !options::instNoEntail
.wasSetByUser() ){
1923 options::instNoEntail
.set( false );
1925 if( !options::instWhenMode
.wasSetByUser() && options::cbqiModel() ){
1926 //only instantiation should happen at last call when model is avaiable
1927 options::instWhenMode
.set( quantifiers::INST_WHEN_LAST_CALL
);
1930 //only supported in pure arithmetic
1931 options::cbqiNestedQE
.set(false);
1934 //implied options...
1935 if( options::strictTriggers() ){
1936 if( !options::userPatternsQuant
.wasSetByUser() ){
1937 options::userPatternsQuant
.set( quantifiers::USER_PAT_MODE_TRUST
);
1940 if( options::qcfMode
.wasSetByUser() || options::qcfTConstraint() ){
1941 options::quantConflictFind
.set( true );
1943 if( options::cbqi() &&
1944 ( options::cbqiNestedQE() || options::decisionMode()==decision::DECISION_STRATEGY_INTERNAL
) ){
1945 //only complete with prenex = disj_normal or normal
1946 if( options::prenexQuant()<=quantifiers::PRENEX_QUANT_DISJ_NORMAL
){
1947 options::prenexQuant
.set( quantifiers::PRENEX_QUANT_DISJ_NORMAL
);
1950 if( options::cbqiNestedQE() ){
1951 options::prenexQuantUser
.set( true );
1952 if( !options::preSkolemQuant
.wasSetByUser() ){
1953 options::preSkolemQuant
.set( true );
1956 //for induction techniques
1957 if( options::quantInduction() ){
1958 if( !options::dtStcInduction
.wasSetByUser() ){
1959 options::dtStcInduction
.set( true );
1961 if( !options::intWfInduction
.wasSetByUser() ){
1962 options::intWfInduction
.set( true );
1965 if( options::dtStcInduction() ){
1966 //leads to unfairness FIXME
1967 if( !options::dtForceAssignment
.wasSetByUser() ){
1968 options::dtForceAssignment
.set( true );
1970 //try to remove ITEs from quantified formulas
1971 if( !options::iteDtTesterSplitQuant
.wasSetByUser() ){
1972 options::iteDtTesterSplitQuant
.set( true );
1974 if( !options::iteLiftQuant
.wasSetByUser() ){
1975 options::iteLiftQuant
.set( quantifiers::ITE_LIFT_QUANT_MODE_ALL
);
1978 if( options::intWfInduction() ){
1979 if( !options::purifyTriggers
.wasSetByUser() ){
1980 options::purifyTriggers
.set( true );
1983 if( options::conjectureNoFilter() ){
1984 if( !options::conjectureFilterActiveTerms
.wasSetByUser() ){
1985 options::conjectureFilterActiveTerms
.set( false );
1987 if( !options::conjectureFilterCanonical
.wasSetByUser() ){
1988 options::conjectureFilterCanonical
.set( false );
1990 if( !options::conjectureFilterModel
.wasSetByUser() ){
1991 options::conjectureFilterModel
.set( false );
1994 if( options::conjectureGenPerRound
.wasSetByUser() ){
1995 if( options::conjectureGenPerRound()>0 ){
1996 options::conjectureGen
.set( true );
1998 options::conjectureGen
.set( false );
2001 //can't pre-skolemize nested quantifiers without UF theory
2002 if( !d_logic
.isTheoryEnabled(THEORY_UF
) && options::preSkolemQuant() ){
2003 if( !options::preSkolemQuantNested
.wasSetByUser() ){
2004 options::preSkolemQuantNested
.set( false );
2007 if( !d_logic
.isTheoryEnabled(THEORY_DATATYPES
) ){
2008 options::quantDynamicSplit
.set( quantifiers::QUANT_DSPLIT_MODE_NONE
);
2011 //until bugs 371,431 are fixed
2012 if( ! options::minisatUseElim
.wasSetByUser()){
2013 //AJR: cannot use minisat elim for new implementation of sets TODO: why?
2014 if( d_logic
.isTheoryEnabled(THEORY_SETS
) || d_logic
.isQuantified() || options::produceModels() || options::produceAssignments() || options::checkModels() ){
2015 options::minisatUseElim
.set( false );
2018 else if (options::minisatUseElim()) {
2019 if (options::produceModels()) {
2020 Notice() << "SmtEngine: turning off produce-models to support minisatUseElim" << endl
;
2021 setOption("produce-models", SExpr("false"));
2023 if (options::produceAssignments()) {
2024 Notice() << "SmtEngine: turning off produce-assignments to support minisatUseElim" << endl
;
2025 setOption("produce-assignments", SExpr("false"));
2027 if (options::checkModels()) {
2028 Notice() << "SmtEngine: turning off check-models to support minisatUseElim" << endl
;
2029 setOption("check-models", SExpr("false"));
2033 // For now, these array theory optimizations do not support model-building
2034 if (options::produceModels() || options::produceAssignments() || options::checkModels()) {
2035 options::arraysOptimizeLinear
.set(false);
2036 options::arraysLazyRIntro1
.set(false);
2039 // Non-linear arithmetic does not support models unless nlExt is enabled
2040 if (d_logic
.isTheoryEnabled(THEORY_ARITH
) && !d_logic
.isLinear() && !options::nlExt() ) {
2041 if (options::produceModels()) {
2042 if(options::produceModels
.wasSetByUser()) {
2043 throw OptionException("produce-model not supported with nonlinear arith");
2045 Warning() << "SmtEngine: turning off produce-models because unsupported for nonlinear arith" << endl
;
2046 setOption("produce-models", SExpr("false"));
2048 if (options::produceAssignments()) {
2049 if(options::produceAssignments
.wasSetByUser()) {
2050 throw OptionException("produce-assignments not supported with nonlinear arith");
2052 Warning() << "SmtEngine: turning off produce-assignments because unsupported for nonlinear arith" << endl
;
2053 setOption("produce-assignments", SExpr("false"));
2055 if (options::checkModels()) {
2056 if(options::checkModels
.wasSetByUser()) {
2057 throw OptionException("check-models not supported with nonlinear arith");
2059 Warning() << "SmtEngine: turning off check-models because unsupported for nonlinear arith" << endl
;
2060 setOption("check-models", SExpr("false"));
2064 if(options::incrementalSolving() && options::proof()) {
2065 Warning() << "SmtEngine: turning off incremental solving mode (not yet supported with --proof, try --tear-down-incremental instead)" << endl
;
2066 setOption("incremental", SExpr("false"));
2070 void SmtEngine::setInfo(const std::string
& key
, const CVC4::SExpr
& value
)
2071 throw(OptionException
, ModalException
) {
2073 SmtScope
smts(this);
2075 Trace("smt") << "SMT setInfo(" << key
<< ", " << value
<< ")" << endl
;
2077 if(Dump
.isOn("benchmark")) {
2078 if(key
== "status") {
2079 string s
= value
.getValue();
2080 BenchmarkStatus status
=
2081 (s
== "sat") ? SMT_SATISFIABLE
:
2082 ((s
== "unsat") ? SMT_UNSATISFIABLE
: SMT_UNKNOWN
);
2083 Dump("benchmark") << SetBenchmarkStatusCommand(status
);
2085 Dump("benchmark") << SetInfoCommand(key
, value
);
2089 // Check for CVC4-specific info keys (prefixed with "cvc4-" or "cvc4_")
2090 if(key
.length() > 5) {
2091 string prefix
= key
.substr(0, 5);
2092 if(prefix
== "cvc4-" || prefix
== "cvc4_") {
2093 string cvc4key
= key
.substr(5);
2094 if(cvc4key
== "logic") {
2095 if(! value
.isAtom()) {
2096 throw OptionException("argument to (set-info :cvc4-logic ..) must be a string");
2098 SmtScope
smts(this);
2099 d_logic
= value
.getValue();
2103 throw UnrecognizedOptionException();
2108 // Check for standard info keys (SMT-LIB v1, SMT-LIB v2, ...)
2109 if(key
== "source" ||
2110 key
== "category" ||
2111 key
== "difficulty" ||
2115 } else if(key
== "name") {
2116 d_filename
= value
.getValue();
2118 } else if(key
== "smt-lib-version") {
2119 if( (value
.isInteger() && value
.getIntegerValue() == Integer(2)) ||
2120 (value
.isRational() && value
.getRationalValue() == Rational(2)) ||
2121 value
.getValue() == "2" ||
2122 value
.getValue() == "2.0" ) {
2123 options::inputLanguage
.set(language::input::LANG_SMTLIB_V2_0
);
2125 // supported SMT-LIB version
2126 if(!options::outputLanguage
.wasSetByUser() &&
2127 ( options::outputLanguage() == language::output::LANG_SMTLIB_V2_5
|| options::outputLanguage() == language::output::LANG_SMTLIB_V2_6
)) {
2128 options::outputLanguage
.set(language::output::LANG_SMTLIB_V2_0
);
2129 *options::out() << language::SetLanguage(language::output::LANG_SMTLIB_V2_0
);
2132 } else if( (value
.isRational() && value
.getRationalValue() == Rational(5, 2)) ||
2133 value
.getValue() == "2.5" ) {
2134 options::inputLanguage
.set(language::input::LANG_SMTLIB_V2_5
);
2136 // supported SMT-LIB version
2137 if(!options::outputLanguage
.wasSetByUser() &&
2138 options::outputLanguage() == language::output::LANG_SMTLIB_V2_0
) {
2139 options::outputLanguage
.set(language::output::LANG_SMTLIB_V2_5
);
2140 *options::out() << language::SetLanguage(language::output::LANG_SMTLIB_V2_5
);
2143 } else if( (value
.isRational() && value
.getRationalValue() == Rational(13, 5)) ||
2144 value
.getValue() == "2.6" ) {
2145 options::inputLanguage
.set(language::input::LANG_SMTLIB_V2_6
);
2147 // supported SMT-LIB version
2148 if(!options::outputLanguage
.wasSetByUser() &&
2149 options::outputLanguage() == language::output::LANG_SMTLIB_V2_0
) {
2150 options::outputLanguage
.set(language::output::LANG_SMTLIB_V2_6
);
2151 *options::out() << language::SetLanguage(language::output::LANG_SMTLIB_V2_6
);
2155 Warning() << "Warning: unsupported smt-lib-version: " << value
<< endl
;
2156 throw UnrecognizedOptionException();
2157 } else if(key
== "status") {
2159 if(value
.isAtom()) {
2160 s
= value
.getValue();
2162 if(s
!= "sat" && s
!= "unsat" && s
!= "unknown") {
2163 throw OptionException("argument to (set-info :status ..) must be "
2164 "`sat' or `unsat' or `unknown'");
2166 d_status
= Result(s
, d_filename
);
2169 throw UnrecognizedOptionException();
2172 CVC4::SExpr
SmtEngine::getInfo(const std::string
& key
) const {
2174 SmtScope
smts(this);
2176 Trace("smt") << "SMT getInfo(" << key
<< ")" << endl
;
2177 if(key
== "all-statistics") {
2178 vector
<SExpr
> stats
;
2179 for(StatisticsRegistry::const_iterator i
= NodeManager::fromExprManager(d_exprManager
)->getStatisticsRegistry()->begin();
2180 i
!= NodeManager::fromExprManager(d_exprManager
)->getStatisticsRegistry()->end();
2183 v
.push_back((*i
).first
);
2184 v
.push_back((*i
).second
);
2187 for(StatisticsRegistry::const_iterator i
= d_statisticsRegistry
->begin();
2188 i
!= d_statisticsRegistry
->end();
2191 v
.push_back((*i
).first
);
2192 v
.push_back((*i
).second
);
2195 return SExpr(stats
);
2196 } else if(key
== "error-behavior") {
2197 // immediate-exit | continued-execution
2198 if( options::continuedExecution() || options::interactive() ) {
2199 return SExpr(SExpr::Keyword("continued-execution"));
2201 return SExpr(SExpr::Keyword("immediate-exit"));
2203 } else if(key
== "name") {
2204 return SExpr(Configuration::getName());
2205 } else if(key
== "version") {
2206 return SExpr(Configuration::getVersionString());
2207 } else if(key
== "authors") {
2208 return SExpr(Configuration::about());
2209 } else if(key
== "status") {
2210 // sat | unsat | unknown
2211 switch(d_status
.asSatisfiabilityResult().isSat()) {
2213 return SExpr(SExpr::Keyword("sat"));
2215 return SExpr(SExpr::Keyword("unsat"));
2217 return SExpr(SExpr::Keyword("unknown"));
2219 } else if(key
== "reason-unknown") {
2220 if(!d_status
.isNull() && d_status
.isUnknown()) {
2222 ss
<< d_status
.whyUnknown();
2223 string s
= ss
.str();
2224 transform(s
.begin(), s
.end(), s
.begin(), ::tolower
);
2225 return SExpr(SExpr::Keyword(s
));
2227 throw ModalException("Can't get-info :reason-unknown when the "
2228 "last result wasn't unknown!");
2230 } else if(key
== "assertion-stack-levels") {
2231 AlwaysAssert(d_userLevels
.size() <=
2232 std::numeric_limits
<unsigned long int>::max());
2233 return SExpr(static_cast<unsigned long int>(d_userLevels
.size()));
2234 } else if(key
== "all-options") {
2235 // get the options, like all-statistics
2236 std::vector
< std::vector
<std::string
> > current_options
=
2237 Options::current()->getOptions();
2238 return SExpr::parseListOfListOfAtoms(current_options
);
2240 throw UnrecognizedOptionException();
2244 void SmtEngine::defineFunction(Expr func
,
2245 const std::vector
<Expr
>& formals
,
2247 SmtScope
smts(this);
2249 Trace("smt") << "SMT defineFunction(" << func
<< ")" << endl
;
2250 for(std::vector
<Expr
>::const_iterator i
= formals
.begin(); i
!= formals
.end(); ++i
) {
2251 if((*i
).getKind() != kind::BOUND_VARIABLE
) {
2253 ss
<< "All formal arguments to defined functions must be BOUND_VARIABLEs, but in the\n"
2254 << "definition of function " << func
<< ", formal\n"
2255 << " " << *i
<< "\n"
2256 << "has kind " << (*i
).getKind();
2257 throw TypeCheckingException(func
, ss
.str());
2262 ss
<< language::SetLanguage(language::SetLanguage::getLanguage(Dump
.getStream()))
2264 DefineFunctionCommand
c(ss
.str(), func
, formals
, formula
);
2265 addToModelCommandAndDump(c
, ExprManager::VAR_FLAG_DEFINED
, true, "declarations");
2268 PROOF( if (options::checkUnsatCores()) {
2269 d_defineCommands
.push_back(c
.clone());
2273 // Substitute out any abstract values in formula
2274 Expr form
= d_private
->substituteAbstractValues(Node::fromExpr(formula
)).toExpr();
2277 Type formulaType
= form
.getType(options::typeChecking());
2279 Type funcType
= func
.getType();
2280 // We distinguish here between definitions of constants and functions,
2281 // because the type checking for them is subtly different. Perhaps we
2282 // should instead have SmtEngine::defineFunction() and
2283 // SmtEngine::defineConstant() for better clarity, although then that
2284 // doesn't match the SMT-LIBv2 standard...
2285 if(formals
.size() > 0) {
2286 Type rangeType
= FunctionType(funcType
).getRangeType();
2287 if(! formulaType
.isComparableTo(rangeType
)) {
2289 ss
<< "Type of defined function does not match its declaration\n"
2290 << "The function : " << func
<< "\n"
2291 << "Declared type : " << rangeType
<< "\n"
2292 << "The body : " << formula
<< "\n"
2293 << "Body type : " << formulaType
;
2294 throw TypeCheckingException(func
, ss
.str());
2297 if(! formulaType
.isComparableTo(funcType
)) {
2299 ss
<< "Declared type of defined constant does not match its definition\n"
2300 << "The constant : " << func
<< "\n"
2301 << "Declared type : " << funcType
<< " " << Type::getTypeNode(funcType
)->getId() << "\n"
2302 << "The definition : " << formula
<< "\n"
2303 << "Definition type: " << formulaType
<< " " << Type::getTypeNode(formulaType
)->getId();
2304 throw TypeCheckingException(func
, ss
.str());
2307 TNode funcNode
= func
.getTNode();
2308 vector
<Node
> formalsNodes
;
2309 for(vector
<Expr
>::const_iterator i
= formals
.begin(),
2310 iend
= formals
.end();
2313 formalsNodes
.push_back((*i
).getNode());
2315 TNode formNode
= form
.getTNode();
2316 DefinedFunction
def(funcNode
, formalsNodes
, formNode
);
2317 // Permit (check-sat) (define-fun ...) (get-value ...) sequences.
2318 // Otherwise, (check-sat) (get-value ((! foo :named bar))) breaks
2319 // d_haveAdditions = true;
2320 Debug("smt") << "definedFunctions insert " << funcNode
<< " " << formNode
<< endl
;
2321 d_definedFunctions
->insert(funcNode
, def
);
2324 bool SmtEngine::isDefinedFunction( Expr func
){
2325 Node nf
= Node::fromExpr( func
);
2326 Debug("smt") << "isDefined function " << nf
<< "?" << std::endl
;
2327 return d_definedFunctions
->find(nf
) != d_definedFunctions
->end();
2330 Node
SmtEnginePrivate::expandDefinitions(TNode n
, unordered_map
<Node
, Node
, NodeHashFunction
>& cache
, bool expandOnly
)
2331 throw(TypeCheckingException
, LogicException
, UnsafeInterruptException
) {
2333 stack
< triple
<Node
, Node
, bool> > worklist
;
2335 worklist
.push(make_triple(Node(n
), Node(n
), false));
2336 // The worklist is made of triples, each is input / original node then the output / rewritten node
2337 // and finally a flag tracking whether the children have been explored (i.e. if this is a downward
2341 spendResource(options::preprocessStep());
2342 n
= worklist
.top().first
; // n is the input / original
2343 Node node
= worklist
.top().second
; // node is the output / result
2344 bool childrenPushed
= worklist
.top().third
;
2347 // Working downwards
2348 if(!childrenPushed
) {
2349 Kind k
= n
.getKind();
2351 // we can short circuit (variable) leaves
2353 SmtEngine::DefinedFunctionMap::const_iterator i
= d_smt
.d_definedFunctions
->find(n
);
2354 if(i
!= d_smt
.d_definedFunctions
->end()) {
2355 // replacement must be closed
2356 if((*i
).second
.getFormals().size() > 0) {
2357 result
.push(d_smt
.d_nodeManager
->mkNode(kind::LAMBDA
, d_smt
.d_nodeManager
->mkNode(kind::BOUND_VAR_LIST
, (*i
).second
.getFormals()), (*i
).second
.getFormula()));
2360 // don't bother putting in the cache
2361 result
.push((*i
).second
.getFormula());
2364 // don't bother putting in the cache
2369 // maybe it's in the cache
2370 unordered_map
<Node
, Node
, NodeHashFunction
>::iterator cacheHit
= cache
.find(n
);
2371 if(cacheHit
!= cache
.end()) {
2372 TNode ret
= (*cacheHit
).second
;
2373 result
.push(ret
.isNull() ? n
: ret
);
2377 // otherwise expand it
2378 bool doExpand
= k
== kind::APPLY
;
2380 if( options::macrosQuant() ){
2381 //expand if we have inferred an operator corresponds to a defined function
2382 doExpand
= k
==kind::APPLY_UF
&& d_smt
.isDefinedFunction( n
.getOperator().toExpr() );
2386 vector
<Node
> formals
;
2388 if( n
.getOperator().getKind() == kind::LAMBDA
){
2389 TNode op
= n
.getOperator();
2391 for( unsigned i
=0; i
<op
[0].getNumChildren(); i
++ ){
2392 formals
.push_back( op
[0][i
] );
2396 // application of a user-defined symbol
2397 TNode func
= n
.getOperator();
2398 SmtEngine::DefinedFunctionMap::const_iterator i
= d_smt
.d_definedFunctions
->find(func
);
2399 if(i
== d_smt
.d_definedFunctions
->end()) {
2400 throw TypeCheckingException(n
.toExpr(), string("Undefined function: `") + func
.toString() + "'");
2402 DefinedFunction def
= (*i
).second
;
2403 formals
= def
.getFormals();
2405 if(Debug
.isOn("expand")) {
2406 Debug("expand") << "found: " << n
<< endl
;
2407 Debug("expand") << " func: " << func
<< endl
;
2408 string name
= func
.getAttribute(expr::VarNameAttr());
2409 Debug("expand") << " : \"" << name
<< "\"" << endl
;
2411 if(Debug
.isOn("expand")) {
2412 Debug("expand") << " defn: " << def
.getFunction() << endl
2414 if(formals
.size() > 0) {
2415 copy( formals
.begin(), formals
.end() - 1,
2416 ostream_iterator
<Node
>(Debug("expand"), ", ") );
2417 Debug("expand") << formals
.back();
2419 Debug("expand") << "]" << endl
2420 << " " << def
.getFunction().getType() << endl
2421 << " " << def
.getFormula() << endl
;
2424 fm
= def
.getFormula();
2427 Node instance
= fm
.substitute(formals
.begin(),
2430 n
.begin() + formals
.size());
2431 Debug("expand") << "made : " << instance
<< endl
;
2433 Node expanded
= expandDefinitions(instance
, cache
, expandOnly
);
2434 cache
[n
] = (n
== expanded
? Node::null() : expanded
);
2435 result
.push(expanded
);
2438 } else if(! expandOnly
) {
2439 // do not do any theory stuff if expandOnly is true
2441 theory::Theory
* t
= d_smt
.d_theoryEngine
->theoryOf(node
);
2444 LogicRequest
req(d_smt
);
2445 node
= t
->expandDefinition(req
, n
);
2448 // the partial functions can fall through, in which case we still
2449 // consider their children
2450 worklist
.push(make_triple(Node(n
), node
, true)); // Original and rewritten result
2452 for(size_t i
= 0; i
< node
.getNumChildren(); ++i
) {
2453 worklist
.push(make_triple(node
[i
], node
[i
], false)); // Rewrite the children of the result only
2458 // Reconstruct the node from it's (now rewritten) children on the stack
2460 Debug("expand") << "cons : " << node
<< endl
;
2461 if(node
.getNumChildren()>0) {
2462 //cout << "cons : " << node << endl;
2463 NodeBuilder
<> nb(node
.getKind());
2464 if(node
.getMetaKind() == kind::metakind::PARAMETERIZED
) {
2465 Debug("expand") << "op : " << node
.getOperator() << endl
;
2466 //cout << "op : " << node.getOperator() << endl;
2467 nb
<< node
.getOperator();
2469 for(size_t i
= 0; i
< node
.getNumChildren(); ++i
) {
2470 Assert(!result
.empty());
2471 Node expanded
= result
.top();
2473 //cout << "exchld : " << expanded << endl;
2474 Debug("expand") << "exchld : " << expanded
<< endl
;
2479 cache
[n
] = n
== node
? Node::null() : node
; // Only cache once all subterms are expanded
2482 } while(!worklist
.empty());
2484 AlwaysAssert(result
.size() == 1);
2486 return result
.top();
2489 //TODO: clean this up
2490 struct intToBV_stack_element
{
2492 bool children_added
;
2493 intToBV_stack_element(TNode node
)
2494 : node(node
), children_added(false) {}
2495 };/* struct intToBV_stack_element */
2497 typedef std::unordered_map
<Node
, Node
, NodeHashFunction
> NodeMap
;
2499 Node
SmtEnginePrivate::intToBVMakeBinary(TNode n
, NodeMap
& cache
) {
2500 // Do a topological sort of the subexpressions and substitute them
2501 vector
<intToBV_stack_element
> toVisit
;
2502 toVisit
.push_back(n
);
2504 while (!toVisit
.empty())
2506 // The current node we are processing
2507 intToBV_stack_element
& stackHead
= toVisit
.back();
2508 TNode current
= stackHead
.node
;
2510 NodeMap::iterator find
= cache
.find(current
);
2511 if (find
!= cache
.end()) {
2515 if (stackHead
.children_added
) {
2516 // Children have been processed, so rebuild this node
2518 NodeManager
* nm
= NodeManager::currentNM();
2519 if (current
.getNumChildren() > 2 && (current
.getKind() == kind::PLUS
|| current
.getKind() == kind::MULT
)) {
2520 Assert(cache
.find(current
[0]) != cache
.end());
2521 result
= cache
[current
[0]];
2522 for (unsigned i
= 1; i
< current
.getNumChildren(); ++ i
) {
2523 Assert(cache
.find(current
[i
]) != cache
.end());
2524 Node child
= current
[i
];
2525 Node childRes
= cache
[current
[i
]];
2526 result
= nm
->mkNode(current
.getKind(), result
, childRes
);
2530 NodeBuilder
<> builder(current
.getKind());
2531 for (unsigned i
= 0; i
< current
.getNumChildren(); ++ i
) {
2532 Assert(cache
.find(current
[i
]) != cache
.end());
2533 builder
<< cache
[current
[i
]];
2537 cache
[current
] = result
;
2540 // Mark that we have added the children if any
2541 if (current
.getNumChildren() > 0) {
2542 stackHead
.children_added
= true;
2543 // We need to add the children
2544 for(TNode::iterator child_it
= current
.begin(); child_it
!= current
.end(); ++ child_it
) {
2545 TNode childNode
= *child_it
;
2546 NodeMap::iterator childFind
= cache
.find(childNode
);
2547 if (childFind
== cache
.end()) {
2548 toVisit
.push_back(childNode
);
2552 cache
[current
] = current
;
2560 Node
SmtEnginePrivate::intToBV(TNode n
, NodeMap
& cache
) {
2561 int size
= options::solveIntAsBV();
2562 AlwaysAssert(size
> 0);
2563 AlwaysAssert(!options::incrementalSolving());
2565 vector
<intToBV_stack_element
> toVisit
;
2566 NodeMap binaryCache
;
2567 Node n_binary
= intToBVMakeBinary(n
, binaryCache
);
2568 toVisit
.push_back(TNode(n_binary
));
2570 while (!toVisit
.empty())
2572 // The current node we are processing
2573 intToBV_stack_element
& stackHead
= toVisit
.back();
2574 TNode current
= stackHead
.node
;
2576 // If node is already in the cache we're done, pop from the stack
2577 NodeMap::iterator find
= cache
.find(current
);
2578 if (find
!= cache
.end()) {
2583 // Not yet substituted, so process
2584 NodeManager
* nm
= NodeManager::currentNM();
2585 if (stackHead
.children_added
) {
2586 // Children have been processed, so rebuild this node
2587 vector
<Node
> children
;
2589 for (unsigned i
= 0; i
< current
.getNumChildren(); ++ i
) {
2590 Assert(cache
.find(current
[i
]) != cache
.end());
2591 TNode childRes
= cache
[current
[i
]];
2592 TypeNode type
= childRes
.getType();
2593 if (type
.isBitVector()) {
2594 unsigned bvsize
= type
.getBitVectorSize();
2599 children
.push_back(childRes
);
2602 kind::Kind_t newKind
= current
.getKind();
2606 Assert(children
.size() == 2);
2607 newKind
= kind::BITVECTOR_PLUS
;
2611 Assert(children
.size() == 2);
2612 newKind
= kind::BITVECTOR_MULT
;
2616 Assert(children
.size() == 2);
2617 newKind
= kind::BITVECTOR_SUB
;
2621 Assert(children
.size() == 1);
2622 newKind
= kind::BITVECTOR_NEG
;
2626 newKind
= kind::BITVECTOR_SLT
;
2629 newKind
= kind::BITVECTOR_SLE
;
2632 newKind
= kind::BITVECTOR_SGT
;
2635 newKind
= kind::BITVECTOR_SGE
;
2641 if (Theory::theoryOf(current
) == THEORY_BOOL
) {
2644 throw TypeCheckingException(current
.toExpr(), string("Cannot translate to BV: ") + current
.toString());
2646 for (unsigned i
= 0; i
< children
.size(); ++i
) {
2647 TypeNode type
= children
[i
].getType();
2648 if (!type
.isBitVector()) {
2651 unsigned bvsize
= type
.getBitVectorSize();
2654 Node signExtendOp
= nm
->mkConst
<BitVectorSignExtend
>(BitVectorSignExtend(max
- bvsize
));
2655 children
[i
] = nm
->mkNode(signExtendOp
, children
[i
]);
2659 NodeBuilder
<> builder(newKind
);
2660 for (unsigned i
= 0; i
< children
.size(); ++i
) {
2661 builder
<< children
[i
];
2663 // Mark the substitution and continue
2664 Node result
= builder
;
2666 result
= Rewriter::rewrite(result
);
2667 cache
[current
] = result
;
2670 // Mark that we have added the children if any
2671 if (current
.getNumChildren() > 0) {
2672 stackHead
.children_added
= true;
2673 // We need to add the children
2674 for(TNode::iterator child_it
= current
.begin(); child_it
!= current
.end(); ++ child_it
) {
2675 TNode childNode
= *child_it
;
2676 NodeMap::iterator childFind
= cache
.find(childNode
);
2677 if (childFind
== cache
.end()) {
2678 toVisit
.push_back(childNode
);
2682 // It's a leaf: could be a variable or a numeral
2683 Node result
= current
;
2684 if (current
.isVar()) {
2685 if (current
.getType() == nm
->integerType()) {
2686 result
= nm
->mkSkolem("__intToBV_var", nm
->mkBitVectorType(size
),
2687 "Variable introduced in intToBV pass");
2690 AlwaysAssert(current
.getType() == nm
->booleanType());
2693 else if (current
.isConst()) {
2694 switch (current
.getKind()) {
2695 case kind::CONST_RATIONAL
: {
2696 Rational constant
= current
.getConst
<Rational
>();
2697 AlwaysAssert(constant
.isIntegral());
2698 AlwaysAssert(constant
>= 0);
2699 BitVector
bv(size
, constant
.getNumerator());
2700 if (bv
.toSignedInt() != constant
.getNumerator()) {
2701 throw TypeCheckingException(current
.toExpr(), string("Not enough bits for constant in intToBV: ") + current
.toString());
2703 result
= nm
->mkConst(bv
);
2706 case kind::CONST_BOOLEAN
:
2709 throw TypeCheckingException(current
.toExpr(), string("Cannot translate const to BV: ") + current
.toString());
2713 throw TypeCheckingException(current
.toExpr(), string("Cannot translate to BV: ") + current
.toString());
2715 cache
[current
] = result
;
2720 return cache
[n_binary
];
2723 Node
SmtEnginePrivate::realToInt(TNode n
, NodeMap
& cache
, std::vector
< Node
>& var_eq
) {
2724 Trace("real-as-int-debug") << "Convert : " << n
<< std::endl
;
2725 NodeMap::iterator find
= cache
.find(n
);
2726 if (find
!= cache
.end()) {
2727 return (*find
).second
;
2730 if( n
.getNumChildren()>0 ){
2731 if( n
.getKind()==kind::EQUAL
|| n
.getKind()==kind::GEQ
|| n
.getKind()==kind::LT
|| n
.getKind()==kind::GT
|| n
.getKind()==kind::LEQ
){
2732 ret
= Rewriter::rewrite( n
);
2733 Trace("real-as-int-debug") << "Now looking at : " << ret
<< std::endl
;
2734 if( !ret
.isConst() ){
2735 Node ret_lit
= ret
.getKind()==kind::NOT
? ret
[0] : ret
;
2736 bool ret_pol
= ret
.getKind()!=kind::NOT
;
2737 std::map
< Node
, Node
> msum
;
2738 if( QuantArith::getMonomialSumLit( ret_lit
, msum
) ){
2739 //get common coefficient
2740 std::vector
< Node
> coeffs
;
2741 for( std::map
< Node
, Node
>::iterator itm
= msum
.begin(); itm
!= msum
.end(); ++itm
){
2742 Node v
= itm
->first
;
2743 Node c
= itm
->second
;
2745 Assert( c
.isConst() );
2746 coeffs
.push_back( NodeManager::currentNM()->mkConst( Rational( c
.getConst
<Rational
>().getDenominator() ) ) );
2749 Node cc
= coeffs
.empty() ? Node::null() : ( coeffs
.size()==1 ? coeffs
[0] : Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::MULT
, coeffs
) ) );
2750 std::vector
< Node
> sum
;
2751 for( std::map
< Node
, Node
>::iterator itm
= msum
.begin(); itm
!= msum
.end(); ++itm
){
2752 Node v
= itm
->first
;
2753 Node c
= itm
->second
;
2756 c
= cc
.isNull() ? NodeManager::currentNM()->mkConst( Rational( 1 ) ) : cc
;
2759 c
= Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::MULT
, c
, cc
) );
2762 Assert( c
.getType().isInteger() );
2766 Node vv
= realToInt( v
, cache
, var_eq
);
2767 if( vv
.getType().isInteger() ){
2768 sum
.push_back( NodeManager::currentNM()->mkNode( kind::MULT
, c
, vv
) );
2770 throw TypeCheckingException(v
.toExpr(), string("Cannot translate to Int: ") + v
.toString());
2774 Node sumt
= sum
.empty() ? NodeManager::currentNM()->mkConst( Rational( 0 ) ) : ( sum
.size()==1 ? sum
[0] : NodeManager::currentNM()->mkNode( kind::PLUS
, sum
) );
2775 ret
= NodeManager::currentNM()->mkNode( ret_lit
.getKind(), sumt
, NodeManager::currentNM()->mkConst( Rational( 0 ) ) );
2779 Trace("real-as-int") << "Convert : " << std::endl
;
2780 Trace("real-as-int") << " " << n
<< std::endl
;
2781 Trace("real-as-int") << " " << ret
<< std::endl
;
2783 throw TypeCheckingException(n
.toExpr(), string("Cannot translate to Int: ") + n
.toString());
2787 bool childChanged
= false;
2788 std::vector
< Node
> children
;
2789 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
2790 Node nc
= realToInt( n
[i
], cache
, var_eq
);
2791 childChanged
= childChanged
|| nc
!=n
[i
];
2792 children
.push_back( nc
);
2795 ret
= NodeManager::currentNM()->mkNode( n
.getKind(), children
);
2800 if( !n
.getType().isInteger() ){
2801 ret
= NodeManager::currentNM()->mkSkolem("__realToInt_var", NodeManager::currentNM()->integerType(), "Variable introduced in realToInt pass");
2802 var_eq
.push_back( n
.eqNode( ret
) );
2811 Node
SmtEnginePrivate::purifyNlTerms(TNode n
, NodeMap
& cache
, NodeMap
& bcache
, std::vector
< Node
>& var_eq
, bool beneathMult
) {
2813 NodeMap::iterator find
= bcache
.find(n
);
2814 if (find
!= bcache
.end()) {
2815 return (*find
).second
;
2818 NodeMap::iterator find
= cache
.find(n
);
2819 if (find
!= cache
.end()) {
2820 return (*find
).second
;
2824 if( n
.getNumChildren()>0 ){
2825 if( beneathMult
&& n
.getKind()!=kind::MULT
){
2827 ret
= NodeManager::currentNM()->mkSkolem("__purifyNl_var", n
.getType(), "Variable introduced in purifyNl pass");
2828 Node np
= purifyNlTerms( n
, cache
, bcache
, var_eq
, false );
2829 var_eq
.push_back( np
.eqNode( ret
) );
2831 bool beneathMultNew
= beneathMult
|| n
.getKind()==kind::MULT
;
2832 bool childChanged
= false;
2833 std::vector
< Node
> children
;
2834 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
2835 Node nc
= purifyNlTerms( n
[i
], cache
, bcache
, var_eq
, beneathMultNew
);
2836 childChanged
= childChanged
|| nc
!=n
[i
];
2837 children
.push_back( nc
);
2840 ret
= NodeManager::currentNM()->mkNode( n
.getKind(), children
);
2852 void SmtEnginePrivate::removeITEs() {
2853 d_smt
.finalOptionsAreSet();
2854 spendResource(options::preprocessStep());
2855 Trace("simplify") << "SmtEnginePrivate::removeITEs()" << endl
;
2857 // Remove all of the ITE occurrences and normalize
2858 d_iteRemover
.run(d_assertions
.ref(), d_iteSkolemMap
, true);
2859 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
2860 d_assertions
.replace(i
, Rewriter::rewrite(d_assertions
[i
]));
2864 void SmtEnginePrivate::staticLearning() {
2865 d_smt
.finalOptionsAreSet();
2866 spendResource(options::preprocessStep());
2868 TimerStat::CodeTimer
staticLearningTimer(d_smt
.d_stats
->d_staticLearningTime
);
2870 Trace("simplify") << "SmtEnginePrivate::staticLearning()" << endl
;
2872 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
2874 NodeBuilder
<> learned(kind::AND
);
2875 learned
<< d_assertions
[i
];
2876 d_smt
.d_theoryEngine
->ppStaticLearn(d_assertions
[i
], learned
);
2877 if(learned
.getNumChildren() == 1) {
2880 d_assertions
.replace(i
, learned
);
2885 // do dumping (before/after any preprocessing pass)
2886 static void dumpAssertions(const char* key
, const AssertionPipeline
& assertionList
) {
2887 if( Dump
.isOn("assertions") &&
2888 Dump
.isOn(string("assertions:") + key
) ) {
2889 // Push the simplified assertions to the dump output stream
2890 for(unsigned i
= 0; i
< assertionList
.size(); ++ i
) {
2891 TNode n
= assertionList
[i
];
2892 Dump("assertions") << AssertCommand(Expr(n
.toExpr()));
2897 // returns false if it learns a conflict
2898 bool SmtEnginePrivate::nonClausalSimplify() {
2899 spendResource(options::preprocessStep());
2900 d_smt
.finalOptionsAreSet();
2902 if(options::unsatCores() || options::fewerPreprocessingHoles()) {
2906 TimerStat::CodeTimer
nonclausalTimer(d_smt
.d_stats
->d_nonclausalSimplificationTime
);
2908 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify()" << endl
;
2909 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
2910 Trace("simplify") << "Assertion #" << i
<< " : " << d_assertions
[i
] << std::endl
;
2913 if(d_propagatorNeedsFinish
) {
2914 d_propagator
.finish();
2915 d_propagatorNeedsFinish
= false;
2917 d_propagator
.initialize();
2919 // Assert all the assertions to the propagator
2920 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
2921 << "asserting to propagator" << endl
;
2922 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
2923 Assert(Rewriter::rewrite(d_assertions
[i
]) == d_assertions
[i
]);
2924 // Don't reprocess substitutions
2925 if (d_substitutionsIndex
> 0 && i
== d_substitutionsIndex
) {
2928 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): asserting " << d_assertions
[i
] << endl
;
2929 Debug("cores") << "d_propagator assertTrue: " << d_assertions
[i
] << std::endl
;
2930 d_propagator
.assertTrue(d_assertions
[i
]);
2933 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
2934 << "propagating" << endl
;
2935 if (d_propagator
.propagate()) {
2936 // If in conflict, just return false
2937 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
2938 << "conflict in non-clausal propagation" << endl
;
2939 Node falseNode
= NodeManager::currentNM()->mkConst
<bool>(false);
2940 Assert(!options::unsatCores() && !options::fewerPreprocessingHoles());
2941 d_assertions
.clear();
2942 addFormula(falseNode
, false, false);
2943 d_propagatorNeedsFinish
= true;
2948 Trace("simplify") << "Iterate through " << d_nonClausalLearnedLiterals
.size() << " learned literals." << std::endl
;
2949 // No conflict, go through the literals and solve them
2950 SubstitutionMap
constantPropagations(d_smt
.d_context
);
2951 SubstitutionMap
newSubstitutions(d_smt
.d_context
);
2952 SubstitutionMap::iterator pos
;
2954 for(unsigned i
= 0, i_end
= d_nonClausalLearnedLiterals
.size(); i
< i_end
; ++ i
) {
2955 // Simplify the literal we learned wrt previous substitutions
2956 Node learnedLiteral
= d_nonClausalLearnedLiterals
[i
];
2957 Assert(Rewriter::rewrite(learnedLiteral
) == learnedLiteral
);
2958 Assert(d_topLevelSubstitutions
.apply(learnedLiteral
) == learnedLiteral
);
2959 Trace("simplify") << "Process learnedLiteral : " << learnedLiteral
<< std::endl
;
2960 Node learnedLiteralNew
= newSubstitutions
.apply(learnedLiteral
);
2961 if (learnedLiteral
!= learnedLiteralNew
) {
2962 learnedLiteral
= Rewriter::rewrite(learnedLiteralNew
);
2964 Trace("simplify") << "Process learnedLiteral, after newSubs : " << learnedLiteral
<< std::endl
;
2966 learnedLiteralNew
= constantPropagations
.apply(learnedLiteral
);
2967 if (learnedLiteralNew
== learnedLiteral
) {
2970 ++d_smt
.d_stats
->d_numConstantProps
;
2971 learnedLiteral
= Rewriter::rewrite(learnedLiteralNew
);
2973 Trace("simplify") << "Process learnedLiteral, after constProp : " << learnedLiteral
<< std::endl
;
2974 // It might just simplify to a constant
2975 if (learnedLiteral
.isConst()) {
2976 if (learnedLiteral
.getConst
<bool>()) {
2977 // If the learned literal simplifies to true, it's redundant
2980 // If the learned literal simplifies to false, we're in conflict
2981 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
2983 << d_nonClausalLearnedLiterals
[i
] << endl
;
2984 Assert(!options::unsatCores());
2985 d_assertions
.clear();
2986 addFormula(NodeManager::currentNM()->mkConst
<bool>(false), false, false);
2987 d_propagatorNeedsFinish
= true;
2992 // Solve it with the corresponding theory, possibly adding new
2993 // substitutions to newSubstitutions
2994 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
2995 << "solving " << learnedLiteral
<< endl
;
2997 Theory::PPAssertStatus solveStatus
=
2998 d_smt
.d_theoryEngine
->solve(learnedLiteral
, newSubstitutions
);
3000 switch (solveStatus
) {
3001 case Theory::PP_ASSERT_STATUS_SOLVED
: {
3002 // The literal should rewrite to true
3003 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
3004 << "solved " << learnedLiteral
<< endl
;
3005 Assert(Rewriter::rewrite(newSubstitutions
.apply(learnedLiteral
)).isConst());
3006 // vector<pair<Node, Node> > equations;
3007 // constantPropagations.simplifyLHS(d_topLevelSubstitutions, equations, true);
3008 // if (equations.empty()) {
3011 // Assert(equations[0].first.isConst() && equations[0].second.isConst() && equations[0].first != equations[0].second);
3012 // else fall through
3015 case Theory::PP_ASSERT_STATUS_CONFLICT
:
3016 // If in conflict, we return false
3017 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
3018 << "conflict while solving "
3019 << learnedLiteral
<< endl
;
3020 Assert(!options::unsatCores());
3021 d_assertions
.clear();
3022 addFormula(NodeManager::currentNM()->mkConst
<bool>(false), false, false);
3023 d_propagatorNeedsFinish
= true;
3026 if (d_doConstantProp
&& learnedLiteral
.getKind() == kind::EQUAL
&& (learnedLiteral
[0].isConst() || learnedLiteral
[1].isConst())) {
3027 // constant propagation
3030 if (learnedLiteral
[0].isConst()) {
3031 t
= learnedLiteral
[1];
3032 c
= learnedLiteral
[0];
3035 t
= learnedLiteral
[0];
3036 c
= learnedLiteral
[1];
3038 Assert(!t
.isConst());
3039 Assert(constantPropagations
.apply(t
) == t
);
3040 Assert(d_topLevelSubstitutions
.apply(t
) == t
);
3041 Assert(newSubstitutions
.apply(t
) == t
);
3042 constantPropagations
.addSubstitution(t
, c
);
3043 // vector<pair<Node,Node> > equations;
3044 // constantPropagations.simplifyLHS(t, c, equations, true);
3045 // if (!equations.empty()) {
3046 // Assert(equations[0].first.isConst() && equations[0].second.isConst() && equations[0].first != equations[0].second);
3047 // d_assertions.clear();
3048 // addFormula(NodeManager::currentNM()->mkConst<bool>(false), false, false);
3051 // d_topLevelSubstitutions.simplifyRHS(constantPropagations);
3055 d_nonClausalLearnedLiterals
[j
++] = d_nonClausalLearnedLiterals
[i
];
3061 #ifdef CVC4_ASSERTIONS
3062 // NOTE: When debugging this code, consider moving this check inside of the
3063 // loop over d_nonClausalLearnedLiterals. This check has been moved outside
3064 // because it is costly for certain inputs (see bug 508).
3066 // Check data structure invariants:
3067 // 1. for each lhs of d_topLevelSubstitutions, does not appear anywhere in rhs of d_topLevelSubstitutions or anywhere in constantPropagations
3068 // 2. each lhs of constantPropagations rewrites to itself
3069 // 3. if l -> r is a constant propagation and l is a subterm of l' with l' -> r' another constant propagation, then l'[l/r] -> r' should be a
3070 // constant propagation too
3071 // 4. each lhs of constantPropagations is different from each rhs
3072 for (pos
= newSubstitutions
.begin(); pos
!= newSubstitutions
.end(); ++pos
) {
3073 Assert((*pos
).first
.isVar());
3074 Assert(d_topLevelSubstitutions
.apply((*pos
).first
) == (*pos
).first
);
3075 Assert(d_topLevelSubstitutions
.apply((*pos
).second
) == (*pos
).second
);
3076 Assert(newSubstitutions
.apply(newSubstitutions
.apply((*pos
).second
)) == newSubstitutions
.apply((*pos
).second
));
3078 for (pos
= constantPropagations
.begin(); pos
!= constantPropagations
.end(); ++pos
) {
3079 Assert((*pos
).second
.isConst());
3080 Assert(Rewriter::rewrite((*pos
).first
) == (*pos
).first
);
3081 // Node newLeft = d_topLevelSubstitutions.apply((*pos).first);
3082 // if (newLeft != (*pos).first) {
3083 // newLeft = Rewriter::rewrite(newLeft);
3084 // Assert(newLeft == (*pos).second ||
3085 // (constantPropagations.hasSubstitution(newLeft) && constantPropagations.apply(newLeft) == (*pos).second));
3087 // newLeft = constantPropagations.apply((*pos).first);
3088 // if (newLeft != (*pos).first) {
3089 // newLeft = Rewriter::rewrite(newLeft);
3090 // Assert(newLeft == (*pos).second ||
3091 // (constantPropagations.hasSubstitution(newLeft) && constantPropagations.apply(newLeft) == (*pos).second));
3093 Assert(constantPropagations
.apply((*pos
).second
) == (*pos
).second
);
3095 #endif /* CVC4_ASSERTIONS */
3097 // Resize the learnt
3098 Trace("simplify") << "Resize non-clausal learned literals to " << j
<< std::endl
;
3099 d_nonClausalLearnedLiterals
.resize(j
);
3101 unordered_set
<TNode
, TNodeHashFunction
> s
;
3102 Trace("debugging") << "NonClausal simplify pre-preprocess\n";
3103 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
3104 Node assertion
= d_assertions
[i
];
3105 Node assertionNew
= newSubstitutions
.apply(assertion
);
3106 Trace("debugging") << "assertion = " << assertion
<< endl
;
3107 Trace("debugging") << "assertionNew = " << assertionNew
<< endl
;
3108 if (assertion
!= assertionNew
) {
3109 assertion
= Rewriter::rewrite(assertionNew
);
3110 Trace("debugging") << "rewrite(assertion) = " << assertion
<< endl
;
3112 Assert(Rewriter::rewrite(assertion
) == assertion
);
3114 assertionNew
= constantPropagations
.apply(assertion
);
3115 if (assertionNew
== assertion
) {
3118 ++d_smt
.d_stats
->d_numConstantProps
;
3119 Trace("debugging") << "assertionNew = " << assertionNew
<< endl
;
3120 assertion
= Rewriter::rewrite(assertionNew
);
3121 Trace("debugging") << "assertionNew = " << assertionNew
<< endl
;
3123 Trace("debugging") << "\n";
3124 s
.insert(assertion
);
3125 d_assertions
.replace(i
, assertion
);
3126 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
3127 << "non-clausal preprocessed: "
3128 << assertion
<< endl
;
3131 // If in incremental mode, add substitutions to the list of assertions
3132 if (d_substitutionsIndex
> 0) {
3133 NodeBuilder
<> substitutionsBuilder(kind::AND
);
3134 substitutionsBuilder
<< d_assertions
[d_substitutionsIndex
];
3135 pos
= newSubstitutions
.begin();
3136 for (; pos
!= newSubstitutions
.end(); ++pos
) {
3137 // Add back this substitution as an assertion
3138 TNode lhs
= (*pos
).first
, rhs
= newSubstitutions
.apply((*pos
).second
);
3139 Node n
= NodeManager::currentNM()->mkNode(kind::EQUAL
, lhs
, rhs
);
3140 substitutionsBuilder
<< n
;
3141 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): will notify SAT layer of substitution: " << n
<< endl
;
3143 if (substitutionsBuilder
.getNumChildren() > 1) {
3144 d_assertions
.replace(d_substitutionsIndex
,
3145 Rewriter::rewrite(Node(substitutionsBuilder
)));
3148 // If not in incremental mode, must add substitutions to model
3149 TheoryModel
* m
= d_smt
.d_theoryEngine
->getModel();
3151 for(pos
= newSubstitutions
.begin(); pos
!= newSubstitutions
.end(); ++pos
) {
3152 Node n
= (*pos
).first
;
3153 Node v
= newSubstitutions
.apply((*pos
).second
);
3154 Trace("model") << "Add substitution : " << n
<< " " << v
<< endl
;
3155 m
->addSubstitution( n
, v
);
3160 NodeBuilder
<> learnedBuilder(kind::AND
);
3161 Assert(d_realAssertionsEnd
<= d_assertions
.size());
3162 learnedBuilder
<< d_assertions
[d_realAssertionsEnd
- 1];
3164 for (unsigned i
= 0; i
< d_nonClausalLearnedLiterals
.size(); ++ i
) {
3165 Node learned
= d_nonClausalLearnedLiterals
[i
];
3166 Assert(d_topLevelSubstitutions
.apply(learned
) == learned
);
3167 Node learnedNew
= newSubstitutions
.apply(learned
);
3168 if (learned
!= learnedNew
) {
3169 learned
= Rewriter::rewrite(learnedNew
);
3171 Assert(Rewriter::rewrite(learned
) == learned
);
3173 learnedNew
= constantPropagations
.apply(learned
);
3174 if (learnedNew
== learned
) {
3177 ++d_smt
.d_stats
->d_numConstantProps
;
3178 learned
= Rewriter::rewrite(learnedNew
);
3180 if (s
.find(learned
) != s
.end()) {
3184 learnedBuilder
<< learned
;
3185 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
3186 << "non-clausal learned : "
3189 d_nonClausalLearnedLiterals
.clear();
3191 for (pos
= constantPropagations
.begin(); pos
!= constantPropagations
.end(); ++pos
) {
3192 Node cProp
= (*pos
).first
.eqNode((*pos
).second
);
3193 Assert(d_topLevelSubstitutions
.apply(cProp
) == cProp
);
3194 Node cPropNew
= newSubstitutions
.apply(cProp
);
3195 if (cProp
!= cPropNew
) {
3196 cProp
= Rewriter::rewrite(cPropNew
);
3197 Assert(Rewriter::rewrite(cProp
) == cProp
);
3199 if (s
.find(cProp
) != s
.end()) {
3203 learnedBuilder
<< cProp
;
3204 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
3205 << "non-clausal constant propagation : "
3209 // Add new substitutions to topLevelSubstitutions
3210 // Note that we don't have to keep rhs's in full solved form
3211 // because SubstitutionMap::apply does a fixed-point iteration when substituting
3212 d_topLevelSubstitutions
.addSubstitutions(newSubstitutions
);
3214 if(learnedBuilder
.getNumChildren() > 1) {
3215 d_assertions
.replace(d_realAssertionsEnd
- 1,
3216 Rewriter::rewrite(Node(learnedBuilder
)));
3219 d_propagatorNeedsFinish
= true;
3223 void SmtEnginePrivate::bvAbstraction() {
3224 Trace("bv-abstraction") << "SmtEnginePrivate::bvAbstraction()" << endl
;
3225 std::vector
<Node
> new_assertions
;
3226 bool changed
= d_smt
.d_theoryEngine
->ppBvAbstraction(d_assertions
.ref(), new_assertions
);
3227 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
3228 d_assertions
.replace(i
, Rewriter::rewrite(new_assertions
[i
]));
3230 // if we are using the lazy solver and the abstraction
3231 // applies, then UF symbols were introduced
3232 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY
&&
3234 LogicRequest
req(d_smt
);
3235 req
.widenLogic(THEORY_UF
);
3240 void SmtEnginePrivate::bvToBool() {
3241 Trace("bv-to-bool") << "SmtEnginePrivate::bvToBool()" << endl
;
3242 spendResource(options::preprocessStep());
3243 std::vector
<Node
> new_assertions
;
3244 d_smt
.d_theoryEngine
->ppBvToBool(d_assertions
.ref(), new_assertions
);
3245 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
3246 d_assertions
.replace(i
, Rewriter::rewrite(new_assertions
[i
]));
3250 void SmtEnginePrivate::boolToBv() {
3251 Trace("bool-to-bv") << "SmtEnginePrivate::boolToBv()" << endl
;
3252 spendResource(options::preprocessStep());
3253 std::vector
<Node
> new_assertions
;
3254 d_smt
.d_theoryEngine
->ppBoolToBv(d_assertions
.ref(), new_assertions
);
3255 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
3256 d_assertions
.replace(i
, Rewriter::rewrite(new_assertions
[i
]));
3260 bool SmtEnginePrivate::simpITE() {
3261 TimerStat::CodeTimer
simpITETimer(d_smt
.d_stats
->d_simpITETime
);
3263 spendResource(options::preprocessStep());
3265 Trace("simplify") << "SmtEnginePrivate::simpITE()" << endl
;
3267 unsigned numAssertionOnEntry
= d_assertions
.size();
3268 for (unsigned i
= 0; i
< d_assertions
.size(); ++i
) {
3269 spendResource(options::preprocessStep());
3270 Node result
= d_smt
.d_theoryEngine
->ppSimpITE(d_assertions
[i
]);
3271 d_assertions
.replace(i
, result
);
3272 if(result
.isConst() && !result
.getConst
<bool>()){
3276 bool result
= d_smt
.d_theoryEngine
->donePPSimpITE(d_assertions
.ref());
3277 if(numAssertionOnEntry
< d_assertions
.size()){
3278 compressBeforeRealAssertions(numAssertionOnEntry
);
3283 void SmtEnginePrivate::compressBeforeRealAssertions(size_t before
){
3284 size_t curr
= d_assertions
.size();
3285 if(before
>= curr
||
3286 d_realAssertionsEnd
<= 0 ||
3287 d_realAssertionsEnd
>= curr
){
3292 // original: [0 ... d_realAssertionsEnd)
3294 // ites skolems [d_realAssertionsEnd, before)
3296 // added [before, curr)
3298 Assert(0 < d_realAssertionsEnd
);
3299 Assert(d_realAssertionsEnd
<= before
);
3300 Assert(before
< curr
);
3302 std::vector
<Node
> intoConjunction
;
3303 for(size_t i
= before
; i
<curr
; ++i
){
3304 intoConjunction
.push_back(d_assertions
[i
]);
3306 d_assertions
.resize(before
);
3307 size_t lastBeforeItes
= d_realAssertionsEnd
- 1;
3308 intoConjunction
.push_back(d_assertions
[lastBeforeItes
]);
3309 Node newLast
= util::NaryBuilder::mkAssoc(kind::AND
, intoConjunction
);
3310 d_assertions
.replace(lastBeforeItes
, newLast
);
3311 Assert(d_assertions
.size() == before
);
3314 void SmtEnginePrivate::unconstrainedSimp() {
3315 TimerStat::CodeTimer
unconstrainedSimpTimer(d_smt
.d_stats
->d_unconstrainedSimpTime
);
3316 spendResource(options::preprocessStep());
3317 Trace("simplify") << "SmtEnginePrivate::unconstrainedSimp()" << endl
;
3318 d_smt
.d_theoryEngine
->ppUnconstrainedSimp(d_assertions
.ref());
3321 void SmtEnginePrivate::traceBackToAssertions(const std::vector
<Node
>& nodes
, std::vector
<TNode
>& assertions
) {
3322 const booleans::CircuitPropagator::BackEdgesMap
& backEdges
= d_propagator
.getBackEdges();
3323 for(vector
<Node
>::const_iterator i
= nodes
.begin(); i
!= nodes
.end(); ++i
) {
3324 booleans::CircuitPropagator::BackEdgesMap::const_iterator j
= backEdges
.find(*i
);
3325 // term must appear in map, otherwise how did we get here?!
3326 Assert(j
!= backEdges
.end());
3327 // if term maps to empty, that means it's a top-level assertion
3328 if(!(*j
).second
.empty()) {
3329 traceBackToAssertions((*j
).second
, assertions
);
3331 assertions
.push_back(*i
);
3336 size_t SmtEnginePrivate::removeFromConjunction(Node
& n
, const std::unordered_set
<unsigned long>& toRemove
) {
3337 Assert(n
.getKind() == kind::AND
);
3338 size_t removals
= 0;
3339 for(Node::iterator j
= n
.begin(); j
!= n
.end(); ++j
) {
3340 size_t subremovals
= 0;
3342 if(toRemove
.find(sub
.getId()) != toRemove
.end() ||
3343 (sub
.getKind() == kind::AND
&& (subremovals
= removeFromConjunction(sub
, toRemove
)) > 0)) {
3344 NodeBuilder
<> b(kind::AND
);
3345 b
.append(n
.begin(), j
);
3346 if(subremovals
> 0) {
3347 removals
+= subremovals
;
3352 for(++j
; j
!= n
.end(); ++j
) {
3353 if(toRemove
.find((*j
).getId()) != toRemove
.end()) {
3355 } else if((*j
).getKind() == kind::AND
) {
3357 if((subremovals
= removeFromConjunction(sub
, toRemove
)) > 0) {
3358 removals
+= subremovals
;
3367 if(b
.getNumChildren() == 0) {
3370 } else if(b
.getNumChildren() == 1) {
3376 n
= Rewriter::rewrite(n
);
3381 Assert(removals
== 0);
3385 void SmtEnginePrivate::doMiplibTrick() {
3386 Assert(d_realAssertionsEnd
== d_assertions
.size());
3387 Assert(!options::incrementalSolving());
3389 const booleans::CircuitPropagator::BackEdgesMap
& backEdges
= d_propagator
.getBackEdges();
3390 unordered_set
<unsigned long> removeAssertions
;
3392 NodeManager
* nm
= NodeManager::currentNM();
3393 Node zero
= nm
->mkConst(Rational(0)), one
= nm
->mkConst(Rational(1));
3395 unordered_map
<TNode
, Node
, TNodeHashFunction
> intVars
;
3396 for(vector
<Node
>::const_iterator i
= d_boolVars
.begin(); i
!= d_boolVars
.end(); ++i
) {
3397 if(d_propagator
.isAssigned(*i
)) {
3398 Debug("miplib") << "ineligible: " << *i
<< " because assigned " << d_propagator
.getAssignment(*i
) << endl
;
3402 vector
<TNode
> assertions
;
3403 booleans::CircuitPropagator::BackEdgesMap::const_iterator j
= backEdges
.find(*i
);
3404 // if not in back edges map, the bool var is unconstrained, showing up in no assertions.
3405 // if maps to an empty vector, that means the bool var was asserted itself.
3406 if(j
!= backEdges
.end()) {
3407 if(!(*j
).second
.empty()) {
3408 traceBackToAssertions((*j
).second
, assertions
);
3410 assertions
.push_back(*i
);
3413 Debug("miplib") << "for " << *i
<< endl
;
3414 bool eligible
= true;
3415 map
<pair
<Node
, Node
>, uint64_t> marks
;
3416 map
<pair
<Node
, Node
>, vector
<Rational
> > coef
;
3417 map
<pair
<Node
, Node
>, vector
<Rational
> > checks
;
3418 map
<pair
<Node
, Node
>, vector
<TNode
> > asserts
;
3419 for(vector
<TNode
>::const_iterator j
= assertions
.begin(); j
!= assertions
.end(); ++j
) {
3420 Debug("miplib") << " found: " << *j
<< endl
;
3421 if((*j
).getKind() != kind::IMPLIES
) {
3423 Debug("miplib") << " -- INELIGIBLE -- (not =>)" << endl
;
3426 Node conj
= BooleanSimplification::simplify((*j
)[0]);
3427 if(conj
.getKind() == kind::AND
&& conj
.getNumChildren() > 6) {
3429 Debug("miplib") << " -- INELIGIBLE -- (N-ary /\\ too big)" << endl
;
3432 if(conj
.getKind() != kind::AND
&& !conj
.isVar() && !(conj
.getKind() == kind::NOT
&& conj
[0].isVar())) {
3434 Debug("miplib") << " -- INELIGIBLE -- (not /\\ or literal)" << endl
;
3437 if((*j
)[1].getKind() != kind::EQUAL
||
3438 !( ( (*j
)[1][0].isVar() &&
3439 (*j
)[1][1].getKind() == kind::CONST_RATIONAL
) ||
3440 ( (*j
)[1][0].getKind() == kind::CONST_RATIONAL
&&
3441 (*j
)[1][1].isVar() ) )) {
3443 Debug("miplib") << " -- INELIGIBLE -- (=> (and X X) X)" << endl
;
3446 if(conj
.getKind() == kind::AND
) {
3448 bool found_x
= false;
3449 map
<TNode
, bool> neg
;
3450 for(Node::iterator ii
= conj
.begin(); ii
!= conj
.end(); ++ii
) {
3452 posv
.push_back(*ii
);
3454 found_x
= found_x
|| *i
== *ii
;
3455 } else if((*ii
).getKind() == kind::NOT
&& (*ii
)[0].isVar()) {
3456 posv
.push_back((*ii
)[0]);
3457 neg
[(*ii
)[0]] = true;
3458 found_x
= found_x
|| *i
== (*ii
)[0];
3461 Debug("miplib") << " -- INELIGIBLE -- (non-var: " << *ii
<< ")" << endl
;
3464 if(d_propagator
.isAssigned(posv
.back())) {
3466 Debug("miplib") << " -- INELIGIBLE -- (" << posv
.back() << " asserted)" << endl
;
3475 Debug("miplib") << " --INELIGIBLE -- (couldn't find " << *i
<< " in conjunction)" << endl
;
3478 sort(posv
.begin(), posv
.end());
3479 const Node pos
= NodeManager::currentNM()->mkNode(kind::AND
, posv
);
3480 const TNode var
= ((*j
)[1][0].getKind() == kind::CONST_RATIONAL
) ? (*j
)[1][1] : (*j
)[1][0];
3481 const pair
<Node
, Node
> pos_var(pos
, var
);
3482 const Rational
& constant
= ((*j
)[1][0].getKind() == kind::CONST_RATIONAL
) ? (*j
)[1][0].getConst
<Rational
>() : (*j
)[1][1].getConst
<Rational
>();
3484 unsigned countneg
= 0, thepos
= 0;
3485 for(unsigned ii
= 0; ii
< pos
.getNumChildren(); ++ii
) {
3490 mark
|= (0x1 << ii
);
3493 if((marks
[pos_var
] & (1lu << mark
)) != 0) {
3495 Debug("miplib") << " -- INELIGIBLE -- (remarked)" << endl
;
3498 Debug("miplib") << "mark is " << mark
<< " -- " << (1lu << mark
) << endl
;
3499 marks
[pos_var
] |= (1lu << mark
);
3500 Debug("miplib") << "marks[" << pos
<< "," << var
<< "] now " << marks
[pos_var
] << endl
;
3501 if(countneg
== pos
.getNumChildren()) {
3504 Debug("miplib") << " -- INELIGIBLE -- (nonzero constant)" << endl
;
3507 } else if(countneg
== pos
.getNumChildren() - 1) {
3508 Assert(coef
[pos_var
].size() <= 6 && thepos
< 6);
3509 if(coef
[pos_var
].size() <= thepos
) {
3510 coef
[pos_var
].resize(thepos
+ 1);
3512 coef
[pos_var
][thepos
] = constant
;
3514 if(checks
[pos_var
].size() <= mark
) {
3515 checks
[pos_var
].resize(mark
+ 1);
3517 checks
[pos_var
][mark
] = constant
;
3519 asserts
[pos_var
].push_back(*j
);
3522 if(x
!= *i
&& x
!= (*i
).notNode()) {
3524 Debug("miplib") << " -- INELIGIBLE -- (x not present where I expect it)" << endl
;
3527 const bool xneg
= (x
.getKind() == kind::NOT
);
3528 x
= xneg
? x
[0] : x
;
3529 Debug("miplib") << " x:" << x
<< " " << xneg
<< endl
;
3530 const TNode var
= ((*j
)[1][0].getKind() == kind::CONST_RATIONAL
) ? (*j
)[1][1] : (*j
)[1][0];
3531 const pair
<Node
, Node
> x_var(x
, var
);
3532 const Rational
& constant
= ((*j
)[1][0].getKind() == kind::CONST_RATIONAL
) ? (*j
)[1][0].getConst
<Rational
>() : (*j
)[1][1].getConst
<Rational
>();
3533 unsigned mark
= (xneg
? 0 : 1);
3534 if((marks
[x_var
] & (1u << mark
)) != 0) {
3536 Debug("miplib") << " -- INELIGIBLE -- (remarked)" << endl
;
3539 marks
[x_var
] |= (1u << mark
);
3543 Debug("miplib") << " -- INELIGIBLE -- (nonzero constant)" << endl
;
3547 Assert(coef
[x_var
].size() <= 6);
3548 coef
[x_var
].resize(6);
3549 coef
[x_var
][0] = constant
;
3551 asserts
[x_var
].push_back(*j
);
3555 for(map
<pair
<Node
, Node
>, uint64_t>::const_iterator j
= marks
.begin(); j
!= marks
.end(); ++j
) {
3556 const TNode pos
= (*j
).first
.first
;
3557 const TNode var
= (*j
).first
.second
;
3558 const pair
<Node
, Node
>& pos_var
= (*j
).first
;
3559 const uint64_t mark
= (*j
).second
;
3560 const unsigned numVars
= pos
.getKind() == kind::AND
? pos
.getNumChildren() : 1;
3561 uint64_t expected
= (uint64_t(1) << (1 << numVars
)) - 1;
3562 expected
= (expected
== 0) ? -1 : expected
; // fix for overflow
3563 Debug("miplib") << "[" << pos
<< "] => " << hex
<< mark
<< " expect " << expected
<< dec
<< endl
;
3564 Assert(pos
.getKind() == kind::AND
|| pos
.isVar());
3565 if(mark
!= expected
) {
3566 Debug("miplib") << " -- INELIGIBLE " << pos
<< " -- (insufficiently marked, got " << mark
<< " for " << numVars
<< " vars, expected " << expected
<< endl
;
3568 if(mark
!= 3) { // exclude single-var case; nothing to check there
3569 uint64_t sz
= (uint64_t(1) << checks
[pos_var
].size()) - 1;
3570 sz
= (sz
== 0) ? -1 : sz
; // fix for overflow
3571 Assert(sz
== mark
, "expected size %u == mark %u", sz
, mark
);
3572 for(size_t k
= 0; k
< checks
[pos_var
].size(); ++k
) {
3573 if((k
& (k
- 1)) != 0) {
3575 Debug("miplib") << k
<< " => " << checks
[pos_var
][k
] << endl
;
3576 for(size_t v
= 1, kk
= k
; kk
!= 0; ++v
, kk
>>= 1) {
3577 if((kk
& 0x1) == 1) {
3578 Assert(pos
.getKind() == kind::AND
);
3579 Debug("miplib") << "var " << v
<< " : " << pos
[v
- 1] << " coef:" << coef
[pos_var
][v
- 1] << endl
;
3580 sum
+= coef
[pos_var
][v
- 1];
3583 Debug("miplib") << "checkSum is " << sum
<< " input says " << checks
[pos_var
][k
] << endl
;
3584 if(sum
!= checks
[pos_var
][k
]) {
3586 Debug("miplib") << " -- INELIGIBLE " << pos
<< " -- (nonlinear combination)" << endl
;
3590 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
3595 eligible
= true; // next is still eligible
3599 Debug("miplib") << " -- ELIGIBLE " << *i
<< " , " << pos
<< " --" << endl
;
3600 vector
<Node
> newVars
;
3601 expr::NodeSelfIterator ii
, iiend
;
3602 if(pos
.getKind() == kind::AND
) {
3606 ii
= expr::NodeSelfIterator::self(pos
);
3607 iiend
= expr::NodeSelfIterator::selfEnd(pos
);
3609 for(; ii
!= iiend
; ++ii
) {
3610 Node
& varRef
= intVars
[*ii
];
3611 if(varRef
.isNull()) {
3613 ss
<< "mipvar_" << *ii
;
3614 Node newVar
= nm
->mkSkolem(ss
.str(), nm
->integerType(), "a variable introduced due to scrubbing a miplib encoding", NodeManager::SKOLEM_EXACT_NAME
);
3615 Node geq
= Rewriter::rewrite(nm
->mkNode(kind::GEQ
, newVar
, zero
));
3616 Node leq
= Rewriter::rewrite(nm
->mkNode(kind::LEQ
, newVar
, one
));
3617 addFormula(Rewriter::rewrite(geq
.andNode(leq
)), false, false);
3618 SubstitutionMap
nullMap(&d_fakeContext
);
3619 Theory::PPAssertStatus status CVC4_UNUSED
; // just for assertions
3620 status
= d_smt
.d_theoryEngine
->solve(geq
, nullMap
);
3621 Assert(status
== Theory::PP_ASSERT_STATUS_UNSOLVED
,
3622 "unexpected solution from arith's ppAssert()");
3623 Assert(nullMap
.empty(),
3624 "unexpected substitution from arith's ppAssert()");
3625 status
= d_smt
.d_theoryEngine
->solve(leq
, nullMap
);
3626 Assert(status
== Theory::PP_ASSERT_STATUS_UNSOLVED
,
3627 "unexpected solution from arith's ppAssert()");
3628 Assert(nullMap
.empty(),
3629 "unexpected substitution from arith's ppAssert()");
3630 d_smt
.d_theoryEngine
->getModel()->addSubstitution(*ii
, newVar
.eqNode(one
));
3631 newVars
.push_back(newVar
);
3634 newVars
.push_back(varRef
);
3636 if(!d_smt
.d_logic
.areIntegersUsed()) {
3637 d_smt
.d_logic
= d_smt
.d_logic
.getUnlockedCopy();
3638 d_smt
.d_logic
.enableIntegers();
3639 d_smt
.d_logic
.lock();
3643 if(pos
.getKind() == kind::AND
) {
3644 NodeBuilder
<> sumb(kind::PLUS
);
3645 for(size_t ii
= 0; ii
< pos
.getNumChildren(); ++ii
) {
3646 sumb
<< nm
->mkNode(kind::MULT
, nm
->mkConst(coef
[pos_var
][ii
]), newVars
[ii
]);
3650 sum
= nm
->mkNode(kind::MULT
, nm
->mkConst(coef
[pos_var
][0]), newVars
[0]);
3652 Debug("miplib") << "vars[] " << var
<< endl
3653 << " eq " << Rewriter::rewrite(sum
) << endl
;
3654 Node newAssertion
= var
.eqNode(Rewriter::rewrite(sum
));
3655 if(d_topLevelSubstitutions
.hasSubstitution(newAssertion
[0])) {
3656 //Warning() << "RE-SUBSTITUTION " << newAssertion[0] << endl;
3657 //Warning() << "REPLACE " << newAssertion[1] << endl;
3658 //Warning() << "ORIG " << d_topLevelSubstitutions.getSubstitution(newAssertion[0]) << endl;
3659 Assert(d_topLevelSubstitutions
.getSubstitution(newAssertion
[0]) == newAssertion
[1]);
3660 } else if(pos
.getNumChildren() <= options::arithMLTrickSubstitutions()) {
3661 d_topLevelSubstitutions
.addSubstitution(newAssertion
[0], newAssertion
[1]);
3662 Debug("miplib") << "addSubs: " << newAssertion
[0] << " to " << newAssertion
[1] << endl
;
3664 Debug("miplib") << "skipSubs: " << newAssertion
[0] << " to " << newAssertion
[1] << " (threshold is " << options::arithMLTrickSubstitutions() << ")" << endl
;
3666 newAssertion
= Rewriter::rewrite(newAssertion
);
3667 Debug("miplib") << " " << newAssertion
<< endl
;
3668 addFormula(newAssertion
, false, false);
3669 Debug("miplib") << " assertions to remove: " << endl
;
3670 for(vector
<TNode
>::const_iterator k
= asserts
[pos_var
].begin(), k_end
= asserts
[pos_var
].end(); k
!= k_end
; ++k
) {
3671 Debug("miplib") << " " << *k
<< endl
;
3672 removeAssertions
.insert((*k
).getId());
3678 if(!removeAssertions
.empty()) {
3679 Debug("miplib") << "SmtEnginePrivate::simplify(): scrubbing miplib encoding..." << endl
;
3680 for(size_t i
= 0; i
< d_realAssertionsEnd
; ++i
) {
3681 if(removeAssertions
.find(d_assertions
[i
].getId()) != removeAssertions
.end()) {
3682 Debug("miplib") << "SmtEnginePrivate::simplify(): - removing " << d_assertions
[i
] << endl
;
3683 d_assertions
[i
] = d_true
;
3684 ++d_smt
.d_stats
->d_numMiplibAssertionsRemoved
;
3685 } else if(d_assertions
[i
].getKind() == kind::AND
) {
3686 size_t removals
= removeFromConjunction(d_assertions
[i
], removeAssertions
);
3688 Debug("miplib") << "SmtEnginePrivate::simplify(): - reduced " << d_assertions
[i
] << endl
;
3689 Debug("miplib") << "SmtEnginePrivate::simplify(): - by " << removals
<< " conjuncts" << endl
;
3690 d_smt
.d_stats
->d_numMiplibAssertionsRemoved
+= removals
;
3693 Debug("miplib") << "had: " << d_assertions
[i
] << endl
;
3694 d_assertions
[i
] = Rewriter::rewrite(d_topLevelSubstitutions
.apply(d_assertions
[i
]));
3695 Debug("miplib") << "now: " << d_assertions
[i
] << endl
;
3698 Debug("miplib") << "SmtEnginePrivate::simplify(): miplib pass found nothing." << endl
;
3700 d_realAssertionsEnd
= d_assertions
.size();
3704 // returns false if simplification led to "false"
3705 bool SmtEnginePrivate::simplifyAssertions()
3706 throw(TypeCheckingException
, LogicException
, UnsafeInterruptException
) {
3707 spendResource(options::preprocessStep());
3708 Assert(d_smt
.d_pendingPops
== 0);
3710 ScopeCounter
depth(d_simplifyAssertionsDepth
);
3712 Trace("simplify") << "SmtEnginePrivate::simplify()" << endl
;
3714 dumpAssertions("pre-nonclausal", d_assertions
);
3716 if(options::simplificationMode() != SIMPLIFICATION_MODE_NONE
) {
3717 // Perform non-clausal simplification
3718 Chat() << "...performing nonclausal simplification..." << endl
;
3719 Trace("simplify") << "SmtEnginePrivate::simplify(): "
3720 << "performing non-clausal simplification" << endl
;
3721 bool noConflict
= nonClausalSimplify();
3726 // We piggy-back off of the BackEdgesMap in the CircuitPropagator to
3727 // do the miplib trick.
3728 if( // check that option is on
3729 options::arithMLTrick() &&
3730 // miplib rewrites aren't safe in incremental mode
3731 ! options::incrementalSolving() &&
3732 // only useful in arith
3733 d_smt
.d_logic
.isTheoryEnabled(THEORY_ARITH
) &&
3734 // we add new assertions and need this (in practice, this
3735 // restriction only disables miplib processing during
3736 // re-simplification, which we don't expect to be useful anyway)
3737 d_realAssertionsEnd
== d_assertions
.size() ) {
3738 Chat() << "...fixing miplib encodings..." << endl
;
3739 Trace("simplify") << "SmtEnginePrivate::simplify(): "
3740 << "looking for miplib pseudobooleans..." << endl
;
3742 TimerStat::CodeTimer
miplibTimer(d_smt
.d_stats
->d_miplibPassTime
);
3746 Trace("simplify") << "SmtEnginePrivate::simplify(): "
3747 << "skipping miplib pseudobooleans pass (either incrementalSolving is on, or miplib pbs are turned off)..." << endl
;
3751 dumpAssertions("post-nonclausal", d_assertions
);
3752 Trace("smt") << "POST nonClausalSimplify" << endl
;
3753 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
3755 // before ppRewrite check if only core theory for BV theory
3756 d_smt
.d_theoryEngine
->staticInitializeBVOptions(d_assertions
.ref());
3758 dumpAssertions("pre-theorypp", d_assertions
);
3760 // Theory preprocessing
3761 if (d_smt
.d_earlyTheoryPP
) {
3762 Chat() << "...doing early theory preprocessing..." << endl
;
3763 TimerStat::CodeTimer
codeTimer(d_smt
.d_stats
->d_theoryPreprocessTime
);
3764 // Call the theory preprocessors
3765 d_smt
.d_theoryEngine
->preprocessStart();
3766 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
3767 Assert(Rewriter::rewrite(d_assertions
[i
]) == d_assertions
[i
]);
3768 d_assertions
.replace(i
, d_smt
.d_theoryEngine
->preprocess(d_assertions
[i
]));
3769 Assert(Rewriter::rewrite(d_assertions
[i
]) == d_assertions
[i
]);
3773 dumpAssertions("post-theorypp", d_assertions
);
3774 Trace("smt") << "POST theoryPP" << endl
;
3775 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
3777 // ITE simplification
3778 if(options::doITESimp() &&
3779 (d_simplifyAssertionsDepth
<= 1 || options::doITESimpOnRepeat())) {
3780 Chat() << "...doing ITE simplification..." << endl
;
3781 bool noConflict
= simpITE();
3783 Chat() << "...ITE simplification found unsat..." << endl
;
3788 dumpAssertions("post-itesimp", d_assertions
);
3789 Trace("smt") << "POST iteSimp" << endl
;
3790 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
3792 // Unconstrained simplification
3793 if(options::unconstrainedSimp()) {
3794 Chat() << "...doing unconstrained simplification..." << endl
;
3795 unconstrainedSimp();
3798 dumpAssertions("post-unconstrained", d_assertions
);
3799 Trace("smt") << "POST unconstrainedSimp" << endl
;
3800 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
3802 if(options::repeatSimp() && options::simplificationMode() != SIMPLIFICATION_MODE_NONE
) {
3803 Chat() << "...doing another round of nonclausal simplification..." << endl
;
3804 Trace("simplify") << "SmtEnginePrivate::simplify(): "
3805 << " doing repeated simplification" << endl
;
3806 bool noConflict
= nonClausalSimplify();
3812 dumpAssertions("post-repeatsimp", d_assertions
);
3813 Trace("smt") << "POST repeatSimp" << endl
;
3814 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
3816 } catch(TypeCheckingExceptionPrivate
& tcep
) {
3817 // Calls to this function should have already weeded out any
3818 // typechecking exceptions via (e.g.) ensureBoolean(). But a
3819 // theory could still create a new expression that isn't
3820 // well-typed, and we don't want the C++ runtime to abort our
3821 // process without any error notice.
3823 ss
<< "A bad expression was produced. Original exception follows:\n"
3825 InternalError(ss
.str().c_str());
3830 Result
SmtEngine::check() {
3831 Assert(d_fullyInited
);
3832 Assert(d_pendingPops
== 0);
3834 Trace("smt") << "SmtEngine::check()" << endl
;
3836 ResourceManager
* resourceManager
= d_private
->getResourceManager();
3838 resourceManager
->beginCall();
3840 // Only way we can be out of resource is if cumulative budget is on
3841 if (resourceManager
->cumulativeLimitOn() &&
3842 resourceManager
->out()) {
3843 Result::UnknownExplanation why
= resourceManager
->outOfResources() ?
3844 Result::RESOURCEOUT
: Result::TIMEOUT
;
3845 return Result(Result::VALIDITY_UNKNOWN
, why
, d_filename
);
3848 // Make sure the prop layer has all of the assertions
3849 Trace("smt") << "SmtEngine::check(): processing assertions" << endl
;
3850 d_private
->processAssertions();
3851 Trace("smt") << "SmtEngine::check(): done processing assertions" << endl
;
3853 // Turn off stop only for QF_LRA
3854 // TODO: Bring up in a meeting where to put this
3855 if(options::decisionStopOnly() && !options::decisionMode
.wasSetByUser() ){
3857 (not d_logic
.isQuantified() &&
3858 d_logic
.isPure(THEORY_ARITH
) && d_logic
.isLinear() && !d_logic
.isDifferenceLogic() && !d_logic
.areIntegersUsed()
3860 if(d_private
->d_iteSkolemMap
.empty()){
3861 options::decisionStopOnly
.set(false);
3862 d_decisionEngine
->clearStrategies();
3863 Trace("smt") << "SmtEngine::check(): turning off stop only" << endl
;
3868 TimerStat::CodeTimer
solveTimer(d_stats
->d_solveTime
);
3870 Chat() << "solving..." << endl
;
3871 Trace("smt") << "SmtEngine::check(): running check" << endl
;
3872 Result result
= d_propEngine
->checkSat();
3874 resourceManager
->endCall();
3875 Trace("limit") << "SmtEngine::check(): cumulative millis " << resourceManager
->getTimeUsage()
3876 << ", resources " << resourceManager
->getResourceUsage() << endl
;
3879 return Result(result
, d_filename
);
3882 Result
SmtEngine::quickCheck() {
3883 Assert(d_fullyInited
);
3884 Trace("smt") << "SMT quickCheck()" << endl
;
3885 return Result(Result::VALIDITY_UNKNOWN
, Result::REQUIRES_FULL_CHECK
, d_filename
);
3889 void SmtEnginePrivate::collectSkolems(TNode n
, set
<TNode
>& skolemSet
, unordered_map
<Node
, bool, NodeHashFunction
>& cache
)
3891 unordered_map
<Node
, bool, NodeHashFunction
>::iterator it
;
3893 if (it
!= cache
.end()) {
3897 size_t sz
= n
.getNumChildren();
3899 IteSkolemMap::iterator it
= d_iteSkolemMap
.find(n
);
3900 if (it
!= d_iteSkolemMap
.end()) {
3901 skolemSet
.insert(n
);
3908 for (; k
< sz
; ++k
) {
3909 collectSkolems(n
[k
], skolemSet
, cache
);
3915 bool SmtEnginePrivate::checkForBadSkolems(TNode n
, TNode skolem
, unordered_map
<Node
, bool, NodeHashFunction
>& cache
)
3917 unordered_map
<Node
, bool, NodeHashFunction
>::iterator it
;
3919 if (it
!= cache
.end()) {
3920 return (*it
).second
;
3923 size_t sz
= n
.getNumChildren();
3925 IteSkolemMap::iterator it
= d_iteSkolemMap
.find(n
);
3927 if (it
!= d_iteSkolemMap
.end()) {
3928 if (!((*it
).first
< n
)) {
3937 for (; k
< sz
; ++k
) {
3938 if (checkForBadSkolems(n
[k
], skolem
, cache
)) {
3948 void SmtEnginePrivate::applySubstitutionsToAssertions() {
3949 if(!options::unsatCores()) {
3950 Chat() << "applying substitutions..." << endl
;
3951 Trace("simplify") << "SmtEnginePrivate::processAssertions(): "
3952 << "applying substitutions" << endl
;
3953 // TODO(b/1255): Substitutions in incremental mode should be managed with a
3954 // proper data structure.
3956 // When solving incrementally, all substitutions are piled into the
3957 // assertion at d_substitutionsIndex: we don't want to apply substitutions
3958 // to this assertion or information will be lost.
3959 unsigned substitutionAssertion
= d_substitutionsIndex
> 0 ? d_substitutionsIndex
: d_assertions
.size();
3960 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
3961 if (i
== substitutionAssertion
) {
3964 Trace("simplify") << "applying to " << d_assertions
[i
] << endl
;
3965 spendResource(options::preprocessStep());
3966 d_assertions
.replace(i
, Rewriter::rewrite(d_topLevelSubstitutions
.apply(d_assertions
[i
])));
3967 Trace("simplify") << " got " << d_assertions
[i
] << endl
;
3972 void SmtEnginePrivate::processAssertions() {
3973 TimerStat::CodeTimer
paTimer(d_smt
.d_stats
->d_processAssertionsTime
);
3974 spendResource(options::preprocessStep());
3975 Assert(d_smt
.d_fullyInited
);
3976 Assert(d_smt
.d_pendingPops
== 0);
3978 // Dump the assertions
3979 dumpAssertions("pre-everything", d_assertions
);
3981 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() begin" << endl
;
3982 Trace("smt") << "SmtEnginePrivate::processAssertions()" << endl
;
3984 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
3986 if (d_assertions
.size() == 0) {
3991 if (d_assertionsProcessed
&& options::incrementalSolving()) {
3992 // TODO(b/1255): Substitutions in incremental mode should be managed with a
3993 // proper data structure.
3995 // Placeholder for storing substitutions
3996 d_substitutionsIndex
= d_assertions
.size();
3997 d_assertions
.push_back(NodeManager::currentNM()->mkConst
<bool>(true));
4000 // Add dummy assertion in last position - to be used as a
4001 // placeholder for any new assertions to get added
4002 d_assertions
.push_back(NodeManager::currentNM()->mkConst
<bool>(true));
4003 // any assertions added beyond realAssertionsEnd must NOT affect the
4004 // equisatisfiability
4005 d_realAssertionsEnd
= d_assertions
.size();
4007 // Assertions are NOT guaranteed to be rewritten by this point
4009 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-definition-expansion" << endl
;
4010 dumpAssertions("pre-definition-expansion", d_assertions
);
4012 Chat() << "expanding definitions..." << endl
;
4013 Trace("simplify") << "SmtEnginePrivate::simplify(): expanding definitions" << endl
;
4014 TimerStat::CodeTimer
codeTimer(d_smt
.d_stats
->d_definitionExpansionTime
);
4015 unordered_map
<Node
, Node
, NodeHashFunction
> cache
;
4016 for(unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
4017 d_assertions
.replace(i
, expandDefinitions(d_assertions
[i
], cache
));
4020 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-definition-expansion" << endl
;
4021 dumpAssertions("post-definition-expansion", d_assertions
);
4023 // save the assertions now
4026 for (unsigned i
= 0; i
< d_assertions
.size(); ++i
) {
4027 ProofManager::currentPM()->addAssertion(d_assertions
[i
].toExpr());
4031 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
4033 if( options::nlExtPurify() ){
4034 unordered_map
<Node
, Node
, NodeHashFunction
> cache
;
4035 unordered_map
<Node
, Node
, NodeHashFunction
> bcache
;
4036 std::vector
< Node
> var_eq
;
4037 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
4038 d_assertions
.replace(i
, purifyNlTerms(d_assertions
[i
], cache
, bcache
, var_eq
));
4040 if( !var_eq
.empty() ){
4041 unsigned lastIndex
= d_assertions
.size()-1;
4042 var_eq
.insert( var_eq
.begin(), d_assertions
[lastIndex
] );
4043 d_assertions
.replace(lastIndex
, NodeManager::currentNM()->mkNode( kind::AND
, var_eq
) );
4047 if( options::ceGuidedInst() ){
4048 //register sygus conjecture pre-rewrite (motivated by solution reconstruction)
4049 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
4050 d_smt
.d_theoryEngine
->getQuantifiersEngine()->getCegInstantiation()->preregisterAssertion( d_assertions
[i
] );
4054 if (options::solveRealAsInt()) {
4055 Chat() << "converting reals to ints..." << endl
;
4056 unordered_map
<Node
, Node
, NodeHashFunction
> cache
;
4057 std::vector
< Node
> var_eq
;
4058 for(unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
4059 d_assertions
.replace(i
, realToInt(d_assertions
[i
], cache
, var_eq
));
4062 if( !var_eq.empty() ){
4063 unsigned lastIndex = d_assertions.size()-1;
4064 var_eq.insert( var_eq.begin(), d_assertions[lastIndex] );
4065 d_assertions.replace(last_index, NodeManager::currentNM()->mkNode( kind::AND, var_eq ) );
4070 if (options::solveIntAsBV() > 0) {
4071 Chat() << "converting ints to bit-vectors..." << endl
;
4072 unordered_map
<Node
, Node
, NodeHashFunction
> cache
;
4073 for(unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
4074 d_assertions
.replace(i
, intToBV(d_assertions
[i
], cache
));
4078 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
&&
4079 !d_smt
.d_logic
.isPure(THEORY_BV
) &&
4080 d_smt
.d_logic
.getLogicString() != "QF_UFBV" &&
4081 d_smt
.d_logic
.getLogicString() != "QF_ABV") {
4082 throw ModalException("Eager bit-blasting does not currently support theory combination. "
4083 "Note that in a QF_BV problem UF symbols can be introduced for division. "
4084 "Try --bv-div-zero-const to interpret division by zero as a constant.");
4087 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
) {
4088 d_smt
.d_theoryEngine
->mkAckermanizationAssertions(d_assertions
.ref());
4091 if ( options::bvAbstraction() &&
4092 !options::incrementalSolving()) {
4093 dumpAssertions("pre-bv-abstraction", d_assertions
);
4095 dumpAssertions("post-bv-abstraction", d_assertions
);
4098 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
4100 bool noConflict
= true;
4102 // Unconstrained simplification
4103 if(options::unconstrainedSimp()) {
4104 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-unconstrained-simp" << endl
;
4105 dumpAssertions("pre-unconstrained-simp", d_assertions
);
4106 Chat() << "...doing unconstrained simplification..." << endl
;
4107 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
4108 d_assertions
.replace(i
, Rewriter::rewrite(d_assertions
[i
]));
4110 unconstrainedSimp();
4111 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-unconstrained-simp" << endl
;
4112 dumpAssertions("post-unconstrained-simp", d_assertions
);
4115 if(options::bvIntroducePow2()){
4116 theory::bv::BVIntroducePow2::pow2Rewrite(d_assertions
.ref());
4119 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-substitution" << endl
;
4120 dumpAssertions("pre-substitution", d_assertions
);
4122 if(options::unsatCores()) {
4123 // special rewriting pass for unsat cores, since many of the passes below are skipped
4124 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
4125 d_assertions
.replace(i
, Rewriter::rewrite(d_assertions
[i
]));
4128 applySubstitutionsToAssertions();
4130 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-substitution" << endl
;
4131 dumpAssertions("post-substitution", d_assertions
);
4133 // Assertions ARE guaranteed to be rewritten by this point
4135 // Lift bit-vectors of size 1 to bool
4136 if(options::bitvectorToBool()) {
4137 dumpAssertions("pre-bv-to-bool", d_assertions
);
4138 Chat() << "...doing bvToBool..." << endl
;
4140 dumpAssertions("post-bv-to-bool", d_assertions
);
4141 Trace("smt") << "POST bvToBool" << endl
;
4143 // Convert non-top-level Booleans to bit-vectors of size 1
4144 if(options::boolToBitvector()) {
4145 dumpAssertions("pre-bool-to-bv", d_assertions
);
4146 Chat() << "...doing boolToBv..." << endl
;
4148 dumpAssertions("post-bool-to-bv", d_assertions
);
4149 Trace("smt") << "POST boolToBv" << endl
;
4151 if(options::sepPreSkolemEmp()) {
4152 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
4153 Node prev
= d_assertions
[i
];
4154 Node next
= sep::TheorySepRewriter::preprocess( prev
);
4156 d_assertions
.replace( i
, Rewriter::rewrite( next
) );
4157 Trace("sep-preprocess") << "*** Preprocess sep " << prev
<< endl
;
4158 Trace("sep-preprocess") << " ...got " << d_assertions
[i
] << endl
;
4163 if( d_smt
.d_logic
.isQuantified() ){
4164 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-quant-preprocess" << endl
;
4166 dumpAssertions("pre-skolem-quant", d_assertions
);
4167 //remove rewrite rules, apply pre-skolemization to existential quantifiers
4168 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
4169 Node prev
= d_assertions
[i
];
4170 Node next
= quantifiers::QuantifiersRewriter::preprocess( prev
);
4172 d_assertions
.replace( i
, Rewriter::rewrite( next
) );
4173 Trace("quantifiers-preprocess") << "*** Pre-skolemize " << prev
<< endl
;
4174 Trace("quantifiers-preprocess") << " ...got " << d_assertions
[i
] << endl
;
4177 dumpAssertions("post-skolem-quant", d_assertions
);
4178 if( options::macrosQuant() ){
4179 //quantifiers macro expansion
4180 quantifiers::QuantifierMacros
qm( d_smt
.d_theoryEngine
->getQuantifiersEngine() );
4183 success
= qm
.simplify( d_assertions
.ref(), true );
4185 //finalize the definitions
4186 qm
.finalizeDefinitions();
4189 //fmf-fun : assume admissible functions, applying preprocessing reduction to FMF
4190 if( options::fmfFunWellDefined() ){
4191 quantifiers::FunDefFmf fdf
;
4192 Assert( d_smt
.d_fmfRecFunctionsDefined
!=NULL
);
4193 //must carry over current definitions (for incremental)
4194 for( context::CDList
<Node
>::const_iterator fit
= d_smt
.d_fmfRecFunctionsDefined
->begin();
4195 fit
!= d_smt
.d_fmfRecFunctionsDefined
->end(); ++fit
) {
4197 Assert( d_smt
.d_fmfRecFunctionsAbs
.find( f
)!=d_smt
.d_fmfRecFunctionsAbs
.end() );
4198 TypeNode ft
= d_smt
.d_fmfRecFunctionsAbs
[f
];
4199 fdf
.d_sorts
[f
] = ft
;
4200 std::map
< Node
, std::vector
< Node
> >::iterator fcit
= d_smt
.d_fmfRecFunctionsConcrete
.find( f
);
4201 Assert( fcit
!=d_smt
.d_fmfRecFunctionsConcrete
.end() );
4202 for( unsigned j
=0; j
<fcit
->second
.size(); j
++ ){
4203 fdf
.d_input_arg_inj
[f
].push_back( fcit
->second
[j
] );
4206 fdf
.simplify( d_assertions
.ref() );
4207 //must store new definitions (for incremental)
4208 for( unsigned i
=0; i
<fdf
.d_funcs
.size(); i
++ ){
4209 Node f
= fdf
.d_funcs
[i
];
4210 d_smt
.d_fmfRecFunctionsAbs
[f
] = fdf
.d_sorts
[f
];
4211 d_smt
.d_fmfRecFunctionsConcrete
[f
].clear();
4212 for( unsigned j
=0; j
<fdf
.d_input_arg_inj
[f
].size(); j
++ ){
4213 d_smt
.d_fmfRecFunctionsConcrete
[f
].push_back( fdf
.d_input_arg_inj
[f
][j
] );
4215 d_smt
.d_fmfRecFunctionsDefined
->push_back( f
);
4218 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-quant-preprocess" << endl
;
4221 if( options::sortInference() || options::ufssFairnessMonotone() ){
4222 //sort inference technique
4223 SortInference
* si
= d_smt
.d_theoryEngine
->getSortInference();
4224 si
->simplify( d_assertions
.ref(), options::sortInference(), options::ufssFairnessMonotone() );
4225 for( std::map
< Node
, Node
>::iterator it
= si
->d_model_replace_f
.begin(); it
!= si
->d_model_replace_f
.end(); ++it
){
4226 d_smt
.setPrintFuncInModel( it
->first
.toExpr(), false );
4227 d_smt
.setPrintFuncInModel( it
->second
.toExpr(), true );
4231 if( options::pbRewrites() ){
4232 d_pbsProcessor
.learn(d_assertions
.ref());
4233 if(d_pbsProcessor
.likelyToHelp()){
4234 d_pbsProcessor
.applyReplacements(d_assertions
.ref());
4238 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-simplify" << endl
;
4239 dumpAssertions("pre-simplify", d_assertions
);
4240 Chat() << "simplifying assertions..." << endl
;
4241 noConflict
= simplifyAssertions();
4243 ++(d_smt
.d_stats
->d_simplifiedToFalse
);
4245 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-simplify" << endl
;
4246 dumpAssertions("post-simplify", d_assertions
);
4248 dumpAssertions("pre-static-learning", d_assertions
);
4249 if(options::doStaticLearning()) {
4250 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-static-learning" << endl
;
4251 // Perform static learning
4252 Chat() << "doing static learning..." << endl
;
4253 Trace("simplify") << "SmtEnginePrivate::simplify(): "
4254 << "performing static learning" << endl
;
4256 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-static-learning" << endl
;
4258 dumpAssertions("post-static-learning", d_assertions
);
4260 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
4263 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-ite-removal" << endl
;
4264 dumpAssertions("pre-ite-removal", d_assertions
);
4266 Chat() << "removing term ITEs..." << endl
;
4267 TimerStat::CodeTimer
codeTimer(d_smt
.d_stats
->d_iteRemovalTime
);
4268 // Remove ITEs, updating d_iteSkolemMap
4269 d_smt
.d_stats
->d_numAssertionsPre
+= d_assertions
.size();
4271 // This is needed because when solving incrementally, removeITEs may introduce
4272 // skolems that were solved for earlier and thus appear in the substitution
4274 applySubstitutionsToAssertions();
4275 d_smt
.d_stats
->d_numAssertionsPost
+= d_assertions
.size();
4277 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-ite-removal" << endl
;
4278 dumpAssertions("post-ite-removal", d_assertions
);
4280 dumpAssertions("pre-repeat-simplify", d_assertions
);
4281 if(options::repeatSimp()) {
4282 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-repeat-simplify" << endl
;
4283 Chat() << "re-simplifying assertions..." << endl
;
4284 ScopeCounter
depth(d_simplifyAssertionsDepth
);
4285 noConflict
&= simplifyAssertions();
4287 // Need to fix up assertion list to maintain invariants:
4288 // Let Sk be the set of Skolem variables introduced by ITE's. Let <_sk be the order in which these variables were introduced
4289 // during ite removal.
4290 // For each skolem variable sk, let iteExpr = iteMap(sk) be the ite expr mapped to by sk.
4292 // cache for expression traversal
4293 unordered_map
<Node
, bool, NodeHashFunction
> cache
;
4295 // First, find all skolems that appear in the substitution map - their associated iteExpr will need
4296 // to be moved to the main assertion set
4297 set
<TNode
> skolemSet
;
4298 SubstitutionMap::iterator pos
= d_topLevelSubstitutions
.begin();
4299 for (; pos
!= d_topLevelSubstitutions
.end(); ++pos
) {
4300 collectSkolems((*pos
).first
, skolemSet
, cache
);
4301 collectSkolems((*pos
).second
, skolemSet
, cache
);
4304 // We need to ensure:
4305 // 1. iteExpr has the form (ite cond (sk = t) (sk = e))
4306 // 2. if some sk' in Sk appears in cond, t, or e, then sk' <_sk sk
4307 // If either of these is violated, we must add iteExpr as a proper assertion
4308 IteSkolemMap::iterator it
= d_iteSkolemMap
.begin();
4309 IteSkolemMap::iterator iend
= d_iteSkolemMap
.end();
4310 NodeBuilder
<> builder(kind::AND
);
4311 builder
<< d_assertions
[d_realAssertionsEnd
- 1];
4312 vector
<TNode
> toErase
;
4313 for (; it
!= iend
; ++it
) {
4314 if (skolemSet
.find((*it
).first
) == skolemSet
.end()) {
4315 TNode iteExpr
= d_assertions
[(*it
).second
];
4316 if (iteExpr
.getKind() == kind::ITE
&&
4317 iteExpr
[1].getKind() == kind::EQUAL
&&
4318 iteExpr
[1][0] == (*it
).first
&&
4319 iteExpr
[2].getKind() == kind::EQUAL
&&
4320 iteExpr
[2][0] == (*it
).first
) {
4322 bool bad
= checkForBadSkolems(iteExpr
[0], (*it
).first
, cache
);
4323 bad
= bad
|| checkForBadSkolems(iteExpr
[1][1], (*it
).first
, cache
);
4324 bad
= bad
|| checkForBadSkolems(iteExpr
[2][1], (*it
).first
, cache
);
4330 // Move this iteExpr into the main assertions
4331 builder
<< d_assertions
[(*it
).second
];
4332 d_assertions
[(*it
).second
] = NodeManager::currentNM()->mkConst
<bool>(true);
4333 toErase
.push_back((*it
).first
);
4335 if(builder
.getNumChildren() > 1) {
4336 while (!toErase
.empty()) {
4337 d_iteSkolemMap
.erase(toErase
.back());
4340 d_assertions
[d_realAssertionsEnd
- 1] = Rewriter::rewrite(Node(builder
));
4342 // TODO(b/1256): For some reason this is needed for some benchmarks, such as
4343 // http://cvc4.cs.nyu.edu/benchmarks/smtlib2/QF_AUFBV/dwp_formulas/try5_small_difret_functions_dwp_tac.re_node_set_remove_at.il.dwp.smt2
4345 applySubstitutionsToAssertions();
4346 // Assert(iteRewriteAssertionsEnd == d_assertions.size());
4348 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-repeat-simplify" << endl
;
4350 dumpAssertions("post-repeat-simplify", d_assertions
);
4352 dumpAssertions("pre-rewrite-apply-to-const", d_assertions
);
4353 if(options::rewriteApplyToConst()) {
4354 Chat() << "Rewriting applies to constants..." << endl
;
4355 TimerStat::CodeTimer
codeTimer(d_smt
.d_stats
->d_rewriteApplyToConstTime
);
4356 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
4357 d_assertions
[i
] = Rewriter::rewrite(rewriteApplyToConst(d_assertions
[i
]));
4360 dumpAssertions("post-rewrite-apply-to-const", d_assertions
);
4362 // begin: INVARIANT to maintain: no reordering of assertions or
4363 // introducing new ones
4364 #ifdef CVC4_ASSERTIONS
4365 unsigned iteRewriteAssertionsEnd
= d_assertions
.size();
4368 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
4370 Debug("smt") << "SmtEnginePrivate::processAssertions() POST SIMPLIFICATION" << endl
;
4371 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
4373 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-theory-preprocessing" << endl
;
4374 dumpAssertions("pre-theory-preprocessing", d_assertions
);
4376 Chat() << "theory preprocessing..." << endl
;
4377 TimerStat::CodeTimer
codeTimer(d_smt
.d_stats
->d_theoryPreprocessTime
);
4378 // Call the theory preprocessors
4379 d_smt
.d_theoryEngine
->preprocessStart();
4380 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
4381 d_assertions
.replace(i
, d_smt
.d_theoryEngine
->preprocess(d_assertions
[i
]));
4384 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-theory-preprocessing" << endl
;
4385 dumpAssertions("post-theory-preprocessing", d_assertions
);
4387 // If we are using eager bit-blasting wrap assertions in fake atom so that
4388 // everything gets bit-blasted to internal SAT solver
4389 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
) {
4390 for (unsigned i
= 0; i
< d_assertions
.size(); ++i
) {
4391 TNode atom
= d_assertions
[i
];
4392 Node eager_atom
= NodeManager::currentNM()->mkNode(kind::BITVECTOR_EAGER_ATOM
, atom
);
4393 d_assertions
.replace(i
, eager_atom
);
4394 TheoryModel
* m
= d_smt
.d_theoryEngine
->getModel();
4395 m
->addSubstitution(eager_atom
, atom
);
4399 //notify theory engine new preprocessed assertions
4400 d_smt
.d_theoryEngine
->notifyPreprocessedAssertions( d_assertions
.ref() );
4402 // Push the formula to decision engine
4404 Chat() << "pushing to decision engine..." << endl
;
4405 Assert(iteRewriteAssertionsEnd
== d_assertions
.size());
4406 d_smt
.d_decisionEngine
->addAssertions
4407 (d_assertions
.ref(), d_realAssertionsEnd
, d_iteSkolemMap
);
4410 // end: INVARIANT to maintain: no reordering of assertions or
4411 // introducing new ones
4413 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() end" << endl
;
4414 dumpAssertions("post-everything", d_assertions
);
4416 // Push the formula to SAT
4418 Chat() << "converting to CNF..." << endl
;
4419 TimerStat::CodeTimer
codeTimer(d_smt
.d_stats
->d_cnfConversionTime
);
4420 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
4421 Chat() << "+ " << d_assertions
[i
] << std::endl
;
4422 d_smt
.d_propEngine
->assertFormula(d_assertions
[i
]);
4426 d_assertionsProcessed
= true;
4428 d_assertions
.clear();
4429 d_iteSkolemMap
.clear();
4432 void SmtEnginePrivate::addFormula(TNode n
, bool inUnsatCore
, bool inInput
)
4433 throw(TypeCheckingException
, LogicException
) {
4440 Trace("smt") << "SmtEnginePrivate::addFormula(" << n
<< "), inUnsatCore = " << inUnsatCore
<< ", inInput = " << inInput
<< endl
;
4442 // Give it to proof manager
4445 // n is an input assertion
4446 if (inUnsatCore
|| options::unsatCores() || options::dumpUnsatCores() || options::checkUnsatCores() || options::fewerPreprocessingHoles()) {
4448 ProofManager::currentPM()->addCoreAssertion(n
.toExpr());
4451 // n is the result of an unknown preprocessing step, add it to dependency map to null
4452 ProofManager::currentPM()->addDependence(n
, Node::null());
4454 // rewrite rules are by default in the unsat core because
4455 // they need to be applied until saturation
4456 if(options::unsatCores() &&
4457 n
.getKind() == kind::REWRITE_RULE
){
4458 ProofManager::currentPM()->addUnsatCore(n
.toExpr());
4462 // Add the normalized formula to the queue
4463 d_assertions
.push_back(n
);
4464 //d_assertions.push_back(Rewriter::rewrite(n));
4467 void SmtEngine::ensureBoolean(const Expr
& e
) throw(TypeCheckingException
) {
4468 Type type
= e
.getType(options::typeChecking());
4469 Type boolType
= d_exprManager
->booleanType();
4470 if(type
!= boolType
) {
4472 ss
<< "Expected " << boolType
<< "\n"
4473 << "The assertion : " << e
<< "\n"
4474 << "Its type : " << type
;
4475 throw TypeCheckingException(e
, ss
.str());
4479 Result
SmtEngine::checkSat(const Expr
& ex
, bool inUnsatCore
) throw(Exception
) {
4480 return checkSatisfiability(ex
, inUnsatCore
, false);
4481 } /* SmtEngine::checkSat() */
4483 Result
SmtEngine::query(const Expr
& ex
, bool inUnsatCore
) throw(Exception
) {
4484 Assert(!ex
.isNull());
4485 return checkSatisfiability(ex
, inUnsatCore
, true);
4486 } /* SmtEngine::query() */
4488 Result
SmtEngine::checkSatisfiability(const Expr
& ex
, bool inUnsatCore
, bool isQuery
) {
4490 Assert(ex
.isNull() || ex
.getExprManager() == d_exprManager
);
4491 SmtScope
smts(this);
4492 finalOptionsAreSet();
4495 Trace("smt") << "SmtEngine::" << (isQuery
? "query" : "checkSat") << "(" << ex
<< ")" << endl
;
4497 if(d_queryMade
&& !options::incrementalSolving()) {
4498 throw ModalException("Cannot make multiple queries unless "
4499 "incremental solving is enabled "
4500 "(try --incremental)");
4505 // Substitute out any abstract values in ex.
4506 e
= d_private
->substituteAbstractValues(Node::fromExpr(ex
)).toExpr();
4507 // Ensure expr is type-checked at this point.
4511 // check to see if a postsolve() is pending
4512 if(d_needPostsolve
) {
4513 d_theoryEngine
->postsolve();
4514 d_needPostsolve
= false;
4520 // Note that a query has been made
4525 d_problemExtended
= true;
4526 Expr ea
= isQuery
? e
.notExpr() : e
;
4527 if(d_assertionList
!= NULL
) {
4528 d_assertionList
->push_back(ea
);
4530 d_private
->addFormula(ea
.getNode(), inUnsatCore
);
4533 Result
r(Result::SAT_UNKNOWN
, Result::UNKNOWN_REASON
);
4534 r
= isQuery
? check().asValidityResult() : check().asSatisfiabilityResult();
4536 if ( ( options::solveRealAsInt() || options::solveIntAsBV() > 0 ) && r
.asSatisfiabilityResult().isSat() == Result::UNSAT
) {
4537 r
= Result(Result::SAT_UNKNOWN
, Result::UNKNOWN_REASON
);
4540 d_needPostsolve
= true;
4542 // Dump the query if requested
4543 if(Dump
.isOn("benchmark")) {
4544 // the expr already got dumped out if assertion-dumping is on
4546 Dump("benchmark") << QueryCommand(ex
);
4548 Dump("benchmark") << CheckSatCommand(ex
);
4555 // Remember the status
4558 d_problemExtended
= false;
4560 Trace("smt") << "SmtEngine::" << (isQuery
? "query" : "checkSat") << "(" << e
<< ") => " << r
<< endl
;
4562 // Check that SAT results generate a model correctly.
4563 if(options::checkModels()) {
4564 if(r
.asSatisfiabilityResult().isSat() == Result::SAT
||
4565 (r
.isUnknown() && r
.whyUnknown() == Result::INCOMPLETE
) ){
4566 checkModel(/* hard failure iff */ ! r
.isUnknown());
4569 // Check that UNSAT results generate a proof correctly.
4570 if(options::checkProofs()) {
4571 if(r
.asSatisfiabilityResult().isSat() == Result::UNSAT
) {
4572 TimerStat::CodeTimer
checkProofTimer(d_stats
->d_checkProofTime
);
4576 // Check that UNSAT results generate an unsat core correctly.
4577 if(options::checkUnsatCores()) {
4578 if(r
.asSatisfiabilityResult().isSat() == Result::UNSAT
) {
4579 TimerStat::CodeTimer
checkUnsatCoreTimer(d_stats
->d_checkUnsatCoreTime
);
4585 } catch (UnsafeInterruptException
& e
) {
4586 AlwaysAssert(d_private
->getResourceManager()->out());
4587 Result::UnknownExplanation why
= d_private
->getResourceManager()->outOfResources() ?
4588 Result::RESOURCEOUT
: Result::TIMEOUT
;
4589 return Result(Result::SAT_UNKNOWN
, why
, d_filename
);
4593 Result
SmtEngine::checkSynth(const Expr
& e
) throw(Exception
) {
4594 SmtScope
smts(this);
4595 Trace("smt") << "Check synth: " << e
<< std::endl
;
4596 Trace("smt-synth") << "Check synthesis conjecture: " << e
<< std::endl
;
4598 if (options::sygusQePreproc())
4600 // the following does quantifier elimination as a preprocess step
4601 // for "non-ground single invocation synthesis conjectures":
4602 // exists f. forall xy. P[ f(x), x, y ]
4603 // We run quantifier elimination:
4604 // exists y. P[ z, x, y ] ----> Q[ z, x ]
4605 // Where we replace the original conjecture with:
4606 // exists f. forall x. Q[ f(x), x ]
4607 // For more details, see Example 6 of Reynolds et al. SYNT 2017.
4608 Node conj
= Node::fromExpr(e
);
4609 if (conj
.getKind() == kind::FORALL
&& conj
[1].getKind() == kind::EXISTS
)
4611 Node conj_se
= Node::fromExpr(expandDefinitions(conj
[1][1].toExpr()));
4613 Trace("smt-synth") << "Compute single invocation for " << conj_se
<< "..."
4615 quantifiers::SingleInvocationPartition sip
;
4616 std::vector
<Node
> funcs
;
4617 funcs
.insert(funcs
.end(), conj
[0].begin(), conj
[0].end());
4618 sip
.init(funcs
, conj_se
.negate());
4619 Trace("smt-synth") << "...finished, got:" << std::endl
;
4620 sip
.debugPrint("smt-synth");
4622 if (!sip
.isPurelySingleInvocation() && sip
.isNonGroundSingleInvocation())
4624 // create new smt engine to do quantifier elimination
4625 SmtEngine
smt_qe(d_exprManager
);
4626 smt_qe
.setLogic(getLogicInfo());
4627 Trace("smt-synth") << "Property is non-ground single invocation, run "
4628 "QE to obtain single invocation."
4630 // partition variables
4631 std::vector
<Node
> qe_vars
;
4632 std::vector
<Node
> nqe_vars
;
4633 for (unsigned i
= 0; i
< sip
.d_all_vars
.size(); i
++)
4635 Node v
= sip
.d_all_vars
[i
];
4636 if (std::find(sip
.d_si_vars
.begin(), sip
.d_si_vars
.end(), v
)
4637 == sip
.d_si_vars
.end())
4639 qe_vars
.push_back(v
);
4643 nqe_vars
.push_back(v
);
4646 std::vector
<Node
> orig
;
4647 std::vector
<Node
> subs
;
4648 // skolemize non-qe variables
4649 for (unsigned i
= 0; i
< nqe_vars
.size(); i
++)
4651 Node k
= NodeManager::currentNM()->mkSkolem(
4653 nqe_vars
[i
].getType(),
4654 "qe for non-ground single invocation");
4655 orig
.push_back(nqe_vars
[i
]);
4657 Trace("smt-synth") << " subs : " << nqe_vars
[i
] << " -> " << k
4660 for (std::map
<Node
, bool>::iterator it
= sip
.d_funcs
.begin();
4661 it
!= sip
.d_funcs
.end();
4664 orig
.push_back(sip
.d_func_inv
[it
->first
]);
4665 Node k
= NodeManager::currentNM()->mkSkolem(
4667 sip
.d_func_fo_var
[it
->first
].getType(),
4668 "qe for function in non-ground single invocation");
4670 Trace("smt-synth") << " subs : " << sip
.d_func_inv
[it
->first
]
4671 << " -> " << k
<< std::endl
;
4673 Node conj_se_ngsi
= sip
.getFullSpecification();
4674 Trace("smt-synth") << "Full specification is " << conj_se_ngsi
4676 Node conj_se_ngsi_subs
= conj_se_ngsi
.substitute(
4677 orig
.begin(), orig
.end(), subs
.begin(), subs
.end());
4678 Assert(!qe_vars
.empty());
4679 conj_se_ngsi_subs
= NodeManager::currentNM()->mkNode(
4681 NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST
, qe_vars
),
4682 conj_se_ngsi_subs
.negate());
4684 Trace("smt-synth") << "Run quantifier elimination on "
4685 << conj_se_ngsi_subs
<< std::endl
;
4686 Expr qe_res
= smt_qe
.doQuantifierElimination(
4687 conj_se_ngsi_subs
.toExpr(), true, false);
4688 Trace("smt-synth") << "Result : " << qe_res
<< std::endl
;
4690 // create single invocation conjecture
4691 Node qe_res_n
= Node::fromExpr(qe_res
);
4692 qe_res_n
= qe_res_n
.substitute(
4693 subs
.begin(), subs
.end(), orig
.begin(), orig
.end());
4694 if (!nqe_vars
.empty())
4696 qe_res_n
= NodeManager::currentNM()->mkNode(
4698 NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST
, nqe_vars
),
4701 Assert(conj
.getNumChildren() == 3);
4702 qe_res_n
= NodeManager::currentNM()->mkNode(
4703 kind::FORALL
, conj
[0], qe_res_n
, conj
[2]);
4704 Trace("smt-synth") << "Converted conjecture after QE : " << qe_res_n
4706 e_check
= qe_res_n
.toExpr();
4711 return checkSatisfiability( e_check
, true, false );
4714 Result
SmtEngine::assertFormula(const Expr
& ex
, bool inUnsatCore
) throw(TypeCheckingException
, LogicException
, UnsafeInterruptException
) {
4715 Assert(ex
.getExprManager() == d_exprManager
);
4716 SmtScope
smts(this);
4717 finalOptionsAreSet();
4720 Trace("smt") << "SmtEngine::assertFormula(" << ex
<< ")" << endl
;
4722 if (Dump
.isOn("raw-benchmark")) {
4723 Dump("raw-benchmark") << AssertCommand(ex
);
4726 // Substitute out any abstract values in ex
4727 Expr e
= d_private
->substituteAbstractValues(Node::fromExpr(ex
)).toExpr();
4730 if(d_assertionList
!= NULL
) {
4731 d_assertionList
->push_back(e
);
4733 d_private
->addFormula(e
.getNode(), inUnsatCore
);
4734 return quickCheck().asValidityResult();
4735 }/* SmtEngine::assertFormula() */
4737 Node
SmtEngine::postprocess(TNode node
, TypeNode expectedType
) const {
4741 Expr
SmtEngine::simplify(const Expr
& ex
) throw(TypeCheckingException
, LogicException
, UnsafeInterruptException
) {
4742 Assert(ex
.getExprManager() == d_exprManager
);
4743 SmtScope
smts(this);
4744 finalOptionsAreSet();
4746 Trace("smt") << "SMT simplify(" << ex
<< ")" << endl
;
4748 if(Dump
.isOn("benchmark")) {
4749 Dump("benchmark") << SimplifyCommand(ex
);
4752 Expr e
= d_private
->substituteAbstractValues(Node::fromExpr(ex
)).toExpr();
4753 if( options::typeChecking() ) {
4754 e
.getType(true); // ensure expr is type-checked at this point
4757 // Make sure all preprocessing is done
4758 d_private
->processAssertions();
4759 Node n
= d_private
->simplify(Node::fromExpr(e
));
4760 n
= postprocess(n
, TypeNode::fromType(e
.getType()));
4764 Expr
SmtEngine::expandDefinitions(const Expr
& ex
) throw(TypeCheckingException
, LogicException
, UnsafeInterruptException
) {
4765 d_private
->spendResource(options::preprocessStep());
4767 Assert(ex
.getExprManager() == d_exprManager
);
4768 SmtScope
smts(this);
4769 finalOptionsAreSet();
4771 Trace("smt") << "SMT expandDefinitions(" << ex
<< ")" << endl
;
4773 // Substitute out any abstract values in ex.
4774 Expr e
= d_private
->substituteAbstractValues(Node::fromExpr(ex
)).toExpr();
4775 if(options::typeChecking()) {
4776 // Ensure expr is type-checked at this point.
4779 if(Dump
.isOn("benchmark")) {
4780 Dump("benchmark") << ExpandDefinitionsCommand(e
);
4782 unordered_map
<Node
, Node
, NodeHashFunction
> cache
;
4783 Node n
= d_private
->expandDefinitions(Node::fromExpr(e
), cache
, /* expandOnly = */ true);
4784 n
= postprocess(n
, TypeNode::fromType(e
.getType()));
4789 // TODO(#1108): Simplify the error reporting of this method.
4790 Expr
SmtEngine::getValue(const Expr
& ex
) const throw(ModalException
, TypeCheckingException
, LogicException
, UnsafeInterruptException
) {
4791 Assert(ex
.getExprManager() == d_exprManager
);
4792 SmtScope
smts(this);
4794 Trace("smt") << "SMT getValue(" << ex
<< ")" << endl
;
4795 if(Dump
.isOn("benchmark")) {
4796 Dump("benchmark") << GetValueCommand(ex
);
4799 if(!options::produceModels()) {
4801 "Cannot get value when produce-models options is off.";
4802 throw ModalException(msg
);
4804 if(d_status
.isNull() ||
4805 d_status
.asSatisfiabilityResult() == Result::UNSAT
||
4806 d_problemExtended
) {
4808 "Cannot get value unless immediately preceded by SAT/INVALID or UNKNOWN response.";
4809 throw RecoverableModalException(msg
);
4812 // Substitute out any abstract values in ex.
4813 Expr e
= d_private
->substituteAbstractValues(Node::fromExpr(ex
)).toExpr();
4815 // Ensure expr is type-checked at this point.
4816 e
.getType(options::typeChecking());
4818 // do not need to apply preprocessing substitutions (should be recorded
4819 // in model already)
4821 Node n
= Node::fromExpr(e
);
4822 Trace("smt") << "--- getting value of " << n
<< endl
;
4823 TypeNode expectedType
= n
.getType();
4825 // Expand, then normalize
4826 unordered_map
<Node
, Node
, NodeHashFunction
> cache
;
4827 n
= d_private
->expandDefinitions(n
, cache
);
4828 // There are two ways model values for terms are computed (for historical
4829 // reasons). One way is that used in check-model; the other is that
4830 // used by the Model classes. It's not clear to me exactly how these
4831 // two are different, but they need to be unified. This ugly hack here
4832 // is to fix bug 554 until we can revamp boolean-terms and models [MGD]
4835 if(!n
.getType().isFunction()) {
4836 n
= Rewriter::rewrite(n
);
4839 Trace("smt") << "--- getting value of " << n
<< endl
;
4840 TheoryModel
* m
= d_theoryEngine
->getModel();
4843 resultNode
= m
->getValue(n
);
4845 Trace("smt") << "--- got value " << n
<< " = " << resultNode
<< endl
;
4846 resultNode
= postprocess(resultNode
, expectedType
);
4847 Trace("smt") << "--- model-post returned " << resultNode
<< endl
;
4848 Trace("smt") << "--- model-post returned " << resultNode
.getType() << endl
;
4849 Trace("smt") << "--- model-post expected " << expectedType
<< endl
;
4851 // type-check the result we got
4852 Assert(resultNode
.isNull() || resultNode
.getType().isSubtypeOf(expectedType
),
4853 "Run with -t smt for details.");
4855 // ensure it's a constant
4856 Assert(resultNode
.getKind() == kind::LAMBDA
|| resultNode
.isConst());
4858 if(options::abstractValues() && resultNode
.getType().isArray()) {
4859 resultNode
= d_private
->mkAbstractValue(resultNode
);
4860 Trace("smt") << "--- abstract value >> " << resultNode
<< endl
;
4863 return resultNode
.toExpr();
4866 bool SmtEngine::addToAssignment(const Expr
& ex
) {
4867 SmtScope
smts(this);
4868 finalOptionsAreSet();
4870 // Substitute out any abstract values in ex
4871 Expr e
= d_private
->substituteAbstractValues(Node::fromExpr(ex
)).toExpr();
4872 Type type
= e
.getType(options::typeChecking());
4874 PrettyCheckArgument(
4875 type
.isBoolean(), e
,
4876 "expected Boolean-typed variable or function application "
4877 "in addToAssignment()" );
4878 Node n
= e
.getNode();
4879 // must be an APPLY of a zero-ary defined function, or a variable
4880 PrettyCheckArgument(
4881 ( ( n
.getKind() == kind::APPLY
&&
4882 ( d_definedFunctions
->find(n
.getOperator()) !=
4883 d_definedFunctions
->end() ) &&
4884 n
.getNumChildren() == 0 ) ||
4886 "expected variable or defined-function application "
4887 "in addToAssignment(),\ngot %s", e
.toString().c_str() );
4888 if(!options::produceAssignments()) {
4891 if(d_assignments
== NULL
) {
4892 d_assignments
= new(true) AssignmentSet(d_context
);
4894 d_assignments
->insert(n
);
4899 // TODO(#1108): Simplify the error reporting of this method.
4900 CVC4::SExpr
SmtEngine::getAssignment() {
4901 Trace("smt") << "SMT getAssignment()" << endl
;
4902 SmtScope
smts(this);
4903 finalOptionsAreSet();
4904 if(Dump
.isOn("benchmark")) {
4905 Dump("benchmark") << GetAssignmentCommand();
4907 if(!options::produceAssignments()) {
4909 "Cannot get the current assignment when "
4910 "produce-assignments option is off.";
4911 throw ModalException(msg
);
4913 if(d_status
.isNull() ||
4914 d_status
.asSatisfiabilityResult() == Result::UNSAT
||
4915 d_problemExtended
) {
4917 "Cannot get the current assignment unless immediately "
4918 "preceded by SAT/INVALID or UNKNOWN response.";
4919 throw RecoverableModalException(msg
);
4922 if(d_assignments
== NULL
) {
4923 return SExpr(vector
<SExpr
>());
4926 vector
<SExpr
> sexprs
;
4927 TypeNode boolType
= d_nodeManager
->booleanType();
4928 TheoryModel
* m
= d_theoryEngine
->getModel();
4929 for(AssignmentSet::key_iterator i
= d_assignments
->key_begin(),
4930 iend
= d_assignments
->key_end();
4933 Assert((*i
).getType() == boolType
);
4935 Trace("smt") << "--- getting value of " << *i
<< endl
;
4937 // Expand, then normalize
4938 unordered_map
<Node
, Node
, NodeHashFunction
> cache
;
4939 Node n
= d_private
->expandDefinitions(*i
, cache
);
4940 n
= Rewriter::rewrite(n
);
4942 Trace("smt") << "--- getting value of " << n
<< endl
;
4945 resultNode
= m
->getValue(n
);
4948 // type-check the result we got
4949 Assert(resultNode
.isNull() || resultNode
.getType() == boolType
);
4951 // ensure it's a constant
4952 Assert(resultNode
.isConst());
4955 if((*i
).getKind() == kind::APPLY
) {
4956 Assert((*i
).getNumChildren() == 0);
4957 v
.push_back(SExpr(SExpr::Keyword((*i
).getOperator().toString())));
4959 Assert((*i
).isVar());
4960 v
.push_back(SExpr(SExpr::Keyword((*i
).toString())));
4962 v
.push_back(SExpr(SExpr::Keyword(resultNode
.toString())));
4963 sexprs
.push_back(SExpr(v
));
4965 return SExpr(sexprs
);
4968 void SmtEngine::addToModelCommandAndDump(const Command
& c
, uint32_t flags
, bool userVisible
, const char* dumpTag
) {
4969 Trace("smt") << "SMT addToModelCommandAndDump(" << c
<< ")" << endl
;
4970 SmtScope
smts(this);
4971 // If we aren't yet fully inited, the user might still turn on
4972 // produce-models. So let's keep any commands around just in
4973 // case. This is useful in two cases: (1) SMT-LIBv1 auto-declares
4974 // sort "U" in QF_UF before setLogic() is run and we still want to
4975 // support finding card(U) with --finite-model-find, and (2) to
4976 // decouple SmtEngine and ExprManager if the user does a few
4977 // ExprManager::mkSort() before SmtEngine::setOption("produce-models")
4978 // and expects to find their cardinalities in the model.
4979 if(/* userVisible && */
4980 (!d_fullyInited
|| options::produceModels()) &&
4981 (flags
& ExprManager::VAR_FLAG_DEFINED
) == 0) {
4983 if(flags
& ExprManager::VAR_FLAG_GLOBAL
) {
4984 d_modelGlobalCommands
.push_back(c
.clone());
4986 d_modelCommands
->push_back(c
.clone());
4989 if(Dump
.isOn(dumpTag
)) {
4993 d_dumpCommands
.push_back(c
.clone());
4998 // TODO(#1108): Simplify the error reporting of this method.
4999 Model
* SmtEngine::getModel() {
5000 Trace("smt") << "SMT getModel()" << endl
;
5001 SmtScope
smts(this);
5003 finalOptionsAreSet();
5005 if(Dump
.isOn("benchmark")) {
5006 Dump("benchmark") << GetModelCommand();
5009 if(d_status
.isNull() ||
5010 d_status
.asSatisfiabilityResult() == Result::UNSAT
||
5011 d_problemExtended
) {
5013 "Cannot get the current model unless immediately "
5014 "preceded by SAT/INVALID or UNKNOWN response.";
5015 throw RecoverableModalException(msg
);
5017 if(!options::produceModels()) {
5019 "Cannot get model when produce-models options is off.";
5020 throw ModalException(msg
);
5022 TheoryModel
* m
= d_theoryEngine
->getModel();
5023 m
->d_inputName
= d_filename
;
5027 void SmtEngine::checkUnsatCore() {
5028 Assert(options::unsatCores(), "cannot check unsat core if unsat cores are turned off");
5030 Notice() << "SmtEngine::checkUnsatCore(): generating unsat core" << endl
;
5031 UnsatCore core
= getUnsatCore();
5033 SmtEngine
coreChecker(d_exprManager
);
5034 coreChecker
.setLogic(getLogicInfo());
5037 std::vector
<Command
*>::const_iterator itg
= d_defineCommands
.begin();
5038 for (; itg
!= d_defineCommands
.end(); ++itg
) {
5039 (*itg
)->invoke(&coreChecker
);
5043 Notice() << "SmtEngine::checkUnsatCore(): pushing core assertions (size == " << core
.size() << ")" << endl
;
5044 for(UnsatCore::iterator i
= core
.begin(); i
!= core
.end(); ++i
) {
5045 Notice() << "SmtEngine::checkUnsatCore(): pushing core member " << *i
<< endl
;
5046 coreChecker
.assertFormula(*i
);
5048 const bool checkUnsatCores
= options::checkUnsatCores();
5051 options::checkUnsatCores
.set(false);
5052 options::checkProofs
.set(false);
5053 r
= coreChecker
.checkSat();
5055 options::checkUnsatCores
.set(checkUnsatCores
);
5058 Notice() << "SmtEngine::checkUnsatCore(): result is " << r
<< endl
;
5059 if(r
.asSatisfiabilityResult().isUnknown()) {
5060 InternalError("SmtEngine::checkUnsatCore(): could not check core result unknown.");
5063 if(r
.asSatisfiabilityResult().isSat()) {
5064 InternalError("SmtEngine::checkUnsatCore(): produced core was satisfiable.");
5068 void SmtEngine::checkModel(bool hardFailure
) {
5069 // --check-model implies --produce-assertions, which enables the
5070 // assertion list, so we should be ok.
5071 Assert(d_assertionList
!= NULL
, "don't have an assertion list to check in SmtEngine::checkModel()");
5073 TimerStat::CodeTimer
checkModelTimer(d_stats
->d_checkModelTime
);
5075 // Throughout, we use Notice() to give diagnostic output.
5077 // If this function is running, the user gave --check-model (or equivalent),
5078 // and if Notice() is on, the user gave --verbose (or equivalent).
5080 Notice() << "SmtEngine::checkModel(): generating model" << endl
;
5081 TheoryModel
* m
= d_theoryEngine
->getModel();
5083 // Check individual theory assertions
5084 d_theoryEngine
->checkTheoryAssertionsWithModel(hardFailure
);
5089 // We have a "fake context" for the substitution map (we don't need it
5090 // to be context-dependent)
5091 context::Context fakeContext
;
5092 SubstitutionMap
substitutions(&fakeContext
, /* substituteUnderQuantifiers = */ false);
5094 for(size_t k
= 0; k
< m
->getNumCommands(); ++k
) {
5095 const DeclareFunctionCommand
* c
= dynamic_cast<const DeclareFunctionCommand
*>(m
->getCommand(k
));
5096 Notice() << "SmtEngine::checkModel(): model command " << k
<< " : " << m
->getCommand(k
) << endl
;
5098 // we don't care about DECLARE-DATATYPES, DECLARE-SORT, ...
5099 Notice() << "SmtEngine::checkModel(): skipping..." << endl
;
5101 // We have a DECLARE-FUN:
5103 // We'll first do some checks, then add to our substitution map
5104 // the mapping: function symbol |-> value
5106 Expr func
= c
->getFunction();
5107 Node val
= m
->getValue(func
);
5109 Notice() << "SmtEngine::checkModel(): adding substitution: " << func
<< " |-> " << val
<< endl
;
5111 // (1) if the value is a lambda, ensure the lambda doesn't contain the
5112 // function symbol (since then the definition is recursive)
5113 if (val
.getKind() == kind::LAMBDA
) {
5114 // first apply the model substitutions we have so far
5115 Debug("boolean-terms") << "applying subses to " << val
[1] << endl
;
5116 Node n
= substitutions
.apply(val
[1]);
5117 Debug("boolean-terms") << "++ got " << n
<< endl
;
5118 // now check if n contains func by doing a substitution
5119 // [func->func2] and checking equality of the Nodes.
5120 // (this just a way to check if func is in n.)
5121 SubstitutionMap
subs(&fakeContext
);
5122 Node func2
= NodeManager::currentNM()->mkSkolem("", TypeNode::fromType(func
.getType()), "", NodeManager::SKOLEM_NO_NOTIFY
);
5123 subs
.addSubstitution(func
, func2
);
5124 if(subs
.apply(n
) != n
) {
5125 Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE DEFINED IN TERMS OF ITSELF ***" << endl
;
5127 ss
<< "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
5128 << "considering model value for " << func
<< endl
5129 << "body of lambda is: " << val
<< endl
;
5131 ss
<< "body substitutes to: " << n
<< endl
;
5133 ss
<< "so " << func
<< " is defined in terms of itself." << endl
5134 << "Run with `--check-models -v' for additional diagnostics.";
5135 InternalError(ss
.str());
5139 // (2) check that the value is actually a value
5140 else if (!val
.isConst()) {
5141 Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE NOT A CONSTANT ***" << endl
;
5143 ss
<< "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
5144 << "model value for " << func
<< endl
5145 << " is " << val
<< endl
5146 << "and that is not a constant (.isConst() == false)." << endl
5147 << "Run with `--check-models -v' for additional diagnostics.";
5148 InternalError(ss
.str());
5151 // (3) check that it's the correct (sub)type
5152 // This was intended to be a more general check, but for now we can't do that because
5153 // e.g. "1" is an INT, which isn't a subrange type [1..10] (etc.).
5154 else if(func
.getType().isInteger() && !val
.getType().isInteger()) {
5155 Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE NOT CORRECT TYPE ***" << endl
;
5157 ss
<< "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
5158 << "model value for " << func
<< endl
5159 << " is " << val
<< endl
5160 << "value type is " << val
.getType() << endl
5161 << "should be of type " << func
.getType() << endl
5162 << "Run with `--check-models -v' for additional diagnostics.";
5163 InternalError(ss
.str());
5166 // (4) checks complete, add the substitution
5167 Debug("boolean-terms") << "cm: adding subs " << func
<< " :=> " << val
<< endl
;
5168 substitutions
.addSubstitution(func
, val
);
5172 // Now go through all our user assertions checking if they're satisfied.
5173 for(AssertionList::const_iterator i
= d_assertionList
->begin(); i
!= d_assertionList
->end(); ++i
) {
5174 Notice() << "SmtEngine::checkModel(): checking assertion " << *i
<< endl
;
5175 Node n
= Node::fromExpr(*i
);
5177 // Apply any define-funs from the problem.
5179 unordered_map
<Node
, Node
, NodeHashFunction
> cache
;
5180 n
= d_private
->expandDefinitions(n
, cache
);
5182 Notice() << "SmtEngine::checkModel(): -- expands to " << n
<< endl
;
5184 // Apply our model value substitutions.
5185 Debug("boolean-terms") << "applying subses to " << n
<< endl
;
5186 n
= substitutions
.apply(n
);
5187 Debug("boolean-terms") << "++ got " << n
<< endl
;
5188 Notice() << "SmtEngine::checkModel(): -- substitutes to " << n
<< endl
;
5190 if( n
.getKind() != kind::REWRITE_RULE
){
5191 // In case it's a quantifier (or contains one), look up its value before
5192 // simplifying, or the quantifier might be irreparably altered.
5194 Notice() << "SmtEngine::checkModel(): -- get value : " << n
<< std::endl
;
5196 // Note this "skip" is done here, rather than above. This is
5197 // because (1) the quantifier could in principle simplify to false,
5198 // which should be reported, and (2) checking for the quantifier
5199 // above, before simplification, doesn't catch buried quantifiers
5200 // anyway (those not at the top-level).
5201 Notice() << "SmtEngine::checkModel(): -- skipping rewrite-rules assertion"
5206 // Simplify the result.
5207 n
= d_private
->simplify(n
);
5208 Notice() << "SmtEngine::checkModel(): -- simplifies to " << n
<< endl
;
5210 // Replace the already-known ITEs (this is important for ground ITEs under quantifiers).
5211 n
= d_private
->d_iteRemover
.replace(n
);
5212 Notice() << "SmtEngine::checkModel(): -- ite replacement gives " << n
<< endl
;
5214 // Apply our model value substitutions (again), as things may have been simplified.
5215 Debug("boolean-terms") << "applying subses to " << n
<< endl
;
5216 n
= substitutions
.apply(n
);
5217 Debug("boolean-terms") << "++ got " << n
<< endl
;
5218 Notice() << "SmtEngine::checkModel(): -- re-substitutes to " << n
<< endl
;
5220 // As a last-ditch effort, ask model to simplify it.
5221 // Presently, this is only an issue for quantifiers, which can have a value
5222 // but don't show up in our substitution map above.
5224 Notice() << "SmtEngine::checkModel(): -- model-substitutes to " << n
<< endl
;
5226 if( d_logic
.isQuantified() ){
5227 // AJR: since quantified formulas are not checkable, we assign them to true/false based on the satisfying assignment.
5228 // however, quantified formulas can be modified during preprocess, so they may not correspond to those in the satisfying assignment.
5229 // hence we use a relaxed version of check model here.
5230 // this is necessary until preprocessing passes explicitly record how they rewrite quantified formulas
5231 if( hardFailure
&& !n
.isConst() && n
.getKind() != kind::LAMBDA
){
5232 Notice() << "SmtEngine::checkModel(): -- relax check model wrt quantified formulas..." << endl
;
5233 AlwaysAssert( quantifiers::QuantifiersRewriter::containsQuantifiers( n
) );
5234 Warning() << "Warning : SmtEngine::checkModel(): cannot check simplified assertion : " << n
<< endl
;
5238 AlwaysAssert(!hardFailure
|| n
.isConst() || n
.getKind() == kind::LAMBDA
);
5240 // The result should be == true.
5241 if(n
!= NodeManager::currentNM()->mkConst(true)) {
5242 Notice() << "SmtEngine::checkModel(): *** PROBLEM: EXPECTED `TRUE' ***"
5245 ss
<< "SmtEngine::checkModel(): "
5246 << "ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
5247 << "assertion: " << *i
<< endl
5248 << "simplifies to: " << n
<< endl
5249 << "expected `true'." << endl
5250 << "Run with `--check-models -v' for additional diagnostics.";
5252 InternalError(ss
.str());
5254 Warning() << ss
.str() << endl
;
5258 Notice() << "SmtEngine::checkModel(): all assertions checked out OK !" << endl
;
5261 // TODO(#1108): Simplify the error reporting of this method.
5262 UnsatCore
SmtEngine::getUnsatCore() {
5263 Trace("smt") << "SMT getUnsatCore()" << endl
;
5264 SmtScope
smts(this);
5265 finalOptionsAreSet();
5266 if(Dump
.isOn("benchmark")) {
5267 Dump("benchmark") << GetUnsatCoreCommand();
5270 if(!options::unsatCores()) {
5271 throw ModalException("Cannot get an unsat core when produce-unsat-cores option is off.");
5273 if(d_status
.isNull() ||
5274 d_status
.asSatisfiabilityResult() != Result::UNSAT
||
5275 d_problemExtended
) {
5276 throw RecoverableModalException(
5277 "Cannot get an unsat core unless immediately preceded by UNSAT/VALID "
5281 d_proofManager
->traceUnsatCore();// just to trigger core creation
5282 return UnsatCore(this, d_proofManager
->extractUnsatCore());
5283 #else /* IS_PROOFS_BUILD */
5284 throw ModalException("This build of CVC4 doesn't have proof support (required for unsat cores).");
5285 #endif /* IS_PROOFS_BUILD */
5288 // TODO(#1108): Simplify the error reporting of this method.
5289 Proof
* SmtEngine::getProof() {
5290 Trace("smt") << "SMT getProof()" << endl
;
5291 SmtScope
smts(this);
5292 finalOptionsAreSet();
5293 if(Dump
.isOn("benchmark")) {
5294 Dump("benchmark") << GetProofCommand();
5297 if(!options::proof()) {
5298 throw ModalException("Cannot get a proof when produce-proofs option is off.");
5300 if(d_status
.isNull() ||
5301 d_status
.asSatisfiabilityResult() != Result::UNSAT
||
5302 d_problemExtended
) {
5303 throw RecoverableModalException(
5304 "Cannot get a proof unless immediately preceded by UNSAT/VALID "
5308 return ProofManager::getProof(this);
5309 #else /* IS_PROOFS_BUILD */
5310 throw ModalException("This build of CVC4 doesn't have proof support.");
5311 #endif /* IS_PROOFS_BUILD */
5314 void SmtEngine::printInstantiations( std::ostream
& out
) {
5315 SmtScope
smts(this);
5316 if( options::instFormatMode()==INST_FORMAT_MODE_SZS
){
5317 out
<< "% SZS output start Proof for " << d_filename
.c_str() << std::endl
;
5319 if( d_theoryEngine
){
5320 d_theoryEngine
->printInstantiations( out
);
5324 if( options::instFormatMode()==INST_FORMAT_MODE_SZS
){
5325 out
<< "% SZS output end Proof for " << d_filename
.c_str() << std::endl
;
5329 void SmtEngine::printSynthSolution( std::ostream
& out
) {
5330 SmtScope
smts(this);
5331 if( d_theoryEngine
){
5332 d_theoryEngine
->printSynthSolution( out
);
5338 Expr
SmtEngine::doQuantifierElimination(const Expr
& e
, bool doFull
,
5339 bool strict
) throw(Exception
) {
5340 SmtScope
smts(this);
5341 if(!d_logic
.isPure(THEORY_ARITH
) && strict
){
5342 Warning() << "Unexpected logic for quantifier elimination " << d_logic
<< endl
;
5344 Trace("smt-qe") << "Do quantifier elimination " << e
<< std::endl
;
5345 Node n_e
= Node::fromExpr( e
);
5346 if (n_e
.getKind() != kind::EXISTS
&& n_e
.getKind() != kind::FORALL
)
5348 throw ModalException(
5349 "Expecting a quantified formula as argument to get-qe.");
5351 //tag the quantified formula with the quant-elim attribute
5352 TypeNode t
= NodeManager::currentNM()->booleanType();
5353 Node n_attr
= NodeManager::currentNM()->mkSkolem("qe", t
, "Auxiliary variable for qe attr.");
5354 std::vector
< Node
> node_values
;
5355 d_theoryEngine
->setUserAttribute( doFull
? "quant-elim" : "quant-elim-partial", n_attr
, node_values
, "");
5356 n_attr
= NodeManager::currentNM()->mkNode(kind::INST_ATTRIBUTE
, n_attr
);
5357 n_attr
= NodeManager::currentNM()->mkNode(kind::INST_PATTERN_LIST
, n_attr
);
5358 std::vector
< Node
> e_children
;
5359 e_children
.push_back( n_e
[0] );
5360 e_children
.push_back(n_e
.getKind() == kind::EXISTS
? n_e
[1]
5362 e_children
.push_back( n_attr
);
5363 Node nn_e
= NodeManager::currentNM()->mkNode( kind::EXISTS
, e_children
);
5364 Trace("smt-qe-debug") << "Query for quantifier elimination : " << nn_e
<< std::endl
;
5365 Assert( nn_e
.getNumChildren()==3 );
5366 Result r
= checkSatisfiability(nn_e
.toExpr(), true, true);
5367 Trace("smt-qe") << "Query returned " << r
<< std::endl
;
5368 if(r
.asSatisfiabilityResult().isSat() != Result::UNSAT
) {
5369 if( r
.asSatisfiabilityResult().isSat() != Result::SAT
&& doFull
){
5371 ss
<< "While performing quantifier elimination, unexpected result : " << r
<< " for query.";
5372 InternalError(ss
.str().c_str());
5374 std::vector
< Node
> inst_qs
;
5375 d_theoryEngine
->getInstantiatedQuantifiedFormulas( inst_qs
);
5376 Assert( inst_qs
.size()<=1 );
5378 if( inst_qs
.size()==1 ){
5379 Node top_q
= inst_qs
[0];
5380 //Node top_q = Rewriter::rewrite( nn_e ).negate();
5381 Assert( top_q
.getKind()==kind::FORALL
);
5382 Trace("smt-qe") << "Get qe for " << top_q
<< std::endl
;
5383 ret_n
= d_theoryEngine
->getInstantiatedConjunction( top_q
);
5384 Trace("smt-qe") << "Returned : " << ret_n
<< std::endl
;
5385 if (n_e
.getKind() == kind::EXISTS
)
5387 ret_n
= Rewriter::rewrite(ret_n
.negate());
5390 ret_n
= NodeManager::currentNM()->mkConst(n_e
.getKind() != kind::EXISTS
);
5392 return ret_n
.toExpr();
5394 return NodeManager::currentNM()
5395 ->mkConst(n_e
.getKind() == kind::EXISTS
)
5400 void SmtEngine::getInstantiatedQuantifiedFormulas( std::vector
< Expr
>& qs
) {
5401 SmtScope
smts(this);
5402 if( d_theoryEngine
){
5403 std::vector
< Node
> qs_n
;
5404 d_theoryEngine
->getInstantiatedQuantifiedFormulas( qs_n
);
5405 for( unsigned i
=0; i
<qs_n
.size(); i
++ ){
5406 qs
.push_back( qs_n
[i
].toExpr() );
5413 void SmtEngine::getInstantiations( Expr q
, std::vector
< Expr
>& insts
) {
5414 SmtScope
smts(this);
5415 if( d_theoryEngine
){
5416 std::vector
< Node
> insts_n
;
5417 d_theoryEngine
->getInstantiations( Node::fromExpr( q
), insts_n
);
5418 for( unsigned i
=0; i
<insts_n
.size(); i
++ ){
5419 insts
.push_back( insts_n
[i
].toExpr() );
5426 void SmtEngine::getInstantiationTermVectors( Expr q
, std::vector
< std::vector
< Expr
> >& tvecs
) {
5427 SmtScope
smts(this);
5428 Assert(options::trackInstLemmas());
5429 if( d_theoryEngine
){
5430 std::vector
< std::vector
< Node
> > tvecs_n
;
5431 d_theoryEngine
->getInstantiationTermVectors( Node::fromExpr( q
), tvecs_n
);
5432 for( unsigned i
=0; i
<tvecs_n
.size(); i
++ ){
5433 std::vector
< Expr
> tvec
;
5434 for( unsigned j
=0; j
<tvecs_n
[i
].size(); j
++ ){
5435 tvec
.push_back( tvecs_n
[i
][j
].toExpr() );
5437 tvecs
.push_back( tvec
);
5444 vector
<Expr
> SmtEngine::getAssertions() {
5445 SmtScope
smts(this);
5446 finalOptionsAreSet();
5448 if(Dump
.isOn("benchmark")) {
5449 Dump("benchmark") << GetAssertionsCommand();
5451 Trace("smt") << "SMT getAssertions()" << endl
;
5452 if(!options::produceAssertions()) {
5454 "Cannot query the current assertion list when not in produce-assertions mode.";
5455 throw ModalException(msg
);
5457 Assert(d_assertionList
!= NULL
);
5458 // copy the result out
5459 return vector
<Expr
>(d_assertionList
->begin(), d_assertionList
->end());
5462 void SmtEngine::push() throw(ModalException
, LogicException
, UnsafeInterruptException
) {
5463 SmtScope
smts(this);
5464 finalOptionsAreSet();
5466 Trace("smt") << "SMT push()" << endl
;
5467 d_private
->notifyPush();
5468 d_private
->processAssertions();
5469 if(Dump
.isOn("benchmark")) {
5470 Dump("benchmark") << PushCommand();
5472 if(!options::incrementalSolving()) {
5473 throw ModalException("Cannot push when not solving incrementally (use --incremental)");
5476 // check to see if a postsolve() is pending
5477 if(d_needPostsolve
) {
5478 d_theoryEngine
->postsolve();
5479 d_needPostsolve
= false;
5482 // The problem isn't really "extended" yet, but this disallows
5483 // get-model after a push, simplifying our lives somewhat and
5484 // staying symmtric with pop.
5485 d_problemExtended
= true;
5487 d_userLevels
.push_back(d_userContext
->getLevel());
5489 Trace("userpushpop") << "SmtEngine: pushed to level "
5490 << d_userContext
->getLevel() << endl
;
5493 void SmtEngine::pop() {
5494 SmtScope
smts(this);
5495 finalOptionsAreSet();
5496 Trace("smt") << "SMT pop()" << endl
;
5497 if(Dump
.isOn("benchmark")) {
5498 Dump("benchmark") << PopCommand();
5500 if(!options::incrementalSolving()) {
5501 throw ModalException("Cannot pop when not solving incrementally (use --incremental)");
5503 if(d_userLevels
.size() == 0) {
5504 throw ModalException("Cannot pop beyond the first user frame");
5507 // check to see if a postsolve() is pending
5508 if(d_needPostsolve
) {
5509 d_theoryEngine
->postsolve();
5510 d_needPostsolve
= false;
5513 // The problem isn't really "extended" yet, but this disallows
5514 // get-model after a pop, simplifying our lives somewhat. It might
5515 // not be strictly necessary to do so, since the pops occur lazily,
5516 // but also it would be weird to have a legally-executed (get-model)
5517 // that only returns a subset of the assignment (because the rest
5518 // is no longer in scope!).
5519 d_problemExtended
= true;
5521 AlwaysAssert(d_userContext
->getLevel() > 0);
5522 AlwaysAssert(d_userLevels
.back() < d_userContext
->getLevel());
5523 while (d_userLevels
.back() < d_userContext
->getLevel()) {
5526 d_userLevels
.pop_back();
5528 // Clear out assertion queues etc., in case anything is still in there
5529 d_private
->notifyPop();
5531 Trace("userpushpop") << "SmtEngine: popped to level "
5532 << d_userContext
->getLevel() << endl
;
5533 // FIXME: should we reset d_status here?
5534 // SMT-LIBv2 spec seems to imply no, but it would make sense to..
5537 void SmtEngine::internalPush() {
5538 Assert(d_fullyInited
);
5539 Trace("smt") << "SmtEngine::internalPush()" << endl
;
5541 if(options::incrementalSolving()) {
5542 d_private
->processAssertions();
5543 TimerStat::CodeTimer
pushPopTimer(d_stats
->d_pushPopTime
);
5544 d_userContext
->push();
5545 // the d_context push is done inside of the SAT solver
5546 d_propEngine
->push();
5550 void SmtEngine::internalPop(bool immediate
) {
5551 Assert(d_fullyInited
);
5552 Trace("smt") << "SmtEngine::internalPop()" << endl
;
5553 if(options::incrementalSolving()) {
5561 void SmtEngine::doPendingPops() {
5562 Assert(d_pendingPops
== 0 || options::incrementalSolving());
5563 while(d_pendingPops
> 0) {
5564 TimerStat::CodeTimer
pushPopTimer(d_stats
->d_pushPopTime
);
5565 d_propEngine
->pop();
5566 // the d_context pop is done inside of the SAT solver
5567 d_userContext
->pop();
5572 void SmtEngine::reset() throw() {
5573 SmtScope
smts(this);
5574 ExprManager
*em
= d_exprManager
;
5575 Trace("smt") << "SMT reset()" << endl
;
5576 if(Dump
.isOn("benchmark")) {
5577 Dump("benchmark") << ResetCommand();
5580 opts
.copyValues(d_originalOptions
);
5582 NodeManager::fromExprManager(em
)->getOptions().copyValues(opts
);
5583 new(this) SmtEngine(em
);
5586 void SmtEngine::resetAssertions() throw() {
5587 SmtScope
smts(this);
5589 Trace("smt") << "SMT resetAssertions()" << endl
;
5590 if(Dump
.isOn("benchmark")) {
5591 Dump("benchmark") << ResetAssertionsCommand();
5594 while(!d_userLevels
.empty()) {
5598 // Also remember the global push/pop around everything.
5599 Assert(d_userLevels
.size() == 0 && d_userContext
->getLevel() == 1);
5600 d_context
->popto(0);
5601 d_userContext
->popto(0);
5602 DeleteAndClearCommandVector(d_modelGlobalCommands
);
5603 d_userContext
->push();
5607 void SmtEngine::interrupt() throw(ModalException
) {
5608 if(!d_fullyInited
) {
5611 d_propEngine
->interrupt();
5612 d_theoryEngine
->interrupt();
5615 void SmtEngine::setResourceLimit(unsigned long units
, bool cumulative
) {
5616 d_private
->getResourceManager()->setResourceLimit(units
, cumulative
);
5618 void SmtEngine::setTimeLimit(unsigned long milis
, bool cumulative
) {
5619 d_private
->getResourceManager()->setTimeLimit(milis
, cumulative
);
5622 unsigned long SmtEngine::getResourceUsage() const {
5623 return d_private
->getResourceManager()->getResourceUsage();
5626 unsigned long SmtEngine::getTimeUsage() const {
5627 return d_private
->getResourceManager()->getTimeUsage();
5630 unsigned long SmtEngine::getResourceRemaining() const throw(ModalException
) {
5631 return d_private
->getResourceManager()->getResourceRemaining();
5634 unsigned long SmtEngine::getTimeRemaining() const throw(ModalException
) {
5635 return d_private
->getResourceManager()->getTimeRemaining();
5638 Statistics
SmtEngine::getStatistics() const throw() {
5639 return Statistics(*d_statisticsRegistry
);
5642 SExpr
SmtEngine::getStatistic(std::string name
) const throw() {
5643 return d_statisticsRegistry
->getStatistic(name
);
5646 void SmtEngine::safeFlushStatistics(int fd
) const {
5647 d_statisticsRegistry
->safeFlushInformation(fd
);
5650 void SmtEngine::setUserAttribute(const std::string
& attr
, Expr expr
, std::vector
<Expr
> expr_values
, std::string str_value
) {
5651 SmtScope
smts(this);
5652 std::vector
<Node
> node_values
;
5653 for( unsigned i
=0; i
<expr_values
.size(); i
++ ){
5654 node_values
.push_back( expr_values
[i
].getNode() );
5656 d_theoryEngine
->setUserAttribute(attr
, expr
.getNode(), node_values
, str_value
);
5659 void SmtEngine::setPrintFuncInModel(Expr f
, bool p
) {
5660 Trace("setp-model") << "Set printInModel " << f
<< " to " << p
<< std::endl
;
5661 for( unsigned i
=0; i
<d_modelGlobalCommands
.size(); i
++ ){
5662 Command
* c
= d_modelGlobalCommands
[i
];
5663 DeclareFunctionCommand
* dfc
= dynamic_cast<DeclareFunctionCommand
*>(c
);
5665 if( dfc
->getFunction()==f
){
5666 dfc
->setPrintInModel( p
);
5670 for( unsigned i
=0; i
<d_modelCommands
->size(); i
++ ){
5671 Command
* c
= (*d_modelCommands
)[i
];
5672 DeclareFunctionCommand
* dfc
= dynamic_cast<DeclareFunctionCommand
*>(c
);
5674 if( dfc
->getFunction()==f
){
5675 dfc
->setPrintInModel( p
);
5683 void SmtEngine::beforeSearch() throw(ModalException
) {
5685 throw ModalException(
5686 "SmtEngine::beforeSearch called after initialization.");
5691 void SmtEngine::setOption(const std::string
& key
, const CVC4::SExpr
& value
)
5692 throw(OptionException
, ModalException
) {
5694 NodeManagerScope
nms(d_nodeManager
);
5695 Trace("smt") << "SMT setOption(" << key
<< ", " << value
<< ")" << endl
;
5697 if(Dump
.isOn("benchmark")) {
5698 Dump("benchmark") << SetOptionCommand(key
, value
);
5701 if(key
== "command-verbosity") {
5702 if(!value
.isAtom()) {
5703 const vector
<SExpr
>& cs
= value
.getChildren();
5704 if(cs
.size() == 2 &&
5705 (cs
[0].isKeyword() || cs
[0].isString()) &&
5706 cs
[1].isInteger()) {
5707 string c
= cs
[0].getValue();
5708 const Integer
& v
= cs
[1].getIntegerValue();
5709 if(v
< 0 || v
> 2) {
5710 throw OptionException("command-verbosity must be 0, 1, or 2");
5712 d_commandVerbosity
[c
] = v
;
5716 throw OptionException("command-verbosity value must be a tuple (command-name, integer)");
5719 if(!value
.isAtom()) {
5720 throw OptionException("bad value for :" + key
);
5723 string optionarg
= value
.getValue();
5724 Options
& nodeManagerOptions
= NodeManager::currentNM()->getOptions();
5725 nodeManagerOptions
.setOption(key
, optionarg
);
5728 CVC4::SExpr
SmtEngine::getOption(const std::string
& key
) const
5729 throw(OptionException
) {
5731 NodeManagerScope
nms(d_nodeManager
);
5733 Trace("smt") << "SMT getOption(" << key
<< ")" << endl
;
5735 if(key
.length() >= 18 &&
5736 key
.compare(0, 18, "command-verbosity:") == 0) {
5737 map
<string
, Integer
>::const_iterator i
= d_commandVerbosity
.find(key
.c_str() + 18);
5738 if(i
!= d_commandVerbosity
.end()) {
5739 return SExpr((*i
).second
);
5741 i
= d_commandVerbosity
.find("*");
5742 if(i
!= d_commandVerbosity
.end()) {
5743 return SExpr((*i
).second
);
5745 return SExpr(Integer(2));
5748 if(Dump
.isOn("benchmark")) {
5749 Dump("benchmark") << GetOptionCommand(key
);
5752 if(key
== "command-verbosity") {
5753 vector
<SExpr
> result
;
5754 SExpr defaultVerbosity
;
5755 for(map
<string
, Integer
>::const_iterator i
= d_commandVerbosity
.begin();
5756 i
!= d_commandVerbosity
.end();
5759 v
.push_back(SExpr((*i
).first
));
5760 v
.push_back(SExpr((*i
).second
));
5761 if((*i
).first
== "*") {
5762 // put the default at the end of the SExpr
5763 defaultVerbosity
= SExpr(v
);
5765 result
.push_back(SExpr(v
));
5768 // put the default at the end of the SExpr
5769 if(!defaultVerbosity
.isAtom()) {
5770 result
.push_back(defaultVerbosity
);
5772 // ensure the default is always listed
5774 v
.push_back(SExpr("*"));
5775 v
.push_back(SExpr(Integer(2)));
5776 result
.push_back(SExpr(v
));
5778 return SExpr(result
);
5781 Options
& nodeManagerOptions
= NodeManager::currentNM()->getOptions();
5782 return SExpr::parseAtom(nodeManagerOptions
.getOption(key
));
5785 void SmtEngine::setReplayStream(ExprStream
* replayStream
) {
5786 AlwaysAssert(!d_fullyInited
,
5787 "Cannot set replay stream once fully initialized");
5788 d_replayStream
= replayStream
;
5791 bool SmtEngine::getExpressionName(Expr e
, std::string
& name
) const {
5792 return d_private
->getExpressionName(e
, name
);
5795 void SmtEngine::setExpressionName(Expr e
, const std::string
& name
) {
5796 Trace("smt-debug") << "Set expression name " << e
<< " to " << name
<< std::endl
;
5797 d_private
->setExpressionName(e
,name
);
5800 }/* CVC4 namespace */