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

Line Exec Source
1
/*********************                                                        */
2
/*! \file sygus_process_conj.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 Techniqures for static preprocessing and analysis of
13
 ** sygus conjectures.
14
 **/
15
16
#include "cvc4_private.h"
17
18
#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_PROCESS_CONJ_H
19
#define CVC4__THEORY__QUANTIFIERS__SYGUS_PROCESS_CONJ_H
20
21
#include <map>
22
#include <unordered_map>
23
#include <unordered_set>
24
#include <vector>
25
26
#include "expr/node.h"
27
#include "expr/type_node.h"
28
29
namespace CVC4 {
30
namespace theory {
31
32
class QuantifiersEngine;
33
34
namespace quantifiers {
35
36
/** This file contains techniques that compute
37
 * argument relevancy for synthesis functions
38
 *
39
 * Let F be a synthesis conjecture of the form:
40
 *   exists f. forall X. P( f, X )
41
 *
42
 * The classes below compute whether certain arguments of
43
 * the function-to-synthesize f are irrelevant.
44
 * Assume that f is a binary function, where possible solutions
45
 * to the above conjecture are of the form:
46
 *   f -> (lambda (xy) t[x,y])
47
 * We say e.g. that the 2nd argument of f is irrelevant if we
48
 * can determine:
49
 *   F has a solution
50
 * if and only if
51
 *   F has a solution of the form f -> (lambda (xy) t[x] )
52
 * We conclude that arguments are irrelevant using the following
53
 * techniques.
54
 *
55
 *
56
 * (1) Argument invariance:
57
 *
58
 * Let s[z] be a term whose free variables are contained in { z }.
59
 * If all occurrences of f-applications in F are of the form:
60
 *   f(t, s[t])
61
 * then:
62
 *   f = (lambda (xy) r[x,y])
63
 * is a solution to F only if:
64
 *   f = (lambda (xy) r[x,s[x]])
65
 * is as well.
66
 * Hence the second argument of f is not relevant.
67
 *
68
 *
69
 * (2) Variable irrelevance:
70
 *
71
 * If F is equivalent to:
72
 *   exists f. forall w z u1...un. C1 ^...^Cm,
73
 * where for i=1...m, Ci is of the form:
74
 *   ( w1 = f(tm1[z], u1) ^
75
 *     ... ^
76
 *     wn = f(tmn[z], un) ) => Pm(w1...wn, z)
77
 * then the second argument of f is irrelevant.
78
 * We call u1...un single occurrence variables
79
 * (in Ci).
80
 *
81
 *
82
 * TODO (#1210) others, generalize (2)?
83
 *
84
 */
85
86
/** This structure stores information regarding
87
 * an argument of a function to synthesize.
88
 *
89
 * It is used to store whether the argument
90
 * position in the function to synthesize is
91
 * relevant.
92
 */
93
480
class SynthConjectureProcessArg
94
{
95
 public:
96
80
  SynthConjectureProcessArg() : d_var_single_occ(false), d_relevant(false) {}
97
  /** template definition
98
   * This is the term s[z] described
99
   * under "Argument Invariance" above.
100
   */
101
  Node d_template;
102
  /** single occurrence
103
   * Whether we are trying to show this argument
104
   * is irrelevant by "Variable irrelevance"
105
   * described above.
106
   */
107
  bool d_var_single_occ;
108
  /** whether this argument is relevant
109
   * An argument is marked as relevant if:
110
   * (A) it is explicitly marked as relevant
111
   *     due to a function application containing
112
   *     a relevant term at this argument position, or
113
   * (B) if it is given conflicting template definitions.
114
   */
115
  bool d_relevant;
116
};
117
118
/** This structure stores information regarding conjecture-specific
119
* analysis of a single function to synthesize within
120
* a conjecture to synthesize.
121
*
122
* It maintains information about each of the function to
123
* synthesize's arguments.
124
*/
125
struct SynthConjectureProcessFun
126
{
127
 public:
128
8
  SynthConjectureProcessFun() {}
129
8
  ~SynthConjectureProcessFun() {}
130
  /** initialize this class for function f */
131
  void init(Node f);
132
  /** process terms
133
   *
134
   * This is called once per conjunction in
135
   * the synthesis conjecture.
136
   *
137
   * ns are the f-applications to process,
138
   * ks are the variables we introduced to flatten them,
139
   * nf is the flattened form of our conjecture to process,
140
   * free_vars maps all subterms of n and nf to the set
141
   *   of variables (in set synth_fv) they contain.
142
   *
143
   * This updates information regarding which arguments
144
   * of the function-to-synthesize are relevant.
145
   */
146
  void processTerms(
147
      std::vector<Node>& ns,
148
      std::vector<Node>& ks,
149
      Node nf,
150
      std::unordered_set<Node, NodeHashFunction>& synth_fv,
151
      std::unordered_map<Node,
152
                         std::unordered_set<Node, NodeHashFunction>,
153
                         NodeHashFunction>& free_vars);
154
  /** is the i^th argument of the function-to-synthesize of this class relevant?
155
   */
156
  bool isArgRelevant(unsigned i);
157
  /** get irrelevant arguments for the function-to-synthesize of this class */
158
  void getIrrelevantArgs(std::unordered_set<unsigned>& args);
159
160
 private:
161
  /** the synth fun associated with this */
162
  Node d_synth_fun;
163
  /** properties of each argument */
164
  std::vector<SynthConjectureProcessArg> d_arg_props;
165
  /** variables for each argument type of f
166
   *
167
   * These are used to express templates for argument
168
   * invariance, in the data member
169
   * SynthConjectureProcessArg::d_template.
170
   */
171
  std::vector<Node> d_arg_vars;
172
  /** map from d_arg_vars to the argument #
173
   * they represent.
174
   */
175
  std::unordered_map<Node, unsigned, NodeHashFunction> d_arg_var_num;
176
  /** check match
177
   * This function returns true iff we can infer:
178
   *   cn * { x -> n_arg_map[d_arg_var_num[x]] | x in d_arg_vars } = n
179
   * In other words, cn and n are equivalent
180
   * via the substitution mapping argument variables to terms
181
   * specified by n_arg_map. The rewriter is used for inferring
182
   * this equivalence.
183
   *
184
   * For example, if n_arg_map contains { 1 -> t, 2 -> s }, then
185
   *   checkMatch( x1+x2, t+s, n_arg_map ) returns true,
186
   *   checkMatch( x1+1, t+1, n_arg_map ) returns true,
187
   *   checkMatch( 0, 0, n_arg_map ) returns true,
188
   *   checkMatch( x1+1, s, n_arg_map ) returns false.
189
   */
190
  bool checkMatch(Node cn,
191
                  Node n,
192
                  std::unordered_map<unsigned, Node>& n_arg_map);
193
  /** infer definition
194
   *
195
   * In the following, we say a term is a "template
196
   * definition" if its free variables are a subset of d_arg_vars.
197
   *
198
   * If this function returns a non-null node ret, then
199
   *   checkMatch( ret, n, term_to_arg_carry^-1 ) returns true.
200
   * and ret is a template definition.
201
   *
202
   * The free variables for all subterms of n are stored in
203
   * free_vars. The map term_to_arg_carry is injective.
204
   *
205
   * For example, if term_to_arg_carry contains { t -> 1, s -> 2 } and
206
   * free_vars is { t -> {y}, r -> {y}, s -> {}, q -> {}, ... -> {} }, then
207
   *   inferDefinition( 0, term_to_arg_carry, free_vars )
208
   *     returns 0
209
   *   inferDefinition( t, term_to_arg_carry, free_vars )
210
   *     returns x1
211
   *   inferDefinition( t+s+q, term_to_arg_carry, free_vars )
212
   *     returns x1+x2+q
213
   *   inferDefinition( t+r, term_to_arg_carry, free_vars )
214
   *     returns null
215
   *
216
   * Notice that multiple definitions are possible, e.g. above:
217
   *  inferDefinition( s, term_to_arg_carry, free_vars )
218
   *    may return either s or x2
219
   * TODO (#1210) : try multiple definitions?
220
   */
221
  Node inferDefinition(
222
      Node n,
223
      std::unordered_map<Node, unsigned, NodeHashFunction>& term_to_arg_carry,
224
      std::unordered_map<Node,
225
                         std::unordered_set<Node, NodeHashFunction>,
226
                         NodeHashFunction>& free_vars);
227
  /** Assign relevant definition
228
   *
229
   * If def is non-null,
230
   * this function assigns def as a template definition
231
   * for the argument positions in args.
232
   * This is called when there exists a term of the form
233
   *   f( t1....tn )
234
   * in the synthesis conjecture that we are processing,
235
   * where t_i = def * sigma for all i \in args,
236
   * for some substitution sigma, where def is a template
237
   * definition.
238
   *
239
   * If def is null, then there exists a term of the form
240
   *   f( t1....tn )
241
   * where t_i = s for for all i \in args, and s is not
242
   * a template definition. In this case, at least one
243
   * argument in args must be marked as a relevant
244
   * argument position.
245
   *
246
   * Returns a value rid such that:
247
   * (1) rid occurs in args,
248
   * (2) if def is null, then argument rid was marked
249
   *     relevant by this call.
250
   */
251
  unsigned assignRelevantDef(Node def, std::vector<unsigned>& args);
252
  /** returns true if n is in d_arg_vars, updates arg_index
253
   * to its position in d_arg_vars.
254
   */
255
  bool isArgVar(Node n, unsigned& arg_index);
256
};
257
258
/** Ceg Conjecture Process
259
 *
260
 * This class implements static techniques for preprocessing and analysis of
261
 * sygus conjectures.
262
 *
263
 * It is used as a back-end to SynthConjecture, which calls it using the
264
 * following interface: (1) When a sygus conjecture is asserted, we call
265
 * SynthConjectureProcess::simplify( q ),
266
 *     where q is the sygus conjecture in original form.
267
 *
268
 * (2) After a sygus conjecture is simplified and converted to deep
269
 * embedding form, we call SynthConjectureProcess::initialize( n, candidates ).
270
 *
271
 * (3) During enumerative SyGuS search, calls may be made by
272
 * the extension of the quantifier-free datatypes decision procedure for
273
 * sygus to SynthConjectureProcess::getSymmetryBreakingPredicate(...), which are
274
 * used for pruning search space based on conjecture-specific analysis.
275
 */
276
class SynthConjectureProcess
277
{
278
 public:
279
  SynthConjectureProcess(QuantifiersEngine* qe);
280
  ~SynthConjectureProcess();
281
  /** simplify the synthesis conjecture q
282
   * Returns a formula that is equivalent to q.
283
   * This simplification pass is called before all others
284
   * in SynthConjecture::assign.
285
   *
286
   * This function is intended for simplifications that
287
   * impact whether or not the synthesis conjecture is
288
   * single-invocation.
289
   */
290
  Node preSimplify(Node q);
291
  /** simplify the synthesis conjecture q
292
   * Returns a formula that is equivalent to q.
293
   * This simplification pass is called after all others
294
   * in SynthConjecture::assign.
295
   */
296
  Node postSimplify(Node q);
297
  /** initialize
298
   *
299
   * n is the "base instantiation" of the deep-embedding version of
300
   *   the synthesis conjecture under "candidates".
301
   *   (see SynthConjecture::d_base_inst)
302
   */
303
  void initialize(Node n, std::vector<Node>& candidates);
304
  /** is the i^th argument of the function-to-synthesize f relevant? */
305
  bool isArgRelevant(Node f, unsigned i);
306
  /** get irrelevant arguments for function-to-synthesize f
307
   * returns true if f is a function-to-synthesize.
308
   */
309
  bool getIrrelevantArgs(Node f, std::unordered_set<unsigned>& args);
310
  /** get symmetry breaking predicate
311
  *
312
  * Returns a formula that restricts the enumerative search space (for a given
313
  * depth) for a term x of sygus type tn whose top symbol is the tindex^{th}
314
  * constructor, where x is a subterm of enumerator e.
315
  */
316
  Node getSymmetryBreakingPredicate(
317
      Node x, Node e, TypeNode tn, unsigned tindex, unsigned depth);
318
  /** print out debug information about this conjecture */
319
  void debugPrint(const char* c);
320
 private:
321
  /** process conjunct
322
   *
323
   * This sets up initial information about functions to synthesize
324
   * where n is a conjunct of the synthesis conjecture, and synth_fv
325
   * is the set of (inner) universal variables in the synthesis
326
   * conjecture.
327
   */
328
  void processConjunct(Node n,
329
                       Node f,
330
                       std::unordered_set<Node, NodeHashFunction>& synth_fv);
331
  /** flatten
332
   *
333
   * Flattens all applications of f in term n.
334
   * This may add new variables to synth_fv, which
335
   * are introduced at all positions of functions
336
   * to synthesize in a bottom-up fashion. For each
337
   * variable k introduced for a function application
338
   * f(t), we add ( k -> f(t) ) to defs and ( f -> k )
339
   * to fun_to_defs.
340
   */
341
  Node flatten(Node n,
342
               Node f,
343
               std::unordered_set<Node, NodeHashFunction>& synth_fv,
344
               std::unordered_map<Node, Node, NodeHashFunction>& defs);
345
  /** get free variables
346
   * Constructs a map of all free variables that occur in n
347
   * from synth_fv and stores them in the map free_vars.
348
   */
349
  void getFreeVariables(
350
      Node n,
351
      std::unordered_set<Node, NodeHashFunction>& synth_fv,
352
      std::unordered_map<Node,
353
                         std::unordered_set<Node, NodeHashFunction>,
354
                         NodeHashFunction>& free_vars);
355
  /** for each synth-fun, information that is specific to this conjecture */
356
  std::map<Node, SynthConjectureProcessFun> d_sf_info;
357
358
  /** get component vector */
359
  void getComponentVector(Kind k, Node n, std::vector<Node>& args);
360
};
361
362
} /* namespace CVC4::theory::quantifiers */
363
} /* namespace CVC4::theory */
364
} /* namespace CVC4 */
365
366
#endif