diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 76 |
1 files changed, 4 insertions, 72 deletions
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); } |