1 files changed, 53 insertions, 3 deletions

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