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 void InstMatch::set(TNode var, TNode n){
 138   Assert( !var.isNull() );
 139   if( !n.isNull() &&// For a strange use in inst_match.cpp InstMatchGeneratorSimple::addInstantiations
 140         //var.getType() == n.getType()
 141         !n.getType().isSubtypeOf( var.getType() ) ){
 142     Trace("inst-match-warn") << var.getAttribute(InstConstantAttribute()) << std::endl;
 143     Trace("inst-match-warn") << var << " " << var.getType() << n << " " << n.getType() << std::endl ;
 144     Assert(false);
 145   }
 146   d_map[var] = n;
 147 }
 148
 149 /** add match m for quantifier f starting at index, take into account equalities q, return true if successful */
 150 void InstMatchTrie::addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, int index, ImtIndexOrder* imtio ){
 151   if( long(index)<long(f[0].getNumChildren()) && ( !imtio || long(index)<long(imtio->d_order.size()) ) ){
 152     int i_index = imtio ? imtio->d_order[index] : index;
 153     Node n = m.getValue( qe->getTermDatabase()->getInstantiationConstant( f, i_index ) );
 154     d_data[n].addInstMatch2( qe, f, m, index+1, imtio );
 155   }
 156 }
 157
 158 /** exists match */
 159 bool InstMatchTrie::existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, int index, ImtIndexOrder* imtio ){
 160   if( long(index)==long(f[0].getNumChildren()) || ( imtio && long(index)==long(imtio->d_order.size()) ) ){
 161     return true;
 162   }else{
 163     int i_index = imtio ? imtio->d_order[index] : index;
 164     Node n = m.getValue( qe->getTermDatabase()->getInstantiationConstant( f, i_index ) );
 165     std::map< Node, InstMatchTrie >::iterator it = d_data.find( n );
 166     if( it!=d_data.end() ){
 167       if( it->second.existsInstMatch2( qe, f, m, modEq, modInst, index+1, imtio ) ){
 168         return true;
 169       }
 170     }
 171     //check if m is an instance of another instantiation if modInst is true
 172     if( modInst ){
 173       if( !n.isNull() ){
 174         Node nl;
 175         it = d_data.find( nl );
 176         if( it!=d_data.end() ){
 177           if( it->second.existsInstMatch2( qe, f, m, modEq, modInst, index+1, imtio ) ){
 178             return true;
 179           }
 180         }
 181       }
 182     }
 183     if( modEq ){
 184       //check modulo equality if any other instantiation match exists
 185       if( !n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){
 186         eq::EqClassIterator eqc( qe->getEqualityQuery()->getEngine()->getRepresentative( n ),
 187                                  qe->getEqualityQuery()->getEngine() );
 188         while( !eqc.isFinished() ){
 189           Node en = (*eqc);
 190           if( en!=n ){
 191             std::map< Node, InstMatchTrie >::iterator itc = d_data.find( en );
 192             if( itc!=d_data.end() ){
 193               if( itc->second.existsInstMatch2( qe, f, m, modEq, modInst, index+1, imtio ) ){
 194                 return true;
 195               }
 196             }
 197           }
 198           ++eqc;
 199         }
 200       }
 201     }
 202     return false;
 203   }
 204 }
 205
 206 bool InstMatchTrie::existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, ImtIndexOrder* imtio ){
 207   return existsInstMatch2( qe, f, m, modEq, modInst, 0, imtio );
 208 }
 209
 210 bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, ImtIndexOrder* imtio ){
 211   if( !existsInstMatch( qe, f, m, modEq, modInst, imtio ) ){
 212     addInstMatch2( qe, f, m, 0, imtio );
 213     return true;
 214   }else{
 215     return false;
 216   }
 217 }
 218
 219
 220 }/* CVC4::theory::inst namespace */
 221 }/* CVC4::theory namespace */
 222 }/* CVC4 namespace */