summaryrefslogtreecommitdiff
path: root/src/theory/theory_engine.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r--src/theory/theory_engine.cpp322
1 files changed, 19 insertions, 303 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 618fda4c0..1ab4c228b 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -26,8 +26,6 @@
#include "options/bv_options.h"
#include "options/options.h"
#include "options/quantifiers_options.h"
-#include "proof/cnf_proof.h"
-#include "proof/lemma_proof.h"
#include "proof/proof_manager.h"
#include "proof/theory_proof.h"
#include "smt/ite_removal.h"
@@ -55,104 +53,6 @@ using namespace CVC4::theory;
namespace CVC4 {
-inline void flattenAnd(Node n, std::vector<TNode>& out){
- Assert(n.getKind() == kind::AND);
- for(Node::iterator i=n.begin(), i_end=n.end(); i != i_end; ++i){
- Node curr = *i;
- if(curr.getKind() == kind::AND){
- flattenAnd(curr, out);
- }else{
- out.push_back(curr);
- }
- }
-}
-
-inline Node flattenAnd(Node n){
- std::vector<TNode> out;
- flattenAnd(n, out);
- return NodeManager::currentNM()->mkNode(kind::AND, out);
-}
-
-theory::LemmaStatus TheoryEngine::EngineOutputChannel::lemma(TNode lemma,
- ProofRule rule,
- bool removable,
- bool preprocess,
- bool sendAtoms)
- throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {
- Debug("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << ", preprocess = " << preprocess << std::endl;
- ++ 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);
-
- 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);
- });
-
- theory::LemmaStatus result = d_engine->lemma(lemma,
- rule,
- false,
- removable,
- preprocess,
- sendAtoms ? d_theory : theory::THEORY_LAST,
- proofRecipe);
- PROOF(delete proofRecipe;);
- return result;
-}
-
-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);
- return result;
-}
-
-bool TheoryEngine::EngineOutputChannel::propagate(TNode literal)
- throw(AssertionException, UnsafeInterruptException) {
- Debug("theory::propagate") << "EngineOutputChannel<" << d_theory << ">::propagate(" << literal << ")" << std::endl;
- ++ d_statistics.propagations;
- d_engine->d_outputChannelUsed = true;
- return d_engine->propagate(literal, d_theory);
-}
-
-void TheoryEngine::EngineOutputChannel::conflict(TNode conflictNode, Proof* pf)
- throw(AssertionException, UnsafeInterruptException) {
- Trace("theory::conflict") << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode << ")" << std::endl;
- Assert (pf == NULL); // Theory shouldn't be producing proofs yet
- ++ d_statistics.conflicts;
- d_engine->d_outputChannelUsed = true;
- d_engine->conflict(conflictNode, d_theory);
-}
-
void TheoryEngine::finishInit() {
// initialize the quantifiers engine
d_quantEngine = new QuantifiersEngine(d_context, d_userContext, this);
@@ -597,10 +497,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, 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
// if (true) {
@@ -1066,7 +963,7 @@ bool TheoryEngine::markPropagation(TNode assertion, TNode originalAssertion, the
void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId) {
- Trace("theory::assertToTheory") << "TheoryEngine::assertToTheory(" << assertion << ", " << originalAssertion << "," << toTheoryId << ", " << fromTheoryId << ")" << endl;
+ Trace("theory::assertToTheory") << "TheoryEngine::assertToTheory(" << assertion << ", " << toTheoryId << ", " << fromTheoryId << ")" << endl;
Assert(toTheoryId != fromTheoryId);
if(toTheoryId != THEORY_SAT_SOLVER &&
@@ -1279,23 +1176,6 @@ bool TheoryEngine::propagate(TNode literal, theory::TheoryId theory) {
assertToTheory(literal, literal, /* to */ THEORY_BUILTIN, /* from */ theory);
}
} else {
- // We could be propagating a unit-clause lemma. In this case, we need to provide a
- // recipe.
- // TODO: Consider putting this someplace else? This is the only refence to the proof
- // manager in this class.
-
- PROOF({
- LemmaProofRecipe proofRecipe;
- proofRecipe.addBaseAssertion(literal);
-
- Node emptyNode;
- LemmaProofRecipe::ProofStep proofStep(theory, emptyNode);
- proofStep.addAssertion(literal);
- proofRecipe.addStep(proofStep);
-
- ProofManager::getCnfProof()->setProofRecipe(&proofRecipe);
- });
-
// Just send off to the SAT solver
Assert(d_propEngine->isSatLiteral(literal));
assertToTheory(literal, literal, /* to */ THEORY_SAT_SOLVER, /* from */ theory);
@@ -1390,7 +1270,7 @@ static Node mkExplanation(const std::vector<NodeTheoryPair>& explanation) {
return conjunction;
}
-Node TheoryEngine::getExplanationAndRecipe(TNode node, LemmaProofRecipe* proofRecipe) {
+NodeTheoryPair TheoryEngine::getExplanationAndExplainer(TNode node) {
Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << "): current propagation index = " << d_propagationMapTimestamp << endl;
bool polarity = node.getKind() != kind::NOT;
@@ -1398,90 +1278,32 @@ Node TheoryEngine::getExplanationAndRecipe(TNode node, LemmaProofRecipe* proofRe
// If we're not in shared mode, explanations are simple
if (!d_logicInfo.isSharingEnabled()) {
- Debug("theory::explain") << "TheoryEngine::getExplanation: sharing is NOT enabled. "
- << " Responsible theory is: "
- << theoryOf(atom)->getId() << std::endl;
-
Node explanation = theoryOf(atom)->explain(node);
Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => " << explanation << endl;
- PROOF({
- if(proofRecipe) {
- Node emptyNode;
- LemmaProofRecipe::ProofStep proofStep(theoryOf(atom)->getId(), emptyNode);
- proofStep.addAssertion(node);
- proofRecipe->addBaseAssertion(node);
-
- if (explanation.getKind() == kind::AND) {
- // If the explanation is a conjunction, the recipe for the corresponding lemma is
- // the negation of its conjuncts.
- Node flat = flattenAnd(explanation);
- for (unsigned i = 0; i < flat.getNumChildren(); ++i) {
- if (flat[i].isConst() && flat[i].getConst<bool>()) {
- ++ i;
- continue;
- }
- if (flat[i].getKind() == kind::NOT &&
- flat[i][0].isConst() && !flat[i][0].getConst<bool>()) {
- ++ i;
- continue;
- }
- Debug("theory::explain") << "TheoryEngine::getExplanationAndRecipe: adding recipe assertion: "
- << flat[i].negate() << std::endl;
- proofStep.addAssertion(flat[i].negate());
- proofRecipe->addBaseAssertion(flat[i].negate());
- }
- } else {
- // The recipe for proving it is by negating it. "True" is not an acceptable reason.
- if (!((explanation.isConst() && explanation.getConst<bool>()) ||
- (explanation.getKind() == kind::NOT &&
- explanation[0].isConst() && !explanation[0].getConst<bool>()))) {
- proofStep.addAssertion(explanation.negate());
- proofRecipe->addBaseAssertion(explanation.negate());
- }
- }
-
- proofRecipe->addStep(proofStep);
- }
- });
-
- return explanation;
+ return NodeTheoryPair(explanation, theoryOf(atom)->getId());
}
- Debug("theory::explain") << "TheoryEngine::getExplanation: sharing IS enabled" << std::endl;
-
// Initial thing to explain
NodeTheoryPair toExplain(node, THEORY_SAT_SOLVER, d_propagationMapTimestamp);
Assert(d_propagationMap.find(toExplain) != d_propagationMap.end());
NodeTheoryPair nodeExplainerPair = d_propagationMap[toExplain];
- Debug("theory::explain") << "TheoryEngine::getExplanation: explainer for node "
- << nodeExplainerPair.node
- << " is theory: " << nodeExplainerPair.theory << std::endl;
TheoryId explainer = nodeExplainerPair.theory;
// Create the workplace for explanations
std::vector<NodeTheoryPair> explanationVector;
explanationVector.push_back(d_propagationMap[toExplain]);
// Process the explanation
- if (proofRecipe) {
- Node emptyNode;
- LemmaProofRecipe::ProofStep proofStep(explainer, emptyNode);
- proofStep.addAssertion(node);
- proofRecipe->addStep(proofStep);
- proofRecipe->addBaseAssertion(node);
- }
-
- getExplanation(explanationVector, proofRecipe);
+ getExplanation(explanationVector);
Node explanation = mkExplanation(explanationVector);
Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => " << explanation << endl;
- return explanation;
+ return NodeTheoryPair(explanation, explainer);
}
Node TheoryEngine::getExplanation(TNode node) {
- LemmaProofRecipe *dontCareRecipe = NULL;
- return getExplanationAndRecipe(node, dontCareRecipe);
+ return getExplanationAndExplainer(node).node;
}
struct AtomsCollect {
@@ -1584,7 +1406,7 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
bool removable,
bool preprocess,
theory::TheoryId atomsTo,
- LemmaProofRecipe* proofRecipe) {
+ theory::TheoryId ownerTheory) {
// For resource-limiting (also does a time check).
// spendResource();
@@ -1634,10 +1456,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, ownerTheory, 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, ownerTheory, node);
}
// WARNING: Below this point don't assume additionalLemmas[0] to be not negated.
@@ -1671,69 +1493,22 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
<< CheckSatCommand(conflict.toExpr());
}
- LemmaProofRecipe* proofRecipe = NULL;
- PROOF({
- proofRecipe = new LemmaProofRecipe;
- Node emptyNode;
- LemmaProofRecipe::ProofStep proofStep(theoryId, emptyNode);
-
- if (conflict.getKind() == kind::AND) {
- for (unsigned i = 0; i < conflict.getNumChildren(); ++i) {
- proofStep.addAssertion(conflict[i].negate());
- }
- } else {
- proofStep.addAssertion(conflict.negate());
- }
-
- proofRecipe->addStep(proofStep);
- });
-
// In the multiple-theories case, we need to reconstruct the conflict
if (d_logicInfo.isSharingEnabled()) {
// Create the workplace for explanations
std::vector<NodeTheoryPair> explanationVector;
explanationVector.push_back(NodeTheoryPair(conflict, theoryId, d_propagationMapTimestamp));
-
// Process the explanation
- getExplanation(explanationVector, proofRecipe);
+ getExplanation(explanationVector);
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, theoryId);
} else {
// When only one theory, the conflict should need no processing
Assert(properConflict(conflict));
- PROOF({
- if (conflict.getKind() == kind::AND) {
- // If the conflict is a conjunction, the corresponding lemma is derived by negating
- // its conjuncts.
- for (unsigned i = 0; i < conflict.getNumChildren(); ++i) {
- if (conflict[i].isConst() && conflict[i].getConst<bool>()) {
- ++ i;
- continue;
- }
- if (conflict[i].getKind() == kind::NOT &&
- conflict[i][0].isConst() && !conflict[i][0].getConst<bool>()) {
- ++ i;
- continue;
- }
- proofRecipe->getStep(0)->addAssertion(conflict[i].negate());
- proofRecipe->addBaseAssertion(conflict[i].negate());
- }
- } else {
- proofRecipe->getStep(0)->addAssertion(conflict.negate());
- proofRecipe->addBaseAssertion(conflict.negate());
- }
- });
-
- lemma(conflict, RULE_CONFLICT, true, true, false, THEORY_LAST, proofRecipe);
+ lemma(conflict, RULE_CONFLICT, true, true, false, THEORY_LAST, theoryId);
}
-
- PROOF({
- delete proofRecipe;
- proofRecipe = NULL;
- });
}
void TheoryEngine::staticInitializeBVOptions(const std::vector<Node>& assertions) {
@@ -1885,21 +1660,19 @@ bool TheoryEngine::donePPSimpITE(std::vector<Node>& assertions){
return result;
}
-void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector, LemmaProofRecipe* proofRecipe) {
+void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector)
+{
Assert(explanationVector.size() > 0);
unsigned i = 0; // Index of the current literal we are processing
unsigned j = 0; // Index of the last literal we are keeping
- std::set<Node> inputAssertions;
- PROOF(inputAssertions = proofRecipe->getStep(0)->getAssertions(););
-
while (i < explanationVector.size()) {
+
// Get the current literal to explain
NodeTheoryPair toExplain = explanationVector[i];
- Debug("theory::explain") << "[i=" << i << "] TheoryEngine::explain(): processing [" << toExplain.timestamp << "] " << toExplain.node << " sent from " << toExplain.theory << endl;
-
+ Debug("theory::explain") << "TheoryEngine::explain(): processing [" << toExplain.timestamp << "] " << toExplain.node << " sent from " << toExplain.theory << endl;
// If a true constant or a negation of a false constant we can ignore it
if (toExplain.node.isConst() && toExplain.node.getConst<bool>()) {
@@ -1913,7 +1686,6 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector
// If from the SAT solver, keep it
if (toExplain.theory == THEORY_SAT_SOLVER) {
- Debug("theory::explain") << "\tLiteral came from THEORY_SAT_SOLVER. Kepping it." << endl;
explanationVector[j++] = explanationVector[i++];
continue;
}
@@ -1932,26 +1704,10 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector
// See if it was sent to the theory by another theory
PropagationMap::const_iterator find = d_propagationMap.find(toExplain);
if (find != d_propagationMap.end()) {
- Debug("theory::explain") << "\tTerm was propagated by another theory (theory = "
- << theoryOf((*find).second.theory)->getId() << ")" << std::endl;
// There is some propagation, check if its a timely one
if ((*find).second.timestamp < toExplain.timestamp) {
- Debug("theory::explain") << "\tRelevant timetsamp, pushing "
- << (*find).second.node << "to index = " << explanationVector.size() << std::endl;
explanationVector.push_back((*find).second);
- ++i;
-
- PROOF({
- if (toExplain.node != (*find).second.node) {
- Debug("pf::explain") << "TheoryEngine::getExplanation: Rewrite alert! toAssert = " << toExplain.node
- << ", toExplain = " << (*find).second.node << std::endl;
-
- if (proofRecipe) {
- proofRecipe->addRewriteRule(toExplain.node, (*find).second.node);
- }
- }
- })
-
+ ++ i;
continue;
}
}
@@ -1960,62 +1716,22 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector
Node explanation;
if (toExplain.theory == THEORY_BUILTIN) {
explanation = d_sharedTerms.explain(toExplain.node);
- Debug("theory::explain") << "\tTerm was propagated by THEORY_BUILTIN. Explanation: " << explanation << std::endl;
} else {
explanation = theoryOf(toExplain.theory)->explain(toExplain.node);
- Debug("theory::explain") << "\tTerm was propagated by owner theory: "
- << theoryOf(toExplain.theory)->getId()
- << ". Explanation: " << explanation << std::endl;
}
-
Debug("theory::explain") << "TheoryEngine::explain(): got explanation " << explanation << " got from " << toExplain.theory << endl;
Assert(explanation != toExplain.node, "wasn't sent to you, so why are you explaining it trivially");
// Mark the explanation
NodeTheoryPair newExplain(explanation, toExplain.theory, toExplain.timestamp);
explanationVector.push_back(newExplain);
-
++ i;
-
- PROOF({
- if (proofRecipe) {
- // If we're expanding the target node of the explanation (this is the first expansion...),
- // we don't want to add it as a separate proof step. It is already part of the assertions.
- if (inputAssertions.find(toExplain.node) == inputAssertions.end()) {
- LemmaProofRecipe::ProofStep proofStep(toExplain.theory, toExplain.node);
- if (explanation.getKind() == kind::AND) {
- Node flat = flattenAnd(explanation);
- for (unsigned k = 0; k < flat.getNumChildren(); ++ k) {
- // If a true constant or a negation of a false constant we can ignore it
- if (! ((flat[k].isConst() && flat[k].getConst<bool>()) ||
- (flat[k].getKind() == kind::NOT && flat[k][0].isConst() && !flat[k][0].getConst<bool>()))) {
- proofStep.addAssertion(flat[k].negate());
- }
- }
- } else {
- if (! ((explanation.isConst() && explanation.getConst<bool>()) ||
- (explanation.getKind() == kind::NOT && explanation[0].isConst() && !explanation[0].getConst<bool>()))) {
- proofStep.addAssertion(explanation.negate());
- }
- }
- proofRecipe->addStep(proofStep);
- }
- }
- });
}
// Keep only the relevant literals
explanationVector.resize(j);
-
- PROOF({
- if (proofRecipe) {
- // The remaining literals are the base of the proof
- for (unsigned k = 0; k < explanationVector.size(); ++k) {
- proofRecipe->addBaseAssertion(explanationVector[k].node.negate());
- }
- }
- });
}
+
void TheoryEngine::ppUnconstrainedSimp(vector<Node>& assertions)
{
d_unconstrainedSimp->processAssertions(assertions);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback