summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/prop/cnf_stream.cpp9
-rw-r--r--src/prop/cnf_stream.h8
-rw-r--r--src/prop/prop_engine.cpp3
-rw-r--r--src/prop/prop_engine.h3
-rw-r--r--src/prop/theory_proxy.cpp3
-rw-r--r--src/theory/theory_engine.cpp95
-rw-r--r--src/theory/theory_engine.h10
7 files changed, 67 insertions, 64 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index eda736b8a..f2401041e 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -678,8 +678,7 @@ void TseitinCnfStream::convertAndAssert(TNode node,
bool removable,
bool negated,
ProofRule proof_id,
- TNode from,
- LemmaProofRecipe* proofRecipe) {
+ TNode from) {
Debug("cnf") << "convertAndAssert(" << node
<< ", removable = " << (removable ? "true" : "false")
<< ", negated = " << (negated ? "true" : "false") << ")" << endl;
@@ -689,12 +688,6 @@ void TseitinCnfStream::convertAndAssert(TNode node,
Node assertion = negated ? node.notNode() : (Node)node;
Node from_assertion = negated? from.notNode() : (Node) from;
- if (proofRecipe) {
- Debug("pf::sat") << "TseitinCnfStream::convertAndAssert: setting proof recipe" << std::endl;
- proofRecipe->dump("pf::sat");
- d_cnfProof->setProofRecipe(proofRecipe);
- }
-
if (proof_id != RULE_INVALID) {
d_cnfProof->pushCurrentAssertion(from.isNull() ? assertion : from_assertion);
d_cnfProof->registerAssertion(from.isNull() ? assertion : from_assertion, proof_id);
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 6cc10d878..661108dd0 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -37,8 +37,6 @@
namespace CVC4 {
-class LemmaProofRecipe;
-
namespace prop {
class PropEngine;
@@ -210,9 +208,8 @@ public:
* @param node node to convert and assert
* @param removable whether the sat solver can choose to remove the clauses
* @param negated whether we are asserting the node negated
- * @param proofRecipe contains the proof recipe for proving this node
*/
- virtual void convertAndAssert(TNode node, bool removable, bool negated, ProofRule proof_id, TNode from = TNode::null(), LemmaProofRecipe* proofRecipe = NULL) = 0;
+ virtual void convertAndAssert(TNode node, bool removable, bool negated, ProofRule proof_id, TNode from = TNode::null()) = 0;
/**
* Get the node that is represented by the given SatLiteral.
@@ -282,8 +279,7 @@ public:
* @param negated true if negated
*/
void convertAndAssert(TNode node, bool removable,
- bool negated, ProofRule rule, TNode from = TNode::null(),
- LemmaProofRecipe* proofRecipe = NULL);
+ bool negated, ProofRule rule, TNode from = TNode::null());
/**
* Constructs the stream to use the given sat solver.
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index eb607e901..6cdf17f30 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -132,13 +132,12 @@ void PropEngine::assertFormula(TNode node) {
void PropEngine::assertLemma(TNode node, bool negated,
bool removable,
ProofRule rule,
- LemmaProofRecipe* proofRecipe,
TNode from) {
//Assert(d_inCheckSat, "Sat solver should be in solve()!");
Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl;
// Assert as (possibly) removable
- d_cnfStream->convertAndAssert(node, removable, negated, rule, from, proofRecipe);
+ d_cnfStream->convertAndAssert(node, removable, negated, rule, from);
}
void PropEngine::requirePhase(TNode n, bool phase) {
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index c02015931..f966def26 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -37,7 +37,6 @@ namespace CVC4 {
class ResourceManager;
class DecisionEngine;
class TheoryEngine;
-class LemmaProofRecipe;
namespace theory {
class TheoryRegistrar;
@@ -135,7 +134,7 @@ public:
* @param removable whether this lemma can be quietly removed based
* on an activity heuristic (or not)
*/
- void assertLemma(TNode node, bool negated, bool removable, ProofRule rule, LemmaProofRecipe* proofRecipe, TNode from = TNode::null());
+ void assertLemma(TNode node, bool negated, bool removable, ProofRule rule, TNode from = TNode::null());
/**
* If ever n is decided upon, it must be in the given phase. This
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 6e8f1fbbf..5f5eac733 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -181,8 +181,7 @@ void TheoryProxy::notifyRestart() {
Debug("shared") << "=) " << asNode << std::endl;
}
- LemmaProofRecipe* noProofRecipe = NULL;
- d_propEngine->assertLemma(d_theoryEngine->preprocess(asNode), false, true, RULE_INVALID, noProofRecipe);
+ d_propEngine->assertLemma(d_theoryEngine->preprocess(asNode), false, true, RULE_INVALID);
} else {
Debug("shared") << "=(" << asNode << std::endl;
}
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 0ec55a5e6..0aaf602e3 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -83,35 +83,8 @@ theory::LemmaStatus TheoryEngine::EngineOutputChannel::lemma(TNode lemma,
++ d_statistics.lemmas;
d_engine->d_outputChannelUsed = true;
- LemmaProofRecipe* proofRecipe = NULL;
PROOF({
- // Theory lemmas have one step that proves the empty clause
- proofRecipe = new LemmaProofRecipe;
-
- Node emptyNode;
- LemmaProofRecipe::ProofStep proofStep(d_theory, emptyNode);
-
- proofRecipe->setOriginalLemma(lemma);
-
- Node rewritten;
- if (lemma.getKind() == kind::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);
+ registerLemmaRecipe(lemma, lemma, d_theory);
});
theory::LemmaStatus result = d_engine->lemma(lemma,
@@ -119,22 +92,59 @@ theory::LemmaStatus TheoryEngine::EngineOutputChannel::lemma(TNode lemma,
false,
removable,
preprocess,
- sendAtoms ? d_theory : theory::THEORY_LAST,
- proofRecipe);
- PROOF(delete proofRecipe;);
+ sendAtoms ? d_theory : theory::THEORY_LAST);
+ // PROOF(delete proofRecipe;);
return result;
}
+void TheoryEngine::EngineOutputChannel::registerLemmaRecipe(Node lemma, Node originalLemma, 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.
+ if (lemma.getKind() == kind::AND) {
+ for (unsigned i = 0; i < lemma.getNumChildren(); ++i)
+ registerLemmaRecipe(lemma[i], originalLemma, theoryId);
+ }
+
+ // 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() == kind::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 TheoryEngine::EngineOutputChannel::splitLemma(TNode lemma, bool removable)
throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {
Debug("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl;
++ d_statistics.lemmas;
d_engine->d_outputChannelUsed = true;
-
- LemmaProofRecipe* proofRecipe = NULL;
Debug("pf::explain") << "TheoryEngine::EngineOutputChannel::splitLemma( " << lemma << " )" << std::endl;
- theory::LemmaStatus result = d_engine->lemma(lemma, RULE_SPLIT, false, removable, false, d_theory, proofRecipe);
+ theory::LemmaStatus result = d_engine->lemma(lemma, RULE_SPLIT, false, removable, false, d_theory);
return result;
}
@@ -629,8 +639,7 @@ void TheoryEngine::combineTheories() {
// We need to split on it
Debug("combineTheories") << "TheoryEngine::combineTheories(): requesting a split " << endl;
- LemmaProofRecipe* proofRecipe = NULL;
- lemma(equality.orNode(equality.notNode()), RULE_INVALID, false, false, false, carePair.theory, proofRecipe);
+ lemma(equality.orNode(equality.notNode()), RULE_INVALID, false, false, false, carePair.theory);
// This code is supposed to force preference to follow what the theory models already have
// but it doesn't seem to make a big difference - need to explore more -Clark
@@ -1616,8 +1625,7 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
bool negated,
bool removable,
bool preprocess,
- theory::TheoryId atomsTo,
- LemmaProofRecipe* proofRecipe) {
+ theory::TheoryId atomsTo) {
// For resource-limiting (also does a time check).
// spendResource();
@@ -1667,10 +1675,10 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
}
// assert to prop engine
- d_propEngine->assertLemma(additionalLemmas[0], negated, removable, rule, proofRecipe, node);
+ d_propEngine->assertLemma(additionalLemmas[0], negated, removable, rule, node);
for (unsigned i = 1; i < additionalLemmas.size(); ++ i) {
additionalLemmas[i] = theory::Rewriter::rewrite(additionalLemmas[i]);
- d_propEngine->assertLemma(additionalLemmas[i], false, removable, rule, proofRecipe, node);
+ d_propEngine->assertLemma(additionalLemmas[i], false, removable, rule, node);
}
// WARNING: Below this point don't assume additionalLemmas[0] to be not negated.
@@ -1729,10 +1737,11 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
// Process the explanation
getExplanation(explanationVector, proofRecipe);
+ PROOF(ProofManager::getCnfProof()->setProofRecipe(proofRecipe));
Node fullConflict = mkExplanation(explanationVector);
Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): full = " << fullConflict << endl;
Assert(properConflict(fullConflict));
- lemma(fullConflict, RULE_CONFLICT, true, true, false, THEORY_LAST, proofRecipe);
+ lemma(fullConflict, RULE_CONFLICT, true, true, false, THEORY_LAST);
} else {
// When only one theory, the conflict should need no processing
@@ -1758,9 +1767,11 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
proofRecipe->getStep(0)->addAssertion(conflict.negate());
proofRecipe->addBaseAssertion(conflict.negate());
}
+
+ ProofManager::getCnfProof()->setProofRecipe(proofRecipe);
});
- lemma(conflict, RULE_CONFLICT, true, true, false, THEORY_LAST, proofRecipe);
+ lemma(conflict, RULE_CONFLICT, true, true, false, THEORY_LAST);
}
PROOF({
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index eed58864a..ea8628f9c 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -322,6 +322,13 @@ class TheoryEngine {
void handleUserAttribute( const char* attr, theory::Theory* t ){
d_engine->handleUserAttribute( attr, t );
}
+
+ private:
+
+ /**
+ * A helper function for registering lemma recipes with the proof engine
+ */
+ void registerLemmaRecipe(Node lemma, Node originalLemma, theory::TheoryId theoryId);
};/* class TheoryEngine::EngineOutputChannel */
/**
@@ -429,8 +436,7 @@ class TheoryEngine {
bool negated,
bool removable,
bool preprocess,
- theory::TheoryId atomsTo,
- LemmaProofRecipe* proofRecipe);
+ theory::TheoryId atomsTo);
/** Enusre that the given atoms are send to the given theory */
void ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::TheoryId theory);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback