diff options
author | Tim King <taking@google.com> | 2016-01-05 16:29:44 -0800 |
---|---|---|
committer | Tim King <taking@google.com> | 2016-01-05 16:29:44 -0800 |
commit | 5eabda0f55cee3be81aa7ae126269c32e818322f (patch) | |
tree | b873e4cb8e5d37ff3bb70596494bc5964aaef135 /src/prop | |
parent | b717513e2a1d956c4456d13e0625957fc84c2449 (diff) |
Add SmtGlobals Class
- The options replayStream, lemmaInputChannel, lemmaOutputChannel have been removed due to their datatypes. These datatypes were previously pointers to types that were not usable from the options/ library.
- The option replayLog has been removed due to inconsistent memory management.
- SmtGlobals is a class that wraps a pointer to each of these removed options. These can each be set independently.
- There is a single SmtGlobals per SmtEngine with the lifetime of the SmtEngine.
- A pointer to this is freely given to the user of an SmtEngine to parameterize the solver after construction.
- Selected classes have been given a copy of this pointer in their constructors.
- Removed the dependence on Node from Result. Moving Result back into util/.
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/cnf_stream.cpp | 33 | ||||
-rw-r--r-- | src/prop/cnf_stream.h | 20 | ||||
-rw-r--r-- | src/prop/prop_engine.cpp | 14 | ||||
-rw-r--r-- | src/prop/prop_engine.h | 8 | ||||
-rw-r--r-- | src/prop/theory_proxy.cpp | 55 | ||||
-rw-r--r-- | src/prop/theory_proxy.h | 98 |
6 files changed, 141 insertions, 87 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index ffbc67cc4..b3666875d 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -45,21 +45,26 @@ using namespace CVC4::kind; namespace CVC4 { namespace prop { -CnfStream::CnfStream(SatSolver *satSolver, Registrar* registrar, context::Context* context, bool fullLitToNodeMap) : - d_satSolver(satSolver), - d_booleanVariables(context), - d_nodeToLiteralMap(context), - d_literalToNodeMap(context), - d_fullLitToNodeMap(fullLitToNodeMap), - d_convertAndAssertCounter(0), - d_registrar(registrar), - d_assertionTable(context), - d_removable(false) { +CnfStream::CnfStream(SatSolver* satSolver, Registrar* registrar, + context::Context* context, SmtGlobals* globals, + bool fullLitToNodeMap) + : d_satSolver(satSolver), + d_booleanVariables(context), + d_nodeToLiteralMap(context), + d_literalToNodeMap(context), + d_fullLitToNodeMap(fullLitToNodeMap), + d_convertAndAssertCounter(0), + d_registrar(registrar), + d_assertionTable(context), + d_globals(globals), + d_removable(false) { } -TseitinCnfStream::TseitinCnfStream(SatSolver* satSolver, Registrar* registrar, context::Context* context, bool fullLitToNodeMap) : - CnfStream(satSolver, registrar, context, fullLitToNodeMap) { -} +TseitinCnfStream::TseitinCnfStream(SatSolver* satSolver, Registrar* registrar, + context::Context* context, + SmtGlobals* globals, bool fullLitToNodeMap) + : CnfStream(satSolver, registrar, context, globals, fullLitToNodeMap) +{} void CnfStream::assertClause(TNode node, SatClause& c, ProofRule proof_id) { Debug("cnf") << "Inserting into stream " << c << " node = " << node << ", proof id = " << proof_id << endl; @@ -184,7 +189,7 @@ SatLiteral CnfStream::newLiteral(TNode node, bool isTheoryAtom, bool preRegister // If it's a theory literal, need to store it for back queries if ( isTheoryAtom || d_fullLitToNodeMap || - ( CVC4_USE_REPLAY && options::replayLog() != NULL ) || + ( CVC4_USE_REPLAY && d_globals->getReplayLog() != NULL ) || (Dump.isOn("clauses")) ) { d_literalToNodeMap.insert_safe(lit, node); diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index d5d01d126..cfab216fe 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -25,14 +25,15 @@ #ifndef __CVC4__PROP__CNF_STREAM_H #define __CVC4__PROP__CNF_STREAM_H +#include <ext/hash_map> + +#include "context/cdinsert_hashmap.h" +#include "context/cdlist.h" #include "expr/node.h" -#include "prop/theory_proxy.h" -#include "prop/registrar.h" #include "proof/proof_manager.h" -#include "context/cdlist.h" -#include "context/cdinsert_hashmap.h" - -#include <ext/hash_map> +#include "prop/registrar.h" +#include "prop/theory_proxy.h" +#include "smt/smt_globals.h" namespace CVC4 { namespace prop { @@ -86,6 +87,9 @@ protected: /** A table of assertions, used for regenerating proofs. */ context::CDList<Node> d_assertionTable; + /** Container for misc. globals. */ + SmtGlobals* d_globals; + /** * How many literals were already mapped at the top-level when we * tried to convertAndAssert() something. This @@ -191,7 +195,7 @@ public: * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping, * even for non-theory literals */ - CnfStream(SatSolver* satSolver, Registrar* registrar, context::Context* context, bool fullLitToNodeMap = false); + CnfStream(SatSolver* satSolver, Registrar* registrar, context::Context* context, SmtGlobals* globals, bool fullLitToNodeMap = false); /** * Destructs a CnfStream. This implementation does nothing, but we @@ -291,7 +295,7 @@ public: * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping, * even for non-theory literals */ - TseitinCnfStream(SatSolver* satSolver, Registrar* registrar, context::Context* context, bool fullLitToNodeMap = false); + TseitinCnfStream(SatSolver* satSolver, Registrar* registrar, context::Context* context, SmtGlobals* globals, bool fullLitToNodeMap = false); private: diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 2a1b05619..96ca7480f 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -25,7 +25,6 @@ #include "decision/decision_engine.h" #include "expr/expr.h" #include "expr/resource_manager.h" -#include "expr/result.h" #include "options/base_options.h" #include "options/decision_options.h" #include "options/main_options.h" @@ -40,7 +39,7 @@ #include "smt_util/command.h" #include "theory/theory_engine.h" #include "theory/theory_registrar.h" - +#include "util/result.h" using namespace std; using namespace CVC4::context; @@ -68,7 +67,7 @@ public: } }; -PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext, Context* userContext) : +PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext, Context* userContext, SmtGlobals* globals) : d_inCheckSat(false), d_theoryEngine(te), d_decisionEngine(de), @@ -78,7 +77,9 @@ PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext d_registrar(NULL), d_cnfStream(NULL), d_interrupted(false), - d_resourceManager(NodeManager::currentResourceManager()) { + d_resourceManager(NodeManager::currentResourceManager()), + d_globals(globals) +{ Debug("prop") << "Constructing the PropEngine" << endl; @@ -86,14 +87,13 @@ PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext d_registrar = new theory::TheoryRegistrar(d_theoryEngine); d_cnfStream = new CVC4::prop::TseitinCnfStream - (d_satSolver, d_registrar, - userContext, + (d_satSolver, d_registrar, userContext, d_globals, // fullLitToNode Map = options::threads() > 1 || options::decisionMode() == decision::DECISION_STRATEGY_RELEVANCY ); - d_theoryProxy = new TheoryProxy(this, d_theoryEngine, d_decisionEngine, d_context, d_cnfStream); + d_theoryProxy = new TheoryProxy(this, d_theoryEngine, d_decisionEngine, d_context, d_cnfStream, d_globals); d_satSolver->initialize(d_context, d_theoryProxy); d_decisionEngine->setSatSolver(d_satSolver); diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 57ff3c5c0..dfa84ef14 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -25,10 +25,11 @@ #include "base/modal_exception.h" #include "expr/node.h" -#include "expr/result.h" #include "options/options.h" #include "proof/proof_manager.h" +#include "smt/smt_globals.h" #include "util/unsafe_interrupt_exception.h" +#include "util/result.h" namespace CVC4 { @@ -91,12 +92,15 @@ class PropEngine { /** Dump out the satisfying assignment (after SAT result) */ void printSatisfyingAssignment(); + /** Container for misc. globals. */ + SmtGlobals* d_globals; + public: /** * Create a PropEngine with a particular decision and theory engine. */ - PropEngine(TheoryEngine*, DecisionEngine*, context::Context* satContext, context::Context* userContext); + PropEngine(TheoryEngine*, DecisionEngine*, context::Context* satContext, context::Context* userContext, SmtGlobals* global); /** * Destructor. diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 386b12391..d0830b9a5 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -31,6 +31,43 @@ namespace CVC4 { namespace prop { +TheoryProxy::TheoryProxy(PropEngine* propEngine, + TheoryEngine* theoryEngine, + DecisionEngine* decisionEngine, + context::Context* context, + CnfStream* cnfStream, + SmtGlobals* globals) + : d_propEngine(propEngine), + d_cnfStream(cnfStream), + d_decisionEngine(decisionEngine), + d_theoryEngine(theoryEngine), + d_globals(globals), + d_queue(context) +{} + +TheoryProxy::~TheoryProxy() { + /* nothing to do for now */ +} + +/** The lemma input channel we are using. */ +LemmaInputChannel* TheoryProxy::inputChannel() { + return d_globals->getLemmaInputChannel(); +} + +/** The lemma output channel we are using. */ +LemmaOutputChannel* TheoryProxy::outputChannel() { + return d_globals->getLemmaOutputChannel(); +} + +std::ostream* TheoryProxy::replayLog() { + return d_globals->getReplayLog(); +} + +ExprStream* TheoryProxy::replayStream() { + return d_globals->getReplayStream(); +} + + void TheoryProxy::variableNotify(SatVariable var) { d_theoryEngine->preRegister(getNode(SatLiteral(var))); } @@ -108,10 +145,10 @@ void TheoryProxy::notifyRestart() { static uint32_t lemmaCount = 0; - if(options::lemmaInputChannel() != NULL) { - while(options::lemmaInputChannel()->hasNewLemma()) { + if(inputChannel() != NULL) { + while(inputChannel()->hasNewLemma()) { Debug("shared") << "shared" << std::endl; - Expr lemma = options::lemmaInputChannel()->getNewLemma(); + Expr lemma = inputChannel()->getNewLemma(); Node asNode = lemma.getNode(); asNode = theory::Rewriter::rewrite(asNode); @@ -135,7 +172,7 @@ void TheoryProxy::notifyRestart() { void TheoryProxy::notifyNewLemma(SatClause& lemma) { Assert(lemma.size() > 0); - if(options::lemmaOutputChannel() != NULL) { + if(outputChannel() != NULL) { if(lemma.size() == 1) { // cannot share units yet //options::lemmaOutputChannel()->notifyNewLemma(d_cnfStream->getNode(lemma[0]).toExpr()); @@ -148,7 +185,7 @@ void TheoryProxy::notifyNewLemma(SatClause& lemma) { if(d_shared.find(n) == d_shared.end()) { d_shared.insert(n); - options::lemmaOutputChannel()->notifyNewLemma(n.toExpr()); + outputChannel()->notifyNewLemma(n.toExpr()); } else { Debug("shared") <<"drop new " << n << std::endl; } @@ -158,8 +195,8 @@ void TheoryProxy::notifyNewLemma(SatClause& lemma) { SatLiteral TheoryProxy::getNextReplayDecision() { #ifdef CVC4_REPLAY - if(options::replayStream() != NULL) { - Expr e = options::replayStream()->nextExpr(); + if(replayStream() != NULL) { + Expr e = replayStream()->nextExpr(); if(!e.isNull()) { // we get null node when out of decisions to replay // convert & return ++d_replayedDecisions; @@ -172,9 +209,9 @@ SatLiteral TheoryProxy::getNextReplayDecision() { void TheoryProxy::logDecision(SatLiteral lit) { #ifdef CVC4_REPLAY - if(options::replayLog() != NULL) { + if(replayLog() != NULL) { Assert(lit != undefSatLiteral, "logging an `undef' decision ?!"); - *options::replayLog() << d_cnfStream->getNode(lit) << std::endl; + (*replayLog()) << d_cnfStream->getNode(lit) << std::endl; } #endif /* CVC4_REPLAY */ } diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index 413b4941d..59bc859cb 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -23,9 +23,15 @@ // Optional blocks below will be unconditionally included #define __CVC4_USE_MINISAT +#include <iosfwd> + #include "context/cdqueue.h" +#include "expr/node.h" #include "expr/statistics_registry.h" #include "prop/sat_solver.h" +#include "smt/smt_globals.h" +#include "smt_util/lemma_output_channel.h" +#include "smt_util/lemma_input_channel.h" #include "theory/theory.h" namespace CVC4 { @@ -42,40 +48,13 @@ 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 decision engine we are using */ - DecisionEngine* d_decisionEngine; - - /** The theory engine we are using */ - TheoryEngine* d_theoryEngine; - - /** Queue of asserted facts */ - context::CDQueue<TNode> d_queue; - - /** - * Set of all lemmas that have been "shared" in the portfolio---i.e., - * all imported and exported lemmas. - */ - std::hash_set<Node, NodeHashFunction> d_shared; - - /** - * Statistic: the number of replayed decisions (via --replay). - */ - KEEP_STATISTIC(IntStat, d_replayedDecisions, - "prop::theoryproxy::replayedDecisions", 0); - public: TheoryProxy(PropEngine* propEngine, TheoryEngine* theoryEngine, DecisionEngine* decisionEngine, context::Context* context, - CnfStream* cnfStream); + CnfStream* cnfStream, + SmtGlobals* globals); ~TheoryProxy(); @@ -117,25 +96,50 @@ public: SatValue getDecisionPolarity(SatVariable var); -};/* class SatSolver */ + private: + /** The prop engine we are using. */ + PropEngine* d_propEngine; -/* Functions that delegate to the concrete SAT solver. */ - -inline TheoryProxy::TheoryProxy(PropEngine* propEngine, - TheoryEngine* theoryEngine, - DecisionEngine* decisionEngine, - context::Context* context, - CnfStream* cnfStream) : - d_propEngine(propEngine), - d_cnfStream(cnfStream), - d_decisionEngine(decisionEngine), - d_theoryEngine(theoryEngine), - d_queue(context) -{} - -inline TheoryProxy::~TheoryProxy() { - /* nothing to do for now */ -} + /** The CNF engine we are using. */ + CnfStream* d_cnfStream; + + /** The decision engine we are using. */ + DecisionEngine* d_decisionEngine; + + /** The theory engine we are using. */ + TheoryEngine* d_theoryEngine; + + + /** + * Container for inputChannel, outputChannel, replayLog, and + * replayStream. + */ + SmtGlobals* d_globals; + + /** The lemma input channel we are using. */ + LemmaInputChannel* inputChannel(); + + /** The lemma output channel we are using. */ + LemmaOutputChannel* outputChannel(); + + std::ostream* replayLog(); + ExprStream* replayStream(); + + /** Queue of asserted facts */ + context::CDQueue<TNode> d_queue; + + /** + * Set of all lemmas that have been "shared" in the portfolio---i.e., + * all imported and exported lemmas. + */ + std::hash_set<Node, NodeHashFunction> d_shared; + + /** + * Statistic: the number of replayed decisions (via --replay). + */ + KEEP_STATISTIC(IntStat, d_replayedDecisions, + "prop::theoryproxy::replayedDecisions", 0); +};/* class SatSolver */ }/* CVC4::prop namespace */ |