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

Line Exec Source
1
/*********************                                                        */
2
/*! \file inst_match_generator.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner, Tim King
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 inst match generator class
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H
18
#define CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H
19
20
#include <map>
21
#include "expr/node.h"
22
#include "theory/quantifiers/inst_match.h"
23
#include "theory/quantifiers/ematching/im_generator.h"
24
25
namespace CVC4 {
26
namespace theory {
27
namespace inst {
28
29
class CandidateGenerator;
30
31
/** InstMatchGenerator class
32
*
33
* This is the default generator class for non-simple single triggers, that is,
34
* triggers composed of a single term with nested term applications.
35
* For example, { f( y, f( x, a ) ) } and { f( g( x ), a ) } are non-simple
36
* triggers.
37
*
38
* Handling non-simple triggers is done by constructing a linked list of
39
* InstMatchGenerator classes (see mkInstMatchGenerator), where each
40
* InstMatchGenerator has a "d_next" pointer.  If d_next is NULL,
41
* then this is the end of the InstMatchGenerator and the last
42
* InstMatchGenerator is responsible for finalizing the instantiation.
43
*
44
* For (EX1), for the trigger f( y, f( x, a ) ), we construct the linked list:
45
*
46
* [ f( y, f( x, a ) ) ] -> [ f( x, a ) ] -> NULL
47
*
48
* In a call to getNextMatch,
49
* if we match against a ground term f( b, c ), then the first InstMatchGenerator
50
* in this list binds y to b, and tells the InstMatchGenerator [ f( x, a ) ] to
51
* match f-applications in the equivalence class of c.
52
*
53
* CVC4 employs techniques that ensure that the number of instantiations
54
* is worst-case polynomial wrt the number of ground terms.
55
* Consider the axiom/pattern/context (EX2) :
56
*
57
*          axiom : forall x1 x2 x3 x4. F[ x1...x4 ]
58
*
59
*        trigger : P( f( x1 ), f( x2 ), f( x3 ), f( x4 ) )
60
*
61
* ground context : ~P( a, a, a, a ), a = f( c_1 ) = ... = f( c_100 )
62
*
63
* If E-matching were applied exhaustively, then x1, x2, x3, x4 would be
64
* instantiated with all combinations of c_1, ... c_100, giving 100^4
65
* instantiations.
66
*
67
* Instead, we enforce that at most 1 instantiation is produced for a
68
* ( pattern, ground term ) pair per round. Meaning, only one instantiation is
69
* generated when matching P( a, a, a, a ) against the generator
70
* [P( f( x1 ), f( x2 ), f( x3 ), f( x4 ) )]. For details, see Section 3 of
71
* Reynolds, Vampire 2016.
72
*
73
* To enforce these policies, we use a flag "d_active_add" which dictates the
74
* behavior of the last element in the linked list. If d_active_add is
75
*   true -> a call to getNextMatch(...) returns 1 only if adding the
76
*           instantiation via a call to IMGenerator::sendInstantiation(...)
77
*           successfully enqueues a lemma via a call to
78
*           Instantiate::addInstantiation(...). This call may fail e.g. if we
79
*           have already added the instantiation, or the instantiation is
80
*           entailed.
81
*   false -> a call to getNextMatch(...) returns 1 whenever an m is
82
*            constructed, where typically the caller would use m.
83
* This is important since a return value >0 signals that the current matched
84
* terms should be flushed. Consider the above example (EX1), where
85
* [ f(y,f(x,a)) ] is being matched against f(b,c),
86
* [ f(x,a) ] is being matched against f(d,a) where c=f(d,a)
87
* A successfully added instantiation { x->d, y->b } here signals we should
88
* not produce further instantiations that match f(y,f(x,a)) with f(b,c).
89
*
90
* A number of special cases of triggers are covered by this generator (see
91
* implementation of initialize), including :
92
*   Literal triggers, e.g. x >= a, ~x = y
93
*   Selector triggers, e.g. head( x )
94
*   Triggers with invertible subterms, e.g. f( x+1 )
95
*   Variable triggers, e.g. x
96
*
97
* All triggers above can be in the context of an equality, e.g.
98
* { f( y, f( x, a ) ) = b } is a trigger that matches f( y, f( x, a ) ) to
99
* ground terms in the equivalence class of b.
100
* { ~f( y, f( x, a ) ) = b } is a trigger that matches f( y, f( x, a ) ) to any
101
* ground terms not in the equivalence class of b.
102
*/
103
class InstMatchGenerator : public IMGenerator {
104
 public:
105
  /** destructor */
106
  ~InstMatchGenerator() override;
107
108
  /** Reset instantiation round. */
109
  void resetInstantiationRound() override;
110
  /** Reset. */
111
  bool reset(Node eqc) override;
112
  /** Get the next match. */
113
  int getNextMatch(Node q, InstMatch& m) override;
114
  /** Add instantiations. */
115
  uint64_t addInstantiations(Node q) override;
116
117
  /** set active add flag (true by default)
118
   *
119
  * If active add is true, we call sendInstantiation in calls to getNextMatch,
120
  * instead of returning the match. This is necessary so that we can ensure
121
  * policies that are dependent upon knowing when instantiations are
122
  * successfully added to the output channel through
123
  * Instantiate::addInstantiation(...).
124
  */
125
  void setActiveAdd(bool val);
126
  /** Get active score for this inst match generator
127
   *
128
   * See Trigger::getActiveScore for details.
129
   */
130
  int getActiveScore() override;
131
  /** exclude match
132
   *
133
   * Exclude matching d_match_pattern with Node n on subsequent calls to
134
   * getNextMatch.
135
   */
136
7648
  void excludeMatch(Node n) { d_curr_exclude_match[n] = true; }
137
  /** Get current match.
138
   * Returns the term we are currently matching.
139
   */
140
7648
  Node getCurrentMatch() { return d_curr_matched; }
141
  /** set that this match generator is independent
142
   *
143
  * A match generator is indepndent when this generator fails to produce a
144
  * match in a call to getNextMatch, the overall matching fails.
145
  */
146
1225
  void setIndependent() { d_independent_gen = true; }
147
  //-------------------------------construction of inst match generators
148
  /** mkInstMatchGenerator for single triggers, calls the method below */
149
  static InstMatchGenerator* mkInstMatchGenerator(Trigger* tparent,
150
                                                  Node q,
151
                                                  Node pat);
152
  /** mkInstMatchGenerator for the multi trigger case
153
  *
154
  * This linked list of InstMatchGenerator classes with one
155
  * InstMatchGeneratorMultiLinear at the head and a list of trailing
156
  * InstMatchGenerators corresponding to each unique subterm of pats with
157
  * free variables.
158
  */
159
  static InstMatchGenerator* mkInstMatchGeneratorMulti(Trigger* tparent,
160
                                                       Node q,
161
                                                       std::vector<Node>& pats);
162
  /** mkInstMatchGenerator
163
  *
164
  * This generates a linked list of InstMatchGenerators for each unique
165
  * subterm of pats with free variables.
166
  *
167
  * q is the quantified formula associated with the generator we are making
168
  * pats is a set of terms we are making InstMatchGenerator nodes for
169
  * qe is a pointer to the quantifiers engine (used for querying necessary
170
  * information during initialization) pat_map_init maps from terms to
171
  * generators we have already made for them.
172
  *
173
  * It calls initialize(...) for all InstMatchGenerators generated by this call.
174
  */
175
  static InstMatchGenerator* mkInstMatchGenerator(
176
      Trigger* tparent,
177
      Node q,
178
      std::vector<Node>& pats,
179
      std::map<Node, InstMatchGenerator*>& pat_map_init);
180
  //-------------------------------end construction of inst match generators
181
182
 protected:
183
  /** constructors
184
   *
185
  * These are intentionally private, and are called during linked list
186
  * construction in mkInstMatchGenerator.
187
  */
188
  InstMatchGenerator(Trigger* tparent, Node pat);
189
  /** The pattern we are producing matches for.
190
   *
191
  * This term and d_match_pattern can be different since this
192
  * term may involve  information regarding phase and (dis)equality entailment,
193
  * or other special cases of Triggers.
194
  *
195
  * For example, for the trigger for P( x ) = false, which matches P( x ) with
196
  * P( t ) in the equivalence class of false,
197
  *   P( x ) = false is d_pattern
198
  *   P( x ) is d_match_pattern
199
  * Another example, for pure theory triggers like head( x ), we have
200
  *   head( x ) is d_pattern
201
  *   x is d_match_pattern
202
  * since head( x ) can match any (List) datatype term x.
203
  *
204
  * If null, this is a multi trigger that is merging matches from d_children,
205
  * which is used in InstMatchGeneratorMulti.
206
  */
207
  Node d_pattern;
208
  /** The match pattern
209
   * This is the term that is matched against ground terms,
210
   * see examples above.
211
   */
212
  Node d_match_pattern;
213
  /** The current term we are matching. */
214
  Node d_curr_matched;
215
  /** do we need to call reset on this generator? */
216
  bool d_needsReset;
217
  /** candidate generator
218
   * This is the back-end utility for InstMatchGenerator.
219
   * It generates a stream of candidate terms to match against d_match_pattern
220
   * below, dependending upon what kind of term we are matching
221
   * (e.g. a matchable term, a variable, a relation, etc.).
222
   */
223
  CandidateGenerator* d_cg;
224
  /** children generators
225
   * These match generators correspond to the children of the term
226
   * we are matching with this generator.
227
   * For example [ f( x, a ) ] is a child of [ f( y, f( x, a ) ) ]
228
   * in the example (EX1) above.
229
   */
230
  std::vector<InstMatchGenerator*> d_children;
231
  /** for each child, the index in the term
232
   * For example [ f( x, a ) ] has index 1 in [ f( y, f( x, a ) ) ]
233
   * in the example (EX1) above, indicating it is the 2nd child
234
   * of the term.
235
   */
236
  std::vector<size_t> d_children_index;
237
  /** children types
238
   *
239
   * If d_match_pattern is an instantiation constant, then this is a singleton
240
   * vector containing the variable number of the d_match_pattern itself.
241
   * If d_match_patterm is a term of the form f( t1, ..., tn ), then for each
242
   * index i, d_children[i] stores the type of node ti is, where:
243
   *   >= 0 : variable (indicates its number),
244
   *   -1 : ground term,
245
   *   -2 : child term.
246
   */
247
  std::vector<int64_t> d_children_types;
248
  /** The next generator in the linked list
249
   * that this generator is a part of.
250
   */
251
  InstMatchGenerator* d_next;
252
  /** The equivalence class we are currently matching in. */
253
  Node d_eq_class;
254
  /** If non-null, then this is a relational trigger of the form x ~
255
   * d_eq_class_rel. */
256
  Node d_eq_class_rel;
257
  /** Excluded matches
258
  * Stores the terms we are not allowed to match.
259
  * These can for instance be specified by the smt2
260
  * extended syntax (! ... :no-pattern).
261
  */
262
  std::map<Node, bool> d_curr_exclude_match;
263
  /** Current first candidate
264
  * Used in a key fail-quickly optimization which generates
265
  * the first candidate term to match during reset().
266
  */
267
  Node d_curr_first_candidate;
268
  /** Indepdendent generate
269
  * If this flag is true, failures to match should be cached.
270
  */
271
  bool d_independent_gen;
272
  /** active add flag, described above. */
273
  bool d_active_add;
274
  /** cached value of d_match_pattern.getType() */
275
  TypeNode d_match_pattern_type;
276
  /** the match operator for d_match_pattern
277
   *
278
   * See TermDatabase::getMatchOperator for details on match operators.
279
   */
280
  Node d_match_pattern_op;
281
  /** get the match against ground term or formula t.
282
   *
283
   * d_match_pattern and t should have the same shape, that is,
284
   * their match operator (see TermDatabase::getMatchOperator) is the same.
285
   * only valid for use where !d_match_pattern.isNull().
286
   */
287
  int getMatch(Node q, Node t, InstMatch& m);
288
  /** Initialize this generator.
289
   *
290
   * q is the quantified formula associated with this generator.
291
   *
292
   * This constructs the appropriate information about what
293
   * patterns we are matching and children generators.
294
   *
295
   * It may construct new (child) generators needed to implement
296
   * the matching algorithm for this term. For each new generator
297
   * constructed in this way, it adds them to gens.
298
   */
299
  void initialize(Node q,
300
                  std::vector<InstMatchGenerator*>& gens);
301
  /** Continue next match
302
   *
303
  * This is called during getNextMatch when the current generator in the linked
304
  * list succesfully satisfies its matching constraint. This function either
305
  * calls getNextMatch of the next element in the linked list, or finalizes the
306
  * match (calling sendInstantiation(...) if active add is true, or returning a
307
  * value >0 if active add is false).  Its return value has the same semantics
308
  * as getNextMatch.
309
  */
310
  int continueNextMatch(Node q,
311
                        InstMatch& m,
312
                        InferenceId id);
313
  /** Get inst match generator
314
   *
315
   * Gets the InstMatchGenerator that implements the
316
   * appropriate matching algorithm for n within q
317
   * within a linked list of InstMatchGenerators.
318
   */
319
  static InstMatchGenerator* getInstMatchGenerator(Trigger* tparent,
320
                                                   Node q,
321
                                                   Node n);
322
};/* class InstMatchGenerator */
323
324
}
325
}
326
}
327
328
#endif