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): Kshitij Bansal, Francois Bobot, Clark Barrett
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2014  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( TNode 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::getTerms( QuantifiersEngine* qe, Node f, std::vector< Node >& inst ){
 131   for( size_t i=0; i<f[0].getNumChildren(); i++ ){
 132     Node val = get( i );
 133     if( val.isNull() ){
 134       Node ic =  qe->getTermDatabase()->getInstantiationConstant( f, i );
 135       val = qe->getTermDatabase()->getFreeVariableForInstConstant( ic );
 136     }
 137     inst.push_back( val );
 138   }
 139 }
 140
 141 void InstMatch::setValue( int i, TNode n ) {
 142   d_vals[i] = n;
 143 }
 144
 145 bool InstMatch::set( QuantifiersEngine* qe, int i, TNode n ) {
 146   if( !d_vals[i].isNull() ){
 147     if( qe->getEqualityQuery()->areEqual( d_vals[i], n ) ){
 148       return true;
 149     }else{
 150       return false;
 151     }
 152   }else{
 153     d_vals[i] = n;
 154     return true;
 155   }
 156 }
 157
 158 bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq,
 159                                   bool modInst, ImtIndexOrder* imtio, bool onlyExist, int index ) {
 160   if( index==(int)f[0].getNumChildren() || ( imtio && index==(int)imtio->d_order.size() ) ){
 161     return false;
 162   }else{
 163     int i_index = imtio ? imtio->d_order[index] : index;
 164     Node n = m[i_index];
 165     std::map< Node, InstMatchTrie >::iterator it = d_data.find( n );
 166     if( it!=d_data.end() ){
 167       bool ret = it->second.addInstMatch( qe, f, m, modEq, modInst, imtio, onlyExist, index+1 );
 168       if( !onlyExist || !ret ){
 169         return ret;
 170       }
 171     }
 172     /*
 173     //check if m is an instance of another instantiation if modInst is true
 174     if( modInst ){
 175       if( !n.isNull() ){
 176         Node nl;
 177         std::map< Node, InstMatchTrie >::iterator itm = d_data.find( nl );
 178         if( itm!=d_data.end() ){
 179           if( !itm->second.addInstMatch( qe, f, m, modEq, modInst, imtio, true, index+1 ) ){
 180             return false;
 181           }
 182         }
 183       }
 184     }
 185     */
 186     if( modEq ){
 187       //check modulo equality if any other instantiation match exists
 188       if( !n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){
 189         eq::EqClassIterator eqc( qe->getEqualityQuery()->getEngine()->getRepresentative( n ),
 190                                  qe->getEqualityQuery()->getEngine() );
 191         while( !eqc.isFinished() ){
 192           Node en = (*eqc);
 193           if( en!=n ){
 194             std::map< Node, InstMatchTrie >::iterator itc = d_data.find( en );
 195             if( itc!=d_data.end() ){
 196               if( itc->second.addInstMatch( qe, f, m, modEq, modInst, imtio, true, index+1 ) ){
 197                 return false;
 198               }
 199             }
 200           }
 201           ++eqc;
 202         }
 203       }
 204     }
 205     if( !onlyExist ){
 206       d_data[n].addInstMatch( qe, f, m, modEq, modInst, imtio, false, index+1 );
 207     }
 208     return true;
 209   }
 210 }
 211
 212 void InstMatchTrie::print( std::ostream& out, Node q, std::vector< TNode >& terms ) const {
 213   if( terms.size()==q[0].getNumChildren() ){
 214     out << "  ( ";
 215     for( unsigned i=0; i<terms.size(); i++ ){
 216       if( i>0 ){ out << ", ";}
 217       out << terms[i];
 218     }
 219     out << " )" << std::endl;
 220   }else{
 221     for( std::map< Node, InstMatchTrie >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){
 222       terms.push_back( it->first );
 223       it->second.print( out, q, terms );
 224       terms.pop_back();
 225     }
 226   }
 227 }
 228
 229
 230 bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m,
 231                                     context::Context* c, bool modEq, bool modInst, int index, bool onlyExist ){
 232   bool reset = false;
 233   if( !d_valid.get() ){
 234     if( onlyExist ){
 235       return true;
 236     }else{
 237       d_valid.set( true );
 238       reset = true;
 239     }
 240   }
 241   if( index==(int)f[0].getNumChildren() ){
 242     return reset;
 243   }else{
 244     Node n = m[ index ];
 245     std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n );
 246     if( it!=d_data.end() ){
 247       bool ret = it->second->addInstMatch( qe, f, m, c, modEq, modInst, index+1, onlyExist );
 248       if( !onlyExist || !ret ){
 249         return reset || ret;
 250       }
 251     }
 252     //check if m is an instance of another instantiation if modInst is true
 253     /*
 254     if( modInst ){
 255       if( !n.isNull() ){
 256         Node nl;
 257         std::map< Node, CDInstMatchTrie* >::iterator itm = d_data.find( nl );
 258         if( itm!=d_data.end() ){
 259           if( !itm->second->addInstMatch( qe, f, m, c, modEq, modInst, index+1, true ) ){
 260             return false;
 261           }
 262         }
 263       }
 264     }
 265     */
 266     if( modEq ){
 267       //check modulo equality if any other instantiation match exists
 268       if( !n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){
 269         eq::EqClassIterator eqc( qe->getEqualityQuery()->getEngine()->getRepresentative( n ),
 270                                  qe->getEqualityQuery()->getEngine() );
 271         while( !eqc.isFinished() ){
 272           Node en = (*eqc);
 273           if( en!=n ){
 274             std::map< Node, CDInstMatchTrie* >::iterator itc = d_data.find( en );
 275             if( itc!=d_data.end() ){
 276               if( itc->second->addInstMatch( qe, f, m, c, modEq, modInst, index+1, true ) ){
 277                 return false;
 278               }
 279             }
 280           }
 281           ++eqc;
 282         }
 283       }
 284     }
 285
 286     if( !onlyExist ){
 287       // std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n );
 288       CDInstMatchTrie* imt = new CDInstMatchTrie( c );
 289       d_data[n] = imt;
 290       imt->addInstMatch( qe, f, m, c, modEq, modInst, index+1, false );
 291     }
 292     return true;
 293   }
 294 }
 295
 296 void CDInstMatchTrie::print( std::ostream& out, Node q, std::vector< TNode >& terms ) const{
 297   if( d_valid.get() ){
 298     if( terms.size()==q[0].getNumChildren() ){
 299       out << "  ( ";
 300       for( unsigned i=0; i<terms.size(); i++ ){
 301         if( i>0 ) out << ", ";
 302         out << terms[i];
 303       }
 304       out << " )" << std::endl;
 305     }else{
 306       for( std::map< Node, CDInstMatchTrie* >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){
 307         terms.push_back( it->first );
 308         it->second->print( out, q, terms );
 309         terms.pop_back();
 310       }
 311     }
 312   }
 313 }
 314
 315 }/* CVC4::theory::inst namespace */
 316 }/* CVC4::theory namespace */
 317 }/* CVC4 namespace */