diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-04-10 00:44:20 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-04-10 00:44:20 +0000 |
commit | 969b144a5f9630d646afdf0ff0a053df38d0ed1a (patch) | |
tree | 92eb38ad161abfe3af979a86285549168d118c5e /src/prop/cnf_stream.cpp | |
parent | 8495ee8e7de4a7e472d72cfb20290940c59794e3 (diff) |
merge from replay branch
Diffstat (limited to 'src/prop/cnf_stream.cpp')
-rw-r--r-- | src/prop/cnf_stream.cpp | 19 |
1 files changed, 14 insertions, 5 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index fc7fa600a..6732b09bc 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -31,11 +31,18 @@ using namespace std; using namespace CVC4::kind; +#ifdef CVC4_REPLAY +# define CVC4_USE_REPLAY true +#else /* CVC4_REPLAY */ +# define CVC4_USE_REPLAY false +#endif /* CVC4_REPLAY */ + namespace CVC4 { namespace prop { CnfStream::CnfStream(SatInputInterface *satSolver, theory::Registrar registrar) : - d_satSolver(satSolver), d_registrar(registrar) { + d_satSolver(satSolver), + d_registrar(registrar) { } void CnfStream::recordTranslation(TNode node) { @@ -46,7 +53,6 @@ void CnfStream::recordTranslation(TNode node) { } } - TseitinCnfStream::TseitinCnfStream(SatInputInterface* satSolver, theory::Registrar registrar) : CnfStream(satSolver, registrar) { } @@ -88,7 +94,7 @@ bool CnfStream::hasLiteral(TNode n) const { } SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) { - Debug("cnf") << "newLiteral(" << node << ")" << endl; + Debug("cnf") << "newLiteral(" << node << ", " << theoryLiteral << ")" << endl; // Get the literal for this node SatLiteral lit; @@ -108,14 +114,16 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) { d_translationCache[node].level = level; d_translationCache[node.notNode()].level = level; - // If it's a theory literal, store it for back queries - if (theoryLiteral) { + // If it's a theory literal, need to store it for back queries + if ( theoryLiteral || + ( CVC4_USE_REPLAY && Options::current()->replayLog != NULL ) ) { d_nodeCache[lit] = node; d_nodeCache[~lit] = node.notNode(); } // Here, you can have it Debug("cnf") << "newLiteral(" << node << ") => " << lit << endl; + // have to keep track of this, because with the call to preRegister(), // the cnf stream is re-entrant! bool wasAssertingLemma = d_assertingLemma; @@ -155,6 +163,7 @@ SatLiteral CnfStream::convertAtom(TNode node) { SatLiteral CnfStream::getLiteral(TNode node) { TranslationCache::iterator find = d_translationCache.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; Debug("cnf") << "CnfStream::getLiteral(" << node << ") => " << literal << std::endl; |