From 78f459b303ed292a297a36cd0c435fdd025b0865 Mon Sep 17 00:00:00 2001 From: Dejan Jovanović Date: Mon, 26 Nov 2012 17:40:31 +0000 Subject: fixup for incremental solving --- src/prop/cnf_stream.cpp | 266 ++++++-------------------------- src/prop/cnf_stream.h | 61 ++------ src/prop/minisat/core/Solver.cc | 292 +++++++++++++++++++----------------- src/prop/minisat/core/Solver.h | 49 ++++-- src/prop/minisat/core/SolverTypes.h | 1 + src/prop/minisat/minisat.cpp | 8 - src/prop/minisat/minisat.h | 4 - src/prop/minisat/simp/SimpSolver.cc | 9 +- src/prop/prop_engine.cpp | 14 +- src/prop/prop_engine.h | 7 - src/prop/sat_solver.h | 5 +- src/prop/theory_proxy.cpp | 4 - src/prop/theory_proxy.h | 6 - src/theory/bv/bitblaster.cpp | 2 +- src/theory/logic_info.cpp | 7 +- src/theory/logic_info.h | 3 +- src/theory/theory_engine.cpp | 4 +- 17 files changed, 268 insertions(+), 474 deletions(-) (limited to 'src') 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& outputVariables) const { @@ -239,7 +214,7 @@ void CnfStream::getBooleanVariables(std::vector& 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 */ diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index c085fd384..6ab639712 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -47,19 +47,10 @@ class CnfStream { public: /** Cache of what nodes have been registered to a literal. */ - typedef __gnu_cxx::hash_map NodeCache; - - /** Per node translation information */ - struct TranslationInfo { - bool recorded; - /** The level at which this node was translated (negative if not translated) */ - int level; - /** The literal of this node */ - SatLiteral literal; - }; + typedef context::CDHashMap LiteralToNodeMap; /** Cache of what literals have been registered to a node. */ - typedef __gnu_cxx::hash_map TranslationCache; + typedef context::CDHashMap NodeToLiteralMap; protected: @@ -69,8 +60,11 @@ protected: /** Boolean variables that we translated */ context::CDList d_booleanVariables; - TranslationCache d_translationCache; - NodeCache d_nodeCache; + /** Map from nodes to literals */ + NodeToLiteralMap d_nodeToLiteralMap; + + /** Map from literals to nodes */ + LiteralToNodeMap d_literalToNodeMap; /** * True if the lit-to-Node map should be kept for all lits, not just @@ -82,9 +76,6 @@ protected: /** The "registrar" for pre-registration of terms */ Registrar* d_registrar; - /** Top level nodes that we translated */ - std::vector d_translationTrail; - /** * How many literals were already mapped at the top-level when we * tried to convertAndAssert() something. This @@ -111,23 +102,11 @@ protected: return node; } - /** Record this translation */ - void recordTranslation(TNode node, bool alwaysRecord = false); - - /** - * Moves the node and all of it's parents to level 0. - */ - void moveToBaseLevel(TNode node); - - /** - * Mark the node, and all parent at levels above level as untranslated. - */ - void undoTranslate(TNode node, int level); - /** * Are we asserting a removable clause (true) or a permanent clause (false). - * This is set at the begining of convertAndAssert so that it doesn't - * need to be passed on over the stack. + * This is set at the beginning of convertAndAssert so that it doesn't + * need to be passed on over the stack. Only pure clauses can be asserted as + * removable. */ bool d_removable; @@ -218,13 +197,6 @@ public: */ TNode getNode(const SatLiteral& literal); - /** - * Returns true if the node has been cached in the translation cache. - * @param node the node - * @return true if the node has been cached - */ - bool isTranslated(TNode node) const; - /** * Returns true iff the node has an assigned literal (it might not be translated). * @param node the node @@ -253,19 +225,14 @@ public: */ void getBooleanVariables(std::vector& outputVariables) const; - const TranslationCache& getTranslationCache() const { - return d_translationCache; + const NodeToLiteralMap& getTranslationCache() const { + return d_nodeToLiteralMap; } - const NodeCache& getNodeCache() const { - return d_nodeCache; + const LiteralToNodeMap& getNodeCache() const { + return d_literalToNodeMap; } - /** - * Removes all the translation information of clauses that have the given associated assert level. - */ - void removeClausesAboveLevel(int level); - };/* class CnfStream */ diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index ba36ac879..f7d67d445 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -157,7 +157,7 @@ Var Solver::newVar(bool sign, bool dvar, bool theoryAtom) watches .init(mkLit(v, false)); watches .init(mkLit(v, true )); assigns .push(l_Undef); - vardata .push(mkVarData(CRef_Undef, 0, assertionLevel, -1)); + vardata .push(VarData(CRef_Undef, -1, -1, assertionLevel, -1)); activity .push(rnd_init_act ? drand(random_seed) * 0.00001 : 0); seen .push(0); polarity .push(sign); @@ -177,6 +177,33 @@ Var Solver::newVar(bool sign, bool dvar, bool theoryAtom) return v; } +void Solver::resizeVars(int newSize) { + assert(enable_incremental); + assert(decisionLevel() == 0); + Assert(newSize >= 2, "always keep true/false"); + if (newSize < nVars()) { + int shrinkSize = nVars() - newSize; + + // Resize watches up to the negated last literal + watches.resizeTo(mkLit(newSize-1, true)); + + // Resize all info arrays + assigns.shrink(shrinkSize); + vardata.shrink(shrinkSize); + activity.shrink(shrinkSize); + seen.shrink(shrinkSize); + polarity.shrink(shrinkSize); + decision.shrink(shrinkSize); + theory.shrink(shrinkSize); + + } + + if (Debug.isOn("minisat::pop")) { + for (int i = 0; i < trail.size(); ++ i) { + assert(var(trail[i]) < nVars()); + } + } +} CRef Solver::reason(Var x) { @@ -202,18 +229,31 @@ CRef Solver::reason(Var x) { int i, j; Lit prev = lit_Undef; for (i = 0, j = 0; i < explanation.size(); ++ i) { - int varLevel = intro_level(var(explanation[i])); - if (varLevel > explLevel) { - explLevel = varLevel; - } + // This clause is valid theory propagation, so it's level is the level of the top literal + explLevel = std::max(explLevel, intro_level(var(explanation[i]))); + Assert(value(explanation[i]) != l_Undef); Assert(i == 0 || trail_index(var(explanation[0])) > trail_index(var(explanation[i]))); - // ignore zero level literals - if (i == 0 || (level(var(explanation[i])) > 0 && explanation[i] != prev)) { + + // Always keep the first literal + if (i == 0) { prev = explanation[j++] = explanation[i]; + continue; + } + // Ignore duplicate literals + if (explanation[i] == prev) { + continue; + } + // Ignore zero level literals + if (level(var(explanation[i])) == 0 && user_level(var(explanation[i]) == 0)) { + continue; } + // Keep this literal + prev = explanation[j++] = explanation[i]; } explanation.shrink(i - j); + + // We need an explanation clause so we add a fake literal if (j == 1) { // Add not TRUE to the clause explanation.push(mkLit(varTrue, true)); @@ -221,9 +261,10 @@ CRef Solver::reason(Var x) { // Construct the reason CRef real_reason = ca.alloc(explLevel, explanation, true); - vardata[x] = mkVarData(real_reason, level(x), intro_level(x), trail_index(x)); + vardata[x] = VarData(real_reason, level(x), user_level(x), intro_level(x), trail_index(x)); clauses_removable.push(real_reason); attachClause(real_reason); + return real_reason; } @@ -235,16 +276,38 @@ bool Solver::addClause_(vec& ps, bool removable) sort(ps); Lit p; int i, j; + // Which user-level to assert this clause at + int clauseLevel = removable ? 0 : assertionLevel; + // Check the clause for tautologies and similar + int falseLiteralsCount = 0; for (i = j = 0, p = lit_Undef; i < ps.size(); i++) { - if ((ps[i] == ~p) || (value(ps[i]) == l_True && level(var(ps[i])) == 0)) { + // Update the level + clauseLevel = std::max(clauseLevel, intro_level(var(ps[i]))); + // Tautologies are ignored + if (ps[i] == ~p) { // Clause can be ignored return true; } - if ((ps[i] != p) && (value(ps[i]) != l_False || level(var(ps[i])) > 0)) { - // This literal is a keeper - ps[j++] = p = ps[i]; + // Clauses with 0-level true literals are also ignored + if (value(ps[i]) == l_True && level(var(ps[i])) == 0 && user_level(var(ps[i])) == 0) { + return true; } + // Ignore repeated literals + if (ps[i] == p) { + continue; + } + // If a literals is false at 0 level (both sat and user level) we also ignore it + if (value(ps[i]) == l_False) { + if (level(var(ps[i])) == 0 && user_level(var(ps[i])) == 0) { + continue; + } else { + // If we decide to keep it, we count it into the false literals + falseLiteralsCount ++; + } + } + // This literal is a keeper + ps[j++] = p = ps[i]; } // Fit to size @@ -256,24 +319,35 @@ bool Solver::addClause_(vec& ps, bool removable) ps.copyTo(lemmas.last()); lemmas_removable.push(removable); } else { - // Add the clause and attach if not a lemma - if (ps.size() == 0) { + // If all false, we're in conflict + if (ps.size() == falseLiteralsCount) { return ok = false; - } else if (ps.size() == 1) { - if(assigns[var(ps[0])] == l_Undef) { - uncheckedEnqueue(ps[0]); - - PROOF( ProofManager::getSatProof()->registerUnitClause(ps[0], true); ) + } - return ok = (propagate(CHECK_WITHOUTH_THEORY) == CRef_Undef); - } else return ok; - } else { - CRef cr = ca.alloc(assertionLevel, ps, false); + CRef cr = CRef_Undef; + + // If not unit, add the clause + if (ps.size() > 1) { + + lemma_lt lt(*this); + sort(ps, lt); + + cr = ca.alloc(clauseLevel, ps, false); clauses_persistent.push(cr); attachClause(cr); - + PROOF( ProofManager::getSatProof()->registerClause(cr, true); ) } + + // Check if it propagates + if (ps.size() == falseLiteralsCount + 1) { + if(assigns[var(ps[0])] == l_Undef) { + assert(assigns[var(ps[0])] != l_False); + uncheckedEnqueue(ps[0], cr); + PROOF( if (ps.size() == 1) { ProofManager::getSatProof()->registerUnitClause(ps[0], true); } ) + return ok = (propagate(CHECK_WITHOUTH_THEORY) == CRef_Undef); + } else return ok; + } } return true; @@ -313,7 +387,7 @@ void Solver::detachClause(CRef cr, bool strict) { void Solver::removeClause(CRef cr) { Clause& c = ca[cr]; - Debug("minisat") << "Solver::removeClause(" << c << ")" << std::endl; + Debug("minisat::remove-clause") << "Solver::removeClause(" << c << ")" << std::endl; detachClause(cr); // Don't leave pointers to free'd memory! if (locked(c)) vardata[var(c[0])].reason = CRef_Undef; @@ -348,9 +422,7 @@ void Solver::cancelUntil(int level) { vardata[x].trail_index = -1; if ((phase_saving > 1 || (phase_saving == 1) && c > trail_lim.last()) && (polarity[x] & 0x2) == 0) polarity[x] = sign(trail[c]); - if(intro_level(x) != -1) {// might be unregistered - insertVarOrder(x); - } + insertVarOrder(x); } qhead = trail_lim[level]; trail.shrink(trail.size() - trail_lim[level]); @@ -413,7 +485,7 @@ Lit Solver::pickBranchLit() rnd_decisions++; } // Activity based decision: - while (next == var_Undef || value(next) != l_Undef || !decision[next]) { + while (next >= nVars() || next == var_Undef || value(next) != l_Undef || !decision[next]) { if (order_heap.empty()){ next = var_Undef; break; @@ -473,15 +545,13 @@ int Solver::analyze(CRef confl, vec& out_learnt, int& out_btlevel) out_learnt.push(); // (leave room for the asserting literal) int index = trail.size() - 1; - int max_level = 0; // Maximal level of the resolved clauses + int max_resolution_level = 0; // Maximal level of the resolved clauses PROOF( ProofManager::getSatProof()->startResChain(confl); ) do{ assert(confl != CRef_Undef); // (otherwise should be UIP) Clause& c = ca[confl]; - if (c.level() > max_level) { - max_level = c.level(); - } + max_resolution_level = std::max(max_resolution_level, c.level()); if (c.removable()) claBumpActivity(c); @@ -497,6 +567,12 @@ int Solver::analyze(CRef confl, vec& out_learnt, int& out_btlevel) else out_learnt.push(q); } else { + // We could be resolving a literal propagated by a clause/theory using + // information from a higher level + if (!seen[var(q)] && level(var(q)) == 0) { + max_resolution_level = std::max(max_resolution_level, user_level(var(q))); + } + // FIXME: can we do it lazily if we actually need the proof? if (level(var(q)) == 0) { PROOF( ProofManager::getSatProof()->resolveOutUnit(q); ) @@ -531,22 +607,20 @@ int Solver::analyze(CRef confl, vec& out_learnt, int& out_btlevel) out_learnt[j++] = out_learnt[i]; } else { // Check if the literal is redundant - int red_level = litRedundant(out_learnt[i], abstract_level); - if (red_level < 0) { + if (!litRedundant(out_learnt[i], abstract_level)) { // Literal is not redundant out_learnt[j++] = out_learnt[i]; } else { - // PROOF( ProofManager::getSatProof()->storeLitRedundant(out_learnt[i]); ) - // Literal is redundant, mark the level of the redundancy derivation - if (max_level < red_level) { - max_level = red_level; - } + // Literal is redundant, to be safe, mark the level as current assertion level + // TODO: maybe optimize + max_resolution_level = std::max(max_resolution_level, user_level(var(out_learnt[i]))); } } } }else if (ccmin_mode == 1){ + Unreachable(); for (i = j = 1; i < out_learnt.size(); i++){ Var x = var(out_learnt[i]); @@ -587,26 +661,22 @@ int Solver::analyze(CRef confl, vec& out_learnt, int& out_btlevel) for (int j = 0; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0; // ('seen[]' is now cleared) // Return the maximal resolution level - return max_level; + return max_resolution_level; } // Check if 'p' can be removed. 'abstract_levels' is used to abort early if the algorithm is // visiting literals at levels that cannot be removed later. -int Solver::litRedundant(Lit p, uint32_t abstract_levels) +bool Solver::litRedundant(Lit p, uint32_t abstract_levels) { analyze_stack.clear(); analyze_stack.push(p); int top = analyze_toclear.size(); - int max_level = 0; while (analyze_stack.size() > 0){ CRef c_reason = reason(var(analyze_stack.last())); assert(c_reason != CRef_Undef); Clause& c = ca[c_reason]; int c_size = c.size(); analyze_stack.pop(); - if (c.level() > max_level) { - max_level = c.level(); - } // Since calling reason might relocate to resize, c is not necesserily the right reference, we must // use the allocator each time @@ -621,13 +691,13 @@ int Solver::litRedundant(Lit p, uint32_t abstract_levels) for (int j = top; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0; analyze_toclear.shrink(analyze_toclear.size() - top); - return -1; + return false; } } } } - return max_level; + return true; } @@ -674,18 +744,14 @@ void Solver::uncheckedEnqueue(Lit p, CRef from) { Debug("minisat") << "unchecked enqueue of " << p << " (" << trail_index(var(p)) << ") trail size is " << trail.size() << " cap is " << trail.capacity() << std::endl; assert(value(p) == l_Undef); + assert(var(p) < nVars()); assigns[var(p)] = lbool(!sign(p)); - vardata[var(p)] = mkVarData(from, decisionLevel(), intro_level(var(p)), trail.size()); + vardata[var(p)] = VarData(from, decisionLevel(), assertionLevel, intro_level(var(p)), trail.size()); trail.push_(p); if (theory[var(p)]) { // Enqueue to the theory proxy->enqueueTheoryLiteral(MinisatSatSolver::toSatLiteral(p)); } - if (from == CRef_Undef) { - if (assertionLevel > 0) { - trail_user.push(p); - } - } } @@ -943,26 +1009,12 @@ void Solver::removeClausesAboveLevel(vec& cs, int level) for (i = j = 0; i < cs.size(); i++){ Clause& c = ca[cs[i]]; if (c.level() > level) { - if(Debug.isOn("minisat")) { - Debug("minisat") << "removeClausesAboveLevel(" << level << "): removing level-" << c.level() << " clause: " << c << ":"; - for(int i = 0; i < c.size(); ++i) { - Debug("minisat") << " " << c[i]; - } - Debug("minisat") << std::endl; - } - removeClause(cs[i]); + assert(!locked(c)); + removeClause(cs[i]); } else { - if(Debug.isOn("minisat")) { - Debug("minisat") << "removeClausesAboveLevel(" << level << "): leaving level-" << c.level() << " clause: " << c << ":"; - for(int i = 0; i < c.size(); ++i) { - Debug("minisat") << " " << c[i]; - } - Debug("minisat") << std::endl; - } cs[j++] = cs[i]; } } - Debug("minisat") << "removeClausesAboveLevel(" << level << "): removed " << i - j << " clauses in all, left " << j << std::endl; cs.shrink(i - j); } @@ -1408,10 +1460,8 @@ void Solver::push() popTrail(); ++assertionLevel; Debug("minisat") << "in user push, increasing assertion level to " << assertionLevel << std::endl; - trail_user.push(lit_Undef); trail_ok.push(ok); - trail_user_lim.push(trail.size()); - assert(trail_user_lim.size() == assertionLevel); + assigns_lim.push(assigns.size()); context->push(); // SAT context for CVC4 @@ -1422,83 +1472,44 @@ void Solver::pop() { assert(enable_incremental); - Debug("minisat") << "MINISAT POP at level " << decisionLevel() << " (context " << context->getLevel() << "), popping trail..." << std::endl; + // Pop the trail to 0 level popTrail(); - Debug("minisat") << "MINISAT POP now at " << decisionLevel() << " (context " << context->getLevel() << ")" << std::endl; - assert(decisionLevel() == 0); - assert(trail_user_lim.size() == assertionLevel); + // Pop the trail below the user level --assertionLevel; - - Debug("minisat") << "MINISAT POP assertionLevel is now down to " << assertionLevel << ", trail.size is " << trail.size() << ", need to get down to " << trail_user_lim.last() << std::endl; - Debug("minisat") << "in user pop, reducing assertion level to " << assertionLevel << " and removing clauses above this from db" << std::endl; - - // Remove all the clauses asserted (and implied) above the new base level - removeClausesAboveLevel(clauses_removable, assertionLevel); - removeClausesAboveLevel(clauses_persistent, assertionLevel); - - Debug("minisat") << "in user pop, at " << trail_lim.size() << " : " << assertionLevel << std::endl; - - int downto = trail_user_lim.last(); - while(downto < trail.size()) { + while (true) { Debug("minisat") << "== unassigning " << trail.last() << std::endl; Var x = var(trail.last()); - assigns [x] = l_Undef; - vardata[x].trail_index = -1; - if(phase_saving >= 1 && (polarity[x] & 0x2) == 0) - polarity[x] = sign(trail.last()); - if(intro_level(x) != -1) {// might be unregistered + if (user_level(x) > assertionLevel) { + assigns [x] = l_Undef; + vardata[x] = VarData(CRef_Undef, -1, -1, intro_level(x), -1); + if(phase_saving >= 1 && (polarity[x] & 0x2) == 0) + polarity[x] = sign(trail.last()); insertVarOrder(x); + trail.pop(); + } else { + break; } - trail.pop(); } + // The head should be at the trail top qhead = trail.size(); - Debug("minisat") << "MINISAT POP assertionLevel is now down to " << assertionLevel << ", trail.size is " << trail.size() << ", should be at " << trail_user_lim.last() << std::endl; - assert(trail_user_lim.last() == qhead); - trail_user_lim.pop(); - - // Unset any units learned or added at this level - Debug("minisat") << "in user pop, unsetting level units for level " << assertionLevel << std::endl; - while(trail_user.last() != lit_Undef) { - Lit l = trail_user.last(); - Debug("minisat") << "== unassigning " << l << std::endl; - Var x = var(l); - assigns [x] = l_Undef; - vardata[x].trail_index = -1; - if (phase_saving >= 1 && (polarity[x] & 0x2) == 0) - polarity[x] = sign(l); - if(intro_level(x) != -1) {// might be unregistered - insertVarOrder(x); - } - trail_user.pop(); - } - trail_user.pop(); - ok = trail_ok.last(); - trail_ok.pop(); - Debug("minisat") << "in user pop, done unsetting level units" << std::endl; - Debug("minisat") << "about to removeClausesAboveLevel(" << assertionLevel << ") in CNF" << std::endl; + // Remove the clause + removeClausesAboveLevel(clauses_persistent, assertionLevel); + removeClausesAboveLevel(clauses_removable, assertionLevel); + // Pop the SAT context to notify everyone context->pop(); // SAT context for CVC4 - // Notify the cnf - proxy->removeClausesAboveLevel(assertionLevel); -} - -void Solver::unregisterVar(Lit lit) { - Debug("minisat") << "unregisterVar " << lit << std::endl; - Var v = var(lit); - vardata[v].intro_level = -1; - setDecisionVar(v, false); -} + // Pop the created variables + resizeVars(assigns_lim.last()); + assigns_lim.pop(); + variables_to_register.clear(); -void Solver::renewVar(Lit lit, int level) { - Debug("minisat") << "renewVar " << lit << " " << level << std::endl; - Var v = var(lit); - vardata[v].intro_level = (level == -1 ? getAssertionLevel() : level); - setDecisionVar(v, true); - // explicitly not resetting polarity phase-locking here + // Pop the OK + ok = trail_ok.last(); + trail_ok.pop(); } bool Solver::flipDecision() { @@ -1599,7 +1610,16 @@ CRef Solver::updateLemmas() { // Attach it if non-unit CRef lemma_ref = CRef_Undef; if (lemma.size() > 1) { - lemma_ref = ca.alloc(assertionLevel, lemma, removable); + // If the lemmas is removable, we can compute its level by the level + int clauseLevel = assertionLevel; + if (removable) { + clauseLevel = 0; + for (int i = 0; i < lemma.size(); ++ i) { + clauseLevel = std::max(clauseLevel, intro_level(var(lemma[i]))); + } + } + + lemma_ref = ca.alloc(clauseLevel, lemma, removable); if (removable) { clauses_removable.push(lemma_ref); } else { diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index fdc9a98b7..0dad68a08 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -105,6 +105,9 @@ protected: /** Variables to re-register with theory solvers on backtracks */ vec variables_to_register; + /** Keep only newSize variables */ + void resizeVars(int newSize); + public: // Constructor/Destructor: @@ -151,9 +154,6 @@ public: void push (); void pop (); - void unregisterVar(Lit lit); // Unregister the literal (set assertion level to -1) - void renewVar(Lit lit, int level = -1); // Register the literal (set assertion level to the given level, or current level if -1) - bool addClause (const vec& ps, bool removable); // Add a clause to the solver. bool addEmptyClause(bool removable); // Add the empty clause, making the solver contradictory. bool addClause (Lit p, bool removable); // Add a unit clause to the solver. @@ -258,8 +258,26 @@ protected: // Helper structures: // - struct VarData { CRef reason; int level; int intro_level; int trail_index; }; - static inline VarData mkVarData(CRef cr, int l, int intro_l, int trail_i){ VarData d = {cr, l, intro_l, trail_i}; return d; } + struct VarData { + // Reason for the literal being in the trail + CRef reason; + // Sat level when the literal was added to the trail + int level; + // User level when the literal was added to the trail + int user_level; + // Use level at which this literal was introduced + int intro_level; + // The index in the trail + int trail_index; + + VarData(CRef reason, int level, int user_level, int intro_level, int trail_index) + : reason(reason) + , level(level) + , user_level(user_level) + , intro_level(intro_level) + , trail_index(trail_index) + {} + }; struct Watcher { CRef cref; @@ -293,13 +311,12 @@ protected: OccLists, WatcherDeleted> watches; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true). vec assigns; // The current assignments. + vec assigns_lim; // The size by levels of the current assignment vec polarity; // The preferred polarity of each variable (bit 0) and whether it's locked (bit 1). vec decision; // Declares if a variable is eligible for selection in the decision heuristic. vec flipped; // Which trail_lim decisions have been flipped in this context. vec trail; // Assignment stack; stores all assigments made in the order they were made. vec trail_lim; // Separator indices for different decision levels in 'trail'. - vec trail_user; // Stack of assignments to UNdo on user pop. - vec trail_user_lim; // Separator indices for different user levels in 'trail'. vec trail_ok; // Stack of "whether we're in conflict" flags. vec vardata; // Stores reason and level for each variable. int qhead; // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat). @@ -361,7 +378,7 @@ protected: void popTrail (); // Backtrack the trail to the previous push position int analyze (CRef confl, vec& out_learnt, int& out_btlevel); // (bt = backtrack) void analyzeFinal (Lit p, vec& out_conflict); // COULD THIS BE IMPLEMENTED BY THE ORDINARIY "analyze" BY SOME REASONABLE GENERALIZATION? - int litRedundant (Lit p, uint32_t abstract_levels); // (helper method for 'analyze()') - returns the maximal level of the clauses proving redundancy of p + bool litRedundant (Lit p, uint32_t abstract_levels); // (helper method for 'analyze()') - true if p is redundant lbool search (int nof_conflicts); // Search for a given number of conflicts. lbool solve_ (); // Main solve method (assumptions given in 'assumptions'). void reduceDB (); // Reduce the set of learnt clauses. @@ -396,7 +413,8 @@ protected: bool isPropagatedBy (Var x, const Clause& c) const; // Is the value of the variable propagated by the clause Clause C int level (Var x) const; - int intro_level (Var x) const; // Level at which this variable was introduced + int user_level (Var x) const; // User level at which this variable was asserted + int intro_level (Var x) const; // User level at which this variable was created int trail_index (Var x) const; // Index in the trail double progressEstimate () const; // DELETE THIS ?? IT'S NOT VERY USEFUL ... bool withinBudget () const; @@ -429,13 +447,16 @@ inline bool Solver::isPropagatedBy(Var x, const Clause& c) const { return vardat inline bool Solver::isDecision(Var x) const { Debug("minisat") << "var " << x << " is a decision iff " << (vardata[x].reason == CRef_Undef) << " && " << level(x) << " > 0" << std::endl; return vardata[x].reason == CRef_Undef && level(x) > 0; } -inline int Solver::level (Var x) const { return vardata[x].level; } +inline int Solver::level (Var x) const { assert(x < vardata.size()); return vardata[x].level; } + +inline int Solver::user_level(Var x) const { assert(x < vardata.size()); return vardata[x].user_level; } -inline int Solver::intro_level(Var x) const { return vardata[x].intro_level; } +inline int Solver::intro_level(Var x) const { assert(x < vardata.size()); return vardata[x].intro_level; } -inline int Solver::trail_index(Var x) const { return vardata[x].trail_index; } +inline int Solver::trail_index(Var x) const { assert(x < vardata.size()); return vardata[x].trail_index; } inline void Solver::insertVarOrder(Var x) { + assert(x < vardata.size()); if (!order_heap.inHeap(x) && decision[x]) order_heap.insert(x); } inline void Solver::varDecayActivity() { var_inc *= (1 / var_decay); } @@ -476,8 +497,8 @@ inline void Solver::newDecisionLevel() { trail_lim.push inline int Solver::decisionLevel () const { return trail_lim.size(); } inline uint32_t Solver::abstractLevel (Var x) const { return 1 << (level(x) & 31); } -inline lbool Solver::value (Var x) const { return assigns[x]; } -inline lbool Solver::value (Lit p) const { return assigns[var(p)] ^ sign(p); } +inline lbool Solver::value (Var x) const { assert(x < nVars()); return assigns[x]; } +inline lbool Solver::value (Lit p) const { assert(var(p) < nVars()); return assigns[var(p)] ^ sign(p); } inline lbool Solver::modelValue (Var x) const { return model[x]; } inline lbool Solver::modelValue (Lit p) const { return model[var(p)] ^ sign(p); } inline int Solver::nAssigns () const { return trail.size(); } diff --git a/src/prop/minisat/core/SolverTypes.h b/src/prop/minisat/core/SolverTypes.h index 9cd0d8848..fac4c92c1 100644 --- a/src/prop/minisat/core/SolverTypes.h +++ b/src/prop/minisat/core/SolverTypes.h @@ -340,6 +340,7 @@ class OccLists OccLists(const Deleted& d) : deleted(d) {} void init (const Idx& idx){ occs.growTo(toInt(idx)+1); dirty.growTo(toInt(idx)+1, 0); } + void resizeTo (const Idx& idx){ int shrinkSize = occs.size() - (toInt(idx) + 1); occs.shrink(shrinkSize); } // Vec& operator[](const Idx& idx){ return occs[toInt(idx)]; } Vec& operator[](const Idx& idx){ return occs[toInt(idx)]; } Vec& lookup (const Idx& idx){ if (dirty[toInt(idx)]) clean(idx); return occs[toInt(idx)]; } diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index e550d5ef2..886dc0f72 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -212,14 +212,6 @@ void MinisatSatSolver::pop(){ d_minisat->pop(); } -void MinisatSatSolver::unregisterVar(SatLiteral lit) { - d_minisat->unregisterVar(toMinisatLit(lit)); -} - -void MinisatSatSolver::renewVar(SatLiteral lit, int level) { - d_minisat->renewVar(toMinisatLit(lit), level); -} - /// Statistics for MinisatSatSolver MinisatSatSolver::Statistics::Statistics() : diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h index f87e4ae53..723f257f7 100644 --- a/src/prop/minisat/minisat.h +++ b/src/prop/minisat/minisat.h @@ -80,10 +80,6 @@ public: void pop(); - void unregisterVar(SatLiteral lit); - - void renewVar(SatLiteral lit, int level = -1); - void requirePhase(SatLiteral lit); bool flipDecision(); diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc index bf04cec8d..ed2dc04b9 100644 --- a/src/prop/minisat/simp/SimpSolver.cc +++ b/src/prop/minisat/simp/SimpSolver.cc @@ -98,10 +98,9 @@ SimpSolver::~SimpSolver() Var SimpSolver::newVar(bool sign, bool dvar, bool theoryAtom) { Var v = Solver::newVar(sign, dvar,theoryAtom); - frozen .push((char)theoryAtom); - eliminated.push((char)false); - if (use_simplification){ + frozen .push((char)theoryAtom); + eliminated.push((char)false); n_occ .push(0); n_occ .push(0); occurs .init(v); @@ -159,8 +158,10 @@ lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp) bool SimpSolver::addClause_(vec& ps, bool removable) { #ifndef NDEBUG - for (int i = 0; i < ps.size(); i++) + if (use_simplification) { + for (int i = 0; i < ps.size(); i++) assert(!isEliminated(var(ps[i]))); + } #endif int nclauses = clauses_persistent.size(); diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 6e51b55f3..1bd5dc8b7 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -130,22 +130,22 @@ bool PropEngine::flipDecision() { } bool PropEngine::isDecision(Node lit) const { - Assert(isTranslatedSatLiteral(lit)); + Assert(isSatLiteral(lit)); return d_satSolver->isDecision(d_cnfStream->getLiteral(lit).getSatVariable()); } void PropEngine::printSatisfyingAssignment(){ - const CnfStream::TranslationCache& transCache = + const CnfStream::NodeToLiteralMap& transCache = d_cnfStream->getTranslationCache(); Debug("prop-value") << "Literal | Value | Expr" << endl << "----------------------------------------" << "-----------------" << endl; - for(CnfStream::TranslationCache::const_iterator i = transCache.begin(), + for(CnfStream::NodeToLiteralMap::const_iterator i = transCache.begin(), end = transCache.end(); i != end; ++i) { - pair curr = *i; - SatLiteral l = curr.second.literal; + pair curr = *i; + SatLiteral l = curr.second; if(!l.isNegated()) { Node n = curr.first; SatValue value = d_satSolver->modelValue(l); @@ -220,10 +220,6 @@ bool PropEngine::isSatLiteral(TNode node) const { return d_cnfStream->hasLiteral(node); } -bool PropEngine::isTranslatedSatLiteral(TNode node) const { - return d_cnfStream->isTranslated(node); -} - bool PropEngine::hasValue(TNode node, bool& value) const { Assert(node.getType().isBoolean()); Assert(d_cnfStream->hasLiteral(node)); diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index f52118ac4..9540d3921 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -245,13 +245,6 @@ public: */ bool isSatLiteral(TNode node) const; - /** - * Return true if node has an associated SAT literal that is - * currently translated (i.e., it's relevant to the current - * user push/pop level). - */ - bool isTranslatedSatLiteral(TNode node) const; - /** * Check if the node has a value and return it if yes. */ diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index 4dadcbf38..e5d876b48 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -64,10 +64,7 @@ public: /** Call modelValue() when the search is done.*/ virtual SatValue modelValue(SatLiteral l) = 0; - virtual void unregisterVar(SatLiteral lit) = 0; - - virtual void renewVar(SatLiteral lit, int level = -1) = 0; - + /** Get the current assertion level */ virtual unsigned getAssertionLevel() const = 0; };/* class SatSolver */ diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 5d9ce2206..6246ef7e5 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -101,10 +101,6 @@ bool TheoryProxy::theoryNeedCheck() const { return d_theoryEngine->needCheck(); } -void TheoryProxy::removeClausesAboveLevel(int level) { - d_cnfStream->removeClausesAboveLevel(level); -} - TNode TheoryProxy::getNode(SatLiteral lit) { return d_cnfStream->getNode(lit); } diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index a227db5b4..74ee790d8 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -97,17 +97,11 @@ public: bool theoryNeedCheck() const; - void removeClausesAboveLevel(int level); - /** * Notifies of a new variable at a decision level. */ void variableNotify(SatVariable var); - void unregisterVar(SatLiteral lit); - - void renewVar(SatLiteral lit, int level = -1); - TNode getNode(SatLiteral lit); void notifyRestart(); diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp index aca81e176..91482526a 100644 --- a/src/theory/bv/bitblaster.cpp +++ b/src/theory/bv/bitblaster.cpp @@ -100,7 +100,7 @@ void Bitblaster::bbAtom(TNode node) { Node atom_definition = mkNode(kind::IFF, node, atom_bb); if (!options::bitvectorEagerBitblast()) { - d_cnfStream->convertAndAssert(atom_definition, true, false); + d_cnfStream->convertAndAssert(atom_definition, false, false); d_bitblastedAtoms.insert(node); } else { d_bvOutput->lemma(atom_definition, false); diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp index e76e2ace9..f90bee19d 100644 --- a/src/theory/logic_info.cpp +++ b/src/theory/logic_info.cpp @@ -31,7 +31,7 @@ namespace CVC4 { LogicInfo::LogicInfo() : d_logicString(""), - d_theories(), + d_theories(THEORY_LAST, false), d_sharingTheories(0), d_integers(true), d_reals(true), @@ -40,14 +40,13 @@ LogicInfo::LogicInfo() : d_locked(false) { for(TheoryId id = THEORY_FIRST; id < THEORY_LAST; ++id) { - d_theories[id] = false;// ensure it's cleared enableTheory(id); } } LogicInfo::LogicInfo(std::string logicString) throw(IllegalArgumentException) : d_logicString(""), - d_theories(), + d_theories(THEORY_LAST, false), d_sharingTheories(0), d_integers(false), d_reals(false), @@ -61,7 +60,7 @@ LogicInfo::LogicInfo(std::string logicString) throw(IllegalArgumentException) : LogicInfo::LogicInfo(const char* logicString) throw(IllegalArgumentException) : d_logicString(""), - d_theories(), + d_theories(THEORY_LAST, false), d_sharingTheories(0), d_integers(false), d_reals(false), diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h index e2d8f3da6..fd81ea629 100644 --- a/src/theory/logic_info.h +++ b/src/theory/logic_info.h @@ -22,6 +22,7 @@ #define __CVC4__LOGIC_INFO_H #include +#include #include "expr/kind.h" namespace CVC4 { @@ -43,7 +44,7 @@ namespace CVC4 { */ class CVC4_PUBLIC LogicInfo { mutable std::string d_logicString; /**< an SMT-LIB-like logic string */ - bool d_theories[theory::THEORY_LAST]; /**< set of active theories */ + std::vector d_theories; /**< set of active theories */ size_t d_sharingTheories; /**< count of theories that need sharing */ // for arithmetic diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index cd3b34879..60d79e90e 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -341,7 +341,7 @@ void TheoryEngine::check(Theory::Effort effort) { Debug("theory") << "TheoryEngine::check(" << effort << "): done, we are " << (d_inConflict ? "unsat" : "sat") << (d_lemmasAdded ? " with new lemmas" : " with no new lemmas") << std::endl; } catch(const theory::Interrupted&) { - Trace("theory") << "TheoryEngine::check() => conflict" << endl; + Trace("theory") << "TheoryEngine::check() => interrupted" << endl; } // If fulleffort, check all theories @@ -519,7 +519,7 @@ bool TheoryEngine::properConflict(TNode conflict) const { } bool TheoryEngine::properPropagation(TNode lit) const { - if(!getPropEngine()->isTranslatedSatLiteral(lit)) { + if(!getPropEngine()->isSatLiteral(lit)) { return false; } bool b; -- cgit v1.2.3