diff options
Diffstat (limited to 'src/prop/prop_engine.cpp')
| -rw-r--r-- | src/prop/prop_engine.cpp | 20 |
1 files changed, 3 insertions, 17 deletions
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 2436aed04..89b919109 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -44,13 +44,6 @@ 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 { @@ -76,9 +69,7 @@ public: PropEngine::PropEngine(TheoryEngine* te, Context* satContext, - UserContext* userContext, - std::ostream* replayLog, - ExprStream* replayStream) + UserContext* userContext) : d_inCheckSat(false), d_theoryEngine(te), d_context(satContext), @@ -101,13 +92,8 @@ PropEngine::PropEngine(TheoryEngine* te, d_cnfStream = new CVC4::prop::TseitinCnfStream( d_satSolver, d_registrar, userContext, true); - d_theoryProxy = new TheoryProxy(this, - d_theoryEngine, - d_decisionEngine.get(), - d_context, - d_cnfStream, - replayLog, - replayStream); + d_theoryProxy = new TheoryProxy( + this, d_theoryEngine, d_decisionEngine.get(), d_context, d_cnfStream); d_satSolver->initialize(d_context, d_theoryProxy); d_decisionEngine->setSatSolver(d_satSolver); |