Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/proof/trust_node.h	Lines:	3	3	100.0 %
Date:	2021-09-29	Branches:	0	0	0.0 %


/******************************************************************************
 * 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;

/** 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);
  /** Make a trust node, replacing the original generator */
  static TrustNode mkReplaceGenTrustNode(const TrustNode& orig,
                                         ProofGenerator* g);
  /** 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 cvc5

#endif /* CVC5__PROOF__TRUST_NODE_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Gereon Kremer
4		*
5		* This file is part of the cvc5 project.
6		*
7		* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8		* in the top-level source directory and their institutional affiliations.
9		* All rights reserved. See the file COPYING in the top-level source
10		* directory for licensing information.
11		* ****************************************************************************
12		*
13		* The trust node utility.
14		*/
15
16		#include "cvc5_private.h"
17
18		#ifndef CVC5__PROOF__TRUST_NODE_H
19		#define CVC5__PROOF__TRUST_NODE_H
20
21		#include "expr/node.h"
22
23		namespace cvc5 {
24
25		class ProofGenerator;
26		class ProofNode;
27
28		/** A kind for trust nodes */
29		enum class TrustNodeKind : uint32_t
30		{
31		CONFLICT,
32		LEMMA,
33		PROP_EXP,
34		REWRITE,
35		INVALID
36		};
37		/**
38		* Converts a proof rule to a string. Note: This function is also used in
39		* `safe_print()`. Changing this function name or signature will result in
40		* `safe_print()` printing "<unsupported>" instead of the proper strings for
41		* the enum values.
42		*
43		* Returns a string with static lifetime: it should not be freed.
44		*
45		* @param tnk The trust node kind
46		* @return The name of the trust node kind
47		*/
48		const char* toString(TrustNodeKind tnk);
49
50		/**
51		* Writes a trust node kind name to a stream.
52		*
53		* @param out The stream to write to
54		* @param tnk The trust node kind to write to the stream
55		* @return The stream
56		*/
57		std::ostream& operator<<(std::ostream& out, TrustNodeKind tnk);
58
59		/**
60		* A trust node is a pair (F, G) where F is a formula and G is a proof
61		* generator that can construct a proof for F if asked.
62		*
63		* More generally, a trust node is any node that can be used for a specific
64		* purpose that requires justification, such as being passed to
65		* OutputChannel::lemma. That justification is intended to be given by the
66		* generator that is required to construct this object.
67		*
68		* They are intended to be constructed by ProofGenerator objects themselves (a
69		* proof generator wraps itself in TrustNode it returns) and passed
70		* to ProofOutputChannel by theory solvers.
71		*
72		* The static functions for constructing them check that the generator, if
73		* provided, is capable of proving the given conflict or lemma, or an assertion
74		* failure occurs. Otherwise an assertion error is given.
75		*
76		* While this is not enforced, a `TrustNode` generally encapsulates a closed
77		* proof of the formula: one without free assumptions.
78		*/
79	4235337	class TrustNode
80		{
81		public:
82	1448885	TrustNode() : d_tnk(TrustNodeKind::INVALID), d_gen(nullptr) {}
83		/** Make a proven node for conflict */
84		static TrustNode mkTrustConflict(Node conf, ProofGenerator* g = nullptr);
85		/** Make a proven node for lemma */
86		static TrustNode mkTrustLemma(Node lem, ProofGenerator* g = nullptr);
87		/** Make a proven node for explanation of propagated literal */
88		static TrustNode mkTrustPropExp(TNode lit,
89		Node exp,
90		ProofGenerator* g = nullptr);
91		/** Make a proven node for rewrite */
92		static TrustNode mkTrustRewrite(TNode n,
93		Node nr,
94		ProofGenerator* g = nullptr);
95		/** Make a trust node, replacing the original generator */
96		static TrustNode mkReplaceGenTrustNode(const TrustNode& orig,
97		ProofGenerator* g);
98		/** The null proven node */
99		static TrustNode null();
100	9467441	~TrustNode() {}
101		/** get kind */
102		TrustNodeKind getKind() const;
103		/** get node
104		*
105		* This is the node that is used in a common interface, either:
106		* (1) A T-unsat conjunction conf to pass to OutputChannel::conflict,
107		* (2) A valid T-formula lem to pass to OutputChannel::lemma,
108		* (3) A conjunction of literals exp to return in Theory::explain(lit), or
109		* (4) A result of rewriting a term n into an equivalent one nr.
110		*
111		* Notice that this node does not necessarily correspond to a valid formula.
112		* The call getProven() below retrieves a valid formula corresponding to
113		* the above calls.
114		*/
115		Node getNode() const;
116		/** get proven
117		*
118		* This is the corresponding formula that is proven by the proof generator
119		* for the above cases:
120		* (1) (not conf), for conflicts,
121		* (2) lem, for lemmas,
122		* (3) (=> exp lit), for propagations from explanations,
123		* (4) (= n nr), for results of rewriting.
124		*
125		* When constructing this trust node, the proof generator should be able to
126		* provide a proof for this fact.
127		*/
128		Node getProven() const;
129		/** get generator */
130		ProofGenerator* getGenerator() const;
131		/** is null? */
132		bool isNull() const;
133		/**
134		* Gets the proof node for this trust node, which is obtained by
135		* calling the generator's getProofFor method on the proven node.
136		*/
137		std::shared_ptr<ProofNode> toProofNode() const;
138
139		/** Get the proven formula corresponding to a conflict call */
140		static Node getConflictProven(Node conf);
141		/** Get the proven formula corresponding to a lemma call */
142		static Node getLemmaProven(Node lem);
143		/** Get the proven formula corresponding to explanations for propagation */
144		static Node getPropExpProven(TNode lit, Node exp);
145		/** Get the proven formula corresponding to a rewrite */
146		static Node getRewriteProven(TNode n, Node nr);
147		/** For debugging */
148		std::string identifyGenerator() const;
149
150		/**
151		* debug check closed on Trace c, context ctx is string for debugging
152		*
153		* @param reqNullGen Whether we consider a null generator to be a failure.
154		*/
155		void debugCheckClosed(const char* c, const char* ctx, bool reqNullGen = true);
156
157		private:
158		TrustNode(TrustNodeKind tnk, Node p, ProofGenerator* g = nullptr);
159		/** The kind */
160		TrustNodeKind d_tnk;
161		/** The proven node */
162		Node d_proven;
163		/** The generator */
164		ProofGenerator* d_gen;
165		};
166
167		/**
168		* Writes a trust node to a stream.
169		*
170		* @param out The stream to write to
171		* @param n The trust node to write to the stream
172		* @return The stream
173		*/
174		std::ostream& operator<<(std::ostream& out, TrustNode n);
175
176		} // namespace cvc5
177
178		#endif /* CVC5__PROOF__TRUST_NODE_H */