1 /********************* */
2 /*! \file inst_strategy_e_matching.cpp
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Morgan Deters, Mathias Preiner
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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 Implementation of e matching instantiation strategies
15 #include "theory/quantifiers/ematching/inst_strategy_e_matching.h"
16 #include "theory/quantifiers/ematching/inst_match_generator.h"
17 #include "theory/quantifiers/quant_relevance.h"
18 #include "theory/quantifiers/quantifiers_attributes.h"
19 #include "theory/quantifiers/term_database.h"
20 #include "theory/quantifiers/term_util.h"
21 #include "theory/quantifiers_engine.h"
22 #include "theory/theory_engine.h"
23 #include "util/random.h"
30 using namespace context
;
36 namespace quantifiers
{
39 //1 : user patterns (when user-pat!={resort,ignore}), auto-gen patterns (for non-user pattern quantifiers, or when user-pat={resort,ignore})
40 //2 : user patterns (when user-pat=resort), auto gen patterns (for user pattern quantifiers when user-pat=use)
42 // user-pat=interleave alternates between use and resort
44 struct sortQuantifiersForSymbol
{
45 QuantRelevance
* d_quant_rel
;
46 std::map
< Node
, Node
> d_op_map
;
47 bool operator() (Node i
, Node j
) {
48 int nqfsi
= d_quant_rel
->getNumQuantifiersForSymbol(d_op_map
[i
]);
49 int nqfsj
= d_quant_rel
->getNumQuantifiersForSymbol(d_op_map
[j
]);
52 }else if( nqfsi
>nqfsj
){
61 bool operator() (Node i
, Node j
) {
62 int wi
= Trigger::getTriggerWeight( i
);
63 int wj
= Trigger::getTriggerWeight( j
);
72 void InstStrategyUserPatterns::processResetInstantiationRound( Theory::Effort effort
){
73 Trace("inst-alg-debug") << "reset user triggers" << std::endl
;
75 for( std::map
< Node
, std::vector
< Trigger
* > >::iterator it
= d_user_gen
.begin(); it
!= d_user_gen
.end(); ++it
){
76 for( unsigned i
=0; i
<it
->second
.size(); i
++ ){
77 it
->second
[i
]->resetInstantiationRound();
78 it
->second
[i
]->reset( Node::null() );
81 Trace("inst-alg-debug") << "done reset user triggers" << std::endl
;
84 int InstStrategyUserPatterns::process( Node f
, Theory::Effort effort
, int e
){
86 return STATUS_UNFINISHED
;
89 d_quantEngine
->getInstUserPatMode() == options::UserPatMode::RESORT
? 2
92 return STATUS_UNFINISHED
;
93 }else if( e
==peffort
){
96 Trace("inst-alg") << "-> User-provided instantiate " << f
<< "..." << std::endl
;
97 if (d_quantEngine
->getInstUserPatMode() == options::UserPatMode::RESORT
)
99 for( unsigned i
=0; i
<d_user_gen_wait
[f
].size(); i
++ ){
100 Trigger
* t
= Trigger::mkTrigger( d_quantEngine
, f
, d_user_gen_wait
[f
][i
], true, Trigger::TR_RETURN_NULL
);
102 d_user_gen
[f
].push_back( t
);
105 d_user_gen_wait
[f
].clear();
108 for( unsigned i
=0; i
<d_user_gen
[f
].size(); i
++ ){
109 bool processTrigger
= true;
110 if( processTrigger
){
111 Trace("process-trigger") << " Process (user) ";
112 d_user_gen
[f
][i
]->debugPrint("process-trigger");
113 Trace("process-trigger") << "..." << std::endl
;
114 int numInst
= d_user_gen
[f
][i
]->addInstantiations();
115 Trace("process-trigger") << " Done, numInst = " << numInst
<< "." << std::endl
;
116 d_quantEngine
->d_statistics
.d_instantiations_user_patterns
+= numInst
;
117 if( d_user_gen
[f
][i
]->isMultiTrigger() ){
118 d_quantEngine
->d_statistics
.d_multi_trigger_instantiations
+= numInst
;
120 if( d_quantEngine
->inConflict() ){
127 return STATUS_UNKNOWN
;
130 void InstStrategyUserPatterns::addUserPattern( Node q
, Node pat
){
131 Assert(pat
.getKind() == INST_PATTERN
);
134 std::vector
< Node
> nodes
;
135 for( unsigned i
=0; i
<pat
.getNumChildren(); i
++ ){
136 Node pat_use
= Trigger::getIsUsableTrigger( pat
[i
], q
);
137 if( pat_use
.isNull() ){
138 Trace("trigger-warn") << "User-provided trigger is not usable : " << pat
<< " because of " << pat
[i
] << std::endl
;
142 nodes
.push_back( pat_use
);
146 Trace("user-pat") << "Add user pattern: " << pat
<< " for " << q
<< std::endl
;
148 if (d_quantEngine
->getInstUserPatMode() == options::UserPatMode::RESORT
)
150 d_user_gen_wait
[q
].push_back( nodes
);
154 Trigger
* t
= Trigger::mkTrigger( d_quantEngine
, q
, nodes
, true, Trigger::TR_MAKE_NEW
);
156 d_user_gen
[q
].push_back( t
);
158 Trace("trigger-warn") << "Failed to construct trigger : " << pat
<< " due to variable mismatch" << std::endl
;
164 InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers(QuantifiersEngine
* qe
,
166 : InstStrategy(qe
), d_quant_rel(qr
)
168 //how to select trigger terms
169 d_tr_strategy
= options::triggerSelMode();
170 //whether to select new triggers during the search
171 if( options::incrementTriggers() ){
172 d_regenerate_frequency
= 3;
175 d_regenerate_frequency
= 1;
176 d_regenerate
= false;
180 void InstStrategyAutoGenTriggers::processResetInstantiationRound( Theory::Effort effort
){
181 Trace("inst-alg-debug") << "reset auto-gen triggers" << std::endl
;
183 for( unsigned r
=0; r
<2; r
++ ){
184 for( std::map
< Node
, std::map
< Trigger
*, bool > >::iterator it
= d_auto_gen_trigger
[r
].begin(); it
!= d_auto_gen_trigger
[r
].end(); ++it
){
185 for( std::map
< Trigger
*, bool >::iterator itt
= it
->second
.begin(); itt
!= it
->second
.end(); ++itt
){
186 itt
->first
->resetInstantiationRound();
187 itt
->first
->reset( Node::null() );
191 d_processed_trigger
.clear();
192 Trace("inst-alg-debug") << "done reset auto-gen triggers" << std::endl
;
195 int InstStrategyAutoGenTriggers::process( Node f
, Theory::Effort effort
, int e
){
196 options::UserPatMode upMode
= d_quantEngine
->getInstUserPatMode();
197 if (hasUserPatterns(f
) && upMode
== options::UserPatMode::TRUST
)
199 return STATUS_UNKNOWN
;
203 int peffort
= (hasUserPatterns(f
) && upMode
!= options::UserPatMode::IGNORE
204 && upMode
!= options::UserPatMode::RESORT
)
208 return STATUS_UNFINISHED
;
210 Trace("inst-alg") << "-> Auto-gen instantiate " << f
<< "..." << std::endl
;
213 if( d_counter
.find( f
)==d_counter
.end() ){
218 gen
= d_regenerate
&& d_counter
[f
]%d_regenerate_frequency
==0;
224 generateTriggers( f
);
225 if( d_counter
[f
]==0 && d_auto_gen_trigger
[0][f
].empty() && d_auto_gen_trigger
[1][f
].empty() && f
.getNumChildren()==2 ){
226 Trace("trigger-warn") << "Could not find trigger for " << f
<< std::endl
;
231 // d_processed_trigger.clear();
232 // d_quantEngine->getEqualityQuery()->setLiberal( true );
234 if (options::triggerActiveSelMode() != options::TriggerActiveSelMode::ALL
)
237 Trigger
* max_trigger
= NULL
;
238 for( std::map
< Trigger
*, bool >::iterator itt
= d_auto_gen_trigger
[0][f
].begin(); itt
!= d_auto_gen_trigger
[0][f
].end(); ++itt
){
239 int score
= itt
->first
->getActiveScore();
240 if (options::triggerActiveSelMode()
241 == options::TriggerActiveSelMode::MIN
)
243 if( score
>=0 && ( score
<max_score
|| max_score
<0 ) ){
245 max_trigger
= itt
->first
;
250 if( score
>max_score
){
252 max_trigger
= itt
->first
;
255 d_auto_gen_trigger
[0][f
][itt
->first
] = false;
257 if( max_trigger
!=NULL
){
258 d_auto_gen_trigger
[0][f
][max_trigger
] = true;
262 bool hasInst
= false;
263 for( unsigned r
=0; r
<2; r
++ ){
264 for( std::map
< Trigger
*, bool >::iterator itt
= d_auto_gen_trigger
[r
][f
].begin(); itt
!= d_auto_gen_trigger
[r
][f
].end(); ++itt
){
265 Trigger
* tr
= itt
->first
;
267 bool processTrigger
= itt
->second
;
268 if( processTrigger
&& d_processed_trigger
[f
].find( tr
)==d_processed_trigger
[f
].end() ){
269 d_processed_trigger
[f
][tr
] = true;
270 Trace("process-trigger") << " Process ";
271 tr
->debugPrint("process-trigger");
272 Trace("process-trigger") << "..." << std::endl
;
273 int numInst
= tr
->addInstantiations();
274 hasInst
= numInst
>0 || hasInst
;
275 Trace("process-trigger") << " Done, numInst = " << numInst
<< "." << std::endl
;
276 d_quantEngine
->d_statistics
.d_instantiations_auto_gen
+= numInst
;
278 d_quantEngine
->d_statistics
.d_multi_trigger_instantiations
+= numInst
;
280 if( d_quantEngine
->inConflict() ){
286 if( d_quantEngine
->inConflict() || ( hasInst
&& options::multiTriggerPriority() ) ){
291 // d_quantEngine->getEqualityQuery()->setLiberal( false );
293 return STATUS_UNKNOWN
;
298 void InstStrategyAutoGenTriggers::generateTriggers( Node f
){
299 Trace("auto-gen-trigger-debug") << "Generate triggers for " << f
<< ", #var=" << f
[0].getNumChildren() << "..." << std::endl
;
300 if( d_patTerms
[0].find( f
)==d_patTerms
[0].end() ){
301 //determine all possible pattern terms based on trigger term selection strategy d_tr_strategy
302 d_patTerms
[0][f
].clear();
303 d_patTerms
[1][f
].clear();
304 bool ntrivTriggers
= options::relationalTriggers();
305 std::vector
< Node
> patTermsF
;
306 std::map
< Node
, inst::TriggerTermInfo
> tinfo
;
307 //well-defined function: can assume LHS is only trigger
308 if( options::quantFunWellDefined() ){
309 Node hd
= QuantAttributes::getFunDefHead( f
);
311 hd
= d_quantEngine
->getTermUtil()
312 ->substituteBoundVariablesToInstConstants(hd
, f
);
313 patTermsF
.push_back( hd
);
314 tinfo
[hd
].init( f
, hd
);
317 //otherwise, use algorithm for collecting pattern terms
318 if( patTermsF
.empty() ){
319 Node bd
= d_quantEngine
->getTermUtil()->getInstConstantBody( f
);
320 Trigger::collectPatTerms( f
, bd
, patTermsF
, d_tr_strategy
, d_user_no_gen
[f
], tinfo
, true );
323 std::sort( patTermsF
.begin(), patTermsF
.end(), st
);
325 if( Trace
.isOn("auto-gen-trigger-debug") ){
326 Trace("auto-gen-trigger-debug") << "Collected pat terms for " << bd
<< ", no-patterns : " << d_user_no_gen
[f
].size() << std::endl
;
327 for( unsigned i
=0; i
<patTermsF
.size(); i
++ ){
328 Assert(tinfo
.find(patTermsF
[i
]) != tinfo
.end());
329 Trace("auto-gen-trigger-debug") << " " << patTermsF
[i
] << std::endl
;
330 Trace("auto-gen-trigger-debug2") << " info = [" << tinfo
[patTermsF
[i
]].d_reqPol
<< ", " << tinfo
[patTermsF
[i
]].d_reqPolEq
<< ", " << tinfo
[patTermsF
[i
]].d_fv
.size() << "]" << std::endl
;
332 Trace("auto-gen-trigger-debug") << std::endl
;
335 //sort into single/multi triggers, calculate which terms should not be considered
336 std::map
< Node
, bool > vcMap
;
337 std::map
< Node
, bool > rmPatTermsF
;
338 int last_weight
= -1;
339 for( unsigned i
=0; i
<patTermsF
.size(); i
++ ){
340 Assert(patTermsF
[i
].getKind() != NOT
);
342 for( unsigned j
=0; j
<tinfo
[ patTermsF
[i
] ].d_fv
.size(); j
++ ){
343 if( vcMap
.find( tinfo
[ patTermsF
[i
] ].d_fv
[j
] )==vcMap
.end() ){
344 vcMap
[tinfo
[ patTermsF
[i
] ].d_fv
[j
]] = true;
348 int curr_w
= Trigger::getTriggerWeight( patTermsF
[i
] );
349 // triggers whose value is maximum (2) are considered expendable.
350 if (ntrivTriggers
&& !newVar
&& last_weight
!= -1 && curr_w
> last_weight
353 Trace("auto-gen-trigger-debug") << "...exclude expendible non-trivial trigger : " << patTermsF
[i
] << std::endl
;
354 rmPatTermsF
[patTermsF
[i
]] = true;
356 last_weight
= curr_w
;
359 d_num_trigger_vars
[f
] = vcMap
.size();
360 if( d_num_trigger_vars
[f
]>0 && d_num_trigger_vars
[f
]<f
[0].getNumChildren() ){
361 Trace("auto-gen-trigger-partial") << "Quantified formula : " << f
<< std::endl
;
362 Trace("auto-gen-trigger-partial") << "...does not contain all variables in triggers!!!" << std::endl
;
363 // Invoke partial trigger strategy: partition variables of quantified
364 // formula into (X,Y) where X are contained in a trigger and Y are not.
365 // We then force a split of the quantified formula so that it becomes:
366 // forall X. forall Y. P( X, Y )
367 // and hence is treatable by E-matching. We only do this for "standard"
368 // quantified formulas (those with only two children), since this
369 // technique should not be used for e.g. quantifiers marked for
370 // quantifier elimination.
372 QuantAttributes::computeQuantAttributes(f
, qa
);
373 if (options::partialTriggers() && qa
.isStandard())
375 std::vector
< Node
> vcs
[2];
376 for( unsigned i
=0; i
<f
[0].getNumChildren(); i
++ ){
377 Node ic
= d_quantEngine
->getTermUtil()->getInstantiationConstant( f
, i
);
378 vcs
[ vcMap
.find( ic
)==vcMap
.end() ? 0 : 1 ].push_back( f
[0][i
] );
380 for( unsigned i
=0; i
<2; i
++ ){
381 d_vc_partition
[i
][f
] = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST
, vcs
[i
] );
387 for( unsigned i
=0; i
<patTermsF
.size(); i
++ ){
388 Node pat
= patTermsF
[i
];
389 if( rmPatTermsF
.find( pat
)==rmPatTermsF
.end() ){
390 Trace("auto-gen-trigger-debug") << "...processing pattern " << pat
<< std::endl
;
392 //process the pattern: if it has a required polarity, consider it
393 Assert(tinfo
.find(pat
) != tinfo
.end());
394 int rpol
= tinfo
[pat
].d_reqPol
;
395 Node rpoleq
= tinfo
[pat
].d_reqPolEq
;
396 unsigned num_fv
= tinfo
[pat
].d_fv
.size();
397 Trace("auto-gen-trigger-debug") << "...required polarity for " << pat
<< " is " << rpol
<< ", eq=" << rpoleq
<< std::endl
;
399 Assert(rpol
== 1 || rpol
== -1);
400 if( Trigger::isRelationalTrigger( pat
) ){
401 pat
= rpol
==-1 ? pat
.negate() : pat
;
403 Assert(Trigger::isAtomicTrigger(pat
));
404 if( pat
.getType().isBoolean() && rpoleq
.isNull() ){
405 if (options::literalMatchMode() == options::LiteralMatchMode::USE
)
407 pat
= NodeManager::currentNM()->mkNode( EQUAL
, pat
, NodeManager::currentNM()->mkConst( rpol
==-1 ) ).negate();
409 else if (options::literalMatchMode()
410 != options::LiteralMatchMode::NONE
)
412 pat
= NodeManager::currentNM()->mkNode( EQUAL
, pat
, NodeManager::currentNM()->mkConst( rpol
==1 ) );
415 Assert(!rpoleq
.isNull());
417 if (options::literalMatchMode()
418 != options::LiteralMatchMode::NONE
)
420 //all equivalence classes except rpoleq
421 pat
= NodeManager::currentNM()->mkNode( EQUAL
, pat
, rpoleq
).negate();
424 if (options::literalMatchMode()
425 == options::LiteralMatchMode::AGG
)
427 //only equivalence class rpoleq
428 pat
= NodeManager::currentNM()->mkNode( EQUAL
, pat
, rpoleq
);
430 //all equivalence classes that are not disequal to rpoleq TODO?
434 Trace("auto-gen-trigger-debug") << "...got : " << pat
<< std::endl
;
436 if( Trigger::isRelationalTrigger( pat
) ){
437 //consider both polarities
438 addPatternToPool( f
, pat
.negate(), num_fv
, mpat
);
441 addPatternToPool( f
, pat
, num_fv
, mpat
);
444 //tinfo not used below this point
445 d_made_multi_trigger
[f
] = false;
446 Trace("auto-gen-trigger") << "Single trigger pool for " << f
<< " : " << std::endl
;
447 for( unsigned i
=0; i
<d_patTerms
[0][f
].size(); i
++ ){
448 Trace("auto-gen-trigger") << " " << d_patTerms
[0][f
][i
] << std::endl
;
450 if( !d_patTerms
[1][f
].empty() ){
451 Trace("auto-gen-trigger") << "Multi-trigger term pool for " << f
<< " : " << std::endl
;
452 for( unsigned i
=0; i
<d_patTerms
[1][f
].size(); i
++ ){
453 Trace("auto-gen-trigger") << " " << d_patTerms
[1][f
][i
] << std::endl
;
458 unsigned rmin
= d_patTerms
[0][f
].empty() ? 1 : 0;
459 unsigned rmax
= options::multiTriggerWhenSingle() ? 1 : rmin
;
460 for( unsigned r
=rmin
; r
<=rmax
; r
++ ){
461 std::vector
< Node
> patTerms
;
462 for( int i
=0; i
<(int)d_patTerms
[r
][f
].size(); i
++ ){
463 if( r
==1 || d_single_trigger_gen
.find( d_patTerms
[r
][f
][i
] )==d_single_trigger_gen
.end() ){
464 patTerms
.push_back( d_patTerms
[r
][f
][i
] );
467 if( !patTerms
.empty() ){
468 Trace("auto-gen-trigger") << "Generate trigger for " << f
<< std::endl
;
469 //sort terms based on relevance
470 if( options::relevantTriggers() ){
472 sortQuantifiersForSymbol sqfs
;
473 sqfs
.d_quant_rel
= d_quant_rel
;
474 for( unsigned i
=0; i
<patTerms
.size(); i
++ ){
475 Assert(d_pat_to_mpat
.find(patTerms
[i
]) != d_pat_to_mpat
.end());
476 Assert(d_pat_to_mpat
[patTerms
[i
]].hasOperator());
477 sqfs
.d_op_map
[ patTerms
[i
] ] = d_pat_to_mpat
[patTerms
[i
]].getOperator();
479 //sort based on # occurrences (this will cause Trigger to select rarer symbols)
480 std::sort( patTerms
.begin(), patTerms
.end(), sqfs
);
481 if (Debug
.isOn("relevant-trigger"))
483 Debug("relevant-trigger")
484 << "Terms based on relevance: " << std::endl
;
485 for (const Node
& p
: patTerms
)
487 Debug("relevant-trigger")
488 << " " << p
<< " from " << d_pat_to_mpat
[p
] << " (";
489 Debug("relevant-trigger")
490 << d_quant_rel
->getNumQuantifiersForSymbol(
491 d_pat_to_mpat
[p
].getOperator())
496 //now, generate the trigger...
498 if( d_is_single_trigger
[ patTerms
[0] ] ){
499 tr
= Trigger::mkTrigger( d_quantEngine
, f
, patTerms
[0], false, Trigger::TR_RETURN_NULL
, d_num_trigger_vars
[f
] );
500 d_single_trigger_gen
[ patTerms
[0] ] = true;
502 //only generate multi trigger if option set, or if no single triggers exist
503 if( !d_patTerms
[0][f
].empty() ){
504 if( options::multiTriggerWhenSingle() ){
505 Trace("multi-trigger-debug") << "Resort to choosing multi-triggers..." << std::endl
;
510 // if we are re-generating triggers, shuffle based on some method
511 if (d_made_multi_trigger
[f
])
513 std::shuffle(patTerms
.begin(),
515 Random::getRandom()); // shuffle randomly
519 d_made_multi_trigger
[f
] = true;
521 //will possibly want to get an old trigger
522 tr
= Trigger::mkTrigger( d_quantEngine
, f
, patTerms
, false, Trigger::TR_GET_OLD
, d_num_trigger_vars
[f
] );
526 //if we are generating additional triggers...
527 if( !tr
->isMultiTrigger() ){
529 if( index
<patTerms
.size() ){
530 //Notice() << "check add additional" << std::endl;
531 //check if similar patterns exist, and if so, add them additionally
532 unsigned nqfs_curr
= 0;
533 if( options::relevantTriggers() ){
534 nqfs_curr
= d_quant_rel
->getNumQuantifiersForSymbol(
535 patTerms
[0].getOperator());
539 while( success
&& index
<patTerms
.size() && d_is_single_trigger
[ patTerms
[index
] ] ){
541 if (!options::relevantTriggers()
542 || d_quant_rel
->getNumQuantifiersForSymbol(
543 patTerms
[index
].getOperator())
546 d_single_trigger_gen
[ patTerms
[index
] ] = true;
547 Trigger
* tr2
= Trigger::mkTrigger( d_quantEngine
, f
, patTerms
[index
], false, Trigger::TR_RETURN_NULL
, d_num_trigger_vars
[f
] );
548 addTrigger( tr2
, f
);
553 //Notice() << "done check add additional" << std::endl;
561 void InstStrategyAutoGenTriggers::addPatternToPool( Node q
, Node pat
, unsigned num_fv
, Node mpat
) {
562 d_pat_to_mpat
[pat
] = mpat
;
563 unsigned num_vars
= options::partialTriggers() ? d_num_trigger_vars
[q
] : q
[0].getNumChildren();
564 if( num_fv
==num_vars
&& ( options::pureThTriggers() || !Trigger::isPureTheoryTrigger( pat
) ) ){
565 d_patTerms
[0][q
].push_back( pat
);
566 d_is_single_trigger
[ pat
] = true;
568 d_patTerms
[1][q
].push_back( pat
);
569 d_is_single_trigger
[ pat
] = false;
574 void InstStrategyAutoGenTriggers::addTrigger( inst::Trigger
* tr
, Node q
) {
576 if( d_num_trigger_vars
[q
]<q
[0].getNumChildren() ){
577 //partial trigger : generate implication to mark user pattern
579 d_quantEngine
->getTermUtil()->substituteInstConstantsToBoundVariables(
580 tr
->getInstPattern(), q
);
581 Node ipl
= NodeManager::currentNM()->mkNode(INST_PATTERN_LIST
, pat
);
582 Node qq
= NodeManager::currentNM()->mkNode( FORALL
, d_vc_partition
[1][q
], NodeManager::currentNM()->mkNode( FORALL
, d_vc_partition
[0][q
], q
[1] ), ipl
);
583 Trace("auto-gen-trigger-partial") << "Make partially specified user pattern: " << std::endl
;
584 Trace("auto-gen-trigger-partial") << " " << qq
<< std::endl
;
585 Node lem
= NodeManager::currentNM()->mkNode( OR
, q
.negate(), qq
);
586 d_quantEngine
->addLemma( lem
);
589 if( tr
->isMultiTrigger() ){
590 //disable all other multi triggers
591 for( std::map
< Trigger
*, bool >::iterator it
= d_auto_gen_trigger
[1][q
].begin(); it
!= d_auto_gen_trigger
[1][q
].end(); ++it
){
592 d_auto_gen_trigger
[1][q
][ it
->first
] = false;
598 //making it during an instantiation round, so must reset
599 if( d_auto_gen_trigger
[tindex
][q
].find( tr
)==d_auto_gen_trigger
[tindex
][q
].end() ){
600 tr
->resetInstantiationRound();
601 tr
->reset( Node::null() );
603 d_auto_gen_trigger
[tindex
][q
][tr
] = true;
608 bool InstStrategyAutoGenTriggers::hasUserPatterns( Node q
) {
609 if( q
.getNumChildren()==3 ){
610 std::map
< Node
, bool >::iterator it
= d_hasUserPatterns
.find( q
);
611 if( it
==d_hasUserPatterns
.end() ){
613 for( unsigned i
=0; i
<q
[2].getNumChildren(); i
++ ){
614 if( q
[2][i
].getKind()==INST_PATTERN
){
619 d_hasUserPatterns
[q
] = hasPat
;
629 void InstStrategyAutoGenTriggers::addUserNoPattern( Node q
, Node pat
) {
630 Assert(pat
.getKind() == INST_NO_PATTERN
&& pat
.getNumChildren() == 1);
631 if( std::find( d_user_no_gen
[q
].begin(), d_user_no_gen
[q
].end(), pat
[0] )==d_user_no_gen
[q
].end() ){
632 Trace("user-pat") << "Add user no-pattern: " << pat
[0] << " for " << q
<< std::endl
;
633 d_user_no_gen
[q
].push_back( pat
[0] );
637 } /* CVC4::theory::quantifiers namespace */
638 } /* CVC4::theory namespace */
639 } /* CVC4 namespace */