diff options
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/managed_ostreams.cpp | 27 | ||||
-rw-r--r-- | src/smt/managed_ostreams.h | 21 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 76 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 11 |
4 files changed, 4 insertions, 131 deletions
diff --git a/src/smt/managed_ostreams.cpp b/src/smt/managed_ostreams.cpp index a73ec44f4..7615325b7 100644 --- a/src/smt/managed_ostreams.cpp +++ b/src/smt/managed_ostreams.cpp @@ -163,31 +163,4 @@ void ManagedDiagnosticOutputChannel::addSpecialCases(OstreamOpener* opener) opener->addSpecialCase("stderr", &std::cerr); } - -ManagedReplayLogOstream::ManagedReplayLogOstream() : d_replayLog(NULL) {} -ManagedReplayLogOstream::~ManagedReplayLogOstream(){ - if(d_replayLog != NULL) { - (*d_replayLog) << std::flush; - } -} - -std::string ManagedReplayLogOstream::defaultSource() const { - return options::replayLogFilename(); -} - -void ManagedReplayLogOstream::initialize(std::ostream* outStream) { - if(outStream != NULL){ - *outStream << language::SetLanguage(options::outputLanguage()) - << expr::ExprSetDepth(-1); - } - /* Do this regardless of managing the memory. */ - d_replayLog = outStream; -} - -/** Adds special cases to an ostreamopener. */ -void ManagedReplayLogOstream::addSpecialCases(OstreamOpener* opener) const { - opener->addSpecialCase("-", &std::cout); -} - - }/* CVC4 namespace */ diff --git a/src/smt/managed_ostreams.h b/src/smt/managed_ostreams.h index f495f8e72..bc12bbe39 100644 --- a/src/smt/managed_ostreams.h +++ b/src/smt/managed_ostreams.h @@ -156,27 +156,6 @@ class ManagedDiagnosticOutputChannel : public ManagedOstream { void addSpecialCases(OstreamOpener* opener) const override; };/* class ManagedRegularOutputChannel */ -/** This controls the memory associated with replay-log. */ -class ManagedReplayLogOstream : public ManagedOstream { - public: - ManagedReplayLogOstream(); - ~ManagedReplayLogOstream(); - - std::ostream* getReplayLog() const { return d_replayLog; } - const char* getName() const override { return "replay-log"; } - std::string defaultSource() const override; - - protected: - /** Initializes an output stream. Not necessarily managed. */ - void initialize(std::ostream* outStream) override; - - /** Adds special cases to an ostreamopener. */ - void addSpecialCases(OstreamOpener* opener) const override; - - private: - std::ostream* d_replayLog; -};/* class ManagedRegularOutputChannel */ - }/* CVC4 namespace */ #endif /* CVC4__MANAGED_OSTREAMS_H */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 30c1cd0f5..10fc76bf7 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -294,40 +294,6 @@ class BeforeSearchListener : public Listener { SmtEngine* d_smt; }; /* class BeforeSearchListener */ -class UseTheoryListListener : public Listener { - public: - UseTheoryListListener(TheoryEngine* theoryEngine) - : d_theoryEngine(theoryEngine) - {} - - void notify() override - { - std::stringstream commaList(options::useTheoryList()); - std::string token; - - Debug("UseTheoryListListener") << "UseTheoryListListener::notify() " - << options::useTheoryList() << std::endl; - - while(std::getline(commaList, token, ',')){ - if(token == "help") { - puts(theory::useTheoryHelp); - exit(1); - } - if(theory::useTheoryValidate(token)) { - d_theoryEngine->enableTheoryAlternative(token); - } else { - throw OptionException( - std::string("unknown option for --use-theory : `") + token + - "'. Try --use-theory=help."); - } - } - } - - private: - TheoryEngine* d_theoryEngine; -}; /* class UseTheoryListListener */ - - class SetDefaultExprDepthListener : public Listener { public: void notify() override @@ -433,15 +399,11 @@ class SmtEnginePrivate : public NodeManagerListener { /** Manager for the memory of --dump-to. */ ManagedDumpOStream d_managedDumpChannel; - /** Manager for --replay-log. */ - ManagedReplayLogOstream d_managedReplayLog; - /** * This list contains: * softResourceOut * hardResourceOut * beforeSearchListener - * UseTheoryListListener * * This needs to be deleted before both NodeManager's Options, * SmtEngine, d_resourceManager, and TheoryEngine. @@ -554,7 +516,6 @@ class SmtEnginePrivate : public NodeManagerListener { d_managedRegularChannel(), d_managedDiagnosticChannel(), d_managedDumpChannel(), - d_managedReplayLog(), d_listenerRegistrations(new ListenerRegistrationList()), d_propagator(true, true), d_assertions(), @@ -618,9 +579,6 @@ class SmtEnginePrivate : public NodeManagerListener { d_listenerRegistrations->add( nodeManagerOptions.registerDumpToFileNameListener( new SetToDefaultSourceListener(&d_managedDumpChannel), true)); - d_listenerRegistrations->add( - nodeManagerOptions.registerSetReplayLogFilename( - new SetToDefaultSourceListener(&d_managedReplayLog), true)); } catch (OptionException& e) { @@ -814,17 +772,6 @@ class SmtEnginePrivate : public NodeManagerListener { return retval; } - void addUseTheoryListListener(TheoryEngine* theoryEngine){ - Options& nodeManagerOptions = NodeManager::currentNM()->getOptions(); - d_listenerRegistrations->add( - nodeManagerOptions.registerUseTheoryListListener( - new UseTheoryListListener(theoryEngine), true)); - } - - std::ostream* getReplayLog() const { - return d_managedReplayLog.getReplayLog(); - } - //------------------------------- expression names // implements setExpressionName, as described in smt_engine.h void setExpressionName(Expr e, std::string name) { @@ -874,7 +821,6 @@ SmtEngine::SmtEngine(ExprManager* em) d_status(), d_expectedStatus(), d_smtMode(SMT_MODE_START), - d_replayStream(nullptr), d_private(nullptr), d_statisticsRegistry(nullptr), d_stats(nullptr) @@ -923,8 +869,6 @@ void SmtEngine::finishInit() #endif } - d_private->addUseTheoryListListener(getTheoryEngine()); - // set the random seed Random::getRandom().setSeed(options::seed()); @@ -938,11 +882,8 @@ void SmtEngine::finishInit() * are unregistered by the obsolete PropEngine object before registered * again by the new PropEngine object */ d_propEngine.reset(nullptr); - d_propEngine.reset(new PropEngine(getTheoryEngine(), - getContext(), - getUserContext(), - d_private->getReplayLog(), - d_replayStream)); + d_propEngine.reset( + new PropEngine(getTheoryEngine(), getContext(), getUserContext())); Trace("smt-debug") << "Setting up theory engine..." << std::endl; d_theoryEngine->setPropEngine(getPropEngine()); @@ -4337,11 +4278,8 @@ void SmtEngine::resetAssertions() * statistics are unregistered by the obsolete PropEngine object before * registered again by the new PropEngine object */ d_propEngine.reset(nullptr); - d_propEngine.reset(new PropEngine(getTheoryEngine(), - getContext(), - getUserContext(), - d_private->getReplayLog(), - d_replayStream)); + d_propEngine.reset( + new PropEngine(getTheoryEngine(), getContext(), getUserContext())); d_theoryEngine->setPropEngine(getPropEngine()); } @@ -4534,12 +4472,6 @@ CVC4::SExpr SmtEngine::getOption(const std::string& key) const return SExpr::parseAtom(nodeManagerOptions.getOption(key)); } -void SmtEngine::setReplayStream(ExprStream* replayStream) { - AlwaysAssert(!d_fullyInited) - << "Cannot set replay stream once fully initialized"; - d_replayStream = replayStream; -} - bool SmtEngine::getExpressionName(Expr e, std::string& name) const { return d_private->getExpressionName(e, name); } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index f5abda1b0..2cb227fc9 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -28,7 +28,6 @@ #include "context/cdlist_forward.h" #include "expr/expr.h" #include "expr/expr_manager.h" -#include "expr/expr_stream.h" #include "options/options.h" #include "proof/unsat_core.h" #include "smt/logic_exception.h" @@ -800,13 +799,6 @@ class CVC4_PUBLIC SmtEngine void beforeSearch(); /** - * Expermintal feature: Sets the sequence of decisions. - * This currently requires very fine grained knowledge about literal - * translation. - */ - void setReplayStream(ExprStream* exprStream); - - /** * Get expression name. * * Return true if given expressoion has a name in the current context. @@ -1243,9 +1235,6 @@ class CVC4_PUBLIC SmtEngine */ std::map<std::string, Integer> d_commandVerbosity; - /** ReplayStream for the solver. */ - ExprStream* d_replayStream; - /** * A private utility class to SmtEngine. */ |