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
21 #include "theory/quantifiers/inst_match_trie.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/ematching/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 * It returns the number of instantiations added using calls to calls to
93 * Instantiate::addInstantiation(...).
95 virtual int addInstantiations(Node q
,
96 QuantifiersEngine
* qe
,
103 * A heuristic value indicating how active this generator is.
105 virtual int getActiveScore( QuantifiersEngine
* qe
) { return 0; }
107 /** send instantiation
109 * This method sends instantiation, specified by m, to the parent trigger
110 * object, which will in turn make a call to
111 * Instantiate::addInstantiation(...). This method returns true if a
112 * call to Instantiate::addInstantiation(...) was successfully made,
113 * indicating that an instantiation was enqueued in the quantifier engine's
116 bool sendInstantiation(Trigger
* tparent
, InstMatch
& m
);
117 };/* class IMGenerator */
119 class CandidateGenerator
;
121 /** InstMatchGenerator class
123 * This is the default generator class for non-simple single triggers, that is,
124 * triggers composed of a single term with nested term applications.
125 * For example, { f( y, f( x, a ) ) } and { f( g( x ), a ) } are non-simple
128 * Handling non-simple triggers is done by constructing a linked list of
129 * InstMatchGenerator classes (see mkInstMatchGenerator), where each
130 * InstMatchGenerator has a "d_next" pointer. If d_next is NULL,
131 * then this is the end of the InstMatchGenerator and the last
132 * InstMatchGenerator is responsible for finalizing the instantiation.
134 * For (EX1), for the trigger f( y, f( x, a ) ), we construct the linked list:
136 * [ f( y, f( x, a ) ) ] -> [ f( x, a ) ] -> NULL
138 * In a call to getNextMatch,
139 * if we match against a ground term f( b, c ), then the first InstMatchGenerator
140 * in this list binds y to b, and tells the InstMatchGenerator [ f( x, a ) ] to
141 * match f-applications in the equivalence class of c.
143 * CVC4 employs techniques that ensure that the number of instantiations
144 * is worst-case polynomial wrt the number of ground terms.
145 * Consider the axiom/pattern/context (EX2) :
147 * axiom : forall x1 x2 x3 x4. F[ x1...x4 ]
149 * trigger : P( f( x1 ), f( x2 ), f( x3 ), f( x4 ) )
151 * ground context : ~P( a, a, a, a ), a = f( c_1 ) = ... = f( c_100 )
153 * If E-matching were applied exhaustively, then x1, x2, x3, x4 would be
154 * instantiated with all combinations of c_1, ... c_100, giving 100^4
157 * Instead, we enforce that at most 1 instantiation is produced for a
158 * ( pattern, ground term ) pair per round. Meaning, only one instantiation is
159 * generated when matching P( a, a, a, a ) against the generator
160 * [P( f( x1 ), f( x2 ), f( x3 ), f( x4 ) )]. For details, see Section 3 of
161 * Reynolds, Vampire 2016.
163 * To enforce these policies, we use a flag "d_active_add" which dictates the
164 * behavior of the last element in the linked list. If d_active_add is
165 * true -> a call to getNextMatch(...) returns 1 only if adding the
166 * instantiation via a call to IMGenerator::sendInstantiation(...)
167 * successfully enqueues a lemma via a call to
168 * Instantiate::addInstantiation(...). This call may fail e.g. if we
169 * have already added the instantiation, or the instantiation is
171 * false -> a call to getNextMatch(...) returns 1 whenever an m is
172 * constructed, where typically the caller would use m.
173 * This is important since a return value >0 signals that the current matched
174 * terms should be flushed. Consider the above example (EX1), where
175 * [ f(y,f(x,a)) ] is being matched against f(b,c),
176 * [ f(x,a) ] is being matched against f(d,a) where c=f(d,a)
177 * A successfully added instantiation { x->d, y->b } here signals we should
178 * not produce further instantiations that match f(y,f(x,a)) with f(b,c).
180 * A number of special cases of triggers are covered by this generator (see
181 * implementation of initialize), including :
182 * Literal triggers, e.g. x >= a, ~x = y
183 * Selector triggers, e.g. head( x )
184 * Triggers with invertible subterms, e.g. f( x+1 )
185 * Variable triggers, e.g. x
187 * All triggers above can be in the context of an equality, e.g.
188 * { f( y, f( x, a ) ) = b } is a trigger that matches f( y, f( x, a ) ) to
189 * ground terms in the equivalence class of b.
190 * { ~f( y, f( x, a ) ) = b } is a trigger that matches f( y, f( x, a ) ) to any
191 * ground terms not in the equivalence class of b.
193 class InstMatchGenerator
: public IMGenerator
{
196 ~InstMatchGenerator() override
;
198 /** Reset instantiation round. */
199 void resetInstantiationRound(QuantifiersEngine
* qe
) override
;
201 bool reset(Node eqc
, QuantifiersEngine
* qe
) override
;
202 /** Get the next match. */
203 int getNextMatch(Node q
,
205 QuantifiersEngine
* qe
,
206 Trigger
* tparent
) override
;
207 /** Add instantiations. */
208 int addInstantiations(Node q
,
209 QuantifiersEngine
* qe
,
210 Trigger
* tparent
) override
;
212 /** set active add flag (true by default)
214 * If active add is true, we call sendInstantiation in calls to getNextMatch,
215 * instead of returning the match. This is necessary so that we can ensure
216 * policies that are dependent upon knowing when instantiations are
217 * successfully added to the output channel through
218 * Instantiate::addInstantiation(...).
220 void setActiveAdd(bool val
);
221 /** Get active score for this inst match generator
223 * See Trigger::getActiveScore for details.
225 int getActiveScore(QuantifiersEngine
* qe
) override
;
228 * Exclude matching d_match_pattern with Node n on subsequent calls to
231 void excludeMatch(Node n
) { d_curr_exclude_match
[n
] = true; }
232 /** Get current match.
233 * Returns the term we are currently matching.
235 Node
getCurrentMatch() { return d_curr_matched
; }
236 /** set that this match generator is independent
238 * A match generator is indepndent when this generator fails to produce a
239 * match in a call to getNextMatch, the overall matching fails.
241 void setIndependent() { d_independent_gen
= true; }
242 //-------------------------------construction of inst match generators
243 /** mkInstMatchGenerator for single triggers, calls the method below */
244 static InstMatchGenerator
* mkInstMatchGenerator(Node q
,
246 QuantifiersEngine
* qe
);
247 /** mkInstMatchGenerator for the multi trigger case
249 * This linked list of InstMatchGenerator classes with one
250 * InstMatchGeneratorMultiLinear at the head and a list of trailing
251 * InstMatchGenerators corresponding to each unique subterm of pats with
254 static InstMatchGenerator
* mkInstMatchGeneratorMulti(Node q
,
255 std::vector
<Node
>& pats
,
256 QuantifiersEngine
* qe
);
257 /** mkInstMatchGenerator
259 * This generates a linked list of InstMatchGenerators for each unique
260 * subterm of pats with free variables.
262 * q is the quantified formula associated with the generator we are making
263 * pats is a set of terms we are making InstMatchGenerator nodes for
264 * qe is a pointer to the quantifiers engine (used for querying necessary
265 * information during initialization) pat_map_init maps from terms to
266 * generators we have already made for them.
268 * It calls initialize(...) for all InstMatchGenerators generated by this call.
270 static InstMatchGenerator
* mkInstMatchGenerator(
272 std::vector
<Node
>& pats
,
273 QuantifiersEngine
* qe
,
274 std::map
<Node
, InstMatchGenerator
*>& pat_map_init
);
275 //-------------------------------end construction of inst match generators
280 * These are intentionally private, and are called during linked list
281 * construction in mkInstMatchGenerator.
283 InstMatchGenerator(Node pat
);
284 InstMatchGenerator();
285 /** The pattern we are producing matches for.
287 * This term and d_match_pattern can be different since this
288 * term may involve information regarding phase and (dis)equality entailment,
289 * or other special cases of Triggers.
291 * For example, for the trigger for P( x ) = false, which matches P( x ) with
292 * P( t ) in the equivalence class of false,
293 * P( x ) = false is d_pattern
294 * P( x ) is d_match_pattern
295 * Another example, for pure theory triggers like head( x ), we have
296 * head( x ) is d_pattern
297 * x is d_match_pattern
298 * since head( x ) can match any (List) datatype term x.
300 * If null, this is a multi trigger that is merging matches from d_children,
301 * which is used in InstMatchGeneratorMulti.
304 /** The match pattern
305 * This is the term that is matched against ground terms,
306 * see examples above.
308 Node d_match_pattern
;
309 /** The current term we are matching. */
311 /** do we need to call reset on this generator? */
313 /** candidate generator
314 * This is the back-end utility for InstMatchGenerator.
315 * It generates a stream of candidate terms to match against d_match_pattern
316 * below, dependending upon what kind of term we are matching
317 * (e.g. a matchable term, a variable, a relation, etc.).
319 CandidateGenerator
* d_cg
;
320 /** children generators
321 * These match generators correspond to the children of the term
322 * we are matching with this generator.
323 * For example [ f( x, a ) ] is a child of [ f( y, f( x, a ) ) ]
324 * in the example (EX1) above.
326 std::vector
<InstMatchGenerator
*> d_children
;
327 /** for each child, the index in the term
328 * For example [ f( x, a ) ] has index 1 in [ f( y, f( x, a ) ) ]
329 * in the example (EX1) above, indicating it is the 2nd child
332 std::vector
<int> d_children_index
;
335 * If d_match_pattern is an instantiation constant, then this is a singleton
336 * vector containing the variable number of the d_match_pattern itself.
337 * If d_match_patterm is a term of the form f( t1, ..., tn ), then for each
338 * index i, d_children[i] stores the type of node ti is, where:
339 * >= 0 : variable (indicates its number),
343 std::vector
<int> d_children_types
;
344 /** The next generator in the linked list
345 * that this generator is a part of.
347 InstMatchGenerator
* d_next
;
348 /** The equivalence class we are currently matching in. */
350 /** If non-null, then this is a relational trigger of the form x ~
354 * Stores the terms we are not allowed to match.
355 * These can for instance be specified by the smt2
356 * extended syntax (! ... :no-pattern).
358 std::map
<Node
, bool> d_curr_exclude_match
;
359 /** Current first candidate
360 * Used in a key fail-quickly optimization which generates
361 * the first candidate term to match during reset().
363 Node d_curr_first_candidate
;
364 /** Indepdendent generate
365 * If this flag is true, failures to match should be cached.
367 bool d_independent_gen
;
368 /** active add flag, described above. */
370 /** cached value of d_match_pattern.getType() */
371 TypeNode d_match_pattern_type
;
372 /** the match operator for d_match_pattern
374 * See TermDatabase::getMatchOperator for details on match operators.
376 Node d_match_pattern_op
;
377 /** get the match against ground term or formula t.
379 * d_match_pattern and t should have the same shape, that is,
380 * their match operator (see TermDatabase::getMatchOperator) is the same.
381 * only valid for use where !d_match_pattern.isNull().
384 Node q
, Node t
, InstMatch
& m
, QuantifiersEngine
* qe
, Trigger
* tparent
);
385 /** Initialize this generator.
387 * q is the quantified formula associated with this generator.
389 * This constructs the appropriate information about what
390 * patterns we are matching and children generators.
392 * It may construct new (child) generators needed to implement
393 * the matching algorithm for this term. For each new generator
394 * constructed in this way, it adds them to gens.
396 void initialize(Node q
,
397 QuantifiersEngine
* qe
,
398 std::vector
<InstMatchGenerator
*>& gens
);
399 /** Continue next match
401 * This is called during getNextMatch when the current generator in the linked
402 * list succesfully satisfies its matching constraint. This function either
403 * calls getNextMatch of the next element in the linked list, or finalizes the
404 * match (calling sendInstantiation(...) if active add is true, or returning a
405 * value >0 if active add is false). Its return value has the same semantics
408 int continueNextMatch(Node q
,
410 QuantifiersEngine
* qe
,
412 /** Get inst match generator
414 * Gets the InstMatchGenerator that implements the
415 * appropriate matching algorithm for n within q
416 * within a linked list of InstMatchGenerators.
418 static InstMatchGenerator
* getInstMatchGenerator(Node q
, Node n
);
419 };/* class InstMatchGenerator */
421 /** match generator for Boolean term ITEs
422 * This handles the special case of triggers that look like ite( x, BV1, BV0 ).
424 class VarMatchGeneratorBooleanTerm
: public InstMatchGenerator
{
426 VarMatchGeneratorBooleanTerm( Node var
, Node comp
);
429 bool reset(Node eqc
, QuantifiersEngine
* qe
) override
434 /** Get the next match. */
435 int getNextMatch(Node q
,
437 QuantifiersEngine
* qe
,
438 Trigger
* tparent
) override
;
441 /** stores the true branch of the Boolean ITE */
443 /** stores whether we have written a value for var in the current match. */
447 /** match generator for purified terms
448 * This handles the special case of invertible terms like x+1 (see
449 * Trigger::getTermInversionVariable).
451 class VarMatchGeneratorTermSubs
: public InstMatchGenerator
{
453 VarMatchGeneratorTermSubs( Node var
, Node subs
);
456 bool reset(Node eqc
, QuantifiersEngine
* qe
) override
461 /** Get the next match. */
462 int getNextMatch(Node q
,
464 QuantifiersEngine
* qe
,
465 Trigger
* tparent
) override
;
468 /** variable we are matching (x in the example x+1). */
470 /** cache of d_var.getType() */
472 /** The substitution for what we match (x-1 in the example x+1). */
474 /** stores whether we have written a value for d_var in the current match. */
478 /** InstMatchGeneratorMultiLinear class
480 * This is the default implementation of multi-triggers.
482 * Handling multi-triggers using this class is done by constructing a linked
483 * list of InstMatchGenerator classes (see mkInstMatchGeneratorMulti), with one
484 * InstMatchGeneratorMultiLinear at the head and a list of trailing
485 * InstMatchGenerators.
487 * CVC4 employs techniques that ensure that the number of instantiations
488 * is worst-case polynomial wrt the number of ground terms, where this class
489 * lifts this policy to multi-triggers. In particular consider
491 * multi-trigger : { f( x1 ), f( x2 ), f( x3 ), f( x4 ) }
493 * For this multi-trigger, we insist that for each i=1...4, and each ground term
494 * t, there is at most 1 instantiation added as a result of matching
495 * ( f( x1 ), f( x2 ), f( x3 ), f( x4 ) )
496 * against ground terms of the form
497 * ( s_1, s_2, s_3, s_4 ) where t = s_i for i=1,...,4.
498 * Meaning we add instantiations for the multi-trigger
499 * ( f( x1 ), f( x2 ), f( x3 ), f( x4 ) ) based on matching pairwise against:
500 * ( f( c_i11 ), f( c_i21 ), f( c_i31 ), f( c_i41 ) )
501 * ( f( c_i12 ), f( c_i22 ), f( c_i32 ), f( c_i42 ) )
502 * ( f( c_i13 ), f( c_i23 ), f( c_i33 ), f( c_i43 ) )
503 * Where we require c_i{jk} != c_i{jl} for each i=1...4, k != l.
505 * For example, we disallow adding instantiations based on matching against both
506 * ( f( c_1 ), f( c_2 ), f( c_4 ), f( c_6 ) ) and
507 * ( f( c_1 ), f( c_3 ), f( c_5 ), f( c_7 ) )
508 * against ( f( x1 ), f( x2 ), f( x3 ), f( x4 ) ), since f( c_1 ) is matched
509 * against f( x1 ) twice.
511 * This policy can be disabled by --no-multi-trigger-linear.
514 class InstMatchGeneratorMultiLinear
: public InstMatchGenerator
{
515 friend class InstMatchGenerator
;
519 bool reset(Node eqc
, QuantifiersEngine
* qe
) override
;
520 /** Get the next match. */
521 int getNextMatch(Node q
,
523 QuantifiersEngine
* qe
,
524 Trigger
* tparent
) override
;
527 /** reset the children of this generator */
528 int resetChildren(QuantifiersEngine
* qe
);
530 InstMatchGeneratorMultiLinear(Node q
,
531 std::vector
<Node
>& pats
,
532 QuantifiersEngine
* qe
);
533 };/* class InstMatchGeneratorMulti */
535 /** InstMatchGeneratorMulti
537 * This is an earlier implementation of multi-triggers
538 * that is enabled by --multi-trigger-cache.
539 * This generator takes the product of instantiations
540 * found by single trigger matching, and does
541 * not have the guarantee that the number of
542 * instantiations is polynomial wrt the number of
545 class InstMatchGeneratorMulti
: public IMGenerator
{
548 InstMatchGeneratorMulti(Node q
,
549 std::vector
<Node
>& pats
,
550 QuantifiersEngine
* qe
);
552 ~InstMatchGeneratorMulti() override
;
554 /** Reset instantiation round. */
555 void resetInstantiationRound(QuantifiersEngine
* qe
) override
;
557 bool reset(Node eqc
, QuantifiersEngine
* qe
) override
;
558 /** Add instantiations. */
559 int addInstantiations(Node q
,
560 QuantifiersEngine
* qe
,
561 Trigger
* tparent
) override
;
565 typedef std::pair
< std::pair
< int, int >, InstMatchTrie
* > IndexedTrie
;
566 /** process new match
568 * Called during addInstantiations(...).
569 * Indicates we produced a match m for child fromChildIndex
570 * addedLemmas is how many instantiations we succesfully send
571 * via IMGenerator::sendInstantiation(...) calls.
573 void processNewMatch(QuantifiersEngine
* qe
,
578 /** helper for process new match
579 * tr is the inst match trie (term index) we are currently traversing.
580 * trieIndex is depth we are in trie tr.
581 * childIndex is the index of the term in the multi trigger we are currently
583 * endChildIndex is the index of the term in the multi trigger that generated
584 * a new term, and hence we will end when the product
585 * computed by this function returns to.
586 * modEq is whether we are matching modulo equality.
588 void processNewInstantiations(QuantifiersEngine
* qe
,
597 /** Map from pattern nodes to indices of variables they contain. */
598 std::map
< Node
, std::vector
< int > > d_var_contains
;
599 /** Map from variable indices to pattern nodes that contain them. */
600 std::map
< int, std::vector
< Node
> > d_var_to_node
;
601 /** quantified formula we are producing matches for */
603 /** children generators
604 * These are inst match generators for each term in the multi trigger.
606 std::vector
< InstMatchGenerator
* > d_children
;
607 /** variable orderings
608 * Stores a heuristically determined variable ordering (unique
609 * variables first) for each term in the multi trigger.
611 std::map
< unsigned, InstMatchTrie::ImtIndexOrder
* > d_imtio
;
612 /** inst match tries for each child node
613 * This data structure stores all InstMatch objects generated
614 * by matching for each term in the multi trigger.
616 std::vector
< InstMatchTrieOrdered
> d_children_trie
;
617 };/* class InstMatchGeneratorMulti */
619 /** InstMatchGeneratorSimple class
621 * This is the default generator class for simple single triggers.
622 * For example, { f( x, a ) }, { f( x, x ) } and { f( x, y ) } are simple single
623 * triggers. In practice, around 70-90% of triggers are simple single triggers.
625 * Notice that simple triggers also can have an attached polarity.
626 * For example, { P( x ) = false }, { f( x, y ) = a } and { ~f( a, x ) = b } are
627 * simple single triggers.
629 * The implementation traverses the term indices in TermDatabase for adding
630 * instantiations, which is more efficient than the techniques required for
631 * handling non-simple single triggers.
633 * In contrast to other instantiation generators, it does not call
634 * IMGenerator::sendInstantiation and for performance reasons instead calls
635 * qe->getInstantiate()->addInstantiation(...) directly.
637 class InstMatchGeneratorSimple
: public IMGenerator
{
640 InstMatchGeneratorSimple(Node q
, Node pat
, QuantifiersEngine
* qe
);
642 /** Reset instantiation round. */
643 void resetInstantiationRound(QuantifiersEngine
* qe
) override
;
644 /** Add instantiations. */
645 int addInstantiations(Node q
,
646 QuantifiersEngine
* qe
,
647 Trigger
* tparent
) override
;
648 /** Get active score. */
649 int getActiveScore(QuantifiersEngine
* qe
) override
;
652 /** quantified formula for the trigger term */
654 /** the trigger term */
655 Node d_match_pattern
;
656 /** equivalence class polarity information
658 * This stores the required polarity/equivalence class with this trigger.
659 * If d_eqc is non-null, we only produce matches { x->t } such that
660 * our context does not entail
661 * ( d_match_pattern*{ x->t } = d_eqc) if d_pol = true, or
662 * ( d_match_pattern*{ x->t } != d_eqc) if d_pol = false.
663 * where * denotes application of substitution.
667 /** Match pattern arg types.
668 * Cached values of d_match_pattern[i].getType().
670 std::vector
< TypeNode
> d_match_pattern_arg_types
;
671 /** The match operator d_match_pattern (see TermDb::getMatchOperator). */
673 /** Map from child number to variable index. */
674 std::map
< int, int > d_var_num
;
675 /** add instantiations, helper function.
677 * m is the current match we are building,
678 * addedLemmas is the number of lemmas we have added via calls to
679 * qe->getInstantiate()->aaddInstantiation(...),
680 * argIndex is the argument index in d_match_pattern we are currently
682 * tat is the term index we are currently traversing.
684 void addInstantiations(InstMatch
& m
,
685 QuantifiersEngine
* qe
,
688 quantifiers::TermArgTrie
* tat
);
689 };/* class InstMatchGeneratorSimple */