src/theory/quantifiers/inst_match.cpp

   1 /*********************                                                        */
   2 /*! \file inst_match.cpp
   3  ** \verbatim
   4  ** Original author: Morgan Deters
   5  ** Major contributors: Andrew Reynolds
   6  ** Minor contributors (to current version): Clark Barrett, Francois Bobot
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2013  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( Node f ) {
  31   for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
  32     d_vals.push_back( Node::null() );
  33   }
  34 }
  35
  36 InstMatch::InstMatch( InstMatch* m ) {
  37   d_vals.insert( d_vals.end(), m->d_vals.begin(), m->d_vals.end() );
  38 }
  39
  40 bool InstMatch::add( InstMatch& m ){
  41   for( unsigned i=0; i<d_vals.size(); i++ ){
  42     if( d_vals[i].isNull() ){
  43       d_vals[i] = m.d_vals[i];
  44     }
  45   }
  46   return true;
  47 }
  48
  49 bool InstMatch::merge( EqualityQuery* q, InstMatch& m ){
  50   for( unsigned i=0; i<m.d_vals.size(); i++ ){
  51     if( !m.d_vals[i].isNull() ){
  52       if( d_vals[i].isNull() ){
  53         d_vals[i] = m.d_vals[i];
  54       }else{
  55         if( !q->areEqual( d_vals[i], m.d_vals[i]) ){
  56           clear();
  57           return false;
  58         }
  59       }
  60     }
  61   }
  62   return true;
  63 }
  64
  65 void InstMatch::debugPrint( const char* c ){
  66   for( unsigned i=0; i<d_vals.size(); i++ ){
  67     if( !d_vals[i].isNull() ){
  68       Debug( c ) << "   " << i << " -> " << d_vals[i] << std::endl;
  69     }
  70   }
  71 }
  72
  73 bool InstMatch::isComplete() {
  74   for( unsigned i=0; i<d_vals.size(); i++ ){
  75     if( d_vals[i].isNull() ){
  76       return false;
  77     }
  78   }
  79   return true;
  80 }
  81
  82 bool InstMatch::empty() {
  83   for( unsigned i=0; i<d_vals.size(); i++ ){
  84     if( !d_vals[i].isNull() ){
  85       return false;
  86     }
  87   }
  88   return true;
  89 }
  90
  91 void InstMatch::makeComplete( Node f, QuantifiersEngine* qe ){
  92   for( unsigned i=0; i<d_vals.size(); i++ ){
  93     if( d_vals[i].isNull() ){
  94       Node ic = qe->getTermDatabase()->getInstantiationConstant( f, i );
  95       d_vals[i] = qe->getTermDatabase()->getFreeVariableForInstConstant( ic );
  96     }
  97   }
  98 }
  99
 100 void InstMatch::makeRepresentative( QuantifiersEngine* qe ){
 101   for( unsigned i=0; i<d_vals.size(); i++ ){
 102     if( !d_vals[i].isNull() ){
 103       if( qe->getEqualityQuery()->getEngine()->hasTerm( d_vals[i] ) ){
 104         d_vals[i] = qe->getEqualityQuery()->getEngine()->getRepresentative( d_vals[i] );
 105       }
 106     }
 107   }
 108 }
 109
 110 void InstMatch::applyRewrite(){
 111   for( unsigned i=0; i<d_vals.size(); i++ ){
 112     if( !d_vals[i].isNull() ){
 113       d_vals[i] = Rewriter::rewrite( d_vals[i] );
 114     }
 115   }
 116 }
 117
 118 void InstMatch::clear() {
 119   for( unsigned i=0; i<d_vals.size(); i++ ){
 120     d_vals[i] = Node::null();
 121   }
 122 }
 123
 124 /** get value */
 125
 126 Node InstMatch::get( int i ) {
 127   return d_vals[i];
 128 }
 129
 130 void InstMatch::setValue( int i, TNode n ) {
 131   d_vals[i] = n;
 132 }
 133
 134 bool InstMatch::set( QuantifiersEngine* qe, int i, TNode n ) {
 135   if( !d_vals[i].isNull() ){
 136     if( qe->getEqualityQuery()->areEqual( d_vals[i], n ) ){
 137       return true;
 138     }else{
 139       return false;
 140     }
 141   }else{
 142     d_vals[i] = n;
 143     return true;
 144   }
 145 }
 146
 147 bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq,
 148                                   bool modInst, ImtIndexOrder* imtio, bool onlyExist, int index ) {
 149   if( index==(int)f[0].getNumChildren() || ( imtio && index==(int)imtio->d_order.size() ) ){
 150     return false;
 151   }else{
 152     int i_index = imtio ? imtio->d_order[index] : index;
 153     Node n = m[i_index];
 154     std::map< Node, InstMatchTrie >::iterator it = d_data.find( n );
 155     if( it!=d_data.end() ){
 156       bool ret = it->second.addInstMatch( qe, f, m, modEq, modInst, imtio, onlyExist, index+1 );
 157       if( !onlyExist || !ret ){
 158         return ret;
 159       }
 160     }
 161     /*
 162     //check if m is an instance of another instantiation if modInst is true
 163     if( modInst ){
 164       if( !n.isNull() ){
 165         Node nl;
 166         std::map< Node, InstMatchTrie >::iterator itm = d_data.find( nl );
 167         if( itm!=d_data.end() ){
 168           if( !itm->second.addInstMatch( qe, f, m, modEq, modInst, imtio, true, index+1 ) ){
 169             return false;
 170           }
 171         }
 172       }
 173     }
 174     */
 175     if( modEq ){
 176       //check modulo equality if any other instantiation match exists
 177       if( !n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){
 178         eq::EqClassIterator eqc( qe->getEqualityQuery()->getEngine()->getRepresentative( n ),
 179                                  qe->getEqualityQuery()->getEngine() );
 180         while( !eqc.isFinished() ){
 181           Node en = (*eqc);
 182           if( en!=n ){
 183             std::map< Node, InstMatchTrie >::iterator itc = d_data.find( en );
 184             if( itc!=d_data.end() ){
 185               if( itc->second.addInstMatch( qe, f, m, modEq, modInst, imtio, true, index+1 ) ){
 186                 return false;
 187               }
 188             }
 189           }
 190           ++eqc;
 191         }
 192       }
 193     }
 194     if( !onlyExist ){
 195       d_data[n].addInstMatch( qe, f, m, modEq, modInst, imtio, false, index+1 );
 196     }
 197     return true;
 198   }
 199 }
 200
 201 void InstMatchTrie::print( const char * c, Node q, std::vector< Node >& terms ) const {
 202   if( terms.size()==q[0].getNumChildren() ){
 203     Trace(c) << "  ( ";
 204     for( unsigned i=0; i<terms.size(); i++ ){
 205       if( i>0 ) Trace(c) << ", ";
 206       Trace(c) << terms[i];
 207     }
 208     Trace(c) << " )" << std::endl;
 209   }else{
 210     for( std::map< Node, InstMatchTrie >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){
 211       terms.push_back( it->first );
 212       it->second.print( c, q, terms );
 213       terms.pop_back();
 214     }
 215   }
 216 }
 217
 218
 219 bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m,
 220                                     context::Context* c, bool modEq, bool modInst, int index, bool onlyExist ){
 221   bool reset = false;
 222   if( !d_valid.get() ){
 223     if( onlyExist ){
 224       return true;
 225     }else{
 226       d_valid.set( true );
 227       reset = true;
 228     }
 229   }
 230   if( index==(int)f[0].getNumChildren() ){
 231     return reset;
 232   }else{
 233     Node n = m[ index ];
 234     std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n );
 235     if( it!=d_data.end() ){
 236       bool ret = it->second->addInstMatch( qe, f, m, c, modEq, modInst, index+1, onlyExist );
 237       if( !onlyExist || !ret ){
 238         return reset || ret;
 239       }
 240     }
 241     //check if m is an instance of another instantiation if modInst is true
 242     /*
 243     if( modInst ){
 244       if( !n.isNull() ){
 245         Node nl;
 246         std::map< Node, CDInstMatchTrie* >::iterator itm = d_data.find( nl );
 247         if( itm!=d_data.end() ){
 248           if( !itm->second->addInstMatch( qe, f, m, c, modEq, modInst, index+1, true ) ){
 249             return false;
 250           }
 251         }
 252       }
 253     }
 254     */
 255     if( modEq ){
 256       //check modulo equality if any other instantiation match exists
 257       if( !n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){
 258         eq::EqClassIterator eqc( qe->getEqualityQuery()->getEngine()->getRepresentative( n ),
 259                                  qe->getEqualityQuery()->getEngine() );
 260         while( !eqc.isFinished() ){
 261           Node en = (*eqc);
 262           if( en!=n ){
 263             std::map< Node, CDInstMatchTrie* >::iterator itc = d_data.find( en );
 264             if( itc!=d_data.end() ){
 265               if( itc->second->addInstMatch( qe, f, m, c, modEq, modInst, index+1, true ) ){
 266                 return false;
 267               }
 268             }
 269           }
 270           ++eqc;
 271         }
 272       }
 273     }
 274
 275     if( !onlyExist ){
 276       // std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n );
 277       CDInstMatchTrie* imt = new CDInstMatchTrie( c );
 278       d_data[n] = imt;
 279       imt->addInstMatch( qe, f, m, c, modEq, modInst, index+1, false );
 280     }
 281     return true;
 282   }
 283 }
 284
 285 void CDInstMatchTrie::print( const char * c, Node q, std::vector< Node >& terms ) const{
 286   if( d_valid.get() ){
 287     if( terms.size()==q[0].getNumChildren() ){
 288       Trace(c) << "  ( ";
 289       for( unsigned i=0; i<terms.size(); i++ ){
 290         if( i>0 ) Trace(c) << ", ";
 291         Trace(c) << terms[i];
 292       }
 293       Trace(c) << " )" << std::endl;
 294     }else{
 295       for( std::map< Node, CDInstMatchTrie* >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){
 296         terms.push_back( it->first );
 297         it->second->print( c, q, terms );
 298         terms.pop_back();
 299       }
 300     }
 301   }
 302 }
 303
 304 }/* CVC4::theory::inst namespace */
 305 }/* CVC4::theory namespace */
 306 }/* CVC4 namespace */