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, 96 insertions, 0 deletions

diff --git a/src/decision/decision_engine_old.cpp b/src/decision/decision_engine_old.cpp
new file mode 100644
index 000000000..8ef7ad1f4
--- /dev/null
+++ b/src/decision/decision_engine_old.cpp
@@ -0,0 +1,96 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Kshitij Bansal, Aina Niemetz, Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Old implementation of the decision engine
+ */
+#include "decision/decision_engine_old.h"
+
+#include "decision/decision_attributes.h"
+#include "decision/justification_heuristic.h"
+#include "expr/node.h"
+#include "options/decision_options.h"
+#include "options/smt_options.h"
+#include "util/resource_manager.h"
+
+using namespace std;
+
+namespace cvc5 {
+
+DecisionEngineOld::DecisionEngineOld(context::Context* sc,
+                                     context::UserContext* uc)
+    : d_cnfStream(nullptr),
+      d_satSolver(nullptr),
+      d_satContext(sc),
+      d_userContext(uc),
+      d_result(sc, SAT_VALUE_UNKNOWN),
+      d_engineState(0),
+      d_enabledITEStrategy(nullptr)
+{
+  Trace("decision") << "Creating decision engine" << std::endl;
+  Assert(d_engineState == 0);
+  d_engineState = 1;
+
+  Trace("decision-init") << "DecisionEngineOld::init()" << std::endl;
+  Trace("decision-init") << " * options->decisionMode: "
+                         << options::decisionMode() << std::endl;
+  Trace("decision-init") << " * options->decisionStopOnly: "
+                         << options::decisionStopOnly() << std::endl;
+
+  if (options::decisionMode() == options::DecisionMode::JUSTIFICATION)
+  {
+    d_enabledITEStrategy.reset(new decision::JustificationHeuristic(
+        this, d_userContext, d_satContext));
+  }
+}
+
+void DecisionEngineOld::shutdown()
+{
+  Trace("decision") << "Shutting down decision engine" << std::endl;
+
+  Assert(d_engineState == 1);
+  d_engineState = 2;
+  d_enabledITEStrategy.reset(nullptr);
+}
+
+SatLiteral DecisionEngineOld::getNext(bool& stopSearch)
+{
+  Assert(d_cnfStream != nullptr)
+      << "Forgot to set cnfStream for decision engine?";
+  Assert(d_satSolver != nullptr)
+      << "Forgot to set satSolver for decision engine?";
+
+  return d_enabledITEStrategy == nullptr
+             ? undefSatLiteral
+             : d_enabledITEStrategy->getNext(stopSearch);
+}
+
+void DecisionEngineOld::addAssertion(TNode assertion)
+{
+  // new assertions, reset whatever result we knew
+  d_result = SAT_VALUE_UNKNOWN;
+  if (d_enabledITEStrategy != nullptr)
+  {
+    d_enabledITEStrategy->addAssertion(assertion);
+  }
+}
+
+void DecisionEngineOld::addSkolemDefinition(TNode lem, TNode skolem)
+{
+  // new assertions, reset whatever result we knew
+  d_result = SAT_VALUE_UNKNOWN;
+  if (d_enabledITEStrategy != nullptr)
+  {
+    d_enabledITEStrategy->addSkolemDefinition(lem, skolem);
+  }
+}
+
+}  // namespace cvc5