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): Kshitij Bansal, Morgan Deters
   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 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 #include "util/datatype.h"
  23 #include "theory/datatypes/datatypes_rewriter.h"
  24
  25 using namespace std;
  26 using namespace CVC4;
  27 using namespace CVC4::kind;
  28 using namespace CVC4::context;
  29 using namespace CVC4::theory;
  30 using namespace CVC4::theory::quantifiers;
  31
  32 using namespace CVC4::theory::inst;
  33
  34 TNode TermArgTrie::existsTerm( std::vector< TNode >& reps, int argIndex ) {
  35   if( argIndex==(int)reps.size() ){
  36     if( d_data.empty() ){
  37       return Node::null();
  38     }else{
  39       return d_data.begin()->first;
  40     }
  41   }else{
  42     std::map< TNode, TermArgTrie >::iterator it = d_data.find( reps[argIndex] );
  43     if( it==d_data.end() ){
  44       return Node::null();
  45     }else{
  46       return it->second.existsTerm( reps, argIndex+1 );
  47     }
  48   }
  49 }
  50
  51 bool TermArgTrie::addTerm( TNode n, std::vector< TNode >& reps, int argIndex ){
  52   if( argIndex==(int)reps.size() ){
  53     if( d_data.empty() ){
  54       //store n in d_data (this should be interpretted as the "data" and not as a reference to a child)
  55       d_data[n].clear();
  56       return true;
  57     }else{
  58       return false;
  59     }
  60   }else{
  61     return d_data[reps[argIndex]].addTerm( n, reps, argIndex+1 );
  62   }
  63 }
  64
  65 void TermArgTrie::debugPrint( const char * c, Node n, unsigned depth ) {
  66   for( std::map< TNode, TermArgTrie >::iterator it = d_data.begin(); it != d_data.end(); ++it ){
  67     for( unsigned i=0; i<depth; i++ ){ Debug(c) << "  "; }
  68     Debug(c) << it->first << std::endl;
  69     it->second.debugPrint( c, n, depth+1 );
  70   }
  71 }
  72
  73 TermDb::TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ) : d_quantEngine( qe ), d_op_ccount( u ) {
  74   d_true = NodeManager::currentNM()->mkConst( true );
  75   d_false = NodeManager::currentNM()->mkConst( false );
  76 }
  77
  78 /** ground terms */
  79 unsigned TermDb::getNumGroundTerms( Node f ) {
  80   std::map< Node, std::vector< Node > >::iterator it = d_op_map.find( f );
  81   if( it!=d_op_map.end() ){
  82     return it->second.size();
  83   }else{
  84     return 0;
  85   }
  86   //return d_op_ccount[f];
  87 }
  88
  89 Node TermDb::getOperator( Node n ) {
  90   //return n.getOperator();
  91   Kind k = n.getKind();
  92   if( k==SELECT || k==STORE || k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON ){
  93     //since it is parametric, use a particular one as op
  94     TypeNode tn = n[0].getType();
  95     Node op = n.getOperator();
  96     std::map< Node, std::map< TypeNode, Node > >::iterator ito = d_par_op_map.find( op );
  97     if( ito!=d_par_op_map.end() ){
  98       std::map< TypeNode, Node >::iterator it = ito->second.find( tn );
  99       if( it!=ito->second.end() ){
 100         return it->second;
 101       }
 102     }
 103     d_par_op_map[op][tn] = n;
 104     return n;
 105   }else if( inst::Trigger::isAtomicTriggerKind( k ) ){
 106     return n.getOperator();
 107   }else{
 108     return Node::null();
 109   }
 110 }
 111
 112 void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
 113   //don't add terms in quantifier bodies
 114   if( withinQuant && !options::registerQuantBodyTerms() ){
 115     return;
 116   }
 117   if( d_processed.find( n )==d_processed.end() ){
 118     d_processed.insert(n);
 119     d_type_map[ n.getType() ].push_back( n );
 120     //if this is an atomic trigger, consider adding it
 121     //Call the children?
 122     if( inst::Trigger::isAtomicTrigger( n ) ){
 123       if( !TermDb::hasInstConstAttr(n) ){
 124         Trace("term-db") << "register term in db " << n << std::endl;
 125         //std::cout << "register trigger term " << n << std::endl;
 126         Node op = getOperator( n );
 127         /*
 128         int occ = d_op_ccount[op];
 129         if( occ<(int)d_op_map[op].size() ){
 130           d_op_map[op][occ] = n;
 131         }else{
 132           d_op_map[op].push_back( n );
 133         }
 134         d_op_ccount[op].set( occ + 1 );
 135         */
 136         d_op_map[op].push_back( n );
 137         added.insert( n );
 138
 139         for( size_t i=0; i<n.getNumChildren(); i++ ){
 140           addTerm( n[i], added, withinQuant );
 141           if( options::eagerInstQuant() ){
 142             if( !n.hasAttribute(InstLevelAttribute()) && n.getAttribute(InstLevelAttribute())==0 ){
 143               int addedLemmas = 0;
 144               for( size_t i=0; i<d_op_triggers[op].size(); i++ ){
 145                 addedLemmas += d_op_triggers[op][i]->addTerm( n );
 146               }
 147               //Message() << "Terms, added lemmas: " << addedLemmas << std::endl;
 148               d_quantEngine->flushLemmas( &d_quantEngine->getOutputChannel() );
 149             }
 150           }
 151         }
 152       }
 153     }else{
 154       for( int i=0; i<(int)n.getNumChildren(); i++ ){
 155         addTerm( n[i], added, withinQuant );
 156       }
 157     }
 158   }
 159 }
 160
 161 void TermDb::computeArgReps( TNode n ) {
 162   if( d_arg_reps.find( n )==d_arg_reps.end() ){
 163     eq::EqualityEngine * ee = d_quantEngine->getTheoryEngine()->getMasterEqualityEngine();
 164     for( unsigned j=0; j<n.getNumChildren(); j++ ){
 165       TNode r = ee->hasTerm( n[j] ) ? ee->getRepresentative( n[j] ) : n[j];
 166       d_arg_reps[n].push_back( r );
 167     }
 168   }
 169 }
 170
 171 void TermDb::computeUfEqcTerms( TNode f ) {
 172   if( d_func_map_eqc_trie.find( f )==d_func_map_eqc_trie.end() ){
 173     d_func_map_eqc_trie[f].clear();
 174     eq::EqualityEngine * ee = d_quantEngine->getTheoryEngine()->getMasterEqualityEngine();
 175     for( unsigned i=0; i<d_op_map[f].size(); i++ ){
 176       TNode n = d_op_map[f][i];
 177       if( !n.getAttribute(NoMatchAttribute()) ){
 178         computeArgReps( n );
 179         TNode r = ee->hasTerm( n ) ? ee->getRepresentative( n ) : n;
 180         d_func_map_eqc_trie[f].d_data[r].addTerm( n, d_arg_reps[n] );
 181       }
 182     }
 183   }
 184 }
 185
 186 TNode TermDb::evaluateTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep ) {
 187   Trace("term-db-eval") << "evaluate term : " << n << std::endl;
 188   eq::EqualityEngine * ee = d_quantEngine->getTheoryEngine()->getMasterEqualityEngine();
 189   if( ee->hasTerm( n ) ){
 190     Trace("term-db-eval") << "...exists in ee, return rep " << std::endl;
 191     return ee->getRepresentative( n );
 192   }else if( n.getKind()==BOUND_VARIABLE ){
 193     Assert( subs.find( n )!=subs.end() );
 194     Trace("term-db-eval") << "...substitution is : " << subs[n] << std::endl;
 195     if( subsRep ){
 196       Assert( ee->hasTerm( subs[n] ) );
 197       Assert( ee->getRepresentative( subs[n] )==subs[n] );
 198       return subs[n];
 199     }else{
 200       return evaluateTerm( subs[n], subs, subsRep );
 201     }
 202   }else{
 203     if( n.hasOperator() ){
 204       TNode f = getOperator( n );
 205       if( !f.isNull() ){
 206         std::vector< TNode > args;
 207         for( unsigned i=0; i<n.getNumChildren(); i++ ){
 208           TNode c = evaluateTerm( n[i], subs, subsRep );
 209           if( c.isNull() ){
 210             return TNode::null();
 211           }
 212           Trace("term-db-eval") << "Got child : " << c << std::endl;
 213           args.push_back( c );
 214         }
 215         Trace("term-db-eval") << "Get term from DB" << std::endl;
 216         TNode nn = d_func_map_trie[f].existsTerm( args );
 217         Trace("term-db-eval") << "Got term " << nn << std::endl;
 218         if( !nn.isNull() ){
 219           if( ee->hasTerm( nn ) ){
 220             Trace("term-db-eval") << "return rep " << std::endl;
 221             return ee->getRepresentative( nn );
 222           }else{
 223             //Assert( false );
 224           }
 225         }
 226       }
 227     }
 228     return TNode::null();
 229   }
 230 }
 231
 232 bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol ) {
 233   Trace("term-db-eval") << "Check entailed : " << n << ", pol = " << pol << std::endl;
 234   Assert( n.getType().isBoolean() );
 235   if( n.getKind()==EQUAL ){
 236     TNode n1 = evaluateTerm( n[0], subs, subsRep );
 237     if( !n1.isNull() ){
 238       TNode n2 = evaluateTerm( n[1], subs, subsRep );
 239       if( !n2.isNull() ){
 240         eq::EqualityEngine * ee = d_quantEngine->getTheoryEngine()->getMasterEqualityEngine();
 241         Assert( ee->hasTerm( n1 ) );
 242         Assert( ee->hasTerm( n2 ) );
 243         if( pol ){
 244           return ee->areEqual( n1, n2 );
 245         }else{
 246           return ee->areDisequal( n1, n2, false );
 247         }
 248       }
 249     }
 250   }else if( n.getKind()==APPLY_UF ){
 251     TNode n1 = evaluateTerm( n, subs, subsRep );
 252     if( !n1.isNull() ){
 253       eq::EqualityEngine * ee = d_quantEngine->getTheoryEngine()->getMasterEqualityEngine();
 254       Assert( ee->hasTerm( n1 ) );
 255       TNode n2 = pol ? d_true : d_false;
 256       if( ee->hasTerm( n2 ) ){
 257         return ee->areEqual( n1, n2 );
 258       }
 259     }
 260   }else if( n.getKind()==NOT ){
 261     return isEntailed( n[0], subs, subsRep, !pol );
 262   }else if( n.getKind()==OR || n.getKind()==AND ){
 263     for( unsigned i=0; i<n.getNumChildren(); i++ ){
 264       if( isEntailed( n[i], subs, subsRep, pol ) ){
 265         if( ( pol && n.getKind()==OR ) || ( !pol && n.getKind()==AND ) ){
 266           return true;
 267         }
 268       }else{
 269         if( ( !pol && n.getKind()==OR ) || ( pol && n.getKind()==AND ) ){
 270           return false;
 271         }
 272       }
 273     }
 274     return true;
 275   }else if( n.getKind()==IFF || n.getKind()==ITE ){
 276     for( unsigned i=0; i<2; i++ ){
 277       if( isEntailed( n[0], subs, subsRep, i==0 ) ){
 278         unsigned ch = ( n.getKind()==IFF || i==0 ) ? 1 : 2;
 279         bool reqPol = ( n.getKind()==ITE || i==0 ) ? pol : !pol;
 280         return isEntailed( n[ch], subs, subsRep, reqPol );
 281       }
 282     }
 283   }
 284   return false;
 285 }
 286
 287 void TermDb::reset( Theory::Effort effort ){
 288    int nonCongruentCount = 0;
 289    int congruentCount = 0;
 290    int alreadyCongruentCount = 0;
 291    d_op_nonred_count.clear();
 292    d_arg_reps.clear();
 293    d_func_map_trie.clear();
 294    d_func_map_eqc_trie.clear();
 295    //rebuild d_func/pred_map_trie for each operation, this will calculate all congruent terms
 296    for( std::map< Node, std::vector< Node > >::iterator it = d_op_map.begin(); it != d_op_map.end(); ++it ){
 297      d_op_nonred_count[ it->first ] = 0;
 298      if( !it->second.empty() ){
 299        for( unsigned i=0; i<it->second.size(); i++ ){
 300          Node n = it->second[i];
 301          computeModelBasisArgAttribute( n );
 302          if( !n.getAttribute(NoMatchAttribute()) ){
 303            computeArgReps( n );
 304            if( !d_func_map_trie[ it->first ].addTerm( n, d_arg_reps[n] ) ){
 305              NoMatchAttribute nma;
 306              n.setAttribute(nma,true);
 307              Debug("term-db-cong") << n << " is redundant." << std::endl;
 308              congruentCount++;
 309            }else{
 310              nonCongruentCount++;
 311              d_op_nonred_count[ it->first ]++;
 312            }
 313          }else{
 314            congruentCount++;
 315            alreadyCongruentCount++;
 316          }
 317        }
 318      }
 319    }
 320    Debug("term-db-cong") << "TermDb: Reset" << std::endl;
 321    Debug("term-db-cong") << "Congruent/Non-Congruent = ";
 322    Debug("term-db-cong") << congruentCount << "(" << alreadyCongruentCount << ") / " << nonCongruentCount << std::endl;
 323    if( Debug.isOn("term-db") ){
 324       Debug("term-db") << "functions : " << std::endl;
 325       for( std::map< Node, std::vector< Node > >::iterator it = d_op_map.begin(); it != d_op_map.end(); ++it ){
 326         if( it->second.size()>0 ){
 327           Debug("term-db") << "- " << it->first << std::endl;
 328           d_func_map_trie[ it->first ].debugPrint("term-db", it->second[0]);
 329         }
 330       }
 331    }
 332 }
 333
 334 TermArgTrie * TermDb::getTermArgTrie( Node f ) {
 335   std::map< Node, TermArgTrie >::iterator itut = d_func_map_trie.find( f );
 336   if( itut!=d_func_map_trie.end() ){
 337     return &itut->second;
 338   }else{
 339     return NULL;
 340   }
 341 }
 342
 343 TermArgTrie * TermDb::getTermArgTrie( Node eqc, Node f ) {
 344   computeUfEqcTerms( f );
 345   std::map< Node, TermArgTrie >::iterator itut = d_func_map_eqc_trie.find( f );
 346   if( itut==d_func_map_eqc_trie.end() ){
 347     return NULL;
 348   }else{
 349     if( eqc.isNull() ){
 350       return &itut->second;
 351     }else{
 352       std::map< TNode, TermArgTrie >::iterator itute = itut->second.d_data.find( eqc );
 353       if( itute!=itut->second.d_data.end() ){
 354         return &itute->second;
 355       }else{
 356         return NULL;
 357       }
 358     }
 359   }
 360 }
 361
 362 TNode TermDb::existsTerm( Node f, Node n ) {
 363   computeArgReps( n );
 364   return d_func_map_trie[f].existsTerm( d_arg_reps[n] );
 365 }
 366
 367 Node TermDb::getModelBasisTerm( TypeNode tn, int i ){
 368   if( d_model_basis_term.find( tn )==d_model_basis_term.end() ){
 369     Node mbt;
 370     if( tn.isInteger() || tn.isReal() ){
 371       mbt = NodeManager::currentNM()->mkConst( Rational( 0 ) );
 372     }else if( !tn.isSort() ){
 373       mbt = tn.mkGroundTerm();
 374     }else{
 375       if( options::fmfFreshDistConst() || d_type_map[ tn ].empty() ){
 376         std::stringstream ss;
 377         ss << Expr::setlanguage(options::outputLanguage());
 378         ss << "e_" << tn;
 379         mbt = NodeManager::currentNM()->mkSkolem( ss.str(), tn, "is a model basis term" );
 380         Trace("mkVar") << "ModelBasis:: Make variable " << mbt << " : " << tn << std::endl;
 381       }else{
 382         mbt = d_type_map[ tn ][ 0 ];
 383       }
 384     }
 385     ModelBasisAttribute mba;
 386     mbt.setAttribute(mba,true);
 387     d_model_basis_term[tn] = mbt;
 388     Trace("model-basis-term") << "Choose " << mbt << " as model basis term for " << tn << std::endl;
 389   }
 390   return d_model_basis_term[tn];
 391 }
 392
 393 Node TermDb::getModelBasisOpTerm( Node op ){
 394   if( d_model_basis_op_term.find( op )==d_model_basis_op_term.end() ){
 395     TypeNode t = op.getType();
 396     std::vector< Node > children;
 397     children.push_back( op );
 398     for( int i=0; i<(int)(t.getNumChildren()-1); i++ ){
 399       children.push_back( getModelBasisTerm( t[i] ) );
 400     }
 401     if( children.size()==1 ){
 402       d_model_basis_op_term[op] = op;
 403     }else{
 404       d_model_basis_op_term[op] = NodeManager::currentNM()->mkNode( APPLY_UF, children );
 405     }
 406   }
 407   return d_model_basis_op_term[op];
 408 }
 409
 410 Node TermDb::getModelBasis( Node f, Node n ){
 411   //make model basis
 412   if( d_model_basis_terms.find( f )==d_model_basis_terms.end() ){
 413     for( int j=0; j<(int)f[0].getNumChildren(); j++ ){
 414       d_model_basis_terms[f].push_back( getModelBasisTerm( f[0][j].getType() ) );
 415     }
 416   }
 417   Node gn = n.substitute( d_inst_constants[f].begin(), d_inst_constants[f].end(),
 418                           d_model_basis_terms[f].begin(), d_model_basis_terms[f].end() );
 419   return gn;
 420 }
 421
 422 Node TermDb::getModelBasisBody( Node f ){
 423   if( d_model_basis_body.find( f )==d_model_basis_body.end() ){
 424     Node n = getInstConstantBody( f );
 425     d_model_basis_body[f] = getModelBasis( f, n );
 426   }
 427   return d_model_basis_body[f];
 428 }
 429
 430 void TermDb::computeModelBasisArgAttribute( Node n ){
 431   if( !n.hasAttribute(ModelBasisArgAttribute()) ){
 432     //ensure that the model basis terms have been defined
 433     if( n.getKind()==APPLY_UF ){
 434       getModelBasisOpTerm( n.getOperator() );
 435     }
 436     uint64_t val = 0;
 437     //determine if it has model basis attribute
 438     for( int j=0; j<(int)n.getNumChildren(); j++ ){
 439       if( n[j].getAttribute(ModelBasisAttribute()) ){
 440         val++;
 441       }
 442     }
 443     ModelBasisArgAttribute mbaa;
 444     n.setAttribute( mbaa, val );
 445   }
 446 }
 447
 448 void TermDb::makeInstantiationConstantsFor( Node f ){
 449   if( d_inst_constants.find( f )==d_inst_constants.end() ){
 450     Debug("quantifiers-engine") << "Instantiation constants for " << f << " : " << std::endl;
 451     for( int i=0; i<(int)f[0].getNumChildren(); i++ ){
 452       d_vars[f].push_back( f[0][i] );
 453       //make instantiation constants
 454       Node ic = NodeManager::currentNM()->mkInstConstant( f[0][i].getType() );
 455       d_inst_constants_map[ic] = f;
 456       d_inst_constants[ f ].push_back( ic );
 457       Debug("quantifiers-engine") << "  " << ic << std::endl;
 458       //set the var number attribute
 459       InstVarNumAttribute ivna;
 460       ic.setAttribute(ivna,i);
 461       InstConstantAttribute ica;
 462       ic.setAttribute(ica,f);
 463       //also set the no-match attribute
 464       NoMatchAttribute nma;
 465       ic.setAttribute(nma,true);
 466     }
 467   }
 468 }
 469
 470
 471 Node TermDb::getInstConstAttr( Node n ) {
 472   if (!n.hasAttribute(InstConstantAttribute()) ){
 473     Node f;
 474     for( int i=0; i<(int)n.getNumChildren(); i++ ){
 475       f = getInstConstAttr(n[i]);
 476       if( !f.isNull() ){
 477         break;
 478       }
 479     }
 480     InstConstantAttribute ica;
 481     n.setAttribute(ica,f);
 482     if( !f.isNull() ){
 483       //also set the no-match attribute
 484       NoMatchAttribute nma;
 485       n.setAttribute(nma,true);
 486     }
 487   }
 488   return n.getAttribute(InstConstantAttribute());
 489 }
 490
 491 bool TermDb::hasInstConstAttr( Node n ) {
 492   return !getInstConstAttr(n).isNull();
 493 }
 494
 495 void TermDb::getBoundVars( Node n, std::vector< Node >& bvs) {
 496   if (n.getKind()==BOUND_VARIABLE ){
 497     if ( std::find( bvs.begin(), bvs.end(), n)==bvs.end() ){
 498       bvs.push_back( n );
 499     }
 500   }else{
 501     for( unsigned i=0; i<n.getNumChildren(); i++) {
 502       getBoundVars(n[i], bvs);
 503     }
 504   }
 505 }
 506
 507
 508 /** get the i^th instantiation constant of f */
 509 Node TermDb::getInstantiationConstant( Node f, int i ) const {
 510   std::map< Node, std::vector< Node > >::const_iterator it = d_inst_constants.find( f );
 511   if( it!=d_inst_constants.end() ){
 512     return it->second[i];
 513   }else{
 514     return Node::null();
 515   }
 516 }
 517
 518 /** get number of instantiation constants for f */
 519 int TermDb::getNumInstantiationConstants( Node f ) const {
 520   std::map< Node, std::vector< Node > >::const_iterator it = d_inst_constants.find( f );
 521   if( it!=d_inst_constants.end() ){
 522     return (int)it->second.size();
 523   }else{
 524     return 0;
 525   }
 526 }
 527
 528 Node TermDb::getInstConstantBody( Node f ){
 529   std::map< Node, Node >::iterator it = d_inst_const_body.find( f );
 530   if( it==d_inst_const_body.end() ){
 531     makeInstantiationConstantsFor( f );
 532     Node n = getInstConstantNode( f[1], f );
 533     d_inst_const_body[ f ] = n;
 534     return n;
 535   }else{
 536     return it->second;
 537   }
 538 }
 539
 540 Node TermDb::getCounterexampleLiteral( Node f ){
 541   if( d_ce_lit.find( f )==d_ce_lit.end() ){
 542     Node ceBody = getInstConstantBody( f );
 543     //check if any variable are of bad types, and fail if so
 544     for( size_t i=0; i<d_inst_constants[f].size(); i++ ){
 545       if( d_inst_constants[f][i].getType().isBoolean() ){
 546         d_ce_lit[ f ] = Node::null();
 547         return Node::null();
 548       }
 549     }
 550     //otherwise, ensure literal
 551     Node ceLit = d_quantEngine->getValuation().ensureLiteral( ceBody.notNode() );
 552     d_ce_lit[ f ] = ceLit;
 553   }
 554   return d_ce_lit[ f ];
 555 }
 556
 557 Node TermDb::getInstConstantNode( Node n, Node f ){
 558   return convertNodeToPattern(n,f,d_vars[f],d_inst_constants[ f ]);
 559 }
 560
 561 Node TermDb::convertNodeToPattern( Node n, Node f, const std::vector<Node> & vars,
 562                                               const std::vector<Node> & inst_constants){
 563   Node n2 = n.substitute( vars.begin(), vars.end(),
 564                           inst_constants.begin(),
 565                           inst_constants.end() );
 566   return n2;
 567 }
 568
 569
 570 void getSelfSel( const DatatypeConstructor& dc, Node n, TypeNode ntn, std::vector< Node >& selfSel ){
 571   for( unsigned j=0; j<dc.getNumArgs(); j++ ){
 572     TypeNode tn = TypeNode::fromType( ((SelectorType)dc[j].getSelector().getType()).getRangeType() );
 573     std::vector< Node > ssc;
 574     if( tn==ntn ){
 575       ssc.push_back( n );
 576     }
 577     /* TODO
 578     else if( datatypes::DatatypesRewriter::isTypeDatatype( tn ) && std::find( visited.begin(), visited.end(), tn )==visited.end() ){
 579       visited.push_back( tn );
 580       const Datatype& dt = ((DatatypeType)(subs[0].getType()).toType()).getDatatype();
 581       std::vector< Node > disj;
 582       for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
 583         getSelfSel( dt[i], n, ntn, ssc );
 584       }
 585       visited.pop_back();
 586     }
 587     */
 588     for( unsigned k=0; k<ssc.size(); k++ ){
 589       selfSel.push_back( NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, dc[j].getSelector(), n ) );
 590     }
 591   }
 592 }
 593
 594
 595 Node TermDb::mkSkolemizedBody( Node f, Node n, std::vector< TypeNode >& argTypes, std::vector< TNode >& fvs,
 596                                std::vector< Node >& sk, Node& sub, std::vector< unsigned >& sub_vars ) {
 597   //calculate the variables and substitution
 598   std::vector< TNode > ind_vars;
 599   std::vector< unsigned > ind_var_indicies;
 600   std::vector< TNode > vars;
 601   std::vector< unsigned > var_indicies;
 602   for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
 603     if( isInductionTerm( f[0][i] ) ){
 604       ind_vars.push_back( f[0][i] );
 605       ind_var_indicies.push_back( i );
 606     }else{
 607       vars.push_back( f[0][i] );
 608       var_indicies.push_back( i );
 609     }
 610     Node s;
 611     //make the new function symbol
 612     if( argTypes.empty() ){
 613       s = NodeManager::currentNM()->mkSkolem( "skv", f[0][i].getType(), "created during skolemization" );
 614     }else{
 615       TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, f[0][i].getType() );
 616       Node op = NodeManager::currentNM()->mkSkolem( "skop", typ, "op created during pre-skolemization" );
 617       //DOTHIS: set attribute on op, marking that it should not be selected as trigger
 618       std::vector< Node > funcArgs;
 619       funcArgs.push_back( op );
 620       funcArgs.insert( funcArgs.end(), fvs.begin(), fvs.end() );
 621       s = NodeManager::currentNM()->mkNode( kind::APPLY_UF, funcArgs );
 622     }
 623     sk.push_back( s );
 624   }
 625   Node ret;
 626   if( vars.empty() ){
 627     ret = n;
 628   }else{
 629     std::vector< Node > var_sk;
 630     for( unsigned i=0; i<var_indicies.size(); i++ ){
 631       var_sk.push_back( sk[var_indicies[i]] );
 632     }
 633     Assert( vars.size()==var_sk.size() );
 634     ret = n.substitute( vars.begin(), vars.end(), var_sk.begin(), var_sk.end() );
 635   }
 636   if( !ind_vars.empty() ){
 637     Trace("stc-ind") << "Ind strengthen : (not " << f << ")" << std::endl;
 638     Trace("stc-ind") << "Skolemized is : " << ret << std::endl;
 639     Node nret;
 640     Node n_str_ind;
 641     TypeNode tn = ind_vars[0].getType();
 642     if( options::dtStcInduction() && datatypes::DatatypesRewriter::isTypeDatatype(tn) ){
 643       Node k = sk[ind_var_indicies[0]];
 644       const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
 645       std::vector< Node > disj;
 646       for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
 647         std::vector< Node > selfSel;
 648         getSelfSel( dt[i], k, tn, selfSel );
 649         std::vector< Node > conj;
 650         conj.push_back( NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[i].getTester() ), k ).negate() );
 651         for( unsigned j=0; j<selfSel.size(); j++ ){
 652           conj.push_back( ret.substitute( ind_vars[0], selfSel[j] ).negate() );
 653         }
 654         disj.push_back( conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( OR, conj ) );
 655       }
 656       Assert( !disj.empty() );
 657       n_str_ind = disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( AND, disj );
 658       Trace("stc-ind") << "Strengthening is : " << n_str_ind << std::endl;
 659       nret = ret.substitute( ind_vars[0], k );
 660     }else{
 661       Trace("stc-ind") << "Unknown induction for term : " << ind_vars[0] << ", type = " << tn << std::endl;
 662       Assert( false );
 663     }
 664
 665     std::vector< Node > rem_ind_vars;
 666     rem_ind_vars.insert( rem_ind_vars.end(), ind_vars.begin()+1, ind_vars.end() );
 667     if( !rem_ind_vars.empty() ){
 668       Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, rem_ind_vars );
 669       nret = NodeManager::currentNM()->mkNode( FORALL, bvl, nret );
 670       nret = Rewriter::rewrite( nret );
 671       sub = nret;
 672       sub_vars.insert( sub_vars.end(), ind_var_indicies.begin()+1, ind_var_indicies.end() );
 673       n_str_ind = NodeManager::currentNM()->mkNode( FORALL, bvl, n_str_ind.negate() ).negate();
 674     }
 675     ret = NodeManager::currentNM()->mkNode( OR, nret, n_str_ind );
 676   }
 677   Trace("quantifiers-sk") << "mkSkolem body for " << f << " returns : " << ret << std::endl;
 678   return ret;
 679 }
 680
 681 Node TermDb::getSkolemizedBody( Node f ){
 682   Assert( f.getKind()==FORALL );
 683   if( d_skolem_body.find( f )==d_skolem_body.end() ){
 684     std::vector< TypeNode > fvTypes;
 685     std::vector< TNode > fvs;
 686     Node sub;
 687     std::vector< unsigned > sub_vars;
 688     d_skolem_body[ f ] = mkSkolemizedBody( f, f[1], fvTypes, fvs, d_skolem_constants[f], sub, sub_vars );
 689     //store sub quantifier information
 690     if( !sub.isNull() ){
 691       Assert( sub[0].getNumChildren()==sub_vars.size() );
 692       d_skolem_sub_quant[f] = sub;
 693       d_skolem_sub_quant_vars[f].insert( d_skolem_sub_quant_vars[f].end(), sub_vars.begin(), sub_vars.end() );
 694     }
 695     Assert( d_skolem_constants[f].size()==f[0].getNumChildren() );
 696     if( options::sortInference() ){
 697       for( unsigned i=0; i<d_skolem_constants[f].size(); i++ ){
 698         //carry information for sort inference
 699         d_quantEngine->getTheoryEngine()->getSortInference()->setSkolemVar( f, f[0][i], d_skolem_constants[f][i] );
 700       }
 701     }
 702   }
 703   return d_skolem_body[ f ];
 704 }
 705
 706 void TermDb::getSkolemConstants( Node f, std::vector< Node >& sk, bool expSub ) {
 707   std::map< Node, std::vector< Node > >::iterator it = d_skolem_constants.find( f );
 708   if( it!=d_skolem_constants.end() ){
 709     sk.insert( sk.end(), it->second.begin(), it->second.end() );
 710     if( expSub ){
 711       std::map< Node, Node >::iterator its = d_skolem_sub_quant.find( f );
 712       if( its!=d_skolem_sub_quant.end() && !its->second.isNull() ){
 713         std::vector< Node > ssk;
 714         getSkolemConstants( its->second, ssk, true );
 715         Assert( ssk.size()==d_skolem_sub_quant_vars[f].size() );
 716         for( unsigned i=0; i<d_skolem_sub_quant_vars[f].size(); i++ ){
 717           sk[d_skolem_sub_quant_vars[f][i]] = ssk[i];
 718         }
 719       }
 720     }
 721     Assert( sk.size()==f[0].getNumChildren() );
 722   }
 723 }
 724
 725 Node TermDb::getFreeVariableForInstConstant( Node n ){
 726   TypeNode tn = n.getType();
 727   if( d_free_vars.find( tn )==d_free_vars.end() ){
 728         for( unsigned i=0; i<d_type_map[ tn ].size(); i++ ){
 729           if( !quantifiers::TermDb::hasInstConstAttr(d_type_map[ tn ][ i ]) ){
 730             d_free_vars[tn] = d_type_map[ tn ][ i ];
 731           }
 732         }
 733         if( d_free_vars.find( tn )==d_free_vars.end() ){
 734       //if integer or real, make zero
 735       if( tn.isInteger() || tn.isReal() ){
 736         Rational z(0);
 737         d_free_vars[tn] = NodeManager::currentNM()->mkConst( z );
 738       }else{
 739             d_free_vars[tn] = NodeManager::currentNM()->mkSkolem( "freevar", tn, "is a free variable created by termdb" );
 740             Trace("mkVar") << "FreeVar:: Make variable " << d_free_vars[tn] << " : " << tn << std::endl;
 741       }
 742     }
 743   }
 744   return d_free_vars[tn];
 745 }
 746
 747 const std::vector<Node> & TermDb::getParents(TNode n, TNode f, int arg){
 748   std::hash_map< Node, std::hash_map< Node, std::hash_map< int, std::vector< Node > >,NodeHashFunction  >,NodeHashFunction  >::const_iterator
 749     rn = d_parents.find( n );
 750   if( rn !=d_parents.end() ){
 751     std::hash_map< Node, std::hash_map< int, std::vector< Node > > , NodeHashFunction  > ::const_iterator
 752       rf = rn->second.find(f);
 753     if( rf != rn->second.end() ){
 754       std::hash_map< int, std::vector< Node > > ::const_iterator
 755         ra = rf->second.find(arg);
 756       if( ra != rf->second.end() ){
 757         return ra->second;
 758       }
 759     }
 760   }
 761   static std::vector<Node> empty;
 762   return empty;
 763 }
 764
 765 void TermDb::computeVarContains( Node n ) {
 766   if( d_var_contains.find( n )==d_var_contains.end() ){
 767     d_var_contains[n].clear();
 768     computeVarContains2( n, n );
 769   }
 770 }
 771
 772 void TermDb::computeVarContains2( Node n, Node parent ){
 773   if( n.getKind()==INST_CONSTANT ){
 774     if( std::find( d_var_contains[parent].begin(), d_var_contains[parent].end(), n )==d_var_contains[parent].end() ){
 775       d_var_contains[parent].push_back( n );
 776     }
 777   }else{
 778     for( int i=0; i<(int)n.getNumChildren(); i++ ){
 779       computeVarContains2( n[i], parent );
 780     }
 781   }
 782 }
 783
 784 bool TermDb::isVariableSubsume( Node n1, Node n2 ){
 785   if( n1==n2 ){
 786     return true;
 787   }else{
 788     //Notice() << "is variable subsume ? " << n1 << " " << n2 << std::endl;
 789     computeVarContains( n1 );
 790     computeVarContains( n2 );
 791     for( int i=0; i<(int)d_var_contains[n2].size(); i++ ){
 792       if( std::find( d_var_contains[n1].begin(), d_var_contains[n1].end(), d_var_contains[n2][i] )==d_var_contains[n1].end() ){
 793         //Notice() << "no" << std::endl;
 794         return false;
 795       }
 796     }
 797     //Notice() << "yes" << std::endl;
 798     return true;
 799   }
 800 }
 801
 802 void TermDb::getVarContains( Node f, std::vector< Node >& pats, std::map< Node, std::vector< Node > >& varContains ){
 803   for( int i=0; i<(int)pats.size(); i++ ){
 804     computeVarContains( pats[i] );
 805     varContains[ pats[i] ].clear();
 806     for( int j=0; j<(int)d_var_contains[pats[i]].size(); j++ ){
 807       if( d_var_contains[pats[i]][j].getAttribute(InstConstantAttribute())==f ){
 808         varContains[ pats[i] ].push_back( d_var_contains[pats[i]][j] );
 809       }
 810     }
 811   }
 812 }
 813
 814 void TermDb::getVarContainsNode( Node f, Node n, std::vector< Node >& varContains ){
 815   computeVarContains( n );
 816   for( int j=0; j<(int)d_var_contains[n].size(); j++ ){
 817     if( d_var_contains[n][j].getAttribute(InstConstantAttribute())==f ){
 818       varContains.push_back( d_var_contains[n][j] );
 819     }
 820   }
 821 }
 822
 823 /** is n1 an instance of n2 or vice versa? */
 824 int TermDb::isInstanceOf( Node n1, Node n2 ){
 825   if( n1==n2 ){
 826     return 1;
 827   }else if( n1.getKind()==n2.getKind() ){
 828     if( n1.getKind()==APPLY_UF ){
 829       if( n1.getOperator()==n2.getOperator() ){
 830         int result = 0;
 831         for( int i=0; i<(int)n1.getNumChildren(); i++ ){
 832           if( n1[i]!=n2[i] ){
 833             int cResult = isInstanceOf( n1[i], n2[i] );
 834             if( cResult==0 ){
 835               return 0;
 836             }else if( cResult!=result ){
 837               if( result!=0 ){
 838                 return 0;
 839               }else{
 840                 result = cResult;
 841               }
 842             }
 843           }
 844         }
 845         return result;
 846       }
 847     }
 848     return 0;
 849   }else if( n2.getKind()==INST_CONSTANT ){
 850     computeVarContains( n1 );
 851     //if( std::find( d_var_contains[ n1 ].begin(), d_var_contains[ n1 ].end(), n2 )!=d_var_contains[ n1 ].end() ){
 852     //  return 1;
 853     //}
 854     if( d_var_contains[ n1 ].size()==1 && d_var_contains[ n1 ][ 0 ]==n2 ){
 855       return 1;
 856     }
 857   }else if( n1.getKind()==INST_CONSTANT ){
 858     computeVarContains( n2 );
 859     //if( std::find( d_var_contains[ n2 ].begin(), d_var_contains[ n2 ].end(), n1 )!=d_var_contains[ n2 ].end() ){
 860     //  return -1;
 861     //}
 862     if( d_var_contains[ n2 ].size()==1 && d_var_contains[ n2 ][ 0 ]==n1 ){
 863       return 1;
 864     }
 865   }
 866   return 0;
 867 }
 868
 869 bool TermDb::isUnifiableInstanceOf( Node n1, Node n2, std::map< Node, Node >& subs ){
 870   if( n1==n2 ){
 871     return true;
 872   }else if( n2.getKind()==INST_CONSTANT ){
 873     //if( !node_contains( n1, n2 ) ){
 874     //  return false;
 875     //}
 876     if( subs.find( n2 )==subs.end() ){
 877       subs[n2] = n1;
 878     }else if( subs[n2]!=n1 ){
 879       return false;
 880     }
 881     return true;
 882   }else if( n1.getKind()==n2.getKind() && n1.getMetaKind()==kind::metakind::PARAMETERIZED ){
 883     if( n1.getOperator()!=n2.getOperator() ){
 884       return false;
 885     }
 886     for( int i=0; i<(int)n1.getNumChildren(); i++ ){
 887       if( !isUnifiableInstanceOf( n1[i], n2[i], subs ) ){
 888         return false;
 889       }
 890     }
 891     return true;
 892   }else{
 893     return false;
 894   }
 895 }
 896
 897 void TermDb::filterInstances( std::vector< Node >& nodes ){
 898   std::vector< bool > active;
 899   active.resize( nodes.size(), true );
 900   for( int i=0; i<(int)nodes.size(); i++ ){
 901     for( int j=i+1; j<(int)nodes.size(); j++ ){
 902       if( active[i] && active[j] ){
 903         int result = isInstanceOf( nodes[i], nodes[j] );
 904         if( result==1 ){
 905           Trace("filter-instances") << nodes[j] << " is an instance of " << nodes[i] << std::endl;
 906           active[j] = false;
 907         }else if( result==-1 ){
 908           Trace("filter-instances") << nodes[i] << " is an instance of " << nodes[j] << std::endl;
 909           active[i] = false;
 910         }
 911       }
 912     }
 913   }
 914   std::vector< Node > temp;
 915   for( int i=0; i<(int)nodes.size(); i++ ){
 916     if( active[i] ){
 917       temp.push_back( nodes[i] );
 918     }
 919   }
 920   nodes.clear();
 921   nodes.insert( nodes.begin(), temp.begin(), temp.end() );
 922 }
 923
 924 void TermDb::registerTrigger( theory::inst::Trigger* tr, Node op ){
 925   if( std::find( d_op_triggers[op].begin(), d_op_triggers[op].end(), tr )==d_op_triggers[op].end() ){
 926     d_op_triggers[op].push_back( tr );
 927   }
 928 }
 929
 930 bool TermDb::isInductionTerm( Node n ) {
 931   if( options::dtStcInduction() && datatypes::DatatypesRewriter::isTermDatatype( n ) ){
 932     return true;
 933   }
 934   return false;
 935 }
 936
 937
 938 bool TermDb::isRewriteRule( Node q ) {
 939   return !getRewriteRule( q ).isNull();
 940 }
 941
 942 Node TermDb::getRewriteRule( Node q ) {
 943   if( q.getKind()==FORALL && q.getNumChildren()==3 && q[2].getNumChildren()>0 && q[2][0][0].getKind()==REWRITE_RULE ){
 944     return q[2][0][0];
 945   }else{
 946     return Node::null();
 947   }
 948 }