src/theory/quantifiers/term_database.cpp

   1 /*********************                                                        */
   2 /*! \file term_database.cpp
   3  ** \verbatim
   4  ** Original author: Andrew Reynolds
   5  ** Major contributors: Francois Bobot
   6  ** Minor contributors (to current version): Morgan Deters
   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 term databse class
  13  **/
  14
  15 #include "theory/quantifiers/term_database.h"
  16 #include "theory/quantifiers_engine.h"
  17 #include "theory/quantifiers/trigger.h"
  18 #include "theory/theory_engine.h"
  19 #include "theory/quantifiers/first_order_model.h"
  20 #include "theory/quantifiers/options.h"
  21 #include "theory/quantifiers/theory_quantifiers.h"
  22
  23 using namespace std;
  24 using namespace CVC4;
  25 using namespace CVC4::kind;
  26 using namespace CVC4::context;
  27 using namespace CVC4::theory;
  28 using namespace CVC4::theory::quantifiers;
  29
  30 using namespace CVC4::theory::inst;
  31
  32 bool TermArgTrie::addTerm2( QuantifiersEngine* qe, Node n, int argIndex ){
  33   if( argIndex<(int)n.getNumChildren() ){
  34     Node r = qe->getEqualityQuery()->getRepresentative( n[ argIndex ] );
  35     std::map< Node, TermArgTrie >::iterator it = d_data.find( r );
  36     if( it==d_data.end() ){
  37       d_data[r].addTerm2( qe, n, argIndex+1 );
  38       return true;
  39     }else{
  40       return it->second.addTerm2( qe, n, argIndex+1 );
  41     }
  42   }else{
  43     //store n in d_data (this should be interpretted as the "data" and not as a reference to a child)
  44     d_data[n].d_data.clear();
  45     return false;
  46   }
  47 }
  48
  49 TermDb::TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ) : d_quantEngine( qe ), d_op_ccount( u ) {
  50
  51 }
  52
  53 /** ground terms */
  54 unsigned TermDb::getNumGroundTerms( Node f ) {
  55   std::map< Node, std::vector< Node > >::iterator it = d_op_map.find( f );
  56   if( it!=d_op_map.end() ){
  57     return it->second.size();
  58   }else{
  59     return 0;
  60   }
  61   //return d_op_ccount[f];
  62 }
  63
  64 Node TermDb::getOperator( Node n ) {
  65   //return n.getOperator();
  66
  67   if( n.getKind()==SELECT || n.getKind()==STORE ){
  68     //since it is parametric, use a particular one as op
  69     TypeNode tn1 = n[0].getType();
  70     TypeNode tn2 = n[1].getType();
  71     Node op = n.getOperator();
  72     std::map< Node, std::map< TypeNode, std::map< TypeNode, Node > > >::iterator ito = d_par_op_map.find( op );
  73     if( ito!=d_par_op_map.end() ){
  74       std::map< TypeNode, std::map< TypeNode, Node > >::iterator it = ito->second.find( tn1 );
  75       if( it!=ito->second.end() ){
  76         std::map< TypeNode, Node >::iterator it2 = it->second.find( tn2 );
  77         if( it2!=it->second.end() ){
  78           return it2->second;
  79         }
  80       }
  81     }
  82     d_par_op_map[op][tn1][tn2] = n;
  83     return n;
  84   }else if( n.getKind()==APPLY_UF ){
  85     return n.getOperator();
  86   }else{
  87     return Node::null();
  88   }
  89 }
  90
  91 void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
  92   //don't add terms in quantifier bodies
  93   if( withinQuant && !options::registerQuantBodyTerms() ){
  94     return;
  95   }
  96   if( d_processed.find( n )==d_processed.end() ){
  97     d_processed.insert(n);
  98     d_type_map[ n.getType() ].push_back( n );
  99     //if this is an atomic trigger, consider adding it
 100     //Call the children?
 101     if( inst::Trigger::isAtomicTrigger( n ) ){
 102       if( !TermDb::hasInstConstAttr(n) ){
 103         Trace("term-db") << "register term in db " << n << std::endl;
 104         //std::cout << "register trigger term " << n << std::endl;
 105         Node op = getOperator( n );
 106         /*
 107         int occ = d_op_ccount[op];
 108         if( occ<(int)d_op_map[op].size() ){
 109           d_op_map[op][occ] = n;
 110         }else{
 111           d_op_map[op].push_back( n );
 112         }
 113         d_op_ccount[op].set( occ + 1 );
 114         */
 115         d_op_map[op].push_back( n );
 116         added.insert( n );
 117
 118         for( size_t i=0; i<n.getNumChildren(); i++ ){
 119           addTerm( n[i], added, withinQuant );
 120           if( options::eagerInstQuant() ){
 121             if( !n.hasAttribute(InstLevelAttribute()) && n.getAttribute(InstLevelAttribute())==0 ){
 122               int addedLemmas = 0;
 123               for( size_t i=0; i<d_op_triggers[op].size(); i++ ){
 124                 addedLemmas += d_op_triggers[op][i]->addTerm( n );
 125               }
 126               //Message() << "Terms, added lemmas: " << addedLemmas << std::endl;
 127               d_quantEngine->flushLemmas( &d_quantEngine->getOutputChannel() );
 128             }
 129           }
 130         }
 131       }
 132     }else{
 133       for( int i=0; i<(int)n.getNumChildren(); i++ ){
 134         addTerm( n[i], added, withinQuant );
 135       }
 136     }
 137   }
 138 }
 139
 140  void TermDb::reset( Theory::Effort effort ){
 141    int nonCongruentCount = 0;
 142    int congruentCount = 0;
 143    int alreadyCongruentCount = 0;
 144    //rebuild d_func/pred_map_trie for each operation, this will calculate all congruent terms
 145    for( std::map< Node, std::vector< Node > >::iterator it = d_op_map.begin(); it != d_op_map.end(); ++it ){
 146      d_op_nonred_count[ it->first ] = 0;
 147      if( !it->second.empty() ){
 148        if( it->second[0].getType().isBoolean() ){
 149          d_pred_map_trie[ 0 ][ it->first ].d_data.clear();
 150          d_pred_map_trie[ 1 ][ it->first ].d_data.clear();
 151        }else{
 152          d_func_map_trie[ it->first ].d_data.clear();
 153          for( int i=0; i<(int)it->second.size(); i++ ){
 154            Node n = it->second[i];
 155            computeModelBasisArgAttribute( n );
 156            if( !n.getAttribute(NoMatchAttribute()) ){
 157              if( !d_func_map_trie[ it->first ].addTerm( d_quantEngine, n ) ){
 158                NoMatchAttribute nma;
 159                n.setAttribute(nma,true);
 160                Debug("term-db-cong") << n << " is redundant." << std::endl;
 161                congruentCount++;
 162              }else{
 163                nonCongruentCount++;
 164                d_op_nonred_count[ it->first ]++;
 165              }
 166            }else{
 167              congruentCount++;
 168              alreadyCongruentCount++;
 169            }
 170          }
 171        }
 172      }
 173    }
 174    for( int i=0; i<2; i++ ){
 175      Node n = NodeManager::currentNM()->mkConst( i==1 );
 176      if( d_quantEngine->getEqualityQuery()->getEngine()->hasTerm( n ) ){
 177        eq::EqClassIterator eqc( d_quantEngine->getEqualityQuery()->getEngine()->getRepresentative( n ),
 178                                 d_quantEngine->getEqualityQuery()->getEngine() );
 179        while( !eqc.isFinished() ){
 180          Node en = (*eqc);
 181          computeModelBasisArgAttribute( en );
 182          if( en.getKind()==APPLY_UF && !TermDb::hasInstConstAttr(en) ){
 183            if( !en.getAttribute(NoMatchAttribute()) ){
 184              Node op = getOperator( en );
 185              if( !d_pred_map_trie[i][op].addTerm( d_quantEngine, en ) ){
 186                NoMatchAttribute nma;
 187                en.setAttribute(nma,true);
 188                Debug("term-db-cong") << en << " is redundant." << std::endl;
 189                congruentCount++;
 190              }else{
 191                nonCongruentCount++;
 192                d_op_nonred_count[ op ]++;
 193              }
 194            }else{
 195              alreadyCongruentCount++;
 196            }
 197          }
 198          ++eqc;
 199        }
 200      }
 201    }
 202    Debug("term-db-cong") << "TermDb: Reset" << std::endl;
 203    Debug("term-db-cong") << "Congruent/Non-Congruent = ";
 204    Debug("term-db-cong") << congruentCount << "(" << alreadyCongruentCount << ") / " << nonCongruentCount << std::endl;
 205 }
 206
 207 Node TermDb::getModelBasisTerm( TypeNode tn, int i ){
 208   if( d_model_basis_term.find( tn )==d_model_basis_term.end() ){
 209     Node mbt;
 210     if( tn.isInteger() || tn.isReal() ){
 211       mbt = NodeManager::currentNM()->mkConst( Rational( 0 ) );
 212     }else if( !tn.isSort() ){
 213       mbt = tn.mkGroundTerm();
 214     }else{
 215       if( options::fmfFreshDistConst() || d_type_map[ tn ].empty() ){
 216         std::stringstream ss;
 217         ss << Expr::setlanguage(options::outputLanguage());
 218         ss << "e_" << tn;
 219         mbt = NodeManager::currentNM()->mkSkolem( ss.str(), tn, "is a model basis term" );
 220         Trace("mkVar") << "ModelBasis:: Make variable " << mbt << " : " << tn << std::endl;
 221       }else{
 222         mbt = d_type_map[ tn ][ 0 ];
 223       }
 224     }
 225     ModelBasisAttribute mba;
 226     mbt.setAttribute(mba,true);
 227     d_model_basis_term[tn] = mbt;
 228     Trace("model-basis-term") << "Choose " << mbt << " as model basis term for " << tn << std::endl;
 229   }
 230   return d_model_basis_term[tn];
 231 }
 232
 233 Node TermDb::getModelBasisOpTerm( Node op ){
 234   if( d_model_basis_op_term.find( op )==d_model_basis_op_term.end() ){
 235     TypeNode t = op.getType();
 236     std::vector< Node > children;
 237     children.push_back( op );
 238     for( int i=0; i<(int)(t.getNumChildren()-1); i++ ){
 239       children.push_back( getModelBasisTerm( t[i] ) );
 240     }
 241     if( children.size()==1 ){
 242       d_model_basis_op_term[op] = op;
 243     }else{
 244       d_model_basis_op_term[op] = NodeManager::currentNM()->mkNode( APPLY_UF, children );
 245     }
 246   }
 247   return d_model_basis_op_term[op];
 248 }
 249
 250 Node TermDb::getModelBasis( Node f, Node n ){
 251   //make model basis
 252   if( d_model_basis_terms.find( f )==d_model_basis_terms.end() ){
 253     for( int j=0; j<(int)f[0].getNumChildren(); j++ ){
 254       d_model_basis_terms[f].push_back( getModelBasisTerm( f[0][j].getType() ) );
 255     }
 256   }
 257   Node gn = n.substitute( d_inst_constants[f].begin(), d_inst_constants[f].end(),
 258                           d_model_basis_terms[f].begin(), d_model_basis_terms[f].end() );
 259   return gn;
 260 }
 261
 262 Node TermDb::getModelBasisBody( Node f ){
 263   if( d_model_basis_body.find( f )==d_model_basis_body.end() ){
 264     Node n = getInstConstantBody( f );
 265     d_model_basis_body[f] = getModelBasis( f, n );
 266   }
 267   return d_model_basis_body[f];
 268 }
 269
 270 void TermDb::computeModelBasisArgAttribute( Node n ){
 271   if( !n.hasAttribute(ModelBasisArgAttribute()) ){
 272     //ensure that the model basis terms have been defined
 273     if( n.getKind()==APPLY_UF ){
 274       getModelBasisOpTerm( n.getOperator() );
 275     }
 276     uint64_t val = 0;
 277     //determine if it has model basis attribute
 278     for( int j=0; j<(int)n.getNumChildren(); j++ ){
 279       if( n[j].getAttribute(ModelBasisAttribute()) ){
 280         val++;
 281       }
 282     }
 283     ModelBasisArgAttribute mbaa;
 284     n.setAttribute( mbaa, val );
 285   }
 286 }
 287
 288 void TermDb::makeInstantiationConstantsFor( Node f ){
 289   if( d_inst_constants.find( f )==d_inst_constants.end() ){
 290     Debug("quantifiers-engine") << "Instantiation constants for " << f << " : " << std::endl;
 291     for( int i=0; i<(int)f[0].getNumChildren(); i++ ){
 292       d_vars[f].push_back( f[0][i] );
 293       //make instantiation constants
 294       Node ic = NodeManager::currentNM()->mkInstConstant( f[0][i].getType() );
 295       d_inst_constants_map[ic] = f;
 296       d_inst_constants[ f ].push_back( ic );
 297       Debug("quantifiers-engine") << "  " << ic << std::endl;
 298       //set the var number attribute
 299       InstVarNumAttribute ivna;
 300       ic.setAttribute(ivna,i);
 301       InstConstantAttribute ica;
 302       ic.setAttribute(ica,f);
 303       //also set the no-match attribute
 304       NoMatchAttribute nma;
 305       ic.setAttribute(nma,true);
 306     }
 307   }
 308 }
 309
 310
 311 Node TermDb::getInstConstAttr( Node n ) {
 312   if (!n.hasAttribute(InstConstantAttribute()) ){
 313     Node f;
 314     for( int i=0; i<(int)n.getNumChildren(); i++ ){
 315       f = getInstConstAttr(n[i]);
 316       if( !f.isNull() ){
 317         break;
 318       }
 319     }
 320     InstConstantAttribute ica;
 321     n.setAttribute(ica,f);
 322     if( !f.isNull() ){
 323       //also set the no-match attribute
 324       NoMatchAttribute nma;
 325       n.setAttribute(nma,true);
 326     }
 327   }
 328   return n.getAttribute(InstConstantAttribute());
 329 }
 330
 331 bool TermDb::hasInstConstAttr( Node n ) {
 332   return !getInstConstAttr(n).isNull();
 333 }
 334
 335 void TermDb::getBoundVars( Node n, std::vector< Node >& bvs) {
 336   if (n.getKind()==BOUND_VARIABLE ){
 337     if ( std::find( bvs.begin(), bvs.end(), n)==bvs.end() ){
 338       bvs.push_back( n );
 339     }
 340   }else{
 341     for( unsigned i=0; i<n.getNumChildren(); i++) {
 342       getBoundVars(n[i], bvs);
 343     }
 344   }
 345 }
 346
 347
 348 /** get the i^th instantiation constant of f */
 349 Node TermDb::getInstantiationConstant( Node f, int i ) const {
 350   std::map< Node, std::vector< Node > >::const_iterator it = d_inst_constants.find( f );
 351   if( it!=d_inst_constants.end() ){
 352     return it->second[i];
 353   }else{
 354     return Node::null();
 355   }
 356 }
 357
 358 /** get number of instantiation constants for f */
 359 int TermDb::getNumInstantiationConstants( Node f ) const {
 360   std::map< Node, std::vector< Node > >::const_iterator it = d_inst_constants.find( f );
 361   if( it!=d_inst_constants.end() ){
 362     return (int)it->second.size();
 363   }else{
 364     return 0;
 365   }
 366 }
 367
 368 Node TermDb::getInstConstantBody( Node f ){
 369   std::map< Node, Node >::iterator it = d_inst_const_body.find( f );
 370   if( it==d_inst_const_body.end() ){
 371     makeInstantiationConstantsFor( f );
 372     Node n = getInstConstantNode( f[1], f );
 373     d_inst_const_body[ f ] = n;
 374     return n;
 375   }else{
 376     return it->second;
 377   }
 378 }
 379
 380 Node TermDb::getCounterexampleLiteral( Node f ){
 381   if( d_ce_lit.find( f )==d_ce_lit.end() ){
 382     Node ceBody = getInstConstantBody( f );
 383     //check if any variable are of bad types, and fail if so
 384     for( size_t i=0; i<d_inst_constants[f].size(); i++ ){
 385       if( d_inst_constants[f][i].getType().isBoolean() ){
 386         d_ce_lit[ f ] = Node::null();
 387         return Node::null();
 388       }
 389     }
 390     //otherwise, ensure literal
 391     Node ceLit = d_quantEngine->getValuation().ensureLiteral( ceBody.notNode() );
 392     d_ce_lit[ f ] = ceLit;
 393   }
 394   return d_ce_lit[ f ];
 395 }
 396
 397 Node TermDb::getInstConstantNode( Node n, Node f ){
 398   return convertNodeToPattern(n,f,d_vars[f],d_inst_constants[ f ]);
 399 }
 400
 401 Node TermDb::convertNodeToPattern( Node n, Node f, const std::vector<Node> & vars,
 402                                               const std::vector<Node> & inst_constants){
 403   Node n2 = n.substitute( vars.begin(), vars.end(),
 404                           inst_constants.begin(),
 405                           inst_constants.end() );
 406   return n2;
 407 }
 408
 409
 410
 411 Node TermDb::getSkolemizedBody( Node f ){
 412   Assert( f.getKind()==FORALL );
 413   if( d_skolem_body.find( f )==d_skolem_body.end() ){
 414     std::vector< Node > vars;
 415     for( int i=0; i<(int)f[0].getNumChildren(); i++ ){
 416       Node skv = NodeManager::currentNM()->mkSkolem( "skv", f[0][i].getType(), "is a termdb-created skolemized body" );
 417       d_skolem_constants[ f ].push_back( skv );
 418       vars.push_back( f[0][i] );
 419       //carry information for sort inference
 420       if( options::sortInference() ){
 421         d_quantEngine->getTheoryEngine()->getSortInference()->setSkolemVar( f, f[0][i], skv );
 422       }
 423     }
 424     d_skolem_body[ f ] = f[ 1 ].substitute( vars.begin(), vars.end(),
 425                                             d_skolem_constants[ f ].begin(), d_skolem_constants[ f ].end() );
 426   }
 427   return d_skolem_body[ f ];
 428 }
 429
 430 Node TermDb::getFreeVariableForInstConstant( Node n ){
 431   TypeNode tn = n.getType();
 432   if( d_free_vars.find( tn )==d_free_vars.end() ){
 433         for( unsigned i=0; i<d_type_map[ tn ].size(); i++ ){
 434           if( !quantifiers::TermDb::hasInstConstAttr(d_type_map[ tn ][ i ]) ){
 435             d_free_vars[tn] = d_type_map[ tn ][ i ];
 436           }
 437         }
 438         if( d_free_vars.find( tn )==d_free_vars.end() ){
 439       //if integer or real, make zero
 440       if( tn.isInteger() || tn.isReal() ){
 441         Rational z(0);
 442         d_free_vars[tn] = NodeManager::currentNM()->mkConst( z );
 443       }else{
 444             d_free_vars[tn] = NodeManager::currentNM()->mkSkolem( "freevar", tn, "is a free variable created by termdb" );
 445             Trace("mkVar") << "FreeVar:: Make variable " << d_free_vars[tn] << " : " << tn << std::endl;
 446       }
 447     }
 448   }
 449   return d_free_vars[tn];
 450 }
 451
 452 const std::vector<Node> & TermDb::getParents(TNode n, TNode f, int arg){
 453   std::hash_map< Node, std::hash_map< Node, std::hash_map< int, std::vector< Node > >,NodeHashFunction  >,NodeHashFunction  >::const_iterator
 454     rn = d_parents.find( n );
 455   if( rn !=d_parents.end() ){
 456     std::hash_map< Node, std::hash_map< int, std::vector< Node > > , NodeHashFunction  > ::const_iterator
 457       rf = rn->second.find(f);
 458     if( rf != rn->second.end() ){
 459       std::hash_map< int, std::vector< Node > > ::const_iterator
 460         ra = rf->second.find(arg);
 461       if( ra != rf->second.end() ){
 462         return ra->second;
 463       }
 464     }
 465   }
 466   static std::vector<Node> empty;
 467   return empty;
 468 }
 469
 470 void TermDb::computeVarContains( Node n ) {
 471   if( d_var_contains.find( n )==d_var_contains.end() ){
 472     d_var_contains[n].clear();
 473     computeVarContains2( n, n );
 474   }
 475 }
 476
 477 void TermDb::computeVarContains2( Node n, Node parent ){
 478   if( n.getKind()==INST_CONSTANT ){
 479     if( std::find( d_var_contains[parent].begin(), d_var_contains[parent].end(), n )==d_var_contains[parent].end() ){
 480       d_var_contains[parent].push_back( n );
 481     }
 482   }else{
 483     for( int i=0; i<(int)n.getNumChildren(); i++ ){
 484       computeVarContains2( n[i], parent );
 485     }
 486   }
 487 }
 488
 489 bool TermDb::isVariableSubsume( Node n1, Node n2 ){
 490   if( n1==n2 ){
 491     return true;
 492   }else{
 493     //Notice() << "is variable subsume ? " << n1 << " " << n2 << std::endl;
 494     computeVarContains( n1 );
 495     computeVarContains( n2 );
 496     for( int i=0; i<(int)d_var_contains[n2].size(); i++ ){
 497       if( std::find( d_var_contains[n1].begin(), d_var_contains[n1].end(), d_var_contains[n2][i] )==d_var_contains[n1].end() ){
 498         //Notice() << "no" << std::endl;
 499         return false;
 500       }
 501     }
 502     //Notice() << "yes" << std::endl;
 503     return true;
 504   }
 505 }
 506
 507 void TermDb::getVarContains( Node f, std::vector< Node >& pats, std::map< Node, std::vector< Node > >& varContains ){
 508   for( int i=0; i<(int)pats.size(); i++ ){
 509     computeVarContains( pats[i] );
 510     varContains[ pats[i] ].clear();
 511     for( int j=0; j<(int)d_var_contains[pats[i]].size(); j++ ){
 512       if( d_var_contains[pats[i]][j].getAttribute(InstConstantAttribute())==f ){
 513         varContains[ pats[i] ].push_back( d_var_contains[pats[i]][j] );
 514       }
 515     }
 516   }
 517 }
 518
 519 void TermDb::getVarContainsNode( Node f, Node n, std::vector< Node >& varContains ){
 520   computeVarContains( n );
 521   for( int j=0; j<(int)d_var_contains[n].size(); j++ ){
 522     if( d_var_contains[n][j].getAttribute(InstConstantAttribute())==f ){
 523       varContains.push_back( d_var_contains[n][j] );
 524     }
 525   }
 526 }
 527
 528 /** is n1 an instance of n2 or vice versa? */
 529 int TermDb::isInstanceOf( Node n1, Node n2 ){
 530   if( n1==n2 ){
 531     return 1;
 532   }else if( n1.getKind()==n2.getKind() ){
 533     if( n1.getKind()==APPLY_UF ){
 534       if( n1.getOperator()==n2.getOperator() ){
 535         int result = 0;
 536         for( int i=0; i<(int)n1.getNumChildren(); i++ ){
 537           if( n1[i]!=n2[i] ){
 538             int cResult = isInstanceOf( n1[i], n2[i] );
 539             if( cResult==0 ){
 540               return 0;
 541             }else if( cResult!=result ){
 542               if( result!=0 ){
 543                 return 0;
 544               }else{
 545                 result = cResult;
 546               }
 547             }
 548           }
 549         }
 550         return result;
 551       }
 552     }
 553     return 0;
 554   }else if( n2.getKind()==INST_CONSTANT ){
 555     computeVarContains( n1 );
 556     //if( std::find( d_var_contains[ n1 ].begin(), d_var_contains[ n1 ].end(), n2 )!=d_var_contains[ n1 ].end() ){
 557     //  return 1;
 558     //}
 559     if( d_var_contains[ n1 ].size()==1 && d_var_contains[ n1 ][ 0 ]==n2 ){
 560       return 1;
 561     }
 562   }else if( n1.getKind()==INST_CONSTANT ){
 563     computeVarContains( n2 );
 564     //if( std::find( d_var_contains[ n2 ].begin(), d_var_contains[ n2 ].end(), n1 )!=d_var_contains[ n2 ].end() ){
 565     //  return -1;
 566     //}
 567     if( d_var_contains[ n2 ].size()==1 && d_var_contains[ n2 ][ 0 ]==n1 ){
 568       return 1;
 569     }
 570   }
 571   return 0;
 572 }
 573
 574 bool TermDb::isUnifiableInstanceOf( Node n1, Node n2, std::map< Node, Node >& subs ){
 575   if( n1==n2 ){
 576     return true;
 577   }else if( n2.getKind()==INST_CONSTANT ){
 578     //if( !node_contains( n1, n2 ) ){
 579     //  return false;
 580     //}
 581     if( subs.find( n2 )==subs.end() ){
 582       subs[n2] = n1;
 583     }else if( subs[n2]!=n1 ){
 584       return false;
 585     }
 586     return true;
 587   }else if( n1.getKind()==n2.getKind() && n1.getMetaKind()==kind::metakind::PARAMETERIZED ){
 588     if( n1.getOperator()!=n2.getOperator() ){
 589       return false;
 590     }
 591     for( int i=0; i<(int)n1.getNumChildren(); i++ ){
 592       if( !isUnifiableInstanceOf( n1[i], n2[i], subs ) ){
 593         return false;
 594       }
 595     }
 596     return true;
 597   }else{
 598     return false;
 599   }
 600 }
 601
 602 void TermDb::filterInstances( std::vector< Node >& nodes ){
 603   std::vector< bool > active;
 604   active.resize( nodes.size(), true );
 605   for( int i=0; i<(int)nodes.size(); i++ ){
 606     for( int j=i+1; j<(int)nodes.size(); j++ ){
 607       if( active[i] && active[j] ){
 608         int result = isInstanceOf( nodes[i], nodes[j] );
 609         if( result==1 ){
 610           Trace("filter-instances") << nodes[j] << " is an instance of " << nodes[i] << std::endl;
 611           active[j] = false;
 612         }else if( result==-1 ){
 613           Trace("filter-instances") << nodes[i] << " is an instance of " << nodes[j] << std::endl;
 614           active[i] = false;
 615         }
 616       }
 617     }
 618   }
 619   std::vector< Node > temp;
 620   for( int i=0; i<(int)nodes.size(); i++ ){
 621     if( active[i] ){
 622       temp.push_back( nodes[i] );
 623     }
 624   }
 625   nodes.clear();
 626   nodes.insert( nodes.begin(), temp.begin(), temp.end() );
 627 }
 628
 629 void TermDb::registerTrigger( theory::inst::Trigger* tr, Node op ){
 630   if( std::find( d_op_triggers[op].begin(), d_op_triggers[op].end(), tr )==d_op_triggers[op].end() ){
 631     d_op_triggers[op].push_back( tr );
 632   }
 633 }
 634
 635 bool TermDb::isRewriteRule( Node q ) {
 636   return !getRewriteRule( q ).isNull();
 637 }
 638
 639 Node TermDb::getRewriteRule( Node q ) {
 640   if( q.getKind()==FORALL && q.getNumChildren()==3 && q[2].getNumChildren()>0 && q[2][0][0].getKind()==REWRITE_RULE ){
 641     return q[2][0][0];
 642   }else{
 643     return Node::null();
 644   }
 645 }