src/theory/theory.cpp

   1 /*********************                                                        */
   2 /*! \file theory.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Tim King, Dejan Jovanovic, Clark Barrett
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Base for theory interface.
  13  **
  14  ** Base for theory interface.
  15  **/
  16
  17 #include "theory/theory.h"
  18
  19 #include <vector>
  20 #include <sstream>
  21 #include <iostream>
  22 #include <string>
  23
  24 #include "base/cvc4_assert.h"
  25 #include "smt/smt_statistics_registry.h"
  26 #include "theory/substitutions.h"
  27 #include "theory/quantifiers_engine.h"
  28
  29
  30 using namespace std;
  31
  32 namespace CVC4 {
  33 namespace theory {
  34
  35 /** Default value for the uninterpreted sorts is the UF theory */
  36 TheoryId Theory::s_uninterpretedSortOwner = THEORY_UF;
  37
  38 std::ostream& operator<<(std::ostream& os, Theory::Effort level){
  39   switch(level){
  40   case Theory::EFFORT_STANDARD:
  41     os << "EFFORT_STANDARD"; break;
  42   case Theory::EFFORT_FULL:
  43     os << "EFFORT_FULL"; break;
  44   case Theory::EFFORT_COMBINATION:
  45     os << "EFFORT_COMBINATION"; break;
  46   case Theory::EFFORT_LAST_CALL:
  47     os << "EFFORT_LAST_CALL"; break;
  48   default:
  49       Unreachable();
  50   }
  51   return os;
  52 }/* ostream& operator<<(ostream&, Theory::Effort) */
  53
  54
  55 Theory::Theory(TheoryId id, context::Context* satContext,
  56                context::UserContext* userContext, OutputChannel& out,
  57                Valuation valuation, const LogicInfo& logicInfo,
  58                std::string name) throw()
  59     : d_id(id)
  60     , d_instanceName(name)
  61     , d_satContext(satContext)
  62     , d_userContext(userContext)
  63     , d_logicInfo(logicInfo)
  64     , d_facts(satContext)
  65     , d_factsHead(satContext, 0)
  66     , d_sharedTermsIndex(satContext, 0)
  67     , d_careGraph(NULL)
  68     , d_quantEngine(NULL)
  69     , d_extt(NULL)
  70     , d_checkTime(getFullInstanceName() + "::checkTime")
  71     , d_computeCareGraphTime(getFullInstanceName() + "::computeCareGraphTime")
  72     , d_sharedTerms(satContext)
  73     , d_out(&out)
  74     , d_valuation(valuation)
  75     , d_proofsEnabled(false)
  76 {
  77   smtStatisticsRegistry()->registerStat(&d_checkTime);
  78   smtStatisticsRegistry()->registerStat(&d_computeCareGraphTime);
  79 }
  80
  81 Theory::~Theory() {
  82   smtStatisticsRegistry()->unregisterStat(&d_checkTime);
  83   smtStatisticsRegistry()->unregisterStat(&d_computeCareGraphTime);
  84 }
  85
  86 TheoryId Theory::theoryOf(TheoryOfMode mode, TNode node) {
  87   TheoryId tid = THEORY_BUILTIN;
  88   switch(mode) {
  89   case THEORY_OF_TYPE_BASED:
  90     // Constants, variables, 0-ary constructors
  91     if (node.isVar() || node.isConst()) {
  92       tid = Theory::theoryOf(node.getType());
  93     } else if (node.getKind() == kind::EQUAL) {
  94       // Equality is owned by the theory that owns the domain
  95       tid = Theory::theoryOf(node[0].getType());
  96     } else {
  97       // Regular nodes are owned by the kind
  98       tid = kindToTheoryId(node.getKind());
  99     }
 100     break;
 101   case THEORY_OF_TERM_BASED:
 102     // Variables
 103     if (node.isVar()) {
 104       if (Theory::theoryOf(node.getType()) != theory::THEORY_BOOL) {
 105         // We treat the variables as uninterpreted
 106         tid = s_uninterpretedSortOwner;
 107       } else {
 108         // Except for the Boolean ones, which we just ignore anyhow
 109         tid = theory::THEORY_BOOL;
 110       }
 111     } else if (node.isConst()) {
 112       // Constants go to the theory of the type
 113       tid = Theory::theoryOf(node.getType());
 114     } else if (node.getKind() == kind::EQUAL) { // Equality
 115       // If one of them is an ITE, it's irelevant, since they will get replaced out anyhow
 116       if (node[0].getKind() == kind::ITE) {
 117         tid = Theory::theoryOf(node[0].getType());
 118       } else if (node[1].getKind() == kind::ITE) {
 119         tid = Theory::theoryOf(node[1].getType());
 120       } else {
 121         TNode l = node[0];
 122         TNode r = node[1];
 123         TypeNode ltype = l.getType();
 124         TypeNode rtype = r.getType();
 125         if( ltype != rtype ){
 126           tid = Theory::theoryOf(l.getType());
 127         }else {
 128           // If both sides belong to the same theory the choice is easy
 129           TheoryId T1 = Theory::theoryOf(l);
 130           TheoryId T2 = Theory::theoryOf(r);
 131           if (T1 == T2) {
 132             tid = T1;
 133           } else {
 134             TheoryId T3 = Theory::theoryOf(ltype);
 135             // This is a case of
 136             // * x*y = f(z) -> UF
 137             // * x = c      -> UF
 138             // * f(x) = read(a, y) -> either UF or ARRAY
 139             // at least one of the theories has to be parametric, i.e. theory of the type is different
 140             // from the theory of the term
 141             if (T1 == T3) {
 142               tid = T2;
 143             } else if (T2 == T3) {
 144               tid = T1;
 145             } else {
 146               // If both are parametric, we take the smaller one (arbitrary)
 147               tid = T1 < T2 ? T1 : T2;
 148             }
 149           }
 150         }
 151       }
 152     } else {
 153       // Regular nodes are owned by the kind
 154       tid = kindToTheoryId(node.getKind());
 155     }
 156     break;
 157   default:
 158     Unreachable();
 159   }
 160   Trace("theory::internal") << "theoryOf(" << mode << ", " << node << ") -> " << tid << std::endl;
 161   return tid;
 162 }
 163
 164 void Theory::addSharedTermInternal(TNode n) {
 165   Debug("sharing") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << endl;
 166   Debug("theory::assertions") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << endl;
 167   d_sharedTerms.push_back(n);
 168   addSharedTerm(n);
 169 }
 170
 171 void Theory::computeCareGraph() {
 172   Debug("sharing") << "Theory::computeCareGraph<" << getId() << ">()" << endl;
 173   for (unsigned i = 0; i < d_sharedTerms.size(); ++ i) {
 174     TNode a = d_sharedTerms[i];
 175     TypeNode aType = a.getType();
 176     for (unsigned j = i + 1; j < d_sharedTerms.size(); ++ j) {
 177       TNode b = d_sharedTerms[j];
 178       if (b.getType() != aType) {
 179         // We don't care about the terms of different types
 180         continue;
 181       }
 182       switch (d_valuation.getEqualityStatus(a, b)) {
 183       case EQUALITY_TRUE_AND_PROPAGATED:
 184       case EQUALITY_FALSE_AND_PROPAGATED:
 185         // If we know about it, we should have propagated it, so we can skip
 186         break;
 187       default:
 188         // Let's split on it
 189         addCarePair(a, b);
 190         break;
 191       }
 192     }
 193   }
 194 }
 195
 196 void Theory::printFacts(std::ostream& os) const {
 197   unsigned i, n = d_facts.size();
 198   for(i = 0; i < n; i++){
 199     const Assertion& a_i = d_facts[i];
 200     Node assertion  = a_i;
 201     os << d_id << '[' << i << ']' << " " << assertion << endl;
 202   }
 203 }
 204
 205 void Theory::debugPrintFacts() const{
 206   DebugChannel.getStream() << "Theory::debugPrintFacts()" << endl;
 207   printFacts(DebugChannel.getStream());
 208 }
 209
 210 std::hash_set<TNode, TNodeHashFunction> Theory::currentlySharedTerms() const{
 211   std::hash_set<TNode, TNodeHashFunction> currentlyShared;
 212   for (shared_terms_iterator i = shared_terms_begin(),
 213            i_end = shared_terms_end(); i != i_end; ++i) {
 214     currentlyShared.insert (*i);
 215   }
 216   return currentlyShared;
 217 }
 218
 219
 220 void Theory::collectTerms(TNode n, set<Node>& termSet) const
 221 {
 222   if (termSet.find(n) != termSet.end()) {
 223     return;
 224   }
 225   Trace("theory::collectTerms") << "Theory::collectTerms: adding " << n << endl;
 226   termSet.insert(n);
 227   if (n.getKind() == kind::NOT || n.getKind() == kind::EQUAL || !isLeaf(n)) {
 228     for(TNode::iterator child_it = n.begin(); child_it != n.end(); ++child_it) {
 229       collectTerms(*child_it, termSet);
 230     }
 231   }
 232 }
 233
 234
 235 void Theory::computeRelevantTerms(set<Node>& termSet, bool includeShared) const
 236 {
 237   // Collect all terms appearing in assertions
 238   context::CDList<Assertion>::const_iterator assert_it = facts_begin(), assert_it_end = facts_end();
 239   for (; assert_it != assert_it_end; ++assert_it) {
 240     collectTerms(*assert_it, termSet);
 241   }
 242
 243   if (!includeShared) return;
 244
 245   // Add terms that are shared terms
 246   context::CDList<TNode>::const_iterator shared_it = shared_terms_begin(), shared_it_end = shared_terms_end();
 247   for (; shared_it != shared_it_end; ++shared_it) {
 248     collectTerms(*shared_it, termSet);
 249   }
 250 }
 251
 252
 253 Theory::PPAssertStatus Theory::ppAssert(TNode in,
 254                                         SubstitutionMap& outSubstitutions)
 255 {
 256   if (in.getKind() == kind::EQUAL) {
 257     // (and (= x t) phi) can be replaced by phi[x/t] if
 258     // 1) x is a variable
 259     // 2) x is not in the term t
 260     // 3) x : T and t : S, then S <: T
 261     if (in[0].isVar() && !in[1].hasSubterm(in[0]) &&
 262         (in[1].getType()).isSubtypeOf(in[0].getType()) ){
 263       outSubstitutions.addSubstitution(in[0], in[1]);
 264       return PP_ASSERT_STATUS_SOLVED;
 265     }
 266     if (in[1].isVar() && !in[0].hasSubterm(in[1]) &&
 267         (in[0].getType()).isSubtypeOf(in[1].getType())){
 268       outSubstitutions.addSubstitution(in[1], in[0]);
 269       return PP_ASSERT_STATUS_SOLVED;
 270     }
 271     if (in[0].isConst() && in[1].isConst()) {
 272       if (in[0] != in[1]) {
 273         return PP_ASSERT_STATUS_CONFLICT;
 274       }
 275     }
 276   }
 277
 278   return PP_ASSERT_STATUS_UNSOLVED;
 279 }
 280
 281 std::pair<bool, Node> Theory::entailmentCheck(
 282     TNode lit,
 283     const EntailmentCheckParameters* params,
 284     EntailmentCheckSideEffects* out) {
 285   return make_pair(false, Node::null());
 286 }
 287
 288 EntailmentCheckParameters::EntailmentCheckParameters(TheoryId tid)
 289   : d_tid(tid) {
 290 }
 291
 292 std::string Theory::getFullInstanceName() const {
 293   std::stringstream ss;
 294   ss << "theory<" << d_id << ">" << d_instanceName;
 295   return ss.str();
 296 }
 297
 298 EntailmentCheckParameters::~EntailmentCheckParameters(){}
 299
 300 TheoryId EntailmentCheckParameters::getTheoryId() const {
 301   return d_tid;
 302 }
 303
 304 EntailmentCheckSideEffects::EntailmentCheckSideEffects(TheoryId tid)
 305   : d_tid(tid)
 306 {}
 307
 308 TheoryId EntailmentCheckSideEffects::getTheoryId() const {
 309   return d_tid;
 310 }
 311
 312 EntailmentCheckSideEffects::~EntailmentCheckSideEffects() {
 313 }
 314
 315
 316 ExtTheory::ExtTheory( Theory * p ) : d_parent( p ),
 317 d_ext_func_terms( p->getSatContext() ), d_ci_inactive( p->getUserContext() ),
 318 d_lemmas( p->getUserContext() ), d_pp_lemmas( p->getUserContext() ), d_has_extf( p->getSatContext() ){
 319   d_true = NodeManager::currentNM()->mkConst( true );
 320 }
 321
 322 //gets all leaf terms in n
 323 void ExtTheory::collectVars( Node n, std::vector< Node >& vars, std::map< Node, bool >& visited ) {
 324   if( !n.isConst() ){
 325     if( visited.find( n )==visited.end() ){
 326       visited[n] = true;
 327       //treat terms not belonging to this theory as leaf
 328       if( n.getNumChildren()>0 ){//&& Theory::theoryOf(n)==d_parent->getId() ){
 329         for( unsigned i=0; i<n.getNumChildren(); i++ ){
 330           collectVars( n[i], vars, visited );
 331         }
 332       }else{
 333         vars.push_back( n );
 334       }
 335     }
 336   }
 337 }
 338
 339 //do inferences
 340 void ExtTheory::getSubstitutedTerms( int effort, std::vector< Node >& terms, std::vector< Node >& sterms, std::vector< std::vector< Node > >& exp ) {
 341   Trace("extt-debug") << "Currently " << d_ext_func_terms.size() << " extended functions." << std::endl;
 342   Trace("extt-debug") << "..." << terms.size() << " to reduce." << std::endl;
 343   if( !terms.empty() ){
 344     //all variables we need to find a substitution for
 345     std::vector< Node > vars;
 346     std::vector< Node > sub;
 347     std::map< Node, std::vector< Node > > expc;
 348     for( unsigned i=0; i<terms.size(); i++ ){
 349       //do substitution, rewrite
 350       Node n = terms[i];
 351       std::map< Node, ExtfInfo >::iterator iti = d_extf_info.find( n );
 352       Assert( iti!=d_extf_info.end() );
 353       for( unsigned i=0; i<iti->second.d_vars.size(); i++ ){
 354         if( std::find( vars.begin(), vars.end(), iti->second.d_vars[i] )==vars.end() ){
 355           vars.push_back( iti->second.d_vars[i] );
 356         }
 357       }
 358     }
 359     //get the current substitution for all variables
 360     if( d_parent->getCurrentSubstitution( effort, vars, sub, expc ) ){
 361       Assert( vars.size()==sub.size() );
 362       for( unsigned i=0; i<terms.size(); i++ ){
 363         //do substitution
 364         Node n = terms[i];
 365         Node ns = n.substitute( vars.begin(), vars.end(), sub.begin(), sub.end() );
 366         std::vector< Node > expn;
 367         if( ns!=n ){
 368           //build explanation: explanation vars = sub for each vars in FV( n )
 369           std::map< Node, ExtfInfo >::iterator iti = d_extf_info.find( n );
 370           Assert( iti!=d_extf_info.end() );
 371           for( unsigned j=0; j<iti->second.d_vars.size(); j++ ){
 372             Node v = iti->second.d_vars[j];
 373             std::map< Node, std::vector< Node > >::iterator itx = expc.find( v );
 374             if( itx!=expc.end() ){
 375               for( unsigned k=0; k<itx->second.size(); k++ ){
 376                 if( std::find( expn.begin(), expn.end(), itx->second[k] )==expn.end() ){
 377                   expn.push_back( itx->second[k] );
 378                 }
 379               }
 380             }
 381           }
 382         }
 383         Trace("extt-debug") << "  have " << n << " == " << ns << ", exp size=" << expn.size() << "." << std::endl;
 384         //add to vector
 385         sterms.push_back( ns );
 386         exp.push_back( expn );
 387       }
 388     }else{
 389       for( unsigned i=0; i<terms.size(); i++ ){
 390         sterms.push_back( terms[i] );
 391       }
 392     }
 393   }
 394 }
 395
 396 bool ExtTheory::doInferencesInternal( int effort, std::vector< Node >& terms, std::vector< Node >& nred, bool batch, bool isRed ) {
 397   if( batch ){
 398     bool addedLemma = false;
 399     if( isRed ){
 400       for( unsigned i=0; i<terms.size(); i++ ){
 401         Node n = terms[i];
 402         Node nr;
 403         //TODO: reduction with substitution?
 404         int ret = d_parent->getReduction( effort, n, nr );
 405         if( ret==0 ){
 406           nred.push_back( n );
 407         }else{
 408           if( !nr.isNull() && n!=nr ){
 409             Node lem = NodeManager::currentNM()->mkNode( n.getType().isBoolean() ? kind::IFF : kind::EQUAL, n, nr );
 410             if( sendLemma( lem, true ) ){
 411               Trace("extt-lemma") << "ExtTheory : Reduction lemma : " << lem << std::endl;
 412               addedLemma = true;
 413             }
 414           }
 415           markReduced( terms[i], ret<0 );
 416         }
 417       }
 418     }else{
 419       std::vector< Node > sterms;
 420       std::vector< std::vector< Node > > exp;
 421       getSubstitutedTerms( effort, terms, sterms, exp );
 422       for( unsigned i=0; i<terms.size(); i++ ){
 423         bool processed = false;
 424         if( sterms[i]!=terms[i] ){
 425           Node sr = Rewriter::rewrite( sterms[i] );
 426           if( sr.isConst() ){
 427             processed = true;
 428             markReduced( terms[i] );
 429             Node eq = terms[i].eqNode( sr );
 430             Node expn = exp[i].size()>1 ? NodeManager::currentNM()->mkNode( kind::AND, exp[i] ) : ( exp[i].size()==1 ? exp[i][0] : d_true );
 431             Trace("extt-debug") << "ExtTheory::doInferences : infer : " << eq << " by " << expn << std::endl;
 432             Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, expn, eq );
 433             Trace("extt-debug") << "...send lemma " << lem << std::endl;
 434             if( sendLemma( lem ) ){
 435               Trace("extt-lemma") << "ExtTheory : Constant rewrite lemma : " << lem << std::endl;
 436               addedLemma = true;
 437             }
 438           }
 439         }
 440         if( !processed ){
 441           nred.push_back( terms[i] );
 442         }
 443       }
 444     }
 445     return addedLemma;
 446   }else{
 447     std::vector< Node > nnred;
 448     if( terms.empty() ){
 449       for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){
 450         if( (*it).second && !isContextIndependentInactive( (*it).first ) ){
 451           std::vector< Node > nterms;
 452           nterms.push_back( (*it).first );
 453           if( doInferencesInternal( effort, nterms, nnred, true, isRed ) ){
 454             return true;
 455           }
 456         }
 457       }
 458     }else{
 459       for( unsigned i=0; i<terms.size(); i++ ){
 460         std::vector< Node > nterms;
 461         nterms.push_back( terms[i] );
 462         if( doInferencesInternal( effort, nterms, nnred, true, isRed ) ){
 463           return true;
 464         }
 465       }
 466     }
 467     return false;
 468   }
 469 }
 470
 471 bool ExtTheory::sendLemma( Node lem, bool preprocess ) {
 472   if( preprocess ){
 473     if( d_pp_lemmas.find( lem )==d_pp_lemmas.end() ){
 474       d_pp_lemmas.insert( lem );
 475       d_parent->getOutputChannel().lemma( lem, false, true );
 476       return true;
 477     }
 478   }else{
 479     if( d_lemmas.find( lem )==d_lemmas.end() ){
 480       d_lemmas.insert( lem );
 481       d_parent->getOutputChannel().lemma( lem );
 482       return true;
 483     }
 484   }
 485   return false;
 486 }
 487
 488 bool ExtTheory::doInferences( int effort, std::vector< Node >& terms, std::vector< Node >& nred, bool batch ) {
 489   if( !terms.empty() ){
 490     return doInferencesInternal( effort, terms, nred, batch, false );
 491   }else{
 492     return false;
 493   }
 494 }
 495
 496 bool ExtTheory::doInferences( int effort, std::vector< Node >& nred, bool batch ) {
 497   std::vector< Node > terms;
 498   getActive( terms );
 499   return doInferencesInternal( effort, terms, nred, batch, false );
 500 }
 501
 502 bool ExtTheory::doReductions( int effort, std::vector< Node >& terms, std::vector< Node >& nred, bool batch ) {
 503   if( !terms.empty() ){
 504     return doInferencesInternal( effort, terms, nred, batch, true );
 505   }else{
 506     return false;
 507   }
 508 }
 509
 510 bool ExtTheory::doReductions( int effort, std::vector< Node >& nred, bool batch ) {
 511   std::vector< Node > terms;
 512   getActive( terms );
 513   return doInferencesInternal( effort, terms, nred, batch, true );
 514 }
 515
 516
 517 //register term
 518 void ExtTheory::registerTerm( Node n ) {
 519   if( d_extf_kind.find( n.getKind() )!=d_extf_kind.end() ){
 520     if( d_ext_func_terms.find( n )==d_ext_func_terms.end() ){
 521       Trace("extt-debug") << "Found extended function : " << n << " in " << d_parent->getId() << std::endl;
 522       d_ext_func_terms[n] = true;
 523       d_has_extf = n;
 524       std::map< Node, bool > visited;
 525       collectVars( n, d_extf_info[n].d_vars, visited );
 526     }
 527   }
 528 }
 529
 530 void ExtTheory::registerTermRec( Node n ) {
 531   std::map< Node, bool > visited;
 532   registerTermRec( n, visited );
 533 }
 534
 535 void ExtTheory::registerTermRec( Node n, std::map< Node, bool >& visited ) {
 536   if( visited.find( n )==visited.end() ){
 537     visited[n] = true;
 538     registerTerm( n );
 539     for( unsigned i=0; i<n.getNumChildren(); i++ ){
 540       registerTermRec( n[i], visited );
 541     }
 542   }
 543 }
 544
 545 //mark reduced
 546 void ExtTheory::markReduced( Node n, bool contextDepend ) {
 547   d_ext_func_terms[n] = false;
 548   if( !contextDepend ){
 549     d_ci_inactive.insert( n );
 550   }
 551
 552   //update has_extf
 553   if( d_has_extf.get()==n ){
 554     for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){
 555       //if not already reduced
 556       if( (*it).second && !isContextIndependentInactive( (*it).first ) ){
 557          d_has_extf = (*it).first;
 558       }
 559     }
 560
 561   }
 562 }
 563
 564 //mark congruent
 565 void ExtTheory::markCongruent( Node a, Node b ) {
 566   NodeBoolMap::const_iterator it = d_ext_func_terms.find( b );
 567   if( it!=d_ext_func_terms.end() ){
 568     if( d_ext_func_terms.find( a )==d_ext_func_terms.end() ){
 569       d_ext_func_terms[a] = (*it).second;
 570     }else{
 571       d_ext_func_terms[a] = d_ext_func_terms[a] && (*it).second;
 572     }
 573     d_ext_func_terms[b] = false;
 574   }
 575 }
 576
 577 bool ExtTheory::isContextIndependentInactive( Node n ) {
 578   return d_ci_inactive.find( n )!=d_ci_inactive.end();
 579 }
 580
 581 bool ExtTheory::hasActiveTerm() {
 582   return !d_has_extf.get().isNull();
 583 }
 584
 585 //is active
 586 bool ExtTheory::isActive( Node n ) {
 587   NodeBoolMap::const_iterator it = d_ext_func_terms.find( n );
 588   if( it!=d_ext_func_terms.end() ){
 589     return (*it).second && !isContextIndependentInactive( n );
 590   }else{
 591     return false;
 592   }
 593 }
 594 //get active
 595 void ExtTheory::getActive( std::vector< Node >& active ) {
 596   for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){
 597     //if not already reduced
 598     if( (*it).second && !isContextIndependentInactive( (*it).first ) ){
 599       active.push_back( (*it).first );
 600     }
 601   }
 602 }
 603
 604 void ExtTheory::getActive( std::vector< Node >& active, Kind k ) {
 605   for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){
 606     //if not already reduced
 607     if( (*it).first.getKind()==k && (*it).second && !isContextIndependentInactive( (*it).first ) ){
 608       active.push_back( (*it).first );
 609     }
 610   }
 611 }
 612
 613 }/* CVC4::theory namespace */
 614 }/* CVC4 namespace */