diff options
Diffstat (limited to 'src/theory/theory_engine.cpp')
| -rw-r--r-- | src/theory/theory_engine.cpp | 111 |
1 files changed, 69 insertions, 42 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index a3c74e7e2..d176b015d 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -740,7 +740,7 @@ void TheoryEngine::combineTheories() { // The equality in question (order for no repetition) Node equality = carePair.d_a.eqNode(carePair.d_b); - // EqualityStatus es = getEqualityStatus(carePair.a, carePair.b); + // EqualityStatus es = getEqualityStatus(carePair.d_a, carePair.d_b); // Debug("combineTheories") << "TheoryEngine::combineTheories(): " << // (es == EQUALITY_TRUE_AND_PROPAGATED ? "EQUALITY_TRUE_AND_PROPAGATED" : // es == EQUALITY_FALSE_AND_PROPAGATED ? "EQUALITY_FALSE_AND_PROPAGATED" : @@ -1453,9 +1453,11 @@ void TheoryEngine::assertFact(TNode literal) AtomRequests::atom_iterator it = d_atomRequests.getAtomIterator(atom); while (!it.done()) { const AtomRequests::Request& request = it.get(); - Node toAssert = polarity ? (Node) request.atom : request.atom.notNode(); + Node toAssert = + polarity ? (Node)request.d_atom : request.d_atom.notNode(); Debug("theory::atoms") << "TheoryEngine::assertFact(" << literal << "): sending requested " << toAssert << endl; - assertToTheory(toAssert, literal, request.toTheory, THEORY_SAT_SOLVER); + assertToTheory( + toAssert, literal, request.d_toTheory, THEORY_SAT_SOLVER); it.next(); } @@ -1634,8 +1636,8 @@ static Node mkExplanation(const std::vector<NodeTheoryPair>& explanation) { std::set<TNode> all; for (unsigned i = 0; i < explanation.size(); ++ i) { - Assert(explanation[i].theory == THEORY_SAT_SOLVER); - all.insert(explanation[i].node); + Assert(explanation[i].d_theory == THEORY_SAT_SOLVER); + all.insert(explanation[i].d_node); } if (all.size() == 0) { @@ -1645,7 +1647,7 @@ static Node mkExplanation(const std::vector<NodeTheoryPair>& explanation) { if (all.size() == 1) { // All the same, or just one - return explanation[0].node; + return explanation[0].d_node; } NodeBuilder<> conjunction(kind::AND); @@ -1723,10 +1725,11 @@ Node TheoryEngine::getExplanationAndRecipe(TNode node, LemmaProofRecipe* proofRe 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; + Debug("theory::explain") + << "TheoryEngine::getExplanation: explainer for node " + << nodeExplainerPair.d_node + << " is theory: " << nodeExplainerPair.d_theory << std::endl; + TheoryId explainer = nodeExplainerPair.d_theory; // Create the workplace for explanations std::vector<NodeTheoryPair> explanationVector; @@ -2074,31 +2077,42 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector // 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") + << "[i=" << i << "] TheoryEngine::explain(): processing [" + << toExplain.d_timestamp << "] " << toExplain.d_node << " sent from " + << toExplain.d_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>()) { + if (toExplain.d_node.isConst() && toExplain.d_node.getConst<bool>()) + { ++ i; continue; } - if (toExplain.node.getKind() == kind::NOT && toExplain.node[0].isConst() && !toExplain.node[0].getConst<bool>()) { + if (toExplain.d_node.getKind() == kind::NOT && toExplain.d_node[0].isConst() + && !toExplain.d_node[0].getConst<bool>()) + { ++ i; continue; } // If from the SAT solver, keep it - if (toExplain.theory == THEORY_SAT_SOLVER) { + if (toExplain.d_theory == THEORY_SAT_SOLVER) + { Debug("theory::explain") << "\tLiteral came from THEORY_SAT_SOLVER. Kepping it." << endl; explanationVector[j++] = explanationVector[i++]; continue; } // If an and, expand it - if (toExplain.node.getKind() == kind::AND) { - Debug("theory::explain") << "TheoryEngine::explain(): expanding " << toExplain.node << " got from " << toExplain.theory << endl; - for (unsigned k = 0; k < toExplain.node.getNumChildren(); ++ k) { - NodeTheoryPair newExplain(toExplain.node[k], toExplain.theory, toExplain.timestamp); + if (toExplain.d_node.getKind() == kind::AND) + { + Debug("theory::explain") + << "TheoryEngine::explain(): expanding " << toExplain.d_node + << " got from " << toExplain.d_theory << endl; + for (unsigned k = 0; k < toExplain.d_node.getNumChildren(); ++k) + { + NodeTheoryPair newExplain( + toExplain.d_node[k], toExplain.d_theory, toExplain.d_timestamp); explanationVector.push_back(newExplain); } ++ i; @@ -2110,24 +2124,31 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector if (find != d_propagationMap.end()) { Debug("theory::explain") << "\tTerm was propagated by another theory (theory = " - << getTheoryString((*find).second.theory) << ")" << std::endl; + << getTheoryString((*find).second.d_theory) << ")" << 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; + if ((*find).second.d_timestamp < toExplain.d_timestamp) + { + Debug("theory::explain") + << "\tRelevant timetsamp, pushing " << (*find).second.d_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 (toExplain.d_node != (*find).second.d_node) + { + Debug("pf::explain") + << "TheoryEngine::getExplanation: Rewrite alert! toAssert = " + << toExplain.d_node << ", toExplain = " << (*find).second.d_node + << std::endl; - if (proofRecipe) { - proofRecipe->addRewriteRule(toExplain.node, (*find).second.node); - } + if (proofRecipe) + { + proofRecipe->addRewriteRule(toExplain.d_node, + (*find).second.d_node); } - }) + } + }) continue; } @@ -2135,21 +2156,27 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector // It was produced by the theory, so ask for an explanation Node explanation; - if (toExplain.theory == THEORY_BUILTIN) { - explanation = d_sharedTerms.explain(toExplain.node); + if (toExplain.d_theory == THEORY_BUILTIN) + { + explanation = d_sharedTerms.explain(toExplain.d_node); Debug("theory::explain") << "\tTerm was propagated by THEORY_BUILTIN. Explanation: " << explanation << std::endl; - } else { - explanation = theoryOf(toExplain.theory)->explain(toExplain.node); + } + else + { + explanation = theoryOf(toExplain.d_theory)->explain(toExplain.d_node); Debug("theory::explain") << "\tTerm was propagated by owner theory: " - << theoryOf(toExplain.theory)->getId() + << theoryOf(toExplain.d_theory)->getId() << ". Explanation: " << explanation << std::endl; } - Debug("theory::explain") << "TheoryEngine::explain(): got explanation " << explanation << " got from " << toExplain.theory << endl; - Assert(explanation != toExplain.node) + Debug("theory::explain") + << "TheoryEngine::explain(): got explanation " << explanation + << " got from " << toExplain.d_theory << endl; + Assert(explanation != toExplain.d_node) << "wasn't sent to you, so why are you explaining it trivially"; // Mark the explanation - NodeTheoryPair newExplain(explanation, toExplain.theory, toExplain.timestamp); + NodeTheoryPair newExplain( + explanation, toExplain.d_theory, toExplain.d_timestamp); explanationVector.push_back(newExplain); ++ i; @@ -2160,10 +2187,10 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector // 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 (!ContainsKey(*inputAssertions, toExplain.node)) + if (!ContainsKey(*inputAssertions, toExplain.d_node)) { - LemmaProofRecipe::ProofStep proofStep(toExplain.theory, - toExplain.node); + LemmaProofRecipe::ProofStep proofStep(toExplain.d_theory, + toExplain.d_node); if (explanation.getKind() == kind::AND) { Node flat = flattenAnd(explanation); @@ -2202,7 +2229,7 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector 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()); + proofRecipe->addBaseAssertion(explanationVector[k].d_node.negate()); } } }); |