1 /********************* */
2 /*! \file theory_engine.cpp
4 ** Original author: Morgan Deters
5 ** Major contributors: Dejan Jovanovic
6 ** Minor contributors (to current version): Christopher L. Conway, Kshitij Bansal, Liana Hadarean, Clark Barrett, Tim King, Andrew Reynolds
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2013 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 theory engine
20 #include "decision/decision_engine.h"
22 #include "expr/attribute.h"
23 #include "expr/node.h"
24 #include "expr/node_builder.h"
25 #include "options/options.h"
26 #include "util/lemma_output_channel.h"
28 #include "theory/theory.h"
29 #include "theory/theory_engine.h"
30 #include "theory/rewriter.h"
31 #include "theory/theory_traits.h"
33 #include "smt/logic_exception.h"
35 #include "util/node_visitor.h"
36 #include "util/ite_removal.h"
38 //#include "theory/ite_simplifier.h"
39 //#include "theory/ite_compressor.h"
40 #include "theory/ite_utilities.h"
41 #include "theory/unconstrained_simplifier.h"
43 #include "theory/theory_model.h"
45 #include "theory/quantifiers_engine.h"
46 #include "theory/quantifiers/theory_quantifiers.h"
47 #include "theory/quantifiers/options.h"
48 #include "theory/quantifiers/model_engine.h"
49 #include "theory/quantifiers/first_order_model.h"
51 #include "theory/uf/equality_engine.h"
53 #include "theory/rewriterules/efficient_e_matching.h"
55 #include "proof/proof_manager.h"
60 using namespace CVC4::theory
;
62 void TheoryEngine::finishInit() {
63 // initialize the quantifiers engine
64 d_quantEngine
= new QuantifiersEngine(d_context
, d_userContext
, this);
66 if (d_logicInfo
.isQuantified()) {
67 d_quantEngine
->finishInit();
68 Assert(d_masterEqualityEngine
== 0);
69 d_masterEqualityEngine
= new eq::EqualityEngine(d_masterEENotify
,getSatContext(), "theory::master");
71 for(TheoryId theoryId
= theory::THEORY_FIRST
; theoryId
!= theory::THEORY_LAST
; ++ theoryId
) {
72 if (d_theoryTable
[theoryId
]) {
73 d_theoryTable
[theoryId
]->setQuantifiersEngine(d_quantEngine
);
74 d_theoryTable
[theoryId
]->setMasterEqualityEngine(d_masterEqualityEngine
);
79 for(TheoryId theoryId
= theory::THEORY_FIRST
; theoryId
!= theory::THEORY_LAST
; ++ theoryId
) {
80 if (d_theoryTable
[theoryId
]) {
81 d_theoryTable
[theoryId
]->finishInit();
86 void TheoryEngine::eqNotifyNewClass(TNode t
){
87 d_quantEngine
->addTermToDatabase( t
);
88 if( d_logicInfo
.isQuantified() && options::quantConflictFind() ){
89 d_quantEngine
->getConflictFind()->newEqClass( t
);
93 void TheoryEngine::eqNotifyPreMerge(TNode t1
, TNode t2
){
94 //TODO: add notification to efficient E-matching
95 if( d_logicInfo
.isQuantified() ){
96 d_quantEngine
->getEfficientEMatcher()->merge( t1
, t2
);
97 if( options::quantConflictFind() ){
98 d_quantEngine
->getConflictFind()->merge( t1
, t2
);
103 void TheoryEngine::eqNotifyPostMerge(TNode t1
, TNode t2
){
107 void TheoryEngine::eqNotifyDisequal(TNode t1
, TNode t2
, TNode reason
){
108 if( d_logicInfo
.isQuantified() ){
109 if( options::quantConflictFind() ){
110 d_quantEngine
->getConflictFind()->assertDisequal( t1
, t2
);
116 TheoryEngine::TheoryEngine(context::Context
* context
,
117 context::UserContext
* userContext
,
118 RemoveITE
& iteRemover
,
119 const LogicInfo
& logicInfo
)
120 : d_propEngine(NULL
),
121 d_decisionEngine(NULL
),
123 d_userContext(userContext
),
124 d_logicInfo(logicInfo
),
125 d_sharedTerms(this, context
),
126 d_masterEqualityEngine(NULL
),
127 d_masterEENotify(*this),
130 d_curr_model_builder(NULL
),
132 d_possiblePropagations(context
),
133 d_hasPropagated(context
),
134 d_inConflict(context
, false),
135 d_hasShutDown(false),
136 d_incomplete(context
, false),
137 d_propagationMap(context
),
138 d_propagationMapTimestamp(context
, 0),
139 d_propagatedLiterals(context
),
140 d_propagatedLiteralsIndex(context
, 0),
141 d_atomRequests(context
),
142 d_iteRemover(iteRemover
),
143 d_combineTheoriesTime("TheoryEngine::combineTheoriesTime"),
146 d_interrupted(false),
147 d_inPreregister(false),
148 d_factsAsserted(context
, false),
149 d_preRegistrationVisitor(this, context
),
150 d_sharedTermsVisitor(d_sharedTerms
),
151 d_unconstrainedSimp(new UnconstrainedSimplifier(context
, logicInfo
)),
152 d_bvToBoolPreprocessor()
154 for(TheoryId theoryId
= theory::THEORY_FIRST
; theoryId
!= theory::THEORY_LAST
; ++ theoryId
) {
155 d_theoryTable
[theoryId
] = NULL
;
156 d_theoryOut
[theoryId
] = NULL
;
159 // build model information if applicable
160 d_curr_model
= new theory::TheoryModel(userContext
, "DefaultModel", true);
161 d_curr_model_builder
= new theory::TheoryEngineModelBuilder(this);
163 StatisticsRegistry::registerStat(&d_combineTheoriesTime
);
164 d_true
= NodeManager::currentNM()->mkConst
<bool>(true);
165 d_false
= NodeManager::currentNM()->mkConst
<bool>(false);
167 PROOF (ProofManager::currentPM()->initTheoryProof(); );
169 d_iteUtilities
= new ITEUtilities(d_iteRemover
.getContainsVisitor());
172 TheoryEngine::~TheoryEngine() {
173 Assert(d_hasShutDown
);
175 for(TheoryId theoryId
= theory::THEORY_FIRST
; theoryId
!= theory::THEORY_LAST
; ++ theoryId
) {
176 if(d_theoryTable
[theoryId
] != NULL
) {
177 delete d_theoryTable
[theoryId
];
178 delete d_theoryOut
[theoryId
];
182 delete d_curr_model_builder
;
185 delete d_quantEngine
;
187 delete d_masterEqualityEngine
;
189 StatisticsRegistry::unregisterStat(&d_combineTheoriesTime
);
191 delete d_unconstrainedSimp
;
193 delete d_iteUtilities
;
196 void TheoryEngine::interrupt() throw(ModalException
) {
197 d_interrupted
= true;
200 void TheoryEngine::preRegister(TNode preprocessed
) {
202 if(Dump
.isOn("missed-t-propagations")) {
203 d_possiblePropagations
.push_back(preprocessed
);
205 d_preregisterQueue
.push(preprocessed
);
207 if (!d_inPreregister
) {
208 // We're in pre-register
209 d_inPreregister
= true;
211 // Process the pre-registration queue
212 while (!d_preregisterQueue
.empty()) {
213 // Get the next atom to pre-register
214 preprocessed
= d_preregisterQueue
.front();
215 d_preregisterQueue
.pop();
217 if (d_logicInfo
.isSharingEnabled() && preprocessed
.getKind() == kind::EQUAL
) {
218 // When sharing is enabled, we propagate from the shared terms manager also
219 d_sharedTerms
.addEqualityToPropagate(preprocessed
);
222 // Pre-register the terms in the atom
223 Theory::Set theories
= NodeVisitor
<PreRegisterVisitor
>::run(d_preRegistrationVisitor
, preprocessed
);
224 theories
= Theory::setRemove(THEORY_BOOL
, theories
);
225 // Remove the top theory, if any more that means multiple theories were involved
226 bool multipleTheories
= Theory::setRemove(Theory::theoryOf(preprocessed
), theories
);
228 // These checks don't work with finite model finding, because it
229 // uses Rational constants to represent cardinality constraints,
230 // even though arithmetic isn't actually involved.
231 if(!options::finiteModelFind()) {
232 while((i
= Theory::setPop(theories
)) != THEORY_LAST
) {
233 if(!d_logicInfo
.isTheoryEnabled(i
)) {
234 LogicInfo newLogicInfo
= d_logicInfo
.getUnlockedCopy();
235 newLogicInfo
.enableTheory(i
);
238 ss
<< "The logic was specified as " << d_logicInfo
.getLogicString()
239 << ", which doesn't include " << i
240 << ", but found a term in that theory." << endl
241 << "You might want to extend your logic to "
242 << newLogicInfo
.getLogicString() << endl
;
243 throw LogicException(ss
.str());
247 if (multipleTheories
) {
248 // Collect the shared terms if there are multiple theories
249 NodeVisitor
<SharedTermsVisitor
>::run(d_sharedTermsVisitor
, preprocessed
);
253 // Leaving pre-register
254 d_inPreregister
= false;
258 void TheoryEngine::printAssertions(const char* tag
) {
259 if (Trace
.isOn(tag
)) {
261 for (TheoryId theoryId
= THEORY_FIRST
; theoryId
< THEORY_LAST
; ++theoryId
) {
262 Theory
* theory
= d_theoryTable
[theoryId
];
263 if (theory
&& d_logicInfo
.isTheoryEnabled(theoryId
)) {
264 Trace(tag
) << "--------------------------------------------" << endl
;
265 Trace(tag
) << "Assertions of " << theory
->getId() << ": " << endl
;
266 context::CDList
<Assertion
>::const_iterator it
= theory
->facts_begin(), it_end
= theory
->facts_end();
267 for (unsigned i
= 0; it
!= it_end
; ++ it
, ++i
) {
268 if ((*it
).isPreregistered
) {
269 Trace(tag
) << "[" << i
<< "]: ";
271 Trace(tag
) << "(" << i
<< "): ";
273 Trace(tag
) << (*it
).assertion
<< endl
;
276 if (d_logicInfo
.isSharingEnabled()) {
277 Trace(tag
) << "Shared terms of " << theory
->getId() << ": " << endl
;
278 context::CDList
<TNode
>::const_iterator it
= theory
->shared_terms_begin(), it_end
= theory
->shared_terms_end();
279 for (unsigned i
= 0; it
!= it_end
; ++ it
, ++i
) {
280 Trace(tag
) << "[" << i
<< "]: " << (*it
) << endl
;
288 void TheoryEngine::dumpAssertions(const char* tag
) {
289 if (Dump
.isOn(tag
)) {
290 Dump(tag
) << CommentCommand("Starting completeness check");
291 for (TheoryId theoryId
= THEORY_FIRST
; theoryId
< THEORY_LAST
; ++theoryId
) {
292 Theory
* theory
= d_theoryTable
[theoryId
];
293 if (theory
&& d_logicInfo
.isTheoryEnabled(theoryId
)) {
294 Dump(tag
) << CommentCommand("Completeness check");
295 Dump(tag
) << PushCommand();
297 // Dump the shared terms
298 if (d_logicInfo
.isSharingEnabled()) {
299 Dump(tag
) << CommentCommand("Shared terms");
300 context::CDList
<TNode
>::const_iterator it
= theory
->shared_terms_begin(), it_end
= theory
->shared_terms_end();
301 for (unsigned i
= 0; it
!= it_end
; ++ it
, ++i
) {
304 Dump(tag
) << CommentCommand(ss
.str());
308 // Dump the assertions
309 Dump(tag
) << CommentCommand("Assertions");
310 context::CDList
<Assertion
>::const_iterator it
= theory
->facts_begin(), it_end
= theory
->facts_end();
311 for (; it
!= it_end
; ++ it
) {
313 Node assertionNode
= (*it
).assertion
;
314 // Purify all the terms
316 if ((*it
).isPreregistered
) {
317 Dump(tag
) << CommentCommand("Preregistered");
319 Dump(tag
) << CommentCommand("Shared assertion");
321 Dump(tag
) << AssertCommand(assertionNode
.toExpr());
323 Dump(tag
) << CheckSatCommand();
325 Dump(tag
) << PopCommand();
332 * Check all (currently-active) theories for conflicts.
333 * @param effort the effort level to use
335 void TheoryEngine::check(Theory::Effort effort
) {
337 d_propEngine
->checkTime();
339 // Reset the interrupt flag
340 d_interrupted
= false;
342 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
343 #undef CVC4_FOR_EACH_THEORY_STATEMENT
345 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
346 if (theory::TheoryTraits<THEORY>::hasCheck && d_logicInfo.isTheoryEnabled(THEORY)) { \
347 theoryOf(THEORY)->check(effort); \
348 if (d_inConflict) { \
356 // Mark the output channel unused (if this is FULL_EFFORT, and nothing
357 // is done by the theories, no additional check will be needed)
358 d_outputChannelUsed
= false;
360 // Mark the lemmas flag (no lemmas added)
361 d_lemmasAdded
= false;
363 Debug("theory") << "TheoryEngine::check(" << effort
<< "): d_factsAsserted = " << (d_factsAsserted
? "true" : "false") << endl
;
365 // If in full effort, we have a fake new assertion just to jumpstart the checking
366 if (Theory::fullEffort(effort
)) {
367 d_factsAsserted
= true;
371 while (d_factsAsserted
&& !d_inConflict
&& !d_lemmasAdded
) {
373 Debug("theory") << "TheoryEngine::check(" << effort
<< "): running check" << endl
;
375 Trace("theory::assertions") << endl
;
376 if (Trace
.isOn("theory::assertions")) {
377 printAssertions("theory::assertions");
380 // Note that we've discharged all the facts
381 d_factsAsserted
= false;
384 CVC4_FOR_EACH_THEORY
;
386 if(Dump
.isOn("missed-t-conflicts")) {
387 Dump("missed-t-conflicts")
388 << CommentCommand("Completeness check for T-conflicts; expect sat")
389 << CheckSatCommand();
392 Debug("theory") << "TheoryEngine::check(" << effort
<< "): running propagation after the initial check" << endl
;
394 // We are still satisfiable, propagate as much as possible
397 // We do combination if all has been processed and we are in fullcheck
398 if (Theory::fullEffort(effort
) && d_logicInfo
.isSharingEnabled() && !d_factsAsserted
&& !d_lemmasAdded
) {
399 // Do the combination
400 Debug("theory") << "TheoryEngine::check(" << effort
<< "): running combination" << endl
;
405 // Must consult quantifiers theory for last call to ensure sat, or otherwise add a lemma
406 if( effort
== Theory::EFFORT_FULL
&& ! d_inConflict
&& ! needCheck() ) {
407 //d_theoryTable[THEORY_STRINGS]->check(Theory::EFFORT_LAST_CALL);
408 if(d_logicInfo
.isQuantified()) {
409 // quantifiers engine must pass effort last call check
410 d_quantEngine
->check(Theory::EFFORT_LAST_CALL
);
411 // if we have given up, then possibly flip decision
412 if(options::flipDecision()) {
413 if(d_incomplete
&& !d_inConflict
&& !needCheck()) {
414 ((theory::quantifiers::TheoryQuantifiers
*) d_theoryTable
[THEORY_QUANTIFIERS
])->flipDecision();
417 // if returning incomplete or SAT, we have ensured that the model in the quantifiers engine has been built
418 } else if(options::produceModels()) {
419 // must build model at this point
420 d_curr_model_builder
->buildModel(d_curr_model
, true);
424 Debug("theory") << "TheoryEngine::check(" << effort
<< "): done, we are " << (d_inConflict
? "unsat" : "sat") << (d_lemmasAdded
? " with new lemmas" : " with no new lemmas") << endl
;
426 if(!d_inConflict
&& Theory::fullEffort(effort
) && d_masterEqualityEngine
!= NULL
&& !d_lemmasAdded
) {
427 AlwaysAssert(d_masterEqualityEngine
->consistent());
429 } catch(const theory::Interrupted
&) {
430 Trace("theory") << "TheoryEngine::check() => interrupted" << endl
;
432 // If fulleffort, check all theories
433 if(Dump
.isOn("theory::fullcheck") && Theory::fullEffort(effort
)) {
434 if (!d_inConflict
&& !needCheck()) {
435 dumpAssertions("theory::fullcheck");
440 void TheoryEngine::combineTheories() {
442 Debug("sharing") << "TheoryEngine::combineTheories()" << endl
;
444 TimerStat::CodeTimer
combineTheoriesTimer(d_combineTheoriesTime
);
446 // Care graph we'll be building
449 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
450 #undef CVC4_FOR_EACH_THEORY_STATEMENT
452 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
453 if (theory::TheoryTraits<THEORY>::isParametric && d_logicInfo.isTheoryEnabled(THEORY)) { \
454 theoryOf(THEORY)->getCareGraph(careGraph); \
457 // Call on each parametric theory to give us its care graph
458 CVC4_FOR_EACH_THEORY
;
460 Debug("sharing") << "TheoryEngine::combineTheories(): care graph size = " << careGraph
.size() << endl
;
462 // Now add splitters for the ones we are interested in
463 CareGraph::const_iterator care_it
= careGraph
.begin();
464 CareGraph::const_iterator care_it_end
= careGraph
.end();
465 for (; care_it
!= care_it_end
; ++ care_it
) {
466 const CarePair
& carePair
= *care_it
;
468 Debug("sharing") << "TheoryEngine::combineTheories(): checking " << carePair
.a
<< " = " << carePair
.b
<< " from " << carePair
.theory
<< endl
;
470 Assert(d_sharedTerms
.isShared(carePair
.a
) || carePair
.a
.isConst());
471 Assert(d_sharedTerms
.isShared(carePair
.b
) || carePair
.b
.isConst());
473 // The equality in question (order for no repetition)
474 Node equality
= carePair
.a
.eqNode(carePair
.b
);
476 // We need to split on it
477 Debug("sharing") << "TheoryEngine::combineTheories(): requesting a split " << endl
;
478 lemma(equality
.orNode(equality
.notNode()), false, false, false, carePair
.theory
);
482 void TheoryEngine::propagate(Theory::Effort effort
) {
483 // Reset the interrupt flag
484 d_interrupted
= false;
486 // Definition of the statement that is to be run by every theory
487 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
488 #undef CVC4_FOR_EACH_THEORY_STATEMENT
490 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
491 if (theory::TheoryTraits<THEORY>::hasPropagate && d_logicInfo.isTheoryEnabled(THEORY)) { \
492 theoryOf(THEORY)->propagate(effort); \
495 // Reset the interrupt flag
496 d_interrupted
= false;
498 // Propagate for each theory using the statement above
499 CVC4_FOR_EACH_THEORY
;
501 if(Dump
.isOn("missed-t-propagations")) {
502 for(unsigned i
= 0; i
< d_possiblePropagations
.size(); ++i
) {
503 Node atom
= d_possiblePropagations
[i
];
505 if(d_propEngine
->hasValue(atom
, value
)) {
508 // Doesn't have a value, check it (and the negation)
509 if(d_hasPropagated
.find(atom
) == d_hasPropagated
.end()) {
510 Dump("missed-t-propagations")
511 << CommentCommand("Completeness check for T-propagations; expect invalid")
512 << EchoCommand(atom
.toString())
513 << QueryCommand(atom
.toExpr())
514 << EchoCommand(atom
.notNode().toString())
515 << QueryCommand(atom
.notNode().toExpr());
521 Node
TheoryEngine::getNextDecisionRequest() {
522 // Definition of the statement that is to be run by every theory
523 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
524 #undef CVC4_FOR_EACH_THEORY_STATEMENT
526 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
527 if (theory::TheoryTraits<THEORY>::hasGetNextDecisionRequest && d_logicInfo.isTheoryEnabled(THEORY)) { \
528 Node n = theoryOf(THEORY)->getNextDecisionRequest(); \
534 // Request decision from each theory using the statement above
535 CVC4_FOR_EACH_THEORY
;
540 bool TheoryEngine::properConflict(TNode conflict
) const {
542 if (conflict
.getKind() == kind::AND
) {
543 for (unsigned i
= 0; i
< conflict
.getNumChildren(); ++ i
) {
544 if (! getPropEngine()->hasValue(conflict
[i
], value
)) {
545 Debug("properConflict") << "Bad conflict is due to unassigned atom: "
546 << conflict
[i
] << endl
;
550 Debug("properConflict") << "Bad conflict is due to false atom: "
551 << conflict
[i
] << endl
;
554 if (conflict
[i
] != Rewriter::rewrite(conflict
[i
])) {
555 Debug("properConflict") << "Bad conflict is due to atom not in normal form: "
556 << conflict
[i
] << " vs " << Rewriter::rewrite(conflict
[i
]) << endl
;
561 if (! getPropEngine()->hasValue(conflict
, value
)) {
562 Debug("properConflict") << "Bad conflict is due to unassigned atom: "
567 Debug("properConflict") << "Bad conflict is due to false atom: "
571 if (conflict
!= Rewriter::rewrite(conflict
)) {
572 Debug("properConflict") << "Bad conflict is due to atom not in normal form: "
573 << conflict
<< " vs " << Rewriter::rewrite(conflict
) << endl
;
580 bool TheoryEngine::properPropagation(TNode lit
) const {
581 if(!getPropEngine()->isSatLiteral(lit
)) {
585 return !getPropEngine()->hasValue(lit
, b
);
588 bool TheoryEngine::properExplanation(TNode node
, TNode expl
) const {
589 // Explanation must be either a conjunction of true literals that have true SAT values already
590 // or a singled literal that has a true SAT value already.
591 if (expl
.getKind() == kind::AND
) {
592 for (unsigned i
= 0; i
< expl
.getNumChildren(); ++ i
) {
594 if (!d_propEngine
->hasValue(expl
[i
], value
) || !value
) {
600 return d_propEngine
->hasValue(expl
, value
) && value
;
605 void TheoryEngine::collectModelInfo( theory::TheoryModel
* m
, bool fullModel
){
606 //have shared term engine collectModelInfo
607 // d_sharedTerms.collectModelInfo( m, fullModel );
608 // Consult each active theory to get all relevant information
609 // concerning the model.
610 for(TheoryId theoryId
= theory::THEORY_FIRST
; theoryId
< theory::THEORY_LAST
; ++theoryId
) {
611 if(d_logicInfo
.isTheoryEnabled(theoryId
)) {
612 Trace("model-builder") << " CollectModelInfo on theory: " << theoryId
<< endl
;
613 d_theoryTable
[theoryId
]->collectModelInfo( m
, fullModel
);
616 // Get the Boolean variables
617 vector
<TNode
> boolVars
;
618 d_propEngine
->getBooleanVariables(boolVars
);
619 vector
<TNode
>::iterator it
, iend
= boolVars
.end();
620 bool hasValue
, value
;
621 for (it
= boolVars
.begin(); it
!= iend
; ++it
) {
623 hasValue
= d_propEngine
->hasValue(var
, value
);
624 // TODO: Assert that hasValue is true?
628 Trace("model-builder-assertions") << "(assert" << (value
? " " : " (not ") << var
<< (value
? ");" : "));") << endl
;
629 m
->assertPredicate(var
, value
);
634 TheoryModel
* TheoryEngine::getModel() {
635 Debug("model") << "TheoryEngine::getModel()" << endl
;
636 if( d_logicInfo
.isQuantified() ) {
637 Debug("model") << "Get model from quantifiers engine." << endl
;
638 return d_quantEngine
->getModel();
640 Debug("model") << "Get default model." << endl
;
645 bool TheoryEngine::presolve() {
646 // Reset the interrupt flag
647 d_interrupted
= false;
650 // Definition of the statement that is to be run by every theory
651 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
652 #undef CVC4_FOR_EACH_THEORY_STATEMENT
654 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
655 if (theory::TheoryTraits<THEORY>::hasPresolve) { \
656 theoryOf(THEORY)->presolve(); \
662 // Presolve for each theory using the statement above
663 CVC4_FOR_EACH_THEORY
;
664 } catch(const theory::Interrupted
&) {
665 Trace("theory") << "TheoryEngine::presolve() => interrupted" << endl
;
667 // return whether we have a conflict
669 }/* TheoryEngine::presolve() */
671 void TheoryEngine::postsolve() {
672 // Reset the interrupt flag
673 d_interrupted
= false;
674 bool CVC4_UNUSED wasInConflict
= d_inConflict
;
677 // Definition of the statement that is to be run by every theory
678 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
679 #undef CVC4_FOR_EACH_THEORY_STATEMENT
681 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
682 if (theory::TheoryTraits<THEORY>::hasPostsolve) { \
683 theoryOf(THEORY)->postsolve(); \
684 Assert(! d_inConflict || wasInConflict, "conflict raised during postsolve()"); \
687 // Postsolve for each theory using the statement above
688 CVC4_FOR_EACH_THEORY
;
689 } catch(const theory::Interrupted
&) {
690 Trace("theory") << "TheoryEngine::postsolve() => interrupted" << endl
;
692 }/* TheoryEngine::postsolve() */
695 void TheoryEngine::notifyRestart() {
696 // Reset the interrupt flag
697 d_interrupted
= false;
699 // Definition of the statement that is to be run by every theory
700 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
701 #undef CVC4_FOR_EACH_THEORY_STATEMENT
703 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
704 if (theory::TheoryTraits<THEORY>::hasNotifyRestart && d_logicInfo.isTheoryEnabled(THEORY)) { \
705 theoryOf(THEORY)->notifyRestart(); \
708 // notify each theory using the statement above
709 CVC4_FOR_EACH_THEORY
;
712 void TheoryEngine::ppStaticLearn(TNode in
, NodeBuilder
<>& learned
) {
713 // Reset the interrupt flag
714 d_interrupted
= false;
716 // Definition of the statement that is to be run by every theory
717 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
718 #undef CVC4_FOR_EACH_THEORY_STATEMENT
720 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
721 if (theory::TheoryTraits<THEORY>::hasPpStaticLearn) { \
722 theoryOf(THEORY)->ppStaticLearn(in, learned); \
725 // static learning for each theory using the statement above
726 CVC4_FOR_EACH_THEORY
;
729 void TheoryEngine::shutdown() {
730 // Set this first; if a Theory shutdown() throws an exception,
731 // at least the destruction of the TheoryEngine won't confound
733 d_hasShutDown
= true;
735 // Shutdown all the theories
736 for(TheoryId theoryId
= theory::THEORY_FIRST
; theoryId
< theory::THEORY_LAST
; ++theoryId
) {
737 if(d_theoryTable
[theoryId
]) {
738 theoryOf(theoryId
)->shutdown();
745 theory::Theory::PPAssertStatus
TheoryEngine::solve(TNode literal
, SubstitutionMap
& substitutionOut
) {
746 // Reset the interrupt flag
747 d_interrupted
= false;
749 TNode atom
= literal
.getKind() == kind::NOT
? literal
[0] : literal
;
750 Trace("theory::solve") << "TheoryEngine::solve(" << literal
<< "): solving with " << theoryOf(atom
)->getId() << endl
;
752 if(! d_logicInfo
.isTheoryEnabled(Theory::theoryOf(atom
)) &&
753 Theory::theoryOf(atom
) != THEORY_SAT_SOLVER
) {
755 ss
<< "The logic was specified as " << d_logicInfo
.getLogicString()
756 << ", which doesn't include " << Theory::theoryOf(atom
)
757 << ", but got a preprocessing-time fact for that theory." << endl
758 << "The fact:" << endl
760 throw LogicException(ss
.str());
763 Theory::PPAssertStatus solveStatus
= theoryOf(atom
)->ppAssert(literal
, substitutionOut
);
764 Trace("theory::solve") << "TheoryEngine::solve(" << literal
<< ") => " << solveStatus
<< endl
;
768 // Recursively traverse a term and call the theory rewriter on its sub-terms
769 Node
TheoryEngine::ppTheoryRewrite(TNode term
) {
770 NodeMap::iterator find
= d_ppCache
.find(term
);
771 if (find
!= d_ppCache
.end()) {
772 return (*find
).second
;
774 unsigned nc
= term
.getNumChildren();
776 return theoryOf(term
)->ppRewrite(term
);
778 Trace("theory-pp") << "ppTheoryRewrite { " << term
<< endl
;
781 if (theoryOf(term
)->ppDontRewriteSubterm(term
)) {
782 newTerm
= Rewriter::rewrite(term
);
784 NodeBuilder
<> newNode(term
.getKind());
785 if (term
.getMetaKind() == kind::metakind::PARAMETERIZED
) {
786 newNode
<< term
.getOperator();
789 for (i
= 0; i
< nc
; ++i
) {
790 newNode
<< ppTheoryRewrite(term
[i
]);
792 newTerm
= Rewriter::rewrite(Node(newNode
));
794 Node newTerm2
= theoryOf(newTerm
)->ppRewrite(newTerm
);
795 if (newTerm
!= newTerm2
) {
796 newTerm
= ppTheoryRewrite(Rewriter::rewrite(newTerm2
));
798 d_ppCache
[term
] = newTerm
;
799 Trace("theory-pp")<< "ppTheoryRewrite returning " << newTerm
<< "}" << endl
;
804 void TheoryEngine::preprocessStart()
810 struct preprocess_stack_element
{
813 preprocess_stack_element(TNode node
)
814 : node(node
), children_added(false) {}
815 };/* struct preprocess_stack_element */
818 Node
TheoryEngine::preprocess(TNode assertion
) {
820 Trace("theory::preprocess") << "TheoryEngine::preprocess(" << assertion
<< ")" << endl
;
822 // Do a topological sort of the subexpressions and substitute them
823 vector
<preprocess_stack_element
> toVisit
;
824 toVisit
.push_back(assertion
);
826 while (!toVisit
.empty())
828 // The current node we are processing
829 preprocess_stack_element
& stackHead
= toVisit
.back();
830 TNode current
= stackHead
.node
;
832 Debug("theory::internal") << "TheoryEngine::preprocess(" << assertion
<< "): processing " << current
<< endl
;
834 // If node already in the cache we're done, pop from the stack
835 NodeMap::iterator find
= d_ppCache
.find(current
);
836 if (find
!= d_ppCache
.end()) {
841 if(! d_logicInfo
.isTheoryEnabled(Theory::theoryOf(current
)) &&
842 Theory::theoryOf(current
) != THEORY_SAT_SOLVER
) {
844 ss
<< "The logic was specified as " << d_logicInfo
.getLogicString()
845 << ", which doesn't include " << Theory::theoryOf(current
)
846 << ", but got a preprocessing-time fact for that theory." << endl
847 << "The fact:" << endl
849 throw LogicException(ss
.str());
852 // If this is an atom, we preprocess its terms with the theory ppRewriter
853 if (Theory::theoryOf(current
) != THEORY_BOOL
) {
854 Node ppRewritten
= ppTheoryRewrite(current
);
855 d_ppCache
[current
] = ppRewritten
;
856 Assert(Rewriter::rewrite(d_ppCache
[current
]) == d_ppCache
[current
]);
860 // Not yet substituted, so process
861 if (stackHead
.children_added
) {
862 // Children have been processed, so substitute
863 NodeBuilder
<> builder(current
.getKind());
864 if (current
.getMetaKind() == kind::metakind::PARAMETERIZED
) {
865 builder
<< current
.getOperator();
867 for (unsigned i
= 0; i
< current
.getNumChildren(); ++ i
) {
868 Assert(d_ppCache
.find(current
[i
]) != d_ppCache
.end());
869 builder
<< d_ppCache
[current
[i
]];
871 // Mark the substitution and continue
872 Node result
= builder
;
873 if (result
!= current
) {
874 result
= Rewriter::rewrite(result
);
876 Debug("theory::internal") << "TheoryEngine::preprocess(" << assertion
<< "): setting " << current
<< " -> " << result
<< endl
;
877 d_ppCache
[current
] = result
;
880 // Mark that we have added the children if any
881 if (current
.getNumChildren() > 0) {
882 stackHead
.children_added
= true;
883 // We need to add the children
884 for(TNode::iterator child_it
= current
.begin(); child_it
!= current
.end(); ++ child_it
) {
885 TNode childNode
= *child_it
;
886 NodeMap::iterator childFind
= d_ppCache
.find(childNode
);
887 if (childFind
== d_ppCache
.end()) {
888 toVisit
.push_back(childNode
);
892 // No children, so we're done
893 Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << assertion
<< "): setting " << current
<< " -> " << current
<< endl
;
894 d_ppCache
[current
] = current
;
900 // Return the substituted version
901 return d_ppCache
[assertion
];
904 bool TheoryEngine::markPropagation(TNode assertion
, TNode originalAssertion
, theory::TheoryId toTheoryId
, theory::TheoryId fromTheoryId
) {
906 // What and where we are asserting
907 NodeTheoryPair
toAssert(assertion
, toTheoryId
, d_propagationMapTimestamp
);
908 // What and where it came from
909 NodeTheoryPair
toExplain(originalAssertion
, fromTheoryId
, d_propagationMapTimestamp
);
911 // See if the theory already got this literal
912 PropagationMap::const_iterator find
= d_propagationMap
.find(toAssert
);
913 if (find
!= d_propagationMap
.end()) {
914 // The theory already knows this
915 Trace("theory::assertToTheory") << "TheoryEngine::markPropagation(): already there" << endl
;
919 Trace("theory::assertToTheory") << "TheoryEngine::markPropagation(): marking [" << d_propagationMapTimestamp
<< "] " << assertion
<< ", " << toTheoryId
<< " from " << originalAssertion
<< ", " << fromTheoryId
<< endl
;
921 // Mark the propagation
922 d_propagationMap
[toAssert
] = toExplain
;
923 d_propagationMapTimestamp
= d_propagationMapTimestamp
+ 1;
929 void TheoryEngine::assertToTheory(TNode assertion
, TNode originalAssertion
, theory::TheoryId toTheoryId
, theory::TheoryId fromTheoryId
) {
931 Trace("theory::assertToTheory") << "TheoryEngine::assertToTheory(" << assertion
<< ", " << toTheoryId
<< ", " << fromTheoryId
<< ")" << endl
;
933 Assert(toTheoryId
!= fromTheoryId
);
934 if(! d_logicInfo
.isTheoryEnabled(toTheoryId
) &&
935 toTheoryId
!= THEORY_SAT_SOLVER
) {
937 ss
<< "The logic was specified as " << d_logicInfo
.getLogicString()
938 << ", which doesn't include " << toTheoryId
939 << ", but got an asserted fact to that theory." << endl
940 << "The fact:" << endl
942 throw LogicException(ss
.str());
949 // If sharing is disabled, things are easy
950 if (!d_logicInfo
.isSharingEnabled()) {
951 Assert(assertion
== originalAssertion
);
952 if (fromTheoryId
== THEORY_SAT_SOLVER
) {
953 // Send to the apropriate theory
954 theory::Theory
* toTheory
= theoryOf(toTheoryId
);
955 // We assert it, and we know it's preregistereed
956 toTheory
->assertFact(assertion
, true);
957 // Mark that we have more information
958 d_factsAsserted
= true;
960 Assert(toTheoryId
== THEORY_SAT_SOLVER
);
961 // Check for propositional conflict
963 if (d_propEngine
->hasValue(assertion
, value
)) {
965 Trace("theory::propagate") << "TheoryEngine::assertToTheory(" << assertion
<< ", " << toTheoryId
<< ", " << fromTheoryId
<< "): conflict (no sharing)" << endl
;
971 d_propagatedLiterals
.push_back(assertion
);
976 // Polarity of the assertion
977 bool polarity
= assertion
.getKind() != kind::NOT
;
979 // Atom of the assertion
980 TNode atom
= polarity
? assertion
: assertion
[0];
982 // If sending to the shared terms database, it's also simple
983 if (toTheoryId
== THEORY_BUILTIN
) {
984 Assert(atom
.getKind() == kind::EQUAL
, "atom should be an EQUALity, not `%s'", atom
.toString().c_str());
985 if (markPropagation(assertion
, originalAssertion
, toTheoryId
, fromTheoryId
)) {
986 d_sharedTerms
.assertEquality(atom
, polarity
, assertion
);
991 // Things from the SAT solver are already normalized, so they go
992 // directly to the apropriate theory
993 if (fromTheoryId
== THEORY_SAT_SOLVER
) {
994 // We know that this is normalized, so just send it off to the theory
995 if (markPropagation(assertion
, originalAssertion
, toTheoryId
, fromTheoryId
)) {
996 // Is it preregistered
997 bool preregistered
= d_propEngine
->isSatLiteral(assertion
) && Theory::theoryOf(assertion
) == toTheoryId
;
999 theoryOf(toTheoryId
)->assertFact(assertion
, preregistered
);
1000 // Mark that we have more information
1001 d_factsAsserted
= true;
1006 // Propagations to the SAT solver are just enqueued for pickup by
1007 // the SAT solver later
1008 if (toTheoryId
== THEORY_SAT_SOLVER
) {
1009 if (markPropagation(assertion
, originalAssertion
, toTheoryId
, fromTheoryId
)) {
1010 // Enqueue for propagation to the SAT solver
1011 d_propagatedLiterals
.push_back(assertion
);
1012 // Check for propositional conflicts
1014 if (d_propEngine
->hasValue(assertion
, value
) && !value
) {
1015 Trace("theory::propagate") << "TheoryEngine::assertToTheory(" << assertion
<< ", " << toTheoryId
<< ", " << fromTheoryId
<< "): conflict (sharing)" << endl
;
1016 d_inConflict
= true;
1022 Assert(atom
.getKind() == kind::EQUAL
);
1025 Node normalizedLiteral
= Rewriter::rewrite(assertion
);
1027 // See if it rewrites false directly -> conflict
1028 if (normalizedLiteral
.isConst()) {
1029 if (!normalizedLiteral
.getConst
<bool>()) {
1030 // Mark the propagation for explanations
1031 if (markPropagation(normalizedLiteral
, originalAssertion
, toTheoryId
, fromTheoryId
)) {
1032 // Get the explanation (conflict will figure out where it came from)
1033 conflict(normalizedLiteral
, toTheoryId
);
1041 // Try and assert (note that we assert the non-normalized one)
1042 if (markPropagation(assertion
, originalAssertion
, toTheoryId
, fromTheoryId
)) {
1043 // Check if has been pre-registered with the theory
1044 bool preregistered
= d_propEngine
->isSatLiteral(assertion
) && Theory::theoryOf(assertion
) == toTheoryId
;
1046 theoryOf(toTheoryId
)->assertFact(assertion
, preregistered
);
1047 d_factsAsserted
= true;
1053 void TheoryEngine::assertFact(TNode literal
)
1055 Trace("theory") << "TheoryEngine::assertFact(" << literal
<< ")" << endl
;
1057 d_propEngine
->checkTime();
1059 // If we're in conflict, nothing to do
1065 bool polarity
= literal
.getKind() != kind::NOT
;
1066 TNode atom
= polarity
? literal
: literal
[0];
1068 if (d_logicInfo
.isSharingEnabled()) {
1070 // If any shared terms, it's time to do sharing work
1071 if (d_sharedTerms
.hasSharedTerms(atom
)) {
1072 // Notify the theories the shared terms
1073 SharedTermsDatabase::shared_terms_iterator it
= d_sharedTerms
.begin(atom
);
1074 SharedTermsDatabase::shared_terms_iterator it_end
= d_sharedTerms
.end(atom
);
1075 for (; it
!= it_end
; ++ it
) {
1077 Theory::Set theories
= d_sharedTerms
.getTheoriesToNotify(atom
, term
);
1078 for (TheoryId id
= THEORY_FIRST
; id
!= THEORY_LAST
; ++ id
) {
1079 if (Theory::setContains(id
, theories
)) {
1080 theoryOf(id
)->addSharedTermInternal(term
);
1083 d_sharedTerms
.markNotified(term
, theories
);
1087 // If it's an equality, assert it to the shared term manager, even though the terms are not
1088 // yet shared. As the terms become shared later, the shared terms manager will then add them
1089 // to the assert the equality to the interested theories
1090 if (atom
.getKind() == kind::EQUAL
) {
1091 // Assert it to the the owning theory
1092 assertToTheory(literal
, literal
, /* to */ Theory::theoryOf(atom
), /* from */ THEORY_SAT_SOLVER
);
1093 // Shared terms manager will assert to interested theories directly, as the terms become shared
1094 assertToTheory(literal
, literal
, /* to */ THEORY_BUILTIN
, /* from */ THEORY_SAT_SOLVER
);
1096 // Now, let's check for any atom triggers from lemmas
1097 AtomRequests::atom_iterator it
= d_atomRequests
.getAtomIterator(atom
);
1098 while (!it
.done()) {
1099 const AtomRequests::Request
& request
= it
.get();
1100 Node toAssert
= polarity
? (Node
) request
.atom
: request
.atom
.notNode();
1101 Debug("theory::atoms") << "TheoryEngine::assertFact(" << literal
<< "): sending requested " << toAssert
<< endl
;
1102 assertToTheory(toAssert
, literal
, request
.toTheory
, THEORY_SAT_SOLVER
);
1107 // Not an equality, just assert to the appropriate theory
1108 assertToTheory(literal
, literal
, /* to */ Theory::theoryOf(atom
), /* from */ THEORY_SAT_SOLVER
);
1111 // Assert the fact to the appropriate theory directly
1112 assertToTheory(literal
, literal
, /* to */ Theory::theoryOf(atom
), /* from */ THEORY_SAT_SOLVER
);
1116 bool TheoryEngine::propagate(TNode literal
, theory::TheoryId theory
) {
1118 Debug("theory::propagate") << "TheoryEngine::propagate(" << literal
<< ", " << theory
<< ")" << endl
;
1120 d_propEngine
->checkTime();
1122 if(Dump
.isOn("t-propagations")) {
1123 Dump("t-propagations") << CommentCommand("negation of theory propagation: expect valid")
1124 << QueryCommand(literal
.toExpr());
1126 if(Dump
.isOn("missed-t-propagations")) {
1127 d_hasPropagated
.insert(literal
);
1131 bool polarity
= literal
.getKind() != kind::NOT
;
1132 TNode atom
= polarity
? literal
: literal
[0];
1134 if (d_logicInfo
.isSharingEnabled() && atom
.getKind() == kind::EQUAL
) {
1135 if (d_propEngine
->isSatLiteral(literal
)) {
1136 // We propagate SAT literals to SAT
1137 assertToTheory(literal
, literal
, /* to */ THEORY_SAT_SOLVER
, /* from */ theory
);
1139 if (theory
!= THEORY_BUILTIN
) {
1140 // Assert to the shared terms database
1141 assertToTheory(literal
, literal
, /* to */ THEORY_BUILTIN
, /* from */ theory
);
1144 // Just send off to the SAT solver
1145 Assert(d_propEngine
->isSatLiteral(literal
));
1146 assertToTheory(literal
, literal
, /* to */ THEORY_SAT_SOLVER
, /* from */ theory
);
1149 return !d_inConflict
;
1153 theory::EqualityStatus
TheoryEngine::getEqualityStatus(TNode a
, TNode b
) {
1154 Assert(a
.getType().isComparableTo(b
.getType()));
1155 if (d_sharedTerms
.isShared(a
) && d_sharedTerms
.isShared(b
)) {
1156 if (d_sharedTerms
.areEqual(a
,b
)) {
1157 return EQUALITY_TRUE_AND_PROPAGATED
;
1159 else if (d_sharedTerms
.areDisequal(a
,b
)) {
1160 return EQUALITY_FALSE_AND_PROPAGATED
;
1163 return theoryOf(Theory::theoryOf(a
.getType()))->getEqualityStatus(a
, b
);
1166 Node
TheoryEngine::getModelValue(TNode var
) {
1167 Assert(d_sharedTerms
.isShared(var
));
1168 return theoryOf(Theory::theoryOf(var
.getType()))->getModelValue(var
);
1171 static Node
mkExplanation(const std::vector
<NodeTheoryPair
>& explanation
) {
1173 std::set
<TNode
> all
;
1174 for (unsigned i
= 0; i
< explanation
.size(); ++ i
) {
1175 Assert(explanation
[i
].theory
== THEORY_SAT_SOLVER
);
1176 all
.insert(explanation
[i
].node
);
1179 if (all
.size() == 0) {
1180 // Normalize to true
1181 return NodeManager::currentNM()->mkConst
<bool>(true);
1184 if (all
.size() == 1) {
1185 // All the same, or just one
1186 return explanation
[0].node
;
1189 NodeBuilder
<> conjunction(kind::AND
);
1190 std::set
<TNode
>::const_iterator it
= all
.begin();
1191 std::set
<TNode
>::const_iterator it_end
= all
.end();
1192 while (it
!= it_end
) {
1201 Node
TheoryEngine::getExplanation(TNode node
) {
1202 Debug("theory::explain") << "TheoryEngine::getExplanation(" << node
<< "): current propagation index = " << d_propagationMapTimestamp
<< endl
;
1204 bool polarity
= node
.getKind() != kind::NOT
;
1205 TNode atom
= polarity
? node
: node
[0];
1207 // If we're not in shared mode, explanations are simple
1208 if (!d_logicInfo
.isSharingEnabled()) {
1209 Node explanation
= theoryOf(atom
)->explain(node
);
1210 Debug("theory::explain") << "TheoryEngine::getExplanation(" << node
<< ") => " << explanation
<< endl
;
1214 // Initial thing to explain
1215 NodeTheoryPair
toExplain(node
, THEORY_SAT_SOLVER
, d_propagationMapTimestamp
);
1216 Assert(d_propagationMap
.find(toExplain
) != d_propagationMap
.end());
1217 // Create the workplace for explanations
1218 std::vector
<NodeTheoryPair
> explanationVector
;
1219 explanationVector
.push_back(d_propagationMap
[toExplain
]);
1220 // Process the explanation
1221 getExplanation(explanationVector
);
1222 Node explanation
= mkExplanation(explanationVector
);
1224 Debug("theory::explain") << "TheoryEngine::getExplanation(" << node
<< ") => " << explanation
<< endl
;
1229 struct AtomsCollect
{
1231 std::vector
<TNode
> d_atoms
;
1232 std::hash_set
<TNode
, TNodeHashFunction
> d_visited
;
1236 typedef void return_type
;
1238 bool alreadyVisited(TNode current
, TNode parent
) {
1239 // Check if already visited
1240 if (d_visited
.find(current
) != d_visited
.end()) return true;
1241 // Don't visit non-boolean
1242 if (!current
.getType().isBoolean()) return true;
1247 void visit(TNode current
, TNode parent
) {
1248 if (Theory::theoryOf(current
) != theory::THEORY_BOOL
) {
1249 d_atoms
.push_back(current
);
1251 d_visited
.insert(current
);
1254 void start(TNode node
) {}
1255 void done(TNode node
) {}
1257 std::vector
<TNode
> getAtoms() const {
1262 void TheoryEngine::ensureLemmaAtoms(const std::vector
<TNode
>& atoms
, theory::TheoryId atomsTo
) {
1263 for (unsigned i
= 0; i
< atoms
.size(); ++ i
) {
1265 // Non-equality atoms are either owned by theory or they don't make sense
1266 if (atoms
[i
].getKind() != kind::EQUAL
) {
1272 // Simple normalization to not repeat stuff
1273 if (eq
[0] > eq
[1]) {
1274 eq
= eq
[1].eqNode(eq
[0]);
1277 // Rewrite the equality
1278 Node eqNormalized
= Rewriter::rewrite(atoms
[i
]);
1280 Debug("theory::atoms") << "TheoryEngine::ensureLemmaAtoms(): " << eq
<< " with nf " << eqNormalized
<< endl
;
1282 // If the equality is a boolean constant, we send immediately
1283 if (eqNormalized
.isConst()) {
1284 if (eqNormalized
.getConst
<bool>()) {
1285 assertToTheory(eq
, eqNormalized
, /** to */ atomsTo
, /** Sat solver */ theory::THEORY_SAT_SOLVER
);
1287 assertToTheory(eq
.notNode(), eqNormalized
.notNode(), /** to */ atomsTo
, /** Sat solver */ theory::THEORY_SAT_SOLVER
);
1292 Assert(eqNormalized
.getKind() == kind::EQUAL
);
1295 // If the normalization did the just flips, keep the flip
1296 if (eqNormalized
[0] == eq
[1] && eqNormalized
[1] == eq
[0]) {
1300 // Check if the equality is already known by the sat solver
1301 if (d_propEngine
->isSatLiteral(eqNormalized
)) {
1303 if (d_propEngine
->hasValue(eqNormalized
, value
)) {
1305 assertToTheory(eq
, eqNormalized
, atomsTo
, theory::THEORY_SAT_SOLVER
);
1308 assertToTheory(eq
.notNode(), eqNormalized
.notNode(), atomsTo
, theory::THEORY_SAT_SOLVER
);
1314 // If the theory is asking about a different form, or the form is ok but if will go to a different theory
1315 // then we must figure it out
1316 if (eqNormalized
!= eq
|| Theory::theoryOf(eq
) != atomsTo
) {
1317 // If you get eqNormalized, send atoms[i] to atomsTo
1318 d_atomRequests
.add(eqNormalized
, eq
, atomsTo
);
1323 theory::LemmaStatus
TheoryEngine::lemma(TNode node
, bool negated
, bool removable
, bool preprocess
, theory::TheoryId atomsTo
) {
1325 // Do we need to check atoms
1326 if (atomsTo
!= theory::THEORY_LAST
) {
1327 Debug("theory::atoms") << "TheoryEngine::lemma(" << node
<< ", " << atomsTo
<< ")" << endl
;
1328 AtomsCollect collectAtoms
;
1329 NodeVisitor
<AtomsCollect
>::run(collectAtoms
, node
);
1330 ensureLemmaAtoms(collectAtoms
.getAtoms(), atomsTo
);
1333 if(Dump
.isOn("t-lemmas")) {
1338 Dump("t-lemmas") << CommentCommand("theory lemma: expect valid")
1339 << QueryCommand(n
.toExpr());
1342 // Share with other portfolio threads
1343 if(options::lemmaOutputChannel() != NULL
) {
1344 options::lemmaOutputChannel()->notifyNewLemma(node
.toExpr());
1347 // Run theory preprocessing, maybe
1348 Node ppNode
= preprocess
? this->preprocess(node
) : Node(node
);
1351 std::vector
<Node
> additionalLemmas
;
1352 IteSkolemMap iteSkolemMap
;
1353 additionalLemmas
.push_back(ppNode
);
1354 d_iteRemover
.run(additionalLemmas
, iteSkolemMap
);
1355 additionalLemmas
[0] = theory::Rewriter::rewrite(additionalLemmas
[0]);
1357 if(Debug
.isOn("lemma-ites")) {
1358 Debug("lemma-ites") << "removed ITEs from lemma: " << ppNode
<< endl
;
1359 Debug("lemma-ites") << " + now have the following "
1360 << additionalLemmas
.size() << " lemma(s):" << endl
;
1361 for(std::vector
<Node
>::const_iterator i
= additionalLemmas
.begin();
1362 i
!= additionalLemmas
.end();
1364 Debug("lemma-ites") << " + " << *i
<< endl
;
1366 Debug("lemma-ites") << endl
;
1369 // assert to prop engine
1370 d_propEngine
->assertLemma(additionalLemmas
[0], negated
, removable
);
1371 for (unsigned i
= 1; i
< additionalLemmas
.size(); ++ i
) {
1372 additionalLemmas
[i
] = theory::Rewriter::rewrite(additionalLemmas
[i
]);
1373 d_propEngine
->assertLemma(additionalLemmas
[i
], false, removable
);
1376 // WARNING: Below this point don't assume additionalLemmas[0] to be not negated.
1377 // WARNING: Below this point don't assume additionalLemmas[0] to be not negated.
1379 // Can't we just get rid of passing around this 'negated' stuff?
1380 // Is it that hard for the propEngine to figure that out itself?
1381 // (I like the use of triple negation <evil laugh>.) --K
1382 additionalLemmas
[0] = additionalLemmas
[0].notNode();
1385 // WARNING: Below this point don't assume additionalLemmas[0] to be not negated.
1386 // WARNING: Below this point don't assume additionalLemmas[0] to be not negated.
1388 // assert to decision engine
1390 d_decisionEngine
->addAssertions(additionalLemmas
, 1, iteSkolemMap
);
1393 // Mark that we added some lemmas
1394 d_lemmasAdded
= true;
1396 // Lemma analysis isn't online yet; this lemma may only live for this
1398 return theory::LemmaStatus(additionalLemmas
[0], d_userContext
->getLevel());
1401 void TheoryEngine::conflict(TNode conflict
, TheoryId theoryId
) {
1403 Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict
<< ", " << theoryId
<< ")" << endl
;
1405 // Mark that we are in conflict
1406 d_inConflict
= true;
1408 if(Dump
.isOn("t-conflicts")) {
1409 Dump("t-conflicts") << CommentCommand("theory conflict: expect unsat")
1410 << CheckSatCommand(conflict
.toExpr());
1413 // In the multiple-theories case, we need to reconstruct the conflict
1414 if (d_logicInfo
.isSharingEnabled()) {
1415 // Create the workplace for explanations
1416 std::vector
<NodeTheoryPair
> explanationVector
;
1417 explanationVector
.push_back(NodeTheoryPair(conflict
, theoryId
, d_propagationMapTimestamp
));
1418 // Process the explanation
1419 getExplanation(explanationVector
);
1420 Node fullConflict
= mkExplanation(explanationVector
);
1421 Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict
<< ", " << theoryId
<< "): full = " << fullConflict
<< endl
;
1422 Assert(properConflict(fullConflict
));
1423 lemma(fullConflict
, true, true, false, THEORY_LAST
);
1425 // When only one theory, the conflict should need no processing
1426 Assert(properConflict(conflict
));
1427 lemma(conflict
, true, true, false, THEORY_LAST
);
1431 void TheoryEngine::ppBvToBool(const std::vector
<Node
>& assertions
, std::vector
<Node
>& new_assertions
) {
1432 d_bvToBoolPreprocessor
.liftBoolToBV(assertions
, new_assertions
);
1435 Node
TheoryEngine::ppSimpITE(TNode assertion
)
1437 if(!d_iteRemover
.containsTermITE(assertion
)){
1441 Node result
= d_iteUtilities
->simpITE(assertion
);
1442 Node res_rewritten
= Rewriter::rewrite(result
);
1444 if(options::simplifyWithCareEnabled()){
1445 Chat() << "starting simplifyWithCare()" << endl
;
1446 Node postSimpWithCare
= d_iteUtilities
->simplifyWithCare(res_rewritten
);
1447 Chat() << "ending simplifyWithCare()"
1448 << " post simplifyWithCare()" << postSimpWithCare
.getId() << endl
;
1449 result
= Rewriter::rewrite(postSimpWithCare
);
1451 result
= res_rewritten
;
1458 bool TheoryEngine::donePPSimpITE(std::vector
<Node
>& assertions
){
1460 if(d_iteUtilities
->simpIteDidALotOfWorkHeuristic()){
1461 if(options::compressItes()){
1462 result
= d_iteUtilities
->compress(assertions
);
1466 // if false, don't bother to reclaim memory here.
1467 NodeManager
* nm
= NodeManager::currentNM();
1468 if(nm
->poolSize() >= options::zombieHuntThreshold()){
1469 Chat() << "..ite simplifier did quite a bit of work.. " << nm
->poolSize() << endl
;
1470 Chat() << "....node manager contains " << nm
->poolSize() << " nodes before cleanup" << endl
;
1471 d_iteUtilities
->clear();
1472 Rewriter::garbageCollect();
1473 d_iteRemover
.garbageCollect();
1474 nm
->reclaimZombiesUntil(options::zombieHuntThreshold());
1475 Chat() << "....node manager contains " << nm
->poolSize() << " nodes after cleanup" << endl
;
1482 void TheoryEngine::getExplanation(std::vector
<NodeTheoryPair
>& explanationVector
)
1484 Assert(explanationVector
.size() > 0);
1486 unsigned i
= 0; // Index of the current literal we are processing
1487 unsigned j
= 0; // Index of the last literal we are keeping
1489 while (i
< explanationVector
.size()) {
1491 // Get the current literal to explain
1492 NodeTheoryPair toExplain
= explanationVector
[i
];
1494 Debug("theory::explain") << "TheoryEngine::explain(): processing [" << toExplain
.timestamp
<< "] " << toExplain
.node
<< " sent from " << toExplain
.theory
<< endl
;
1496 // If a true constant or a negation of a false constant we can ignore it
1497 if (toExplain
.node
.isConst() && toExplain
.node
.getConst
<bool>()) {
1501 if (toExplain
.node
.getKind() == kind::NOT
&& toExplain
.node
[0].isConst() && !toExplain
.node
[0].getConst
<bool>()) {
1506 // If from the SAT solver, keep it
1507 if (toExplain
.theory
== THEORY_SAT_SOLVER
) {
1508 explanationVector
[j
++] = explanationVector
[i
++];
1512 // If an and, expand it
1513 if (toExplain
.node
.getKind() == kind::AND
) {
1514 Debug("theory::explain") << "TheoryEngine::explain(): expanding " << toExplain
.node
<< " got from " << toExplain
.theory
<< endl
;
1515 for (unsigned k
= 0; k
< toExplain
.node
.getNumChildren(); ++ k
) {
1516 NodeTheoryPair
newExplain(toExplain
.node
[k
], toExplain
.theory
, toExplain
.timestamp
);
1517 explanationVector
.push_back(newExplain
);
1523 // See if it was sent to the theory by another theory
1524 PropagationMap::const_iterator find
= d_propagationMap
.find(toExplain
);
1525 if (find
!= d_propagationMap
.end()) {
1526 // There is some propagation, check if its a timely one
1527 if ((*find
).second
.timestamp
< toExplain
.timestamp
) {
1528 explanationVector
.push_back((*find
).second
);
1534 // It was produced by the theory, so ask for an explanation
1536 if (toExplain
.theory
== THEORY_BUILTIN
) {
1537 explanation
= d_sharedTerms
.explain(toExplain
.node
);
1539 explanation
= theoryOf(toExplain
.theory
)->explain(toExplain
.node
);
1541 Debug("theory::explain") << "TheoryEngine::explain(): got explanation " << explanation
<< " got from " << toExplain
.theory
<< endl
;
1542 Assert(explanation
!= toExplain
.node
, "wasn't sent to you, so why are you explaining it trivially");
1543 // Mark the explanation
1544 NodeTheoryPair
newExplain(explanation
, toExplain
.theory
, toExplain
.timestamp
);
1545 explanationVector
.push_back(newExplain
);
1549 // Keep only the relevant literals
1550 explanationVector
.resize(j
);
1554 void TheoryEngine::ppUnconstrainedSimp(vector
<Node
>& assertions
)
1556 d_unconstrainedSimp
->processAssertions(assertions
);
1560 void TheoryEngine::setUserAttribute(const std::string
& attr
, Node n
) {
1561 Trace("te-attr") << "set user attribute " << attr
<< " " << n
<< endl
;
1562 if( d_attr_handle
.find( attr
)!=d_attr_handle
.end() ){
1563 for( size_t i
=0; i
<d_attr_handle
[attr
].size(); i
++ ){
1564 d_attr_handle
[attr
][i
]->setUserAttribute(attr
, n
);
1567 //unhandled exception?
1571 void TheoryEngine::handleUserAttribute(const char* attr
, Theory
* t
) {
1572 Trace("te-attr") << "Handle user attribute " << attr
<< " " << t
<< endl
;
1573 std::string
str( attr
);
1574 d_attr_handle
[ str
].push_back( t
);
1577 void TheoryEngine::checkTheoryAssertionsWithModel() {
1578 for(TheoryId theoryId
= THEORY_FIRST
; theoryId
< THEORY_LAST
; ++theoryId
) {
1579 if(theoryId
!= THEORY_REWRITERULES
) {
1580 Theory
* theory
= d_theoryTable
[theoryId
];
1581 if(theory
&& d_logicInfo
.isTheoryEnabled(theoryId
)) {
1582 for(context::CDList
<Assertion
>::const_iterator it
= theory
->facts_begin(),
1583 it_end
= theory
->facts_end();
1586 Node assertion
= (*it
).assertion
;
1587 Node val
= getModel()->getValue(assertion
);
1590 ss
<< theoryId
<< " has an asserted fact that the model doesn't satisfy." << endl
1591 << "The fact: " << assertion
<< endl
1592 << "Model value: " << val
<< endl
;
1593 InternalError(ss
.str());