1 /********************* */
2 /*! \file smt_engine.cpp
4 ** Top contributors (to current version):
5 ** Morgan Deters, Andrew Reynolds, Tim King
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
8 ** in the top-level source directory) and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
12 ** \brief The main entry point into the CVC4 library's SMT interface
14 ** The main entry point into the CVC4 library's SMT interface.
17 #include "smt/smt_engine.h"
26 #include <unordered_map>
27 #include <unordered_set>
31 #include "base/configuration.h"
32 #include "base/configuration_private.h"
33 #include "base/exception.h"
34 #include "base/listener.h"
35 #include "base/modal_exception.h"
36 #include "base/output.h"
37 #include "context/cdhashmap.h"
38 #include "context/cdhashset.h"
39 #include "context/cdlist.h"
40 #include "context/context.h"
41 #include "decision/decision_engine.h"
42 #include "expr/attribute.h"
43 #include "expr/expr.h"
44 #include "expr/kind.h"
45 #include "expr/metakind.h"
46 #include "expr/node.h"
47 #include "expr/node_builder.h"
48 #include "expr/node_self_iterator.h"
49 #include "options/arith_options.h"
50 #include "options/arrays_options.h"
51 #include "options/base_options.h"
52 #include "options/booleans_options.h"
53 #include "options/bv_options.h"
54 #include "options/datatypes_options.h"
55 #include "options/decision_mode.h"
56 #include "options/decision_options.h"
57 #include "options/language.h"
58 #include "options/main_options.h"
59 #include "options/open_ostream.h"
60 #include "options/option_exception.h"
61 #include "options/printer_options.h"
62 #include "options/proof_options.h"
63 #include "options/prop_options.h"
64 #include "options/quantifiers_options.h"
65 #include "options/sep_options.h"
66 #include "options/set_language.h"
67 #include "options/smt_options.h"
68 #include "options/strings_options.h"
69 #include "options/theory_options.h"
70 #include "options/uf_options.h"
71 #include "preprocessing/passes/apply_substs.h"
72 #include "preprocessing/passes/bool_to_bv.h"
73 #include "preprocessing/passes/bv_abstraction.h"
74 #include "preprocessing/passes/bv_ackermann.h"
75 #include "preprocessing/passes/bv_gauss.h"
76 #include "preprocessing/passes/bv_intro_pow2.h"
77 #include "preprocessing/passes/bv_to_bool.h"
78 #include "preprocessing/passes/int_to_bv.h"
79 #include "preprocessing/passes/pseudo_boolean_processor.h"
80 #include "preprocessing/passes/real_to_int.h"
81 #include "preprocessing/passes/rewrite.h"
82 #include "preprocessing/passes/sep_skolem_emp.h"
83 #include "preprocessing/passes/static_learning.h"
84 #include "preprocessing/passes/symmetry_breaker.h"
85 #include "preprocessing/passes/symmetry_detect.h"
86 #include "preprocessing/passes/synth_rew_rules.h"
87 #include "preprocessing/preprocessing_pass.h"
88 #include "preprocessing/preprocessing_pass_context.h"
89 #include "preprocessing/preprocessing_pass_registry.h"
90 #include "printer/printer.h"
91 #include "proof/proof.h"
92 #include "proof/proof_manager.h"
93 #include "proof/theory_proof.h"
94 #include "proof/unsat_core.h"
95 #include "prop/prop_engine.h"
96 #include "smt/command.h"
97 #include "smt/command_list.h"
98 #include "smt/logic_request.h"
99 #include "smt/managed_ostreams.h"
100 #include "smt/smt_engine_scope.h"
101 #include "smt/term_formula_removal.h"
102 #include "smt/update_ostream.h"
103 #include "smt_util/boolean_simplification.h"
104 #include "smt_util/nary_builder.h"
105 #include "smt_util/node_visitor.h"
106 #include "theory/booleans/circuit_propagator.h"
107 #include "theory/bv/theory_bv_rewriter.h"
108 #include "theory/logic_info.h"
109 #include "theory/quantifiers/fun_def_process.h"
110 #include "theory/quantifiers/global_negate.h"
111 #include "theory/quantifiers/macros.h"
112 #include "theory/quantifiers/quantifiers_rewriter.h"
113 #include "theory/quantifiers/single_inv_partition.h"
114 #include "theory/quantifiers/sygus/ce_guided_instantiation.h"
115 #include "theory/quantifiers/sygus_inference.h"
116 #include "theory/quantifiers/term_util.h"
117 #include "theory/rewriter.h"
118 #include "theory/sort_inference.h"
119 #include "theory/strings/theory_strings.h"
120 #include "theory/substitutions.h"
121 #include "theory/theory_engine.h"
122 #include "theory/theory_model.h"
123 #include "theory/theory_traits.h"
124 #include "util/hash.h"
125 #include "util/proof.h"
126 #include "util/random.h"
127 #include "util/resource_manager.h"
130 using namespace CVC4
;
131 using namespace CVC4::smt
;
132 using namespace CVC4::preprocessing
;
133 using namespace CVC4::preprocessing::passes
;
134 using namespace CVC4::prop
;
135 using namespace CVC4::context
;
136 using namespace CVC4::theory
;
141 struct DeleteCommandFunction
: public std::unary_function
<const Command
*, void>
143 void operator()(const Command
* command
) { delete command
; }
146 void DeleteAndClearCommandVector(std::vector
<Command
*>& commands
) {
147 std::for_each(commands
.begin(), commands
.end(), DeleteCommandFunction());
151 /** Useful for counting the number of recursive calls. */
156 ScopeCounter(unsigned& d
) : d_depth(d
) {
165 * Representation of a defined function. We keep these around in
166 * SmtEngine to permit expanding definitions late (and lazily), to
167 * support getValue() over defined functions, to support user output
168 * in terms of defined functions, etc.
170 class DefinedFunction
{
172 vector
<Node
> d_formals
;
176 DefinedFunction(Node func
, vector
<Node
> formals
, Node formula
) :
181 Node
getFunction() const { return d_func
; }
182 vector
<Node
> getFormals() const { return d_formals
; }
183 Node
getFormula() const { return d_formula
; }
184 };/* class DefinedFunction */
186 struct SmtEngineStatistics
{
187 /** time spent in gaussian elimination */
188 TimerStat d_gaussElimTime
;
189 /** time spent in definition-expansion */
190 TimerStat d_definitionExpansionTime
;
191 /** time spent in non-clausal simplification */
192 TimerStat d_nonclausalSimplificationTime
;
193 /** time spent in miplib pass */
194 TimerStat d_miplibPassTime
;
195 /** number of assertions removed by miplib pass */
196 IntStat d_numMiplibAssertionsRemoved
;
197 /** number of constant propagations found during nonclausal simp */
198 IntStat d_numConstantProps
;
199 /** time spent in simplifying ITEs */
200 TimerStat d_simpITETime
;
201 /** time spent in simplifying ITEs */
202 TimerStat d_unconstrainedSimpTime
;
203 /** time spent removing ITEs */
204 TimerStat d_iteRemovalTime
;
205 /** time spent in theory preprocessing */
206 TimerStat d_theoryPreprocessTime
;
207 /** time spent in theory preprocessing */
208 TimerStat d_rewriteApplyToConstTime
;
209 /** time spent converting to CNF */
210 TimerStat d_cnfConversionTime
;
211 /** Num of assertions before ite removal */
212 IntStat d_numAssertionsPre
;
213 /** Num of assertions after ite removal */
214 IntStat d_numAssertionsPost
;
215 /** time spent in checkModel() */
216 TimerStat d_checkModelTime
;
217 /** time spent in checkProof() */
218 TimerStat d_checkProofTime
;
219 /** time spent in checkUnsatCore() */
220 TimerStat d_checkUnsatCoreTime
;
221 /** time spent in PropEngine::checkSat() */
222 TimerStat d_solveTime
;
223 /** time spent in pushing/popping */
224 TimerStat d_pushPopTime
;
225 /** time spent in processAssertions() */
226 TimerStat d_processAssertionsTime
;
228 /** Has something simplified to false? */
229 IntStat d_simplifiedToFalse
;
230 /** Number of resource units spent. */
231 ReferenceStat
<uint64_t> d_resourceUnitsUsed
;
233 SmtEngineStatistics() :
234 d_gaussElimTime("smt::SmtEngine::gaussElimTime"),
235 d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"),
236 d_nonclausalSimplificationTime("smt::SmtEngine::nonclausalSimplificationTime"),
237 d_miplibPassTime("smt::SmtEngine::miplibPassTime"),
238 d_numMiplibAssertionsRemoved("smt::SmtEngine::numMiplibAssertionsRemoved", 0),
239 d_numConstantProps("smt::SmtEngine::numConstantProps", 0),
240 d_simpITETime("smt::SmtEngine::simpITETime"),
241 d_unconstrainedSimpTime("smt::SmtEngine::unconstrainedSimpTime"),
242 d_iteRemovalTime("smt::SmtEngine::iteRemovalTime"),
243 d_theoryPreprocessTime("smt::SmtEngine::theoryPreprocessTime"),
244 d_rewriteApplyToConstTime("smt::SmtEngine::rewriteApplyToConstTime"),
245 d_cnfConversionTime("smt::SmtEngine::cnfConversionTime"),
246 d_numAssertionsPre("smt::SmtEngine::numAssertionsPreITERemoval", 0),
247 d_numAssertionsPost("smt::SmtEngine::numAssertionsPostITERemoval", 0),
248 d_checkModelTime("smt::SmtEngine::checkModelTime"),
249 d_checkProofTime("smt::SmtEngine::checkProofTime"),
250 d_checkUnsatCoreTime("smt::SmtEngine::checkUnsatCoreTime"),
251 d_solveTime("smt::SmtEngine::solveTime"),
252 d_pushPopTime("smt::SmtEngine::pushPopTime"),
253 d_processAssertionsTime("smt::SmtEngine::processAssertionsTime"),
254 d_simplifiedToFalse("smt::SmtEngine::simplifiedToFalse", 0),
255 d_resourceUnitsUsed("smt::SmtEngine::resourceUnitsUsed")
258 smtStatisticsRegistry()->registerStat(&d_gaussElimTime
);
259 smtStatisticsRegistry()->registerStat(&d_definitionExpansionTime
);
260 smtStatisticsRegistry()->registerStat(&d_nonclausalSimplificationTime
);
261 smtStatisticsRegistry()->registerStat(&d_miplibPassTime
);
262 smtStatisticsRegistry()->registerStat(&d_numMiplibAssertionsRemoved
);
263 smtStatisticsRegistry()->registerStat(&d_numConstantProps
);
264 smtStatisticsRegistry()->registerStat(&d_simpITETime
);
265 smtStatisticsRegistry()->registerStat(&d_unconstrainedSimpTime
);
266 smtStatisticsRegistry()->registerStat(&d_iteRemovalTime
);
267 smtStatisticsRegistry()->registerStat(&d_theoryPreprocessTime
);
268 smtStatisticsRegistry()->registerStat(&d_rewriteApplyToConstTime
);
269 smtStatisticsRegistry()->registerStat(&d_cnfConversionTime
);
270 smtStatisticsRegistry()->registerStat(&d_numAssertionsPre
);
271 smtStatisticsRegistry()->registerStat(&d_numAssertionsPost
);
272 smtStatisticsRegistry()->registerStat(&d_checkModelTime
);
273 smtStatisticsRegistry()->registerStat(&d_checkProofTime
);
274 smtStatisticsRegistry()->registerStat(&d_checkUnsatCoreTime
);
275 smtStatisticsRegistry()->registerStat(&d_solveTime
);
276 smtStatisticsRegistry()->registerStat(&d_pushPopTime
);
277 smtStatisticsRegistry()->registerStat(&d_processAssertionsTime
);
278 smtStatisticsRegistry()->registerStat(&d_simplifiedToFalse
);
279 smtStatisticsRegistry()->registerStat(&d_resourceUnitsUsed
);
282 ~SmtEngineStatistics() {
283 smtStatisticsRegistry()->unregisterStat(&d_gaussElimTime
);
284 smtStatisticsRegistry()->unregisterStat(&d_definitionExpansionTime
);
285 smtStatisticsRegistry()->unregisterStat(&d_nonclausalSimplificationTime
);
286 smtStatisticsRegistry()->unregisterStat(&d_miplibPassTime
);
287 smtStatisticsRegistry()->unregisterStat(&d_numMiplibAssertionsRemoved
);
288 smtStatisticsRegistry()->unregisterStat(&d_numConstantProps
);
289 smtStatisticsRegistry()->unregisterStat(&d_simpITETime
);
290 smtStatisticsRegistry()->unregisterStat(&d_unconstrainedSimpTime
);
291 smtStatisticsRegistry()->unregisterStat(&d_iteRemovalTime
);
292 smtStatisticsRegistry()->unregisterStat(&d_theoryPreprocessTime
);
293 smtStatisticsRegistry()->unregisterStat(&d_rewriteApplyToConstTime
);
294 smtStatisticsRegistry()->unregisterStat(&d_cnfConversionTime
);
295 smtStatisticsRegistry()->unregisterStat(&d_numAssertionsPre
);
296 smtStatisticsRegistry()->unregisterStat(&d_numAssertionsPost
);
297 smtStatisticsRegistry()->unregisterStat(&d_checkModelTime
);
298 smtStatisticsRegistry()->unregisterStat(&d_checkProofTime
);
299 smtStatisticsRegistry()->unregisterStat(&d_checkUnsatCoreTime
);
300 smtStatisticsRegistry()->unregisterStat(&d_solveTime
);
301 smtStatisticsRegistry()->unregisterStat(&d_pushPopTime
);
302 smtStatisticsRegistry()->unregisterStat(&d_processAssertionsTime
);
303 smtStatisticsRegistry()->unregisterStat(&d_simplifiedToFalse
);
304 smtStatisticsRegistry()->unregisterStat(&d_resourceUnitsUsed
);
306 };/* struct SmtEngineStatistics */
309 class SoftResourceOutListener
: public Listener
{
311 SoftResourceOutListener(SmtEngine
& smt
) : d_smt(&smt
) {}
312 void notify() override
314 SmtScope
scope(d_smt
);
315 Assert(smt::smtEngineInScope());
320 }; /* class SoftResourceOutListener */
323 class HardResourceOutListener
: public Listener
{
325 HardResourceOutListener(SmtEngine
& smt
) : d_smt(&smt
) {}
326 void notify() override
328 SmtScope
scope(d_smt
);
329 theory::Rewriter::clearCaches();
333 }; /* class HardResourceOutListener */
335 class SetLogicListener
: public Listener
{
337 SetLogicListener(SmtEngine
& smt
) : d_smt(&smt
) {}
338 void notify() override
340 LogicInfo
inOptions(options::forceLogicString());
341 d_smt
->setLogic(inOptions
);
345 }; /* class SetLogicListener */
347 class BeforeSearchListener
: public Listener
{
349 BeforeSearchListener(SmtEngine
& smt
) : d_smt(&smt
) {}
350 void notify() override
{ d_smt
->beforeSearch(); }
354 }; /* class BeforeSearchListener */
356 class UseTheoryListListener
: public Listener
{
358 UseTheoryListListener(TheoryEngine
* theoryEngine
)
359 : d_theoryEngine(theoryEngine
)
362 void notify() override
364 std::stringstream
commaList(options::useTheoryList());
367 Debug("UseTheoryListListener") << "UseTheoryListListener::notify() "
368 << options::useTheoryList() << std::endl
;
370 while(std::getline(commaList
, token
, ',')){
371 if(token
== "help") {
372 puts(theory::useTheoryHelp
);
375 if(theory::useTheoryValidate(token
)) {
376 d_theoryEngine
->enableTheoryAlternative(token
);
378 throw OptionException(
379 std::string("unknown option for --use-theory : `") + token
+
380 "'. Try --use-theory=help.");
386 TheoryEngine
* d_theoryEngine
;
387 }; /* class UseTheoryListListener */
390 class SetDefaultExprDepthListener
: public Listener
{
392 void notify() override
394 int depth
= options::defaultExprDepth();
395 Debug
.getStream() << expr::ExprSetDepth(depth
);
396 Trace
.getStream() << expr::ExprSetDepth(depth
);
397 Notice
.getStream() << expr::ExprSetDepth(depth
);
398 Chat
.getStream() << expr::ExprSetDepth(depth
);
399 Message
.getStream() << expr::ExprSetDepth(depth
);
400 Warning
.getStream() << expr::ExprSetDepth(depth
);
401 // intentionally exclude Dump stream from this list
405 class SetDefaultExprDagListener
: public Listener
{
407 void notify() override
409 int dag
= options::defaultDagThresh();
410 Debug
.getStream() << expr::ExprDag(dag
);
411 Trace
.getStream() << expr::ExprDag(dag
);
412 Notice
.getStream() << expr::ExprDag(dag
);
413 Chat
.getStream() << expr::ExprDag(dag
);
414 Message
.getStream() << expr::ExprDag(dag
);
415 Warning
.getStream() << expr::ExprDag(dag
);
416 Dump
.getStream() << expr::ExprDag(dag
);
420 class SetPrintExprTypesListener
: public Listener
{
422 void notify() override
424 bool value
= options::printExprTypes();
425 Debug
.getStream() << expr::ExprPrintTypes(value
);
426 Trace
.getStream() << expr::ExprPrintTypes(value
);
427 Notice
.getStream() << expr::ExprPrintTypes(value
);
428 Chat
.getStream() << expr::ExprPrintTypes(value
);
429 Message
.getStream() << expr::ExprPrintTypes(value
);
430 Warning
.getStream() << expr::ExprPrintTypes(value
);
431 // intentionally exclude Dump stream from this list
435 class DumpModeListener
: public Listener
{
437 void notify() override
439 const std::string
& value
= options::dumpModeString();
440 Dump
.setDumpFromString(value
);
444 class PrintSuccessListener
: public Listener
{
446 void notify() override
448 bool value
= options::printSuccess();
449 Debug
.getStream() << Command::printsuccess(value
);
450 Trace
.getStream() << Command::printsuccess(value
);
451 Notice
.getStream() << Command::printsuccess(value
);
452 Chat
.getStream() << Command::printsuccess(value
);
453 Message
.getStream() << Command::printsuccess(value
);
454 Warning
.getStream() << Command::printsuccess(value
);
455 *options::out() << Command::printsuccess(value
);
462 * This is an inelegant solution, but for the present, it will work.
463 * The point of this is to separate the public and private portions of
464 * the SmtEngine class, so that smt_engine.h doesn't
465 * include "expr/node.h", which is a private CVC4 header (and can lead
466 * to linking errors due to the improper inlining of non-visible symbols
469 * The "real" solution (that which is usually implemented) is to move
470 * ALL the implementation to SmtEnginePrivate and maintain a
471 * heap-allocated instance of it in SmtEngine. SmtEngine (the public
472 * one) becomes an "interface shell" which simply acts as a forwarder
475 class SmtEnginePrivate
: public NodeManagerListener
{
478 typedef unordered_map
<Node
, Node
, NodeHashFunction
> NodeToNodeHashMap
;
479 typedef unordered_map
<Node
, bool, NodeHashFunction
> NodeToBoolHashMap
;
482 * Manager for limiting time and abstract resource usage.
484 ResourceManager
* d_resourceManager
;
486 /** Manager for the memory of regular-output-channel. */
487 ManagedRegularOutputChannel d_managedRegularChannel
;
489 /** Manager for the memory of diagnostic-output-channel. */
490 ManagedDiagnosticOutputChannel d_managedDiagnosticChannel
;
492 /** Manager for the memory of --dump-to. */
493 ManagedDumpOStream d_managedDumpChannel
;
495 /** Manager for --replay-log. */
496 ManagedReplayLogOstream d_managedReplayLog
;
499 * This list contains:
503 * beforeSearchListener
504 * UseTheoryListListener
506 * This needs to be deleted before both NodeManager's Options,
507 * SmtEngine, d_resourceManager, and TheoryEngine.
509 ListenerRegistrationList
* d_listenerRegistrations
;
511 /** Learned literals */
512 vector
<Node
> d_nonClausalLearnedLiterals
;
514 /** Size of assertions array when preprocessing starts */
515 unsigned d_realAssertionsEnd
;
517 /** A circuit propagator for non-clausal propositional deduction */
518 booleans::CircuitPropagator d_propagator
;
519 bool d_propagatorNeedsFinish
;
520 std::vector
<Node
> d_boolVars
;
522 /** Assertions in the preprocessing pipeline */
523 AssertionPipeline d_assertions
;
525 /** Whether any assertions have been processed */
526 CDO
<bool> d_assertionsProcessed
;
532 * A context that never pushes/pops, for use by CD structures (like
533 * SubstitutionMaps) that should be "global".
535 context::Context d_fakeContext
;
538 * A map of AbsractValues to their actual constants. Only used if
539 * options::abstractValues() is on.
541 SubstitutionMap d_abstractValueMap
;
544 * A mapping of all abstract values (actual value |-> abstract) that
545 * we've handed out. This is necessary to ensure that we give the
546 * same AbstractValues for the same real constants. Only used if
547 * options::abstractValues() is on.
549 NodeToNodeHashMap d_abstractValues
;
551 /** Number of calls of simplify assertions active.
553 unsigned d_simplifyAssertionsDepth
;
555 /** TODO: whether certain preprocess steps are necessary */
556 //bool d_needsExpandDefs;
558 //------------------------------- expression names
559 /** mapping from expressions to name */
560 context::CDHashMap
< Node
, std::string
, NodeHashFunction
> d_exprNames
;
561 //------------------------------- end expression names
564 * Map from skolem variables to index in d_assertions containing
565 * corresponding introduced Boolean ite
567 IteSkolemMap d_iteSkolemMap
;
569 /** Instance of the ITE remover */
570 RemoveTermFormulas d_iteRemover
;
572 /* Finishes the initialization of the private portion of SMTEngine. */
576 std::unique_ptr
<PreprocessingPassContext
> d_preprocessingPassContext
;
577 PreprocessingPassRegistry d_preprocessingPassRegistry
;
579 static const bool d_doConstantProp
= true;
582 * Runs the nonclausal solver and tries to solve all the assigned
585 * Returns false if the formula simplifies to "false"
587 bool nonClausalSimplify();
590 * Performs static learning on the assertions.
592 void staticLearning();
595 * Remove ITEs from the assertions.
599 Node
realToInt(TNode n
, NodeToNodeHashMap
& cache
, std::vector
< Node
>& var_eq
);
600 Node
purifyNlTerms(TNode n
, NodeToNodeHashMap
& cache
, NodeToNodeHashMap
& bcache
, std::vector
< Node
>& var_eq
, bool beneathMult
= false);
603 * Helper function to fix up assertion list to restore invariants needed after
606 void collectSkolems(TNode n
, set
<TNode
>& skolemSet
, NodeToBoolHashMap
& cache
);
609 * Helper function to fix up assertion list to restore invariants needed after
612 bool checkForBadSkolems(TNode n
, TNode skolem
, NodeToBoolHashMap
& cache
);
614 // Simplify ITE structure
617 // Simplify based on unconstrained values
618 void unconstrainedSimp();
621 * Ensures the assertions asserted after before now effectively come before
622 * d_realAssertionsEnd.
624 void compressBeforeRealAssertions(size_t before
);
627 * Trace nodes back to their assertions using CircuitPropagator's
630 void traceBackToAssertions(const std::vector
<Node
>& nodes
,
631 std::vector
<TNode
>& assertions
);
634 * Remove conjuncts in toRemove from conjunction n. Return # of removed
637 size_t removeFromConjunction(Node
& n
,
638 const std::unordered_set
<unsigned long>& toRemove
);
640 /** Scrub miplib encodings. */
641 void doMiplibTrick();
644 * Perform non-clausal simplification of a Node. This involves
645 * Theory implementations, but does NOT involve the SAT solver in
648 * Returns false if the formula simplifies to "false"
650 bool simplifyAssertions();
653 SmtEnginePrivate(SmtEngine
& smt
)
655 d_managedRegularChannel(),
656 d_managedDiagnosticChannel(),
657 d_managedDumpChannel(),
658 d_managedReplayLog(),
659 d_listenerRegistrations(new ListenerRegistrationList()),
660 d_nonClausalLearnedLiterals(),
661 d_realAssertionsEnd(0),
662 d_propagator(d_nonClausalLearnedLiterals
, true, true),
663 d_propagatorNeedsFinish(false),
664 d_assertions(d_smt
.d_userContext
),
665 d_assertionsProcessed(smt
.d_userContext
, false),
667 d_abstractValueMap(&d_fakeContext
),
669 d_simplifyAssertionsDepth(0),
670 // d_needsExpandDefs(true), //TODO?
671 d_exprNames(smt
.d_userContext
),
673 d_iteRemover(smt
.d_userContext
)
675 d_smt
.d_nodeManager
->subscribeEvents(this);
676 d_true
= NodeManager::currentNM()->mkConst(true);
677 d_resourceManager
= NodeManager::currentResourceManager();
679 d_listenerRegistrations
->add(d_resourceManager
->registerSoftListener(
680 new SoftResourceOutListener(d_smt
)));
682 d_listenerRegistrations
->add(d_resourceManager
->registerHardListener(
683 new HardResourceOutListener(d_smt
)));
685 Options
& nodeManagerOptions
= NodeManager::currentNM()->getOptions();
686 d_listenerRegistrations
->add(
687 nodeManagerOptions
.registerForceLogicListener(
688 new SetLogicListener(d_smt
), true));
690 // Multiple options reuse BeforeSearchListener so registration requires an
691 // extra bit of care.
692 // We can safely not call notify on this before search listener at
693 // registration time. This d_smt cannot be beforeSearch at construction
694 // time. Therefore the BeforeSearchListener is a no-op. Therefore it does
695 // not have to be called.
696 d_listenerRegistrations
->add(
697 nodeManagerOptions
.registerBeforeSearchListener(
698 new BeforeSearchListener(d_smt
)));
700 // These do need registration calls.
701 d_listenerRegistrations
->add(
702 nodeManagerOptions
.registerSetDefaultExprDepthListener(
703 new SetDefaultExprDepthListener(), true));
704 d_listenerRegistrations
->add(
705 nodeManagerOptions
.registerSetDefaultExprDagListener(
706 new SetDefaultExprDagListener(), true));
707 d_listenerRegistrations
->add(
708 nodeManagerOptions
.registerSetPrintExprTypesListener(
709 new SetPrintExprTypesListener(), true));
710 d_listenerRegistrations
->add(
711 nodeManagerOptions
.registerSetDumpModeListener(
712 new DumpModeListener(), true));
713 d_listenerRegistrations
->add(
714 nodeManagerOptions
.registerSetPrintSuccessListener(
715 new PrintSuccessListener(), true));
716 d_listenerRegistrations
->add(
717 nodeManagerOptions
.registerSetRegularOutputChannelListener(
718 new SetToDefaultSourceListener(&d_managedRegularChannel
), true));
719 d_listenerRegistrations
->add(
720 nodeManagerOptions
.registerSetDiagnosticOutputChannelListener(
721 new SetToDefaultSourceListener(&d_managedDiagnosticChannel
), true));
722 d_listenerRegistrations
->add(
723 nodeManagerOptions
.registerDumpToFileNameListener(
724 new SetToDefaultSourceListener(&d_managedDumpChannel
), true));
725 d_listenerRegistrations
->add(
726 nodeManagerOptions
.registerSetReplayLogFilename(
727 new SetToDefaultSourceListener(&d_managedReplayLog
), true));
732 delete d_listenerRegistrations
;
734 if(d_propagatorNeedsFinish
) {
735 d_propagator
.finish();
736 d_propagatorNeedsFinish
= false;
738 d_smt
.d_nodeManager
->unsubscribeEvents(this);
741 void unregisterPreprocessingPasses()
743 d_preprocessingPassRegistry
.unregisterPasses();
746 ResourceManager
* getResourceManager() { return d_resourceManager
; }
747 void spendResource(unsigned amount
)
749 d_resourceManager
->spendResource(amount
);
752 void nmNotifyNewSort(TypeNode tn
, uint32_t flags
) override
754 DeclareTypeCommand
c(tn
.getAttribute(expr::VarNameAttr()),
757 if((flags
& ExprManager::SORT_FLAG_PLACEHOLDER
) == 0) {
758 d_smt
.addToModelCommandAndDump(c
, flags
);
762 void nmNotifyNewSortConstructor(TypeNode tn
, uint32_t flags
) override
764 DeclareTypeCommand
c(tn
.getAttribute(expr::VarNameAttr()),
765 tn
.getAttribute(expr::SortArityAttr()),
767 if ((flags
& ExprManager::SORT_FLAG_PLACEHOLDER
) == 0)
769 d_smt
.addToModelCommandAndDump(c
);
773 void nmNotifyNewDatatypes(const std::vector
<DatatypeType
>& dtts
) override
775 DatatypeDeclarationCommand
c(dtts
);
776 d_smt
.addToModelCommandAndDump(c
);
779 void nmNotifyNewVar(TNode n
, uint32_t flags
) override
781 DeclareFunctionCommand
c(n
.getAttribute(expr::VarNameAttr()),
783 n
.getType().toType());
784 if((flags
& ExprManager::VAR_FLAG_DEFINED
) == 0) {
785 d_smt
.addToModelCommandAndDump(c
, flags
);
787 if(n
.getType().isBoolean() && !options::incrementalSolving()) {
788 d_boolVars
.push_back(n
);
792 void nmNotifyNewSkolem(TNode n
,
793 const std::string
& comment
,
794 uint32_t flags
) override
796 string id
= n
.getAttribute(expr::VarNameAttr());
797 DeclareFunctionCommand
c(id
, n
.toExpr(), n
.getType().toType());
798 if(Dump
.isOn("skolems") && comment
!= "") {
799 Dump("skolems") << CommentCommand(id
+ " is " + comment
);
801 if((flags
& ExprManager::VAR_FLAG_DEFINED
) == 0) {
802 d_smt
.addToModelCommandAndDump(c
, flags
, false, "skolems");
804 if(n
.getType().isBoolean() && !options::incrementalSolving()) {
805 d_boolVars
.push_back(n
);
809 void nmNotifyDeleteNode(TNode n
) override
{}
811 Node
applySubstitutions(TNode node
)
813 return Rewriter::rewrite(
814 d_assertions
.getTopLevelSubstitutions().apply(node
));
818 * Process the assertions that have been asserted.
820 void processAssertions();
822 /** Process a user push.
829 * Process a user pop. Clears out the non-context-dependent stuff in this
830 * SmtEnginePrivate. Necessary to clear out our assertion vectors in case
831 * someone does a push-assert-pop without a check-sat. It also pops the
832 * last map of expression names from notifyPush.
835 d_assertions
.clear();
836 d_nonClausalLearnedLiterals
.clear();
837 d_realAssertionsEnd
= 0;
838 d_iteSkolemMap
.clear();
842 * Adds a formula to the current context. Action here depends on
843 * the SimplificationMode (in the current Options scope); the
844 * formula might be pushed out to the propositional layer
845 * immediately, or it might be simplified and kept, or it might not
846 * even be simplified.
847 * the 2nd and 3rd arguments added for bookkeeping for proofs
849 void addFormula(TNode n
, bool inUnsatCore
, bool inInput
= true);
851 /** Expand definitions in n. */
852 Node
expandDefinitions(TNode n
,
853 NodeToNodeHashMap
& cache
,
854 bool expandOnly
= false);
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
)
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),
1017 d_globalNegation(false),
1019 d_replayStream(NULL
),
1021 d_statisticsRegistry(NULL
),
1023 d_channels(new LemmaChannels())
1025 SmtScope
smts(this);
1026 d_originalOptions
.copyValues(em
->getOptions());
1027 d_private
= new smt::SmtEnginePrivate(*this);
1028 d_statisticsRegistry
= new StatisticsRegistry();
1029 d_stats
= new SmtEngineStatistics();
1030 d_stats
->d_resourceUnitsUsed
.setData(
1031 d_private
->getResourceManager()->getResourceUsage());
1033 // The ProofManager is constructed before any other proof objects such as
1034 // SatProof and TheoryProofs. The TheoryProofEngine and the SatProof are
1035 // initialized in TheoryEngine and PropEngine respectively.
1036 Assert(d_proofManager
== NULL
);
1038 // d_proofManager must be created before Options has been finished
1039 // being parsed from the input file. Because of this, we cannot trust
1040 // that options::proof() is set correctly yet.
1042 d_proofManager
= new ProofManager(d_userContext
);
1045 // We have mutual dependency here, so we add the prop engine to the theory
1046 // engine later (it is non-essential there)
1047 d_theoryEngine
= new TheoryEngine(d_context
, d_userContext
,
1048 d_private
->d_iteRemover
,
1049 const_cast<const LogicInfo
&>(d_logic
),
1053 for(TheoryId id
= theory::THEORY_FIRST
; id
< theory::THEORY_LAST
; ++id
) {
1054 TheoryConstructor::addTheory(d_theoryEngine
, id
);
1055 //register with proof engine if applicable
1057 ProofManager::currentPM()->getTheoryProofEngine()->registerTheory(d_theoryEngine
->theoryOf(id
));
1061 d_private
->addUseTheoryListListener(d_theoryEngine
);
1063 // global push/pop around everything, to ensure proper destruction
1064 // of context-dependent data structures
1065 d_userContext
->push();
1068 d_definedFunctions
= new(true) DefinedFunctionMap(d_userContext
);
1069 d_fmfRecFunctionsDefined
= new(true) NodeList(d_userContext
);
1070 d_modelCommands
= new(true) smt::CommandList(d_userContext
);
1073 void SmtEngine::finishInit() {
1074 Trace("smt-debug") << "SmtEngine::finishInit" << std::endl
;
1075 // ensure that our heuristics are properly set up
1078 Trace("smt-debug") << "Making decision engine..." << std::endl
;
1080 d_decisionEngine
= new DecisionEngine(d_context
, d_userContext
);
1081 d_decisionEngine
->init(); // enable appropriate strategies
1083 Trace("smt-debug") << "Making prop engine..." << std::endl
;
1084 d_propEngine
= new PropEngine(d_theoryEngine
, d_decisionEngine
, d_context
,
1085 d_userContext
, d_private
->getReplayLog(),
1086 d_replayStream
, d_channels
);
1088 Trace("smt-debug") << "Setting up theory engine..." << std::endl
;
1089 d_theoryEngine
->setPropEngine(d_propEngine
);
1090 d_theoryEngine
->setDecisionEngine(d_decisionEngine
);
1091 Trace("smt-debug") << "Finishing init for theory engine..." << std::endl
;
1092 d_theoryEngine
->finishInit();
1094 Trace("smt-debug") << "Set up assertion list..." << std::endl
;
1095 // [MGD 10/20/2011] keep around in incremental mode, due to a
1096 // cleanup ordering issue and Nodes/TNodes. If SAT is popped
1097 // first, some user-context-dependent TNodes might still exist
1099 if(options::produceAssertions() ||
1100 options::incrementalSolving()) {
1101 // In the case of incremental solving, we appear to need these to
1102 // ensure the relevant Nodes remain live.
1103 d_assertionList
= new(true) AssertionList(d_userContext
);
1106 // dump out a set-logic command
1107 if(Dump
.isOn("benchmark")) {
1108 if (Dump
.isOn("raw-benchmark")) {
1109 Dump("raw-benchmark") << SetBenchmarkLogicCommand(d_logic
.getLogicString());
1111 LogicInfo everything
;
1113 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.")
1114 << SetBenchmarkLogicCommand(everything
.getLogicString());
1118 Trace("smt-debug") << "Dump declaration commands..." << std::endl
;
1119 // dump out any pending declaration commands
1120 for(unsigned i
= 0; i
< d_dumpCommands
.size(); ++i
) {
1121 Dump("declarations") << *d_dumpCommands
[i
];
1122 delete d_dumpCommands
[i
];
1124 d_dumpCommands
.clear();
1126 PROOF( ProofManager::currentPM()->setLogic(d_logic
); );
1128 for(TheoryId id
= theory::THEORY_FIRST
; id
< theory::THEORY_LAST
; ++id
) {
1129 ProofManager::currentPM()->getTheoryProofEngine()->
1130 finishRegisterTheory(d_theoryEngine
->theoryOf(id
));
1133 d_private
->finishInit();
1134 Trace("smt-debug") << "SmtEngine::finishInit done" << std::endl
;
1137 void SmtEngine::finalOptionsAreSet() {
1142 if(! d_logic
.isLocked()) {
1146 // finish initialization, create the prop engine, etc.
1149 AlwaysAssert( d_propEngine
->getAssertionLevel() == 0,
1150 "The PropEngine has pushed but the SmtEngine "
1151 "hasn't finished initializing!" );
1153 d_fullyInited
= true;
1154 Assert(d_logic
.isLocked());
1156 d_propEngine
->assertFormula(NodeManager::currentNM()->mkConst
<bool>(true));
1157 d_propEngine
->assertFormula(NodeManager::currentNM()->mkConst
<bool>(false).notNode());
1160 void SmtEngine::shutdown() {
1163 while(options::incrementalSolving() && d_userContext
->getLevel() > 1) {
1167 // check to see if a postsolve() is pending
1168 if(d_needPostsolve
) {
1169 d_theoryEngine
->postsolve();
1170 d_needPostsolve
= false;
1173 if(d_propEngine
!= NULL
) {
1174 d_propEngine
->shutdown();
1176 if(d_theoryEngine
!= NULL
) {
1177 d_theoryEngine
->shutdown();
1179 if(d_decisionEngine
!= NULL
) {
1180 d_decisionEngine
->shutdown();
1184 SmtEngine::~SmtEngine()
1186 SmtScope
smts(this);
1191 // global push/pop around everything, to ensure proper destruction
1192 // of context-dependent data structures
1193 d_context
->popto(0);
1194 d_userContext
->popto(0);
1196 if(d_assignments
!= NULL
) {
1197 d_assignments
->deleteSelf();
1200 if(d_assertionList
!= NULL
) {
1201 d_assertionList
->deleteSelf();
1204 for(unsigned i
= 0; i
< d_dumpCommands
.size(); ++i
) {
1205 delete d_dumpCommands
[i
];
1206 d_dumpCommands
[i
] = NULL
;
1208 d_dumpCommands
.clear();
1210 DeleteAndClearCommandVector(d_modelGlobalCommands
);
1212 if(d_modelCommands
!= NULL
) {
1213 d_modelCommands
->deleteSelf();
1216 d_definedFunctions
->deleteSelf();
1217 d_fmfRecFunctionsDefined
->deleteSelf();
1219 //destroy all passes before destroying things that they refer to
1220 d_private
->unregisterPreprocessingPasses();
1222 delete d_theoryEngine
;
1223 d_theoryEngine
= NULL
;
1224 delete d_propEngine
;
1225 d_propEngine
= NULL
;
1226 delete d_decisionEngine
;
1227 d_decisionEngine
= NULL
;
1230 // d_proofManager is always created when proofs are enabled at configure time.
1231 // Becuase of this, this code should not be wrapped in PROOF() which
1232 // additionally checks flags such as options::proof().
1234 delete d_proofManager
;
1235 d_proofManager
= NULL
;
1240 delete d_statisticsRegistry
;
1241 d_statisticsRegistry
= NULL
;
1246 delete d_userContext
;
1247 d_userContext
= NULL
;
1254 } catch(Exception
& e
) {
1255 Warning() << "CVC4 threw an exception during cleanup." << endl
1260 void SmtEngine::setLogic(const LogicInfo
& logic
)
1262 SmtScope
smts(this);
1264 throw ModalException("Cannot set logic in SmtEngine after the engine has "
1265 "finished initializing.");
1271 void SmtEngine::setLogic(const std::string
& s
)
1273 SmtScope
smts(this);
1275 setLogic(LogicInfo(s
));
1276 } catch(IllegalArgumentException
& e
) {
1277 throw LogicException(e
.what());
1281 void SmtEngine::setLogic(const char* logic
) { setLogic(string(logic
)); }
1282 LogicInfo
SmtEngine::getLogicInfo() const {
1285 void SmtEngine::setLogicInternal()
1287 Assert(!d_fullyInited
, "setting logic in SmtEngine but the engine has already"
1288 " finished initializing for this run");
1292 void SmtEngine::setDefaults() {
1293 Random::getRandom().setSeed(options::seed());
1294 // Language-based defaults
1295 if (!options::bitvectorDivByZeroConst
.wasSetByUser())
1297 options::bitvectorDivByZeroConst
.set(
1298 language::isInputLang_smt2_6(options::inputLanguage()));
1300 bool is_sygus
= false;
1301 if (options::inputLanguage() == language::input::LANG_SYGUS
)
1304 if (!options::ceGuidedInst
.wasSetByUser())
1306 options::ceGuidedInst
.set(true);
1308 // must use Ferrante/Rackoff for real arithmetic
1309 if (!options::cbqiMidpoint
.wasSetByUser())
1311 options::cbqiMidpoint
.set(true);
1313 if (options::sygusRepairConst())
1315 if (!options::cbqi
.wasSetByUser())
1317 options::cbqi
.set(true);
1322 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
)
1324 if (options::produceModels()
1325 && (d_logic
.isTheoryEnabled(THEORY_ARRAYS
)
1326 || d_logic
.isTheoryEnabled(THEORY_UF
)))
1328 if (options::bitblastMode
.wasSetByUser()
1329 || options::produceModels
.wasSetByUser())
1331 throw OptionException(std::string(
1332 "Eager bit-blasting currently does not support model generation "
1333 "for the combination of bit-vectors with arrays or uinterpreted "
1334 "functions. Try --bitblast=lazy"));
1336 Notice() << "SmtEngine: setting bit-blast mode to lazy to support model"
1337 << "generation" << endl
;
1338 setOption("bitblastMode", SExpr("lazy"));
1341 if (options::incrementalSolving() && !d_logic
.isPure(THEORY_BV
))
1343 throw OptionException(
1344 "Incremental eager bit-blasting is currently "
1345 "only supported for QF_BV. Try --bitblast=lazy.");
1349 if(options::forceLogicString
.wasSetByUser()) {
1350 d_logic
= LogicInfo(options::forceLogicString());
1351 }else if (options::solveIntAsBV() > 0) {
1352 d_logic
= LogicInfo("QF_BV");
1353 }else if (d_logic
.getLogicString() == "QF_NRA" && options::solveRealAsInt()) {
1354 d_logic
= LogicInfo("QF_NIA");
1355 } else if ((d_logic
.getLogicString() == "QF_UFBV" ||
1356 d_logic
.getLogicString() == "QF_ABV") &&
1357 options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
) {
1358 d_logic
= LogicInfo("QF_BV");
1362 /* - disabled for 1.4 release [MGD 2014.06.25]
1363 if(!d_logic.hasEverything() && d_logic.isTheoryEnabled(THEORY_STRINGS) ) {
1364 if(! options::stringExp.wasSetByUser()) {
1365 options::stringExp.set( true );
1366 Trace("smt") << "turning on strings-exp, for the theory of strings" << std::endl;
1371 if(options::stringExp()) {
1372 if( !d_logic
.isQuantified() ) {
1373 d_logic
= d_logic
.getUnlockedCopy();
1374 d_logic
.enableQuantifiers();
1376 Trace("smt") << "turning on quantifier logic, for strings-exp"
1379 if(! options::fmfBound
.wasSetByUser()) {
1380 options::fmfBound
.set( true );
1381 Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl
;
1383 if(! options::fmfInstEngine
.wasSetByUser()) {
1384 options::fmfInstEngine
.set( true );
1385 Trace("smt") << "turning on fmf-inst-engine, for strings-exp" << std::endl
;
1388 if(! options::rewriteDivk.wasSetByUser()) {
1389 options::rewriteDivk.set( true );
1390 Trace("smt") << "turning on rewrite-divk, for strings-exp" << std::endl;
1393 if(! options::stringFMF.wasSetByUser()) {
1394 options::stringFMF.set( true );
1395 Trace("smt") << "turning on strings-fmf, for strings-exp" << std::endl;
1400 // sygus inference may require datatypes
1401 if (options::sygusInference())
1403 d_logic
= d_logic
.getUnlockedCopy();
1404 d_logic
.enableTheory(THEORY_DATATYPES
);
1408 if ((options::checkModels() || options::checkSynthSol())
1409 && !options::produceAssertions())
1411 Notice() << "SmtEngine: turning on produce-assertions to support "
1412 << "check-models or check-synth-sol." << endl
;
1413 setOption("produce-assertions", SExpr("true"));
1416 // Disable options incompatible with incremental solving, unsat cores, and
1417 // proofs or output an error if enabled explicitly
1418 if (options::incrementalSolving() || options::unsatCores()
1419 || options::proof())
1421 if (options::unconstrainedSimp())
1423 if (options::unconstrainedSimp
.wasSetByUser())
1425 throw OptionException(
1426 "unconstrained simplification not supported with unsat "
1427 "cores/proofs/incremental solving");
1429 Notice() << "SmtEngine: turning off unconstrained simplification to "
1430 "support unsat cores/proofs/incremental solving"
1432 options::unconstrainedSimp
.set(false);
1437 // Turn on unconstrained simplification for QF_AUFBV
1438 if (!options::unconstrainedSimp
.wasSetByUser())
1440 // bool qf_sat = d_logic.isPure(THEORY_BOOL) &&
1441 // !d_logic.isQuantified(); bool uncSimp = false && !qf_sat &&
1442 // !options::incrementalSolving();
1443 bool uncSimp
= !d_logic
.isQuantified() && !options::produceModels()
1444 && !options::produceAssignments()
1445 && !options::checkModels()
1446 && (d_logic
.isTheoryEnabled(THEORY_ARRAYS
)
1447 && d_logic
.isTheoryEnabled(THEORY_BV
));
1448 Trace("smt") << "setting unconstrained simplification to " << uncSimp
1450 options::unconstrainedSimp
.set(uncSimp
);
1454 // Disable options incompatible with unsat cores and proofs or output an
1455 // error if enabled explicitly
1456 if (options::unsatCores() || options::proof())
1458 if (options::simplificationMode() != SIMPLIFICATION_MODE_NONE
)
1460 if (options::simplificationMode
.wasSetByUser())
1462 throw OptionException(
1463 "simplification not supported with unsat cores/proofs");
1465 Notice() << "SmtEngine: turning off simplification to support unsat "
1468 options::simplificationMode
.set(SIMPLIFICATION_MODE_NONE
);
1471 if (options::pbRewrites())
1473 if (options::pbRewrites
.wasSetByUser())
1475 throw OptionException(
1476 "pseudoboolean rewrites not supported with unsat cores/proofs");
1478 Notice() << "SmtEngine: turning off pseudoboolean rewrites to support "
1479 "unsat cores/proofs"
1481 setOption("pb-rewrites", false);
1484 if (options::sortInference())
1486 if (options::sortInference
.wasSetByUser())
1488 throw OptionException(
1489 "sort inference not supported with unsat cores/proofs");
1491 Notice() << "SmtEngine: turning off sort inference to support unsat "
1494 options::sortInference
.set(false);
1497 if (options::preSkolemQuant())
1499 if (options::preSkolemQuant
.wasSetByUser())
1501 throw OptionException(
1502 "pre-skolemization not supported with unsat cores/proofs");
1504 Notice() << "SmtEngine: turning off pre-skolemization to support unsat "
1507 options::preSkolemQuant
.set(false);
1510 if (options::bitvectorToBool())
1512 if (options::bitvectorToBool
.wasSetByUser())
1514 throw OptionException(
1515 "bv-to-bool not supported with unsat cores/proofs");
1517 Notice() << "SmtEngine: turning off bitvector-to-bool to support unsat "
1520 options::bitvectorToBool
.set(false);
1523 if (options::boolToBitvector())
1525 if (options::boolToBitvector
.wasSetByUser())
1527 throw OptionException(
1528 "bool-to-bv not supported with unsat cores/proofs");
1530 Notice() << "SmtEngine: turning off bool-to-bitvector to support unsat "
1533 options::boolToBitvector
.set(false);
1536 if (options::bvIntroducePow2())
1538 if (options::bvIntroducePow2
.wasSetByUser())
1540 throw OptionException(
1541 "bv-intro-pow2 not supported with unsat cores/proofs");
1543 Notice() << "SmtEngine: turning off bv-intro-pow2 to support "
1544 "unsat-cores/proofs"
1546 setOption("bv-intro-pow2", false);
1549 if (options::repeatSimp())
1551 if (options::repeatSimp
.wasSetByUser())
1553 throw OptionException(
1554 "repeat-simp not supported with unsat cores/proofs");
1556 Notice() << "SmtEngine: turning off repeat-simp to support unsat "
1559 setOption("repeat-simp", false);
1562 if (options::globalNegate())
1564 if (options::globalNegate
.wasSetByUser())
1566 throw OptionException(
1567 "global-negate not supported with unsat cores/proofs");
1569 Notice() << "SmtEngine: turning off global-negate to support unsat "
1572 setOption("global-negate", false);
1577 // by default, nonclausal simplification is off for QF_SAT
1578 if (!options::simplificationMode
.wasSetByUser())
1580 bool qf_sat
= d_logic
.isPure(THEORY_BOOL
) && !d_logic
.isQuantified();
1581 Trace("smt") << "setting simplification mode to <"
1582 << d_logic
.getLogicString() << "> " << (!qf_sat
) << endl
;
1583 // simplification=none works better for SMT LIB benchmarks with
1584 // quantifiers, not others options::simplificationMode.set(qf_sat ||
1585 // quantifiers ? SIMPLIFICATION_MODE_NONE : SIMPLIFICATION_MODE_BATCH);
1586 options::simplificationMode
.set(qf_sat
? SIMPLIFICATION_MODE_NONE
1587 : SIMPLIFICATION_MODE_BATCH
);
1591 if (options::cbqiBv() && d_logic
.isQuantified())
1593 if(options::boolToBitvector
.wasSetByUser()) {
1594 throw OptionException(
1595 "bool-to-bv not supported with CBQI BV for quantified logics");
1597 Notice() << "SmtEngine: turning off bool-to-bitvector to support CBQI BV"
1599 options::boolToBitvector
.set(false);
1602 // cases where we need produce models
1603 if (!options::produceModels()
1604 && (options::produceAssignments() || options::sygusRewSynthCheck()
1607 Notice() << "SmtEngine: turning on produce-models" << endl
;
1608 setOption("produce-models", SExpr("true"));
1611 // Set the options for the theoryOf
1612 if(!options::theoryOfMode
.wasSetByUser()) {
1613 if(d_logic
.isSharingEnabled() &&
1614 !d_logic
.isTheoryEnabled(THEORY_BV
) &&
1615 !d_logic
.isTheoryEnabled(THEORY_STRINGS
) &&
1616 !d_logic
.isTheoryEnabled(THEORY_SETS
) ) {
1617 Trace("smt") << "setting theoryof-mode to term-based" << endl
;
1618 options::theoryOfMode
.set(THEORY_OF_TERM_BASED
);
1622 // strings require LIA, UF; widen the logic
1623 if(d_logic
.isTheoryEnabled(THEORY_STRINGS
)) {
1624 LogicInfo
log(d_logic
.getUnlockedCopy());
1625 // Strings requires arith for length constraints, and also UF
1626 if(!d_logic
.isTheoryEnabled(THEORY_UF
)) {
1627 Trace("smt") << "because strings are enabled, also enabling UF" << endl
;
1628 log
.enableTheory(THEORY_UF
);
1630 if(!d_logic
.isTheoryEnabled(THEORY_ARITH
) || d_logic
.isDifferenceLogic() || !d_logic
.areIntegersUsed()) {
1631 Trace("smt") << "because strings are enabled, also enabling linear integer arithmetic" << endl
;
1632 log
.enableTheory(THEORY_ARITH
);
1633 log
.enableIntegers();
1634 log
.arithOnlyLinear();
1639 if(d_logic
.isTheoryEnabled(THEORY_ARRAYS
) || d_logic
.isTheoryEnabled(THEORY_DATATYPES
) || d_logic
.isTheoryEnabled(THEORY_SETS
)) {
1640 if(!d_logic
.isTheoryEnabled(THEORY_UF
)) {
1641 LogicInfo
log(d_logic
.getUnlockedCopy());
1642 Trace("smt") << "because a theory that permits Boolean terms is enabled, also enabling UF" << endl
;
1643 log
.enableTheory(THEORY_UF
);
1649 // by default, symmetry breaker is on only for non-incremental QF_UF
1650 if(! options::ufSymmetryBreaker
.wasSetByUser()) {
1651 bool qf_uf_noinc
= d_logic
.isPure(THEORY_UF
) && !d_logic
.isQuantified()
1652 && !options::incrementalSolving() && !options::proof()
1653 && !options::unsatCores();
1654 Trace("smt") << "setting uf symmetry breaker to " << qf_uf_noinc
<< endl
;
1655 options::ufSymmetryBreaker
.set(qf_uf_noinc
);
1658 // If in arrays, set the UF handler to arrays
1659 if(d_logic
.isTheoryEnabled(THEORY_ARRAYS
) && ( !d_logic
.isQuantified() ||
1660 (d_logic
.isQuantified() && !d_logic
.isTheoryEnabled(THEORY_UF
)))) {
1661 Theory::setUninterpretedSortOwner(THEORY_ARRAYS
);
1663 Theory::setUninterpretedSortOwner(THEORY_UF
);
1666 // Turn on ite simplification for QF_LIA and QF_AUFBV
1667 // WARNING: These checks match much more than just QF_AUFBV and
1668 // QF_LIA logics. --K [2014/10/15]
1669 if(! options::doITESimp
.wasSetByUser()) {
1670 bool qf_aufbv
= !d_logic
.isQuantified() &&
1671 d_logic
.isTheoryEnabled(THEORY_ARRAYS
) &&
1672 d_logic
.isTheoryEnabled(THEORY_UF
) &&
1673 d_logic
.isTheoryEnabled(THEORY_BV
);
1674 bool qf_lia
= !d_logic
.isQuantified() &&
1675 d_logic
.isPure(THEORY_ARITH
) &&
1676 d_logic
.isLinear() &&
1677 !d_logic
.isDifferenceLogic() &&
1678 !d_logic
.areRealsUsed();
1680 bool iteSimp
= (qf_aufbv
|| qf_lia
);
1681 Trace("smt") << "setting ite simplification to " << iteSimp
<< endl
;
1682 options::doITESimp
.set(iteSimp
);
1684 if(! options::compressItes
.wasSetByUser() ){
1685 bool qf_lia
= !d_logic
.isQuantified() &&
1686 d_logic
.isPure(THEORY_ARITH
) &&
1687 d_logic
.isLinear() &&
1688 !d_logic
.isDifferenceLogic() &&
1689 !d_logic
.areRealsUsed();
1691 bool compressIte
= qf_lia
;
1692 Trace("smt") << "setting ite compression to " << compressIte
<< endl
;
1693 options::compressItes
.set(compressIte
);
1695 if(! options::simplifyWithCareEnabled
.wasSetByUser() ){
1696 bool qf_aufbv
= !d_logic
.isQuantified() &&
1697 d_logic
.isTheoryEnabled(THEORY_ARRAYS
) &&
1698 d_logic
.isTheoryEnabled(THEORY_UF
) &&
1699 d_logic
.isTheoryEnabled(THEORY_BV
);
1701 bool withCare
= qf_aufbv
;
1702 Trace("smt") << "setting ite simplify with care to " << withCare
<< endl
;
1703 options::simplifyWithCareEnabled
.set(withCare
);
1705 // Turn off array eager index splitting for QF_AUFLIA
1706 if(! options::arraysEagerIndexSplitting
.wasSetByUser()) {
1707 if (not d_logic
.isQuantified() &&
1708 d_logic
.isTheoryEnabled(THEORY_ARRAYS
) &&
1709 d_logic
.isTheoryEnabled(THEORY_UF
) &&
1710 d_logic
.isTheoryEnabled(THEORY_ARITH
)) {
1711 Trace("smt") << "setting array eager index splitting to false" << endl
;
1712 options::arraysEagerIndexSplitting
.set(false);
1715 // Turn on model-based arrays for QF_AX (unless models are enabled)
1716 // if(! options::arraysModelBased.wasSetByUser()) {
1717 // if (not d_logic.isQuantified() &&
1718 // d_logic.isTheoryEnabled(THEORY_ARRAYS) &&
1719 // d_logic.isPure(THEORY_ARRAYS) &&
1720 // !options::produceModels() &&
1721 // !options::checkModels()) {
1722 // Trace("smt") << "turning on model-based array solver" << endl;
1723 // options::arraysModelBased.set(true);
1726 // Turn on multiple-pass non-clausal simplification for QF_AUFBV
1727 if(! options::repeatSimp
.wasSetByUser()) {
1728 bool repeatSimp
= !d_logic
.isQuantified() &&
1729 (d_logic
.isTheoryEnabled(THEORY_ARRAYS
) &&
1730 d_logic
.isTheoryEnabled(THEORY_UF
) &&
1731 d_logic
.isTheoryEnabled(THEORY_BV
)) &&
1732 !options::unsatCores();
1733 Trace("smt") << "setting repeat simplification to " << repeatSimp
<< endl
;
1734 options::repeatSimp
.set(repeatSimp
);
1736 // Unconstrained simp currently does *not* support model generation
1737 if (options::unconstrainedSimp
.wasSetByUser() && options::unconstrainedSimp()) {
1738 if (options::produceModels()) {
1739 if (options::produceModels
.wasSetByUser()) {
1740 throw OptionException("Cannot use unconstrained-simp with model generation.");
1742 Notice() << "SmtEngine: turning off produce-models to support unconstrainedSimp" << endl
;
1743 setOption("produce-models", SExpr("false"));
1745 if (options::produceAssignments()) {
1746 if (options::produceAssignments
.wasSetByUser()) {
1747 throw OptionException("Cannot use unconstrained-simp with model generation (produce-assignments).");
1749 Notice() << "SmtEngine: turning off produce-assignments to support unconstrainedSimp" << endl
;
1750 setOption("produce-assignments", SExpr("false"));
1752 if (options::checkModels()) {
1753 if (options::checkModels
.wasSetByUser()) {
1754 throw OptionException("Cannot use unconstrained-simp with model generation (check-models).");
1756 Notice() << "SmtEngine: turning off check-models to support unconstrainedSimp" << endl
;
1757 setOption("check-models", SExpr("false"));
1761 if (! options::bvEagerExplanations
.wasSetByUser() &&
1762 d_logic
.isTheoryEnabled(THEORY_ARRAYS
) &&
1763 d_logic
.isTheoryEnabled(THEORY_BV
)) {
1764 Trace("smt") << "enabling eager bit-vector explanations " << endl
;
1765 options::bvEagerExplanations
.set(true);
1768 // Turn on arith rewrite equalities only for pure arithmetic
1769 if(! options::arithRewriteEq
.wasSetByUser()) {
1770 bool arithRewriteEq
= d_logic
.isPure(THEORY_ARITH
) && d_logic
.isLinear() && !d_logic
.isQuantified();
1771 Trace("smt") << "setting arith rewrite equalities " << arithRewriteEq
<< endl
;
1772 options::arithRewriteEq
.set(arithRewriteEq
);
1774 if(! options::arithHeuristicPivots
.wasSetByUser()) {
1775 int16_t heuristicPivots
= 5;
1776 if(d_logic
.isPure(THEORY_ARITH
) && !d_logic
.isQuantified()) {
1777 if(d_logic
.isDifferenceLogic()) {
1778 heuristicPivots
= -1;
1779 } else if(!d_logic
.areIntegersUsed()) {
1780 heuristicPivots
= 0;
1783 Trace("smt") << "setting arithHeuristicPivots " << heuristicPivots
<< endl
;
1784 options::arithHeuristicPivots
.set(heuristicPivots
);
1786 if(! options::arithPivotThreshold
.wasSetByUser()){
1787 uint16_t pivotThreshold
= 2;
1788 if(d_logic
.isPure(THEORY_ARITH
) && !d_logic
.isQuantified()){
1789 if(d_logic
.isDifferenceLogic()){
1790 pivotThreshold
= 16;
1793 Trace("smt") << "setting arith arithPivotThreshold " << pivotThreshold
<< endl
;
1794 options::arithPivotThreshold
.set(pivotThreshold
);
1796 if(! options::arithStandardCheckVarOrderPivots
.wasSetByUser()){
1797 int16_t varOrderPivots
= -1;
1798 if(d_logic
.isPure(THEORY_ARITH
) && !d_logic
.isQuantified()){
1799 varOrderPivots
= 200;
1801 Trace("smt") << "setting arithStandardCheckVarOrderPivots " << varOrderPivots
<< endl
;
1802 options::arithStandardCheckVarOrderPivots
.set(varOrderPivots
);
1804 // Turn off early theory preprocessing if arithRewriteEq is on
1805 if (options::arithRewriteEq()) {
1806 d_earlyTheoryPP
= false;
1808 if (d_logic
.isPure(THEORY_ARITH
) && !d_logic
.areRealsUsed())
1810 if (!options::nlExtTangentPlanesInterleave
.wasSetByUser())
1812 Trace("smt") << "setting nlExtTangentPlanesInterleave to true" << endl
;
1813 options::nlExtTangentPlanesInterleave
.set(true);
1817 // Set decision mode based on logic (if not set by user)
1818 if(!options::decisionMode
.wasSetByUser()) {
1819 decision::DecisionMode decMode
=
1821 d_logic
.hasEverything() ? decision::DECISION_STRATEGY_JUSTIFICATION
:
1823 (not d_logic
.isQuantified() &&
1824 d_logic
.isPure(THEORY_BV
)
1826 // QF_AUFBV or QF_ABV or QF_UFBV
1827 (not d_logic
.isQuantified() &&
1828 (d_logic
.isTheoryEnabled(THEORY_ARRAYS
) ||
1829 d_logic
.isTheoryEnabled(THEORY_UF
)) &&
1830 d_logic
.isTheoryEnabled(THEORY_BV
)
1832 // QF_AUFLIA (and may be ends up enabling QF_AUFLRA?)
1833 (not d_logic
.isQuantified() &&
1834 d_logic
.isTheoryEnabled(THEORY_ARRAYS
) &&
1835 d_logic
.isTheoryEnabled(THEORY_UF
) &&
1836 d_logic
.isTheoryEnabled(THEORY_ARITH
)
1839 (not d_logic
.isQuantified() &&
1840 d_logic
.isPure(THEORY_ARITH
) && d_logic
.isLinear() && !d_logic
.isDifferenceLogic() && !d_logic
.areIntegersUsed()
1843 d_logic
.isQuantified() ||
1845 d_logic
.isTheoryEnabled(THEORY_STRINGS
)
1846 ? decision::DECISION_STRATEGY_JUSTIFICATION
1847 : decision::DECISION_STRATEGY_INTERNAL
1852 d_logic
.hasEverything() || d_logic
.isTheoryEnabled(THEORY_STRINGS
) ? false :
1854 (not d_logic
.isQuantified() &&
1855 d_logic
.isTheoryEnabled(THEORY_ARRAYS
) &&
1856 d_logic
.isTheoryEnabled(THEORY_UF
) &&
1857 d_logic
.isTheoryEnabled(THEORY_ARITH
)
1860 (not d_logic
.isQuantified() &&
1861 d_logic
.isPure(THEORY_ARITH
) && d_logic
.isLinear() && !d_logic
.isDifferenceLogic() && !d_logic
.areIntegersUsed()
1866 Trace("smt") << "setting decision mode to " << decMode
<< endl
;
1867 options::decisionMode
.set(decMode
);
1868 options::decisionStopOnly
.set(stoponly
);
1870 if( options::incrementalSolving() ){
1871 //disable modes not supported by incremental
1872 options::sortInference
.set( false );
1873 options::ufssFairnessMonotone
.set( false );
1874 options::quantEpr
.set( false );
1875 options::globalNegate
.set(false);
1877 if( d_logic
.hasCardinalityConstraints() ){
1878 //must have finite model finding on
1879 options::finiteModelFind
.set( true );
1882 //if it contains a theory with non-termination, do not strictly enforce that quantifiers and theory combination must be interleaved
1883 if( d_logic
.isTheoryEnabled(THEORY_STRINGS
) || (d_logic
.isTheoryEnabled(THEORY_ARITH
) && !d_logic
.isLinear()) ){
1884 if( !options::instWhenStrictInterleave
.wasSetByUser() ){
1885 options::instWhenStrictInterleave
.set( false );
1889 //local theory extensions
1890 if( options::localTheoryExt() ){
1891 if( !options::instMaxLevel
.wasSetByUser() ){
1892 options::instMaxLevel
.set( 0 );
1895 if( options::instMaxLevel()!=-1 ){
1896 Notice() << "SmtEngine: turning off cbqi to support instMaxLevel" << endl
;
1897 options::cbqi
.set(false);
1899 //track instantiations?
1900 if( options::cbqiNestedQE() || ( options::proof() && !options::trackInstLemmas
.wasSetByUser() ) ){
1901 options::trackInstLemmas
.set( true );
1904 if( ( options::fmfBoundLazy
.wasSetByUser() && options::fmfBoundLazy() ) ||
1905 ( options::fmfBoundInt
.wasSetByUser() && options::fmfBoundInt() ) ) {
1906 options::fmfBound
.set( true );
1908 //now have determined whether fmfBoundInt is on/off
1909 //apply fmfBoundInt options
1910 if( options::fmfBound() ){
1911 //must have finite model finding on
1912 options::finiteModelFind
.set( true );
1913 if (!options::mbqiMode
.wasSetByUser()
1914 || (options::mbqiMode() != quantifiers::MBQI_NONE
1915 && options::mbqiMode() != quantifiers::MBQI_FMC
))
1917 //if bounded integers are set, use no MBQI by default
1918 options::mbqiMode
.set( quantifiers::MBQI_NONE
);
1920 if( ! options::prenexQuant
.wasSetByUser() ){
1921 options::prenexQuant
.set( quantifiers::PRENEX_QUANT_NONE
);
1924 if( options::ufHo() ){
1925 //if higher-order, then current variants of model-based instantiation cannot be used
1926 if( options::mbqiMode()!=quantifiers::MBQI_NONE
){
1927 options::mbqiMode
.set( quantifiers::MBQI_NONE
);
1930 if( options::mbqiMode()==quantifiers::MBQI_ABS
){
1931 if( !d_logic
.isPure(THEORY_UF
) ){
1932 //MBQI_ABS is only supported in pure quantified UF
1933 options::mbqiMode
.set( quantifiers::MBQI_FMC
);
1936 if( options::fmfFunWellDefinedRelevant() ){
1937 if( !options::fmfFunWellDefined
.wasSetByUser() ){
1938 options::fmfFunWellDefined
.set( true );
1941 if( options::fmfFunWellDefined() ){
1942 if( !options::finiteModelFind
.wasSetByUser() ){
1943 options::finiteModelFind
.set( true );
1947 if( options::quantEpr() ){
1948 if( !options::preSkolemQuant
.wasSetByUser() ){
1949 options::preSkolemQuant
.set( true );
1953 //now, have determined whether finite model find is on/off
1954 //apply finite model finding options
1955 if( options::finiteModelFind() ){
1956 //apply conservative quantifiers splitting
1957 if( !options::quantDynamicSplit
.wasSetByUser() ){
1958 options::quantDynamicSplit
.set( quantifiers::QUANT_DSPLIT_MODE_DEFAULT
);
1960 //do not eliminate extended arithmetic symbols from quantified formulas
1961 if( !options::elimExtArithQuant
.wasSetByUser() ){
1962 options::elimExtArithQuant
.set( false );
1964 if( !options::eMatching
.wasSetByUser() ){
1965 options::eMatching
.set( options::fmfInstEngine() );
1967 if( !options::instWhenMode
.wasSetByUser() ){
1968 //instantiate only on last call
1969 if( options::eMatching() ){
1970 options::instWhenMode
.set( quantifiers::INST_WHEN_LAST_CALL
);
1973 if( options::mbqiMode()==quantifiers::MBQI_ABS
){
1974 if( !options::preSkolemQuant
.wasSetByUser() ){
1975 options::preSkolemQuant
.set( true );
1977 if( !options::preSkolemQuantNested
.wasSetByUser() ){
1978 options::preSkolemQuantNested
.set( true );
1980 if( !options::fmfOneInstPerRound
.wasSetByUser() ){
1981 options::fmfOneInstPerRound
.set( true );
1986 //apply counterexample guided instantiation options
1987 // if we are attempting to rewrite everything to SyGuS, use ceGuidedInst
1988 if (options::sygusInference())
1990 if (!options::ceGuidedInst
.wasSetByUser())
1992 options::ceGuidedInst
.set(true);
1994 // optimization: apply preskolemization, makes it succeed more often
1995 if (!options::preSkolemQuant
.wasSetByUser())
1997 options::preSkolemQuant
.set(true);
1999 if (!options::preSkolemQuantNested
.wasSetByUser())
2001 options::preSkolemQuantNested
.set(true);
2004 if( options::cegqiSingleInvMode()!=quantifiers::CEGQI_SI_MODE_NONE
){
2005 if( !options::ceGuidedInst
.wasSetByUser() ){
2006 options::ceGuidedInst
.set( true );
2009 if( options::ceGuidedInst() ){
2010 //counterexample-guided instantiation for sygus
2011 if( !options::cegqiSingleInvMode
.wasSetByUser() ){
2012 options::cegqiSingleInvMode
.set( quantifiers::CEGQI_SI_MODE_USE
);
2014 if( !options::quantConflictFind
.wasSetByUser() ){
2015 options::quantConflictFind
.set( false );
2017 if( !options::instNoEntail
.wasSetByUser() ){
2018 options::instNoEntail
.set( false );
2020 if (options::sygusRew())
2022 options::sygusRewSynth
.set(true);
2023 options::sygusRewVerify
.set(true);
2025 if (options::sygusRewSynth() || options::sygusRewVerify())
2027 // rewrite rule synthesis implies that sygus stream must be true
2028 options::sygusStream
.set(true);
2030 if (options::sygusStream())
2032 // PBE and streaming modes are incompatible
2033 if (!options::sygusSymBreakPbe
.wasSetByUser())
2035 options::sygusSymBreakPbe
.set(false);
2037 if (!options::sygusUnifPbe
.wasSetByUser())
2039 options::sygusUnifPbe
.set(false);
2042 //do not allow partial functions
2043 if( !options::bitvectorDivByZeroConst
.wasSetByUser() ){
2044 options::bitvectorDivByZeroConst
.set( true );
2046 if( !options::dtRewriteErrorSel
.wasSetByUser() ){
2047 options::dtRewriteErrorSel
.set( true );
2050 if( !options::miniscopeQuant
.wasSetByUser() ){
2051 options::miniscopeQuant
.set( false );
2053 if( !options::miniscopeQuantFreeVar
.wasSetByUser() ){
2054 options::miniscopeQuantFreeVar
.set( false );
2057 if( !options::rewriteDivk
.wasSetByUser()) {
2058 options::rewriteDivk
.set( true );
2061 if( !options::macrosQuant
.wasSetByUser()) {
2062 options::macrosQuant
.set( false );
2064 if( !options::cbqiPreRegInst
.wasSetByUser()) {
2065 options::cbqiPreRegInst
.set( true );
2068 //counterexample-guided instantiation for non-sygus
2069 // enable if any possible quantifiers with arithmetic, datatypes or bitvectors
2070 if (d_logic
.isQuantified()
2071 && ((options::decisionMode() != decision::DECISION_STRATEGY_INTERNAL
2072 && (d_logic
.isTheoryEnabled(THEORY_ARITH
)
2073 || d_logic
.isTheoryEnabled(THEORY_DATATYPES
)
2074 || d_logic
.isTheoryEnabled(THEORY_BV
)
2075 || d_logic
.isTheoryEnabled(THEORY_FP
)))
2076 || d_logic
.isPure(THEORY_ARITH
) || d_logic
.isPure(THEORY_BV
)
2077 || options::cbqiAll()))
2079 if( !options::cbqi
.wasSetByUser() ){
2080 options::cbqi
.set( true );
2082 // check whether we should apply full cbqi
2083 if (d_logic
.isPure(THEORY_BV
))
2085 if (!options::cbqiFullEffort
.wasSetByUser())
2087 options::cbqiFullEffort
.set(true);
2091 if( options::cbqi() ){
2093 if( !options::rewriteDivk
.wasSetByUser()) {
2094 options::rewriteDivk
.set( true );
2096 if (options::incrementalSolving())
2098 // cannot do nested quantifier elimination in incremental mode
2099 options::cbqiNestedQE
.set(false);
2101 if (d_logic
.isPure(THEORY_ARITH
) || d_logic
.isPure(THEORY_BV
))
2103 options::cbqiAll
.set( false );
2104 if( !options::quantConflictFind
.wasSetByUser() ){
2105 options::quantConflictFind
.set( false );
2107 if( !options::instNoEntail
.wasSetByUser() ){
2108 options::instNoEntail
.set( false );
2110 if( !options::instWhenMode
.wasSetByUser() && options::cbqiModel() ){
2111 //only instantiation should happen at last call when model is avaiable
2112 options::instWhenMode
.set( quantifiers::INST_WHEN_LAST_CALL
);
2115 // only supported in pure arithmetic or pure BV
2116 options::cbqiNestedQE
.set(false);
2119 if (options::cbqiNestedQE()
2120 || options::decisionMode() == decision::DECISION_STRATEGY_INTERNAL
)
2122 // only complete with prenex = disj_normal or normal
2123 if (options::prenexQuant() <= quantifiers::PRENEX_QUANT_DISJ_NORMAL
)
2125 options::prenexQuant
.set(quantifiers::PRENEX_QUANT_DISJ_NORMAL
);
2128 else if (options::globalNegate())
2130 if (!options::prenexQuant
.wasSetByUser())
2132 options::prenexQuant
.set(quantifiers::PRENEX_QUANT_NONE
);
2136 //implied options...
2137 if( options::strictTriggers() ){
2138 if( !options::userPatternsQuant
.wasSetByUser() ){
2139 options::userPatternsQuant
.set( quantifiers::USER_PAT_MODE_TRUST
);
2142 if( options::qcfMode
.wasSetByUser() || options::qcfTConstraint() ){
2143 options::quantConflictFind
.set( true );
2145 if( options::cbqiNestedQE() ){
2146 options::prenexQuantUser
.set( true );
2147 if( !options::preSkolemQuant
.wasSetByUser() ){
2148 options::preSkolemQuant
.set( true );
2151 //for induction techniques
2152 if( options::quantInduction() ){
2153 if( !options::dtStcInduction
.wasSetByUser() ){
2154 options::dtStcInduction
.set( true );
2156 if( !options::intWfInduction
.wasSetByUser() ){
2157 options::intWfInduction
.set( true );
2160 if( options::dtStcInduction() ){
2161 //try to remove ITEs from quantified formulas
2162 if( !options::iteDtTesterSplitQuant
.wasSetByUser() ){
2163 options::iteDtTesterSplitQuant
.set( true );
2165 if( !options::iteLiftQuant
.wasSetByUser() ){
2166 options::iteLiftQuant
.set( quantifiers::ITE_LIFT_QUANT_MODE_ALL
);
2169 if( options::intWfInduction() ){
2170 if( !options::purifyTriggers
.wasSetByUser() ){
2171 options::purifyTriggers
.set( true );
2174 if( options::conjectureNoFilter() ){
2175 if( !options::conjectureFilterActiveTerms
.wasSetByUser() ){
2176 options::conjectureFilterActiveTerms
.set( false );
2178 if( !options::conjectureFilterCanonical
.wasSetByUser() ){
2179 options::conjectureFilterCanonical
.set( false );
2181 if( !options::conjectureFilterModel
.wasSetByUser() ){
2182 options::conjectureFilterModel
.set( false );
2185 if( options::conjectureGenPerRound
.wasSetByUser() ){
2186 if( options::conjectureGenPerRound()>0 ){
2187 options::conjectureGen
.set( true );
2189 options::conjectureGen
.set( false );
2192 //can't pre-skolemize nested quantifiers without UF theory
2193 if( !d_logic
.isTheoryEnabled(THEORY_UF
) && options::preSkolemQuant() ){
2194 if( !options::preSkolemQuantNested
.wasSetByUser() ){
2195 options::preSkolemQuantNested
.set( false );
2198 if( !d_logic
.isTheoryEnabled(THEORY_DATATYPES
) ){
2199 options::quantDynamicSplit
.set( quantifiers::QUANT_DSPLIT_MODE_NONE
);
2202 //until bugs 371,431 are fixed
2203 if( ! options::minisatUseElim
.wasSetByUser()){
2204 // cannot use minisat elimination for logics where a theory solver
2205 // introduces new literals into the search. This includes quantifiers
2206 // (quantifier instantiation), and the lemma schemas used in non-linear
2207 // and sets. We also can't use it if models are enabled.
2208 if (d_logic
.isTheoryEnabled(THEORY_SETS
) || d_logic
.isQuantified()
2209 || options::produceModels() || options::produceAssignments()
2210 || options::checkModels()
2211 || (d_logic
.isTheoryEnabled(THEORY_ARITH
) && !d_logic
.isLinear()))
2213 options::minisatUseElim
.set( false );
2216 else if (options::minisatUseElim()) {
2217 if (options::produceModels()) {
2218 Notice() << "SmtEngine: turning off produce-models to support minisatUseElim" << endl
;
2219 setOption("produce-models", SExpr("false"));
2221 if (options::produceAssignments()) {
2222 Notice() << "SmtEngine: turning off produce-assignments to support minisatUseElim" << endl
;
2223 setOption("produce-assignments", SExpr("false"));
2225 if (options::checkModels()) {
2226 Notice() << "SmtEngine: turning off check-models to support minisatUseElim" << endl
;
2227 setOption("check-models", SExpr("false"));
2231 // For now, these array theory optimizations do not support model-building
2232 if (options::produceModels() || options::produceAssignments() || options::checkModels()) {
2233 options::arraysOptimizeLinear
.set(false);
2234 options::arraysLazyRIntro1
.set(false);
2237 // Non-linear arithmetic does not support models unless nlExt is enabled
2238 if ((d_logic
.isTheoryEnabled(THEORY_ARITH
) && !d_logic
.isLinear()
2239 && !options::nlExt())
2240 || options::globalNegate())
2242 std::string reason
=
2243 options::globalNegate() ? "--global-negate" : "nonlinear arithmetic";
2244 if (options::produceModels()) {
2245 if(options::produceModels
.wasSetByUser()) {
2246 throw OptionException(
2247 std::string("produce-model not supported with " + reason
));
2250 << "SmtEngine: turning off produce-models because unsupported for "
2252 setOption("produce-models", SExpr("false"));
2254 if (options::produceAssignments()) {
2255 if(options::produceAssignments
.wasSetByUser()) {
2256 throw OptionException(
2257 std::string("produce-assignments not supported with " + reason
));
2259 Warning() << "SmtEngine: turning off produce-assignments because "
2262 setOption("produce-assignments", SExpr("false"));
2264 if (options::checkModels()) {
2265 if(options::checkModels
.wasSetByUser()) {
2266 throw OptionException(
2267 std::string("check-models not supported with " + reason
));
2270 << "SmtEngine: turning off check-models because unsupported for "
2272 setOption("check-models", SExpr("false"));
2276 if(options::incrementalSolving() && options::proof()) {
2277 Warning() << "SmtEngine: turning off incremental solving mode (not yet supported with --proof, try --tear-down-incremental instead)" << endl
;
2278 setOption("incremental", SExpr("false"));
2281 if (options::proof())
2283 if (options::bitvectorAlgebraicSolver())
2285 if (options::bitvectorAlgebraicSolver
.wasSetByUser())
2287 throw OptionException(
2288 "--bv-algebraic-solver is not supported with proofs");
2290 Notice() << "SmtEngine: turning off bv algebraic solver to support proofs"
2292 options::bitvectorAlgebraicSolver
.set(false);
2294 if (options::bitvectorEqualitySolver())
2296 if (options::bitvectorEqualitySolver
.wasSetByUser())
2298 throw OptionException("--bv-eq-solver is not supported with proofs");
2300 Notice() << "SmtEngine: turning off bv eq solver to support proofs"
2302 options::bitvectorEqualitySolver
.set(false);
2304 if (options::bitvectorInequalitySolver())
2306 if (options::bitvectorInequalitySolver
.wasSetByUser())
2308 throw OptionException(
2309 "--bv-inequality-solver is not supported with proofs");
2311 Notice() << "SmtEngine: turning off bv ineq solver to support proofs"
2313 options::bitvectorInequalitySolver
.set(false);
2317 if (!options::bitvectorEqualitySolver())
2319 if (options::bvLazyRewriteExtf())
2321 if (options::bvLazyRewriteExtf
.wasSetByUser())
2323 throw OptionException(
2324 "--bv-lazy-rewrite-extf requires --bv-eq-solver to be set");
2328 << "disabling bvLazyRewriteExtf since equality solver is disabled"
2330 options::bvLazyRewriteExtf
.set(false);
2334 void SmtEngine::setProblemExtended(bool value
)
2336 d_problemExtended
= value
;
2337 if (value
) { d_assumptions
.clear(); }
2340 void SmtEngine::setInfo(const std::string
& key
, const CVC4::SExpr
& value
)
2342 SmtScope
smts(this);
2344 Trace("smt") << "SMT setInfo(" << key
<< ", " << value
<< ")" << endl
;
2346 if(Dump
.isOn("benchmark")) {
2347 if(key
== "status") {
2348 string s
= value
.getValue();
2349 BenchmarkStatus status
=
2350 (s
== "sat") ? SMT_SATISFIABLE
:
2351 ((s
== "unsat") ? SMT_UNSATISFIABLE
: SMT_UNKNOWN
);
2352 Dump("benchmark") << SetBenchmarkStatusCommand(status
);
2354 Dump("benchmark") << SetInfoCommand(key
, value
);
2358 // Check for CVC4-specific info keys (prefixed with "cvc4-" or "cvc4_")
2359 if(key
.length() > 5) {
2360 string prefix
= key
.substr(0, 5);
2361 if(prefix
== "cvc4-" || prefix
== "cvc4_") {
2362 string cvc4key
= key
.substr(5);
2363 if(cvc4key
== "logic") {
2364 if(! value
.isAtom()) {
2365 throw OptionException("argument to (set-info :cvc4-logic ..) must be a string");
2367 SmtScope
smts(this);
2368 d_logic
= value
.getValue();
2372 throw UnrecognizedOptionException();
2377 // Check for standard info keys (SMT-LIB v1, SMT-LIB v2, ...)
2379 || key
== "category"
2380 || key
== "difficulty"
2382 || key
== "license")
2386 } else if(key
== "name") {
2387 d_filename
= value
.getValue();
2390 else if (key
== "smt-lib-version" && !options::inputLanguage
.wasSetByUser())
2392 language::input::Language ilang
= language::input::LANG_AUTO
;
2393 if( (value
.isInteger() && value
.getIntegerValue() == Integer(2)) ||
2394 (value
.isRational() && value
.getRationalValue() == Rational(2)) ||
2395 value
.getValue() == "2" ||
2396 value
.getValue() == "2.0" ) {
2397 ilang
= language::input::LANG_SMTLIB_V2_0
;
2398 } else if( (value
.isRational() && value
.getRationalValue() == Rational(5, 2)) ||
2399 value
.getValue() == "2.5" ) {
2400 ilang
= language::input::LANG_SMTLIB_V2_5
;
2401 } else if( (value
.isRational() && value
.getRationalValue() == Rational(13, 5)) ||
2402 value
.getValue() == "2.6" ) {
2403 ilang
= language::input::LANG_SMTLIB_V2_6
;
2405 else if (value
.getValue() == "2.6.1")
2407 ilang
= language::input::LANG_SMTLIB_V2_6_1
;
2411 Warning() << "Warning: unsupported smt-lib-version: " << value
<< endl
;
2412 throw UnrecognizedOptionException();
2414 options::inputLanguage
.set(ilang
);
2415 // also update the output language
2416 if (!options::outputLanguage
.wasSetByUser())
2418 language::output::Language olang
= language::toOutputLanguage(ilang
);
2419 if (options::outputLanguage() != olang
)
2421 options::outputLanguage
.set(olang
);
2422 *options::out() << language::SetLanguage(olang
);
2426 } else if(key
== "status") {
2428 if(value
.isAtom()) {
2429 s
= value
.getValue();
2431 if(s
!= "sat" && s
!= "unsat" && s
!= "unknown") {
2432 throw OptionException("argument to (set-info :status ..) must be "
2433 "`sat' or `unsat' or `unknown'");
2435 d_status
= Result(s
, d_filename
);
2438 throw UnrecognizedOptionException();
2441 CVC4::SExpr
SmtEngine::getInfo(const std::string
& key
) const {
2443 SmtScope
smts(this);
2445 Trace("smt") << "SMT getInfo(" << key
<< ")" << endl
;
2446 if(key
== "all-statistics") {
2447 vector
<SExpr
> stats
;
2448 for(StatisticsRegistry::const_iterator i
= NodeManager::fromExprManager(d_exprManager
)->getStatisticsRegistry()->begin();
2449 i
!= NodeManager::fromExprManager(d_exprManager
)->getStatisticsRegistry()->end();
2452 v
.push_back((*i
).first
);
2453 v
.push_back((*i
).second
);
2456 for(StatisticsRegistry::const_iterator i
= d_statisticsRegistry
->begin();
2457 i
!= d_statisticsRegistry
->end();
2460 v
.push_back((*i
).first
);
2461 v
.push_back((*i
).second
);
2464 return SExpr(stats
);
2465 } else if(key
== "error-behavior") {
2466 // immediate-exit | continued-execution
2467 if( options::continuedExecution() || options::interactive() ) {
2468 return SExpr(SExpr::Keyword("continued-execution"));
2470 return SExpr(SExpr::Keyword("immediate-exit"));
2472 } else if(key
== "name") {
2473 return SExpr(Configuration::getName());
2474 } else if(key
== "version") {
2475 return SExpr(Configuration::getVersionString());
2476 } else if(key
== "authors") {
2477 return SExpr(Configuration::about());
2478 } else if(key
== "status") {
2479 // sat | unsat | unknown
2480 switch(d_status
.asSatisfiabilityResult().isSat()) {
2482 return SExpr(SExpr::Keyword("sat"));
2484 return SExpr(SExpr::Keyword("unsat"));
2486 return SExpr(SExpr::Keyword("unknown"));
2488 } else if(key
== "reason-unknown") {
2489 if(!d_status
.isNull() && d_status
.isUnknown()) {
2491 ss
<< d_status
.whyUnknown();
2492 string s
= ss
.str();
2493 transform(s
.begin(), s
.end(), s
.begin(), ::tolower
);
2494 return SExpr(SExpr::Keyword(s
));
2496 throw ModalException("Can't get-info :reason-unknown when the "
2497 "last result wasn't unknown!");
2499 } else if(key
== "assertion-stack-levels") {
2500 AlwaysAssert(d_userLevels
.size() <=
2501 std::numeric_limits
<unsigned long int>::max());
2502 return SExpr(static_cast<unsigned long int>(d_userLevels
.size()));
2503 } else if(key
== "all-options") {
2504 // get the options, like all-statistics
2505 std::vector
< std::vector
<std::string
> > current_options
=
2506 Options::current()->getOptions();
2507 return SExpr::parseListOfListOfAtoms(current_options
);
2509 throw UnrecognizedOptionException();
2513 void SmtEngine::debugCheckFormals(const std::vector
<Expr
>& formals
, Expr func
)
2515 for(std::vector
<Expr
>::const_iterator i
= formals
.begin(); i
!= formals
.end(); ++i
) {
2516 if((*i
).getKind() != kind::BOUND_VARIABLE
) {
2518 ss
<< "All formal arguments to defined functions must be BOUND_VARIABLEs, but in the\n"
2519 << "definition of function " << func
<< ", formal\n"
2520 << " " << *i
<< "\n"
2521 << "has kind " << (*i
).getKind();
2522 throw TypeCheckingException(func
, ss
.str());
2527 void SmtEngine::debugCheckFunctionBody(Expr formula
,
2528 const std::vector
<Expr
>& formals
,
2531 Type formulaType
= formula
.getType(options::typeChecking());
2532 Type funcType
= func
.getType();
2533 // We distinguish here between definitions of constants and functions,
2534 // because the type checking for them is subtly different. Perhaps we
2535 // should instead have SmtEngine::defineFunction() and
2536 // SmtEngine::defineConstant() for better clarity, although then that
2537 // doesn't match the SMT-LIBv2 standard...
2538 if(formals
.size() > 0) {
2539 Type rangeType
= FunctionType(funcType
).getRangeType();
2540 if(! formulaType
.isComparableTo(rangeType
)) {
2542 ss
<< "Type of defined function does not match its declaration\n"
2543 << "The function : " << func
<< "\n"
2544 << "Declared type : " << rangeType
<< "\n"
2545 << "The body : " << formula
<< "\n"
2546 << "Body type : " << formulaType
;
2547 throw TypeCheckingException(func
, ss
.str());
2550 if(! formulaType
.isComparableTo(funcType
)) {
2552 ss
<< "Declared type of defined constant does not match its definition\n"
2553 << "The constant : " << func
<< "\n"
2554 << "Declared type : " << funcType
<< " " << Type::getTypeNode(funcType
)->getId() << "\n"
2555 << "The definition : " << formula
<< "\n"
2556 << "Definition type: " << formulaType
<< " " << Type::getTypeNode(formulaType
)->getId();
2557 throw TypeCheckingException(func
, ss
.str());
2562 void SmtEngine::defineFunction(Expr func
,
2563 const std::vector
<Expr
>& formals
,
2566 SmtScope
smts(this);
2568 Trace("smt") << "SMT defineFunction(" << func
<< ")" << endl
;
2569 debugCheckFormals(formals
, func
);
2572 ss
<< language::SetLanguage(
2573 language::SetLanguage::getLanguage(Dump
.getStream()))
2575 DefineFunctionCommand
c(ss
.str(), func
, formals
, formula
);
2576 addToModelCommandAndDump(
2577 c
, ExprManager::VAR_FLAG_DEFINED
, true, "declarations");
2579 PROOF(if (options::checkUnsatCores()) {
2580 d_defineCommands
.push_back(c
.clone());
2584 debugCheckFunctionBody(formula
, formals
, func
);
2586 // Substitute out any abstract values in formula
2588 d_private
->substituteAbstractValues(Node::fromExpr(formula
)).toExpr();
2590 TNode funcNode
= func
.getTNode();
2591 vector
<Node
> formalsNodes
;
2592 for(vector
<Expr
>::const_iterator i
= formals
.begin(),
2593 iend
= formals
.end();
2596 formalsNodes
.push_back((*i
).getNode());
2598 TNode formNode
= form
.getTNode();
2599 DefinedFunction
def(funcNode
, formalsNodes
, formNode
);
2600 // Permit (check-sat) (define-fun ...) (get-value ...) sequences.
2601 // Otherwise, (check-sat) (get-value ((! foo :named bar))) breaks
2602 // d_haveAdditions = true;
2603 Debug("smt") << "definedFunctions insert " << funcNode
<< " " << formNode
<< endl
;
2604 d_definedFunctions
->insert(funcNode
, def
);
2607 void SmtEngine::defineFunctionsRec(
2608 const std::vector
<Expr
>& funcs
,
2609 const std::vector
<std::vector
<Expr
> >& formals
,
2610 const std::vector
<Expr
>& formulas
)
2612 SmtScope
smts(this);
2613 finalOptionsAreSet();
2615 Trace("smt") << "SMT defineFunctionsRec(...)" << endl
;
2617 if (funcs
.size() != formals
.size() && funcs
.size() != formulas
.size())
2620 ss
<< "Number of functions, formals, and function bodies passed to "
2621 "defineFunctionsRec do not match:"
2623 << " #functions : " << funcs
.size() << "\n"
2624 << " #arg lists : " << formals
.size() << "\n"
2625 << " #function bodies : " << formulas
.size() << "\n";
2626 throw ModalException(ss
.str());
2628 for (unsigned i
= 0, size
= funcs
.size(); i
< size
; i
++)
2630 // check formal argument list
2631 debugCheckFormals(formals
[i
], funcs
[i
]);
2633 debugCheckFunctionBody(formulas
[i
], formals
[i
], funcs
[i
]);
2636 if (Dump
.isOn("raw-benchmark"))
2638 Dump("raw-benchmark") << DefineFunctionRecCommand(funcs
, formals
, formulas
);
2641 ExprManager
* em
= getExprManager();
2642 for (unsigned i
= 0, size
= funcs
.size(); i
< size
; i
++)
2644 // we assert a quantified formula
2646 // make the function application
2647 if (formals
[i
].empty())
2649 // it has no arguments
2650 func_app
= funcs
[i
];
2654 std::vector
<Expr
> children
;
2655 children
.push_back(funcs
[i
]);
2656 children
.insert(children
.end(), formals
[i
].begin(), formals
[i
].end());
2657 func_app
= em
->mkExpr(kind::APPLY_UF
, children
);
2659 Expr lem
= em
->mkExpr(kind::EQUAL
, func_app
, formulas
[i
]);
2660 if (!formals
[i
].empty())
2662 // set the attribute to denote this is a function definition
2663 std::string
attr_name("fun-def");
2664 Expr aexpr
= em
->mkExpr(kind::INST_ATTRIBUTE
, func_app
);
2665 aexpr
= em
->mkExpr(kind::INST_PATTERN_LIST
, aexpr
);
2666 std::vector
<Expr
> expr_values
;
2667 std::string str_value
;
2668 setUserAttribute(attr_name
, func_app
, expr_values
, str_value
);
2669 // make the quantified formula
2670 Expr boundVars
= em
->mkExpr(kind::BOUND_VAR_LIST
, formals
[i
]);
2671 lem
= em
->mkExpr(kind::FORALL
, boundVars
, lem
, aexpr
);
2673 // assert the quantified formula
2674 // notice we don't call assertFormula directly, since this would
2675 // duplicate the output on raw-benchmark.
2676 Expr e
= d_private
->substituteAbstractValues(Node::fromExpr(lem
)).toExpr();
2677 if (d_assertionList
!= NULL
)
2679 d_assertionList
->push_back(e
);
2681 d_private
->addFormula(e
.getNode(), false);
2685 void SmtEngine::defineFunctionRec(Expr func
,
2686 const std::vector
<Expr
>& formals
,
2689 std::vector
<Expr
> funcs
;
2690 funcs
.push_back(func
);
2691 std::vector
<std::vector
<Expr
> > formals_multi
;
2692 formals_multi
.push_back(formals
);
2693 std::vector
<Expr
> formulas
;
2694 formulas
.push_back(formula
);
2695 defineFunctionsRec(funcs
, formals_multi
, formulas
);
2698 bool SmtEngine::isDefinedFunction( Expr func
){
2699 Node nf
= Node::fromExpr( func
);
2700 Debug("smt") << "isDefined function " << nf
<< "?" << std::endl
;
2701 return d_definedFunctions
->find(nf
) != d_definedFunctions
->end();
2704 void SmtEnginePrivate::finishInit()
2706 d_preprocessingPassContext
.reset(
2707 new PreprocessingPassContext(&d_smt
, d_resourceManager
));
2708 // TODO: register passes here (this will likely change when we add support for
2709 // actually assembling preprocessing pipelines).
2710 std::unique_ptr
<ApplySubsts
> applySubsts(
2711 new ApplySubsts(d_preprocessingPassContext
.get()));
2712 std::unique_ptr
<BoolToBV
> boolToBv(
2713 new BoolToBV(d_preprocessingPassContext
.get()));
2714 std::unique_ptr
<BvAbstraction
> bvAbstract(
2715 new BvAbstraction(d_preprocessingPassContext
.get()));
2716 std::unique_ptr
<BVAckermann
> bvAckermann(
2717 new BVAckermann(d_preprocessingPassContext
.get()));
2718 std::unique_ptr
<BVGauss
> bvGauss(
2719 new BVGauss(d_preprocessingPassContext
.get()));
2720 std::unique_ptr
<BvIntroPow2
> bvIntroPow2(
2721 new BvIntroPow2(d_preprocessingPassContext
.get()));
2722 std::unique_ptr
<BVToBool
> bvToBool(
2723 new BVToBool(d_preprocessingPassContext
.get()));
2724 std::unique_ptr
<IntToBV
> intToBV(
2725 new IntToBV(d_preprocessingPassContext
.get()));
2726 std::unique_ptr
<PseudoBooleanProcessor
> pbProc(
2727 new PseudoBooleanProcessor(d_preprocessingPassContext
.get()));
2728 std::unique_ptr
<RealToInt
> realToInt(
2729 new RealToInt(d_preprocessingPassContext
.get()));
2730 std::unique_ptr
<Rewrite
> rewrite(
2731 new Rewrite(d_preprocessingPassContext
.get()));
2732 std::unique_ptr
<StaticLearning
> staticLearning(
2733 new StaticLearning(d_preprocessingPassContext
.get()));
2734 std::unique_ptr
<SymBreakerPass
> sbProc(
2735 new SymBreakerPass(d_preprocessingPassContext
.get()));
2736 std::unique_ptr
<SynthRewRulesPass
> srrProc(
2737 new SynthRewRulesPass(d_preprocessingPassContext
.get()));
2738 std::unique_ptr
<SepSkolemEmp
> sepSkolemEmp(
2739 new SepSkolemEmp(d_preprocessingPassContext
.get()));
2740 d_preprocessingPassRegistry
.registerPass("apply-substs",
2741 std::move(applySubsts
));
2742 d_preprocessingPassRegistry
.registerPass("bool-to-bv", std::move(boolToBv
));
2743 d_preprocessingPassRegistry
.registerPass("bv-abstraction",
2744 std::move(bvAbstract
));
2745 d_preprocessingPassRegistry
.registerPass("bv-ackermann",
2746 std::move(bvAckermann
));
2747 d_preprocessingPassRegistry
.registerPass("bv-gauss", std::move(bvGauss
));
2748 d_preprocessingPassRegistry
.registerPass("bv-intro-pow2",
2749 std::move(bvIntroPow2
));
2750 d_preprocessingPassRegistry
.registerPass("bv-to-bool", std::move(bvToBool
));
2751 d_preprocessingPassRegistry
.registerPass("int-to-bv", std::move(intToBV
));
2752 d_preprocessingPassRegistry
.registerPass("pseudo-boolean-processor",
2754 d_preprocessingPassRegistry
.registerPass("real-to-int", std::move(realToInt
));
2755 d_preprocessingPassRegistry
.registerPass("rewrite", std::move(rewrite
));
2756 d_preprocessingPassRegistry
.registerPass("sep-skolem-emp",
2757 std::move(sepSkolemEmp
));
2758 d_preprocessingPassRegistry
.registerPass("static-learning",
2759 std::move(staticLearning
));
2760 d_preprocessingPassRegistry
.registerPass("sym-break", std::move(sbProc
));
2761 d_preprocessingPassRegistry
.registerPass("synth-rr", std::move(srrProc
));
2764 Node
SmtEnginePrivate::expandDefinitions(TNode n
, unordered_map
<Node
, Node
, NodeHashFunction
>& cache
, bool expandOnly
)
2766 stack
< triple
<Node
, Node
, bool> > worklist
;
2768 worklist
.push(make_triple(Node(n
), Node(n
), false));
2769 // The worklist is made of triples, each is input / original node then the output / rewritten node
2770 // and finally a flag tracking whether the children have been explored (i.e. if this is a downward
2774 spendResource(options::preprocessStep());
2775 n
= worklist
.top().first
; // n is the input / original
2776 Node node
= worklist
.top().second
; // node is the output / result
2777 bool childrenPushed
= worklist
.top().third
;
2780 // Working downwards
2781 if(!childrenPushed
) {
2782 Kind k
= n
.getKind();
2784 // we can short circuit (variable) leaves
2786 SmtEngine::DefinedFunctionMap::const_iterator i
= d_smt
.d_definedFunctions
->find(n
);
2787 if(i
!= d_smt
.d_definedFunctions
->end()) {
2788 // replacement must be closed
2789 if((*i
).second
.getFormals().size() > 0) {
2790 result
.push(d_smt
.d_nodeManager
->mkNode(kind::LAMBDA
, d_smt
.d_nodeManager
->mkNode(kind::BOUND_VAR_LIST
, (*i
).second
.getFormals()), (*i
).second
.getFormula()));
2793 // don't bother putting in the cache
2794 result
.push((*i
).second
.getFormula());
2797 // don't bother putting in the cache
2802 // maybe it's in the cache
2803 unordered_map
<Node
, Node
, NodeHashFunction
>::iterator cacheHit
= cache
.find(n
);
2804 if(cacheHit
!= cache
.end()) {
2805 TNode ret
= (*cacheHit
).second
;
2806 result
.push(ret
.isNull() ? n
: ret
);
2810 // otherwise expand it
2811 bool doExpand
= k
== kind::APPLY
;
2813 // options that assign substitutions to APPLY_UF
2814 if (options::macrosQuant() || options::sygusInference())
2816 //expand if we have inferred an operator corresponds to a defined function
2817 doExpand
= k
==kind::APPLY_UF
&& d_smt
.isDefinedFunction( n
.getOperator().toExpr() );
2821 vector
<Node
> formals
;
2823 if( n
.getOperator().getKind() == kind::LAMBDA
){
2824 TNode op
= n
.getOperator();
2826 for( unsigned i
=0; i
<op
[0].getNumChildren(); i
++ ){
2827 formals
.push_back( op
[0][i
] );
2831 // application of a user-defined symbol
2832 TNode func
= n
.getOperator();
2833 SmtEngine::DefinedFunctionMap::const_iterator i
= d_smt
.d_definedFunctions
->find(func
);
2834 if(i
== d_smt
.d_definedFunctions
->end()) {
2835 throw TypeCheckingException(n
.toExpr(), string("Undefined function: `") + func
.toString() + "'");
2837 DefinedFunction def
= (*i
).second
;
2838 formals
= def
.getFormals();
2840 if(Debug
.isOn("expand")) {
2841 Debug("expand") << "found: " << n
<< endl
;
2842 Debug("expand") << " func: " << func
<< endl
;
2843 string name
= func
.getAttribute(expr::VarNameAttr());
2844 Debug("expand") << " : \"" << name
<< "\"" << endl
;
2846 if(Debug
.isOn("expand")) {
2847 Debug("expand") << " defn: " << def
.getFunction() << endl
2849 if(formals
.size() > 0) {
2850 copy( formals
.begin(), formals
.end() - 1,
2851 ostream_iterator
<Node
>(Debug("expand"), ", ") );
2852 Debug("expand") << formals
.back();
2854 Debug("expand") << "]" << endl
2855 << " " << def
.getFunction().getType() << endl
2856 << " " << def
.getFormula() << endl
;
2859 fm
= def
.getFormula();
2862 Node instance
= fm
.substitute(formals
.begin(),
2865 n
.begin() + formals
.size());
2866 Debug("expand") << "made : " << instance
<< endl
;
2868 Node expanded
= expandDefinitions(instance
, cache
, expandOnly
);
2869 cache
[n
] = (n
== expanded
? Node::null() : expanded
);
2870 result
.push(expanded
);
2873 } else if(! expandOnly
) {
2874 // do not do any theory stuff if expandOnly is true
2876 theory::Theory
* t
= d_smt
.d_theoryEngine
->theoryOf(node
);
2879 LogicRequest
req(d_smt
);
2880 node
= t
->expandDefinition(req
, n
);
2883 // the partial functions can fall through, in which case we still
2884 // consider their children
2885 worklist
.push(make_triple(Node(n
), node
, true)); // Original and rewritten result
2887 for(size_t i
= 0; i
< node
.getNumChildren(); ++i
) {
2888 worklist
.push(make_triple(node
[i
], node
[i
], false)); // Rewrite the children of the result only
2893 // Reconstruct the node from it's (now rewritten) children on the stack
2895 Debug("expand") << "cons : " << node
<< endl
;
2896 if(node
.getNumChildren()>0) {
2897 //cout << "cons : " << node << endl;
2898 NodeBuilder
<> nb(node
.getKind());
2899 if(node
.getMetaKind() == kind::metakind::PARAMETERIZED
) {
2900 Debug("expand") << "op : " << node
.getOperator() << endl
;
2901 //cout << "op : " << node.getOperator() << endl;
2902 nb
<< node
.getOperator();
2904 for(size_t i
= 0; i
< node
.getNumChildren(); ++i
) {
2905 Assert(!result
.empty());
2906 Node expanded
= result
.top();
2908 //cout << "exchld : " << expanded << endl;
2909 Debug("expand") << "exchld : " << expanded
<< endl
;
2914 cache
[n
] = n
== node
? Node::null() : node
; // Only cache once all subterms are expanded
2917 } while(!worklist
.empty());
2919 AlwaysAssert(result
.size() == 1);
2921 return result
.top();
2924 typedef std::unordered_map
<Node
, Node
, NodeHashFunction
> NodeMap
;
2926 Node
SmtEnginePrivate::purifyNlTerms(TNode n
, NodeMap
& cache
, NodeMap
& bcache
, std::vector
< Node
>& var_eq
, bool beneathMult
) {
2928 NodeMap::iterator find
= bcache
.find(n
);
2929 if (find
!= bcache
.end()) {
2930 return (*find
).second
;
2933 NodeMap::iterator find
= cache
.find(n
);
2934 if (find
!= cache
.end()) {
2935 return (*find
).second
;
2939 if( n
.getNumChildren()>0 ){
2941 && (n
.getKind() == kind::PLUS
|| n
.getKind() == kind::MINUS
))
2943 // don't do it if it rewrites to a constant
2944 Node nr
= Rewriter::rewrite(n
);
2947 // return the rewritten constant
2953 ret
= NodeManager::currentNM()->mkSkolem(
2956 "Variable introduced in purifyNl pass");
2957 Node np
= purifyNlTerms(n
, cache
, bcache
, var_eq
, false);
2958 var_eq
.push_back(np
.eqNode(ret
));
2959 Trace("nl-ext-purify")
2960 << "Purify : " << ret
<< " -> " << np
<< std::endl
;
2965 bool beneathMultNew
= beneathMult
|| n
.getKind()==kind::MULT
;
2966 bool childChanged
= false;
2967 std::vector
< Node
> children
;
2968 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
2969 Node nc
= purifyNlTerms( n
[i
], cache
, bcache
, var_eq
, beneathMultNew
);
2970 childChanged
= childChanged
|| nc
!=n
[i
];
2971 children
.push_back( nc
);
2974 ret
= NodeManager::currentNM()->mkNode( n
.getKind(), children
);
2986 void SmtEnginePrivate::removeITEs() {
2987 d_smt
.finalOptionsAreSet();
2988 spendResource(options::preprocessStep());
2989 Trace("simplify") << "SmtEnginePrivate::removeITEs()" << endl
;
2991 // Remove all of the ITE occurrences and normalize
2992 d_iteRemover
.run(d_assertions
.ref(), d_iteSkolemMap
, true);
2993 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
2994 d_assertions
.replace(i
, Rewriter::rewrite(d_assertions
[i
]));
3000 // do dumping (before/after any preprocessing pass)
3001 static void dumpAssertions(const char* key
,
3002 const AssertionPipeline
& assertionList
) {
3003 if( Dump
.isOn("assertions") &&
3004 Dump
.isOn(string("assertions:") + key
) ) {
3005 // Push the simplified assertions to the dump output stream
3006 for(unsigned i
= 0; i
< assertionList
.size(); ++ i
) {
3007 TNode n
= assertionList
[i
];
3008 Dump("assertions") << AssertCommand(Expr(n
.toExpr()));
3013 // returns false if it learns a conflict
3014 bool SmtEnginePrivate::nonClausalSimplify() {
3015 spendResource(options::preprocessStep());
3016 d_smt
.finalOptionsAreSet();
3018 if(options::unsatCores() || options::fewerPreprocessingHoles()) {
3022 TimerStat::CodeTimer
nonclausalTimer(d_smt
.d_stats
->d_nonclausalSimplificationTime
);
3024 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify()" << endl
;
3025 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
3026 Trace("simplify") << "Assertion #" << i
<< " : " << d_assertions
[i
] << std::endl
;
3029 if(d_propagatorNeedsFinish
) {
3030 d_propagator
.finish();
3031 d_propagatorNeedsFinish
= false;
3033 d_propagator
.initialize();
3035 // Assert all the assertions to the propagator
3036 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
3037 << "asserting to propagator" << endl
;
3038 CDO
<unsigned>& substs_index
= d_assertions
.getSubstitutionsIndex();
3039 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
3040 Assert(Rewriter::rewrite(d_assertions
[i
]) == d_assertions
[i
]);
3041 // Don't reprocess substitutions
3042 if (substs_index
> 0 && i
== substs_index
)
3046 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): asserting " << d_assertions
[i
] << endl
;
3047 Debug("cores") << "d_propagator assertTrue: " << d_assertions
[i
] << std::endl
;
3048 d_propagator
.assertTrue(d_assertions
[i
]);
3051 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
3052 << "propagating" << endl
;
3053 if (d_propagator
.propagate()) {
3054 // If in conflict, just return false
3055 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
3056 << "conflict in non-clausal propagation" << endl
;
3057 Node falseNode
= NodeManager::currentNM()->mkConst
<bool>(false);
3058 Assert(!options::unsatCores() && !options::fewerPreprocessingHoles());
3059 d_assertions
.clear();
3060 addFormula(falseNode
, false, false);
3061 d_propagatorNeedsFinish
= true;
3066 Trace("simplify") << "Iterate through " << d_nonClausalLearnedLiterals
.size() << " learned literals." << std::endl
;
3067 // No conflict, go through the literals and solve them
3068 SubstitutionMap
& top_level_substs
= d_assertions
.getTopLevelSubstitutions();
3069 SubstitutionMap
constantPropagations(d_smt
.d_context
);
3070 SubstitutionMap
newSubstitutions(d_smt
.d_context
);
3071 SubstitutionMap::iterator pos
;
3073 for(unsigned i
= 0, i_end
= d_nonClausalLearnedLiterals
.size(); i
< i_end
; ++ i
) {
3074 // Simplify the literal we learned wrt previous substitutions
3075 Node learnedLiteral
= d_nonClausalLearnedLiterals
[i
];
3076 Assert(Rewriter::rewrite(learnedLiteral
) == learnedLiteral
);
3077 Assert(top_level_substs
.apply(learnedLiteral
) == learnedLiteral
);
3078 Trace("simplify") << "Process learnedLiteral : " << learnedLiteral
<< std::endl
;
3079 Node learnedLiteralNew
= newSubstitutions
.apply(learnedLiteral
);
3080 if (learnedLiteral
!= learnedLiteralNew
) {
3081 learnedLiteral
= Rewriter::rewrite(learnedLiteralNew
);
3083 Trace("simplify") << "Process learnedLiteral, after newSubs : " << learnedLiteral
<< std::endl
;
3085 learnedLiteralNew
= constantPropagations
.apply(learnedLiteral
);
3086 if (learnedLiteralNew
== learnedLiteral
) {
3089 ++d_smt
.d_stats
->d_numConstantProps
;
3090 learnedLiteral
= Rewriter::rewrite(learnedLiteralNew
);
3092 Trace("simplify") << "Process learnedLiteral, after constProp : " << learnedLiteral
<< std::endl
;
3093 // It might just simplify to a constant
3094 if (learnedLiteral
.isConst()) {
3095 if (learnedLiteral
.getConst
<bool>()) {
3096 // If the learned literal simplifies to true, it's redundant
3099 // If the learned literal simplifies to false, we're in conflict
3100 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
3102 << d_nonClausalLearnedLiterals
[i
] << endl
;
3103 Assert(!options::unsatCores());
3104 d_assertions
.clear();
3105 addFormula(NodeManager::currentNM()->mkConst
<bool>(false), false, false);
3106 d_propagatorNeedsFinish
= true;
3111 // Solve it with the corresponding theory, possibly adding new
3112 // substitutions to newSubstitutions
3113 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
3114 << "solving " << learnedLiteral
<< endl
;
3116 Theory::PPAssertStatus solveStatus
=
3117 d_smt
.d_theoryEngine
->solve(learnedLiteral
, newSubstitutions
);
3119 switch (solveStatus
) {
3120 case Theory::PP_ASSERT_STATUS_SOLVED
: {
3121 // The literal should rewrite to true
3122 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
3123 << "solved " << learnedLiteral
<< endl
;
3124 Assert(Rewriter::rewrite(newSubstitutions
.apply(learnedLiteral
)).isConst());
3125 // vector<pair<Node, Node> > equations;
3126 // constantPropagations.simplifyLHS(top_level_substs, equations,
3127 // true); if (equations.empty()) {
3130 // Assert(equations[0].first.isConst() &&
3131 // equations[0].second.isConst() && equations[0].first !=
3132 // equations[0].second);
3133 // else fall through
3136 case Theory::PP_ASSERT_STATUS_CONFLICT
:
3137 // If in conflict, we return false
3138 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
3139 << "conflict while solving "
3140 << learnedLiteral
<< endl
;
3141 Assert(!options::unsatCores());
3142 d_assertions
.clear();
3143 addFormula(NodeManager::currentNM()->mkConst
<bool>(false), false, false);
3144 d_propagatorNeedsFinish
= true;
3147 if (d_doConstantProp
&& learnedLiteral
.getKind() == kind::EQUAL
&& (learnedLiteral
[0].isConst() || learnedLiteral
[1].isConst())) {
3148 // constant propagation
3151 if (learnedLiteral
[0].isConst()) {
3152 t
= learnedLiteral
[1];
3153 c
= learnedLiteral
[0];
3156 t
= learnedLiteral
[0];
3157 c
= learnedLiteral
[1];
3159 Assert(!t
.isConst());
3160 Assert(constantPropagations
.apply(t
) == t
);
3161 Assert(top_level_substs
.apply(t
) == t
);
3162 Assert(newSubstitutions
.apply(t
) == t
);
3163 constantPropagations
.addSubstitution(t
, c
);
3164 // vector<pair<Node,Node> > equations;
3165 // constantPropagations.simplifyLHS(t, c, equations, true);
3166 // if (!equations.empty()) {
3167 // Assert(equations[0].first.isConst() &&
3168 // equations[0].second.isConst() && equations[0].first !=
3169 // equations[0].second); d_assertions.clear();
3170 // addFormula(NodeManager::currentNM()->mkConst<bool>(false), false,
3173 // top_level_substs.simplifyRHS(constantPropagations);
3177 d_nonClausalLearnedLiterals
[j
++] = d_nonClausalLearnedLiterals
[i
];
3183 #ifdef CVC4_ASSERTIONS
3184 // NOTE: When debugging this code, consider moving this check inside of the
3185 // loop over d_nonClausalLearnedLiterals. This check has been moved outside
3186 // because it is costly for certain inputs (see bug 508).
3188 // Check data structure invariants:
3189 // 1. for each lhs of top_level_substs, does not appear anywhere in rhs of
3190 // top_level_substs or anywhere in constantPropagations
3191 // 2. each lhs of constantPropagations rewrites to itself
3192 // 3. if l -> r is a constant propagation and l is a subterm of l' with l' ->
3193 // r' another constant propagation, then l'[l/r] -> r' should be a
3194 // constant propagation too
3195 // 4. each lhs of constantPropagations is different from each rhs
3196 for (pos
= newSubstitutions
.begin(); pos
!= newSubstitutions
.end(); ++pos
) {
3197 Assert((*pos
).first
.isVar());
3198 Assert(top_level_substs
.apply((*pos
).first
) == (*pos
).first
);
3199 Assert(top_level_substs
.apply((*pos
).second
) == (*pos
).second
);
3200 Assert(newSubstitutions
.apply(newSubstitutions
.apply((*pos
).second
)) == newSubstitutions
.apply((*pos
).second
));
3202 for (pos
= constantPropagations
.begin(); pos
!= constantPropagations
.end(); ++pos
) {
3203 Assert((*pos
).second
.isConst());
3204 Assert(Rewriter::rewrite((*pos
).first
) == (*pos
).first
);
3205 // Node newLeft = top_level_substs.apply((*pos).first);
3206 // if (newLeft != (*pos).first) {
3207 // newLeft = Rewriter::rewrite(newLeft);
3208 // Assert(newLeft == (*pos).second ||
3209 // (constantPropagations.hasSubstitution(newLeft) &&
3210 // constantPropagations.apply(newLeft) == (*pos).second));
3212 // newLeft = constantPropagations.apply((*pos).first);
3213 // if (newLeft != (*pos).first) {
3214 // newLeft = Rewriter::rewrite(newLeft);
3215 // Assert(newLeft == (*pos).second ||
3216 // (constantPropagations.hasSubstitution(newLeft) &&
3217 // constantPropagations.apply(newLeft) == (*pos).second));
3219 Assert(constantPropagations
.apply((*pos
).second
) == (*pos
).second
);
3221 #endif /* CVC4_ASSERTIONS */
3223 // Resize the learnt
3224 Trace("simplify") << "Resize non-clausal learned literals to " << j
<< std::endl
;
3225 d_nonClausalLearnedLiterals
.resize(j
);
3227 unordered_set
<TNode
, TNodeHashFunction
> s
;
3228 Trace("debugging") << "NonClausal simplify pre-preprocess\n";
3229 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
3230 Node assertion
= d_assertions
[i
];
3231 Node assertionNew
= newSubstitutions
.apply(assertion
);
3232 Trace("debugging") << "assertion = " << assertion
<< endl
;
3233 Trace("debugging") << "assertionNew = " << assertionNew
<< endl
;
3234 if (assertion
!= assertionNew
) {
3235 assertion
= Rewriter::rewrite(assertionNew
);
3236 Trace("debugging") << "rewrite(assertion) = " << assertion
<< endl
;
3238 Assert(Rewriter::rewrite(assertion
) == assertion
);
3240 assertionNew
= constantPropagations
.apply(assertion
);
3241 if (assertionNew
== assertion
) {
3244 ++d_smt
.d_stats
->d_numConstantProps
;
3245 Trace("debugging") << "assertionNew = " << assertionNew
<< endl
;
3246 assertion
= Rewriter::rewrite(assertionNew
);
3247 Trace("debugging") << "assertionNew = " << assertionNew
<< endl
;
3249 Trace("debugging") << "\n";
3250 s
.insert(assertion
);
3251 d_assertions
.replace(i
, assertion
);
3252 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
3253 << "non-clausal preprocessed: "
3254 << assertion
<< endl
;
3257 // If in incremental mode, add substitutions to the list of assertions
3258 if (substs_index
> 0)
3260 NodeBuilder
<> substitutionsBuilder(kind::AND
);
3261 substitutionsBuilder
<< d_assertions
[substs_index
];
3262 pos
= newSubstitutions
.begin();
3263 for (; pos
!= newSubstitutions
.end(); ++pos
) {
3264 // Add back this substitution as an assertion
3265 TNode lhs
= (*pos
).first
, rhs
= newSubstitutions
.apply((*pos
).second
);
3266 Node n
= NodeManager::currentNM()->mkNode(kind::EQUAL
, lhs
, rhs
);
3267 substitutionsBuilder
<< n
;
3268 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): will notify SAT layer of substitution: " << n
<< endl
;
3270 if (substitutionsBuilder
.getNumChildren() > 1) {
3271 d_assertions
.replace(substs_index
,
3272 Rewriter::rewrite(Node(substitutionsBuilder
)));
3275 // If not in incremental mode, must add substitutions to model
3276 TheoryModel
* m
= d_smt
.d_theoryEngine
->getModel();
3278 for(pos
= newSubstitutions
.begin(); pos
!= newSubstitutions
.end(); ++pos
) {
3279 Node n
= (*pos
).first
;
3280 Node v
= newSubstitutions
.apply((*pos
).second
);
3281 Trace("model") << "Add substitution : " << n
<< " " << v
<< endl
;
3282 m
->addSubstitution( n
, v
);
3287 NodeBuilder
<> learnedBuilder(kind::AND
);
3288 Assert(d_realAssertionsEnd
<= d_assertions
.size());
3289 learnedBuilder
<< d_assertions
[d_realAssertionsEnd
- 1];
3291 for (unsigned i
= 0; i
< d_nonClausalLearnedLiterals
.size(); ++ i
) {
3292 Node learned
= d_nonClausalLearnedLiterals
[i
];
3293 Assert(top_level_substs
.apply(learned
) == learned
);
3294 Node learnedNew
= newSubstitutions
.apply(learned
);
3295 if (learned
!= learnedNew
) {
3296 learned
= Rewriter::rewrite(learnedNew
);
3298 Assert(Rewriter::rewrite(learned
) == learned
);
3300 learnedNew
= constantPropagations
.apply(learned
);
3301 if (learnedNew
== learned
) {
3304 ++d_smt
.d_stats
->d_numConstantProps
;
3305 learned
= Rewriter::rewrite(learnedNew
);
3307 if (s
.find(learned
) != s
.end()) {
3311 learnedBuilder
<< learned
;
3312 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
3313 << "non-clausal learned : "
3316 d_nonClausalLearnedLiterals
.clear();
3318 for (pos
= constantPropagations
.begin(); pos
!= constantPropagations
.end(); ++pos
) {
3319 Node cProp
= (*pos
).first
.eqNode((*pos
).second
);
3320 Assert(top_level_substs
.apply(cProp
) == cProp
);
3321 Node cPropNew
= newSubstitutions
.apply(cProp
);
3322 if (cProp
!= cPropNew
) {
3323 cProp
= Rewriter::rewrite(cPropNew
);
3324 Assert(Rewriter::rewrite(cProp
) == cProp
);
3326 if (s
.find(cProp
) != s
.end()) {
3330 learnedBuilder
<< cProp
;
3331 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
3332 << "non-clausal constant propagation : "
3336 // Add new substitutions to topLevelSubstitutions
3337 // Note that we don't have to keep rhs's in full solved form
3338 // because SubstitutionMap::apply does a fixed-point iteration when substituting
3339 top_level_substs
.addSubstitutions(newSubstitutions
);
3341 if(learnedBuilder
.getNumChildren() > 1) {
3342 d_assertions
.replace(d_realAssertionsEnd
- 1,
3343 Rewriter::rewrite(Node(learnedBuilder
)));
3346 d_propagatorNeedsFinish
= true;
3350 bool SmtEnginePrivate::simpITE() {
3351 TimerStat::CodeTimer
simpITETimer(d_smt
.d_stats
->d_simpITETime
);
3353 spendResource(options::preprocessStep());
3355 Trace("simplify") << "SmtEnginePrivate::simpITE()" << endl
;
3357 unsigned numAssertionOnEntry
= d_assertions
.size();
3358 for (unsigned i
= 0; i
< d_assertions
.size(); ++i
) {
3359 spendResource(options::preprocessStep());
3360 Node result
= d_smt
.d_theoryEngine
->ppSimpITE(d_assertions
[i
]);
3361 d_assertions
.replace(i
, result
);
3362 if(result
.isConst() && !result
.getConst
<bool>()){
3366 bool result
= d_smt
.d_theoryEngine
->donePPSimpITE(d_assertions
.ref());
3367 if(numAssertionOnEntry
< d_assertions
.size()){
3368 compressBeforeRealAssertions(numAssertionOnEntry
);
3373 void SmtEnginePrivate::compressBeforeRealAssertions(size_t before
){
3374 size_t curr
= d_assertions
.size();
3375 if(before
>= curr
||
3376 d_realAssertionsEnd
<= 0 ||
3377 d_realAssertionsEnd
>= curr
){
3382 // original: [0 ... d_realAssertionsEnd)
3384 // ites skolems [d_realAssertionsEnd, before)
3386 // added [before, curr)
3388 Assert(0 < d_realAssertionsEnd
);
3389 Assert(d_realAssertionsEnd
<= before
);
3390 Assert(before
< curr
);
3392 std::vector
<Node
> intoConjunction
;
3393 for(size_t i
= before
; i
<curr
; ++i
){
3394 intoConjunction
.push_back(d_assertions
[i
]);
3396 d_assertions
.resize(before
);
3397 size_t lastBeforeItes
= d_realAssertionsEnd
- 1;
3398 intoConjunction
.push_back(d_assertions
[lastBeforeItes
]);
3399 Node newLast
= util::NaryBuilder::mkAssoc(kind::AND
, intoConjunction
);
3400 d_assertions
.replace(lastBeforeItes
, newLast
);
3401 Assert(d_assertions
.size() == before
);
3404 void SmtEnginePrivate::unconstrainedSimp() {
3405 TimerStat::CodeTimer
unconstrainedSimpTimer(d_smt
.d_stats
->d_unconstrainedSimpTime
);
3406 spendResource(options::preprocessStep());
3407 Trace("simplify") << "SmtEnginePrivate::unconstrainedSimp()" << endl
;
3408 d_smt
.d_theoryEngine
->ppUnconstrainedSimp(d_assertions
.ref());
3411 void SmtEnginePrivate::traceBackToAssertions(const std::vector
<Node
>& nodes
, std::vector
<TNode
>& assertions
) {
3412 const booleans::CircuitPropagator::BackEdgesMap
& backEdges
= d_propagator
.getBackEdges();
3413 for(vector
<Node
>::const_iterator i
= nodes
.begin(); i
!= nodes
.end(); ++i
) {
3414 booleans::CircuitPropagator::BackEdgesMap::const_iterator j
= backEdges
.find(*i
);
3415 // term must appear in map, otherwise how did we get here?!
3416 Assert(j
!= backEdges
.end());
3417 // if term maps to empty, that means it's a top-level assertion
3418 if(!(*j
).second
.empty()) {
3419 traceBackToAssertions((*j
).second
, assertions
);
3421 assertions
.push_back(*i
);
3426 size_t SmtEnginePrivate::removeFromConjunction(Node
& n
, const std::unordered_set
<unsigned long>& toRemove
) {
3427 Assert(n
.getKind() == kind::AND
);
3428 size_t removals
= 0;
3429 for(Node::iterator j
= n
.begin(); j
!= n
.end(); ++j
) {
3430 size_t subremovals
= 0;
3432 if(toRemove
.find(sub
.getId()) != toRemove
.end() ||
3433 (sub
.getKind() == kind::AND
&& (subremovals
= removeFromConjunction(sub
, toRemove
)) > 0)) {
3434 NodeBuilder
<> b(kind::AND
);
3435 b
.append(n
.begin(), j
);
3436 if(subremovals
> 0) {
3437 removals
+= subremovals
;
3442 for(++j
; j
!= n
.end(); ++j
) {
3443 if(toRemove
.find((*j
).getId()) != toRemove
.end()) {
3445 } else if((*j
).getKind() == kind::AND
) {
3447 if((subremovals
= removeFromConjunction(sub
, toRemove
)) > 0) {
3448 removals
+= subremovals
;
3457 if(b
.getNumChildren() == 0) {
3460 } else if(b
.getNumChildren() == 1) {
3466 n
= Rewriter::rewrite(n
);
3471 Assert(removals
== 0);
3475 void SmtEnginePrivate::doMiplibTrick() {
3476 Assert(d_realAssertionsEnd
== d_assertions
.size());
3477 Assert(!options::incrementalSolving());
3479 const booleans::CircuitPropagator::BackEdgesMap
& backEdges
= d_propagator
.getBackEdges();
3480 unordered_set
<unsigned long> removeAssertions
;
3482 NodeManager
* nm
= NodeManager::currentNM();
3483 Node zero
= nm
->mkConst(Rational(0)), one
= nm
->mkConst(Rational(1));
3485 SubstitutionMap
& top_level_substs
= d_assertions
.getTopLevelSubstitutions();
3486 unordered_map
<TNode
, Node
, TNodeHashFunction
> intVars
;
3487 for(vector
<Node
>::const_iterator i
= d_boolVars
.begin(); i
!= d_boolVars
.end(); ++i
) {
3488 if(d_propagator
.isAssigned(*i
)) {
3489 Debug("miplib") << "ineligible: " << *i
<< " because assigned " << d_propagator
.getAssignment(*i
) << endl
;
3493 vector
<TNode
> assertions
;
3494 booleans::CircuitPropagator::BackEdgesMap::const_iterator j
= backEdges
.find(*i
);
3495 // if not in back edges map, the bool var is unconstrained, showing up in no assertions.
3496 // if maps to an empty vector, that means the bool var was asserted itself.
3497 if(j
!= backEdges
.end()) {
3498 if(!(*j
).second
.empty()) {
3499 traceBackToAssertions((*j
).second
, assertions
);
3501 assertions
.push_back(*i
);
3504 Debug("miplib") << "for " << *i
<< endl
;
3505 bool eligible
= true;
3506 map
<pair
<Node
, Node
>, uint64_t> marks
;
3507 map
<pair
<Node
, Node
>, vector
<Rational
> > coef
;
3508 map
<pair
<Node
, Node
>, vector
<Rational
> > checks
;
3509 map
<pair
<Node
, Node
>, vector
<TNode
> > asserts
;
3510 for(vector
<TNode
>::const_iterator j
= assertions
.begin(); j
!= assertions
.end(); ++j
) {
3511 Debug("miplib") << " found: " << *j
<< endl
;
3512 if((*j
).getKind() != kind::IMPLIES
) {
3514 Debug("miplib") << " -- INELIGIBLE -- (not =>)" << endl
;
3517 Node conj
= BooleanSimplification::simplify((*j
)[0]);
3518 if(conj
.getKind() == kind::AND
&& conj
.getNumChildren() > 6) {
3520 Debug("miplib") << " -- INELIGIBLE -- (N-ary /\\ too big)" << endl
;
3523 if(conj
.getKind() != kind::AND
&& !conj
.isVar() && !(conj
.getKind() == kind::NOT
&& conj
[0].isVar())) {
3525 Debug("miplib") << " -- INELIGIBLE -- (not /\\ or literal)" << endl
;
3528 if((*j
)[1].getKind() != kind::EQUAL
||
3529 !( ( (*j
)[1][0].isVar() &&
3530 (*j
)[1][1].getKind() == kind::CONST_RATIONAL
) ||
3531 ( (*j
)[1][0].getKind() == kind::CONST_RATIONAL
&&
3532 (*j
)[1][1].isVar() ) )) {
3534 Debug("miplib") << " -- INELIGIBLE -- (=> (and X X) X)" << endl
;
3537 if(conj
.getKind() == kind::AND
) {
3539 bool found_x
= false;
3540 map
<TNode
, bool> neg
;
3541 for(Node::iterator ii
= conj
.begin(); ii
!= conj
.end(); ++ii
) {
3543 posv
.push_back(*ii
);
3545 found_x
= found_x
|| *i
== *ii
;
3546 } else if((*ii
).getKind() == kind::NOT
&& (*ii
)[0].isVar()) {
3547 posv
.push_back((*ii
)[0]);
3548 neg
[(*ii
)[0]] = true;
3549 found_x
= found_x
|| *i
== (*ii
)[0];
3552 Debug("miplib") << " -- INELIGIBLE -- (non-var: " << *ii
<< ")" << endl
;
3555 if(d_propagator
.isAssigned(posv
.back())) {
3557 Debug("miplib") << " -- INELIGIBLE -- (" << posv
.back() << " asserted)" << endl
;
3566 Debug("miplib") << " --INELIGIBLE -- (couldn't find " << *i
<< " in conjunction)" << endl
;
3569 sort(posv
.begin(), posv
.end());
3570 const Node pos
= NodeManager::currentNM()->mkNode(kind::AND
, posv
);
3571 const TNode var
= ((*j
)[1][0].getKind() == kind::CONST_RATIONAL
) ? (*j
)[1][1] : (*j
)[1][0];
3572 const pair
<Node
, Node
> pos_var(pos
, var
);
3573 const Rational
& constant
= ((*j
)[1][0].getKind() == kind::CONST_RATIONAL
) ? (*j
)[1][0].getConst
<Rational
>() : (*j
)[1][1].getConst
<Rational
>();
3575 unsigned countneg
= 0, thepos
= 0;
3576 for(unsigned ii
= 0; ii
< pos
.getNumChildren(); ++ii
) {
3581 mark
|= (0x1 << ii
);
3584 if((marks
[pos_var
] & (1lu << mark
)) != 0) {
3586 Debug("miplib") << " -- INELIGIBLE -- (remarked)" << endl
;
3589 Debug("miplib") << "mark is " << mark
<< " -- " << (1lu << mark
) << endl
;
3590 marks
[pos_var
] |= (1lu << mark
);
3591 Debug("miplib") << "marks[" << pos
<< "," << var
<< "] now " << marks
[pos_var
] << endl
;
3592 if(countneg
== pos
.getNumChildren()) {
3595 Debug("miplib") << " -- INELIGIBLE -- (nonzero constant)" << endl
;
3598 } else if(countneg
== pos
.getNumChildren() - 1) {
3599 Assert(coef
[pos_var
].size() <= 6 && thepos
< 6);
3600 if(coef
[pos_var
].size() <= thepos
) {
3601 coef
[pos_var
].resize(thepos
+ 1);
3603 coef
[pos_var
][thepos
] = constant
;
3605 if(checks
[pos_var
].size() <= mark
) {
3606 checks
[pos_var
].resize(mark
+ 1);
3608 checks
[pos_var
][mark
] = constant
;
3610 asserts
[pos_var
].push_back(*j
);
3613 if(x
!= *i
&& x
!= (*i
).notNode()) {
3615 Debug("miplib") << " -- INELIGIBLE -- (x not present where I expect it)" << endl
;
3618 const bool xneg
= (x
.getKind() == kind::NOT
);
3619 x
= xneg
? x
[0] : x
;
3620 Debug("miplib") << " x:" << x
<< " " << xneg
<< endl
;
3621 const TNode var
= ((*j
)[1][0].getKind() == kind::CONST_RATIONAL
) ? (*j
)[1][1] : (*j
)[1][0];
3622 const pair
<Node
, Node
> x_var(x
, var
);
3623 const Rational
& constant
= ((*j
)[1][0].getKind() == kind::CONST_RATIONAL
) ? (*j
)[1][0].getConst
<Rational
>() : (*j
)[1][1].getConst
<Rational
>();
3624 unsigned mark
= (xneg
? 0 : 1);
3625 if((marks
[x_var
] & (1u << mark
)) != 0) {
3627 Debug("miplib") << " -- INELIGIBLE -- (remarked)" << endl
;
3630 marks
[x_var
] |= (1u << mark
);
3634 Debug("miplib") << " -- INELIGIBLE -- (nonzero constant)" << endl
;
3638 Assert(coef
[x_var
].size() <= 6);
3639 coef
[x_var
].resize(6);
3640 coef
[x_var
][0] = constant
;
3642 asserts
[x_var
].push_back(*j
);
3646 for(map
<pair
<Node
, Node
>, uint64_t>::const_iterator j
= marks
.begin(); j
!= marks
.end(); ++j
) {
3647 const TNode pos
= (*j
).first
.first
;
3648 const TNode var
= (*j
).first
.second
;
3649 const pair
<Node
, Node
>& pos_var
= (*j
).first
;
3650 const uint64_t mark
= (*j
).second
;
3651 const unsigned numVars
= pos
.getKind() == kind::AND
? pos
.getNumChildren() : 1;
3652 uint64_t expected
= (uint64_t(1) << (1 << numVars
)) - 1;
3653 expected
= (expected
== 0) ? -1 : expected
; // fix for overflow
3654 Debug("miplib") << "[" << pos
<< "] => " << hex
<< mark
<< " expect " << expected
<< dec
<< endl
;
3655 Assert(pos
.getKind() == kind::AND
|| pos
.isVar());
3656 if(mark
!= expected
) {
3657 Debug("miplib") << " -- INELIGIBLE " << pos
<< " -- (insufficiently marked, got " << mark
<< " for " << numVars
<< " vars, expected " << expected
<< endl
;
3659 if(mark
!= 3) { // exclude single-var case; nothing to check there
3660 uint64_t sz
= (uint64_t(1) << checks
[pos_var
].size()) - 1;
3661 sz
= (sz
== 0) ? -1 : sz
; // fix for overflow
3662 Assert(sz
== mark
, "expected size %u == mark %u", sz
, mark
);
3663 for(size_t k
= 0; k
< checks
[pos_var
].size(); ++k
) {
3664 if((k
& (k
- 1)) != 0) {
3666 Debug("miplib") << k
<< " => " << checks
[pos_var
][k
] << endl
;
3667 for(size_t v
= 1, kk
= k
; kk
!= 0; ++v
, kk
>>= 1) {
3668 if((kk
& 0x1) == 1) {
3669 Assert(pos
.getKind() == kind::AND
);
3670 Debug("miplib") << "var " << v
<< " : " << pos
[v
- 1] << " coef:" << coef
[pos_var
][v
- 1] << endl
;
3671 sum
+= coef
[pos_var
][v
- 1];
3674 Debug("miplib") << "checkSum is " << sum
<< " input says " << checks
[pos_var
][k
] << endl
;
3675 if(sum
!= checks
[pos_var
][k
]) {
3677 Debug("miplib") << " -- INELIGIBLE " << pos
<< " -- (nonlinear combination)" << endl
;
3681 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
3686 eligible
= true; // next is still eligible
3690 Debug("miplib") << " -- ELIGIBLE " << *i
<< " , " << pos
<< " --" << endl
;
3691 vector
<Node
> newVars
;
3692 expr::NodeSelfIterator ii
, iiend
;
3693 if(pos
.getKind() == kind::AND
) {
3697 ii
= expr::NodeSelfIterator::self(pos
);
3698 iiend
= expr::NodeSelfIterator::selfEnd(pos
);
3700 for(; ii
!= iiend
; ++ii
) {
3701 Node
& varRef
= intVars
[*ii
];
3702 if(varRef
.isNull()) {
3704 ss
<< "mipvar_" << *ii
;
3705 Node newVar
= nm
->mkSkolem(ss
.str(), nm
->integerType(), "a variable introduced due to scrubbing a miplib encoding", NodeManager::SKOLEM_EXACT_NAME
);
3706 Node geq
= Rewriter::rewrite(nm
->mkNode(kind::GEQ
, newVar
, zero
));
3707 Node leq
= Rewriter::rewrite(nm
->mkNode(kind::LEQ
, newVar
, one
));
3708 addFormula(Rewriter::rewrite(geq
.andNode(leq
)), false, false);
3709 SubstitutionMap
nullMap(&d_fakeContext
);
3710 Theory::PPAssertStatus status CVC4_UNUSED
; // just for assertions
3711 status
= d_smt
.d_theoryEngine
->solve(geq
, nullMap
);
3712 Assert(status
== Theory::PP_ASSERT_STATUS_UNSOLVED
,
3713 "unexpected solution from arith's ppAssert()");
3714 Assert(nullMap
.empty(),
3715 "unexpected substitution from arith's ppAssert()");
3716 status
= d_smt
.d_theoryEngine
->solve(leq
, nullMap
);
3717 Assert(status
== Theory::PP_ASSERT_STATUS_UNSOLVED
,
3718 "unexpected solution from arith's ppAssert()");
3719 Assert(nullMap
.empty(),
3720 "unexpected substitution from arith's ppAssert()");
3721 d_smt
.d_theoryEngine
->getModel()->addSubstitution(*ii
, newVar
.eqNode(one
));
3722 newVars
.push_back(newVar
);
3725 newVars
.push_back(varRef
);
3727 if(!d_smt
.d_logic
.areIntegersUsed()) {
3728 d_smt
.d_logic
= d_smt
.d_logic
.getUnlockedCopy();
3729 d_smt
.d_logic
.enableIntegers();
3730 d_smt
.d_logic
.lock();
3734 if(pos
.getKind() == kind::AND
) {
3735 NodeBuilder
<> sumb(kind::PLUS
);
3736 for(size_t ii
= 0; ii
< pos
.getNumChildren(); ++ii
) {
3737 sumb
<< nm
->mkNode(kind::MULT
, nm
->mkConst(coef
[pos_var
][ii
]), newVars
[ii
]);
3741 sum
= nm
->mkNode(kind::MULT
, nm
->mkConst(coef
[pos_var
][0]), newVars
[0]);
3743 Debug("miplib") << "vars[] " << var
<< endl
3744 << " eq " << Rewriter::rewrite(sum
) << endl
;
3745 Node newAssertion
= var
.eqNode(Rewriter::rewrite(sum
));
3746 if (top_level_substs
.hasSubstitution(newAssertion
[0]))
3748 // Warning() << "RE-SUBSTITUTION " << newAssertion[0] << endl;
3749 // Warning() << "REPLACE " << newAssertion[1] << endl;
3750 // Warning() << "ORIG " <<
3751 // top_level_substs.getSubstitution(newAssertion[0]) << endl;
3752 Assert(top_level_substs
.getSubstitution(newAssertion
[0])
3753 == newAssertion
[1]);
3754 } else if(pos
.getNumChildren() <= options::arithMLTrickSubstitutions()) {
3755 top_level_substs
.addSubstitution(newAssertion
[0], newAssertion
[1]);
3756 Debug("miplib") << "addSubs: " << newAssertion
[0] << " to " << newAssertion
[1] << endl
;
3758 Debug("miplib") << "skipSubs: " << newAssertion
[0] << " to " << newAssertion
[1] << " (threshold is " << options::arithMLTrickSubstitutions() << ")" << endl
;
3760 newAssertion
= Rewriter::rewrite(newAssertion
);
3761 Debug("miplib") << " " << newAssertion
<< endl
;
3762 addFormula(newAssertion
, false, false);
3763 Debug("miplib") << " assertions to remove: " << endl
;
3764 for(vector
<TNode
>::const_iterator k
= asserts
[pos_var
].begin(), k_end
= asserts
[pos_var
].end(); k
!= k_end
; ++k
) {
3765 Debug("miplib") << " " << *k
<< endl
;
3766 removeAssertions
.insert((*k
).getId());
3772 if(!removeAssertions
.empty()) {
3773 Debug("miplib") << "SmtEnginePrivate::simplify(): scrubbing miplib encoding..." << endl
;
3774 for(size_t i
= 0; i
< d_realAssertionsEnd
; ++i
) {
3775 if(removeAssertions
.find(d_assertions
[i
].getId()) != removeAssertions
.end()) {
3776 Debug("miplib") << "SmtEnginePrivate::simplify(): - removing " << d_assertions
[i
] << endl
;
3777 d_assertions
[i
] = d_true
;
3778 ++d_smt
.d_stats
->d_numMiplibAssertionsRemoved
;
3779 } else if(d_assertions
[i
].getKind() == kind::AND
) {
3780 size_t removals
= removeFromConjunction(d_assertions
[i
], removeAssertions
);
3782 Debug("miplib") << "SmtEnginePrivate::simplify(): - reduced " << d_assertions
[i
] << endl
;
3783 Debug("miplib") << "SmtEnginePrivate::simplify(): - by " << removals
<< " conjuncts" << endl
;
3784 d_smt
.d_stats
->d_numMiplibAssertionsRemoved
+= removals
;
3787 Debug("miplib") << "had: " << d_assertions
[i
] << endl
;
3789 Rewriter::rewrite(top_level_substs
.apply(d_assertions
[i
]));
3790 Debug("miplib") << "now: " << d_assertions
[i
] << endl
;
3793 Debug("miplib") << "SmtEnginePrivate::simplify(): miplib pass found nothing." << endl
;
3795 d_realAssertionsEnd
= d_assertions
.size();
3799 // returns false if simplification led to "false"
3800 bool SmtEnginePrivate::simplifyAssertions()
3802 spendResource(options::preprocessStep());
3803 Assert(d_smt
.d_pendingPops
== 0);
3805 ScopeCounter
depth(d_simplifyAssertionsDepth
);
3807 Trace("simplify") << "SmtEnginePrivate::simplify()" << endl
;
3809 dumpAssertions("pre-nonclausal", d_assertions
);
3811 if(options::simplificationMode() != SIMPLIFICATION_MODE_NONE
) {
3812 // Perform non-clausal simplification
3813 Chat() << "...performing nonclausal simplification..." << endl
;
3814 Trace("simplify") << "SmtEnginePrivate::simplify(): "
3815 << "performing non-clausal simplification" << endl
;
3816 bool noConflict
= nonClausalSimplify();
3821 // We piggy-back off of the BackEdgesMap in the CircuitPropagator to
3822 // do the miplib trick.
3823 if( // check that option is on
3824 options::arithMLTrick() &&
3825 // miplib rewrites aren't safe in incremental mode
3826 ! options::incrementalSolving() &&
3827 // only useful in arith
3828 d_smt
.d_logic
.isTheoryEnabled(THEORY_ARITH
) &&
3829 // we add new assertions and need this (in practice, this
3830 // restriction only disables miplib processing during
3831 // re-simplification, which we don't expect to be useful anyway)
3832 d_realAssertionsEnd
== d_assertions
.size() ) {
3833 Chat() << "...fixing miplib encodings..." << endl
;
3834 Trace("simplify") << "SmtEnginePrivate::simplify(): "
3835 << "looking for miplib pseudobooleans..." << endl
;
3837 TimerStat::CodeTimer
miplibTimer(d_smt
.d_stats
->d_miplibPassTime
);
3841 Trace("simplify") << "SmtEnginePrivate::simplify(): "
3842 << "skipping miplib pseudobooleans pass (either incrementalSolving is on, or miplib pbs are turned off)..." << endl
;
3846 dumpAssertions("post-nonclausal", d_assertions
);
3847 Trace("smt") << "POST nonClausalSimplify" << endl
;
3848 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
3850 // before ppRewrite check if only core theory for BV theory
3851 d_smt
.d_theoryEngine
->staticInitializeBVOptions(d_assertions
.ref());
3853 dumpAssertions("pre-theorypp", d_assertions
);
3855 // Theory preprocessing
3856 if (d_smt
.d_earlyTheoryPP
) {
3857 Chat() << "...doing early theory preprocessing..." << endl
;
3858 TimerStat::CodeTimer
codeTimer(d_smt
.d_stats
->d_theoryPreprocessTime
);
3859 // Call the theory preprocessors
3860 d_smt
.d_theoryEngine
->preprocessStart();
3861 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
3862 Assert(Rewriter::rewrite(d_assertions
[i
]) == d_assertions
[i
]);
3863 d_assertions
.replace(i
, d_smt
.d_theoryEngine
->preprocess(d_assertions
[i
]));
3864 Assert(Rewriter::rewrite(d_assertions
[i
]) == d_assertions
[i
]);
3868 dumpAssertions("post-theorypp", d_assertions
);
3869 Trace("smt") << "POST theoryPP" << endl
;
3870 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
3872 // ITE simplification
3873 if(options::doITESimp() &&
3874 (d_simplifyAssertionsDepth
<= 1 || options::doITESimpOnRepeat())) {
3875 Chat() << "...doing ITE simplification..." << endl
;
3876 bool noConflict
= simpITE();
3878 Chat() << "...ITE simplification found unsat..." << endl
;
3883 dumpAssertions("post-itesimp", d_assertions
);
3884 Trace("smt") << "POST iteSimp" << endl
;
3885 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
3887 // Unconstrained simplification
3888 if(options::unconstrainedSimp()) {
3889 Chat() << "...doing unconstrained simplification..." << endl
;
3890 unconstrainedSimp();
3893 dumpAssertions("post-unconstrained", d_assertions
);
3894 Trace("smt") << "POST unconstrainedSimp" << endl
;
3895 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
3897 if(options::repeatSimp() && options::simplificationMode() != SIMPLIFICATION_MODE_NONE
) {
3898 Chat() << "...doing another round of nonclausal simplification..." << endl
;
3899 Trace("simplify") << "SmtEnginePrivate::simplify(): "
3900 << " doing repeated simplification" << endl
;
3901 bool noConflict
= nonClausalSimplify();
3907 dumpAssertions("post-repeatsimp", d_assertions
);
3908 Trace("smt") << "POST repeatSimp" << endl
;
3909 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
3911 } catch(TypeCheckingExceptionPrivate
& tcep
) {
3912 // Calls to this function should have already weeded out any
3913 // typechecking exceptions via (e.g.) ensureBoolean(). But a
3914 // theory could still create a new expression that isn't
3915 // well-typed, and we don't want the C++ runtime to abort our
3916 // process without any error notice.
3918 ss
<< "A bad expression was produced. Original exception follows:\n"
3920 InternalError(ss
.str().c_str());
3925 Result
SmtEngine::check() {
3926 Assert(d_fullyInited
);
3927 Assert(d_pendingPops
== 0);
3929 Trace("smt") << "SmtEngine::check()" << endl
;
3931 ResourceManager
* resourceManager
= d_private
->getResourceManager();
3933 resourceManager
->beginCall();
3935 // Only way we can be out of resource is if cumulative budget is on
3936 if (resourceManager
->cumulativeLimitOn() &&
3937 resourceManager
->out()) {
3938 Result::UnknownExplanation why
= resourceManager
->outOfResources() ?
3939 Result::RESOURCEOUT
: Result::TIMEOUT
;
3940 return Result(Result::VALIDITY_UNKNOWN
, why
, d_filename
);
3943 // Make sure the prop layer has all of the assertions
3944 Trace("smt") << "SmtEngine::check(): processing assertions" << endl
;
3945 d_private
->processAssertions();
3946 Trace("smt") << "SmtEngine::check(): done processing assertions" << endl
;
3948 // Turn off stop only for QF_LRA
3949 // TODO: Bring up in a meeting where to put this
3950 if(options::decisionStopOnly() && !options::decisionMode
.wasSetByUser() ){
3952 (not d_logic
.isQuantified() &&
3953 d_logic
.isPure(THEORY_ARITH
) && d_logic
.isLinear() && !d_logic
.isDifferenceLogic() && !d_logic
.areIntegersUsed()
3955 if(d_private
->d_iteSkolemMap
.empty()){
3956 options::decisionStopOnly
.set(false);
3957 d_decisionEngine
->clearStrategies();
3958 Trace("smt") << "SmtEngine::check(): turning off stop only" << endl
;
3963 TimerStat::CodeTimer
solveTimer(d_stats
->d_solveTime
);
3965 Chat() << "solving..." << endl
;
3966 Trace("smt") << "SmtEngine::check(): running check" << endl
;
3967 Result result
= d_propEngine
->checkSat();
3969 resourceManager
->endCall();
3970 Trace("limit") << "SmtEngine::check(): cumulative millis " << resourceManager
->getTimeUsage()
3971 << ", resources " << resourceManager
->getResourceUsage() << endl
;
3974 return Result(result
, d_filename
);
3977 Result
SmtEngine::quickCheck() {
3978 Assert(d_fullyInited
);
3979 Trace("smt") << "SMT quickCheck()" << endl
;
3980 return Result(Result::VALIDITY_UNKNOWN
, Result::REQUIRES_FULL_CHECK
, d_filename
);
3984 void SmtEnginePrivate::collectSkolems(TNode n
, set
<TNode
>& skolemSet
, unordered_map
<Node
, bool, NodeHashFunction
>& cache
)
3986 unordered_map
<Node
, bool, NodeHashFunction
>::iterator it
;
3988 if (it
!= cache
.end()) {
3992 size_t sz
= n
.getNumChildren();
3994 IteSkolemMap::iterator it
= d_iteSkolemMap
.find(n
);
3995 if (it
!= d_iteSkolemMap
.end()) {
3996 skolemSet
.insert(n
);
4003 for (; k
< sz
; ++k
) {
4004 collectSkolems(n
[k
], skolemSet
, cache
);
4010 bool SmtEnginePrivate::checkForBadSkolems(TNode n
, TNode skolem
, unordered_map
<Node
, bool, NodeHashFunction
>& cache
)
4012 unordered_map
<Node
, bool, NodeHashFunction
>::iterator it
;
4014 if (it
!= cache
.end()) {
4015 return (*it
).second
;
4018 size_t sz
= n
.getNumChildren();
4020 IteSkolemMap::iterator it
= d_iteSkolemMap
.find(n
);
4022 if (it
!= d_iteSkolemMap
.end()) {
4023 if (!((*it
).first
< n
)) {
4032 for (; k
< sz
; ++k
) {
4033 if (checkForBadSkolems(n
[k
], skolem
, cache
)) {
4043 void SmtEnginePrivate::processAssertions() {
4044 TimerStat::CodeTimer
paTimer(d_smt
.d_stats
->d_processAssertionsTime
);
4045 spendResource(options::preprocessStep());
4046 Assert(d_smt
.d_fullyInited
);
4047 Assert(d_smt
.d_pendingPops
== 0);
4048 SubstitutionMap
& top_level_substs
= d_assertions
.getTopLevelSubstitutions();
4050 // Dump the assertions
4051 dumpAssertions("pre-everything", d_assertions
);
4053 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() begin" << endl
;
4054 Trace("smt") << "SmtEnginePrivate::processAssertions()" << endl
;
4056 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
4058 if (d_assertions
.size() == 0) {
4063 if (options::bvGaussElim())
4065 TimerStat::CodeTimer
gaussElimTimer(d_smt
.d_stats
->d_gaussElimTime
);
4066 d_preprocessingPassRegistry
.getPass("bv-gauss")->apply(&d_assertions
);
4069 if (d_assertionsProcessed
&& options::incrementalSolving()) {
4070 // TODO(b/1255): Substitutions in incremental mode should be managed with a
4071 // proper data structure.
4073 // Placeholder for storing substitutions
4074 d_assertions
.getSubstitutionsIndex() = d_assertions
.size();
4075 d_assertions
.push_back(NodeManager::currentNM()->mkConst
<bool>(true));
4078 // Add dummy assertion in last position - to be used as a
4079 // placeholder for any new assertions to get added
4080 d_assertions
.push_back(NodeManager::currentNM()->mkConst
<bool>(true));
4081 // any assertions added beyond realAssertionsEnd must NOT affect the
4082 // equisatisfiability
4083 d_realAssertionsEnd
= d_assertions
.size();
4085 // Assertions are NOT guaranteed to be rewritten by this point
4087 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-definition-expansion" << endl
;
4088 dumpAssertions("pre-definition-expansion", d_assertions
);
4090 Chat() << "expanding definitions..." << endl
;
4091 Trace("simplify") << "SmtEnginePrivate::simplify(): expanding definitions" << endl
;
4092 TimerStat::CodeTimer
codeTimer(d_smt
.d_stats
->d_definitionExpansionTime
);
4093 unordered_map
<Node
, Node
, NodeHashFunction
> cache
;
4094 for(unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
4095 d_assertions
.replace(i
, expandDefinitions(d_assertions
[i
], cache
));
4098 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-definition-expansion" << endl
;
4099 dumpAssertions("post-definition-expansion", d_assertions
);
4101 // save the assertions now
4104 for (unsigned i
= 0; i
< d_assertions
.size(); ++i
) {
4105 ProofManager::currentPM()->addAssertion(d_assertions
[i
].toExpr());
4109 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
4111 if (options::globalNegate())
4113 // global negation of the formula
4114 quantifiers::GlobalNegate gn
;
4115 gn
.simplify(d_assertions
.ref());
4116 d_smt
.d_globalNegation
= !d_smt
.d_globalNegation
;
4119 if( options::nlExtPurify() ){
4120 unordered_map
<Node
, Node
, NodeHashFunction
> cache
;
4121 unordered_map
<Node
, Node
, NodeHashFunction
> bcache
;
4122 std::vector
< Node
> var_eq
;
4123 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
4124 Node a
= d_assertions
[i
];
4125 d_assertions
.replace(i
, purifyNlTerms(a
, cache
, bcache
, var_eq
));
4126 Trace("nl-ext-purify")
4127 << "Purify : " << a
<< " -> " << d_assertions
[i
] << std::endl
;
4129 if( !var_eq
.empty() ){
4130 unsigned lastIndex
= d_assertions
.size()-1;
4131 var_eq
.insert( var_eq
.begin(), d_assertions
[lastIndex
] );
4132 d_assertions
.replace(lastIndex
, NodeManager::currentNM()->mkNode( kind::AND
, var_eq
) );
4136 if( options::ceGuidedInst() ){
4137 //register sygus conjecture pre-rewrite (motivated by solution reconstruction)
4138 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
4139 d_smt
.d_theoryEngine
->getQuantifiersEngine()->getCegInstantiation()->preregisterAssertion( d_assertions
[i
] );
4143 if (options::solveRealAsInt()) {
4144 d_preprocessingPassRegistry
.getPass("real-to-int")->apply(&d_assertions
);
4147 if (options::solveIntAsBV() > 0)
4149 d_preprocessingPassRegistry
.getPass("int-to-bv")->apply(&d_assertions
);
4152 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
&&
4153 !d_smt
.d_logic
.isPure(THEORY_BV
) &&
4154 d_smt
.d_logic
.getLogicString() != "QF_UFBV" &&
4155 d_smt
.d_logic
.getLogicString() != "QF_ABV") {
4156 throw ModalException("Eager bit-blasting does not currently support theory combination. "
4157 "Note that in a QF_BV problem UF symbols can be introduced for division. "
4158 "Try --bv-div-zero-const to interpret division by zero as a constant.");
4161 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
4162 && !options::incrementalSolving())
4164 d_preprocessingPassRegistry
.getPass("bv-ackermann")->apply(&d_assertions
);
4167 if (options::bvAbstraction() && !options::incrementalSolving())
4169 d_preprocessingPassRegistry
.getPass("bv-abstraction")->apply(&d_assertions
);
4172 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
4174 bool noConflict
= true;
4176 if (options::extRewPrep())
4178 theory::quantifiers::ExtendedRewriter
extr(options::extRewPrepAgg());
4179 for (unsigned i
= 0; i
< d_assertions
.size(); ++i
)
4181 Node a
= d_assertions
[i
];
4182 d_assertions
.replace(i
, extr
.extendedRewrite(a
));
4186 // Unconstrained simplification
4187 if(options::unconstrainedSimp()) {
4188 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-unconstrained-simp" << endl
;
4189 dumpAssertions("pre-unconstrained-simp", d_assertions
);
4190 d_preprocessingPassRegistry
.getPass("rewrite")->apply(&d_assertions
);
4191 unconstrainedSimp();
4192 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-unconstrained-simp" << endl
;
4193 dumpAssertions("post-unconstrained-simp", d_assertions
);
4196 if(options::bvIntroducePow2())
4198 d_preprocessingPassRegistry
.getPass("bv-intro-pow2")->apply(&d_assertions
);
4201 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-substitution" << endl
;
4202 dumpAssertions("pre-substitution", d_assertions
);
4204 if (options::unsatCores())
4206 // special rewriting pass for unsat cores, since many of the passes below
4208 d_preprocessingPassRegistry
.getPass("rewrite")->apply(&d_assertions
);
4212 d_preprocessingPassRegistry
.getPass("apply-substs")->apply(&d_assertions
);
4214 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-substitution" << endl
;
4215 dumpAssertions("post-substitution", d_assertions
);
4217 // Assertions ARE guaranteed to be rewritten by this point
4218 #ifdef CVC4_ASSERTIONS
4219 for (unsigned i
= 0; i
< d_assertions
.size(); ++i
)
4221 Assert(Rewriter::rewrite(d_assertions
[i
]) == d_assertions
[i
]);
4225 // Lift bit-vectors of size 1 to bool
4226 if(options::bitvectorToBool()) {
4227 dumpAssertions("pre-bv-to-bool", d_assertions
);
4228 Chat() << "...doing bvToBool..." << endl
;
4229 d_preprocessingPassRegistry
.getPass("bv-to-bool")->apply(&d_assertions
);
4230 dumpAssertions("post-bv-to-bool", d_assertions
);
4231 Trace("smt") << "POST bvToBool" << endl
;
4233 // Convert non-top-level Booleans to bit-vectors of size 1
4234 if(options::boolToBitvector()) {
4235 dumpAssertions("pre-bool-to-bv", d_assertions
);
4236 Chat() << "...doing boolToBv..." << endl
;
4237 d_preprocessingPassRegistry
.getPass("bool-to-bv")->apply(&d_assertions
);
4238 dumpAssertions("post-bool-to-bv", d_assertions
);
4239 Trace("smt") << "POST boolToBv" << endl
;
4241 if(options::sepPreSkolemEmp()) {
4242 d_preprocessingPassRegistry
.getPass("sep-skolem-emp")->apply(&d_assertions
);
4245 if( d_smt
.d_logic
.isQuantified() ){
4246 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-quant-preprocess" << endl
;
4248 dumpAssertions("pre-skolem-quant", d_assertions
);
4249 //remove rewrite rules, apply pre-skolemization to existential quantifiers
4250 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
4251 Node prev
= d_assertions
[i
];
4252 Node next
= quantifiers::QuantifiersRewriter::preprocess( prev
);
4254 d_assertions
.replace( i
, Rewriter::rewrite( next
) );
4255 Trace("quantifiers-preprocess") << "*** Pre-skolemize " << prev
<< endl
;
4256 Trace("quantifiers-preprocess") << " ...got " << d_assertions
[i
] << endl
;
4259 dumpAssertions("post-skolem-quant", d_assertions
);
4260 if( options::macrosQuant() ){
4261 //quantifiers macro expansion
4262 quantifiers::QuantifierMacros
qm( d_smt
.d_theoryEngine
->getQuantifiersEngine() );
4265 success
= qm
.simplify( d_assertions
.ref(), true );
4267 //finalize the definitions
4268 qm
.finalizeDefinitions();
4271 //fmf-fun : assume admissible functions, applying preprocessing reduction to FMF
4272 if( options::fmfFunWellDefined() ){
4273 quantifiers::FunDefFmf fdf
;
4274 Assert( d_smt
.d_fmfRecFunctionsDefined
!=NULL
);
4275 //must carry over current definitions (for incremental)
4276 for( context::CDList
<Node
>::const_iterator fit
= d_smt
.d_fmfRecFunctionsDefined
->begin();
4277 fit
!= d_smt
.d_fmfRecFunctionsDefined
->end(); ++fit
) {
4279 Assert( d_smt
.d_fmfRecFunctionsAbs
.find( f
)!=d_smt
.d_fmfRecFunctionsAbs
.end() );
4280 TypeNode ft
= d_smt
.d_fmfRecFunctionsAbs
[f
];
4281 fdf
.d_sorts
[f
] = ft
;
4282 std::map
< Node
, std::vector
< Node
> >::iterator fcit
= d_smt
.d_fmfRecFunctionsConcrete
.find( f
);
4283 Assert( fcit
!=d_smt
.d_fmfRecFunctionsConcrete
.end() );
4284 for( unsigned j
=0; j
<fcit
->second
.size(); j
++ ){
4285 fdf
.d_input_arg_inj
[f
].push_back( fcit
->second
[j
] );
4288 fdf
.simplify( d_assertions
.ref() );
4289 //must store new definitions (for incremental)
4290 for( unsigned i
=0; i
<fdf
.d_funcs
.size(); i
++ ){
4291 Node f
= fdf
.d_funcs
[i
];
4292 d_smt
.d_fmfRecFunctionsAbs
[f
] = fdf
.d_sorts
[f
];
4293 d_smt
.d_fmfRecFunctionsConcrete
[f
].clear();
4294 for( unsigned j
=0; j
<fdf
.d_input_arg_inj
[f
].size(); j
++ ){
4295 d_smt
.d_fmfRecFunctionsConcrete
[f
].push_back( fdf
.d_input_arg_inj
[f
][j
] );
4297 d_smt
.d_fmfRecFunctionsDefined
->push_back( f
);
4300 if (options::sygusInference())
4302 // try recast as sygus
4303 quantifiers::SygusInference si
;
4304 if (si
.simplify(d_assertions
.ref()))
4306 Trace("smt-proc") << "...converted to sygus conjecture." << std::endl
;
4309 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-quant-preprocess" << endl
;
4312 if( options::sortInference() || options::ufssFairnessMonotone() ){
4313 //sort inference technique
4314 SortInference
* si
= d_smt
.d_theoryEngine
->getSortInference();
4315 si
->simplify( d_assertions
.ref(), options::sortInference(), options::ufssFairnessMonotone() );
4316 for( std::map
< Node
, Node
>::iterator it
= si
->d_model_replace_f
.begin(); it
!= si
->d_model_replace_f
.end(); ++it
){
4317 d_smt
.setPrintFuncInModel( it
->first
.toExpr(), false );
4318 d_smt
.setPrintFuncInModel( it
->second
.toExpr(), true );
4322 if( options::pbRewrites() ){
4323 d_preprocessingPassRegistry
.getPass("pseudo-boolean-processor")
4324 ->apply(&d_assertions
);
4327 if (options::synthRrPrep())
4329 // do candidate rewrite rule synthesis
4330 d_preprocessingPassRegistry
.getPass("synth-rr")->apply(&d_assertions
);
4333 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-simplify" << endl
;
4334 dumpAssertions("pre-simplify", d_assertions
);
4335 Chat() << "simplifying assertions..." << endl
;
4336 noConflict
= simplifyAssertions();
4338 ++(d_smt
.d_stats
->d_simplifiedToFalse
);
4340 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-simplify" << endl
;
4341 dumpAssertions("post-simplify", d_assertions
);
4343 if (options::symmetryBreakerExp() && !options::incrementalSolving())
4345 // apply symmetry breaking if not in incremental mode
4346 d_preprocessingPassRegistry
.getPass("sym-break")->apply(&d_assertions
);
4349 if(options::doStaticLearning()) {
4350 d_preprocessingPassRegistry
.getPass("static-learning")
4351 ->apply(&d_assertions
);
4353 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
4355 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-ite-removal" << endl
;
4356 dumpAssertions("pre-ite-removal", d_assertions
);
4358 Chat() << "removing term ITEs..." << endl
;
4359 TimerStat::CodeTimer
codeTimer(d_smt
.d_stats
->d_iteRemovalTime
);
4360 // Remove ITEs, updating d_iteSkolemMap
4361 d_smt
.d_stats
->d_numAssertionsPre
+= d_assertions
.size();
4363 // This is needed because when solving incrementally, removeITEs may introduce
4364 // skolems that were solved for earlier and thus appear in the substitution
4366 d_preprocessingPassRegistry
.getPass("apply-substs")->apply(&d_assertions
);
4367 d_smt
.d_stats
->d_numAssertionsPost
+= d_assertions
.size();
4369 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-ite-removal" << endl
;
4370 dumpAssertions("post-ite-removal", d_assertions
);
4372 dumpAssertions("pre-repeat-simplify", d_assertions
);
4373 if(options::repeatSimp()) {
4374 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-repeat-simplify" << endl
;
4375 Chat() << "re-simplifying assertions..." << endl
;
4376 ScopeCounter
depth(d_simplifyAssertionsDepth
);
4377 noConflict
&= simplifyAssertions();
4379 // Need to fix up assertion list to maintain invariants:
4380 // Let Sk be the set of Skolem variables introduced by ITE's. Let <_sk be the order in which these variables were introduced
4381 // during ite removal.
4382 // For each skolem variable sk, let iteExpr = iteMap(sk) be the ite expr mapped to by sk.
4384 // cache for expression traversal
4385 unordered_map
<Node
, bool, NodeHashFunction
> cache
;
4387 // First, find all skolems that appear in the substitution map - their associated iteExpr will need
4388 // to be moved to the main assertion set
4389 set
<TNode
> skolemSet
;
4390 SubstitutionMap::iterator pos
= top_level_substs
.begin();
4391 for (; pos
!= top_level_substs
.end(); ++pos
)
4393 collectSkolems((*pos
).first
, skolemSet
, cache
);
4394 collectSkolems((*pos
).second
, skolemSet
, cache
);
4397 // We need to ensure:
4398 // 1. iteExpr has the form (ite cond (sk = t) (sk = e))
4399 // 2. if some sk' in Sk appears in cond, t, or e, then sk' <_sk sk
4400 // If either of these is violated, we must add iteExpr as a proper assertion
4401 IteSkolemMap::iterator it
= d_iteSkolemMap
.begin();
4402 IteSkolemMap::iterator iend
= d_iteSkolemMap
.end();
4403 NodeBuilder
<> builder(kind::AND
);
4404 builder
<< d_assertions
[d_realAssertionsEnd
- 1];
4405 vector
<TNode
> toErase
;
4406 for (; it
!= iend
; ++it
) {
4407 if (skolemSet
.find((*it
).first
) == skolemSet
.end()) {
4408 TNode iteExpr
= d_assertions
[(*it
).second
];
4409 if (iteExpr
.getKind() == kind::ITE
&&
4410 iteExpr
[1].getKind() == kind::EQUAL
&&
4411 iteExpr
[1][0] == (*it
).first
&&
4412 iteExpr
[2].getKind() == kind::EQUAL
&&
4413 iteExpr
[2][0] == (*it
).first
) {
4415 bool bad
= checkForBadSkolems(iteExpr
[0], (*it
).first
, cache
);
4416 bad
= bad
|| checkForBadSkolems(iteExpr
[1][1], (*it
).first
, cache
);
4417 bad
= bad
|| checkForBadSkolems(iteExpr
[2][1], (*it
).first
, cache
);
4423 // Move this iteExpr into the main assertions
4424 builder
<< d_assertions
[(*it
).second
];
4425 d_assertions
[(*it
).second
] = NodeManager::currentNM()->mkConst
<bool>(true);
4426 toErase
.push_back((*it
).first
);
4428 if(builder
.getNumChildren() > 1) {
4429 while (!toErase
.empty()) {
4430 d_iteSkolemMap
.erase(toErase
.back());
4433 d_assertions
[d_realAssertionsEnd
- 1] = Rewriter::rewrite(Node(builder
));
4435 // TODO(b/1256): For some reason this is needed for some benchmarks, such as
4436 // QF_AUFBV/dwp_formulas/try5_small_difret_functions_dwp_tac.re_node_set_remove_at.il.dwp.smt2
4438 d_preprocessingPassRegistry
.getPass("apply-substs")->apply(&d_assertions
);
4439 // Assert(iteRewriteAssertionsEnd == d_assertions.size());
4441 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-repeat-simplify" << endl
;
4443 dumpAssertions("post-repeat-simplify", d_assertions
);
4445 dumpAssertions("pre-rewrite-apply-to-const", d_assertions
);
4446 if(options::rewriteApplyToConst()) {
4447 Chat() << "Rewriting applies to constants..." << endl
;
4448 TimerStat::CodeTimer
codeTimer(d_smt
.d_stats
->d_rewriteApplyToConstTime
);
4449 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
4450 d_assertions
[i
] = Rewriter::rewrite(rewriteApplyToConst(d_assertions
[i
]));
4453 dumpAssertions("post-rewrite-apply-to-const", d_assertions
);
4455 // begin: INVARIANT to maintain: no reordering of assertions or
4456 // introducing new ones
4457 #ifdef CVC4_ASSERTIONS
4458 unsigned iteRewriteAssertionsEnd
= d_assertions
.size();
4461 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
4463 Debug("smt") << "SmtEnginePrivate::processAssertions() POST SIMPLIFICATION" << endl
;
4464 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
4466 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-theory-preprocessing" << endl
;
4467 dumpAssertions("pre-theory-preprocessing", d_assertions
);
4469 Chat() << "theory preprocessing..." << endl
;
4470 TimerStat::CodeTimer
codeTimer(d_smt
.d_stats
->d_theoryPreprocessTime
);
4471 // Call the theory preprocessors
4472 d_smt
.d_theoryEngine
->preprocessStart();
4473 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
4474 d_assertions
.replace(i
, d_smt
.d_theoryEngine
->preprocess(d_assertions
[i
]));
4477 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-theory-preprocessing" << endl
;
4478 dumpAssertions("post-theory-preprocessing", d_assertions
);
4480 // If we are using eager bit-blasting wrap assertions in fake atom so that
4481 // everything gets bit-blasted to internal SAT solver
4482 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
) {
4483 for (unsigned i
= 0; i
< d_assertions
.size(); ++i
) {
4484 TNode atom
= d_assertions
[i
];
4485 Node eager_atom
= NodeManager::currentNM()->mkNode(kind::BITVECTOR_EAGER_ATOM
, atom
);
4486 d_assertions
.replace(i
, eager_atom
);
4487 TheoryModel
* m
= d_smt
.d_theoryEngine
->getModel();
4488 m
->addSubstitution(eager_atom
, atom
);
4492 //notify theory engine new preprocessed assertions
4493 d_smt
.d_theoryEngine
->notifyPreprocessedAssertions( d_assertions
.ref() );
4495 // Push the formula to decision engine
4497 Chat() << "pushing to decision engine..." << endl
;
4498 Assert(iteRewriteAssertionsEnd
== d_assertions
.size());
4499 d_smt
.d_decisionEngine
->addAssertions
4500 (d_assertions
.ref(), d_realAssertionsEnd
, d_iteSkolemMap
);
4503 // end: INVARIANT to maintain: no reordering of assertions or
4504 // introducing new ones
4506 Trace("smt-proc") << "SmtEnginePrivate::processAssertions() end" << endl
;
4507 dumpAssertions("post-everything", d_assertions
);
4509 // Push the formula to SAT
4511 Chat() << "converting to CNF..." << endl
;
4512 TimerStat::CodeTimer
codeTimer(d_smt
.d_stats
->d_cnfConversionTime
);
4513 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
4514 Chat() << "+ " << d_assertions
[i
] << std::endl
;
4515 d_smt
.d_propEngine
->assertFormula(d_assertions
[i
]);
4519 d_assertionsProcessed
= true;
4521 d_assertions
.clear();
4522 d_iteSkolemMap
.clear();
4525 void SmtEnginePrivate::addFormula(TNode n
, bool inUnsatCore
, bool inInput
)
4532 Trace("smt") << "SmtEnginePrivate::addFormula(" << n
<< "), inUnsatCore = " << inUnsatCore
<< ", inInput = " << inInput
<< endl
;
4534 // Give it to proof manager
4537 // n is an input assertion
4538 if (inUnsatCore
|| options::unsatCores() || options::dumpUnsatCores() || options::checkUnsatCores() || options::fewerPreprocessingHoles()) {
4540 ProofManager::currentPM()->addCoreAssertion(n
.toExpr());
4543 // n is the result of an unknown preprocessing step, add it to dependency map to null
4544 ProofManager::currentPM()->addDependence(n
, Node::null());
4546 // rewrite rules are by default in the unsat core because
4547 // they need to be applied until saturation
4548 if(options::unsatCores() &&
4549 n
.getKind() == kind::REWRITE_RULE
){
4550 ProofManager::currentPM()->addUnsatCore(n
.toExpr());
4554 // Add the normalized formula to the queue
4555 d_assertions
.push_back(n
);
4556 //d_assertions.push_back(Rewriter::rewrite(n));
4559 void SmtEngine::ensureBoolean(const Expr
& e
)
4561 Type type
= e
.getType(options::typeChecking());
4562 Type boolType
= d_exprManager
->booleanType();
4563 if(type
!= boolType
) {
4565 ss
<< "Expected " << boolType
<< "\n"
4566 << "The assertion : " << e
<< "\n"
4567 << "Its type : " << type
;
4568 throw TypeCheckingException(e
, ss
.str());
4572 Result
SmtEngine::checkSat(const Expr
& assumption
, bool inUnsatCore
)
4574 return checkSatisfiability(assumption
, inUnsatCore
, false);
4577 Result
SmtEngine::checkSat(const vector
<Expr
>& assumptions
, bool inUnsatCore
)
4579 return checkSatisfiability(assumptions
, inUnsatCore
, false);
4582 Result
SmtEngine::query(const Expr
& assumption
, bool inUnsatCore
)
4584 Assert(!assumption
.isNull());
4585 return checkSatisfiability(assumption
, inUnsatCore
, true);
4588 Result
SmtEngine::query(const vector
<Expr
>& assumptions
, bool inUnsatCore
)
4590 return checkSatisfiability(assumptions
, inUnsatCore
, true);
4593 Result
SmtEngine::checkSatisfiability(const Expr
& expr
,
4597 return checkSatisfiability(
4598 expr
.isNull() ? vector
<Expr
>() : vector
<Expr
>{expr
},
4603 Result
SmtEngine::checkSatisfiability(const vector
<Expr
>& assumptions
,
4609 SmtScope
smts(this);
4610 finalOptionsAreSet();
4613 Trace("smt") << "SmtEngine::" << (isQuery
? "query" : "checkSat") << "("
4614 << assumptions
<< ")" << endl
;
4616 if(d_queryMade
&& !options::incrementalSolving()) {
4617 throw ModalException("Cannot make multiple queries unless "
4618 "incremental solving is enabled "
4619 "(try --incremental)");
4622 // check to see if a postsolve() is pending
4623 if(d_needPostsolve
) {
4624 d_theoryEngine
->postsolve();
4625 d_needPostsolve
= false;
4627 // Note that a query has been made
4629 // reset global negation
4630 d_globalNegation
= false;
4632 bool didInternalPush
= false;
4634 setProblemExtended(true);
4638 size_t size
= assumptions
.size();
4641 /* Assume: not (BIGAND assumptions) */
4642 d_assumptions
.push_back(
4643 d_exprManager
->mkExpr(kind::AND
, assumptions
).notExpr());
4647 /* Assume: not expr */
4648 d_assumptions
.push_back(assumptions
[0].notExpr());
4653 /* Assume: BIGAND assumptions */
4654 d_assumptions
= assumptions
;
4657 if (!d_assumptions
.empty())
4660 didInternalPush
= true;
4663 Result
r(Result::SAT_UNKNOWN
, Result::UNKNOWN_REASON
);
4664 for (Expr e
: d_assumptions
)
4666 // Substitute out any abstract values in ex.
4667 e
= d_private
->substituteAbstractValues(Node::fromExpr(e
)).toExpr();
4668 Assert(e
.getExprManager() == d_exprManager
);
4669 // Ensure expr is type-checked at this point.
4672 /* Add assumption */
4673 if (d_assertionList
!= NULL
)
4675 d_assertionList
->push_back(e
);
4677 d_private
->addFormula(e
.getNode(), inUnsatCore
);
4680 r
= isQuery
? check().asValidityResult() : check().asSatisfiabilityResult();
4682 if ((options::solveRealAsInt() || options::solveIntAsBV() > 0)
4683 && r
.asSatisfiabilityResult().isSat() == Result::UNSAT
)
4685 r
= Result(Result::SAT_UNKNOWN
, Result::UNKNOWN_REASON
);
4687 // flipped if we did a global negation
4688 if (d_globalNegation
)
4690 Trace("smt") << "SmtEngine::process global negate " << r
<< std::endl
;
4691 if (r
.asSatisfiabilityResult().isSat() == Result::UNSAT
)
4693 r
= Result(Result::SAT
);
4695 else if (r
.asSatisfiabilityResult().isSat() == Result::SAT
)
4697 // only if satisfaction complete
4698 if (d_logic
.isPure(THEORY_ARITH
) || d_logic
.isPure(THEORY_BV
))
4700 r
= Result(Result::UNSAT
);
4704 r
= Result(Result::SAT_UNKNOWN
, Result::UNKNOWN_REASON
);
4707 Trace("smt") << "SmtEngine::global negate returned " << r
<< std::endl
;
4710 d_needPostsolve
= true;
4712 // Dump the query if requested
4713 if (Dump
.isOn("benchmark"))
4715 size_t size
= assumptions
.size();
4716 // the expr already got dumped out if assertion-dumping is on
4717 if (isQuery
&& size
== 1)
4719 Dump("benchmark") << QueryCommand(assumptions
[0]);
4723 Dump("benchmark") << CheckSatCommand();
4727 Dump("benchmark") << CheckSatAssumingCommand(d_assumptions
,
4732 d_propEngine
->resetTrail();
4735 if (didInternalPush
)
4740 // Remember the status
4743 setProblemExtended(false);
4745 Trace("smt") << "SmtEngine::" << (isQuery
? "query" : "checkSat") << "("
4746 << assumptions
<< ") => " << r
<< endl
;
4748 // Check that SAT results generate a model correctly.
4749 if(options::checkModels()) {
4750 // TODO (#1693) check model when unknown result?
4751 if (r
.asSatisfiabilityResult().isSat() == Result::SAT
)
4756 // Check that UNSAT results generate a proof correctly.
4757 if(options::checkProofs()) {
4758 if(r
.asSatisfiabilityResult().isSat() == Result::UNSAT
) {
4759 TimerStat::CodeTimer
checkProofTimer(d_stats
->d_checkProofTime
);
4763 // Check that UNSAT results generate an unsat core correctly.
4764 if(options::checkUnsatCores()) {
4765 if(r
.asSatisfiabilityResult().isSat() == Result::UNSAT
) {
4766 TimerStat::CodeTimer
checkUnsatCoreTimer(d_stats
->d_checkUnsatCoreTime
);
4770 // Check that synthesis solutions satisfy the conjecture
4771 if (options::checkSynthSol()
4772 && r
.asSatisfiabilityResult().isSat() == Result::UNSAT
)
4774 checkSynthSolution();
4778 } catch (UnsafeInterruptException
& e
) {
4779 AlwaysAssert(d_private
->getResourceManager()->out());
4780 Result::UnknownExplanation why
= d_private
->getResourceManager()->outOfResources() ?
4781 Result::RESOURCEOUT
: Result::TIMEOUT
;
4782 return Result(Result::SAT_UNKNOWN
, why
, d_filename
);
4786 vector
<Expr
> SmtEngine::getUnsatAssumptions(void)
4788 Trace("smt") << "SMT getUnsatAssumptions()" << endl
;
4789 SmtScope
smts(this);
4790 if (!options::unsatAssumptions())
4792 throw ModalException(
4793 "Cannot get unsat assumptions when produce-unsat-assumptions option "
4796 if (d_status
.isNull()
4797 || d_status
.asSatisfiabilityResult() != Result::UNSAT
4798 || d_problemExtended
)
4800 throw RecoverableModalException(
4801 "Cannot get unsat assumptions unless immediately preceded by "
4802 "UNSAT/VALID response.");
4804 finalOptionsAreSet();
4805 if (Dump
.isOn("benchmark"))
4807 Dump("benchmark") << GetUnsatCoreCommand();
4809 UnsatCore core
= getUnsatCore();
4811 for (const Expr
& e
: d_assumptions
)
4813 if (find(core
.begin(), core
.end(), e
) != core
.end()) { res
.push_back(e
); }
4818 Result
SmtEngine::checkSynth(const Expr
& e
)
4820 SmtScope
smts(this);
4821 Trace("smt") << "Check synth: " << e
<< std::endl
;
4822 Trace("smt-synth") << "Check synthesis conjecture: " << e
<< std::endl
;
4824 if (options::sygusQePreproc())
4826 // the following does quantifier elimination as a preprocess step
4827 // for "non-ground single invocation synthesis conjectures":
4828 // exists f. forall xy. P[ f(x), x, y ]
4829 // We run quantifier elimination:
4830 // exists y. P[ z, x, y ] ----> Q[ z, x ]
4831 // Where we replace the original conjecture with:
4832 // exists f. forall x. Q[ f(x), x ]
4833 // For more details, see Example 6 of Reynolds et al. SYNT 2017.
4834 Node conj
= Node::fromExpr(e
);
4835 if (conj
.getKind() == kind::FORALL
&& conj
[1].getKind() == kind::EXISTS
)
4837 Node conj_se
= Node::fromExpr(expandDefinitions(conj
[1][1].toExpr()));
4839 Trace("smt-synth") << "Compute single invocation for " << conj_se
<< "..."
4841 quantifiers::SingleInvocationPartition sip
;
4842 std::vector
<Node
> funcs
;
4843 funcs
.insert(funcs
.end(), conj
[0].begin(), conj
[0].end());
4844 sip
.init(funcs
, conj_se
.negate());
4845 Trace("smt-synth") << "...finished, got:" << std::endl
;
4846 sip
.debugPrint("smt-synth");
4848 if (!sip
.isPurelySingleInvocation() && sip
.isNonGroundSingleInvocation())
4850 // create new smt engine to do quantifier elimination
4851 SmtEngine
smt_qe(d_exprManager
);
4852 smt_qe
.setLogic(getLogicInfo());
4853 Trace("smt-synth") << "Property is non-ground single invocation, run "
4854 "QE to obtain single invocation."
4856 NodeManager
* nm
= NodeManager::currentNM();
4857 // partition variables
4858 std::vector
<Node
> all_vars
;
4859 sip
.getAllVariables(all_vars
);
4860 std::vector
<Node
> si_vars
;
4861 sip
.getSingleInvocationVariables(si_vars
);
4862 std::vector
<Node
> qe_vars
;
4863 std::vector
<Node
> nqe_vars
;
4864 for (unsigned i
= 0, size
= all_vars
.size(); i
< size
; i
++)
4866 Node v
= all_vars
[i
];
4867 if (std::find(si_vars
.begin(), si_vars
.end(), v
) == si_vars
.end())
4869 qe_vars
.push_back(v
);
4873 nqe_vars
.push_back(v
);
4876 std::vector
<Node
> orig
;
4877 std::vector
<Node
> subs
;
4878 // skolemize non-qe variables
4879 for (unsigned i
= 0; i
< nqe_vars
.size(); i
++)
4881 Node k
= nm
->mkSkolem("k",
4882 nqe_vars
[i
].getType(),
4883 "qe for non-ground single invocation");
4884 orig
.push_back(nqe_vars
[i
]);
4886 Trace("smt-synth") << " subs : " << nqe_vars
[i
] << " -> " << k
4889 std::vector
<Node
> funcs
;
4890 sip
.getFunctions(funcs
);
4891 for (unsigned i
= 0, size
= funcs
.size(); i
< size
; i
++)
4894 Node fi
= sip
.getFunctionInvocationFor(f
);
4895 Node fv
= sip
.getFirstOrderVariableForFunction(f
);
4896 Assert(!fi
.isNull());
4901 "qe for function in non-ground single invocation");
4903 Trace("smt-synth") << " subs : " << fi
<< " -> " << k
<< std::endl
;
4905 Node conj_se_ngsi
= sip
.getFullSpecification();
4906 Trace("smt-synth") << "Full specification is " << conj_se_ngsi
4908 Node conj_se_ngsi_subs
= conj_se_ngsi
.substitute(
4909 orig
.begin(), orig
.end(), subs
.begin(), subs
.end());
4910 Assert(!qe_vars
.empty());
4912 nm
->mkNode(kind::EXISTS
,
4913 nm
->mkNode(kind::BOUND_VAR_LIST
, qe_vars
),
4914 conj_se_ngsi_subs
.negate());
4916 Trace("smt-synth") << "Run quantifier elimination on "
4917 << conj_se_ngsi_subs
<< std::endl
;
4918 Expr qe_res
= smt_qe
.doQuantifierElimination(
4919 conj_se_ngsi_subs
.toExpr(), true, false);
4920 Trace("smt-synth") << "Result : " << qe_res
<< std::endl
;
4922 // create single invocation conjecture
4923 Node qe_res_n
= Node::fromExpr(qe_res
);
4924 qe_res_n
= qe_res_n
.substitute(
4925 subs
.begin(), subs
.end(), orig
.begin(), orig
.end());
4926 if (!nqe_vars
.empty())
4928 qe_res_n
= nm
->mkNode(kind::EXISTS
,
4929 nm
->mkNode(kind::BOUND_VAR_LIST
, nqe_vars
),
4932 Assert(conj
.getNumChildren() == 3);
4933 qe_res_n
= nm
->mkNode(kind::FORALL
, conj
[0], qe_res_n
, conj
[2]);
4934 Trace("smt-synth") << "Converted conjecture after QE : " << qe_res_n
4936 e_check
= qe_res_n
.toExpr();
4941 return checkSatisfiability( e_check
, true, false );
4944 Result
SmtEngine::assertFormula(const Expr
& ex
, bool inUnsatCore
)
4946 Assert(ex
.getExprManager() == d_exprManager
);
4947 SmtScope
smts(this);
4948 finalOptionsAreSet();
4951 Trace("smt") << "SmtEngine::assertFormula(" << ex
<< ")" << endl
;
4953 if (Dump
.isOn("raw-benchmark")) {
4954 Dump("raw-benchmark") << AssertCommand(ex
);
4957 // Substitute out any abstract values in ex
4958 Expr e
= d_private
->substituteAbstractValues(Node::fromExpr(ex
)).toExpr();
4961 if(d_assertionList
!= NULL
) {
4962 d_assertionList
->push_back(e
);
4964 d_private
->addFormula(e
.getNode(), inUnsatCore
);
4965 return quickCheck().asValidityResult();
4966 }/* SmtEngine::assertFormula() */
4968 Node
SmtEngine::postprocess(TNode node
, TypeNode expectedType
) const {
4972 Expr
SmtEngine::simplify(const Expr
& ex
)
4974 Assert(ex
.getExprManager() == d_exprManager
);
4975 SmtScope
smts(this);
4976 finalOptionsAreSet();
4978 Trace("smt") << "SMT simplify(" << ex
<< ")" << endl
;
4980 if(Dump
.isOn("benchmark")) {
4981 Dump("benchmark") << SimplifyCommand(ex
);
4984 Expr e
= d_private
->substituteAbstractValues(Node::fromExpr(ex
)).toExpr();
4985 if( options::typeChecking() ) {
4986 e
.getType(true); // ensure expr is type-checked at this point
4989 // Make sure all preprocessing is done
4990 d_private
->processAssertions();
4991 Node n
= d_private
->simplify(Node::fromExpr(e
));
4992 n
= postprocess(n
, TypeNode::fromType(e
.getType()));
4996 Expr
SmtEngine::expandDefinitions(const Expr
& ex
)
4998 d_private
->spendResource(options::preprocessStep());
5000 Assert(ex
.getExprManager() == d_exprManager
);
5001 SmtScope
smts(this);
5002 finalOptionsAreSet();
5004 Trace("smt") << "SMT expandDefinitions(" << ex
<< ")" << endl
;
5006 // Substitute out any abstract values in ex.
5007 Expr e
= d_private
->substituteAbstractValues(Node::fromExpr(ex
)).toExpr();
5008 if(options::typeChecking()) {
5009 // Ensure expr is type-checked at this point.
5012 if(Dump
.isOn("benchmark")) {
5013 Dump("benchmark") << ExpandDefinitionsCommand(e
);
5015 unordered_map
<Node
, Node
, NodeHashFunction
> cache
;
5016 Node n
= d_private
->expandDefinitions(Node::fromExpr(e
), cache
, /* expandOnly = */ true);
5017 n
= postprocess(n
, TypeNode::fromType(e
.getType()));
5022 // TODO(#1108): Simplify the error reporting of this method.
5023 Expr
SmtEngine::getValue(const Expr
& ex
) const
5025 Assert(ex
.getExprManager() == d_exprManager
);
5026 SmtScope
smts(this);
5028 Trace("smt") << "SMT getValue(" << ex
<< ")" << endl
;
5029 if(Dump
.isOn("benchmark")) {
5030 Dump("benchmark") << GetValueCommand(ex
);
5033 if(!options::produceModels()) {
5035 "Cannot get value when produce-models options is off.";
5036 throw ModalException(msg
);
5038 if(d_status
.isNull() ||
5039 d_status
.asSatisfiabilityResult() == Result::UNSAT
||
5040 d_problemExtended
) {
5042 "Cannot get value unless immediately preceded by SAT/INVALID or UNKNOWN response.";
5043 throw RecoverableModalException(msg
);
5046 // Substitute out any abstract values in ex.
5047 Expr e
= d_private
->substituteAbstractValues(Node::fromExpr(ex
)).toExpr();
5049 // Ensure expr is type-checked at this point.
5050 e
.getType(options::typeChecking());
5052 // do not need to apply preprocessing substitutions (should be recorded
5053 // in model already)
5055 Node n
= Node::fromExpr(e
);
5056 Trace("smt") << "--- getting value of " << n
<< endl
;
5057 TypeNode expectedType
= n
.getType();
5059 // Expand, then normalize
5060 unordered_map
<Node
, Node
, NodeHashFunction
> cache
;
5061 n
= d_private
->expandDefinitions(n
, cache
);
5062 // There are two ways model values for terms are computed (for historical
5063 // reasons). One way is that used in check-model; the other is that
5064 // used by the Model classes. It's not clear to me exactly how these
5065 // two are different, but they need to be unified. This ugly hack here
5066 // is to fix bug 554 until we can revamp boolean-terms and models [MGD]
5069 if(!n
.getType().isFunction()) {
5070 n
= Rewriter::rewrite(n
);
5073 Trace("smt") << "--- getting value of " << n
<< endl
;
5074 TheoryModel
* m
= d_theoryEngine
->getModel();
5077 resultNode
= m
->getValue(n
);
5079 Trace("smt") << "--- got value " << n
<< " = " << resultNode
<< endl
;
5080 resultNode
= postprocess(resultNode
, expectedType
);
5081 Trace("smt") << "--- model-post returned " << resultNode
<< endl
;
5082 Trace("smt") << "--- model-post returned " << resultNode
.getType() << endl
;
5083 Trace("smt") << "--- model-post expected " << expectedType
<< endl
;
5085 // type-check the result we got
5086 Assert(resultNode
.isNull() || resultNode
.getType().isSubtypeOf(expectedType
),
5087 "Run with -t smt for details.");
5089 // ensure it's a constant
5090 Assert(resultNode
.getKind() == kind::LAMBDA
|| resultNode
.isConst());
5092 if(options::abstractValues() && resultNode
.getType().isArray()) {
5093 resultNode
= d_private
->mkAbstractValue(resultNode
);
5094 Trace("smt") << "--- abstract value >> " << resultNode
<< endl
;
5097 return resultNode
.toExpr();
5100 bool SmtEngine::addToAssignment(const Expr
& ex
) {
5101 SmtScope
smts(this);
5102 finalOptionsAreSet();
5104 // Substitute out any abstract values in ex
5105 Expr e
= d_private
->substituteAbstractValues(Node::fromExpr(ex
)).toExpr();
5106 Type type
= e
.getType(options::typeChecking());
5108 PrettyCheckArgument(
5109 type
.isBoolean(), e
,
5110 "expected Boolean-typed variable or function application "
5111 "in addToAssignment()" );
5112 Node n
= e
.getNode();
5113 // must be an APPLY of a zero-ary defined function, or a variable
5114 PrettyCheckArgument(
5115 ( ( n
.getKind() == kind::APPLY
&&
5116 ( d_definedFunctions
->find(n
.getOperator()) !=
5117 d_definedFunctions
->end() ) &&
5118 n
.getNumChildren() == 0 ) ||
5120 "expected variable or defined-function application "
5121 "in addToAssignment(),\ngot %s", e
.toString().c_str() );
5122 if(!options::produceAssignments()) {
5125 if(d_assignments
== NULL
) {
5126 d_assignments
= new(true) AssignmentSet(d_context
);
5128 d_assignments
->insert(n
);
5133 // TODO(#1108): Simplify the error reporting of this method.
5134 vector
<pair
<Expr
, Expr
>> SmtEngine::getAssignment()
5136 Trace("smt") << "SMT getAssignment()" << endl
;
5137 SmtScope
smts(this);
5138 finalOptionsAreSet();
5139 if(Dump
.isOn("benchmark")) {
5140 Dump("benchmark") << GetAssignmentCommand();
5142 if(!options::produceAssignments()) {
5144 "Cannot get the current assignment when "
5145 "produce-assignments option is off.";
5146 throw ModalException(msg
);
5148 if(d_status
.isNull() ||
5149 d_status
.asSatisfiabilityResult() == Result::UNSAT
||
5150 d_problemExtended
) {
5152 "Cannot get the current assignment unless immediately "
5153 "preceded by SAT/INVALID or UNKNOWN response.";
5154 throw RecoverableModalException(msg
);
5157 vector
<pair
<Expr
,Expr
>> res
;
5158 if (d_assignments
!= nullptr)
5160 TypeNode boolType
= d_nodeManager
->booleanType();
5161 TheoryModel
* m
= d_theoryEngine
->getModel();
5162 for (AssignmentSet::key_iterator i
= d_assignments
->key_begin(),
5163 iend
= d_assignments
->key_end();
5168 Assert(as
.getType() == boolType
);
5170 Trace("smt") << "--- getting value of " << as
<< endl
;
5172 // Expand, then normalize
5173 unordered_map
<Node
, Node
, NodeHashFunction
> cache
;
5174 Node n
= d_private
->expandDefinitions(as
, cache
);
5175 n
= Rewriter::rewrite(n
);
5177 Trace("smt") << "--- getting value of " << n
<< endl
;
5181 resultNode
= m
->getValue(n
);
5184 // type-check the result we got
5185 Assert(resultNode
.isNull() || resultNode
.getType() == boolType
);
5187 // ensure it's a constant
5188 Assert(resultNode
.isConst());
5190 Assert(as
.getKind() == kind::APPLY
|| as
.isVar());
5191 Assert(as
.getKind() != kind::APPLY
|| as
.getNumChildren() == 0);
5192 res
.emplace_back(as
.toExpr(), resultNode
.toExpr());
5198 void SmtEngine::addToModelCommandAndDump(const Command
& c
, uint32_t flags
, bool userVisible
, const char* dumpTag
) {
5199 Trace("smt") << "SMT addToModelCommandAndDump(" << c
<< ")" << endl
;
5200 SmtScope
smts(this);
5201 // If we aren't yet fully inited, the user might still turn on
5202 // produce-models. So let's keep any commands around just in
5203 // case. This is useful in two cases: (1) SMT-LIBv1 auto-declares
5204 // sort "U" in QF_UF before setLogic() is run and we still want to
5205 // support finding card(U) with --finite-model-find, and (2) to
5206 // decouple SmtEngine and ExprManager if the user does a few
5207 // ExprManager::mkSort() before SmtEngine::setOption("produce-models")
5208 // and expects to find their cardinalities in the model.
5209 if(/* userVisible && */
5210 (!d_fullyInited
|| options::produceModels()) &&
5211 (flags
& ExprManager::VAR_FLAG_DEFINED
) == 0) {
5213 if(flags
& ExprManager::VAR_FLAG_GLOBAL
) {
5214 d_modelGlobalCommands
.push_back(c
.clone());
5216 d_modelCommands
->push_back(c
.clone());
5219 if(Dump
.isOn(dumpTag
)) {
5223 d_dumpCommands
.push_back(c
.clone());
5228 // TODO(#1108): Simplify the error reporting of this method.
5229 Model
* SmtEngine::getModel() {
5230 Trace("smt") << "SMT getModel()" << endl
;
5231 SmtScope
smts(this);
5233 finalOptionsAreSet();
5235 if(Dump
.isOn("benchmark")) {
5236 Dump("benchmark") << GetModelCommand();
5239 if (!options::assignFunctionValues())
5242 "Cannot get the model when --assign-function-values is false.";
5243 throw RecoverableModalException(msg
);
5246 if(d_status
.isNull() ||
5247 d_status
.asSatisfiabilityResult() == Result::UNSAT
||
5248 d_problemExtended
) {
5250 "Cannot get the current model unless immediately "
5251 "preceded by SAT/INVALID or UNKNOWN response.";
5252 throw RecoverableModalException(msg
);
5254 if(!options::produceModels()) {
5256 "Cannot get model when produce-models options is off.";
5257 throw ModalException(msg
);
5259 TheoryModel
* m
= d_theoryEngine
->getModel();
5260 m
->d_inputName
= d_filename
;
5264 std::pair
<Expr
, Expr
> SmtEngine::getSepHeapAndNilExpr(void)
5266 if (!d_logic
.isTheoryEnabled(THEORY_SEP
))
5269 "Cannot obtain separation logic expressions if not using the "
5270 "separation logic theory.";
5271 throw RecoverableModalException(msg
);
5273 NodeManagerScope
nms(d_nodeManager
);
5276 Model
* m
= getModel();
5277 if (m
->getHeapModel(heap
, nil
))
5279 return std::make_pair(heap
, nil
);
5282 "SmtEngine::getSepHeapAndNilExpr(): failed to obtain heap/nil "
5283 "expressions from theory model.");
5286 Expr
SmtEngine::getSepHeapExpr() { return getSepHeapAndNilExpr().first
; }
5288 Expr
SmtEngine::getSepNilExpr() { return getSepHeapAndNilExpr().second
; }
5290 void SmtEngine::checkUnsatCore() {
5291 Assert(options::unsatCores(), "cannot check unsat core if unsat cores are turned off");
5293 Notice() << "SmtEngine::checkUnsatCore(): generating unsat core" << endl
;
5294 UnsatCore core
= getUnsatCore();
5296 SmtEngine
coreChecker(d_exprManager
);
5297 coreChecker
.setLogic(getLogicInfo());
5300 std::vector
<Command
*>::const_iterator itg
= d_defineCommands
.begin();
5301 for (; itg
!= d_defineCommands
.end(); ++itg
) {
5302 (*itg
)->invoke(&coreChecker
);
5306 Notice() << "SmtEngine::checkUnsatCore(): pushing core assertions (size == " << core
.size() << ")" << endl
;
5307 for(UnsatCore::iterator i
= core
.begin(); i
!= core
.end(); ++i
) {
5308 Notice() << "SmtEngine::checkUnsatCore(): pushing core member " << *i
<< endl
;
5309 coreChecker
.assertFormula(*i
);
5311 const bool checkUnsatCores
= options::checkUnsatCores();
5314 options::checkUnsatCores
.set(false);
5315 options::checkProofs
.set(false);
5316 r
= coreChecker
.checkSat();
5318 options::checkUnsatCores
.set(checkUnsatCores
);
5321 Notice() << "SmtEngine::checkUnsatCore(): result is " << r
<< endl
;
5322 if(r
.asSatisfiabilityResult().isUnknown()) {
5323 InternalError("SmtEngine::checkUnsatCore(): could not check core result unknown.");
5326 if(r
.asSatisfiabilityResult().isSat()) {
5327 InternalError("SmtEngine::checkUnsatCore(): produced core was satisfiable.");
5331 void SmtEngine::checkModel(bool hardFailure
) {
5332 // --check-model implies --produce-assertions, which enables the
5333 // assertion list, so we should be ok.
5334 Assert(d_assertionList
!= NULL
, "don't have an assertion list to check in SmtEngine::checkModel()");
5336 TimerStat::CodeTimer
checkModelTimer(d_stats
->d_checkModelTime
);
5338 // Throughout, we use Notice() to give diagnostic output.
5340 // If this function is running, the user gave --check-model (or equivalent),
5341 // and if Notice() is on, the user gave --verbose (or equivalent).
5343 Notice() << "SmtEngine::checkModel(): generating model" << endl
;
5344 TheoryModel
* m
= d_theoryEngine
->getModel();
5346 // check-model is not guaranteed to succeed if approximate values were used
5347 if (m
->hasApproximations())
5350 << "WARNING: running check-model on a model with approximate values..."
5354 // Check individual theory assertions
5355 d_theoryEngine
->checkTheoryAssertionsWithModel(hardFailure
);
5360 // We have a "fake context" for the substitution map (we don't need it
5361 // to be context-dependent)
5362 context::Context fakeContext
;
5363 SubstitutionMap
substitutions(&fakeContext
, /* substituteUnderQuantifiers = */ false);
5365 for(size_t k
= 0; k
< m
->getNumCommands(); ++k
) {
5366 const DeclareFunctionCommand
* c
= dynamic_cast<const DeclareFunctionCommand
*>(m
->getCommand(k
));
5367 Notice() << "SmtEngine::checkModel(): model command " << k
<< " : " << m
->getCommand(k
) << endl
;
5369 // we don't care about DECLARE-DATATYPES, DECLARE-SORT, ...
5370 Notice() << "SmtEngine::checkModel(): skipping..." << endl
;
5372 // We have a DECLARE-FUN:
5374 // We'll first do some checks, then add to our substitution map
5375 // the mapping: function symbol |-> value
5377 Expr func
= c
->getFunction();
5378 Node val
= m
->getValue(func
);
5380 Notice() << "SmtEngine::checkModel(): adding substitution: " << func
<< " |-> " << val
<< endl
;
5382 // (1) if the value is a lambda, ensure the lambda doesn't contain the
5383 // function symbol (since then the definition is recursive)
5384 if (val
.getKind() == kind::LAMBDA
) {
5385 // first apply the model substitutions we have so far
5386 Debug("boolean-terms") << "applying subses to " << val
[1] << endl
;
5387 Node n
= substitutions
.apply(val
[1]);
5388 Debug("boolean-terms") << "++ got " << n
<< endl
;
5389 // now check if n contains func by doing a substitution
5390 // [func->func2] and checking equality of the Nodes.
5391 // (this just a way to check if func is in n.)
5392 SubstitutionMap
subs(&fakeContext
);
5393 Node func2
= NodeManager::currentNM()->mkSkolem("", TypeNode::fromType(func
.getType()), "", NodeManager::SKOLEM_NO_NOTIFY
);
5394 subs
.addSubstitution(func
, func2
);
5395 if(subs
.apply(n
) != n
) {
5396 Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE DEFINED IN TERMS OF ITSELF ***" << endl
;
5398 ss
<< "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
5399 << "considering model value for " << func
<< endl
5400 << "body of lambda is: " << val
<< endl
;
5402 ss
<< "body substitutes to: " << n
<< endl
;
5404 ss
<< "so " << func
<< " is defined in terms of itself." << endl
5405 << "Run with `--check-models -v' for additional diagnostics.";
5406 InternalError(ss
.str());
5410 // (2) check that the value is actually a value
5411 else if (!val
.isConst()) {
5412 Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE NOT A CONSTANT ***" << endl
;
5414 ss
<< "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
5415 << "model value for " << func
<< endl
5416 << " is " << val
<< endl
5417 << "and that is not a constant (.isConst() == false)." << endl
5418 << "Run with `--check-models -v' for additional diagnostics.";
5419 InternalError(ss
.str());
5422 // (3) check that it's the correct (sub)type
5423 // This was intended to be a more general check, but for now we can't do that because
5424 // e.g. "1" is an INT, which isn't a subrange type [1..10] (etc.).
5425 else if(func
.getType().isInteger() && !val
.getType().isInteger()) {
5426 Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE NOT CORRECT TYPE ***" << endl
;
5428 ss
<< "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
5429 << "model value for " << func
<< endl
5430 << " is " << val
<< endl
5431 << "value type is " << val
.getType() << endl
5432 << "should be of type " << func
.getType() << endl
5433 << "Run with `--check-models -v' for additional diagnostics.";
5434 InternalError(ss
.str());
5437 // (4) checks complete, add the substitution
5438 Debug("boolean-terms") << "cm: adding subs " << func
<< " :=> " << val
<< endl
;
5439 substitutions
.addSubstitution(func
, val
);
5443 // Now go through all our user assertions checking if they're satisfied.
5444 for(AssertionList::const_iterator i
= d_assertionList
->begin(); i
!= d_assertionList
->end(); ++i
) {
5445 Notice() << "SmtEngine::checkModel(): checking assertion " << *i
<< endl
;
5446 Node n
= Node::fromExpr(*i
);
5448 // Apply any define-funs from the problem.
5450 unordered_map
<Node
, Node
, NodeHashFunction
> cache
;
5451 n
= d_private
->expandDefinitions(n
, cache
);
5453 Notice() << "SmtEngine::checkModel(): -- expands to " << n
<< endl
;
5455 // Apply our model value substitutions.
5456 Debug("boolean-terms") << "applying subses to " << n
<< endl
;
5457 n
= substitutions
.apply(n
);
5458 Debug("boolean-terms") << "++ got " << n
<< endl
;
5459 Notice() << "SmtEngine::checkModel(): -- substitutes to " << n
<< endl
;
5461 if( n
.getKind() != kind::REWRITE_RULE
){
5462 // In case it's a quantifier (or contains one), look up its value before
5463 // simplifying, or the quantifier might be irreparably altered.
5465 Notice() << "SmtEngine::checkModel(): -- get value : " << n
<< std::endl
;
5467 // Note this "skip" is done here, rather than above. This is
5468 // because (1) the quantifier could in principle simplify to false,
5469 // which should be reported, and (2) checking for the quantifier
5470 // above, before simplification, doesn't catch buried quantifiers
5471 // anyway (those not at the top-level).
5472 Notice() << "SmtEngine::checkModel(): -- skipping rewrite-rules assertion"
5477 // Simplify the result.
5478 n
= d_private
->simplify(n
);
5479 Notice() << "SmtEngine::checkModel(): -- simplifies to " << n
<< endl
;
5481 // Replace the already-known ITEs (this is important for ground ITEs under quantifiers).
5482 n
= d_private
->d_iteRemover
.replace(n
);
5483 Notice() << "SmtEngine::checkModel(): -- ite replacement gives " << n
<< endl
;
5485 // Apply our model value substitutions (again), as things may have been simplified.
5486 Debug("boolean-terms") << "applying subses to " << n
<< endl
;
5487 n
= substitutions
.apply(n
);
5488 Debug("boolean-terms") << "++ got " << n
<< endl
;
5489 Notice() << "SmtEngine::checkModel(): -- re-substitutes to " << n
<< endl
;
5491 // As a last-ditch effort, ask model to simplify it.
5492 // Presently, this is only an issue for quantifiers, which can have a value
5493 // but don't show up in our substitution map above.
5495 Notice() << "SmtEngine::checkModel(): -- model-substitutes to " << n
<< endl
;
5497 if( d_logic
.isQuantified() ){
5498 // AJR: since quantified formulas are not checkable, we assign them to true/false based on the satisfying assignment.
5499 // however, quantified formulas can be modified during preprocess, so they may not correspond to those in the satisfying assignment.
5500 // hence we use a relaxed version of check model here.
5501 // this is necessary until preprocessing passes explicitly record how they rewrite quantified formulas
5502 if( hardFailure
&& !n
.isConst() && n
.getKind() != kind::LAMBDA
){
5503 Notice() << "SmtEngine::checkModel(): -- relax check model wrt quantified formulas..." << endl
;
5504 AlwaysAssert( quantifiers::QuantifiersRewriter::containsQuantifiers( n
) );
5505 Warning() << "Warning : SmtEngine::checkModel(): cannot check simplified assertion : " << n
<< endl
;
5509 AlwaysAssert(!hardFailure
|| n
.isConst() || n
.getKind() == kind::LAMBDA
);
5511 // The result should be == true.
5512 if(n
!= NodeManager::currentNM()->mkConst(true)) {
5513 Notice() << "SmtEngine::checkModel(): *** PROBLEM: EXPECTED `TRUE' ***"
5516 ss
<< "SmtEngine::checkModel(): "
5517 << "ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
5518 << "assertion: " << *i
<< endl
5519 << "simplifies to: " << n
<< endl
5520 << "expected `true'." << endl
5521 << "Run with `--check-models -v' for additional diagnostics.";
5523 InternalError(ss
.str());
5525 Warning() << ss
.str() << endl
;
5529 Notice() << "SmtEngine::checkModel(): all assertions checked out OK !" << endl
;
5532 void SmtEngine::checkSynthSolution()
5534 NodeManager
* nm
= NodeManager::currentNM();
5535 Notice() << "SmtEngine::checkSynthSolution(): checking synthesis solution" << endl
;
5536 map
<Node
, Node
> sol_map
;
5537 /* Get solutions and build auxiliary vectors for substituting */
5538 d_theoryEngine
->getSynthSolutions(sol_map
);
5539 if (sol_map
.empty())
5541 Trace("check-synth-sol") << "No solution to check!\n";
5544 Trace("check-synth-sol") << "Got solution map:\n";
5545 std::vector
<Node
> function_vars
, function_sols
;
5546 for (const auto& pair
: sol_map
)
5548 Trace("check-synth-sol") << pair
.first
<< " --> " << pair
.second
<< "\n";
5549 function_vars
.push_back(pair
.first
);
5550 function_sols
.push_back(pair
.second
);
5552 Trace("check-synth-sol") << "Starting new SMT Engine\n";
5553 /* Start new SMT engine to check solutions */
5554 SmtEngine
solChecker(d_exprManager
);
5555 solChecker
.setLogic(getLogicInfo());
5556 setOption("check-synth-sol", SExpr("false"));
5558 Trace("check-synth-sol") << "Retrieving assertions\n";
5559 // Build conjecture from original assertions
5560 if (d_assertionList
== NULL
)
5562 Trace("check-synth-sol") << "No assertions to check\n";
5565 for (AssertionList::const_iterator i
= d_assertionList
->begin();
5566 i
!= d_assertionList
->end();
5569 Notice() << "SmtEngine::checkSynthSolution(): checking assertion " << *i
<< endl
;
5570 Trace("check-synth-sol") << "Retrieving assertion " << *i
<< "\n";
5571 Node conj
= Node::fromExpr(*i
);
5572 // Apply any define-funs from the problem.
5574 unordered_map
<Node
, Node
, NodeHashFunction
> cache
;
5575 conj
= d_private
->expandDefinitions(conj
, cache
);
5577 Notice() << "SmtEngine::checkSynthSolution(): -- expands to " << conj
<< endl
;
5578 Trace("check-synth-sol") << "Expanded assertion " << conj
<< "\n";
5579 if (conj
.getKind() != kind::FORALL
)
5581 Trace("check-synth-sol") << "Not a checkable assertion.\n";
5585 // Apply solution map to conjecture body
5587 /* Whether property is quantifier free */
5588 if (conj
[1].getKind() != kind::EXISTS
)
5590 conjBody
= conj
[1].substitute(function_vars
.begin(),
5591 function_vars
.end(),
5592 function_sols
.begin(),
5593 function_sols
.end());
5597 conjBody
= conj
[1][1].substitute(function_vars
.begin(),
5598 function_vars
.end(),
5599 function_sols
.begin(),
5600 function_sols
.end());
5602 /* Skolemize property */
5603 std::vector
<Node
> vars
, skos
;
5604 for (unsigned j
= 0, size
= conj
[1][0].getNumChildren(); j
< size
; ++j
)
5606 vars
.push_back(conj
[1][0][j
]);
5607 std::stringstream ss
;
5609 skos
.push_back(nm
->mkSkolem(ss
.str(), conj
[1][0][j
].getType()));
5610 Trace("check-synth-sol") << "\tSkolemizing " << conj
[1][0][j
] << " to "
5611 << skos
.back() << "\n";
5613 conjBody
= conjBody
.substitute(
5614 vars
.begin(), vars
.end(), skos
.begin(), skos
.end());
5616 Notice() << "SmtEngine::checkSynthSolution(): -- body substitutes to "
5617 << conjBody
<< endl
;
5618 Trace("check-synth-sol") << "Substituted body of assertion to " << conjBody
5620 solChecker
.assertFormula(conjBody
.toExpr());
5621 Result r
= solChecker
.checkSat();
5622 Notice() << "SmtEngine::checkSynthSolution(): result is " << r
<< endl
;
5623 Trace("check-synth-sol") << "Satsifiability check: " << r
<< "\n";
5624 if (r
.asSatisfiabilityResult().isUnknown())
5627 "SmtEngine::checkSynthSolution(): could not check solution, result "
5630 else if (r
.asSatisfiabilityResult().isSat())
5633 "SmtEngine::checkSynthSolution(): produced solution leads to "
5634 "satisfiable negated conjecture.");
5636 solChecker
.resetAssertions();
5640 // TODO(#1108): Simplify the error reporting of this method.
5641 UnsatCore
SmtEngine::getUnsatCore() {
5642 Trace("smt") << "SMT getUnsatCore()" << endl
;
5643 SmtScope
smts(this);
5644 finalOptionsAreSet();
5645 if(Dump
.isOn("benchmark")) {
5646 Dump("benchmark") << GetUnsatCoreCommand();
5649 if(!options::unsatCores()) {
5650 throw ModalException("Cannot get an unsat core when produce-unsat-cores option is off.");
5652 if(d_status
.isNull() ||
5653 d_status
.asSatisfiabilityResult() != Result::UNSAT
||
5654 d_problemExtended
) {
5655 throw RecoverableModalException(
5656 "Cannot get an unsat core unless immediately preceded by UNSAT/VALID "
5660 d_proofManager
->traceUnsatCore();// just to trigger core creation
5661 return UnsatCore(this, d_proofManager
->extractUnsatCore());
5662 #else /* IS_PROOFS_BUILD */
5663 throw ModalException("This build of CVC4 doesn't have proof support (required for unsat cores).");
5664 #endif /* IS_PROOFS_BUILD */
5667 // TODO(#1108): Simplify the error reporting of this method.
5668 const Proof
& SmtEngine::getProof()
5670 Trace("smt") << "SMT getProof()" << endl
;
5671 SmtScope
smts(this);
5672 finalOptionsAreSet();
5673 if(Dump
.isOn("benchmark")) {
5674 Dump("benchmark") << GetProofCommand();
5677 if(!options::proof()) {
5678 throw ModalException("Cannot get a proof when produce-proofs option is off.");
5680 if(d_status
.isNull() ||
5681 d_status
.asSatisfiabilityResult() != Result::UNSAT
||
5682 d_problemExtended
) {
5683 throw RecoverableModalException(
5684 "Cannot get a proof unless immediately preceded by UNSAT/VALID "
5688 return ProofManager::getProof(this);
5689 #else /* IS_PROOFS_BUILD */
5690 throw ModalException("This build of CVC4 doesn't have proof support.");
5691 #endif /* IS_PROOFS_BUILD */
5694 void SmtEngine::printInstantiations( std::ostream
& out
) {
5695 SmtScope
smts(this);
5696 if( options::instFormatMode()==INST_FORMAT_MODE_SZS
){
5697 out
<< "% SZS output start Proof for " << d_filename
.c_str() << std::endl
;
5699 if( d_theoryEngine
){
5700 d_theoryEngine
->printInstantiations( out
);
5704 if( options::instFormatMode()==INST_FORMAT_MODE_SZS
){
5705 out
<< "% SZS output end Proof for " << d_filename
.c_str() << std::endl
;
5709 void SmtEngine::printSynthSolution( std::ostream
& out
) {
5710 SmtScope
smts(this);
5711 if( d_theoryEngine
){
5712 d_theoryEngine
->printSynthSolution( out
);
5718 void SmtEngine::getSynthSolutions(std::map
<Expr
, Expr
>& sol_map
)
5720 SmtScope
smts(this);
5721 map
<Node
, Node
> sol_mapn
;
5722 Assert(d_theoryEngine
!= nullptr);
5723 d_theoryEngine
->getSynthSolutions(sol_mapn
);
5724 for (std::pair
<const Node
, Node
>& s
: sol_mapn
)
5726 sol_map
[s
.first
.toExpr()] = s
.second
.toExpr();
5730 Expr
SmtEngine::doQuantifierElimination(const Expr
& e
, bool doFull
, bool strict
)
5732 SmtScope
smts(this);
5733 if(!d_logic
.isPure(THEORY_ARITH
) && strict
){
5734 Warning() << "Unexpected logic for quantifier elimination " << d_logic
<< endl
;
5736 Trace("smt-qe") << "Do quantifier elimination " << e
<< std::endl
;
5737 Node n_e
= Node::fromExpr( e
);
5738 if (n_e
.getKind() != kind::EXISTS
&& n_e
.getKind() != kind::FORALL
)
5740 throw ModalException(
5741 "Expecting a quantified formula as argument to get-qe.");
5743 //tag the quantified formula with the quant-elim attribute
5744 TypeNode t
= NodeManager::currentNM()->booleanType();
5745 Node n_attr
= NodeManager::currentNM()->mkSkolem("qe", t
, "Auxiliary variable for qe attr.");
5746 std::vector
< Node
> node_values
;
5747 d_theoryEngine
->setUserAttribute( doFull
? "quant-elim" : "quant-elim-partial", n_attr
, node_values
, "");
5748 n_attr
= NodeManager::currentNM()->mkNode(kind::INST_ATTRIBUTE
, n_attr
);
5749 n_attr
= NodeManager::currentNM()->mkNode(kind::INST_PATTERN_LIST
, n_attr
);
5750 std::vector
< Node
> e_children
;
5751 e_children
.push_back( n_e
[0] );
5752 e_children
.push_back(n_e
.getKind() == kind::EXISTS
? n_e
[1]
5754 e_children
.push_back( n_attr
);
5755 Node nn_e
= NodeManager::currentNM()->mkNode( kind::EXISTS
, e_children
);
5756 Trace("smt-qe-debug") << "Query for quantifier elimination : " << nn_e
<< std::endl
;
5757 Assert( nn_e
.getNumChildren()==3 );
5758 Result r
= checkSatisfiability(nn_e
.toExpr(), true, true);
5759 Trace("smt-qe") << "Query returned " << r
<< std::endl
;
5760 if(r
.asSatisfiabilityResult().isSat() != Result::UNSAT
) {
5761 if( r
.asSatisfiabilityResult().isSat() != Result::SAT
&& doFull
){
5763 ss
<< "While performing quantifier elimination, unexpected result : " << r
<< " for query.";
5764 InternalError(ss
.str().c_str());
5766 std::vector
< Node
> inst_qs
;
5767 d_theoryEngine
->getInstantiatedQuantifiedFormulas( inst_qs
);
5768 Assert( inst_qs
.size()<=1 );
5770 if( inst_qs
.size()==1 ){
5771 Node top_q
= inst_qs
[0];
5772 //Node top_q = Rewriter::rewrite( nn_e ).negate();
5773 Assert( top_q
.getKind()==kind::FORALL
);
5774 Trace("smt-qe") << "Get qe for " << top_q
<< std::endl
;
5775 ret_n
= d_theoryEngine
->getInstantiatedConjunction( top_q
);
5776 Trace("smt-qe") << "Returned : " << ret_n
<< std::endl
;
5777 if (n_e
.getKind() == kind::EXISTS
)
5779 ret_n
= Rewriter::rewrite(ret_n
.negate());
5782 ret_n
= NodeManager::currentNM()->mkConst(n_e
.getKind() != kind::EXISTS
);
5784 // do extended rewrite to minimize the size of the formula aggressively
5785 theory::quantifiers::ExtendedRewriter
extr(true);
5786 ret_n
= extr
.extendedRewrite(ret_n
);
5787 return ret_n
.toExpr();
5789 return NodeManager::currentNM()
5790 ->mkConst(n_e
.getKind() == kind::EXISTS
)
5795 void SmtEngine::getInstantiatedQuantifiedFormulas( std::vector
< Expr
>& qs
) {
5796 SmtScope
smts(this);
5797 if( d_theoryEngine
){
5798 std::vector
< Node
> qs_n
;
5799 d_theoryEngine
->getInstantiatedQuantifiedFormulas( qs_n
);
5800 for( unsigned i
=0; i
<qs_n
.size(); i
++ ){
5801 qs
.push_back( qs_n
[i
].toExpr() );
5808 void SmtEngine::getInstantiations( Expr q
, std::vector
< Expr
>& insts
) {
5809 SmtScope
smts(this);
5810 if( d_theoryEngine
){
5811 std::vector
< Node
> insts_n
;
5812 d_theoryEngine
->getInstantiations( Node::fromExpr( q
), insts_n
);
5813 for( unsigned i
=0; i
<insts_n
.size(); i
++ ){
5814 insts
.push_back( insts_n
[i
].toExpr() );
5821 void SmtEngine::getInstantiationTermVectors( Expr q
, std::vector
< std::vector
< Expr
> >& tvecs
) {
5822 SmtScope
smts(this);
5823 Assert(options::trackInstLemmas());
5824 if( d_theoryEngine
){
5825 std::vector
< std::vector
< Node
> > tvecs_n
;
5826 d_theoryEngine
->getInstantiationTermVectors( Node::fromExpr( q
), tvecs_n
);
5827 for( unsigned i
=0; i
<tvecs_n
.size(); i
++ ){
5828 std::vector
< Expr
> tvec
;
5829 for( unsigned j
=0; j
<tvecs_n
[i
].size(); j
++ ){
5830 tvec
.push_back( tvecs_n
[i
][j
].toExpr() );
5832 tvecs
.push_back( tvec
);
5839 vector
<Expr
> SmtEngine::getAssertions() {
5840 SmtScope
smts(this);
5841 finalOptionsAreSet();
5843 if(Dump
.isOn("benchmark")) {
5844 Dump("benchmark") << GetAssertionsCommand();
5846 Trace("smt") << "SMT getAssertions()" << endl
;
5847 if(!options::produceAssertions()) {
5849 "Cannot query the current assertion list when not in produce-assertions mode.";
5850 throw ModalException(msg
);
5852 Assert(d_assertionList
!= NULL
);
5853 // copy the result out
5854 return vector
<Expr
>(d_assertionList
->begin(), d_assertionList
->end());
5857 void SmtEngine::push()
5859 SmtScope
smts(this);
5860 finalOptionsAreSet();
5862 Trace("smt") << "SMT push()" << endl
;
5863 d_private
->notifyPush();
5864 d_private
->processAssertions();
5865 if(Dump
.isOn("benchmark")) {
5866 Dump("benchmark") << PushCommand();
5868 if(!options::incrementalSolving()) {
5869 throw ModalException("Cannot push when not solving incrementally (use --incremental)");
5872 // check to see if a postsolve() is pending
5873 if(d_needPostsolve
) {
5874 d_theoryEngine
->postsolve();
5875 d_needPostsolve
= false;
5878 // The problem isn't really "extended" yet, but this disallows
5879 // get-model after a push, simplifying our lives somewhat and
5880 // staying symmtric with pop.
5881 setProblemExtended(true);
5883 d_userLevels
.push_back(d_userContext
->getLevel());
5885 Trace("userpushpop") << "SmtEngine: pushed to level "
5886 << d_userContext
->getLevel() << endl
;
5889 void SmtEngine::pop() {
5890 SmtScope
smts(this);
5891 finalOptionsAreSet();
5892 Trace("smt") << "SMT pop()" << endl
;
5893 if(Dump
.isOn("benchmark")) {
5894 Dump("benchmark") << PopCommand();
5896 if(!options::incrementalSolving()) {
5897 throw ModalException("Cannot pop when not solving incrementally (use --incremental)");
5899 if(d_userLevels
.size() == 0) {
5900 throw ModalException("Cannot pop beyond the first user frame");
5903 // check to see if a postsolve() is pending
5904 if(d_needPostsolve
) {
5905 d_theoryEngine
->postsolve();
5906 d_needPostsolve
= false;
5909 // The problem isn't really "extended" yet, but this disallows
5910 // get-model after a pop, simplifying our lives somewhat. It might
5911 // not be strictly necessary to do so, since the pops occur lazily,
5912 // but also it would be weird to have a legally-executed (get-model)
5913 // that only returns a subset of the assignment (because the rest
5914 // is no longer in scope!).
5915 setProblemExtended(true);
5917 AlwaysAssert(d_userContext
->getLevel() > 0);
5918 AlwaysAssert(d_userLevels
.back() < d_userContext
->getLevel());
5919 while (d_userLevels
.back() < d_userContext
->getLevel()) {
5922 d_userLevels
.pop_back();
5924 // Clear out assertion queues etc., in case anything is still in there
5925 d_private
->notifyPop();
5927 Trace("userpushpop") << "SmtEngine: popped to level "
5928 << d_userContext
->getLevel() << endl
;
5929 // FIXME: should we reset d_status here?
5930 // SMT-LIBv2 spec seems to imply no, but it would make sense to..
5933 void SmtEngine::internalPush() {
5934 Assert(d_fullyInited
);
5935 Trace("smt") << "SmtEngine::internalPush()" << endl
;
5937 if(options::incrementalSolving()) {
5938 d_private
->processAssertions();
5939 TimerStat::CodeTimer
pushPopTimer(d_stats
->d_pushPopTime
);
5940 d_userContext
->push();
5941 // the d_context push is done inside of the SAT solver
5942 d_propEngine
->push();
5946 void SmtEngine::internalPop(bool immediate
) {
5947 Assert(d_fullyInited
);
5948 Trace("smt") << "SmtEngine::internalPop()" << endl
;
5949 if(options::incrementalSolving()) {
5957 void SmtEngine::doPendingPops() {
5958 Assert(d_pendingPops
== 0 || options::incrementalSolving());
5959 while(d_pendingPops
> 0) {
5960 TimerStat::CodeTimer
pushPopTimer(d_stats
->d_pushPopTime
);
5961 d_propEngine
->pop();
5962 // the d_context pop is done inside of the SAT solver
5963 d_userContext
->pop();
5968 void SmtEngine::reset()
5970 SmtScope
smts(this);
5971 ExprManager
*em
= d_exprManager
;
5972 Trace("smt") << "SMT reset()" << endl
;
5973 if(Dump
.isOn("benchmark")) {
5974 Dump("benchmark") << ResetCommand();
5977 opts
.copyValues(d_originalOptions
);
5979 NodeManager::fromExprManager(em
)->getOptions().copyValues(opts
);
5980 new(this) SmtEngine(em
);
5983 void SmtEngine::resetAssertions()
5985 SmtScope
smts(this);
5988 Trace("smt") << "SMT resetAssertions()" << endl
;
5989 if(Dump
.isOn("benchmark")) {
5990 Dump("benchmark") << ResetAssertionsCommand();
5993 while(!d_userLevels
.empty()) {
5997 // Also remember the global push/pop around everything.
5998 Assert(d_userLevels
.size() == 0 && d_userContext
->getLevel() == 1);
5999 d_context
->popto(0);
6000 d_userContext
->popto(0);
6001 DeleteAndClearCommandVector(d_modelGlobalCommands
);
6002 d_userContext
->push();
6006 void SmtEngine::interrupt()
6008 if(!d_fullyInited
) {
6011 d_propEngine
->interrupt();
6012 d_theoryEngine
->interrupt();
6015 void SmtEngine::setResourceLimit(unsigned long units
, bool cumulative
) {
6016 d_private
->getResourceManager()->setResourceLimit(units
, cumulative
);
6018 void SmtEngine::setTimeLimit(unsigned long milis
, bool cumulative
) {
6019 d_private
->getResourceManager()->setTimeLimit(milis
, cumulative
);
6022 unsigned long SmtEngine::getResourceUsage() const {
6023 return d_private
->getResourceManager()->getResourceUsage();
6026 unsigned long SmtEngine::getTimeUsage() const {
6027 return d_private
->getResourceManager()->getTimeUsage();
6030 unsigned long SmtEngine::getResourceRemaining() const
6032 return d_private
->getResourceManager()->getResourceRemaining();
6035 unsigned long SmtEngine::getTimeRemaining() const
6037 return d_private
->getResourceManager()->getTimeRemaining();
6040 Statistics
SmtEngine::getStatistics() const
6042 return Statistics(*d_statisticsRegistry
);
6045 SExpr
SmtEngine::getStatistic(std::string name
) const
6047 return d_statisticsRegistry
->getStatistic(name
);
6050 void SmtEngine::safeFlushStatistics(int fd
) const {
6051 d_statisticsRegistry
->safeFlushInformation(fd
);
6054 void SmtEngine::setUserAttribute(const std::string
& attr
,
6056 const std::vector
<Expr
>& expr_values
,
6057 const std::string
& str_value
)
6059 SmtScope
smts(this);
6060 std::vector
<Node
> node_values
;
6061 for( unsigned i
=0; i
<expr_values
.size(); i
++ ){
6062 node_values
.push_back( expr_values
[i
].getNode() );
6064 d_theoryEngine
->setUserAttribute(attr
, expr
.getNode(), node_values
, str_value
);
6067 void SmtEngine::setPrintFuncInModel(Expr f
, bool p
) {
6068 Trace("setp-model") << "Set printInModel " << f
<< " to " << p
<< std::endl
;
6069 for( unsigned i
=0; i
<d_modelGlobalCommands
.size(); i
++ ){
6070 Command
* c
= d_modelGlobalCommands
[i
];
6071 DeclareFunctionCommand
* dfc
= dynamic_cast<DeclareFunctionCommand
*>(c
);
6073 if( dfc
->getFunction()==f
){
6074 dfc
->setPrintInModel( p
);
6078 for( unsigned i
=0; i
<d_modelCommands
->size(); i
++ ){
6079 Command
* c
= (*d_modelCommands
)[i
];
6080 DeclareFunctionCommand
* dfc
= dynamic_cast<DeclareFunctionCommand
*>(c
);
6082 if( dfc
->getFunction()==f
){
6083 dfc
->setPrintInModel( p
);
6089 void SmtEngine::beforeSearch()
6092 throw ModalException(
6093 "SmtEngine::beforeSearch called after initialization.");
6098 void SmtEngine::setOption(const std::string
& key
, const CVC4::SExpr
& value
)
6100 NodeManagerScope
nms(d_nodeManager
);
6101 Trace("smt") << "SMT setOption(" << key
<< ", " << value
<< ")" << endl
;
6103 if(Dump
.isOn("benchmark")) {
6104 Dump("benchmark") << SetOptionCommand(key
, value
);
6107 if(key
== "command-verbosity") {
6108 if(!value
.isAtom()) {
6109 const vector
<SExpr
>& cs
= value
.getChildren();
6110 if(cs
.size() == 2 &&
6111 (cs
[0].isKeyword() || cs
[0].isString()) &&
6112 cs
[1].isInteger()) {
6113 string c
= cs
[0].getValue();
6114 const Integer
& v
= cs
[1].getIntegerValue();
6115 if(v
< 0 || v
> 2) {
6116 throw OptionException("command-verbosity must be 0, 1, or 2");
6118 d_commandVerbosity
[c
] = v
;
6122 throw OptionException("command-verbosity value must be a tuple (command-name, integer)");
6125 if(!value
.isAtom()) {
6126 throw OptionException("bad value for :" + key
);
6129 string optionarg
= value
.getValue();
6130 Options
& nodeManagerOptions
= NodeManager::currentNM()->getOptions();
6131 nodeManagerOptions
.setOption(key
, optionarg
);
6134 CVC4::SExpr
SmtEngine::getOption(const std::string
& key
) const
6136 NodeManagerScope
nms(d_nodeManager
);
6138 Trace("smt") << "SMT getOption(" << key
<< ")" << endl
;
6140 if(key
.length() >= 18 &&
6141 key
.compare(0, 18, "command-verbosity:") == 0) {
6142 map
<string
, Integer
>::const_iterator i
= d_commandVerbosity
.find(key
.c_str() + 18);
6143 if(i
!= d_commandVerbosity
.end()) {
6144 return SExpr((*i
).second
);
6146 i
= d_commandVerbosity
.find("*");
6147 if(i
!= d_commandVerbosity
.end()) {
6148 return SExpr((*i
).second
);
6150 return SExpr(Integer(2));
6153 if(Dump
.isOn("benchmark")) {
6154 Dump("benchmark") << GetOptionCommand(key
);
6157 if(key
== "command-verbosity") {
6158 vector
<SExpr
> result
;
6159 SExpr defaultVerbosity
;
6160 for(map
<string
, Integer
>::const_iterator i
= d_commandVerbosity
.begin();
6161 i
!= d_commandVerbosity
.end();
6164 v
.push_back(SExpr((*i
).first
));
6165 v
.push_back(SExpr((*i
).second
));
6166 if((*i
).first
== "*") {
6167 // put the default at the end of the SExpr
6168 defaultVerbosity
= SExpr(v
);
6170 result
.push_back(SExpr(v
));
6173 // put the default at the end of the SExpr
6174 if(!defaultVerbosity
.isAtom()) {
6175 result
.push_back(defaultVerbosity
);
6177 // ensure the default is always listed
6179 v
.push_back(SExpr("*"));
6180 v
.push_back(SExpr(Integer(2)));
6181 result
.push_back(SExpr(v
));
6183 return SExpr(result
);
6186 Options
& nodeManagerOptions
= NodeManager::currentNM()->getOptions();
6187 return SExpr::parseAtom(nodeManagerOptions
.getOption(key
));
6190 void SmtEngine::setReplayStream(ExprStream
* replayStream
) {
6191 AlwaysAssert(!d_fullyInited
,
6192 "Cannot set replay stream once fully initialized");
6193 d_replayStream
= replayStream
;
6196 bool SmtEngine::getExpressionName(Expr e
, std::string
& name
) const {
6197 return d_private
->getExpressionName(e
, name
);
6200 void SmtEngine::setExpressionName(Expr e
, const std::string
& name
) {
6201 Trace("smt-debug") << "Set expression name " << e
<< " to " << name
<< std::endl
;
6202 d_private
->setExpressionName(e
,name
);
6205 }/* CVC4 namespace */