1 /********************* */
2 /*! \file inst_match_generator.h
4 ** Top contributors (to current version):
5 ** Morgan Deters, Andrew Reynolds, Tim King
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2017 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
12 ** \brief inst match generator class
15 #include "cvc4_private.h"
17 #ifndef __CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H
18 #define __CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H
20 #include "theory/quantifiers/inst_match.h"
26 class QuantifiersEngine
;
27 namespace quantifiers
{
37 * Virtual base class for generating InstMatch objects, which correspond to
38 * quantifier instantiations. The main use of this class is as a backend utility
39 * to Trigger (see theory/quantifiers/trigger.h).
41 * Some functions below take as argument a pointer to the current quantifiers
42 * engine, which is used for making various queries about what terms and
43 * equalities exist in the current context.
45 * Some functions below take a pointer to a parent Trigger object, which is used
46 * to post-process and finalize the instantiations through
47 * sendInstantiation(...), where the parent trigger will make calls to
48 * qe->getInstantiate()->addInstantiation(...). The latter function is the entry
49 * point in which instantiate lemmas are enqueued to be sent on the output
54 virtual ~IMGenerator() {}
55 /** Reset instantiation round.
57 * Called once at beginning of an instantiation round.
59 virtual void resetInstantiationRound(QuantifiersEngine
* qe
) {}
62 * eqc is the equivalence class to search in (any if eqc=null).
63 * Returns true if this generator can produce instantiations, and false
64 * otherwise. An example of when it returns false is if it can be determined
65 * that no appropriate matchable terms occur based on eqc.
67 virtual bool reset(Node eqc
, QuantifiersEngine
* qe
) { return true; }
68 /** Get the next match.
70 * Must call reset( eqc ) before this function. This constructs an
71 * instantiation, which it populates in data structure m,
72 * based on the current context using the implemented matching algorithm.
74 * q is the quantified formula we are adding instantiations for
75 * m is the InstMatch object we are generating
77 * Returns a value >0 if an instantiation was successfully generated
79 virtual int getNextMatch(Node q
,
81 QuantifiersEngine
* qe
,
86 /** add instantiations
88 * This add all available instantiations for q based on the current context
89 * using the implemented matching algorithm. It typically is implemented as a
90 * fixed point of getNextMatch above.
92 * baseMatch is a mapping of default values that should be used for variables
93 * that are not bound by this (not frequently used). (TODO remove #1389)
95 * It returns the number of instantiations added using calls to calls to
96 * Instantiate::addInstantiation(...).
98 virtual int addInstantiations(Node q
,
100 QuantifiersEngine
* qe
,
107 * A heuristic value indicating how active this generator is.
109 virtual int getActiveScore( QuantifiersEngine
* qe
) { return 0; }
111 /** send instantiation
113 * This method sends instantiation, specified by m, to the parent trigger
114 * object, which will in turn make a call to
115 * Instantiate::addInstantiation(...). This method returns true if a
116 * call to Instantiate::addInstantiation(...) was successfully made,
117 * indicating that an instantiation was enqueued in the quantifier engine's
120 bool sendInstantiation(Trigger
* tparent
, InstMatch
& m
);
121 };/* class IMGenerator */
123 class CandidateGenerator
;
125 /** InstMatchGenerator class
127 * This is the default generator class for non-simple single triggers, that is,
128 * triggers composed of a single term with nested term applications.
129 * For example, { f( y, f( x, a ) ) } and { f( g( x ), a ) } are non-simple
132 * Handling non-simple triggers is done by constructing a linked list of
133 * InstMatchGenerator classes (see mkInstMatchGenerator), where each
134 * InstMatchGenerator has a "d_next" pointer. If d_next is NULL,
135 * then this is the end of the InstMatchGenerator and the last
136 * InstMatchGenerator is responsible for finalizing the instantiation.
138 * For (EX1), for the trigger f( y, f( x, a ) ), we construct the linked list:
140 * [ f( y, f( x, a ) ) ] -> [ f( x, a ) ] -> NULL
142 * In a call to getNextMatch,
143 * if we match against a ground term f( b, c ), then the first InstMatchGenerator
144 * in this list binds y to b, and tells the InstMatchGenerator [ f( x, a ) ] to
145 * match f-applications in the equivalence class of c.
147 * CVC4 employs techniques that ensure that the number of instantiations
148 * is worst-case polynomial wrt the number of ground terms.
149 * Consider the axiom/pattern/context (EX2) :
151 * axiom : forall x1 x2 x3 x4. F[ x1...x4 ]
153 * trigger : P( f( x1 ), f( x2 ), f( x3 ), f( x4 ) )
155 * ground context : ~P( a, a, a, a ), a = f( c_1 ) = ... = f( c_100 )
157 * If E-matching were applied exhaustively, then x1, x2, x3, x4 would be
158 * instantiated with all combinations of c_1, ... c_100, giving 100^4
161 * Instead, we enforce that at most 1 instantiation is produced for a
162 * ( pattern, ground term ) pair per round. Meaning, only one instantiation is
163 * generated when matching P( a, a, a, a ) against the generator
164 * [P( f( x1 ), f( x2 ), f( x3 ), f( x4 ) )]. For details, see Section 3 of
165 * Reynolds, Vampire 2016.
167 * To enforce these policies, we use a flag "d_active_add" which dictates the
168 * behavior of the last element in the linked list. If d_active_add is
169 * true -> a call to getNextMatch(...) returns 1 only if adding the
170 * instantiation via a call to IMGenerator::sendInstantiation(...)
171 * successfully enqueues a lemma via a call to
172 * Instantiate::addInstantiation(...). This call may fail e.g. if we
173 * have already added the instantiation, or the instantiation is
175 * false -> a call to getNextMatch(...) returns 1 whenever an m is
176 * constructed, where typically the caller would use m.
177 * This is important since a return value >0 signals that the current matched
178 * terms should be flushed. Consider the above example (EX1), where
179 * [ f(y,f(x,a)) ] is being matched against f(b,c),
180 * [ f(x,a) ] is being matched against f(d,a) where c=f(d,a)
181 * A successfully added instantiation { x->d, y->b } here signals we should
182 * not produce further instantiations that match f(y,f(x,a)) with f(b,c).
184 * A number of special cases of triggers are covered by this generator (see
185 * implementation of initialize), including :
186 * Literal triggers, e.g. x >= a, ~x = y
187 * Selector triggers, e.g. head( x )
188 * Triggers with invertible subterms, e.g. f( x+1 )
189 * Variable triggers, e.g. x
191 * All triggers above can be in the context of an equality, e.g.
192 * { f( y, f( x, a ) ) = b } is a trigger that matches f( y, f( x, a ) ) to
193 * ground terms in the equivalence class of b.
194 * { ~f( y, f( x, a ) ) = b } is a trigger that matches f( y, f( x, a ) ) to any
195 * ground terms not in the equivalence class of b.
197 class InstMatchGenerator
: public IMGenerator
{
200 virtual ~InstMatchGenerator() throw();
203 // options for producing matches
204 MATCH_GEN_DEFAULT
= 0,
205 // others (internally used)
206 MATCH_GEN_INTERNAL_ERROR
,
209 /** Reset instantiation round. */
210 void resetInstantiationRound(QuantifiersEngine
* qe
) override
;
212 bool reset(Node eqc
, QuantifiersEngine
* qe
) override
;
213 /** Get the next match. */
214 int getNextMatch(Node q
,
216 QuantifiersEngine
* qe
,
217 Trigger
* tparent
) override
;
218 /** Add instantiations. */
219 int addInstantiations(Node q
,
220 InstMatch
& baseMatch
,
221 QuantifiersEngine
* qe
,
222 Trigger
* tparent
) override
;
224 /** set active add flag (true by default)
226 * If active add is true, we call sendInstantiation in calls to getNextMatch,
227 * instead of returning the match. This is necessary so that we can ensure
228 * policies that are dependent upon knowing when instantiations are
229 * successfully added to the output channel through
230 * Instantiate::addInstantiation(...).
232 void setActiveAdd(bool val
);
233 /** Get active score for this inst match generator
235 * See Trigger::getActiveScore for details.
237 int getActiveScore(QuantifiersEngine
* qe
);
240 * Exclude matching d_match_pattern with Node n on subsequent calls to
243 void excludeMatch(Node n
) { d_curr_exclude_match
[n
] = true; }
244 /** Get current match.
245 * Returns the term we are currently matching.
247 Node
getCurrentMatch() { return d_curr_matched
; }
248 /** set that this match generator is independent
250 * A match generator is indepndent when this generator fails to produce a
251 * match in a call to getNextMatch, the overall matching fails.
253 void setIndependent() { d_independent_gen
= true; }
254 //-------------------------------construction of inst match generators
255 /** mkInstMatchGenerator for single triggers, calls the method below */
256 static InstMatchGenerator
* mkInstMatchGenerator(Node q
,
258 QuantifiersEngine
* qe
);
259 /** mkInstMatchGenerator for the multi trigger case
261 * This linked list of InstMatchGenerator classes with one
262 * InstMatchGeneratorMultiLinear at the head and a list of trailing
263 * InstMatchGenerators corresponding to each unique subterm of pats with
266 static InstMatchGenerator
* mkInstMatchGeneratorMulti(Node q
,
267 std::vector
<Node
>& pats
,
268 QuantifiersEngine
* qe
);
269 /** mkInstMatchGenerator
271 * This generates a linked list of InstMatchGenerators for each unique
272 * subterm of pats with free variables.
274 * q is the quantified formula associated with the generator we are making
275 * pats is a set of terms we are making InstMatchGenerator nodes for
276 * qe is a pointer to the quantifiers engine (used for querying necessary
277 * information during initialization) pat_map_init maps from terms to
278 * generators we have already made for them.
280 * It calls initialize(...) for all InstMatchGenerators generated by this call.
282 static InstMatchGenerator
* mkInstMatchGenerator(
284 std::vector
<Node
>& pats
,
285 QuantifiersEngine
* qe
,
286 std::map
<Node
, InstMatchGenerator
*>& pat_map_init
);
287 //-------------------------------end construction of inst match generators
292 * These are intentionally private, and are called during linked list
293 * construction in mkInstMatchGenerator.
295 InstMatchGenerator(Node pat
);
296 InstMatchGenerator();
297 /** The pattern we are producing matches for.
299 * This term and d_match_pattern can be different since this
300 * term may involve information regarding phase and (dis)equality entailment,
301 * or other special cases of Triggers.
303 * For example, for the trigger for P( x ) = false, which matches P( x ) with
304 * P( t ) in the equivalence class of false,
305 * P( x ) = false is d_pattern
306 * P( x ) is d_match_pattern
307 * Another example, for pure theory triggers like head( x ), we have
308 * head( x ) is d_pattern
309 * x is d_match_pattern
310 * since head( x ) can match any (List) datatype term x.
312 * If null, this is a multi trigger that is merging matches from d_children,
313 * which is used in InstMatchGeneratorMulti.
316 /** The match pattern
317 * This is the term that is matched against ground terms,
318 * see examples above.
320 Node d_match_pattern
;
321 /** The current term we are matching. */
323 /** do we need to call reset on this generator? */
325 /** candidate generator
326 * This is the back-end utility for InstMatchGenerator.
327 * It generates a stream of candidate terms to match against d_match_pattern
328 * below, dependending upon what kind of term we are matching
329 * (e.g. a matchable term, a variable, a relation, etc.).
331 CandidateGenerator
* d_cg
;
332 /** policy to use for matching
333 * This is one of MATCH_GEN_* above.
334 * TODO: this can be simplified/removed (#1283).
337 /** children generators
338 * These match generators correspond to the children of the term
339 * we are matching with this generator.
340 * For example [ f( x, a ) ] is a child of [ f( y, f( x, a ) ) ]
341 * in the example (EX1) above.
343 std::vector
<InstMatchGenerator
*> d_children
;
344 /** for each child, the index in the term
345 * For example [ f( x, a ) ] has index 1 in [ f( y, f( x, a ) ) ]
346 * in the example (EX1) above, indicating it is the 2nd child
349 std::vector
<int> d_children_index
;
350 /** children types 0 : variable, 1 : child term, -1 : ground term */
351 std::vector
<int> d_children_types
;
352 /** The next generator in the linked list
353 * that this generator is a part of.
355 InstMatchGenerator
* d_next
;
356 /** The equivalence class we are currently matching in. */
358 /** If non-null, then this is a relational trigger of the form x ~
361 /** For each child index of this node, the variable numbers of the children.
362 * For example, if this is generator is for the term f( x3, a, x1, x2 )
363 * the quantified formula
364 * forall x1 x2 x3. (...).
365 * Then d_var_num[0] = 2, d_var_num[2] = 0 and d_var_num[3] = 1.
367 std::map
<int, int> d_var_num
;
369 * Stores the terms we are not allowed to match.
370 * These can for instance be specified by the smt2
371 * extended syntax (! ... :no-pattern).
373 std::map
<Node
, bool> d_curr_exclude_match
;
374 /** Current first candidate
375 * Used in a key fail-quickly optimization which generates
376 * the first candidate term to match during reset().
378 Node d_curr_first_candidate
;
379 /** Indepdendent generate
380 * If this flag is true, failures to match should be cached.
382 bool d_independent_gen
;
383 /** active add flag, described above. */
385 /** cached value of d_match_pattern.getType() */
386 TypeNode d_match_pattern_type
;
387 /** the match operator for d_match_pattern
389 * See TermDatabase::getMatchOperator for details on match operators.
391 Node d_match_pattern_op
;
392 /** get the match against ground term or formula t.
394 * d_match_pattern and t should have the same shape, that is,
395 * their match operator (see TermDatabase::getMatchOperator) is the same.
396 * only valid for use where !d_match_pattern.isNull().
399 Node q
, Node t
, InstMatch
& m
, QuantifiersEngine
* qe
, Trigger
* tparent
);
400 /** Initialize this generator.
402 * q is the quantified formula associated with this generator.
404 * This constructs the appropriate information about what
405 * patterns we are matching and children generators.
407 * It may construct new (child) generators needed to implement
408 * the matching algorithm for this term. For each new generator
409 * constructed in this way, it adds them to gens.
411 void initialize(Node q
,
412 QuantifiersEngine
* qe
,
413 std::vector
<InstMatchGenerator
*>& gens
);
414 /** Continue next match
416 * This is called during getNextMatch when the current generator in the linked
417 * list succesfully satisfies its matching constraint. This function either
418 * calls getNextMatch of the next element in the linked list, or finalizes the
419 * match (calling sendInstantiation(...) if active add is true, or returning a
420 * value >0 if active add is false). Its return value has the same semantics
423 int continueNextMatch(Node q
,
425 QuantifiersEngine
* qe
,
427 /** Get inst match generator
429 * Gets the InstMatchGenerator that implements the
430 * appropriate matching algorithm for n within q
431 * within a linked list of InstMatchGenerators.
433 static InstMatchGenerator
* getInstMatchGenerator(Node q
, Node n
);
434 };/* class InstMatchGenerator */
436 /** match generator for Boolean term ITEs
437 * This handles the special case of triggers that look like ite( x, BV1, BV0 ).
439 class VarMatchGeneratorBooleanTerm
: public InstMatchGenerator
{
441 VarMatchGeneratorBooleanTerm( Node var
, Node comp
);
442 virtual ~VarMatchGeneratorBooleanTerm() throw() {}
444 bool reset(Node eqc
, QuantifiersEngine
* qe
) override
449 /** Get the next match. */
450 int getNextMatch(Node q
,
452 QuantifiersEngine
* qe
,
453 Trigger
* tparent
) override
;
456 /** stores the true branch of the Boolean ITE */
458 /** stores whether we have written a value for var in the current match. */
462 /** match generator for purified terms
463 * This handles the special case of invertible terms like x+1 (see
464 * Trigger::getTermInversionVariable).
466 class VarMatchGeneratorTermSubs
: public InstMatchGenerator
{
468 VarMatchGeneratorTermSubs( Node var
, Node subs
);
469 virtual ~VarMatchGeneratorTermSubs() throw() {}
471 bool reset(Node eqc
, QuantifiersEngine
* qe
) override
476 /** Get the next match. */
477 int getNextMatch(Node q
,
479 QuantifiersEngine
* qe
,
480 Trigger
* tparent
) override
;
483 /** variable we are matching (x in the example x+1). */
485 /** cache of d_var.getType() */
487 /** The substitution for what we match (x-1 in the example x+1). */
489 /** stores whether we have written a value for d_var in the current match. */
493 /** InstMatchGeneratorMultiLinear class
495 * This is the default implementation of multi-triggers.
497 * Handling multi-triggers using this class is done by constructing a linked
498 * list of InstMatchGenerator classes (see mkInstMatchGeneratorMulti), with one
499 * InstMatchGeneratorMultiLinear at the head and a list of trailing
500 * InstMatchGenerators.
502 * CVC4 employs techniques that ensure that the number of instantiations
503 * is worst-case polynomial wrt the number of ground terms, where this class
504 * lifts this policy to multi-triggers. In particular consider
506 * multi-trigger : { f( x1 ), f( x2 ), f( x3 ), f( x4 ) }
508 * For this multi-trigger, we insist that for each i=1...4, and each ground term
509 * t, there is at most 1 instantiation added as a result of matching
510 * ( f( x1 ), f( x2 ), f( x3 ), f( x4 ) )
511 * against ground terms of the form
512 * ( s_1, s_2, s_3, s_4 ) where t = s_i for i=1,...,4.
513 * Meaning we add instantiations for the multi-trigger
514 * ( f( x1 ), f( x2 ), f( x3 ), f( x4 ) ) based on matching pairwise against:
515 * ( f( c_i11 ), f( c_i21 ), f( c_i31 ), f( c_i41 ) )
516 * ( f( c_i12 ), f( c_i22 ), f( c_i32 ), f( c_i42 ) )
517 * ( f( c_i13 ), f( c_i23 ), f( c_i33 ), f( c_i43 ) )
518 * Where we require c_i{jk} != c_i{jl} for each i=1...4, k != l.
520 * For example, we disallow adding instantiations based on matching against both
521 * ( f( c_1 ), f( c_2 ), f( c_4 ), f( c_6 ) ) and
522 * ( f( c_1 ), f( c_3 ), f( c_5 ), f( c_7 ) )
523 * against ( f( x1 ), f( x2 ), f( x3 ), f( x4 ) ), since f( c_1 ) is matched
524 * against f( x1 ) twice.
526 * This policy can be disabled by --no-multi-trigger-linear.
529 class InstMatchGeneratorMultiLinear
: public InstMatchGenerator
{
530 friend class InstMatchGenerator
;
534 virtual ~InstMatchGeneratorMultiLinear() throw();
537 bool reset(Node eqc
, QuantifiersEngine
* qe
) override
;
538 /** Get the next match. */
539 int getNextMatch(Node q
,
541 QuantifiersEngine
* qe
,
542 Trigger
* tparent
) override
;
545 /** reset the children of this generator */
546 int resetChildren(QuantifiersEngine
* qe
);
548 InstMatchGeneratorMultiLinear(Node q
,
549 std::vector
<Node
>& pats
,
550 QuantifiersEngine
* qe
);
551 };/* class InstMatchGeneratorMulti */
553 /** InstMatchGeneratorMulti
555 * This is an earlier implementation of multi-triggers
556 * that is enabled by --multi-trigger-cache.
557 * This generator takes the product of instantiations
558 * found by single trigger matching, and does
559 * not have the guarantee that the number of
560 * instantiations is polynomial wrt the number of
563 class InstMatchGeneratorMulti
: public IMGenerator
{
566 InstMatchGeneratorMulti(Node q
,
567 std::vector
<Node
>& pats
,
568 QuantifiersEngine
* qe
);
570 virtual ~InstMatchGeneratorMulti() throw();
572 /** Reset instantiation round. */
573 void resetInstantiationRound(QuantifiersEngine
* qe
) override
;
575 bool reset(Node eqc
, QuantifiersEngine
* qe
) override
;
576 /** Add instantiations. */
577 int addInstantiations(Node q
,
578 InstMatch
& baseMatch
,
579 QuantifiersEngine
* qe
,
580 Trigger
* tparent
) override
;
584 typedef std::pair
< std::pair
< int, int >, InstMatchTrie
* > IndexedTrie
;
585 /** process new match
587 * Called during addInstantiations(...).
588 * Indicates we produced a match m for child fromChildIndex
589 * addedLemmas is how many instantiations we succesfully send
590 * via IMGenerator::sendInstantiation(...) calls.
592 void processNewMatch(QuantifiersEngine
* qe
,
597 /** helper for process new match
598 * tr is the inst match trie (term index) we are currently traversing.
599 * trieIndex is depth we are in trie tr.
600 * childIndex is the index of the term in the multi trigger we are currently
602 * endChildIndex is the index of the term in the multi trigger that generated
603 * a new term, and hence we will end when the product
604 * computed by this function returns to.
605 * modEq is whether we are matching modulo equality.
607 void processNewInstantiations(QuantifiersEngine
* qe
,
616 /** Map from pattern nodes to indices of variables they contain. */
617 std::map
< Node
, std::vector
< int > > d_var_contains
;
618 /** Map from variable indices to pattern nodes that contain them. */
619 std::map
< int, std::vector
< Node
> > d_var_to_node
;
620 /** quantified formula we are producing matches for */
622 /** children generators
623 * These are inst match generators for each term in the multi trigger.
625 std::vector
< InstMatchGenerator
* > d_children
;
626 /** variable orderings
627 * Stores a heuristically determined variable ordering (unique
628 * variables first) for each term in the multi trigger.
630 std::map
< unsigned, InstMatchTrie::ImtIndexOrder
* > d_imtio
;
631 /** inst match tries for each child node
632 * This data structure stores all InstMatch objects generated
633 * by matching for each term in the multi trigger.
635 std::vector
< InstMatchTrieOrdered
> d_children_trie
;
636 };/* class InstMatchGeneratorMulti */
638 /** InstMatchGeneratorSimple class
640 * This is the default generator class for simple single triggers.
641 * For example, { f( x, a ) }, { f( x, x ) } and { f( x, y ) } are simple single
642 * triggers. In practice, around 70-90% of triggers are simple single triggers.
644 * Notice that simple triggers also can have an attached polarity.
645 * For example, { P( x ) = false }, { f( x, y ) = a } and { ~f( a, x ) = b } are
646 * simple single triggers.
648 * The implementation traverses the term indices in TermDatabase for adding
649 * instantiations, which is more efficient than the techniques required for
650 * handling non-simple single triggers.
652 * In contrast to other instantiation generators, it does not call
653 * IMGenerator::sendInstantiation and for performance reasons instead calls
654 * qe->getInstantiate()->addInstantiation(...) directly.
656 class InstMatchGeneratorSimple
: public IMGenerator
{
659 InstMatchGeneratorSimple(Node q
, Node pat
, QuantifiersEngine
* qe
);
661 ~InstMatchGeneratorSimple() throw() {}
662 /** Reset instantiation round. */
663 void resetInstantiationRound(QuantifiersEngine
* qe
) override
;
664 /** Add instantiations. */
665 int addInstantiations(Node q
,
666 InstMatch
& baseMatch
,
667 QuantifiersEngine
* qe
,
668 Trigger
* tparent
) override
;
669 /** Get active score. */
670 int getActiveScore(QuantifiersEngine
* qe
) override
;
673 /** quantified formula for the trigger term */
675 /** the trigger term */
676 Node d_match_pattern
;
677 /** equivalence class polarity information
679 * This stores the required polarity/equivalence class with this trigger.
680 * If d_eqc is non-null, we only produce matches { x->t } such that
681 * our context does not entail
682 * ( d_match_pattern*{ x->t } = d_eqc) if d_pol = true, or
683 * ( d_match_pattern*{ x->t } != d_eqc) if d_pol = false.
684 * where * denotes application of substitution.
688 /** Match pattern arg types.
689 * Cached values of d_match_pattern[i].getType().
691 std::vector
< TypeNode
> d_match_pattern_arg_types
;
692 /** The match operator d_match_pattern (see TermDb::getMatchOperator). */
694 /** Map from child number to variable index. */
695 std::map
< int, int > d_var_num
;
696 /** add instantiations, helper function.
698 * m is the current match we are building,
699 * addedLemmas is the number of lemmas we have added via calls to
700 * qe->getInstantiate()->aaddInstantiation(...),
701 * argIndex is the argument index in d_match_pattern we are currently
703 * tat is the term index we are currently traversing.
705 void addInstantiations(InstMatch
& m
,
706 QuantifiersEngine
* qe
,
709 quantifiers::TermArgTrie
* tat
);
710 };/* class InstMatchGeneratorSimple */