diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-10-03 17:59:33 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-10-03 17:59:33 +0000 |
commit | f0547f8a6fe9cecefde8b1d0c3dc8fcf50219c6b (patch) | |
tree | a2afaaa295c8964408dd7c53127df61527e00d90 /src/prop/cnf_stream.h | |
parent | b8a010d260c90efa5433a71dd317a03f051c2592 (diff) |
adding ::getBooleanVariables to the PropEngine
you can get the Boolean variables in the TheoryEngine now by using d_propEngine->getBooleanVariables
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 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<TNode> 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<TNode>& 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: |