1 /********************* */
2 /*! \file inst_strategy_e_matching.cpp
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Morgan Deters, Tim King
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2016 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/inst_strategy_e_matching.h"
16 #include "theory/quantifiers/inst_match_generator.h"
17 #include "theory/quantifiers/relevant_domain.h"
18 #include "theory/quantifiers/term_database.h"
19 #include "theory/theory_engine.h"
23 using namespace CVC4::kind
;
24 using namespace CVC4::context
;
25 using namespace CVC4::theory
;
26 using namespace CVC4::theory::inst
;
27 using namespace CVC4::theory::quantifiers
;
30 //1 : user patterns (when user-pat!={resort,ignore}), auto-gen patterns (for non-user pattern quantifiers, or when user-pat={resort,ignore})
31 //2 : user patterns (when user-pat=resort), auto gen patterns (for user pattern quantifiers when user-pat=use)
33 // user-pat=interleave alternates between use and resort
35 struct sortQuantifiersForSymbol
{
36 QuantifiersEngine
* d_qe
;
37 bool operator() (Node i
, Node j
) {
38 int nqfsi
= d_qe
->getQuantifierRelevance()->getNumQuantifiersForSymbol( i
.getOperator() );
39 int nqfsj
= d_qe
->getQuantifierRelevance()->getNumQuantifiersForSymbol( j
.getOperator() );
42 }else if( nqfsi
>nqfsj
){
51 bool operator() (Node i
, Node j
) {
52 int wi
= Trigger::getTriggerWeight( i
);
53 int wj
= Trigger::getTriggerWeight( j
);
62 void InstStrategyUserPatterns::processResetInstantiationRound( Theory::Effort effort
){
63 Trace("inst-alg-debug") << "reset user triggers" << std::endl
;
65 for( std::map
< Node
, std::vector
< Trigger
* > >::iterator it
= d_user_gen
.begin(); it
!= d_user_gen
.end(); ++it
){
66 for( unsigned i
=0; i
<it
->second
.size(); i
++ ){
67 it
->second
[i
]->resetInstantiationRound();
68 it
->second
[i
]->reset( Node::null() );
71 Trace("inst-alg-debug") << "done reset user triggers" << std::endl
;
74 int InstStrategyUserPatterns::process( Node f
, Theory::Effort effort
, int e
){
76 return STATUS_UNFINISHED
;
78 int peffort
= d_quantEngine
->getInstUserPatMode()==USER_PAT_MODE_RESORT
? 2 : 1;
80 return STATUS_UNFINISHED
;
81 }else if( e
==peffort
){
84 Trace("inst-alg") << "-> User-provided instantiate " << f
<< "..." << std::endl
;
85 if( d_quantEngine
->getInstUserPatMode()==USER_PAT_MODE_RESORT
){
87 for( unsigned i
=0; i
<d_user_gen_wait
[f
].size(); i
++ ){
88 Trigger
* t
= Trigger::mkTrigger( d_quantEngine
, f
, d_user_gen_wait
[f
][i
], matchOption
, true, Trigger::TR_RETURN_NULL
);
90 d_user_gen
[f
].push_back( t
);
93 d_user_gen_wait
[f
].clear();
96 for( unsigned i
=0; i
<d_user_gen
[f
].size(); i
++ ){
97 bool processTrigger
= true;
99 Trace("process-trigger") << " Process (user) ";
100 d_user_gen
[f
][i
]->debugPrint("process-trigger");
101 Trace("process-trigger") << "..." << std::endl
;
102 InstMatch
baseMatch( f
);
103 int numInst
= d_user_gen
[f
][i
]->addInstantiations( baseMatch
);
104 Trace("process-trigger") << " Done, numInst = " << numInst
<< "." << std::endl
;
105 d_quantEngine
->d_statistics
.d_instantiations_user_patterns
+= numInst
;
106 if( d_user_gen
[f
][i
]->isMultiTrigger() ){
107 d_quantEngine
->d_statistics
.d_multi_trigger_instantiations
+= numInst
;
109 if( d_quantEngine
->inConflict() ){
116 return STATUS_UNKNOWN
;
119 void InstStrategyUserPatterns::addUserPattern( Node q
, Node pat
){
120 Assert( pat
.getKind()==INST_PATTERN
);
123 std::vector
< Node
> nodes
;
124 for( unsigned i
=0; i
<pat
.getNumChildren(); i
++ ){
125 Node pat_use
= Trigger::getIsUsableTrigger( pat
[i
], q
);
126 if( pat_use
.isNull() ){
127 Trace("trigger-warn") << "User-provided trigger is not usable : " << pat
<< " because of " << pat
[i
] << std::endl
;
131 nodes
.push_back( pat_use
);
135 Trace("user-pat") << "Add user pattern: " << pat
<< " for " << q
<< std::endl
;
138 if( d_quantEngine
->getInstUserPatMode()==USER_PAT_MODE_RESORT
){
139 d_user_gen_wait
[q
].push_back( nodes
);
141 Trigger
* t
= Trigger::mkTrigger( d_quantEngine
, q
, nodes
, matchOption
, true, Trigger::TR_MAKE_NEW
);
143 d_user_gen
[q
].push_back( t
);
145 Trace("trigger-warn") << "Failed to construct trigger : " << pat
<< " due to variable mismatch" << std::endl
;
151 InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers( QuantifiersEngine
* qe
) : InstStrategy( qe
){
152 //how to select trigger terms
153 if( options::triggerSelMode()==quantifiers::TRIGGER_SEL_DEFAULT
){
154 d_tr_strategy
= quantifiers::TRIGGER_SEL_MIN
;
156 d_tr_strategy
= options::triggerSelMode();
158 //whether to select new triggers during the search
159 if( options::incrementTriggers() ){
160 d_regenerate_frequency
= 3;
163 d_regenerate
= false;
167 void InstStrategyAutoGenTriggers::processResetInstantiationRound( Theory::Effort effort
){
168 Trace("inst-alg-debug") << "reset auto-gen triggers" << std::endl
;
170 for( unsigned r
=0; r
<2; r
++ ){
171 for( std::map
< Node
, std::map
< Trigger
*, bool > >::iterator it
= d_auto_gen_trigger
[r
].begin(); it
!= d_auto_gen_trigger
[r
].end(); ++it
){
172 for( std::map
< Trigger
*, bool >::iterator itt
= it
->second
.begin(); itt
!= it
->second
.end(); ++itt
){
173 itt
->first
->resetInstantiationRound();
174 itt
->first
->reset( Node::null() );
178 d_processed_trigger
.clear();
179 Trace("inst-alg-debug") << "done reset auto-gen triggers" << std::endl
;
182 int InstStrategyAutoGenTriggers::process( Node f
, Theory::Effort effort
, int e
){
183 UserPatMode upMode
= d_quantEngine
->getInstUserPatMode();
184 if( hasUserPatterns( f
) && upMode
==USER_PAT_MODE_TRUST
){
185 return STATUS_UNKNOWN
;
187 int peffort
= ( hasUserPatterns( f
) && upMode
!=USER_PAT_MODE_IGNORE
&& upMode
!=USER_PAT_MODE_RESORT
) ? 2 : 1;
189 return STATUS_UNFINISHED
;
191 Trace("inst-alg") << "-> Auto-gen instantiate " << f
<< "..." << std::endl
;
194 if( d_counter
.find( f
)==d_counter
.end() ){
199 gen
= d_regenerate
&& d_counter
[f
]%d_regenerate_frequency
==0;
205 generateTriggers( f
);
206 if( d_counter
[f
]==0 && d_auto_gen_trigger
[0][f
].empty() && d_auto_gen_trigger
[1][f
].empty() && f
.getNumChildren()==2 ){
207 Trace("trigger-warn") << "Could not find trigger for " << f
<< std::endl
;
212 // d_processed_trigger.clear();
213 // d_quantEngine->getEqualityQuery()->setLiberal( true );
215 bool hasInst
= false;
216 for( unsigned r
=0; r
<2; r
++ ){
217 for( std::map
< Trigger
*, bool >::iterator itt
= d_auto_gen_trigger
[r
][f
].begin(); itt
!= d_auto_gen_trigger
[r
][f
].end(); ++itt
){
218 Trigger
* tr
= itt
->first
;
220 bool processTrigger
= itt
->second
;
221 if( processTrigger
&& d_processed_trigger
[f
].find( tr
)==d_processed_trigger
[f
].end() ){
222 d_processed_trigger
[f
][tr
] = true;
223 Trace("process-trigger") << " Process ";
224 tr
->debugPrint("process-trigger");
225 Trace("process-trigger") << "..." << std::endl
;
226 InstMatch
baseMatch( f
);
227 int numInst
= tr
->addInstantiations( baseMatch
);
228 hasInst
= numInst
>0 || hasInst
;
229 Trace("process-trigger") << " Done, numInst = " << numInst
<< "." << std::endl
;
230 d_quantEngine
->d_statistics
.d_instantiations_auto_gen
+= numInst
;
232 d_quantEngine
->d_statistics
.d_multi_trigger_instantiations
+= numInst
;
234 if( d_quantEngine
->inConflict() ){
240 if( d_quantEngine
->inConflict() || ( hasInst
&& options::multiTriggerPriority() ) ){
245 // d_quantEngine->getEqualityQuery()->setLiberal( false );
247 return STATUS_UNKNOWN
;
252 void InstStrategyAutoGenTriggers::generateTriggers( Node f
){
253 Trace("auto-gen-trigger-debug") << "Generate triggers for " << f
<< ", #var=" << f
[0].getNumChildren() << "..." << std::endl
;
254 if( d_patTerms
[0].find( f
)==d_patTerms
[0].end() ){
255 //determine all possible pattern terms based on trigger term selection strategy d_tr_strategy
256 d_patTerms
[0][f
].clear();
257 d_patTerms
[1][f
].clear();
258 bool ntrivTriggers
= options::relationalTriggers();
259 std::vector
< Node
> patTermsF
;
260 std::map
< Node
, inst::TriggerTermInfo
> tinfo
;
261 //well-defined function: can assume LHS is only trigger
262 if( options::quantFunWellDefined() ){
263 Node hd
= TermDb::getFunDefHead( f
);
265 hd
= d_quantEngine
->getTermDatabase()->getInstConstantNode( hd
, f
);
266 patTermsF
.push_back( hd
);
267 tinfo
[hd
].init( f
, hd
);
270 //otherwise, use algorithm for collecting pattern terms
271 if( patTermsF
.empty() ){
272 Node bd
= d_quantEngine
->getTermDatabase()->getInstConstantBody( f
);
273 Trigger::collectPatTerms( f
, bd
, patTermsF
, d_tr_strategy
, d_user_no_gen
[f
], tinfo
, true );
276 std::sort( patTermsF
.begin(), patTermsF
.end(), st
);
278 if( Trace
.isOn("auto-gen-trigger-debug") ){
279 Trace("auto-gen-trigger-debug") << "Collected pat terms for " << bd
<< ", no-patterns : " << d_user_no_gen
[f
].size() << std::endl
;
280 for( unsigned i
=0; i
<patTermsF
.size(); i
++ ){
281 Assert( tinfo
.find( patTermsF
[i
] )!=tinfo
.end() );
282 Trace("auto-gen-trigger-debug") << " " << patTermsF
[i
];
283 Trace("auto-gen-trigger-debug") << " info[" << tinfo
[patTermsF
[i
]].d_reqPol
<< ", " << tinfo
[patTermsF
[i
]].d_reqPolEq
<< ", " << tinfo
[patTermsF
[i
]].d_fv
.size() << "]" << std::endl
;
285 Trace("auto-gen-trigger-debug") << std::endl
;
288 //sort into single/multi triggers, calculate which terms should not be considered
289 std::map
< Node
, bool > vcMap
;
290 std::map
< Node
, bool > rmPatTermsF
;
291 int last_weight
= -1;
292 for( unsigned i
=0; i
<patTermsF
.size(); i
++ ){
293 Assert( patTermsF
[i
].getKind()!=NOT
);
295 for( unsigned j
=0; j
<tinfo
[ patTermsF
[i
] ].d_fv
.size(); j
++ ){
296 if( vcMap
.find( tinfo
[ patTermsF
[i
] ].d_fv
[j
] )==vcMap
.end() ){
297 vcMap
[tinfo
[ patTermsF
[i
] ].d_fv
[j
]] = true;
301 int curr_w
= Trigger::getTriggerWeight( patTermsF
[i
] );
302 if( ntrivTriggers
&& !newVar
&& last_weight
!=-1 && curr_w
>last_weight
){
303 Trace("auto-gen-trigger-debug") << "...exclude expendible non-trivial trigger : " << patTermsF
[i
] << std::endl
;
304 rmPatTermsF
[patTermsF
[i
]] = true;
306 last_weight
= curr_w
;
309 for( unsigned i
=0; i
<patTermsF
.size(); i
++ ){
310 Node pat
= patTermsF
[i
];
311 if( rmPatTermsF
.find( pat
)==rmPatTermsF
.end() ){
312 Trace("auto-gen-trigger-debug") << "...processing pattern " << pat
<< std::endl
;
313 //process the pattern: if it has a required polarity, consider it
314 Assert( tinfo
.find( pat
)!=tinfo
.end() );
315 int rpol
= tinfo
[pat
].d_reqPol
;
316 Node rpoleq
= tinfo
[pat
].d_reqPolEq
;
317 unsigned num_fv
= tinfo
[pat
].d_fv
.size();
318 Trace("auto-gen-trigger-debug") << "...required polarity for " << pat
<< " is " << rpol
<< ", eq=" << rpoleq
<< std::endl
;
320 if( Trigger::isRelationalTrigger( pat
) ){
321 pat
= rpol
==-1 ? pat
.negate() : pat
;
323 Assert( Trigger::isAtomicTrigger( pat
) );
324 if( pat
.getType().isBoolean() && rpoleq
.isNull() ){
325 pat
= NodeManager::currentNM()->mkNode( IFF
, pat
, NodeManager::currentNM()->mkConst( rpol
==-1 ) ).negate();
327 Assert( !rpoleq
.isNull() );
329 //all equivalence classes except rpoleq
330 pat
= NodeManager::currentNM()->mkNode( EQUAL
, pat
, rpoleq
).negate();
332 //all equivalence classes that are not disequal to rpoleq TODO
336 Trace("auto-gen-trigger-debug") << "...got : " << pat
<< std::endl
;
338 if( Trigger::isRelationalTrigger( pat
) ){
339 //consider both polarities
340 addPatternToPool( f
, pat
.negate(), num_fv
);
343 addPatternToPool( f
, pat
, num_fv
);
346 //tinfo not used below this point
347 d_made_multi_trigger
[f
] = false;
348 Trace("auto-gen-trigger") << "Single trigger pool for " << f
<< " : " << std::endl
;
349 for( unsigned i
=0; i
<d_patTerms
[0][f
].size(); i
++ ){
350 Trace("auto-gen-trigger") << " " << d_patTerms
[0][f
][i
] << std::endl
;
352 if( !d_patTerms
[1][f
].empty() ){
353 Trace("auto-gen-trigger") << "Multi-trigger term pool for " << f
<< " : " << std::endl
;
354 for( unsigned i
=0; i
<d_patTerms
[1][f
].size(); i
++ ){
355 Trace("auto-gen-trigger") << " " << d_patTerms
[1][f
][i
] << std::endl
;
360 unsigned rmin
= d_patTerms
[0][f
].empty() ? 1 : 0;
361 unsigned rmax
= options::multiTriggerWhenSingle() ? 1 : rmin
;
362 for( unsigned r
=rmin
; r
<=rmax
; r
++ ){
363 std::vector
< Node
> patTerms
;
364 for( int i
=0; i
<(int)d_patTerms
[r
][f
].size(); i
++ ){
365 if( r
==1 || d_single_trigger_gen
.find( d_patTerms
[r
][f
][i
] )==d_single_trigger_gen
.end() ){
366 patTerms
.push_back( d_patTerms
[r
][f
][i
] );
369 if( !patTerms
.empty() ){
370 Trace("auto-gen-trigger") << "Generate trigger for " << f
<< std::endl
;
371 //sort terms based on relevance
372 if( options::relevantTriggers() ){
373 sortQuantifiersForSymbol sqfs
;
374 sqfs
.d_qe
= d_quantEngine
;
375 //sort based on # occurrences (this will cause Trigger to select rarer symbols)
376 std::sort( patTerms
.begin(), patTerms
.end(), sqfs
);
377 Debug("relevant-trigger") << "Terms based on relevance: " << std::endl
;
378 for( unsigned i
=0; i
<patTerms
.size(); i
++ ){
379 Debug("relevant-trigger") << " " << patTerms
[i
] << " (";
380 Debug("relevant-trigger") << d_quantEngine
->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms
[i
].getOperator() ) << ")" << std::endl
;
383 //now, generate the trigger...
386 if( d_is_single_trigger
[ patTerms
[0] ] ){
387 tr
= Trigger::mkTrigger( d_quantEngine
, f
, patTerms
[0], matchOption
, false, Trigger::TR_RETURN_NULL
);
388 d_single_trigger_gen
[ patTerms
[0] ] = true;
390 //only generate multi trigger if option set, or if no single triggers exist
391 if( !d_patTerms
[0][f
].empty() ){
392 if( options::multiTriggerWhenSingle() ){
393 Trace("multi-trigger-debug") << "Resort to choosing multi-triggers..." << std::endl
;
398 //if we are re-generating triggers, shuffle based on some method
399 if( d_made_multi_trigger
[f
] ){
400 std::random_shuffle( patTerms
.begin(), patTerms
.end() ); //shuffle randomly
402 d_made_multi_trigger
[f
] = true;
404 //will possibly want to get an old trigger
405 tr
= Trigger::mkTrigger( d_quantEngine
, f
, patTerms
, matchOption
, false, Trigger::TR_GET_OLD
);
409 if( tr
->isMultiTrigger() ){
410 //disable all other multi triggers
411 for( std::map
< Trigger
*, bool >::iterator it
= d_auto_gen_trigger
[1][f
].begin(); it
!= d_auto_gen_trigger
[1][f
].end(); ++it
){
412 d_auto_gen_trigger
[1][f
][ it
->first
] = false;
418 //making it during an instantiation round, so must reset
419 if( d_auto_gen_trigger
[tindex
][f
].find( tr
)==d_auto_gen_trigger
[tindex
][f
].end() ){
420 tr
->resetInstantiationRound();
421 tr
->reset( Node::null() );
423 d_auto_gen_trigger
[tindex
][f
][tr
] = true;
424 //if we are generating additional triggers...
427 if( index
<(int)patTerms
.size() ){
428 //Notice() << "check add additional" << std::endl;
429 //check if similar patterns exist, and if so, add them additionally
431 if( options::relevantTriggers() ){
432 nqfs_curr
= d_quantEngine
->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms
[0].getOperator() );
436 while( success
&& index
<(int)patTerms
.size() && d_is_single_trigger
[ patTerms
[index
] ] ){
438 if( !options::relevantTriggers() ||
439 d_quantEngine
->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms
[index
].getOperator() )<=nqfs_curr
){
440 d_single_trigger_gen
[ patTerms
[index
] ] = true;
441 Trigger
* tr2
= Trigger::mkTrigger( d_quantEngine
, f
, patTerms
[index
], matchOption
, false, Trigger::TR_RETURN_NULL
);
443 //Notice() << "Add additional trigger " << patTerms[index] << std::endl;
444 tr2
->resetInstantiationRound();
445 tr2
->reset( Node::null() );
446 d_auto_gen_trigger
[0][f
][tr2
] = true;
452 //Notice() << "done check add additional" << std::endl;
460 void InstStrategyAutoGenTriggers::addPatternToPool( Node q
, Node pat
, unsigned num_fv
) {
461 if( num_fv
==q
[0].getNumChildren() && ( options::pureThTriggers() || !Trigger::isPureTheoryTrigger( pat
) ) ){
462 d_patTerms
[0][q
].push_back( pat
);
463 d_is_single_trigger
[ pat
] = true;
465 d_patTerms
[1][q
].push_back( pat
);
466 d_is_single_trigger
[ pat
] = false;
470 bool InstStrategyAutoGenTriggers::hasUserPatterns( Node q
) {
471 if( q
.getNumChildren()==3 ){
472 std::map
< Node
, bool >::iterator it
= d_hasUserPatterns
.find( q
);
473 if( it
==d_hasUserPatterns
.end() ){
475 for( unsigned i
=0; i
<q
[2].getNumChildren(); i
++ ){
476 if( q
[2][i
].getKind()==INST_PATTERN
){
481 d_hasUserPatterns
[q
] = hasPat
;
491 void InstStrategyAutoGenTriggers::addUserNoPattern( Node q
, Node pat
) {
492 Assert( pat
.getKind()==INST_NO_PATTERN
&& pat
.getNumChildren()==1 );
493 if( std::find( d_user_no_gen
[q
].begin(), d_user_no_gen
[q
].end(), pat
[0] )==d_user_no_gen
[q
].end() ){
494 Trace("user-pat") << "Add user no-pattern: " << pat
[0] << " for " << q
<< std::endl
;
495 d_user_no_gen
[q
].push_back( pat
[0] );
500 bool InstStrategyLocalTheoryExt::isLocalTheoryExt( Node f ) {
501 std::map< Node, bool >::iterator itq = d_quant.find( f );
502 if( itq==d_quant.end() ){
504 Node bd = d_quantEngine->getTermDatabase()->getInstConstantBody( f );
505 std::vector< Node > vars;
506 std::vector< Node > patTerms;
507 bool ret = Trigger::isLocalTheoryExt( bd, vars, patTerms );
510 //add all variables to trigger that don't already occur
511 for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
512 Node x = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i );
513 if( std::find( vars.begin(), vars.end(), x )==vars.end() ){
514 patTerms.push_back( x );
517 Trace("local-t-ext") << "Local theory extensions trigger for " << f << " : " << std::endl;
518 for( unsigned i=0; i<patTerms.size(); i++ ){
519 Trace("local-t-ext") << " " << patTerms[i] << std::endl;
521 Trace("local-t-ext") << std::endl;
523 Trigger * tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, matchOption, true, Trigger::TR_GET_OLD );
524 d_lte_trigger[f] = tr;
526 Trace("local-t-ext") << "No local theory extensions trigger for " << f << "." << std::endl;
527 Trace("local-t-ext-warn") << "WARNING: not local theory extensions : " << f << std::endl;
536 FullSaturation::FullSaturation( QuantifiersEngine
* qe
) : QuantifiersModule( qe
){
540 bool FullSaturation::needsCheck( Theory::Effort e
){
541 if( options::fullSaturateInst() ){
542 if( d_quantEngine
->getInstWhenNeedsCheck( e
) ){
546 if( options::fullSaturateQuant() ){
547 if( e
>=Theory::EFFORT_LAST_CALL
){
554 void FullSaturation::reset_round( Theory::Effort e
) {
558 void FullSaturation::check( Theory::Effort e
, unsigned quant_e
) {
559 bool doCheck
= false;
560 bool fullEffort
= false;
561 if( options::fullSaturateInst() ){
562 //we only add when interleaved with other strategies
563 doCheck
= quant_e
==QuantifiersEngine::QEFFORT_STANDARD
&& d_quantEngine
->hasAddedLemma();
565 if( options::fullSaturateQuant() && !doCheck
){
566 doCheck
= quant_e
==QuantifiersEngine::QEFFORT_LAST_CALL
;
567 fullEffort
= !d_quantEngine
->hasAddedLemma();
571 if( Trace
.isOn("fs-engine") ){
572 clSet
= double(clock())/double(CLOCKS_PER_SEC
);
573 Trace("fs-engine") << "---Full Saturation Round, effort = " << e
<< "---" << std::endl
;
576 for( unsigned i
=0; i
<d_quantEngine
->getModel()->getNumAssertedQuantifiers(); i
++ ){
577 Node q
= d_quantEngine
->getModel()->getAssertedQuantifier( i
, true );
578 if( d_quantEngine
->hasOwnership( q
, this ) && d_quantEngine
->getModel()->isQuantifierActive( q
) ){
579 if( process( q
, fullEffort
) ){
582 if( d_quantEngine
->inConflict() ){
588 if( Trace
.isOn("fs-engine") ){
589 Trace("fs-engine") << "Added lemmas = " << addedLemmas
<< std::endl
;
590 double clSet2
= double(clock())/double(CLOCKS_PER_SEC
);
591 Trace("fs-engine") << "Finished instantiation engine, time = " << (clSet2
-clSet
) << std::endl
;
596 bool FullSaturation::process( Node f
, bool fullEffort
){
597 //first, try from relevant domain
598 RelevantDomain
* rd
= d_quantEngine
->getRelevantDomain();
599 unsigned rstart
= options::fullSaturateQuantRd() ? 0 : 1;
600 unsigned rend
= fullEffort
? 1 : rstart
;
601 for( unsigned r
=rstart
; r
<=rend
; r
++ ){
604 if( d_guessed.find( f )==d_guessed.end() ){
605 Trace("inst-alg") << "-> Guess instantiate " << f << "..." << std::endl;
608 if( d_quantEngine->addInstantiation( f, m ) ){
609 ++(d_quantEngine->d_statistics.d_instantiations_guess);
616 Trace("inst-alg") << "-> Relevant domain instantiate " << f
<< "..." << std::endl
;
618 Trace("inst-alg") << "-> Ground term instantiate " << f
<< "..." << std::endl
;
621 unsigned final_max_i
= 0;
622 std::vector
< unsigned > maxs
;
623 std::vector
< bool > max_zero
;
624 bool has_zero
= false;
625 for(unsigned i
=0; i
<f
[0].getNumChildren(); i
++ ){
628 ts
= rd
->getRDomain( f
, i
)->d_terms
.size();
630 ts
= d_quantEngine
->getTermDatabase()->getNumTypeGroundTerms( f
[0][i
].getType() );
632 max_zero
.push_back( fullEffort
&& ts
==0 );
633 ts
= ( fullEffort
&& ts
==0 ) ? 1 : ts
;
634 Trace("inst-alg-rd") << "Variable " << i
<< " has " << ts
<< " in relevant domain." << std::endl
;
639 maxs
.push_back( ts
);
640 if( ts
>final_max_i
){
646 std::vector
< TypeNode
> ftypes
;
647 for( unsigned i
=0; i
<f
[0].getNumChildren(); i
++ ){
648 ftypes
.push_back( f
[0][i
].getType() );
651 Trace("inst-alg-rd") << "Will do " << final_max_i
<< " stages of instantiation." << std::endl
;
654 while( max_i
<=final_max_i
){
655 Trace("inst-alg-rd") << "Try stage " << max_i
<< "..." << std::endl
;
656 std::vector
< unsigned > childIndex
;
659 while( index
>=0 && index
<(int)f
[0].getNumChildren() ){
660 if( index
==(int)childIndex
.size() ){
661 childIndex
.push_back( -1 );
663 Assert( index
==(int)(childIndex
.size())-1 );
664 unsigned nv
= childIndex
[index
]+1;
665 if( options::cbqi() && r
==1 && !max_zero
[index
] ){
666 //skip inst constant nodes
667 while( nv
<maxs
[index
] && nv
<=max_i
&&
668 quantifiers::TermDb::hasInstConstAttr( d_quantEngine
->getTermDatabase()->getTypeGroundTerm( ftypes
[index
], nv
) ) ){
672 if( nv
<maxs
[index
] && nv
<=max_i
){
673 childIndex
[index
] = nv
;
676 childIndex
.pop_back();
683 Trace("inst-alg-rd") << "Try instantiation { ";
684 for( unsigned j
=0; j
<childIndex
.size(); j
++ ){
685 Trace("inst-alg-rd") << childIndex
[j
] << " ";
687 Trace("inst-alg-rd") << "}" << std::endl
;
689 std::vector
< Node
> terms
;
690 for( unsigned i
=0; i
<f
[0].getNumChildren(); i
++ ){
692 //no terms available, will report incomplete instantiation
693 terms
.push_back( Node::null() );
694 Trace("inst-alg-rd") << " null" << std::endl
;
696 terms
.push_back( rd
->getRDomain( f
, i
)->d_terms
[childIndex
[i
]] );
697 Trace("inst-alg-rd") << " " << rd
->getRDomain( f
, i
)->d_terms
[childIndex
[i
]] << std::endl
;
699 terms
.push_back( d_quantEngine
->getTermDatabase()->getTypeGroundTerm( ftypes
[i
], childIndex
[i
] ) );
700 Trace("inst-alg-rd") << " " << d_quantEngine
->getTermDatabase()->getTypeGroundTerm( ftypes
[i
], childIndex
[i
] ) << std::endl
;
703 if( d_quantEngine
->addInstantiation( f
, terms
, false ) ){
704 Trace("inst-alg-rd") << "Success!" << std::endl
;
705 ++(d_quantEngine
->d_statistics
.d_instantiations_guess
);
721 void FullSaturation::registerQuantifier( Node q
) {