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
|
/******************************************************************************
* Top contributors (to current version):
* Andres Noetzli, Andrew Reynolds, Morgan Deters
*
* 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.
* ****************************************************************************
*
* The TheoryRewriter class.
*
* The interface that theory rewriters implement.
*/
#include "cvc5_private.h"
#ifndef CVC5__THEORY__THEORY_REWRITER_H
#define CVC5__THEORY__THEORY_REWRITER_H
#include "expr/node.h"
#include "theory/trust_node.h"
namespace cvc5 {
namespace theory {
class Rewriter;
/**
* Theory rewriters signal whether more rewriting is needed (or not)
* by using a member of this enumeration. See RewriteResponse, below.
*/
enum RewriteStatus
{
/** The node is fully rewritten (no more rewrites apply) */
REWRITE_DONE,
/** The node may be rewritten further */
REWRITE_AGAIN,
/** Subnodes of the node may be rewritten further */
REWRITE_AGAIN_FULL
}; /* enum RewriteStatus */
/**
* Instances of this class serve as response codes from
* TheoryRewriter::preRewrite() and TheoryRewriter::postRewrite(). The response
* consists of the rewritten node as well as a status that indicates whether
* more rewriting is needed or not.
*/
struct RewriteResponse
{
const RewriteStatus d_status;
const Node d_node;
RewriteResponse(RewriteStatus status, Node n) : d_status(status), d_node(n) {}
}; /* struct RewriteResponse */
/** Same as above, with trust node instead of node. */
struct TrustRewriteResponse
{
TrustRewriteResponse(RewriteStatus status,
Node n,
Node nr,
ProofGenerator* pg);
/** The status of the rewrite */
const RewriteStatus d_status;
/**
* The trust node corresponding to the rewrite.
*/
TrustNode d_node;
};
/**
* The interface that a theory rewriter has to implement.
*
* Note: A theory rewriter is expected to handle all kinds of a theory, even
* the ones that are removed by `Theory::expandDefinition()` since it may be
* called on terms before the definitions have been expanded.
*/
class TheoryRewriter
{
public:
virtual ~TheoryRewriter() = default;
/**
* Registers the rewrites of a given theory with the rewriter.
*
* @param rewriter The rewriter to register the rewrites with.
*/
virtual void registerRewrites(Rewriter* rewriter) {}
/**
* Performs a pre-rewrite step.
*
* @param node The node to rewrite
*/
virtual RewriteResponse postRewrite(TNode node) = 0;
/**
* Performs a pre-rewrite step, with proofs.
*
* @param node The node to rewrite
*/
virtual TrustRewriteResponse postRewriteWithProof(TNode node);
/**
* Performs a post-rewrite step.
*
* @param node The node to rewrite
*/
virtual RewriteResponse preRewrite(TNode node) = 0;
/**
* Performs a pre-rewrite step, with proofs.
*
* @param node The node to rewrite
*/
virtual TrustRewriteResponse preRewriteWithProof(TNode node);
/** rewrite equality extended
*
* This method returns a formula that is equivalent to the equality between
* two terms s = t, given by node.
*
* Specifically, this method performs rewrites whose conclusion is not
* necessarily one of { s = t, t = s, true, false }. This is in constrast
* to postRewrite and preRewrite above, where the rewritten form of an
* equality must be one of these.
*
* @param node The node to rewrite
*/
virtual Node rewriteEqualityExt(Node node);
/** rewrite equality extended, with proofs
*
* @param node The node to rewrite
* @return A trust node of kind TrustNodeKind::REWRITE, or the null trust
* node if no rewrites are applied.
*/
virtual TrustNode rewriteEqualityExtWithProof(Node node);
/**
* Expand definitions in the term node. This returns a term that is
* equivalent to node. It wraps this term in a TrustNode of kind
* TrustNodeKind::REWRITE. If node is unchanged by this method, the
* null TrustNode may be returned. This is an optimization to avoid
* constructing the trivial equality (= node node) internally within
* TrustNode.
*
* The purpose of this method is typically to eliminate the operators in node
* that are syntax sugar that cannot otherwise be eliminated during rewriting.
* For example, division relies on the introduction of an uninterpreted
* function for the divide-by-zero case, which we do not introduce with
* the standard rewrite methods.
*
* Some theories have kinds that are effectively definitions and should be
* expanded before they are handled. Definitions allow a much wider range of
* actions than the normal forms given by the rewriter. However no
* assumptions can be made about subterms having been expanded or rewritten.
* Where possible rewrite rules should be used, definitions should only be
* used when rewrites are not possible, for example in handling
* under-specified operations using partially defined functions.
*/
virtual TrustNode expandDefinition(Node node);
};
} // namespace theory
} // namespace cvc5
#endif /* CVC5__THEORY__THEORY_REWRITER_H */
|
