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
|
/******************************************************************************
* Top contributors (to current version):
* Andres Noetzli, Andrew Reynolds, Dejan Jovanovic
*
* 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 Rewriter class.
*/
#include "cvc5_private.h"
#pragma once
#include "expr/node.h"
#include "theory/theory_rewriter.h"
namespace cvc5 {
class Env;
class TConvProofGenerator;
class ProofNodeManager;
class TrustNode;
namespace theory {
class Evaluator;
/**
* The main rewriter class.
*/
class Rewriter {
friend class cvc5::Env; // to set the resource manager
public:
Rewriter();
/**
* !!! Temporary until static access to rewriter is eliminated.
*
* Rewrites the node using theoryOf() to determine which rewriter to
* use on the node.
*/
static Node rewrite(TNode node);
/**
* !!! Temporary until static access to rewriter is eliminated.
*/
static Node callExtendedRewrite(TNode node, bool aggr = true);
/**
* Rewrites the equality node using theoryOf() to determine which rewriter to
* use on the node corresponding to an equality s = t.
*
* Specifically, this method performs rewrites whose conclusion is not
* necessarily one of { s = t, t = s, true, false }, which is an invariant
* guaranted by the above method. This invariant is motivated by theory
* combination, which needs to guarantee that equalities between terms
* can be communicated for all pairs of terms.
*/
Node rewriteEqualityExt(TNode node);
/**
* !!! Temporary until static access to rewriter is eliminated. This method
* should be moved to same place as evaluate (currently in Env).
*
* Extended rewrite of the given node. This method is implemented by a
* custom ExtendRewriter class that wraps this class to perform custom
* rewrites (usually those that are not useful for solving, but e.g. useful
* for SyGuS symmetry breaking).
* @param node The node to rewrite
* @param aggr Whether to perform aggressive rewrites.
*/
Node extendedRewrite(TNode node, bool aggr = true);
/**
* Rewrite with proof production, which is managed by the term conversion
* proof generator managed by this class (d_tpg). This method requires a call
* to setProofNodeManager prior to this call.
*
* @param node The node to rewrite.
* @param isExtEq Whether node is an equality which we are applying
* rewriteEqualityExt on.
* @return The trust node of kind TrustNodeKind::REWRITE that contains the
* rewritten form of node.
*/
TrustNode rewriteWithProof(TNode node,
bool isExtEq = false);
/** Set proof node manager */
void setProofNodeManager(ProofNodeManager* pnm);
/** Garbage collects the rewrite caches. */
void clearCaches();
/**
* Registers a theory rewriter with this rewriter. The rewriter does not own
* the theory rewriters.
*
* @param tid The theory that the theory rewriter should be associated with.
* @param trew The theory rewriter to register.
*/
void registerTheoryRewriter(theory::TheoryId tid, TheoryRewriter* trew);
/** Get the theory rewriter for the given id */
TheoryRewriter* getTheoryRewriter(theory::TheoryId theoryId);
private:
/**
* Get the rewriter associated with the SolverEngine in scope.
*
* TODO(#3468): Get rid of this function (it relies on there being an
* singleton with the current SolverEngine in scope)
*/
static Rewriter* getInstance();
/** Returns the appropriate cache for a node */
Node getPreRewriteCache(theory::TheoryId theoryId, TNode node);
/** Returns the appropriate cache for a node */
Node getPostRewriteCache(theory::TheoryId theoryId, TNode node);
/** Sets the appropriate cache for a node */
void setPreRewriteCache(theory::TheoryId theoryId, TNode node, TNode cache);
/** Sets the appropriate cache for a node */
void setPostRewriteCache(theory::TheoryId theoryId, TNode node, TNode cache);
/**
* Rewrites the node using the given theory rewriter.
*/
Node rewriteTo(theory::TheoryId theoryId,
Node node,
TConvProofGenerator* tcpg = nullptr);
/** Calls the pre-rewriter for the given theory */
RewriteResponse preRewrite(theory::TheoryId theoryId,
TNode n,
TConvProofGenerator* tcpg = nullptr);
/** Calls the post-rewriter for the given theory */
RewriteResponse postRewrite(theory::TheoryId theoryId,
TNode n,
TConvProofGenerator* tcpg = nullptr);
/** processes a trust rewrite response */
RewriteResponse processTrustRewriteResponse(
theory::TheoryId theoryId,
const TrustRewriteResponse& tresponse,
bool isPre,
TConvProofGenerator* tcpg);
/**
* Calls the equality-rewriter for the given theory.
*/
Node callRewriteEquality(theory::TheoryId theoryId, TNode equality);
void clearCachesInternal();
/** The resource manager, for tracking resource usage */
ResourceManager* d_resourceManager;
/** Theory rewriters used by this rewriter instance */
TheoryRewriter* d_theoryRewriters[theory::THEORY_LAST];
/** The proof generator */
std::unique_ptr<TConvProofGenerator> d_tpg;
#ifdef CVC5_ASSERTIONS
std::unique_ptr<std::unordered_set<Node>> d_rewriteStack = nullptr;
#endif /* CVC5_ASSERTIONS */
};/* class Rewriter */
} // namespace theory
} // namespace cvc5
|
