Move ownership of DecisionEngine into PropEngine. (#3850)

This is in preparation of fixing the issue we currently have with reset-assertions.

This also removes a competition hack for QF_LRA.

2 files changed, 3 insertions, 12 deletions

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index a39c014a6..60ad00fc5 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -315,7 +315,6 @@ TheoryEngine::TheoryEngine(context::Context* context,
                            RemoveTermFormulas& iteRemover,
                            const LogicInfo& logicInfo)
     : d_propEngine(nullptr),
-      d_decisionEngine(nullptr),
       d_context(context),
       d_userContext(userContext),
       d_logicInfo(logicInfo),
@@ -1924,8 +1923,9 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
   }
 
   // assert to decision engine
-  if(!removable) {
-    d_decisionEngine->addAssertions(additionalLemmas);
+  if (!removable)
+  {
+    d_propEngine->addAssertionsToDecisionEngine(additionalLemmas);
   }
 
   // Mark that we added some lemmas
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 1757d7a6d..e8223f1a1 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -101,7 +101,6 @@ namespace theory {
   class EntailmentCheckSideEffects;
 }/* CVC4::theory namespace */
 
-class DecisionEngine;
 class RemoveTermFormulas;
 
 /**
@@ -119,9 +118,6 @@ class TheoryEngine {
   /** Associated PropEngine engine */
   prop::PropEngine* d_propEngine;
 
-  /** Access to decision engine */
-  DecisionEngine* d_decisionEngine;
-
   /** Our context */
   context::Context* d_context;
 
@@ -505,11 +501,6 @@ class TheoryEngine {
     d_propEngine = propEngine;
   }
 
-  inline void setDecisionEngine(DecisionEngine* decisionEngine) {
-    Assert(d_decisionEngine == NULL);
-    d_decisionEngine = decisionEngine;
-  }
-
   /** Called when all initialization of options/logic is done */
   void finishInit();