Add utilities in preparation for deep restarts (#8642)

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index eebd54492a64917c7216664300d7f6870630c18f..fdbcf96675a2ddebb3a9c118db4b23425dc03204 100644 (file)
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -711,5 +711,10 @@ std::vector<Node> PropEngine::getLearnedZeroLevelLiterals(
   return d_theoryProxy->getLearnedZeroLevelLiterals(ltype);
 }
 
+std::vector<Node> PropEngine::getLearnedZeroLevelLiteralsForRestart() const
+{
+  return d_theoryProxy->getLearnedZeroLevelLiteralsForRestart();
+}
+
 }  // namespace prop
 }  // namespace cvc5::internal

diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index be4306934b6aeca6e17dce6f6f4ea635d3c5d4f2..5afb38716bd087e1eed3b5e8fe3f5ed80e7deee8 100644 (file)
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -25,6 +25,7 @@
 #include "expr/node.h"
 #include "proof/proof.h"
 #include "proof/trust_node.h"
+#include "prop/learned_db.h"
 #include "prop/skolem_def_manager.h"
 #include "smt/env_obj.h"
 #include "theory/output_channel.h"
@@ -313,6 +314,9 @@ class PropEngine : protected EnvObj
   std::vector<Node> getLearnedZeroLevelLiterals(
       modes::LearnedLitType ltype) const;
 
+  /** Get the zero-level assertions that should be used on deep restart */
+  std::vector<Node> getLearnedZeroLevelLiteralsForRestart() const;
+
  private:
   /** Dump out the satisfying assignment (after SAT result) */
   void printSatisfyingAssignment();

diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index abd37695c4ce630307c13d72b2f338d60476662e..d6c6f6a56964d0b284feea5d5063afeb1718d867 100644 (file)
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -50,7 +50,8 @@ TheoryProxy::TheoryProxy(Env& env,
       d_queue(context()),
       d_tpp(env, *theoryEngine),
       d_skdm(skdm),
-      d_zll(nullptr)
+      d_zll(nullptr),
+      d_stopSearch(false, userContext())
 {
   bool trackZeroLevel = isOutputOn(OutputTag::LEARNED_LITS)
                         || options().smt.produceLearnedLiterals;
@@ -70,6 +71,7 @@ void TheoryProxy::presolve()
 {
   d_decisionEngine->presolve();
   d_theoryEngine->presolve();
+  d_stopSearch = false;
 }
 
 void TheoryProxy::notifyTopLevelSubstitution(const Node& lhs,
@@ -136,6 +138,10 @@ void TheoryProxy::theoryCheck(theory::Theory::Effort effort) {
     d_queue.pop();
     if (d_zll != nullptr)
     {
+      if (d_stopSearch.get())
+      {
+        break;
+      }
       int32_t alevel = d_propEngine->getDecisionLevel(assertion);
       d_zll->notifyAsserted(assertion, alevel);
     }
@@ -155,7 +161,10 @@ void TheoryProxy::theoryCheck(theory::Theory::Effort effort) {
       d_decisionEngine->notifyActiveSkolemDefs(activeSkolemDefs);
     }
   }
-  d_theoryEngine->check(effort);
+  if (!d_stopSearch.get())
+  {
+    d_theoryEngine->check(effort);
+  }
 }
 
 void TheoryProxy::theoryPropagate(std::vector<SatLiteral>& output) {
@@ -235,6 +244,11 @@ SatLiteral TheoryProxy::getNextTheoryDecisionRequest() {
 SatLiteral TheoryProxy::getNextDecisionEngineRequest(bool &stopSearch) {
   Assert(d_decisionEngine != NULL);
   Assert(stopSearch != true);
+  if (d_stopSearch.get())
+  {
+    stopSearch = true;
+    return undefSatLiteral;
+  }
   SatLiteral ret = d_decisionEngine->getNext(stopSearch);
   if(stopSearch) {
     Trace("decision") << "  ***  Decision Engine stopped search *** " << std::endl;
@@ -243,12 +257,16 @@ SatLiteral TheoryProxy::getNextDecisionEngineRequest(bool &stopSearch) {
 }
 
 bool TheoryProxy::theoryNeedCheck() const {
+  if (d_stopSearch.get())
+  {
+    return false;
+  }
   return d_theoryEngine->needCheck();
 }
 
 bool TheoryProxy::isIncomplete() const
 {
-  return d_theoryEngine->isIncomplete();
+  return d_stopSearch.get() || d_theoryEngine->isIncomplete();
 }
 
 TNode TheoryProxy::getNode(SatLiteral lit) {
@@ -268,7 +286,7 @@ void TheoryProxy::spendResource(Resource r)
 bool TheoryProxy::isDecisionRelevant(SatVariable var) { return true; }
 
 bool TheoryProxy::isDecisionEngineDone() {
-  return d_decisionEngine->isDone();
+  return d_decisionEngine->isDone() || d_stopSearch.get();
 }
 
 SatValue TheoryProxy::getDecisionPolarity(SatVariable var) {
@@ -321,5 +339,14 @@ std::vector<Node> TheoryProxy::getLearnedZeroLevelLiterals(
   return {};
 }
 
+std::vector<Node> TheoryProxy::getLearnedZeroLevelLiteralsForRestart() const
+{
+  if (d_zll != nullptr)
+  {
+    return d_zll->getLearnedZeroLevelLiteralsForRestart();
+  }
+  return {};
+}
+
 }  // namespace prop
 }  // namespace cvc5::internal

diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index 8d0270fa46ce458acea8676c51767073da5f3c1d..a3b824799d46e9ef5c00919f3bc2e8bee0fb2218 100644 (file)
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -179,6 +179,8 @@ class TheoryProxy : protected EnvObj, public Registrar
   /** Get the zero-level assertions */
   std::vector<Node> getLearnedZeroLevelLiterals(
       modes::LearnedLitType ltype) const;
+  /** Get the zero-level assertions that should be used on deep restart */
+  std::vector<Node> getLearnedZeroLevelLiteralsForRestart() const;
 
  private:
   /** The prop engine we are using. */
@@ -217,6 +219,8 @@ class TheoryProxy : protected EnvObj, public Registrar
   /** The zero level learner */
   std::unique_ptr<ZeroLevelLearner> d_zll;
 
+  /** Whether we have been requested to stop the search */
+  context::CDO<bool> d_stopSearch;
 }; /* class TheoryProxy */
 
 }  // namespace prop

diff --git a/src/prop/zero_level_learner.cpp b/src/prop/zero_level_learner.cpp
index a98136ca8c7b4249ca36b699c10a54900c1a4256..32eb90059708d4ac9156d7d6e8289867a9a6df36 100644 (file)
--- a/src/prop/zero_level_learner.cpp
+++ b/src/prop/zero_level_learner.cpp
@@ -265,6 +265,30 @@ std::vector<Node> ZeroLevelLearner::getLearnedZeroLevelLiterals(
   return ret;
 }
 
+std::vector<Node> ZeroLevelLearner::getLearnedZeroLevelLiteralsForRestart()
+    const
+{
+  std::vector<Node> ret;
+  for (modes::LearnedLitType ltype : d_learnedTypes)
+  {
+    std::vector<Node> rett = getLearnedZeroLevelLiterals(ltype);
+    ret.insert(ret.end(), rett.begin(), rett.end());
+  }
+  return ret;
+}
+
+bool ZeroLevelLearner::hasLearnedLiteralForRestart() const
+{
+  for (modes::LearnedLitType ltype : d_learnedTypes)
+  {
+    if (d_ldb.getNumLearnedLiterals(ltype) > 0)
+    {
+      return true;
+    }
+  }
+  return false;
+}
+
 bool ZeroLevelLearner::isLearnable(modes::LearnedLitType ltype) const
 {
   return d_learnedTypes.find(ltype) != d_learnedTypes.end();

diff --git a/src/prop/zero_level_learner.h b/src/prop/zero_level_learner.h
index e61d4158415ddffce764888542418bbede9c78f2..16b5e7e3c017ffe396f2936cb6539aa459e74e1c 100644 (file)
--- a/src/prop/zero_level_learner.h
+++ b/src/prop/zero_level_learner.h
@@ -64,6 +64,8 @@ class ZeroLevelLearner : protected EnvObj
   /** Get the zero-level assertions */
   std::vector<Node> getLearnedZeroLevelLiterals(
       modes::LearnedLitType ltype) const;
+  /** Get the zero-level assertions that should be used on deep restart */
+  std::vector<Node> getLearnedZeroLevelLiteralsForRestart() const;
 
  private:
   static void getAtoms(TNode a,
@@ -77,6 +79,8 @@ class ZeroLevelLearner : protected EnvObj
   bool isLearnable(modes::LearnedLitType ltype) const;
   /** get solved */
   bool getSolved(const Node& lit, Subs& subs);
+  /** has learned literal */
+  bool hasLearnedLiteralForRestart() const;
 
   /** The theory engine we are using */
   TheoryEngine* d_theoryEngine;