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.

1 files changed, 9 insertions, 3 deletions

diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 061fbbca6..707244ff5 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -27,6 +27,7 @@
 #include "expr/expr_stream.h"
 #include "expr/node.h"
 #include "options/options.h"
+#include "preprocessing/assertion_pipeline.h"
 #include "proof/proof_manager.h"
 #include "util/resource_manager.h"
 #include "util/result.h"
@@ -60,9 +61,8 @@ class PropEngine
    * Create a PropEngine with a particular decision and theory engine.
    */
   PropEngine(TheoryEngine*,
-             DecisionEngine*,
              context::Context* satContext,
-             context::Context* userContext,
+             context::UserContext* userContext,
              std::ostream* replayLog,
              ExprStream* replayStream);
 
@@ -105,6 +105,12 @@ class PropEngine
                    TNode from = TNode::null());
 
   /**
+   * Pass a list of assertions from an AssertionPipeline to the decision engine.
+   */
+  void addAssertionsToDecisionEngine(
+      const preprocessing::AssertionPipeline& assertions);
+
+  /**
    * If ever n is decided upon, it must be in the given phase.  This
    * occurs *globally*, i.e., even if the literal is untranslated by
    * user pop and retranslated, it keeps this phase.  The associated
@@ -223,7 +229,7 @@ class PropEngine
   TheoryEngine* d_theoryEngine;
 
   /** The decision engine we will be using */
-  DecisionEngine* d_decisionEngine;
+  std::unique_ptr<DecisionEngine> d_decisionEngine;
 
   /** The context */
   context::Context* d_context;