Connect difficulty manager to TheoryEngine (#7161)

This also introduces the produceDifficulty option which is analogous to produceUnsatCores.

It requires another unsat cores mode PP_ONLY, indicating that we are only tracking proofs of preprocessing. This option should perhaps be renamed to proofMode instead of unsatCoresMode, since its use is more general than for unsat cores. This will be addressed in a future refactoring.

7 files changed, 136 insertions, 14 deletions

diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 7d0dab720..26af86ca2 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -196,6 +196,9 @@ name   = "SMT Layer"
 [[option.mode.ASSUMPTIONS]]
   name = "assumptions"
   help = "Produce unsat cores using solving under assumptions and preprocessing proofs."
+[[option.mode.PP_ONLY]]
+  name = "pp-only"
+  help = "Not producing unsat cores, but tracking proofs of preprocessing (internal only)."
 
 [[option]]
   name       = "minimalUnsatCores"
@@ -221,6 +224,14 @@ name   = "SMT Layer"
   help       = "turn on unsat assumptions generation"
 
 [[option]]
+  name       = "produceDifficulty"
+  category   = "regular"
+  long       = "produce-difficulty"
+  type       = "bool"
+  default    = "false"
+  help       = "enable tracking of difficulty."
+
+[[option]]
   name       = "difficultyMode"
   category   = "regular"
   long       = "difficulty-mode=MODE"
diff --git a/src/smt/env.cpp b/src/smt/env.cpp
index 12e3c7520..f42a51dd0 100644
--- a/src/smt/env.cpp
+++ b/src/smt/env.cpp
@@ -86,8 +86,10 @@ bool Env::isSatProofProducing() const
 {
   return d_proofNodeManager != nullptr
          && (!d_options.smt.unsatCores
-             || d_options.smt.unsatCoresMode
-                    != options::UnsatCoresMode::ASSUMPTIONS);
+             || (d_options.smt.unsatCoresMode
+                     != options::UnsatCoresMode::ASSUMPTIONS
+                 && d_options.smt.unsatCoresMode
+                        != options::UnsatCoresMode::PP_ONLY));
 }
 
 bool Env::isTheoryProofProducing() const
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 6e7939ff7..a226de807 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -81,6 +81,14 @@ void SetDefaults::setDefaultsPre(Options& opts)
   {
     opts.driver.dumpUnsatCores = true;
   }
+  if (opts.smt.produceDifficulty)
+  {
+    if (opts.smt.unsatCoresMode == options::UnsatCoresMode::OFF)
+    {
+      opts.smt.unsatCoresMode = options::UnsatCoresMode::PP_ONLY;
+    }
+    opts.proof.proofGranularityMode = options::ProofGranularityMode::OFF;
+  }
   if (opts.smt.checkUnsatCores || opts.driver.dumpUnsatCores
       || opts.smt.unsatAssumptions || opts.smt.minimalUnsatCores
       || opts.smt.unsatCoresMode != options::UnsatCoresMode::OFF)
@@ -1142,8 +1150,9 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts,
 bool SetDefaults::safeUnsatCores(const Options& opts) const
 {
   // whether we want to force safe unsat cores, i.e., if we are in the default
-  // ASSUMPTIONS mode, since other ones are experimental
-  return opts.smt.unsatCoresMode == options::UnsatCoresMode::ASSUMPTIONS;
+  // ASSUMPTIONS mode or PP_ONLY, since other ones are experimental
+  return opts.smt.unsatCoresMode == options::UnsatCoresMode::ASSUMPTIONS
+         || opts.smt.unsatCoresMode == options::UnsatCoresMode::PP_ONLY;
 }
 
 bool SetDefaults::incompatibleWithQuantifiers(Options& opts,
diff --git a/src/theory/relevance_manager.cpp b/src/theory/relevance_manager.cpp
index 9746f4a22..e1a342178 100644
--- a/src/theory/relevance_manager.cpp
+++ b/src/theory/relevance_manager.cpp
@@ -17,6 +17,9 @@
 
 #include <sstream>
 
+#include "options/smt_options.h"
+#include "smt/env.h"
+
 using namespace cvc5::kind;
 
 namespace cvc5 {
@@ -24,8 +27,22 @@ namespace theory {
 
 RelevanceManager::RelevanceManager(context::UserContext* userContext,
                                    Valuation val)
-    : d_val(val), d_input(userContext), d_computed(false), d_success(false)
+    : d_val(val),
+      d_input(userContext),
+      d_computed(false),
+      d_success(false),
+      d_trackRSetExp(false),
+      d_miniscopeTopLevel(true)
 {
+  if (options::produceDifficulty())
+  {
+    d_dman.reset(new DifficultyManager(userContext, val));
+    d_trackRSetExp = true;
+    // we cannot miniscope AND at the top level, since we need to
+    // preserve the exact form of preprocessed assertions so the dependencies
+    // are tracked.
+    d_miniscopeTopLevel = false;
+  }
 }
 
 void RelevanceManager::notifyPreprocessedAssertions(
@@ -35,7 +52,7 @@ void RelevanceManager::notifyPreprocessedAssertions(
   std::vector<Node> toProcess;
   for (const Node& a : assertions)
   {
-    if (a.getKind() == AND)
+    if (d_miniscopeTopLevel && a.getKind() == AND)
     {
       // split top-level AND
       for (const Node& ac : a)
@@ -64,8 +81,10 @@ void RelevanceManager::addAssertionsInternal(std::vector<Node>& toProcess)
   while (i < toProcess.size())
   {
     Node a = toProcess[i];
-    if (a.getKind() == AND)
+    if (d_miniscopeTopLevel && a.getKind() == AND)
     {
+      // difficulty tracking disables miniscoping of AND
+      Assert(d_dman == nullptr);
       // split AND
       for (const Node& ac : a)
       {
@@ -91,6 +110,7 @@ void RelevanceManager::computeRelevance()
 {
   d_computed = true;
   d_rset.clear();
+  d_rsetExp.clear();
   Trace("rel-manager") << "RelevanceManager::computeRelevance..." << std::endl;
   std::unordered_map<TNode, int> cache;
   for (const Node& node: d_input)
@@ -271,6 +291,10 @@ int RelevanceManager::justify(TNode n, std::unordered_map<TNode, int>& cache)
         {
           ret = value ? 1 : -1;
           d_rset.insert(cur);
+          if (d_trackRSetExp)
+          {
+            d_rsetExp[cur] = n;
+          }
         }
         cache[cur] = ret;
       }
@@ -326,5 +350,31 @@ const std::unordered_set<TNode>& RelevanceManager::getRelevantAssertions(
   return d_rset;
 }
 
+void RelevanceManager::notifyLemma(Node n)
+{
+  if (d_dman != nullptr)
+  {
+    // ensure we know which literals are relevant, and why
+    computeRelevance();
+    d_dman->notifyLemma(d_rsetExp, n);
+  }
+}
+
+void RelevanceManager::notifyCandidateModel(TheoryModel* m)
+{
+  if (d_dman != nullptr)
+  {
+    d_dman->notifyCandidateModel(d_input, m);
+  }
+}
+
+void RelevanceManager::getDifficultyMap(std::map<Node, Node>& dmap)
+{
+  if (d_dman != nullptr)
+  {
+    d_dman->getDifficultyMap(dmap);
+  }
+}
+
 }  // namespace theory
 }  // namespace cvc5
diff --git a/src/theory/relevance_manager.h b/src/theory/relevance_manager.h
index 6c69861fd..f8cd8e1ee 100644
--- a/src/theory/relevance_manager.h
+++ b/src/theory/relevance_manager.h
@@ -23,11 +23,14 @@
 
 #include "context/cdlist.h"
 #include "expr/node.h"
+#include "theory/difficulty_manager.h"
 #include "theory/valuation.h"
 
 namespace cvc5 {
 namespace theory {
 
+class TheoryModel;
+
 /**
  * This class manages queries related to relevance of asserted literals.
  * In particular, note the following definition:
@@ -100,11 +103,20 @@ class RelevanceManager
    * if not already done so. This call is valid during a full effort check in
    * TheoryEngine, or after TheoryEngine has terminated with "sat". This method
    * sets the flag success to false if we failed to compute relevant
-   * assertions, which can occur if
+   * assertions, which occurs if the values from the SAT solver do not satisfy
+   * the assertions we are notified of. This should never happen.
    *
    * The value of this return is only valid if success was not updated to false.
    */
   const std::unordered_set<TNode>& getRelevantAssertions(bool& success);
+  /** Notify lemma, for difficulty measurements */
+  void notifyLemma(Node n);
+  /** Notify that m is a (candidate) model, for difficulty measurements */
+  void notifyCandidateModel(TheoryModel* m);
+  /**
+   * Get difficulty map
+   */
+  void getDifficultyMap(std::map<Node, Node>& dmap);
 
  private:
   /**
@@ -157,6 +169,22 @@ class RelevanceManager
    * aborts and indicates that all literals are relevant.
    */
   bool d_success;
+  /** Are we tracking the sources of why a literal is relevant */
+  bool d_trackRSetExp;
+  /**
+   * Whether we have miniscoped top-level AND of assertions, which is done
+   * as an optimization. This is disabled if e.g. we are computing difficulty,
+   * which requires preserving the original form of the preprocessed
+   * assertions.
+   */
+  bool d_miniscopeTopLevel;
+  /**
+   * Map from the domain of d_rset to the assertion in d_input that is the
+   * reason why that literal is currently relevant.
+   */
+  std::map<TNode, TNode> d_rsetExp;
+  /** Difficulty module */
+  std::unique_ptr<DifficultyManager> d_dman;
 };
 
 }  // namespace theory
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index be4b7dd76..54cfc9a6d 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -155,10 +155,9 @@ void TheoryEngine::finishInit()
                     << options::tcMode() << " not supported";
   }
   // create the relevance filter if any option requires it
-  if (options::relevanceFilter())
+  if (options::relevanceFilter() || options::produceDifficulty())
   {
-    d_relManager.reset(
-        new RelevanceManager(userContext(), theory::Valuation(this)));
+    d_relManager.reset(new RelevanceManager(userContext(), Valuation(this)));
   }
 
   // initialize the quantifiers engine
@@ -530,6 +529,11 @@ void TheoryEngine::check(Theory::Effort effort) {
           d_quantEngine->check(Theory::EFFORT_LAST_CALL);
         }
       }
+      // notify the relevant manager
+      if (d_relManager != nullptr)
+      {
+        d_relManager->notifyCandidateModel(getModel());
+      }
       if (!d_inConflict && !needCheck())
       {
         // We only mark that we are in "SAT mode". We build the model later only
@@ -1140,6 +1144,12 @@ const std::unordered_set<TNode>& TheoryEngine::getRelevantAssertions(
   return d_relManager->getRelevantAssertions(success);
 }
 
+void TheoryEngine::getDifficultyMap(std::map<Node, Node>& dmap)
+{
+  Assert(d_relManager != nullptr);
+  d_relManager->getDifficultyMap(dmap);
+}
+
 Node TheoryEngine::getModelValue(TNode var) {
   if (var.isConst())
   {
@@ -1365,14 +1375,18 @@ void TheoryEngine::lemma(TrustNode tlemma,
   // If specified, we must add this lemma to the set of those that need to be
   // justified, where note we pass all auxiliary lemmas in skAsserts as well,
   // since these by extension must be justified as well.
-  if (d_relManager != nullptr && isLemmaPropertyNeedsJustify(p))
+  if (d_relManager != nullptr)
   {
     std::vector<Node> skAsserts;
     std::vector<Node> sks;
     Node retLemma =
         d_propEngine->getPreprocessedTerm(tlemma.getProven(), skAsserts, sks);
-    d_relManager->notifyPreprocessedAssertion(retLemma);
-    d_relManager->notifyPreprocessedAssertions(skAsserts);
+    if (isLemmaPropertyNeedsJustify(p))
+    {
+      d_relManager->notifyPreprocessedAssertion(retLemma);
+      d_relManager->notifyPreprocessedAssertions(skAsserts);
+    }
+    d_relManager->notifyLemma(retLemma);
   }
 
   // Mark that we added some lemmas
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 496966149..4e8beb967 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -390,6 +390,14 @@ class TheoryEngine : protected EnvObj
   const std::unordered_set<TNode>& getRelevantAssertions(bool& success);
 
   /**
+   * Get difficulty map, which populates dmap, mapping preprocessed assertions
+   * to a value that estimates their difficulty for solving the current problem.
+   *
+   * For details, see theory/difficuly_manager.h.
+   */
+  void getDifficultyMap(std::map<Node, Node>& dmap);
+
+  /**
    * Forwards an entailment check according to the given theoryOfMode.
    * See theory.h for documentation on entailmentCheck().
    */