diff options
author | Tim King <taking@cs.nyu.edu> | 2010-06-29 20:53:47 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-06-29 20:53:47 +0000 |
commit | e792bb8628ea7010fa9c452bf1aa7ba1b60291a3 (patch) | |
tree | ddc12f92092627b7aee2a63dca8dd66279b2970e /src/prop/sat.cpp | |
parent | e7e9c10006b5b243a73832ed97c5dec79df6c90a (diff) |
Merging the unate-propagator branch into the trunk. This is a big update so expect a little turbulence. This commit will not compile. There will be a second commit that fixes this in a moment. I am delaying a change to avoid svn whining about a conflict.
Diffstat (limited to 'src/prop/sat.cpp')
-rw-r--r-- | src/prop/sat.cpp | 45 |
1 files changed, 43 insertions, 2 deletions
diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp index 207bda4db..a7b536a57 100644 --- a/src/prop/sat.cpp +++ b/src/prop/sat.cpp @@ -26,9 +26,9 @@ namespace CVC4 { namespace prop { -void SatSolver::theoryCheck(SatClause& conflict) { +void SatSolver::theoryCheck(theory::Theory::Effort effort, SatClause& conflict) { // Try theory propagation - bool ok = d_theoryEngine->check(theory::Theory::FULL_EFFORT); + bool ok = d_theoryEngine->check(effort); // If in conflict construct the conflict clause if (!ok) { // We have a conflict, get it @@ -47,6 +47,47 @@ void SatSolver::theoryCheck(SatClause& conflict) { } } +void SatSolver::theoryPropagate(std::vector<SatLiteral>& output) { + // Propagate + d_theoryEngine->propagate(); + // Get the propagated literals + const std::vector<TNode>& outputNodes = d_theoryEngine->getPropagatedLiterals(); + // If any literals, make a clause + const unsigned i_end = outputNodes.size(); + for (unsigned i = 0; i < i_end; ++ i) { + Debug("prop-explain") << "theoryPropagate() => " << outputNodes[i].toString() << endl; + // The second argument ("true") instructs the CNF stream to create + // a new literal mapping if it doesn't exist. This can happen due + // to a circular dependence, if a SAT literal "a" is asserted as a + // unit to the SAT solver, a round of theory propagation can occur + // before all Nodes have SAT variable mappings. + SatLiteral l = d_cnfStream->getLiteral(outputNodes[i], true); + output.push_back(l); + } +} + +void SatSolver::explainPropagation(SatLiteral l, SatClause& explanation) { + TNode lNode = d_cnfStream->getNode(l); + Debug("prop-explain") << "explainPropagation(" << lNode.toString() << ")" << endl; + Node theoryExplanation = d_theoryEngine->getExplanation(lNode); + Debug("prop-explain") << "explainPropagation() => " << theoryExplanation.toString() << endl; + if (lNode.getKind() == kind::AND) { + Node::const_iterator it = theoryExplanation.begin(); + Node::const_iterator it_end = theoryExplanation.end(); + explanation.push(l); + for (; it != it_end; ++ it) { + explanation.push(~d_cnfStream->getLiteral(*it)); + } + } else { + explanation.push(l); + explanation.push(~d_cnfStream->getLiteral(theoryExplanation)); + } +} + +void SatSolver::clearPropagatedLiterals() { + d_theoryEngine->clearPropagatedLiterals(); +} + void SatSolver::enqueueTheoryLiteral(const SatLiteral& l) { Node literalNode = d_cnfStream->getNode(l); Debug("prop") << "enqueueing theory literal " << l << " " << literalNode << std::endl; |