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