diff options
Diffstat (limited to 'src/theory/engine_output_channel.cpp')
| -rw-r--r-- | src/theory/engine_output_channel.cpp | 196 |
1 files changed, 25 insertions, 171 deletions
diff --git a/src/theory/engine_output_channel.cpp b/src/theory/engine_output_channel.cpp index d83d2ba62..cb346d02d 100644 --- a/src/theory/engine_output_channel.cpp +++ b/src/theory/engine_output_channel.cpp @@ -2,10 +2,10 @@ /*! \file engine_output_channel.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Guy Katz, Tim King + ** Andrew Reynolds, Tim King, Morgan Deters ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** @@ -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,161 +67,23 @@ void EngineOutputChannel::safePoint(ResourceManager::Resource r) } } -theory::LemmaStatus EngineOutputChannel::lemma(TNode lemma, - ProofRule rule, - bool removable, - bool preprocess, - bool sendAtoms) +theory::LemmaStatus EngineOutputChannel::lemma(TNode lemma, LemmaProperty p) { Debug("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" - << ", preprocess = " << preprocess << std::endl; + << ", properties = " << p << std::endl; ++d_statistics.lemmas; d_engine->d_outputChannelUsed = true; - PROOF({ registerLemmaRecipe(lemma, lemma, preprocess, d_theory); }); - TrustNode tlem = TrustNode::mkTrustLemma(lemma); - theory::LemmaStatus result = - d_engine->lemma(tlem.getNode(), - rule, - false, - removable, - preprocess, - sendAtoms ? d_theory : theory::THEORY_LAST); + theory::LemmaStatus result = d_engine->lemma( + tlem, + p, + isLemmaPropertySendAtoms(p) ? d_theory : theory::THEORY_LAST, + d_theory); 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(" @@ -236,8 +94,8 @@ theory::LemmaStatus EngineOutputChannel::splitLemma(TNode lemma, bool removable) Debug("pf::explain") << "EngineOutputChannel::splitLemma( " << lemma << " )" << std::endl; TrustNode tlem = TrustNode::mkTrustLemma(lemma); - theory::LemmaStatus result = d_engine->lemma( - tlem.getNode(), RULE_SPLIT, false, removable, false, d_theory); + LemmaProperty p = removable ? LemmaProperty::REMOVABLE : LemmaProperty::NONE; + theory::LemmaStatus result = d_engine->lemma(tlem, p, d_theory); return result; } @@ -250,17 +108,15 @@ 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); - d_engine->conflict(tConf.getNode(), d_theory); + d_engine->conflict(tConf, d_theory); } void EngineOutputChannel::demandRestart() @@ -273,7 +129,7 @@ void EngineOutputChannel::demandRestart() Trace("theory::restart") << "EngineOutputChannel<" << d_theory << ">::restart(" << restartVar << ")" << std::endl; ++d_statistics.restartDemands; - lemma(restartVar, RULE_INVALID, true); + lemma(restartVar, LemmaProperty::REMOVABLE); } void EngineOutputChannel::requirePhase(TNode n, bool phase) @@ -305,22 +161,21 @@ void EngineOutputChannel::trustedConflict(TrustNode pconf) { Assert(pconf.getKind() == TrustNodeKind::CONFLICT); Trace("theory::conflict") - << "EngineOutputChannel<" << d_theory << ">::conflict(" << pconf.getNode() - << ")" << std::endl; + << "EngineOutputChannel<" << d_theory << ">::trustedConflict(" + << pconf.getNode() << ")" << std::endl; if (pconf.getGenerator() != nullptr) { ++d_statistics.trustedConflicts; } ++d_statistics.conflicts; d_engine->d_outputChannelUsed = true; - d_engine->conflict(pconf.getNode(), d_theory); + d_engine->conflict(pconf, d_theory); } -LemmaStatus EngineOutputChannel::trustedLemma(TrustNode plem, - bool removable, - bool preprocess, - bool sendAtoms) +LemmaStatus EngineOutputChannel::trustedLemma(TrustNode plem, LemmaProperty p) { + Debug("theory::lemma") << "EngineOutputChannel<" << d_theory + << ">::trustedLemma(" << plem << ")" << std::endl; Assert(plem.getKind() == TrustNodeKind::LEMMA); if (plem.getGenerator() != nullptr) { @@ -329,12 +184,11 @@ LemmaStatus EngineOutputChannel::trustedLemma(TrustNode plem, ++d_statistics.lemmas; d_engine->d_outputChannelUsed = true; // now, call the normal interface for lemma - return d_engine->lemma(plem.getNode(), - RULE_INVALID, - false, - removable, - preprocess, - sendAtoms ? d_theory : theory::THEORY_LAST); + return d_engine->lemma( + plem, + p, + isLemmaPropertySendAtoms(p) ? d_theory : theory::THEORY_LAST, + d_theory); } } // namespace theory |