diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-02-20 17:59:33 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-02-20 17:59:33 +0000 |
commit | 3d2b33d66998261f9369cccc098140f64bc8b417 (patch) | |
tree | 9176ad2684415f8fb95f75a5655e8b17dcdf9793 /src/prop/cnf_stream.h | |
parent | 92155f5e40ed2cf452dc5e2f618e7be6542293e8 (diff) |
portfolio merge
Diffstat (limited to 'src/prop/cnf_stream.h')
-rw-r--r-- | src/prop/cnf_stream.h | 13 |
1 files changed, 11 insertions, 2 deletions
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 5eaeeef94..c9fd4a08b 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -69,6 +69,13 @@ protected: TranslationCache d_translationCache; NodeCache d_nodeCache; + /** + * True if the lit-to-Node map should be kept for all lits, not just + * theory lits. This is true if e.g. replay logging is on, which + * dumps the Nodes corresponding to decision literals. + */ + const bool d_fullLitToNodeMap; + /** The "registrar" for pre-registration of terms */ theory::Registrar d_registrar; @@ -179,8 +186,10 @@ public: * set of clauses and sends them to the given sat solver. * @param satSolver the sat solver to use * @param registrar the entity that takes care of preregistration of Nodes + * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping, + * even for non-theory literals. */ - CnfStream(SatInputInterface* satSolver, theory::Registrar registrar); + CnfStream(SatInputInterface* satSolver, theory::Registrar registrar, bool fullLitToNodeMap = false); /** * Destructs a CnfStream. This implementation does nothing, but we @@ -283,7 +292,7 @@ public: private: /** - * Same as above, except that removable is rememebered. + * Same as above, except that removable is remembered. */ void convertAndAssert(TNode node, bool negated); |