GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/extended_rewrite.h Lines: 1 1 100.0 %
Date: 2021-03-23 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file extended_rewrite.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner
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 extended rewriting class
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H
18
#define CVC4__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H
19
20
#include <unordered_map>
21
22
#include "expr/node.h"
23
24
namespace CVC4 {
25
namespace theory {
26
namespace quantifiers {
27
28
/** Extended rewriter
29
 *
30
 * This class is used for all rewriting that is not necessarily
31
 * helpful for quantifier-free solving, but is helpful
32
 * in other use cases. An example of this is SyGuS, where rewriting
33
 * can be used for generalizing refinement lemmas, and hence
34
 * should be highly aggressive.
35
 *
36
 * This class extended the standard techniques for rewriting
37
 * with techniques, including but not limited to:
38
 * - Redundant child elimination,
39
 * - Sorting children of commutative operators,
40
 * - Boolean constraint propagation,
41
 * - Equality chain normalization,
42
 * - Negation normal form,
43
 * - Simple ITE pulling,
44
 * - ITE conditional variable elimination,
45
 * - ITE condition subsumption.
46
 */
47
class ExtendedRewriter
48
{
49
 public:
50
  ExtendedRewriter(bool aggr = true);
51
11300
  ~ExtendedRewriter() {}
52
  /** return the extended rewritten form of n */
53
  Node extendedRewrite(Node n);
54
55
 private:
56
  /**
57
   * Whether this extended rewriter applies aggressive rewriting techniques,
58
   * which are more expensive. Examples of aggressive rewriting include:
59
   * - conditional rewriting,
60
   * - condition merging,
61
   * - sorting childing of commutative operators with more than 5 children.
62
   *
63
   * Aggressive rewriting is applied for SyGuS, whereas non-aggressive rewriting
64
   * may be applied as a preprocessing step.
65
   */
66
  bool d_aggr;
67
  /** true/false nodes */
68
  Node d_true;
69
  Node d_false;
70
  /** cache that the extended rewritten form of n is ret */
71
  void setCache(Node n, Node ret);
72
  /** get the cache for n */
73
  Node getCache(Node n);
74
  /** add to children
75
   *
76
   * Adds nc to the vector of children, if dropDup is true, we do not add
77
   * nc if it already occurs in children. This method returns false in this
78
   * case, otherwise it returns true.
79
   */
80
  bool addToChildren(Node nc, std::vector<Node>& children, bool dropDup);
81
82
  //--------------------------------------generic utilities
83
  /** Rewrite ITE, for example:
84
   *
85
   * ite( ~C, s, t ) ---> ite( C, t, s )
86
   * ite( A or B, s, t ) ---> ite( ~A and ~B, t, s )
87
   * ite( x = c, x, t ) --> ite( x = c, c, t )
88
   * t * { x -> c } = s => ite( x = c, s, t ) ---> t
89
   *
90
   * The parameter "full" indicates an effort level that this rewrite will
91
   * take. If full is false, then we do only perform rewrites that
92
   * strictly decrease the term size of n.
93
   */
94
  Node extendedRewriteIte(Kind itek, Node n, bool full = true);
95
  /** Rewrite AND/OR
96
   *
97
   * This implements BCP, factoring, and equality resolution for the Boolean
98
   * term n whose top symbolic is AND/OR.
99
   */
100
  Node extendedRewriteAndOr(Node n);
101
  /** Pull ITE, for example:
102
   *
103
   *   D=C2 ---> false
104
   *     implies
105
   *   D=ite( C, C1, C2 ) --->  C ^ D=C1
106
   *
107
   *   f(t,t1) --> s  and  f(t,t2)---> s
108
   *     implies
109
   *   f(t,ite(C,t1,t2)) ---> s
110
   *
111
   * If this function returns a non-null node ret, then n ---> ret.
112
   */
113
  Node extendedRewritePullIte(Kind itek, Node n);
114
  /** Negation Normal Form (NNF), for example:
115
   *
116
   *   ~( A & B ) ---> ( ~ A | ~B )
117
   *   ~( ite( A, B, C ) ---> ite( A, ~B, ~C )
118
   *
119
   * If this function returns a non-null node ret, then n ---> ret.
120
   */
121
  Node extendedRewriteNnf(Node n);
122
  /** (type-independent) Boolean constraint propagation, for example:
123
   *
124
   *   ~A & ( B V A ) ---> ~A & B
125
   *   A & ( B = ( A V C ) ) ---> A & B
126
   *
127
   * This function takes as arguments the kinds that specify AND, OR, and NOT.
128
   * It additionally takes as argument a map bcp_kinds. If this map is
129
   * non-empty, then all terms that have a Kind that is *not* in this map should
130
   * be treated as immutable. This is for instance to prevent propagation
131
   * beneath illegal terms. As an example:
132
   *   (bvand A (bvor A B)) is equivalent to (bvand A (bvor 1...1 B)), but
133
   *   (bvand A (bvplus A B)) is not equivalent to (bvand A (bvplus 1..1 B)),
134
   * hence, when using this function to do BCP for bit-vectors, we have that
135
   * BITVECTOR_AND is a bcp_kind, but BITVECTOR_PLUS is not.
136
   *
137
   * If this function returns a non-null node ret, then n ---> ret.
138
   */
139
  Node extendedRewriteBcp(
140
      Kind andk, Kind ork, Kind notk, std::map<Kind, bool>& bcp_kinds, Node n);
141
  /** (type-independent) factoring, for example:
142
   *
143
   *   ( A V B ) ^ ( A V C ) ----> A V ( B ^ C )
144
   *   ( A ^ B ) V ( A ^ C ) ----> A ^ ( B V C )
145
   *
146
   * This function takes as arguments the kinds that specify AND, OR, NOT.
147
   * We assume that the children of n do not contain duplicates.
148
   */
149
  Node extendedRewriteFactoring(Kind andk, Kind ork, Kind notk, Node n);
150
  /** (type-independent) equality resolution, for example:
151
   *
152
   *   ( A V C ) & ( A = B ) ---> ( B V C ) & ( A = B )
153
   *   ( A V ~B ) & ( A = B ) ----> ( A = B )
154
   *   ( A V B ) & ( A xor B ) ----> ( A xor B )
155
   *   ( A & B ) V ( A xor B ) ----> B V ( A xor B )
156
   *
157
   * This function takes as arguments the kinds that specify AND, OR, EQUAL,
158
   * and NOT. The equal kind eqk is interpreted as XOR if isXor is true.
159
   * It additionally takes as argument a map bcp_kinds, which
160
   * serves the same purpose as the above function.
161
   * If this function returns a non-null node ret, then n ---> ret.
162
   */
163
  Node extendedRewriteEqRes(Kind andk,
164
                            Kind ork,
165
                            Kind eqk,
166
                            Kind notk,
167
                            std::map<Kind, bool>& bcp_kinds,
168
                            Node n,
169
                            bool isXor = false);
170
  /** (type-independent) Equality chain rewriting, for example:
171
   *
172
   *   A = ( A = B ) ---> B
173
   *   ( A = D ) = ( C = B ) ---> A = ( B = ( C = D ) )
174
   *   A = ( A & B ) ---> ~A | B
175
   *
176
   * If this function returns a non-null node ret, then n ---> ret.
177
   * This function takes as arguments the kinds that specify EQUAL, AND, OR,
178
   * and NOT. If the flag isXor is true, the eqk is treated as XOR.
179
   */
180
  Node extendedRewriteEqChain(
181
      Kind eqk, Kind andk, Kind ork, Kind notk, Node n, bool isXor = false);
182
  /** extended rewrite aggressive
183
   *
184
   * All aggressive rewriting techniques (those that should be prioritized
185
   * at a lower level) go in this function.
186
   */
187
  Node extendedRewriteAggr(Node n);
188
  /** Decompose right associative chain
189
   *
190
   * For term f( ... f( f( base, tn ), t{n-1} ) ... t1 ), returns term base, and
191
   * appends t1...tn to children.
192
   */
193
  Node decomposeRightAssocChain(Kind k, Node n, std::vector<Node>& children);
194
  /** Make right associative chain
195
   *
196
   * Sorts children to obtain list { tn...t1 }, and returns the term
197
   * f( ... f( f( base, tn ), t{n-1} ) ... t1 ).
198
   */
199
  Node mkRightAssocChain(Kind k, Node base, std::vector<Node>& children);
200
  /** Partial substitute
201
   *
202
   * Applies the substitution specified by assign to n, recursing only beneath
203
   * terms whose Kind appears in rkinds (when rkinds is empty), and additionally
204
   * never recursing beneath WITNESS.
205
   */
206
  Node partialSubstitute(Node n,
207
                         const std::map<Node, Node>& assign,
208
                         const std::map<Kind, bool>& rkinds);
209
  /** same as above, with vectors */
210
  Node partialSubstitute(Node n,
211
                         const std::vector<Node>& vars,
212
                         const std::vector<Node>& subs,
213
                         const std::map<Kind, bool>& rkinds);
214
  /** solve equality
215
   *
216
   * If this function returns a non-null node n', then n' is equivalent to n
217
   * and is of the form that can be used by inferSubstitution below.
218
   */
219
  Node solveEquality(Node n);
220
  /** infer substitution
221
   *
222
   * If n is an equality of the form x = t, where t is either:
223
   * (1) a constant, or
224
   * (2) a variable y such that x < y based on an ordering,
225
   * then this method adds x to vars and y to subs and return true, otherwise
226
   * it returns false.
227
   * If usePred is true, we may additionally add n -> true, or n[0] -> false
228
   * is n is a negation.
229
   */
230
  bool inferSubstitution(Node n,
231
                         std::vector<Node>& vars,
232
                         std::vector<Node>& subs,
233
                         bool usePred = false);
234
  /** extended rewrite
235
   *
236
   * Prints debug information, indicating the rewrite n ---> ret was found.
237
   */
238
  inline void debugExtendedRewrite(Node n, Node ret, const char* c) const;
239
  //--------------------------------------end generic utilities
240
241
  //--------------------------------------theory-specific top-level calls
242
  /** extended rewrite strings
243
   *
244
   * If this method returns a non-null node ret', then ret is equivalent to
245
   * ret'.
246
   */
247
  Node extendedRewriteStrings(Node ret);
248
  //--------------------------------------end theory-specific top-level calls
249
};
250
251
} /* CVC4::theory::quantifiers namespace */
252
} /* CVC4::theory namespace */
253
} /* CVC4 namespace */
254
255
#endif /* CVC4__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H */