src/theory/rr_inst_match.cpp

   1 /*********************                                                        */
   2 /*! \file rr_inst_match.cpp
   3  ** \verbatim
   4  ** Original author: ajreynol
   5  ** Major contributors: bobot
   6  ** Minor contributors (to current version): mdeters
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009-2012  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 inst match class
  15  **/
  16
  17 #include "theory/inst_match.h"
  18 #include "theory/theory_engine.h"
  19 #include "theory/quantifiers_engine.h"
  20 #include "theory/uf/theory_uf_instantiator.h"
  21 #include "theory/uf/equality_engine.h"
  22 #include "theory/arrays/theory_arrays.h"
  23 #include "theory/datatypes/theory_datatypes.h"
  24 #include "theory/rr_inst_match.h"
  25 #include "theory/rr_trigger.h"
  26 #include "theory/rr_inst_match_impl.h"
  27 #include "theory/rr_candidate_generator.h"
  28
  29 using namespace CVC4;
  30 using namespace CVC4::kind;
  31 using namespace CVC4::context;
  32 using namespace CVC4::theory;
  33 using namespace CVC4::theory::rrinst;
  34 using namespace CVC4::theory::uf::rrinst;
  35 using namespace CVC4::theory::eq::rrinst;
  36
  37 namespace CVC4{
  38 namespace theory{
  39 namespace rrinst{
  40
  41 typedef CVC4::theory::inst::InstMatch InstMatch;
  42 typedef CVC4::theory::inst::CandidateGeneratorQueue CandidateGeneratorQueue;
  43
  44 template<bool modEq>
  45 class InstMatchTrie2Pairs
  46 {
  47   typename std::vector< std::vector < typename InstMatchTrie2Gen<modEq>::Tree > > d_data;
  48   InstMatchTrie2Gen<modEq> d_backtrack;
  49 public:
  50   InstMatchTrie2Pairs(context::Context* c,  QuantifiersEngine* q, size_t n):
  51   d_backtrack(c,q) {
  52     // resize to a triangle
  53     //
  54     // |     *
  55     // |   * *
  56     // | * * *
  57     // | -----> i
  58     d_data.resize(n);
  59     for(size_t i=0; i < n; ++i){
  60       d_data[i].resize(i+1,typename InstMatchTrie2Gen<modEq>::Tree(0));
  61     }
  62   };
  63   InstMatchTrie2Pairs(const InstMatchTrie2Pairs &) CVC4_UNDEFINED;
  64   const InstMatchTrie2Pairs & operator =(const InstMatchTrie2Pairs & e) CVC4_UNDEFINED;
  65   /** add match m in the trie,
  66       return true if it was never seen */
  67   inline bool addInstMatch( size_t i, size_t j, InstMatch& m){
  68     size_t k = std::min(i,j);
  69     size_t l = std::max(i,j);
  70     return d_backtrack.addInstMatch(m,&(d_data[l][k]));
  71   };
  72   inline bool addInstMatch( size_t i, InstMatch& m){
  73     return d_backtrack.addInstMatch(m,&(d_data[i][i]));
  74   };
  75
  76 };
  77
  78
  79 // Currently the implementation doesn't take into account that
  80 // variable should have the same value given.
  81 // TODO use the d_children way perhaps
  82 // TODO replace by a real dictionnary
  83 // We should create a real substitution? slower more precise
  84 // We don't do that often
  85 bool nonunifiable( TNode t0, TNode pat, const std::vector<Node> & vars){
  86   if(pat.isNull()) return true;
  87
  88   typedef std::vector<std::pair<TNode,TNode> > tstack;
  89   tstack stack(1,std::make_pair(t0,pat)); // t * pat
  90
  91   while(!stack.empty()){
  92     const std::pair<TNode,TNode> p = stack.back(); stack.pop_back();
  93     const TNode & t = p.first;
  94     const TNode & pat = p.second;
  95
  96     // t or pat is a variable currently we consider that can match anything
  97     if( find(vars.begin(),vars.end(),t) != vars.end() ) continue;
  98     if( pat.getKind() == INST_CONSTANT ) continue;
  99
 100     // t and pat are nonunifiable
 101     if( !Trigger::isAtomicTrigger( t ) || !Trigger::isAtomicTrigger( pat ) ) {
 102       if(t == pat) continue;
 103       else return true;
 104     };
 105     if( t.getOperator() != pat.getOperator() ) return true;
 106
 107     //put the children on the stack
 108     for( size_t i=0; i < pat.getNumChildren(); i++ ){
 109       stack.push_back(std::make_pair(t[i],pat[i]));
 110     };
 111   }
 112   // The heuristic can't find non-unifiability
 113   return false;
 114 };
 115
 116 /** New things */
 117 class DumbMatcher: public Matcher{
 118   void resetInstantiationRound( QuantifiersEngine* qe ){};
 119   bool reset( TNode n, InstMatch& m, QuantifiersEngine* qe ){
 120     return false;
 121   }
 122   bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){
 123     return false;
 124   }
 125 };
 126
 127 class DumbPatMatcher: public PatMatcher{
 128   void resetInstantiationRound( QuantifiersEngine* qe ){};
 129   bool reset( InstMatch& m, QuantifiersEngine* qe ){
 130     return false;
 131   }
 132   bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){
 133     return false;
 134   }
 135 };
 136
 137
 138 /* The order of the matching is:
 139    reset arg1, nextMatch arg1, reset arg2, nextMatch arg2, ... */
 140 ApplyMatcher::ApplyMatcher( Node pat, QuantifiersEngine* qe): d_pattern(pat){
 141   //  Assert( pat.hasAttribute(InstConstantAttribute()) );
 142
 143   //set-up d_variables, d_constants, d_childrens
 144   for( size_t i=0; i< d_pattern.getNumChildren(); ++i ){
 145     EqualityQuery* q = qe->getEqualityQuery(d_pattern[i].getType());
 146     Assert( q != NULL );
 147     if( d_pattern[i].hasAttribute(InstConstantAttribute()) ){
 148       if( d_pattern[i].getKind()==INST_CONSTANT ){
 149         //It's a variable
 150         d_variables.push_back(make_triple((TNode)d_pattern[i],i,q));
 151       }else{
 152         //It's neither a constant argument neither a variable
 153         //we create the matcher for the subpattern
 154         d_childrens.push_back(make_triple(mkMatcher((TNode)d_pattern[i], qe),i,q));
 155       };
 156     }else{
 157       // It's a constant
 158       d_constants.push_back(make_triple((TNode)d_pattern[i],i,q));
 159     }
 160   }
 161 }
 162
 163 void ApplyMatcher::resetInstantiationRound( QuantifiersEngine* qe ){
 164   for( size_t i=0; i< d_childrens.size(); i++ ){
 165     d_childrens[i].first->resetInstantiationRound( qe );
 166   }
 167 }
 168
 169 bool ApplyMatcher::reset(TNode t, InstMatch & m, QuantifiersEngine* qe){
 170   Debug("matching") << "Matching " << t << " against pattern " << d_pattern << " ("
 171                     << m.size() << ")"  << std::endl;
 172
 173   //if t is null
 174   Assert( !t.isNull() );
 175   Assert( !t.hasAttribute(InstConstantAttribute()) );
 176   Assert( t.getKind()==d_pattern.getKind() );
 177   Assert( (t.getKind()!=APPLY_UF && t.getKind()!=APPLY_CONSTRUCTOR)
 178           || t.getOperator()==d_pattern.getOperator() );
 179
 180   typedef std::vector< triple<TNode,size_t,EqualityQuery*> >::iterator iterator;
 181   for(iterator i = d_constants.begin(), end = d_constants.end();
 182       i != end; ++i){
 183     if( !i->third->areEqual( i->first, t[i->second] ) ){
 184       Debug("matching-fail") << "Match fail arg: " << i->first << " and " << t[i->second] << std::endl;
 185       //setMatchFail( qe, d_pattern[i], t[i] );
 186       //ground arguments are not equal
 187       return false;
 188     }
 189   }
 190
 191   d_binded.clear();
 192   bool set;
 193   for(iterator i = d_variables.begin(), end = d_variables.end();
 194       i != end; ++i){
 195     if( !m.setMatch( i->third, i->first, t[i->second], set) ){
 196       //match is in conflict
 197       Debug("matching-debug") << "Match in conflict " << t[i->second] << " and "
 198                               << i->first << " because "
 199                               << m.get(i->first)
 200                               << std::endl;
 201       Debug("matching-fail") << "Match fail: " << m.get(i->first) << " and " << t[i->second] << std::endl;
 202       //setMatchFail( qe, partial[0].d_map[d_pattern[i]], t[i] );
 203       m.erase(d_binded.begin(), d_binded.end());
 204       return false;
 205     }else{
 206       if(set){ //The variable has just been set
 207         d_binded.push_back(i->first);
 208       }
 209     }
 210   }
 211
 212   //now, fit children into match
 213   //we will be requesting candidates for matching terms for each child
 214   d_reps.clear();
 215   for( size_t i=0; i< d_childrens.size(); i++ ){
 216     Debug("matching-debug") << "Take the representative of " << t[ d_childrens[i].second ] << std::endl;
 217     Assert( d_childrens[i].third->hasTerm(t[ d_childrens[i].second ]) );
 218     Node rep = d_childrens[i].third->getRepresentative( t[ d_childrens[i].second ] );
 219     d_reps.push_back( rep );
 220   }
 221
 222   if(d_childrens.size() == 0) return true;
 223   else return getNextMatch(m, qe, true);
 224 }
 225
 226 bool ApplyMatcher::getNextMatch(InstMatch& m, QuantifiersEngine* qe, bool reset){
 227   Assert(d_childrens.size() > 0);
 228   const size_t max = d_childrens.size() - 1;
 229   size_t index = reset ? 0 : max;
 230   Assert(d_childrens.size() == d_reps.size());
 231   while(true){
 232     if(reset ?
 233        d_childrens[index].first->reset( d_reps[index], m, qe ) :
 234        d_childrens[index].first->getNextMatch( m, qe )){
 235       if(index==max) return true;
 236       ++index;
 237       reset=true;
 238     }else{
 239       if(index==0){
 240         m.erase(d_binded.begin(), d_binded.end());
 241         return false;
 242       }
 243       --index;
 244       reset=false;
 245     };
 246   }
 247 }
 248
 249 bool ApplyMatcher::getNextMatch(InstMatch& m, QuantifiersEngine* qe){
 250   if(d_childrens.size() == 0){
 251     m.erase(d_binded.begin(), d_binded.end());
 252     return false;
 253   } else return getNextMatch(m, qe, false);
 254 }
 255
 256 /** Proxy that call the sub-matcher on the result return by the given candidate generator */
 257 template <class CG, class M>
 258 class CandidateGeneratorMatcher: public Matcher{
 259   /** candidate generator */
 260   CG d_cg;
 261   /** the sub-matcher */
 262   M d_m;
 263 public:
 264   CandidateGeneratorMatcher(CG cg, M m): d_cg(cg), d_m(m)
 265   {/* last is Null */};
 266   void resetInstantiationRound( QuantifiersEngine* qe ){
 267     d_cg.resetInstantiationRound();
 268     d_m.resetInstantiationRound(qe);
 269   };
 270   bool reset( TNode n, InstMatch& m, QuantifiersEngine* qe ){
 271     d_cg.reset(n);
 272     return findMatch(m,qe);
 273   }
 274   bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){
 275     // The sub-matcher has another match
 276     return d_m.getNextMatch(m, qe) || findMatch(m,qe);
 277   }
 278 private:
 279   bool findMatch( InstMatch& m, QuantifiersEngine* qe ){
 280     // Otherwise try to find a new candidate that has at least one match
 281     while(true){
 282       TNode n = d_cg.getNextCandidate();//kept somewhere Term-db
 283       Debug("matching") << "GenCand " << n << " (" << this << ")" << std::endl;
 284       if(n.isNull()) return false;
 285       if(d_m.reset(n,m,qe)) return true;
 286     };
 287   }
 288 };
 289
 290 /** Proxy that call the sub-matcher on the result return by the given candidate generator */
 291 template<class M>
 292 class PatOfMatcher: public PatMatcher{
 293   M d_m;
 294 public:
 295   inline PatOfMatcher(M m): d_m(m){}
 296   void resetInstantiationRound(QuantifiersEngine* qe){
 297     d_m.resetInstantiationRound(qe);
 298   }
 299   bool reset(InstMatch& m, QuantifiersEngine* qe){
 300     return d_m.reset(Node::null(),m,qe);
 301   };
 302   bool getNextMatch(InstMatch& m, QuantifiersEngine* qe){
 303     return d_m.getNextMatch(m,qe);
 304   };
 305 };
 306
 307 class ArithMatcher: public Matcher{
 308 private:
 309   /** for arithmetic matching */
 310   std::map< Node, Node > d_arith_coeffs;
 311   /** get the match against ground term or formula t.
 312       d_match_mattern and t should have the same shape.
 313       only valid for use where !d_match_pattern.isNull().
 314   */
 315   /** the variable that are set by this matcher */
 316   std::vector< TNode > d_binded; /* TNode because the variables are already in d_arith_coeffs */
 317   Node d_pattern; //for debugging
 318 public:
 319   ArithMatcher(Node pat, QuantifiersEngine* qe);
 320   void resetInstantiationRound( QuantifiersEngine* qe ){};
 321   bool reset( TNode n, InstMatch& m, QuantifiersEngine* qe );
 322   bool getNextMatch( InstMatch& m, QuantifiersEngine* qe );
 323 };
 324
 325 /** Match just a variable */
 326 class VarMatcher: public Matcher{
 327   Node d_var;
 328   bool d_binded; /* True if the reset bind the variable to some value */
 329   EqualityQuery* d_q;
 330 public:
 331   VarMatcher(Node var, QuantifiersEngine* qe): d_var(var), d_binded(false){
 332     d_q = qe->getEqualityQuery(var.getType());
 333   }
 334   void resetInstantiationRound( QuantifiersEngine* qe ){};
 335   bool reset( TNode n, InstMatch& m, QuantifiersEngine* qe ){
 336     if(!m.setMatch( d_q, d_var, n, d_binded )){
 337       //match is in conflict
 338       Debug("matching-fail") << "Match fail: " << m.get(d_var)
 339                              << " and " << n << std::endl;
 340       return false;
 341     } else return true;
 342   };
 343   bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){
 344     //match is in conflict
 345     if (d_binded) m.erase(d_var);
 346     return false;
 347   }
 348 };
 349
 350 template <class M, class Test >
 351 class TestMatcher: public Matcher{
 352   M d_m;
 353   Test d_test;
 354 public:
 355   inline TestMatcher(M m, Test test): d_m(m), d_test(test){}
 356   inline void resetInstantiationRound(QuantifiersEngine* qe){
 357     d_m.resetInstantiationRound(qe);
 358   }
 359   inline bool reset(TNode n, InstMatch& m, QuantifiersEngine* qe){
 360     return d_test(n) && d_m.reset(n, m, qe);
 361   }
 362   inline bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){
 363     return d_m.getNextMatch(m, qe);
 364   }
 365 };
 366
 367 class LegalOpTest/*: public unary_function<TNode,bool>*/ {
 368   Node d_op;
 369 public:
 370   inline LegalOpTest(Node op): d_op(op){}
 371   inline bool operator() (TNode n) {
 372     return
 373       CandidateGenerator::isLegalCandidate(n) &&
 374       // ( // n.getKind()==SELECT || n.getKind()==STORE ||
 375       //  n.getKind()==APPLY_UF || n.getKind()==APPLY_CONSTRUCTOR) &&
 376       n.hasOperator() &&
 377       n.getOperator()==d_op;
 378   };
 379 };
 380
 381 class LegalKindTest/* : public unary_function<TNode,bool>*/ {
 382   Kind d_kind;
 383 public:
 384   inline LegalKindTest(Kind kind): d_kind(kind){}
 385   inline bool operator() (TNode n) {
 386     return
 387       CandidateGenerator::isLegalCandidate(n) &&
 388       n.getKind()==d_kind;
 389   };
 390 };
 391
 392 class LegalTypeTest/* : public unary_function<TNode,bool>*/ {
 393   TypeNode d_type;
 394 public:
 395   inline LegalTypeTest(TypeNode type): d_type(type){}
 396   inline bool operator() (TNode n) {
 397     return
 398       CandidateGenerator::isLegalCandidate(n) &&
 399       n.getType()==d_type;
 400   };
 401 };
 402
 403 class LegalTest/* : public unary_function<TNode,bool>*/ {
 404 public:
 405   inline bool operator() (TNode n) {
 406     return CandidateGenerator::isLegalCandidate(n);
 407   };
 408 };
 409
 410 size_t numFreeVar(TNode t){
 411   size_t n = 0;
 412   for( size_t i=0, size =t.getNumChildren(); i < size; ++i ){
 413     if( t[i].hasAttribute(InstConstantAttribute()) ){
 414       if( t[i].getKind()==INST_CONSTANT ){
 415         //variable
 416         ++n;
 417       }else{
 418         //neither variable nor constant
 419         n += numFreeVar(t[i]);
 420       }
 421     }
 422   }
 423   return n;
 424 }
 425
 426 class OpMatcher: public Matcher{
 427   /* The matcher */
 428   typedef ApplyMatcher AuxMatcher3;
 429   typedef TestMatcher< AuxMatcher3, LegalOpTest > AuxMatcher2;
 430   typedef CandidateGeneratorMatcher< CandidateGeneratorTheoryEeClass, AuxMatcher2> AuxMatcher1;
 431   AuxMatcher1 d_cgm;
 432   static inline AuxMatcher1 createCgm(Node pat, QuantifiersEngine* qe){
 433     Assert( pat.getKind() == kind::APPLY_UF );
 434     /** In reverse order of matcher sequence */
 435     AuxMatcher3 am3(pat,qe);
 436     /** Keep only the one that have the good operator */
 437     AuxMatcher2 am2(am3,LegalOpTest(pat.getOperator()));
 438     /** Iter on the equivalence class of the given term */
 439     uf::TheoryUF* uf = static_cast<uf::TheoryUF *>(qe->getTheoryEngine()->getTheory( theory::THEORY_UF ));
 440     eq::EqualityEngine* ee = static_cast<eq::EqualityEngine*>(uf->getEqualityEngine());
 441     CandidateGeneratorTheoryEeClass cdtUfEq(ee);
 442     /* Create a matcher from the candidate generator */
 443     AuxMatcher1 am1(cdtUfEq,am2);
 444     return am1;
 445   }
 446   size_t d_num_var;
 447   Node d_pat;
 448 public:
 449   OpMatcher( Node pat, QuantifiersEngine* qe ):
 450     d_cgm(createCgm(pat, qe)),d_num_var(numFreeVar(pat)),
 451     d_pat(pat) {}
 452
 453   void resetInstantiationRound( QuantifiersEngine* qe ){
 454     d_cgm.resetInstantiationRound(qe);
 455   };
 456   bool reset( TNode t, InstMatch& m, QuantifiersEngine* qe ){
 457     // size_t m_size = m.d_map.size();
 458     // if(m_size == d_num_var){
 459     //   uf::EqualityEngine<uf::TheoryUF::NotifyClass>* ee = (static_cast<uf::TheoryUF*>(qe->getTheoryEngine()->getTheory( theory::THEORY_UF )))->getEqualityEngine();
 460     //   std::cout << "!";
 461     //   return ee->areEqual(m.subst(d_pat),t);
 462     // }else{
 463     // std::cout << m.d_map.size() << std::endl;
 464     return d_cgm.reset(t, m, qe);
 465     // }
 466   }
 467   bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){
 468     return d_cgm.getNextMatch(m, qe);
 469   }
 470 };
 471
 472 class DatatypesMatcher: public Matcher{
 473   /* The matcher */
 474   typedef ApplyMatcher AuxMatcher3;
 475   typedef TestMatcher< AuxMatcher3, LegalOpTest > AuxMatcher2;
 476   typedef CandidateGeneratorMatcher< CandidateGeneratorTheoryEeClass, AuxMatcher2> AuxMatcher1;
 477   AuxMatcher1 d_cgm;
 478   static inline AuxMatcher1 createCgm(Node pat, QuantifiersEngine* qe){
 479     Assert( pat.getKind() == kind::APPLY_CONSTRUCTOR,
 480             "For datatypes only constructor are accepted in pattern" );
 481     /** In reverse order of matcher sequence */
 482     AuxMatcher3 am3(pat,qe);
 483     /** Keep only the one that have the good operator */
 484     AuxMatcher2 am2(am3,LegalOpTest(pat.getOperator()));
 485     /** Iter on the equivalence class of the given term */
 486     datatypes::TheoryDatatypes* dt = static_cast<datatypes::TheoryDatatypes *>(qe->getTheoryEngine()->getTheory( theory::THEORY_DATATYPES ));
 487     eq::EqualityEngine* ee = static_cast<eq::EqualityEngine*>(dt->getEqualityEngine());
 488     CandidateGeneratorTheoryEeClass cdtDtEq(ee);
 489     /* Create a matcher from the candidate generator */
 490     AuxMatcher1 am1(cdtDtEq,am2);
 491     return am1;
 492   }
 493   Node d_pat;
 494 public:
 495   DatatypesMatcher( Node pat, QuantifiersEngine* qe ):
 496     d_cgm(createCgm(pat, qe)),
 497     d_pat(pat) {}
 498
 499   void resetInstantiationRound( QuantifiersEngine* qe ){
 500     d_cgm.resetInstantiationRound(qe);
 501   };
 502   bool reset( TNode t, InstMatch& m, QuantifiersEngine* qe ){
 503     Debug("matching") << "datatypes: " << t << " matches " << d_pat << std::endl;
 504     return d_cgm.reset(t, m, qe);
 505   }
 506   bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){
 507     return d_cgm.getNextMatch(m, qe);
 508   }
 509 };
 510
 511 class ArrayMatcher: public Matcher{
 512   /* The matcher */
 513   typedef ApplyMatcher AuxMatcher3;
 514   typedef TestMatcher< AuxMatcher3, LegalKindTest > AuxMatcher2;
 515   typedef CandidateGeneratorMatcher< CandidateGeneratorTheoryEeClass, AuxMatcher2> AuxMatcher1;
 516   AuxMatcher1 d_cgm;
 517   static inline AuxMatcher1 createCgm(Node pat, QuantifiersEngine* qe){
 518     Assert( pat.getKind() == kind::SELECT || pat.getKind() == kind::STORE );
 519     /** In reverse order of matcher sequence */
 520     AuxMatcher3 am3(pat,qe);
 521     /** Keep only the one that have the good operator */
 522     AuxMatcher2 am2(am3, LegalKindTest(pat.getKind()));
 523     /** Iter on the equivalence class of the given term */
 524     arrays::TheoryArrays* ar = static_cast<arrays::TheoryArrays *>(qe->getTheoryEngine()->getTheory( theory::THEORY_ARRAY ));
 525     eq::EqualityEngine* ee =
 526       static_cast<eq::EqualityEngine*>(ar->getEqualityEngine());
 527     CandidateGeneratorTheoryEeClass cdtUfEq(ee);
 528     /* Create a matcher from the candidate generator */
 529     AuxMatcher1 am1(cdtUfEq,am2);
 530     return am1;
 531   }
 532   size_t d_num_var;
 533   Node d_pat;
 534 public:
 535   ArrayMatcher( Node pat, QuantifiersEngine* qe ):
 536     d_cgm(createCgm(pat, qe)),d_num_var(numFreeVar(pat)),
 537     d_pat(pat) {}
 538
 539   void resetInstantiationRound( QuantifiersEngine* qe ){
 540     d_cgm.resetInstantiationRound(qe);
 541   };
 542   bool reset( TNode t, InstMatch& m, QuantifiersEngine* qe ){
 543     // size_t m_size = m.d_map.size();
 544     // if(m_size == d_num_var){
 545     //   uf::EqualityEngine<uf::TheoryUF::NotifyClass>* ee = (static_cast<uf::TheoryUF*>(qe->getTheoryEngine()->getTheory( theory::THEORY_UF )))->getEqualityEngine();
 546     //   std::cout << "!";
 547     //   return ee->areEqual(m.subst(d_pat),t);
 548     // }else{
 549     // std::cout << m.d_map.size() << std::endl;
 550     return d_cgm.reset(t, m, qe);
 551     // }
 552   }
 553   bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){
 554     return d_cgm.getNextMatch(m, qe);
 555   }
 556 };
 557
 558 class AllOpMatcher: public PatMatcher{
 559   /* The matcher */
 560   typedef ApplyMatcher AuxMatcher3;
 561   typedef TestMatcher< AuxMatcher3, LegalTest > AuxMatcher2;
 562   typedef CandidateGeneratorMatcher< CandidateGeneratorTheoryUfOp, AuxMatcher2> AuxMatcher1;
 563   AuxMatcher1 d_cgm;
 564   static inline AuxMatcher1 createCgm(Node pat, QuantifiersEngine* qe){
 565     Assert( pat.hasOperator() );
 566     /** In reverse order of matcher sequence */
 567     AuxMatcher3 am3(pat,qe);
 568     /** Keep only the one that have the good operator */
 569     AuxMatcher2 am2(am3,LegalTest());
 570     /** Iter on the equivalence class of the given term */
 571     TermDb* tdb = qe->getTermDatabase();
 572     CandidateGeneratorTheoryUfOp cdtUfEq(pat.getOperator(),tdb);
 573     /* Create a matcher from the candidate generator */
 574     AuxMatcher1 am1(cdtUfEq,am2);
 575     return am1;
 576   }
 577   size_t d_num_var;
 578   Node d_pat;
 579 public:
 580   AllOpMatcher( TNode pat, QuantifiersEngine* qe ):
 581     d_cgm(createCgm(pat, qe)), d_num_var(numFreeVar(pat)),
 582     d_pat(pat) {}
 583
 584   void resetInstantiationRound( QuantifiersEngine* qe ){
 585     d_cgm.resetInstantiationRound(qe);
 586   };
 587   bool reset( InstMatch& m, QuantifiersEngine* qe ){
 588     //    std::cout << m.d_map.size() << "/" << d_num_var << std::endl;
 589     return d_cgm.reset(Node::null(), m, qe);
 590   }
 591   bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){
 592     return d_cgm.getNextMatch(m, qe);
 593   }
 594 };
 595
 596 template <bool classes> /** true classes | false class */
 597 class GenericCandidateGeneratorClasses: public CandidateGenerator{
 598 private:
 599   CandidateGenerator* d_cg;
 600   QuantifiersEngine* d_qe;
 601
 602 public:
 603   void mkCandidateGenerator(){
 604     if(classes)
 605       d_cg = d_qe->getRRCanGenClasses();
 606     else
 607      d_cg = d_qe->getRRCanGenClass();
 608   }
 609
 610   GenericCandidateGeneratorClasses(QuantifiersEngine* qe):
 611     d_qe(qe) {
 612     mkCandidateGenerator();
 613   }
 614   ~GenericCandidateGeneratorClasses(){
 615     delete(d_cg);
 616   }
 617   const GenericCandidateGeneratorClasses & operator =(const GenericCandidateGeneratorClasses & m){
 618     mkCandidateGenerator();
 619     return m;
 620   };
 621   GenericCandidateGeneratorClasses(const GenericCandidateGeneratorClasses & m):
 622   d_qe(m.d_qe){
 623     mkCandidateGenerator();
 624   }
 625   void resetInstantiationRound(){
 626     d_cg->resetInstantiationRound();
 627   };
 628   void reset( TNode eqc ){
 629     Assert( !classes || eqc.isNull() );
 630     d_cg->reset(eqc);
 631   }; //* the argument is not used
 632   TNode getNextCandidate(){
 633     return d_cg->getNextCandidate();
 634   };
 635 }; /* MetaCandidateGeneratorClasses */
 636
 637
 638 class GenericMatcher: public Matcher{
 639   /* The matcher */
 640   typedef ApplyMatcher AuxMatcher3;
 641   typedef TestMatcher< AuxMatcher3, LegalOpTest > AuxMatcher2;
 642   typedef CandidateGeneratorMatcher< GenericCandidateGeneratorClasses<false>, AuxMatcher2> AuxMatcher1;
 643   AuxMatcher1 d_cgm;
 644   static inline AuxMatcher1 createCgm(Node pat, QuantifiersEngine* qe){
 645     /** In reverse order of matcher sequence */
 646     AuxMatcher3 am3(pat,qe);
 647     /** Keep only the one that have the good operator */
 648     AuxMatcher2 am2(am3,LegalOpTest(pat.getOperator()));
 649     /** Iter on the equivalence class of the given term */
 650     GenericCandidateGeneratorClasses<false> cdtG(qe);
 651     /* Create a matcher from the candidate generator */
 652     AuxMatcher1 am1(cdtG,am2);
 653     return am1;
 654   }
 655   Node d_pat;
 656 public:
 657   GenericMatcher( Node pat, QuantifiersEngine* qe ):
 658     d_cgm(createCgm(pat, qe)),
 659     d_pat(pat) {}
 660
 661   void resetInstantiationRound( QuantifiersEngine* qe ){
 662     d_cgm.resetInstantiationRound(qe);
 663   };
 664   bool reset( TNode t, InstMatch& m, QuantifiersEngine* qe ){
 665     return d_cgm.reset(t, m, qe);
 666   }
 667   bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){
 668     return d_cgm.getNextMatch(m, qe);
 669   }
 670 };
 671
 672
 673 class GenericPatMatcher: public PatMatcher{
 674   /* The matcher */
 675   typedef ApplyMatcher AuxMatcher3;
 676   typedef TestMatcher< AuxMatcher3, LegalOpTest > AuxMatcher2;
 677   typedef CandidateGeneratorMatcher< GenericCandidateGeneratorClasses<true>, AuxMatcher2> AuxMatcher1;
 678   AuxMatcher1 d_cgm;
 679   static inline AuxMatcher1 createCgm(Node pat, QuantifiersEngine* qe){
 680     /** In reverse order of matcher sequence */
 681     AuxMatcher3 am3(pat,qe);
 682     /** Keep only the one that have the good operator */
 683     AuxMatcher2 am2(am3,LegalOpTest(pat.getOperator()));
 684     /** Iter on the equivalence class of the given term */
 685     GenericCandidateGeneratorClasses<true> cdtG(qe);
 686     /* Create a matcher from the candidate generator */
 687     AuxMatcher1 am1(cdtG,am2);
 688     return am1;
 689   }
 690   Node d_pat;
 691 public:
 692   GenericPatMatcher( Node pat, QuantifiersEngine* qe ):
 693     d_cgm(createCgm(pat, qe)),
 694     d_pat(pat) {}
 695
 696   void resetInstantiationRound( QuantifiersEngine* qe ){
 697     d_cgm.resetInstantiationRound(qe);
 698   };
 699   bool reset( InstMatch& m, QuantifiersEngine* qe ){
 700     return d_cgm.reset(Node::null(), m, qe);
 701   }
 702   bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){
 703     return d_cgm.getNextMatch(m, qe);
 704   }
 705 };
 706
 707 class MetaCandidateGeneratorClasses: public CandidateGenerator{
 708 private:
 709   CandidateGenerator* d_cg;
 710   TypeNode d_ty;
 711   TheoryEngine* d_te;
 712
 713 public:
 714   CandidateGenerator* mkCandidateGenerator(TypeNode ty, TheoryEngine* te){
 715     Debug("inst-match-gen") << "MetaCandidateGenerator for type: " << ty
 716                             << " Theory : " << Theory::theoryOf(ty) << std::endl;
 717     if( Theory::theoryOf(ty) == theory::THEORY_DATATYPES ){
 718       // datatypes::TheoryDatatypes* dt = static_cast<datatypes::TheoryDatatypes *>(te->getTheory( theory::THEORY_DATATYPES ));
 719       // return new datatypes::rrinst::CandidateGeneratorTheoryClasses(dt);
 720       Unimplemented("MetaCandidateGeneratorClasses for THEORY_DATATYPES");
 721     }else if ( Theory::theoryOf(ty) == theory::THEORY_ARRAY ){
 722       arrays::TheoryArrays* ar = static_cast<arrays::TheoryArrays *>(te->getTheory( theory::THEORY_ARRAY ));
 723       eq::EqualityEngine* ee =
 724         static_cast<eq::EqualityEngine*>(ar->getEqualityEngine());
 725       return new CandidateGeneratorTheoryEeClasses(ee);
 726     } else {
 727       uf::TheoryUF* uf = static_cast<uf::TheoryUF*>(te->getTheory( theory::THEORY_UF ));
 728       eq::EqualityEngine* ee =
 729         static_cast<eq::EqualityEngine*>(uf->getEqualityEngine());
 730       return new CandidateGeneratorTheoryEeClasses(ee);
 731     }
 732   }
 733   MetaCandidateGeneratorClasses(TypeNode ty, TheoryEngine* te):
 734     d_ty(ty), d_te(te) {
 735     d_cg = mkCandidateGenerator(ty,te);
 736   }
 737   ~MetaCandidateGeneratorClasses(){
 738     delete(d_cg);
 739   }
 740   const MetaCandidateGeneratorClasses & operator =(const MetaCandidateGeneratorClasses & m){
 741     d_cg = mkCandidateGenerator(m.d_ty, m.d_te);
 742     return m;
 743   };
 744   MetaCandidateGeneratorClasses(const MetaCandidateGeneratorClasses & m):
 745   d_ty(m.d_ty), d_te(m.d_te){
 746     d_cg = mkCandidateGenerator(m.d_ty, m.d_te);
 747   }
 748   void resetInstantiationRound(){
 749     d_cg->resetInstantiationRound();
 750   };
 751   void reset( TNode eqc ){
 752     d_cg->reset(eqc);
 753   }; //* the argument is not used
 754   TNode getNextCandidate(){
 755     return d_cg->getNextCandidate();
 756   };
 757 }; /* MetaCandidateGeneratorClasses */
 758
 759 /** Match just a variable */
 760 class AllVarMatcher: public PatMatcher{
 761 private:
 762   /* generator */
 763   typedef VarMatcher AuxMatcher3;
 764   typedef TestMatcher< AuxMatcher3, LegalTypeTest > AuxMatcher2;
 765   typedef CandidateGeneratorMatcher< MetaCandidateGeneratorClasses, AuxMatcher2 > AuxMatcher1;
 766   AuxMatcher1 d_cgm;
 767   static inline AuxMatcher1 createCgm(TNode pat, QuantifiersEngine* qe){
 768     Assert( pat.getKind()==INST_CONSTANT );
 769     TypeNode ty = pat.getType();
 770     Debug("inst-match-gen") << "create AllVarMatcher for type: " << ty << std::endl;
 771     /** In reverse order of matcher sequence */
 772     /** Distribute it to all the pattern */
 773     AuxMatcher3 am3(pat,qe);
 774     /** Keep only the one that have the good type */
 775     AuxMatcher2 am2(am3,LegalTypeTest(ty));
 776     /** Generate one term by eq classes */
 777     MetaCandidateGeneratorClasses mcdt(ty,qe->getTheoryEngine());
 778     /* Create a matcher from the candidate generator */
 779     AuxMatcher1 am1(mcdt,am2);
 780     return am1;
 781   }
 782 public:
 783   AllVarMatcher( TNode pat, QuantifiersEngine* qe ):
 784     d_cgm(createCgm(pat, qe)){}
 785
 786   void resetInstantiationRound( QuantifiersEngine* qe ){
 787     d_cgm.resetInstantiationRound(qe);
 788   };
 789   bool reset( InstMatch& m, QuantifiersEngine* qe ){
 790     return d_cgm.reset(Node::null(), m, qe); //cdtUfEq doesn't use it's argument for reset
 791   }
 792   bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){
 793     return d_cgm.getNextMatch(m, qe);
 794   }
 795 };
 796
 797 /** Match all the pattern with the same term */
 798 class SplitMatcher: public Matcher{
 799 private:
 800   const size_t size;
 801   ApplyMatcher d_m; /** Use ApplyMatcher by creating a fake application */
 802 public:
 803   SplitMatcher(std::vector< Node > pats, QuantifiersEngine* qe):
 804     size(pats.size()),
 805     d_m(NodeManager::currentNM()->mkNode(kind::INST_PATTERN,pats), qe) {}
 806   void resetInstantiationRound( QuantifiersEngine* qe ){
 807     d_m.resetInstantiationRound(qe);
 808   };
 809   bool reset( TNode ex, InstMatch& m, QuantifiersEngine* qe ){
 810     NodeBuilder<> n(kind::INST_PATTERN);
 811     for(size_t i = 0; i < size; ++i) n << ex;
 812     Node nn = n;
 813     return d_m.reset(nn,m,qe);
 814   };
 815   bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){
 816     return getNextMatch(m, qe);
 817   }
 818 };
 819
 820
 821 /** Match uf term in a fixed equivalence class */
 822 class UfCstEqMatcher: public PatMatcher{
 823 private:
 824   /* equivalence class to match */
 825   Node d_cst;
 826   /* generator */
 827   OpMatcher d_cgm;
 828 public:
 829   UfCstEqMatcher( Node pat, Node cst, QuantifiersEngine* qe ):
 830     d_cst(cst),
 831     d_cgm(OpMatcher(pat,qe)) {};
 832   void resetInstantiationRound( QuantifiersEngine* qe ){
 833     d_cgm.resetInstantiationRound(qe);
 834   };
 835   bool reset( InstMatch& m, QuantifiersEngine* qe ){
 836     return d_cgm.reset(d_cst, m, qe);
 837   }
 838   bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){
 839     return d_cgm.getNextMatch(m, qe);
 840   }
 841 };
 842
 843 /** Match equalities */
 844 class UfEqMatcher: public PatMatcher{
 845 private:
 846   /* generator */
 847   typedef SplitMatcher AuxMatcher3;
 848   typedef TestMatcher< AuxMatcher3, LegalTypeTest > AuxMatcher2;
 849   typedef CandidateGeneratorMatcher< CandidateGeneratorTheoryEeClasses, AuxMatcher2 > AuxMatcher1;
 850   AuxMatcher1 d_cgm;
 851   static inline AuxMatcher1 createCgm(std::vector<Node> & pat, QuantifiersEngine* qe){
 852     Assert( pat.size() > 0);
 853     TypeNode ty = pat[0].getType();
 854     for(size_t i = 1; i < pat.size(); ++i){
 855       Assert(pat[i].getType() == ty);
 856     }
 857     /** In reverse order of matcher sequence */
 858     /** Distribute it to all the pattern */
 859     AuxMatcher3 am3(pat,qe);
 860     /** Keep only the one that have the good type */
 861     AuxMatcher2 am2(am3,LegalTypeTest(ty));
 862     /** Generate one term by eq classes */
 863     uf::TheoryUF* uf = static_cast<uf::TheoryUF*>(qe->getTheoryEngine()->getTheory( theory::THEORY_UF ));
 864     eq::EqualityEngine* ee =
 865       static_cast<eq::EqualityEngine*>(uf->getEqualityEngine());
 866     CandidateGeneratorTheoryEeClasses cdtUfEq(ee);
 867     /* Create a matcher from the candidate generator */
 868     AuxMatcher1 am1(cdtUfEq,am2);
 869     return am1;
 870   }
 871 public:
 872   UfEqMatcher( std::vector<Node> & pat, QuantifiersEngine* qe ):
 873     d_cgm(createCgm(pat, qe)){}
 874
 875   void resetInstantiationRound( QuantifiersEngine* qe ){
 876     d_cgm.resetInstantiationRound(qe);
 877   };
 878   bool reset( InstMatch& m, QuantifiersEngine* qe ){
 879     return d_cgm.reset(Node::null(), m, qe); //cdtUfEq doesn't use it's argument for reset
 880   }
 881   bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){
 882     return d_cgm.getNextMatch(m, qe);
 883   }
 884 };
 885
 886
 887 /** Match dis-equalities */
 888 class UfDeqMatcher: public PatMatcher{
 889 private:
 890   /* generator */
 891   typedef ApplyMatcher AuxMatcher3;
 892
 893   class EqTest/* : public unary_function<Node,bool>*/ {
 894     TypeNode d_type;
 895   public:
 896     inline EqTest(TypeNode type): d_type(type){};
 897     inline bool operator() (Node n) {
 898       return
 899         CandidateGenerator::isLegalCandidate(n) &&
 900         n.getKind() == kind::EQUAL &&
 901         n[0].getType()==d_type;
 902     };
 903   };
 904   typedef TestMatcher< AuxMatcher3, EqTest > AuxMatcher2;
 905   typedef CandidateGeneratorMatcher< CandidateGeneratorTheoryEeClass, AuxMatcher2 > AuxMatcher1;
 906   AuxMatcher1 d_cgm;
 907   Node false_term;
 908   static inline AuxMatcher1 createCgm(Node pat, QuantifiersEngine* qe){
 909     Assert( pat.getKind() == kind::NOT);
 910     TNode eq = pat[0];
 911     Assert( eq.getKind() == kind::EQUAL);
 912     TypeNode ty = eq[0].getType();
 913     /** In reverse order of matcher sequence */
 914     /** Distribute it to all the pattern */
 915     AuxMatcher3 am3(eq,qe);
 916     /** Keep only the one that have the good type */
 917     AuxMatcher2 am2(am3,EqTest(ty));
 918     /** Will generate all the terms of the eq class of false */
 919     uf::TheoryUF* uf = static_cast<uf::TheoryUF*>(qe->getTheoryEngine()->getTheory( theory::THEORY_UF ));
 920     eq::EqualityEngine* ee =
 921       static_cast<eq::EqualityEngine*>(uf->getEqualityEngine());
 922     CandidateGeneratorTheoryEeClass cdtUfEq(ee);
 923     /* Create a matcher from the candidate generator */
 924     AuxMatcher1 am1(cdtUfEq,am2);
 925     return am1;
 926   }
 927 public:
 928   UfDeqMatcher( Node pat, QuantifiersEngine* qe ):
 929     d_cgm(createCgm(pat, qe)),
 930     false_term((static_cast<uf::TheoryUF*>(qe->getTheoryEngine()->getTheory( theory::THEORY_UF )))->getEqualityEngine()->
 931                 getRepresentative(NodeManager::currentNM()->mkConst<bool>(false) )){};
 932   void resetInstantiationRound( QuantifiersEngine* qe ){
 933     d_cgm.resetInstantiationRound(qe);
 934   };
 935   bool reset( InstMatch& m, QuantifiersEngine* qe ){
 936     return d_cgm.reset(false_term, m, qe);
 937   }
 938   bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){
 939     return d_cgm.getNextMatch(m, qe);
 940   }
 941 };
 942
 943 Matcher* mkMatcher( Node pat, QuantifiersEngine* qe ){
 944   Debug("inst-match-gen") << "mkMatcher: Pattern term is " << pat << std::endl;
 945
 946   // if( pat.getKind() == kind::APPLY_UF){
 947   //   return new OpMatcher(pat, qe);
 948   // } else if( pat.getKind() == kind::APPLY_CONSTRUCTOR ){
 949   //   return new DatatypesMatcher(pat, qe);
 950   // } else if( pat.getKind() == kind::SELECT || pat.getKind() == kind::STORE ){
 951   //   return new ArrayMatcher(pat, qe);
 952   if( pat.getKind() == kind::APPLY_UF ||
 953       pat.getKind() == kind::APPLY_CONSTRUCTOR ||
 954       pat.getKind() == kind::SELECT || pat.getKind() == kind::STORE ){
 955     return new GenericMatcher(pat, qe);
 956   } else { /* Arithmetic? */
 957     /** TODO: something simpler to see if the pattern is a good
 958         arithmetic pattern */
 959     std::map< Node, Node > d_arith_coeffs;
 960     if( !Trigger::getPatternArithmetic( pat.getAttribute(InstConstantAttribute()), pat, d_arith_coeffs ) ){
 961       Message() << "(?) Unknown matching pattern is " << pat << std::endl;
 962       Unimplemented("pattern not implemented");
 963       return new DumbMatcher();
 964     }else{
 965       Debug("matching-arith") << "Generated arithmetic pattern for " << pat << ": " << std::endl;
 966       for( std::map< Node, Node >::iterator it = d_arith_coeffs.begin(); it != d_arith_coeffs.end(); ++it ){
 967         Debug("matching-arith") << "   " << it->first << " -> " << it->second << std::endl;
 968       }
 969       ArithMatcher am3 (pat, qe);
 970       TestMatcher<ArithMatcher, LegalTypeTest>
 971         am2(am3,LegalTypeTest(pat.getType()));
 972       /* generator */
 973       uf::TheoryUF* uf = static_cast<uf::TheoryUF*>(qe->getTheoryEngine()->getTheory( theory::THEORY_UF ));
 974       eq::EqualityEngine* ee =
 975         static_cast<eq::EqualityEngine*> (uf->getEqualityEngine());
 976       CandidateGeneratorTheoryEeClass cdtUfEq(ee);
 977       return new CandidateGeneratorMatcher< CandidateGeneratorTheoryEeClass,
 978         TestMatcher<ArithMatcher, LegalTypeTest> > (cdtUfEq,am2);
 979     }
 980   }
 981 };
 982
 983 PatMatcher* mkPattern( Node pat, QuantifiersEngine* qe ){
 984   Debug("inst-match-gen") << "Pattern term is " << pat << std::endl;
 985   Assert( pat.hasAttribute(InstConstantAttribute()) );
 986
 987   if( pat.getKind()==kind::NOT && pat[0].getKind() == kind::EQUAL){
 988     /* Difference */
 989     return new UfDeqMatcher(pat, qe);
 990   } else if (pat.getKind() == kind::EQUAL){
 991     if( !pat[0].hasAttribute(InstConstantAttribute() )){
 992         Assert(pat[1].hasAttribute(InstConstantAttribute()));
 993         return new UfCstEqMatcher(pat[1], pat[0], qe);
 994     }else if( !pat[1].hasAttribute(InstConstantAttribute() )){
 995       Assert(pat[0].hasAttribute(InstConstantAttribute()));
 996       return new UfCstEqMatcher(pat[0], pat[1], qe);
 997     }else{
 998       std::vector< Node > pats(pat.begin(),pat.end());
 999       return new UfEqMatcher(pats,qe);
1000     }
1001   } else if( Trigger::isAtomicTrigger( pat ) ){
1002     return new AllOpMatcher(pat, qe);
1003     // return new GenericPatMatcher(pat, qe);
1004   } else if( pat.getKind()==INST_CONSTANT ){
1005     // just a variable
1006     return new AllVarMatcher(pat, qe);
1007   } else { /* Arithmetic? */
1008     /** TODO: something simpler to see if the pattern is a good
1009         arithmetic pattern */
1010     std::map< Node, Node > d_arith_coeffs;
1011     if( !Trigger::getPatternArithmetic( pat.getAttribute(InstConstantAttribute()), pat, d_arith_coeffs ) ){
1012       Debug("inst-match-gen") << "(?) Unknown matching pattern is " << pat << std::endl;
1013       Message() << "(?) Unknown matching pattern is " << pat << std::endl;
1014       return new DumbPatMatcher();
1015     }else{
1016       Debug("matching-arith") << "Generated arithmetic pattern for " << pat << ": " << std::endl;
1017       for( std::map< Node, Node >::iterator it = d_arith_coeffs.begin(); it != d_arith_coeffs.end(); ++it ){
1018         Debug("matching-arith") << "   " << it->first << " -> " << it->second << std::endl;
1019       }
1020       ArithMatcher am3 (pat, qe);
1021       TestMatcher<ArithMatcher, LegalTest>
1022         am2(am3,LegalTest());
1023       /* generator */
1024       TermDb* tdb = qe->getTermDatabase();
1025       CandidateGeneratorTheoryUfType cdtUfEq(pat.getType(),tdb);
1026       typedef CandidateGeneratorMatcher< CandidateGeneratorTheoryUfType,
1027                                           TestMatcher<ArithMatcher, LegalTest> > AuxMatcher1;
1028       return new PatOfMatcher<AuxMatcher1>(AuxMatcher1(cdtUfEq,am2));
1029     }
1030   }
1031 };
1032
1033 ArithMatcher::ArithMatcher(Node pat, QuantifiersEngine* qe): d_pattern(pat){
1034
1035   if(Trigger::getPatternArithmetic(pat.getAttribute(InstConstantAttribute()), pat, d_arith_coeffs ) )
1036     {
1037     Debug("inst-match-gen") << "(?) Unknown matching pattern is " << d_pattern << std::endl;
1038     Assert(false);
1039   }else{
1040     Debug("matching-arith") << "Generated arithmetic pattern for " << d_pattern << ": " << std::endl;
1041     for( std::map< Node, Node >::iterator it = d_arith_coeffs.begin(); it != d_arith_coeffs.end(); ++it ){
1042       Debug("matching-arith") << "   " << it->first << " -> " << it->second << std::endl;
1043     }
1044   }
1045
1046 };
1047
1048 bool ArithMatcher::reset( TNode t, InstMatch& m, QuantifiersEngine* qe ){
1049   Debug("matching-arith") << "Matching " << t << " " << d_pattern << std::endl;
1050   d_binded.clear();
1051   if( !d_arith_coeffs.empty() ){
1052     NodeBuilder<> tb(kind::PLUS);
1053     Node ic = Node::null();
1054     for( std::map< Node, Node >::iterator it = d_arith_coeffs.begin(); it != d_arith_coeffs.end(); ++it ){
1055       Debug("matching-arith") << it->first << " -> " << it->second << std::endl;
1056       if( !it->first.isNull() ){
1057         if( m.find( it->first )==m.end() ){
1058           //see if we can choose this to set
1059           if( ic.isNull() && ( it->second.isNull() || !it->first.getType().isInteger() ) ){
1060             ic = it->first;
1061           }
1062         }else{
1063           Debug("matching-arith") << "already set " << m.get( it->first ) << std::endl;
1064           Node tm = m.get( it->first );
1065           if( !it->second.isNull() ){
1066             tm = NodeManager::currentNM()->mkNode( MULT, it->second, tm );
1067           }
1068           tb << tm;
1069         }
1070       }else{
1071         tb << it->second;
1072       }
1073     }
1074     if( !ic.isNull() ){
1075       Node tm;
1076       if( tb.getNumChildren()==0 ){
1077         tm = t;
1078       }else{
1079         tm = tb.getNumChildren()==1 ? tb.getChild( 0 ) : tb;
1080         tm = NodeManager::currentNM()->mkNode( MINUS, t, tm );
1081       }
1082       if( !d_arith_coeffs[ ic ].isNull() ){
1083         Assert( !ic.getType().isInteger() );
1084         Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / d_arith_coeffs[ ic ].getConst<Rational>() );
1085         tm = NodeManager::currentNM()->mkNode( MULT, coeff, tm );
1086       }
1087       m.set( ic, Rewriter::rewrite( tm ));
1088       d_binded.push_back(ic);
1089       //set the rest to zeros
1090       for( std::map< Node, Node >::iterator it = d_arith_coeffs.begin(); it != d_arith_coeffs.end(); ++it ){
1091         if( !it->first.isNull() ){
1092           if( m.find( it->first )==m.end() ){
1093             m.set( it->first, NodeManager::currentNM()->mkConst( Rational(0) ));
1094             d_binded.push_back(ic);
1095           }
1096         }
1097       }
1098       Debug("matching-arith") << "Setting " << ic << " to " << tm << std::endl;
1099       return true;
1100     }else{
1101       m.erase(d_binded.begin(), d_binded.end());
1102       return false;
1103     }
1104   }else{
1105     m.erase(d_binded.begin(), d_binded.end());
1106     return false;
1107   }
1108 };
1109
1110 bool ArithMatcher::getNextMatch( InstMatch& m, QuantifiersEngine* qe ){
1111   m.erase(d_binded.begin(), d_binded.end());
1112   return false;
1113 };
1114
1115
1116 class MultiPatsMatcher: public PatsMatcher{
1117 private:
1118   bool d_reset_done;
1119   std::vector< PatMatcher* > d_patterns;
1120   InstMatch d_im;
1121   bool reset( QuantifiersEngine* qe ){
1122     d_im.clear();
1123     d_reset_done = true;
1124
1125     return getNextMatch(qe,true);
1126   };
1127
1128   bool getNextMatch(QuantifiersEngine* qe, bool reset){
1129     const size_t max = d_patterns.size() - 1;
1130     size_t index = reset ? 0 : max;
1131     while(true){
1132       Debug("matching") << "MultiPatsMatcher::index " << index << "/"
1133                         << max << (reset ? " reset_phase" : "") << std::endl;
1134       if(reset ?
1135          d_patterns[index]->reset( d_im, qe ) :
1136          d_patterns[index]->getNextMatch( d_im, qe )){
1137         if(index==max) return true;
1138         ++index;
1139         reset=true;
1140       }else{
1141         if(index==0) return false;
1142         --index;
1143         reset=false;
1144       };
1145     }
1146   }
1147
1148 public:
1149   MultiPatsMatcher(std::vector< Node > & pats, QuantifiersEngine* qe):
1150     d_reset_done(false){
1151     Assert(pats.size() > 0);
1152     for( size_t i=0; i< pats.size(); i++ ){
1153       d_patterns.push_back(mkPattern(pats[i],qe));
1154     };
1155   };
1156   void resetInstantiationRound( QuantifiersEngine* qe ){
1157     for( size_t i=0; i< d_patterns.size(); i++ ){
1158       d_patterns[i]->resetInstantiationRound( qe );
1159     };
1160     d_reset_done = false;
1161     d_im.clear();
1162   };
1163   bool getNextMatch( QuantifiersEngine* qe ){
1164     Assert(d_patterns.size()>0);
1165     if(d_reset_done) return getNextMatch(qe,false);
1166     else return reset(qe);
1167   }
1168   const InstMatch& getInstMatch(){return d_im;};
1169
1170   int addInstantiations( InstMatch& baseMatch, Node quant, QuantifiersEngine* qe);
1171 };
1172
1173 enum EffiStep{
1174   ES_STOP,
1175   ES_GET_MONO_CANDIDATE,
1176   ES_GET_MULTI_CANDIDATE,
1177   ES_RESET1,
1178   ES_RESET2,
1179   ES_NEXT1,
1180   ES_NEXT2,
1181   ES_RESET_OTHER,
1182   ES_NEXT_OTHER,
1183 };
1184 static inline std::ostream& operator<<(std::ostream& out, const EffiStep& step) {
1185   switch(step){
1186   case ES_STOP: out << "STOP"; break;
1187   case ES_GET_MONO_CANDIDATE: out << "GET_MONO_CANDIDATE"; break;
1188   case ES_GET_MULTI_CANDIDATE: out << "GET_MULTI_CANDIDATE"; break;
1189   case ES_RESET1: out << "RESET1"; break;
1190   case ES_RESET2: out << "RESET2"; break;
1191   case ES_NEXT1: out << "NEXT1"; break;
1192   case ES_NEXT2: out << "NEXT2"; break;
1193   case ES_RESET_OTHER: out << "RESET_OTHER"; break;
1194   case ES_NEXT_OTHER: out << "NEXT_OTHER"; break;
1195   }
1196   return out;
1197 }
1198
1199
1200 int MultiPatsMatcher::addInstantiations( InstMatch& baseMatch, Node quant, QuantifiersEngine* qe){
1201   //now, try to add instantiation for each match produced
1202   int addedLemmas = 0;
1203   resetInstantiationRound( qe );
1204   d_im.add( baseMatch );
1205   while( getNextMatch( qe ) ){
1206     InstMatch im_copy = getInstMatch();
1207     //m.makeInternal( d_quantEngine->getEqualityQuery() );
1208     if( qe->addInstantiation( quant, im_copy ) ){
1209       addedLemmas++;
1210     }
1211   }
1212   //return number of lemmas added
1213   return addedLemmas;
1214 }
1215
1216 PatsMatcher* mkPatterns( std::vector< Node > pat, QuantifiersEngine* qe ){
1217   return new MultiPatsMatcher( pat, qe);
1218 }
1219
1220 class MultiEfficientPatsMatcher: public PatsMatcher{
1221 private:
1222   bool d_phase_mono;
1223   bool d_phase_new_term;
1224   std::vector< PatMatcher* > d_patterns;
1225   std::vector< Matcher* > d_direct_patterns;
1226   InstMatch d_im;
1227   uf::EfficientHandler d_eh;
1228   uf::EfficientHandler::MultiCandidate d_mc;
1229   InstMatchTrie2Pairs<true> d_cache;
1230   std::vector<Node> d_pats;
1231   // bool indexDone( size_t i){
1232   //   return i == d_c.first.second ||
1233   //     ( i == d_c.second.second && d_c.second.first.empty());
1234   // }
1235
1236
1237
1238   static const EffiStep ES_START = ES_GET_MONO_CANDIDATE;
1239   EffiStep d_step;
1240
1241   //return true if it becomes bigger than d_patterns.size() - 1
1242   bool incrIndex(size_t & index){
1243     if(index == d_patterns.size() - 1) return true;
1244     ++index;
1245     if(index == d_mc.first.second
1246        || (!d_phase_mono && index == d_mc.second.second))
1247       return incrIndex(index);
1248     else return false;
1249   }
1250
1251   //return true if it becomes smaller than 0
1252   bool decrIndex(size_t & index){
1253     if(index == 0) return true;
1254     --index;
1255     if(index == d_mc.first.second
1256        || (!d_phase_mono && index == d_mc.second.second))
1257       return decrIndex(index);
1258     else return false;
1259   }
1260
1261   bool resetOther( QuantifiersEngine* qe ){
1262     return getNextMatchOther(qe,true);
1263   };
1264
1265
1266   bool getNextMatchOther(QuantifiersEngine* qe, bool reset){
1267     size_t index = reset ? 0 : d_patterns.size();
1268     if(!reset && decrIndex(index)) return false;
1269     if( reset &&
1270         (index == d_mc.first.second
1271          || (!d_phase_mono && index == d_mc.second.second))
1272         && incrIndex(index)) return true;
1273     while(true){
1274       Debug("matching") << "MultiEfficientPatsMatcher::index " << index << "/"
1275                         << d_patterns.size() - 1 << std::endl;
1276       if(reset ?
1277          d_patterns[index]->reset( d_im, qe ) :
1278          d_patterns[index]->getNextMatch( d_im, qe )){
1279         if(incrIndex(index)) return true;
1280         reset=true;
1281       }else{
1282         if(decrIndex(index)) return false;
1283         reset=false;
1284       };
1285     }
1286   }
1287
1288   inline EffiStep TestMonoCache(QuantifiersEngine* qe){
1289     if( //!d_phase_new_term ||
1290        d_pats.size() == 1) return ES_RESET_OTHER;
1291     if(d_cache.addInstMatch(d_mc.first.second,d_im)){
1292       Debug("inst-match::cache") << "Cache miss" << d_im << std::endl;
1293       ++qe->d_statistics.d_mono_candidates_cache_miss;
1294       return ES_RESET_OTHER;
1295     } else {
1296       Debug("inst-match::cache") << "Cache hit" << d_im << std::endl;
1297       ++qe->d_statistics.d_mono_candidates_cache_hit;
1298       return ES_NEXT1;
1299     }
1300     // ++qe->d_statistics.d_mono_candidates_cache_miss;
1301     // return ES_RESET_OTHER;
1302   }
1303
1304   inline EffiStep TestMultiCache(QuantifiersEngine* qe){
1305     if(d_cache.addInstMatch(d_mc.first.second,d_mc.second.second,d_im)){
1306       ++qe->d_statistics.d_multi_candidates_cache_miss;
1307       return ES_RESET_OTHER;
1308     } else {
1309       ++qe->d_statistics.d_multi_candidates_cache_hit;
1310       return ES_NEXT2;
1311     }
1312   }
1313
1314
1315 public:
1316
1317   bool getNextMatch( QuantifiersEngine* qe ){
1318     Assert( d_step == ES_START || d_step == ES_NEXT_OTHER || d_step == ES_STOP );
1319     while(true){
1320       Debug("matching") << "d_step=" << d_step << " "
1321                         << "d_im=" << d_im << std::endl;
1322       switch(d_step){
1323       case ES_GET_MONO_CANDIDATE:
1324         Assert(d_im.empty());
1325         if(d_phase_new_term ? d_eh.getNextMonoCandidate(d_mc.first) : d_eh.getNextMonoCandidateNewTerm(d_mc.first)){
1326           if(d_phase_new_term) ++qe->d_statistics.d_num_mono_candidates_new_term;
1327           else ++qe->d_statistics.d_num_mono_candidates;
1328           d_phase_mono = true;
1329           d_step = ES_RESET1;
1330         } else if (!d_phase_new_term){
1331           d_phase_new_term = true;
1332           d_step = ES_GET_MONO_CANDIDATE;
1333         } else {
1334           d_phase_new_term = false;
1335           d_step = ES_GET_MULTI_CANDIDATE;
1336         }
1337         break;
1338       case ES_GET_MULTI_CANDIDATE:
1339         Assert(d_im.empty());
1340         if(d_eh.getNextMultiCandidate(d_mc)){
1341           ++qe->d_statistics.d_num_multi_candidates;
1342           d_phase_mono = false;
1343           d_step = ES_RESET1;
1344         } else d_step = ES_STOP;
1345         break;
1346       case ES_RESET1:
1347         if(d_direct_patterns[d_mc.first.second]->reset(d_mc.first.first,d_im,qe))
1348           d_step = d_phase_mono ? TestMonoCache(qe) : ES_RESET2;
1349         else d_step = d_phase_mono ? ES_GET_MONO_CANDIDATE : ES_GET_MULTI_CANDIDATE;
1350         break;
1351       case ES_RESET2:
1352         Assert(!d_phase_mono);
1353         if(d_direct_patterns[d_mc.second.second]->reset(d_mc.second.first,d_im,qe))
1354           d_step = TestMultiCache(qe);
1355         else d_step = ES_NEXT1;
1356         break;
1357       case ES_NEXT1:
1358         if(d_direct_patterns[d_mc.first.second]->getNextMatch(d_im,qe))
1359           d_step = d_phase_mono ? TestMonoCache(qe) : ES_RESET2;
1360         else d_step = d_phase_mono ? ES_GET_MONO_CANDIDATE : ES_GET_MULTI_CANDIDATE;
1361         break;
1362       case ES_NEXT2:
1363         if(d_direct_patterns[d_mc.second.second]->getNextMatch(d_im,qe))
1364           d_step = TestMultiCache(qe);
1365         else d_step = ES_NEXT1;
1366         break;
1367       case ES_RESET_OTHER:
1368         if(resetOther(qe)){
1369           d_step = ES_NEXT_OTHER;
1370           return true;
1371         } else d_step = d_phase_mono ? ES_NEXT1 : ES_NEXT2;
1372         break;
1373       case ES_NEXT_OTHER:
1374         {
1375           if(!getNextMatchOther(qe,false)){
1376             d_step = d_phase_mono ? ES_NEXT1 : ES_NEXT2;
1377           }else{
1378             d_step = ES_NEXT_OTHER;
1379             return true;
1380           }
1381         }
1382         break;
1383       case ES_STOP:
1384         Assert(d_im.empty());
1385         return false;
1386       }
1387     }
1388   }
1389
1390   MultiEfficientPatsMatcher(std::vector< Node > & pats, QuantifiersEngine* qe):
1391     d_eh(qe->getTheoryEngine()->getSatContext()),
1392     d_cache(qe->getTheoryEngine()->getSatContext(),qe,pats.size()),
1393     d_pats(pats), d_step(ES_START) {
1394     Assert(pats.size() > 0);
1395     for( size_t i=0; i< pats.size(); i++ ){
1396       d_patterns.push_back(mkPattern(pats[i],qe));
1397       if(pats[i].getKind()==kind::INST_CONSTANT){
1398         d_direct_patterns.push_back(new VarMatcher(pats[i],qe));
1399       } else if( pats[i].getKind() == kind::NOT && pats[i][0].getKind() == kind::EQUAL){
1400         d_direct_patterns.push_back(new ApplyMatcher(pats[i][0],qe));
1401       } else {
1402         d_direct_patterns.push_back(new ApplyMatcher(pats[i],qe));
1403       }
1404     };
1405     Theory* th_uf = qe->getTheoryEngine()->getTheory( theory::THEORY_UF );
1406     uf::InstantiatorTheoryUf* ith = (uf::InstantiatorTheoryUf*)th_uf->getInstantiator();
1407     ith->registerEfficientHandler(d_eh, pats);
1408   };
1409   void resetInstantiationRound( QuantifiersEngine* qe ){
1410     Assert(d_step == ES_START || d_step == ES_STOP);
1411     for( size_t i=0; i< d_patterns.size(); i++ ){
1412       d_patterns[i]->resetInstantiationRound( qe );
1413       d_direct_patterns[i]->resetInstantiationRound( qe );
1414     };
1415     d_step = ES_START;
1416     d_phase_new_term = false;
1417     Assert(d_im.empty());
1418   };
1419
1420   const InstMatch& getInstMatch(){return d_im;};
1421
1422   int addInstantiations( InstMatch& baseMatch, Node quant, QuantifiersEngine* qe);
1423 };
1424
1425 int MultiEfficientPatsMatcher::addInstantiations( InstMatch& baseMatch, Node quant, QuantifiersEngine* qe){
1426   //now, try to add instantiation for each match produced
1427   int addedLemmas = 0;
1428   Assert(baseMatch.empty());
1429   resetInstantiationRound( qe );
1430   while( getNextMatch( qe ) ){
1431     InstMatch im_copy = getInstMatch();
1432     //m.makeInternal( d_quantEngine->getEqualityQuery() );
1433     if( qe->addInstantiation( quant, im_copy ) ){
1434       addedLemmas++;
1435     }
1436   }
1437   //return number of lemmas added
1438   return addedLemmas;
1439 };
1440
1441 PatsMatcher* mkPatternsEfficient( std::vector< Node > pat, QuantifiersEngine* qe ){
1442   return new MultiEfficientPatsMatcher( pat, qe);
1443 }
1444
1445 } /* CVC4::theory::rrinst */
1446 } /* CVC4::theory */
1447 } /* CVC4 */