summaryrefslogtreecommitdiff
path: root/src/theory/engine_output_channel.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/engine_output_channel.cpp')
-rw-r--r--src/theory/engine_output_channel.cpp153
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);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback