summaryrefslogtreecommitdiff
path: root/src/smt
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt')
-rw-r--r--src/smt/managed_ostreams.cpp27
-rw-r--r--src/smt/managed_ostreams.h21
-rw-r--r--src/smt/smt_engine.cpp76
-rw-r--r--src/smt/smt_engine.h11
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.
*/
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback