diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-11-26 17:40:31 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-11-26 17:40:31 +0000 |
commit | 78f459b303ed292a297a36cd0c435fdd025b0865 (patch) | |
tree | 80be491bc4525d70d599fbd72869dd592f70d56a /src/prop/cnf_stream.cpp | |
parent | c3ca3d8c58cc9954f8ad190e1e2dedbcbb5372f0 (diff) |
fixup for incremental solving
Diffstat (limited to 'src/prop/cnf_stream.cpp')
-rw-r--r-- | src/prop/cnf_stream.cpp | 266 |
1 files changed, 43 insertions, 223 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 69418af0f..9f2138e9d 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -45,24 +45,11 @@ namespace prop { CnfStream::CnfStream(SatSolver *satSolver, Registrar* registrar, context::Context* context, bool fullLitToNodeMap) : d_satSolver(satSolver), d_booleanVariables(context), + d_nodeToLiteralMap(context), + d_literalToNodeMap(context), d_fullLitToNodeMap(fullLitToNodeMap), - d_registrar(registrar) { -} - -void CnfStream::recordTranslation(TNode node, bool alwaysRecord) { - Debug("cnf") << "recordTranslation(" << alwaysRecord << "," << d_removable << "): " << node << std::endl; - if (!d_removable) { - 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; - } - } + d_registrar(registrar), + d_removable(false) { } TseitinCnfStream::TseitinCnfStream(SatSolver* satSolver, Registrar* registrar, context::Context* context, bool fullLitToNodeMap) : @@ -108,27 +95,24 @@ void CnfStream::assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral assertClause(node, clause); } -bool CnfStream::isTranslated(TNode n) const { - TranslationCache::const_iterator find = d_translationCache.find(n); - return find != d_translationCache.end() && (*find).second.level >= 0; -} - bool CnfStream::hasLiteral(TNode n) const { - TranslationCache::const_iterator find = d_translationCache.find(n); - return find != d_translationCache.end(); + NodeToLiteralMap::const_iterator find = d_nodeToLiteralMap.find(n); + return find != d_nodeToLiteralMap.end(); } void TseitinCnfStream::ensureLiteral(TNode n) { + + // These are not removable + d_removable = false; + Debug("cnf") << "ensureLiteral(" << n << ")" << endl; if(hasLiteral(n)) { - // Already a literal! - // 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()) { + SatLiteral lit = getLiteral(n); + LiteralToNodeMap::iterator i = d_literalToNodeMap.find(lit); + if(i == d_literalToNodeMap.end()) { // Store backward-mappings - d_nodeCache[lit] = n; - d_nodeCache[~lit] = n.notNode(); + d_literalToNodeMap[lit] = n; + d_literalToNodeMap[~lit] = n.notNode(); } return; } @@ -156,8 +140,8 @@ void TseitinCnfStream::ensureLiteral(TNode n) { lit = toCNF(n, false); // Store backward-mappings - d_nodeCache[lit] = n; - d_nodeCache[~lit] = n.notNode(); + d_literalToNodeMap[lit] = n; + d_literalToNodeMap[~lit] = n.notNode(); } else { // We have a theory atom or variable. lit = convertAtom(n); @@ -184,27 +168,18 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) { } else { lit = SatLiteral(d_satSolver->newVar(theoryLiteral)); } - d_translationCache[node].literal = lit; - d_translationCache[node.notNode()].literal = ~lit; + d_nodeToLiteralMap[node] = lit; + d_nodeToLiteralMap[node.notNode()] = ~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->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::replayLog() != NULL ) || (Dump.isOn("clauses")) ) { - d_nodeCache[lit] = node; - d_nodeCache[~lit] = node.notNode(); + d_literalToNodeMap[lit] = node; + d_literalToNodeMap[~lit] = node.notNode(); } // If a theory literal, we pre-register it @@ -222,11 +197,11 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) { 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; + LiteralToNodeMap::iterator find = d_literalToNodeMap.find(literal); + Assert(find != d_literalToNodeMap.end()); + Assert(d_nodeToLiteralMap.find((*find).second) != d_nodeToLiteralMap.end()); + Debug("cnf") << "getNode(" << literal << ") => " << (*find).second << endl; + return (*find).second; } void CnfStream::getBooleanVariables(std::vector<TNode>& outputVariables) const { @@ -239,7 +214,7 @@ void CnfStream::getBooleanVariables(std::vector<TNode>& outputVariables) const { SatLiteral CnfStream::convertAtom(TNode node) { Debug("cnf") << "convertAtom(" << node << ")" << endl; - Assert(!isTranslated(node), "atom already mapped!"); + Assert(!hasLiteral(node), "atom already mapped!"); // Is this a variable add it to the list if (node.isVar()) { @@ -249,27 +224,24 @@ SatLiteral CnfStream::convertAtom(TNode node) { // Make a new literal (variables are not considered theory literals) SatLiteral lit = newLiteral(node, !node.isVar()); - // 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 the resulting literal return lit; } SatLiteral CnfStream::getLiteral(TNode node) { - TranslationCache::iterator find = d_translationCache.find(node); + NodeToLiteralMap::iterator find = d_nodeToLiteralMap.find(node); Assert(!node.isNull(), "CnfStream: can't getLiteral() of null node"); - Assert(find != d_translationCache.end(), "Literal not in the CNF Cache: %s\n", node.toString().c_str()); - SatLiteral literal = find->second.literal; + Assert(find != d_nodeToLiteralMap.end(), "Literal not in the CNF Cache: %s\n", node.toString().c_str()); + SatLiteral literal = (*find).second; Debug("cnf") << "CnfStream::getLiteral(" << node << ") => " << literal << std::endl; return literal; } SatLiteral TseitinCnfStream::handleXor(TNode xorNode) { - Assert(!isTranslated(xorNode), "Atom already mapped!"); + Assert(!hasLiteral(xorNode), "Atom already mapped!"); Assert(xorNode.getKind() == XOR, "Expecting an XOR expression!"); Assert(xorNode.getNumChildren() == 2, "Expecting exactly 2 children!"); + Assert(!d_removable, "Removable clauses can not contain Boolean structure"); SatLiteral a = toCNF(xorNode[0]); SatLiteral b = toCNF(xorNode[1]); @@ -281,18 +253,14 @@ 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; } SatLiteral TseitinCnfStream::handleOr(TNode orNode) { - Assert(!isTranslated(orNode), "Atom already mapped!"); + Assert(!hasLiteral(orNode), "Atom already mapped!"); Assert(orNode.getKind() == OR, "Expecting an OR expression!"); Assert(orNode.getNumChildren() > 1, "Expecting more then 1 child!"); + Assert(!d_removable, "Removable clauses can not contain Boolean structure"); // Number of children unsigned n_children = orNode.getNumChildren(); @@ -321,19 +289,15 @@ 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; } SatLiteral TseitinCnfStream::handleAnd(TNode andNode) { - Assert(!isTranslated(andNode), "Atom already mapped!"); + Assert(!hasLiteral(andNode), "Atom already mapped!"); Assert(andNode.getKind() == AND, "Expecting an AND expression!"); Assert(andNode.getNumChildren() > 1, "Expecting more than 1 child!"); + Assert(!d_removable, "Removable clauses can not contain Boolean structure"); // Number of children unsigned n_children = andNode.getNumChildren(); @@ -363,18 +327,14 @@ SatLiteral TseitinCnfStream::handleAnd(TNode andNode) { // 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; } SatLiteral TseitinCnfStream::handleImplies(TNode impliesNode) { - Assert(!isTranslated(impliesNode), "Atom already mapped!"); + Assert(!hasLiteral(impliesNode), "Atom already mapped!"); Assert(impliesNode.getKind() == IMPLIES, "Expecting an IMPLIES expression!"); Assert(impliesNode.getNumChildren() == 2, "Expecting exactly 2 children!"); + Assert(!d_removable, "Removable clauses can not contain Boolean structure"); // Convert the children to cnf SatLiteral a = toCNF(impliesNode[0]); @@ -392,17 +352,12 @@ 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; } SatLiteral TseitinCnfStream::handleIff(TNode iffNode) { - Assert(!isTranslated(iffNode), "Atom already mapped!"); + Assert(!hasLiteral(iffNode), "Atom already mapped!"); Assert(iffNode.getKind() == IFF, "Expecting an IFF expression!"); Assert(iffNode.getNumChildren() == 2, "Expecting exactly 2 children!"); @@ -429,17 +384,12 @@ 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; } SatLiteral TseitinCnfStream::handleNot(TNode notNode) { - Assert(!isTranslated(notNode), "Atom already mapped!"); + Assert(!hasLiteral(notNode), "Atom already mapped!"); Assert(notNode.getKind() == NOT, "Expecting a NOT expression!"); Assert(notNode.getNumChildren() == 1, "Expecting exactly 1 child!"); @@ -451,6 +401,7 @@ SatLiteral TseitinCnfStream::handleNot(TNode notNode) { SatLiteral TseitinCnfStream::handleIte(TNode iteNode) { Assert(iteNode.getKind() == ITE); Assert(iteNode.getNumChildren() == 3); + Assert(!d_removable, "Removable clauses can not contain Boolean structure"); Debug("cnf") << "handleIte(" << iteNode[0] << " " << iteNode[1] << " " << iteNode[2] << ")" << endl; @@ -480,11 +431,6 @@ 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; } @@ -496,7 +442,7 @@ SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) { Node negatedNode = node.notNode(); // If the non-negated node has already been translated, get the translation - if(isTranslated(node)) { + if(hasLiteral(node)) { Debug("cnf") << "toCNF(): already translated" << endl; nodeLit = getLiteral(node); } else { @@ -564,7 +510,6 @@ void TseitinCnfStream::convertAndAssertAnd(TNode node, 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); @@ -581,7 +526,6 @@ void TseitinCnfStream::convertAndAssertOr(TNode node, 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); @@ -622,8 +566,6 @@ void TseitinCnfStream::convertAndAssertXor(TNode node, bool negated) { clause2[1] = ~q; assertClause(node, clause2); } - recordTranslation(node[0]); - recordTranslation(node[1]); } void TseitinCnfStream::convertAndAssertIff(TNode node, bool negated) { @@ -654,8 +596,6 @@ void TseitinCnfStream::convertAndAssertIff(TNode node, bool negated) { clause2[1] = q; assertClause(node, clause2); } - recordTranslation(node[0]); - recordTranslation(node[1]); } void TseitinCnfStream::convertAndAssertImplies(TNode node, bool negated) { @@ -668,8 +608,6 @@ void TseitinCnfStream::convertAndAssertImplies(TNode node, bool negated) { 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], false); @@ -692,10 +630,6 @@ void TseitinCnfStream::convertAndAssertIte(TNode node, bool negated) { clause2[0] = p; clause2[1] = r; assertClause(node, clause2); - - recordTranslation(node[0]); - recordTranslation(node[1]); - recordTranslation(node[2]); } // At the top level we must ensure that all clauses that are asserted are @@ -710,17 +644,6 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool removable, bool negated void TseitinCnfStream::convertAndAssert(TNode node, bool negated) { Debug("cnf") << "convertAndAssert(" << node << ", negated = " << (negated ? "true" : "false") << ")" << endl; - /* - if(isTranslated(node)) { - Debug("cnf") << "==> fortunate literal detected!" << endl; - ++d_fortunateLiterals; - SatLiteral lit = getLiteral(node); - //d_satSolver->renewVar(lit); - assertClause(node, negated ? ~lit : lit); - return; - } - */ - switch(node.getKind()) { case AND: convertAndAssertAnd(node, negated); @@ -746,112 +669,9 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool negated) { default: // Atoms assertClause(node, toCNF(node, negated)); - recordTranslation(node); break; } } -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(); - // If already untranslated, we're done - if (infoPos.level == -1) continue; - // Otherwise we have to undo the translation - undoTranslate(node, level); - } -} - -void CnfStream::undoTranslate(TNode node, int level) { - Debug("cnf") << "undoTranslate(): " << node << " (level " << level << ")" << endl; - - TranslationCache::iterator it = d_translationCache.find(node); - - // If not in translation cache, done (the parent was an atom) - if (it == d_translationCache.end()) { - Debug("cnf") << " ==> not in cache, ignore" << endl; - return; - } - - // Get the translation information - TranslationInfo& infoPos = (*it).second; - - // If already untranslated, we are done - if (infoPos.level == -1) { - Debug("cnf") << " ==> already untranslated, ignore" << endl; - return; - } - - // If under the given level we're also done - if (infoPos.level <= level) { - Debug("cnf") << " ==> level too low, ignore" << endl; - return; - } - - Debug("cnf") << " ==> untranslating" << endl; - - // Untranslate - infoPos.level = -1; - infoPos.recorded = false; - - // 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); - Debug("cnf") << " ==> untranslating negation, too" << endl; - // Untranslate the negation - it = d_translationCache.find(node.notNode()); - Assert(it != d_translationCache.end()); - TranslationInfo& infoNeg = (*it).second; - infoNeg.level = -1; - infoNeg.recorded = false; - } - - // undoTranslate the children - TNode::iterator child = node.begin(); - TNode::iterator child_end = node.end(); - while (child != child_end) { - undoTranslate(*child, level); - ++ child; - } - - Debug("cnf") << "undoTranslate(): finished untranslating " << node << " (level " << level << ")" << endl; -} - -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 */ |