1 files changed, 150 insertions, 0 deletions
diff --git a/src/proof/trust_node.cpp b/src/proof/trust_node.cpp
new file mode 100644
index 000000000..d99e6de51
--- /dev/null
+++ b/src/proof/trust_node.cpp
@@ -0,0 +1,150 @@
+/******************************************************************************
+ * 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 the trust node utility.
+ */
+
+#include "proof/trust_node.h"
+
+#include "proof/proof_ensure_closed.h"
+#include "proof/proof_generator.h"
+
+namespace cvc5 {
+namespace theory {
+
+const char* toString(TrustNodeKind tnk)
+{
+  switch (tnk)
+  {
+    case TrustNodeKind::CONFLICT: return "CONFLICT";
+    case TrustNodeKind::LEMMA: return "LEMMA";
+    case TrustNodeKind::PROP_EXP: return "PROP_EXP";
+    case TrustNodeKind::REWRITE: return "REWRITE";
+    default: return "?";
+  }
+}
+
+std::ostream& operator<<(std::ostream& out, TrustNodeKind tnk)
+{
+  out << toString(tnk);
+  return out;
+}
+
+TrustNode TrustNode::mkTrustConflict(Node conf, ProofGenerator* g)
+{
+  Node ckey = getConflictProven(conf);
+  // if a generator is provided, should confirm that it can prove it
+  Assert(g == nullptr || g->hasProofFor(ckey));
+  return TrustNode(TrustNodeKind::CONFLICT, ckey, g);
+}
+
+TrustNode TrustNode::mkTrustLemma(Node lem, ProofGenerator* g)
+{
+  Node lkey = getLemmaProven(lem);
+  // if a generator is provided, should confirm that it can prove it
+  Assert(g == nullptr || g->hasProofFor(lkey));
+  return TrustNode(TrustNodeKind::LEMMA, lkey, g);
+}
+
+TrustNode TrustNode::mkTrustPropExp(TNode lit, Node exp, ProofGenerator* g)
+{
+  Node pekey = getPropExpProven(lit, exp);
+  Assert(g == nullptr || g->hasProofFor(pekey));
+  return TrustNode(TrustNodeKind::PROP_EXP, pekey, g);
+}
+
+TrustNode TrustNode::mkTrustRewrite(TNode n, Node nr, ProofGenerator* g)
+{
+  Node rkey = getRewriteProven(n, nr);
+  Assert(g == nullptr || g->hasProofFor(rkey));
+  return TrustNode(TrustNodeKind::REWRITE, rkey, g);
+}
+
+TrustNode TrustNode::null()
+{
+  return TrustNode(TrustNodeKind::INVALID, Node::null());
+}
+
+TrustNode::TrustNode(TrustNodeKind tnk, Node p, ProofGenerator* g)
+    : d_tnk(tnk), d_proven(p), d_gen(g)
+{
+  // does not make sense to provide null node with generator
+  Assert(!d_proven.isNull() || d_gen == nullptr);
+}
+
+TrustNodeKind TrustNode::getKind() const { return d_tnk; }
+
+Node TrustNode::getNode() const
+{
+  switch (d_tnk)
+  {
+    // the node of lemma is the node itself
+    case TrustNodeKind::LEMMA: return d_proven;
+    // the node of the rewrite is the right hand side of EQUAL
+    case TrustNodeKind::REWRITE: return d_proven[1];
+    // the node of an explained propagation is the antecendant of an IMPLIES
+    // the node of a conflict is underneath a NOT
+    default: return d_proven[0];
+  }
+}
+
+Node TrustNode::getProven() const { return d_proven; }
+
+ProofGenerator* TrustNode::getGenerator() const { return d_gen; }
+
+bool TrustNode::isNull() const { return d_proven.isNull(); }
+
+std::shared_ptr<ProofNode> TrustNode::toProofNode() const
+{
+  if (d_gen == nullptr)
+  {
+    return nullptr;
+  }
+  return d_gen->getProofFor(d_proven);
+}
+
+Node TrustNode::getConflictProven(Node conf) { return conf.notNode(); }
+
+Node TrustNode::getLemmaProven(Node lem) { return lem; }
+
+Node TrustNode::getPropExpProven(TNode lit, Node exp)
+{
+  return NodeManager::currentNM()->mkNode(kind::IMPLIES, exp, lit);
+}
+
+Node TrustNode::getRewriteProven(TNode n, Node nr) { return n.eqNode(nr); }
+
+void TrustNode::debugCheckClosed(const char* c,
+                                 const char* ctx,
+                                 bool reqNullGen)
+{
+  pfgEnsureClosed(d_proven, d_gen, c, ctx, reqNullGen);
+}
+
+std::string TrustNode::identifyGenerator() const
+{
+  if (d_gen == nullptr)
+  {
+    return "null";
+  }
+  return d_gen->identify();
+}
+
+std::ostream& operator<<(std::ostream& out, TrustNode n)
+{
+  out << "(" << n.getKind() << " " << n.getProven() << " "
+      << n.identifyGenerator() << ")";
+  return out;
+}
+
+}  // namespace theory
+}  // namespace cvc5