diff options
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 154 |
1 files changed, 97 insertions, 57 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index dec648688..d176b015d 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -472,12 +472,15 @@ void TheoryEngine::printAssertions(const char* tag) { Trace(tag) << "Assertions of " << theory->getId() << ": " << endl; context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end(); for (unsigned i = 0; it != it_end; ++ it, ++i) { - if ((*it).isPreregistered) { - Trace(tag) << "[" << i << "]: "; - } else { - Trace(tag) << "(" << i << "): "; - } - Trace(tag) << (*it).assertion << endl; + if ((*it).d_isPreregistered) + { + Trace(tag) << "[" << i << "]: "; + } + else + { + Trace(tag) << "(" << i << "): "; + } + Trace(tag) << (*it).d_assertion << endl; } if (d_logicInfo.isSharingEnabled()) { @@ -517,12 +520,15 @@ void TheoryEngine::dumpAssertions(const char* tag) { context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end(); for (; it != it_end; ++ it) { // Get the assertion - Node assertionNode = (*it).assertion; + Node assertionNode = (*it).d_assertion; // Purify all the terms - if ((*it).isPreregistered) { + if ((*it).d_isPreregistered) + { Dump(tag) << CommentCommand("Preregistered"); - } else { + } + else + { Dump(tag) << CommentCommand("Shared assertion"); } Dump(tag) << AssertCommand(assertionNode.toExpr()); @@ -725,14 +731,16 @@ void TheoryEngine::combineTheories() { for (; care_it != care_it_end; ++ care_it) { const CarePair& carePair = *care_it; - Debug("combineTheories") << "TheoryEngine::combineTheories(): checking " << carePair.a << " = " << carePair.b << " from " << carePair.theory << endl; + Debug("combineTheories") + << "TheoryEngine::combineTheories(): checking " << carePair.d_a << " = " + << carePair.d_b << " from " << carePair.d_theory << endl; - Assert(d_sharedTerms.isShared(carePair.a) || carePair.a.isConst()); - Assert(d_sharedTerms.isShared(carePair.b) || carePair.b.isConst()); + Assert(d_sharedTerms.isShared(carePair.d_a) || carePair.d_a.isConst()); + Assert(d_sharedTerms.isShared(carePair.d_b) || carePair.d_b.isConst()); // The equality in question (order for no repetition) - Node equality = carePair.a.eqNode(carePair.b); - // EqualityStatus es = getEqualityStatus(carePair.a, carePair.b); + Node equality = carePair.d_a.eqNode(carePair.d_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" : @@ -746,7 +754,12 @@ void TheoryEngine::combineTheories() { // We need to split on it Debug("combineTheories") << "TheoryEngine::combineTheories(): requesting a split " << endl; - lemma(equality.orNode(equality.notNode()), RULE_INVALID, false, false, false, carePair.theory); + lemma(equality.orNode(equality.notNode()), + RULE_INVALID, + false, + false, + false, + carePair.d_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 @@ -1440,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(); } @@ -1621,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) { @@ -1632,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); @@ -1710,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; @@ -2061,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; @@ -2097,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; } @@ -2122,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; @@ -2147,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); @@ -2189,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()); } } }); @@ -2224,7 +2264,7 @@ void TheoryEngine::checkTheoryAssertionsWithModel(bool hardFailure) { it_end = theory->facts_end(); it != it_end; ++it) { - Node assertion = (*it).assertion; + Node assertion = (*it).d_assertion; Node val = getModel()->getValue(assertion); if (val != d_true) { |