1 files changed, 178 insertions, 0 deletions
diff --git a/src/proof/trust_node.h b/src/proof/trust_node.h
new file mode 100644
index 000000000..200dececd
--- /dev/null
+++ b/src/proof/trust_node.h
@@ -0,0 +1,178 @@
+/******************************************************************************
+ * 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.
+ * ****************************************************************************
+ *
+ * The trust node utility.
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__PROOF__TRUST_NODE_H
+#define CVC5__PROOF__TRUST_NODE_H
+
+#include "expr/node.h"
+
+namespace cvc5 {
+
+class ProofGenerator;
+class ProofNode;
+
+namespace theory {
+
+/** A kind for trust nodes */
+enum class TrustNodeKind : uint32_t
+{
+  CONFLICT,
+  LEMMA,
+  PROP_EXP,
+  REWRITE,
+  INVALID
+};
+/**
+ * Converts a proof rule to a string. Note: This function is also used in
+ * `safe_print()`. Changing this function name or signature will result in
+ * `safe_print()` printing "<unsupported>" instead of the proper strings for
+ * the enum values.
+ *
+ * Returns a string with static lifetime: it should not be freed.
+ *
+ * @param tnk The trust node kind
+ * @return The name of the trust node kind
+ */
+const char* toString(TrustNodeKind tnk);
+
+/**
+ * Writes a trust node kind name to a stream.
+ *
+ * @param out The stream to write to
+ * @param tnk The trust node kind to write to the stream
+ * @return The stream
+ */
+std::ostream& operator<<(std::ostream& out, TrustNodeKind tnk);
+
+/**
+ * A trust node is a pair (F, G) where F is a formula and G is a proof
+ * generator that can construct a proof for F if asked.
+ *
+ * More generally, a trust node is any node that can be used for a specific
+ * purpose that requires justification, such as being passed to
+ * OutputChannel::lemma. That justification is intended to be given by the
+ * generator that is required to construct this object.
+ *
+ * They are intended to be constructed by ProofGenerator objects themselves (a
+ * proof generator wraps itself in TrustNode it returns) and passed
+ * to ProofOutputChannel by theory solvers.
+ *
+ * The static functions for constructing them check that the generator, if
+ * provided, is capable of proving the given conflict or lemma, or an assertion
+ * failure occurs. Otherwise an assertion error is given.
+ *
+ * While this is not enforced, a `TrustNode` generally encapsulates a **closed**
+ * proof of the formula: one without free assumptions.
+ */
+class TrustNode
+{
+ public:
+  TrustNode() : d_tnk(TrustNodeKind::INVALID), d_gen(nullptr) {}
+  /** Make a proven node for conflict */
+  static TrustNode mkTrustConflict(Node conf, ProofGenerator* g = nullptr);
+  /** Make a proven node for lemma */
+  static TrustNode mkTrustLemma(Node lem, ProofGenerator* g = nullptr);
+  /** Make a proven node for explanation of propagated literal */
+  static TrustNode mkTrustPropExp(TNode lit,
+                                  Node exp,
+                                  ProofGenerator* g = nullptr);
+  /** Make a proven node for rewrite */
+  static TrustNode mkTrustRewrite(TNode n,
+                                  Node nr,
+                                  ProofGenerator* g = nullptr);
+  /** The null proven node */
+  static TrustNode null();
+  ~TrustNode() {}
+  /** get kind */
+  TrustNodeKind getKind() const;
+  /** get node
+   *
+   * This is the node that is used in a common interface, either:
+   * (1) A T-unsat conjunction conf to pass to OutputChannel::conflict,
+   * (2) A valid T-formula lem to pass to OutputChannel::lemma,
+   * (3) A conjunction of literals exp to return in Theory::explain(lit), or
+   * (4) A result of rewriting a term n into an equivalent one nr.
+   *
+   * Notice that this node does not necessarily correspond to a valid formula.
+   * The call getProven() below retrieves a valid formula corresponding to
+   * the above calls.
+   */
+  Node getNode() const;
+  /** get proven
+   *
+   * This is the corresponding formula that is proven by the proof generator
+   * for the above cases:
+   * (1) (not conf), for conflicts,
+   * (2) lem, for lemmas,
+   * (3) (=> exp lit), for propagations from explanations,
+   * (4) (= n nr), for results of rewriting.
+   *
+   * When constructing this trust node, the proof generator should be able to
+   * provide a proof for this fact.
+   */
+  Node getProven() const;
+  /** get generator */
+  ProofGenerator* getGenerator() const;
+  /** is null? */
+  bool isNull() const;
+  /**
+   * Gets the proof node for this trust node, which is obtained by
+   * calling the generator's getProofFor method on the proven node.
+   */
+  std::shared_ptr<ProofNode> toProofNode() const;
+
+  /** Get the proven formula corresponding to a conflict call */
+  static Node getConflictProven(Node conf);
+  /** Get the proven formula corresponding to a lemma call */
+  static Node getLemmaProven(Node lem);
+  /** Get the proven formula corresponding to explanations for propagation */
+  static Node getPropExpProven(TNode lit, Node exp);
+  /** Get the proven formula corresponding to a rewrite */
+  static Node getRewriteProven(TNode n, Node nr);
+  /** For debugging */
+  std::string identifyGenerator() const;
+
+  /**
+   * debug check closed on Trace c, context ctx is string for debugging
+   *
+   * @param reqNullGen Whether we consider a null generator to be a failure.
+   */
+  void debugCheckClosed(const char* c, const char* ctx, bool reqNullGen = true);
+
+ private:
+  TrustNode(TrustNodeKind tnk, Node p, ProofGenerator* g = nullptr);
+  /** The kind */
+  TrustNodeKind d_tnk;
+  /** The proven node */
+  Node d_proven;
+  /** The generator */
+  ProofGenerator* d_gen;
+};
+
+/**
+ * Writes a trust node to a stream.
+ *
+ * @param out The stream to write to
+ * @param n The trust node to write to the stream
+ * @return The stream
+ */
+std::ostream& operator<<(std::ostream& out, TrustNode n);
+
+}  // namespace theory
+}  // namespace cvc5
+
+#endif /* CVC5__PROOF__TRUST_NODE_H */