summaryrefslogtreecommitdiff
path: root/src/prop/cnf_stream.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop/cnf_stream.cpp')
-rw-r--r--src/prop/cnf_stream.cpp166
1 files changed, 138 insertions, 28 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index da41b1de4..0c692501f 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -37,6 +37,14 @@ CnfStream::CnfStream(SatInputInterface *satSolver) :
d_satSolver(satSolver) {
}
+void CnfStream::recordTranslation(TNode node) {
+ if (d_assertingLemma) {
+ d_lemmas.push_back(stripNot(node));
+ } else {
+ d_translationTrail.push_back(stripNot(node));
+ }
+}
+
TseitinCnfStream::TseitinCnfStream(SatInputInterface* satSolver) :
CnfStream(satSolver) {
}
@@ -67,42 +75,61 @@ void CnfStream::assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral
assertClause(node, clause);
}
-bool CnfStream::isCached(TNode n) const {
- return d_translationCache.find(n) != d_translationCache.end();
+bool CnfStream::isTranslated(TNode n) const {
+ TranslationCache::const_iterator find = d_translationCache.find(n);
+ return find != d_translationCache.end() && find->second.level >= 0;
}
-SatLiteral CnfStream::lookupInCache(TNode node) const {
- Assert(isCached(node), "Node is not in CNF translation cache");
- return d_translationCache.find(node)->second;
-}
-
-void CnfStream::cacheTranslation(TNode node, SatLiteral lit) {
- Debug("cnf") << "caching translation " << node << " to " << lit << endl;
- // We always cash both the node and the negation at the same time
- d_translationCache[node] = lit;
- d_translationCache[node.notNode()] = ~lit;
+bool CnfStream::hasLiteral(TNode n) const {
+ TranslationCache::const_iterator find = d_translationCache.find(n);
+ return find != d_translationCache.end();
}
SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) {
- SatLiteral lit = Minisat::mkLit(d_satSolver->newVar(theoryLiteral));
- cacheTranslation(node, lit);
+ Debug("cnf") << "newLiteral(" << node << ")" << endl;
+
+ // Get the literal for this node
+ SatLiteral lit;
+ if (!hasLiteral(node)) {
+ // If no literal, well make one
+ lit = Minisat::mkLit(d_satSolver->newVar(theoryLiteral));
+ d_translationCache[node].literal = lit;
+ d_translationCache[node.notNode()].literal = ~lit;
+ } else {
+ // We already have a literal
+ lit = getLiteral(node);
+ d_satSolver->renewVar(lit);
+ }
+
+ // We will translate clauses, so remember the level
+ int level = d_satSolver->getLevel();
+ d_translationCache[node].level = level;
+ d_translationCache[node.notNode()].level = level;
+
+ // If it's a theory literal, store it for back queries
if (theoryLiteral) {
d_nodeCache[lit] = node;
d_nodeCache[~lit] = node.notNode();
}
+
+ // Here, you can have it
+ Debug("cnf") << "newLiteral(" << node << ") => " << lit << endl;
return lit;
}
-Node CnfStream::getNode(const SatLiteral& literal) {
+TNode CnfStream::getNode(const SatLiteral& literal) {
+ Debug("cnf") << "getNode(" << literal << ")" << endl;
NodeCache::iterator find = d_nodeCache.find(literal);
Assert(find != d_nodeCache.end());
+ Assert(d_translationCache.find(find->second) != d_translationCache.end());
+ Debug("cnf") << "getNode(" << literal << ") => " << find->second << endl;
return find->second;
}
SatLiteral CnfStream::convertAtom(TNode node) {
Debug("cnf") << "convertAtom(" << node << ")" << endl;
- Assert(!isCached(node), "atom already mapped!");
+ Assert(!isTranslated(node), "atom already mapped!");
bool theoryLiteral = node.getKind() != kind::VARIABLE;
SatLiteral lit = newLiteral(node, theoryLiteral);
@@ -121,13 +148,13 @@ SatLiteral CnfStream::convertAtom(TNode node) {
SatLiteral CnfStream::getLiteral(TNode node) {
TranslationCache::iterator find = d_translationCache.find(node);
Assert(find != d_translationCache.end(), "Literal not in the CNF Cache");
- SatLiteral literal = find->second;
+ SatLiteral literal = find->second.literal;
Debug("cnf") << "CnfStream::getLiteral(" << node << ") => " << literal << std::endl;
return literal;
}
SatLiteral TseitinCnfStream::handleXor(TNode xorNode) {
- Assert(!isCached(xorNode), "Atom already mapped!");
+ Assert(!isTranslated(xorNode), "Atom already mapped!");
Assert(xorNode.getKind() == XOR, "Expecting an XOR expression!");
Assert(xorNode.getNumChildren() == 2, "Expecting exactly 2 children!");
@@ -145,7 +172,7 @@ SatLiteral TseitinCnfStream::handleXor(TNode xorNode) {
}
SatLiteral TseitinCnfStream::handleOr(TNode orNode) {
- Assert(!isCached(orNode), "Atom already mapped!");
+ Assert(!isTranslated(orNode), "Atom already mapped!");
Assert(orNode.getKind() == OR, "Expecting an OR expression!");
Assert(orNode.getNumChildren() > 1, "Expecting more then 1 child!");
@@ -181,7 +208,7 @@ SatLiteral TseitinCnfStream::handleOr(TNode orNode) {
}
SatLiteral TseitinCnfStream::handleAnd(TNode andNode) {
- Assert(!isCached(andNode), "Atom already mapped!");
+ Assert(!isTranslated(andNode), "Atom already mapped!");
Assert(andNode.getKind() == AND, "Expecting an AND expression!");
Assert(andNode.getNumChildren() > 1, "Expecting more than 1 child!");
@@ -216,7 +243,7 @@ SatLiteral TseitinCnfStream::handleAnd(TNode andNode) {
}
SatLiteral TseitinCnfStream::handleImplies(TNode impliesNode) {
- Assert(!isCached(impliesNode), "Atom already mapped!");
+ Assert(!isTranslated(impliesNode), "Atom already mapped!");
Assert(impliesNode.getKind() == IMPLIES, "Expecting an IMPLIES expression!");
Assert(impliesNode.getNumChildren() == 2, "Expecting exactly 2 children!");
@@ -241,7 +268,7 @@ SatLiteral TseitinCnfStream::handleImplies(TNode impliesNode) {
SatLiteral TseitinCnfStream::handleIff(TNode iffNode) {
- Assert(!isCached(iffNode), "Atom already mapped!");
+ Assert(!isTranslated(iffNode), "Atom already mapped!");
Assert(iffNode.getKind() == IFF, "Expecting an IFF expression!");
Assert(iffNode.getNumChildren() == 2, "Expecting exactly 2 children!");
@@ -273,15 +300,12 @@ SatLiteral TseitinCnfStream::handleIff(TNode iffNode) {
SatLiteral TseitinCnfStream::handleNot(TNode notNode) {
- Assert(!isCached(notNode), "Atom already mapped!");
+ Assert(!isTranslated(notNode), "Atom already mapped!");
Assert(notNode.getKind() == NOT, "Expecting a NOT expression!");
Assert(notNode.getNumChildren() == 1, "Expecting exactly 1 child!");
SatLiteral notLit = ~toCNF(notNode[0]);
- // Since we don't introduce new variables, we need to cache the translation
- cacheTranslation(notNode, notLit);
-
return notLit;
}
@@ -328,8 +352,12 @@ SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) {
Node negatedNode = node.notNode();
// If the non-negated node has already been translated, get the translation
- if(isCached(node)) {
- nodeLit = lookupInCache(node);
+ if(isTranslated(node)) {
+ nodeLit = getLiteral(node);
+ // If we are asserting a lemma, we need to take the whole tree to level 0
+ if (d_assertingLemma) {
+ moveToBaseLevel(node);
+ }
} else {
// Handle each Boolean operator case
switch(node.getKind()) {
@@ -395,6 +423,7 @@ void TseitinCnfStream::convertAndAssertAnd(TNode node, bool lemma, bool negated)
for(int i = 0; i < nChildren; ++ disjunct, ++ i) {
Assert( disjunct != node.end() );
clause[i] = toCNF(*disjunct, true);
+ recordTranslation(*disjunct);
}
Assert(disjunct == node.end());
assertClause(node, clause);
@@ -411,6 +440,7 @@ void TseitinCnfStream::convertAndAssertOr(TNode node, bool lemma, bool negated)
for(int i = 0; i < nChildren; ++ disjunct, ++ i) {
Assert( disjunct != node.end() );
clause[i] = toCNF(*disjunct, false);
+ recordTranslation(*disjunct);
}
Assert(disjunct == node.end());
assertClause(node, clause);
@@ -451,6 +481,8 @@ void TseitinCnfStream::convertAndAssertXor(TNode node, bool lemma, bool negated)
clause2[1] = ~q;
assertClause(node, clause2);
}
+ recordTranslation(node[0]);
+ recordTranslation(node[1]);
}
void TseitinCnfStream::convertAndAssertIff(TNode node, bool lemma, bool negated) {
@@ -481,6 +513,8 @@ void TseitinCnfStream::convertAndAssertIff(TNode node, bool lemma, bool negated)
clause2[1] = q;
assertClause(node, clause2);
}
+ recordTranslation(node[0]);
+ recordTranslation(node[1]);
}
void TseitinCnfStream::convertAndAssertImplies(TNode node, bool lemma, bool negated) {
@@ -493,6 +527,8 @@ void TseitinCnfStream::convertAndAssertImplies(TNode node, bool lemma, bool nega
clause[0] = ~p;
clause[1] = q;
assertClause(node, clause);
+ recordTranslation(node[0]);
+ recordTranslation(node[1]);
} else {// Construct the
// !(p => q) is the same as (p && ~q)
convertAndAssert(node[0], lemma, false);
@@ -523,6 +559,10 @@ void TseitinCnfStream::convertAndAssertIte(TNode node, bool lemma, bool negated)
clause4[0] = r;
clause4[1] = p;
assertClause(node, clause4);
+
+ recordTranslation(node[0]);
+ recordTranslation(node[1]);
+ recordTranslation(node[2]);
}
// At the top level we must ensure that all clauses that are asserted are
@@ -556,9 +596,79 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool lemma, bool negated) {
default:
// Atoms
assertClause(node, toCNF(node, negated));
+ recordTranslation(node);
break;
}
}
+void CnfStream::removeClausesAboveLevel(int level) {
+ while (d_translationTrail.size() > 0) {
+ TNode node = d_translationTrail.back();
+ Debug("cnf") << "Removing node " << node << " from CNF translation" << endl;
+ d_translationTrail.pop_back();
+ // Get the translation informations
+ TranslationInfo& infoPos = d_translationCache.find(node)->second;
+ // If already untranslated, we're done
+ if (infoPos.level == -1) continue;
+ // If the level of the node is less or equal to given we are done
+ if (infoPos.level <= level) break;
+ // Otherwise we have to undo the translation
+ undoTranslate(node, level);
+ }
+}
+
+void CnfStream::undoTranslate(TNode node, int level) {
+ // Get the translation information
+ TranslationInfo& infoPos = d_translationCache.find(node)->second;
+ // If already untranslated, we are done
+ if (infoPos.level == -1) return;
+ // If under the given level we're also done
+ if (infoPos.level <= level) return;
+ // Untranslate
+ infoPos.level = -1;
+ // Untranslate the negation node
+ // If not a not node, unregister it from sat and untranslate the negation
+ if (node.getKind() != kind::NOT) {
+ // Unregister the literal from SAT
+ SatLiteral lit = getLiteral(node);
+ d_satSolver->unregisterVar(lit);
+ // Untranslate the negation
+ TranslationInfo& infoNeg = d_translationCache.find(node.notNode())->second;
+ infoNeg.level = -1;
+ }
+ // undoTranslate the children
+ TNode::iterator child = node.begin();
+ TNode::iterator child_end = node.end();
+ while (child != child_end) {
+ undoTranslate(*child, level);
+ ++ child;
+ }
+}
+
+void CnfStream::moveToBaseLevel(TNode node) {
+ TNode posNode = stripNot(node);
+ TranslationInfo& infoPos = d_translationCache.find(posNode)->second;
+
+ Assert(infoPos.level >= 0);
+ if (infoPos.level == 0) return;
+
+ TNode negNode = node.notNode();
+ TranslationInfo& infoNeg = d_translationCache.find(negNode)->second;
+
+ infoPos.level = 0;
+ infoNeg.level = 0;
+
+ d_satSolver->renewVar(infoPos.literal, 0);
+
+ // undoTranslate the children
+ TNode::iterator child = posNode.begin();
+ TNode::iterator child_end = posNode.end();
+ while (child != child_end) {
+ moveToBaseLevel(*child);
+ ++ child;
+ }
+
+}
+
}/* CVC4::prop namespace */
}/* CVC4 namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback