1 files changed, 37 insertions, 25 deletions

diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
index e54e1fc3c..4cf057840 100644
--- a/src/decision/decision_engine.h
+++ b/src/decision/decision_engine.h
@@ -18,20 +18,12 @@
 #ifndef CVC5__DECISION__DECISION_ENGINE_H
 #define CVC5__DECISION__DECISION_ENGINE_H
 
-#include "decision/justification_strategy.h"
 #include "expr/node.h"
 #include "prop/cnf_stream.h"
 #include "prop/sat_solver.h"
 #include "prop/sat_solver_types.h"
 
 namespace cvc5 {
-
-namespace prop {
-class SkolemDefManager;
-}
-
-class DecisionEngineOld;
-
 namespace decision {
 
 class DecisionEngine
@@ -39,48 +31,68 @@ class DecisionEngine
  public:
   /** Constructor */
   DecisionEngine(context::Context* sc,
-                 context::UserContext* uc,
-                 prop::SkolemDefManager* skdm,
                  ResourceManager* rm);
+  virtual ~DecisionEngine() {}
 
   /** Finish initialize */
   void finishInit(prop::CDCLTSatSolverInterface* ss, prop::CnfStream* cs);
 
   /** Presolve, called at the beginning of each check-sat call */
-  void presolve();
+  virtual void presolve() {}
 
-  /** Gets the next decision based on strategies that are enabled */
+  /**
+   * Gets the next decision based on strategies that are enabled. This sets
+   * stopSearch to true if no further SAT variables need to be assigned in
+   * this SAT context.
+   */
   prop::SatLiteral getNext(bool& stopSearch);
 
   /** Is the DecisionEngine in a state where it has solved everything? */
-  bool isDone();
+  virtual bool isDone() = 0;
 
   /**
    * Notify this class that assertion is an (input) assertion, not corresponding
    * to a skolem definition.
    */
-  void addAssertion(TNode assertion);
+  virtual void addAssertion(TNode assertion) = 0;
   /**
-   * !!!! temporary until the old justification implementation is deleted.
-   * Notify this class  that lem is the skolem definition for skolem, which is
+   * Notify this class that lem is the skolem definition for skolem, which is
    * a part of the current assertions.
    */
-  void addSkolemDefinition(TNode lem, TNode skolem);
+  virtual void addSkolemDefinition(TNode lem, TNode skolem) = 0;
   /**
    * Notify this class that the literal n has been asserted, possibly
    * propagated by the SAT solver.
    */
-  void notifyAsserted(TNode n);
+  virtual void notifyAsserted(TNode n) {}
 
- private:
-  /** The old implementation */
-  std::unique_ptr<DecisionEngineOld> d_decEngineOld;
-  /** The new implementation */
-  std::unique_ptr<JustificationStrategy> d_jstrat;
+ protected:
+  /** Get next internal, the engine-specific implementation of getNext */
+  virtual prop::SatLiteral getNextInternal(bool& stopSearch) = 0;
+  /** Pointer to the SAT context */
+  context::Context* d_context;
   /** Pointer to resource manager for associated SmtEngine */
   ResourceManager* d_resourceManager;
-  /** using old implementation? */
-  bool d_useOld;
+  /** Pointer to the CNF stream */
+  prop::CnfStream* d_cnfStream;
+  /** Pointer to the SAT solver */
+  prop::CDCLTSatSolverInterface* d_satSolver;
+};
+
+/**
+ * Instance of the above class which does nothing. This is used when
+ * the decision mode is set to internal.
+ */
+class DecisionEngineEmpty : public DecisionEngine
+{
+ public:
+  DecisionEngineEmpty(context::Context* sc, ResourceManager* rm);
+  bool isDone() override;
+  void addAssertion(TNode assertion) override;
+  void addSkolemDefinition(TNode lem, TNode skolem) override;
+
+ protected:
+  prop::SatLiteral getNextInternal(bool& stopSearch) override;
 };
 
 }  // namespace decision