diff options
Diffstat (limited to 'src/prop/theory_proxy.h')
-rw-r--r-- | src/prop/theory_proxy.h | 20 |
1 files changed, 1 insertions, 19 deletions
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index 0d76b473f..089d2082d 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -27,7 +27,6 @@ #include <unordered_set> #include "context/cdqueue.h" -#include "expr/expr_stream.h" #include "expr/node.h" #include "prop/sat_solver.h" #include "theory/theory.h" @@ -54,9 +53,7 @@ class TheoryProxy TheoryEngine* theoryEngine, DecisionEngine* decisionEngine, context::Context* context, - CnfStream* cnfStream, - std::ostream* replayLog, - ExprStream* replayStream); + CnfStream* cnfStream); ~TheoryProxy(); @@ -83,10 +80,6 @@ class TheoryProxy void notifyRestart(); - SatLiteral getNextReplayDecision(); - - void logDecision(SatLiteral lit); - void spendResource(ResourceManager::Resource r); bool isDecisionEngineDone(); @@ -111,12 +104,6 @@ class TheoryProxy /** The theory engine we are using. */ TheoryEngine* d_theoryEngine; - /** Stream on which to log replay events. */ - std::ostream* d_replayLog; - - /** Stream for replaying decisions. */ - ExprStream* d_replayStream; - /** Queue of asserted facts */ context::CDQueue<TNode> d_queue; @@ -126,11 +113,6 @@ class TheoryProxy */ std::unordered_set<Node, NodeHashFunction> d_shared; - /** - * Statistic: the number of replayed decisions (via --replay). - */ - IntStat d_replayedDecisions; - }; /* class SatSolver */ }/* CVC4::prop namespace */ |