src/theory/rr_inst_match_impl.h

   1 /*********************                                                        */
   2 /*! \file rr_inst_match_impl.h
   3  ** \verbatim
   4  ** Original author: bobot
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): ajreynol, 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 inst match class
  15  **/
  16
  17 #include "cvc4_private.h"
  18
  19 #ifndef __CVC4__RR_INST_MATCH_IMPL_H
  20 #define __CVC4__RR_INST_MATCH_IMPL_H
  21
  22 #include "theory/rr_inst_match.h"
  23 #include "theory/theory_engine.h"
  24 #include "theory/quantifiers_engine.h"
  25 #include "theory/rr_candidate_generator.h"
  26 #include "theory/uf/equality_engine.h"
  27
  28 namespace CVC4 {
  29 namespace theory {
  30 namespace rrinst {
  31
  32 template<bool modEq>
  33 InstMatchTrie2Gen<modEq>::InstMatchTrie2Gen(context::Context* c,  QuantifiersEngine* qe):
  34   d_context(c), d_mods(c) {
  35   d_eQ = qe->getEqualityQuery();
  36   d_cG = qe->getRRCanGenClass();
  37 };
  38
  39 /** add match m for quantifier f starting at index, take into account equalities q, return true if successful */
  40 template<bool modEq>
  41 void InstMatchTrie2Gen<modEq>::addSubTree( Tree * root, mapIter current, mapIter end, size_t currLevel ) {
  42   if( current == end ) return;
  43
  44   Assert(root->e.find(current->second) == root->e.end());
  45   Tree * root2 = new Tree(currLevel);
  46   root->e.insert(std::make_pair(current->second, root2));
  47   addSubTree(root2, ++current, end, currLevel );
  48 }
  49
  50 /** exists match */
  51 template<bool modEq>
  52 bool InstMatchTrie2Gen<modEq>::existsInstMatch(InstMatchTrie2Gen<modEq>::Tree * root,
  53                                             mapIter & current, mapIter & end,
  54                                             Tree * & e, mapIter & diverge) const{
  55   if( current == end ) {
  56     Debug("Trie2") << "Trie2 Bottom " << std::endl;
  57     --current;
  58     return true;
  59   }; //Already their
  60
  61   if (current->first > diverge->first){
  62     // this point is the deepest point currently seen map are ordered
  63     e = root;
  64     diverge = current;
  65   };
  66
  67   TNode n = current->second;
  68   typename InstMatchTrie2Gen<modEq>::Tree::MLevel::iterator it =
  69     root->e.find( n );
  70   if( it!=root->e.end() &&
  71       existsInstMatch( (*it).second, ++current, end, e, diverge) ){
  72     Debug("Trie2") << "Trie2 Directly here " << n << std::endl;
  73     --current;
  74     return true;
  75   }
  76   Assert( it==root->e.end() || e != root );
  77
  78   // Even if n is in the trie others of the equivalence class
  79   // can also be in it since the equality can have appeared
  80   // after they have been added
  81   if( modEq && d_eQ->hasTerm( n ) ){
  82     //check modulo equality if any other instantiation match exists
  83     d_cG->reset( d_eQ->getRepresentative( n ) );
  84     for(TNode en = d_cG->getNextCandidate() ; !en.isNull() ;
  85         en = d_cG->getNextCandidate() ){
  86       if( en == n ) continue; // already tested
  87       typename InstMatchTrie2Gen<modEq>::Tree::MLevel::iterator itc =
  88         root->e.find( en );
  89       if( itc!=root->e.end() &&
  90           existsInstMatch( (*itc).second, ++current, end, e, diverge) ){
  91         Debug("Trie2") << "Trie2 Indirectly here by equality " << n << " = " << en << std::endl;
  92         --current;
  93         return true;
  94       }
  95       Assert( itc==root->e.end() || e != root );
  96     }
  97   }
  98   --current;
  99   return false;
 100 }
 101
 102 template<bool modEq>
 103 bool InstMatchTrie2Gen<modEq>::
 104 addInstMatch( InstMatch& m, InstMatchTrie2Gen<modEq>::Tree* e ) {
 105   d_cG->resetInstantiationRound();
 106  mapIter begin = m.begin();
 107  mapIter end = m.end();
 108  mapIter diverge = begin;
 109  if( !existsInstMatch(e, begin, end, e, diverge ) ){
 110    Assert(!diverge->second.isNull());
 111    size_t currLevel = d_context->getLevel();
 112    addSubTree( e, diverge, end, currLevel );
 113    if(e->level != currLevel)
 114      //If same level that e, will be removed at the same time than e
 115      d_mods.push_back(std::make_pair(e,diverge->second));
 116    return true;
 117  }else{
 118    return false;
 119  }
 120 }
 121
 122 }/* CVC4::theory::rrinst namespace */
 123
 124 }/* CVC4::theory namespace */
 125
 126 }/* CVC4 namespace */
 127
 128 #endif /*  __CVC4__RR_INST_MATCH_IMPL_H */