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.

1 files changed, 88 insertions, 0 deletions

diff --git a/src/smt/difficulty_post_processor.h b/src/smt/difficulty_post_processor.h
new file mode 100644
index 000000000..ef1c9a9ea
--- /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