GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/proof_checker.h Lines: 4 5 80.0 %
Date: 2021-03-23 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file proof_checker.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, 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 checker utility
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__EXPR__PROOF_CHECKER_H
18
#define CVC4__EXPR__PROOF_CHECKER_H
19
20
#include <map>
21
22
#include "expr/node.h"
23
#include "expr/proof_rule.h"
24
#include "util/statistics_registry.h"
25
#include "util/stats_histogram.h"
26
27
namespace CVC4 {
28
29
class ProofChecker;
30
class ProofNode;
31
32
/** A virtual base class for checking a proof rule */
33
class ProofRuleChecker
34
{
35
 public:
36
76778
  ProofRuleChecker() {}
37
76751
  virtual ~ProofRuleChecker() {}
38
  /**
39
   * This checks a single step in a proof.
40
   *
41
   * Return the formula that is proven by a proof node with the given id,
42
   * premises and arguments, or null if such a proof node is not well-formed.
43
   *
44
   * Note that the input/output of this method expects to be terms in *Skolem
45
   * form*, which is passed to checkInternal below. Rule checkers may
46
   * convert premises to witness form when necessary.
47
   *
48
   * @param id The id of the proof node to check
49
   * @param children The premises of the proof node to check. These are nodes
50
   * corresponding to the conclusion (ProofNode::getResult) of the children
51
   * of the proof node we are checking in Skolem form.
52
   * @param args The arguments of the proof node to check
53
   * @return The conclusion of the proof node, in Skolem form, if successful or
54
   * null if such a proof node is malformed.
55
   */
56
  Node check(PfRule id,
57
             const std::vector<Node>& children,
58
             const std::vector<Node>& args);
59
60
  /** get an index from a node, return false if we fail */
61
  static bool getUInt32(TNode n, uint32_t& i);
62
  /** get a Boolean from a node, return false if we fail */
63
  static bool getBool(TNode n, bool& b);
64
  /** get a Kind from a node, return false if we fail */
65
  static bool getKind(TNode n, Kind& k);
66
  /** Make a Kind into a node */
67
  static Node mkKindNode(Kind k);
68
69
  /** Register all rules owned by this rule checker into pc. */
70
  virtual void registerTo(ProofChecker* pc) {}
71
72
 protected:
73
  /**
74
   * This checks a single step in a proof.
75
   *
76
   * @param id The id of the proof node to check
77
   * @param children The premises of the proof node to check. These are nodes
78
   * corresponding to the conclusion (ProofNode::getResult) of the children
79
   * of the proof node we are checking.
80
   * @param args The arguments of the proof node to check
81
   * @return The conclusion of the proof node if successful or null if such a
82
   * proof node is malformed.
83
   */
84
  virtual Node checkInternal(PfRule id,
85
                             const std::vector<Node>& children,
86
                             const std::vector<Node>& args) = 0;
87
};
88
89
/** Statistics class */
90
class ProofCheckerStatistics
91
{
92
 public:
93
  ProofCheckerStatistics();
94
  ~ProofCheckerStatistics();
95
  /** Counts the number of checks for each kind of proof rule */
96
  IntegralHistogramStat<PfRule> d_ruleChecks;
97
  /** Total number of rule checks */
98
  IntStat d_totalRuleChecks;
99
};
100
101
/** A class for checking proofs */
102
class ProofChecker
103
{
104
 public:
105
962
  ProofChecker(uint32_t pclevel = 0) : d_pclevel(pclevel) {}
106
962
  ~ProofChecker() {}
107
  /**
108
   * Return the formula that is proven by proof node pn, or null if pn is not
109
   * well-formed. If expected is non-null, then we return null if pn does not
110
   * prove expected.
111
   *
112
   * @param pn The proof node to check
113
   * @param expected The (optional) formula that is the expected conclusion of
114
   * the proof node.
115
   * @return The conclusion of the proof node if successful or null if the
116
   * proof is malformed, or if no checker is available for id.
117
   */
118
  Node check(ProofNode* pn, Node expected = Node::null());
119
  /** Same as above, with explicit arguments
120
   *
121
   * @param id The id of the proof node to check
122
   * @param children The children of the proof node to check
123
   * @param args The arguments of the proof node to check
124
   * @param expected The (optional) formula that is the expected conclusion of
125
   * the proof node.
126
   * @return The conclusion of the proof node if successful or null if the
127
   * proof is malformed, or if no checker is available for id.
128
   */
129
  Node check(PfRule id,
130
             const std::vector<std::shared_ptr<ProofNode>>& children,
131
             const std::vector<Node>& args,
132
             Node expected = Node::null());
133
  /**
134
   * Same as above, without conclusions instead of proof node children. This
135
   * is used for debugging. In particular, this function does not throw an
136
   * assertion failure when a proof step is malformed and can be used without
137
   * constructing proof nodes.
138
   *
139
   * @param id The id of the proof node to check
140
   * @param children The conclusions of the children of the proof node to check
141
   * @param args The arguments of the proof node to check
142
   * @param expected The (optional) formula that is the expected conclusion of
143
   * the proof node.
144
   * @param traceTag The trace tag to print debug information to
145
   * @return The conclusion of the proof node if successful or null if the
146
   * proof is malformed, or if no checker is available for id.
147
   */
148
  Node checkDebug(PfRule id,
149
                  const std::vector<Node>& cchildren,
150
                  const std::vector<Node>& args,
151
                  Node expected = Node::null(),
152
                  const char* traceTag = "");
153
  /** Indicate that psc is the checker for proof rule id */
154
  void registerChecker(PfRule id, ProofRuleChecker* psc);
155
  /**
156
   * Indicate that id is a trusted rule with the given pedantic level, e.g.:
157
   *  0: (mandatory) always a failure to use the given id
158
   *  1: (major) failure on all (non-zero) pedantic levels
159
   * 10: (minor) failure only on pedantic levels >= 10.
160
   */
161
  void registerTrustedChecker(PfRule id,
162
                              ProofRuleChecker* psc,
163
                              uint32_t plevel = 10);
164
  /** get checker for */
165
  ProofRuleChecker* getCheckerFor(PfRule id);
166
167
  /**
168
   * Get the pedantic level for id if it has been assigned a pedantic
169
   * level via registerTrustedChecker above, or zero otherwise.
170
   */
171
  uint32_t getPedanticLevel(PfRule id) const;
172
173
  /**
174
   * Is pedantic failure? If so, we return true and write a debug message on the
175
   * output stream out if enableOutput is true.
176
   */
177
  bool isPedanticFailure(PfRule id,
178
                         std::ostream& out,
179
                         bool enableOutput = true) const;
180
181
 private:
182
  /** statistics class */
183
  ProofCheckerStatistics d_stats;
184
  /** Maps proof rules to their checker */
185
  std::map<PfRule, ProofRuleChecker*> d_checker;
186
  /** Maps proof trusted rules to their pedantic level */
187
  std::map<PfRule, uint32_t> d_plevel;
188
  /** The pedantic level of this checker */
189
  uint32_t d_pclevel;
190
  /**
191
   * Check internal. This is used by check and checkDebug above. It writes
192
   * checking errors on out when enableOutput is true. We treat trusted checkers
193
   * (nullptr in the range of the map d_checker) as failures if
194
   * useTrustedChecker = false.
195
   */
196
  Node checkInternal(PfRule id,
197
                     const std::vector<Node>& cchildren,
198
                     const std::vector<Node>& args,
199
                     Node expected,
200
                     std::stringstream& out,
201
                     bool useTrustedChecker,
202
                     bool enableOutput);
203
};
204
205
}  // namespace CVC4
206
207
#endif /* CVC4__EXPR__PROOF_CHECKER_H */