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 "base/map_util.h"
23 #include "decision/decision_engine.h"
24 #include "expr/attribute.h"
25 #include "expr/node.h"
26 #include "expr/node_algorithm.h"
27 #include "expr/node_builder.h"
28 #include "options/bv_options.h"
29 #include "options/options.h"
30 #include "options/proof_options.h"
31 #include "options/quantifiers_options.h"
32 #include "proof/cnf_proof.h"
33 #include "proof/lemma_proof.h"
34 #include "proof/proof_manager.h"
35 #include "proof/theory_proof.h"
36 #include "smt/logic_exception.h"
37 #include "smt/term_formula_removal.h"
38 #include "smt_util/lemma_output_channel.h"
39 #include "smt_util/node_visitor.h"
40 #include "theory/arith/arith_ite_utils.h"
41 #include "theory/bv/theory_bv_utils.h"
42 #include "theory/care_graph.h"
43 #include "theory/quantifiers/first_order_model.h"
44 #include "theory/quantifiers/fmf/model_engine.h"
45 #include "theory/quantifiers/theory_quantifiers.h"
46 #include "theory/quantifiers_engine.h"
47 #include "theory/rewriter.h"
48 #include "theory/theory.h"
49 #include "theory/theory_model.h"
50 #include "theory/theory_traits.h"
51 #include "theory/uf/equality_engine.h"
52 #include "theory/unconstrained_simplifier.h"
53 #include "util/resource_manager.h"
57 using namespace CVC4::theory
;
61 inline void flattenAnd(Node n
, std::vector
<TNode
>& out
){
62 Assert(n
.getKind() == kind::AND
);
63 for(Node::iterator i
=n
.begin(), i_end
=n
.end(); i
!= i_end
; ++i
){
65 if(curr
.getKind() == kind::AND
){
66 flattenAnd(curr
, out
);
73 inline Node
flattenAnd(Node n
){
74 std::vector
<TNode
> out
;
76 return NodeManager::currentNM()->mkNode(kind::AND
, out
);
79 theory::LemmaStatus
TheoryEngine::EngineOutputChannel::lemma(TNode lemma
,
84 Debug("theory::lemma") << "EngineOutputChannel<" << d_theory
<< ">::lemma("
86 << ", preprocess = " << preprocess
<< std::endl
;
87 ++d_statistics
.lemmas
;
88 d_engine
->d_outputChannelUsed
= true;
90 PROOF({ registerLemmaRecipe(lemma
, lemma
, preprocess
, d_theory
); });
92 theory::LemmaStatus result
=
93 d_engine
->lemma(lemma
, rule
, false, removable
, preprocess
,
94 sendAtoms
? d_theory
: theory::THEORY_LAST
);
98 void TheoryEngine::EngineOutputChannel::registerLemmaRecipe(Node lemma
, Node originalLemma
, bool preprocess
, theory::TheoryId theoryId
) {
99 // During CNF conversion, conjunctions will be broken down into
100 // multiple lemmas. In order for the recipes to match, we have to do
102 NodeManager
* nm
= NodeManager::currentNM();
105 lemma
= d_engine
->preprocess(lemma
);
107 bool negated
= (lemma
.getKind() == kind::NOT
);
108 Node nnLemma
= negated
? lemma
[0] : lemma
;
110 switch (nnLemma
.getKind()) {
114 for (unsigned i
= 0; i
< nnLemma
.getNumChildren(); ++i
)
115 registerLemmaRecipe(nnLemma
[i
], originalLemma
, false, theoryId
);
117 NodeBuilder
<> builder(kind::OR
);
118 for (unsigned i
= 0; i
< nnLemma
.getNumChildren(); ++i
)
119 builder
<< nnLemma
[i
].negate();
121 Node disjunction
= (builder
.getNumChildren() == 1) ? builder
[0] : builder
;
122 registerLemmaRecipe(disjunction
, originalLemma
, false, theoryId
);
127 if( nnLemma
[0].getType().isBoolean() ){
129 registerLemmaRecipe(nm
->mkNode(kind::OR
, nnLemma
[0], nnLemma
[1].negate()), originalLemma
, false, theoryId
);
130 registerLemmaRecipe(nm
->mkNode(kind::OR
, nnLemma
[0].negate(), nnLemma
[1]), originalLemma
, false, theoryId
);
132 registerLemmaRecipe(nm
->mkNode(kind::OR
, nnLemma
[0], nnLemma
[1]), originalLemma
, false, theoryId
);
133 registerLemmaRecipe(nm
->mkNode(kind::OR
, nnLemma
[0].negate(), nnLemma
[1].negate()), originalLemma
, false, theoryId
);
140 registerLemmaRecipe(nm
->mkNode(kind::OR
, nnLemma
[0].negate(), nnLemma
[1]), originalLemma
, false, theoryId
);
141 registerLemmaRecipe(nm
->mkNode(kind::OR
, nnLemma
[0], nnLemma
[2]), originalLemma
, false, theoryId
);
143 registerLemmaRecipe(nm
->mkNode(kind::OR
, nnLemma
[0].negate(), nnLemma
[1].negate()), originalLemma
, false, theoryId
);
144 registerLemmaRecipe(nm
->mkNode(kind::OR
, nnLemma
[0], nnLemma
[2].negate()), originalLemma
, false, theoryId
);
152 // Theory lemmas have one step that proves the empty clause
153 LemmaProofRecipe proofRecipe
;
155 LemmaProofRecipe::ProofStep
proofStep(theoryId
, emptyNode
);
157 // Remember the original lemma, so we can report this later when asked to
158 proofRecipe
.setOriginalLemma(originalLemma
);
160 // Record the assertions and rewrites
162 if (lemma
.getKind() == kind::OR
) {
163 for (unsigned i
= 0; i
< lemma
.getNumChildren(); ++i
) {
164 rewritten
= theory::Rewriter::rewrite(lemma
[i
]);
165 if (rewritten
!= lemma
[i
]) {
166 proofRecipe
.addRewriteRule(lemma
[i
].negate(), rewritten
.negate());
168 proofStep
.addAssertion(lemma
[i
]);
169 proofRecipe
.addBaseAssertion(rewritten
);
172 rewritten
= theory::Rewriter::rewrite(lemma
);
173 if (rewritten
!= lemma
) {
174 proofRecipe
.addRewriteRule(lemma
.negate(), rewritten
.negate());
176 proofStep
.addAssertion(lemma
);
177 proofRecipe
.addBaseAssertion(rewritten
);
179 proofRecipe
.addStep(proofStep
);
180 ProofManager::getCnfProof()->setProofRecipe(&proofRecipe
);
183 theory::LemmaStatus
TheoryEngine::EngineOutputChannel::splitLemma(
184 TNode lemma
, bool removable
) {
185 Debug("theory::lemma") << "EngineOutputChannel<" << d_theory
<< ">::lemma("
186 << lemma
<< ")" << std::endl
;
187 ++d_statistics
.lemmas
;
188 d_engine
->d_outputChannelUsed
= true;
190 Debug("pf::explain") << "TheoryEngine::EngineOutputChannel::splitLemma( "
191 << lemma
<< " )" << std::endl
;
192 theory::LemmaStatus result
=
193 d_engine
->lemma(lemma
, RULE_SPLIT
, false, removable
, false, d_theory
);
197 bool TheoryEngine::EngineOutputChannel::propagate(TNode literal
) {
198 Debug("theory::propagate") << "EngineOutputChannel<" << d_theory
199 << ">::propagate(" << literal
<< ")" << std::endl
;
200 ++d_statistics
.propagations
;
201 d_engine
->d_outputChannelUsed
= true;
202 return d_engine
->propagate(literal
, d_theory
);
205 void TheoryEngine::EngineOutputChannel::conflict(TNode conflictNode
,
206 std::unique_ptr
<Proof
> proof
)
208 Trace("theory::conflict")
209 << "EngineOutputChannel<" << d_theory
<< ">::conflict(" << conflictNode
211 Assert(!proof
); // Theory shouldn't be producing proofs yet
212 ++d_statistics
.conflicts
;
213 d_engine
->d_outputChannelUsed
= true;
214 d_engine
->conflict(conflictNode
, d_theory
);
217 void TheoryEngine::finishInit() {
219 //initialize the quantifiers engine, master equality engine, model, model builder
220 if( d_logicInfo
.isQuantified() ) {
221 // initialize the quantifiers engine
222 d_quantEngine
= new QuantifiersEngine(d_context
, d_userContext
, this);
223 Assert(d_masterEqualityEngine
== 0);
224 d_masterEqualityEngine
= new eq::EqualityEngine(d_masterEENotify
,getSatContext(), "theory::master", false);
226 for(TheoryId theoryId
= theory::THEORY_FIRST
; theoryId
!= theory::THEORY_LAST
; ++ theoryId
) {
227 if (d_theoryTable
[theoryId
]) {
228 d_theoryTable
[theoryId
]->setQuantifiersEngine(d_quantEngine
);
229 d_theoryTable
[theoryId
]->setMasterEqualityEngine(d_masterEqualityEngine
);
233 d_curr_model_builder
= d_quantEngine
->getModelBuilder();
234 d_curr_model
= d_quantEngine
->getModel();
236 d_curr_model
= new theory::TheoryModel(
237 d_userContext
, "DefaultModel", options::assignFunctionValues());
238 d_aloc_curr_model
= true;
240 //make the default builder, e.g. in the case that the quantifiers engine does not have a model builder
241 if( d_curr_model_builder
==NULL
){
242 d_curr_model_builder
= new theory::TheoryEngineModelBuilder(this);
243 d_aloc_curr_model_builder
= true;
246 for(TheoryId theoryId
= theory::THEORY_FIRST
; theoryId
!= theory::THEORY_LAST
; ++ theoryId
) {
247 if (d_theoryTable
[theoryId
]) {
248 d_theoryTable
[theoryId
]->finishInit();
253 void TheoryEngine::eqNotifyNewClass(TNode t
){
254 if (d_logicInfo
.isQuantified()) {
255 d_quantEngine
->eqNotifyNewClass( t
);
259 void TheoryEngine::eqNotifyPreMerge(TNode t1
, TNode t2
){
260 if (d_logicInfo
.isQuantified()) {
261 d_quantEngine
->eqNotifyPreMerge( t1
, t2
);
265 void TheoryEngine::eqNotifyPostMerge(TNode t1
, TNode t2
){
266 if (d_logicInfo
.isQuantified()) {
267 d_quantEngine
->eqNotifyPostMerge( t1
, t2
);
271 void TheoryEngine::eqNotifyDisequal(TNode t1
, TNode t2
, TNode reason
){
272 if (d_logicInfo
.isQuantified()) {
273 d_quantEngine
->eqNotifyDisequal( t1
, t2
, reason
);
278 TheoryEngine::TheoryEngine(context::Context
* context
,
279 context::UserContext
* userContext
,
280 RemoveTermFormulas
& iteRemover
,
281 const LogicInfo
& logicInfo
,
282 LemmaChannels
* channels
)
283 : d_propEngine(NULL
),
284 d_decisionEngine(NULL
),
286 d_userContext(userContext
),
287 d_logicInfo(logicInfo
),
288 d_sharedTerms(this, context
),
289 d_masterEqualityEngine(NULL
),
290 d_masterEENotify(*this),
293 d_aloc_curr_model(false),
294 d_curr_model_builder(NULL
),
295 d_aloc_curr_model_builder(false),
297 d_possiblePropagations(context
),
298 d_hasPropagated(context
),
299 d_inConflict(context
, false),
300 d_hasShutDown(false),
301 d_incomplete(context
, false),
302 d_propagationMap(context
),
303 d_propagationMapTimestamp(context
, 0),
304 d_propagatedLiterals(context
),
305 d_propagatedLiteralsIndex(context
, 0),
306 d_atomRequests(context
),
307 d_tform_remover(iteRemover
),
308 d_combineTheoriesTime("TheoryEngine::combineTheoriesTime"),
311 d_interrupted(false),
312 d_resourceManager(NodeManager::currentResourceManager()),
313 d_channels(channels
),
314 d_inPreregister(false),
315 d_factsAsserted(context
, false),
316 d_preRegistrationVisitor(this, context
),
317 d_sharedTermsVisitor(d_sharedTerms
),
318 d_unconstrainedSimp(new UnconstrainedSimplifier(context
, logicInfo
)),
319 d_theoryAlternatives(),
321 d_arithSubstitutionsAdded("theory::arith::zzz::arith::substitutions", 0)
323 for(TheoryId theoryId
= theory::THEORY_FIRST
; theoryId
!= theory::THEORY_LAST
;
326 d_theoryTable
[theoryId
] = NULL
;
327 d_theoryOut
[theoryId
] = NULL
;
330 smtStatisticsRegistry()->registerStat(&d_combineTheoriesTime
);
331 d_true
= NodeManager::currentNM()->mkConst
<bool>(true);
332 d_false
= NodeManager::currentNM()->mkConst
<bool>(false);
335 ProofManager::currentPM()->initTheoryProofEngine();
338 smtStatisticsRegistry()->registerStat(&d_arithSubstitutionsAdded
);
341 TheoryEngine::~TheoryEngine() {
342 Assert(d_hasShutDown
);
344 for(TheoryId theoryId
= theory::THEORY_FIRST
; theoryId
!= theory::THEORY_LAST
; ++ theoryId
) {
345 if(d_theoryTable
[theoryId
] != NULL
) {
346 delete d_theoryTable
[theoryId
];
347 delete d_theoryOut
[theoryId
];
351 if( d_aloc_curr_model_builder
){
352 delete d_curr_model_builder
;
354 if( d_aloc_curr_model
){
358 delete d_quantEngine
;
360 delete d_masterEqualityEngine
;
362 smtStatisticsRegistry()->unregisterStat(&d_combineTheoriesTime
);
364 delete d_unconstrainedSimp
;
366 smtStatisticsRegistry()->unregisterStat(&d_arithSubstitutionsAdded
);
369 void TheoryEngine::interrupt() { d_interrupted
= true; }
370 void TheoryEngine::preRegister(TNode preprocessed
) {
372 Debug("theory") << "TheoryEngine::preRegister( " << preprocessed
<< ")" << std::endl
;
373 if(Dump
.isOn("missed-t-propagations")) {
374 d_possiblePropagations
.push_back(preprocessed
);
376 d_preregisterQueue
.push(preprocessed
);
378 if (!d_inPreregister
) {
379 // We're in pre-register
380 d_inPreregister
= true;
382 // Process the pre-registration queue
383 while (!d_preregisterQueue
.empty()) {
384 // Get the next atom to pre-register
385 preprocessed
= d_preregisterQueue
.front();
386 d_preregisterQueue
.pop();
388 if (d_logicInfo
.isSharingEnabled() && preprocessed
.getKind() == kind::EQUAL
) {
389 // When sharing is enabled, we propagate from the shared terms manager also
390 d_sharedTerms
.addEqualityToPropagate(preprocessed
);
393 // the atom should not have free variables
394 Debug("theory") << "TheoryEngine::preRegister: " << preprocessed
396 Assert(!expr::hasFreeVar(preprocessed
));
397 // Pre-register the terms in the atom
398 Theory::Set theories
= NodeVisitor
<PreRegisterVisitor
>::run(d_preRegistrationVisitor
, preprocessed
);
399 theories
= Theory::setRemove(THEORY_BOOL
, theories
);
400 // Remove the top theory, if any more that means multiple theories were involved
401 bool multipleTheories
= Theory::setRemove(Theory::theoryOf(preprocessed
), theories
);
403 // These checks don't work with finite model finding, because it
404 // uses Rational constants to represent cardinality constraints,
405 // even though arithmetic isn't actually involved.
406 if(!options::finiteModelFind()) {
407 while((i
= Theory::setPop(theories
)) != THEORY_LAST
) {
408 if(!d_logicInfo
.isTheoryEnabled(i
)) {
409 LogicInfo newLogicInfo
= d_logicInfo
.getUnlockedCopy();
410 newLogicInfo
.enableTheory(i
);
413 ss
<< "The logic was specified as " << d_logicInfo
.getLogicString()
414 << ", which doesn't include " << i
415 << ", but found a term in that theory." << endl
416 << "You might want to extend your logic to "
417 << newLogicInfo
.getLogicString() << endl
;
418 throw LogicException(ss
.str());
422 if (multipleTheories
) {
423 // Collect the shared terms if there are multiple theories
424 NodeVisitor
<SharedTermsVisitor
>::run(d_sharedTermsVisitor
, preprocessed
);
428 // Leaving pre-register
429 d_inPreregister
= false;
433 void TheoryEngine::printAssertions(const char* tag
) {
434 if (Trace
.isOn(tag
)) {
436 for (TheoryId theoryId
= THEORY_FIRST
; theoryId
< THEORY_LAST
; ++theoryId
) {
437 Theory
* theory
= d_theoryTable
[theoryId
];
438 if (theory
&& d_logicInfo
.isTheoryEnabled(theoryId
)) {
439 Trace(tag
) << "--------------------------------------------" << endl
;
440 Trace(tag
) << "Assertions of " << theory
->getId() << ": " << endl
;
441 context::CDList
<Assertion
>::const_iterator it
= theory
->facts_begin(), it_end
= theory
->facts_end();
442 for (unsigned i
= 0; it
!= it_end
; ++ it
, ++i
) {
443 if ((*it
).isPreregistered
) {
444 Trace(tag
) << "[" << i
<< "]: ";
446 Trace(tag
) << "(" << i
<< "): ";
448 Trace(tag
) << (*it
).assertion
<< endl
;
451 if (d_logicInfo
.isSharingEnabled()) {
452 Trace(tag
) << "Shared terms of " << theory
->getId() << ": " << endl
;
453 context::CDList
<TNode
>::const_iterator it
= theory
->shared_terms_begin(), it_end
= theory
->shared_terms_end();
454 for (unsigned i
= 0; it
!= it_end
; ++ it
, ++i
) {
455 Trace(tag
) << "[" << i
<< "]: " << (*it
) << endl
;
463 void TheoryEngine::dumpAssertions(const char* tag
) {
464 if (Dump
.isOn(tag
)) {
465 Dump(tag
) << CommentCommand("Starting completeness check");
466 for (TheoryId theoryId
= THEORY_FIRST
; theoryId
< THEORY_LAST
; ++theoryId
) {
467 Theory
* theory
= d_theoryTable
[theoryId
];
468 if (theory
&& d_logicInfo
.isTheoryEnabled(theoryId
)) {
469 Dump(tag
) << CommentCommand("Completeness check");
470 Dump(tag
) << PushCommand();
472 // Dump the shared terms
473 if (d_logicInfo
.isSharingEnabled()) {
474 Dump(tag
) << CommentCommand("Shared terms");
475 context::CDList
<TNode
>::const_iterator it
= theory
->shared_terms_begin(), it_end
= theory
->shared_terms_end();
476 for (unsigned i
= 0; it
!= it_end
; ++ it
, ++i
) {
479 Dump(tag
) << CommentCommand(ss
.str());
483 // Dump the assertions
484 Dump(tag
) << CommentCommand("Assertions");
485 context::CDList
<Assertion
>::const_iterator it
= theory
->facts_begin(), it_end
= theory
->facts_end();
486 for (; it
!= it_end
; ++ it
) {
488 Node assertionNode
= (*it
).assertion
;
489 // Purify all the terms
491 if ((*it
).isPreregistered
) {
492 Dump(tag
) << CommentCommand("Preregistered");
494 Dump(tag
) << CommentCommand("Shared assertion");
496 Dump(tag
) << AssertCommand(assertionNode
.toExpr());
498 Dump(tag
) << CheckSatCommand();
500 Dump(tag
) << PopCommand();
507 * Check all (currently-active) theories for conflicts.
508 * @param effort the effort level to use
510 void TheoryEngine::check(Theory::Effort effort
) {
513 // Reset the interrupt flag
514 d_interrupted
= false;
516 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
517 #undef CVC4_FOR_EACH_THEORY_STATEMENT
519 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
520 if (theory::TheoryTraits<THEORY>::hasCheck && d_logicInfo.isTheoryEnabled(THEORY)) { \
521 theoryOf(THEORY)->check(effort); \
522 if (d_inConflict) { \
523 Debug("conflict") << THEORY << " in conflict. " << std::endl; \
531 // Mark the output channel unused (if this is FULL_EFFORT, and nothing
532 // is done by the theories, no additional check will be needed)
533 d_outputChannelUsed
= false;
535 // Mark the lemmas flag (no lemmas added)
536 d_lemmasAdded
= false;
538 Debug("theory") << "TheoryEngine::check(" << effort
<< "): d_factsAsserted = " << (d_factsAsserted
? "true" : "false") << endl
;
540 // If in full effort, we have a fake new assertion just to jumpstart the checking
541 if (Theory::fullEffort(effort
)) {
542 d_factsAsserted
= true;
546 while (d_factsAsserted
&& !d_inConflict
&& !d_lemmasAdded
) {
548 Debug("theory") << "TheoryEngine::check(" << effort
<< "): running check" << endl
;
550 Trace("theory::assertions") << endl
;
551 if (Trace
.isOn("theory::assertions")) {
552 printAssertions("theory::assertions");
555 if(Theory::fullEffort(effort
)) {
556 Trace("theory::assertions::fulleffort") << endl
;
557 if (Trace
.isOn("theory::assertions::fulleffort")) {
558 printAssertions("theory::assertions::fulleffort");
562 // Note that we've discharged all the facts
563 d_factsAsserted
= false;
566 CVC4_FOR_EACH_THEORY
;
568 if(Dump
.isOn("missed-t-conflicts")) {
569 Dump("missed-t-conflicts")
570 << CommentCommand("Completeness check for T-conflicts; expect sat")
571 << CheckSatCommand();
574 Debug("theory") << "TheoryEngine::check(" << effort
<< "): running propagation after the initial check" << endl
;
576 // We are still satisfiable, propagate as much as possible
579 // We do combination if all has been processed and we are in fullcheck
580 if (Theory::fullEffort(effort
) && d_logicInfo
.isSharingEnabled() && !d_factsAsserted
&& !d_lemmasAdded
&& !d_inConflict
) {
581 // Do the combination
582 Debug("theory") << "TheoryEngine::check(" << effort
<< "): running combination" << endl
;
584 if(d_logicInfo
.isQuantified()){
585 d_quantEngine
->notifyCombineTheories();
590 // Must consult quantifiers theory for last call to ensure sat, or otherwise add a lemma
591 if( Theory::fullEffort(effort
) && ! d_inConflict
&& ! needCheck() ) {
592 Trace("theory::assertions-model") << endl
;
593 if (Trace
.isOn("theory::assertions-model")) {
594 printAssertions("theory::assertions-model");
596 //checks for theories requiring the model go at last call
597 d_curr_model
->reset();
598 for (TheoryId theoryId
= THEORY_FIRST
; theoryId
< THEORY_LAST
; ++theoryId
) {
599 if( theoryId
!=THEORY_QUANTIFIERS
){
600 Theory
* theory
= d_theoryTable
[theoryId
];
601 if (theory
&& d_logicInfo
.isTheoryEnabled(theoryId
)) {
602 if( theory
->needsCheckLastEffort() ){
603 if( !d_curr_model
->isBuilt() ){
604 if( !d_curr_model_builder
->buildModel(d_curr_model
) ){
608 theory
->check(Theory::EFFORT_LAST_CALL
);
615 if(d_logicInfo
.isQuantified()) {
616 // quantifiers engine must check at last call effort
617 d_quantEngine
->check(Theory::EFFORT_LAST_CALL
);
620 if (!d_inConflict
&& !needCheck())
622 if (options::produceModels() && !d_curr_model
->isBuilt())
624 // must build model at this point
625 d_curr_model_builder
->buildModel(d_curr_model
);
630 Debug("theory") << "TheoryEngine::check(" << effort
<< "): done, we are " << (d_inConflict
? "unsat" : "sat") << (d_lemmasAdded
? " with new lemmas" : " with no new lemmas");
631 Debug("theory") << ", need check = " << (needCheck() ? "YES" : "NO") << endl
;
633 if( Theory::fullEffort(effort
) && !d_inConflict
&& !needCheck()) {
634 // case where we are about to answer SAT
635 if( d_masterEqualityEngine
!= NULL
){
636 AlwaysAssert(d_masterEqualityEngine
->consistent());
638 if (d_curr_model
->isBuilt())
640 // model construction should always succeed unless lemmas were added
641 AlwaysAssert(d_curr_model
->isBuiltSuccess());
642 if (options::produceModels())
644 // if we are incomplete, there is no guarantee on the model.
645 // thus, we do not check the model here. (related to #1693)
646 // we also don't debug-check the model if the checkModels()
648 if (!d_incomplete
&& options::checkModels())
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
;
1467 const LogicInfo
& TheoryEngine::getLogicInfo() const { return d_logicInfo
; }
1469 theory::EqualityStatus
TheoryEngine::getEqualityStatus(TNode a
, TNode b
) {
1470 Assert(a
.getType().isComparableTo(b
.getType()));
1471 if (d_sharedTerms
.isShared(a
) && d_sharedTerms
.isShared(b
)) {
1472 if (d_sharedTerms
.areEqual(a
,b
)) {
1473 return EQUALITY_TRUE_AND_PROPAGATED
;
1475 else if (d_sharedTerms
.areDisequal(a
,b
)) {
1476 return EQUALITY_FALSE_AND_PROPAGATED
;
1479 return theoryOf(Theory::theoryOf(a
.getType()))->getEqualityStatus(a
, b
);
1482 Node
TheoryEngine::getModelValue(TNode var
) {
1485 // the model value of a constant must be itself
1488 Assert(d_sharedTerms
.isShared(var
));
1489 return theoryOf(Theory::theoryOf(var
.getType()))->getModelValue(var
);
1493 Node
TheoryEngine::ensureLiteral(TNode n
) {
1494 Debug("ensureLiteral") << "rewriting: " << n
<< std::endl
;
1495 Node rewritten
= Rewriter::rewrite(n
);
1496 Debug("ensureLiteral") << " got: " << rewritten
<< std::endl
;
1497 Node preprocessed
= preprocess(rewritten
);
1498 Debug("ensureLiteral") << "preprocessed: " << preprocessed
<< std::endl
;
1499 d_propEngine
->ensureLiteral(preprocessed
);
1500 return preprocessed
;
1504 void TheoryEngine::printInstantiations( std::ostream
& out
) {
1505 if( d_quantEngine
){
1506 d_quantEngine
->printInstantiations( out
);
1508 out
<< "Internal error : instantiations not available when quantifiers are not present." << std::endl
;
1513 void TheoryEngine::printSynthSolution( std::ostream
& out
) {
1514 if( d_quantEngine
){
1515 d_quantEngine
->printSynthSolution( out
);
1517 out
<< "Internal error : synth solution not available when quantifiers are not present." << std::endl
;
1522 void TheoryEngine::getInstantiatedQuantifiedFormulas( std::vector
< Node
>& qs
) {
1523 if( d_quantEngine
){
1524 d_quantEngine
->getInstantiatedQuantifiedFormulas( qs
);
1530 void TheoryEngine::getInstantiations( Node q
, std::vector
< Node
>& insts
) {
1531 if( d_quantEngine
){
1532 d_quantEngine
->getInstantiations( q
, insts
);
1538 void TheoryEngine::getInstantiationTermVectors( Node q
, std::vector
< std::vector
< Node
> >& tvecs
) {
1539 if( d_quantEngine
){
1540 d_quantEngine
->getInstantiationTermVectors( q
, tvecs
);
1546 void TheoryEngine::getInstantiations( std::map
< Node
, std::vector
< Node
> >& insts
) {
1547 if( d_quantEngine
){
1548 d_quantEngine
->getInstantiations( insts
);
1554 void TheoryEngine::getInstantiationTermVectors( std::map
< Node
, std::vector
< std::vector
< Node
> > >& insts
) {
1555 if( d_quantEngine
){
1556 d_quantEngine
->getInstantiationTermVectors( insts
);
1562 Node
TheoryEngine::getInstantiatedConjunction( Node q
) {
1563 if( d_quantEngine
){
1564 return d_quantEngine
->getInstantiatedConjunction( q
);
1567 return Node::null();
1572 static Node
mkExplanation(const std::vector
<NodeTheoryPair
>& explanation
) {
1574 std::set
<TNode
> all
;
1575 for (unsigned i
= 0; i
< explanation
.size(); ++ i
) {
1576 Assert(explanation
[i
].theory
== THEORY_SAT_SOLVER
);
1577 all
.insert(explanation
[i
].node
);
1580 if (all
.size() == 0) {
1581 // Normalize to true
1582 return NodeManager::currentNM()->mkConst
<bool>(true);
1585 if (all
.size() == 1) {
1586 // All the same, or just one
1587 return explanation
[0].node
;
1590 NodeBuilder
<> conjunction(kind::AND
);
1591 std::set
<TNode
>::const_iterator it
= all
.begin();
1592 std::set
<TNode
>::const_iterator it_end
= all
.end();
1593 while (it
!= it_end
) {
1601 Node
TheoryEngine::getExplanationAndRecipe(TNode node
, LemmaProofRecipe
* proofRecipe
) {
1602 Debug("theory::explain") << "TheoryEngine::getExplanation(" << node
<< "): current propagation index = " << d_propagationMapTimestamp
<< endl
;
1604 bool polarity
= node
.getKind() != kind::NOT
;
1605 TNode atom
= polarity
? node
: node
[0];
1607 // If we're not in shared mode, explanations are simple
1608 if (!d_logicInfo
.isSharingEnabled()) {
1609 Debug("theory::explain") << "TheoryEngine::getExplanation: sharing is NOT enabled. "
1610 << " Responsible theory is: "
1611 << theoryOf(atom
)->getId() << std::endl
;
1613 Node explanation
= theoryOf(atom
)->explain(node
);
1614 Debug("theory::explain") << "TheoryEngine::getExplanation(" << node
<< ") => " << explanation
<< endl
;
1618 LemmaProofRecipe::ProofStep
proofStep(theoryOf(atom
)->getId(), emptyNode
);
1619 proofStep
.addAssertion(node
);
1620 proofRecipe
->addBaseAssertion(node
);
1622 if (explanation
.getKind() == kind::AND
) {
1623 // If the explanation is a conjunction, the recipe for the corresponding lemma is
1624 // the negation of its conjuncts.
1625 Node flat
= flattenAnd(explanation
);
1626 for (unsigned i
= 0; i
< flat
.getNumChildren(); ++i
) {
1627 if (flat
[i
].isConst() && flat
[i
].getConst
<bool>()) {
1631 if (flat
[i
].getKind() == kind::NOT
&&
1632 flat
[i
][0].isConst() && !flat
[i
][0].getConst
<bool>()) {
1636 Debug("theory::explain") << "TheoryEngine::getExplanationAndRecipe: adding recipe assertion: "
1637 << flat
[i
].negate() << std::endl
;
1638 proofStep
.addAssertion(flat
[i
].negate());
1639 proofRecipe
->addBaseAssertion(flat
[i
].negate());
1642 // The recipe for proving it is by negating it. "True" is not an acceptable reason.
1643 if (!((explanation
.isConst() && explanation
.getConst
<bool>()) ||
1644 (explanation
.getKind() == kind::NOT
&&
1645 explanation
[0].isConst() && !explanation
[0].getConst
<bool>()))) {
1646 proofStep
.addAssertion(explanation
.negate());
1647 proofRecipe
->addBaseAssertion(explanation
.negate());
1651 proofRecipe
->addStep(proofStep
);
1658 Debug("theory::explain") << "TheoryEngine::getExplanation: sharing IS enabled" << std::endl
;
1660 // Initial thing to explain
1661 NodeTheoryPair
toExplain(node
, THEORY_SAT_SOLVER
, d_propagationMapTimestamp
);
1662 Assert(d_propagationMap
.find(toExplain
) != d_propagationMap
.end());
1664 NodeTheoryPair nodeExplainerPair
= d_propagationMap
[toExplain
];
1665 Debug("theory::explain") << "TheoryEngine::getExplanation: explainer for node "
1666 << nodeExplainerPair
.node
1667 << " is theory: " << nodeExplainerPair
.theory
<< std::endl
;
1668 TheoryId explainer
= nodeExplainerPair
.theory
;
1670 // Create the workplace for explanations
1671 std::vector
<NodeTheoryPair
> explanationVector
;
1672 explanationVector
.push_back(d_propagationMap
[toExplain
]);
1673 // Process the explanation
1676 LemmaProofRecipe::ProofStep
proofStep(explainer
, emptyNode
);
1677 proofStep
.addAssertion(node
);
1678 proofRecipe
->addStep(proofStep
);
1679 proofRecipe
->addBaseAssertion(node
);
1682 getExplanation(explanationVector
, proofRecipe
);
1683 Node explanation
= mkExplanation(explanationVector
);
1685 Debug("theory::explain") << "TheoryEngine::getExplanation(" << node
<< ") => " << explanation
<< endl
;
1690 Node
TheoryEngine::getExplanation(TNode node
) {
1691 LemmaProofRecipe
*dontCareRecipe
= NULL
;
1692 return getExplanationAndRecipe(node
, dontCareRecipe
);
1695 struct AtomsCollect
{
1697 std::vector
<TNode
> d_atoms
;
1698 std::unordered_set
<TNode
, TNodeHashFunction
> d_visited
;
1702 typedef void return_type
;
1704 bool alreadyVisited(TNode current
, TNode parent
) {
1705 // Check if already visited
1706 if (d_visited
.find(current
) != d_visited
.end()) return true;
1707 // Don't visit non-boolean
1708 if (!current
.getType().isBoolean()) return true;
1713 void visit(TNode current
, TNode parent
) {
1714 if (Theory::theoryOf(current
) != theory::THEORY_BOOL
) {
1715 d_atoms
.push_back(current
);
1717 d_visited
.insert(current
);
1720 void start(TNode node
) {}
1721 void done(TNode node
) {}
1723 std::vector
<TNode
> getAtoms() const {
1728 void TheoryEngine::ensureLemmaAtoms(const std::vector
<TNode
>& atoms
, theory::TheoryId atomsTo
) {
1729 for (unsigned i
= 0; i
< atoms
.size(); ++ i
) {
1731 // Non-equality atoms are either owned by theory or they don't make sense
1732 if (atoms
[i
].getKind() != kind::EQUAL
) {
1738 // Simple normalization to not repeat stuff
1739 if (eq
[0] > eq
[1]) {
1740 eq
= eq
[1].eqNode(eq
[0]);
1743 // Rewrite the equality
1744 Node eqNormalized
= Rewriter::rewrite(atoms
[i
]);
1746 Debug("theory::atoms") << "TheoryEngine::ensureLemmaAtoms(): " << eq
<< " with nf " << eqNormalized
<< endl
;
1748 // If the equality is a boolean constant, we send immediately
1749 if (eqNormalized
.isConst()) {
1750 if (eqNormalized
.getConst
<bool>()) {
1751 assertToTheory(eq
, eqNormalized
, /** to */ atomsTo
, /** Sat solver */ theory::THEORY_SAT_SOLVER
);
1753 assertToTheory(eq
.notNode(), eqNormalized
.notNode(), /** to */ atomsTo
, /** Sat solver */ theory::THEORY_SAT_SOLVER
);
1756 }else if( eqNormalized
.getKind() != kind::EQUAL
){
1757 Assert( eqNormalized
.getKind()==kind::BOOLEAN_TERM_VARIABLE
||
1758 ( eqNormalized
.getKind()==kind::NOT
&& eqNormalized
[0].getKind()==kind::BOOLEAN_TERM_VARIABLE
) );
1759 // this happens for Boolean term equalities V = true that are rewritten to V, we should skip
1760 // TODO : revisit this
1764 // If the normalization did the just flips, keep the flip
1765 if (eqNormalized
[0] == eq
[1] && eqNormalized
[1] == eq
[0]) {
1769 // Check if the equality is already known by the sat solver
1770 if (d_propEngine
->isSatLiteral(eqNormalized
)) {
1772 if (d_propEngine
->hasValue(eqNormalized
, value
)) {
1774 assertToTheory(eq
, eqNormalized
, atomsTo
, theory::THEORY_SAT_SOLVER
);
1777 assertToTheory(eq
.notNode(), eqNormalized
.notNode(), atomsTo
, theory::THEORY_SAT_SOLVER
);
1783 // If the theory is asking about a different form, or the form is ok but if will go to a different theory
1784 // then we must figure it out
1785 if (eqNormalized
!= eq
|| Theory::theoryOf(eq
) != atomsTo
) {
1786 // If you get eqNormalized, send atoms[i] to atomsTo
1787 d_atomRequests
.add(eqNormalized
, eq
, atomsTo
);
1792 theory::LemmaStatus
TheoryEngine::lemma(TNode node
,
1797 theory::TheoryId atomsTo
) {
1798 // For resource-limiting (also does a time check).
1801 // Do we need to check atoms
1802 if (atomsTo
!= theory::THEORY_LAST
) {
1803 Debug("theory::atoms") << "TheoryEngine::lemma(" << node
<< ", " << atomsTo
<< ")" << endl
;
1804 AtomsCollect collectAtoms
;
1805 NodeVisitor
<AtomsCollect
>::run(collectAtoms
, node
);
1806 ensureLemmaAtoms(collectAtoms
.getAtoms(), atomsTo
);
1809 if(Dump
.isOn("t-lemmas")) {
1814 Dump("t-lemmas") << CommentCommand("theory lemma: expect valid")
1815 << QueryCommand(n
.toExpr());
1818 // Share with other portfolio threads
1819 if(d_channels
->getLemmaOutputChannel() != NULL
) {
1820 d_channels
->getLemmaOutputChannel()->notifyNewLemma(node
.toExpr());
1823 std::vector
<Node
> additionalLemmas
;
1824 IteSkolemMap iteSkolemMap
;
1826 // Run theory preprocessing, maybe
1827 Node ppNode
= preprocess
? this->preprocess(node
) : Node(node
);
1830 Debug("ite") << "Remove ITE from " << ppNode
<< std::endl
;
1831 additionalLemmas
.push_back(ppNode
);
1832 d_tform_remover
.run(additionalLemmas
, iteSkolemMap
);
1833 Debug("ite") << "..done " << additionalLemmas
[0] << std::endl
;
1834 additionalLemmas
[0] = theory::Rewriter::rewrite(additionalLemmas
[0]);
1836 if(Debug
.isOn("lemma-ites")) {
1837 Debug("lemma-ites") << "removed ITEs from lemma: " << ppNode
<< endl
;
1838 Debug("lemma-ites") << " + now have the following "
1839 << additionalLemmas
.size() << " lemma(s):" << endl
;
1840 for(std::vector
<Node
>::const_iterator i
= additionalLemmas
.begin();
1841 i
!= additionalLemmas
.end();
1843 Debug("lemma-ites") << " + " << *i
<< endl
;
1845 Debug("lemma-ites") << endl
;
1848 // assert to prop engine
1849 d_propEngine
->assertLemma(additionalLemmas
[0], negated
, removable
, rule
, node
);
1850 for (unsigned i
= 1; i
< additionalLemmas
.size(); ++ i
) {
1851 additionalLemmas
[i
] = theory::Rewriter::rewrite(additionalLemmas
[i
]);
1852 d_propEngine
->assertLemma(additionalLemmas
[i
], false, removable
, rule
, node
);
1855 // WARNING: Below this point don't assume additionalLemmas[0] to be not negated.
1857 additionalLemmas
[0] = additionalLemmas
[0].notNode();
1861 // assert to decision engine
1863 d_decisionEngine
->addAssertions(additionalLemmas
, 1, iteSkolemMap
);
1866 // Mark that we added some lemmas
1867 d_lemmasAdded
= true;
1869 // Lemma analysis isn't online yet; this lemma may only live for this
1871 return theory::LemmaStatus(additionalLemmas
[0], d_userContext
->getLevel());
1874 void TheoryEngine::conflict(TNode conflict
, TheoryId theoryId
) {
1876 Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict
<< ", " << theoryId
<< ")" << endl
;
1878 // Mark that we are in conflict
1879 d_inConflict
= true;
1881 if(Dump
.isOn("t-conflicts")) {
1882 Dump("t-conflicts") << CommentCommand("theory conflict: expect unsat")
1883 << CheckSatCommand(conflict
.toExpr());
1886 LemmaProofRecipe
* proofRecipe
= NULL
;
1888 proofRecipe
= new LemmaProofRecipe
;
1890 LemmaProofRecipe::ProofStep
proofStep(theoryId
, emptyNode
);
1892 if (conflict
.getKind() == kind::AND
) {
1893 for (unsigned i
= 0; i
< conflict
.getNumChildren(); ++i
) {
1894 proofStep
.addAssertion(conflict
[i
].negate());
1897 proofStep
.addAssertion(conflict
.negate());
1900 proofRecipe
->addStep(proofStep
);
1903 // In the multiple-theories case, we need to reconstruct the conflict
1904 if (d_logicInfo
.isSharingEnabled()) {
1905 // Create the workplace for explanations
1906 std::vector
<NodeTheoryPair
> explanationVector
;
1907 explanationVector
.push_back(NodeTheoryPair(conflict
, theoryId
, d_propagationMapTimestamp
));
1909 // Process the explanation
1910 getExplanation(explanationVector
, proofRecipe
);
1911 PROOF(ProofManager::getCnfProof()->setProofRecipe(proofRecipe
));
1912 Node fullConflict
= mkExplanation(explanationVector
);
1913 Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict
<< ", " << theoryId
<< "): full = " << fullConflict
<< endl
;
1914 Assert(properConflict(fullConflict
));
1915 lemma(fullConflict
, RULE_CONFLICT
, true, true, false, THEORY_LAST
);
1918 // When only one theory, the conflict should need no processing
1919 Assert(properConflict(conflict
));
1921 if (conflict
.getKind() == kind::AND
) {
1922 // If the conflict is a conjunction, the corresponding lemma is derived by negating
1924 for (unsigned i
= 0; i
< conflict
.getNumChildren(); ++i
) {
1925 if (conflict
[i
].isConst() && conflict
[i
].getConst
<bool>()) {
1929 if (conflict
[i
].getKind() == kind::NOT
&&
1930 conflict
[i
][0].isConst() && !conflict
[i
][0].getConst
<bool>()) {
1934 proofRecipe
->getStep(0)->addAssertion(conflict
[i
].negate());
1935 proofRecipe
->addBaseAssertion(conflict
[i
].negate());
1938 proofRecipe
->getStep(0)->addAssertion(conflict
.negate());
1939 proofRecipe
->addBaseAssertion(conflict
.negate());
1942 ProofManager::getCnfProof()->setProofRecipe(proofRecipe
);
1945 lemma(conflict
, RULE_CONFLICT
, true, true, false, THEORY_LAST
);
1954 void TheoryEngine::staticInitializeBVOptions(
1955 const std::vector
<Node
>& assertions
)
1957 bool useSlicer
= true;
1958 if (options::bitvectorEqualitySlicer() == bv::BITVECTOR_SLICER_ON
)
1960 if (!d_logicInfo
.isPure(theory::THEORY_BV
) || d_logicInfo
.isQuantified())
1961 throw ModalException(
1962 "Slicer currently only supports pure QF_BV formulas. Use "
1963 "--bv-eq-slicer=off");
1964 if (options::incrementalSolving())
1965 throw ModalException(
1966 "Slicer does not currently support incremental mode. Use "
1967 "--bv-eq-slicer=off");
1968 if (options::produceModels())
1969 throw ModalException(
1970 "Slicer does not currently support model generation. Use "
1971 "--bv-eq-slicer=off");
1973 else if (options::bitvectorEqualitySlicer() == bv::BITVECTOR_SLICER_OFF
)
1977 else if (options::bitvectorEqualitySlicer() == bv::BITVECTOR_SLICER_AUTO
)
1979 if ((!d_logicInfo
.isPure(theory::THEORY_BV
) || d_logicInfo
.isQuantified())
1980 || options::incrementalSolving()
1981 || options::produceModels())
1984 bv::utils::TNodeBoolMap cache
;
1985 for (unsigned i
= 0; i
< assertions
.size(); ++i
)
1987 useSlicer
= useSlicer
&& bv::utils::isCoreTerm(assertions
[i
], cache
);
1993 bv::TheoryBV
* bv_theory
= (bv::TheoryBV
*)d_theoryTable
[THEORY_BV
];
1994 bv_theory
->enableCoreTheorySlicer();
1998 void TheoryEngine::getExplanation(std::vector
<NodeTheoryPair
>& explanationVector
, LemmaProofRecipe
* proofRecipe
) {
1999 Assert(explanationVector
.size() > 0);
2001 unsigned i
= 0; // Index of the current literal we are processing
2002 unsigned j
= 0; // Index of the last literal we are keeping
2004 std::unique_ptr
<std::set
<Node
>> inputAssertions
= nullptr;
2008 inputAssertions
.reset(
2009 new std::set
<Node
>(proofRecipe
->getStep(0)->getAssertions()));
2013 while (i
< explanationVector
.size()) {
2014 // Get the current literal to explain
2015 NodeTheoryPair toExplain
= explanationVector
[i
];
2017 Debug("theory::explain") << "[i=" << i
<< "] TheoryEngine::explain(): processing [" << toExplain
.timestamp
<< "] " << toExplain
.node
<< " sent from " << toExplain
.theory
<< endl
;
2020 // If a true constant or a negation of a false constant we can ignore it
2021 if (toExplain
.node
.isConst() && toExplain
.node
.getConst
<bool>()) {
2025 if (toExplain
.node
.getKind() == kind::NOT
&& toExplain
.node
[0].isConst() && !toExplain
.node
[0].getConst
<bool>()) {
2030 // If from the SAT solver, keep it
2031 if (toExplain
.theory
== THEORY_SAT_SOLVER
) {
2032 Debug("theory::explain") << "\tLiteral came from THEORY_SAT_SOLVER. Kepping it." << endl
;
2033 explanationVector
[j
++] = explanationVector
[i
++];
2037 // If an and, expand it
2038 if (toExplain
.node
.getKind() == kind::AND
) {
2039 Debug("theory::explain") << "TheoryEngine::explain(): expanding " << toExplain
.node
<< " got from " << toExplain
.theory
<< endl
;
2040 for (unsigned k
= 0; k
< toExplain
.node
.getNumChildren(); ++ k
) {
2041 NodeTheoryPair
newExplain(toExplain
.node
[k
], toExplain
.theory
, toExplain
.timestamp
);
2042 explanationVector
.push_back(newExplain
);
2048 // See if it was sent to the theory by another theory
2049 PropagationMap::const_iterator find
= d_propagationMap
.find(toExplain
);
2050 if (find
!= d_propagationMap
.end()) {
2051 Debug("theory::explain") << "\tTerm was propagated by another theory (theory = "
2052 << theoryOf((*find
).second
.theory
)->getId() << ")" << std::endl
;
2053 // There is some propagation, check if its a timely one
2054 if ((*find
).second
.timestamp
< toExplain
.timestamp
) {
2055 Debug("theory::explain") << "\tRelevant timetsamp, pushing "
2056 << (*find
).second
.node
<< "to index = " << explanationVector
.size() << std::endl
;
2057 explanationVector
.push_back((*find
).second
);
2061 if (toExplain
.node
!= (*find
).second
.node
) {
2062 Debug("pf::explain") << "TheoryEngine::getExplanation: Rewrite alert! toAssert = " << toExplain
.node
2063 << ", toExplain = " << (*find
).second
.node
<< std::endl
;
2066 proofRecipe
->addRewriteRule(toExplain
.node
, (*find
).second
.node
);
2075 // It was produced by the theory, so ask for an explanation
2077 if (toExplain
.theory
== THEORY_BUILTIN
) {
2078 explanation
= d_sharedTerms
.explain(toExplain
.node
);
2079 Debug("theory::explain") << "\tTerm was propagated by THEORY_BUILTIN. Explanation: " << explanation
<< std::endl
;
2081 explanation
= theoryOf(toExplain
.theory
)->explain(toExplain
.node
);
2082 Debug("theory::explain") << "\tTerm was propagated by owner theory: "
2083 << theoryOf(toExplain
.theory
)->getId()
2084 << ". Explanation: " << explanation
<< std::endl
;
2087 Debug("theory::explain") << "TheoryEngine::explain(): got explanation " << explanation
<< " got from " << toExplain
.theory
<< endl
;
2088 Assert( explanation
!= toExplain
.node
, "wasn't sent to you, so why are you explaining it trivially");
2089 // Mark the explanation
2090 NodeTheoryPair
newExplain(explanation
, toExplain
.theory
, toExplain
.timestamp
);
2091 explanationVector
.push_back(newExplain
);
2096 if (proofRecipe
&& inputAssertions
)
2098 // If we're expanding the target node of the explanation (this is the
2099 // first expansion...), we don't want to add it as a separate proof
2100 // step. It is already part of the assertions.
2101 if (!ContainsKey(*inputAssertions
, toExplain
.node
))
2103 LemmaProofRecipe::ProofStep
proofStep(toExplain
.theory
,
2105 if (explanation
.getKind() == kind::AND
)
2107 Node flat
= flattenAnd(explanation
);
2108 for (unsigned k
= 0; k
< flat
.getNumChildren(); ++k
)
2110 // If a true constant or a negation of a false constant we can
2112 if (!((flat
[k
].isConst() && flat
[k
].getConst
<bool>())
2113 || (flat
[k
].getKind() == kind::NOT
&& flat
[k
][0].isConst()
2114 && !flat
[k
][0].getConst
<bool>())))
2116 proofStep
.addAssertion(flat
[k
].negate());
2122 if (!((explanation
.isConst() && explanation
.getConst
<bool>())
2123 || (explanation
.getKind() == kind::NOT
2124 && explanation
[0].isConst()
2125 && !explanation
[0].getConst
<bool>())))
2127 proofStep
.addAssertion(explanation
.negate());
2130 proofRecipe
->addStep(proofStep
);
2136 // Keep only the relevant literals
2137 explanationVector
.resize(j
);
2141 // The remaining literals are the base of the proof
2142 for (unsigned k
= 0; k
< explanationVector
.size(); ++k
) {
2143 proofRecipe
->addBaseAssertion(explanationVector
[k
].node
.negate());
2149 void TheoryEngine::ppUnconstrainedSimp(vector
<Node
>& assertions
)
2151 d_unconstrainedSimp
->processAssertions(assertions
);
2154 void TheoryEngine::setUserAttribute(const std::string
& attr
,
2156 const std::vector
<Node
>& node_values
,
2157 const std::string
& str_value
)
2159 Trace("te-attr") << "set user attribute " << attr
<< " " << n
<< endl
;
2160 if( d_attr_handle
.find( attr
)!=d_attr_handle
.end() ){
2161 for( size_t i
=0; i
<d_attr_handle
[attr
].size(); i
++ ){
2162 d_attr_handle
[attr
][i
]->setUserAttribute(attr
, n
, node_values
, str_value
);
2165 //unhandled exception?
2169 void TheoryEngine::handleUserAttribute(const char* attr
, Theory
* t
) {
2170 Trace("te-attr") << "Handle user attribute " << attr
<< " " << t
<< endl
;
2171 std::string
str( attr
);
2172 d_attr_handle
[ str
].push_back( t
);
2175 void TheoryEngine::checkTheoryAssertionsWithModel(bool hardFailure
) {
2176 for(TheoryId theoryId
= THEORY_FIRST
; theoryId
< THEORY_LAST
; ++theoryId
) {
2177 Theory
* theory
= d_theoryTable
[theoryId
];
2178 if(theory
&& d_logicInfo
.isTheoryEnabled(theoryId
)) {
2179 for(context::CDList
<Assertion
>::const_iterator it
= theory
->facts_begin(),
2180 it_end
= theory
->facts_end();
2183 Node assertion
= (*it
).assertion
;
2184 Node val
= getModel()->getValue(assertion
);
2187 ss
<< theoryId
<< " has an asserted fact that the model doesn't satisfy." << endl
2188 << "The fact: " << assertion
<< endl
2189 << "Model value: " << val
<< endl
;
2191 InternalError(ss
.str());
2199 std::pair
<bool, Node
> TheoryEngine::entailmentCheck(theory::TheoryOfMode mode
, TNode lit
, const EntailmentCheckParameters
* params
, EntailmentCheckSideEffects
* seffects
) {
2200 TNode atom
= (lit
.getKind() == kind::NOT
) ? lit
[0] : lit
;
2201 if( atom
.getKind()==kind::AND
|| atom
.getKind()==kind::OR
|| atom
.getKind()==kind::IMPLIES
){
2202 //Boolean connective, recurse
2203 std::vector
< Node
> children
;
2204 bool pol
= (lit
.getKind()!=kind::NOT
);
2205 bool is_conjunction
= pol
==(lit
.getKind()==kind::AND
);
2206 for( unsigned i
=0; i
<atom
.getNumChildren(); i
++ ){
2208 if( pol
==( lit
.getKind()==kind::IMPLIES
&& i
==0 ) ){
2209 ch
= atom
[i
].negate();
2211 std::pair
<bool, Node
> chres
= entailmentCheck( mode
, ch
, params
, seffects
);
2213 if( !is_conjunction
){
2216 children
.push_back( chres
.second
);
2218 }else if( !chres
.first
&& is_conjunction
){
2219 return std::pair
<bool, Node
>(false, Node::null());
2222 if( is_conjunction
){
2223 return std::pair
<bool, Node
>(true, NodeManager::currentNM()->mkNode(kind::AND
, children
));
2225 return std::pair
<bool, Node
>(false, Node::null());
2227 }else if( atom
.getKind()==kind::ITE
|| ( atom
.getKind()==kind::EQUAL
&& atom
[0].getType().isBoolean() ) ){
2228 bool pol
= (lit
.getKind()!=kind::NOT
);
2229 for( unsigned r
=0; r
<2; r
++ ){
2234 std::pair
<bool, Node
> chres
= entailmentCheck( mode
, ch
, params
, seffects
);
2236 Node ch2
= atom
[ atom
.getKind()==kind::ITE
? r
+1 : 1 ];
2237 if( pol
==( atom
.getKind()==kind::ITE
? true : r
==1 ) ){
2240 std::pair
<bool, Node
> chres2
= entailmentCheck( mode
, ch2
, params
, seffects
);
2242 return std::pair
<bool, Node
>(true, NodeManager::currentNM()->mkNode(kind::AND
, chres
.second
, chres2
.second
));
2248 return std::pair
<bool, Node
>(false, Node::null());
2250 //it is a theory atom
2251 theory::TheoryId tid
= theory::Theory::theoryOf(mode
, atom
);
2252 theory::Theory
* th
= theoryOf(tid
);
2255 Assert(params
== NULL
|| tid
== params
->getTheoryId());
2256 Assert(seffects
== NULL
|| tid
== seffects
->getTheoryId());
2257 Trace("theory-engine-entc") << "Entailment check : " << lit
<< std::endl
;
2259 std::pair
<bool, Node
> chres
= th
->entailmentCheck(lit
, params
, seffects
);
2264 void TheoryEngine::spendResource(unsigned amount
)
2266 d_resourceManager
->spendResource(amount
);
2269 void TheoryEngine::enableTheoryAlternative(const std::string
& name
){
2270 Debug("TheoryEngine::enableTheoryAlternative")
2271 << "TheoryEngine::enableTheoryAlternative(" << name
<< ")" << std::endl
;
2273 d_theoryAlternatives
.insert(name
);
2276 bool TheoryEngine::useTheoryAlternative(const std::string
& name
) {
2277 return d_theoryAlternatives
.find(name
) != d_theoryAlternatives
.end();
2281 TheoryEngine::Statistics::Statistics(theory::TheoryId theory
):
2282 conflicts(getStatsPrefix(theory
) + "::conflicts", 0),
2283 propagations(getStatsPrefix(theory
) + "::propagations", 0),
2284 lemmas(getStatsPrefix(theory
) + "::lemmas", 0),
2285 requirePhase(getStatsPrefix(theory
) + "::requirePhase", 0),
2286 restartDemands(getStatsPrefix(theory
) + "::restartDemands", 0)
2288 smtStatisticsRegistry()->registerStat(&conflicts
);
2289 smtStatisticsRegistry()->registerStat(&propagations
);
2290 smtStatisticsRegistry()->registerStat(&lemmas
);
2291 smtStatisticsRegistry()->registerStat(&requirePhase
);
2292 smtStatisticsRegistry()->registerStat(&restartDemands
);
2295 TheoryEngine::Statistics::~Statistics() {
2296 smtStatisticsRegistry()->unregisterStat(&conflicts
);
2297 smtStatisticsRegistry()->unregisterStat(&propagations
);
2298 smtStatisticsRegistry()->unregisterStat(&lemmas
);
2299 smtStatisticsRegistry()->unregisterStat(&requirePhase
);
2300 smtStatisticsRegistry()->unregisterStat(&restartDemands
);
2303 }/* CVC4 namespace */