diff options
author | Tim King <taking@google.com> | 2016-01-28 12:35:45 -0800 |
---|---|---|
committer | Tim King <taking@google.com> | 2016-01-28 12:35:45 -0800 |
commit | 2ba8bb701ce289ba60afec01b653b0930cc59298 (patch) | |
tree | 46df365b7b41ce662a0f94de5b11c3ed20829851 /src/prop | |
parent | 42b665f2a00643c81b42932fab1441987628c5a5 (diff) |
Adding listeners to Options.
- Options
-- Added the new option attribute :notify. One can get a notify() call on the Listener after a the option's value is updated. This is the new preferred way to achieve dynamic dispatch for options.
-- Removed SmtOptionsHandler and pushed its functionality into OptionsHandler and Listeners.
-- Added functions to Options for registering listeners of the notify calls.
-- Changed a number of options to use the new listener infrastructure.
-- Fixed a number of warnings in options.
-- Added the ArgumentExtender class to better capture how arguments are inserted while parsing options and ease memory management. Previously this was the "preemptGetopt" procedure.
-- Moved options/options_handler_interface.{cpp,h} to options/options_handler.{cpp,h}.
- Theories
-- Reimplemented alternative theories to use a datastructure stored on TheoryEngine instead of on Options.
- Ostream Handling:
-- Added new functionality that generalized how ostreams are opened, options/open_stream.h.
-- Simplified the memory management for different ostreams, smt/managed_ostreams.h.
-- Had the SmtEnginePrivate manage the memory for the ostreams set by options.
-- Simplified how the setting of ostreams are updated, smt/update_ostream.h.
- Configuration and Tags:
-- Configuration can now be used during predicates and handlers for options.
-- Moved configuration.{cpp,h,i} and configuration_private.h from util/ into base/.
-- Moved {Debug,Trace}_tags.* from being generated in options/ into base/.
- cvc4_private.h
-- Upgraded #warning's in cvc4_private.h and cvc4_private_library.h to #error's.
-- Added public first-order (non-templatized) member functions for options get and set the value of options outside of libcvc4. Fixed all of the use locations.
-- Made lib/lib/clock_gettime.h a cvc4_private_library.h header.
- Antlr
-- Fixed antlr and cvc4 macro definition conflicts that caused warnings.
- SmtGlobals
-- Refactored replayStream and replayLog out of SmtGlobals.
-- Renamed SmtGlobals to LemmaChannels and moved the implementation into smt_util/lemma_channels.{h,cpp}.
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/bvminisat/bvminisat.h | 2 | ||||
-rw-r--r-- | src/prop/cnf_stream.cpp | 21 | ||||
-rw-r--r-- | src/prop/cnf_stream.h | 10 | ||||
-rw-r--r-- | src/prop/prop_engine.cpp | 24 | ||||
-rw-r--r-- | src/prop/prop_engine.h | 12 | ||||
-rw-r--r-- | src/prop/theory_proxy.cpp | 28 | ||||
-rw-r--r-- | src/prop/theory_proxy.h | 25 |
7 files changed, 59 insertions, 63 deletions
diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h index 383948e3e..ec8c3455a 100644 --- a/src/prop/bvminisat/bvminisat.h +++ b/src/prop/bvminisat/bvminisat.h @@ -122,7 +122,7 @@ public: private: /* Disable the default constructor. */ - BVMinisatSatSolver() CVC4_UNUSED; + BVMinisatSatSolver() CVC4_UNDEFINED; class Statistics { public: diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index a3d411738..1cd32bee8 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -37,18 +37,12 @@ using namespace std; using namespace CVC4::kind; -#ifdef CVC4_REPLAY -# define CVC4_USE_REPLAY true -#else /* CVC4_REPLAY */ -# define CVC4_USE_REPLAY false -#endif /* CVC4_REPLAY */ - namespace CVC4 { namespace prop { CnfStream::CnfStream(SatSolver* satSolver, Registrar* registrar, - context::Context* context, SmtGlobals* globals, - bool fullLitToNodeMap, std::string name) + context::Context* context, bool fullLitToNodeMap, + std::string name) : d_satSolver(satSolver), d_booleanVariables(context), d_nodeToLiteralMap(context), @@ -58,15 +52,13 @@ CnfStream::CnfStream(SatSolver* satSolver, Registrar* registrar, d_registrar(registrar), d_name(name), d_cnfProof(NULL), - d_globals(globals), d_removable(false) { } TseitinCnfStream::TseitinCnfStream(SatSolver* satSolver, Registrar* registrar, context::Context* context, - SmtGlobals* globals, bool fullLitToNodeMap, - std::string name) - : CnfStream(satSolver, registrar, context, globals, fullLitToNodeMap, name) + bool fullLitToNodeMap, std::string name) + : CnfStream(satSolver, registrar, context, fullLitToNodeMap, name) {} void CnfStream::assertClause(TNode node, SatClause& c) { @@ -200,10 +192,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 && d_globals->getReplayLog() != NULL ) || - (Dump.isOn("clauses")) ) { - + if ( isTheoryAtom || d_fullLitToNodeMap || (Dump.isOn("clauses")) ) { d_literalToNodeMap.insert_safe(lit, node); d_literalToNodeMap.insert_safe(~lit, node.notNode()); } diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index a07944a58..a6b6781ca 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -33,7 +33,7 @@ #include "proof/proof_manager.h" #include "prop/registrar.h" #include "prop/theory_proxy.h" -#include "smt/smt_globals.h" +#include "smt_util/lemma_channels.h" namespace CVC4 { namespace prop { @@ -90,9 +90,6 @@ protected: /** Pointer to the proof corresponding to this CnfStream */ CnfProof* d_cnfProof; - /** Container for misc. globals. */ - SmtGlobals* d_globals; - /** * How many literals were already mapped at the top-level when we * tried to convertAndAssert() something. This @@ -194,7 +191,6 @@ public: CnfStream(SatSolver* satSolver, Registrar* registrar, context::Context* context, - SmtGlobals* globals, bool fullLitToNodeMap = false, std::string name=""); @@ -291,7 +287,9 @@ public: * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping, * even for non-theory literals */ - TseitinCnfStream(SatSolver* satSolver, Registrar* registrar, context::Context* context, SmtGlobals* globals, bool fullLitToNodeMap = false, std::string name = ""); + TseitinCnfStream(SatSolver* satSolver, Registrar* registrar, + context::Context* context, bool fullLitToNodeMap = false, + std::string name = ""); private: diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 593c522a8..36d6408b5 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -45,6 +45,13 @@ using namespace std; using namespace CVC4::context; + +#ifdef CVC4_REPLAY +# define CVC4_USE_REPLAY true +#else /* CVC4_REPLAY */ +# define CVC4_USE_REPLAY false +#endif /* CVC4_REPLAY */ + namespace CVC4 { namespace prop { @@ -68,7 +75,9 @@ public: } }; -PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext, Context* userContext, SmtGlobals* globals) : +PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext, + Context* userContext, std::ostream* replayLog, + ExprStream* replayStream, LemmaChannels* channels) : d_inCheckSat(false), d_theoryEngine(te), d_decisionEngine(de), @@ -78,8 +87,7 @@ PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext d_registrar(NULL), d_cnfStream(NULL), d_interrupted(false), - d_resourceManager(NodeManager::currentResourceManager()), - d_globals(globals) + d_resourceManager(NodeManager::currentResourceManager()) { Debug("prop") << "Constructing the PropEngine" << endl; @@ -88,13 +96,15 @@ 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_globals, + (d_satSolver, d_registrar, userContext, // fullLitToNode Map = options::threads() > 1 || - options::decisionMode() == decision::DECISION_STRATEGY_RELEVANCY - ); + options::decisionMode() == decision::DECISION_STRATEGY_RELEVANCY || + ( CVC4_USE_REPLAY && replayLog != NULL )); - d_theoryProxy = new TheoryProxy(this, d_theoryEngine, d_decisionEngine, d_context, d_cnfStream, d_globals); + d_theoryProxy = new TheoryProxy( + this, d_theoryEngine, d_decisionEngine, d_context, d_cnfStream, replayLog, + replayStream, channels); 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 dfa84ef14..a71d4832d 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -24,12 +24,13 @@ #include <sys/time.h> #include "base/modal_exception.h" +#include "expr/expr_stream.h" #include "expr/node.h" #include "options/options.h" #include "proof/proof_manager.h" -#include "smt/smt_globals.h" -#include "util/unsafe_interrupt_exception.h" +#include "smt_util/lemma_channels.h" #include "util/result.h" +#include "util/unsafe_interrupt_exception.h" namespace CVC4 { @@ -92,15 +93,14 @@ 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, SmtGlobals* global); + PropEngine(TheoryEngine*, DecisionEngine*, context::Context* satContext, + context::Context* userContext, std::ostream* replayLog, + ExprStream* replayStream, LemmaChannels* channels); /** * Destructor. diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 5304691a6..5de97d0d8 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -39,12 +39,16 @@ TheoryProxy::TheoryProxy(PropEngine* propEngine, DecisionEngine* decisionEngine, context::Context* context, CnfStream* cnfStream, - SmtGlobals* globals) + std::ostream* replayLog, + ExprStream* replayStream, + LemmaChannels* channels) : d_propEngine(propEngine), d_cnfStream(cnfStream), d_decisionEngine(decisionEngine), d_theoryEngine(theoryEngine), - d_globals(globals), + d_channels(channels), + d_replayLog(replayLog), + d_replayStream(replayStream), d_queue(context), d_replayedDecisions("prop::theoryproxy::replayedDecisions", 0) { @@ -58,20 +62,12 @@ TheoryProxy::~TheoryProxy() { /** The lemma input channel we are using. */ LemmaInputChannel* TheoryProxy::inputChannel() { - return d_globals->getLemmaInputChannel(); + return d_channels->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(); + return d_channels->getLemmaOutputChannel(); } @@ -203,8 +199,8 @@ void TheoryProxy::notifyNewLemma(SatClause& lemma) { SatLiteral TheoryProxy::getNextReplayDecision() { #ifdef CVC4_REPLAY - if(replayStream() != NULL) { - Expr e = replayStream()->nextExpr(); + if(d_replayStream != NULL) { + Expr e = d_replayStream->nextExpr(); if(!e.isNull()) { // we get null node when out of decisions to replay // convert & return ++d_replayedDecisions; @@ -217,9 +213,9 @@ SatLiteral TheoryProxy::getNextReplayDecision() { void TheoryProxy::logDecision(SatLiteral lit) { #ifdef CVC4_REPLAY - if(replayLog() != NULL) { + if(d_replayLog != NULL) { Assert(lit != undefSatLiteral, "logging an `undef' decision ?!"); - (*replayLog()) << d_cnfStream->getNode(lit) << std::endl; + (*d_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 261db8c87..acc242ab6 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -26,11 +26,12 @@ #include <iosfwd> #include "context/cdqueue.h" +#include "expr/expr_stream.h" #include "expr/node.h" #include "prop/sat_solver.h" -#include "smt/smt_globals.h" -#include "smt_util/lemma_output_channel.h" +#include "smt_util/lemma_channels.h" #include "smt_util/lemma_input_channel.h" +#include "smt_util/lemma_output_channel.h" #include "theory/theory.h" #include "util/statistics_registry.h" @@ -54,7 +55,9 @@ public: DecisionEngine* decisionEngine, context::Context* context, CnfStream* cnfStream, - SmtGlobals* globals); + std::ostream* replayLog, + ExprStream* replayStream, + LemmaChannels* globals); ~TheoryProxy(); @@ -110,11 +113,14 @@ public: TheoryEngine* d_theoryEngine; - /** - * Container for inputChannel, outputChannel, replayLog, and - * replayStream. - */ - SmtGlobals* d_globals; + /** Container for inputChannel() and outputChannel(). */ + LemmaChannels* d_channels; + + /** Stream on which to log replay events. */ + std::ostream* d_replayLog; + + /** Stream for replaying decisions. */ + ExprStream* d_replayStream; /** The lemma input channel we are using. */ LemmaInputChannel* inputChannel(); @@ -122,9 +128,6 @@ public: /** The lemma output channel we are using. */ LemmaOutputChannel* outputChannel(); - std::ostream* replayLog(); - ExprStream* replayStream(); - /** Queue of asserted facts */ context::CDQueue<TNode> d_queue; |