diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-03-11 20:53:41 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-03-11 20:53:41 +0000 |
commit | 90d829959edf8ad97bd837230933c8443f63b95b (patch) | |
tree | c16151da149b9db04d84f726efe12076c1d75846 /src/prop | |
parent | 7cc72123f6b422a53c8840ca034cfdb353be59bf (diff) |
Changing const TNode& to TNode in the CNF conversion + a new small benchmark that fail on "x != x"
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/cnf_stream.cpp | 34 | ||||
-rw-r--r-- | src/prop/cnf_stream.h | 32 | ||||
-rw-r--r-- | src/prop/sat.h | 2 |
3 files changed, 34 insertions, 34 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index a5924a544..44768009e 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -61,23 +61,23 @@ void CnfStream::assertClause(SatLiteral a, SatLiteral b, SatLiteral c) { assertClause(clause); } -bool CnfStream::isCached(const TNode& n) const { +bool CnfStream::isCached(TNode n) const { return d_translationCache.find(n) != d_translationCache.end(); } -SatLiteral CnfStream::lookupInCache(const TNode& n) const { +SatLiteral CnfStream::lookupInCache(TNode n) const { Assert(isCached(n), "Node is not in CNF translation cache"); return d_translationCache.find(n)->second; } -void CnfStream::cacheTranslation(const TNode& node, SatLiteral lit) { +void CnfStream::cacheTranslation(TNode node, SatLiteral lit) { Debug("cnf") << "caching translation " << node << " to " << lit << endl; // We always cash bot the node and the negation at the same time d_translationCache[node] = lit; d_translationCache[node.notNode()] = ~lit; } -SatLiteral CnfStream::newLiteral(const TNode& node, bool theoryLiteral) { +SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) { SatLiteral lit = SatLiteral(d_satSolver->newVar(theoryLiteral)); cacheTranslation(node, lit); if (theoryLiteral) { @@ -96,7 +96,7 @@ Node CnfStream::getNode(const SatLiteral& literal) { return node; } -SatLiteral CnfStream::getLiteral(const TNode& node) { +SatLiteral CnfStream::getLiteral(TNode node) { TranslationCache::iterator find = d_translationCache.find(node); Assert(find != d_translationCache.end(), "Literal not in the CNF Cache"); SatLiteral literal = find->second; @@ -104,14 +104,14 @@ SatLiteral CnfStream::getLiteral(const TNode& node) { return literal; } -SatLiteral TseitinCnfStream::handleAtom(const TNode& node) { +SatLiteral TseitinCnfStream::handleAtom(TNode node) { Assert(node.isAtomic(), "handleAtom(n) expects n to be an atom"); Assert(!isCached(node), "atom already mapped!"); Debug("cnf") << "handleAtom(" << node << ")" << endl; - bool theoryLiteral = node.getKind() != kind::VARIABLE; - SatLiteral lit = newLiteral(node, theoryLiteral); + bool theoryLiteral = node.getKind() != kind::VARIABLE; + SatLiteral lit = newLiteral(node, theoryLiteral); switch(node.getKind()) { case TRUE: @@ -127,7 +127,7 @@ SatLiteral TseitinCnfStream::handleAtom(const TNode& node) { return lit; } -SatLiteral TseitinCnfStream::handleXor(const TNode& xorNode) { +SatLiteral TseitinCnfStream::handleXor(TNode xorNode) { Assert(!isCached(xorNode), "Atom already mapped!"); Assert(xorNode.getKind() == XOR, "Expecting an XOR expression!"); Assert(xorNode.getNumChildren() == 2, "Expecting exactly 2 children!"); @@ -145,7 +145,7 @@ SatLiteral TseitinCnfStream::handleXor(const TNode& xorNode) { return xorLit; } -SatLiteral TseitinCnfStream::handleOr(const TNode& orNode) { +SatLiteral TseitinCnfStream::handleOr(TNode orNode) { Assert(!isCached(orNode), "Atom already mapped!"); Assert(orNode.getKind() == OR, "Expecting an OR expression!"); Assert(orNode.getNumChildren() > 1, "Expecting more then 1 child!"); @@ -181,7 +181,7 @@ SatLiteral TseitinCnfStream::handleOr(const TNode& orNode) { return orLit; } -SatLiteral TseitinCnfStream::handleAnd(const TNode& andNode) { +SatLiteral TseitinCnfStream::handleAnd(TNode andNode) { Assert(!isCached(andNode), "Atom already mapped!"); Assert(andNode.getKind() == AND, "Expecting an AND expression!"); Assert(andNode.getNumChildren() > 1, "Expecting more than 1 child!"); @@ -216,7 +216,7 @@ SatLiteral TseitinCnfStream::handleAnd(const TNode& andNode) { return andLit; } -SatLiteral TseitinCnfStream::handleImplies(const TNode& impliesNode) { +SatLiteral TseitinCnfStream::handleImplies(TNode impliesNode) { Assert(!isCached(impliesNode), "Atom already mapped!"); Assert(impliesNode.getKind() == IMPLIES, "Expecting an IMPLIES expression!"); Assert(impliesNode.getNumChildren() == 2, "Expecting exactly 2 children!"); @@ -241,7 +241,7 @@ SatLiteral TseitinCnfStream::handleImplies(const TNode& impliesNode) { } -SatLiteral TseitinCnfStream::handleIff(const TNode& iffNode) { +SatLiteral TseitinCnfStream::handleIff(TNode iffNode) { Assert(!isCached(iffNode), "Atom already mapped!"); Assert(iffNode.getKind() == IFF, "Expecting an IFF expression!"); Assert(iffNode.getNumChildren() == 2, "Expecting exactly 2 children!"); @@ -271,7 +271,7 @@ SatLiteral TseitinCnfStream::handleIff(const TNode& iffNode) { } -SatLiteral TseitinCnfStream::handleNot(const TNode& notNode) { +SatLiteral TseitinCnfStream::handleNot(TNode notNode) { Assert(!isCached(notNode), "Atom already mapped!"); Assert(notNode.getKind() == NOT, "Expecting a NOT expression!"); Assert(notNode.getNumChildren() == 1, "Expecting exactly 2 children!"); @@ -284,7 +284,7 @@ SatLiteral TseitinCnfStream::handleNot(const TNode& notNode) { return notLit; } -SatLiteral TseitinCnfStream::handleIte(const TNode& iteNode) { +SatLiteral TseitinCnfStream::handleIte(TNode iteNode) { Assert(iteNode.getKind() == ITE); Assert(iteNode.getNumChildren() == 3); @@ -309,7 +309,7 @@ SatLiteral TseitinCnfStream::handleIte(const TNode& iteNode) { return iteLit; } -SatLiteral TseitinCnfStream::toCNF(const TNode& node) { +SatLiteral TseitinCnfStream::toCNF(TNode node) { // If the node has already been translated, return the previous translation if(isCached(node)) { @@ -342,7 +342,7 @@ SatLiteral TseitinCnfStream::toCNF(const TNode& node) { } } -void TseitinCnfStream::convertAndAssert(const TNode& node) { +void TseitinCnfStream::convertAndAssert(TNode node) { Debug("cnf") << "convertAndAssert(" << node << ")" << endl; // If the node is a conjuntion, we handle each conjunct separatelu if(node.getKind() == AND) { diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 2581046c1..7d7912e10 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -87,14 +87,14 @@ protected: * @param node the node * @return true if the node has been cached */ - bool isCached(const TNode& node) const; + bool isCached(TNode node) const; /** * Returns the cashed literal corresponding to the given node. * @param node the node to lookup * @return returns the corresponding literal */ - SatLiteral lookupInCache(const TNode& n) const; + SatLiteral lookupInCache(TNode n) const; /** * Caches the pair of the node and the literal corresponding to the @@ -102,7 +102,7 @@ protected: * @param node node * @param lit */ - void cacheTranslation(const TNode& node, SatLiteral lit); + void cacheTranslation(TNode node, SatLiteral lit); /** * Acquires a new variable from the SAT solver to represent the node and @@ -112,7 +112,7 @@ protected: * informed when set to true/false * @return the literal corresponding to the formula */ - SatLiteral newLiteral(const TNode& node, bool theoryLiteral = false); + SatLiteral newLiteral(TNode node, bool theoryLiteral = false); public: @@ -136,7 +136,7 @@ public: * @param node node to convert and assert * @param whether the sat solver can choose to remove this clause */ - virtual void convertAndAssert(const TNode& node) = 0; + virtual void convertAndAssert(TNode node) = 0; /** * Returns a node the is represented by a give SatLiteral literal. @@ -149,7 +149,7 @@ public: * Returns the literal the represents the given node in the SAT CNF * representation. */ - SatLiteral getLiteral(const TNode& node); + SatLiteral getLiteral(TNode node); }; /* class CnfStream */ @@ -171,7 +171,7 @@ public: * Convert a given formula to CNF and assert it to the SAT solver. * @param node the formula to assert */ - void convertAndAssert(const TNode& node); + void convertAndAssert(TNode node); /** * Constructs the stream to use the given sat solver. @@ -191,21 +191,21 @@ private: // - returning l // // handleX( n ) can assume that n is not in d_translationCache - SatLiteral handleAtom(const TNode& node); - SatLiteral handleNot(const TNode& node); - SatLiteral handleXor(const TNode& node); - SatLiteral handleImplies(const TNode& node); - SatLiteral handleIff(const TNode& node); - SatLiteral handleIte(const TNode& node); - SatLiteral handleAnd(const TNode& node); - SatLiteral handleOr(const TNode& node); + SatLiteral handleAtom(TNode node); + SatLiteral handleNot(TNode node); + SatLiteral handleXor(TNode node); + SatLiteral handleImplies(TNode node); + SatLiteral handleIff(TNode node); + SatLiteral handleIte(TNode node); + SatLiteral handleAnd(TNode node); + SatLiteral handleOr(TNode node); /** * Transforms the node into CNF recursively. * @param node the formula to transform * @return the literal representing the root of the formula */ - SatLiteral toCNF(const TNode& node); + SatLiteral toCNF(TNode node); }; /* class TseitinCnfStream */ diff --git a/src/prop/sat.h b/src/prop/sat.h index f10531080..ec38bb019 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -179,7 +179,7 @@ void SatSolver::theoryCheck(SatClause& conflict) { Node conflictNode = d_theoryEngine->getConflict(); // If the conflict is there, construct the conflict clause if (!conflictNode.isNull()) { - Debug("prop") << "SatSolver::theoryCheck() => conflict" << std::endl; + Debug("prop") << "SatSolver::theoryCheck() => conflict: " << conflictNode << std::endl; Node::const_iterator literal_it = conflictNode.begin(); Node::const_iterator literal_end = conflictNode.end(); while (literal_it != literal_end) { |