diff options
Diffstat (limited to 'src/prop/prop_engine.h')
| -rw-r--r-- | src/prop/prop_engine.h | 12 |
1 files changed, 6 insertions, 6 deletions
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. |