--- /dev/null
+/********************* */
+/*! \file trust_node.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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.\endverbatim
+ **
+ ** \brief Implementation of the trust node utility
+ **/
+
+#include "theory/trust_node.h"
+
+#include "expr/proof_generator.h"
+
+namespace CVC4 {
+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";
+ 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::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
+{
+ return d_tnk == TrustNodeKind::LEMMA ? d_proven : 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(); }
+
+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);
+}
+
+std::ostream& operator<<(std::ostream& out, TrustNode n)
+{
+ out << "(trust " << n.getNode() << ")";
+ return out;
+}
+
+} // namespace theory
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file trust_node.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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.\endverbatim
+ **
+ ** \brief The trust node utility
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__TRUST_NODE_H
+#define CVC4__THEORY__TRUST_NODE_H
+
+#include "expr/node.h"
+
+namespace CVC4 {
+
+class ProofGenerator;
+
+namespace theory {
+
+/** A kind for trust nodes */
+enum class TrustNodeKind : uint32_t
+{
+ CONFLICT,
+ LEMMA,
+ PROP_EXP,
+ 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);
+ /** 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, or
+ * (3) A conjunction of literals exp to return in Theory::explain(lit).
+ *
+ * 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.
+ *
+ * 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;
+
+ /** 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);
+
+ 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 CVC4
+
+#endif /* CVC4__THEORY__TRUST_NODE_H */
projects / cvc5.git / commitdiff