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(
236 d_userContext
, "DefaultModel", options::assignFunctionValues());
237 d_aloc_curr_model
= true;
239 //make the default builder, e.g. in the case that the quantifiers engine does not have a model builder
240 if( d_curr_model_builder
==NULL
){
241 d_curr_model_builder
= new theory::TheoryEngineModelBuilder(this);
242 d_aloc_curr_model_builder
= true;
245 for(TheoryId theoryId
= theory::THEORY_FIRST
; theoryId
!= theory::THEORY_LAST
; ++ theoryId
) {
246 if (d_theoryTable
[theoryId
]) {
247 d_theoryTable
[theoryId
]->finishInit();
252 void TheoryEngine::eqNotifyNewClass(TNode t
){
253 if (d_logicInfo
.isQuantified()) {
254 d_quantEngine
->eqNotifyNewClass( t
);
258 void TheoryEngine::eqNotifyPreMerge(TNode t1
, TNode t2
){
259 if (d_logicInfo
.isQuantified()) {
260 d_quantEngine
->eqNotifyPreMerge( t1
, t2
);
264 void TheoryEngine::eqNotifyPostMerge(TNode t1
, TNode t2
){
265 if (d_logicInfo
.isQuantified()) {
266 d_quantEngine
->eqNotifyPostMerge( t1
, t2
);
270 void TheoryEngine::eqNotifyDisequal(TNode t1
, TNode t2
, TNode reason
){
271 if (d_logicInfo
.isQuantified()) {
272 d_quantEngine
->eqNotifyDisequal( t1
, t2
, reason
);
277 TheoryEngine::TheoryEngine(context::Context
* context
,
278 context::UserContext
* userContext
,
279 RemoveTermFormulas
& iteRemover
,
280 const LogicInfo
& logicInfo
,
281 LemmaChannels
* channels
)
282 : d_propEngine(NULL
),
283 d_decisionEngine(NULL
),
285 d_userContext(userContext
),
286 d_logicInfo(logicInfo
),
287 d_sharedTerms(this, context
),
288 d_masterEqualityEngine(NULL
),
289 d_masterEENotify(*this),
292 d_aloc_curr_model(false),
293 d_curr_model_builder(NULL
),
294 d_aloc_curr_model_builder(false),
296 d_possiblePropagations(context
),
297 d_hasPropagated(context
),
298 d_inConflict(context
, false),
299 d_hasShutDown(false),
300 d_incomplete(context
, false),
301 d_propagationMap(context
),
302 d_propagationMapTimestamp(context
, 0),
303 d_propagatedLiterals(context
),
304 d_propagatedLiteralsIndex(context
, 0),
305 d_atomRequests(context
),
306 d_tform_remover(iteRemover
),
307 d_combineTheoriesTime("TheoryEngine::combineTheoriesTime"),
310 d_interrupted(false),
311 d_resourceManager(NodeManager::currentResourceManager()),
312 d_channels(channels
),
313 d_inPreregister(false),
314 d_factsAsserted(context
, false),
315 d_preRegistrationVisitor(this, context
),
316 d_sharedTermsVisitor(d_sharedTerms
),
317 d_unconstrainedSimp(new UnconstrainedSimplifier(context
, logicInfo
)),
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
);
618 if(d_logicInfo
.isQuantified()) {
619 // quantifiers engine must check at last call effort
620 d_quantEngine
->check(Theory::EFFORT_LAST_CALL
);
623 if (!d_inConflict
&& !needCheck())
625 if (options::produceModels() && !d_curr_model
->isBuilt())
627 // must build model at this point
628 d_curr_model_builder
->buildModel(d_curr_model
);
633 Debug("theory") << "TheoryEngine::check(" << effort
<< "): done, we are " << (d_inConflict
? "unsat" : "sat") << (d_lemmasAdded
? " with new lemmas" : " with no new lemmas");
634 Debug("theory") << ", need check = " << (needCheck() ? "YES" : "NO") << endl
;
636 if( Theory::fullEffort(effort
) && !d_inConflict
&& !needCheck()) {
637 // case where we are about to answer SAT
638 if( d_masterEqualityEngine
!= NULL
){
639 AlwaysAssert(d_masterEqualityEngine
->consistent());
641 if (d_curr_model
->isBuilt())
643 // model construction should always succeed unless lemmas were added
644 AlwaysAssert(d_curr_model
->isBuiltSuccess());
645 if (options::produceModels())
647 // if we are incomplete, there is no guarantee on the model.
648 // thus, we do not check the model here. (related to #1693)
649 // we also don't debug-check the model if the checkModels()
651 if (!d_incomplete
&& options::checkModels())
653 d_curr_model_builder
->debugCheckModel(d_curr_model
);
655 // Do post-processing of model from the theories (used for THEORY_SEP
656 // to construct heap model)
657 postProcessModel(d_curr_model
);
661 } catch(const theory::Interrupted
&) {
662 Trace("theory") << "TheoryEngine::check() => interrupted" << endl
;
664 // If fulleffort, check all theories
665 if(Dump
.isOn("theory::fullcheck") && Theory::fullEffort(effort
)) {
666 if (!d_inConflict
&& !needCheck()) {
667 dumpAssertions("theory::fullcheck");
672 void TheoryEngine::combineTheories() {
674 Trace("combineTheories") << "TheoryEngine::combineTheories()" << endl
;
676 TimerStat::CodeTimer
combineTheoriesTimer(d_combineTheoriesTime
);
678 // Care graph we'll be building
681 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
682 #undef CVC4_FOR_EACH_THEORY_STATEMENT
684 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
685 if (theory::TheoryTraits<THEORY>::isParametric && d_logicInfo.isTheoryEnabled(THEORY)) { \
686 theoryOf(THEORY)->getCareGraph(&careGraph); \
689 // Call on each parametric theory to give us its care graph
690 CVC4_FOR_EACH_THEORY
;
692 Trace("combineTheories") << "TheoryEngine::combineTheories(): care graph size = " << careGraph
.size() << endl
;
694 // Now add splitters for the ones we are interested in
695 CareGraph::const_iterator care_it
= careGraph
.begin();
696 CareGraph::const_iterator care_it_end
= careGraph
.end();
698 for (; care_it
!= care_it_end
; ++ care_it
) {
699 const CarePair
& carePair
= *care_it
;
701 Debug("combineTheories") << "TheoryEngine::combineTheories(): checking " << carePair
.a
<< " = " << carePair
.b
<< " from " << carePair
.theory
<< endl
;
703 Assert(d_sharedTerms
.isShared(carePair
.a
) || carePair
.a
.isConst());
704 Assert(d_sharedTerms
.isShared(carePair
.b
) || carePair
.b
.isConst());
706 // The equality in question (order for no repetition)
707 Node equality
= carePair
.a
.eqNode(carePair
.b
);
708 // EqualityStatus es = getEqualityStatus(carePair.a, carePair.b);
709 // Debug("combineTheories") << "TheoryEngine::combineTheories(): " <<
710 // (es == EQUALITY_TRUE_AND_PROPAGATED ? "EQUALITY_TRUE_AND_PROPAGATED" :
711 // es == EQUALITY_FALSE_AND_PROPAGATED ? "EQUALITY_FALSE_AND_PROPAGATED" :
712 // es == EQUALITY_TRUE ? "EQUALITY_TRUE" :
713 // es == EQUALITY_FALSE ? "EQUALITY_FALSE" :
714 // es == EQUALITY_TRUE_IN_MODEL ? "EQUALITY_TRUE_IN_MODEL" :
715 // es == EQUALITY_FALSE_IN_MODEL ? "EQUALITY_FALSE_IN_MODEL" :
716 // es == EQUALITY_UNKNOWN ? "EQUALITY_UNKNOWN" :
717 // "Unexpected case") << endl;
719 // We need to split on it
720 Debug("combineTheories") << "TheoryEngine::combineTheories(): requesting a split " << endl
;
722 lemma(equality
.orNode(equality
.notNode()), RULE_INVALID
, false, false, false, carePair
.theory
);
724 // This code is supposed to force preference to follow what the theory models already have
725 // but it doesn't seem to make a big difference - need to explore more -Clark
727 // if (es == EQUALITY_TRUE || es == EQUALITY_TRUE_IN_MODEL) {
728 Node e
= ensureLiteral(equality
);
729 d_propEngine
->requirePhase(e
, true);
731 // else if (es == EQUALITY_FALSE_IN_MODEL) {
732 // Node e = ensureLiteral(equality);
733 // d_propEngine->requirePhase(e, false);
739 void TheoryEngine::propagate(Theory::Effort effort
) {
740 // Reset the interrupt flag
741 d_interrupted
= false;
743 // Definition of the statement that is to be run by every theory
744 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
745 #undef CVC4_FOR_EACH_THEORY_STATEMENT
747 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
748 if (theory::TheoryTraits<THEORY>::hasPropagate && d_logicInfo.isTheoryEnabled(THEORY)) { \
749 theoryOf(THEORY)->propagate(effort); \
752 // Reset the interrupt flag
753 d_interrupted
= false;
755 // Propagate for each theory using the statement above
756 CVC4_FOR_EACH_THEORY
;
758 if(Dump
.isOn("missed-t-propagations")) {
759 for(unsigned i
= 0; i
< d_possiblePropagations
.size(); ++i
) {
760 Node atom
= d_possiblePropagations
[i
];
762 if(d_propEngine
->hasValue(atom
, value
)) {
765 // Doesn't have a value, check it (and the negation)
766 if(d_hasPropagated
.find(atom
) == d_hasPropagated
.end()) {
767 Dump("missed-t-propagations")
768 << CommentCommand("Completeness check for T-propagations; expect invalid")
769 << EchoCommand(atom
.toString())
770 << QueryCommand(atom
.toExpr())
771 << EchoCommand(atom
.notNode().toString())
772 << QueryCommand(atom
.notNode().toExpr());
778 Node
TheoryEngine::getNextDecisionRequest() {
779 // Definition of the statement that is to be run by every theory
780 unsigned min_priority
= 0;
782 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
783 #undef CVC4_FOR_EACH_THEORY_STATEMENT
785 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
786 if (theory::TheoryTraits<THEORY>::hasGetNextDecisionRequest && d_logicInfo.isTheoryEnabled(THEORY)) { \
788 Node n = theoryOf(THEORY)->getNextDecisionRequest( priority ); \
789 if(! n.isNull() && ( dec.isNull() || priority<min_priority ) ) { \
791 min_priority = priority; \
795 // Request decision from each theory using the statement above
796 CVC4_FOR_EACH_THEORY
;
801 bool TheoryEngine::properConflict(TNode conflict
) const {
803 if (conflict
.getKind() == kind::AND
) {
804 for (unsigned i
= 0; i
< conflict
.getNumChildren(); ++ i
) {
805 if (! getPropEngine()->hasValue(conflict
[i
], value
)) {
806 Debug("properConflict") << "Bad conflict is due to unassigned atom: "
807 << conflict
[i
] << endl
;
811 Debug("properConflict") << "Bad conflict is due to false atom: "
812 << conflict
[i
] << endl
;
815 if (conflict
[i
] != Rewriter::rewrite(conflict
[i
])) {
816 Debug("properConflict") << "Bad conflict is due to atom not in normal form: "
817 << conflict
[i
] << " vs " << Rewriter::rewrite(conflict
[i
]) << endl
;
822 if (! getPropEngine()->hasValue(conflict
, value
)) {
823 Debug("properConflict") << "Bad conflict is due to unassigned atom: "
828 Debug("properConflict") << "Bad conflict is due to false atom: "
832 if (conflict
!= Rewriter::rewrite(conflict
)) {
833 Debug("properConflict") << "Bad conflict is due to atom not in normal form: "
834 << conflict
<< " vs " << Rewriter::rewrite(conflict
) << endl
;
841 bool TheoryEngine::properPropagation(TNode lit
) const {
842 if(!getPropEngine()->isSatLiteral(lit
)) {
846 return !getPropEngine()->hasValue(lit
, b
);
849 bool TheoryEngine::properExplanation(TNode node
, TNode expl
) const {
850 // Explanation must be either a conjunction of true literals that have true SAT values already
851 // or a singled literal that has a true SAT value already.
852 if (expl
.getKind() == kind::AND
) {
853 for (unsigned i
= 0; i
< expl
.getNumChildren(); ++ i
) {
855 if (!d_propEngine
->hasValue(expl
[i
], value
) || !value
) {
861 return d_propEngine
->hasValue(expl
, value
) && value
;
866 bool TheoryEngine::collectModelInfo(theory::TheoryModel
* m
)
868 //have shared term engine collectModelInfo
869 // d_sharedTerms.collectModelInfo( m );
870 // Consult each active theory to get all relevant information
871 // concerning the model.
872 for(TheoryId theoryId
= theory::THEORY_FIRST
; theoryId
< theory::THEORY_LAST
; ++theoryId
) {
873 if(d_logicInfo
.isTheoryEnabled(theoryId
)) {
874 Trace("model-builder") << " CollectModelInfo on theory: " << theoryId
<< endl
;
875 if (!d_theoryTable
[theoryId
]->collectModelInfo(m
))
881 // Get the Boolean variables
882 vector
<TNode
> boolVars
;
883 d_propEngine
->getBooleanVariables(boolVars
);
884 vector
<TNode
>::iterator it
, iend
= boolVars
.end();
885 bool hasValue
, value
;
886 for (it
= boolVars
.begin(); it
!= iend
; ++it
) {
888 hasValue
= d_propEngine
->hasValue(var
, value
);
889 // TODO: Assert that hasValue is true?
893 Trace("model-builder-assertions") << "(assert" << (value
? " " : " (not ") << var
<< (value
? ");" : "));") << endl
;
894 if (!m
->assertPredicate(var
, value
))
902 void TheoryEngine::postProcessModel( theory::TheoryModel
* m
){
903 for(TheoryId theoryId
= theory::THEORY_FIRST
; theoryId
< theory::THEORY_LAST
; ++theoryId
) {
904 if(d_logicInfo
.isTheoryEnabled(theoryId
)) {
905 Trace("model-builder-debug") << " PostProcessModel on theory: " << theoryId
<< endl
;
906 d_theoryTable
[theoryId
]->postProcessModel( m
);
912 TheoryModel
* TheoryEngine::getModel() {
916 void TheoryEngine::getSynthSolutions(std::map
<Node
, Node
>& sol_map
)
920 d_quantEngine
->getSynthSolutions(sol_map
);
928 bool TheoryEngine::presolve() {
929 // Reset the interrupt flag
930 d_interrupted
= false;
933 // Definition of the statement that is to be run by every theory
934 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
935 #undef CVC4_FOR_EACH_THEORY_STATEMENT
937 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
938 if (theory::TheoryTraits<THEORY>::hasPresolve) { \
939 theoryOf(THEORY)->presolve(); \
945 // Presolve for each theory using the statement above
946 CVC4_FOR_EACH_THEORY
;
947 } catch(const theory::Interrupted
&) {
948 Trace("theory") << "TheoryEngine::presolve() => interrupted" << endl
;
950 // return whether we have a conflict
952 }/* TheoryEngine::presolve() */
954 void TheoryEngine::postsolve() {
955 // Reset the interrupt flag
956 d_interrupted
= false;
957 bool CVC4_UNUSED wasInConflict
= d_inConflict
;
960 // Definition of the statement that is to be run by every theory
961 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
962 #undef CVC4_FOR_EACH_THEORY_STATEMENT
964 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
965 if (theory::TheoryTraits<THEORY>::hasPostsolve) { \
966 theoryOf(THEORY)->postsolve(); \
967 Assert(! d_inConflict || wasInConflict, "conflict raised during postsolve()"); \
970 // Postsolve for each theory using the statement above
971 CVC4_FOR_EACH_THEORY
;
972 } catch(const theory::Interrupted
&) {
973 Trace("theory") << "TheoryEngine::postsolve() => interrupted" << endl
;
975 }/* TheoryEngine::postsolve() */
978 void TheoryEngine::notifyRestart() {
979 // Reset the interrupt flag
980 d_interrupted
= false;
982 // Definition of the statement that is to be run by every theory
983 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
984 #undef CVC4_FOR_EACH_THEORY_STATEMENT
986 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
987 if (theory::TheoryTraits<THEORY>::hasNotifyRestart && d_logicInfo.isTheoryEnabled(THEORY)) { \
988 theoryOf(THEORY)->notifyRestart(); \
991 // notify each theory using the statement above
992 CVC4_FOR_EACH_THEORY
;
995 void TheoryEngine::ppStaticLearn(TNode in
, NodeBuilder
<>& learned
) {
996 // Reset the interrupt flag
997 d_interrupted
= false;
999 // Definition of the statement that is to be run by every theory
1000 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
1001 #undef CVC4_FOR_EACH_THEORY_STATEMENT
1003 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
1004 if (theory::TheoryTraits<THEORY>::hasPpStaticLearn) { \
1005 theoryOf(THEORY)->ppStaticLearn(in, learned); \
1008 // static learning for each theory using the statement above
1009 CVC4_FOR_EACH_THEORY
;
1012 void TheoryEngine::shutdown() {
1013 // Set this first; if a Theory shutdown() throws an exception,
1014 // at least the destruction of the TheoryEngine won't confound
1016 d_hasShutDown
= true;
1018 // Shutdown all the theories
1019 for(TheoryId theoryId
= theory::THEORY_FIRST
; theoryId
< theory::THEORY_LAST
; ++theoryId
) {
1020 if(d_theoryTable
[theoryId
]) {
1021 theoryOf(theoryId
)->shutdown();
1028 theory::Theory::PPAssertStatus
TheoryEngine::solve(TNode literal
, SubstitutionMap
& substitutionOut
) {
1029 // Reset the interrupt flag
1030 d_interrupted
= false;
1032 TNode atom
= literal
.getKind() == kind::NOT
? literal
[0] : literal
;
1033 Trace("theory::solve") << "TheoryEngine::solve(" << literal
<< "): solving with " << theoryOf(atom
)->getId() << endl
;
1035 if(! d_logicInfo
.isTheoryEnabled(Theory::theoryOf(atom
)) &&
1036 Theory::theoryOf(atom
) != THEORY_SAT_SOLVER
) {
1038 ss
<< "The logic was specified as " << d_logicInfo
.getLogicString()
1039 << ", which doesn't include " << Theory::theoryOf(atom
)
1040 << ", but got a preprocessing-time fact for that theory." << endl
1041 << "The fact:" << endl
1043 throw LogicException(ss
.str());
1046 Theory::PPAssertStatus solveStatus
= theoryOf(atom
)->ppAssert(literal
, substitutionOut
);
1047 Trace("theory::solve") << "TheoryEngine::solve(" << literal
<< ") => " << solveStatus
<< endl
;
1051 // Recursively traverse a term and call the theory rewriter on its sub-terms
1052 Node
TheoryEngine::ppTheoryRewrite(TNode term
) {
1053 NodeMap::iterator find
= d_ppCache
.find(term
);
1054 if (find
!= d_ppCache
.end()) {
1055 return (*find
).second
;
1057 unsigned nc
= term
.getNumChildren();
1059 return theoryOf(term
)->ppRewrite(term
);
1061 Trace("theory-pp") << "ppTheoryRewrite { " << term
<< endl
;
1064 // do not rewrite inside quantifiers
1065 if (term
.getKind() == kind::FORALL
|| term
.getKind() == kind::EXISTS
1066 || term
.getKind() == kind::CHOICE
1067 || term
.getKind() == kind::LAMBDA
)
1069 newTerm
= Rewriter::rewrite(term
);
1073 NodeBuilder
<> newNode(term
.getKind());
1074 if (term
.getMetaKind() == kind::metakind::PARAMETERIZED
) {
1075 newNode
<< term
.getOperator();
1078 for (i
= 0; i
< nc
; ++i
) {
1079 newNode
<< ppTheoryRewrite(term
[i
]);
1081 newTerm
= Rewriter::rewrite(Node(newNode
));
1083 Node newTerm2
= theoryOf(newTerm
)->ppRewrite(newTerm
);
1084 if (newTerm
!= newTerm2
) {
1085 newTerm
= ppTheoryRewrite(Rewriter::rewrite(newTerm2
));
1087 d_ppCache
[term
] = newTerm
;
1088 Trace("theory-pp")<< "ppTheoryRewrite returning " << newTerm
<< "}" << endl
;
1093 void TheoryEngine::preprocessStart()
1099 struct preprocess_stack_element
{
1101 bool children_added
;
1102 preprocess_stack_element(TNode node
)
1103 : node(node
), children_added(false) {}
1104 };/* struct preprocess_stack_element */
1107 Node
TheoryEngine::preprocess(TNode assertion
) {
1109 Trace("theory::preprocess") << "TheoryEngine::preprocess(" << assertion
<< ")" << endl
;
1112 // Do a topological sort of the subexpressions and substitute them
1113 vector
<preprocess_stack_element
> toVisit
;
1114 toVisit
.push_back(assertion
);
1116 while (!toVisit
.empty())
1118 // The current node we are processing
1119 preprocess_stack_element
& stackHead
= toVisit
.back();
1120 TNode current
= stackHead
.node
;
1122 Debug("theory::internal") << "TheoryEngine::preprocess(" << assertion
<< "): processing " << current
<< endl
;
1124 // If node already in the cache we're done, pop from the stack
1125 NodeMap::iterator find
= d_ppCache
.find(current
);
1126 if (find
!= d_ppCache
.end()) {
1131 if(! d_logicInfo
.isTheoryEnabled(Theory::theoryOf(current
)) &&
1132 Theory::theoryOf(current
) != THEORY_SAT_SOLVER
) {
1134 ss
<< "The logic was specified as " << d_logicInfo
.getLogicString()
1135 << ", which doesn't include " << Theory::theoryOf(current
)
1136 << ", but got a preprocessing-time fact for that theory." << endl
1137 << "The fact:" << endl
1139 throw LogicException(ss
.str());
1142 // If this is an atom, we preprocess its terms with the theory ppRewriter
1143 if (Theory::theoryOf(current
) != THEORY_BOOL
) {
1144 Node ppRewritten
= ppTheoryRewrite(current
);
1145 d_ppCache
[current
] = ppRewritten
;
1146 Assert(Rewriter::rewrite(d_ppCache
[current
]) == d_ppCache
[current
]);
1150 // Not yet substituted, so process
1151 if (stackHead
.children_added
) {
1152 // Children have been processed, so substitute
1153 NodeBuilder
<> builder(current
.getKind());
1154 if (current
.getMetaKind() == kind::metakind::PARAMETERIZED
) {
1155 builder
<< current
.getOperator();
1157 for (unsigned i
= 0; i
< current
.getNumChildren(); ++ i
) {
1158 Assert(d_ppCache
.find(current
[i
]) != d_ppCache
.end());
1159 builder
<< d_ppCache
[current
[i
]];
1161 // Mark the substitution and continue
1162 Node result
= builder
;
1163 if (result
!= current
) {
1164 result
= Rewriter::rewrite(result
);
1166 Debug("theory::internal") << "TheoryEngine::preprocess(" << assertion
<< "): setting " << current
<< " -> " << result
<< endl
;
1167 d_ppCache
[current
] = result
;
1170 // Mark that we have added the children if any
1171 if (current
.getNumChildren() > 0) {
1172 stackHead
.children_added
= true;
1173 // We need to add the children
1174 for(TNode::iterator child_it
= current
.begin(); child_it
!= current
.end(); ++ child_it
) {
1175 TNode childNode
= *child_it
;
1176 NodeMap::iterator childFind
= d_ppCache
.find(childNode
);
1177 if (childFind
== d_ppCache
.end()) {
1178 toVisit
.push_back(childNode
);
1182 // No children, so we're done
1183 Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << assertion
<< "): setting " << current
<< " -> " << current
<< endl
;
1184 d_ppCache
[current
] = current
;
1190 // Return the substituted version
1191 return d_ppCache
[assertion
];
1194 void TheoryEngine::notifyPreprocessedAssertions(
1195 const std::vector
<Node
>& assertions
) {
1196 // call all the theories
1197 for (TheoryId theoryId
= theory::THEORY_FIRST
; theoryId
< theory::THEORY_LAST
;
1199 if (d_theoryTable
[theoryId
]) {
1200 theoryOf(theoryId
)->ppNotifyAssertions(assertions
);
1205 bool TheoryEngine::markPropagation(TNode assertion
, TNode originalAssertion
, theory::TheoryId toTheoryId
, theory::TheoryId fromTheoryId
) {
1207 // What and where we are asserting
1208 NodeTheoryPair
toAssert(assertion
, toTheoryId
, d_propagationMapTimestamp
);
1209 // What and where it came from
1210 NodeTheoryPair
toExplain(originalAssertion
, fromTheoryId
, d_propagationMapTimestamp
);
1212 // See if the theory already got this literal
1213 PropagationMap::const_iterator find
= d_propagationMap
.find(toAssert
);
1214 if (find
!= d_propagationMap
.end()) {
1215 // The theory already knows this
1216 Trace("theory::assertToTheory") << "TheoryEngine::markPropagation(): already there" << endl
;
1220 Trace("theory::assertToTheory") << "TheoryEngine::markPropagation(): marking [" << d_propagationMapTimestamp
<< "] " << assertion
<< ", " << toTheoryId
<< " from " << originalAssertion
<< ", " << fromTheoryId
<< endl
;
1222 // Mark the propagation
1223 d_propagationMap
[toAssert
] = toExplain
;
1224 d_propagationMapTimestamp
= d_propagationMapTimestamp
+ 1;
1230 void TheoryEngine::assertToTheory(TNode assertion
, TNode originalAssertion
, theory::TheoryId toTheoryId
, theory::TheoryId fromTheoryId
) {
1232 Trace("theory::assertToTheory") << "TheoryEngine::assertToTheory(" << assertion
<< ", " << originalAssertion
<< "," << toTheoryId
<< ", " << fromTheoryId
<< ")" << endl
;
1234 Assert(toTheoryId
!= fromTheoryId
);
1235 if(toTheoryId
!= THEORY_SAT_SOLVER
&&
1236 ! d_logicInfo
.isTheoryEnabled(toTheoryId
)) {
1238 ss
<< "The logic was specified as " << d_logicInfo
.getLogicString()
1239 << ", which doesn't include " << toTheoryId
1240 << ", but got an asserted fact to that theory." << endl
1241 << "The fact:" << endl
1243 throw LogicException(ss
.str());
1250 // If sharing is disabled, things are easy
1251 if (!d_logicInfo
.isSharingEnabled()) {
1252 Assert(assertion
== originalAssertion
);
1253 if (fromTheoryId
== THEORY_SAT_SOLVER
) {
1254 // Send to the apropriate theory
1255 theory::Theory
* toTheory
= theoryOf(toTheoryId
);
1256 // We assert it, and we know it's preregistereed
1257 toTheory
->assertFact(assertion
, true);
1258 // Mark that we have more information
1259 d_factsAsserted
= true;
1261 Assert(toTheoryId
== THEORY_SAT_SOLVER
);
1262 // Check for propositional conflict
1264 if (d_propEngine
->hasValue(assertion
, value
)) {
1266 Trace("theory::propagate") << "TheoryEngine::assertToTheory(" << assertion
<< ", " << toTheoryId
<< ", " << fromTheoryId
<< "): conflict (no sharing)" << endl
;
1267 d_inConflict
= true;
1272 d_propagatedLiterals
.push_back(assertion
);
1277 // Polarity of the assertion
1278 bool polarity
= assertion
.getKind() != kind::NOT
;
1280 // Atom of the assertion
1281 TNode atom
= polarity
? assertion
: assertion
[0];
1283 // If sending to the shared terms database, it's also simple
1284 if (toTheoryId
== THEORY_BUILTIN
) {
1285 Assert(atom
.getKind() == kind::EQUAL
, "atom should be an EQUALity, not `%s'", atom
.toString().c_str());
1286 if (markPropagation(assertion
, originalAssertion
, toTheoryId
, fromTheoryId
)) {
1287 d_sharedTerms
.assertEquality(atom
, polarity
, assertion
);
1292 // Things from the SAT solver are already normalized, so they go
1293 // directly to the apropriate theory
1294 if (fromTheoryId
== THEORY_SAT_SOLVER
) {
1295 // We know that this is normalized, so just send it off to the theory
1296 if (markPropagation(assertion
, originalAssertion
, toTheoryId
, fromTheoryId
)) {
1297 // Is it preregistered
1298 bool preregistered
= d_propEngine
->isSatLiteral(assertion
) && Theory::theoryOf(assertion
) == toTheoryId
;
1300 theoryOf(toTheoryId
)->assertFact(assertion
, preregistered
);
1301 // Mark that we have more information
1302 d_factsAsserted
= true;
1307 // Propagations to the SAT solver are just enqueued for pickup by
1308 // the SAT solver later
1309 if (toTheoryId
== THEORY_SAT_SOLVER
) {
1310 if (markPropagation(assertion
, originalAssertion
, toTheoryId
, fromTheoryId
)) {
1311 // Enqueue for propagation to the SAT solver
1312 d_propagatedLiterals
.push_back(assertion
);
1313 // Check for propositional conflicts
1315 if (d_propEngine
->hasValue(assertion
, value
) && !value
) {
1316 Trace("theory::propagate") << "TheoryEngine::assertToTheory(" << assertion
<< ", " << toTheoryId
<< ", " << fromTheoryId
<< "): conflict (sharing)" << endl
;
1317 d_inConflict
= true;
1323 Assert(atom
.getKind() == kind::EQUAL
);
1326 Node normalizedLiteral
= Rewriter::rewrite(assertion
);
1328 // See if it rewrites false directly -> conflict
1329 if (normalizedLiteral
.isConst()) {
1330 if (!normalizedLiteral
.getConst
<bool>()) {
1331 // Mark the propagation for explanations
1332 if (markPropagation(normalizedLiteral
, originalAssertion
, toTheoryId
, fromTheoryId
)) {
1333 // Get the explanation (conflict will figure out where it came from)
1334 conflict(normalizedLiteral
, toTheoryId
);
1342 // Try and assert (note that we assert the non-normalized one)
1343 if (markPropagation(assertion
, originalAssertion
, toTheoryId
, fromTheoryId
)) {
1344 // Check if has been pre-registered with the theory
1345 bool preregistered
= d_propEngine
->isSatLiteral(assertion
) && Theory::theoryOf(assertion
) == toTheoryId
;
1347 theoryOf(toTheoryId
)->assertFact(assertion
, preregistered
);
1348 d_factsAsserted
= true;
1354 void TheoryEngine::assertFact(TNode literal
)
1356 Trace("theory") << "TheoryEngine::assertFact(" << literal
<< ")" << endl
;
1360 // If we're in conflict, nothing to do
1366 bool polarity
= literal
.getKind() != kind::NOT
;
1367 TNode atom
= polarity
? literal
: literal
[0];
1369 if (d_logicInfo
.isSharingEnabled()) {
1371 // If any shared terms, it's time to do sharing work
1372 if (d_sharedTerms
.hasSharedTerms(atom
)) {
1373 // Notify the theories the shared terms
1374 SharedTermsDatabase::shared_terms_iterator it
= d_sharedTerms
.begin(atom
);
1375 SharedTermsDatabase::shared_terms_iterator it_end
= d_sharedTerms
.end(atom
);
1376 for (; it
!= it_end
; ++ it
) {
1378 Theory::Set theories
= d_sharedTerms
.getTheoriesToNotify(atom
, term
);
1379 for (TheoryId id
= THEORY_FIRST
; id
!= THEORY_LAST
; ++ id
) {
1380 if (Theory::setContains(id
, theories
)) {
1381 theoryOf(id
)->addSharedTermInternal(term
);
1384 d_sharedTerms
.markNotified(term
, theories
);
1388 // If it's an equality, assert it to the shared term manager, even though the terms are not
1389 // yet shared. As the terms become shared later, the shared terms manager will then add them
1390 // to the assert the equality to the interested theories
1391 if (atom
.getKind() == kind::EQUAL
) {
1392 // Assert it to the the owning theory
1393 assertToTheory(literal
, literal
, /* to */ Theory::theoryOf(atom
), /* from */ THEORY_SAT_SOLVER
);
1394 // Shared terms manager will assert to interested theories directly, as the terms become shared
1395 assertToTheory(literal
, literal
, /* to */ THEORY_BUILTIN
, /* from */ THEORY_SAT_SOLVER
);
1397 // Now, let's check for any atom triggers from lemmas
1398 AtomRequests::atom_iterator it
= d_atomRequests
.getAtomIterator(atom
);
1399 while (!it
.done()) {
1400 const AtomRequests::Request
& request
= it
.get();
1401 Node toAssert
= polarity
? (Node
) request
.atom
: request
.atom
.notNode();
1402 Debug("theory::atoms") << "TheoryEngine::assertFact(" << literal
<< "): sending requested " << toAssert
<< endl
;
1403 assertToTheory(toAssert
, literal
, request
.toTheory
, THEORY_SAT_SOLVER
);
1408 // Not an equality, just assert to the appropriate theory
1409 assertToTheory(literal
, literal
, /* to */ Theory::theoryOf(atom
), /* from */ THEORY_SAT_SOLVER
);
1412 // Assert the fact to the appropriate theory directly
1413 assertToTheory(literal
, literal
, /* to */ Theory::theoryOf(atom
), /* from */ THEORY_SAT_SOLVER
);
1417 bool TheoryEngine::propagate(TNode literal
, theory::TheoryId theory
) {
1419 Debug("theory::propagate") << "TheoryEngine::propagate(" << literal
<< ", " << theory
<< ")" << endl
;
1423 if(Dump
.isOn("t-propagations")) {
1424 Dump("t-propagations") << CommentCommand("negation of theory propagation: expect valid")
1425 << QueryCommand(literal
.toExpr());
1427 if(Dump
.isOn("missed-t-propagations")) {
1428 d_hasPropagated
.insert(literal
);
1432 bool polarity
= literal
.getKind() != kind::NOT
;
1433 TNode atom
= polarity
? literal
: literal
[0];
1435 if (d_logicInfo
.isSharingEnabled() && atom
.getKind() == kind::EQUAL
) {
1436 if (d_propEngine
->isSatLiteral(literal
)) {
1437 // We propagate SAT literals to SAT
1438 assertToTheory(literal
, literal
, /* to */ THEORY_SAT_SOLVER
, /* from */ theory
);
1440 if (theory
!= THEORY_BUILTIN
) {
1441 // Assert to the shared terms database
1442 assertToTheory(literal
, literal
, /* to */ THEORY_BUILTIN
, /* from */ theory
);
1445 // We could be propagating a unit-clause lemma. In this case, we need to provide a
1447 // TODO: Consider putting this someplace else? This is the only refence to the proof
1448 // manager in this class.
1451 LemmaProofRecipe proofRecipe
;
1452 proofRecipe
.addBaseAssertion(literal
);
1455 LemmaProofRecipe::ProofStep
proofStep(theory
, emptyNode
);
1456 proofStep
.addAssertion(literal
);
1457 proofRecipe
.addStep(proofStep
);
1459 ProofManager::getCnfProof()->setProofRecipe(&proofRecipe
);
1462 // Just send off to the SAT solver
1463 Assert(d_propEngine
->isSatLiteral(literal
));
1464 assertToTheory(literal
, literal
, /* to */ THEORY_SAT_SOLVER
, /* from */ theory
);
1467 return !d_inConflict
;
1470 const LogicInfo
& TheoryEngine::getLogicInfo() const { return d_logicInfo
; }
1472 theory::EqualityStatus
TheoryEngine::getEqualityStatus(TNode a
, TNode b
) {
1473 Assert(a
.getType().isComparableTo(b
.getType()));
1474 if (d_sharedTerms
.isShared(a
) && d_sharedTerms
.isShared(b
)) {
1475 if (d_sharedTerms
.areEqual(a
,b
)) {
1476 return EQUALITY_TRUE_AND_PROPAGATED
;
1478 else if (d_sharedTerms
.areDisequal(a
,b
)) {
1479 return EQUALITY_FALSE_AND_PROPAGATED
;
1482 return theoryOf(Theory::theoryOf(a
.getType()))->getEqualityStatus(a
, b
);
1485 Node
TheoryEngine::getModelValue(TNode var
) {
1488 // the model value of a constant must be itself
1491 Assert(d_sharedTerms
.isShared(var
));
1492 return theoryOf(Theory::theoryOf(var
.getType()))->getModelValue(var
);
1496 Node
TheoryEngine::ensureLiteral(TNode n
) {
1497 Debug("ensureLiteral") << "rewriting: " << n
<< std::endl
;
1498 Node rewritten
= Rewriter::rewrite(n
);
1499 Debug("ensureLiteral") << " got: " << rewritten
<< std::endl
;
1500 Node preprocessed
= preprocess(rewritten
);
1501 Debug("ensureLiteral") << "preprocessed: " << preprocessed
<< std::endl
;
1502 d_propEngine
->ensureLiteral(preprocessed
);
1503 return preprocessed
;
1507 void TheoryEngine::printInstantiations( std::ostream
& out
) {
1508 if( d_quantEngine
){
1509 d_quantEngine
->printInstantiations( out
);
1511 out
<< "Internal error : instantiations not available when quantifiers are not present." << std::endl
;
1516 void TheoryEngine::printSynthSolution( std::ostream
& out
) {
1517 if( d_quantEngine
){
1518 d_quantEngine
->printSynthSolution( out
);
1520 out
<< "Internal error : synth solution not available when quantifiers are not present." << std::endl
;
1525 void TheoryEngine::getInstantiatedQuantifiedFormulas( std::vector
< Node
>& qs
) {
1526 if( d_quantEngine
){
1527 d_quantEngine
->getInstantiatedQuantifiedFormulas( qs
);
1533 void TheoryEngine::getInstantiations( Node q
, std::vector
< Node
>& insts
) {
1534 if( d_quantEngine
){
1535 d_quantEngine
->getInstantiations( q
, insts
);
1541 void TheoryEngine::getInstantiationTermVectors( Node q
, std::vector
< std::vector
< Node
> >& tvecs
) {
1542 if( d_quantEngine
){
1543 d_quantEngine
->getInstantiationTermVectors( q
, tvecs
);
1549 void TheoryEngine::getInstantiations( std::map
< Node
, std::vector
< Node
> >& insts
) {
1550 if( d_quantEngine
){
1551 d_quantEngine
->getInstantiations( insts
);
1557 void TheoryEngine::getInstantiationTermVectors( std::map
< Node
, std::vector
< std::vector
< Node
> > >& insts
) {
1558 if( d_quantEngine
){
1559 d_quantEngine
->getInstantiationTermVectors( insts
);
1565 Node
TheoryEngine::getInstantiatedConjunction( Node q
) {
1566 if( d_quantEngine
){
1567 return d_quantEngine
->getInstantiatedConjunction( q
);
1570 return Node::null();
1575 static Node
mkExplanation(const std::vector
<NodeTheoryPair
>& explanation
) {
1577 std::set
<TNode
> all
;
1578 for (unsigned i
= 0; i
< explanation
.size(); ++ i
) {
1579 Assert(explanation
[i
].theory
== THEORY_SAT_SOLVER
);
1580 all
.insert(explanation
[i
].node
);
1583 if (all
.size() == 0) {
1584 // Normalize to true
1585 return NodeManager::currentNM()->mkConst
<bool>(true);
1588 if (all
.size() == 1) {
1589 // All the same, or just one
1590 return explanation
[0].node
;
1593 NodeBuilder
<> conjunction(kind::AND
);
1594 std::set
<TNode
>::const_iterator it
= all
.begin();
1595 std::set
<TNode
>::const_iterator it_end
= all
.end();
1596 while (it
!= it_end
) {
1604 Node
TheoryEngine::getExplanationAndRecipe(TNode node
, LemmaProofRecipe
* proofRecipe
) {
1605 Debug("theory::explain") << "TheoryEngine::getExplanation(" << node
<< "): current propagation index = " << d_propagationMapTimestamp
<< endl
;
1607 bool polarity
= node
.getKind() != kind::NOT
;
1608 TNode atom
= polarity
? node
: node
[0];
1610 // If we're not in shared mode, explanations are simple
1611 if (!d_logicInfo
.isSharingEnabled()) {
1612 Debug("theory::explain") << "TheoryEngine::getExplanation: sharing is NOT enabled. "
1613 << " Responsible theory is: "
1614 << theoryOf(atom
)->getId() << std::endl
;
1616 Node explanation
= theoryOf(atom
)->explain(node
);
1617 Debug("theory::explain") << "TheoryEngine::getExplanation(" << node
<< ") => " << explanation
<< endl
;
1621 LemmaProofRecipe::ProofStep
proofStep(theoryOf(atom
)->getId(), emptyNode
);
1622 proofStep
.addAssertion(node
);
1623 proofRecipe
->addBaseAssertion(node
);
1625 if (explanation
.getKind() == kind::AND
) {
1626 // If the explanation is a conjunction, the recipe for the corresponding lemma is
1627 // the negation of its conjuncts.
1628 Node flat
= flattenAnd(explanation
);
1629 for (unsigned i
= 0; i
< flat
.getNumChildren(); ++i
) {
1630 if (flat
[i
].isConst() && flat
[i
].getConst
<bool>()) {
1634 if (flat
[i
].getKind() == kind::NOT
&&
1635 flat
[i
][0].isConst() && !flat
[i
][0].getConst
<bool>()) {
1639 Debug("theory::explain") << "TheoryEngine::getExplanationAndRecipe: adding recipe assertion: "
1640 << flat
[i
].negate() << std::endl
;
1641 proofStep
.addAssertion(flat
[i
].negate());
1642 proofRecipe
->addBaseAssertion(flat
[i
].negate());
1645 // The recipe for proving it is by negating it. "True" is not an acceptable reason.
1646 if (!((explanation
.isConst() && explanation
.getConst
<bool>()) ||
1647 (explanation
.getKind() == kind::NOT
&&
1648 explanation
[0].isConst() && !explanation
[0].getConst
<bool>()))) {
1649 proofStep
.addAssertion(explanation
.negate());
1650 proofRecipe
->addBaseAssertion(explanation
.negate());
1654 proofRecipe
->addStep(proofStep
);
1661 Debug("theory::explain") << "TheoryEngine::getExplanation: sharing IS enabled" << std::endl
;
1663 // Initial thing to explain
1664 NodeTheoryPair
toExplain(node
, THEORY_SAT_SOLVER
, d_propagationMapTimestamp
);
1665 Assert(d_propagationMap
.find(toExplain
) != d_propagationMap
.end());
1667 NodeTheoryPair nodeExplainerPair
= d_propagationMap
[toExplain
];
1668 Debug("theory::explain") << "TheoryEngine::getExplanation: explainer for node "
1669 << nodeExplainerPair
.node
1670 << " is theory: " << nodeExplainerPair
.theory
<< std::endl
;
1671 TheoryId explainer
= nodeExplainerPair
.theory
;
1673 // Create the workplace for explanations
1674 std::vector
<NodeTheoryPair
> explanationVector
;
1675 explanationVector
.push_back(d_propagationMap
[toExplain
]);
1676 // Process the explanation
1679 LemmaProofRecipe::ProofStep
proofStep(explainer
, emptyNode
);
1680 proofStep
.addAssertion(node
);
1681 proofRecipe
->addStep(proofStep
);
1682 proofRecipe
->addBaseAssertion(node
);
1685 getExplanation(explanationVector
, proofRecipe
);
1686 Node explanation
= mkExplanation(explanationVector
);
1688 Debug("theory::explain") << "TheoryEngine::getExplanation(" << node
<< ") => " << explanation
<< endl
;
1693 Node
TheoryEngine::getExplanation(TNode node
) {
1694 LemmaProofRecipe
*dontCareRecipe
= NULL
;
1695 return getExplanationAndRecipe(node
, dontCareRecipe
);
1698 struct AtomsCollect
{
1700 std::vector
<TNode
> d_atoms
;
1701 std::unordered_set
<TNode
, TNodeHashFunction
> d_visited
;
1705 typedef void return_type
;
1707 bool alreadyVisited(TNode current
, TNode parent
) {
1708 // Check if already visited
1709 if (d_visited
.find(current
) != d_visited
.end()) return true;
1710 // Don't visit non-boolean
1711 if (!current
.getType().isBoolean()) return true;
1716 void visit(TNode current
, TNode parent
) {
1717 if (Theory::theoryOf(current
) != theory::THEORY_BOOL
) {
1718 d_atoms
.push_back(current
);
1720 d_visited
.insert(current
);
1723 void start(TNode node
) {}
1724 void done(TNode node
) {}
1726 std::vector
<TNode
> getAtoms() const {
1731 void TheoryEngine::ensureLemmaAtoms(const std::vector
<TNode
>& atoms
, theory::TheoryId atomsTo
) {
1732 for (unsigned i
= 0; i
< atoms
.size(); ++ i
) {
1734 // Non-equality atoms are either owned by theory or they don't make sense
1735 if (atoms
[i
].getKind() != kind::EQUAL
) {
1741 // Simple normalization to not repeat stuff
1742 if (eq
[0] > eq
[1]) {
1743 eq
= eq
[1].eqNode(eq
[0]);
1746 // Rewrite the equality
1747 Node eqNormalized
= Rewriter::rewrite(atoms
[i
]);
1749 Debug("theory::atoms") << "TheoryEngine::ensureLemmaAtoms(): " << eq
<< " with nf " << eqNormalized
<< endl
;
1751 // If the equality is a boolean constant, we send immediately
1752 if (eqNormalized
.isConst()) {
1753 if (eqNormalized
.getConst
<bool>()) {
1754 assertToTheory(eq
, eqNormalized
, /** to */ atomsTo
, /** Sat solver */ theory::THEORY_SAT_SOLVER
);
1756 assertToTheory(eq
.notNode(), eqNormalized
.notNode(), /** to */ atomsTo
, /** Sat solver */ theory::THEORY_SAT_SOLVER
);
1759 }else if( eqNormalized
.getKind() != kind::EQUAL
){
1760 Assert( eqNormalized
.getKind()==kind::BOOLEAN_TERM_VARIABLE
||
1761 ( eqNormalized
.getKind()==kind::NOT
&& eqNormalized
[0].getKind()==kind::BOOLEAN_TERM_VARIABLE
) );
1762 // this happens for Boolean term equalities V = true that are rewritten to V, we should skip
1763 // TODO : revisit this
1767 // If the normalization did the just flips, keep the flip
1768 if (eqNormalized
[0] == eq
[1] && eqNormalized
[1] == eq
[0]) {
1772 // Check if the equality is already known by the sat solver
1773 if (d_propEngine
->isSatLiteral(eqNormalized
)) {
1775 if (d_propEngine
->hasValue(eqNormalized
, value
)) {
1777 assertToTheory(eq
, eqNormalized
, atomsTo
, theory::THEORY_SAT_SOLVER
);
1780 assertToTheory(eq
.notNode(), eqNormalized
.notNode(), atomsTo
, theory::THEORY_SAT_SOLVER
);
1786 // If the theory is asking about a different form, or the form is ok but if will go to a different theory
1787 // then we must figure it out
1788 if (eqNormalized
!= eq
|| Theory::theoryOf(eq
) != atomsTo
) {
1789 // If you get eqNormalized, send atoms[i] to atomsTo
1790 d_atomRequests
.add(eqNormalized
, eq
, atomsTo
);
1795 theory::LemmaStatus
TheoryEngine::lemma(TNode node
,
1800 theory::TheoryId atomsTo
) {
1801 // For resource-limiting (also does a time check).
1804 // Do we need to check atoms
1805 if (atomsTo
!= theory::THEORY_LAST
) {
1806 Debug("theory::atoms") << "TheoryEngine::lemma(" << node
<< ", " << atomsTo
<< ")" << endl
;
1807 AtomsCollect collectAtoms
;
1808 NodeVisitor
<AtomsCollect
>::run(collectAtoms
, node
);
1809 ensureLemmaAtoms(collectAtoms
.getAtoms(), atomsTo
);
1812 if(Dump
.isOn("t-lemmas")) {
1817 Dump("t-lemmas") << CommentCommand("theory lemma: expect valid")
1818 << QueryCommand(n
.toExpr());
1821 // Share with other portfolio threads
1822 if(d_channels
->getLemmaOutputChannel() != NULL
) {
1823 d_channels
->getLemmaOutputChannel()->notifyNewLemma(node
.toExpr());
1826 std::vector
<Node
> additionalLemmas
;
1827 IteSkolemMap iteSkolemMap
;
1829 // Run theory preprocessing, maybe
1830 Node ppNode
= preprocess
? this->preprocess(node
) : Node(node
);
1833 Debug("ite") << "Remove ITE from " << ppNode
<< std::endl
;
1834 additionalLemmas
.push_back(ppNode
);
1835 d_tform_remover
.run(additionalLemmas
, iteSkolemMap
);
1836 Debug("ite") << "..done " << additionalLemmas
[0] << std::endl
;
1837 additionalLemmas
[0] = theory::Rewriter::rewrite(additionalLemmas
[0]);
1839 if(Debug
.isOn("lemma-ites")) {
1840 Debug("lemma-ites") << "removed ITEs from lemma: " << ppNode
<< endl
;
1841 Debug("lemma-ites") << " + now have the following "
1842 << additionalLemmas
.size() << " lemma(s):" << endl
;
1843 for(std::vector
<Node
>::const_iterator i
= additionalLemmas
.begin();
1844 i
!= additionalLemmas
.end();
1846 Debug("lemma-ites") << " + " << *i
<< endl
;
1848 Debug("lemma-ites") << endl
;
1851 // assert to prop engine
1852 d_propEngine
->assertLemma(additionalLemmas
[0], negated
, removable
, rule
, node
);
1853 for (unsigned i
= 1; i
< additionalLemmas
.size(); ++ i
) {
1854 additionalLemmas
[i
] = theory::Rewriter::rewrite(additionalLemmas
[i
]);
1855 d_propEngine
->assertLemma(additionalLemmas
[i
], false, removable
, rule
, node
);
1858 // WARNING: Below this point don't assume additionalLemmas[0] to be not negated.
1860 additionalLemmas
[0] = additionalLemmas
[0].notNode();
1864 // assert to decision engine
1866 d_decisionEngine
->addAssertions(additionalLemmas
, 1, iteSkolemMap
);
1869 // Mark that we added some lemmas
1870 d_lemmasAdded
= true;
1872 // Lemma analysis isn't online yet; this lemma may only live for this
1874 return theory::LemmaStatus(additionalLemmas
[0], d_userContext
->getLevel());
1877 void TheoryEngine::conflict(TNode conflict
, TheoryId theoryId
) {
1879 Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict
<< ", " << theoryId
<< ")" << endl
;
1881 // Mark that we are in conflict
1882 d_inConflict
= true;
1884 if(Dump
.isOn("t-conflicts")) {
1885 Dump("t-conflicts") << CommentCommand("theory conflict: expect unsat")
1886 << CheckSatCommand(conflict
.toExpr());
1889 LemmaProofRecipe
* proofRecipe
= NULL
;
1891 proofRecipe
= new LemmaProofRecipe
;
1893 LemmaProofRecipe::ProofStep
proofStep(theoryId
, emptyNode
);
1895 if (conflict
.getKind() == kind::AND
) {
1896 for (unsigned i
= 0; i
< conflict
.getNumChildren(); ++i
) {
1897 proofStep
.addAssertion(conflict
[i
].negate());
1900 proofStep
.addAssertion(conflict
.negate());
1903 proofRecipe
->addStep(proofStep
);
1906 // In the multiple-theories case, we need to reconstruct the conflict
1907 if (d_logicInfo
.isSharingEnabled()) {
1908 // Create the workplace for explanations
1909 std::vector
<NodeTheoryPair
> explanationVector
;
1910 explanationVector
.push_back(NodeTheoryPair(conflict
, theoryId
, d_propagationMapTimestamp
));
1912 // Process the explanation
1913 getExplanation(explanationVector
, proofRecipe
);
1914 PROOF(ProofManager::getCnfProof()->setProofRecipe(proofRecipe
));
1915 Node fullConflict
= mkExplanation(explanationVector
);
1916 Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict
<< ", " << theoryId
<< "): full = " << fullConflict
<< endl
;
1917 Assert(properConflict(fullConflict
));
1918 lemma(fullConflict
, RULE_CONFLICT
, true, true, false, THEORY_LAST
);
1921 // When only one theory, the conflict should need no processing
1922 Assert(properConflict(conflict
));
1924 if (conflict
.getKind() == kind::AND
) {
1925 // If the conflict is a conjunction, the corresponding lemma is derived by negating
1927 for (unsigned i
= 0; i
< conflict
.getNumChildren(); ++i
) {
1928 if (conflict
[i
].isConst() && conflict
[i
].getConst
<bool>()) {
1932 if (conflict
[i
].getKind() == kind::NOT
&&
1933 conflict
[i
][0].isConst() && !conflict
[i
][0].getConst
<bool>()) {
1937 proofRecipe
->getStep(0)->addAssertion(conflict
[i
].negate());
1938 proofRecipe
->addBaseAssertion(conflict
[i
].negate());
1941 proofRecipe
->getStep(0)->addAssertion(conflict
.negate());
1942 proofRecipe
->addBaseAssertion(conflict
.negate());
1945 ProofManager::getCnfProof()->setProofRecipe(proofRecipe
);
1948 lemma(conflict
, RULE_CONFLICT
, true, true, false, THEORY_LAST
);
1957 void TheoryEngine::staticInitializeBVOptions(
1958 const std::vector
<Node
>& assertions
)
1960 bool useSlicer
= true;
1961 if (options::bitvectorEqualitySlicer() == bv::BITVECTOR_SLICER_ON
)
1963 if (!d_logicInfo
.isPure(theory::THEORY_BV
) || d_logicInfo
.isQuantified())
1964 throw ModalException(
1965 "Slicer currently only supports pure QF_BV formulas. Use "
1966 "--bv-eq-slicer=off");
1967 if (options::incrementalSolving())
1968 throw ModalException(
1969 "Slicer does not currently support incremental mode. Use "
1970 "--bv-eq-slicer=off");
1971 if (options::produceModels())
1972 throw ModalException(
1973 "Slicer does not currently support model generation. Use "
1974 "--bv-eq-slicer=off");
1976 else if (options::bitvectorEqualitySlicer() == bv::BITVECTOR_SLICER_OFF
)
1980 else if (options::bitvectorEqualitySlicer() == bv::BITVECTOR_SLICER_AUTO
)
1982 if ((!d_logicInfo
.isPure(theory::THEORY_BV
) || d_logicInfo
.isQuantified())
1983 || options::incrementalSolving()
1984 || options::produceModels())
1987 bv::utils::TNodeBoolMap cache
;
1988 for (unsigned i
= 0; i
< assertions
.size(); ++i
)
1990 useSlicer
= useSlicer
&& bv::utils::isCoreTerm(assertions
[i
], cache
);
1996 bv::TheoryBV
* bv_theory
= (bv::TheoryBV
*)d_theoryTable
[THEORY_BV
];
1997 bv_theory
->enableCoreTheorySlicer();
2001 Node
TheoryEngine::ppSimpITE(TNode assertion
)
2003 if (!d_iteUtilities
->containsTermITE(assertion
))
2007 Node result
= d_iteUtilities
->simpITE(assertion
);
2008 Node res_rewritten
= Rewriter::rewrite(result
);
2010 if(options::simplifyWithCareEnabled()){
2011 Chat() << "starting simplifyWithCare()" << endl
;
2012 Node postSimpWithCare
= d_iteUtilities
->simplifyWithCare(res_rewritten
);
2013 Chat() << "ending simplifyWithCare()"
2014 << " post simplifyWithCare()" << postSimpWithCare
.getId() << endl
;
2015 result
= Rewriter::rewrite(postSimpWithCare
);
2017 result
= res_rewritten
;
2023 bool TheoryEngine::donePPSimpITE(std::vector
<Node
>& assertions
){
2024 // This pass does not support dependency tracking yet
2025 // (learns substitutions from all assertions so just
2026 // adding addDependence is not enough)
2027 if (options::unsatCores() || options::fewerPreprocessingHoles()) {
2031 bool simpDidALotOfWork
= d_iteUtilities
->simpIteDidALotOfWorkHeuristic();
2032 if(simpDidALotOfWork
){
2033 if(options::compressItes()){
2034 result
= d_iteUtilities
->compress(assertions
);
2038 // if false, don't bother to reclaim memory here.
2039 NodeManager
* nm
= NodeManager::currentNM();
2040 if(nm
->poolSize() >= options::zombieHuntThreshold()){
2041 Chat() << "..ite simplifier did quite a bit of work.. " << nm
->poolSize() << endl
;
2042 Chat() << "....node manager contains " << nm
->poolSize() << " nodes before cleanup" << endl
;
2043 d_iteUtilities
->clear();
2044 Rewriter::clearCaches();
2045 nm
->reclaimZombiesUntil(options::zombieHuntThreshold());
2046 Chat() << "....node manager contains " << nm
->poolSize() << " nodes after cleanup" << endl
;
2051 // Do theory specific preprocessing passes
2052 if(d_logicInfo
.isTheoryEnabled(theory::THEORY_ARITH
)
2053 && !options::incrementalSolving() ){
2054 if(!simpDidALotOfWork
){
2055 ContainsTermITEVisitor
& contains
=
2056 *(d_iteUtilities
->getContainsVisitor());
2057 arith::ArithIteUtils
aiteu(contains
, d_userContext
, getModel());
2058 bool anyItes
= false;
2059 for(size_t i
= 0; i
< assertions
.size(); ++i
){
2060 Node curr
= assertions
[i
];
2061 if(contains
.containsTermITE(curr
)){
2063 Node res
= aiteu
.reduceVariablesInItes(curr
);
2064 Debug("arith::ite::red") << "@ " << i
<< " ... " << curr
<< endl
<< " ->" << res
<< endl
;
2066 Node more
= aiteu
.reduceConstantIteByGCD(res
);
2067 Debug("arith::ite::red") << " gcd->" << more
<< endl
;
2068 assertions
[i
] = Rewriter::rewrite(more
);
2073 unsigned prevSubCount
= aiteu
.getSubCount();
2074 aiteu
.learnSubstitutions(assertions
);
2075 if(prevSubCount
< aiteu
.getSubCount()){
2076 d_arithSubstitutionsAdded
+= aiteu
.getSubCount() - prevSubCount
;
2077 bool anySuccess
= false;
2078 for(size_t i
= 0, N
= assertions
.size(); i
< N
; ++i
){
2079 Node curr
= assertions
[i
];
2080 Node next
= Rewriter::rewrite(aiteu
.applySubstitutions(curr
));
2081 Node res
= aiteu
.reduceVariablesInItes(next
);
2082 Debug("arith::ite::red") << "@ " << i
<< " ... " << next
<< endl
<< " ->" << res
<< endl
;
2083 Node more
= aiteu
.reduceConstantIteByGCD(res
);
2084 Debug("arith::ite::red") << " gcd->" << more
<< endl
;
2090 for(size_t i
= 0, N
= assertions
.size(); anySuccess
&& i
< N
; ++i
){
2091 Node curr
= assertions
[i
];
2092 Node next
= Rewriter::rewrite(aiteu
.applySubstitutions(curr
));
2093 Node res
= aiteu
.reduceVariablesInItes(next
);
2094 Debug("arith::ite::red") << "@ " << i
<< " ... " << next
<< endl
<< " ->" << res
<< endl
;
2095 Node more
= aiteu
.reduceConstantIteByGCD(res
);
2096 Debug("arith::ite::red") << " gcd->" << more
<< endl
;
2097 assertions
[i
] = Rewriter::rewrite(more
);
2106 void TheoryEngine::getExplanation(std::vector
<NodeTheoryPair
>& explanationVector
, LemmaProofRecipe
* proofRecipe
) {
2107 Assert(explanationVector
.size() > 0);
2109 unsigned i
= 0; // Index of the current literal we are processing
2110 unsigned j
= 0; // Index of the last literal we are keeping
2112 std::set
<Node
> inputAssertions
;
2113 PROOF(inputAssertions
= proofRecipe
->getStep(0)->getAssertions(););
2115 while (i
< explanationVector
.size()) {
2116 // Get the current literal to explain
2117 NodeTheoryPair toExplain
= explanationVector
[i
];
2119 Debug("theory::explain") << "[i=" << i
<< "] TheoryEngine::explain(): processing [" << toExplain
.timestamp
<< "] " << toExplain
.node
<< " sent from " << toExplain
.theory
<< endl
;
2122 // If a true constant or a negation of a false constant we can ignore it
2123 if (toExplain
.node
.isConst() && toExplain
.node
.getConst
<bool>()) {
2127 if (toExplain
.node
.getKind() == kind::NOT
&& toExplain
.node
[0].isConst() && !toExplain
.node
[0].getConst
<bool>()) {
2132 // If from the SAT solver, keep it
2133 if (toExplain
.theory
== THEORY_SAT_SOLVER
) {
2134 Debug("theory::explain") << "\tLiteral came from THEORY_SAT_SOLVER. Kepping it." << endl
;
2135 explanationVector
[j
++] = explanationVector
[i
++];
2139 // If an and, expand it
2140 if (toExplain
.node
.getKind() == kind::AND
) {
2141 Debug("theory::explain") << "TheoryEngine::explain(): expanding " << toExplain
.node
<< " got from " << toExplain
.theory
<< endl
;
2142 for (unsigned k
= 0; k
< toExplain
.node
.getNumChildren(); ++ k
) {
2143 NodeTheoryPair
newExplain(toExplain
.node
[k
], toExplain
.theory
, toExplain
.timestamp
);
2144 explanationVector
.push_back(newExplain
);
2150 // See if it was sent to the theory by another theory
2151 PropagationMap::const_iterator find
= d_propagationMap
.find(toExplain
);
2152 if (find
!= d_propagationMap
.end()) {
2153 Debug("theory::explain") << "\tTerm was propagated by another theory (theory = "
2154 << theoryOf((*find
).second
.theory
)->getId() << ")" << std::endl
;
2155 // There is some propagation, check if its a timely one
2156 if ((*find
).second
.timestamp
< toExplain
.timestamp
) {
2157 Debug("theory::explain") << "\tRelevant timetsamp, pushing "
2158 << (*find
).second
.node
<< "to index = " << explanationVector
.size() << std::endl
;
2159 explanationVector
.push_back((*find
).second
);
2163 if (toExplain
.node
!= (*find
).second
.node
) {
2164 Debug("pf::explain") << "TheoryEngine::getExplanation: Rewrite alert! toAssert = " << toExplain
.node
2165 << ", toExplain = " << (*find
).second
.node
<< std::endl
;
2168 proofRecipe
->addRewriteRule(toExplain
.node
, (*find
).second
.node
);
2177 // It was produced by the theory, so ask for an explanation
2179 if (toExplain
.theory
== THEORY_BUILTIN
) {
2180 explanation
= d_sharedTerms
.explain(toExplain
.node
);
2181 Debug("theory::explain") << "\tTerm was propagated by THEORY_BUILTIN. Explanation: " << explanation
<< std::endl
;
2183 explanation
= theoryOf(toExplain
.theory
)->explain(toExplain
.node
);
2184 Debug("theory::explain") << "\tTerm was propagated by owner theory: "
2185 << theoryOf(toExplain
.theory
)->getId()
2186 << ". Explanation: " << explanation
<< std::endl
;
2189 Debug("theory::explain") << "TheoryEngine::explain(): got explanation " << explanation
<< " got from " << toExplain
.theory
<< endl
;
2190 Assert( explanation
!= toExplain
.node
, "wasn't sent to you, so why are you explaining it trivially");
2191 // Mark the explanation
2192 NodeTheoryPair
newExplain(explanation
, toExplain
.theory
, toExplain
.timestamp
);
2193 explanationVector
.push_back(newExplain
);
2199 // If we're expanding the target node of the explanation (this is the first expansion...),
2200 // we don't want to add it as a separate proof step. It is already part of the assertions.
2201 if (inputAssertions
.find(toExplain
.node
) == inputAssertions
.end()) {
2202 LemmaProofRecipe::ProofStep
proofStep(toExplain
.theory
, toExplain
.node
);
2203 if (explanation
.getKind() == kind::AND
) {
2204 Node flat
= flattenAnd(explanation
);
2205 for (unsigned k
= 0; k
< flat
.getNumChildren(); ++ k
) {
2206 // If a true constant or a negation of a false constant we can ignore it
2207 if (! ((flat
[k
].isConst() && flat
[k
].getConst
<bool>()) ||
2208 (flat
[k
].getKind() == kind::NOT
&& flat
[k
][0].isConst() && !flat
[k
][0].getConst
<bool>()))) {
2209 proofStep
.addAssertion(flat
[k
].negate());
2213 if (! ((explanation
.isConst() && explanation
.getConst
<bool>()) ||
2214 (explanation
.getKind() == kind::NOT
&& explanation
[0].isConst() && !explanation
[0].getConst
<bool>()))) {
2215 proofStep
.addAssertion(explanation
.negate());
2218 proofRecipe
->addStep(proofStep
);
2224 // Keep only the relevant literals
2225 explanationVector
.resize(j
);
2229 // The remaining literals are the base of the proof
2230 for (unsigned k
= 0; k
< explanationVector
.size(); ++k
) {
2231 proofRecipe
->addBaseAssertion(explanationVector
[k
].node
.negate());
2237 void TheoryEngine::ppUnconstrainedSimp(vector
<Node
>& assertions
)
2239 d_unconstrainedSimp
->processAssertions(assertions
);
2242 void TheoryEngine::setUserAttribute(const std::string
& attr
,
2244 const std::vector
<Node
>& node_values
,
2245 const std::string
& str_value
)
2247 Trace("te-attr") << "set user attribute " << attr
<< " " << n
<< endl
;
2248 if( d_attr_handle
.find( attr
)!=d_attr_handle
.end() ){
2249 for( size_t i
=0; i
<d_attr_handle
[attr
].size(); i
++ ){
2250 d_attr_handle
[attr
][i
]->setUserAttribute(attr
, n
, node_values
, str_value
);
2253 //unhandled exception?
2257 void TheoryEngine::handleUserAttribute(const char* attr
, Theory
* t
) {
2258 Trace("te-attr") << "Handle user attribute " << attr
<< " " << t
<< endl
;
2259 std::string
str( attr
);
2260 d_attr_handle
[ str
].push_back( t
);
2263 void TheoryEngine::checkTheoryAssertionsWithModel(bool hardFailure
) {
2264 for(TheoryId theoryId
= THEORY_FIRST
; theoryId
< THEORY_LAST
; ++theoryId
) {
2265 Theory
* theory
= d_theoryTable
[theoryId
];
2266 if(theory
&& d_logicInfo
.isTheoryEnabled(theoryId
)) {
2267 for(context::CDList
<Assertion
>::const_iterator it
= theory
->facts_begin(),
2268 it_end
= theory
->facts_end();
2271 Node assertion
= (*it
).assertion
;
2272 Node val
= getModel()->getValue(assertion
);
2275 ss
<< theoryId
<< " has an asserted fact that the model doesn't satisfy." << endl
2276 << "The fact: " << assertion
<< endl
2277 << "Model value: " << val
<< endl
;
2279 InternalError(ss
.str());
2287 std::pair
<bool, Node
> TheoryEngine::entailmentCheck(theory::TheoryOfMode mode
, TNode lit
, const EntailmentCheckParameters
* params
, EntailmentCheckSideEffects
* seffects
) {
2288 TNode atom
= (lit
.getKind() == kind::NOT
) ? lit
[0] : lit
;
2289 if( atom
.getKind()==kind::AND
|| atom
.getKind()==kind::OR
|| atom
.getKind()==kind::IMPLIES
){
2290 //Boolean connective, recurse
2291 std::vector
< Node
> children
;
2292 bool pol
= (lit
.getKind()!=kind::NOT
);
2293 bool is_conjunction
= pol
==(lit
.getKind()==kind::AND
);
2294 for( unsigned i
=0; i
<atom
.getNumChildren(); i
++ ){
2296 if( pol
==( lit
.getKind()==kind::IMPLIES
&& i
==0 ) ){
2297 ch
= atom
[i
].negate();
2299 std::pair
<bool, Node
> chres
= entailmentCheck( mode
, ch
, params
, seffects
);
2301 if( !is_conjunction
){
2304 children
.push_back( chres
.second
);
2306 }else if( !chres
.first
&& is_conjunction
){
2307 return std::pair
<bool, Node
>(false, Node::null());
2310 if( is_conjunction
){
2311 return std::pair
<bool, Node
>(true, NodeManager::currentNM()->mkNode(kind::AND
, children
));
2313 return std::pair
<bool, Node
>(false, Node::null());
2315 }else if( atom
.getKind()==kind::ITE
|| ( atom
.getKind()==kind::EQUAL
&& atom
[0].getType().isBoolean() ) ){
2316 bool pol
= (lit
.getKind()!=kind::NOT
);
2317 for( unsigned r
=0; r
<2; r
++ ){
2322 std::pair
<bool, Node
> chres
= entailmentCheck( mode
, ch
, params
, seffects
);
2324 Node ch2
= atom
[ atom
.getKind()==kind::ITE
? r
+1 : 1 ];
2325 if( pol
==( atom
.getKind()==kind::ITE
? true : r
==1 ) ){
2328 std::pair
<bool, Node
> chres2
= entailmentCheck( mode
, ch2
, params
, seffects
);
2330 return std::pair
<bool, Node
>(true, NodeManager::currentNM()->mkNode(kind::AND
, chres
.second
, chres2
.second
));
2336 return std::pair
<bool, Node
>(false, Node::null());
2338 //it is a theory atom
2339 theory::TheoryId tid
= theory::Theory::theoryOf(mode
, atom
);
2340 theory::Theory
* th
= theoryOf(tid
);
2343 Assert(params
== NULL
|| tid
== params
->getTheoryId());
2344 Assert(seffects
== NULL
|| tid
== seffects
->getTheoryId());
2345 Trace("theory-engine-entc") << "Entailment check : " << lit
<< std::endl
;
2347 std::pair
<bool, Node
> chres
= th
->entailmentCheck(lit
, params
, seffects
);
2352 void TheoryEngine::spendResource(unsigned amount
)
2354 d_resourceManager
->spendResource(amount
);
2357 void TheoryEngine::enableTheoryAlternative(const std::string
& name
){
2358 Debug("TheoryEngine::enableTheoryAlternative")
2359 << "TheoryEngine::enableTheoryAlternative(" << name
<< ")" << std::endl
;
2361 d_theoryAlternatives
.insert(name
);
2364 bool TheoryEngine::useTheoryAlternative(const std::string
& name
) {
2365 return d_theoryAlternatives
.find(name
) != d_theoryAlternatives
.end();
2369 TheoryEngine::Statistics::Statistics(theory::TheoryId theory
):
2370 conflicts(getStatsPrefix(theory
) + "::conflicts", 0),
2371 propagations(getStatsPrefix(theory
) + "::propagations", 0),
2372 lemmas(getStatsPrefix(theory
) + "::lemmas", 0),
2373 requirePhase(getStatsPrefix(theory
) + "::requirePhase", 0),
2374 flipDecision(getStatsPrefix(theory
) + "::flipDecision", 0),
2375 restartDemands(getStatsPrefix(theory
) + "::restartDemands", 0)
2377 smtStatisticsRegistry()->registerStat(&conflicts
);
2378 smtStatisticsRegistry()->registerStat(&propagations
);
2379 smtStatisticsRegistry()->registerStat(&lemmas
);
2380 smtStatisticsRegistry()->registerStat(&requirePhase
);
2381 smtStatisticsRegistry()->registerStat(&flipDecision
);
2382 smtStatisticsRegistry()->registerStat(&restartDemands
);
2385 TheoryEngine::Statistics::~Statistics() {
2386 smtStatisticsRegistry()->unregisterStat(&conflicts
);
2387 smtStatisticsRegistry()->unregisterStat(&propagations
);
2388 smtStatisticsRegistry()->unregisterStat(&lemmas
);
2389 smtStatisticsRegistry()->unregisterStat(&requirePhase
);
2390 smtStatisticsRegistry()->unregisterStat(&flipDecision
);
2391 smtStatisticsRegistry()->unregisterStat(&restartDemands
);
2394 }/* CVC4 namespace */