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) 20092021 by the authors listed in the file AUTHORS 
8 

** in the toplevel source directory and their institutional affiliations. 
9 

** All rights reserved. See the file COPYING in the toplevel 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 nonsimple 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 nonsimple 
36 

* triggers. 
37 

* 
38 

* Handling nonsimple 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 fapplications in the equivalence class of c. 
52 

* 
53 

* CVC4 employs techniques that ensure that the number of instantiations 
54 

* is worstcase 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 Ematching 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 backend 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 nonnull, 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 (! ... :nopattern). 
261 

*/ 
262 

std::map<Node, bool> d_curr_exclude_match; 
263 

/** Current first candidate 
264 

* Used in a key failquickly 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 