1 files changed, 121 insertions, 0 deletions
diff --git a/src/proof/conv_seq_proof_generator.h b/src/proof/conv_seq_proof_generator.h
new file mode 100644
index 000000000..8d4417134
--- /dev/null
+++ b/src/proof/conv_seq_proof_generator.h
@@ -0,0 +1,121 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Gereon Kremer
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Term conversion sequence proof generator utility.
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__PROOF__CONV_SEQ_PROOF_GENERATOR_H
+#define CVC5__PROOF__CONV_SEQ_PROOF_GENERATOR_H
+
+#include "context/cdhashmap.h"
+#include "expr/node.h"
+#include "proof/proof_generator.h"
+#include "proof/trust_node.h"
+
+namespace cvc5 {
+
+class ProofNodeManager;
+
+/**
+ * The term conversion sequence proof generator. This is used for maintaining
+ * a fixed sequence of proof generators that provide proofs for rewrites
+ * (equalities). We call these the "component generators" of this sequence,
+ * which are typically TConvProofGenerator.
+ */
+class TConvSeqProofGenerator : public ProofGenerator
+{
+ public:
+  /**
+   * @param pnm The proof node manager for constructing ProofNode objects.
+   * @param ts The list of component term conversion generators that are
+   * applied in sequence
+   * @param c The context that this class depends on. If none is provided,
+   * this class is context-independent.
+   * @param name The name of this generator (for debugging).
+   */
+  TConvSeqProofGenerator(ProofNodeManager* pnm,
+                         const std::vector<ProofGenerator*>& ts,
+                         context::Context* c = nullptr,
+                         std::string name = "TConvSeqProofGenerator");
+  ~TConvSeqProofGenerator();
+  /**
+   * Indicate that the index^th proof generator converts term t to s. This
+   * should be called for a unique s for each (t, index). It must be the
+   * case that d_tconv[index] can provide a proof for t = s in the remainder
+   * of the context maintained by this class.
+   */
+  void registerConvertedTerm(Node t, Node s, size_t index);
+  /**
+   * Get the proof for formula f. It should be the case that f is of the form
+   * t_0 = t_n, where it must be the case that t_n is obtained by the following:
+   * For each i=0, ... n, let t_{i+1} be the term such that
+   *   registerConvertedTerm(t_i, t_{i+1}, i)
+   * was called. Otherwise t_{i+1} = t_i.
+   * In other words, t_n is obtained by converting t_0, in order, based on the
+   * calls to registerConvertedTerm.
+   *
+   * @param f The equality fact to get the proof for.
+   * @return The proof for f.
+   */
+  std::shared_ptr<ProofNode> getProofFor(Node f) override;
+  /**
+   * Get subsequence proof for f, with given start and end steps (inclusive).
+   */
+  std::shared_ptr<ProofNode> getSubsequenceProofFor(Node f,
+                                                    size_t start,
+                                                    size_t end);
+  /** Identify this generator (for debugging, etc..) */
+  std::string identify() const override;
+
+  /**
+   * Make trust node from a sequence of converted terms. The number of
+   * terms in cterms should be 1 + the number of component proof generators
+   * maintained by this class. This selects a proof generator that is capable
+   * of proving cterms[0] = cterms[cterms.size()-1], which is either this
+   * generator, or one of the component proof generators, if only one step
+   * rewrote. In the former case, all steps are registered to this class.
+   * Using a component generator is an optimization that saves having to
+   * save the conversion steps or use this class. For example, if we have 2
+   * term conversion components, and call this method on:
+   *   { a, b, c }
+   * then this method calls:
+   *   registerConvertedTerm( a, b, 0 )
+   *   registerConvertedTerm( b, c, 1 )
+   * and returns a trust node proving (= a c) with this class as the proof
+   * generator. On the other hand, if we call this method on:
+   *   { d, d, e }
+   * then we return a trust node proving (= d e) with the 2nd component proof
+   * generator, as it alone is capable of proving this equality.
+   */
+  theory::TrustNode mkTrustRewriteSequence(const std::vector<Node>& cterms);
+
+ protected:
+  using NodeIndexPairHashFunction =
+      PairHashFunction<Node, size_t, std::hash<Node>>;
+  typedef context::
+      CDHashMap<std::pair<Node, size_t>, Node, NodeIndexPairHashFunction>
+          NodeIndexNodeMap;
+  /** The proof node manager */
+  ProofNodeManager* d_pnm;
+  /** The term conversion generators */
+  std::vector<ProofGenerator*> d_tconvs;
+  /** the set of converted terms */
+  NodeIndexNodeMap d_converted;
+  /** Name identifier */
+  std::string d_name;
+};
+
+}  // namespace cvc5
+
+#endif /* CVC5__PROOF__CONV_SEQ_PROOF_GENERATOR_H */