From ff91290122d478dc637fb3e9ff4fe4c0ead5bd32 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 9 Jul 2021 11:50:51 -0500
Subject: Implement stop-only for new justification heuristic (#6847)

This also refactors decision engine so that we use inheritance instead of a dummy flag + members to determine which implementation to use.
---
 src/decision/justification_strategy.cpp | 23 +++++++++++------------
 1 file changed, 11 insertions(+), 12 deletions(-)

(limited to 'src/decision/justification_strategy.cpp')

diff --git a/src/decision/justification_strategy.cpp b/src/decision/justification_strategy.cpp
index b73b24bd0..56d96b32f 100644
--- a/src/decision/justification_strategy.cpp
+++ b/src/decision/justification_strategy.cpp
@@ -25,10 +25,9 @@ namespace decision {
 
 JustificationStrategy::JustificationStrategy(context::Context* c,
                                              context::UserContext* u,
-                                             prop::SkolemDefManager* skdm)
-    : d_context(c),
-      d_cnfStream(nullptr),
-      d_satSolver(nullptr),
+                                             prop::SkolemDefManager* skdm,
+                                             ResourceManager* rm)
+    : DecisionEngine(c, rm),
       d_skdm(skdm),
       d_assertions(
           u,
@@ -40,18 +39,13 @@ JustificationStrategy::JustificationStrategy(context::Context* c,
       d_lastDecisionLit(c),
       d_currStatusDec(false),
       d_useRlvOrder(options::jhRlvOrder()),
+      d_decisionStopOnly(options::decisionMode()
+                         == options::DecisionMode::STOPONLY),
       d_jhSkMode(options::jhSkolemMode()),
       d_jhSkRlvMode(options::jhSkolemRlvMode())
 {
 }
 
-void JustificationStrategy::finishInit(CDCLTSatSolverInterface* ss,
-                                       CnfStream* cs)
-{
-  d_satSolver = ss;
-  d_cnfStream = cs;
-}
-
 void JustificationStrategy::presolve()
 {
   d_lastDecisionLit = Node::null();
@@ -64,7 +58,7 @@ void JustificationStrategy::presolve()
   d_stack.clear();
 }
 
-SatLiteral JustificationStrategy::getNext(bool& stopSearch)
+SatLiteral JustificationStrategy::getNextInternal(bool& stopSearch)
 {
   // ensure we have an assertion
   if (!refreshCurrentAssertion())
@@ -186,6 +180,11 @@ SatLiteral JustificationStrategy::getNext(bool& stopSearch)
           d_lastDecisionLit = next.first;
           // record that we made a decision
           d_currStatusDec = true;
+          if (d_decisionStopOnly)
+          {
+            // only doing stop-only, return undefSatLiteral.
+            return undefSatLiteral;
+          }
           return lastChildVal == SAT_VALUE_FALSE ? ~nsl : nsl;
         }
         else
-- 
cgit v1.2.3