summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/prop/cnf_stream.cpp266
-rw-r--r--src/prop/cnf_stream.h61
-rw-r--r--src/prop/minisat/core/Solver.cc292
-rw-r--r--src/prop/minisat/core/Solver.h49
-rw-r--r--src/prop/minisat/core/SolverTypes.h1
-rw-r--r--src/prop/minisat/minisat.cpp8
-rw-r--r--src/prop/minisat/minisat.h4
-rw-r--r--src/prop/minisat/simp/SimpSolver.cc9
-rw-r--r--src/prop/prop_engine.cpp14
-rw-r--r--src/prop/prop_engine.h7
-rw-r--r--src/prop/sat_solver.h5
-rw-r--r--src/prop/theory_proxy.cpp4
-rw-r--r--src/prop/theory_proxy.h6
-rw-r--r--src/theory/bv/bitblaster.cpp2
-rw-r--r--src/theory/logic_info.cpp7
-rw-r--r--src/theory/logic_info.h3
-rw-r--r--src/theory/theory_engine.cpp4
17 files changed, 268 insertions, 474 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 */
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<SatLiteral, TNode, SatLiteralHashFunction> 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<SatLiteral, TNode, SatLiteralHashFunction> LiteralToNodeMap;
/** Cache of what literals have been registered to a node. */
- typedef __gnu_cxx::hash_map<Node, TranslationInfo, NodeHashFunction> TranslationCache;
+ typedef context::CDHashMap<Node, SatLiteral, NodeHashFunction> NodeToLiteralMap;
protected:
@@ -69,8 +60,11 @@ protected:
/** Boolean variables that we translated */
context::CDList<TNode> 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<TNode> 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;
@@ -219,13 +198,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<TNode>& 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<Lit>& 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<Lit>& 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<Lit>& 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<Lit>& 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<Lit>& 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<Lit>& 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<CRef>& 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<VarIntroInfo> 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<Lit>& 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<Lit, vec<Watcher>, WatcherDeleted>
watches; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
vec<lbool> assigns; // The current assignments.
+ vec<int> assigns_lim; // The size by levels of the current assignment
vec<char> polarity; // The preferred polarity of each variable (bit 0) and whether it's locked (bit 1).
vec<char> decision; // Declares if a variable is eligible for selection in the decision heuristic.
vec<int> flipped; // Which trail_lim decisions have been flipped in this context.
vec<Lit> trail; // Assignment stack; stores all assigments made in the order they were made.
vec<int> trail_lim; // Separator indices for different decision levels in 'trail'.
- vec<Lit> trail_user; // Stack of assignments to UNdo on user pop.
- vec<int> trail_user_lim; // Separator indices for different user levels in 'trail'.
vec<bool> trail_ok; // Stack of "whether we're in conflict" flags.
vec<VarData> 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<Lit>& out_learnt, int& out_btlevel); // (bt = backtrack)
void analyzeFinal (Lit p, vec<Lit>& 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<Lit>& 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<Node, CnfStream::TranslationInfo> curr = *i;
- SatLiteral l = curr.second.literal;
+ pair<Node, SatLiteral> 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
@@ -246,13 +246,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.
*/
bool hasValue(TNode node, bool& value) const;
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 <string>
+#include <vector>
#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<bool> 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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback