src/theory/uf/theory_uf_instantiator.cpp

   1 /*********************                                                        */
   2 /*! \file theory_uf_instantiator.cpp
   3  ** \verbatim
   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
  13  **
  14  ** \brief Implementation of theory uf instantiator class
  15  **/
  16
  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"
  25
  26 using namespace std;
  27 using namespace CVC4;
  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;
  33
  34 namespace CVC4 {
  35 namespace theory {
  36 namespace uf {
  37
  38 inline std::ostream& operator<<(std::ostream& out, const InstantiatorTheoryUf::Ips& ips) {
  39   return out;
  40 };
  41
  42 EqClassInfo::EqClassInfo( context::Context* c ) : d_funs( c ), d_pfuns( c ), d_disequal( c ){
  43
  44 }
  45
  46 //set member
  47 void EqClassInfo::setMember( Node n, quantifiers::TermDb* db ){
  48   if( n.hasOperator() ){
  49     d_funs.insertAtContextLevelZero(n.getOperator(),true);
  50   }
  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);
  57   }
  58 }
  59
  60 //get has function
  61 bool EqClassInfo::hasFunction( Node op ){
  62   return d_funs.find( op )!=d_funs.end();
  63 }
  64
  65 bool EqClassInfo::hasParent( Node op ){
  66   return d_pfuns.find( op )!=d_pfuns.end();
  67 }
  68
  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;
  73   }
  74   for( BoolMap::iterator it = eci->d_pfuns.begin(); it != eci->d_pfuns.end(); it++ ) {
  75     d_pfuns[ (*it).first ] = true;
  76   }
  77 }
  78
  79 inline void outputEqClassInfo( const char* c, const EqClassInfo* eci){
  80   Debug(c) << " funs:";
  81   for( EqClassInfo::BoolMap::iterator it = eci->d_funs.begin(); it != eci->d_funs.end(); it++ ) {
  82     Debug(c) << (*it).first << ",";
  83   }
  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 << ",";
  87   }
  88   Debug(c) << std::endl;
  89 }
  90
  91
  92
  93 InstantiatorTheoryUf::InstantiatorTheoryUf(context::Context* c, CVC4::theory::QuantifiersEngine* qe, Theory* th) :
  94 Instantiator( c, qe, th )
  95 {
  96   if( !options::finiteModelFind() || options::fmfInstEngine() ){
  97     if( options::cbqi() ){
  98       addInstStrategy( new InstStrategyCheckCESolved( this, qe ) );
  99     }
 100     if( options::userPatternsQuant() ){
 101       d_isup = new InstStrategyUserPatterns( this, qe );
 102       addInstStrategy( d_isup );
 103     }else{
 104       d_isup = NULL;
 105     }
 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 ) );
 113     }
 114     //d_isup->setPriorityOver( i_ag );
 115     //d_isup->setPriorityOver( i_agm );
 116     //i_ag->setPriorityOver( i_agm );
 117   }
 118 }
 119
 120 void InstantiatorTheoryUf::preRegisterTerm( Node t ){
 121   //d_quantEngine->addTermToDatabase( t );
 122 }
 123
 124 void InstantiatorTheoryUf::assertNode( Node assertion )
 125 {
 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()) );
 134     }
 135   }
 136 }
 137
 138 void InstantiatorTheoryUf::addUserPattern( Node f, Node pat ){
 139   if( d_isup ){
 140     d_isup->addUserPattern( f, pat );
 141   }
 142   setHasConstraintsFrom( f );
 143 }
 144
 145
 146 void InstantiatorTheoryUf::processResetInstantiationRound( Theory::Effort effort ){
 147   d_ground_reps.clear();
 148 }
 149
 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;
 153 }
 154
 155 void InstantiatorTheoryUf::debugPrint( const char* c )
 156 {
 157
 158 }
 159
 160 bool InstantiatorTheoryUf::hasTerm( Node a ){
 161   return ((TheoryUF*)d_th)->d_equalityEngine.hasTerm( a );
 162 }
 163
 164 bool InstantiatorTheoryUf::areEqual( Node a, Node b ){
 165   if( a==b ){
 166     return true;
 167   }else if( hasTerm( a ) && hasTerm( b ) ){
 168     return ((TheoryUF*)d_th)->d_equalityEngine.areEqual( a, b );
 169   }else{
 170     return false;
 171   }
 172 }
 173
 174 bool InstantiatorTheoryUf::areDisequal( Node a, Node b ){
 175   if( a==b ){
 176     return false;
 177   }else if( hasTerm( a ) && hasTerm( b ) ){
 178     return ((TheoryUF*)d_th)->d_equalityEngine.areDisequal( a, b, false );
 179   }else{
 180     return false;
 181   }
 182 }
 183
 184 Node InstantiatorTheoryUf::getRepresentative( Node a ){
 185   if( hasTerm( a ) ){
 186     return ((TheoryUF*)d_th)->d_equalityEngine.getRepresentative( a );
 187   }else{
 188     return a;
 189   }
 190 }
 191
 192 Node InstantiatorTheoryUf::getInternalRepresentative( Node a ){
 193   if( d_ground_reps.find( a )==d_ground_reps.end() ){
 194     if( !hasTerm( a ) ){
 195       return a;
 196     }else{
 197       Node rep = getRepresentative( a );
 198       if( !rep.hasAttribute(InstConstantAttribute()) ){
 199         //return the representative of a
 200         d_ground_reps[a] = rep;
 201         return rep;
 202       }else{
 203         //otherwise, must search eq class
 204         eq::EqClassIterator eqc_iter( rep, getEqualityEngine() );
 205         rep = Node::null();
 206         while( !eqc_iter.isFinished() ){
 207           if( !(*eqc_iter).hasAttribute(InstConstantAttribute()) ){
 208             d_ground_reps[ a ] = *eqc_iter;
 209             return *eqc_iter;
 210           }
 211           eqc_iter++;
 212         }
 213         d_ground_reps[ a ] = a;
 214       }
 215     }
 216   }
 217   return d_ground_reps[a];
 218 }
 219
 220 eq::EqualityEngine* InstantiatorTheoryUf::getEqualityEngine(){
 221   return &((TheoryUF*)d_th)->d_equalityEngine;
 222 }
 223
 224 void InstantiatorTheoryUf::getEquivalenceClass( Node a, std::vector< Node >& eqc ){
 225   if( hasTerm( a ) ){
 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 );
 231       }
 232       eqc_iter++;
 233     }
 234   }
 235 }
 236
 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)
 246 {
 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);
 255 }
 256
 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);
 266 }
 267
 268 /** new node */
 269 void InstantiatorTheoryUf::newEqClass( TNode n ){
 270   d_quantEngine->addTermToDatabase( n );
 271 }
 272
 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() ){
 282       // op
 283       TNode op = i->getOperator();
 284       std::hash_map< TNode, SetNode, TNodeHashFunction >::iterator
 285         is = h.find(op);
 286       if(is == h.end()){
 287         std::pair<std::hash_map< TNode, SetNode, TNodeHashFunction >::iterator,bool>
 288           p = h.insert(make_pair(op,SetNode()));
 289         is = p.first;
 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);
 295       }
 296     }
 297     if( !d_cand_gen_types.empty() ){
 298       //type
 299       TypeNode ty = i->getType();
 300       std::hash_map< TypeNode, SetNode, TypeNodeHashFunction >::iterator
 301         is = tyh.find(ty);
 302       if(is == tyh.end()){
 303         std::pair<std::hash_map< TypeNode, SetNode, TypeNodeHashFunction >::iterator,bool>
 304           p = tyh.insert(make_pair(ty,SetNode()));
 305         is = p.first;
 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);
 311       }
 312     }
 313   }
 314   //op
 315   for(std::hash_map< TNode, SetNode, TNodeHashFunction >::iterator i=h.begin(), end=h.end();
 316       i != end; ++i){
 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);
 324   }
 325   //type
 326   for(std::hash_map< TypeNode, SetNode, TypeNodeHashFunction >::iterator i=tyh.begin(), end=tyh.end();
 327       i != end; ++i){
 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);
 335   }
 336
 337 }
 338
 339
 340 /** merge */
 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 );
 346
 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;
 349
 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 );
 355     }
 356     computeCandidatesConstants( a, eci_a, b, eci_b);
 357     computeCandidatesConstants( b, eci_b, a, eci_a);
 358
 359     eci_a->merge( eci_b );
 360   }
 361 }
 362
 363 /** assert terms are disequal */
 364 void InstantiatorTheoryUf::assertDisequal( TNode a, TNode b, TNode reason ){
 365
 366 }
 367
 368 EqClassInfo* InstantiatorTheoryUf::getEquivalenceClassInfo( Node n ) {
 369   return d_eqc_ops.find( n )==d_eqc_ops.end() ? NULL : d_eqc_ops[n];
 370 }
 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() );
 376     d_eqc_ops[n] = eci;
 377   }
 378   return d_eqc_ops[n];
 379 }
 380
 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
 395       Node f = itf->first;
 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 ){
 402 #ifdef CVC4_DEBUG
 403           Debug("efficient-e-match") << "      Checking pattern " << cit->first->pat << std::endl;
 404 #endif
 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;
 408
 409           //collect all new relevant terms
 410           SetNode terms;
 411           terms.insert( b );
 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();
 416                t!=end; ++t ){
 417             Debug("efficient-e-match") << (*t) << " ";
 418           }
 419           Debug("efficient-e-match") << std::endl;
 420           //add them as candidates to the candidate generator
 421           cit->first->send(terms);
 422         }
 423       }
 424     }
 425   }
 426 }
 427
 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 ){
 432     Node f = it->first;
 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 ){
 437         Node g = it2->first;
 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 ){
 443 #ifdef CVC4_DEBUG
 444             Debug("efficient-e-match") << "    Checking pattern " << cit->first->pat1 << " and " << cit->first->pat2 << std::endl;
 445 #endif
 446             Debug("efficient-e-match") << "          Check inverted path string ";
 447             outputIps( "efficient-e-match", cit->second );
 448             SetNode a_terms;
 449             a_terms.insert( a );
 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 );
 454             SetNode b_terms;
 455             b_terms.insert( b );
 456             collectTermsIps( cit->third, b_terms );
 457             if( b_terms.empty() ) continue;
 458             //Start debug
 459             Debug("efficient-e-match") << "        -> Possibly Added termsA (" << a_terms.size() << "): ";
 460             for( SetNode::const_iterator t=a_terms.begin(), end=a_terms.end();
 461                  t!=end; ++t ){
 462               Debug("efficient-e-match") << (*t) << " ";
 463             }
 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();
 467                  t!=end; ++t ){
 468               Debug("efficient-e-match") << (*t) << " ";
 469             }
 470             Debug("efficient-e-match") << std::endl;
 471             //End debug
 472
 473             cit->first->send(a_terms,b_terms);
 474           }
 475         }
 476       }
 477     }
 478   }
 479 }
 480
 481
 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();
 490        it != end; ++it ) {
 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 ) {
 496       //The constant
 497       Debug("efficient-e-match") << "    Checking constant " << a << std::endl;
 498       if(getRepresentative(itc->first) != a) continue;
 499       SetNode s;
 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)
 503                                          << std::endl;
 504         if( (*eqc_iter).hasOperator() && (*eqc_iter).getOperator() == it->first ) s.insert(*eqc_iter);
 505         eqc_iter++;
 506       }
 507
 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();
 511            t!=end; ++t ){
 512         Debug("efficient-e-match") << (*t) << " ";
 513       }
 514       Debug("efficient-e-match") << std::endl;
 515       itc->second->send(s);
 516     }
 517   }
 518 }
 519
 520 void InstantiatorTheoryUf::collectTermsIps( Ips& ips, SetNode & terms ){
 521   Assert( ips.size() > 0);
 522   return collectTermsIps( ips, terms,  ips.size() - 1);
 523 }
 524
 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;
 530
 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
 533     SetNode newTerms;
 534     for( SetNode::const_iterator t=terms.begin(), end=terms.end();
 535          t!=end; ++t ){
 536       collectParentsTermsIps( *t, f, arg, newTerms, addRep );
 537     }
 538     terms.swap(newTerms);
 539
 540     Debug("efficient-e-match-debug") << "> Terms are now: ";
 541     for( SetNode::const_iterator t=terms.begin(), end=terms.end();
 542          t!=end; ++t ){
 543       Debug("efficient-e-match-debug") << *t << " ";
 544     }
 545     Debug("efficient-e-match-debug") << std::endl;
 546
 547     if(index!=0) collectTermsIps( ips, terms, index-1 );
 548   }
 549 }
 550
 551 bool InstantiatorTheoryUf::collectParentsTermsIps( Node n, Node f, int arg, SetNode & terms, bool addRep, bool modEq ){ //modEq default true
 552   bool addedTerm = false;
 553
 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)
 561                                        << std::endl;
 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 ){
 565           return true;
 566         }
 567         addedTerm = true;
 568       }
 569       eqc_iter++;
 570     }
 571   }else{
 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 );
 579       terms.insert(t);
 580       addedTerm = true;
 581     }
 582   }
 583   return addedTerm;
 584 }
 585
 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
 590
 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 ) ) );
 595     }
 596   }
 597
 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)) );
 609     }
 610   }
 611   ips.pop_back();
 612 }
 613
 614 void InstantiatorTheoryUf::registerPatternElementPairs( Node pat, PpIpsMap & pp_ips_map,
 615                                                         NodePcDispatcher* npc,
 616                                                         NodePpDispatcher* npp){
 617   Ips ips;
 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++ ){
 623         //found a pp-pair
 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 ));
 632       }
 633     }
 634   }
 635 };
 636
 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
 640
 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 ) ) );
 646     }
 647   }
 648
 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 );
 653     }
 654   }
 655   ips.pop_back();
 656 }
 657
 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() ;
 667          j != jend; ++j){
 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() ;
 670            k != kend; ++k){
 671         //found a pp-pair
 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;
 683         else{
 684           dispatcher = new NodePpDispatcher();
 685 #ifdef CVC4_DEBUG
 686           dispatcher->pat1 = pats[index2];
 687           dispatcher->pat2 = pats[k->first];
 688 #endif
 689           dispatcher->addPpDispatcher(&eh,index2,k->first);
 690         };
 691         d_pp_pairs[ j->first ][ k->second ].push_back( make_triple( dispatcher, j->second, k->third ));
 692       }
 693     }
 694   }
 695
 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() ;
 699          j != jend; ++j){
 700       multi_pp_ips_map[it->first].push_back(make_triple(index2, j->first, j->second));
 701     }
 702   }
 703
 704 }
 705
 706
 707 void InstantiatorTheoryUf::registerEfficientHandler( EfficientHandler& handler,
 708                                                      const std::vector< Node > & pats ){
 709   Assert(pats.size() > 0);
 710
 711   MultiPpIpsMap multi_pp_ips_map;
 712   PpIpsMap 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;
 718
 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);
 723       continue;
 724     }
 725     //to complete
 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();
 731       }
 732       d_cc_pairs[op][cst]->addPcDispatcher(&handler,i);
 733       continue;
 734     }
 735     //end to complete
 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();
 741 #ifdef CVC4_DEBUG
 742       npc->pat = pats[i];
 743       npp->pat1 = pats[i];
 744       npp->pat2 = pats[i];
 745 #endif
 746       d_pat_cand_gens[pats[i]] = make_pair(npc,npp);
 747       registerPatternElementPairs( pats[i], pp_ips_map, npc, npp );
 748     }else{
 749       Ips ips;
 750       findPpSite(pats[i],ips,pp_ips_map);
 751     }
 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);
 757
 758     combineMultiPpIpsMap(pp_ips_map,multi_pp_ips_map,handler,i,pats);
 759
 760     pp_ips_map.clear();
 761   }
 762
 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
 768       continue;
 769     };
 770     d_cand_gen_types[var.getType()].addNewTermDispatcher(&handler,patVars[i]);
 771   }
 772
 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());
 778     TNode c;
 779     SetNode ele;
 780     while( !(c = cg->getNextCandidate()).isNull() ){
 781       if( c.getType() == ty ) ele.insert(c);
 782     }
 783     if( !ele.empty() ){
 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);
 786       // }
 787       if(Debug.isOn("efficient-e-match-stats")){
 788         Debug("efficient-e-match-stats") << "pattern " << pats << " initialized with " << ele.size() << " terms"<< std::endl;
 789       }
 790       handler.addMonoCandidate(ele, 0);
 791     }
 792
 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);
 797     SetNode ele;
 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)
 801                                        << std::endl;
 802       if( (*eqc_iter).hasOperator() && (*eqc_iter).getOperator() == op ) ele.insert(*eqc_iter);
 803       eqc_iter++;
 804     }
 805     if( !ele.empty() ){
 806       if(Debug.isOn("efficient-e-match-stats")){
 807         Debug("efficient-e-match-stats") << "pattern " << pats << " initialized with " << ele.size() << " terms"<< std::endl;
 808       }
 809       handler.addMonoCandidate(ele, 0);
 810     }
 811
 812   } else {
 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()){
 816       SetNode ele;
 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);
 819       // }
 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;
 823       }
 824       handler.addMonoCandidate(ele, 0);
 825     }
 826   }
 827   Debug("efficient-e-match") << "Done." << std::endl;
 828 }
 829
 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 );
 833   }
 834 }
 835
 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);
 844       firstTime = false;
 845       eqc_iter++;
 846     }
 847   }else{
 848     Debug(c) << n;
 849   }
 850 }
 851
 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;
 856   }
 857 }
 858
 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);
 864 }
 865
 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);
 871 }
 872
 873
 874 } /* namespace uf */
 875 } /* namespace theory */
 876 } /* namespace cvc4 */