Merge branch 'master' into cav22-stringscav22-strings

1 files changed, 102 insertions, 0 deletions

diff --git a/src/proof/annotation_proof_generator.h b/src/proof/annotation_proof_generator.h
new file mode 100644
index 000000000..fb737dc44
--- /dev/null
+++ b/src/proof/annotation_proof_generator.h
@@ -0,0 +1,102 @@
+/******************************************************************************
+ * 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.
+ * ****************************************************************************
+ *
+ * The annotation proof generator class.
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__PROOF__ANNOTATION_PROOF_GENERATOR_H
+#define CVC5__PROOF__ANNOTATION_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;
+
+/**
+ * Base class for annotators. An annotator is a utility that implements a
+ * simple transformation on proofs: `annotate` below.
+ */
+class Annotator
+{
+ public:
+  Annotator() {}
+  virtual ~Annotator() {}
+  /**
+   * Annotate the proof node. This must return a proof node that concludes the
+   * same thing as p.
+   */
+  virtual std::shared_ptr<ProofNode> annotate(std::shared_ptr<ProofNode> p) = 0;
+};
+
+/**
+ * Annotation proof generator, used to "wrap" proofs of other proof generators
+ * via the annotate method above.
+ */
+class AnnotationProofGenerator : public ProofGenerator
+{
+  typedef context::CDHashMap<Node, std::pair<ProofGenerator*, Annotator*>>
+      NodeExpMap;
+  typedef context::CDHashMap<Node, std::shared_ptr<ProofNode>> NodeProofNodeMap;
+
+ public:
+  AnnotationProofGenerator(ProofNodeManager* pnm,
+                           context::Context* c = nullptr,
+                           std::string name = "AnnotationProofGenerator");
+  ~AnnotationProofGenerator() {}
+  /** Get the proof for formula f. */
+  std::shared_ptr<ProofNode> getProofFor(Node f) override;
+  /** Can we give the proof for formula f? */
+  bool hasProofFor(Node f) override;
+  /**
+   * Set explanation for fact f, called when pg has a proof for f.
+   *
+   * @param f The fact proven by pg,
+   * @param pg The proof generator that can prove f.
+   * @param a The annotator that will annotate the proof of f, if necessary.
+   */
+  void setExplanationFor(Node f, ProofGenerator* pg, Annotator* a);
+  /**
+   * Transform trust node, will be annotated by the given annotator.
+   */
+  TrustNode transform(const TrustNode& trn, Annotator* a);
+  /** identify */
+  std::string identify() const override;
+
+ protected:
+  /** The proof node manager */
+  ProofNodeManager* d_pnm;
+  /** Name identifier */
+  std::string d_name;
+  /** A dummy context used by this class if none is provided */
+  context::Context d_context;
+  /**
+   * A context-dependent map from formulas to a generator + annotation
+   * pair, which will be used to generate the proof of formulas if asked.
+   * We use the context provided to this class or otherwise d_context above.
+   */
+  NodeExpMap d_exps;
+  /**
+   * A context-dependent map from formulas to the proof nodes we have
+   * returned in calls to getProofFor.
+   */
+  NodeProofNodeMap d_proofs;
+};
+
+}  // namespace cvc5
+
+#endif /* CVC5__PROOF__ANNOTATION_PROOF_GENERATOR_H */