1 /********************* */
2 /*! \file inst_match.cpp
4 ** Original author: ajreynol
5 ** Major contributors: none
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
14 ** \brief Implementation of inst match class
17 #include "theory/inst_match.h"
18 #include "theory/theory_engine.h"
19 #include "theory/quantifiers_engine.h"
20 #include "theory/candidate_generator.h"
21 #include "theory/uf/theory_uf_instantiator.h"
22 #include "theory/uf/equality_engine.h"
23 #include "theory/quantifiers/options.h"
24 #include "theory/quantifiers/model_engine.h"
25 #include "theory/quantifiers/term_database.h"
26 #include "theory/quantifiers/first_order_model.h"
27 #include "theory/quantifiers/term_database.h"
31 using namespace CVC4::kind
;
32 using namespace CVC4::context
;
33 using namespace CVC4::theory
;
34 using namespace CVC4::theory::inst
;
37 InstMatch::InstMatch() {
40 InstMatch::InstMatch( InstMatch
* m
) {
44 bool InstMatch::setMatch( EqualityQuery
* q
, TNode v
, TNode m
, bool & set
){
45 std::map
< Node
, Node
>::iterator vn
= d_map
.find( v
);
46 if( vn
==d_map
.end() ){
49 Debug("matching-debug") << "Add partial " << v
<< "->" << m
<< std::endl
;
53 return q
->areEqual( vn
->second
, m
);
57 bool InstMatch::setMatch( EqualityQuery
* q
, TNode v
, TNode m
){
59 return setMatch(q
,v
,m
,set
);
62 bool InstMatch::add( InstMatch
& m
){
63 for( std::map
< Node
, Node
>::iterator it
= m
.d_map
.begin(); it
!= m
.d_map
.end(); ++it
){
64 if( d_map
.find( it
->first
)==d_map
.end() ){
65 d_map
[it
->first
] = it
->second
;
71 bool InstMatch::merge( EqualityQuery
* q
, InstMatch
& m
){
72 for( std::map
< Node
, Node
>::iterator it
= m
.d_map
.begin(); it
!= m
.d_map
.end(); ++it
){
73 if( d_map
.find( it
->first
)==d_map
.end() ){
74 d_map
[ it
->first
] = it
->second
;
76 if( it
->second
!=d_map
[it
->first
] ){
77 if( !q
->areEqual( it
->second
, d_map
[it
->first
] ) ){
87 void InstMatch::debugPrint( const char* c
){
88 for( std::map
< Node
, Node
>::iterator it
= d_map
.begin(); it
!= d_map
.end(); ++it
){
89 Debug( c
) << " " << it
->first
<< " -> " << it
->second
<< std::endl
;
91 //if( !d_splits.empty() ){
92 // Debug( c ) << " Conditions: ";
93 // for( std::map< Node, Node >::iterator it = d_splits.begin(); it !=d_splits.end(); ++it ){
94 // Debug( c ) << it->first << " = " << it->second << " ";
96 // Debug( c ) << std::endl;
100 void InstMatch::makeComplete( Node f
, QuantifiersEngine
* qe
){
101 for( int i
=0; i
<(int)qe
->getTermDatabase()->d_inst_constants
[f
].size(); i
++ ){
102 Node ic
= qe
->getTermDatabase()->d_inst_constants
[f
][i
];
103 if( d_map
.find( ic
)==d_map
.end() ){
104 d_map
[ ic
] = qe
->getTermDatabase()->getFreeVariableForInstConstant( ic
);
109 void InstMatch::makeInternal( QuantifiersEngine
* qe
){
110 if( options::cbqi() ){
111 for( std::map
< Node
, Node
>::iterator it
= d_map
.begin(); it
!= d_map
.end(); ++it
){
112 if( it
->second
.hasAttribute(InstConstantAttribute()) ){
113 d_map
[ it
->first
] = qe
->getEqualityQuery()->getInternalRepresentative( it
->second
);
114 if( it
->second
.hasAttribute(InstConstantAttribute()) ){
115 d_map
[ it
->first
] = qe
->getTermDatabase()->getFreeVariableForInstConstant( it
->first
);
122 void InstMatch::makeRepresentative( QuantifiersEngine
* qe
){
123 for( std::map
< Node
, Node
>::iterator it
= d_map
.begin(); it
!= d_map
.end(); ++it
){
124 d_map
[ it
->first
] = qe
->getEqualityQuery()->getInternalRepresentative( it
->second
);
125 if( options::cbqi() && it
->second
.hasAttribute(InstConstantAttribute()) ){
126 d_map
[ it
->first
] = qe
->getTermDatabase()->getFreeVariableForInstConstant( it
->first
);
131 void InstMatch::applyRewrite(){
132 for( std::map
< Node
, Node
>::iterator it
= d_map
.begin(); it
!= d_map
.end(); ++it
){
133 it
->second
= Rewriter::rewrite(it
->second
);
137 void InstMatch::computeTermVec( QuantifiersEngine
* qe
, const std::vector
< Node
>& vars
, std::vector
< Node
>& match
){
138 for( int i
=0; i
<(int)vars
.size(); i
++ ){
139 std::map
< Node
, Node
>::iterator it
= d_map
.find( vars
[i
] );
140 if( it
!=d_map
.end() && !it
->second
.isNull() ){
141 match
.push_back( it
->second
);
143 match
.push_back( qe
->getTermDatabase()->getFreeVariableForInstConstant( vars
[i
] ) );
147 void InstMatch::computeTermVec( const std::vector
< Node
>& vars
, std::vector
< Node
>& match
){
148 for( int i
=0; i
<(int)vars
.size(); i
++ ){
149 match
.push_back( d_map
[ vars
[i
] ] );
154 /** add match m for quantifier f starting at index, take into account equalities q, return true if successful */
155 void InstMatchTrie::addInstMatch2( QuantifiersEngine
* qe
, Node f
, InstMatch
& m
, int index
, ImtIndexOrder
* imtio
){
156 if( long(index
)<long(f
[0].getNumChildren()) && ( !imtio
|| long(index
)<long(imtio
->d_order
.size()) ) ){
157 int i_index
= imtio
? imtio
->d_order
[index
] : index
;
158 Node n
= m
.get( qe
->getTermDatabase()->getInstantiationConstant( f
, i_index
) );
159 d_data
[n
].addInstMatch2( qe
, f
, m
, index
+1, imtio
);
164 bool InstMatchTrie::existsInstMatch( QuantifiersEngine
* qe
, Node f
, InstMatch
& m
, bool modEq
, int index
, ImtIndexOrder
* imtio
){
165 if( long(index
)==long(f
[0].getNumChildren()) || ( imtio
&& long(index
)==long(imtio
->d_order
.size()) ) ){
168 int i_index
= imtio
? imtio
->d_order
[index
] : index
;
169 Node n
= m
.get( qe
->getTermDatabase()->getInstantiationConstant( f
, i_index
) );
170 std::map
< Node
, InstMatchTrie
>::iterator it
= d_data
.find( n
);
171 if( it
!=d_data
.end() ){
172 if( it
->second
.existsInstMatch( qe
, f
, m
, modEq
, index
+1, imtio
) ){
177 //check modulo equality if any other instantiation match exists
178 if( qe
->getEqualityQuery()->getEngine()->hasTerm( n
) ){
179 eq::EqClassIterator
eqc( qe
->getEqualityQuery()->getEngine()->getRepresentative( n
),
180 qe
->getEqualityQuery()->getEngine() );
181 while( !eqc
.isFinished() ){
184 std::map
< Node
, InstMatchTrie
>::iterator itc
= d_data
.find( en
);
185 if( itc
!=d_data
.end() ){
186 if( itc
->second
.existsInstMatch( qe
, f
, m
, modEq
, index
+1, imtio
) ){
194 //for( std::map< Node, InstMatchTrie >::iterator itc = d_data.begin(); itc != d_data.end(); ++itc ){
195 // if( itc->first!=n && qe->getEqualityQuery()->areEqual( n, itc->first ) ){
196 // if( itc->second.existsInstMatch( qe, f, m, modEq, index+1 ) ){
206 bool InstMatchTrie::addInstMatch( QuantifiersEngine
* qe
, Node f
, InstMatch
& m
, bool modEq
, ImtIndexOrder
* imtio
){
207 if( !existsInstMatch( qe
, f
, m
, modEq
, 0, imtio
) ){
208 addInstMatch2( qe
, f
, m
, 0, imtio
);
215 InstMatchGenerator::InstMatchGenerator( Node pat
, QuantifiersEngine
* qe
, int matchPolicy
) : d_matchPolicy( matchPolicy
){
216 initializePattern( pat
, qe
);
219 InstMatchGenerator::InstMatchGenerator( std::vector
< Node
>& pats
, QuantifiersEngine
* qe
, int matchPolicy
) : d_matchPolicy( matchPolicy
){
220 if( pats
.size()==1 ){
221 initializePattern( pats
[0], qe
);
223 initializePatterns( pats
, qe
);
227 void InstMatchGenerator::initializePatterns( std::vector
< Node
>& pats
, QuantifiersEngine
* qe
){
228 int childMatchPolicy
= d_matchPolicy
==MATCH_GEN_EFFICIENT_E_MATCH
? 0 : d_matchPolicy
;
229 for( int i
=0; i
<(int)pats
.size(); i
++ ){
230 d_children
.push_back( new InstMatchGenerator( pats
[i
], qe
, childMatchPolicy
) );
232 d_pattern
= Node::null();
233 d_match_pattern
= Node::null();
237 void InstMatchGenerator::initializePattern( Node pat
, QuantifiersEngine
* qe
){
238 Debug("inst-match-gen") << "Pattern term is " << pat
<< std::endl
;
239 Assert( pat
.hasAttribute(InstConstantAttribute()) );
241 d_match_pattern
= pat
;
242 if( d_match_pattern
.getKind()==NOT
){
243 //we want to add the children of the NOT
244 d_match_pattern
= d_pattern
[0];
246 if( d_match_pattern
.getKind()==IFF
|| d_match_pattern
.getKind()==EQUAL
){
247 if( !d_match_pattern
[0].hasAttribute(InstConstantAttribute()) ){
248 Assert( d_match_pattern
[1].hasAttribute(InstConstantAttribute()) );
250 d_pattern
= NodeManager::currentNM()->mkNode( d_match_pattern
.getKind(), d_match_pattern
[1], d_match_pattern
[0] );
251 d_pattern
= pat
.getKind()==NOT
? d_pattern
.notNode() : d_pattern
;
252 if( pat
.getKind()!=NOT
){ //TEMPORARY until we do better implementation of disequality matching
253 d_match_pattern
= d_match_pattern
[1];
255 d_match_pattern
= d_pattern
[0][0];
257 }else if( !d_match_pattern
[1].hasAttribute(InstConstantAttribute()) ){
258 Assert( d_match_pattern
[0].hasAttribute(InstConstantAttribute()) );
259 if( pat
.getKind()!=NOT
){ //TEMPORARY until we do better implementation of disequality matching
260 d_match_pattern
= d_match_pattern
[0];
264 int childMatchPolicy
= MATCH_GEN_DEFAULT
;
265 for( int i
=0; i
<(int)d_match_pattern
.getNumChildren(); i
++ ){
266 if( d_match_pattern
[i
].hasAttribute(InstConstantAttribute()) ){
267 if( d_match_pattern
[i
].getKind()!=INST_CONSTANT
){
268 d_children
.push_back( new InstMatchGenerator( d_match_pattern
[i
], qe
, childMatchPolicy
) );
269 d_children_index
.push_back( i
);
274 Debug("inst-match-gen") << "Pattern is " << d_pattern
<< ", match pattern is " << d_match_pattern
<< std::endl
;
276 //create candidate generator
277 if( d_match_pattern
.getKind()==EQUAL
|| d_match_pattern
.getKind()==IFF
){
278 Assert( d_matchPolicy
==MATCH_GEN_DEFAULT
);
279 //we will be producing candidates via literal matching heuristics
280 if( d_pattern
.getKind()!=NOT
){
281 //candidates will be all equalities
282 d_cg
= new inst::CandidateGeneratorQELitEq( qe
, d_match_pattern
);
284 //candidates will be all disequalities
285 d_cg
= new inst::CandidateGeneratorQELitDeq( qe
, d_match_pattern
);
287 }else if( d_pattern
.getKind()==EQUAL
|| d_pattern
.getKind()==IFF
|| d_pattern
.getKind()==NOT
){
288 Assert( d_matchPolicy
==MATCH_GEN_DEFAULT
);
289 if( d_pattern
.getKind()==NOT
){
290 Unimplemented("Disequal generator unimplemented");
292 Assert( Trigger::isAtomicTrigger( d_match_pattern
) );
293 //we are matching only in a particular equivalence class
294 d_cg
= new inst::CandidateGeneratorQE( qe
, d_match_pattern
.getOperator() );
295 //store the equivalence class that we will call d_cg->reset( ... ) on
296 d_eq_class
= d_pattern
[1];
298 }else if( Trigger::isAtomicTrigger( d_match_pattern
) ){
299 //if( d_matchPolicy==MATCH_GEN_EFFICIENT_E_MATCH ){
300 //Warning() << "Currently efficient e matching is not taken into account for quantifiers: " << d_pattern << std::endl;
302 //we will be scanning lists trying to find d_match_pattern.getOperator()
303 d_cg
= new inst::CandidateGeneratorQE( qe
, d_match_pattern
.getOperator() );
305 d_cg
= new CandidateGeneratorQueue
;
306 if( !Trigger::getPatternArithmetic( d_match_pattern
.getAttribute(InstConstantAttribute()), d_match_pattern
, d_arith_coeffs
) ){
307 Debug("inst-match-gen") << "(?) Unknown matching pattern is " << d_match_pattern
<< std::endl
;
308 Warning() << "(?) Unknown matching pattern is " << d_match_pattern
<< std::endl
;
309 d_matchPolicy
= MATCH_GEN_INTERNAL_ERROR
;
311 Debug("matching-arith") << "Generated arithmetic pattern for " << d_match_pattern
<< ": " << std::endl
;
312 for( std::map
< Node
, Node
>::iterator it
= d_arith_coeffs
.begin(); it
!= d_arith_coeffs
.end(); ++it
){
313 Debug("matching-arith") << " " << it
->first
<< " -> " << it
->second
<< std::endl
;
315 //we will treat this as match gen internal arithmetic
316 d_matchPolicy
= MATCH_GEN_INTERNAL_ARITHMETIC
;
321 /** get match (not modulo equality) */
322 bool InstMatchGenerator::getMatch( Node t
, InstMatch
& m
, QuantifiersEngine
* qe
){
323 Debug("matching") << "Matching " << t
<< " against pattern " << d_match_pattern
<< " ("
324 << m
.size() << ")" << ", " << d_children
.size() << std::endl
;
325 Assert( !d_match_pattern
.isNull() );
326 if( qe
->d_optMatchIgnoreModelBasis
&& t
.getAttribute(ModelBasisAttribute()) ){
328 }else if( d_matchPolicy
==MATCH_GEN_INTERNAL_ARITHMETIC
){
329 return getMatchArithmetic( t
, m
, qe
);
330 }else if( d_matchPolicy
==MATCH_GEN_INTERNAL_ERROR
){
333 EqualityQuery
* q
= qe
->getEqualityQuery();
334 //add m to partial match vector
335 std::vector
< InstMatch
> partial
;
336 partial
.push_back( InstMatch( &m
) );
338 Assert( !t
.isNull() );
339 Assert( !t
.hasAttribute(InstConstantAttribute()) );
340 Assert( t
.getKind()==d_match_pattern
.getKind() );
341 Assert( !Trigger::isAtomicTrigger( d_match_pattern
) || t
.getOperator()==d_match_pattern
.getOperator() );
342 //first, check if ground arguments are not equal, or a match is in conflict
343 for( int i
=0; i
<(int)d_match_pattern
.getNumChildren(); i
++ ){
344 if( d_match_pattern
[i
].hasAttribute(InstConstantAttribute()) ){
345 if( d_match_pattern
[i
].getKind()==INST_CONSTANT
){
346 if( !partial
[0].setMatch( q
, d_match_pattern
[i
], t
[i
] ) ){
347 //match is in conflict
348 Debug("matching-debug") << "Match in conflict " << t
[i
] << " and "
349 << d_match_pattern
[i
] << " because "
350 << partial
[0].get(d_match_pattern
[i
])
352 Debug("matching-fail") << "Match fail: " << partial
[0].get(d_match_pattern
[i
]) << " and " << t
[i
] << std::endl
;
357 if( !q
->areEqual( d_match_pattern
[i
], t
[i
] ) ){
358 Debug("matching-fail") << "Match fail arg: " << d_match_pattern
[i
] << " and " << t
[i
] << std::endl
;
359 //ground arguments are not equal
364 //now, fit children into match
365 //we will be requesting candidates for matching terms for each child
366 std::vector
< Node
> reps
;
367 for( int i
=0; i
<(int)d_children
.size(); i
++ ){
368 Node rep
= q
->getRepresentative( t
[ d_children_index
[i
] ] );
369 reps
.push_back( rep
);
370 d_children
[i
]->d_cg
->reset( rep
);
373 //combine child matches
375 while( index
>=0 && index
<(int)d_children
.size() ){
376 partial
.push_back( InstMatch( &partial
[index
] ) );
377 if( d_children
[index
]->getNextMatch2( partial
[index
+1], qe
) ){
380 d_children
[index
]->d_cg
->reset( reps
[index
] );
382 if( !partial
.empty() ){
397 bool InstMatchGenerator::getNextMatch2( InstMatch
& m
, QuantifiersEngine
* qe
, bool saveMatched
){
398 bool success
= false;
401 //get the next candidate term t
402 t
= d_cg
->getNextCandidate();
403 //if t not null, try to fit it into match m
404 if( !t
.isNull() && t
.getType()==d_match_pattern
.getType() ){
405 success
= getMatch( t
, m
, qe
);
407 }while( !success
&& !t
.isNull() );
408 if (saveMatched
) m
.d_matched
= t
;
412 bool InstMatchGenerator::getMatchArithmetic( Node t
, InstMatch
& m
, QuantifiersEngine
* qe
){
413 Debug("matching-arith") << "Matching " << t
<< " " << d_match_pattern
<< std::endl
;
414 if( !d_arith_coeffs
.empty() ){
415 NodeBuilder
<> tb(kind::PLUS
);
416 Node ic
= Node::null();
417 for( std::map
< Node
, Node
>::iterator it
= d_arith_coeffs
.begin(); it
!= d_arith_coeffs
.end(); ++it
){
418 Debug("matching-arith") << it
->first
<< " -> " << it
->second
<< std::endl
;
419 if( !it
->first
.isNull() ){
420 if( m
.find( it
->first
)==m
.end() ){
421 //see if we can choose this to set
422 if( ic
.isNull() && ( it
->second
.isNull() || !it
->first
.getType().isInteger() ) ){
426 Debug("matching-arith") << "already set " << m
.get( it
->first
) << std::endl
;
427 Node tm
= m
.get( it
->first
);
428 if( !it
->second
.isNull() ){
429 tm
= NodeManager::currentNM()->mkNode( MULT
, it
->second
, tm
);
439 if( tb
.getNumChildren()==0 ){
442 tm
= tb
.getNumChildren()==1 ? tb
.getChild( 0 ) : tb
;
443 tm
= NodeManager::currentNM()->mkNode( MINUS
, t
, tm
);
445 if( !d_arith_coeffs
[ ic
].isNull() ){
446 Assert( !ic
.getType().isInteger() );
447 Node coeff
= NodeManager::currentNM()->mkConst( Rational(1) / d_arith_coeffs
[ ic
].getConst
<Rational
>() );
448 tm
= NodeManager::currentNM()->mkNode( MULT
, coeff
, tm
);
450 m
.set( ic
, Rewriter::rewrite( tm
));
451 //set the rest to zeros
452 for( std::map
< Node
, Node
>::iterator it
= d_arith_coeffs
.begin(); it
!= d_arith_coeffs
.end(); ++it
){
453 if( !it
->first
.isNull() ){
454 if( m
.find( it
->first
)==m
.end() ){
455 m
.set( it
->first
, NodeManager::currentNM()->mkConst( Rational(0) ) );
459 Debug("matching-arith") << "Setting " << ic
<< " to " << tm
<< std::endl
;
470 /** reset instantiation round */
471 void InstMatchGenerator::resetInstantiationRound( QuantifiersEngine
* qe
){
472 if( d_match_pattern
.isNull() ){
473 for( int i
=0; i
<(int)d_children
.size(); i
++ ){
474 d_children
[i
]->resetInstantiationRound( qe
);
478 d_cg
->resetInstantiationRound();
483 void InstMatchGenerator::reset( Node eqc
, QuantifiersEngine
* qe
){
484 if( d_match_pattern
.isNull() ){
485 for( int i
=0; i
<(int)d_children
.size(); i
++ ){
486 d_children
[i
]->reset( eqc
, qe
);
490 if( !d_eq_class
.isNull() ){
491 //we have a specific equivalence class in mind
492 //we are producing matches for f(E) ~ t, where E is a non-ground vector of terms, and t is a ground term
493 //just look in equivalence class of the RHS
494 d_cg
->reset( d_eq_class
);
501 bool InstMatchGenerator::getNextMatch( InstMatch
& m
, QuantifiersEngine
* qe
){
502 m
.d_matched
= Node::null();
503 if( d_match_pattern
.isNull() ){
504 int index
= (int)d_partial
.size();
505 while( index
>=0 && index
<(int)d_children
.size() ){
507 d_partial
.push_back( InstMatch( &d_partial
[index
-1] ) );
509 d_partial
.push_back( InstMatch() );
511 if( d_children
[index
]->getNextMatch( d_partial
[index
], qe
) ){
514 d_children
[index
]->reset( Node::null(), qe
);
515 d_partial
.pop_back();
516 if( !d_partial
.empty() ){
517 d_partial
.pop_back();
523 m
= d_partial
.back();
524 d_partial
.pop_back();
530 bool res
= getNextMatch2( m
, qe
, true );
531 Assert(!res
|| !m
.d_matched
.isNull());
538 // Currently the implementation doesn't take into account that
539 // variable should have the same value given.
540 // TODO use the d_children way perhaps
541 // TODO replace by a real dictionnary
542 // We should create a real substitution? slower more precise
543 // We don't do that often
544 bool InstMatchGenerator::nonunifiable( TNode t0
, const std::vector
<Node
> & vars
){
545 if(d_match_pattern
.isNull()) return true;
547 typedef std::vector
<std::pair
<TNode
,TNode
> > tstack
;
548 tstack
stack(1,std::make_pair(t0
,d_match_pattern
)); // t * pat
550 while(!stack
.empty()){
551 const std::pair
<TNode
,TNode
> p
= stack
.back(); stack
.pop_back();
552 const TNode
& t
= p
.first
;
553 const TNode
& pat
= p
.second
;
555 // t or pat is a variable currently we consider that can match anything
556 if( find(vars
.begin(),vars
.end(),t
) != vars
.end() ) continue;
557 if( pat
.getKind() == INST_CONSTANT
) continue;
559 // t and pat are nonunifiable
560 if( !Trigger::isAtomicTrigger( t
) || !Trigger::isAtomicTrigger( pat
) ) {
561 if(t
== pat
) continue;
564 if( t
.getOperator() != pat
.getOperator() ) return true;
566 //put the children on the stack
567 for( size_t i
=0; i
< pat
.getNumChildren(); i
++ ){
568 stack
.push_back(std::make_pair(t
[i
],pat
[i
]));
571 // The heuristic can't find non-unifiability
575 int InstMatchGenerator::addInstantiations( Node f
, InstMatch
& baseMatch
, QuantifiersEngine
* qe
){
576 //now, try to add instantiation for each match produced
579 while( getNextMatch( m
, qe
) ){
580 //m.makeInternal( d_quantEngine->getEqualityQuery() );
582 if( qe
->addInstantiation( f
, m
) ){
584 if( qe
->d_optInstLimitActive
&& qe
->d_optInstLimit
<=0 ){
590 //return number of lemmas added
594 int InstMatchGenerator::addTerm( Node f
, Node t
, QuantifiersEngine
* qe
){
595 Assert( options::eagerInstQuant() );
596 if( !d_match_pattern
.isNull() ){
598 if( getMatch( t
, m
, qe
) ){
599 if( qe
->addInstantiation( f
, m
) ){
604 for( int i
=0; i
<(int)d_children
.size(); i
++ ){
605 d_children
[i
]->addTerm( f
, t
, qe
);
612 InstMatchGeneratorMulti::InstMatchGeneratorMulti( Node f
, std::vector
< Node
>& pats
, QuantifiersEngine
* qe
, int matchOption
) :
614 Debug("smart-multi-trigger") << "Making smart multi-trigger for " << f
<< std::endl
;
615 std::map
< Node
, std::vector
< Node
> > var_contains
;
616 Trigger::getVarContains( f
, pats
, var_contains
);
617 //convert to indicies
618 for( std::map
< Node
, std::vector
< Node
> >::iterator it
= var_contains
.begin(); it
!= var_contains
.end(); ++it
){
619 Debug("smart-multi-trigger") << "Pattern " << it
->first
<< " contains: ";
620 for( int i
=0; i
<(int)it
->second
.size(); i
++ ){
621 Debug("smart-multi-trigger") << it
->second
[i
] << " ";
622 int index
= it
->second
[i
].getAttribute(InstVarNumAttribute());
623 d_var_contains
[ it
->first
].push_back( index
);
624 d_var_to_node
[ index
].push_back( it
->first
);
626 Debug("smart-multi-trigger") << std::endl
;
628 for( int i
=0; i
<(int)pats
.size(); i
++ ){
630 //make the match generator
631 d_children
.push_back( new InstMatchGenerator( n
, qe
, matchOption
) );
632 //compute unique/shared variables
633 std::vector
< int > unique_vars
;
634 std::map
< int, bool > shared_vars
;
635 int numSharedVars
= 0;
636 for( int j
=0; j
<(int)d_var_contains
[n
].size(); j
++ ){
637 if( d_var_to_node
[ d_var_contains
[n
][j
] ].size()==1 ){
638 Debug("smart-multi-trigger") << "Var " << d_var_contains
[n
][j
] << " is unique to " << pats
[i
] << std::endl
;
639 unique_vars
.push_back( d_var_contains
[n
][j
] );
641 shared_vars
[ d_var_contains
[n
][j
] ] = true;
645 //we use the latest shared variables, then unique variables
646 std::vector
< int > vars
;
647 int index
= i
==0 ? (int)(pats
.size()-1) : (i
-1);
648 while( numSharedVars
>0 && index
!=i
){
649 for( std::map
< int, bool >::iterator it
= shared_vars
.begin(); it
!= shared_vars
.end(); ++it
){
651 if( std::find( d_var_contains
[ pats
[index
] ].begin(), d_var_contains
[ pats
[index
] ].end(), it
->first
)!=
652 d_var_contains
[ pats
[index
] ].end() ){
653 vars
.push_back( it
->first
);
654 shared_vars
[ it
->first
] = false;
659 index
= index
==0 ? (int)(pats
.size()-1) : (index
-1);
661 vars
.insert( vars
.end(), unique_vars
.begin(), unique_vars
.end() );
662 Debug("smart-multi-trigger") << " Index[" << i
<< "]: ";
663 for( int i
=0; i
<(int)vars
.size(); i
++ ){
664 Debug("smart-multi-trigger") << vars
[i
] << " ";
666 Debug("smart-multi-trigger") << std::endl
;
667 //make ordered inst match trie
668 InstMatchTrie::ImtIndexOrder
* imtio
= new InstMatchTrie::ImtIndexOrder
;
669 imtio
->d_order
.insert( imtio
->d_order
.begin(), vars
.begin(), vars
.end() );
670 d_children_trie
.push_back( InstMatchTrieOrdered( imtio
) );
675 /** reset instantiation round (call this whenever equivalence classes have changed) */
676 void InstMatchGeneratorMulti::resetInstantiationRound( QuantifiersEngine
* qe
){
677 for( int i
=0; i
<(int)d_children
.size(); i
++ ){
678 d_children
[i
]->resetInstantiationRound( qe
);
682 /** reset, eqc is the equivalence class to search in (any if eqc=null) */
683 void InstMatchGeneratorMulti::reset( Node eqc
, QuantifiersEngine
* qe
){
684 for( int i
=0; i
<(int)d_children
.size(); i
++ ){
685 d_children
[i
]->reset( eqc
, qe
);
689 int InstMatchGeneratorMulti::addInstantiations( Node f
, InstMatch
& baseMatch
, QuantifiersEngine
* qe
){
691 Debug("smart-multi-trigger") << "Process smart multi trigger" << std::endl
;
692 for( int i
=0; i
<(int)d_children
.size(); i
++ ){
693 Debug("smart-multi-trigger") << "Calculate matches " << i
<< std::endl
;
694 std::vector
< InstMatch
> newMatches
;
696 while( d_children
[i
]->getNextMatch( m
, qe
) ){
697 m
.makeRepresentative( qe
);
698 newMatches
.push_back( InstMatch( &m
) );
701 for( int j
=0; j
<(int)newMatches
.size(); j
++ ){
702 processNewMatch( qe
, newMatches
[j
], i
, addedLemmas
);
708 void InstMatchGeneratorMulti::processNewMatch( QuantifiersEngine
* qe
, InstMatch
& m
, int fromChildIndex
, int& addedLemmas
){
709 //see if these produce new matches
710 d_children_trie
[fromChildIndex
].addInstMatch( qe
, d_f
, m
, true );
711 //possibly only do the following if we know that new matches will be produced?
712 //the issue is that instantiations are filtered in quantifiers engine, and so there is no guarentee that
713 // we can safely skip the following lines, even when we have already produced this match.
714 Debug("smart-multi-trigger") << "Child " << fromChildIndex
<< " produced match " << m
<< std::endl
;
715 //process new instantiations
716 int childIndex
= (fromChildIndex
+1)%(int)d_children
.size();
717 std::vector
< IndexedTrie
> unique_var_tries
;
718 processNewInstantiations( qe
, m
, addedLemmas
, d_children_trie
[childIndex
].getTrie(),
719 unique_var_tries
, 0, childIndex
, fromChildIndex
, true );
722 void InstMatchGeneratorMulti::processNewInstantiations( QuantifiersEngine
* qe
, InstMatch
& m
, int& addedLemmas
, InstMatchTrie
* tr
,
723 std::vector
< IndexedTrie
>& unique_var_tries
,
724 int trieIndex
, int childIndex
, int endChildIndex
, bool modEq
){
725 if( childIndex
==endChildIndex
){
726 //now, process unique variables
727 processNewInstantiations2( qe
, m
, addedLemmas
, unique_var_tries
, 0 );
728 }else if( trieIndex
<(int)d_children_trie
[childIndex
].getOrdering()->d_order
.size() ){
729 int curr_index
= d_children_trie
[childIndex
].getOrdering()->d_order
[trieIndex
];
730 Node curr_ic
= qe
->getTermDatabase()->getInstantiationConstant( d_f
, curr_index
);
731 if( m
.find( curr_ic
)==m
.end() ){
732 //if( d_var_to_node[ curr_index ].size()==1 ){ //FIXME
733 // //unique variable(s), defer calculation
734 // unique_var_tries.push_back( IndexedTrie( std::pair< int, int >( childIndex, trieIndex ), tr ) );
735 // int newChildIndex = (childIndex+1)%(int)d_children.size();
736 // processNewInstantiations( qe, m, d_children_trie[newChildIndex].getTrie(), unique_var_tries,
737 // 0, newChildIndex, endChildIndex, modEq );
739 //shared and non-set variable, add to InstMatch
740 for( std::map
< Node
, InstMatchTrie
>::iterator it
= tr
->d_data
.begin(); it
!= tr
->d_data
.end(); ++it
){
742 mn
.set( curr_ic
, it
->first
);
743 processNewInstantiations( qe
, mn
, addedLemmas
, &(it
->second
), unique_var_tries
,
744 trieIndex
+1, childIndex
, endChildIndex
, modEq
);
748 //shared and set variable, try to merge
749 Node n
= m
.get( curr_ic
);
750 std::map
< Node
, InstMatchTrie
>::iterator it
= tr
->d_data
.find( n
);
751 if( it
!=tr
->d_data
.end() ){
752 processNewInstantiations( qe
, m
, addedLemmas
, &(it
->second
), unique_var_tries
,
753 trieIndex
+1, childIndex
, endChildIndex
, modEq
);
756 //check modulo equality for other possible instantiations
757 if( qe
->getEqualityQuery()->getEngine()->hasTerm( n
) ){
758 eq::EqClassIterator
eqc( qe
->getEqualityQuery()->getEngine()->getRepresentative( n
),
759 qe
->getEqualityQuery()->getEngine() );
760 while( !eqc
.isFinished() ){
763 std::map
< Node
, InstMatchTrie
>::iterator itc
= tr
->d_data
.find( en
);
764 if( itc
!=tr
->d_data
.end() ){
765 processNewInstantiations( qe
, m
, addedLemmas
, &(itc
->second
), unique_var_tries
,
766 trieIndex
+1, childIndex
, endChildIndex
, modEq
);
775 int newChildIndex
= (childIndex
+1)%(int)d_children
.size();
776 processNewInstantiations( qe
, m
, addedLemmas
, d_children_trie
[newChildIndex
].getTrie(), unique_var_tries
,
777 0, newChildIndex
, endChildIndex
, modEq
);
781 void InstMatchGeneratorMulti::processNewInstantiations2( QuantifiersEngine
* qe
, InstMatch
& m
, int& addedLemmas
,
782 std::vector
< IndexedTrie
>& unique_var_tries
,
783 int uvtIndex
, InstMatchTrie
* tr
, int trieIndex
){
784 if( uvtIndex
<(int)unique_var_tries
.size() ){
785 int childIndex
= unique_var_tries
[uvtIndex
].first
.first
;
787 tr
= unique_var_tries
[uvtIndex
].second
;
788 trieIndex
= unique_var_tries
[uvtIndex
].first
.second
;
790 if( trieIndex
<(int)d_children_trie
[childIndex
].getOrdering()->d_order
.size() ){
791 int curr_index
= d_children_trie
[childIndex
].getOrdering()->d_order
[trieIndex
];
792 Node curr_ic
= qe
->getTermDatabase()->getInstantiationConstant( d_f
, curr_index
);
793 //unique non-set variable, add to InstMatch
794 for( std::map
< Node
, InstMatchTrie
>::iterator it
= tr
->d_data
.begin(); it
!= tr
->d_data
.end(); ++it
){
796 mn
.set( curr_ic
, it
->first
);
797 processNewInstantiations2( qe
, mn
, addedLemmas
, unique_var_tries
, uvtIndex
, &(it
->second
), trieIndex
+1 );
800 processNewInstantiations2( qe
, m
, addedLemmas
, unique_var_tries
, uvtIndex
+1 );
803 //m is an instantiation
804 if( qe
->addInstantiation( d_f
, m
) ){
806 Debug("smart-multi-trigger") << "-> Produced instantiation " << m
<< std::endl
;
811 int InstMatchGeneratorMulti::addTerm( Node f
, Node t
, QuantifiersEngine
* qe
){
812 Assert( options::eagerInstQuant() );
814 for( int i
=0; i
<(int)d_children
.size(); i
++ ){
815 if( ((InstMatchGenerator
*)d_children
[i
])->d_match_pattern
.getOperator()==t
.getOperator() ){
817 //if it produces a match, then process it with the rest
818 if( ((InstMatchGenerator
*)d_children
[i
])->getMatch( t
, m
, qe
) ){
819 processNewMatch( qe
, m
, i
, addedLemmas
);
826 int InstMatchGeneratorSimple::addInstantiations( Node f
, InstMatch
& baseMatch
, QuantifiersEngine
* qe
){
830 if( d_match_pattern
.getType()==NodeManager::currentNM()->booleanType() ){
831 for( int i
=0; i
<2; i
++ ){
832 addInstantiations( m
, qe
, addedLemmas
, 0, &(qe
->getTermDatabase()->d_pred_map_trie
[i
][ d_match_pattern
.getOperator() ]) );
835 addInstantiations( m
, qe
, addedLemmas
, 0, &(qe
->getTermDatabase()->d_func_map_trie
[ d_match_pattern
.getOperator() ]) );
840 void InstMatchGeneratorSimple::addInstantiations( InstMatch
& m
, QuantifiersEngine
* qe
, int& addedLemmas
, int argIndex
, quantifiers::TermArgTrie
* tat
){
841 if( argIndex
==(int)d_match_pattern
.getNumChildren() ){
842 //m is an instantiation
843 if( qe
->addInstantiation( d_f
, m
) ){
845 Debug("simple-multi-trigger") << "-> Produced instantiation " << m
<< std::endl
;
848 if( d_match_pattern
[argIndex
].getKind()==INST_CONSTANT
){
849 Node ic
= d_match_pattern
[argIndex
];
850 for( std::map
< Node
, quantifiers::TermArgTrie
>::iterator it
= tat
->d_data
.begin(); it
!= tat
->d_data
.end(); ++it
){
852 if( m
.get( ic
).isNull() || m
.get( ic
)==t
){
853 Node prev
= m
.get( ic
);
855 addInstantiations( m
, qe
, addedLemmas
, argIndex
+1, &(it
->second
) );
860 Node r
= qe
->getEqualityQuery()->getRepresentative( d_match_pattern
[argIndex
] );
861 std::map
< Node
, quantifiers::TermArgTrie
>::iterator it
= tat
->d_data
.find( r
);
862 if( it
!=tat
->d_data
.end() ){
863 addInstantiations( m
, qe
, addedLemmas
, argIndex
+1, &(it
->second
) );
869 int InstMatchGeneratorSimple::addTerm( Node f
, Node t
, QuantifiersEngine
* qe
){
870 Assert( options::eagerInstQuant() );
872 for( int i
=0; i
<(int)t
.getNumChildren(); i
++ ){
873 if( d_match_pattern
[i
].getKind()==INST_CONSTANT
){
874 m
.set(d_match_pattern
[i
], t
[i
]);
875 }else if( !qe
->getEqualityQuery()->areEqual( d_match_pattern
[i
], t
[i
] ) ){
879 return qe
->addInstantiation( f
, m
) ? 1 : 0;