diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-03-08 23:03:48 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-03-08 23:03:48 +0000 |
commit | de0160112edbed8ce9b62bf87172ae2f0e99a013 (patch) | |
tree | c9fc1e4b7f365dbd34a79b8360f3ac8a006aad68 /src/prop/cnf_stream.cpp | |
parent | fc810750142ee15917c6d77d21d987c369ce774b (diff) |
adding simple-uf to the regressions, and the code that apparently solves it
Diffstat (limited to 'src/prop/cnf_stream.cpp')
-rw-r--r-- | src/prop/cnf_stream.cpp | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 2efad3cb2..51992a31c 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -87,6 +87,25 @@ SatLiteral CnfStream::newLiteral(const TNode& node, bool theoryLiteral) { return lit; } +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; +} + +SatLiteral CnfStream::getLiteral(const TNode& node) { + TranslationCache::iterator find = d_translationCache.find(node); + SatLiteral literal; + if(find != d_translationCache.end()) { + literal = find->second; + } + Debug("cnf") << "CnfStream::getLiteral(" << node << ") => " << literal << std::endl; + return literal; +} + SatLiteral TseitinCnfStream::handleAtom(const TNode& node) { Assert(node.isAtomic(), "handleAtom(n) expects n to be an atom"); Assert(!isCached(node), "atom already mapped!"); |