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

Line Exec Source
1
/*********************                                                        */
2
/*! \file quantifiers_rewriter.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Haniel Barbosa, Morgan Deters
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 Rewriter for the theory of inductive quantifiers
13
 **
14
 ** Rewriter for the theory of inductive quantifiers.
15
 **/
16
17
#include "cvc4_private.h"
18
19
#ifndef CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H
20
#define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H
21
22
#include "theory/theory_rewriter.h"
23
#include "theory/trust_node.h"
24
25
namespace CVC4 {
26
namespace theory {
27
namespace quantifiers {
28
29
struct QAttributes;
30
31
/**
32
 * List of steps used by the quantifiers rewriter, details on these steps
33
 * can be found in the class below.
34
 */
35
enum RewriteStep
36
{
37
  /** Eliminate symbols (e.g. implies, xor) */
38
  COMPUTE_ELIM_SYMBOLS = 0,
39
  /** Miniscoping */
40
  COMPUTE_MINISCOPING,
41
  /** Aggressive miniscoping */
42
  COMPUTE_AGGRESSIVE_MINISCOPING,
43
  /** Apply the extended rewriter to quantified formula bodies */
44
  COMPUTE_EXT_REWRITE,
45
  /**
46
   * Term processing (e.g. simplifying terms based on ITE lifting,
47
   * eliminating extended arithmetic symbols).
48
   */
49
  COMPUTE_PROCESS_TERMS,
50
  /** Prenexing */
51
  COMPUTE_PRENEX,
52
  /** Variable elimination */
53
  COMPUTE_VAR_ELIMINATION,
54
  /** Conditional splitting */
55
  COMPUTE_COND_SPLIT,
56
  /** Placeholder for end of steps */
57
  COMPUTE_LAST
58
};
59
std::ostream& operator<<(std::ostream& out, RewriteStep s);
60
61
17987
class QuantifiersRewriter : public TheoryRewriter
62
{
63
 public:
64
  static bool isLiteral( Node n );
65
  //-------------------------------------variable elimination utilities
66
  /** is variable elimination
67
   *
68
   * Returns true if v is not a subterm of s, and the type of s is a subtype of
69
   * the type of v.
70
   */
71
  static bool isVarElim(Node v, Node s);
72
  /** get variable elimination literal
73
   *
74
   * If n asserted with polarity pol is equivalent to an equality of the form
75
   * v = s for some v in args, where isVariableElim( v, s ) holds, then this
76
   * method removes v from args, adds v to vars, adds s to subs, and returns
77
   * true. Otherwise, it returns false.
78
   */
79
  static bool getVarElimLit(Node n,
80
                            bool pol,
81
                            std::vector<Node>& args,
82
                            std::vector<Node>& vars,
83
                            std::vector<Node>& subs);
84
  /** variable eliminate for bit-vector equalities
85
   *
86
   * If this returns a non-null value ret, then var is updated to a member of
87
   * args, lit is equivalent to ( var = ret ).
88
   */
89
  static Node getVarElimLitBv(Node lit,
90
                              const std::vector<Node>& args,
91
                              Node& var);
92
  /** variable eliminate for string equalities
93
   *
94
   * If this returns a non-null value ret, then var is updated to a member of
95
   * args, lit is equivalent to ( var = ret ).
96
   */
97
  static Node getVarElimLitString(Node lit,
98
                                  const std::vector<Node>& args,
99
                                  Node& var);
100
  /** get variable elimination
101
   *
102
   * If n asserted with polarity pol entails a literal lit that corresponds
103
   * to a variable elimination for some v via the above method, we return true.
104
   * In this case, we update args/vars/subs based on eliminating v.
105
   */
106
  static bool getVarElim(Node n,
107
                         bool pol,
108
                         std::vector<Node>& args,
109
                         std::vector<Node>& vars,
110
                         std::vector<Node>& subs);
111
  /** has variable elimination
112
   *
113
   * Returns true if n asserted with polarity pol entails a literal for
114
   * which variable elimination is possible.
115
   */
116
  static bool hasVarElim(Node n, bool pol, std::vector<Node>& args);
117
  /** compute variable elimination inequality
118
   *
119
   * This method eliminates variables from the body of quantified formula
120
   * "body" using (global) reasoning about inequalities. In particular, if there
121
   * exists a variable x that only occurs in body or annotation qa in literals
122
   * of the form x>=t with a fixed polarity P, then we may replace all such
123
   * literals with P. For example, note that:
124
   *   forall xy. x>y OR P(y) is equivalent to forall y. P(y).
125
   *
126
   * In the case that a variable x from args can be eliminated in this way,
127
   * we remove x from args, add x >= t1, ..., x >= tn to bounds, add false, ...,
128
   * false to subs, and return true.
129
   */
130
  static bool getVarElimIneq(Node body,
131
                             std::vector<Node>& args,
132
                             std::vector<Node>& bounds,
133
                             std::vector<Node>& subs,
134
                             QAttributes& qa);
135
  //-------------------------------------end variable elimination utilities
136
 private:
137
  static int getPurifyIdLit2(Node n, std::map<Node, int>& visited);
138
  static bool addCheckElimChild(std::vector<Node>& children,
139
                                Node c,
140
                                Kind k,
141
                                std::map<Node, bool>& lit_pol,
142
                                bool& childrenChanged);
143
  static void addNodeToOrBuilder(Node n, NodeBuilder<>& t);
144
  static void computeArgs(const std::vector<Node>& args,
145
                          std::map<Node, bool>& activeMap,
146
                          Node n,
147
                          std::map<Node, bool>& visited);
148
  static void computeArgVec(const std::vector<Node>& args,
149
                            std::vector<Node>& activeArgs,
150
                            Node n);
151
  static void computeArgVec2(const std::vector<Node>& args,
152
                             std::vector<Node>& activeArgs,
153
                             Node n,
154
                             Node ipl);
155
  static Node computeProcessTerms2(Node body,
156
                                   std::map<Node, Node>& cache,
157
                                   std::vector<Node>& new_vars,
158
                                   std::vector<Node>& new_conds);
159
  static void computeDtTesterIteSplit(
160
      Node n,
161
      std::map<Node, Node>& pcons,
162
      std::map<Node, std::map<int, Node> >& ncons,
163
      std::vector<Node>& conj);
164
165
  //-------------------------------------variable elimination
166
  /** compute variable elimination
167
   *
168
   * This computes variable elimination rewrites for a body of a quantified
169
   * formula with bound variables args. This method updates args to args' and
170
   * returns a node body' such that (forall args. body) is equivalent to
171
   * (forall args'. body'). An example of a variable elimination rewrite is:
172
   *   forall xy. x != a V P( x,y ) ---> forall y. P( a, y )
173
   */
174
  static Node computeVarElimination(Node body,
175
                                    std::vector<Node>& args,
176
                                    QAttributes& qa);
177
  //-------------------------------------end variable elimination
178
  //-------------------------------------conditional splitting
179
  /** compute conditional splitting
180
   *
181
   * This computes conditional splitting rewrites for a body of a quantified
182
   * formula with bound variables args. It returns a body' that is equivalent
183
   * to body. We split body into a conjunction if variable elimination can
184
   * occur in one of the conjuncts. Examples of this are:
185
   *   ite( x=a, P(x), Q(x) ) ----> ( x!=a V P(x) ) ^ ( x=a V Q(x) )
186
   *   (x=a) = P(x) ----> ( x!=a V P(x) ) ^ ( x=a V ~P(x) )
187
   *   ( x!=a ^ P(x) ) V Q(x) ---> ( x!=a V Q(x) ) ^ ( P(x) V Q(x) )
188
   * where in each case, x can be eliminated in the first conjunct.
189
   */
190
  static Node computeCondSplit(Node body,
191
                               const std::vector<Node>& args,
192
                               QAttributes& qa);
193
  //-------------------------------------end conditional splitting
194
  //------------------------------------- process terms
195
  /** compute process terms
196
   *
197
   * This takes as input a quantified formula q with attributes qa whose
198
   * body is body.
199
   *
200
   * This rewrite eliminates problematic terms from the bodies of
201
   * quantified formulas, which includes performing:
202
   * - Certain cases of ITE lifting,
203
   * - Elimination of extended arithmetic functions like to_int/is_int/div/mod,
204
   * - Elimination of select over store.
205
   *
206
   * It may introduce new variables V into new_vars and new conditions C into
207
   * new_conds. It returns a node retBody such that q of the form
208
   *   forall X. body
209
   * is equivalent to:
210
   *   forall X, V. ( C => retBody )
211
   */
212
  static Node computeProcessTerms(Node body,
213
                                  std::vector<Node>& new_vars,
214
                                  std::vector<Node>& new_conds,
215
                                  Node q,
216
                                  QAttributes& qa);
217
  //------------------------------------- end process terms
218
  //------------------------------------- extended rewrite
219
  /** compute extended rewrite
220
   *
221
   * This returns the result of applying the extended rewriter on the body
222
   * of quantified formula q.
223
   */
224
  static Node computeExtendedRewrite(Node q);
225
  //------------------------------------- end extended rewrite
226
 public:
227
  static Node computeElimSymbols( Node body );
228
  /**
229
   * Compute miniscoping in quantified formula q with attributes in qa.
230
   */
231
  static Node computeMiniscoping(Node q, QAttributes& qa);
232
  static Node computeAggressiveMiniscoping( std::vector< Node >& args, Node body );
233
  /**
234
   * This function removes top-level quantifiers from subformulas of body
235
   * appearing with overall polarity pol. It adds quantified variables that
236
   * appear in positive polarity positions into args, and those at negative
237
   * polarity positions in nargs.
238
   *
239
   * If prenexAgg is true, we ensure that all top-level quantifiers are
240
   * eliminated from subformulas. This means that we must expand ITE and
241
   * Boolean equalities to ensure that quantifiers are at fixed polarities.
242
   *
243
   * For example, calling this function on:
244
   *   (or (forall ((x Int)) (P x z)) (not (forall ((y Int)) (Q y z))))
245
   * would return:
246
   *   (or (P x z) (not (Q y z)))
247
   * and add {x} to args, and {y} to nargs.
248
   */
249
  static Node computePrenex(Node q,
250
                            Node body,
251
                            std::unordered_set<Node, NodeHashFunction>& args,
252
                            std::unordered_set<Node, NodeHashFunction>& nargs,
253
                            bool pol,
254
                            bool prenexAgg);
255
  /**
256
   * Apply prenexing aggressively. Returns the prenex normal form of n.
257
   */
258
  static Node computePrenexAgg(Node n, std::map<Node, Node>& visited);
259
  static Node computeSplit( std::vector< Node >& args, Node body, QAttributes& qa );
260
private:
261
 static Node computeOperation(Node f,
262
                              RewriteStep computeOption,
263
                              QAttributes& qa);
264
265
public:
266
 RewriteResponse preRewrite(TNode in) override;
267
 RewriteResponse postRewrite(TNode in) override;
268
269
private:
270
  /** options */
271
 static bool doOperation(Node f, RewriteStep computeOption, QAttributes& qa);
272
273
private:
274
  static Node preSkolemizeQuantifiers(Node n, bool polarity, std::vector< TypeNode >& fvTypes, std::vector<TNode>& fvs);
275
public:
276
  static bool isPrenexNormalForm( Node n );
277
  /** preprocess
278
   *
279
   * This returns the result of applying simple quantifiers-specific
280
   * preprocessing to n, including but not limited to:
281
   * - rewrite rule elimination,
282
   * - pre-skolemization,
283
   * - aggressive prenexing.
284
   * The argument isInst is set to true if n is an instance of a previously
285
   * registered quantified formula. If this flag is true, we do not apply
286
   * certain steps like pre-skolemization since we know they will have no
287
   * effect.
288
   *
289
   * The result is wrapped in a trust node of kind TrustNodeKind::REWRITE.
290
   */
291
  static TrustNode preprocess(Node n, bool isInst = false);
292
  static Node mkForAll(const std::vector<Node>& args,
293
                       Node body,
294
                       QAttributes& qa);
295
  static Node mkForall(const std::vector<Node>& args,
296
                       Node body,
297
                       bool marked = false);
298
  static Node mkForall(const std::vector<Node>& args,
299
                       Node body,
300
                       std::vector<Node>& iplc,
301
                       bool marked = false);
302
}; /* class QuantifiersRewriter */
303
304
}/* CVC4::theory::quantifiers namespace */
305
}/* CVC4::theory namespace */
306
}/* CVC4 namespace */
307
308
#endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H */