Move current decision engine to decision engine old (#6466)

The decision engine is the class that contains strategies for doing e.g. justification heuristic.

The current implementation is hardcoded for the old implementation of justification heuristic.

Since both implementations will be maintained in the short term, this splits the parts of DecisionEngine that are specific to the old implementation to a class DecisionEngineOld.

It refactors the interface of DecisionEngine in a way that is compatible with both implementations.

1 files changed, 10 insertions, 5 deletions

diff --git a/src/decision/decision_strategy.h b/src/decision/decision_strategy.h
index 0376b00cc..87c463c29 100644
--- a/src/decision/decision_strategy.h
+++ b/src/decision/decision_strategy.h
@@ -26,6 +26,8 @@
 
 namespace cvc5 {
 
+class DecisionEngineOld;
+
 namespace context {
   class Context;
   }  // namespace context
@@ -36,10 +38,12 @@ class DecisionEngine;
 
 class DecisionStrategy {
 protected:
-  DecisionEngine* d_decisionEngine;
+ DecisionEngineOld* d_decisionEngine;
+
 public:
-  DecisionStrategy(DecisionEngine* de, context::Context *c) :
-    d_decisionEngine(de) {
+ DecisionStrategy(DecisionEngineOld* de, context::Context* c)
+     : d_decisionEngine(de)
+ {
   }
 
   virtual ~DecisionStrategy() { }
@@ -49,8 +53,9 @@ public:
 
 class ITEDecisionStrategy : public DecisionStrategy {
 public:
-  ITEDecisionStrategy(DecisionEngine* de, context::Context *c) :
-    DecisionStrategy(de, c) {
+ ITEDecisionStrategy(DecisionEngineOld* de, context::Context* c)
+     : DecisionStrategy(de, c)
+ {
   }
   /**
    * Add that assertion is an (input) assertion, not corresponding to a