From: Dejan Jovanović Date: Wed, 3 Oct 2012 17:59:33 +0000 (+0000) Subject: adding ::getBooleanVariables to the PropEngine X-Git-Tag: cvc5-1.0.0~7750 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f0547f8a6fe9cecefde8b1d0c3dc8fcf50219c6b;p=cvc5.git adding ::getBooleanVariables to the PropEngine you can get the Boolean variables in the TheoryEngine now by using d_propEngine->getBooleanVariables --- 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& outputVariables) const { + context::CDList::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()) { - 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 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: 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& 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. @@ -259,6 +259,11 @@ public: */ bool hasValue(TNode node, bool& value) const; + /** + * Returns the Boolean variables known to the SAT solver. + */ + void getBooleanVariables(std::vector& outputVariables) const; + /** * Ensure that the given node will have a designated SAT literal * that is definitionally equal to it. The result of this function diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index a857351a5..d3806199b 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -427,7 +427,7 @@ void SmtEngine::finishInit() { d_decisionEngine = new DecisionEngine(d_context, d_userContext); d_decisionEngine->init(); // enable appropriate strategies - d_propEngine = new PropEngine(d_theoryEngine, d_decisionEngine, d_context); + d_propEngine = new PropEngine(d_theoryEngine, d_decisionEngine, d_context, d_userContext); d_theoryEngine->setPropEngine(d_propEngine); d_theoryEngine->setDecisionEngine(d_decisionEngine); diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp index eb5f3e155..2c45fb603 100644 --- a/src/theory/bv/bitblaster.cpp +++ b/src/theory/bv/bitblaster.cpp @@ -61,7 +61,7 @@ Bitblaster::Bitblaster(context::Context* c, bv::TheoryBV* bv) : d_statistics() { d_satSolver = prop::SatSolverFactory::createMinisat(c); - d_cnfStream = new TseitinCnfStream(d_satSolver, new NullRegistrar()); + d_cnfStream = new TseitinCnfStream(d_satSolver, new NullRegistrar(), new Context()); MinisatNotify* notify = new MinisatNotify(d_cnfStream, bv); d_satSolver->setNotify(notify); diff --git a/test/unit/prop/cnf_stream_white.h b/test/unit/prop/cnf_stream_white.h index 81f108fb2..f5f52d90e 100644 --- a/test/unit/prop/cnf_stream_white.h +++ b/test/unit/prop/cnf_stream_white.h @@ -156,7 +156,7 @@ class CnfStreamWhite : public CxxTest::TestSuite { d_theoryEngine = d_smt->d_theoryEngine; d_satSolver = new FakeSatSolver(); - d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver, new theory::TheoryRegistrar(d_theoryEngine)); + d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver, new theory::TheoryRegistrar(d_theoryEngine), new context::Context()); } void tearDown() {