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
|
/********************* */
/*! \file proof_checker.h
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2019 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"
namespace CVC4 {
namespace theory {
/** Identifiers for rewriters and substitutions.
*
* 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
*/
enum class MethodId : uint32_t
{
//---------------------------- Rewriters
// Rewriter::rewrite(n)
RW_REWRITE,
// Rewriter::rewriteExtEquality(n)
RW_REWRITE_EQ_EXT,
// identity
RW_IDENTITY,
//---------------------------- Substitutions
// (= x y) is interpreted as x -> y, using Node::substitute(...)
SB_DEFAULT,
// (= x y) is interpreted as (= x y) -> true, using Node::substitute(...)
SB_PREDICATE,
};
/** 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 witness form). This encapsulates the exact behavior
* of a REWRITE step in a proof. Rewriting is performed on the Skolem form of
* n.
*
* @param n The node (in witness form) to rewrite,
* @param id The identifier of the rewriter.
* @return The rewritten form of n.
*/
static Node applyRewrite(Node n, MethodId idr = MethodId::RW_REWRITE);
/**
* Apply small-step rewrite on n in witness form (either pre- or
* post-rewrite). This encapsulates the exact behavior of a THEORY_REWRITE
* step in a proof. Rewriting is performed on the Skolem form of n.
*
* @param n The node (in skolem form) to rewrite
* @param preRewrite If true, performs a pre-rewrite or a post-rewrite
* otherwise
* @return The rewritten form of n
*/
static Node applyTheoryRewrite(Node n, bool preRewrite);
/**
* Apply substitution on n (in witness form). This encapsulates the exact
* behavior of a SUBS step in a proof. Substitution is on the Skolem form of
* n.
*
* @param n The node (in witness form) to substitute,
* @param exp The (set of) equalities (in witness form) corresponding to the
* 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 (in witness form) to substitute and rewrite,
* @param exp The (set of) equalities (in witness form) corresponding to the
* substitution
* @param id The identifier of the rewriter.
* @return The substituted, rewritten form of n.
*/
static Node applySubstitutionRewrite(Node n,
const std::vector<Node>& exp,
MethodId ids = MethodId::SB_DEFAULT,
MethodId idr = MethodId::RW_REWRITE);
/** get a rewriter Id from a node, return false if we fail */
static bool getMethodId(TNode n, MethodId& i);
/** 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;
/** get method ids */
bool getMethodIds(const std::vector<Node>& args,
MethodId& ids,
MethodId& idr,
size_t index);
/**
* Apply rewrite (on Skolem form). id is the identifier of the rewriter.
*/
static Node applyRewriteExternal(Node n, MethodId idr = MethodId::RW_REWRITE);
/**
* Apply substitution for n (on Skolem form), where exp is an equality
* (or set of equalities) in Witness form. Returns the result of
* n * { exp[0] -> exp[1] } in Skolem form.
*/
static Node applySubstitutionExternal(Node n, Node exp, MethodId ids);
static Node applySubstitutionExternal(Node n,
const std::vector<Node>& exp,
MethodId ids);
};
} // namespace builtin
} // namespace theory
} // namespace CVC4
#endif /* CVC4__THEORY__BUILTIN__PROOF_CHECKER_H */
|
