From f0547f8a6fe9cecefde8b1d0c3dc8fcf50219c6b Mon Sep 17 00:00:00 2001 From: Dejan Jovanović Date: Wed, 3 Oct 2012 17:59:33 +0000 Subject: adding ::getBooleanVariables to the PropEngine you can get the Boolean variables in the TheoryEngine now by using d_propEngine->getBooleanVariables --- src/prop/cnf_stream.h | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) (limited to 'src/prop/cnf_stream.h') diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 69db89086..5efedd4ca 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -67,6 +67,9 @@ protected: /** The SAT solver we will be using */ SatSolver *d_satSolver; + /** Boolean variables that we translated */ + context::CDList d_booleanVariables; + TranslationCache d_translationCache; NodeCache d_nodeCache; @@ -187,10 +190,11 @@ 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 context the context that the CNF should respect * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping, * even for non-theory literals */ - CnfStream(SatSolver* satSolver, Registrar* registrar, bool fullLitToNodeMap = false); + CnfStream(SatSolver* satSolver, Registrar* registrar, context::Context* context, bool fullLitToNodeMap = false); /** * Destructs a CnfStream. This implementation does nothing, but we @@ -245,6 +249,11 @@ public: */ SatLiteral getLiteral(TNode node); + /** + * Returns the Boolean variables from the input problem. + */ + void getBooleanVariables(std::vector& outputVariables) const; + const TranslationCache& getTranslationCache() const { return d_translationCache; } @@ -290,7 +299,7 @@ public: * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping, * even for non-theory literals */ - TseitinCnfStream(SatSolver* satSolver, Registrar* registrar, bool fullLitToNodeMap = false); + TseitinCnfStream(SatSolver* satSolver, Registrar* registrar, context::Context* context, bool fullLitToNodeMap = false); private: -- cgit v1.2.3