Enable new justification heuristic by default (#6613)

This enables the new implementation of justification heuristic by default.

Fixes #5454, fixes #5785. Fixes wishues 114, 115, 149, 160.

4 files changed, 33 insertions, 7 deletions

diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
index 4116ba90d..d439f33a6 100644
--- a/src/decision/decision_engine.cpp
+++ b/src/decision/decision_engine.cpp
@@ -27,8 +27,9 @@ DecisionEngine::DecisionEngine(context::Context* c,
                                prop::SkolemDefManager* skdm,
                                ResourceManager* rm)
     : d_decEngineOld(new DecisionEngineOld(c, u)),
+      d_jstrat(new JustificationStrategy(c, u, skdm)),
       d_resourceManager(rm),
-      d_useOld(true)
+      d_useOld(options::decisionMode() != options::DecisionMode::JUSTIFICATION)
 {
 }
 
@@ -41,9 +42,16 @@ void DecisionEngine::finishInit(prop::CDCLTSatSolverInterface* ss,
     d_decEngineOld->setCnfStream(cs);
     return;
   }
+  d_jstrat->finishInit(ss, cs);
 }
 
-void DecisionEngine::presolve() {}
+void DecisionEngine::presolve()
+{
+  if (!d_useOld)
+  {
+    d_jstrat->presolve();
+  }
+}
 
 prop::SatLiteral DecisionEngine::getNext(bool& stopSearch)
 {
@@ -52,7 +60,7 @@ prop::SatLiteral DecisionEngine::getNext(bool& stopSearch)
   {
     return d_decEngineOld->getNext(stopSearch);
   }
-  return undefSatLiteral;
+  return d_jstrat->getNext(stopSearch);
 }
 
 bool DecisionEngine::isDone()
@@ -61,7 +69,7 @@ bool DecisionEngine::isDone()
   {
     return d_decEngineOld->isDone();
   }
-  return false;
+  return d_jstrat->isDone();
 }
 
 void DecisionEngine::addAssertion(TNode assertion)
@@ -71,6 +79,7 @@ void DecisionEngine::addAssertion(TNode assertion)
     d_decEngineOld->addAssertion(assertion);
     return;
   }
+  d_jstrat->addAssertion(assertion);
 }
 
 void DecisionEngine::addSkolemDefinition(TNode lem, TNode skolem)
@@ -79,6 +88,10 @@ void DecisionEngine::addSkolemDefinition(TNode lem, TNode skolem)
   {
     d_decEngineOld->addSkolemDefinition(lem, skolem);
   }
+  else
+  {
+    d_jstrat->addSkolemDefinition(lem, skolem);
+  }
 }
 
 void DecisionEngine::notifyAsserted(TNode n)
@@ -87,6 +100,8 @@ void DecisionEngine::notifyAsserted(TNode n)
   {
     return;
   }
+  // old implementation does not use this
+  d_jstrat->notifyAsserted(n);
 }
 
 }  // namespace decision
diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
index de88d656e..e54e1fc3c 100644
--- a/src/decision/decision_engine.h
+++ b/src/decision/decision_engine.h
@@ -18,6 +18,7 @@
 #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"
@@ -60,7 +61,7 @@ class DecisionEngine
    */
   void addAssertion(TNode assertion);
   /**
-   * TODO: remove this interface
+   * !!!! temporary until the old justification implementation is deleted.
    * Notify this class  that lem is the skolem definition for skolem, which is
    * a part of the current assertions.
    */
@@ -74,6 +75,8 @@ class DecisionEngine
  private:
   /** The old implementation */
   std::unique_ptr<DecisionEngineOld> d_decEngineOld;
+  /** The new implementation */
+  std::unique_ptr<JustificationStrategy> d_jstrat;
   /** Pointer to resource manager for associated SmtEngine */
   ResourceManager* d_resourceManager;
   /** using old implementation? */
diff --git a/src/decision/justification_strategy.cpp b/src/decision/justification_strategy.cpp
index 80fca23d5..b73b24bd0 100644
--- a/src/decision/justification_strategy.cpp
+++ b/src/decision/justification_strategy.cpp
@@ -64,12 +64,13 @@ void JustificationStrategy::presolve()
   d_stack.clear();
 }
 
-SatLiteral JustificationStrategy::getNext()
+SatLiteral JustificationStrategy::getNext(bool& stopSearch)
 {
   // ensure we have an assertion
   if (!refreshCurrentAssertion())
   {
     Trace("jh-process") << "getNext, already finished" << std::endl;
+    stopSearch = true;
     return undefSatLiteral;
   }
   Assert(d_stack.hasCurrentAssertion());
@@ -210,6 +211,7 @@ SatLiteral JustificationStrategy::getNext()
   } while (d_stack.hasCurrentAssertion());
   // we exhausted all assertions
   Trace("jh-process") << "...exhausted all assertions" << std::endl;
+  stopSearch = true;
   return undefSatLiteral;
 }
 
@@ -482,6 +484,7 @@ bool JustificationStrategy::isDone() { return !refreshCurrentAssertion(); }
 
 void JustificationStrategy::addAssertion(TNode assertion)
 {
+  Trace("jh-assert") << "addAssertion " << assertion << std::endl;
   std::vector<TNode> toProcess;
   toProcess.push_back(assertion);
   insertToAssertionList(toProcess, false);
@@ -489,6 +492,8 @@ void JustificationStrategy::addAssertion(TNode assertion)
 
 void JustificationStrategy::addSkolemDefinition(TNode lem, TNode skolem)
 {
+  Trace("jh-assert") << "addSkolemDefinition " << lem << " / " << skolem
+                     << std::endl;
   if (d_jhSkRlvMode == options::JutificationSkolemRlvMode::ALWAYS)
   {
     // just add to main assertions list
@@ -565,6 +570,7 @@ void JustificationStrategy::insertToAssertionList(std::vector<TNode>& toProcess,
 
 bool JustificationStrategy::refreshCurrentAssertion()
 {
+  Trace("jh-process") << "refreshCurrentAssertion" << std::endl;
   // if we already have a current assertion, nothing to be done
   TNode curr = d_stack.getCurrentAssertion();
   if (!curr.isNull())
@@ -601,6 +607,7 @@ bool JustificationStrategy::refreshCurrentAssertionFromList(bool useSkolemList)
   SatValue currValue;
   while (!curr.isNull())
   {
+    Trace("jh-process") << "Check assertion " << curr << std::endl;
     // we never add theory literals to our assertions lists
     Assert(!isTheoryLiteral(curr));
     currValue = lookupValue(curr);
diff --git a/src/decision/justification_strategy.h b/src/decision/justification_strategy.h
index 2fa216487..667f53115 100644
--- a/src/decision/justification_strategy.h
+++ b/src/decision/justification_strategy.h
@@ -137,9 +137,10 @@ class JustificationStrategy
    * all relevant input assertions are already propositionally satisfied by
    * the current assignment.
    *
+   * @param stopSearch Set to true if we can stop the search
    * @return The next SAT literal to decide on.
    */
-  prop::SatLiteral getNext();
+  prop::SatLiteral getNext(bool& stopSearch);
 
   /**
    * Are we finished assigning values to literals?