src/theory/quantifiers/inst_match.cpp

   1 /*********************                                                        */
   2 /*! \file inst_match.cpp
   3  ** \verbatim
   4  ** Original author: ajreynol
   5  ** Major contributors: bobot
   6  ** Minor contributors (to current version): barrett, mdeters
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009-2012  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief Implementation of inst match class
  13  **/
  14
  15 #include "theory/quantifiers/inst_match.h"
  16 #include "theory/quantifiers/term_database.h"
  17 #include "theory/quantifiers/quant_util.h"
  18 #include "theory/quantifiers_engine.h"
  19
  20 using namespace std;
  21 using namespace CVC4;
  22 using namespace CVC4::kind;
  23 using namespace CVC4::context;
  24 using namespace CVC4::theory;
  25
  26 namespace CVC4 {
  27 namespace theory {
  28 namespace inst {
  29
  30 InstMatch::InstMatch() {
  31 }
  32
  33 InstMatch::InstMatch( InstMatch* m ) {
  34   d_map = m->d_map;
  35 }
  36
  37 bool InstMatch::setMatch( EqualityQuery* q, TNode v, TNode m, bool & set ){
  38   std::map< Node, Node >::iterator vn = d_map.find( v );
  39   if( vn==d_map.end() || vn->second.isNull() ){
  40     set = true;
  41     this->set(v,m);
  42     Debug("matching-debug") << "Add partial " << v << "->" << m << std::endl;
  43     return true;
  44   }else{
  45     set = false;
  46     return q->areEqual( vn->second, m );
  47   }
  48 }
  49
  50 bool InstMatch::setMatch( EqualityQuery* q, TNode v, TNode m ){
  51   bool set;
  52   return setMatch(q,v,m,set);
  53 }
  54
  55 bool InstMatch::add( InstMatch& m ){
  56   for( std::map< Node, Node >::iterator it = m.d_map.begin(); it != m.d_map.end(); ++it ){
  57     if( !it->second.isNull() ){
  58       std::map< Node, Node >::iterator itf = d_map.find( it->first );
  59       if( itf==d_map.end() || itf->second.isNull() ){
  60         d_map[it->first] = it->second;
  61       }
  62     }
  63   }
  64   return true;
  65 }
  66
  67 bool InstMatch::merge( EqualityQuery* q, InstMatch& m ){
  68   for( std::map< Node, Node >::iterator it = m.d_map.begin(); it != m.d_map.end(); ++it ){
  69     if( !it->second.isNull() ){
  70       std::map< Node, Node >::iterator itf = d_map.find( it->first );
  71       if( itf==d_map.end() || itf->second.isNull() ){
  72         d_map[ it->first ] = it->second;
  73       }else{
  74         if( !q->areEqual( it->second, itf->second ) ){
  75           d_map.clear();
  76           return false;
  77         }
  78       }
  79     }
  80   }
  81   return true;
  82 }
  83
  84 void InstMatch::debugPrint( const char* c ){
  85   for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){
  86     Debug( c ) << "   " << it->first << " -> " << it->second << std::endl;
  87   }
  88   //if( !d_splits.empty() ){
  89   //  Debug( c ) << "   Conditions: ";
  90   //  for( std::map< Node, Node >::iterator it = d_splits.begin(); it !=d_splits.end(); ++it ){
  91   //    Debug( c ) << it->first << " = " << it->second << " ";
  92   //  }
  93   //  Debug( c ) << std::endl;
  94   //}
  95 }
  96
  97 void InstMatch::makeComplete( Node f, QuantifiersEngine* qe ){
  98   for( size_t i=0; i<f[0].getNumChildren(); i++ ){
  99     Node ic = qe->getTermDatabase()->getInstantiationConstant( f, i );
 100     if( d_map.find( ic )==d_map.end() ){
 101       d_map[ ic ] = qe->getTermDatabase()->getFreeVariableForInstConstant( ic );
 102     }
 103   }
 104 }
 105
 106 void InstMatch::makeInternalRepresentative( QuantifiersEngine* qe ){
 107   EqualityQueryQuantifiersEngine* eqqe = (EqualityQueryQuantifiersEngine*)qe->getEqualityQuery();
 108   for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){
 109     d_map[ it->first ] = eqqe->getInternalRepresentative( it->second );
 110   }
 111 }
 112
 113 void InstMatch::makeRepresentative( QuantifiersEngine* qe ){
 114   for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){
 115     if( qe->getEqualityQuery()->getEngine()->hasTerm( it->second ) ){
 116       d_map[ it->first ] = qe->getEqualityQuery()->getEngine()->getRepresentative( it->second );
 117     }
 118   }
 119 }
 120
 121 void InstMatch::applyRewrite(){
 122   for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){
 123     it->second = Rewriter::rewrite(it->second);
 124   }
 125 }
 126
 127 /** get value */
 128 Node InstMatch::getValue( Node var ) const{
 129   std::map< Node, Node >::const_iterator it = d_map.find( var );
 130   if( it!=d_map.end() ){
 131     return it->second;
 132   }else{
 133     return Node::null();
 134   }
 135 }
 136
 137 /** add match m for quantifier f starting at index, take into account equalities q, return true if successful */
 138 void InstMatchTrie::addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, int index, ImtIndexOrder* imtio ){
 139   if( long(index)<long(f[0].getNumChildren()) && ( !imtio || long(index)<long(imtio->d_order.size()) ) ){
 140     int i_index = imtio ? imtio->d_order[index] : index;
 141     Node n = m.getValue( qe->getTermDatabase()->getInstantiationConstant( f, i_index ) );
 142     d_data[n].addInstMatch2( qe, f, m, index+1, imtio );
 143   }
 144 }
 145
 146 /** exists match */
 147 bool InstMatchTrie::existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, int index, ImtIndexOrder* imtio ){
 148   if( long(index)==long(f[0].getNumChildren()) || ( imtio && long(index)==long(imtio->d_order.size()) ) ){
 149     return true;
 150   }else{
 151     int i_index = imtio ? imtio->d_order[index] : index;
 152     Node n = m.getValue( qe->getTermDatabase()->getInstantiationConstant( f, i_index ) );
 153     std::map< Node, InstMatchTrie >::iterator it = d_data.find( n );
 154     if( it!=d_data.end() ){
 155       if( it->second.existsInstMatch2( qe, f, m, modEq, modInst, index+1, imtio ) ){
 156         return true;
 157       }
 158     }
 159     //check if m is an instance of another instantiation if modInst is true
 160     if( modInst ){
 161       if( !n.isNull() ){
 162         Node nl;
 163         it = d_data.find( nl );
 164         if( it!=d_data.end() ){
 165           if( it->second.existsInstMatch2( qe, f, m, modEq, modInst, index+1, imtio ) ){
 166             return true;
 167           }
 168         }
 169       }
 170     }
 171     if( modEq ){
 172       //check modulo equality if any other instantiation match exists
 173       if( !n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){
 174         eq::EqClassIterator eqc( qe->getEqualityQuery()->getEngine()->getRepresentative( n ),
 175                                  qe->getEqualityQuery()->getEngine() );
 176         while( !eqc.isFinished() ){
 177           Node en = (*eqc);
 178           if( en!=n ){
 179             std::map< Node, InstMatchTrie >::iterator itc = d_data.find( en );
 180             if( itc!=d_data.end() ){
 181               if( itc->second.existsInstMatch2( qe, f, m, modEq, modInst, index+1, imtio ) ){
 182                 return true;
 183               }
 184             }
 185           }
 186           ++eqc;
 187         }
 188       }
 189     }
 190     return false;
 191   }
 192 }
 193
 194 bool InstMatchTrie::existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, ImtIndexOrder* imtio ){
 195   return existsInstMatch2( qe, f, m, modEq, modInst, 0, imtio );
 196 }
 197
 198 bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, ImtIndexOrder* imtio ){
 199   if( !existsInstMatch( qe, f, m, modEq, modInst, imtio ) ){
 200     addInstMatch2( qe, f, m, 0, imtio );
 201     return true;
 202   }else{
 203     return false;
 204   }
 205 }
 206
 207
 208 }/* CVC4::theory::inst namespace */
 209 }/* CVC4::theory namespace */
 210 }/* CVC4 namespace */