GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/single_inv_partition.h Lines: 7 7 100.0 %
Date: 2021-03-22 Branches: 5 6 83.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file single_inv_partition.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 utility for single invocation partitioning
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H
18
#define CVC4__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H
19
20
#include <map>
21
#include <vector>
22
23
#include "expr/node.h"
24
#include "expr/type_node.h"
25
26
namespace CVC4 {
27
namespace theory {
28
namespace quantifiers {
29
30
/** single invocation partition
31
 *
32
 * This is a utility to group formulas into single invocation/non-single
33
 * invocation parts, relative to a set of "input functions".
34
 * It can be used when either the set of input functions is fixed,
35
 * or is unknown.
36
 *
37
 * (EX1) For example, if input functions are { f },
38
 * then the formula is ( f( x, y ) = g( y ) V f( x, y ) = b )
39
 * is single invocation since there is only one
40
 * unique application of f, that is, f( x, y ).
41
 * Notice that
42
 *   exists f. forall xy. f( x, y ) = g( y ) V f( x, y ) = b
43
 * is equivalent to:
44
 *   forall xy. exists z. z = g( y ) V z = b
45
 *
46
 * When handling multiple input functions, we only infer a formula
47
 * is single invocation if all (relevant) input functions have the
48
 * same argument types. An input function is relevant if it is
49
 * specified by the input in a call to init() or occurs in the
50
 * formula we are processing.
51
 *
52
 * Notice that this class may introduce auxiliary variables to
53
 * coerce a formula into being single invocation. For example,
54
 * see Example 5 of Reynolds et al. SYNT 2017.
55
 *
56
 */
57
class SingleInvocationPartition
58
{
59
 public:
60
2200
  SingleInvocationPartition() : d_has_input_funcs(false) {}
61
2198
  ~SingleInvocationPartition() {}
62
  /** initialize this partition for formula n, with input functions funcs
63
   *
64
   * This initializes this class to check whether formula n is single
65
   * invocation with respect to the input functions in funcs only.
66
   * Below, the "processed formula" is a formula generated by this
67
   * call that is equivalent to n (if this call is successful).
68
   *
69
   * This method returns true if all input functions have identical
70
   * argument types, and false otherwise. Notice that all
71
   * access functions below are only valid if this class is
72
   * successfully initialized.
73
   */
74
  bool init(std::vector<Node>& funcs, Node n);
75
76
  /** initialize this partition for formula n
77
   *
78
   * In contrast to the above method, this version assumes that
79
   * all uninterpreted functions are input functions. That is, this
80
   * method is equivalent to the above function with funcs containing
81
   * all uninterpreted functions occurring in n.
82
   */
83
  bool init(Node n);
84
85
  /** is the processed formula purely single invocation?
86
   *
87
   * A formula is purely single invocation if it is equivalent to:
88
   *   t[ f1( x ), ..., fn( x ), x ],
89
   * for some F, where f1...fn are the input functions.
90
   * Notice that the free variables of t are exactly x.
91
   */
92
488
  bool isPurelySingleInvocation() { return d_conjuncts[1].empty(); }
93
  /** is the processed formula non-ground single invocation?
94
   *
95
   * A formula is non-ground single invocation if it is equivalent to:
96
   *   F[ f1( x ), ..., fn( x ), x, y ],
97
   * for some F, where f1...fn are the input functions.
98
   */
99
4
  bool isNonGroundSingleInvocation()
100
  {
101
4
    return d_conjuncts[3].size() == d_conjuncts[1].size();
102
  }
103
104
  /** Get the (portion of) the processed formula that is single invocation
105
   *
106
   * Notice this method returns the anti-skolemized version of the input
107
   * formula. In (EX1), this method returns:
108
   *   z = g( y ) V z = b
109
   * where z is the first-order variable for f (see
110
   * getFirstOrderVariableForFunction).
111
   */
112
130
  Node getSingleInvocation() { return getConjunct(0); }
113
  /** Get the (portion of) the processed formula that is not single invocation
114
   *
115
   * This formula and the above form a partition of the conjuncts of the
116
   * processed formula, that is:
117
   *   getSingleInvocation() * sigma ^ getNonSingleInvocation()
118
   * is equivalent to the processed formula, where sigma is a substitution of
119
   * the form:
120
   *   z_1 -> f_1( x ) .... z_n -> f_n( x )
121
   * where z_i are the first-order variables for input functions f_i
122
   * for all i=1,...,n, and x are the single invocation arguments of the input
123
   * formulas (see d_si_vars).
124
   */
125
  Node getNonSingleInvocation() { return getConjunct(1); }
126
  /** get full specification
127
   *
128
   * This returns getSingleInvocation() * sigma ^ getNonSingleInvocation(),
129
   * which is equivalent to the processed formula, where sigma is the
130
   * substitution described above.
131
   */
132
4
  Node getFullSpecification() { return getConjunct(2); }
133
  /** get first order variable for input function f
134
   *
135
   * This corresponds to the variable that we used when anti-skolemizing
136
   * function f. For example, in (EX1), if getSingleInvocation() returns:
137
   *   z = g( y ) V z = b
138
   * Then, getFirstOrderVariableForFunction(f) = z.
139
   */
140
  Node getFirstOrderVariableForFunction(Node f) const;
141
142
  /** get function for first order variable
143
   *
144
   * Opposite direction of above, where:
145
   *   getFunctionForFirstOrderVariable(z) = f.
146
   */
147
  Node getFunctionForFirstOrderVariable(Node v) const;
148
149
  /** get function invocation for
150
   *
151
   * Returns f( x ) where x are the single invocation arguments of the input
152
   * formulas (see d_si_vars). If f is not an input function, it returns null.
153
   */
154
  Node getFunctionInvocationFor(Node f) const;
155
156
  /** get single invocation variables, appends them to sivars */
157
  void getSingleInvocationVariables(std::vector<Node>& sivars) const;
158
159
  /** get all variables
160
   *
161
   * Appends all free variables of the processed formula to vars.
162
   */
163
  void getAllVariables(std::vector<Node>& vars) const;
164
165
  /** get function variables
166
   *
167
   * Appends all first-order variables corresponding to input functions to
168
   * fvars.
169
   */
170
  void getFunctionVariables(std::vector<Node>& fvars) const;
171
172
  /** get functions
173
   *
174
   * Gets all input functions. This has the same order as the list of
175
   * function variables above.
176
   */
177
  void getFunctions(std::vector<Node>& fs) const;
178
179
  /** print debugging information on Trace c */
180
  void debugPrint(const char* c);
181
182
 private:
183
  /** map from input functions to whether they have an anti-skolemizable type
184
   * An anti-skolemizable type is one of the form:
185
   *   ( T1, ..., Tn ) -> T
186
   * where Ti = d_arg_types[i] for i = 1,...,n.
187
   */
188
  std::map<Node, bool> d_funcs;
189
190
  /** map from functions to the invocation we inferred for them */
191
  std::map<Node, Node> d_func_inv;
192
193
  /** the list of first-order variables for functions
194
   * In (EX1), this is the list { z }.
195
   */
196
  std::vector<Node> d_func_vars;
197
198
  /** the arguments that we based the anti-skolemization on.
199
   * In (EX1), this is the list { x, y }.
200
   */
201
  std::vector<Node> d_si_vars;
202
203
  /** every free variable of conjuncts[2] */
204
  std::unordered_set<Node, NodeHashFunction> d_all_vars;
205
  /** map from functions to first-order variables that anti-skolemized them */
206
  std::map<Node, Node> d_func_fo_var;
207
  /** map from first-order variables to the function it anti-skolemized */
208
  std::map<Node, Node> d_fo_var_to_func;
209
210
  /** The argument types for this single invocation partition.
211
   * These are the argument types of the input functions we are
212
   * processing, where notice that:
213
   *   d_si_vars[i].getType()==d_arg_types[i]
214
   */
215
  std::vector<TypeNode> d_arg_types;
216
217
  /** the list of conjuncts with various properties :
218
   * 0 : the single invocation conjuncts (stored in anti-skolemized form),
219
   * 1 : the non-single invocation conjuncts,
220
   * 2 : all conjuncts,
221
   * 3 : non-ground single invocation conjuncts.
222
   */
223
  std::vector<Node> d_conjuncts[4];
224
225
  /** did we initialize this class with input functions? */
226
  bool d_has_input_funcs;
227
  /** the input functions we initialized this class with */
228
  std::vector<Node> d_input_funcs;
229
  /** all input functions */
230
  std::vector<Node> d_all_funcs;
231
  /** skolem of the same type as input functions */
232
  std::vector<Node> d_input_func_sks;
233
234
  /** infer the argument types of uninterpreted function applications
235
   *
236
   * If this method returns true, then typs contains the list of types of
237
   * the arguments (in order) of all uninterpreted functions in n.
238
   * If this method returns false, then there exists (at least) two
239
   * uninterpreted functions in n whose argument types are not identical.
240
   */
241
  bool inferArgTypes(Node n,
242
                     std::vector<TypeNode>& typs,
243
                     std::map<Node, bool>& visited);
244
245
  /** is anti-skolemizable type
246
   *
247
   * This method returns true if f's argument types are equal to the
248
   * argument types we have fixed in this class (see d_arg_types).
249
   */
250
  bool isAntiSkolemizableType(Node f);
251
252
  /**
253
   * This is the entry point for initializing this class,
254
   * which is called by the public init(...) methods.
255
   *   funcs are the input functions (if any were explicitly provide),
256
   *   typs is the types of the arguments of funcs,
257
   *   n is the formula to process,
258
   *   has_funcs is whether input functions were explicitly provided.
259
   */
260
  bool init(std::vector<Node>& funcs,
261
            std::vector<TypeNode>& typs,
262
            Node n,
263
            bool has_funcs);
264
265
  /**
266
   * Collect the top-level conjuncts of the formula (equivalent to)
267
   * n or the negation of n if pol=false, and store them in conj.
268
   */
269
  bool collectConjuncts(Node n, bool pol, std::vector<Node>& conj);
270
271
  /** process conjunct n
272
   *
273
   * This function is called when n is a top-level conjunction in a
274
   * formula that is equivalent to the input formula given to this
275
   * class via init.
276
   *
277
   * args : stores the arguments (if any) that we have seen in an application
278
   *   of an application of an input function in this conjunct.
279
   * terms/subs : this stores a term substitution with entries of the form:
280
   *     f(args) -> z
281
   *   where z is the first-order variable for input function f.
282
   */
283
  bool processConjunct(Node n,
284
                       std::map<Node, bool>& visited,
285
                       std::vector<Node>& args,
286
                       std::vector<Node>& terms,
287
                       std::vector<Node>& subs);
288
289
  /** get the and node corresponding to d_conjuncts[index] */
290
  Node getConjunct(int index);
291
};
292
293
} /* namespace CVC4::theory::quantifiers */
294
} /* namespace CVC4::theory */
295
} /* namespace CVC4 */
296
297
#endif /* CVC4__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H */