diff options
Diffstat (limited to 'src/prop/theory_proxy.h')
-rw-r--r-- | src/prop/theory_proxy.h | 25 |
1 files changed, 14 insertions, 11 deletions
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index 261db8c87..acc242ab6 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -26,11 +26,12 @@ #include <iosfwd> #include "context/cdqueue.h" +#include "expr/expr_stream.h" #include "expr/node.h" #include "prop/sat_solver.h" -#include "smt/smt_globals.h" -#include "smt_util/lemma_output_channel.h" +#include "smt_util/lemma_channels.h" #include "smt_util/lemma_input_channel.h" +#include "smt_util/lemma_output_channel.h" #include "theory/theory.h" #include "util/statistics_registry.h" @@ -54,7 +55,9 @@ public: DecisionEngine* decisionEngine, context::Context* context, CnfStream* cnfStream, - SmtGlobals* globals); + std::ostream* replayLog, + ExprStream* replayStream, + LemmaChannels* globals); ~TheoryProxy(); @@ -110,11 +113,14 @@ public: TheoryEngine* d_theoryEngine; - /** - * Container for inputChannel, outputChannel, replayLog, and - * replayStream. - */ - SmtGlobals* d_globals; + /** Container for inputChannel() and outputChannel(). */ + LemmaChannels* d_channels; + + /** Stream on which to log replay events. */ + std::ostream* d_replayLog; + + /** Stream for replaying decisions. */ + ExprStream* d_replayStream; /** The lemma input channel we are using. */ LemmaInputChannel* inputChannel(); @@ -122,9 +128,6 @@ public: /** The lemma output channel we are using. */ LemmaOutputChannel* outputChannel(); - std::ostream* replayLog(); - ExprStream* replayStream(); - /** Queue of asserted facts */ context::CDQueue<TNode> d_queue; |