Add difficulty post-processor (#7150)

This is work towards supporting a (get-difficulty) command.

This is a helper class for transforming the difficulty of preprocessed assertions to difficulty of the input assertions.

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 4484f94475889ea971d5a3fb5d863c565eb43133..401fc597689af058725323847dcef858075940eb 100644 (file)
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -294,6 +294,8 @@ libcvc5_add_sources(
   smt/check_models.h
   smt/command.cpp
   smt/command.h
+  smt/difficulty_post_processor.cpp
+  smt/difficulty_post_processor.h
   smt/dump.cpp
   smt/dump.h
   smt/dump_manager.cpp

diff --git a/src/smt/difficulty_post_processor.cpp b/src/smt/difficulty_post_processor.cpp
new file mode 100644 (file)
index 0000000..7480922
--- /dev/null
+++ b/src/smt/difficulty_post_processor.cpp
@@ -0,0 +1,77 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Implementation of module for processing the difficulty of input assumptions
+ * based on proof nodes.
+ */
+
+#include "smt/difficulty_post_processor.h"
+
+#include "smt/env.h"
+#include "util/rational.h"
+
+using namespace cvc5::kind;
+using namespace cvc5::theory;
+
+namespace cvc5 {
+namespace smt {
+
+DifficultyPostprocessCallback::DifficultyPostprocessCallback()
+    : d_currDifficulty(0)
+{
+}
+
+bool DifficultyPostprocessCallback::setCurrentDifficulty(Node d)
+{
+  if (d.isConst() && d.getType().isInteger()
+      && d.getConst<Rational>().sgn() >= 0
+      && d.getConst<Rational>().getNumerator().fitsUnsignedInt())
+  {
+    d_currDifficulty = d.getConst<Rational>().getNumerator().toUnsignedInt();
+    return true;
+  }
+  return false;
+}
+
+bool DifficultyPostprocessCallback::shouldUpdate(std::shared_ptr<ProofNode> pn,
+                                                 const std::vector<Node>& fa,
+                                                 bool& continueUpdate)
+{
+  PfRule r = pn->getRule();
+  if (r == PfRule::ASSUME)
+  {
+    Trace("difficulty-debug")
+        << "  found assume: " << pn->getResult() << std::endl;
+    d_accMap[pn->getResult()] += d_currDifficulty;
+  }
+  else if (r == PfRule::MACRO_SR_EQ_INTRO || r == PfRule::MACRO_SR_PRED_INTRO)
+  {
+    // premise is just a substitution, ignore
+    continueUpdate = false;
+    return false;
+  }
+  return true;
+}
+
+void DifficultyPostprocessCallback::getDifficultyMap(
+    std::map<Node, Node>& dmap) const
+{
+  Assert(dmap.empty());
+  NodeManager* nm = NodeManager::currentNM();
+  for (const std::pair<const Node, uint64_t>& d : d_accMap)
+  {
+    dmap[d.first] = nm->mkConst(Rational(d.second));
+  }
+}
+
+}  // namespace smt
+}  // namespace cvc5

diff --git a/src/smt/difficulty_post_processor.h b/src/smt/difficulty_post_processor.h
new file mode 100644 (file)
index 0000000..ef1c9a9
--- /dev/null
+++ b/src/smt/difficulty_post_processor.h
@@ -0,0 +1,88 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Implementation of module for processing the difficulty of input assumptions
+ * based on proof nodes.
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__SMT__DIFFICULTY_POST_PROCESSOR_H
+#define CVC5__SMT__DIFFICULTY_POST_PROCESSOR_H
+
+#include <map>
+
+#include "proof/proof_node_updater.h"
+
+namespace cvc5 {
+namespace smt {
+
+/**
+ * A postprocess callback that computes difficulty based on the structure
+ * of the proof. In particular, this class assesses what the source of an
+ * assertion was by considering the shape of the proof. For instance, if
+ * assertion A entails x=t, and this was used to derive a substitution
+ * { x -> t } to assertion B, then B is the source of B*{ x -> t }. The
+ * difficulty of this assertion is carried to B and not A. The reason is that
+ * A can be understood as a definition, and is eliminated, whereas B was
+ * persistent if B*{ x -> t } was a prepreprocessed assertion.
+ *
+ * Note that this postprocess callback is intended to be run on the proof
+ * of a single preprocessed assertion C. If C was derived by proof with
+ * free assumptions A_1, ..., A_n, then for each A_i that is a "source" as
+ * described above, we increment the difficulty of A_i by the difficulty value
+ * assigned to C.
+ *
+ * This means that the user of this method should:
+ * (1) assign the current difficulty we are incrementing (setCurrentDifficulty),
+ * (2) process the proof using a proof node updater with this callback.
+ * The final difficulty map is accumulated in d_accMap, which can be accessed
+ * at any time via getDifficultyMap.
+ */
+class DifficultyPostprocessCallback : public ProofNodeUpdaterCallback
+{
+ public:
+  DifficultyPostprocessCallback();
+  ~DifficultyPostprocessCallback() {}
+  /**
+   * Set current difficulty of the next proof to process to the (integer)
+   * value stored in Node d. This value will be assigned to all the free
+   * assumptions of the proof we traverse next. This value is stored in
+   * d_currDifficulty.
+   *
+   * @return true if the difficulty value was successfully extracted
+   */
+  bool setCurrentDifficulty(Node d);
+  /**
+   * Should proof pn be updated? This is used to selectively traverse to e.g.
+   * the source of an assertion.
+   */
+  bool shouldUpdate(std::shared_ptr<ProofNode> pn,
+                    const std::vector<Node>& fa,
+                    bool& continueUpdate) override;
+  /** Get the (acculumated) difficulty map for the last processed proof node */
+  void getDifficultyMap(std::map<Node, Node>& dmap) const;
+
+ private:
+  /**
+   * The current difficulty of the assertion whose proof of preprocessing
+   * we are considering.
+   */
+  uint64_t d_currDifficulty;
+  /** The current accumulated difficulty map */
+  std::map<Node, uint64_t> d_accMap;
+};
+
+}  // namespace smt
+}  // namespace cvc5
+
+#endif