diff options
Diffstat (limited to 'src/theory/engine_output_channel.cpp')
-rw-r--r-- | src/theory/engine_output_channel.cpp | 153 |
1 files changed, 4 insertions, 149 deletions
diff --git a/src/theory/engine_output_channel.cpp b/src/theory/engine_output_channel.cpp index a271d6d9c..b6d9a19db 100644 --- a/src/theory/engine_output_channel.cpp +++ b/src/theory/engine_output_channel.cpp @@ -14,10 +14,6 @@ #include "theory/engine_output_channel.h" -#include "proof/cnf_proof.h" -#include "proof/lemma_proof.h" -#include "proof/proof_manager.h" -#include "proof/theory_proof.h" #include "prop/prop_engine.h" #include "smt/smt_statistics_registry.h" #include "theory/theory_engine.h" @@ -71,9 +67,7 @@ void EngineOutputChannel::safePoint(ResourceManager::Resource r) } } -theory::LemmaStatus EngineOutputChannel::lemma(TNode lemma, - ProofRule rule, - LemmaProperty p) +theory::LemmaStatus EngineOutputChannel::lemma(TNode lemma, LemmaProperty p) { Debug("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" @@ -81,151 +75,15 @@ theory::LemmaStatus EngineOutputChannel::lemma(TNode lemma, ++d_statistics.lemmas; d_engine->d_outputChannelUsed = true; - PROOF({ - bool preprocess = isLemmaPropertyPreprocess(p); - registerLemmaRecipe(lemma, lemma, preprocess, d_theory); - }); - TrustNode tlem = TrustNode::mkTrustLemma(lemma); theory::LemmaStatus result = d_engine->lemma( tlem.getNode(), - rule, false, p, isLemmaPropertySendAtoms(p) ? d_theory : theory::THEORY_LAST); return result; } -void EngineOutputChannel::registerLemmaRecipe(Node lemma, - Node originalLemma, - bool preprocess, - theory::TheoryId theoryId) -{ - // During CNF conversion, conjunctions will be broken down into - // multiple lemmas. In order for the recipes to match, we have to do - // the same here. - NodeManager* nm = NodeManager::currentNM(); - - if (preprocess) lemma = d_engine->preprocess(lemma); - - bool negated = (lemma.getKind() == NOT); - Node nnLemma = negated ? lemma[0] : lemma; - - switch (nnLemma.getKind()) - { - case AND: - if (!negated) - { - for (unsigned i = 0; i < nnLemma.getNumChildren(); ++i) - registerLemmaRecipe(nnLemma[i], originalLemma, false, theoryId); - } - else - { - NodeBuilder<> builder(OR); - for (unsigned i = 0; i < nnLemma.getNumChildren(); ++i) - builder << nnLemma[i].negate(); - - Node disjunction = - (builder.getNumChildren() == 1) ? builder[0] : builder; - registerLemmaRecipe(disjunction, originalLemma, false, theoryId); - } - break; - - case EQUAL: - if (nnLemma[0].getType().isBoolean()) - { - if (!negated) - { - registerLemmaRecipe(nm->mkNode(OR, nnLemma[0], nnLemma[1].negate()), - originalLemma, - false, - theoryId); - registerLemmaRecipe(nm->mkNode(OR, nnLemma[0].negate(), nnLemma[1]), - originalLemma, - false, - theoryId); - } - else - { - registerLemmaRecipe(nm->mkNode(OR, nnLemma[0], nnLemma[1]), - originalLemma, - false, - theoryId); - registerLemmaRecipe( - nm->mkNode(OR, nnLemma[0].negate(), nnLemma[1].negate()), - originalLemma, - false, - theoryId); - } - } - break; - - case ITE: - if (!negated) - { - registerLemmaRecipe(nm->mkNode(OR, nnLemma[0].negate(), nnLemma[1]), - originalLemma, - false, - theoryId); - registerLemmaRecipe(nm->mkNode(OR, nnLemma[0], nnLemma[2]), - originalLemma, - false, - theoryId); - } - else - { - registerLemmaRecipe( - nm->mkNode(OR, nnLemma[0].negate(), nnLemma[1].negate()), - originalLemma, - false, - theoryId); - registerLemmaRecipe(nm->mkNode(OR, nnLemma[0], nnLemma[2].negate()), - originalLemma, - false, - theoryId); - } - break; - - default: break; - } - - // Theory lemmas have one step that proves the empty clause - LemmaProofRecipe proofRecipe; - Node emptyNode; - LemmaProofRecipe::ProofStep proofStep(theoryId, emptyNode); - - // Remember the original lemma, so we can report this later when asked to - proofRecipe.setOriginalLemma(originalLemma); - - // Record the assertions and rewrites - Node rewritten; - if (lemma.getKind() == OR) - { - for (unsigned i = 0; i < lemma.getNumChildren(); ++i) - { - rewritten = theory::Rewriter::rewrite(lemma[i]); - if (rewritten != lemma[i]) - { - proofRecipe.addRewriteRule(lemma[i].negate(), rewritten.negate()); - } - proofStep.addAssertion(lemma[i]); - proofRecipe.addBaseAssertion(rewritten); - } - } - else - { - rewritten = theory::Rewriter::rewrite(lemma); - if (rewritten != lemma) - { - proofRecipe.addRewriteRule(lemma.negate(), rewritten.negate()); - } - proofStep.addAssertion(lemma); - proofRecipe.addBaseAssertion(rewritten); - } - proofRecipe.addStep(proofStep); - ProofManager::getCnfProof()->setProofRecipe(&proofRecipe); -} - theory::LemmaStatus EngineOutputChannel::splitLemma(TNode lemma, bool removable) { Debug("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" @@ -238,7 +96,7 @@ theory::LemmaStatus EngineOutputChannel::splitLemma(TNode lemma, bool removable) TrustNode tlem = TrustNode::mkTrustLemma(lemma); LemmaProperty p = removable ? LemmaProperty::REMOVABLE : LemmaProperty::NONE; theory::LemmaStatus result = - d_engine->lemma(tlem.getNode(), RULE_SPLIT, false, p, d_theory); + d_engine->lemma(tlem.getNode(), false, p, d_theory); return result; } @@ -251,13 +109,11 @@ bool EngineOutputChannel::propagate(TNode literal) return d_engine->propagate(literal, d_theory); } -void EngineOutputChannel::conflict(TNode conflictNode, - std::unique_ptr<Proof> proof) +void EngineOutputChannel::conflict(TNode conflictNode) { Trace("theory::conflict") << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode << ")" << std::endl; - Assert(!proof); // Theory shouldn't be producing proofs yet ++d_statistics.conflicts; d_engine->d_outputChannelUsed = true; TrustNode tConf = TrustNode::mkTrustConflict(conflictNode); @@ -274,7 +130,7 @@ void EngineOutputChannel::demandRestart() Trace("theory::restart") << "EngineOutputChannel<" << d_theory << ">::restart(" << restartVar << ")" << std::endl; ++d_statistics.restartDemands; - lemma(restartVar, RULE_INVALID, LemmaProperty::REMOVABLE); + lemma(restartVar, LemmaProperty::REMOVABLE); } void EngineOutputChannel::requirePhase(TNode n, bool phase) @@ -329,7 +185,6 @@ LemmaStatus EngineOutputChannel::trustedLemma(TrustNode plem, LemmaProperty p) // now, call the normal interface for lemma return d_engine->lemma( plem.getNode(), - RULE_INVALID, false, p, isLemmaPropertySendAtoms(p) ? d_theory : theory::THEORY_LAST); |