1 /********************* */
2 /*! \file inst_strategy_e_matching.cpp
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Morgan Deters, Aina Niemetz
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 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
;
88 int peffort
= d_quantEngine
->getInstUserPatMode()==USER_PAT_MODE_RESORT
? 2 : 1;
90 return STATUS_UNFINISHED
;
91 }else if( e
==peffort
){
94 Trace("inst-alg") << "-> User-provided instantiate " << f
<< "..." << std::endl
;
95 if( d_quantEngine
->getInstUserPatMode()==USER_PAT_MODE_RESORT
){
96 for( unsigned i
=0; i
<d_user_gen_wait
[f
].size(); i
++ ){
97 Trigger
* t
= Trigger::mkTrigger( d_quantEngine
, f
, d_user_gen_wait
[f
][i
], true, Trigger::TR_RETURN_NULL
);
99 d_user_gen
[f
].push_back( t
);
102 d_user_gen_wait
[f
].clear();
105 for( unsigned i
=0; i
<d_user_gen
[f
].size(); i
++ ){
106 bool processTrigger
= true;
107 if( processTrigger
){
108 Trace("process-trigger") << " Process (user) ";
109 d_user_gen
[f
][i
]->debugPrint("process-trigger");
110 Trace("process-trigger") << "..." << std::endl
;
111 int numInst
= d_user_gen
[f
][i
]->addInstantiations();
112 Trace("process-trigger") << " Done, numInst = " << numInst
<< "." << std::endl
;
113 d_quantEngine
->d_statistics
.d_instantiations_user_patterns
+= numInst
;
114 if( d_user_gen
[f
][i
]->isMultiTrigger() ){
115 d_quantEngine
->d_statistics
.d_multi_trigger_instantiations
+= numInst
;
117 if( d_quantEngine
->inConflict() ){
124 return STATUS_UNKNOWN
;
127 void InstStrategyUserPatterns::addUserPattern( Node q
, Node pat
){
128 Assert(pat
.getKind() == INST_PATTERN
);
131 std::vector
< Node
> nodes
;
132 for( unsigned i
=0; i
<pat
.getNumChildren(); i
++ ){
133 Node pat_use
= Trigger::getIsUsableTrigger( pat
[i
], q
);
134 if( pat_use
.isNull() ){
135 Trace("trigger-warn") << "User-provided trigger is not usable : " << pat
<< " because of " << pat
[i
] << std::endl
;
139 nodes
.push_back( pat_use
);
143 Trace("user-pat") << "Add user pattern: " << pat
<< " for " << q
<< std::endl
;
145 if( d_quantEngine
->getInstUserPatMode()==USER_PAT_MODE_RESORT
){
146 d_user_gen_wait
[q
].push_back( nodes
);
148 Trigger
* t
= Trigger::mkTrigger( d_quantEngine
, q
, nodes
, true, Trigger::TR_MAKE_NEW
);
150 d_user_gen
[q
].push_back( t
);
152 Trace("trigger-warn") << "Failed to construct trigger : " << pat
<< " due to variable mismatch" << std::endl
;
158 InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers(QuantifiersEngine
* qe
,
160 : InstStrategy(qe
), d_quant_rel(qr
)
162 //how to select trigger terms
163 d_tr_strategy
= options::triggerSelMode();
164 //whether to select new triggers during the search
165 if( options::incrementTriggers() ){
166 d_regenerate_frequency
= 3;
169 d_regenerate_frequency
= 1;
170 d_regenerate
= false;
174 void InstStrategyAutoGenTriggers::processResetInstantiationRound( Theory::Effort effort
){
175 Trace("inst-alg-debug") << "reset auto-gen triggers" << std::endl
;
177 for( unsigned r
=0; r
<2; r
++ ){
178 for( std::map
< Node
, std::map
< Trigger
*, bool > >::iterator it
= d_auto_gen_trigger
[r
].begin(); it
!= d_auto_gen_trigger
[r
].end(); ++it
){
179 for( std::map
< Trigger
*, bool >::iterator itt
= it
->second
.begin(); itt
!= it
->second
.end(); ++itt
){
180 itt
->first
->resetInstantiationRound();
181 itt
->first
->reset( Node::null() );
185 d_processed_trigger
.clear();
186 Trace("inst-alg-debug") << "done reset auto-gen triggers" << std::endl
;
189 int InstStrategyAutoGenTriggers::process( Node f
, Theory::Effort effort
, int e
){
190 UserPatMode upMode
= d_quantEngine
->getInstUserPatMode();
191 if( hasUserPatterns( f
) && upMode
==USER_PAT_MODE_TRUST
){
192 return STATUS_UNKNOWN
;
194 int peffort
= ( hasUserPatterns( f
) && upMode
!=USER_PAT_MODE_IGNORE
&& upMode
!=USER_PAT_MODE_RESORT
) ? 2 : 1;
196 return STATUS_UNFINISHED
;
198 Trace("inst-alg") << "-> Auto-gen instantiate " << f
<< "..." << std::endl
;
201 if( d_counter
.find( f
)==d_counter
.end() ){
206 gen
= d_regenerate
&& d_counter
[f
]%d_regenerate_frequency
==0;
212 generateTriggers( f
);
213 if( d_counter
[f
]==0 && d_auto_gen_trigger
[0][f
].empty() && d_auto_gen_trigger
[1][f
].empty() && f
.getNumChildren()==2 ){
214 Trace("trigger-warn") << "Could not find trigger for " << f
<< std::endl
;
219 // d_processed_trigger.clear();
220 // d_quantEngine->getEqualityQuery()->setLiberal( true );
222 if( options::triggerActiveSelMode()!=TRIGGER_ACTIVE_SEL_ALL
){
224 Trigger
* max_trigger
= NULL
;
225 for( std::map
< Trigger
*, bool >::iterator itt
= d_auto_gen_trigger
[0][f
].begin(); itt
!= d_auto_gen_trigger
[0][f
].end(); ++itt
){
226 int score
= itt
->first
->getActiveScore();
227 if( options::triggerActiveSelMode()==TRIGGER_ACTIVE_SEL_MIN
){
228 if( score
>=0 && ( score
<max_score
|| max_score
<0 ) ){
230 max_trigger
= itt
->first
;
233 if( score
>max_score
){
235 max_trigger
= itt
->first
;
238 d_auto_gen_trigger
[0][f
][itt
->first
] = false;
240 if( max_trigger
!=NULL
){
241 d_auto_gen_trigger
[0][f
][max_trigger
] = true;
245 bool hasInst
= false;
246 for( unsigned r
=0; r
<2; r
++ ){
247 for( std::map
< Trigger
*, bool >::iterator itt
= d_auto_gen_trigger
[r
][f
].begin(); itt
!= d_auto_gen_trigger
[r
][f
].end(); ++itt
){
248 Trigger
* tr
= itt
->first
;
250 bool processTrigger
= itt
->second
;
251 if( processTrigger
&& d_processed_trigger
[f
].find( tr
)==d_processed_trigger
[f
].end() ){
252 d_processed_trigger
[f
][tr
] = true;
253 Trace("process-trigger") << " Process ";
254 tr
->debugPrint("process-trigger");
255 Trace("process-trigger") << "..." << std::endl
;
256 int numInst
= tr
->addInstantiations();
257 hasInst
= numInst
>0 || hasInst
;
258 Trace("process-trigger") << " Done, numInst = " << numInst
<< "." << std::endl
;
259 d_quantEngine
->d_statistics
.d_instantiations_auto_gen
+= numInst
;
261 d_quantEngine
->d_statistics
.d_multi_trigger_instantiations
+= numInst
;
263 if( d_quantEngine
->inConflict() ){
269 if( d_quantEngine
->inConflict() || ( hasInst
&& options::multiTriggerPriority() ) ){
274 // d_quantEngine->getEqualityQuery()->setLiberal( false );
276 return STATUS_UNKNOWN
;
281 void InstStrategyAutoGenTriggers::generateTriggers( Node f
){
282 Trace("auto-gen-trigger-debug") << "Generate triggers for " << f
<< ", #var=" << f
[0].getNumChildren() << "..." << std::endl
;
283 if( d_patTerms
[0].find( f
)==d_patTerms
[0].end() ){
284 //determine all possible pattern terms based on trigger term selection strategy d_tr_strategy
285 d_patTerms
[0][f
].clear();
286 d_patTerms
[1][f
].clear();
287 bool ntrivTriggers
= options::relationalTriggers();
288 std::vector
< Node
> patTermsF
;
289 std::map
< Node
, inst::TriggerTermInfo
> tinfo
;
290 //well-defined function: can assume LHS is only trigger
291 if( options::quantFunWellDefined() ){
292 Node hd
= QuantAttributes::getFunDefHead( f
);
294 hd
= d_quantEngine
->getTermUtil()
295 ->substituteBoundVariablesToInstConstants(hd
, f
);
296 patTermsF
.push_back( hd
);
297 tinfo
[hd
].init( f
, hd
);
300 //otherwise, use algorithm for collecting pattern terms
301 if( patTermsF
.empty() ){
302 Node bd
= d_quantEngine
->getTermUtil()->getInstConstantBody( f
);
303 Trigger::collectPatTerms( f
, bd
, patTermsF
, d_tr_strategy
, d_user_no_gen
[f
], tinfo
, true );
306 std::sort( patTermsF
.begin(), patTermsF
.end(), st
);
308 if( Trace
.isOn("auto-gen-trigger-debug") ){
309 Trace("auto-gen-trigger-debug") << "Collected pat terms for " << bd
<< ", no-patterns : " << d_user_no_gen
[f
].size() << std::endl
;
310 for( unsigned i
=0; i
<patTermsF
.size(); i
++ ){
311 Assert(tinfo
.find(patTermsF
[i
]) != tinfo
.end());
312 Trace("auto-gen-trigger-debug") << " " << patTermsF
[i
] << std::endl
;
313 Trace("auto-gen-trigger-debug2") << " info = [" << tinfo
[patTermsF
[i
]].d_reqPol
<< ", " << tinfo
[patTermsF
[i
]].d_reqPolEq
<< ", " << tinfo
[patTermsF
[i
]].d_fv
.size() << "]" << std::endl
;
315 Trace("auto-gen-trigger-debug") << std::endl
;
318 //sort into single/multi triggers, calculate which terms should not be considered
319 std::map
< Node
, bool > vcMap
;
320 std::map
< Node
, bool > rmPatTermsF
;
321 int last_weight
= -1;
322 for( unsigned i
=0; i
<patTermsF
.size(); i
++ ){
323 Assert(patTermsF
[i
].getKind() != NOT
);
325 for( unsigned j
=0; j
<tinfo
[ patTermsF
[i
] ].d_fv
.size(); j
++ ){
326 if( vcMap
.find( tinfo
[ patTermsF
[i
] ].d_fv
[j
] )==vcMap
.end() ){
327 vcMap
[tinfo
[ patTermsF
[i
] ].d_fv
[j
]] = true;
331 int curr_w
= Trigger::getTriggerWeight( patTermsF
[i
] );
332 // triggers whose value is maximum (2) are considered expendable.
333 if (ntrivTriggers
&& !newVar
&& last_weight
!= -1 && curr_w
> last_weight
336 Trace("auto-gen-trigger-debug") << "...exclude expendible non-trivial trigger : " << patTermsF
[i
] << std::endl
;
337 rmPatTermsF
[patTermsF
[i
]] = true;
339 last_weight
= curr_w
;
342 d_num_trigger_vars
[f
] = vcMap
.size();
343 if( d_num_trigger_vars
[f
]>0 && d_num_trigger_vars
[f
]<f
[0].getNumChildren() ){
344 Trace("auto-gen-trigger-partial") << "Quantified formula : " << f
<< std::endl
;
345 Trace("auto-gen-trigger-partial") << "...does not contain all variables in triggers!!!" << std::endl
;
346 if( options::partialTriggers() ){
347 std::vector
< Node
> vcs
[2];
348 for( unsigned i
=0; i
<f
[0].getNumChildren(); i
++ ){
349 Node ic
= d_quantEngine
->getTermUtil()->getInstantiationConstant( f
, i
);
350 vcs
[ vcMap
.find( ic
)==vcMap
.end() ? 0 : 1 ].push_back( f
[0][i
] );
352 for( unsigned i
=0; i
<2; i
++ ){
353 d_vc_partition
[i
][f
] = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST
, vcs
[i
] );
359 for( unsigned i
=0; i
<patTermsF
.size(); i
++ ){
360 Node pat
= patTermsF
[i
];
361 if( rmPatTermsF
.find( pat
)==rmPatTermsF
.end() ){
362 Trace("auto-gen-trigger-debug") << "...processing pattern " << pat
<< std::endl
;
364 //process the pattern: if it has a required polarity, consider it
365 Assert(tinfo
.find(pat
) != tinfo
.end());
366 int rpol
= tinfo
[pat
].d_reqPol
;
367 Node rpoleq
= tinfo
[pat
].d_reqPolEq
;
368 unsigned num_fv
= tinfo
[pat
].d_fv
.size();
369 Trace("auto-gen-trigger-debug") << "...required polarity for " << pat
<< " is " << rpol
<< ", eq=" << rpoleq
<< std::endl
;
371 Assert(rpol
== 1 || rpol
== -1);
372 if( Trigger::isRelationalTrigger( pat
) ){
373 pat
= rpol
==-1 ? pat
.negate() : pat
;
375 Assert(Trigger::isAtomicTrigger(pat
));
376 if( pat
.getType().isBoolean() && rpoleq
.isNull() ){
377 if( options::literalMatchMode()==LITERAL_MATCH_USE
){
378 pat
= NodeManager::currentNM()->mkNode( EQUAL
, pat
, NodeManager::currentNM()->mkConst( rpol
==-1 ) ).negate();
379 }else if( options::literalMatchMode()!=LITERAL_MATCH_NONE
){
380 pat
= NodeManager::currentNM()->mkNode( EQUAL
, pat
, NodeManager::currentNM()->mkConst( rpol
==1 ) );
383 Assert(!rpoleq
.isNull());
385 if( options::literalMatchMode()!=LITERAL_MATCH_NONE
){
386 //all equivalence classes except rpoleq
387 pat
= NodeManager::currentNM()->mkNode( EQUAL
, pat
, rpoleq
).negate();
390 if( options::literalMatchMode()==LITERAL_MATCH_AGG
){
391 //only equivalence class rpoleq
392 pat
= NodeManager::currentNM()->mkNode( EQUAL
, pat
, rpoleq
);
394 //all equivalence classes that are not disequal to rpoleq TODO?
398 Trace("auto-gen-trigger-debug") << "...got : " << pat
<< std::endl
;
400 if( Trigger::isRelationalTrigger( pat
) ){
401 //consider both polarities
402 addPatternToPool( f
, pat
.negate(), num_fv
, mpat
);
405 addPatternToPool( f
, pat
, num_fv
, mpat
);
408 //tinfo not used below this point
409 d_made_multi_trigger
[f
] = false;
410 Trace("auto-gen-trigger") << "Single trigger pool for " << f
<< " : " << std::endl
;
411 for( unsigned i
=0; i
<d_patTerms
[0][f
].size(); i
++ ){
412 Trace("auto-gen-trigger") << " " << d_patTerms
[0][f
][i
] << std::endl
;
414 if( !d_patTerms
[1][f
].empty() ){
415 Trace("auto-gen-trigger") << "Multi-trigger term pool for " << f
<< " : " << std::endl
;
416 for( unsigned i
=0; i
<d_patTerms
[1][f
].size(); i
++ ){
417 Trace("auto-gen-trigger") << " " << d_patTerms
[1][f
][i
] << std::endl
;
422 unsigned rmin
= d_patTerms
[0][f
].empty() ? 1 : 0;
423 unsigned rmax
= options::multiTriggerWhenSingle() ? 1 : rmin
;
424 for( unsigned r
=rmin
; r
<=rmax
; r
++ ){
425 std::vector
< Node
> patTerms
;
426 for( int i
=0; i
<(int)d_patTerms
[r
][f
].size(); i
++ ){
427 if( r
==1 || d_single_trigger_gen
.find( d_patTerms
[r
][f
][i
] )==d_single_trigger_gen
.end() ){
428 patTerms
.push_back( d_patTerms
[r
][f
][i
] );
431 if( !patTerms
.empty() ){
432 Trace("auto-gen-trigger") << "Generate trigger for " << f
<< std::endl
;
433 //sort terms based on relevance
434 if( options::relevantTriggers() ){
436 sortQuantifiersForSymbol sqfs
;
437 sqfs
.d_quant_rel
= d_quant_rel
;
438 for( unsigned i
=0; i
<patTerms
.size(); i
++ ){
439 Assert(d_pat_to_mpat
.find(patTerms
[i
]) != d_pat_to_mpat
.end());
440 Assert(d_pat_to_mpat
[patTerms
[i
]].hasOperator());
441 sqfs
.d_op_map
[ patTerms
[i
] ] = d_pat_to_mpat
[patTerms
[i
]].getOperator();
443 //sort based on # occurrences (this will cause Trigger to select rarer symbols)
444 std::sort( patTerms
.begin(), patTerms
.end(), sqfs
);
445 if (Debug
.isOn("relevant-trigger"))
447 Debug("relevant-trigger")
448 << "Terms based on relevance: " << std::endl
;
449 for (const Node
& p
: patTerms
)
451 Debug("relevant-trigger")
452 << " " << p
<< " from " << d_pat_to_mpat
[p
] << " (";
453 Debug("relevant-trigger")
454 << d_quant_rel
->getNumQuantifiersForSymbol(
455 d_pat_to_mpat
[p
].getOperator())
460 //now, generate the trigger...
462 if( d_is_single_trigger
[ patTerms
[0] ] ){
463 tr
= Trigger::mkTrigger( d_quantEngine
, f
, patTerms
[0], false, Trigger::TR_RETURN_NULL
, d_num_trigger_vars
[f
] );
464 d_single_trigger_gen
[ patTerms
[0] ] = true;
466 //only generate multi trigger if option set, or if no single triggers exist
467 if( !d_patTerms
[0][f
].empty() ){
468 if( options::multiTriggerWhenSingle() ){
469 Trace("multi-trigger-debug") << "Resort to choosing multi-triggers..." << std::endl
;
474 // if we are re-generating triggers, shuffle based on some method
475 if (d_made_multi_trigger
[f
])
477 std::shuffle(patTerms
.begin(),
479 Random::getRandom()); // shuffle randomly
483 d_made_multi_trigger
[f
] = true;
485 //will possibly want to get an old trigger
486 tr
= Trigger::mkTrigger( d_quantEngine
, f
, patTerms
, false, Trigger::TR_GET_OLD
, d_num_trigger_vars
[f
] );
490 //if we are generating additional triggers...
491 if( !tr
->isMultiTrigger() ){
493 if( index
<patTerms
.size() ){
494 //Notice() << "check add additional" << std::endl;
495 //check if similar patterns exist, and if so, add them additionally
496 unsigned nqfs_curr
= 0;
497 if( options::relevantTriggers() ){
498 nqfs_curr
= d_quant_rel
->getNumQuantifiersForSymbol(
499 patTerms
[0].getOperator());
503 while( success
&& index
<patTerms
.size() && d_is_single_trigger
[ patTerms
[index
] ] ){
505 if (!options::relevantTriggers()
506 || d_quant_rel
->getNumQuantifiersForSymbol(
507 patTerms
[index
].getOperator())
510 d_single_trigger_gen
[ patTerms
[index
] ] = true;
511 Trigger
* tr2
= Trigger::mkTrigger( d_quantEngine
, f
, patTerms
[index
], false, Trigger::TR_RETURN_NULL
, d_num_trigger_vars
[f
] );
512 addTrigger( tr2
, f
);
517 //Notice() << "done check add additional" << std::endl;
525 void InstStrategyAutoGenTriggers::addPatternToPool( Node q
, Node pat
, unsigned num_fv
, Node mpat
) {
526 d_pat_to_mpat
[pat
] = mpat
;
527 unsigned num_vars
= options::partialTriggers() ? d_num_trigger_vars
[q
] : q
[0].getNumChildren();
528 if( num_fv
==num_vars
&& ( options::pureThTriggers() || !Trigger::isPureTheoryTrigger( pat
) ) ){
529 d_patTerms
[0][q
].push_back( pat
);
530 d_is_single_trigger
[ pat
] = true;
532 d_patTerms
[1][q
].push_back( pat
);
533 d_is_single_trigger
[ pat
] = false;
538 void InstStrategyAutoGenTriggers::addTrigger( inst::Trigger
* tr
, Node q
) {
540 if( d_num_trigger_vars
[q
]<q
[0].getNumChildren() ){
541 //partial trigger : generate implication to mark user pattern
543 d_quantEngine
->getTermUtil()->substituteInstConstantsToBoundVariables(
544 tr
->getInstPattern(), q
);
545 Node ipl
= NodeManager::currentNM()->mkNode(INST_PATTERN_LIST
, pat
);
546 Node qq
= NodeManager::currentNM()->mkNode( FORALL
, d_vc_partition
[1][q
], NodeManager::currentNM()->mkNode( FORALL
, d_vc_partition
[0][q
], q
[1] ), ipl
);
547 Trace("auto-gen-trigger-partial") << "Make partially specified user pattern: " << std::endl
;
548 Trace("auto-gen-trigger-partial") << " " << qq
<< std::endl
;
549 Node lem
= NodeManager::currentNM()->mkNode( OR
, q
.negate(), qq
);
550 d_quantEngine
->addLemma( lem
);
553 if( tr
->isMultiTrigger() ){
554 //disable all other multi triggers
555 for( std::map
< Trigger
*, bool >::iterator it
= d_auto_gen_trigger
[1][q
].begin(); it
!= d_auto_gen_trigger
[1][q
].end(); ++it
){
556 d_auto_gen_trigger
[1][q
][ it
->first
] = false;
562 //making it during an instantiation round, so must reset
563 if( d_auto_gen_trigger
[tindex
][q
].find( tr
)==d_auto_gen_trigger
[tindex
][q
].end() ){
564 tr
->resetInstantiationRound();
565 tr
->reset( Node::null() );
567 d_auto_gen_trigger
[tindex
][q
][tr
] = true;
572 bool InstStrategyAutoGenTriggers::hasUserPatterns( Node q
) {
573 if( q
.getNumChildren()==3 ){
574 std::map
< Node
, bool >::iterator it
= d_hasUserPatterns
.find( q
);
575 if( it
==d_hasUserPatterns
.end() ){
577 for( unsigned i
=0; i
<q
[2].getNumChildren(); i
++ ){
578 if( q
[2][i
].getKind()==INST_PATTERN
){
583 d_hasUserPatterns
[q
] = hasPat
;
593 void InstStrategyAutoGenTriggers::addUserNoPattern( Node q
, Node pat
) {
594 Assert(pat
.getKind() == INST_NO_PATTERN
&& pat
.getNumChildren() == 1);
595 if( std::find( d_user_no_gen
[q
].begin(), d_user_no_gen
[q
].end(), pat
[0] )==d_user_no_gen
[q
].end() ){
596 Trace("user-pat") << "Add user no-pattern: " << pat
[0] << " for " << q
<< std::endl
;
597 d_user_no_gen
[q
].push_back( pat
[0] );
601 } /* CVC4::theory::quantifiers namespace */
602 } /* CVC4::theory namespace */
603 } /* CVC4 namespace */