diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-08-16 21:49:42 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-08-16 21:49:42 +0000 |
commit | 7c5ed2290cff5247df673b87d9401993d3ca0fc3 (patch) | |
tree | ff5e8ef54beb4218b75042066101afd480a19063 /src/prop/cnf_stream.cpp | |
parent | 5e857e4329c7e02b236a466e49009cfac0fa1d4a (diff) |
Fixing failures in minisat
Diffstat (limited to 'src/prop/cnf_stream.cpp')
-rw-r--r-- | src/prop/cnf_stream.cpp | 24 |
1 files changed, 6 insertions, 18 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 5d88a9240..5f8eb12b9 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -94,12 +94,9 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) { } Node CnfStream::getNode(const SatLiteral& literal) { - Node node; NodeCache::iterator find = d_nodeCache.find(literal); - if(find != d_nodeCache.end()) { - node = find->second; - } - return node; + Assert(find != d_nodeCache.end()); + return find->second; } SatLiteral CnfStream::convertAtom(TNode node) { @@ -121,20 +118,11 @@ SatLiteral CnfStream::convertAtom(TNode node) { return lit; } -SatLiteral CnfStream::getLiteral(TNode node, bool create /* = false */) { +SatLiteral CnfStream::getLiteral(TNode node) { TranslationCache::iterator find = d_translationCache.find(node); - SatLiteral literal; - if(create) { - if(find == d_translationCache.end()) { - literal = convertAtom(node); - } else { - literal = find->second; - } - } else { - Assert(find != d_translationCache.end(), "Literal not in the CNF Cache"); - literal = find->second; - } - Debug("cnf") << "CnfStream::getLiteral(" << node << ", create = " << create << ") => " << literal << std::endl; + Assert(find != d_translationCache.end(), "Literal not in the CNF Cache"); + SatLiteral literal = find->second; + Debug("cnf") << "CnfStream::getLiteral(" << node << ") => " << literal << std::endl; return literal; } |