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.

8 files changed, 46 insertions, 14 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?
diff --git a/src/options/decision_options.toml b/src/options/decision_options.toml
index 4f3f91ba5..796fd26fa 100644
--- a/src/options/decision_options.toml
+++ b/src/options/decision_options.toml
@@ -17,6 +17,9 @@ name   = "Decision Heuristics"
 [[option.mode.JUSTIFICATION]]
   name = "justification"
   help = "An ATGP-inspired justification heuristic."
+[[option.mode.JUSTIFICATION_OLD]]
+  name = "justification-old"
+  help = "Older implementation of an ATGP-inspired justification heuristic."
 [[option.mode.RELEVANCY]]
   name = "justification-stoponly"
   help = "Use the justification heuristic only to stop early, not for decisions."
@@ -89,7 +92,7 @@ name   = "Decision Heuristics"
   category   = "expert"
   long       = "jh-rlv-order"
   type       = "bool"
-  default    = "false"
+  default    = "true"
   help       = "maintain activity-based ordering for decision justification heuristic"
 
 [[option]]
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 41019d58e..fd86d3a42 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -1606,7 +1606,10 @@ lbool Solver::search(int nof_conflicts)
       // If this was a final check, we are satisfiable
       if (check_type == CHECK_FINAL)
       {
-        bool decisionEngineDone = d_proxy->isDecisionEngineDone();
+        // Note that we are done making decisions when there are no pending decisions
+        // on assumptions, and the decision engine indicates it is done.
+        bool decisionEngineDone = (decisionLevel() >= assumptions.size())
+                                  && d_proxy->isDecisionEngineDone();
         // Unless a lemma has added more stuff to the queues
         if (!decisionEngineDone
             && (!order_heap.empty() || qhead < trail.size()))
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 605c75a14..b0eab66e9 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -77,6 +77,7 @@ void TheoryProxy::theoryCheck(theory::Theory::Effort effort) {
     TNode assertion = d_queue.front();
     d_queue.pop();
     d_theoryEngine->assertFact(assertion);
+    d_decisionEngine->notifyAsserted(assertion);
   }
   d_theoryEngine->check(effort);
 }
diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp
index 89006d154..7176126fb 100644
--- a/src/smt/proof_post_processor.cpp
+++ b/src/smt/proof_post_processor.cpp
@@ -930,13 +930,12 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
     }
     // should give a proof, if not, then tcpg does not agree with the
     // substitution.
-    Assert(pfn != nullptr);
     if (pfn == nullptr)
     {
-      AlwaysAssert(false) << "resort to TRUST_SUBS" << std::endl
-                          << eq << std::endl
-                          << eqq << std::endl
-                          << "from " << children << " applied to " << t;
+      Warning() << "resort to TRUST_SUBS" << std::endl
+                << eq << std::endl
+                << eqq << std::endl
+                << "from " << children << " applied to " << t << std::endl;
       cdp->addStep(eqq, PfRule::TRUST_SUBS, {}, {eqq});
     }
     else