From df5f7fe03fda041429548bcb39abb8916ca2e291 Mon Sep 17 00:00:00 2001 From: Dejan Jovanović Date: Tue, 9 Nov 2010 21:57:06 +0000 Subject: Lemmas on demand work, push-pop, some cleanup. --- src/prop/prop_engine.h | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) (limited to 'src/prop/prop_engine.h') diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index ecef29ac2..b43c2d859 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -24,7 +24,6 @@ #define __CVC4__PROP_ENGINE_H #include "expr/node.h" -#include "util/decision_engine.h" #include "util/options.h" #include "util/result.h" @@ -52,9 +51,6 @@ class PropEngine { /** The global options */ //const Options d_options; - /** The decision engine we will be using */ - DecisionEngine *d_decisionEngine; - /** The theory engine we will be using */ TheoryEngine *d_theoryEngine; @@ -76,7 +72,7 @@ public: /** * Create a PropEngine with a particular decision and theory engine. */ - PropEngine(DecisionEngine*, TheoryEngine*, context::Context*, const Options&); + PropEngine(TheoryEngine*, context::Context*, const Options&); /** * Destructor. -- cgit v1.2.3