diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-03-01 14:48:04 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-03-01 14:48:04 +0000 |
commit | 45a138c326da72890bf889a3670aad503ef4aa1e (patch) | |
tree | fa0c9a8497d0b33f78a9f19212152a61392825cc /src/prop/cnf_stream.cpp | |
parent | 8c0b2d6db32103268f84d89c0d0545c7eb504069 (diff) |
Partial merge from kind-backend branch, including Minisat and CNF work to
support incrementality.
Some clean-up work will likely follow, but the CNF/Minisat stuff should be
left pretty much untouched.
Expected performance change negligible; slightly better on memory:
http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3705&reference_id=3697&mode=&category=&p=5
Note that there are crashes, but that these are exhibited in the nightly
regression run too!
Diffstat (limited to 'src/prop/cnf_stream.cpp')
-rw-r--r-- | src/prop/cnf_stream.cpp | 75 |
1 files changed, 66 insertions, 9 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 9f49d81a2..396454fac 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -50,9 +50,19 @@ CnfStream::CnfStream(SatSolverInterface *satSolver, Registrar* registrar, bool f d_registrar(registrar) { } -void CnfStream::recordTranslation(TNode node) { +void CnfStream::recordTranslation(TNode node, bool alwaysRecord) { + Debug("cnf") << "recordTranslation(" << alwaysRecord << "," << d_removable << "): " << node << std::endl; if (!d_removable) { - d_translationTrail.push_back(stripNot(node)); + node = stripNot(node); + if(d_translationCache.find(node)->second.recorded) { + Debug("cnf") << "--> Already recorded, not recording again." << std::endl; + } else { + Debug("cnf") << "--> Recorded at position " << d_translationTrail.size() << ". (level " << d_translationCache.find(node)->second.level << ")" << std::endl; + Assert(d_translationTrail.empty() || d_translationCache.find(node)->second.level >= d_translationCache.find(d_translationTrail.back())->second.level, "levels on the translation trail should be monotonically increasing ?!"); + d_translationTrail.push_back(node); + d_translationCache.find(node)->second.recorded = true; + d_translationCache.find(node.notNode())->second.recorded = true; + } } } @@ -112,7 +122,8 @@ bool CnfStream::hasLiteral(TNode n) const { void TseitinCnfStream::ensureLiteral(TNode n) { if(hasLiteral(n)) { // Already a literal! - SatLiteral lit = getLiteral(n); + // newLiteral() may be necessary to renew a previously-extant literal + SatLiteral lit = isTranslated(n) ? getLiteral(n) : newLiteral(n, true); NodeCache::iterator i = d_nodeCache.find(lit); if(i == d_nodeCache.end()) { // Store backward-mappings @@ -158,11 +169,12 @@ void TseitinCnfStream::ensureLiteral(TNode n) { SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) { Debug("cnf") << "newLiteral(" << node << ", " << theoryLiteral << ")" << endl; + Assert(node.getKind() != kind::NOT); // Get the literal for this node SatLiteral lit; if (!hasLiteral(node)) { - // If no literal, well make one + // If no literal, we'll make one lit = SatLiteral(d_satSolver->newVar(theoryLiteral)); d_translationCache[node].literal = lit; d_translationCache[node.notNode()].literal = ~lit; @@ -174,13 +186,15 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) { // We will translate clauses, so remember the level int level = d_satSolver->getAssertionLevel(); + d_translationCache[node].recorded = false; + d_translationCache[node.notNode()].recorded = false; d_translationCache[node].level = level; d_translationCache[node.notNode()].level = level; // If it's a theory literal, need to store it for back queries if ( theoryLiteral || d_fullLitToNodeMap || ( CVC4_USE_REPLAY && Options::current()->replayLog != NULL ) || - Dump.isOn("clauses") ) { + (Dump.isOn("clauses")) ) { d_nodeCache[lit] = node; d_nodeCache[~lit] = node.notNode(); } @@ -223,6 +237,11 @@ SatLiteral CnfStream::convertAtom(TNode node) { } } + // We have a literal, so it has to be recorded. The definitional clauses + // go away on user-pop, so this literal will have to be re-vivified if it's + // used subsequently. + recordTranslation(node, true); + return lit; } @@ -250,6 +269,11 @@ SatLiteral TseitinCnfStream::handleXor(TNode xorNode) { assertClause(xorNode, a, ~b, xorLit); assertClause(xorNode, ~a, b, xorLit); + // We have a literal, so it has to be recorded. The definitional clauses + // go away on user-pop, so this literal will have to be re-vivified if it's + // used subsequently. + recordTranslation(xorNode, true); + return xorLit; } @@ -285,6 +309,11 @@ SatLiteral TseitinCnfStream::handleOr(TNode orNode) { // This needs to go last, as the clause might get modified by the SAT solver assertClause(orNode, clause); + // We have a literal, so it has to be recorded. The definitional clauses + // go away on user-pop, so this literal will have to be re-vivified if it's + // used subsequently. + recordTranslation(orNode, true); + // Return the literal return orLit; } @@ -321,6 +350,12 @@ SatLiteral TseitinCnfStream::handleAnd(TNode andNode) { clause[n_children] = andLit; // This needs to go last, as the clause might get modified by the SAT solver assertClause(andNode, clause); + + // We have a literal, so it has to be recorded. The definitional clauses + // go away on user-pop, so this literal will have to be re-vivified if it's + // used subsequently. + recordTranslation(andNode, true); + return andLit; } @@ -345,6 +380,11 @@ SatLiteral TseitinCnfStream::handleImplies(TNode impliesNode) { assertClause(impliesNode, a, impliesLit); assertClause(impliesNode, ~b, impliesLit); + // We have a literal, so it has to be recorded. The definitional clauses + // go away on user-pop, so this literal will have to be re-vivified if it's + // used subsequently. + recordTranslation(impliesNode, true); + return impliesLit; } @@ -377,6 +417,11 @@ SatLiteral TseitinCnfStream::handleIff(TNode iffNode) { assertClause(iffNode, ~a, ~b, iffLit); assertClause(iffNode, a, b, iffLit); + // We have a literal, so it has to be recorded. The definitional clauses + // go away on user-pop, so this literal will have to be re-vivified if it's + // used subsequently. + recordTranslation(iffNode, true); + return iffLit; } @@ -423,6 +468,11 @@ SatLiteral TseitinCnfStream::handleIte(TNode iteNode) { assertClause(iteNode, iteLit, ~condLit, ~thenLit); assertClause(iteNode, iteLit, condLit, ~elseLit); + // We have a literal, so it has to be recorded. The definitional clauses + // go away on user-pop, so this literal will have to be re-vivified if it's + // used subsequently. + recordTranslation(iteNode, true); + return iteLit; } @@ -435,6 +485,7 @@ SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) { // If the non-negated node has already been translated, get the translation if(isTranslated(node)) { + Debug("cnf") << "toCNF(): already translated" << endl; nodeLit = getLiteral(node); } else { // Handle each Boolean operator case @@ -690,15 +741,19 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool negated) { void CnfStream::removeClausesAboveLevel(int level) { while (d_translationTrail.size() > 0) { + Debug("cnf") << "Considering translation trail position " << d_translationTrail.size() << std::endl; TNode node = d_translationTrail.back(); + // Get the translation information + TranslationInfo& infoPos = d_translationCache.find(node)->second; + // If the level of the node is less or equal to given we are done + if (infoPos.level >= 0 && infoPos.level <= level) { + Debug("cnf") << "Node is " << node << " level " << infoPos.level << ", we're done." << std::endl; + break; + } 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); } @@ -734,6 +789,7 @@ void CnfStream::undoTranslate(TNode node, int level) { // Untranslate infoPos.level = -1; + infoPos.recorded = false; // Untranslate the negation node // If not a not node, unregister it from sat and untranslate the negation @@ -747,6 +803,7 @@ void CnfStream::undoTranslate(TNode node, int level) { Assert(it != d_translationCache.end()); TranslationInfo& infoNeg = (*it).second; infoNeg.level = -1; + infoNeg.recorded = false; } // undoTranslate the children |