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 | |
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')
-rw-r--r-- | src/prop/cnf_stream.cpp | 29 | ||||
-rw-r--r-- | src/prop/cnf_stream.h | 13 | ||||
-rw-r--r-- | src/prop/prop_engine.cpp | 9 | ||||
-rw-r--r-- | src/prop/prop_engine.h | 7 |
4 files changed, 41 insertions, 17 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 0f1161a06..f47637b72 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -44,8 +44,9 @@ namespace CVC4 { namespace prop { -CnfStream::CnfStream(SatSolver *satSolver, Registrar* registrar, bool fullLitToNodeMap) : +CnfStream::CnfStream(SatSolver *satSolver, Registrar* registrar, context::Context* context, bool fullLitToNodeMap) : d_satSolver(satSolver), + d_booleanVariables(context), d_fullLitToNodeMap(fullLitToNodeMap), d_registrar(registrar) { } @@ -66,8 +67,8 @@ void CnfStream::recordTranslation(TNode node, bool alwaysRecord) { } } -TseitinCnfStream::TseitinCnfStream(SatSolver* satSolver, Registrar* registrar, bool fullLitToNodeMap) : - CnfStream(satSolver, registrar, fullLitToNodeMap) { +TseitinCnfStream::TseitinCnfStream(SatSolver* satSolver, Registrar* registrar, context::Context* context, bool fullLitToNodeMap) : + CnfStream(satSolver, registrar, context, fullLitToNodeMap) { } void CnfStream::assertClause(TNode node, SatClause& c) { @@ -230,22 +231,26 @@ TNode CnfStream::getNode(const SatLiteral& literal) { return find->second; } +void CnfStream::getBooleanVariables(std::vector<TNode>& outputVariables) const { + context::CDList<TNode>::const_iterator it, it_end; + for (it = d_booleanVariables.begin(); it != d_booleanVariables.end(); ++ it) { + outputVariables.push_back(*it); + } +} + SatLiteral CnfStream::convertAtom(TNode node) { Debug("cnf") << "convertAtom(" << node << ")" << endl; Assert(!isTranslated(node), "atom already mapped!"); - // boolean variables are not theory literals - bool theoryLiteral = node.getKind() != kind::VARIABLE; - SatLiteral lit = newLiteral(node, theoryLiteral); - if(node.getKind() == kind::CONST_BOOLEAN) { - if(node.getConst<bool>()) { - assertClause(node, lit); - } else { - assertClause(node, ~lit); - } + // Is this a variable add it to the list + if (node.isVar()) { + d_booleanVariables.push_back(node); } + // Make a new literal (variables are not considered theory literals) + SatLiteral lit = newLiteral(node, !node.isVar()); + // We have a literal, so it has to be recorded. The definitional clauses // go away on user-pop, so this literal will have to be re-vivified if it's // used subsequently. 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: diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index f115aa6d0..fe25caf29 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -65,11 +65,11 @@ public: } }; -PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* context) : +PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext, Context* userContext) : d_inCheckSat(false), d_theoryEngine(te), d_decisionEngine(de), - d_context(context), + d_context(satContext), d_satSolver(NULL), d_cnfStream(NULL), d_satTimer(*this), @@ -82,6 +82,7 @@ PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* context) : theory::TheoryRegistrar* registrar = new theory::TheoryRegistrar(d_theoryEngine); d_cnfStream = new CVC4::prop::TseitinCnfStream (d_satSolver, registrar, + userContext, // fullLitToNode Map = options::threads() > 1 || options::decisionMode() == decision::DECISION_STRATEGY_RELEVANCY); @@ -246,6 +247,10 @@ bool PropEngine::hasValue(TNode node, bool& value) const { } } +void PropEngine::getBooleanVariables(std::vector<TNode>& outputVariables) const { + d_cnfStream->getBooleanVariables(outputVariables); +} + void PropEngine::ensureLiteral(TNode n) { d_cnfStream->ensureLiteral(n); } diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 2d4e08db7..f3b1ccaf3 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -157,7 +157,7 @@ public: /** * Create a PropEngine with a particular decision and theory engine. */ - PropEngine(TheoryEngine*, DecisionEngine*, context::Context*); + PropEngine(TheoryEngine*, DecisionEngine*, context::Context* satContext, context::Context* userContext); /** * Destructor. @@ -260,6 +260,11 @@ public: bool hasValue(TNode node, bool& value) const; /** + * Returns the Boolean variables known to the SAT solver. + */ + void getBooleanVariables(std::vector<TNode>& outputVariables) const; + + /** * Ensure that the given node will have a designated SAT literal * that is definitionally equal to it. The result of this function * is that the Node can be queried via getSatValue(). |