1 /********************* */
2 /*! \file theory_uf_instantiator.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 theory uf instantiator class
17 #include "theory/uf/theory_uf_instantiator.h"
18 #include "theory/theory_engine.h"
19 #include "theory/uf/theory_uf.h"
20 #include "theory/rewriterules/rr_candidate_generator.h"
21 #include "theory/uf/equality_engine.h"
22 #include "theory/quantifiers/options.h"
23 #include "theory/rewriterules/options.h"
24 #include "theory/quantifiers/term_database.h"
28 using namespace CVC4::kind
;
29 using namespace CVC4::context
;
30 using namespace CVC4::theory
;
31 using namespace CVC4::theory::uf
;
32 using namespace CVC4::theory::inst
;
38 inline std::ostream
& operator<<(std::ostream
& out
, const InstantiatorTheoryUf::Ips
& ips
) {
42 EqClassInfo::EqClassInfo( context::Context
* c
) : d_funs( c
), d_pfuns( c
), d_disequal( c
){
47 void EqClassInfo::setMember( Node n
, quantifiers::TermDb
* db
){
48 if( n
.hasOperator() ){
49 d_funs
.insertAtContextLevelZero(n
.getOperator(),true);
51 //add parent functions
52 for( std::hash_map
< Node
, std::hash_map
< int, std::vector
< Node
> >, NodeHashFunction
>::iterator it
= db
->d_parents
[n
].begin();
53 it
!= db
->d_parents
[n
].end(); ++it
){
54 //TODO Is it true to do it at level 0? That depend when SetMember is called
55 // At worst it is a good overapproximation
56 d_pfuns
.insertAtContextLevelZero( it
->first
, true);
61 bool EqClassInfo::hasFunction( Node op
){
62 return d_funs
.find( op
)!=d_funs
.end();
65 bool EqClassInfo::hasParent( Node op
){
66 return d_pfuns
.find( op
)!=d_pfuns
.end();
69 //merge with another eq class info
70 void EqClassInfo::merge( EqClassInfo
* eci
){
71 for( BoolMap::iterator it
= eci
->d_funs
.begin(); it
!= eci
->d_funs
.end(); it
++ ) {
72 d_funs
[ (*it
).first
] = true;
74 for( BoolMap::iterator it
= eci
->d_pfuns
.begin(); it
!= eci
->d_pfuns
.end(); it
++ ) {
75 d_pfuns
[ (*it
).first
] = true;
79 inline void outputEqClassInfo( const char* c
, const EqClassInfo
* eci
){
81 for( EqClassInfo::BoolMap::iterator it
= eci
->d_funs
.begin(); it
!= eci
->d_funs
.end(); it
++ ) {
82 Debug(c
) << (*it
).first
<< ",";
84 Debug(c
) << std::endl
<< "pfuns:";
85 for( EqClassInfo::BoolMap::iterator it
= eci
->d_pfuns
.begin(); it
!= eci
->d_pfuns
.end(); it
++ ) {
86 Debug(c
) << (*it
).first
<< ",";
88 Debug(c
) << std::endl
;
93 InstantiatorTheoryUf::InstantiatorTheoryUf(context::Context
* c
, CVC4::theory::QuantifiersEngine
* qe
, Theory
* th
) :
94 Instantiator( c
, qe
, th
)
96 if( !options::finiteModelFind() || options::fmfInstEngine() ){
97 if( options::cbqi() ){
98 addInstStrategy( new InstStrategyCheckCESolved( this, qe
) );
100 if( options::userPatternsQuant() ){
101 d_isup
= new InstStrategyUserPatterns( this, qe
);
102 addInstStrategy( d_isup
);
106 InstStrategyAutoGenTriggers
* i_ag
= new InstStrategyAutoGenTriggers( this, qe
, Trigger::TS_ALL
,
107 InstStrategyAutoGenTriggers::RELEVANCE_DEFAULT
, 3 );
108 i_ag
->setGenerateAdditional( true );
109 addInstStrategy( i_ag
);
110 //addInstStrategy( new InstStrategyAddFailSplits( this, ie ) );
111 if( !options::finiteModelFind() ){
112 addInstStrategy( new InstStrategyFreeVariable( this, qe
) );
114 //d_isup->setPriorityOver( i_ag );
115 //d_isup->setPriorityOver( i_agm );
116 //i_ag->setPriorityOver( i_agm );
120 void InstantiatorTheoryUf::preRegisterTerm( Node t
){
121 //d_quantEngine->addTermToDatabase( t );
124 void InstantiatorTheoryUf::assertNode( Node assertion
)
126 Debug("quant-uf-assert") << "InstantiatorTheoryUf::check: " << assertion
<< std::endl
;
127 //preRegisterTerm( assertion );
128 d_quantEngine
->addTermToDatabase( assertion
);
129 if( options::cbqi() ){
130 if( assertion
.hasAttribute(InstConstantAttribute()) ){
131 setHasConstraintsFrom( assertion
.getAttribute(InstConstantAttribute()) );
132 }else if( assertion
.getKind()==NOT
&& assertion
[0].hasAttribute(InstConstantAttribute()) ){
133 setHasConstraintsFrom( assertion
[0].getAttribute(InstConstantAttribute()) );
138 void InstantiatorTheoryUf::addUserPattern( Node f
, Node pat
){
140 d_isup
->addUserPattern( f
, pat
);
142 setHasConstraintsFrom( f
);
146 void InstantiatorTheoryUf::processResetInstantiationRound( Theory::Effort effort
){
147 d_ground_reps
.clear();
150 int InstantiatorTheoryUf::process( Node f
, Theory::Effort effort
, int e
){
151 Debug("quant-uf") << "UF: Try to solve (" << e
<< ") for " << f
<< "... " << std::endl
;
152 return InstStrategy::STATUS_SAT
;
155 void InstantiatorTheoryUf::debugPrint( const char* c
)
160 bool InstantiatorTheoryUf::hasTerm( Node a
){
161 return ((TheoryUF
*)d_th
)->d_equalityEngine
.hasTerm( a
);
164 bool InstantiatorTheoryUf::areEqual( Node a
, Node b
){
167 }else if( hasTerm( a
) && hasTerm( b
) ){
168 return ((TheoryUF
*)d_th
)->d_equalityEngine
.areEqual( a
, b
);
174 bool InstantiatorTheoryUf::areDisequal( Node a
, Node b
){
177 }else if( hasTerm( a
) && hasTerm( b
) ){
178 return ((TheoryUF
*)d_th
)->d_equalityEngine
.areDisequal( a
, b
, false );
184 Node
InstantiatorTheoryUf::getRepresentative( Node a
){
186 return ((TheoryUF
*)d_th
)->d_equalityEngine
.getRepresentative( a
);
192 Node
InstantiatorTheoryUf::getInternalRepresentative( Node a
){
193 if( d_ground_reps
.find( a
)==d_ground_reps
.end() ){
197 Node rep
= getRepresentative( a
);
198 if( !rep
.hasAttribute(InstConstantAttribute()) ){
199 //return the representative of a
200 d_ground_reps
[a
] = rep
;
203 //otherwise, must search eq class
204 eq::EqClassIterator
eqc_iter( rep
, getEqualityEngine() );
206 while( !eqc_iter
.isFinished() ){
207 if( !(*eqc_iter
).hasAttribute(InstConstantAttribute()) ){
208 d_ground_reps
[ a
] = *eqc_iter
;
213 d_ground_reps
[ a
] = a
;
217 return d_ground_reps
[a
];
220 eq::EqualityEngine
* InstantiatorTheoryUf::getEqualityEngine(){
221 return &((TheoryUF
*)d_th
)->d_equalityEngine
;
224 void InstantiatorTheoryUf::getEquivalenceClass( Node a
, std::vector
< Node
>& eqc
){
226 a
= getEqualityEngine()->getRepresentative( a
);
227 eq::EqClassIterator
eqc_iter( a
, getEqualityEngine() );
228 while( !eqc_iter
.isFinished() ){
229 if( std::find( eqc
.begin(), eqc
.end(), *eqc_iter
)==eqc
.end() ){
230 eqc
.push_back( *eqc_iter
);
237 InstantiatorTheoryUf::Statistics::Statistics():
238 //d_instantiations("InstantiatorTheoryUf::Total_Instantiations", 0),
239 d_instantiations_ce_solved("InstantiatorTheoryUf::Instantiations_CE-Solved", 0),
240 d_instantiations_e_induced("InstantiatorTheoryUf::Instantiations_E-Induced", 0),
241 d_instantiations_user_pattern("InstantiatorTheoryUf::Instantiations_User_Pattern", 0),
242 d_instantiations_guess("InstantiatorTheoryUf::Instantiations_Free_Var", 0),
243 d_instantiations_auto_gen("InstantiatorTheoryUf::Instantiations_Auto_Gen", 0),
244 d_instantiations_auto_gen_min("InstantiatorTheoryUf::Instantiations_Auto_Gen_Min", 0),
245 d_splits("InstantiatorTheoryUf::Total_Splits", 0)
247 //StatisticsRegistry::registerStat(&d_instantiations);
248 StatisticsRegistry::registerStat(&d_instantiations_ce_solved
);
249 StatisticsRegistry::registerStat(&d_instantiations_e_induced
);
250 StatisticsRegistry::registerStat(&d_instantiations_user_pattern
);
251 StatisticsRegistry::registerStat(&d_instantiations_guess
);
252 StatisticsRegistry::registerStat(&d_instantiations_auto_gen
);
253 StatisticsRegistry::registerStat(&d_instantiations_auto_gen_min
);
254 StatisticsRegistry::registerStat(&d_splits
);
257 InstantiatorTheoryUf::Statistics::~Statistics(){
258 //StatisticsRegistry::unregisterStat(&d_instantiations);
259 StatisticsRegistry::unregisterStat(&d_instantiations_ce_solved
);
260 StatisticsRegistry::unregisterStat(&d_instantiations_e_induced
);
261 StatisticsRegistry::unregisterStat(&d_instantiations_user_pattern
);
262 StatisticsRegistry::unregisterStat(&d_instantiations_guess
);
263 StatisticsRegistry::unregisterStat(&d_instantiations_auto_gen
);
264 StatisticsRegistry::unregisterStat(&d_instantiations_auto_gen_min
);
265 StatisticsRegistry::unregisterStat(&d_splits
);
269 void InstantiatorTheoryUf::newEqClass( TNode n
){
270 d_quantEngine
->addTermToDatabase( n
);
273 void InstantiatorTheoryUf::newTerms(SetNode
& s
){
274 static NoMatchAttribute rewrittenNodeAttribute
;
275 /* op -> nodes (if the set is empty, the op is not interesting) */
276 std::hash_map
< TNode
, SetNode
, TNodeHashFunction
> h
;
277 /* types -> nodes (if the set is empty, the type is not interesting) */
278 std::hash_map
< TypeNode
, SetNode
, TypeNodeHashFunction
> tyh
;
279 for(SetNode::iterator i
=s
.begin(), end
=s
.end(); i
!= end
; ++i
){
280 if (i
->getAttribute(rewrittenNodeAttribute
)) continue; /* skip it */
281 if( !d_cand_gens
.empty() ){
283 TNode op
= i
->getOperator();
284 std::hash_map
< TNode
, SetNode
, TNodeHashFunction
>::iterator
287 std::pair
<std::hash_map
< TNode
, SetNode
, TNodeHashFunction
>::iterator
,bool>
288 p
= h
.insert(make_pair(op
,SetNode()));
290 if(d_cand_gens
.find(op
) != d_cand_gens
.end()){
291 is
->second
.insert(*i
);
292 } /* else we have inserted an empty set */
293 }else if(!is
->second
.empty()){
294 is
->second
.insert(*i
);
297 if( !d_cand_gen_types
.empty() ){
299 TypeNode ty
= i
->getType();
300 std::hash_map
< TypeNode
, SetNode
, TypeNodeHashFunction
>::iterator
303 std::pair
<std::hash_map
< TypeNode
, SetNode
, TypeNodeHashFunction
>::iterator
,bool>
304 p
= tyh
.insert(make_pair(ty
,SetNode()));
306 if(d_cand_gen_types
.find(ty
) != d_cand_gen_types
.end()){
307 is
->second
.insert(*i
);
308 } /* else we have inserted an empty set */
309 }else if(!is
->second
.empty()){
310 is
->second
.insert(*i
);
315 for(std::hash_map
< TNode
, SetNode
, TNodeHashFunction
>::iterator i
=h
.begin(), end
=h
.end();
317 //new term, add n to candidate generators
318 if(i
->second
.empty()) continue;
319 std::map
< Node
, NodeNewTermDispatcher
>::iterator
320 inpc
= d_cand_gens
.find(i
->first
);
321 //we know that this op exists
322 Assert(inpc
!= d_cand_gens
.end());
323 inpc
->second
.send(i
->second
);
326 for(std::hash_map
< TypeNode
, SetNode
, TypeNodeHashFunction
>::iterator i
=tyh
.begin(), end
=tyh
.end();
328 //new term, add n to candidate generators
329 if(i
->second
.empty()) continue;
330 std::map
< TypeNode
, NodeNewTermDispatcher
>::iterator
331 inpc
= d_cand_gen_types
.find(i
->first
);
332 //we know that this op exists
333 Assert(inpc
!= d_cand_gen_types
.end());
334 inpc
->second
.send(i
->second
);
341 void InstantiatorTheoryUf::merge( TNode a
, TNode b
){
342 if( options::efficientEMatching() ){
343 //merge eqc_ops of b into a
344 EqClassInfo
* eci_a
= getOrCreateEquivalenceClassInfo( a
);
345 EqClassInfo
* eci_b
= getOrCreateEquivalenceClassInfo( b
);
347 if( a
.getKind()!=IFF
&& a
.getKind()!=EQUAL
&& b
.getKind()!=IFF
&& b
.getKind()!=EQUAL
){
348 Debug("efficient-e-match") << "Merging " << a
<< " with " << b
<< std::endl
;
350 //determine new candidates for instantiation
351 computeCandidatesPcPairs( a
, eci_a
, b
, eci_b
);
352 computeCandidatesPcPairs( b
, eci_b
, a
, eci_a
);
353 computeCandidatesPpPairs( a
, eci_a
, b
, eci_b
);
354 computeCandidatesPpPairs( b
, eci_b
, a
, eci_a
);
356 computeCandidatesConstants( a
, eci_a
, b
, eci_b
);
357 computeCandidatesConstants( b
, eci_b
, a
, eci_a
);
359 eci_a
->merge( eci_b
);
363 /** assert terms are disequal */
364 void InstantiatorTheoryUf::assertDisequal( TNode a
, TNode b
, TNode reason
){
368 EqClassInfo
* InstantiatorTheoryUf::getEquivalenceClassInfo( Node n
) {
369 return d_eqc_ops
.find( n
)==d_eqc_ops
.end() ? NULL
: d_eqc_ops
[n
];
371 EqClassInfo
* InstantiatorTheoryUf::getOrCreateEquivalenceClassInfo( Node n
){
372 Assert( n
==getRepresentative( n
) );
373 if( d_eqc_ops
.find( n
)==d_eqc_ops
.end() ){
374 EqClassInfo
* eci
= new EqClassInfo( d_th
->getSatContext() );
375 eci
->setMember( n
, d_quantEngine
->getTermDatabase() );
381 void InstantiatorTheoryUf::computeCandidatesPcPairs( Node a
, EqClassInfo
* eci_a
, Node b
, EqClassInfo
* eci_b
){
382 Debug("efficient-e-match") << "Compute candidates for pc pairs..." << std::endl
;
383 Debug("efficient-e-match") << " Eq class = [";
384 outputEqClass( "efficient-e-match", a
);
385 Debug("efficient-e-match") << "]" << std::endl
;
386 outputEqClassInfo("efficient-e-match",eci_a
);
387 for( BoolMap::iterator it
= eci_a
->d_funs
.begin(); it
!= eci_a
->d_funs
.end(); it
++ ) {
388 //the child function: a member of eq_class( a ) has top symbol g, in other words g is in funs( a )
389 Node g
= (*it
).first
;
390 Debug("efficient-e-match") << " Checking application " << g
<< std::endl
;
391 //look at all parent/child pairs
392 for( std::map
< Node
, std::vector
< std::pair
< NodePcDispatcher
*, Ips
> > >::iterator itf
= d_pc_pairs
[g
].begin();
393 itf
!= d_pc_pairs
[g
].end(); ++itf
){
394 //f/g is a parent/child pair
396 if( eci_b
->hasParent( f
) ){
397 //DO_THIS: determine if f in pfuns( b ), only do the follow if so
398 Debug("efficient-e-match") << " Checking parent application " << f
<< std::endl
;
399 //scan through the list of inverted path strings/candidate generators
400 for( std::vector
< std::pair
< NodePcDispatcher
*, Ips
> >::iterator cit
= itf
->second
.begin();
401 cit
!= itf
->second
.end(); ++cit
){
403 Debug("efficient-e-match") << " Checking pattern " << cit
->first
->pat
<< std::endl
;
405 Debug("efficient-e-match") << " Check inverted path string for pattern ";
406 outputIps( "efficient-e-match", cit
->second
);
407 Debug("efficient-e-match") << std::endl
;
409 //collect all new relevant terms
412 collectTermsIps( cit
->second
, terms
);
413 if( terms
.empty() ) continue;
414 Debug("efficient-e-match") << " -> Added terms (" << terms
.size() << "): ";
415 for( SetNode::const_iterator t
=terms
.begin(), end
=terms
.end();
417 Debug("efficient-e-match") << (*t
) << " ";
419 Debug("efficient-e-match") << std::endl
;
420 //add them as candidates to the candidate generator
421 cit
->first
->send(terms
);
428 void InstantiatorTheoryUf::computeCandidatesPpPairs( Node a
, EqClassInfo
* eci_a
, Node b
, EqClassInfo
* eci_b
){
429 Debug("efficient-e-match") << "Compute candidates for pp pairs..." << std::endl
;
430 for( std::map
< Node
, std::map
< Node
, std::vector
< triple
< NodePpDispatcher
*, Ips
, Ips
> > > >::iterator it
= d_pp_pairs
.begin();
431 it
!= d_pp_pairs
.end(); ++it
){
433 if( eci_a
->hasParent( f
) ){
434 Debug("efficient-e-match") << " Checking parent application " << f
<< std::endl
;
435 for( std::map
< Node
, std::vector
< triple
<NodePpDispatcher
*, Ips
, Ips
> > >::iterator it2
= it
->second
.begin();
436 it2
!= it
->second
.end(); ++it2
){
438 if( eci_b
->hasParent( g
) ){
439 Debug("efficient-e-match") << " Checking parent application " << g
<< std::endl
;
440 //if f in pfuns( a ) and g is in pfuns( b ), only do the follow if so
441 for( std::vector
< triple
<NodePpDispatcher
*, Ips
, Ips
> > ::iterator cit
= it2
->second
.begin();
442 cit
!= it2
->second
.end(); ++cit
){
444 Debug("efficient-e-match") << " Checking pattern " << cit
->first
->pat1
<< " and " << cit
->first
->pat2
<< std::endl
;
446 Debug("efficient-e-match") << " Check inverted path string ";
447 outputIps( "efficient-e-match", cit
->second
);
450 collectTermsIps( cit
->second
, a_terms
);
451 if( a_terms
.empty() ) continue;
452 Debug("efficient-e-match") << " And check inverted path string ";
453 outputIps( "efficient-e-match", cit
->third
);
456 collectTermsIps( cit
->third
, b_terms
);
457 if( b_terms
.empty() ) continue;
459 Debug("efficient-e-match") << " -> Possibly Added termsA (" << a_terms
.size() << "): ";
460 for( SetNode::const_iterator t
=a_terms
.begin(), end
=a_terms
.end();
462 Debug("efficient-e-match") << (*t
) << " ";
464 Debug("efficient-e-match") << std::endl
;
465 Debug("efficient-e-match") << " -> Possibly Added termsB (" << b_terms
.size() << "): ";
466 for( SetNode::const_iterator t
=b_terms
.begin(), end
=b_terms
.end();
468 Debug("efficient-e-match") << (*t
) << " ";
470 Debug("efficient-e-match") << std::endl
;
473 cit
->first
->send(a_terms
,b_terms
);
482 void InstantiatorTheoryUf::computeCandidatesConstants( Node a
, EqClassInfo
* eci_a
, Node b
, EqClassInfo
* eci_b
){
483 Debug("efficient-e-match") << "Compute candidates constants for cc pairs..." << std::endl
;
484 Debug("efficient-e-match") << " Eq class = [";
485 outputEqClass( "efficient-e-match", a
);
486 Debug("efficient-e-match") << "]" << std::endl
;
487 outputEqClassInfo("efficient-e-match",eci_a
);
488 for( std::map
< Node
, std::map
< Node
, NodePcDispatcher
* > >::iterator
489 it
= d_cc_pairs
.begin(), end
= d_cc_pairs
.end();
491 Debug("efficient-e-match") << " Checking application " << it
->first
<< std::endl
;
492 if( !eci_b
->hasFunction(it
->first
) ) continue;
493 for( std::map
< Node
, NodePcDispatcher
* >::iterator
494 itc
= it
->second
.begin(), end
= it
->second
.end();
495 itc
!= end
; ++itc
) {
497 Debug("efficient-e-match") << " Checking constant " << a
<< std::endl
;
498 if(getRepresentative(itc
->first
) != a
) continue;
500 eq::EqClassIterator
eqc_iter( b
, &((TheoryUF
*)d_th
)->d_equalityEngine
);
501 while( !eqc_iter
.isFinished() ){
502 Debug("efficient-e-match-debug") << "> look at " << (*eqc_iter
)
504 if( (*eqc_iter
).hasOperator() && (*eqc_iter
).getOperator() == it
->first
) s
.insert(*eqc_iter
);
508 if( s
.empty() ) continue;
509 Debug("efficient-e-match") << " -> Added terms (" << s
.size() << "): ";
510 for( SetNode::const_iterator t
=s
.begin(), end
=s
.end();
512 Debug("efficient-e-match") << (*t
) << " ";
514 Debug("efficient-e-match") << std::endl
;
515 itc
->second
->send(s
);
520 void InstantiatorTheoryUf::collectTermsIps( Ips
& ips
, SetNode
& terms
){
521 Assert( ips
.size() > 0);
522 return collectTermsIps( ips
, terms
, ips
.size() - 1);
525 void InstantiatorTheoryUf::collectTermsIps( Ips
& ips
, SetNode
& terms
, int index
){
526 if( !terms
.empty() ){
527 Debug("efficient-e-match-debug") << "> Process " << index
<< std::endl
;
528 Node f
= ips
[index
].first
;
529 int arg
= ips
[index
].second
;
531 //for each term in terms, determine if any term (modulo equality) has parent "f" from position "arg"
532 bool addRep
= ( index
!=0 ); // We want to keep the top symbol for the last
534 for( SetNode::const_iterator t
=terms
.begin(), end
=terms
.end();
536 collectParentsTermsIps( *t
, f
, arg
, newTerms
, addRep
);
538 terms
.swap(newTerms
);
540 Debug("efficient-e-match-debug") << "> Terms are now: ";
541 for( SetNode::const_iterator t
=terms
.begin(), end
=terms
.end();
543 Debug("efficient-e-match-debug") << *t
<< " ";
545 Debug("efficient-e-match-debug") << std::endl
;
547 if(index
!=0) collectTermsIps( ips
, terms
, index
-1 );
551 bool InstantiatorTheoryUf::collectParentsTermsIps( Node n
, Node f
, int arg
, SetNode
& terms
, bool addRep
, bool modEq
){ //modEq default true
552 bool addedTerm
= false;
554 if( modEq
&& ((TheoryUF
*)d_th
)->d_equalityEngine
.hasTerm( n
)){
555 Assert( getRepresentative( n
)==n
);
556 //collect modulo equality
557 //DO_THIS: this should (if necessary) compute a current set of (f, arg) parents for n and cache it
558 eq::EqClassIterator
eqc_iter( n
, &((TheoryUF
*)d_th
)->d_equalityEngine
);
559 while( !eqc_iter
.isFinished() ){
560 Debug("efficient-e-match-debug") << "> look at " << (*eqc_iter
)
562 if( collectParentsTermsIps( (*eqc_iter
), f
, arg
, terms
, addRep
, false ) ){
563 //if only one argument, we know we can stop (since all others added will be congruent)
564 if( f
.getType().getNumChildren()==2 ){
572 quantifiers::TermDb
* db
= d_quantEngine
->getTermDatabase();
573 //see if parent f exists from argument arg
574 const std::vector
<Node
> & parents
= db
->getParents(n
,f
,arg
);
575 for( size_t i
=0; i
<parents
.size(); ++i
){
576 TNode t
= parents
[i
];
577 if(!CandidateGenerator::isLegalCandidate(t
)) continue;
578 if( addRep
) t
= getRepresentative( t
);
586 void InstantiatorTheoryUf::registerPatternElementPairs2( Node pat
, Ips
& ips
, PpIpsMap
& pp_ips_map
, NodePcDispatcher
* npc
){
587 Assert( pat
.hasOperator() );
588 //add information for possible pp-pair
589 ips
.push_back( std::pair
< Node
, int >( pat
.getOperator(), 0 ) ); //0 is just a dumb value
591 for( int i
=0; i
<(int)pat
.getNumChildren(); i
++ ){
592 if( pat
[i
].getKind()==INST_CONSTANT
){
593 ips
.back().second
= i
;
594 pp_ips_map
[ pat
[i
] ].push_back( make_pair( pat
.getOperator(), Ips( ips
) ) );
598 for( int i
=0; i
<(int)pat
.getNumChildren(); i
++ ){
599 if( pat
[i
].getKind()==APPLY_UF
){
600 ips
.back().second
= i
;
601 registerPatternElementPairs2( pat
[i
], ips
, pp_ips_map
, npc
);
602 Debug("pattern-element-opt") << "Found pc-pair ( " << pat
.getOperator() << ", " << pat
[i
].getOperator() << " )" << std::endl
;
603 Debug("pattern-element-opt") << " Path = ";
604 outputIps( "pattern-element-opt", ips
);
605 Debug("pattern-element-opt") << std::endl
;
606 //pat.getOperator() and pat[i].getOperator() are a pc-pair
607 d_pc_pairs
[ pat
[i
].getOperator() ][ pat
.getOperator() ]
608 .push_back( make_pair(npc
,Ips(ips
)) );
614 void InstantiatorTheoryUf::registerPatternElementPairs( Node pat
, PpIpsMap
& pp_ips_map
,
615 NodePcDispatcher
* npc
,
616 NodePpDispatcher
* npp
){
618 registerPatternElementPairs2( pat
, ips
, pp_ips_map
, npc
);
619 for( PpIpsMap::iterator it
= pp_ips_map
.begin(); it
!= pp_ips_map
.end(); ++it
){
620 // for each variable construct all the pp-pair
621 for( size_t j
=0; j
<it
->second
.size(); j
++ ){
622 for( size_t k
=j
+1; k
<it
->second
.size(); k
++ ){
624 Debug("pattern-element-opt") << "Found pp-pair ( " << it
->second
[j
].first
<< ", " << it
->second
[k
].first
<< " )" << std::endl
;
625 Debug("pattern-element-opt") << " Paths = ";
626 outputIps( "pattern-element-opt", it
->second
[j
].second
);
627 Debug("pattern-element-opt") << " and ";
628 outputIps( "pattern-element-opt", it
->second
[k
].second
);
629 Debug("pattern-element-opt") << std::endl
;
630 d_pp_pairs
[ it
->second
[j
].first
][ it
->second
[k
].first
]
631 .push_back( make_triple( npp
, it
->second
[j
].second
, it
->second
[k
].second
));
637 void findPpSite(Node pat
, InstantiatorTheoryUf::Ips
& ips
, InstantiatorTheoryUf::PpIpsMap
& pp_ips_map
){
638 Assert( pat
.getKind()==APPLY_UF
);
639 //add information for possible pp-pair
641 ips
.push_back( make_pair( pat
.getOperator(), 0) );
642 for( size_t i
=0; i
<pat
.getNumChildren(); i
++ ){
643 if( pat
[i
].getKind()==INST_CONSTANT
){
644 ips
.back().second
= i
;
645 pp_ips_map
[ pat
[i
] ].push_back( make_pair( pat
.getOperator(), InstantiatorTheoryUf::Ips( ips
) ) );
649 for( size_t i
=0; i
<pat
.getNumChildren(); i
++ ){
650 if( pat
[i
].getKind()==APPLY_UF
){
651 ips
.back().second
= i
;
652 findPpSite( pat
[i
], ips
, pp_ips_map
);
658 void InstantiatorTheoryUf::combineMultiPpIpsMap(PpIpsMap
& pp_ips_map
, MultiPpIpsMap
& multi_pp_ips_map
,
659 EfficientHandler
& eh
, size_t index2
,const std::vector
<Node
> & pats
){
660 hash_map
<size_t,NodePpDispatcher
*> npps
;
661 for( PpIpsMap::iterator it
= pp_ips_map
.begin(); it
!= pp_ips_map
.end(); ++it
){
662 MultiPpIpsMap::iterator mit
= multi_pp_ips_map
.find(it
->first
);
663 if(mit
== multi_pp_ips_map
.end()) continue;
664 // for each variable construct all the pp-pair
665 // j the last pattern treated
666 for( std::vector
< std::pair
< Node
, Ips
> >::iterator j
=it
->second
.begin(), jend
= it
->second
.end() ;
668 // k one of the previous one
669 for( std::vector
< triple
< size_t, Node
, Ips
> >::iterator k
=mit
->second
.begin(), kend
= mit
->second
.end() ;
672 Debug("pattern-element-opt") << "Found multi-pp-pair ( " << j
->first
673 << ", " << k
->second
<< " in "<< k
->first
674 << " )" << std::endl
;
675 Debug("pattern-element-opt") << " Paths = ";
676 outputIps( "pattern-element-opt", j
->second
);
677 Debug("pattern-element-opt") << " and ";
678 outputIps( "pattern-element-opt", k
->third
);
679 Debug("pattern-element-opt") << std::endl
;
680 NodePpDispatcher
* dispatcher
;
681 hash_map
<size_t,NodePpDispatcher
*>::iterator inpp
= npps
.find(k
->first
);
682 if( inpp
!= npps
.end() ) dispatcher
= inpp
->second
;
684 dispatcher
= new NodePpDispatcher();
686 dispatcher
->pat1
= pats
[index2
];
687 dispatcher
->pat2
= pats
[k
->first
];
689 dispatcher
->addPpDispatcher(&eh
,index2
,k
->first
);
691 d_pp_pairs
[ j
->first
][ k
->second
].push_back( make_triple( dispatcher
, j
->second
, k
->third
));
696 /** Put pp_ips_map to multi_pp_ips_map */
697 for( PpIpsMap::iterator it
= pp_ips_map
.begin(); it
!= pp_ips_map
.end(); ++it
){
698 for( std::vector
< std::pair
< Node
, Ips
> >::iterator j
=it
->second
.begin(), jend
= it
->second
.end() ;
700 multi_pp_ips_map
[it
->first
].push_back(make_triple(index2
, j
->first
, j
->second
));
707 void InstantiatorTheoryUf::registerEfficientHandler( EfficientHandler
& handler
,
708 const std::vector
< Node
> & pats
){
709 Assert(pats
.size() > 0);
711 MultiPpIpsMap multi_pp_ips_map
;
713 //In a multi-pattern Pattern that is only a variable are specials,
714 //if the variable appears in another pattern, it can be discarded.
715 //Otherwise new term of this term can be candidate. So we stock them
716 //here before adding them.
717 std::vector
< size_t > patVars
;
719 Debug("pattern-element-opt") << "Register patterns" << pats
<< std::endl
;
720 for(size_t i
= 0; i
< pats
.size(); ++i
){
721 if( pats
[i
].getKind() == kind::INST_CONSTANT
){
722 patVars
.push_back(i
);
726 if( pats
[i
].getKind() == kind::NOT
&& pats
[i
][0].getKind() == kind::EQUAL
){
727 Node cst
= NodeManager::currentNM()->mkConst
<bool>(false);
728 TNode op
= pats
[i
][0].getOperator();
729 if(d_cc_pairs
[op
][cst
] == NULL
){
730 d_cc_pairs
[op
][cst
] = new NodePcDispatcher();
732 d_cc_pairs
[op
][cst
]->addPcDispatcher(&handler
,i
);
736 Debug("pattern-element-opt") << " Register candidate generator..." << pats
[i
] << std::endl
;
737 /* Has the pattern already been seen */
738 if( d_pat_cand_gens
.find( pats
[i
] )==d_pat_cand_gens
.end() ){
739 NodePcDispatcher
* npc
= new NodePcDispatcher();
740 NodePpDispatcher
* npp
= new NodePpDispatcher();
746 d_pat_cand_gens
[pats
[i
]] = make_pair(npc
,npp
);
747 registerPatternElementPairs( pats
[i
], pp_ips_map
, npc
, npp
);
750 findPpSite(pats
[i
],ips
,pp_ips_map
);
752 //Has the top operator already been seen */
753 TNode op
= pats
[i
].getOperator();
754 d_pat_cand_gens
[pats
[i
]].first
->addPcDispatcher(&handler
,i
);
755 d_pat_cand_gens
[pats
[i
]].second
->addPpDispatcher(&handler
,i
,i
);
756 d_cand_gens
[op
].addNewTermDispatcher(&handler
,i
);
758 combineMultiPpIpsMap(pp_ips_map
,multi_pp_ips_map
,handler
,i
,pats
);
763 for(size_t i
= 0; i
< patVars
.size(); ++i
){
764 TNode var
= pats
[patVars
[i
]];
765 Assert( var
.getKind() == kind::INST_CONSTANT
);
766 if( multi_pp_ips_map
.find(var
) != multi_pp_ips_map
.end() ){
767 //The variable appear in another pattern, skip it
770 d_cand_gen_types
[var
.getType()].addNewTermDispatcher(&handler
,patVars
[i
]);
773 //take all terms from the uf term db and add to candidate generator
774 if( pats
[0].getKind() == kind::INST_CONSTANT
){
775 TypeNode ty
= pats
[0].getType();
776 rrinst::CandidateGenerator
* cg
= d_quantEngine
->getRRCanGenClasses(ty
);
777 cg
->reset(Node::null());
780 while( !(c
= cg
->getNextCandidate()).isNull() ){
781 if( c
.getType() == ty
) ele
.insert(c
);
784 // for(std::vector<Node>::iterator i = db->d_op_map[op].begin(), end = db->d_op_map[op].end(); i != end; ++i){
785 // if(CandidateGenerator::isLegalCandidate(*i)) ele.insert(*i);
787 if(Debug
.isOn("efficient-e-match-stats")){
788 Debug("efficient-e-match-stats") << "pattern " << pats
<< " initialized with " << ele
.size() << " terms"<< std::endl
;
790 handler
.addMonoCandidate(ele
, 0);
793 } else if( pats
[0].getKind() == kind::NOT
&& pats
[0][0].getKind() == kind::EQUAL
){
794 Node cst
= NodeManager::currentNM()->mkConst
<bool>(false);
795 TNode op
= pats
[0][0].getOperator();
796 cst
= getRepresentative(cst
);
798 eq::EqClassIterator
eqc_iter( cst
, &((TheoryUF
*)d_th
)->d_equalityEngine
);
799 while( !eqc_iter
.isFinished() ){
800 Debug("efficient-e-match-debug") << "> look at " << (*eqc_iter
)
802 if( (*eqc_iter
).hasOperator() && (*eqc_iter
).getOperator() == op
) ele
.insert(*eqc_iter
);
806 if(Debug
.isOn("efficient-e-match-stats")){
807 Debug("efficient-e-match-stats") << "pattern " << pats
<< " initialized with " << ele
.size() << " terms"<< std::endl
;
809 handler
.addMonoCandidate(ele
, 0);
813 Node op
= pats
[0].getOperator();
814 TermDb
* db
= d_quantEngine
->getTermDatabase();
815 if(db
->d_op_map
[op
].begin() != db
->d_op_map
[op
].end()){
817 // for(std::vector<Node>::iterator i = db->d_op_map[op].begin(), end = db->d_op_map[op].end(); i != end; ++i){
818 // if(CandidateGenerator::isLegalCandidate(*i)) ele.insert(*i);
820 ele
.insert(db
->d_op_map
[op
].begin(), db
->d_op_map
[op
].end());
821 if(Debug
.isOn("efficient-e-match-stats")){
822 Debug("efficient-e-match-stats") << "pattern " << pats
<< " initialized with " << ele
.size() << " terms"<< std::endl
;
824 handler
.addMonoCandidate(ele
, 0);
827 Debug("efficient-e-match") << "Done." << std::endl
;
830 void InstantiatorTheoryUf::registerTrigger( theory::inst::Trigger
* tr
, Node op
){
831 if( std::find( d_op_triggers
[op
].begin(), d_op_triggers
[op
].end(), tr
)==d_op_triggers
[op
].end() ){
832 d_op_triggers
[op
].push_back( tr
);
836 void InstantiatorTheoryUf::outputEqClass( const char* c
, Node n
){
837 if( ((TheoryUF
*)d_th
)->d_equalityEngine
.hasTerm( n
) ){
838 eq::EqClassIterator
eqc_iter( getRepresentative( n
),
839 &((TheoryUF
*)d_th
)->d_equalityEngine
);
840 bool firstTime
= true;
841 while( !eqc_iter
.isFinished() ){
842 if( !firstTime
){ Debug(c
) << ", "; }
843 Debug(c
) << (*eqc_iter
);
852 void InstantiatorTheoryUf::outputIps( const char* c
, Ips
& ips
){
853 for( int i
=0; i
<(int)ips
.size(); i
++ ){
854 if( i
>0 ){ Debug( c
) << "."; }
855 Debug( c
) << ips
[i
].first
<< "." << ips
[i
].second
;
859 rrinst::CandidateGenerator
* InstantiatorTheoryUf::getRRCanGenClasses(){
860 uf::TheoryUF
* uf
= static_cast<uf::TheoryUF
*>(getTheory());
861 eq::EqualityEngine
* ee
=
862 static_cast<eq::EqualityEngine
*>(uf
->getEqualityEngine());
863 return new eq::rrinst::CandidateGeneratorTheoryEeClasses(ee
);
866 rrinst::CandidateGenerator
* InstantiatorTheoryUf::getRRCanGenClass(){
867 uf::TheoryUF
* uf
= static_cast<uf::TheoryUF
*>(getTheory());
868 eq::EqualityEngine
* ee
=
869 static_cast<eq::EqualityEngine
*>(uf
->getEqualityEngine());
870 return new eq::rrinst::CandidateGeneratorTheoryEeClass(ee
);
875 } /* namespace theory */
876 } /* namespace cvc4 */