GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/proof_node_manager.h Lines: 1 1 100.0 %
Date: 2021-03-22 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file proof_node_manager.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Haniel Barbosa, Gereon Kremer
6
 ** This file is part of the CVC4 project.
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.\endverbatim
11
 **
12
 ** \brief Proof node manager utility
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__EXPR__PROOF_NODE_MANAGER_H
18
#define CVC4__EXPR__PROOF_NODE_MANAGER_H
19
20
#include <vector>
21
22
#include "expr/node.h"
23
#include "expr/proof_rule.h"
24
25
namespace CVC4 {
26
27
class ProofChecker;
28
class ProofNode;
29
30
/**
31
 * A manager for proof node objects. This is a trusted interface for creating
32
 * and updating ProofNode objects.
33
 *
34
 * In more detail, we say a ProofNode is "well-formed (with respect to checker
35
 * X)" if its d_proven field is non-null, and corresponds to the formula that
36
 * the ProofNode proves according to X. The ProofNodeManager class constructs
37
 * and update nodes that are well-formed with respect to its underlying checker.
38
 *
39
 * If no checker is provided, then the ProofNodeManager assigns the d_proven
40
 * field of ProofNode based on the provided "expected" argument in mkNode below,
41
 * which must be provided in this case.
42
 *
43
 * The ProofNodeManager is used as a trusted way of updating ProofNode objects
44
 * via updateNode below. In particular, this method leaves the d_proven field
45
 * unchanged and updates (if possible) the remaining content of a given proof
46
 * node.
47
 *
48
 * Notice that ProofNode objects are mutable, and hence this class does not
49
 * cache the results of mkNode. A version of this class that caches
50
 * immutable version of ProofNode objects could be built as an extension
51
 * or layer on top of this class.
52
 */
53
class ProofNodeManager
54
{
55
 public:
56
  ProofNodeManager(ProofChecker* pc = nullptr);
57
962
  ~ProofNodeManager() {}
58
  /**
59
   * This constructs a ProofNode with the given arguments. The expected
60
   * argument, when provided, indicates the formula that the returned node
61
   * is expected to prove. If we find that it does not, based on the underlying
62
   * checker, this method returns nullptr.
63
   *
64
   * @param id The id of the proof node.
65
   * @param children The children of the proof node.
66
   * @param args The arguments of the proof node.
67
   * @param expected (Optional) the expected conclusion of the proof node.
68
   * @return the proof node, or nullptr if the given arguments do not
69
   * consistute a proof of the expected conclusion according to the underlying
70
   * checker, if both are provided. It also returns nullptr if neither the
71
   * checker nor the expected field is provided, since in this case the
72
   * conclusion is unknown.
73
   */
74
  std::shared_ptr<ProofNode> mkNode(
75
      PfRule id,
76
      const std::vector<std::shared_ptr<ProofNode>>& children,
77
      const std::vector<Node>& args,
78
      Node expected = Node::null());
79
  /**
80
   * Make the proof node corresponding to the assumption of fact.
81
   *
82
   * @param fact The fact to assume.
83
   * @return The ASSUME proof of fact.
84
   */
85
  std::shared_ptr<ProofNode> mkAssume(Node fact);
86
  /**
87
   * Make transitivity proof, where children contains one or more proofs of
88
   * equalities that form an ordered chain. In other words, the vector children
89
   * is a legal set of children for an application of TRANS.
90
   */
91
  std::shared_ptr<ProofNode> mkTrans(
92
      const std::vector<std::shared_ptr<ProofNode>>& children,
93
      Node expected = Node::null());
94
95
  /**
96
   * Make scope having body pf and arguments (assumptions-to-close) assumps.
97
   * If ensureClosed is true, then this method throws an assertion failure if
98
   * the returned proof is not closed. This is the case if a free assumption
99
   * of pf is missing from the vector assumps.
100
   *
101
   * For conveinence, the proof pf may be modified to ensure that the overall
102
   * result is closed. For instance, given input:
103
   *   pf = TRANS( ASSUME( x=y ), ASSUME( y=z ) )
104
   *   assumps = { y=x, y=z }
105
   * This method will modify pf to be:
106
   *   pf = TRANS( SYMM( ASSUME( y=x ) ), ASSUME( y=z ) )
107
   * so that y=x matches the free assumption. The returned proof is:
108
   *   SCOPE(TRANS( SYMM( ASSUME( y=x ) ), ASSUME( y=z ) ) :args { y=x, y=z })
109
   *
110
   * When ensureClosed is true, duplicates are eliminated from assumps. The
111
   * reason for this is due to performance, since in this method, assumps is
112
   * converted to an unordered_set to do the above check and hence it is a
113
   * convienient time to eliminate duplicate literals.
114
   *
115
   * Additionally, if both ensureClosed and doMinimize are true, assumps is
116
   * updated to contain exactly the free asumptions of pf. This also includes
117
   * having no duplicates. Furthermore, if assumps is empty after minimization,
118
   * this method is a no-op.
119
   *
120
   * In each case, the update vector assumps is passed as arguments to SCOPE.
121
   *
122
   * @param pf The body of the proof,
123
   * @param assumps The assumptions-to-close of the scope,
124
   * @param ensureClosed Whether to ensure that the proof is closed,
125
   * @param doMinimize Whether to minimize assumptions.
126
   * @param expected the node that the scope should prove.
127
   * @return The scoped proof.
128
   */
129
  std::shared_ptr<ProofNode> mkScope(std::shared_ptr<ProofNode> pf,
130
                                     std::vector<Node>& assumps,
131
                                     bool ensureClosed = true,
132
                                     bool doMinimize = false,
133
                                     Node expected = Node::null());
134
  /**
135
   * This method updates pn to be a proof of the form <id>( children, args ),
136
   * while maintaining its d_proven field. This method returns false if this
137
   * proof manager is using a checker, and we compute that the above proof
138
   * is not a proof of the fact that pn previously proved.
139
   *
140
   * @param pn The proof node to update.
141
   * @param id The updated id of the proof node.
142
   * @param children The updated children of the proof node.
143
   * @param args The updated arguments of the proof node.
144
   * @return true if the update was successful.
145
   *
146
   * Notice that updateNode always returns true if there is no underlying
147
   * checker.
148
   */
149
  bool updateNode(ProofNode* pn,
150
                  PfRule id,
151
                  const std::vector<std::shared_ptr<ProofNode>>& children,
152
                  const std::vector<Node>& args);
153
  /**
154
   * Update node pn to have the contents of pnr. It should be the case that
155
   * pn and pnr prove the same fact, otherwise false is returned and pn is
156
   * unchanged.
157
   */
158
  bool updateNode(ProofNode* pn, ProofNode* pnr);
159
  /** Get the underlying proof checker */
160
  ProofChecker* getChecker() const;
161
162
 private:
163
  /** The (optional) proof checker */
164
  ProofChecker* d_checker;
165
  /** the true node */
166
  Node d_true;
167
  /** Check internal
168
   *
169
   * This returns the result of proof checking a ProofNode with the provided
170
   * arguments with an expected conclusion, which may not null if there is
171
   * no expected conclusion.
172
   *
173
   * This throws an assertion error if we fail to check such a proof node, or
174
   * if expected is provided (non-null) and is different what is proven by the
175
   * other arguments.
176
   */
177
  Node checkInternal(PfRule id,
178
                     const std::vector<std::shared_ptr<ProofNode>>& children,
179
                     const std::vector<Node>& args,
180
                     Node expected);
181
  /**
182
   * Update node internal, return true if successful. This is called by
183
   * the update node methods above. The argument needsCheck is whether we
184
   * need to check the correctness of the rule application. This is false
185
   * for the updateNode routine where pnr is an (already checked) proof node.
186
   */
187
  bool updateNodeInternal(
188
      ProofNode* pn,
189
      PfRule id,
190
      const std::vector<std::shared_ptr<ProofNode>>& children,
191
      const std::vector<Node>& args,
192
      bool needsCheck);
193
};
194
195
}  // namespace CVC4
196
197
#endif /* CVC4__EXPR__PROOF_NODE_H */