GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/rewriter.h Lines: 1 1 100.0 %
Date: 2021-03-23 Branches: 12 16 75.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file rewriter.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andres Noetzli, Andrew Reynolds, Dejan Jovanovic
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief The Rewriter class
13
 **
14
 ** The Rewriter class.
15
 **/
16
17
#include "cvc4_private.h"
18
19
#pragma once
20
21
#include "expr/node.h"
22
#include "theory/theory_rewriter.h"
23
24
namespace CVC4 {
25
26
class TConvProofGenerator;
27
class ProofNodeManager;
28
29
namespace theory {
30
31
class TrustNode;
32
33
namespace builtin {
34
class BuiltinProofRuleChecker;
35
}
36
37
/**
38
 * The rewrite environment holds everything that the individual rewrites have
39
 * access to.
40
 */
41
class RewriteEnvironment
42
{
43
};
44
45
/**
46
 * The identity rewrite just returns the original node.
47
 *
48
 * @param re The rewrite environment
49
 * @param n The node to rewrite
50
 * @return The original node
51
 */
52
RewriteResponse identityRewrite(RewriteEnvironment* re, TNode n);
53
54
/**
55
 * The main rewriter class.
56
 */
57
9601
class Rewriter {
58
  friend builtin::BuiltinProofRuleChecker;
59
60
 public:
61
  Rewriter();
62
63
  /**
64
   * Rewrites the node using theoryOf() to determine which rewriter to
65
   * use on the node.
66
   */
67
  static Node rewrite(TNode node);
68
69
  /**
70
   * Rewrites the equality node using theoryOf() to determine which rewriter to
71
   * use on the node corresponding to an equality s = t.
72
   *
73
   * Specifically, this method performs rewrites whose conclusion is not
74
   * necessarily one of { s = t, t = s, true, false }, which is an invariant
75
   * guaranted by the above method. This invariant is motivated by theory
76
   * combination, which needs to guarantee that equalities between terms
77
   * can be communicated for all pairs of terms.
78
   */
79
  static Node rewriteEqualityExt(TNode node);
80
81
  /**
82
   * Rewrite with proof production, which is managed by the term conversion
83
   * proof generator managed by this class (d_tpg). This method requires a call
84
   * to setProofNodeManager prior to this call.
85
   *
86
   * @param node The node to rewrite.
87
   * @param isExtEq Whether node is an equality which we are applying
88
   * rewriteEqualityExt on.
89
   * @return The trust node of kind TrustNodeKind::REWRITE that contains the
90
   * rewritten form of node.
91
   */
92
  TrustNode rewriteWithProof(TNode node,
93
                             bool isExtEq = false);
94
95
  /** Set proof node manager */
96
  void setProofNodeManager(ProofNodeManager* pnm);
97
98
  /**
99
   * Garbage collects the rewrite caches.
100
   */
101
  static void clearCaches();
102
103
  /**
104
   * Registers a theory rewriter with this rewriter. The rewriter does not own
105
   * the theory rewriters.
106
   *
107
   * @param tid The theory that the theory rewriter should be associated with.
108
   * @param trew The theory rewriter to register.
109
   */
110
  static void registerTheoryRewriter(theory::TheoryId tid,
111
                                     TheoryRewriter* trew);
112
113
  /**
114
   * Register a prerewrite for a given kind.
115
   *
116
   * @param k The kind to register a rewrite for.
117
   * @param fn The function that performs the rewrite.
118
   */
119
  void registerPreRewrite(
120
      Kind k, std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn);
121
122
  /**
123
   * Register a postrewrite for a given kind.
124
   *
125
   * @param k The kind to register a rewrite for.
126
   * @param fn The function that performs the rewrite.
127
   */
128
  void registerPostRewrite(
129
      Kind k, std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn);
130
131
  /**
132
   * Register a prerewrite for equalities belonging to a given theory.
133
   *
134
   * @param tid The theory to register a rewrite for.
135
   * @param fn The function that performs the rewrite.
136
   */
137
  void registerPreRewriteEqual(
138
      theory::TheoryId tid,
139
      std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn);
140
141
  /**
142
   * Register a postrewrite for equalities belonging to a given theory.
143
   *
144
   * @param tid The theory to register a rewrite for.
145
   * @param fn The function that performs the rewrite.
146
   */
147
  void registerPostRewriteEqual(
148
      theory::TheoryId tid,
149
      std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn);
150
151
 private:
152
  /**
153
   * Get the rewriter associated with the SmtEngine in scope.
154
   *
155
   * TODO(#3468): Get rid of this function (it relies on there being an
156
   * singleton with the current SmtEngine in scope)
157
   */
158
  static Rewriter* getInstance();
159
160
  /** Returns the appropriate cache for a node */
161
  Node getPreRewriteCache(theory::TheoryId theoryId, TNode node);
162
163
  /** Returns the appropriate cache for a node */
164
  Node getPostRewriteCache(theory::TheoryId theoryId, TNode node);
165
166
  /** Sets the appropriate cache for a node */
167
  void setPreRewriteCache(theory::TheoryId theoryId, TNode node, TNode cache);
168
169
  /** Sets the appropriate cache for a node */
170
  void setPostRewriteCache(theory::TheoryId theoryId, TNode node, TNode cache);
171
172
  /**
173
   * Rewrites the node using the given theory rewriter.
174
   */
175
  Node rewriteTo(theory::TheoryId theoryId,
176
                 Node node,
177
                 TConvProofGenerator* tcpg = nullptr);
178
179
  /** Calls the pre-rewriter for the given theory */
180
  RewriteResponse preRewrite(theory::TheoryId theoryId,
181
                             TNode n,
182
                             TConvProofGenerator* tcpg = nullptr);
183
184
  /** Calls the post-rewriter for the given theory */
185
  RewriteResponse postRewrite(theory::TheoryId theoryId,
186
                              TNode n,
187
                              TConvProofGenerator* tcpg = nullptr);
188
  /** processes a trust rewrite response */
189
  RewriteResponse processTrustRewriteResponse(
190
      theory::TheoryId theoryId,
191
      const TrustRewriteResponse& tresponse,
192
      bool isPre,
193
      TConvProofGenerator* tcpg);
194
195
  /**
196
   * Calls the equality-rewriter for the given theory.
197
   */
198
  Node callRewriteEquality(theory::TheoryId theoryId, TNode equality);
199
200
  void clearCachesInternal();
201
202
  /** Theory rewriters used by this rewriter instance */
203
  TheoryRewriter* d_theoryRewriters[theory::THEORY_LAST];
204
205
  /** Rewriter table for prewrites. Maps kinds to rewriter function. */
206
  std::function<RewriteResponse(RewriteEnvironment*, TNode)>
207
      d_preRewriters[kind::LAST_KIND];
208
  /** Rewriter table for postrewrites. Maps kinds to rewriter function. */
209
  std::function<RewriteResponse(RewriteEnvironment*, TNode)>
210
      d_postRewriters[kind::LAST_KIND];
211
  /**
212
   * Rewriter table for prerewrites of equalities. Maps theory to rewriter
213
   * function.
214
   */
215
  std::function<RewriteResponse(RewriteEnvironment*, TNode)>
216
      d_preRewritersEqual[theory::THEORY_LAST];
217
  /**
218
   * Rewriter table for postrewrites of equalities. Maps theory to rewriter
219
   * function.
220
   */
221
  std::function<RewriteResponse(RewriteEnvironment*, TNode)>
222
      d_postRewritersEqual[theory::THEORY_LAST];
223
224
  RewriteEnvironment d_re;
225
226
  /** The proof generator */
227
  std::unique_ptr<TConvProofGenerator> d_tpg;
228
#ifdef CVC4_ASSERTIONS
229
  std::unique_ptr<std::unordered_set<Node, NodeHashFunction>> d_rewriteStack =
230
      nullptr;
231
#endif /* CVC4_ASSERTIONS */
232
};/* class Rewriter */
233
234
}/* CVC4::theory namespace */
235
}/* CVC4 namespace */