1 /********************* */
2 /*! \file smt_engine.cpp
4 ** Original author: mdeters
5 ** Major contributors: barrett
6 ** Minor contributors (to current version): lianah, cconway, taking, kshitij, dejan, ajreynol
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009-2012 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** 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.
25 #include <ext/hash_map>
27 #include "context/cdlist.h"
28 #include "context/cdhashset.h"
29 #include "context/context.h"
30 #include "decision/decision_engine.h"
31 #include "decision/decision_mode.h"
32 #include "decision/options.h"
33 #include "expr/command.h"
34 #include "expr/expr.h"
35 #include "expr/kind.h"
36 #include "expr/metakind.h"
37 #include "expr/node_builder.h"
38 #include "expr/node.h"
39 #include "prop/prop_engine.h"
40 #include "smt/modal_exception.h"
41 #include "smt/smt_engine.h"
42 #include "smt/smt_engine_scope.h"
43 #include "theory/theory_engine.h"
44 #include "theory/bv/theory_bv_rewriter.h"
45 #include "proof/proof_manager.h"
46 #include "util/proof.h"
47 #include "util/boolean_simplification.h"
48 #include "util/configuration.h"
49 #include "util/exception.h"
50 #include "smt/command_list.h"
51 #include "smt/options.h"
52 #include "options/option_exception.h"
53 #include "util/output.h"
54 #include "util/hash.h"
55 #include "theory/substitutions.h"
56 #include "theory/uf/options.h"
57 #include "theory/arith/options.h"
58 #include "theory/theory_traits.h"
59 #include "theory/logic_info.h"
60 #include "theory/options.h"
61 #include "theory/booleans/circuit_propagator.h"
62 #include "util/ite_removal.h"
63 #include "theory/model.h"
64 #include "printer/printer.h"
65 #include "prop/options.h"
66 #include "theory/arrays/options.h"
67 #include "util/sort_inference.h"
68 #include "theory/quantifiers/macros.h"
72 using namespace CVC4::smt
;
73 using namespace CVC4::prop
;
74 using namespace CVC4::context
;
75 using namespace CVC4::theory
;
82 * Representation of a defined function. We keep these around in
83 * SmtEngine to permit expanding definitions late (and lazily), to
84 * support getValue() over defined functions, to support user output
85 * in terms of defined functions, etc.
87 class DefinedFunction
{
89 vector
<Node
> d_formals
;
93 DefinedFunction(Node func
, vector
<Node
> formals
, Node formula
) :
98 Node
getFunction() const { return d_func
; }
99 vector
<Node
> getFormals() const { return d_formals
; }
100 Node
getFormula() const { return d_formula
; }
101 };/* class DefinedFunction */
103 struct SmtEngineStatistics
{
104 /** time spent in definition-expansion */
105 TimerStat d_definitionExpansionTime
;
106 /** time spent in non-clausal simplification */
107 TimerStat d_nonclausalSimplificationTime
;
108 /** Num of constant propagations found during nonclausal simp */
109 IntStat d_numConstantProps
;
110 /** time spent in static learning */
111 TimerStat d_staticLearningTime
;
112 /** time spent in simplifying ITEs */
113 TimerStat d_simpITETime
;
114 /** time spent in simplifying ITEs */
115 TimerStat d_unconstrainedSimpTime
;
116 /** time spent removing ITEs */
117 TimerStat d_iteRemovalTime
;
118 /** time spent in theory preprocessing */
119 TimerStat d_theoryPreprocessTime
;
120 /** time spent converting to CNF */
121 TimerStat d_cnfConversionTime
;
122 /** Num of assertions before ite removal */
123 IntStat d_numAssertionsPre
;
124 /** Num of assertions after ite removal */
125 IntStat d_numAssertionsPost
;
126 /** time spent in checkModel() */
127 TimerStat d_checkModelTime
;
129 SmtEngineStatistics() :
130 d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"),
131 d_nonclausalSimplificationTime("smt::SmtEngine::nonclausalSimplificationTime"),
132 d_numConstantProps("smt::SmtEngine::numConstantProps", 0),
133 d_staticLearningTime("smt::SmtEngine::staticLearningTime"),
134 d_simpITETime("smt::SmtEngine::simpITETime"),
135 d_unconstrainedSimpTime("smt::SmtEngine::unconstrainedSimpTime"),
136 d_iteRemovalTime("smt::SmtEngine::iteRemovalTime"),
137 d_theoryPreprocessTime("smt::SmtEngine::theoryPreprocessTime"),
138 d_cnfConversionTime("smt::SmtEngine::cnfConversionTime"),
139 d_numAssertionsPre("smt::SmtEngine::numAssertionsPreITERemoval", 0),
140 d_numAssertionsPost("smt::SmtEngine::numAssertionsPostITERemoval", 0),
141 d_checkModelTime("smt::SmtEngine::checkModelTime") {
143 StatisticsRegistry::registerStat(&d_definitionExpansionTime
);
144 StatisticsRegistry::registerStat(&d_nonclausalSimplificationTime
);
145 StatisticsRegistry::registerStat(&d_numConstantProps
);
146 StatisticsRegistry::registerStat(&d_staticLearningTime
);
147 StatisticsRegistry::registerStat(&d_simpITETime
);
148 StatisticsRegistry::registerStat(&d_unconstrainedSimpTime
);
149 StatisticsRegistry::registerStat(&d_iteRemovalTime
);
150 StatisticsRegistry::registerStat(&d_theoryPreprocessTime
);
151 StatisticsRegistry::registerStat(&d_cnfConversionTime
);
152 StatisticsRegistry::registerStat(&d_numAssertionsPre
);
153 StatisticsRegistry::registerStat(&d_numAssertionsPost
);
154 StatisticsRegistry::registerStat(&d_checkModelTime
);
157 ~SmtEngineStatistics() {
158 StatisticsRegistry::unregisterStat(&d_definitionExpansionTime
);
159 StatisticsRegistry::unregisterStat(&d_nonclausalSimplificationTime
);
160 StatisticsRegistry::unregisterStat(&d_numConstantProps
);
161 StatisticsRegistry::unregisterStat(&d_staticLearningTime
);
162 StatisticsRegistry::unregisterStat(&d_simpITETime
);
163 StatisticsRegistry::unregisterStat(&d_unconstrainedSimpTime
);
164 StatisticsRegistry::unregisterStat(&d_iteRemovalTime
);
165 StatisticsRegistry::unregisterStat(&d_theoryPreprocessTime
);
166 StatisticsRegistry::unregisterStat(&d_cnfConversionTime
);
167 StatisticsRegistry::unregisterStat(&d_numAssertionsPre
);
168 StatisticsRegistry::unregisterStat(&d_numAssertionsPost
);
169 StatisticsRegistry::unregisterStat(&d_checkModelTime
);
171 };/* struct SmtEngineStatistics */
174 * This is an inelegant solution, but for the present, it will work.
175 * The point of this is to separate the public and private portions of
176 * the SmtEngine class, so that smt_engine.h doesn't
177 * include "expr/node.h", which is a private CVC4 header (and can lead
178 * to linking errors due to the improper inlining of non-visible symbols
181 * The "real" solution (that which is usually implemented) is to move
182 * ALL the implementation to SmtEnginePrivate and maintain a
183 * heap-allocated instance of it in SmtEngine. SmtEngine (the public
184 * one) becomes an "interface shell" which simply acts as a forwarder
187 class SmtEnginePrivate
: public NodeManagerListener
{
190 /** The assertions yet to be preprocessed */
191 vector
<Node
> d_assertionsToPreprocess
;
193 /** Learned literals */
194 vector
<Node
> d_nonClausalLearnedLiterals
;
196 /** Size of assertions array when preprocessing starts */
197 unsigned d_realAssertionsEnd
;
199 /** A circuit propagator for non-clausal propositional deduction */
200 booleans::CircuitPropagator d_propagator
;
202 /** Assertions to push to sat */
203 vector
<Node
> d_assertionsToCheck
;
206 * A context that never pushes/pops, for use by CD structures (like
207 * SubstitutionMaps) that should be "global".
209 context::Context d_fakeContext
;
212 * A map of AbsractValues to their actual constants. Only used if
213 * options::abstractValues() is on.
215 theory::SubstitutionMap d_abstractValueMap
;
218 * A mapping of all abstract values (actual value |-> abstract) that
219 * we've handed out. This is necessary to ensure that we give the
220 * same AbstractValues for the same real constants. Only used if
221 * options::abstractValues() is on.
223 hash_map
<Node
, Node
, NodeHashFunction
> d_abstractValues
;
226 * Function symbol used to implement uninterpreted division-by-zero
227 * semantics. Needed to deal with partial division function ("/").
232 * Maps from bit-vector width to divison-by-zero uninterpreted
235 hash_map
<unsigned, Node
> d_BVDivByZero
;
236 hash_map
<unsigned, Node
> d_BVRemByZero
;
240 * Function symbol used to implement uninterpreted
241 * int-division-by-zero semantics. Needed to deal with partial
247 * Function symbol used to implement uninterpreted mod-zero
248 * semantics. Needed to deal with partial function "mod".
253 * Map from skolem variables to index in d_assertionsToCheck containing
254 * corresponding introduced Boolean ite
256 IteSkolemMap d_iteSkolemMap
;
260 /** Instance of the ITE remover */
261 RemoveITE d_iteRemover
;
264 /** The top level substitutions */
265 SubstitutionMap d_topLevelSubstitutions
;
268 * The last substitution that the SAT layer was told about.
269 * In incremental settings, substitutions cannot be performed
270 * "backward," only forward. So SAT needs to be told of all
271 * substitutions that are going to be done. This iterator
272 * holds the last substitution from d_topLevelSubstitutions
273 * that was pushed out to SAT.
274 * If d_lastSubstitutionPos == d_topLevelSubstitutions.end(),
275 * then nothing has been pushed out yet.
277 context::CDO
<SubstitutionMap::iterator
> d_lastSubstitutionPos
;
279 static const bool d_doConstantProp
= true;
282 * Runs the nonclausal solver and tries to solve all the assigned
285 * Returns false if the formula simplifies to "false"
287 bool nonClausalSimplify();
290 * Performs static learning on the assertions.
292 void staticLearning();
295 * Remove ITEs from the assertions.
300 * Helper function to fix up assertion list to restore invariants needed after ite removal
302 bool checkForBadSkolems(TNode n
, TNode skolem
, hash_map
<Node
, bool, NodeHashFunction
>& cache
);
305 // Simplify ITE structure
308 // Simplify based on unconstrained values
309 void unconstrainedSimp();
312 * Any variable in an assertion that is declared as a subtype type
313 * (predicate subtype or integer subrange type) must be constrained
314 * to be in that type.
316 void constrainSubtypes(TNode n
, std::vector
<Node
>& assertions
)
320 * Perform non-clausal simplification of a Node. This involves
321 * Theory implementations, but does NOT involve the SAT solver in
324 * Returns false if the formula simplifies to "false"
326 bool simplifyAssertions() throw(TypeCheckingException
, LogicException
);
330 SmtEnginePrivate(SmtEngine
& smt
) :
332 d_assertionsToPreprocess(),
333 d_nonClausalLearnedLiterals(),
334 d_realAssertionsEnd(0),
335 d_propagator(d_nonClausalLearnedLiterals
, true, true),
336 d_assertionsToCheck(),
338 d_abstractValueMap(&d_fakeContext
),
344 d_iteRemover(smt
.d_userContext
),
345 d_topLevelSubstitutions(smt
.d_userContext
),
346 d_lastSubstitutionPos(smt
.d_userContext
, d_topLevelSubstitutions
.end()) {
347 d_smt
.d_nodeManager
->subscribeEvents(this);
350 void nmNotifyNewSort(TypeNode tn
) {
351 DeclareTypeCommand
c(tn
.getAttribute(expr::VarNameAttr()),
354 d_smt
.addToModelCommandAndDump(c
);
357 void nmNotifyNewSortConstructor(TypeNode tn
) {
358 DeclareTypeCommand
c(tn
.getAttribute(expr::VarNameAttr()),
359 tn
.getAttribute(expr::SortArityAttr()),
361 d_smt
.addToModelCommandAndDump(c
);
364 void nmNotifyNewDatatypes(const std::vector
<DatatypeType
>& dtts
) {
365 DatatypeDeclarationCommand
c(dtts
);
366 d_smt
.addToModelCommandAndDump(c
);
369 void nmNotifyNewVar(TNode n
) {
370 DeclareFunctionCommand
c(n
.getAttribute(expr::VarNameAttr()),
372 n
.getType().toType());
373 d_smt
.addToModelCommandAndDump(c
);
376 void nmNotifyNewSkolem(TNode n
, const std::string
& comment
) {
377 std::string id
= n
.getAttribute(expr::VarNameAttr());
378 DeclareFunctionCommand
c(id
,
380 n
.getType().toType());
381 if(Dump
.isOn("skolems") && comment
!= "") {
382 Dump("skolems") << CommentCommand(id
+ " is " + comment
);
384 d_smt
.addToModelCommandAndDump(c
, "skolems");
387 Node
applySubstitutions(TNode node
) const {
388 return Rewriter::rewrite(d_topLevelSubstitutions
.apply(node
));
392 * Process the assertions that have been asserted.
394 void processAssertions();
397 * Process a user pop. Clears out the non-context-dependent stuff in this
398 * SmtEnginePrivate. Necessary to clear out our assertion vectors in case
399 * someone does a push-assert-pop without a check-sat.
402 d_assertionsToPreprocess
.clear();
403 d_nonClausalLearnedLiterals
.clear();
404 d_assertionsToCheck
.clear();
405 d_realAssertionsEnd
= 0;
406 d_iteSkolemMap
.clear();
410 * Adds a formula to the current context. Action here depends on
411 * the SimplificationMode (in the current Options scope); the
412 * formula might be pushed out to the propositional layer
413 * immediately, or it might be simplified and kept, or it might not
414 * even be simplified.
416 void addFormula(TNode n
)
417 throw(TypeCheckingException
, LogicException
);
420 * Return the uinterpreted function symbol corresponding to division-by-zero
421 * for this particular bit-wdith
422 * @param k should be UREM or UDIV
427 Node
getBVDivByZero(Kind k
, unsigned width
);
430 * Returns the node modeling the division-by-zero semantics of node n.
436 Node
expandBVDivByZero(TNode n
);
439 * Expand definitions in n.
441 Node
expandDefinitions(TNode n
, hash_map
<Node
, Node
, NodeHashFunction
>& cache
)
442 throw(TypeCheckingException
, LogicException
);
445 * Simplify node "in" by expanding definitions and applying any
446 * substitutions learned from preprocessing.
448 Node
simplify(TNode in
) {
449 // Substitute out any abstract values in ex.
450 // Expand definitions.
451 hash_map
<Node
, Node
, NodeHashFunction
> cache
;
452 Node n
= expandDefinitions(in
, cache
).toExpr();
453 // Make sure we've done all preprocessing, etc.
454 Assert(d_assertionsToCheck
.size() == 0 && d_assertionsToPreprocess
.size() == 0);
455 return applySubstitutions(n
).toExpr();
459 * Pre-skolemize quantifiers.
461 Node
preSkolemizeQuantifiers(Node n
, bool polarity
, std::vector
<Node
>& fvs
);
464 * Substitute away all AbstractValues in a node.
466 Node
substituteAbstractValues(TNode n
) {
467 // We need to do this even if options::abstractValues() is off,
468 // since the setting might have changed after we already gave out
469 // some abstract values.
470 return d_abstractValueMap
.apply(n
);
474 * Make a new (or return an existing) abstract value for a node.
475 * Can only use this if options::abstractValues() is on.
477 Node
mkAbstractValue(TNode n
) {
478 Assert(options::abstractValues());
479 Node
& val
= d_abstractValues
[n
];
481 val
= d_smt
.d_nodeManager
->mkConst(AbstractValue(d_abstractValues
.size()));
482 d_abstractValueMap
.addSubstitution(val
, n
);
487 };/* class SmtEnginePrivate */
489 }/* namespace CVC4::smt */
491 using namespace CVC4::smt
;
493 SmtEngine::SmtEngine(ExprManager
* em
) throw() :
494 d_context(em
->getContext()),
496 d_userContext(new UserContext()),
498 d_nodeManager(d_exprManager
->getNodeManager()),
499 d_decisionEngine(NULL
),
500 d_theoryEngine(NULL
),
502 d_definedFunctions(NULL
),
503 d_assertionList(NULL
),
505 d_modelCommands(NULL
),
509 d_fullyInited(false),
510 d_problemExtended(false),
512 d_needPostsolve(false),
513 d_earlyTheoryPP(true),
514 d_timeBudgetCumulative(0),
515 d_timeBudgetPerCall(0),
516 d_resourceBudgetCumulative(0),
517 d_resourceBudgetPerCall(0),
518 d_cumulativeTimeUsed(0),
519 d_cumulativeResourceUsed(0),
521 d_private(new smt::SmtEnginePrivate(*this)),
522 d_statisticsRegistry(new StatisticsRegistry()),
526 d_stats
= new SmtEngineStatistics();
528 // We have mutual dependency here, so we add the prop engine to the theory
529 // engine later (it is non-essential there)
530 d_theoryEngine
= new TheoryEngine(d_context
, d_userContext
, d_private
->d_iteRemover
, const_cast<const LogicInfo
&>(d_logic
));
533 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
534 #undef CVC4_FOR_EACH_THEORY_STATEMENT
536 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
537 d_theoryEngine->addTheory<TheoryTraits<THEORY>::theory_class>(THEORY);
538 CVC4_FOR_EACH_THEORY
;
540 // global push/pop around everything, to ensure proper destruction
541 // of context-dependent data structures
542 d_userContext
->push();
545 d_definedFunctions
= new(true) DefinedFunctionMap(d_userContext
);
546 d_modelCommands
= new(true) smt::CommandList(d_userContext
);
549 void SmtEngine::finishInit() {
550 d_decisionEngine
= new DecisionEngine(d_context
, d_userContext
);
551 d_decisionEngine
->init(); // enable appropriate strategies
553 d_propEngine
= new PropEngine(d_theoryEngine
, d_decisionEngine
, d_context
, d_userContext
);
555 d_theoryEngine
->setPropEngine(d_propEngine
);
556 d_theoryEngine
->setDecisionEngine(d_decisionEngine
);
558 // [MGD 10/20/2011] keep around in incremental mode, due to a
559 // cleanup ordering issue and Nodes/TNodes. If SAT is popped
560 // first, some user-context-dependent TNodes might still exist
562 if(options::interactive() ||
563 options::incrementalSolving()) {
564 // In the case of incremental solving, we appear to need these to
565 // ensure the relevant Nodes remain live.
566 d_assertionList
= new(true) AssertionList(d_userContext
);
569 // dump out a set-logic command
570 if(Dump
.isOn("benchmark")) {
571 // Dump("benchmark") << SetBenchmarkLogicCommand(logic.getLogicString());
572 LogicInfo everything
;
574 Dump("benchmark") << CommentCommand("CVC4 always dumps the most general, \"all-supported\" logic (above), as some internals might require the use of a logic more general than the input.")
575 << SetBenchmarkLogicCommand(everything
.getLogicString());
578 // dump out any pending declaration commands
579 for(unsigned i
= 0; i
< d_dumpCommands
.size(); ++i
) {
580 Dump("declarations") << *d_dumpCommands
[i
];
581 delete d_dumpCommands
[i
];
583 d_dumpCommands
.clear();
585 if(options::perCallResourceLimit() != 0) {
586 setResourceLimit(options::perCallResourceLimit(), false);
588 if(options::cumulativeResourceLimit() != 0) {
589 setResourceLimit(options::cumulativeResourceLimit(), true);
591 if(options::perCallMillisecondLimit() != 0) {
592 setTimeLimit(options::perCallMillisecondLimit(), false);
594 if(options::cumulativeMillisecondLimit() != 0) {
595 setTimeLimit(options::cumulativeMillisecondLimit(), true);
599 void SmtEngine::finalOptionsAreSet() {
604 if(options::checkModels()) {
605 if(! options::produceModels()) {
606 Notice() << "SmtEngine: turning on produce-models to support check-model" << std::endl
;
607 setOption("produce-models", SExpr("true"));
609 if(! options::interactive()) {
610 Notice() << "SmtEngine: turning on interactive-mode to support check-model" << std::endl
;
611 setOption("interactive-mode", SExpr("true"));
615 if(! d_logic
.isLocked()) {
616 // ensure that our heuristics are properly set up
620 // finish initalization, creat the prop engine, etc.
623 AlwaysAssert( d_propEngine
->getAssertionLevel() == 0,
624 "The PropEngine has pushed but the SmtEngine "
625 "hasn't finished initializing!" );
627 d_fullyInited
= true;
628 Assert(d_logic
.isLocked());
630 d_propEngine
->assertFormula(NodeManager::currentNM()->mkConst
<bool>(true));
631 d_propEngine
->assertFormula(NodeManager::currentNM()->mkConst
<bool>(false).notNode());
634 void SmtEngine::shutdown() {
637 while(options::incrementalSolving() && d_userContext
->getLevel() > 1) {
641 // check to see if a postsolve() is pending
642 if(d_needPostsolve
) {
643 d_theoryEngine
->postsolve();
644 d_needPostsolve
= false;
647 if(d_propEngine
!= NULL
) {
648 d_propEngine
->shutdown();
650 if(d_theoryEngine
!= NULL
) {
651 d_theoryEngine
->shutdown();
653 if(d_decisionEngine
!= NULL
) {
654 d_decisionEngine
->shutdown();
658 SmtEngine::~SmtEngine() throw() {
664 // global push/pop around everything, to ensure proper destruction
665 // of context-dependent data structures
667 d_userContext
->pop();
669 if(d_assignments
!= NULL
) {
670 d_assignments
->deleteSelf();
673 if(d_assertionList
!= NULL
) {
674 d_assertionList
->deleteSelf();
677 for(unsigned i
= 0; i
< d_dumpCommands
.size(); ++i
) {
678 delete d_dumpCommands
[i
];
680 d_dumpCommands
.clear();
682 if(d_modelCommands
!= NULL
) {
683 d_modelCommands
->deleteSelf();
686 d_definedFunctions
->deleteSelf();
692 delete d_theoryEngine
;
694 delete d_decisionEngine
;
696 delete d_userContext
;
698 delete d_statisticsRegistry
;
700 } catch(Exception
& e
) {
701 Warning() << "CVC4 threw an exception during cleanup." << endl
706 void SmtEngine::setLogic(const LogicInfo
& logic
) throw(ModalException
) {
713 void SmtEngine::setLogic(const std::string
& s
) throw(ModalException
) {
716 setLogic(LogicInfo(s
));
719 LogicInfo
SmtEngine::getLogicInfo() const {
723 // This function is called when d_logic has just been changed.
724 // The LogicInfo isn't passed in explicitly, because that might
725 // tempt people in the code to use the (potentially unlocked)
726 // version that's passed in, leading to assert-fails in certain
727 // uses of the CVC4 library.
728 void SmtEngine::setLogicInternal() throw() {
729 Assert(!d_fullyInited
, "setting logic in SmtEngine but the engine has already finished initializing for this run");
733 // may need to force uninterpreted functions to be on for non-linear
734 if(((d_logic
.isTheoryEnabled(theory::THEORY_ARITH
) && !d_logic
.isLinear()) ||
735 d_logic
.isTheoryEnabled(theory::THEORY_BV
)) &&
736 !d_logic
.isTheoryEnabled(theory::THEORY_UF
)){
737 d_logic
= d_logic
.getUnlockedCopy();
738 d_logic
.enableTheory(theory::THEORY_UF
);
742 // Set the options for the theoryOf
743 if(!options::theoryOfMode
.wasSetByUser()) {
744 if(d_logic
.isSharingEnabled() && !d_logic
.isTheoryEnabled(THEORY_BV
)) {
745 Theory::setTheoryOfMode(THEORY_OF_TERM_BASED
);
747 Theory::setTheoryOfMode(THEORY_OF_TYPE_BASED
);
750 Theory::setTheoryOfMode(options::theoryOfMode());
753 // by default, symmetry breaker is on only for QF_UF
754 if(! options::ufSymmetryBreaker
.wasSetByUser()) {
755 bool qf_uf
= d_logic
.isPure(THEORY_UF
) && !d_logic
.isQuantified();
756 Trace("smt") << "setting uf symmetry breaker to " << qf_uf
<< std::endl
;
757 options::ufSymmetryBreaker
.set(qf_uf
);
759 // by default, nonclausal simplification is off for QF_SAT and for quantifiers
760 if(! options::simplificationMode
.wasSetByUser()) {
761 bool qf_sat
= d_logic
.isPure(THEORY_BOOL
) && !d_logic
.isQuantified();
762 bool quantifiers
= d_logic
.isQuantified();
763 Trace("smt") << "setting simplification mode to <" << d_logic
.getLogicString() << "> " << (!qf_sat
&& !quantifiers
) << std::endl
;
764 //simplifaction=none works better for SMT LIB benchmarks with quantifiers, not others
765 //options::simplificationMode.set(qf_sat || quantifiers ? SIMPLIFICATION_MODE_NONE : SIMPLIFICATION_MODE_BATCH);
766 options::simplificationMode
.set(qf_sat
? SIMPLIFICATION_MODE_NONE
: SIMPLIFICATION_MODE_BATCH
);
769 // If in arrays, set the UF handler to arrays
770 if(d_logic
.isTheoryEnabled(THEORY_ARRAY
) && !d_logic
.isQuantified()) {
771 Theory::setUninterpretedSortOwner(THEORY_ARRAY
);
773 Theory::setUninterpretedSortOwner(THEORY_UF
);
775 // Turn on ite simplification for QF_LIA and QF_AUFBV
776 if(! options::doITESimp
.wasSetByUser()) {
777 bool iteSimp
= !d_logic
.isQuantified() &&
778 ((d_logic
.isPure(THEORY_ARITH
) && d_logic
.isLinear() && !d_logic
.isDifferenceLogic() && !d_logic
.areRealsUsed()) ||
779 (d_logic
.isTheoryEnabled(THEORY_ARRAY
) && d_logic
.isTheoryEnabled(THEORY_UF
) && d_logic
.isTheoryEnabled(THEORY_BV
)));
780 Trace("smt") << "setting ite simplification to " << iteSimp
<< std::endl
;
781 options::doITESimp
.set(iteSimp
);
783 // Turn on multiple-pass non-clausal simplification for QF_AUFBV
784 if(! options::repeatSimp
.wasSetByUser()) {
785 bool repeatSimp
= !d_logic
.isQuantified() &&
786 (d_logic
.isTheoryEnabled(THEORY_ARRAY
) && d_logic
.isTheoryEnabled(THEORY_UF
) && d_logic
.isTheoryEnabled(THEORY_BV
));
787 Trace("smt") << "setting repeat simplification to " << repeatSimp
<< std::endl
;
788 options::repeatSimp
.set(repeatSimp
);
790 // Turn on unconstrained simplification for QF_AUFBV
791 if(! options::unconstrainedSimp
.wasSetByUser() || options::incrementalSolving()) {
792 // bool qf_sat = d_logic.isPure(THEORY_BOOL) && !d_logic.isQuantified();
793 // bool uncSimp = false && !qf_sat && !options::incrementalSolving();
794 bool uncSimp
= !options::incrementalSolving() && !d_logic
.isQuantified() && !options::produceModels() && !options::checkModels() &&
795 (d_logic
.isTheoryEnabled(THEORY_ARRAY
) && d_logic
.isTheoryEnabled(THEORY_BV
));
796 Trace("smt") << "setting unconstrained simplification to " << uncSimp
<< std::endl
;
797 options::unconstrainedSimp
.set(uncSimp
);
799 // Unconstrained simp currently does *not* support model generation
800 if (options::unconstrainedSimp
.wasSetByUser() && options::unconstrainedSimp()) {
801 if (options::produceModels()) {
802 Notice() << "SmtEngine: turning off produce-models to support unconstrainedSimp" << std::endl
;
803 setOption("produce-models", SExpr("false"));
805 if (options::checkModels()) {
806 Notice() << "SmtEngine: turning off check-models to support unconstrainedSimp" << std::endl
;
807 setOption("check-models", SExpr("false"));
810 // Turn on arith rewrite equalities only for pure arithmetic
811 if(! options::arithRewriteEq
.wasSetByUser()) {
812 bool arithRewriteEq
= d_logic
.isPure(THEORY_ARITH
) && !d_logic
.isQuantified();
813 Trace("smt") << "setting arith rewrite equalities " << arithRewriteEq
<< std::endl
;
814 options::arithRewriteEq
.set(arithRewriteEq
);
816 if(! options::arithHeuristicPivots
.wasSetByUser()) {
817 int16_t heuristicPivots
= 5;
818 if(d_logic
.isPure(THEORY_ARITH
) && !d_logic
.isQuantified()) {
819 if(d_logic
.isDifferenceLogic()) {
820 heuristicPivots
= -1;
821 } else if(!d_logic
.areIntegersUsed()) {
825 Trace("smt") << "setting arithHeuristicPivots " << heuristicPivots
<< std::endl
;
826 options::arithHeuristicPivots
.set(heuristicPivots
);
828 if(! options::arithPivotThreshold
.wasSetByUser()){
829 uint16_t pivotThreshold
= 2;
830 if(d_logic
.isPure(THEORY_ARITH
) && !d_logic
.isQuantified()){
831 if(d_logic
.isDifferenceLogic()){
835 Trace("smt") << "setting arith arithPivotThreshold " << pivotThreshold
<< std::endl
;
836 options::arithPivotThreshold
.set(pivotThreshold
);
838 if(! options::arithStandardCheckVarOrderPivots
.wasSetByUser()){
839 int16_t varOrderPivots
= -1;
840 if(d_logic
.isPure(THEORY_ARITH
) && !d_logic
.isQuantified()){
841 varOrderPivots
= 200;
843 Trace("smt") << "setting arithStandardCheckVarOrderPivots " << varOrderPivots
<< std::endl
;
844 options::arithStandardCheckVarOrderPivots
.set(varOrderPivots
);
846 // Turn off early theory preprocessing if arithRewriteEq is on
847 if (options::arithRewriteEq()) {
848 d_earlyTheoryPP
= false;
850 // Turn on justification heuristic of the decision engine for QF_BV and QF_AUFBV
851 // and also use it in stop-only mode for QF_AUFLIA, QF_LRA and Quantifiers
852 // BUT use neither in ALL_SUPPORTED mode (since it doesn't yet work well
853 // with incrementality)
854 if(!options::decisionMode
.wasSetByUser()) {
855 decision::DecisionMode decMode
=
857 d_logic
.hasEverything() ? decision::DECISION_STRATEGY_INTERNAL
:
859 (not d_logic
.isQuantified() &&
860 d_logic
.isPure(THEORY_BV
)
862 // QF_AUFBV or QF_ABV or QF_UFBV
863 (not d_logic
.isQuantified() &&
864 (d_logic
.isTheoryEnabled(THEORY_ARRAY
) ||
865 d_logic
.isTheoryEnabled(THEORY_UF
)) &&
866 d_logic
.isTheoryEnabled(THEORY_BV
)
868 // QF_AUFLIA (and may be ends up enabling QF_AUFLRA?)
869 (not d_logic
.isQuantified() &&
870 d_logic
.isTheoryEnabled(THEORY_ARRAY
) &&
871 d_logic
.isTheoryEnabled(THEORY_UF
) &&
872 d_logic
.isTheoryEnabled(THEORY_ARITH
)
875 (not d_logic
.isQuantified() &&
876 d_logic
.isPure(THEORY_ARITH
) && d_logic
.isLinear() && !d_logic
.isDifferenceLogic() && !d_logic
.areIntegersUsed()
879 d_logic
.isQuantified()
880 ? decision::DECISION_STRATEGY_JUSTIFICATION
881 : decision::DECISION_STRATEGY_INTERNAL
886 d_logic
.hasEverything() ? false :
888 (not d_logic
.isQuantified() &&
889 d_logic
.isTheoryEnabled(THEORY_ARRAY
) &&
890 d_logic
.isTheoryEnabled(THEORY_UF
) &&
891 d_logic
.isTheoryEnabled(THEORY_ARITH
)
894 (not d_logic
.isQuantified() &&
895 d_logic
.isPure(THEORY_ARITH
) && d_logic
.isLinear() && !d_logic
.isDifferenceLogic() && !d_logic
.areIntegersUsed()
898 d_logic
.isQuantified()
902 Trace("smt") << "setting decision mode to " << decMode
<< std::endl
;
903 options::decisionMode
.set(decMode
);
904 options::decisionStopOnly
.set(stoponly
);
907 //for finite model finding
908 if( ! options::instWhenMode
.wasSetByUser()){
909 if( options::fmfInstEngine() ){
910 Trace("smt") << "setting inst when mode to LAST_CALL" << std::endl
;
911 options::instWhenMode
.set( INST_WHEN_LAST_CALL
);
915 //until bugs 371,431 are fixed
916 if( ! options::minisatUseElim
.wasSetByUser()){
917 if( d_logic
.isQuantified() || options::produceModels() || options::checkModels() ){
918 options::minisatUseElim
.set( false );
921 else if (options::minisatUseElim()) {
922 if (options::produceModels()) {
923 Notice() << "SmtEngine: turning off produce-models to support minisatUseElim" << std::endl
;
924 setOption("produce-models", SExpr("false"));
926 if (options::checkModels()) {
927 Notice() << "SmtEngine: turning off check-models to support minisatUseElim" << std::endl
;
928 setOption("check-models", SExpr("false"));
932 // For now, these array theory optimizations do not support model-building
933 if (options::produceModels() || options::checkModels()) {
934 options::arraysOptimizeLinear
.set(false);
935 options::arraysLazyRIntro1
.set(false);
938 // Non-linear arithmetic does not support models
939 if (d_logic
.isTheoryEnabled(theory::THEORY_ARITH
) &&
940 !d_logic
.isLinear()) {
941 if (options::produceModels()) {
942 Warning() << "SmtEngine: turning off produce-models because unsupported for nonlinear arith" << std::endl
;
943 setOption("produce-models", SExpr("false"));
945 if (options::checkModels()) {
946 Warning() << "SmtEngine: turning off check-models because unsupported for nonlinear arith" << std::endl
;
947 setOption("check-models", SExpr("false"));
952 void SmtEngine::setInfo(const std::string
& key
, const CVC4::SExpr
& value
)
953 throw(OptionException
, ModalException
) {
957 Trace("smt") << "SMT setInfo(" << key
<< ", " << value
<< ")" << endl
;
958 if(Dump
.isOn("benchmark")) {
959 if(key
== "status") {
960 std::string s
= value
.getValue();
961 BenchmarkStatus status
=
962 (s
== "sat") ? SMT_SATISFIABLE
:
963 ((s
== "unsat") ? SMT_UNSATISFIABLE
: SMT_UNKNOWN
);
964 Dump("benchmark") << SetBenchmarkStatusCommand(status
);
966 Dump("benchmark") << SetInfoCommand(key
, value
);
970 // Check for CVC4-specific info keys (prefixed with "cvc4-" or "cvc4_")
971 if(key
.length() > 5) {
972 string prefix
= key
.substr(0, 5);
973 if(prefix
== "cvc4-" || prefix
== "cvc4_") {
974 string cvc4key
= key
.substr(5);
975 if(cvc4key
== "logic") {
976 if(! value
.isAtom()) {
977 throw OptionException("argument to (set-info :cvc4-logic ..) must be a string");
980 d_logic
= value
.getValue();
984 throw UnrecognizedOptionException();
989 // Check for standard info keys (SMT-LIB v1, SMT-LIB v2, ...)
993 key
== "difficulty" ||
997 } else if(key
== "smt-lib-version") {
998 if( (value
.isInteger() && value
.getIntegerValue() == Integer(2)) ||
999 (value
.isRational() && value
.getRationalValue() == Rational(2)) ||
1000 (value
.getValue() == "2") ) {
1001 // supported SMT-LIB version
1004 Warning() << "Warning: unsupported smt-lib-version: " << value
<< endl
;
1005 throw UnrecognizedOptionException();
1006 } else if(key
== "status") {
1008 if(value
.isAtom()) {
1009 s
= value
.getValue();
1011 if(s
!= "sat" && s
!= "unsat" && s
!= "unknown") {
1012 throw OptionException("argument to (set-info :status ..) must be "
1013 "`sat' or `unsat' or `unknown'");
1015 d_status
= Result(s
);
1018 throw UnrecognizedOptionException();
1021 CVC4::SExpr
SmtEngine::getInfo(const std::string
& key
) const
1022 throw(OptionException
, ModalException
) {
1024 SmtScope
smts(this);
1026 Trace("smt") << "SMT getInfo(" << key
<< ")" << endl
;
1027 if(key
== "all-statistics") {
1028 vector
<SExpr
> stats
;
1029 for(StatisticsRegistry::const_iterator i
= NodeManager::fromExprManager(d_exprManager
)->getStatisticsRegistry()->begin();
1030 i
!= NodeManager::fromExprManager(d_exprManager
)->getStatisticsRegistry()->end();
1033 v
.push_back((*i
).first
);
1034 v
.push_back((*i
).second
);
1037 for(StatisticsRegistry::const_iterator i
= d_statisticsRegistry
->begin();
1038 i
!= d_statisticsRegistry
->end();
1041 v
.push_back((*i
).first
);
1042 v
.push_back((*i
).second
);
1046 } else if(key
== "error-behavior") {
1047 // immediate-exit | continued-execution
1048 return SExpr::Keyword("immediate-exit");
1049 } else if(key
== "name") {
1050 return Configuration::getName();
1051 } else if(key
== "version") {
1052 return Configuration::getVersionString();
1053 } else if(key
== "authors") {
1054 return Configuration::about();
1055 } else if(key
== "status") {
1056 // sat | unsat | unknown
1057 switch(d_status
.asSatisfiabilityResult().isSat()) {
1059 return SExpr::Keyword("sat");
1061 return SExpr::Keyword("unsat");
1063 return SExpr::Keyword("unknown");
1065 } else if(key
== "reason-unknown") {
1066 if(!d_status
.isNull() && d_status
.isUnknown()) {
1068 ss
<< d_status
.whyUnknown();
1069 string s
= ss
.str();
1070 transform(s
.begin(), s
.end(), s
.begin(), ::tolower
);
1071 return SExpr::Keyword(s
);
1073 throw ModalException("Can't get-info :reason-unknown when the "
1074 "last result wasn't unknown!");
1077 throw UnrecognizedOptionException();
1081 void SmtEngine::defineFunction(Expr func
,
1082 const std::vector
<Expr
>& formals
,
1084 Trace("smt") << "SMT defineFunction(" << func
<< ")" << endl
;
1085 if(Dump
.isOn("declarations")) {
1087 ss
<< Expr::setlanguage(Expr::setlanguage::getLanguage(Dump
.getStream()))
1089 Dump("declarations") << DefineFunctionCommand(ss
.str(), func
, formals
, formula
);
1091 SmtScope
smts(this);
1093 // Substitute out any abstract values in formula
1094 Expr form
= d_private
->substituteAbstractValues(Node::fromExpr(formula
)).toExpr();
1097 Type formulaType
= form
.getType(options::typeChecking());
1099 Type funcType
= func
.getType();
1100 // We distinguish here between definitions of constants and functions,
1101 // because the type checking for them is subtly different. Perhaps we
1102 // should instead have SmtEngine::defineFunction() and
1103 // SmtEngine::defineConstant() for better clarity, although then that
1104 // doesn't match the SMT-LIBv2 standard...
1105 if(formals
.size() > 0) {
1106 Type rangeType
= FunctionType(funcType
).getRangeType();
1107 if(! formulaType
.isComparableTo(rangeType
)) {
1109 ss
<< "Type of defined function does not match its declaration\n"
1110 << "The function : " << func
<< "\n"
1111 << "Declared type : " << rangeType
<< "\n"
1112 << "The body : " << formula
<< "\n"
1113 << "Body type : " << formulaType
;
1114 throw TypeCheckingException(func
, ss
.str());
1117 if(! formulaType
.isComparableTo(funcType
)) {
1119 ss
<< "Declared type of defined constant does not match its definition\n"
1120 << "The constant : " << func
<< "\n"
1121 << "Declared type : " << funcType
<< "\n"
1122 << "The definition : " << formula
<< "\n"
1123 << "Definition type: " << formulaType
;
1124 throw TypeCheckingException(func
, ss
.str());
1127 TNode funcNode
= func
.getTNode();
1128 vector
<Node
> formalsNodes
;
1129 for(vector
<Expr
>::const_iterator i
= formals
.begin(),
1130 iend
= formals
.end();
1133 formalsNodes
.push_back((*i
).getNode());
1135 TNode formNode
= form
.getTNode();
1136 DefinedFunction
def(funcNode
, formalsNodes
, formNode
);
1137 // Permit (check-sat) (define-fun ...) (get-value ...) sequences.
1138 // Otherwise, (check-sat) (get-value ((! foo :named bar))) breaks
1139 // d_haveAdditions = true;
1140 Debug("smt") << "definedFunctions insert " << funcNode
<< " " << formNode
<< std::endl
;
1141 d_definedFunctions
->insert(funcNode
, def
);
1145 Node
SmtEnginePrivate::getBVDivByZero(Kind k
, unsigned width
) {
1146 NodeManager
* nm
= d_smt
.d_nodeManager
;
1147 if (k
== kind::BITVECTOR_UDIV
) {
1148 if (d_BVDivByZero
.find(width
) == d_BVDivByZero
.end()) {
1149 // lazily create the function symbols
1150 std::ostringstream os
;
1151 os
<< "BVUDivByZero_" << width
;
1152 Node divByZero
= nm
->mkSkolem(os
.str(),
1153 nm
->mkFunctionType(nm
->mkBitVectorType(width
), nm
->mkBitVectorType(width
)),
1154 "partial bvudiv", NodeManager::SKOLEM_EXACT_NAME
);
1155 d_BVDivByZero
[width
] = divByZero
;
1157 return d_BVDivByZero
[width
];
1159 else if (k
== kind::BITVECTOR_UREM
) {
1160 if (d_BVRemByZero
.find(width
) == d_BVRemByZero
.end()) {
1161 std::ostringstream os
;
1162 os
<< "BVURemByZero_" << width
;
1163 Node divByZero
= nm
->mkSkolem(os
.str(),
1164 nm
->mkFunctionType(nm
->mkBitVectorType(width
), nm
->mkBitVectorType(width
)),
1165 "partial bvurem", NodeManager::SKOLEM_EXACT_NAME
);
1166 d_BVRemByZero
[width
] = divByZero
;
1168 return d_BVRemByZero
[width
];
1175 Node
SmtEnginePrivate::expandBVDivByZero(TNode n
) {
1176 // we only deal wioth the unsigned division operators as the signed ones should have been
1177 // expanded in terms of the unsigned operators
1178 NodeManager
* nm
= d_smt
.d_nodeManager
;
1179 unsigned width
= n
.getType().getBitVectorSize();
1180 Node divByZero
= getBVDivByZero(n
.getKind(), width
);
1181 TNode num
= n
[0], den
= n
[1];
1182 Node den_eq_0
= nm
->mkNode(kind::EQUAL
, den
, nm
->mkConst(BitVector(width
, Integer(0))));
1183 Node divByZeroNum
= nm
->mkNode(kind::APPLY_UF
, divByZero
, num
);
1184 Node divTotalNumDen
= nm
->mkNode(n
.getKind() == kind::BITVECTOR_UDIV
? kind::BITVECTOR_UDIV_TOTAL
:
1185 kind::BITVECTOR_UREM_TOTAL
, num
, den
);
1186 Node node
= nm
->mkNode(kind::ITE
, den_eq_0
, divByZeroNum
, divTotalNumDen
);
1191 Node
SmtEnginePrivate::expandDefinitions(TNode n
, hash_map
<Node
, Node
, NodeHashFunction
>& cache
)
1192 throw(TypeCheckingException
, LogicException
) {
1194 Kind k
= n
.getKind();
1196 if(k
!= kind::APPLY
&& n
.getNumChildren() == 0) {
1197 // don't bother putting in the cache
1201 // maybe it's in the cache
1202 hash_map
<Node
, Node
, NodeHashFunction
>::iterator cacheHit
= cache
.find(n
);
1203 if(cacheHit
!= cache
.end()) {
1204 TNode ret
= (*cacheHit
).second
;
1205 return ret
.isNull() ? n
: ret
;
1208 // otherwise expand it
1211 NodeManager
* nm
= d_smt
.d_nodeManager
;
1212 // FIXME: this theory specific code should be factored out of the SmtEngine, somehow
1214 case kind::BITVECTOR_SDIV
:
1215 case kind::BITVECTOR_SREM
:
1216 case kind::BITVECTOR_SMOD
: {
1217 node
= bv::TheoryBVRewriter::eliminateBVSDiv(node
);
1221 case kind::BITVECTOR_UDIV
:
1222 case kind::BITVECTOR_UREM
: {
1223 node
= expandBVDivByZero(node
);
1226 case kind::DIVISION
: {
1227 // partial function: division
1228 if(d_smt
.d_logic
.isLinear()) {
1232 if(d_divByZero
.isNull()) {
1233 d_divByZero
= nm
->mkSkolem("divByZero", nm
->mkFunctionType(nm
->realType(), nm
->realType()),
1234 "partial real division", NodeManager::SKOLEM_EXACT_NAME
);
1236 TNode num
= n
[0], den
= n
[1];
1237 Node den_eq_0
= nm
->mkNode(kind::EQUAL
, den
, nm
->mkConst(Rational(0)));
1238 Node divByZeroNum
= nm
->mkNode(kind::APPLY_UF
, d_divByZero
, num
);
1239 Node divTotalNumDen
= nm
->mkNode(kind::DIVISION_TOTAL
, num
, den
);
1240 node
= nm
->mkNode(kind::ITE
, den_eq_0
, divByZeroNum
, divTotalNumDen
);
1244 case kind::INTS_DIVISION
: {
1245 // partial function: integer div
1246 if(d_smt
.d_logic
.isLinear()) {
1250 if(d_intDivByZero
.isNull()) {
1251 d_intDivByZero
= nm
->mkSkolem("intDivByZero", nm
->mkFunctionType(nm
->integerType(), nm
->integerType()),
1252 "partial integer division", NodeManager::SKOLEM_EXACT_NAME
);
1254 TNode num
= n
[0], den
= n
[1];
1255 Node den_eq_0
= nm
->mkNode(kind::EQUAL
, den
, nm
->mkConst(Rational(0)));
1256 Node intDivByZeroNum
= nm
->mkNode(kind::APPLY_UF
, d_intDivByZero
, num
);
1257 Node intDivTotalNumDen
= nm
->mkNode(kind::INTS_DIVISION_TOTAL
, num
, den
);
1258 node
= nm
->mkNode(kind::ITE
, den_eq_0
, intDivByZeroNum
, intDivTotalNumDen
);
1262 case kind::INTS_MODULUS
: {
1263 // partial function: mod
1264 if(d_smt
.d_logic
.isLinear()) {
1268 if(d_modZero
.isNull()) {
1269 d_modZero
= nm
->mkSkolem("modZero", nm
->mkFunctionType(nm
->integerType(), nm
->integerType()),
1270 "partial modulus", NodeManager::SKOLEM_EXACT_NAME
);
1272 TNode num
= n
[0], den
= n
[1];
1273 Node den_eq_0
= nm
->mkNode(kind::EQUAL
, den
, nm
->mkConst(Rational(0)));
1274 Node modZeroNum
= nm
->mkNode(kind::APPLY_UF
, d_modZero
, num
);
1275 Node modTotalNumDen
= nm
->mkNode(kind::INTS_MODULUS_TOTAL
, num
, den
);
1276 node
= nm
->mkNode(kind::ITE
, den_eq_0
, modZeroNum
, modTotalNumDen
);
1281 // application of a user-defined symbol
1282 TNode func
= n
.getOperator();
1283 SmtEngine::DefinedFunctionMap::const_iterator i
=
1284 d_smt
.d_definedFunctions
->find(func
);
1285 DefinedFunction def
= (*i
).second
;
1286 vector
<Node
> formals
= def
.getFormals();
1288 if(Debug
.isOn("expand")) {
1289 Debug("expand") << "found: " << n
<< endl
;
1290 Debug("expand") << " func: " << func
<< endl
;
1291 string name
= func
.getAttribute(expr::VarNameAttr());
1292 Debug("expand") << " : \"" << name
<< "\"" << endl
;
1294 if(i
== d_smt
.d_definedFunctions
->end()) {
1295 throw TypeCheckingException(n
.toExpr(), std::string("Undefined function: `") + func
.toString() + "'");
1297 if(Debug
.isOn("expand")) {
1298 Debug("expand") << " defn: " << def
.getFunction() << endl
1300 if(formals
.size() > 0) {
1301 copy( formals
.begin(), formals
.end() - 1,
1302 ostream_iterator
<Node
>(Debug("expand"), ", ") );
1303 Debug("expand") << formals
.back();
1305 Debug("expand") << "]" << endl
1306 << " " << def
.getFunction().getType() << endl
1307 << " " << def
.getFormula() << endl
;
1310 TNode fm
= def
.getFormula();
1311 Node instance
= fm
.substitute(formals
.begin(), formals
.end(),
1312 n
.begin(), n
.end());
1313 Debug("expand") << "made : " << instance
<< endl
;
1315 Node expanded
= expandDefinitions(instance
, cache
);
1316 cache
[n
] = (n
== expanded
? Node::null() : expanded
);
1321 // unknown kind for expansion, just iterate over the children
1325 // there should be children here, otherwise we short-circuited a return, above
1326 Assert(node
.getNumChildren() > 0);
1328 // the partial functions can fall through, in which case we still
1329 // consider their children
1330 Debug("expand") << "cons : " << node
<< endl
;
1331 NodeBuilder
<> nb(node
.getKind());
1332 if(node
.getMetaKind() == kind::metakind::PARAMETERIZED
) {
1333 Debug("expand") << "op : " << node
.getOperator() << endl
;
1334 nb
<< node
.getOperator();
1336 for(Node::iterator i
= node
.begin(),
1340 Node expanded
= expandDefinitions(*i
, cache
);
1341 Debug("expand") << "exchld: " << expanded
<< endl
;
1345 cache
[n
] = n
== node
? Node::null() : node
;
1349 // check if the given node contains a universal quantifier
1350 static bool containsQuantifiers(Node n
) {
1351 if(n
.getKind() == kind::FORALL
) {
1354 for(unsigned i
= 0; i
< n
.getNumChildren(); ++i
) {
1355 if(containsQuantifiers(n
[i
])) {
1363 Node
SmtEnginePrivate::preSkolemizeQuantifiers( Node n
, bool polarity
, std::vector
< Node
>& fvs
){
1364 Trace("pre-sk") << "Pre-skolem " << n
<< " " << polarity
<< " " << fvs
.size() << std::endl
;
1365 if( n
.getKind()==kind::NOT
){
1366 Node nn
= preSkolemizeQuantifiers( n
[0], !polarity
, fvs
);
1368 }else if( n
.getKind()==kind::FORALL
){
1370 std::vector
< Node
> children
;
1371 children
.push_back( n
[0] );
1372 //add children to current scope
1373 std::vector
< Node
> fvss
;
1374 fvss
.insert( fvss
.begin(), fvs
.begin(), fvs
.end() );
1375 for( int i
=0; i
<(int)n
[0].getNumChildren(); i
++ ){
1376 fvss
.push_back( n
[0][i
] );
1379 children
.push_back( preSkolemizeQuantifiers( n
[1], polarity
, fvss
) );
1380 if( n
.getNumChildren()==3 ){
1381 children
.push_back( n
[2] );
1383 //return processed quantifier
1384 return NodeManager::currentNM()->mkNode( kind::FORALL
, children
);
1387 Node nn
= preSkolemizeQuantifiers( n
[1], polarity
, fvs
);
1388 //now, substitute skolems for the variables
1389 std::vector
< TypeNode
> argTypes
;
1390 for( int i
=0; i
<(int)fvs
.size(); i
++ ){
1391 argTypes
.push_back( fvs
[i
].getType() );
1393 //calculate the variables and substitution
1394 std::vector
< Node
> vars
;
1395 std::vector
< Node
> subs
;
1396 for( int i
=0; i
<(int)n
[0].getNumChildren(); i
++ ){
1397 vars
.push_back( n
[0][i
] );
1399 for( int i
=0; i
<(int)n
[0].getNumChildren(); i
++ ){
1400 //make the new function symbol
1401 if( argTypes
.empty() ){
1402 Node s
= NodeManager::currentNM()->mkSkolem( "sk_$$", n
[0][i
].getType(), "created during pre-skolemization" );
1403 subs
.push_back( s
);
1405 TypeNode typ
= NodeManager::currentNM()->mkFunctionType( argTypes
, n
[0][i
].getType() );
1406 Node op
= NodeManager::currentNM()->mkSkolem( "skop_$$", typ
, "op created during pre-skolemization" );
1407 //DOTHIS: set attribute on op, marking that it should not be selected as trigger
1408 std::vector
< Node
> funcArgs
;
1409 funcArgs
.push_back( op
);
1410 funcArgs
.insert( funcArgs
.end(), fvs
.begin(), fvs
.end() );
1411 subs
.push_back( NodeManager::currentNM()->mkNode( kind::APPLY_UF
, funcArgs
) );
1414 //apply substitution
1415 nn
= nn
.substitute( vars
.begin(), vars
.end(), subs
.begin(), subs
.end() );
1419 //check if it contains a quantifier as a subterm
1420 bool containsQuant
= false;
1421 if( n
.getType().isBoolean() ){
1422 for( int i
=0; i
<(int)n
.getNumChildren(); i
++ ){
1423 if( containsQuantifiers( n
[i
] ) ){
1424 containsQuant
= true;
1429 //if so, we will write this node
1430 if( containsQuant
){
1431 if( n
.getKind()==kind::ITE
|| n
.getKind()==kind::IFF
|| n
.getKind()==kind::XOR
|| n
.getKind()==kind::IMPLIES
){
1433 //must remove structure
1434 if( n
.getKind()==kind::ITE
){
1435 nn
= NodeManager::currentNM()->mkNode( kind::AND
,
1436 NodeManager::currentNM()->mkNode( kind::OR
, n
[0].notNode(), n
[1] ),
1437 NodeManager::currentNM()->mkNode( kind::OR
, n
[0], n
[2] ) );
1438 }else if( n
.getKind()==kind::IFF
|| n
.getKind()==kind::XOR
){
1439 nn
= NodeManager::currentNM()->mkNode( kind::AND
,
1440 NodeManager::currentNM()->mkNode( kind::OR
, n
[0].notNode(), n
.getKind()==kind::XOR
? n
[1].notNode() : n
[1] ),
1441 NodeManager::currentNM()->mkNode( kind::OR
, n
[0], n
.getKind()==kind::XOR
? n
[1] : n
[1].notNode() ) );
1442 }else if( n
.getKind()==kind::IMPLIES
){
1443 nn
= NodeManager::currentNM()->mkNode( kind::OR
, n
[0].notNode(), n
[1] );
1445 return preSkolemizeQuantifiers( nn
, polarity
, fvs
);
1447 Assert( n
.getKind() == kind::AND
|| n
.getKind() == kind::OR
);
1448 std::vector
< Node
> children
;
1449 for( int i
=0; i
<(int)n
.getNumChildren(); i
++ ){
1450 children
.push_back( preSkolemizeQuantifiers( n
[i
], polarity
, fvs
) );
1452 return NodeManager::currentNM()->mkNode( n
.getKind(), children
);
1460 void SmtEnginePrivate::removeITEs() {
1461 d_smt
.finalOptionsAreSet();
1463 Trace("simplify") << "SmtEnginePrivate::removeITEs()" << endl
;
1465 // Remove all of the ITE occurrences and normalize
1466 d_iteRemover
.run(d_assertionsToCheck
, d_iteSkolemMap
);
1467 for (unsigned i
= 0; i
< d_assertionsToCheck
.size(); ++ i
) {
1468 d_assertionsToCheck
[i
] = Rewriter::rewrite(d_assertionsToCheck
[i
]);
1473 void SmtEnginePrivate::staticLearning() {
1474 d_smt
.finalOptionsAreSet();
1476 TimerStat::CodeTimer
staticLearningTimer(d_smt
.d_stats
->d_staticLearningTime
);
1478 Trace("simplify") << "SmtEnginePrivate::staticLearning()" << endl
;
1480 for (unsigned i
= 0; i
< d_assertionsToCheck
.size(); ++ i
) {
1482 NodeBuilder
<> learned(kind::AND
);
1483 learned
<< d_assertionsToCheck
[i
];
1484 d_smt
.d_theoryEngine
->ppStaticLearn(d_assertionsToCheck
[i
], learned
);
1485 if(learned
.getNumChildren() == 1) {
1488 d_assertionsToCheck
[i
] = learned
;
1493 // do dumping (before/after any preprocessing pass)
1494 static void dumpAssertions(const char* key
,
1495 const std::vector
<Node
>& assertionList
) {
1496 if( Dump
.isOn("assertions") &&
1497 Dump
.isOn(std::string("assertions:") + key
) ) {
1498 // Push the simplified assertions to the dump output stream
1499 for(unsigned i
= 0; i
< assertionList
.size(); ++ i
) {
1500 TNode n
= assertionList
[i
];
1501 Dump("assertions") << AssertCommand(Expr(n
.toExpr()));
1506 // returns false if it learns a conflict
1507 bool SmtEnginePrivate::nonClausalSimplify() {
1508 d_smt
.finalOptionsAreSet();
1510 TimerStat::CodeTimer
nonclausalTimer(d_smt
.d_stats
->d_nonclausalSimplificationTime
);
1512 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify()" << endl
;
1514 d_propagator
.initialize();
1516 // Assert all the assertions to the propagator
1517 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
1518 << "asserting to propagator" << endl
;
1519 for (unsigned i
= 0; i
< d_assertionsToPreprocess
.size(); ++ i
) {
1520 Assert(Rewriter::rewrite(d_assertionsToPreprocess
[i
]) == d_assertionsToPreprocess
[i
]);
1521 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): asserting " << d_assertionsToPreprocess
[i
] << endl
;
1522 d_propagator
.assertTrue(d_assertionsToPreprocess
[i
]);
1525 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
1526 << "propagating" << endl
;
1527 if (d_propagator
.propagate()) {
1528 // If in conflict, just return false
1529 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
1530 << "conflict in non-clausal propagation" << endl
;
1531 d_assertionsToPreprocess
.clear();
1532 d_assertionsToCheck
.push_back(NodeManager::currentNM()->mkConst
<bool>(false));
1533 d_propagator
.finish();
1537 // No, conflict, go through the literals and solve them
1538 SubstitutionMap
constantPropagations(d_smt
.d_context
);
1540 for(unsigned i
= 0, i_end
= d_nonClausalLearnedLiterals
.size(); i
< i_end
; ++ i
) {
1541 // Simplify the literal we learned wrt previous substitutions
1542 Node learnedLiteral
= d_nonClausalLearnedLiterals
[i
];
1543 Assert(Rewriter::rewrite(learnedLiteral
) == learnedLiteral
);
1544 Node learnedLiteralNew
= d_topLevelSubstitutions
.apply(learnedLiteral
);
1545 if (learnedLiteral
!= learnedLiteralNew
) {
1546 learnedLiteral
= Rewriter::rewrite(learnedLiteralNew
);
1549 learnedLiteralNew
= constantPropagations
.apply(learnedLiteral
);
1550 if (learnedLiteralNew
== learnedLiteral
) {
1553 ++d_smt
.d_stats
->d_numConstantProps
;
1554 learnedLiteral
= Rewriter::rewrite(learnedLiteralNew
);
1556 // It might just simplify to a constant
1557 if (learnedLiteral
.isConst()) {
1558 if (learnedLiteral
.getConst
<bool>()) {
1559 // If the learned literal simplifies to true, it's redundant
1562 // If the learned literal simplifies to false, we're in conflict
1563 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
1565 << d_nonClausalLearnedLiterals
[i
] << endl
;
1566 d_assertionsToPreprocess
.clear();
1567 d_assertionsToCheck
.push_back(NodeManager::currentNM()->mkConst
<bool>(false));
1568 d_propagator
.finish();
1572 // Solve it with the corresponding theory
1573 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
1574 << "solving " << learnedLiteral
<< endl
;
1575 Theory::PPAssertStatus solveStatus
=
1576 d_smt
.d_theoryEngine
->solve(learnedLiteral
, d_topLevelSubstitutions
);
1578 switch (solveStatus
) {
1579 case Theory::PP_ASSERT_STATUS_SOLVED
: {
1580 // The literal should rewrite to true
1581 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
1582 << "solved " << learnedLiteral
<< endl
;
1583 Assert(Rewriter::rewrite(d_topLevelSubstitutions
.apply(learnedLiteral
)).isConst());
1584 // vector<pair<Node, Node> > equations;
1585 // constantPropagations.simplifyLHS(d_topLevelSubstitutions, equations, true);
1586 // if (equations.empty()) {
1589 // Assert(equations[0].first.isConst() && equations[0].second.isConst() && equations[0].first != equations[0].second);
1590 // else fall through
1593 case Theory::PP_ASSERT_STATUS_CONFLICT
:
1594 // If in conflict, we return false
1595 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
1596 << "conflict while solving "
1597 << learnedLiteral
<< endl
;
1598 d_assertionsToPreprocess
.clear();
1599 d_assertionsToCheck
.push_back(NodeManager::currentNM()->mkConst
<bool>(false));
1600 d_propagator
.finish();
1603 if (d_doConstantProp
&& learnedLiteral
.getKind() == kind::EQUAL
&& (learnedLiteral
[0].isConst() || learnedLiteral
[1].isConst())) {
1604 // constant propagation
1607 if (learnedLiteral
[0].isConst()) {
1608 t
= learnedLiteral
[1];
1609 c
= learnedLiteral
[0];
1612 t
= learnedLiteral
[0];
1613 c
= learnedLiteral
[1];
1615 Assert(!t
.isConst());
1616 Assert(constantPropagations
.apply(t
) == t
);
1617 Assert(d_topLevelSubstitutions
.apply(t
) == t
);
1618 constantPropagations
.addSubstitution(t
, c
);
1619 // vector<pair<Node,Node> > equations;a
1620 // constantPropagations.simplifyLHS(t, c, equations, true);
1621 // if (!equations.empty()) {
1622 // Assert(equations[0].first.isConst() && equations[0].second.isConst() && equations[0].first != equations[0].second);
1623 // d_assertionsToPreprocess.clear();
1624 // d_assertionsToCheck.push_back(NodeManager::currentNM()->mkConst<bool>(false));
1627 // d_topLevelSubstitutions.simplifyRHS(constantPropagations);
1631 d_nonClausalLearnedLiterals
[j
++] = d_nonClausalLearnedLiterals
[i
];
1636 #ifdef CVC4_ASSERTIONS
1637 // Check data structure invariants:
1638 // 1. for each lhs of d_topLevelSubstitutions, does not appear anywhere in rhs of d_topLevelSubstitutions or anywhere in constantPropagations
1639 // 2. each lhs of constantPropagations rewrites to itself
1640 // 3. if l -> r is a constant propagation and l is a subterm of l' with l' -> r' another constant propagation, then l'[l/r] -> r' should be a
1641 // constant propagation too
1642 // 4. each lhs of constantPropagations is different from each rhs
1643 SubstitutionMap::iterator pos
= d_topLevelSubstitutions
.begin();
1644 for (; pos
!= d_topLevelSubstitutions
.end(); ++pos
) {
1645 Assert((*pos
).first
.isVar());
1646 // Assert(d_topLevelSubstitutions.apply((*pos).second) == (*pos).second);
1648 for (pos
= constantPropagations
.begin(); pos
!= constantPropagations
.end(); ++pos
) {
1649 Assert((*pos
).second
.isConst());
1650 Assert(Rewriter::rewrite((*pos
).first
) == (*pos
).first
);
1651 // Node newLeft = d_topLevelSubstitutions.apply((*pos).first);
1652 // if (newLeft != (*pos).first) {
1653 // newLeft = Rewriter::rewrite(newLeft);
1654 // Assert(newLeft == (*pos).second ||
1655 // (constantPropagations.hasSubstitution(newLeft) && constantPropagations.apply(newLeft) == (*pos).second));
1657 // newLeft = constantPropagations.apply((*pos).first);
1658 // if (newLeft != (*pos).first) {
1659 // newLeft = Rewriter::rewrite(newLeft);
1660 // Assert(newLeft == (*pos).second ||
1661 // (constantPropagations.hasSubstitution(newLeft) && constantPropagations.apply(newLeft) == (*pos).second));
1663 Assert(constantPropagations
.apply((*pos
).second
) == (*pos
).second
);
1667 // Resize the learnt
1668 d_nonClausalLearnedLiterals
.resize(j
);
1670 hash_set
<TNode
, TNodeHashFunction
> s
;
1671 for (unsigned i
= 0; i
< d_assertionsToPreprocess
.size(); ++ i
) {
1672 Node assertion
= d_assertionsToPreprocess
[i
];
1673 Node assertionNew
= d_topLevelSubstitutions
.apply(assertion
);
1674 if (assertion
!= assertionNew
) {
1675 assertion
= Rewriter::rewrite(assertionNew
);
1677 Assert(Rewriter::rewrite(assertion
) == assertion
);
1679 assertionNew
= constantPropagations
.apply(assertion
);
1680 if (assertionNew
== assertion
) {
1683 ++d_smt
.d_stats
->d_numConstantProps
;
1684 assertion
= Rewriter::rewrite(assertionNew
);
1686 s
.insert(assertion
);
1687 d_assertionsToCheck
.push_back(assertion
);
1688 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
1689 << "non-clausal preprocessed: "
1690 << assertion
<< endl
;
1692 d_assertionsToPreprocess
.clear();
1694 NodeBuilder
<> learnedBuilder(kind::AND
);
1695 Assert(d_realAssertionsEnd
<= d_assertionsToCheck
.size());
1696 learnedBuilder
<< d_assertionsToCheck
[d_realAssertionsEnd
- 1];
1698 if( options::incrementalSolving() ||
1699 options::simplificationMode() == SIMPLIFICATION_MODE_INCREMENTAL
) {
1700 // Keep substitutions
1701 SubstitutionMap::iterator pos
= d_lastSubstitutionPos
;
1702 if(pos
== d_topLevelSubstitutions
.end()) {
1703 pos
= d_topLevelSubstitutions
.begin();
1708 while(pos
!= d_topLevelSubstitutions
.end()) {
1709 // Push out this substitution
1710 TNode lhs
= (*pos
).first
, rhs
= (*pos
).second
;
1711 Node n
= NodeManager::currentNM()->mkNode(lhs
.getType().isBoolean() ? kind::IFF
: kind::EQUAL
, lhs
, rhs
);
1712 learnedBuilder
<< n
;
1713 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): will notify SAT layer of substitution: " << n
<< endl
;
1714 d_lastSubstitutionPos
= pos
;
1719 for (unsigned i
= 0; i
< d_nonClausalLearnedLiterals
.size(); ++ i
) {
1720 Node learned
= d_nonClausalLearnedLiterals
[i
];
1721 Node learnedNew
= d_topLevelSubstitutions
.apply(learned
);
1722 if (learned
!= learnedNew
) {
1723 learned
= Rewriter::rewrite(learnedNew
);
1725 Assert(Rewriter::rewrite(learned
) == learned
);
1727 learnedNew
= constantPropagations
.apply(learned
);
1728 if (learnedNew
== learned
) {
1731 ++d_smt
.d_stats
->d_numConstantProps
;
1732 learned
= Rewriter::rewrite(learnedNew
);
1734 if (s
.find(learned
) != s
.end()) {
1738 learnedBuilder
<< learned
;
1739 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
1740 << "non-clausal learned : "
1743 d_nonClausalLearnedLiterals
.clear();
1745 SubstitutionMap::iterator pos
= constantPropagations
.begin();
1746 for (; pos
!= constantPropagations
.end(); ++pos
) {
1747 Node cProp
= (*pos
).first
.eqNode((*pos
).second
);
1748 Node cPropNew
= d_topLevelSubstitutions
.apply(cProp
);
1749 if (cProp
!= cPropNew
) {
1750 cProp
= Rewriter::rewrite(cPropNew
);
1751 Assert(Rewriter::rewrite(cProp
) == cProp
);
1753 if (s
.find(cProp
) != s
.end()) {
1757 learnedBuilder
<< cProp
;
1758 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
1759 << "non-clausal constant propagation : "
1763 if(learnedBuilder
.getNumChildren() > 1) {
1764 d_assertionsToCheck
[d_realAssertionsEnd
- 1] =
1765 Rewriter::rewrite(Node(learnedBuilder
));
1768 d_propagator
.finish();
1773 void SmtEnginePrivate::simpITE() {
1774 TimerStat::CodeTimer
simpITETimer(d_smt
.d_stats
->d_simpITETime
);
1776 Trace("simplify") << "SmtEnginePrivate::simpITE()" << endl
;
1778 for (unsigned i
= 0; i
< d_assertionsToCheck
.size(); ++ i
) {
1780 d_assertionsToCheck
[i
] = d_smt
.d_theoryEngine
->ppSimpITE(d_assertionsToCheck
[i
]);
1785 void SmtEnginePrivate::unconstrainedSimp() {
1786 TimerStat::CodeTimer
unconstrainedSimpTimer(d_smt
.d_stats
->d_unconstrainedSimpTime
);
1788 Trace("simplify") << "SmtEnginePrivate::unconstrainedSimp()" << endl
;
1789 d_smt
.d_theoryEngine
->ppUnconstrainedSimp(d_assertionsToCheck
);
1793 void SmtEnginePrivate::constrainSubtypes(TNode top
, std::vector
<Node
>& assertions
)
1796 Trace("constrainSubtypes") << "constrainSubtypes(): looking at " << top
<< endl
;
1799 stack
<TNode
> worklist
;
1804 TNode n
= worklist
.top();
1807 TypeNode t
= n
.getType();
1808 if(t
.isPredicateSubtype()) {
1809 WarningOnce() << "Warning: CVC4 doesn't yet do checking that predicate subtypes are nonempty domains" << endl
;
1810 Node pred
= t
.getSubtypePredicate();
1812 // pred can be a LAMBDA, a function constant, or a datatype tester
1813 Trace("constrainSubtypes") << "constrainSubtypes(): pred.getType() == " << pred
.getType() << endl
;
1814 if(d_smt
.d_definedFunctions
->find(pred
) != d_smt
.d_definedFunctions
->end()) {
1816 } else if(pred
.getType().isTester()) {
1817 k
= kind::APPLY_TESTER
;
1821 Node app
= NodeManager::currentNM()->mkNode(k
, pred
, n
);
1822 Trace("constrainSubtypes") << "constrainSubtypes(): assert(" << k
<< ") " << app
<< endl
;
1823 assertions
.push_back(app
);
1824 } else if(t
.isSubrange()) {
1825 SubrangeBounds bounds
= t
.getSubrangeBounds();
1826 Trace("constrainSubtypes") << "constrainSubtypes(): got bounds " << bounds
<< endl
;
1827 if(bounds
.lower
.hasBound()) {
1828 Node c
= NodeManager::currentNM()->mkConst(Rational(bounds
.lower
.getBound()));
1829 Node lb
= NodeManager::currentNM()->mkNode(kind::LEQ
, c
, n
);
1830 Trace("constrainSubtypes") << "constrainSubtypes(): assert " << lb
<< endl
;
1831 assertions
.push_back(lb
);
1833 if(bounds
.upper
.hasBound()) {
1834 Node c
= NodeManager::currentNM()->mkConst(Rational(bounds
.upper
.getBound()));
1835 Node ub
= NodeManager::currentNM()->mkNode(kind::LEQ
, n
, c
);
1836 Trace("constrainSubtypes") << "constrainSubtypes(): assert " << ub
<< endl
;
1837 assertions
.push_back(ub
);
1841 for(TNode::iterator i
= n
.begin(); i
!= n
.end(); ++i
) {
1842 if(done
.find(*i
) == done
.end()) {
1847 } while(! worklist
.empty());
1850 // returns false if simplification led to "false"
1851 bool SmtEnginePrivate::simplifyAssertions()
1852 throw(TypeCheckingException
, LogicException
) {
1853 Assert(d_smt
.d_pendingPops
== 0);
1856 Trace("simplify") << "SmtEnginePrivate::simplify()" << endl
;
1858 if(options::simplificationMode() != SIMPLIFICATION_MODE_NONE
) {
1859 // Perform non-clausal simplification
1860 Trace("simplify") << "SmtEnginePrivate::simplify(): "
1861 << "performing non-clausal simplification" << endl
;
1862 bool noConflict
= nonClausalSimplify();
1863 if(!noConflict
) return false;
1865 Assert(d_assertionsToCheck
.empty());
1866 d_assertionsToCheck
.swap(d_assertionsToPreprocess
);
1869 Trace("smt") << "POST nonClasualSimplify" << std::endl
;
1870 Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess
.size() << endl
;
1871 Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck
.size() << endl
;
1873 // Theory preprocessing
1874 if (d_smt
.d_earlyTheoryPP
) {
1875 TimerStat::CodeTimer
codeTimer(d_smt
.d_stats
->d_theoryPreprocessTime
);
1876 // Call the theory preprocessors
1877 d_smt
.d_theoryEngine
->preprocessStart();
1878 for (unsigned i
= 0; i
< d_assertionsToCheck
.size(); ++ i
) {
1879 Assert(Rewriter::rewrite(d_assertionsToCheck
[i
]) == d_assertionsToCheck
[i
]);
1880 d_assertionsToCheck
[i
] = d_smt
.d_theoryEngine
->preprocess(d_assertionsToCheck
[i
]);
1881 Assert(Rewriter::rewrite(d_assertionsToCheck
[i
]) == d_assertionsToCheck
[i
]);
1885 Trace("smt") << "POST theoryPP" << std::endl
;
1886 Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess
.size() << endl
;
1887 Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck
.size() << endl
;
1889 // ITE simplification
1890 if(options::doITESimp()) {
1894 Trace("smt") << "POST iteSimp" << std::endl
;
1895 Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess
.size() << endl
;
1896 Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck
.size() << endl
;
1898 // Unconstrained simplification
1899 if(options::unconstrainedSimp()) {
1900 unconstrainedSimp();
1903 Trace("smt") << "POST unconstrainedSimp" << std::endl
;
1904 Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess
.size() << endl
;
1905 Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck
.size() << endl
;
1907 if(options::repeatSimp() && options::simplificationMode() != SIMPLIFICATION_MODE_NONE
) {
1908 Trace("simplify") << "SmtEnginePrivate::simplify(): "
1909 << " doing repeated simplification" << std::endl
;
1910 d_assertionsToCheck
.swap(d_assertionsToPreprocess
);
1911 Assert(d_assertionsToCheck
.empty());
1912 bool noConflict
= nonClausalSimplify();
1918 Trace("smt") << "POST repeatSimp" << std::endl
;
1919 Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess
.size() << endl
;
1920 Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck
.size() << endl
;
1922 } catch(TypeCheckingExceptionPrivate
& tcep
) {
1923 // Calls to this function should have already weeded out any
1924 // typechecking exceptions via (e.g.) ensureBoolean(). But a
1925 // theory could still create a new expression that isn't
1926 // well-typed, and we don't want the C++ runtime to abort our
1927 // process without any error notice.
1929 ss
<< "A bad expression was produced. Original exception follows:\n"
1931 InternalError(ss
.str().c_str());
1936 Result
SmtEngine::check() {
1937 Assert(d_fullyInited
);
1938 Assert(d_pendingPops
== 0);
1940 Trace("smt") << "SmtEngine::check()" << endl
;
1942 // Make sure the prop layer has all of the assertions
1943 Trace("smt") << "SmtEngine::check(): processing assertions" << endl
;
1944 d_private
->processAssertions();
1946 unsigned long millis
= 0;
1947 if(d_timeBudgetCumulative
!= 0) {
1948 millis
= getTimeRemaining();
1950 return Result(Result::VALIDITY_UNKNOWN
, Result::TIMEOUT
);
1953 if(d_timeBudgetPerCall
!= 0 && (millis
== 0 || d_timeBudgetPerCall
< millis
)) {
1954 millis
= d_timeBudgetPerCall
;
1957 unsigned long resource
= 0;
1958 if(d_resourceBudgetCumulative
!= 0) {
1959 resource
= getResourceRemaining();
1961 return Result(Result::VALIDITY_UNKNOWN
, Result::RESOURCEOUT
);
1964 if(d_resourceBudgetPerCall
!= 0 && (resource
== 0 || d_resourceBudgetPerCall
< resource
)) {
1965 resource
= d_resourceBudgetPerCall
;
1968 Trace("smt") << "SmtEngine::check(): running check" << endl
;
1969 Result result
= d_propEngine
->checkSat(millis
, resource
);
1971 // PropEngine::checkSat() returns the actual amount used in these
1973 d_cumulativeTimeUsed
+= millis
;
1974 d_cumulativeResourceUsed
+= resource
;
1976 Trace("limit") << "SmtEngine::check(): cumulative millis " << d_cumulativeTimeUsed
1977 << ", conflicts " << d_cumulativeResourceUsed
<< endl
;
1982 Result
SmtEngine::quickCheck() {
1983 Assert(d_fullyInited
);
1984 Trace("smt") << "SMT quickCheck()" << endl
;
1985 return Result(Result::VALIDITY_UNKNOWN
, Result::REQUIRES_FULL_CHECK
);
1989 bool SmtEnginePrivate::checkForBadSkolems(TNode n
, TNode skolem
, hash_map
<Node
, bool, NodeHashFunction
>& cache
)
1991 hash_map
<Node
, bool, NodeHashFunction
>::iterator it
;
1993 if (it
!= cache
.end()) {
1994 return (*it
).second
;
1997 size_t sz
= n
.getNumChildren();
1999 IteSkolemMap::iterator it
= d_iteSkolemMap
.find(n
);
2001 if (it
!= d_iteSkolemMap
.end()) {
2002 if (!((*it
).first
< n
)) {
2011 for (; k
< sz
; ++k
) {
2012 if (checkForBadSkolems(n
[k
], skolem
, cache
)) {
2023 void SmtEnginePrivate::processAssertions() {
2024 Assert(d_smt
.d_fullyInited
);
2025 Assert(d_smt
.d_pendingPops
== 0);
2027 // Dump the assertions
2028 dumpAssertions("pre-everything", d_assertionsToPreprocess
);
2030 Trace("smt") << "SmtEnginePrivate::processAssertions()" << endl
;
2032 Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess
.size() << endl
;
2033 Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck
.size() << endl
;
2035 Assert(d_assertionsToCheck
.size() == 0);
2037 // any assertions added beyond realAssertionsEnd must NOT affect the
2038 // equisatisfiability
2039 d_realAssertionsEnd
= d_assertionsToPreprocess
.size();
2040 if(d_realAssertionsEnd
== 0) {
2045 // Assertions are NOT guaranteed to be rewritten by this point
2047 dumpAssertions("pre-definition-expansion", d_assertionsToPreprocess
);
2049 Chat() << "expanding definitions..." << endl
;
2050 Trace("simplify") << "SmtEnginePrivate::simplify(): expanding definitions" << endl
;
2051 TimerStat::CodeTimer
codeTimer(d_smt
.d_stats
->d_definitionExpansionTime
);
2052 hash_map
<Node
, Node
, NodeHashFunction
> cache
;
2053 for (unsigned i
= 0; i
< d_assertionsToPreprocess
.size(); ++ i
) {
2054 d_assertionsToPreprocess
[i
] =
2055 expandDefinitions(d_assertionsToPreprocess
[i
], cache
);
2058 dumpAssertions("post-definition-expansion", d_assertionsToPreprocess
);
2060 Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess
.size() << endl
;
2061 Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck
.size() << endl
;
2063 dumpAssertions("pre-constrain-subtypes", d_assertionsToPreprocess
);
2065 // Any variables of subtype types need to be constrained properly.
2066 // Careful, here: constrainSubtypes() adds to the back of
2067 // d_assertionsToPreprocess, but we don't need to reprocess those.
2068 // We also can't use an iterator, because the vector may be moved in
2069 // memory during this loop.
2070 Chat() << "constraining subtypes..." << endl
;
2071 for(unsigned i
= 0, i_end
= d_assertionsToPreprocess
.size(); i
!= i_end
; ++i
) {
2072 constrainSubtypes(d_assertionsToPreprocess
[i
], d_assertionsToPreprocess
);
2075 dumpAssertions("post-constrain-subtypes", d_assertionsToPreprocess
);
2077 Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess
.size() << endl
;
2078 Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck
.size() << endl
;
2080 dumpAssertions("pre-substitution", d_assertionsToPreprocess
);
2081 // Apply the substitutions we already have, and normalize
2082 Chat() << "applying substitutions..." << endl
;
2083 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
2084 << "applying substitutions" << endl
;
2085 for (unsigned i
= 0; i
< d_assertionsToPreprocess
.size(); ++ i
) {
2086 Trace("simplify") << "applying to " << d_assertionsToPreprocess
[i
] << endl
;
2087 d_assertionsToPreprocess
[i
] =
2088 Rewriter::rewrite(d_topLevelSubstitutions
.apply(d_assertionsToPreprocess
[i
]));
2089 Trace("simplify") << " got " << d_assertionsToPreprocess
[i
] << endl
;
2091 dumpAssertions("post-substitution", d_assertionsToPreprocess
);
2093 // Assertions ARE guaranteed to be rewritten by this point
2095 dumpAssertions("pre-skolem-quant", d_assertionsToPreprocess
);
2096 if( options::preSkolemQuant() ){
2097 //apply pre-skolemization to existential quantifiers
2098 for (unsigned i
= 0; i
< d_assertionsToPreprocess
.size(); ++ i
) {
2099 Node prev
= d_assertionsToPreprocess
[i
];
2100 std::vector
< Node
> fvs
;
2101 d_assertionsToPreprocess
[i
] = Rewriter::rewrite( preSkolemizeQuantifiers( d_assertionsToPreprocess
[i
], true, fvs
) );
2102 if( prev
!=d_assertionsToPreprocess
[i
] ){
2103 Trace("quantifiers-rewrite") << "*** Pre-skolemize " << prev
<< std::endl
;
2104 Trace("quantifiers-rewrite") << " ...got " << d_assertionsToPreprocess
[i
] << std::endl
;
2108 dumpAssertions("post-skolem-quant", d_assertionsToPreprocess
);
2110 if( options::macrosQuant() ){
2111 //quantifiers macro expansion
2112 QuantifierMacros qm
;
2113 qm
.simplify( d_assertionsToPreprocess
);
2116 if( options::sortInference() ){
2117 //sort inference technique
2119 si
.simplify( d_assertionsToPreprocess
);
2122 dumpAssertions("pre-simplify", d_assertionsToPreprocess
);
2123 Chat() << "simplifying assertions..." << endl
;
2124 bool noConflict
= simplifyAssertions();
2125 dumpAssertions("post-simplify", d_assertionsToPreprocess
);
2127 dumpAssertions("pre-static-learning", d_assertionsToCheck
);
2128 if(options::doStaticLearning()) {
2129 // Perform static learning
2130 Chat() << "doing static learning..." << endl
;
2131 Trace("simplify") << "SmtEnginePrivate::simplify(): "
2132 << "performing static learning" << endl
;
2135 dumpAssertions("post-static-learning", d_assertionsToCheck
);
2137 dumpAssertions("pre-ite-removal", d_assertionsToCheck
);
2139 Chat() << "removing term ITEs..." << endl
;
2140 TimerStat::CodeTimer
codeTimer(d_smt
.d_stats
->d_iteRemovalTime
);
2141 // Remove ITEs, updating d_iteSkolemMap
2142 d_smt
.d_stats
->d_numAssertionsPre
+= d_assertionsToCheck
.size();
2144 d_smt
.d_stats
->d_numAssertionsPost
+= d_assertionsToCheck
.size();
2146 dumpAssertions("post-ite-removal", d_assertionsToCheck
);
2148 dumpAssertions("pre-repeat-simplify", d_assertionsToCheck
);
2149 if(options::repeatSimp()) {
2150 d_assertionsToCheck
.swap(d_assertionsToPreprocess
);
2151 Chat() << "simplifying assertions..." << endl
;
2152 noConflict
&= simplifyAssertions();
2154 // Need to fix up assertion list to maintain invariants:
2155 // Let Sk be the set of Skolem variables introduced by ITE's. Let <_sk be the order in which these variables were introduced
2156 // during ite removal.
2157 // For each skolem variable sk, let iteExpr = iteMap(sk) be the ite expr mapped to by sk. We need to ensure:
2158 // 1. iteExpr has the form (ite cond (sk = t) (sk = e))
2159 // 2. if some sk' in Sk appears in cond, t, or e, then sk' <_sk sk
2160 // If either of these is violated, we must add iteExpr as a proper assertion
2161 IteSkolemMap::iterator it
= d_iteSkolemMap
.begin();
2162 IteSkolemMap::iterator iend
= d_iteSkolemMap
.end();
2163 NodeBuilder
<> builder(kind::AND
);
2164 builder
<< d_assertionsToCheck
[d_realAssertionsEnd
- 1];
2165 vector
<TNode
> toErase
;
2166 for (; it
!= iend
; ++it
) {
2167 TNode iteExpr
= d_assertionsToCheck
[(*it
).second
];
2168 if (iteExpr
.getKind() == kind::ITE
&&
2169 iteExpr
[1].getKind() == kind::EQUAL
&&
2170 iteExpr
[1][0] == (*it
).first
&&
2171 iteExpr
[2].getKind() == kind::EQUAL
&&
2172 iteExpr
[2][0] == (*it
).first
) {
2173 hash_map
<Node
, bool, NodeHashFunction
> cache
;
2174 bool bad
= checkForBadSkolems(iteExpr
[0], (*it
).first
, cache
);
2175 bad
= bad
|| checkForBadSkolems(iteExpr
[1][1], (*it
).first
, cache
);
2176 bad
= bad
|| checkForBadSkolems(iteExpr
[2][1], (*it
).first
, cache
);
2181 // Move this iteExpr into the main assertions
2182 builder
<< d_assertionsToCheck
[(*it
).second
];
2183 d_assertionsToCheck
[(*it
).second
] = NodeManager::currentNM()->mkConst
<bool>(true);
2184 toErase
.push_back((*it
).first
);
2186 if(builder
.getNumChildren() > 1) {
2187 while (!toErase
.empty()) {
2188 d_iteSkolemMap
.erase(toErase
.back());
2191 d_assertionsToCheck
[d_realAssertionsEnd
- 1] =
2192 Rewriter::rewrite(Node(builder
));
2194 // For some reason this is needed for some benchmarks, such as
2195 // http://church.cims.nyu.edu/benchmarks/smtlib2/QF_AUFBV/dwp_formulas/try5_small_difret_functions_dwp_tac.re_node_set_remove_at.il.dwp.smt2
2196 // Figure it out later
2198 // Assert(iteRewriteAssertionsEnd == d_assertionsToCheck.size());
2201 dumpAssertions("post-repeat-simplify", d_assertionsToCheck
);
2203 // begin: INVARIANT to maintain: no reordering of assertions or
2204 // introducing new ones
2205 #ifdef CVC4_ASSERTIONS
2206 unsigned iteRewriteAssertionsEnd
= d_assertionsToCheck
.size();
2209 Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess
.size() << endl
;
2210 Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck
.size() << endl
;
2212 Debug("smt") << "SmtEnginePrivate::processAssertions() POST SIMPLIFICATION" << endl
;
2213 Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess
.size() << endl
;
2214 Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck
.size() << endl
;
2216 dumpAssertions("pre-theory-preprocessing", d_assertionsToCheck
);
2218 Chat() << "theory preprocessing..." << endl
;
2219 TimerStat::CodeTimer
codeTimer(d_smt
.d_stats
->d_theoryPreprocessTime
);
2220 // Call the theory preprocessors
2221 d_smt
.d_theoryEngine
->preprocessStart();
2222 for (unsigned i
= 0; i
< d_assertionsToCheck
.size(); ++ i
) {
2223 d_assertionsToCheck
[i
] = d_smt
.d_theoryEngine
->preprocess(d_assertionsToCheck
[i
]);
2226 dumpAssertions("post-theory-preprocessing", d_assertionsToCheck
);
2228 // Push the formula to decision engine
2230 Chat() << "pushing to decision engine..." << endl
;
2231 Assert(iteRewriteAssertionsEnd
== d_assertionsToCheck
.size());
2232 d_smt
.d_decisionEngine
->addAssertions
2233 (d_assertionsToCheck
, d_realAssertionsEnd
, d_iteSkolemMap
);
2236 // end: INVARIANT to maintain: no reordering of assertions or
2237 // introducing new ones
2239 dumpAssertions("post-everything", d_assertionsToCheck
);
2241 // Push the formula to SAT
2243 Chat() << "converting to CNF..." << endl
;
2244 TimerStat::CodeTimer
codeTimer(d_smt
.d_stats
->d_cnfConversionTime
);
2245 for (unsigned i
= 0; i
< d_assertionsToCheck
.size(); ++ i
) {
2246 d_smt
.d_propEngine
->assertFormula(d_assertionsToCheck
[i
]);
2250 d_assertionsToCheck
.clear();
2251 d_iteSkolemMap
.clear();
2254 void SmtEnginePrivate::addFormula(TNode n
)
2255 throw(TypeCheckingException
, LogicException
) {
2257 Trace("smt") << "SmtEnginePrivate::addFormula(" << n
<< ")" << endl
;
2259 // Add the normalized formula to the queue
2260 d_assertionsToPreprocess
.push_back(n
);
2261 //d_assertionsToPreprocess.push_back(Rewriter::rewrite(n));
2263 // If the mode of processing is incremental prepreocess and assert immediately
2264 if (options::simplificationMode() == SIMPLIFICATION_MODE_INCREMENTAL
) {
2265 processAssertions();
2269 void SmtEngine::ensureBoolean(const Expr
& e
) throw(TypeCheckingException
) {
2270 Type type
= e
.getType(options::typeChecking());
2271 Type boolType
= d_exprManager
->booleanType();
2272 if(type
!= boolType
) {
2274 ss
<< "Expected " << boolType
<< "\n"
2275 << "The assertion : " << e
<< "\n"
2276 << "Its type : " << type
;
2277 throw TypeCheckingException(e
, ss
.str());
2281 Result
SmtEngine::checkSat(const Expr
& ex
) throw(TypeCheckingException
, ModalException
, LogicException
) {
2282 Assert(ex
.isNull() || ex
.getExprManager() == d_exprManager
);
2283 SmtScope
smts(this);
2284 finalOptionsAreSet();
2286 Trace("smt") << "SmtEngine::checkSat(" << ex
<< ")" << endl
;
2288 if(d_queryMade
&& !options::incrementalSolving()) {
2289 throw ModalException("Cannot make multiple queries unless "
2290 "incremental solving is enabled "
2291 "(try --incremental)");
2296 // Substitute out any abstract values in ex.
2297 e
= d_private
->substituteAbstractValues(Node::fromExpr(ex
)).toExpr();
2298 // Ensure expr is type-checked at this point.
2302 // check to see if a postsolve() is pending
2303 if(d_needPostsolve
) {
2304 d_theoryEngine
->postsolve();
2305 d_needPostsolve
= false;
2311 // Note that a query has been made
2316 d_problemExtended
= true;
2317 if(d_assertionList
!= NULL
) {
2318 d_assertionList
->push_back(e
);
2320 d_private
->addFormula(e
.getNode());
2324 Result r
= check().asSatisfiabilityResult();
2325 d_needPostsolve
= true;
2327 // Dump the query if requested
2328 if(Dump
.isOn("benchmark")) {
2329 // the expr already got dumped out if assertion-dumping is on
2330 Dump("benchmark") << CheckSatCommand();
2336 // Remember the status
2339 d_problemExtended
= false;
2341 Trace("smt") << "SmtEngine::checkSat(" << e
<< ") => " << r
<< endl
;
2343 // Check that SAT results generate a model correctly.
2344 if(options::checkModels()){
2345 if(r
.asSatisfiabilityResult().isSat() == Result::SAT
||
2346 (r
.isUnknown() && r
.whyUnknown() == Result::INCOMPLETE
) ){
2347 checkModel(/* hard failure iff */ ! r
.isUnknown());
2352 }/* SmtEngine::checkSat() */
2354 Result
SmtEngine::query(const Expr
& ex
) throw(TypeCheckingException
, ModalException
, LogicException
) {
2355 Assert(!ex
.isNull());
2356 Assert(ex
.getExprManager() == d_exprManager
);
2357 SmtScope
smts(this);
2358 finalOptionsAreSet();
2360 Trace("smt") << "SMT query(" << ex
<< ")" << endl
;
2362 if(d_queryMade
&& !options::incrementalSolving()) {
2363 throw ModalException("Cannot make multiple queries unless "
2364 "incremental solving is enabled "
2365 "(try --incremental)");
2368 // Substitute out any abstract values in ex
2369 Expr e
= d_private
->substituteAbstractValues(Node::fromExpr(ex
)).toExpr();
2371 // Ensure that the expression is type-checked at this point, and Boolean
2374 // check to see if a postsolve() is pending
2375 if(d_needPostsolve
) {
2376 d_theoryEngine
->postsolve();
2377 d_needPostsolve
= false;
2383 // Note that a query has been made
2387 d_problemExtended
= true;
2388 d_private
->addFormula(e
.getNode().notNode());
2391 Result r
= check().asValidityResult();
2392 d_needPostsolve
= true;
2394 // Dump the query if requested
2395 if(Dump
.isOn("benchmark")) {
2396 // the expr already got dumped out if assertion-dumping is on
2397 Dump("benchmark") << CheckSatCommand();
2403 // Remember the status
2406 d_problemExtended
= false;
2408 Trace("smt") << "SMT query(" << e
<< ") ==> " << r
<< endl
;
2410 // Check that SAT results generate a model correctly.
2411 if(options::checkModels()){
2412 if(r
.asSatisfiabilityResult().isSat() == Result::SAT
||
2413 (r
.isUnknown() && r
.whyUnknown() == Result::INCOMPLETE
) ){
2414 checkModel(/* hard failure iff */ ! r
.isUnknown());
2419 }/* SmtEngine::query() */
2421 Result
SmtEngine::assertFormula(const Expr
& ex
) throw(TypeCheckingException
, LogicException
) {
2422 Assert(ex
.getExprManager() == d_exprManager
);
2423 SmtScope
smts(this);
2424 finalOptionsAreSet();
2426 Trace("smt") << "SmtEngine::assertFormula(" << ex
<< ")" << endl
;
2428 // Substitute out any abstract values in ex
2429 Expr e
= d_private
->substituteAbstractValues(Node::fromExpr(ex
)).toExpr();
2432 if(d_assertionList
!= NULL
) {
2433 d_assertionList
->push_back(e
);
2435 d_private
->addFormula(e
.getNode());
2436 return quickCheck().asValidityResult();
2439 Expr
SmtEngine::simplify(const Expr
& ex
) throw(TypeCheckingException
, LogicException
) {
2440 Assert(ex
.getExprManager() == d_exprManager
);
2441 SmtScope
smts(this);
2442 finalOptionsAreSet();
2444 Trace("smt") << "SMT simplify(" << ex
<< ")" << endl
;
2446 if(Dump
.isOn("benchmark")) {
2447 Dump("benchmark") << SimplifyCommand(ex
);
2450 Expr e
= d_private
->substituteAbstractValues(Node::fromExpr(ex
)).toExpr();
2451 if( options::typeChecking() ) {
2452 e
.getType(true);// ensure expr is type-checked at this point
2455 // Make sure all preprocessing is done
2456 d_private
->processAssertions();
2457 return d_private
->simplify(Node::fromExpr(e
)).toExpr();
2460 Expr
SmtEngine::expandDefinitions(const Expr
& ex
) throw(TypeCheckingException
, LogicException
) {
2461 Assert(ex
.getExprManager() == d_exprManager
);
2462 SmtScope
smts(this);
2463 finalOptionsAreSet();
2465 Trace("smt") << "SMT expandDefinitions(" << ex
<< ")" << endl
;
2467 // Substitute out any abstract values in ex.
2468 Expr e
= d_private
->substituteAbstractValues(Node::fromExpr(ex
)).toExpr();
2469 if(options::typeChecking()) {
2470 // Ensure expr is type-checked at this point.
2473 if(Dump
.isOn("benchmark")) {
2474 Dump("benchmark") << ExpandDefinitionsCommand(e
);
2476 hash_map
<Node
, Node
, NodeHashFunction
> cache
;
2477 return d_private
->expandDefinitions(Node::fromExpr(e
), cache
).toExpr();
2480 Expr
SmtEngine::getValue(const Expr
& ex
) throw(ModalException
, LogicException
) {
2481 Assert(ex
.getExprManager() == d_exprManager
);
2482 SmtScope
smts(this);
2484 Trace("smt") << "SMT getValue(" << ex
<< ")" << endl
;
2485 if(Dump
.isOn("benchmark")) {
2486 Dump("benchmark") << GetValueCommand(ex
);
2489 if(!options::produceModels()) {
2491 "Cannot get value when produce-models options is off.";
2492 throw ModalException(msg
);
2494 if(d_status
.isNull() ||
2495 d_status
.asSatisfiabilityResult() == Result::UNSAT
||
2496 d_problemExtended
) {
2498 "Cannot get value unless immediately preceded by SAT/INVALID or UNKNOWN response.";
2499 throw ModalException(msg
);
2502 // Substitute out any abstract values in ex.
2503 Expr e
= d_private
->substituteAbstractValues(Node::fromExpr(ex
)).toExpr();
2505 // Ensure expr is type-checked at this point.
2506 e
.getType(options::typeChecking());
2508 // do not need to apply preprocessing substitutions (should be recorded
2509 // in model already)
2511 // Expand, then normalize
2512 hash_map
<Node
, Node
, NodeHashFunction
> cache
;
2513 Node n
= d_private
->expandDefinitions(Node::fromExpr(e
), cache
);
2514 n
= Rewriter::rewrite(n
);
2516 Trace("smt") << "--- getting value of " << n
<< endl
;
2517 TheoryModel
* m
= d_theoryEngine
->getModel();
2520 resultNode
= m
->getValue( n
);
2522 Trace("smt") << "--- got value " << n
<< " = " << resultNode
<< endl
;
2524 // type-check the result we got
2525 Assert(resultNode
.isNull() || resultNode
.getType().isSubtypeOf(n
.getType()));
2527 // ensure it's a constant
2528 Assert(resultNode
.isConst());
2530 if(options::abstractValues() && resultNode
.getType().isArray()) {
2531 resultNode
= d_private
->mkAbstractValue(resultNode
);
2534 return resultNode
.toExpr();
2537 bool SmtEngine::addToAssignment(const Expr
& ex
) throw() {
2538 SmtScope
smts(this);
2539 finalOptionsAreSet();
2541 // Substitute out any abstract values in ex
2542 Expr e
= d_private
->substituteAbstractValues(Node::fromExpr(ex
)).toExpr();
2543 Type type
= e
.getType(options::typeChecking());
2545 CheckArgument( type
.isBoolean(), e
,
2546 "expected Boolean-typed variable or function application "
2547 "in addToAssignment()" );
2548 Node n
= e
.getNode();
2549 // must be an APPLY of a zero-ary defined function, or a variable
2550 CheckArgument( ( ( n
.getKind() == kind::APPLY
&&
2551 ( d_definedFunctions
->find(n
.getOperator()) !=
2552 d_definedFunctions
->end() ) &&
2553 n
.getNumChildren() == 0 ) ||
2555 "expected variable or defined-function application "
2556 "in addToAssignment(),\ngot %s", e
.toString().c_str() );
2557 if(!options::produceAssignments()) {
2560 if(d_assignments
== NULL
) {
2561 d_assignments
= new(true) AssignmentSet(d_context
);
2563 d_assignments
->insert(n
);
2568 CVC4::SExpr
SmtEngine::getAssignment() throw(ModalException
) {
2569 Trace("smt") << "SMT getAssignment()" << endl
;
2570 SmtScope
smts(this);
2571 finalOptionsAreSet();
2572 if(Dump
.isOn("benchmark")) {
2573 Dump("benchmark") << GetAssignmentCommand();
2575 if(!options::produceAssignments()) {
2577 "Cannot get the current assignment when "
2578 "produce-assignments option is off.";
2579 throw ModalException(msg
);
2581 if(d_status
.isNull() ||
2582 d_status
.asSatisfiabilityResult() == Result::UNSAT
||
2583 d_problemExtended
) {
2585 "Cannot get the current assignment unless immediately "
2586 "preceded by SAT/INVALID or UNKNOWN response.";
2587 throw ModalException(msg
);
2590 if(d_assignments
== NULL
) {
2594 vector
<SExpr
> sexprs
;
2595 TypeNode boolType
= d_nodeManager
->booleanType();
2596 for(AssignmentSet::const_iterator i
= d_assignments
->begin(),
2597 iend
= d_assignments
->end();
2600 Assert((*i
).getType() == boolType
);
2603 Node n
= Rewriter::rewrite(*i
);
2605 Trace("smt") << "--- getting value of " << n
<< endl
;
2606 TheoryModel
* m
= d_theoryEngine
->getModel();
2609 resultNode
= m
->getValue( n
);
2612 // type-check the result we got
2613 Assert(resultNode
.isNull() || resultNode
.getType() == boolType
);
2616 if((*i
).getKind() == kind::APPLY
) {
2617 Assert((*i
).getNumChildren() == 0);
2618 v
.push_back((*i
).getOperator().toString());
2620 Assert((*i
).isVar());
2621 v
.push_back((*i
).toString());
2623 v
.push_back(resultNode
.toString());
2624 sexprs
.push_back(v
);
2626 return SExpr(sexprs
);
2629 void SmtEngine::addToModelCommandAndDump(const Command
& c
, const char* dumpTag
) {
2630 Trace("smt") << "SMT addToModelCommand(" << c
<< ")" << endl
;
2631 SmtScope
smts(this);
2632 // If we aren't yet fully inited, the user might still turn on
2633 // produce-models. So let's keep any commands around just in
2634 // case. This is useful in two cases: (1) SMT-LIBv1 auto-declares
2635 // sort "U" in QF_UF before setLogic() is run and we still want to
2636 // support finding card(U) with --finite-model-find, and (2) to
2637 // decouple SmtEngine and ExprManager if the user does a few
2638 // ExprManager::mkSort() before SmtEngine::setOption("produce-models")
2639 // and expects to find their cardinalities in the model.
2640 if( !d_fullyInited
|| options::produceModels() ) {
2642 d_modelCommands
->push_back(c
.clone());
2644 if(Dump
.isOn(dumpTag
)) {
2648 d_dumpCommands
.push_back(c
.clone());
2653 Model
* SmtEngine::getModel() throw(ModalException
) {
2654 Trace("smt") << "SMT getModel()" << endl
;
2655 SmtScope
smts(this);
2657 finalOptionsAreSet();
2659 if(Dump
.isOn("benchmark")) {
2660 Dump("benchmark") << GetModelCommand();
2663 if(d_status
.isNull() ||
2664 d_status
.asSatisfiabilityResult() == Result::UNSAT
||
2665 d_problemExtended
) {
2667 "Cannot get the current model unless immediately "
2668 "preceded by SAT/INVALID or UNKNOWN response.";
2669 throw ModalException(msg
);
2671 if(!options::produceModels()) {
2673 "Cannot get model when produce-models options is off.";
2674 throw ModalException(msg
);
2676 return d_theoryEngine
->getModel();
2679 void SmtEngine::checkModel(bool hardFailure
) {
2680 // --check-model implies --interactive, which enables the assertion list,
2681 // so we should be ok.
2682 Assert(d_assertionList
!= NULL
, "don't have an assertion list to check in SmtEngine::checkModel()");
2684 TimerStat::CodeTimer
checkModelTimer(d_stats
->d_checkModelTime
);
2686 // Throughout, we use Notice() to give diagnostic output.
2688 // If this function is running, the user gave --check-model (or equivalent),
2689 // and if Notice() is on, the user gave --verbose (or equivalent).
2691 Notice() << "SmtEngine::checkModel(): generating model" << endl
;
2692 TheoryModel
* m
= d_theoryEngine
->getModel();
2694 // Check individual theory assertions
2695 d_theoryEngine
->checkTheoryAssertionsWithModel();
2698 // This operator<< routine is non-const (i.e., takes a non-const Model&).
2699 // This confuses the Notice() output routines, so extract the ostream
2700 // from it and output it "manually." Should be fixed by making Model
2702 Notice
.getStream() << *m
;
2705 // We have a "fake context" for the substitution map (we don't need it
2706 // to be context-dependent)
2707 context::Context fakeContext
;
2708 SubstitutionMap
substitutions(&fakeContext
);
2710 for(size_t k
= 0; k
< m
->getNumCommands(); ++k
) {
2711 const DeclareFunctionCommand
* c
= dynamic_cast<const DeclareFunctionCommand
*>(m
->getCommand(k
));
2712 Notice() << "SmtEngine::checkModel(): model command " << k
<< " : " << m
->getCommand(k
) << endl
;
2714 // we don't care about DECLARE-DATATYPES, DECLARE-SORT, ...
2715 Notice() << "SmtEngine::checkModel(): skipping..." << endl
;
2717 // We have a DECLARE-FUN:
2719 // We'll first do some checks, then add to our substitution map
2720 // the mapping: function symbol |-> value
2722 Expr func
= c
->getFunction();
2723 Node val
= m
->getValue(func
);
2725 Notice() << "SmtEngine::checkModel(): adding substitution: " << func
<< " |-> " << val
<< endl
;
2727 // (1) check that the value is actually a value
2728 if(!val
.isConst()) {
2729 Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE NOT A CONSTANT ***" << endl
;
2731 ss
<< "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
2732 << "model value for " << func
<< endl
2733 << " is " << val
<< endl
2734 << "and that is not a constant (.isConst() == false)." << endl
2735 << "Run with `--check-models -v' for additional diagnostics.";
2736 InternalError(ss
.str());
2739 // (2) if the value is a lambda, ensure the lambda doesn't contain the
2740 // function symbol (since then the definition is recursive)
2741 if(val
.getKind() == kind::LAMBDA
) {
2742 // first apply the model substitutions we have so far
2743 Node n
= substitutions
.apply(val
[1]);
2744 // now check if n contains func by doing a substitution
2745 // [func->func2] and checking equality of the Nodes.
2746 // (this just a way to check if func is in n.)
2747 SubstitutionMap
subs(&fakeContext
);
2748 Node func2
= NodeManager::currentNM()->mkSkolem("", TypeNode::fromType(func
.getType()), "", NodeManager::SKOLEM_NO_NOTIFY
);
2749 subs
.addSubstitution(func
, func2
);
2750 if(subs
.apply(n
) != n
) {
2751 Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE DEFINED IN TERMS OF ITSELF ***" << endl
;
2753 ss
<< "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
2754 << "considering model value for " << func
<< endl
2755 << "body of lambda is: " << val
<< endl
;
2757 ss
<< "body substitutes to: " << n
<< endl
;
2759 ss
<< "so " << func
<< " is defined in terms of itself." << endl
2760 << "Run with `--check-models -v' for additional diagnostics.";
2761 InternalError(ss
.str());
2765 // (3) checks complete, add the substitution
2766 substitutions
.addSubstitution(func
, val
);
2770 // Now go through all our user assertions checking if they're satisfied.
2771 for(AssertionList::const_iterator i
= d_assertionList
->begin(); i
!= d_assertionList
->end(); ++i
) {
2772 Notice() << "SmtEngine::checkModel(): checking assertion " << *i
<< endl
;
2773 Node n
= Node::fromExpr(*i
);
2775 // Apply any define-funs from the problem.
2777 hash_map
<Node
, Node
, NodeHashFunction
> cache
;
2778 n
= d_private
->expandDefinitions(n
, cache
);
2781 // Apply our model value substitutions.
2782 n
= substitutions
.apply(n
);
2783 Notice() << "SmtEngine::checkModel(): -- substitutes to " << n
<< endl
;
2785 // Simplify the result.
2786 n
= d_private
->simplify(n
);
2787 Notice() << "SmtEngine::checkModel(): -- simplifies to " << n
<< endl
;
2789 TheoryId thy
= Theory::theoryOf(n
);
2790 if(thy
== THEORY_QUANTIFIERS
|| thy
== THEORY_REWRITERULES
) {
2791 // Note this "skip" is done here, rather than above. This is
2792 // because (1) the quantifier could in principle simplify to false,
2793 // which should be reported, and (2) checking for the quantifier
2794 // above, before simplification, doesn't catch buried quantifiers
2795 // anyway (those not at the top-level).
2796 Notice() << "SmtEngine::checkModel(): -- skipping quantified assertion"
2801 // The result should be == true.
2802 if(n
!= NodeManager::currentNM()->mkConst(true)) {
2803 Notice() << "SmtEngine::checkModel(): *** PROBLEM: EXPECTED `TRUE' ***"
2806 ss
<< "SmtEngine::checkModel(): "
2807 << "ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
2808 << "assertion: " << *i
<< endl
2809 << "simplifies to: " << n
<< endl
2810 << "expected `true'." << endl
2811 << "Run with `--check-models -v' for additional diagnostics.";
2813 InternalError(ss
.str());
2815 Warning() << ss
.str() << endl
;
2819 Notice() << "SmtEngine::checkModel(): all assertions checked out OK !" << endl
;
2822 Proof
* SmtEngine::getProof() throw(ModalException
) {
2823 Trace("smt") << "SMT getProof()" << endl
;
2824 SmtScope
smts(this);
2825 finalOptionsAreSet();
2826 if(Dump
.isOn("benchmark")) {
2827 Dump("benchmark") << GetProofCommand();
2830 if(!options::proof()) {
2832 "Cannot get a proof when produce-proofs option is off.";
2833 throw ModalException(msg
);
2835 if(d_status
.isNull() ||
2836 d_status
.asSatisfiabilityResult() != Result::UNSAT
||
2837 d_problemExtended
) {
2839 "Cannot get a proof unless immediately preceded by UNSAT/VALID response.";
2840 throw ModalException(msg
);
2843 return ProofManager::getProof();
2844 #else /* CVC4_PROOF */
2845 throw ModalException("This build of CVC4 doesn't have proof support.");
2846 #endif /* CVC4_PROOF */
2849 vector
<Expr
> SmtEngine::getAssertions() throw(ModalException
) {
2850 SmtScope
smts(this);
2851 finalOptionsAreSet();
2852 if(Dump
.isOn("benchmark")) {
2853 Dump("benchmark") << GetAssertionsCommand();
2855 Trace("smt") << "SMT getAssertions()" << endl
;
2856 if(!options::interactive()) {
2858 "Cannot query the current assertion list when not in interactive mode.";
2859 throw ModalException(msg
);
2861 Assert(d_assertionList
!= NULL
);
2862 // copy the result out
2863 return vector
<Expr
>(d_assertionList
->begin(), d_assertionList
->end());
2866 void SmtEngine::push() throw(ModalException
, LogicException
) {
2867 SmtScope
smts(this);
2868 finalOptionsAreSet();
2870 Trace("smt") << "SMT push()" << endl
;
2871 d_private
->processAssertions();
2872 if(Dump
.isOn("benchmark")) {
2873 Dump("benchmark") << PushCommand();
2875 if(!options::incrementalSolving()) {
2876 throw ModalException("Cannot push when not solving incrementally (use --incremental)");
2879 // check to see if a postsolve() is pending
2880 if(d_needPostsolve
) {
2881 d_theoryEngine
->postsolve();
2882 d_needPostsolve
= false;
2885 d_userLevels
.push_back(d_userContext
->getLevel());
2887 Trace("userpushpop") << "SmtEngine: pushed to level "
2888 << d_userContext
->getLevel() << endl
;
2891 void SmtEngine::pop() throw(ModalException
) {
2892 SmtScope
smts(this);
2893 finalOptionsAreSet();
2894 Trace("smt") << "SMT pop()" << endl
;
2895 if(Dump
.isOn("benchmark")) {
2896 Dump("benchmark") << PopCommand();
2898 if(!options::incrementalSolving()) {
2899 throw ModalException("Cannot pop when not solving incrementally (use --incremental)");
2901 if(d_userLevels
.size() == 0) {
2902 throw ModalException("Cannot pop beyond the first user frame");
2905 // check to see if a postsolve() is pending
2906 if(d_needPostsolve
) {
2907 d_theoryEngine
->postsolve();
2908 d_needPostsolve
= false;
2911 AlwaysAssert(d_userContext
->getLevel() > 0);
2912 AlwaysAssert(d_userLevels
.back() < d_userContext
->getLevel());
2913 while (d_userLevels
.back() < d_userContext
->getLevel()) {
2916 d_userLevels
.pop_back();
2918 // Clear out assertion queues etc., in case anything is still in there
2919 d_private
->notifyPop();
2921 Trace("userpushpop") << "SmtEngine: popped to level "
2922 << d_userContext
->getLevel() << endl
;
2923 // FIXME: should we reset d_status here?
2924 // SMT-LIBv2 spec seems to imply no, but it would make sense to..
2925 // Still, we want the right exit status after any final sequence
2929 void SmtEngine::internalPush() {
2930 Assert(d_fullyInited
);
2931 Trace("smt") << "SmtEngine::internalPush()" << endl
;
2933 if(options::incrementalSolving()) {
2934 d_private
->processAssertions();
2935 d_userContext
->push();
2936 // the d_context push is done inside of the SAT solver
2937 d_propEngine
->push();
2941 void SmtEngine::internalPop(bool immediate
) {
2942 Assert(d_fullyInited
);
2943 Trace("smt") << "SmtEngine::internalPop()" << endl
;
2944 if(options::incrementalSolving()) {
2952 void SmtEngine::doPendingPops() {
2953 Assert(d_pendingPops
== 0 || options::incrementalSolving());
2954 while(d_pendingPops
> 0) {
2955 d_propEngine
->pop();
2956 // the d_context pop is done inside of the SAT solver
2957 d_userContext
->pop();
2962 void SmtEngine::interrupt() throw(ModalException
) {
2963 if(!d_fullyInited
) {
2966 d_propEngine
->interrupt();
2967 d_theoryEngine
->interrupt();
2970 void SmtEngine::setResourceLimit(unsigned long units
, bool cumulative
) {
2972 Trace("limit") << "SmtEngine: setting cumulative resource limit to " << units
<< endl
;
2973 d_resourceBudgetCumulative
= (units
== 0) ? 0 : (d_cumulativeResourceUsed
+ units
);
2975 Trace("limit") << "SmtEngine: setting per-call resource limit to " << units
<< endl
;
2976 d_resourceBudgetPerCall
= units
;
2980 void SmtEngine::setTimeLimit(unsigned long millis
, bool cumulative
) {
2982 Trace("limit") << "SmtEngine: setting cumulative time limit to " << millis
<< " ms" << endl
;
2983 d_timeBudgetCumulative
= (millis
== 0) ? 0 : (d_cumulativeTimeUsed
+ millis
);
2985 Trace("limit") << "SmtEngine: setting per-call time limit to " << millis
<< " ms" << endl
;
2986 d_timeBudgetPerCall
= millis
;
2990 unsigned long SmtEngine::getResourceUsage() const {
2991 return d_cumulativeResourceUsed
;
2994 unsigned long SmtEngine::getTimeUsage() const {
2995 return d_cumulativeTimeUsed
;
2998 unsigned long SmtEngine::getResourceRemaining() const throw(ModalException
) {
2999 if(d_resourceBudgetCumulative
== 0) {
3000 throw ModalException("No cumulative resource limit is currently set");
3003 return d_resourceBudgetCumulative
<= d_cumulativeResourceUsed
? 0 :
3004 d_resourceBudgetCumulative
- d_cumulativeResourceUsed
;
3007 unsigned long SmtEngine::getTimeRemaining() const throw(ModalException
) {
3008 if(d_timeBudgetCumulative
== 0) {
3009 throw ModalException("No cumulative time limit is currently set");
3012 return d_timeBudgetCumulative
<= d_cumulativeTimeUsed
? 0 :
3013 d_timeBudgetCumulative
- d_cumulativeTimeUsed
;
3016 Statistics
SmtEngine::getStatistics() const throw() {
3017 return Statistics(*d_statisticsRegistry
);
3020 SExpr
SmtEngine::getStatistic(std::string name
) const throw() {
3021 return d_statisticsRegistry
->getStatistic(name
);
3024 void SmtEngine::setUserAttribute(const std::string
& attr
, Expr expr
) {
3025 SmtScope
smts(this);
3026 d_theoryEngine
->setUserAttribute(attr
, expr
.getNode());
3029 }/* CVC4 namespace */