From: Dejan Jovanović Date: Sun, 25 Mar 2012 20:04:43 +0000 (+0000) Subject: sat.h,cpp -> theory_proxy.h,cpp (this is what it defines) X-Git-Tag: cvc5-1.0.0~8268 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=426abc52a0f1631f2adee0eef845e3f8946c5088;p=cvc5.git sat.h,cpp -> theory_proxy.h,cpp (this is what it defines) --- diff --git a/src/prop/Makefile.am b/src/prop/Makefile.am index e6c8752d6..02a6a4714 100644 --- a/src/prop/Makefile.am +++ b/src/prop/Makefile.am @@ -11,8 +11,8 @@ libprop_la_SOURCES = \ registrar.h \ prop_engine.cpp \ prop_engine.h \ - sat.h \ - sat.cpp \ + theory_proxy.h \ + theory_proxy.cpp \ cnf_stream.h \ cnf_stream.cpp \ sat_module.h \ diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 661221441..676cc4c49 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -27,7 +27,7 @@ #include "util/output.h" #include "expr/command.h" #include "expr/expr.h" -#include "prop/sat.h" +#include "prop/theory_proxy.h" #include diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 4812c6a21..af2ff2fcd 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -28,7 +28,7 @@ #define __CVC4__PROP__CNF_STREAM_H #include "expr/node.h" -#include "prop/sat.h" +#include "prop/theory_proxy.h" #include "prop/registrar.h" #include diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 980cb1b3f..65ec025b1 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -25,7 +25,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "prop/minisat/mtl/Sort.h" #include "prop/minisat/core/Solver.h" -#include "prop/sat.h" +#include "prop/theory_proxy.h" #include "prop/sat_module.h" #include "util/output.h" #include "expr/command.h" diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index b7b3c685f..9d6a2c8f6 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -18,7 +18,7 @@ #include "prop/cnf_stream.h" #include "prop/prop_engine.h" -#include "prop/sat.h" +#include "prop/theory_proxy.h" #include "prop/sat_module.h" #include "theory/theory_engine.h" diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp deleted file mode 100644 index ab8be39eb..000000000 --- a/src/prop/sat.cpp +++ /dev/null @@ -1,173 +0,0 @@ -/********************* */ -/*! \file sat.cpp - ** \verbatim - ** Original author: cconway - ** Major contributors: dejan, taking, mdeters - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "prop/cnf_stream.h" -#include "prop/prop_engine.h" -#include "prop/sat.h" -#include "context/context.h" -#include "theory/theory_engine.h" -#include "theory/rewriter.h" -#include "expr/expr_stream.h" - -namespace CVC4 { -namespace prop { - -void TheoryProxy::variableNotify(SatVariable var) { - d_theoryEngine->preRegister(getNode(SatLiteral(var))); -} - -void TheoryProxy::theoryCheck(theory::Theory::Effort effort) { - d_theoryEngine->check(effort); -} - -void TheoryProxy::theoryPropagate(std::vector& output) { - // Get the propagated literals - std::vector outputNodes; - d_theoryEngine->getPropagatedLiterals(outputNodes); - for (unsigned i = 0, i_end = outputNodes.size(); i < i_end; ++ i) { - Debug("prop-explain") << "theoryPropagate() => " << outputNodes[i].toString() << std::endl; - output.push_back(d_cnfStream->getLiteral(outputNodes[i])); - } -} - -void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) { - TNode lNode = d_cnfStream->getNode(l); - Debug("prop-explain") << "explainPropagation(" << lNode << ")" << std::endl; - Node theoryExplanation = d_theoryEngine->getExplanation(lNode); - Debug("prop-explain") << "explainPropagation() => " << theoryExplanation << std::endl; - if (theoryExplanation.getKind() == kind::AND) { - Node::const_iterator it = theoryExplanation.begin(); - Node::const_iterator it_end = theoryExplanation.end(); - explanation.push_back(l); - for (; it != it_end; ++ it) { - explanation.push_back(~d_cnfStream->getLiteral(*it)); - } - } else { - explanation.push_back(l); - explanation.push_back(~d_cnfStream->getLiteral(theoryExplanation)); - } -} - -void TheoryProxy::enqueueTheoryLiteral(const SatLiteral& l) { - Node literalNode = d_cnfStream->getNode(l); - Debug("prop") << "enqueueing theory literal " << l << " " << literalNode << std::endl; - Assert(!literalNode.isNull()); - d_theoryEngine->assertFact(literalNode); -} - -SatLiteral TheoryProxy::getNextDecisionRequest() { - TNode n = d_theoryEngine->getNextDecisionRequest(); - return n.isNull() ? undefSatLiteral : d_cnfStream->getLiteral(n); -} - -bool TheoryProxy::theoryNeedCheck() const { - return d_theoryEngine->needCheck(); -} - -void TheoryProxy::removeClausesAboveLevel(int level) { - d_cnfStream->removeClausesAboveLevel(level); -} - -TNode TheoryProxy::getNode(SatLiteral lit) { - return d_cnfStream->getNode(lit); -} - -void TheoryProxy::notifyRestart() { - d_propEngine->checkTime(); - d_theoryEngine->notifyRestart(); - - static uint32_t lemmaCount = 0; - - if(Options::current()->lemmaInputChannel != NULL) { - while(Options::current()->lemmaInputChannel->hasNewLemma()) { - Debug("shared") << "shared" << std::endl; - Expr lemma = Options::current()->lemmaInputChannel->getNewLemma(); - Node asNode = lemma.getNode(); - asNode = theory::Rewriter::rewrite(asNode); - - if(d_shared.find(asNode) == d_shared.end()) { - d_shared.insert(asNode); - if(asNode.getKind() == kind::OR) { - ++lemmaCount; - if(lemmaCount % 1 == 0) { - Debug("shared") << "=) " << asNode << std::endl; - } - d_propEngine->assertLemma(d_theoryEngine->preprocess(asNode), false, true); - } else { - Debug("shared") << "=(" << asNode << std::endl; - } - } else { - Debug("shared") <<"drop shared " << asNode << std::endl; - } - } - } -} - -void TheoryProxy::notifyNewLemma(SatClause& lemma) { - Assert(lemma.size() > 0); - if(Options::current()->lemmaOutputChannel != NULL) { - if(lemma.size() == 1) { - // cannot share units yet - //Options::current()->lemmaOutputChannel->notifyNewLemma(d_cnfStream->getNode(lemma[0]).toExpr()); - } else { - NodeBuilder<> b(kind::OR); - for(unsigned i = 0, i_end = lemma.size(); i < i_end; ++i) { - b << d_cnfStream->getNode(lemma[i]); - } - Node n = b; - - if(d_shared.find(n) == d_shared.end()) { - d_shared.insert(n); - Options::current()->lemmaOutputChannel->notifyNewLemma(n.toExpr()); - } else { - Debug("shared") <<"drop new " << n << std::endl; - } - } - } -} - -SatLiteral TheoryProxy::getNextReplayDecision() { -#ifdef CVC4_REPLAY - if(Options::current()->replayStream != NULL) { - Expr e = Options::current()->replayStream->nextExpr(); - if(!e.isNull()) { // we get null node when out of decisions to replay - // convert & return - return d_cnfStream->getLiteral(e); - } - } -#endif /* CVC4_REPLAY */ - //FIXME! - return undefSatLiteral; -} - -void TheoryProxy::logDecision(SatLiteral lit) { -#ifdef CVC4_REPLAY - if(Options::current()->replayLog != NULL) { - Assert(lit != undefSatLiteral, "logging an `undef' decision ?!"); - *Options::current()->replayLog << d_cnfStream->getNode(lit) << std::endl; - } -#endif /* CVC4_REPLAY */ -} - -void TheoryProxy::checkTime() { - d_propEngine->checkTime(); -} - -}/* CVC4::prop namespace */ -}/* CVC4 namespace */ diff --git a/src/prop/sat.h b/src/prop/sat.h deleted file mode 100644 index 8456e5d88..000000000 --- a/src/prop/sat.h +++ /dev/null @@ -1,168 +0,0 @@ -/********************* */ -/*! \file sat.h - ** \verbatim - ** Original author: mdeters - ** Major contributors: taking, cconway, dejan - ** Minor contributors (to current version): barrett - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief SAT Solver. - ** - ** SAT Solver. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__PROP__SAT_H -#define __CVC4__PROP__SAT_H - -// Just defining this for now, since there's no other SAT solver bindings. -// Optional blocks below will be unconditionally included -#define __CVC4_USE_MINISAT - -#include "theory/theory.h" -#include "util/options.h" -#include "util/stats.h" - -#include "prop/sat_module.h" - -#ifdef __CVC4_USE_MINISAT - -#include "prop/minisat/core/Solver.h" -#include "prop/minisat/core/SolverTypes.h" -#include "prop/minisat/simp/SimpSolver.h" - -#endif /* __CVC4_USE_MINISAT */ - -namespace CVC4 { - -class TheoryEngine; - -namespace prop { - -class PropEngine; -class CnfStream; - -/** - * The proxy class that allows the SatSolver to communicate with the theories - */ -class TheoryProxy { - - /** The prop engine we are using */ - PropEngine* d_propEngine; - - /** The CNF engine we are using */ - CnfStream* d_cnfStream; - - /** The theory engine we are using */ - TheoryEngine* d_theoryEngine; - - /** Context we will be using to synchronzie the sat solver */ - context::Context* d_context; - - /** - * Set of all lemmas that have been "shared" in the portfolio---i.e., - * all imported and exported lemmas. - */ - std::hash_set d_shared; - -public: - TheoryProxy(PropEngine* propEngine, - TheoryEngine* theoryEngine, - context::Context* context, - CnfStream* cnfStream); - - ~TheoryProxy(); - - - void theoryCheck(theory::Theory::Effort effort); - - void explainPropagation(SatLiteral l, SatClause& explanation); - - void theoryPropagate(SatClause& output); - - void enqueueTheoryLiteral(const SatLiteral& l); - - SatLiteral getNextDecisionRequest(); - - bool theoryNeedCheck() const; - - void removeClausesAboveLevel(int level); - - /** - * Notifies of a new variable at a decision level. - */ - void variableNotify(SatVariable var); - - void unregisterVar(SatLiteral lit); - - void renewVar(SatLiteral lit, int level = -1); - - TNode getNode(SatLiteral lit); - - void notifyRestart(); - - void notifyNewLemma(SatClause& lemma); - - SatLiteral getNextReplayDecision(); - - void logDecision(SatLiteral lit); - - void checkTime(); - -};/* class SatSolver */ - -/* Functions that delegate to the concrete SAT solver. */ - -inline TheoryProxy::TheoryProxy(PropEngine* propEngine, - TheoryEngine* theoryEngine, - context::Context* context, - CnfStream* cnfStream) : - d_propEngine(propEngine), - d_cnfStream(cnfStream), - d_theoryEngine(theoryEngine), - d_context(context) -{} - -}/* CVC4::prop namespace */ - -inline std::ostream& operator <<(std::ostream& out, prop::SatLiteral lit) { - out << lit.toString(); - return out; -} - -inline std::ostream& operator <<(std::ostream& out, const prop::SatClause& clause) { - out << "clause:"; - for(unsigned i = 0; i < clause.size(); ++i) { - out << " " << clause[i]; - } - out << ";"; - return out; -} - -inline std::ostream& operator <<(std::ostream& out, prop::SatLiteralValue val) { - std::string str; - switch(val) { - case prop::SatValUnknown: - str = "_"; - case prop::SatValTrue: - str = "1"; - case prop::SatValFalse: - str = "0"; - default: - str = "Error"; - - out << str; - return out; -} - -} /* prop namespace */ - -}/* CVC4 namespace */ - -#endif /* __CVC4__PROP__SAT_H */ diff --git a/src/prop/sat_module.cpp b/src/prop/sat_module.cpp index cda32a0e8..5e5b78b44 100644 --- a/src/prop/sat_module.cpp +++ b/src/prop/sat_module.cpp @@ -22,7 +22,7 @@ #include "context/context.h" #include "theory/theory_engine.h" #include "expr/expr_stream.h" -#include "prop/sat.h" +#include "prop/theory_proxy.h" // DPLLT Minisat #include "prop/minisat/simp/SimpSolver.h" diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp new file mode 100644 index 000000000..43f7f75af --- /dev/null +++ b/src/prop/theory_proxy.cpp @@ -0,0 +1,173 @@ +/********************* */ +/*! \file sat.cpp + ** \verbatim + ** Original author: cconway + ** Major contributors: dejan, taking, mdeters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "prop/cnf_stream.h" +#include "prop/prop_engine.h" +#include "prop/theory_proxy.h" +#include "context/context.h" +#include "theory/theory_engine.h" +#include "theory/rewriter.h" +#include "expr/expr_stream.h" + +namespace CVC4 { +namespace prop { + +void TheoryProxy::variableNotify(SatVariable var) { + d_theoryEngine->preRegister(getNode(SatLiteral(var))); +} + +void TheoryProxy::theoryCheck(theory::Theory::Effort effort) { + d_theoryEngine->check(effort); +} + +void TheoryProxy::theoryPropagate(std::vector& output) { + // Get the propagated literals + std::vector outputNodes; + d_theoryEngine->getPropagatedLiterals(outputNodes); + for (unsigned i = 0, i_end = outputNodes.size(); i < i_end; ++ i) { + Debug("prop-explain") << "theoryPropagate() => " << outputNodes[i].toString() << std::endl; + output.push_back(d_cnfStream->getLiteral(outputNodes[i])); + } +} + +void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) { + TNode lNode = d_cnfStream->getNode(l); + Debug("prop-explain") << "explainPropagation(" << lNode << ")" << std::endl; + Node theoryExplanation = d_theoryEngine->getExplanation(lNode); + Debug("prop-explain") << "explainPropagation() => " << theoryExplanation << std::endl; + if (theoryExplanation.getKind() == kind::AND) { + Node::const_iterator it = theoryExplanation.begin(); + Node::const_iterator it_end = theoryExplanation.end(); + explanation.push_back(l); + for (; it != it_end; ++ it) { + explanation.push_back(~d_cnfStream->getLiteral(*it)); + } + } else { + explanation.push_back(l); + explanation.push_back(~d_cnfStream->getLiteral(theoryExplanation)); + } +} + +void TheoryProxy::enqueueTheoryLiteral(const SatLiteral& l) { + Node literalNode = d_cnfStream->getNode(l); + Debug("prop") << "enqueueing theory literal " << l << " " << literalNode << std::endl; + Assert(!literalNode.isNull()); + d_theoryEngine->assertFact(literalNode); +} + +SatLiteral TheoryProxy::getNextDecisionRequest() { + TNode n = d_theoryEngine->getNextDecisionRequest(); + return n.isNull() ? undefSatLiteral : d_cnfStream->getLiteral(n); +} + +bool TheoryProxy::theoryNeedCheck() const { + return d_theoryEngine->needCheck(); +} + +void TheoryProxy::removeClausesAboveLevel(int level) { + d_cnfStream->removeClausesAboveLevel(level); +} + +TNode TheoryProxy::getNode(SatLiteral lit) { + return d_cnfStream->getNode(lit); +} + +void TheoryProxy::notifyRestart() { + d_propEngine->checkTime(); + d_theoryEngine->notifyRestart(); + + static uint32_t lemmaCount = 0; + + if(Options::current()->lemmaInputChannel != NULL) { + while(Options::current()->lemmaInputChannel->hasNewLemma()) { + Debug("shared") << "shared" << std::endl; + Expr lemma = Options::current()->lemmaInputChannel->getNewLemma(); + Node asNode = lemma.getNode(); + asNode = theory::Rewriter::rewrite(asNode); + + if(d_shared.find(asNode) == d_shared.end()) { + d_shared.insert(asNode); + if(asNode.getKind() == kind::OR) { + ++lemmaCount; + if(lemmaCount % 1 == 0) { + Debug("shared") << "=) " << asNode << std::endl; + } + d_propEngine->assertLemma(d_theoryEngine->preprocess(asNode), false, true); + } else { + Debug("shared") << "=(" << asNode << std::endl; + } + } else { + Debug("shared") <<"drop shared " << asNode << std::endl; + } + } + } +} + +void TheoryProxy::notifyNewLemma(SatClause& lemma) { + Assert(lemma.size() > 0); + if(Options::current()->lemmaOutputChannel != NULL) { + if(lemma.size() == 1) { + // cannot share units yet + //Options::current()->lemmaOutputChannel->notifyNewLemma(d_cnfStream->getNode(lemma[0]).toExpr()); + } else { + NodeBuilder<> b(kind::OR); + for(unsigned i = 0, i_end = lemma.size(); i < i_end; ++i) { + b << d_cnfStream->getNode(lemma[i]); + } + Node n = b; + + if(d_shared.find(n) == d_shared.end()) { + d_shared.insert(n); + Options::current()->lemmaOutputChannel->notifyNewLemma(n.toExpr()); + } else { + Debug("shared") <<"drop new " << n << std::endl; + } + } + } +} + +SatLiteral TheoryProxy::getNextReplayDecision() { +#ifdef CVC4_REPLAY + if(Options::current()->replayStream != NULL) { + Expr e = Options::current()->replayStream->nextExpr(); + if(!e.isNull()) { // we get null node when out of decisions to replay + // convert & return + return d_cnfStream->getLiteral(e); + } + } +#endif /* CVC4_REPLAY */ + //FIXME! + return undefSatLiteral; +} + +void TheoryProxy::logDecision(SatLiteral lit) { +#ifdef CVC4_REPLAY + if(Options::current()->replayLog != NULL) { + Assert(lit != undefSatLiteral, "logging an `undef' decision ?!"); + *Options::current()->replayLog << d_cnfStream->getNode(lit) << std::endl; + } +#endif /* CVC4_REPLAY */ +} + +void TheoryProxy::checkTime() { + d_propEngine->checkTime(); +} + +}/* CVC4::prop namespace */ +}/* CVC4 namespace */ diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h new file mode 100644 index 000000000..85dcae68b --- /dev/null +++ b/src/prop/theory_proxy.h @@ -0,0 +1,163 @@ +/********************* */ +/*! \file sat.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: taking, cconway, dejan + ** Minor contributors (to current version): barrett + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief SAT Solver. + ** + ** SAT Solver. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PROP__SAT_H +#define __CVC4__PROP__SAT_H + +// Just defining this for now, since there's no other SAT solver bindings. +// Optional blocks below will be unconditionally included +#define __CVC4_USE_MINISAT + +#include "theory/theory.h" +#include "util/options.h" +#include "util/stats.h" + +#include "prop/sat_module.h" + +namespace CVC4 { + +class TheoryEngine; + +namespace prop { + +class PropEngine; +class CnfStream; + +/** + * The proxy class that allows the SatSolver to communicate with the theories + */ +class TheoryProxy { + + /** The prop engine we are using */ + PropEngine* d_propEngine; + + /** The CNF engine we are using */ + CnfStream* d_cnfStream; + + /** The theory engine we are using */ + TheoryEngine* d_theoryEngine; + + /** Context we will be using to synchronzie the sat solver */ + context::Context* d_context; + + /** + * Set of all lemmas that have been "shared" in the portfolio---i.e., + * all imported and exported lemmas. + */ + std::hash_set d_shared; + +public: + TheoryProxy(PropEngine* propEngine, + TheoryEngine* theoryEngine, + context::Context* context, + CnfStream* cnfStream); + + ~TheoryProxy(); + + + void theoryCheck(theory::Theory::Effort effort); + + void explainPropagation(SatLiteral l, SatClause& explanation); + + void theoryPropagate(SatClause& output); + + void enqueueTheoryLiteral(const SatLiteral& l); + + SatLiteral getNextDecisionRequest(); + + bool theoryNeedCheck() const; + + void removeClausesAboveLevel(int level); + + /** + * Notifies of a new variable at a decision level. + */ + void variableNotify(SatVariable var); + + void unregisterVar(SatLiteral lit); + + void renewVar(SatLiteral lit, int level = -1); + + TNode getNode(SatLiteral lit); + + void notifyRestart(); + + void notifyNewLemma(SatClause& lemma); + + SatLiteral getNextReplayDecision(); + + void logDecision(SatLiteral lit); + + void checkTime(); + +};/* class SatSolver */ + +/* Functions that delegate to the concrete SAT solver. */ + +inline TheoryProxy::TheoryProxy(PropEngine* propEngine, + TheoryEngine* theoryEngine, + context::Context* context, + CnfStream* cnfStream) : + d_propEngine(propEngine), + d_cnfStream(cnfStream), + d_theoryEngine(theoryEngine), + d_context(context) +{} + +}/* CVC4::prop namespace */ + +inline std::ostream& operator <<(std::ostream& out, prop::SatLiteral lit) { + out << lit.toString(); + return out; +} + +inline std::ostream& operator <<(std::ostream& out, const prop::SatClause& clause) { + out << "clause:"; + for(unsigned i = 0; i < clause.size(); ++i) { + out << " " << clause[i]; + } + out << ";"; + return out; +} + +inline std::ostream& operator <<(std::ostream& out, prop::SatLiteralValue val) { + std::string str; + switch(val) { + case prop::SatValUnknown: + str = "_"; + break; + case prop::SatValTrue: + str = "1"; + break; + case prop::SatValFalse: + str = "0"; + break; + default: + str = "Error"; + break; + } + + out << str; + return out; +} + +}/* CVC4 namespace */ + +#endif /* __CVC4__PROP__SAT_H */