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
|
/********************* */
/*! \file proof_checker.h
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 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.\endverbatim
**
** \brief Equality proof checker utility
**/
#include "cvc4_private.h"
#ifndef CVC4__THEORY__BUILTIN__PROOF_CHECKER_H
#define CVC4__THEORY__BUILTIN__PROOF_CHECKER_H
#include "expr/node.h"
#include "expr/proof_checker.h"
#include "expr/proof_node.h"
#include "theory/quantifiers/extended_rewrite.h"
namespace CVC4 {
namespace theory {
/**
* Identifiers for rewriters and substitutions, which we abstractly
* classify as "methods". Methods have a unique identifier in the internal
* proof calculus implemented by the checker below.
*
* A "rewriter" is abstractly a method from Node to Node, where the output
* is semantically equivalent to the input. The identifiers below list
* various methods that have this contract. This identifier is used
* in a number of the builtin rules.
*
* A substitution is a method for turning a formula into a substitution.
*/
enum class MethodId : uint32_t
{
//---------------------------- Rewriters
// Rewriter::rewrite(n)
RW_REWRITE,
// d_ext_rew.extendedRewrite(n);
RW_EXT_REWRITE,
// Rewriter::rewriteExtEquality(n)
RW_REWRITE_EQ_EXT,
// Evaluator::evaluate(n)
RW_EVALUATE,
// identity
RW_IDENTITY,
// theory preRewrite, note this is only intended to be used as an argument
// to THEORY_REWRITE in the final proof. It is not implemented in
// applyRewrite below, see documentation in proof_rule.h for THEORY_REWRITE.
RW_REWRITE_THEORY_PRE,
// same as above, for theory postRewrite
RW_REWRITE_THEORY_POST,
//---------------------------- Substitutions
// (= x y) is interpreted as x -> y, using Node::substitute
SB_DEFAULT,
// P, (not P) are interpreted as P -> true, P -> false using Node::substitute
SB_LITERAL,
// P is interpreted as P -> true using Node::substitute
SB_FORMULA,
};
/** Converts a rewriter id to a string. */
const char* toString(MethodId id);
/** Write a rewriter id to out */
std::ostream& operator<<(std::ostream& out, MethodId id);
/** Make a method id node */
Node mkMethodId(MethodId id);
namespace builtin {
/** A checker for builtin proofs */
class BuiltinProofRuleChecker : public ProofRuleChecker
{
public:
BuiltinProofRuleChecker() {}
~BuiltinProofRuleChecker() {}
/**
* Apply rewrite on n (in skolem form). This encapsulates the exact behavior
* of a REWRITE step in a proof.
*
* @param n The node to rewrite,
* @param idr The method identifier of the rewriter, by default RW_REWRITE
* specifying a call to Rewriter::rewrite.
* @return The rewritten form of n.
*/
Node applyRewrite(Node n, MethodId idr = MethodId::RW_REWRITE);
/**
* Get substitution for literal exp. Updates vars/subs to the substitution
* specified by exp for the substitution method ids.
*/
static bool getSubstitutionForLit(Node exp,
TNode& var,
TNode& subs,
MethodId ids = MethodId::SB_DEFAULT);
/**
* Get substitution for formula exp. Adds to vars/subs to the substitution
* specified by exp for the substitution method ids, which may be multiple
* substitutions if exp is of kind AND and ids is SB_DEFAULT (note the other
* substitution types always interpret applications of AND as a formula).
* The vector "from" are the literals from exp that each substitution in
* vars/subs are based on. For example, if exp is (and (= x t) (= y s)), then
* vars = { x, y }, subs = { t, s }, from = { (= x y), (= y s) }.
*/
static bool getSubstitutionFor(Node exp,
std::vector<TNode>& vars,
std::vector<TNode>& subs,
std::vector<TNode>& from,
MethodId ids = MethodId::SB_DEFAULT);
/**
* Apply substitution on n in skolem form. This encapsulates the exact
* behavior of a SUBS step in a proof.
*
* @param n The node to substitute,
* @param exp The (set of) equalities/literals/formulas that the substitution
* is derived from
* @param ids The method identifier of the substitution, by default SB_DEFAULT
* specifying that lhs/rhs of equalities are interpreted as a substitution.
* @return The substituted form of n.
*/
static Node applySubstitution(Node n,
Node exp,
MethodId ids = MethodId::SB_DEFAULT);
static Node applySubstitution(Node n,
const std::vector<Node>& exp,
MethodId ids = MethodId::SB_DEFAULT);
/** Apply substitution + rewriting
*
* Combines the above two steps.
*
* @param n The node to substitute and rewrite,
* @param exp The (set of) equalities corresponding to the substitution
* @param ids The method identifier of the substitution.
* @param idr The method identifier of the rewriter.
* @return The substituted, rewritten form of n.
*/
Node applySubstitutionRewrite(Node n,
const std::vector<Node>& exp,
MethodId ids = MethodId::SB_DEFAULT,
MethodId idr = MethodId::RW_REWRITE);
/** get a method identifier from a node, return false if we fail */
static bool getMethodId(TNode n, MethodId& i);
/**
* Get method identifiers from args starting at the given index. Store their
* values into ids, idr. This method returns false if args does not contain
* valid method identifiers at position index in args.
*/
bool getMethodIds(const std::vector<Node>& args,
MethodId& ids,
MethodId& idr,
size_t index);
/**
* Add method identifiers ids and idr as nodes to args. This does not add ids
* or idr if their values are the default ones.
*/
static void addMethodIds(std::vector<Node>& args, MethodId ids, MethodId idr);
/** get a TheoryId from a node, return false if we fail */
static bool getTheoryId(TNode n, TheoryId& tid);
/** Make a TheoryId into a node */
static Node mkTheoryIdNode(TheoryId tid);
/** Register all rules owned by this rule checker into pc. */
void registerTo(ProofChecker* pc) override;
protected:
/** Return the conclusion of the given proof step, or null if it is invalid */
Node checkInternal(PfRule id,
const std::vector<Node>& children,
const std::vector<Node>& args) override;
/** extended rewriter object */
quantifiers::ExtendedRewriter d_ext_rewriter;
};
} // namespace builtin
} // namespace theory
} // namespace CVC4
#endif /* CVC4__THEORY__BUILTIN__PROOF_CHECKER_H */
|
