1 /********************* */
2 /*! \file theory_engine.cpp
4 ** Top contributors (to current version):
5 ** Dejan Jovanovic, Morgan Deters, Guy Katz
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
8 ** in the top-level source directory) and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
12 ** \brief The theory engine
17 #include "theory/theory_engine.h"
22 #include "decision/decision_engine.h"
23 #include "expr/attribute.h"
24 #include "expr/node.h"
25 #include "expr/node_builder.h"
26 #include "options/bv_options.h"
27 #include "options/options.h"
28 #include "options/proof_options.h"
29 #include "options/quantifiers_options.h"
30 #include "proof/cnf_proof.h"
31 #include "proof/lemma_proof.h"
32 #include "proof/proof_manager.h"
33 #include "proof/theory_proof.h"
34 #include "smt/term_formula_removal.h"
35 #include "smt/logic_exception.h"
36 #include "smt_util/lemma_output_channel.h"
37 #include "smt_util/node_visitor.h"
38 #include "theory/arith/arith_ite_utils.h"
39 #include "theory/bv/theory_bv_utils.h"
40 #include "theory/care_graph.h"
41 #include "theory/ite_utilities.h"
42 #include "theory/quantifiers/first_order_model.h"
43 #include "theory/quantifiers/fmf/model_engine.h"
44 #include "theory/quantifiers/theory_quantifiers.h"
45 #include "theory/quantifiers_engine.h"
46 #include "theory/rewriter.h"
47 #include "theory/theory.h"
48 #include "theory/theory_model.h"
49 #include "theory/theory_traits.h"
50 #include "theory/uf/equality_engine.h"
51 #include "theory/unconstrained_simplifier.h"
52 #include "util/resource_manager.h"
56 using namespace CVC4::theory
;
60 inline void flattenAnd(Node n
, std::vector
<TNode
>& out
){
61 Assert(n
.getKind() == kind::AND
);
62 for(Node::iterator i
=n
.begin(), i_end
=n
.end(); i
!= i_end
; ++i
){
64 if(curr
.getKind() == kind::AND
){
65 flattenAnd(curr
, out
);
72 inline Node
flattenAnd(Node n
){
73 std::vector
<TNode
> out
;
75 return NodeManager::currentNM()->mkNode(kind::AND
, out
);
78 theory::LemmaStatus
TheoryEngine::EngineOutputChannel::lemma(TNode lemma
,
83 Debug("theory::lemma") << "EngineOutputChannel<" << d_theory
<< ">::lemma("
85 << ", preprocess = " << preprocess
<< std::endl
;
86 ++d_statistics
.lemmas
;
87 d_engine
->d_outputChannelUsed
= true;
89 PROOF({ registerLemmaRecipe(lemma
, lemma
, preprocess
, d_theory
); });
91 theory::LemmaStatus result
=
92 d_engine
->lemma(lemma
, rule
, false, removable
, preprocess
,
93 sendAtoms
? d_theory
: theory::THEORY_LAST
);
97 void TheoryEngine::EngineOutputChannel::registerLemmaRecipe(Node lemma
, Node originalLemma
, bool preprocess
, theory::TheoryId theoryId
) {
98 // During CNF conversion, conjunctions will be broken down into
99 // multiple lemmas. In order for the recipes to match, we have to do
101 NodeManager
* nm
= NodeManager::currentNM();
104 lemma
= d_engine
->preprocess(lemma
);
106 bool negated
= (lemma
.getKind() == kind::NOT
);
107 Node nnLemma
= negated
? lemma
[0] : lemma
;
109 switch (nnLemma
.getKind()) {
113 for (unsigned i
= 0; i
< nnLemma
.getNumChildren(); ++i
)
114 registerLemmaRecipe(nnLemma
[i
], originalLemma
, false, theoryId
);
116 NodeBuilder
<> builder(kind::OR
);
117 for (unsigned i
= 0; i
< nnLemma
.getNumChildren(); ++i
)
118 builder
<< nnLemma
[i
].negate();
120 Node disjunction
= (builder
.getNumChildren() == 1) ? builder
[0] : builder
;
121 registerLemmaRecipe(disjunction
, originalLemma
, false, theoryId
);
126 if( nnLemma
[0].getType().isBoolean() ){
128 registerLemmaRecipe(nm
->mkNode(kind::OR
, nnLemma
[0], nnLemma
[1].negate()), originalLemma
, false, theoryId
);
129 registerLemmaRecipe(nm
->mkNode(kind::OR
, nnLemma
[0].negate(), nnLemma
[1]), originalLemma
, false, theoryId
);
131 registerLemmaRecipe(nm
->mkNode(kind::OR
, nnLemma
[0], nnLemma
[1]), originalLemma
, false, theoryId
);
132 registerLemmaRecipe(nm
->mkNode(kind::OR
, nnLemma
[0].negate(), nnLemma
[1].negate()), originalLemma
, false, theoryId
);
139 registerLemmaRecipe(nm
->mkNode(kind::OR
, nnLemma
[0].negate(), nnLemma
[1]), originalLemma
, false, theoryId
);
140 registerLemmaRecipe(nm
->mkNode(kind::OR
, nnLemma
[0], nnLemma
[2]), originalLemma
, false, theoryId
);
142 registerLemmaRecipe(nm
->mkNode(kind::OR
, nnLemma
[0].negate(), nnLemma
[1].negate()), originalLemma
, false, theoryId
);
143 registerLemmaRecipe(nm
->mkNode(kind::OR
, nnLemma
[0], nnLemma
[2].negate()), originalLemma
, false, theoryId
);
151 // Theory lemmas have one step that proves the empty clause
152 LemmaProofRecipe proofRecipe
;
154 LemmaProofRecipe::ProofStep
proofStep(theoryId
, emptyNode
);
156 // Remember the original lemma, so we can report this later when asked to
157 proofRecipe
.setOriginalLemma(originalLemma
);
159 // Record the assertions and rewrites
161 if (lemma
.getKind() == kind::OR
) {
162 for (unsigned i
= 0; i
< lemma
.getNumChildren(); ++i
) {
163 rewritten
= theory::Rewriter::rewrite(lemma
[i
]);
164 if (rewritten
!= lemma
[i
]) {
165 proofRecipe
.addRewriteRule(lemma
[i
].negate(), rewritten
.negate());
167 proofStep
.addAssertion(lemma
[i
]);
168 proofRecipe
.addBaseAssertion(rewritten
);
171 rewritten
= theory::Rewriter::rewrite(lemma
);
172 if (rewritten
!= lemma
) {
173 proofRecipe
.addRewriteRule(lemma
.negate(), rewritten
.negate());
175 proofStep
.addAssertion(lemma
);
176 proofRecipe
.addBaseAssertion(rewritten
);
178 proofRecipe
.addStep(proofStep
);
179 ProofManager::getCnfProof()->setProofRecipe(&proofRecipe
);
182 theory::LemmaStatus
TheoryEngine::EngineOutputChannel::splitLemma(
183 TNode lemma
, bool removable
) {
184 Debug("theory::lemma") << "EngineOutputChannel<" << d_theory
<< ">::lemma("
185 << lemma
<< ")" << std::endl
;
186 ++d_statistics
.lemmas
;
187 d_engine
->d_outputChannelUsed
= true;
189 Debug("pf::explain") << "TheoryEngine::EngineOutputChannel::splitLemma( "
190 << lemma
<< " )" << std::endl
;
191 theory::LemmaStatus result
=
192 d_engine
->lemma(lemma
, RULE_SPLIT
, false, removable
, false, d_theory
);
196 bool TheoryEngine::EngineOutputChannel::propagate(TNode literal
) {
197 Debug("theory::propagate") << "EngineOutputChannel<" << d_theory
198 << ">::propagate(" << literal
<< ")" << std::endl
;
199 ++d_statistics
.propagations
;
200 d_engine
->d_outputChannelUsed
= true;
201 return d_engine
->propagate(literal
, d_theory
);
204 void TheoryEngine::EngineOutputChannel::conflict(TNode conflictNode
,
205 std::unique_ptr
<Proof
> proof
)
207 Trace("theory::conflict")
208 << "EngineOutputChannel<" << d_theory
<< ">::conflict(" << conflictNode
210 Assert(!proof
); // Theory shouldn't be producing proofs yet
211 ++d_statistics
.conflicts
;
212 d_engine
->d_outputChannelUsed
= true;
213 d_engine
->conflict(conflictNode
, d_theory
);
216 void TheoryEngine::finishInit() {
218 //initialize the quantifiers engine, master equality engine, model, model builder
219 if( d_logicInfo
.isQuantified() ) {
220 // initialize the quantifiers engine
221 d_quantEngine
= new QuantifiersEngine(d_context
, d_userContext
, this);
222 Assert(d_masterEqualityEngine
== 0);
223 d_masterEqualityEngine
= new eq::EqualityEngine(d_masterEENotify
,getSatContext(), "theory::master", false);
225 for(TheoryId theoryId
= theory::THEORY_FIRST
; theoryId
!= theory::THEORY_LAST
; ++ theoryId
) {
226 if (d_theoryTable
[theoryId
]) {
227 d_theoryTable
[theoryId
]->setQuantifiersEngine(d_quantEngine
);
228 d_theoryTable
[theoryId
]->setMasterEqualityEngine(d_masterEqualityEngine
);
232 d_curr_model_builder
= d_quantEngine
->getModelBuilder();
233 d_curr_model
= d_quantEngine
->getModel();
235 d_curr_model
= new theory::TheoryModel(d_userContext
, "DefaultModel", true);
236 d_aloc_curr_model
= true;
238 //make the default builder, e.g. in the case that the quantifiers engine does not have a model builder
239 if( d_curr_model_builder
==NULL
){
240 d_curr_model_builder
= new theory::TheoryEngineModelBuilder(this);
241 d_aloc_curr_model_builder
= true;
244 for(TheoryId theoryId
= theory::THEORY_FIRST
; theoryId
!= theory::THEORY_LAST
; ++ theoryId
) {
245 if (d_theoryTable
[theoryId
]) {
246 d_theoryTable
[theoryId
]->finishInit();
251 void TheoryEngine::eqNotifyNewClass(TNode t
){
252 if (d_logicInfo
.isQuantified()) {
253 d_quantEngine
->eqNotifyNewClass( t
);
257 void TheoryEngine::eqNotifyPreMerge(TNode t1
, TNode t2
){
258 if (d_logicInfo
.isQuantified()) {
259 d_quantEngine
->eqNotifyPreMerge( t1
, t2
);
263 void TheoryEngine::eqNotifyPostMerge(TNode t1
, TNode t2
){
264 if (d_logicInfo
.isQuantified()) {
265 d_quantEngine
->eqNotifyPostMerge( t1
, t2
);
269 void TheoryEngine::eqNotifyDisequal(TNode t1
, TNode t2
, TNode reason
){
270 if (d_logicInfo
.isQuantified()) {
271 d_quantEngine
->eqNotifyDisequal( t1
, t2
, reason
);
276 TheoryEngine::TheoryEngine(context::Context
* context
,
277 context::UserContext
* userContext
,
278 RemoveTermFormulas
& iteRemover
,
279 const LogicInfo
& logicInfo
,
280 LemmaChannels
* channels
)
281 : d_propEngine(NULL
),
282 d_decisionEngine(NULL
),
284 d_userContext(userContext
),
285 d_logicInfo(logicInfo
),
286 d_sharedTerms(this, context
),
287 d_masterEqualityEngine(NULL
),
288 d_masterEENotify(*this),
291 d_aloc_curr_model(false),
292 d_curr_model_builder(NULL
),
293 d_aloc_curr_model_builder(false),
295 d_possiblePropagations(context
),
296 d_hasPropagated(context
),
297 d_inConflict(context
, false),
298 d_hasShutDown(false),
299 d_incomplete(context
, false),
300 d_propagationMap(context
),
301 d_propagationMapTimestamp(context
, 0),
302 d_propagatedLiterals(context
),
303 d_propagatedLiteralsIndex(context
, 0),
304 d_atomRequests(context
),
305 d_tform_remover(iteRemover
),
306 d_combineTheoriesTime("TheoryEngine::combineTheoriesTime"),
309 d_interrupted(false),
310 d_resourceManager(NodeManager::currentResourceManager()),
311 d_channels(channels
),
312 d_inPreregister(false),
313 d_factsAsserted(context
, false),
314 d_preRegistrationVisitor(this, context
),
315 d_sharedTermsVisitor(d_sharedTerms
),
316 d_unconstrainedSimp(new UnconstrainedSimplifier(context
, logicInfo
)),
317 d_bvToBoolPreprocessor(),
318 d_theoryAlternatives(),
320 d_arithSubstitutionsAdded("theory::arith::zzz::arith::substitutions", 0)
322 for(TheoryId theoryId
= theory::THEORY_FIRST
; theoryId
!= theory::THEORY_LAST
;
325 d_theoryTable
[theoryId
] = NULL
;
326 d_theoryOut
[theoryId
] = NULL
;
329 smtStatisticsRegistry()->registerStat(&d_combineTheoriesTime
);
330 d_true
= NodeManager::currentNM()->mkConst
<bool>(true);
331 d_false
= NodeManager::currentNM()->mkConst
<bool>(false);
334 ProofManager::currentPM()->initTheoryProofEngine();
337 d_iteUtilities
= new ITEUtilities();
339 smtStatisticsRegistry()->registerStat(&d_arithSubstitutionsAdded
);
342 TheoryEngine::~TheoryEngine() {
343 Assert(d_hasShutDown
);
345 for(TheoryId theoryId
= theory::THEORY_FIRST
; theoryId
!= theory::THEORY_LAST
; ++ theoryId
) {
346 if(d_theoryTable
[theoryId
] != NULL
) {
347 delete d_theoryTable
[theoryId
];
348 delete d_theoryOut
[theoryId
];
352 if( d_aloc_curr_model_builder
){
353 delete d_curr_model_builder
;
355 if( d_aloc_curr_model
){
359 delete d_quantEngine
;
361 delete d_masterEqualityEngine
;
363 smtStatisticsRegistry()->unregisterStat(&d_combineTheoriesTime
);
365 delete d_unconstrainedSimp
;
367 delete d_iteUtilities
;
369 smtStatisticsRegistry()->unregisterStat(&d_arithSubstitutionsAdded
);
372 void TheoryEngine::interrupt() { d_interrupted
= true; }
373 void TheoryEngine::preRegister(TNode preprocessed
) {
375 Debug("theory") << "TheoryEngine::preRegister( " << preprocessed
<< ")" << std::endl
;
376 if(Dump
.isOn("missed-t-propagations")) {
377 d_possiblePropagations
.push_back(preprocessed
);
379 d_preregisterQueue
.push(preprocessed
);
381 if (!d_inPreregister
) {
382 // We're in pre-register
383 d_inPreregister
= true;
385 // Process the pre-registration queue
386 while (!d_preregisterQueue
.empty()) {
387 // Get the next atom to pre-register
388 preprocessed
= d_preregisterQueue
.front();
389 d_preregisterQueue
.pop();
391 if (d_logicInfo
.isSharingEnabled() && preprocessed
.getKind() == kind::EQUAL
) {
392 // When sharing is enabled, we propagate from the shared terms manager also
393 d_sharedTerms
.addEqualityToPropagate(preprocessed
);
396 // the atom should not have free variables
397 Debug("theory") << "TheoryEngine::preRegister: " << preprocessed
399 Assert(!preprocessed
.hasFreeVar());
400 // Pre-register the terms in the atom
401 Theory::Set theories
= NodeVisitor
<PreRegisterVisitor
>::run(d_preRegistrationVisitor
, preprocessed
);
402 theories
= Theory::setRemove(THEORY_BOOL
, theories
);
403 // Remove the top theory, if any more that means multiple theories were involved
404 bool multipleTheories
= Theory::setRemove(Theory::theoryOf(preprocessed
), theories
);
406 // These checks don't work with finite model finding, because it
407 // uses Rational constants to represent cardinality constraints,
408 // even though arithmetic isn't actually involved.
409 if(!options::finiteModelFind()) {
410 while((i
= Theory::setPop(theories
)) != THEORY_LAST
) {
411 if(!d_logicInfo
.isTheoryEnabled(i
)) {
412 LogicInfo newLogicInfo
= d_logicInfo
.getUnlockedCopy();
413 newLogicInfo
.enableTheory(i
);
416 ss
<< "The logic was specified as " << d_logicInfo
.getLogicString()
417 << ", which doesn't include " << i
418 << ", but found a term in that theory." << endl
419 << "You might want to extend your logic to "
420 << newLogicInfo
.getLogicString() << endl
;
421 throw LogicException(ss
.str());
425 if (multipleTheories
) {
426 // Collect the shared terms if there are multiple theories
427 NodeVisitor
<SharedTermsVisitor
>::run(d_sharedTermsVisitor
, preprocessed
);
431 // Leaving pre-register
432 d_inPreregister
= false;
436 void TheoryEngine::printAssertions(const char* tag
) {
437 if (Trace
.isOn(tag
)) {
439 for (TheoryId theoryId
= THEORY_FIRST
; theoryId
< THEORY_LAST
; ++theoryId
) {
440 Theory
* theory
= d_theoryTable
[theoryId
];
441 if (theory
&& d_logicInfo
.isTheoryEnabled(theoryId
)) {
442 Trace(tag
) << "--------------------------------------------" << endl
;
443 Trace(tag
) << "Assertions of " << theory
->getId() << ": " << endl
;
444 context::CDList
<Assertion
>::const_iterator it
= theory
->facts_begin(), it_end
= theory
->facts_end();
445 for (unsigned i
= 0; it
!= it_end
; ++ it
, ++i
) {
446 if ((*it
).isPreregistered
) {
447 Trace(tag
) << "[" << i
<< "]: ";
449 Trace(tag
) << "(" << i
<< "): ";
451 Trace(tag
) << (*it
).assertion
<< endl
;
454 if (d_logicInfo
.isSharingEnabled()) {
455 Trace(tag
) << "Shared terms of " << theory
->getId() << ": " << endl
;
456 context::CDList
<TNode
>::const_iterator it
= theory
->shared_terms_begin(), it_end
= theory
->shared_terms_end();
457 for (unsigned i
= 0; it
!= it_end
; ++ it
, ++i
) {
458 Trace(tag
) << "[" << i
<< "]: " << (*it
) << endl
;
466 void TheoryEngine::dumpAssertions(const char* tag
) {
467 if (Dump
.isOn(tag
)) {
468 Dump(tag
) << CommentCommand("Starting completeness check");
469 for (TheoryId theoryId
= THEORY_FIRST
; theoryId
< THEORY_LAST
; ++theoryId
) {
470 Theory
* theory
= d_theoryTable
[theoryId
];
471 if (theory
&& d_logicInfo
.isTheoryEnabled(theoryId
)) {
472 Dump(tag
) << CommentCommand("Completeness check");
473 Dump(tag
) << PushCommand();
475 // Dump the shared terms
476 if (d_logicInfo
.isSharingEnabled()) {
477 Dump(tag
) << CommentCommand("Shared terms");
478 context::CDList
<TNode
>::const_iterator it
= theory
->shared_terms_begin(), it_end
= theory
->shared_terms_end();
479 for (unsigned i
= 0; it
!= it_end
; ++ it
, ++i
) {
482 Dump(tag
) << CommentCommand(ss
.str());
486 // Dump the assertions
487 Dump(tag
) << CommentCommand("Assertions");
488 context::CDList
<Assertion
>::const_iterator it
= theory
->facts_begin(), it_end
= theory
->facts_end();
489 for (; it
!= it_end
; ++ it
) {
491 Node assertionNode
= (*it
).assertion
;
492 // Purify all the terms
494 if ((*it
).isPreregistered
) {
495 Dump(tag
) << CommentCommand("Preregistered");
497 Dump(tag
) << CommentCommand("Shared assertion");
499 Dump(tag
) << AssertCommand(assertionNode
.toExpr());
501 Dump(tag
) << CheckSatCommand();
503 Dump(tag
) << PopCommand();
510 * Check all (currently-active) theories for conflicts.
511 * @param effort the effort level to use
513 void TheoryEngine::check(Theory::Effort effort
) {
516 // Reset the interrupt flag
517 d_interrupted
= false;
519 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
520 #undef CVC4_FOR_EACH_THEORY_STATEMENT
522 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
523 if (theory::TheoryTraits<THEORY>::hasCheck && d_logicInfo.isTheoryEnabled(THEORY)) { \
524 theoryOf(THEORY)->check(effort); \
525 if (d_inConflict) { \
526 Debug("conflict") << THEORY << " in conflict. " << std::endl; \
534 // Mark the output channel unused (if this is FULL_EFFORT, and nothing
535 // is done by the theories, no additional check will be needed)
536 d_outputChannelUsed
= false;
538 // Mark the lemmas flag (no lemmas added)
539 d_lemmasAdded
= false;
541 Debug("theory") << "TheoryEngine::check(" << effort
<< "): d_factsAsserted = " << (d_factsAsserted
? "true" : "false") << endl
;
543 // If in full effort, we have a fake new assertion just to jumpstart the checking
544 if (Theory::fullEffort(effort
)) {
545 d_factsAsserted
= true;
549 while (d_factsAsserted
&& !d_inConflict
&& !d_lemmasAdded
) {
551 Debug("theory") << "TheoryEngine::check(" << effort
<< "): running check" << endl
;
553 Trace("theory::assertions") << endl
;
554 if (Trace
.isOn("theory::assertions")) {
555 printAssertions("theory::assertions");
558 if(Theory::fullEffort(effort
)) {
559 Trace("theory::assertions::fulleffort") << endl
;
560 if (Trace
.isOn("theory::assertions::fulleffort")) {
561 printAssertions("theory::assertions::fulleffort");
565 // Note that we've discharged all the facts
566 d_factsAsserted
= false;
569 CVC4_FOR_EACH_THEORY
;
571 if(Dump
.isOn("missed-t-conflicts")) {
572 Dump("missed-t-conflicts")
573 << CommentCommand("Completeness check for T-conflicts; expect sat")
574 << CheckSatCommand();
577 Debug("theory") << "TheoryEngine::check(" << effort
<< "): running propagation after the initial check" << endl
;
579 // We are still satisfiable, propagate as much as possible
582 // We do combination if all has been processed and we are in fullcheck
583 if (Theory::fullEffort(effort
) && d_logicInfo
.isSharingEnabled() && !d_factsAsserted
&& !d_lemmasAdded
&& !d_inConflict
) {
584 // Do the combination
585 Debug("theory") << "TheoryEngine::check(" << effort
<< "): running combination" << endl
;
587 if(d_logicInfo
.isQuantified()){
588 d_quantEngine
->notifyCombineTheories();
593 // Must consult quantifiers theory for last call to ensure sat, or otherwise add a lemma
594 if( Theory::fullEffort(effort
) && ! d_inConflict
&& ! needCheck() ) {
595 Trace("theory::assertions-model") << endl
;
596 if (Trace
.isOn("theory::assertions-model")) {
597 printAssertions("theory::assertions-model");
599 //checks for theories requiring the model go at last call
600 d_curr_model
->reset();
601 for (TheoryId theoryId
= THEORY_FIRST
; theoryId
< THEORY_LAST
; ++theoryId
) {
602 if( theoryId
!=THEORY_QUANTIFIERS
){
603 Theory
* theory
= d_theoryTable
[theoryId
];
604 if (theory
&& d_logicInfo
.isTheoryEnabled(theoryId
)) {
605 if( theory
->needsCheckLastEffort() ){
606 if( !d_curr_model
->isBuilt() ){
607 if( !d_curr_model_builder
->buildModel(d_curr_model
) ){
611 theory
->check(Theory::EFFORT_LAST_CALL
);
616 if( ! d_inConflict
&& ! needCheck() ){
617 if(d_logicInfo
.isQuantified()) {
618 // quantifiers engine must check at last call effort
619 d_quantEngine
->check(Theory::EFFORT_LAST_CALL
);
622 if (!d_inConflict
&& !needCheck())
624 if (options::produceModels() && !d_curr_model
->isBuilt())
626 // must build model at this point
627 d_curr_model_builder
->buildModel(d_curr_model
);
632 Debug("theory") << "TheoryEngine::check(" << effort
<< "): done, we are " << (d_inConflict
? "unsat" : "sat") << (d_lemmasAdded
? " with new lemmas" : " with no new lemmas");
633 Debug("theory") << ", need check = " << (needCheck() ? "YES" : "NO") << endl
;
635 if( Theory::fullEffort(effort
) && !d_inConflict
&& !needCheck()) {
636 // case where we are about to answer SAT
637 if( d_masterEqualityEngine
!= NULL
){
638 AlwaysAssert(d_masterEqualityEngine
->consistent());
640 if (d_curr_model
->isBuilt())
642 // model construction should always succeed unless lemmas were added
643 AlwaysAssert(d_curr_model
->isBuiltSuccess());
644 if (options::produceModels())
646 // if we are incomplete, there is no guarantee on the model.
647 // thus, we do not check the model here. (related to #1693)
650 d_curr_model_builder
->debugCheckModel(d_curr_model
);
652 // Do post-processing of model from the theories (used for THEORY_SEP
653 // to construct heap model)
654 postProcessModel(d_curr_model
);
658 } catch(const theory::Interrupted
&) {
659 Trace("theory") << "TheoryEngine::check() => interrupted" << endl
;
661 // If fulleffort, check all theories
662 if(Dump
.isOn("theory::fullcheck") && Theory::fullEffort(effort
)) {
663 if (!d_inConflict
&& !needCheck()) {
664 dumpAssertions("theory::fullcheck");
669 void TheoryEngine::combineTheories() {
671 Trace("combineTheories") << "TheoryEngine::combineTheories()" << endl
;
673 TimerStat::CodeTimer
combineTheoriesTimer(d_combineTheoriesTime
);
675 // Care graph we'll be building
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>::isParametric && d_logicInfo.isTheoryEnabled(THEORY)) { \
683 theoryOf(THEORY)->getCareGraph(&careGraph); \
686 // Call on each parametric theory to give us its care graph
687 CVC4_FOR_EACH_THEORY
;
689 Trace("combineTheories") << "TheoryEngine::combineTheories(): care graph size = " << careGraph
.size() << endl
;
691 // Now add splitters for the ones we are interested in
692 CareGraph::const_iterator care_it
= careGraph
.begin();
693 CareGraph::const_iterator care_it_end
= careGraph
.end();
695 for (; care_it
!= care_it_end
; ++ care_it
) {
696 const CarePair
& carePair
= *care_it
;
698 Debug("combineTheories") << "TheoryEngine::combineTheories(): checking " << carePair
.a
<< " = " << carePair
.b
<< " from " << carePair
.theory
<< endl
;
700 Assert(d_sharedTerms
.isShared(carePair
.a
) || carePair
.a
.isConst());
701 Assert(d_sharedTerms
.isShared(carePair
.b
) || carePair
.b
.isConst());
703 // The equality in question (order for no repetition)
704 Node equality
= carePair
.a
.eqNode(carePair
.b
);
705 // EqualityStatus es = getEqualityStatus(carePair.a, carePair.b);
706 // Debug("combineTheories") << "TheoryEngine::combineTheories(): " <<
707 // (es == EQUALITY_TRUE_AND_PROPAGATED ? "EQUALITY_TRUE_AND_PROPAGATED" :
708 // es == EQUALITY_FALSE_AND_PROPAGATED ? "EQUALITY_FALSE_AND_PROPAGATED" :
709 // es == EQUALITY_TRUE ? "EQUALITY_TRUE" :
710 // es == EQUALITY_FALSE ? "EQUALITY_FALSE" :
711 // es == EQUALITY_TRUE_IN_MODEL ? "EQUALITY_TRUE_IN_MODEL" :
712 // es == EQUALITY_FALSE_IN_MODEL ? "EQUALITY_FALSE_IN_MODEL" :
713 // es == EQUALITY_UNKNOWN ? "EQUALITY_UNKNOWN" :
714 // "Unexpected case") << endl;
716 // We need to split on it
717 Debug("combineTheories") << "TheoryEngine::combineTheories(): requesting a split " << endl
;
719 lemma(equality
.orNode(equality
.notNode()), RULE_INVALID
, false, false, false, carePair
.theory
);
721 // This code is supposed to force preference to follow what the theory models already have
722 // but it doesn't seem to make a big difference - need to explore more -Clark
724 // if (es == EQUALITY_TRUE || es == EQUALITY_TRUE_IN_MODEL) {
725 Node e
= ensureLiteral(equality
);
726 d_propEngine
->requirePhase(e
, true);
728 // else if (es == EQUALITY_FALSE_IN_MODEL) {
729 // Node e = ensureLiteral(equality);
730 // d_propEngine->requirePhase(e, false);
736 void TheoryEngine::propagate(Theory::Effort effort
) {
737 // Reset the interrupt flag
738 d_interrupted
= false;
740 // Definition of the statement that is to be run by every theory
741 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
742 #undef CVC4_FOR_EACH_THEORY_STATEMENT
744 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
745 if (theory::TheoryTraits<THEORY>::hasPropagate && d_logicInfo.isTheoryEnabled(THEORY)) { \
746 theoryOf(THEORY)->propagate(effort); \
749 // Reset the interrupt flag
750 d_interrupted
= false;
752 // Propagate for each theory using the statement above
753 CVC4_FOR_EACH_THEORY
;
755 if(Dump
.isOn("missed-t-propagations")) {
756 for(unsigned i
= 0; i
< d_possiblePropagations
.size(); ++i
) {
757 Node atom
= d_possiblePropagations
[i
];
759 if(d_propEngine
->hasValue(atom
, value
)) {
762 // Doesn't have a value, check it (and the negation)
763 if(d_hasPropagated
.find(atom
) == d_hasPropagated
.end()) {
764 Dump("missed-t-propagations")
765 << CommentCommand("Completeness check for T-propagations; expect invalid")
766 << EchoCommand(atom
.toString())
767 << QueryCommand(atom
.toExpr())
768 << EchoCommand(atom
.notNode().toString())
769 << QueryCommand(atom
.notNode().toExpr());
775 Node
TheoryEngine::getNextDecisionRequest() {
776 // Definition of the statement that is to be run by every theory
777 unsigned min_priority
= 0;
779 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
780 #undef CVC4_FOR_EACH_THEORY_STATEMENT
782 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
783 if (theory::TheoryTraits<THEORY>::hasGetNextDecisionRequest && d_logicInfo.isTheoryEnabled(THEORY)) { \
785 Node n = theoryOf(THEORY)->getNextDecisionRequest( priority ); \
786 if(! n.isNull() && ( dec.isNull() || priority<min_priority ) ) { \
788 min_priority = priority; \
792 // Request decision from each theory using the statement above
793 CVC4_FOR_EACH_THEORY
;
798 bool TheoryEngine::properConflict(TNode conflict
) const {
800 if (conflict
.getKind() == kind::AND
) {
801 for (unsigned i
= 0; i
< conflict
.getNumChildren(); ++ i
) {
802 if (! getPropEngine()->hasValue(conflict
[i
], value
)) {
803 Debug("properConflict") << "Bad conflict is due to unassigned atom: "
804 << conflict
[i
] << endl
;
808 Debug("properConflict") << "Bad conflict is due to false atom: "
809 << conflict
[i
] << endl
;
812 if (conflict
[i
] != Rewriter::rewrite(conflict
[i
])) {
813 Debug("properConflict") << "Bad conflict is due to atom not in normal form: "
814 << conflict
[i
] << " vs " << Rewriter::rewrite(conflict
[i
]) << endl
;
819 if (! getPropEngine()->hasValue(conflict
, value
)) {
820 Debug("properConflict") << "Bad conflict is due to unassigned atom: "
825 Debug("properConflict") << "Bad conflict is due to false atom: "
829 if (conflict
!= Rewriter::rewrite(conflict
)) {
830 Debug("properConflict") << "Bad conflict is due to atom not in normal form: "
831 << conflict
<< " vs " << Rewriter::rewrite(conflict
) << endl
;
838 bool TheoryEngine::properPropagation(TNode lit
) const {
839 if(!getPropEngine()->isSatLiteral(lit
)) {
843 return !getPropEngine()->hasValue(lit
, b
);
846 bool TheoryEngine::properExplanation(TNode node
, TNode expl
) const {
847 // Explanation must be either a conjunction of true literals that have true SAT values already
848 // or a singled literal that has a true SAT value already.
849 if (expl
.getKind() == kind::AND
) {
850 for (unsigned i
= 0; i
< expl
.getNumChildren(); ++ i
) {
852 if (!d_propEngine
->hasValue(expl
[i
], value
) || !value
) {
858 return d_propEngine
->hasValue(expl
, value
) && value
;
863 bool TheoryEngine::collectModelInfo(theory::TheoryModel
* m
)
865 //have shared term engine collectModelInfo
866 // d_sharedTerms.collectModelInfo( m );
867 // Consult each active theory to get all relevant information
868 // concerning the model.
869 for(TheoryId theoryId
= theory::THEORY_FIRST
; theoryId
< theory::THEORY_LAST
; ++theoryId
) {
870 if(d_logicInfo
.isTheoryEnabled(theoryId
)) {
871 Trace("model-builder") << " CollectModelInfo on theory: " << theoryId
<< endl
;
872 if (!d_theoryTable
[theoryId
]->collectModelInfo(m
))
878 // Get the Boolean variables
879 vector
<TNode
> boolVars
;
880 d_propEngine
->getBooleanVariables(boolVars
);
881 vector
<TNode
>::iterator it
, iend
= boolVars
.end();
882 bool hasValue
, value
;
883 for (it
= boolVars
.begin(); it
!= iend
; ++it
) {
885 hasValue
= d_propEngine
->hasValue(var
, value
);
886 // TODO: Assert that hasValue is true?
890 Trace("model-builder-assertions") << "(assert" << (value
? " " : " (not ") << var
<< (value
? ");" : "));") << endl
;
891 if (!m
->assertPredicate(var
, value
))
899 void TheoryEngine::postProcessModel( theory::TheoryModel
* m
){
900 for(TheoryId theoryId
= theory::THEORY_FIRST
; theoryId
< theory::THEORY_LAST
; ++theoryId
) {
901 if(d_logicInfo
.isTheoryEnabled(theoryId
)) {
902 Trace("model-builder-debug") << " PostProcessModel on theory: " << theoryId
<< endl
;
903 d_theoryTable
[theoryId
]->postProcessModel( m
);
909 TheoryModel
* TheoryEngine::getModel() {
913 void TheoryEngine::getSynthSolutions(std::map
<Node
, Node
>& sol_map
)
917 d_quantEngine
->getSynthSolutions(sol_map
);
925 bool TheoryEngine::presolve() {
926 // Reset the interrupt flag
927 d_interrupted
= false;
930 // Definition of the statement that is to be run by every theory
931 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
932 #undef CVC4_FOR_EACH_THEORY_STATEMENT
934 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
935 if (theory::TheoryTraits<THEORY>::hasPresolve) { \
936 theoryOf(THEORY)->presolve(); \
942 // Presolve for each theory using the statement above
943 CVC4_FOR_EACH_THEORY
;
944 } catch(const theory::Interrupted
&) {
945 Trace("theory") << "TheoryEngine::presolve() => interrupted" << endl
;
947 // return whether we have a conflict
949 }/* TheoryEngine::presolve() */
951 void TheoryEngine::postsolve() {
952 // Reset the interrupt flag
953 d_interrupted
= false;
954 bool CVC4_UNUSED wasInConflict
= d_inConflict
;
957 // Definition of the statement that is to be run by every theory
958 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
959 #undef CVC4_FOR_EACH_THEORY_STATEMENT
961 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
962 if (theory::TheoryTraits<THEORY>::hasPostsolve) { \
963 theoryOf(THEORY)->postsolve(); \
964 Assert(! d_inConflict || wasInConflict, "conflict raised during postsolve()"); \
967 // Postsolve for each theory using the statement above
968 CVC4_FOR_EACH_THEORY
;
969 } catch(const theory::Interrupted
&) {
970 Trace("theory") << "TheoryEngine::postsolve() => interrupted" << endl
;
972 }/* TheoryEngine::postsolve() */
975 void TheoryEngine::notifyRestart() {
976 // Reset the interrupt flag
977 d_interrupted
= false;
979 // Definition of the statement that is to be run by every theory
980 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
981 #undef CVC4_FOR_EACH_THEORY_STATEMENT
983 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
984 if (theory::TheoryTraits<THEORY>::hasNotifyRestart && d_logicInfo.isTheoryEnabled(THEORY)) { \
985 theoryOf(THEORY)->notifyRestart(); \
988 // notify each theory using the statement above
989 CVC4_FOR_EACH_THEORY
;
992 void TheoryEngine::ppStaticLearn(TNode in
, NodeBuilder
<>& learned
) {
993 // Reset the interrupt flag
994 d_interrupted
= false;
996 // Definition of the statement that is to be run by every theory
997 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
998 #undef CVC4_FOR_EACH_THEORY_STATEMENT
1000 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
1001 if (theory::TheoryTraits<THEORY>::hasPpStaticLearn) { \
1002 theoryOf(THEORY)->ppStaticLearn(in, learned); \
1005 // static learning for each theory using the statement above
1006 CVC4_FOR_EACH_THEORY
;
1009 void TheoryEngine::shutdown() {
1010 // Set this first; if a Theory shutdown() throws an exception,
1011 // at least the destruction of the TheoryEngine won't confound
1013 d_hasShutDown
= true;
1015 // Shutdown all the theories
1016 for(TheoryId theoryId
= theory::THEORY_FIRST
; theoryId
< theory::THEORY_LAST
; ++theoryId
) {
1017 if(d_theoryTable
[theoryId
]) {
1018 theoryOf(theoryId
)->shutdown();
1025 theory::Theory::PPAssertStatus
TheoryEngine::solve(TNode literal
, SubstitutionMap
& substitutionOut
) {
1026 // Reset the interrupt flag
1027 d_interrupted
= false;
1029 TNode atom
= literal
.getKind() == kind::NOT
? literal
[0] : literal
;
1030 Trace("theory::solve") << "TheoryEngine::solve(" << literal
<< "): solving with " << theoryOf(atom
)->getId() << endl
;
1032 if(! d_logicInfo
.isTheoryEnabled(Theory::theoryOf(atom
)) &&
1033 Theory::theoryOf(atom
) != THEORY_SAT_SOLVER
) {
1035 ss
<< "The logic was specified as " << d_logicInfo
.getLogicString()
1036 << ", which doesn't include " << Theory::theoryOf(atom
)
1037 << ", but got a preprocessing-time fact for that theory." << endl
1038 << "The fact:" << endl
1040 throw LogicException(ss
.str());
1043 Theory::PPAssertStatus solveStatus
= theoryOf(atom
)->ppAssert(literal
, substitutionOut
);
1044 Trace("theory::solve") << "TheoryEngine::solve(" << literal
<< ") => " << solveStatus
<< endl
;
1048 // Recursively traverse a term and call the theory rewriter on its sub-terms
1049 Node
TheoryEngine::ppTheoryRewrite(TNode term
) {
1050 NodeMap::iterator find
= d_ppCache
.find(term
);
1051 if (find
!= d_ppCache
.end()) {
1052 return (*find
).second
;
1054 unsigned nc
= term
.getNumChildren();
1056 return theoryOf(term
)->ppRewrite(term
);
1058 Trace("theory-pp") << "ppTheoryRewrite { " << term
<< endl
;
1061 // do not rewrite inside quantifiers
1062 if (term
.getKind() == kind::FORALL
|| term
.getKind() == kind::EXISTS
1063 || term
.getKind() == kind::CHOICE
1064 || term
.getKind() == kind::LAMBDA
)
1066 newTerm
= Rewriter::rewrite(term
);
1070 NodeBuilder
<> newNode(term
.getKind());
1071 if (term
.getMetaKind() == kind::metakind::PARAMETERIZED
) {
1072 newNode
<< term
.getOperator();
1075 for (i
= 0; i
< nc
; ++i
) {
1076 newNode
<< ppTheoryRewrite(term
[i
]);
1078 newTerm
= Rewriter::rewrite(Node(newNode
));
1080 Node newTerm2
= theoryOf(newTerm
)->ppRewrite(newTerm
);
1081 if (newTerm
!= newTerm2
) {
1082 newTerm
= ppTheoryRewrite(Rewriter::rewrite(newTerm2
));
1084 d_ppCache
[term
] = newTerm
;
1085 Trace("theory-pp")<< "ppTheoryRewrite returning " << newTerm
<< "}" << endl
;
1090 void TheoryEngine::preprocessStart()
1096 struct preprocess_stack_element
{
1098 bool children_added
;
1099 preprocess_stack_element(TNode node
)
1100 : node(node
), children_added(false) {}
1101 };/* struct preprocess_stack_element */
1104 Node
TheoryEngine::preprocess(TNode assertion
) {
1106 Trace("theory::preprocess") << "TheoryEngine::preprocess(" << assertion
<< ")" << endl
;
1109 // Do a topological sort of the subexpressions and substitute them
1110 vector
<preprocess_stack_element
> toVisit
;
1111 toVisit
.push_back(assertion
);
1113 while (!toVisit
.empty())
1115 // The current node we are processing
1116 preprocess_stack_element
& stackHead
= toVisit
.back();
1117 TNode current
= stackHead
.node
;
1119 Debug("theory::internal") << "TheoryEngine::preprocess(" << assertion
<< "): processing " << current
<< endl
;
1121 // If node already in the cache we're done, pop from the stack
1122 NodeMap::iterator find
= d_ppCache
.find(current
);
1123 if (find
!= d_ppCache
.end()) {
1128 if(! d_logicInfo
.isTheoryEnabled(Theory::theoryOf(current
)) &&
1129 Theory::theoryOf(current
) != THEORY_SAT_SOLVER
) {
1131 ss
<< "The logic was specified as " << d_logicInfo
.getLogicString()
1132 << ", which doesn't include " << Theory::theoryOf(current
)
1133 << ", but got a preprocessing-time fact for that theory." << endl
1134 << "The fact:" << endl
1136 throw LogicException(ss
.str());
1139 // If this is an atom, we preprocess its terms with the theory ppRewriter
1140 if (Theory::theoryOf(current
) != THEORY_BOOL
) {
1141 Node ppRewritten
= ppTheoryRewrite(current
);
1142 d_ppCache
[current
] = ppRewritten
;
1143 Assert(Rewriter::rewrite(d_ppCache
[current
]) == d_ppCache
[current
]);
1147 // Not yet substituted, so process
1148 if (stackHead
.children_added
) {
1149 // Children have been processed, so substitute
1150 NodeBuilder
<> builder(current
.getKind());
1151 if (current
.getMetaKind() == kind::metakind::PARAMETERIZED
) {
1152 builder
<< current
.getOperator();
1154 for (unsigned i
= 0; i
< current
.getNumChildren(); ++ i
) {
1155 Assert(d_ppCache
.find(current
[i
]) != d_ppCache
.end());
1156 builder
<< d_ppCache
[current
[i
]];
1158 // Mark the substitution and continue
1159 Node result
= builder
;
1160 if (result
!= current
) {
1161 result
= Rewriter::rewrite(result
);
1163 Debug("theory::internal") << "TheoryEngine::preprocess(" << assertion
<< "): setting " << current
<< " -> " << result
<< endl
;
1164 d_ppCache
[current
] = result
;
1167 // Mark that we have added the children if any
1168 if (current
.getNumChildren() > 0) {
1169 stackHead
.children_added
= true;
1170 // We need to add the children
1171 for(TNode::iterator child_it
= current
.begin(); child_it
!= current
.end(); ++ child_it
) {
1172 TNode childNode
= *child_it
;
1173 NodeMap::iterator childFind
= d_ppCache
.find(childNode
);
1174 if (childFind
== d_ppCache
.end()) {
1175 toVisit
.push_back(childNode
);
1179 // No children, so we're done
1180 Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << assertion
<< "): setting " << current
<< " -> " << current
<< endl
;
1181 d_ppCache
[current
] = current
;
1187 // Return the substituted version
1188 return d_ppCache
[assertion
];
1191 void TheoryEngine::notifyPreprocessedAssertions(
1192 const std::vector
<Node
>& assertions
) {
1193 // call all the theories
1194 for (TheoryId theoryId
= theory::THEORY_FIRST
; theoryId
< theory::THEORY_LAST
;
1196 if (d_theoryTable
[theoryId
]) {
1197 theoryOf(theoryId
)->ppNotifyAssertions(assertions
);
1202 bool TheoryEngine::markPropagation(TNode assertion
, TNode originalAssertion
, theory::TheoryId toTheoryId
, theory::TheoryId fromTheoryId
) {
1204 // What and where we are asserting
1205 NodeTheoryPair
toAssert(assertion
, toTheoryId
, d_propagationMapTimestamp
);
1206 // What and where it came from
1207 NodeTheoryPair
toExplain(originalAssertion
, fromTheoryId
, d_propagationMapTimestamp
);
1209 // See if the theory already got this literal
1210 PropagationMap::const_iterator find
= d_propagationMap
.find(toAssert
);
1211 if (find
!= d_propagationMap
.end()) {
1212 // The theory already knows this
1213 Trace("theory::assertToTheory") << "TheoryEngine::markPropagation(): already there" << endl
;
1217 Trace("theory::assertToTheory") << "TheoryEngine::markPropagation(): marking [" << d_propagationMapTimestamp
<< "] " << assertion
<< ", " << toTheoryId
<< " from " << originalAssertion
<< ", " << fromTheoryId
<< endl
;
1219 // Mark the propagation
1220 d_propagationMap
[toAssert
] = toExplain
;
1221 d_propagationMapTimestamp
= d_propagationMapTimestamp
+ 1;
1227 void TheoryEngine::assertToTheory(TNode assertion
, TNode originalAssertion
, theory::TheoryId toTheoryId
, theory::TheoryId fromTheoryId
) {
1229 Trace("theory::assertToTheory") << "TheoryEngine::assertToTheory(" << assertion
<< ", " << originalAssertion
<< "," << toTheoryId
<< ", " << fromTheoryId
<< ")" << endl
;
1231 Assert(toTheoryId
!= fromTheoryId
);
1232 if(toTheoryId
!= THEORY_SAT_SOLVER
&&
1233 ! d_logicInfo
.isTheoryEnabled(toTheoryId
)) {
1235 ss
<< "The logic was specified as " << d_logicInfo
.getLogicString()
1236 << ", which doesn't include " << toTheoryId
1237 << ", but got an asserted fact to that theory." << endl
1238 << "The fact:" << endl
1240 throw LogicException(ss
.str());
1247 // If sharing is disabled, things are easy
1248 if (!d_logicInfo
.isSharingEnabled()) {
1249 Assert(assertion
== originalAssertion
);
1250 if (fromTheoryId
== THEORY_SAT_SOLVER
) {
1251 // Send to the apropriate theory
1252 theory::Theory
* toTheory
= theoryOf(toTheoryId
);
1253 // We assert it, and we know it's preregistereed
1254 toTheory
->assertFact(assertion
, true);
1255 // Mark that we have more information
1256 d_factsAsserted
= true;
1258 Assert(toTheoryId
== THEORY_SAT_SOLVER
);
1259 // Check for propositional conflict
1261 if (d_propEngine
->hasValue(assertion
, value
)) {
1263 Trace("theory::propagate") << "TheoryEngine::assertToTheory(" << assertion
<< ", " << toTheoryId
<< ", " << fromTheoryId
<< "): conflict (no sharing)" << endl
;
1264 d_inConflict
= true;
1269 d_propagatedLiterals
.push_back(assertion
);
1274 // Polarity of the assertion
1275 bool polarity
= assertion
.getKind() != kind::NOT
;
1277 // Atom of the assertion
1278 TNode atom
= polarity
? assertion
: assertion
[0];
1280 // If sending to the shared terms database, it's also simple
1281 if (toTheoryId
== THEORY_BUILTIN
) {
1282 Assert(atom
.getKind() == kind::EQUAL
, "atom should be an EQUALity, not `%s'", atom
.toString().c_str());
1283 if (markPropagation(assertion
, originalAssertion
, toTheoryId
, fromTheoryId
)) {
1284 d_sharedTerms
.assertEquality(atom
, polarity
, assertion
);
1289 // Things from the SAT solver are already normalized, so they go
1290 // directly to the apropriate theory
1291 if (fromTheoryId
== THEORY_SAT_SOLVER
) {
1292 // We know that this is normalized, so just send it off to the theory
1293 if (markPropagation(assertion
, originalAssertion
, toTheoryId
, fromTheoryId
)) {
1294 // Is it preregistered
1295 bool preregistered
= d_propEngine
->isSatLiteral(assertion
) && Theory::theoryOf(assertion
) == toTheoryId
;
1297 theoryOf(toTheoryId
)->assertFact(assertion
, preregistered
);
1298 // Mark that we have more information
1299 d_factsAsserted
= true;
1304 // Propagations to the SAT solver are just enqueued for pickup by
1305 // the SAT solver later
1306 if (toTheoryId
== THEORY_SAT_SOLVER
) {
1307 if (markPropagation(assertion
, originalAssertion
, toTheoryId
, fromTheoryId
)) {
1308 // Enqueue for propagation to the SAT solver
1309 d_propagatedLiterals
.push_back(assertion
);
1310 // Check for propositional conflicts
1312 if (d_propEngine
->hasValue(assertion
, value
) && !value
) {
1313 Trace("theory::propagate") << "TheoryEngine::assertToTheory(" << assertion
<< ", " << toTheoryId
<< ", " << fromTheoryId
<< "): conflict (sharing)" << endl
;
1314 d_inConflict
= true;
1320 Assert(atom
.getKind() == kind::EQUAL
);
1323 Node normalizedLiteral
= Rewriter::rewrite(assertion
);
1325 // See if it rewrites false directly -> conflict
1326 if (normalizedLiteral
.isConst()) {
1327 if (!normalizedLiteral
.getConst
<bool>()) {
1328 // Mark the propagation for explanations
1329 if (markPropagation(normalizedLiteral
, originalAssertion
, toTheoryId
, fromTheoryId
)) {
1330 // Get the explanation (conflict will figure out where it came from)
1331 conflict(normalizedLiteral
, toTheoryId
);
1339 // Try and assert (note that we assert the non-normalized one)
1340 if (markPropagation(assertion
, originalAssertion
, toTheoryId
, fromTheoryId
)) {
1341 // Check if has been pre-registered with the theory
1342 bool preregistered
= d_propEngine
->isSatLiteral(assertion
) && Theory::theoryOf(assertion
) == toTheoryId
;
1344 theoryOf(toTheoryId
)->assertFact(assertion
, preregistered
);
1345 d_factsAsserted
= true;
1351 void TheoryEngine::assertFact(TNode literal
)
1353 Trace("theory") << "TheoryEngine::assertFact(" << literal
<< ")" << endl
;
1357 // If we're in conflict, nothing to do
1363 bool polarity
= literal
.getKind() != kind::NOT
;
1364 TNode atom
= polarity
? literal
: literal
[0];
1366 if (d_logicInfo
.isSharingEnabled()) {
1368 // If any shared terms, it's time to do sharing work
1369 if (d_sharedTerms
.hasSharedTerms(atom
)) {
1370 // Notify the theories the shared terms
1371 SharedTermsDatabase::shared_terms_iterator it
= d_sharedTerms
.begin(atom
);
1372 SharedTermsDatabase::shared_terms_iterator it_end
= d_sharedTerms
.end(atom
);
1373 for (; it
!= it_end
; ++ it
) {
1375 Theory::Set theories
= d_sharedTerms
.getTheoriesToNotify(atom
, term
);
1376 for (TheoryId id
= THEORY_FIRST
; id
!= THEORY_LAST
; ++ id
) {
1377 if (Theory::setContains(id
, theories
)) {
1378 theoryOf(id
)->addSharedTermInternal(term
);
1381 d_sharedTerms
.markNotified(term
, theories
);
1385 // If it's an equality, assert it to the shared term manager, even though the terms are not
1386 // yet shared. As the terms become shared later, the shared terms manager will then add them
1387 // to the assert the equality to the interested theories
1388 if (atom
.getKind() == kind::EQUAL
) {
1389 // Assert it to the the owning theory
1390 assertToTheory(literal
, literal
, /* to */ Theory::theoryOf(atom
), /* from */ THEORY_SAT_SOLVER
);
1391 // Shared terms manager will assert to interested theories directly, as the terms become shared
1392 assertToTheory(literal
, literal
, /* to */ THEORY_BUILTIN
, /* from */ THEORY_SAT_SOLVER
);
1394 // Now, let's check for any atom triggers from lemmas
1395 AtomRequests::atom_iterator it
= d_atomRequests
.getAtomIterator(atom
);
1396 while (!it
.done()) {
1397 const AtomRequests::Request
& request
= it
.get();
1398 Node toAssert
= polarity
? (Node
) request
.atom
: request
.atom
.notNode();
1399 Debug("theory::atoms") << "TheoryEngine::assertFact(" << literal
<< "): sending requested " << toAssert
<< endl
;
1400 assertToTheory(toAssert
, literal
, request
.toTheory
, THEORY_SAT_SOLVER
);
1405 // Not an equality, just assert to the appropriate theory
1406 assertToTheory(literal
, literal
, /* to */ Theory::theoryOf(atom
), /* from */ THEORY_SAT_SOLVER
);
1409 // Assert the fact to the appropriate theory directly
1410 assertToTheory(literal
, literal
, /* to */ Theory::theoryOf(atom
), /* from */ THEORY_SAT_SOLVER
);
1414 bool TheoryEngine::propagate(TNode literal
, theory::TheoryId theory
) {
1416 Debug("theory::propagate") << "TheoryEngine::propagate(" << literal
<< ", " << theory
<< ")" << endl
;
1420 if(Dump
.isOn("t-propagations")) {
1421 Dump("t-propagations") << CommentCommand("negation of theory propagation: expect valid")
1422 << QueryCommand(literal
.toExpr());
1424 if(Dump
.isOn("missed-t-propagations")) {
1425 d_hasPropagated
.insert(literal
);
1429 bool polarity
= literal
.getKind() != kind::NOT
;
1430 TNode atom
= polarity
? literal
: literal
[0];
1432 if (d_logicInfo
.isSharingEnabled() && atom
.getKind() == kind::EQUAL
) {
1433 if (d_propEngine
->isSatLiteral(literal
)) {
1434 // We propagate SAT literals to SAT
1435 assertToTheory(literal
, literal
, /* to */ THEORY_SAT_SOLVER
, /* from */ theory
);
1437 if (theory
!= THEORY_BUILTIN
) {
1438 // Assert to the shared terms database
1439 assertToTheory(literal
, literal
, /* to */ THEORY_BUILTIN
, /* from */ theory
);
1442 // We could be propagating a unit-clause lemma. In this case, we need to provide a
1444 // TODO: Consider putting this someplace else? This is the only refence to the proof
1445 // manager in this class.
1448 LemmaProofRecipe proofRecipe
;
1449 proofRecipe
.addBaseAssertion(literal
);
1452 LemmaProofRecipe::ProofStep
proofStep(theory
, emptyNode
);
1453 proofStep
.addAssertion(literal
);
1454 proofRecipe
.addStep(proofStep
);
1456 ProofManager::getCnfProof()->setProofRecipe(&proofRecipe
);
1459 // Just send off to the SAT solver
1460 Assert(d_propEngine
->isSatLiteral(literal
));
1461 assertToTheory(literal
, literal
, /* to */ THEORY_SAT_SOLVER
, /* from */ theory
);
1464 return !d_inConflict
;
1468 theory::EqualityStatus
TheoryEngine::getEqualityStatus(TNode a
, TNode b
) {
1469 Assert(a
.getType().isComparableTo(b
.getType()));
1470 if (d_sharedTerms
.isShared(a
) && d_sharedTerms
.isShared(b
)) {
1471 if (d_sharedTerms
.areEqual(a
,b
)) {
1472 return EQUALITY_TRUE_AND_PROPAGATED
;
1474 else if (d_sharedTerms
.areDisequal(a
,b
)) {
1475 return EQUALITY_FALSE_AND_PROPAGATED
;
1478 return theoryOf(Theory::theoryOf(a
.getType()))->getEqualityStatus(a
, b
);
1481 Node
TheoryEngine::getModelValue(TNode var
) {
1482 if (var
.isConst()) return var
; // FIXME: HACK!!!
1483 Assert(d_sharedTerms
.isShared(var
));
1484 return theoryOf(Theory::theoryOf(var
.getType()))->getModelValue(var
);
1488 Node
TheoryEngine::ensureLiteral(TNode n
) {
1489 Debug("ensureLiteral") << "rewriting: " << n
<< std::endl
;
1490 Node rewritten
= Rewriter::rewrite(n
);
1491 Debug("ensureLiteral") << " got: " << rewritten
<< std::endl
;
1492 Node preprocessed
= preprocess(rewritten
);
1493 Debug("ensureLiteral") << "preprocessed: " << preprocessed
<< std::endl
;
1494 d_propEngine
->ensureLiteral(preprocessed
);
1495 return preprocessed
;
1499 void TheoryEngine::printInstantiations( std::ostream
& out
) {
1500 if( d_quantEngine
){
1501 d_quantEngine
->printInstantiations( out
);
1503 out
<< "Internal error : instantiations not available when quantifiers are not present." << std::endl
;
1508 void TheoryEngine::printSynthSolution( std::ostream
& out
) {
1509 if( d_quantEngine
){
1510 d_quantEngine
->printSynthSolution( out
);
1512 out
<< "Internal error : synth solution not available when quantifiers are not present." << std::endl
;
1517 void TheoryEngine::getInstantiatedQuantifiedFormulas( std::vector
< Node
>& qs
) {
1518 if( d_quantEngine
){
1519 d_quantEngine
->getInstantiatedQuantifiedFormulas( qs
);
1525 void TheoryEngine::getInstantiations( Node q
, std::vector
< Node
>& insts
) {
1526 if( d_quantEngine
){
1527 d_quantEngine
->getInstantiations( q
, insts
);
1533 void TheoryEngine::getInstantiationTermVectors( Node q
, std::vector
< std::vector
< Node
> >& tvecs
) {
1534 if( d_quantEngine
){
1535 d_quantEngine
->getInstantiationTermVectors( q
, tvecs
);
1541 void TheoryEngine::getInstantiations( std::map
< Node
, std::vector
< Node
> >& insts
) {
1542 if( d_quantEngine
){
1543 d_quantEngine
->getInstantiations( insts
);
1549 void TheoryEngine::getInstantiationTermVectors( std::map
< Node
, std::vector
< std::vector
< Node
> > >& insts
) {
1550 if( d_quantEngine
){
1551 d_quantEngine
->getInstantiationTermVectors( insts
);
1557 Node
TheoryEngine::getInstantiatedConjunction( Node q
) {
1558 if( d_quantEngine
){
1559 return d_quantEngine
->getInstantiatedConjunction( q
);
1562 return Node::null();
1567 static Node
mkExplanation(const std::vector
<NodeTheoryPair
>& explanation
) {
1569 std::set
<TNode
> all
;
1570 for (unsigned i
= 0; i
< explanation
.size(); ++ i
) {
1571 Assert(explanation
[i
].theory
== THEORY_SAT_SOLVER
);
1572 all
.insert(explanation
[i
].node
);
1575 if (all
.size() == 0) {
1576 // Normalize to true
1577 return NodeManager::currentNM()->mkConst
<bool>(true);
1580 if (all
.size() == 1) {
1581 // All the same, or just one
1582 return explanation
[0].node
;
1585 NodeBuilder
<> conjunction(kind::AND
);
1586 std::set
<TNode
>::const_iterator it
= all
.begin();
1587 std::set
<TNode
>::const_iterator it_end
= all
.end();
1588 while (it
!= it_end
) {
1596 Node
TheoryEngine::getExplanationAndRecipe(TNode node
, LemmaProofRecipe
* proofRecipe
) {
1597 Debug("theory::explain") << "TheoryEngine::getExplanation(" << node
<< "): current propagation index = " << d_propagationMapTimestamp
<< endl
;
1599 bool polarity
= node
.getKind() != kind::NOT
;
1600 TNode atom
= polarity
? node
: node
[0];
1602 // If we're not in shared mode, explanations are simple
1603 if (!d_logicInfo
.isSharingEnabled()) {
1604 Debug("theory::explain") << "TheoryEngine::getExplanation: sharing is NOT enabled. "
1605 << " Responsible theory is: "
1606 << theoryOf(atom
)->getId() << std::endl
;
1608 Node explanation
= theoryOf(atom
)->explain(node
);
1609 Debug("theory::explain") << "TheoryEngine::getExplanation(" << node
<< ") => " << explanation
<< endl
;
1613 LemmaProofRecipe::ProofStep
proofStep(theoryOf(atom
)->getId(), emptyNode
);
1614 proofStep
.addAssertion(node
);
1615 proofRecipe
->addBaseAssertion(node
);
1617 if (explanation
.getKind() == kind::AND
) {
1618 // If the explanation is a conjunction, the recipe for the corresponding lemma is
1619 // the negation of its conjuncts.
1620 Node flat
= flattenAnd(explanation
);
1621 for (unsigned i
= 0; i
< flat
.getNumChildren(); ++i
) {
1622 if (flat
[i
].isConst() && flat
[i
].getConst
<bool>()) {
1626 if (flat
[i
].getKind() == kind::NOT
&&
1627 flat
[i
][0].isConst() && !flat
[i
][0].getConst
<bool>()) {
1631 Debug("theory::explain") << "TheoryEngine::getExplanationAndRecipe: adding recipe assertion: "
1632 << flat
[i
].negate() << std::endl
;
1633 proofStep
.addAssertion(flat
[i
].negate());
1634 proofRecipe
->addBaseAssertion(flat
[i
].negate());
1637 // The recipe for proving it is by negating it. "True" is not an acceptable reason.
1638 if (!((explanation
.isConst() && explanation
.getConst
<bool>()) ||
1639 (explanation
.getKind() == kind::NOT
&&
1640 explanation
[0].isConst() && !explanation
[0].getConst
<bool>()))) {
1641 proofStep
.addAssertion(explanation
.negate());
1642 proofRecipe
->addBaseAssertion(explanation
.negate());
1646 proofRecipe
->addStep(proofStep
);
1653 Debug("theory::explain") << "TheoryEngine::getExplanation: sharing IS enabled" << std::endl
;
1655 // Initial thing to explain
1656 NodeTheoryPair
toExplain(node
, THEORY_SAT_SOLVER
, d_propagationMapTimestamp
);
1657 Assert(d_propagationMap
.find(toExplain
) != d_propagationMap
.end());
1659 NodeTheoryPair nodeExplainerPair
= d_propagationMap
[toExplain
];
1660 Debug("theory::explain") << "TheoryEngine::getExplanation: explainer for node "
1661 << nodeExplainerPair
.node
1662 << " is theory: " << nodeExplainerPair
.theory
<< std::endl
;
1663 TheoryId explainer
= nodeExplainerPair
.theory
;
1665 // Create the workplace for explanations
1666 std::vector
<NodeTheoryPair
> explanationVector
;
1667 explanationVector
.push_back(d_propagationMap
[toExplain
]);
1668 // Process the explanation
1671 LemmaProofRecipe::ProofStep
proofStep(explainer
, emptyNode
);
1672 proofStep
.addAssertion(node
);
1673 proofRecipe
->addStep(proofStep
);
1674 proofRecipe
->addBaseAssertion(node
);
1677 getExplanation(explanationVector
, proofRecipe
);
1678 Node explanation
= mkExplanation(explanationVector
);
1680 Debug("theory::explain") << "TheoryEngine::getExplanation(" << node
<< ") => " << explanation
<< endl
;
1685 Node
TheoryEngine::getExplanation(TNode node
) {
1686 LemmaProofRecipe
*dontCareRecipe
= NULL
;
1687 return getExplanationAndRecipe(node
, dontCareRecipe
);
1690 struct AtomsCollect
{
1692 std::vector
<TNode
> d_atoms
;
1693 std::unordered_set
<TNode
, TNodeHashFunction
> d_visited
;
1697 typedef void return_type
;
1699 bool alreadyVisited(TNode current
, TNode parent
) {
1700 // Check if already visited
1701 if (d_visited
.find(current
) != d_visited
.end()) return true;
1702 // Don't visit non-boolean
1703 if (!current
.getType().isBoolean()) return true;
1708 void visit(TNode current
, TNode parent
) {
1709 if (Theory::theoryOf(current
) != theory::THEORY_BOOL
) {
1710 d_atoms
.push_back(current
);
1712 d_visited
.insert(current
);
1715 void start(TNode node
) {}
1716 void done(TNode node
) {}
1718 std::vector
<TNode
> getAtoms() const {
1723 void TheoryEngine::ensureLemmaAtoms(const std::vector
<TNode
>& atoms
, theory::TheoryId atomsTo
) {
1724 for (unsigned i
= 0; i
< atoms
.size(); ++ i
) {
1726 // Non-equality atoms are either owned by theory or they don't make sense
1727 if (atoms
[i
].getKind() != kind::EQUAL
) {
1733 // Simple normalization to not repeat stuff
1734 if (eq
[0] > eq
[1]) {
1735 eq
= eq
[1].eqNode(eq
[0]);
1738 // Rewrite the equality
1739 Node eqNormalized
= Rewriter::rewrite(atoms
[i
]);
1741 Debug("theory::atoms") << "TheoryEngine::ensureLemmaAtoms(): " << eq
<< " with nf " << eqNormalized
<< endl
;
1743 // If the equality is a boolean constant, we send immediately
1744 if (eqNormalized
.isConst()) {
1745 if (eqNormalized
.getConst
<bool>()) {
1746 assertToTheory(eq
, eqNormalized
, /** to */ atomsTo
, /** Sat solver */ theory::THEORY_SAT_SOLVER
);
1748 assertToTheory(eq
.notNode(), eqNormalized
.notNode(), /** to */ atomsTo
, /** Sat solver */ theory::THEORY_SAT_SOLVER
);
1751 }else if( eqNormalized
.getKind() != kind::EQUAL
){
1752 Assert( eqNormalized
.getKind()==kind::BOOLEAN_TERM_VARIABLE
||
1753 ( eqNormalized
.getKind()==kind::NOT
&& eqNormalized
[0].getKind()==kind::BOOLEAN_TERM_VARIABLE
) );
1754 // this happens for Boolean term equalities V = true that are rewritten to V, we should skip
1755 // TODO : revisit this
1759 // If the normalization did the just flips, keep the flip
1760 if (eqNormalized
[0] == eq
[1] && eqNormalized
[1] == eq
[0]) {
1764 // Check if the equality is already known by the sat solver
1765 if (d_propEngine
->isSatLiteral(eqNormalized
)) {
1767 if (d_propEngine
->hasValue(eqNormalized
, value
)) {
1769 assertToTheory(eq
, eqNormalized
, atomsTo
, theory::THEORY_SAT_SOLVER
);
1772 assertToTheory(eq
.notNode(), eqNormalized
.notNode(), atomsTo
, theory::THEORY_SAT_SOLVER
);
1778 // If the theory is asking about a different form, or the form is ok but if will go to a different theory
1779 // then we must figure it out
1780 if (eqNormalized
!= eq
|| Theory::theoryOf(eq
) != atomsTo
) {
1781 // If you get eqNormalized, send atoms[i] to atomsTo
1782 d_atomRequests
.add(eqNormalized
, eq
, atomsTo
);
1787 theory::LemmaStatus
TheoryEngine::lemma(TNode node
,
1792 theory::TheoryId atomsTo
) {
1793 // For resource-limiting (also does a time check).
1796 // Do we need to check atoms
1797 if (atomsTo
!= theory::THEORY_LAST
) {
1798 Debug("theory::atoms") << "TheoryEngine::lemma(" << node
<< ", " << atomsTo
<< ")" << endl
;
1799 AtomsCollect collectAtoms
;
1800 NodeVisitor
<AtomsCollect
>::run(collectAtoms
, node
);
1801 ensureLemmaAtoms(collectAtoms
.getAtoms(), atomsTo
);
1804 if(Dump
.isOn("t-lemmas")) {
1809 Dump("t-lemmas") << CommentCommand("theory lemma: expect valid")
1810 << QueryCommand(n
.toExpr());
1813 // Share with other portfolio threads
1814 if(d_channels
->getLemmaOutputChannel() != NULL
) {
1815 d_channels
->getLemmaOutputChannel()->notifyNewLemma(node
.toExpr());
1818 std::vector
<Node
> additionalLemmas
;
1819 IteSkolemMap iteSkolemMap
;
1821 // Run theory preprocessing, maybe
1822 Node ppNode
= preprocess
? this->preprocess(node
) : Node(node
);
1825 Debug("ite") << "Remove ITE from " << ppNode
<< std::endl
;
1826 additionalLemmas
.push_back(ppNode
);
1827 d_tform_remover
.run(additionalLemmas
, iteSkolemMap
);
1828 Debug("ite") << "..done " << additionalLemmas
[0] << std::endl
;
1829 additionalLemmas
[0] = theory::Rewriter::rewrite(additionalLemmas
[0]);
1831 if(Debug
.isOn("lemma-ites")) {
1832 Debug("lemma-ites") << "removed ITEs from lemma: " << ppNode
<< endl
;
1833 Debug("lemma-ites") << " + now have the following "
1834 << additionalLemmas
.size() << " lemma(s):" << endl
;
1835 for(std::vector
<Node
>::const_iterator i
= additionalLemmas
.begin();
1836 i
!= additionalLemmas
.end();
1838 Debug("lemma-ites") << " + " << *i
<< endl
;
1840 Debug("lemma-ites") << endl
;
1843 // assert to prop engine
1844 d_propEngine
->assertLemma(additionalLemmas
[0], negated
, removable
, rule
, node
);
1845 for (unsigned i
= 1; i
< additionalLemmas
.size(); ++ i
) {
1846 additionalLemmas
[i
] = theory::Rewriter::rewrite(additionalLemmas
[i
]);
1847 d_propEngine
->assertLemma(additionalLemmas
[i
], false, removable
, rule
, node
);
1850 // WARNING: Below this point don't assume additionalLemmas[0] to be not negated.
1852 additionalLemmas
[0] = additionalLemmas
[0].notNode();
1856 // assert to decision engine
1858 d_decisionEngine
->addAssertions(additionalLemmas
, 1, iteSkolemMap
);
1861 // Mark that we added some lemmas
1862 d_lemmasAdded
= true;
1864 // Lemma analysis isn't online yet; this lemma may only live for this
1866 return theory::LemmaStatus(additionalLemmas
[0], d_userContext
->getLevel());
1869 void TheoryEngine::conflict(TNode conflict
, TheoryId theoryId
) {
1871 Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict
<< ", " << theoryId
<< ")" << endl
;
1873 // Mark that we are in conflict
1874 d_inConflict
= true;
1876 if(Dump
.isOn("t-conflicts")) {
1877 Dump("t-conflicts") << CommentCommand("theory conflict: expect unsat")
1878 << CheckSatCommand(conflict
.toExpr());
1881 LemmaProofRecipe
* proofRecipe
= NULL
;
1883 proofRecipe
= new LemmaProofRecipe
;
1885 LemmaProofRecipe::ProofStep
proofStep(theoryId
, emptyNode
);
1887 if (conflict
.getKind() == kind::AND
) {
1888 for (unsigned i
= 0; i
< conflict
.getNumChildren(); ++i
) {
1889 proofStep
.addAssertion(conflict
[i
].negate());
1892 proofStep
.addAssertion(conflict
.negate());
1895 proofRecipe
->addStep(proofStep
);
1898 // In the multiple-theories case, we need to reconstruct the conflict
1899 if (d_logicInfo
.isSharingEnabled()) {
1900 // Create the workplace for explanations
1901 std::vector
<NodeTheoryPair
> explanationVector
;
1902 explanationVector
.push_back(NodeTheoryPair(conflict
, theoryId
, d_propagationMapTimestamp
));
1904 // Process the explanation
1905 getExplanation(explanationVector
, proofRecipe
);
1906 PROOF(ProofManager::getCnfProof()->setProofRecipe(proofRecipe
));
1907 Node fullConflict
= mkExplanation(explanationVector
);
1908 Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict
<< ", " << theoryId
<< "): full = " << fullConflict
<< endl
;
1909 Assert(properConflict(fullConflict
));
1910 lemma(fullConflict
, RULE_CONFLICT
, true, true, false, THEORY_LAST
);
1913 // When only one theory, the conflict should need no processing
1914 Assert(properConflict(conflict
));
1916 if (conflict
.getKind() == kind::AND
) {
1917 // If the conflict is a conjunction, the corresponding lemma is derived by negating
1919 for (unsigned i
= 0; i
< conflict
.getNumChildren(); ++i
) {
1920 if (conflict
[i
].isConst() && conflict
[i
].getConst
<bool>()) {
1924 if (conflict
[i
].getKind() == kind::NOT
&&
1925 conflict
[i
][0].isConst() && !conflict
[i
][0].getConst
<bool>()) {
1929 proofRecipe
->getStep(0)->addAssertion(conflict
[i
].negate());
1930 proofRecipe
->addBaseAssertion(conflict
[i
].negate());
1933 proofRecipe
->getStep(0)->addAssertion(conflict
.negate());
1934 proofRecipe
->addBaseAssertion(conflict
.negate());
1937 ProofManager::getCnfProof()->setProofRecipe(proofRecipe
);
1940 lemma(conflict
, RULE_CONFLICT
, true, true, false, THEORY_LAST
);
1949 void TheoryEngine::staticInitializeBVOptions(
1950 const std::vector
<Node
>& assertions
)
1952 bool useSlicer
= true;
1953 if (options::bitvectorEqualitySlicer() == bv::BITVECTOR_SLICER_ON
)
1955 if (!d_logicInfo
.isPure(theory::THEORY_BV
) || d_logicInfo
.isQuantified())
1956 throw ModalException(
1957 "Slicer currently only supports pure QF_BV formulas. Use "
1958 "--bv-eq-slicer=off");
1959 if (options::incrementalSolving())
1960 throw ModalException(
1961 "Slicer does not currently support incremental mode. Use "
1962 "--bv-eq-slicer=off");
1963 if (options::produceModels())
1964 throw ModalException(
1965 "Slicer does not currently support model generation. Use "
1966 "--bv-eq-slicer=off");
1968 else if (options::bitvectorEqualitySlicer() == bv::BITVECTOR_SLICER_OFF
)
1972 else if (options::bitvectorEqualitySlicer() == bv::BITVECTOR_SLICER_AUTO
)
1974 if ((!d_logicInfo
.isPure(theory::THEORY_BV
) || d_logicInfo
.isQuantified())
1975 || options::incrementalSolving()
1976 || options::produceModels())
1979 bv::utils::TNodeBoolMap cache
;
1980 for (unsigned i
= 0; i
< assertions
.size(); ++i
)
1982 useSlicer
= useSlicer
&& bv::utils::isCoreTerm(assertions
[i
], cache
);
1988 bv::TheoryBV
* bv_theory
= (bv::TheoryBV
*)d_theoryTable
[THEORY_BV
];
1989 bv_theory
->enableCoreTheorySlicer();
1993 void TheoryEngine::ppBvToBool(const std::vector
<Node
>& assertions
, std::vector
<Node
>& new_assertions
) {
1994 d_bvToBoolPreprocessor
.liftBvToBool(assertions
, new_assertions
);
1997 void TheoryEngine::ppBoolToBv(const std::vector
<Node
>& assertions
, std::vector
<Node
>& new_assertions
) {
1998 d_bvToBoolPreprocessor
.lowerBoolToBv(assertions
, new_assertions
);
2001 bool TheoryEngine::ppBvAbstraction(const std::vector
<Node
>& assertions
, std::vector
<Node
>& new_assertions
) {
2002 bv::TheoryBV
* bv_theory
= (bv::TheoryBV
*)d_theoryTable
[THEORY_BV
];
2003 return bv_theory
->applyAbstraction(assertions
, new_assertions
);
2006 void TheoryEngine::mkAckermanizationAssertions(std::vector
<Node
>& assertions
) {
2007 bv::TheoryBV
* bv_theory
= (bv::TheoryBV
*)d_theoryTable
[THEORY_BV
];
2008 bv_theory
->mkAckermanizationAssertions(assertions
);
2011 Node
TheoryEngine::ppSimpITE(TNode assertion
)
2013 if (!d_iteUtilities
->containsTermITE(assertion
))
2017 Node result
= d_iteUtilities
->simpITE(assertion
);
2018 Node res_rewritten
= Rewriter::rewrite(result
);
2020 if(options::simplifyWithCareEnabled()){
2021 Chat() << "starting simplifyWithCare()" << endl
;
2022 Node postSimpWithCare
= d_iteUtilities
->simplifyWithCare(res_rewritten
);
2023 Chat() << "ending simplifyWithCare()"
2024 << " post simplifyWithCare()" << postSimpWithCare
.getId() << endl
;
2025 result
= Rewriter::rewrite(postSimpWithCare
);
2027 result
= res_rewritten
;
2033 bool TheoryEngine::donePPSimpITE(std::vector
<Node
>& assertions
){
2034 // This pass does not support dependency tracking yet
2035 // (learns substitutions from all assertions so just
2036 // adding addDependence is not enough)
2037 if (options::unsatCores() || options::fewerPreprocessingHoles()) {
2041 bool simpDidALotOfWork
= d_iteUtilities
->simpIteDidALotOfWorkHeuristic();
2042 if(simpDidALotOfWork
){
2043 if(options::compressItes()){
2044 result
= d_iteUtilities
->compress(assertions
);
2048 // if false, don't bother to reclaim memory here.
2049 NodeManager
* nm
= NodeManager::currentNM();
2050 if(nm
->poolSize() >= options::zombieHuntThreshold()){
2051 Chat() << "..ite simplifier did quite a bit of work.. " << nm
->poolSize() << endl
;
2052 Chat() << "....node manager contains " << nm
->poolSize() << " nodes before cleanup" << endl
;
2053 d_iteUtilities
->clear();
2054 Rewriter::clearCaches();
2055 nm
->reclaimZombiesUntil(options::zombieHuntThreshold());
2056 Chat() << "....node manager contains " << nm
->poolSize() << " nodes after cleanup" << endl
;
2061 // Do theory specific preprocessing passes
2062 if(d_logicInfo
.isTheoryEnabled(theory::THEORY_ARITH
)
2063 && !options::incrementalSolving() ){
2064 if(!simpDidALotOfWork
){
2065 ContainsTermITEVisitor
& contains
=
2066 *(d_iteUtilities
->getContainsVisitor());
2067 arith::ArithIteUtils
aiteu(contains
, d_userContext
, getModel());
2068 bool anyItes
= false;
2069 for(size_t i
= 0; i
< assertions
.size(); ++i
){
2070 Node curr
= assertions
[i
];
2071 if(contains
.containsTermITE(curr
)){
2073 Node res
= aiteu
.reduceVariablesInItes(curr
);
2074 Debug("arith::ite::red") << "@ " << i
<< " ... " << curr
<< endl
<< " ->" << res
<< endl
;
2076 Node more
= aiteu
.reduceConstantIteByGCD(res
);
2077 Debug("arith::ite::red") << " gcd->" << more
<< endl
;
2078 assertions
[i
] = Rewriter::rewrite(more
);
2083 unsigned prevSubCount
= aiteu
.getSubCount();
2084 aiteu
.learnSubstitutions(assertions
);
2085 if(prevSubCount
< aiteu
.getSubCount()){
2086 d_arithSubstitutionsAdded
+= aiteu
.getSubCount() - prevSubCount
;
2087 bool anySuccess
= false;
2088 for(size_t i
= 0, N
= assertions
.size(); i
< N
; ++i
){
2089 Node curr
= assertions
[i
];
2090 Node next
= Rewriter::rewrite(aiteu
.applySubstitutions(curr
));
2091 Node res
= aiteu
.reduceVariablesInItes(next
);
2092 Debug("arith::ite::red") << "@ " << i
<< " ... " << next
<< endl
<< " ->" << res
<< endl
;
2093 Node more
= aiteu
.reduceConstantIteByGCD(res
);
2094 Debug("arith::ite::red") << " gcd->" << more
<< endl
;
2100 for(size_t i
= 0, N
= assertions
.size(); anySuccess
&& i
< N
; ++i
){
2101 Node curr
= assertions
[i
];
2102 Node next
= Rewriter::rewrite(aiteu
.applySubstitutions(curr
));
2103 Node res
= aiteu
.reduceVariablesInItes(next
);
2104 Debug("arith::ite::red") << "@ " << i
<< " ... " << next
<< endl
<< " ->" << res
<< endl
;
2105 Node more
= aiteu
.reduceConstantIteByGCD(res
);
2106 Debug("arith::ite::red") << " gcd->" << more
<< endl
;
2107 assertions
[i
] = Rewriter::rewrite(more
);
2116 void TheoryEngine::getExplanation(std::vector
<NodeTheoryPair
>& explanationVector
, LemmaProofRecipe
* proofRecipe
) {
2117 Assert(explanationVector
.size() > 0);
2119 unsigned i
= 0; // Index of the current literal we are processing
2120 unsigned j
= 0; // Index of the last literal we are keeping
2122 std::set
<Node
> inputAssertions
;
2123 PROOF(inputAssertions
= proofRecipe
->getStep(0)->getAssertions(););
2125 while (i
< explanationVector
.size()) {
2126 // Get the current literal to explain
2127 NodeTheoryPair toExplain
= explanationVector
[i
];
2129 Debug("theory::explain") << "[i=" << i
<< "] TheoryEngine::explain(): processing [" << toExplain
.timestamp
<< "] " << toExplain
.node
<< " sent from " << toExplain
.theory
<< endl
;
2132 // If a true constant or a negation of a false constant we can ignore it
2133 if (toExplain
.node
.isConst() && toExplain
.node
.getConst
<bool>()) {
2137 if (toExplain
.node
.getKind() == kind::NOT
&& toExplain
.node
[0].isConst() && !toExplain
.node
[0].getConst
<bool>()) {
2142 // If from the SAT solver, keep it
2143 if (toExplain
.theory
== THEORY_SAT_SOLVER
) {
2144 Debug("theory::explain") << "\tLiteral came from THEORY_SAT_SOLVER. Kepping it." << endl
;
2145 explanationVector
[j
++] = explanationVector
[i
++];
2149 // If an and, expand it
2150 if (toExplain
.node
.getKind() == kind::AND
) {
2151 Debug("theory::explain") << "TheoryEngine::explain(): expanding " << toExplain
.node
<< " got from " << toExplain
.theory
<< endl
;
2152 for (unsigned k
= 0; k
< toExplain
.node
.getNumChildren(); ++ k
) {
2153 NodeTheoryPair
newExplain(toExplain
.node
[k
], toExplain
.theory
, toExplain
.timestamp
);
2154 explanationVector
.push_back(newExplain
);
2160 // See if it was sent to the theory by another theory
2161 PropagationMap::const_iterator find
= d_propagationMap
.find(toExplain
);
2162 if (find
!= d_propagationMap
.end()) {
2163 Debug("theory::explain") << "\tTerm was propagated by another theory (theory = "
2164 << theoryOf((*find
).second
.theory
)->getId() << ")" << std::endl
;
2165 // There is some propagation, check if its a timely one
2166 if ((*find
).second
.timestamp
< toExplain
.timestamp
) {
2167 Debug("theory::explain") << "\tRelevant timetsamp, pushing "
2168 << (*find
).second
.node
<< "to index = " << explanationVector
.size() << std::endl
;
2169 explanationVector
.push_back((*find
).second
);
2173 if (toExplain
.node
!= (*find
).second
.node
) {
2174 Debug("pf::explain") << "TheoryEngine::getExplanation: Rewrite alert! toAssert = " << toExplain
.node
2175 << ", toExplain = " << (*find
).second
.node
<< std::endl
;
2178 proofRecipe
->addRewriteRule(toExplain
.node
, (*find
).second
.node
);
2187 // It was produced by the theory, so ask for an explanation
2189 if (toExplain
.theory
== THEORY_BUILTIN
) {
2190 explanation
= d_sharedTerms
.explain(toExplain
.node
);
2191 Debug("theory::explain") << "\tTerm was propagated by THEORY_BUILTIN. Explanation: " << explanation
<< std::endl
;
2193 explanation
= theoryOf(toExplain
.theory
)->explain(toExplain
.node
);
2194 Debug("theory::explain") << "\tTerm was propagated by owner theory: "
2195 << theoryOf(toExplain
.theory
)->getId()
2196 << ". Explanation: " << explanation
<< std::endl
;
2199 Debug("theory::explain") << "TheoryEngine::explain(): got explanation " << explanation
<< " got from " << toExplain
.theory
<< endl
;
2200 Assert( explanation
!= toExplain
.node
, "wasn't sent to you, so why are you explaining it trivially");
2201 // Mark the explanation
2202 NodeTheoryPair
newExplain(explanation
, toExplain
.theory
, toExplain
.timestamp
);
2203 explanationVector
.push_back(newExplain
);
2209 // If we're expanding the target node of the explanation (this is the first expansion...),
2210 // we don't want to add it as a separate proof step. It is already part of the assertions.
2211 if (inputAssertions
.find(toExplain
.node
) == inputAssertions
.end()) {
2212 LemmaProofRecipe::ProofStep
proofStep(toExplain
.theory
, toExplain
.node
);
2213 if (explanation
.getKind() == kind::AND
) {
2214 Node flat
= flattenAnd(explanation
);
2215 for (unsigned k
= 0; k
< flat
.getNumChildren(); ++ k
) {
2216 // If a true constant or a negation of a false constant we can ignore it
2217 if (! ((flat
[k
].isConst() && flat
[k
].getConst
<bool>()) ||
2218 (flat
[k
].getKind() == kind::NOT
&& flat
[k
][0].isConst() && !flat
[k
][0].getConst
<bool>()))) {
2219 proofStep
.addAssertion(flat
[k
].negate());
2223 if (! ((explanation
.isConst() && explanation
.getConst
<bool>()) ||
2224 (explanation
.getKind() == kind::NOT
&& explanation
[0].isConst() && !explanation
[0].getConst
<bool>()))) {
2225 proofStep
.addAssertion(explanation
.negate());
2228 proofRecipe
->addStep(proofStep
);
2234 // Keep only the relevant literals
2235 explanationVector
.resize(j
);
2239 // The remaining literals are the base of the proof
2240 for (unsigned k
= 0; k
< explanationVector
.size(); ++k
) {
2241 proofRecipe
->addBaseAssertion(explanationVector
[k
].node
.negate());
2247 void TheoryEngine::ppUnconstrainedSimp(vector
<Node
>& assertions
)
2249 d_unconstrainedSimp
->processAssertions(assertions
);
2252 void TheoryEngine::setUserAttribute(const std::string
& attr
,
2254 const std::vector
<Node
>& node_values
,
2255 const std::string
& str_value
)
2257 Trace("te-attr") << "set user attribute " << attr
<< " " << n
<< endl
;
2258 if( d_attr_handle
.find( attr
)!=d_attr_handle
.end() ){
2259 for( size_t i
=0; i
<d_attr_handle
[attr
].size(); i
++ ){
2260 d_attr_handle
[attr
][i
]->setUserAttribute(attr
, n
, node_values
, str_value
);
2263 //unhandled exception?
2267 void TheoryEngine::handleUserAttribute(const char* attr
, Theory
* t
) {
2268 Trace("te-attr") << "Handle user attribute " << attr
<< " " << t
<< endl
;
2269 std::string
str( attr
);
2270 d_attr_handle
[ str
].push_back( t
);
2273 void TheoryEngine::checkTheoryAssertionsWithModel(bool hardFailure
) {
2274 for(TheoryId theoryId
= THEORY_FIRST
; theoryId
< THEORY_LAST
; ++theoryId
) {
2275 Theory
* theory
= d_theoryTable
[theoryId
];
2276 if(theory
&& d_logicInfo
.isTheoryEnabled(theoryId
)) {
2277 for(context::CDList
<Assertion
>::const_iterator it
= theory
->facts_begin(),
2278 it_end
= theory
->facts_end();
2281 Node assertion
= (*it
).assertion
;
2282 Node val
= getModel()->getValue(assertion
);
2285 ss
<< theoryId
<< " has an asserted fact that the model doesn't satisfy." << endl
2286 << "The fact: " << assertion
<< endl
2287 << "Model value: " << val
<< endl
;
2289 InternalError(ss
.str());
2297 std::pair
<bool, Node
> TheoryEngine::entailmentCheck(theory::TheoryOfMode mode
, TNode lit
, const EntailmentCheckParameters
* params
, EntailmentCheckSideEffects
* seffects
) {
2298 TNode atom
= (lit
.getKind() == kind::NOT
) ? lit
[0] : lit
;
2299 if( atom
.getKind()==kind::AND
|| atom
.getKind()==kind::OR
|| atom
.getKind()==kind::IMPLIES
){
2300 //Boolean connective, recurse
2301 std::vector
< Node
> children
;
2302 bool pol
= (lit
.getKind()!=kind::NOT
);
2303 bool is_conjunction
= pol
==(lit
.getKind()==kind::AND
);
2304 for( unsigned i
=0; i
<atom
.getNumChildren(); i
++ ){
2306 if( pol
==( lit
.getKind()==kind::IMPLIES
&& i
==0 ) ){
2307 ch
= atom
[i
].negate();
2309 std::pair
<bool, Node
> chres
= entailmentCheck( mode
, ch
, params
, seffects
);
2311 if( !is_conjunction
){
2314 children
.push_back( chres
.second
);
2316 }else if( !chres
.first
&& is_conjunction
){
2317 return std::pair
<bool, Node
>(false, Node::null());
2320 if( is_conjunction
){
2321 return std::pair
<bool, Node
>(true, NodeManager::currentNM()->mkNode(kind::AND
, children
));
2323 return std::pair
<bool, Node
>(false, Node::null());
2325 }else if( atom
.getKind()==kind::ITE
|| ( atom
.getKind()==kind::EQUAL
&& atom
[0].getType().isBoolean() ) ){
2326 bool pol
= (lit
.getKind()!=kind::NOT
);
2327 for( unsigned r
=0; r
<2; r
++ ){
2332 std::pair
<bool, Node
> chres
= entailmentCheck( mode
, ch
, params
, seffects
);
2334 Node ch2
= atom
[ atom
.getKind()==kind::ITE
? r
+1 : 1 ];
2335 if( pol
==( atom
.getKind()==kind::ITE
? true : r
==1 ) ){
2338 std::pair
<bool, Node
> chres2
= entailmentCheck( mode
, ch2
, params
, seffects
);
2340 return std::pair
<bool, Node
>(true, NodeManager::currentNM()->mkNode(kind::AND
, chres
.second
, chres2
.second
));
2346 return std::pair
<bool, Node
>(false, Node::null());
2348 //it is a theory atom
2349 theory::TheoryId tid
= theory::Theory::theoryOf(mode
, atom
);
2350 theory::Theory
* th
= theoryOf(tid
);
2353 Assert(params
== NULL
|| tid
== params
->getTheoryId());
2354 Assert(seffects
== NULL
|| tid
== seffects
->getTheoryId());
2355 Trace("theory-engine-entc") << "Entailment check : " << lit
<< std::endl
;
2357 std::pair
<bool, Node
> chres
= th
->entailmentCheck(lit
, params
, seffects
);
2362 void TheoryEngine::spendResource(unsigned amount
)
2364 d_resourceManager
->spendResource(amount
);
2367 void TheoryEngine::enableTheoryAlternative(const std::string
& name
){
2368 Debug("TheoryEngine::enableTheoryAlternative")
2369 << "TheoryEngine::enableTheoryAlternative(" << name
<< ")" << std::endl
;
2371 d_theoryAlternatives
.insert(name
);
2374 bool TheoryEngine::useTheoryAlternative(const std::string
& name
) {
2375 return d_theoryAlternatives
.find(name
) != d_theoryAlternatives
.end();
2379 TheoryEngine::Statistics::Statistics(theory::TheoryId theory
):
2380 conflicts(getStatsPrefix(theory
) + "::conflicts", 0),
2381 propagations(getStatsPrefix(theory
) + "::propagations", 0),
2382 lemmas(getStatsPrefix(theory
) + "::lemmas", 0),
2383 requirePhase(getStatsPrefix(theory
) + "::requirePhase", 0),
2384 flipDecision(getStatsPrefix(theory
) + "::flipDecision", 0),
2385 restartDemands(getStatsPrefix(theory
) + "::restartDemands", 0)
2387 smtStatisticsRegistry()->registerStat(&conflicts
);
2388 smtStatisticsRegistry()->registerStat(&propagations
);
2389 smtStatisticsRegistry()->registerStat(&lemmas
);
2390 smtStatisticsRegistry()->registerStat(&requirePhase
);
2391 smtStatisticsRegistry()->registerStat(&flipDecision
);
2392 smtStatisticsRegistry()->registerStat(&restartDemands
);
2395 TheoryEngine::Statistics::~Statistics() {
2396 smtStatisticsRegistry()->unregisterStat(&conflicts
);
2397 smtStatisticsRegistry()->unregisterStat(&propagations
);
2398 smtStatisticsRegistry()->unregisterStat(&lemmas
);
2399 smtStatisticsRegistry()->unregisterStat(&requirePhase
);
2400 smtStatisticsRegistry()->unregisterStat(&flipDecision
);
2401 smtStatisticsRegistry()->unregisterStat(&restartDemands
);
2404 }/* CVC4 namespace */