From 1014428633ca233aa0c51818d995acaca6ebfda6 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 14 Sep 2021 14:58:01 -0500
Subject: [PATCH] Add proof manager method to translate difficulty map (#7159)

This method will be called from SmtEngine in the implementation for (get-difficulty).
---
 src/smt/proof_manager.cpp | 53 +++++++++++++++++++++++++++++++++++++++
 src/smt/proof_manager.h   | 17 +++++++++++++
 2 files changed, 70 insertions(+)

diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp
index 2c3a22a78..4d6e2b495 100644
--- a/src/smt/proof_manager.cpp
+++ b/src/smt/proof_manager.cpp
@@ -24,6 +24,7 @@
 #include "proof/proof_node_algorithm.h"
 #include "proof/proof_node_manager.h"
 #include "smt/assertions.h"
+#include "smt/difficulty_post_processor.h"
 #include "smt/env.h"
 #include "smt/preprocess_proof_generator.h"
 #include "smt/proof_post_processor.h"
@@ -195,6 +196,58 @@ void PfManager::checkProof(std::shared_ptr<ProofNode> pfn, Assertions& as)
                            << std::endl;
 }
 
+void PfManager::translateDifficultyMap(std::map<Node, Node>& dmap,
+                                       Assertions& as)
+{
+  Trace("difficulty") << "PfManager::translateDifficultyMap" << std::endl;
+  if (dmap.empty())
+  {
+    return;
+  }
+  std::map<Node, Node> dmapp = dmap;
+  dmap.clear();
+  std::vector<Node> ppAsserts;
+  for (const std::pair<const Node, Node>& ppa : dmapp)
+  {
+    Trace("difficulty") << "  preprocess difficulty: " << ppa.second << " for "
+                        << ppa.first << std::endl;
+    ppAsserts.push_back(ppa.first);
+  }
+  // assume a SAT refutation from all input assertions that were marked
+  // as having a difficulty
+  CDProof cdp(d_pnm.get());
+  Node fnode = NodeManager::currentNM()->mkConst(false);
+  cdp.addStep(fnode, PfRule::SAT_REFUTATION, ppAsserts, {});
+  std::shared_ptr<ProofNode> pf = cdp.getProofFor(fnode);
+  std::shared_ptr<ProofNode> fpf = getFinalProof(pf, as);
+  Trace("difficulty-debug") << "Final proof is " << *fpf.get() << std::endl;
+  Assert(fpf->getRule() == PfRule::SCOPE);
+  fpf = fpf->getChildren()[0];
+  // analyze proof
+  Assert(fpf->getRule() == PfRule::SAT_REFUTATION);
+  const std::vector<std::shared_ptr<ProofNode>>& children = fpf->getChildren();
+  DifficultyPostprocessCallback dpc;
+  ProofNodeUpdater dpnu(d_pnm.get(), dpc);
+  // For each child of SAT_REFUTATION, we increment the difficulty on all
+  // "source" free assumptions (see DifficultyPostprocessCallback) by the
+  // difficulty of the preprocessed assertion.
+  for (const std::shared_ptr<ProofNode>& c : children)
+  {
+    Node res = c->getResult();
+    Assert(dmapp.find(res) != dmapp.end());
+    Trace("difficulty-debug") << "  process: " << res << std::endl;
+    Trace("difficulty-debug") << "  .dvalue: " << dmapp[res] << std::endl;
+    Trace("difficulty-debug") << "  ..proof: " << *c.get() << std::endl;
+    if (!dpc.setCurrentDifficulty(dmapp[res]))
+    {
+      continue;
+    }
+    dpnu.process(c);
+  }
+  // get the accumulated difficulty map from the callback
+  dpc.getDifficultyMap(dmap);
+}
+
 ProofChecker* PfManager::getProofChecker() const { return d_pchecker.get(); }
 
 ProofNodeManager* PfManager::getProofNodeManager() const { return d_pnm.get(); }
diff --git a/src/smt/proof_manager.h b/src/smt/proof_manager.h
index 034a4554f..45be71771 100644
--- a/src/smt/proof_manager.h
+++ b/src/smt/proof_manager.h
@@ -95,6 +95,23 @@ class PfManager : protected EnvObj
    */
   void checkProof(std::shared_ptr<ProofNode> pfn, Assertions& as);
 
+  /**
+   * Translate difficulty map. This takes a mapping dmap from preprocessed
+   * assertions to values estimating their difficulty. It translates this
+   * map so that dmap contains a mapping from *input* assertions to values
+   * estimating their difficulty.
+   *
+   * It does this translation by constructing a proof of preprocessing for all
+   * preprocessed assertions marked as having a difficulty, traversing those
+   * proofs, and conditionally incrementing the difficulty of the input
+   * assertion on which they depend. This is based on whether the free
+   * assumption is the "source" of an assertion.
+   *
+   * @param dmap Map estimating the difficulty of preprocessed assertions
+   * @param as The input assertions
+   */
+  void translateDifficultyMap(std::map<Node, Node>& dmap, Assertions& as);
+
   /**
    * Get final proof.
    *
-- 
2.30.2