src/theory/theory.cpp

   1 /*********************                                                        */
   2 /*! \file theory.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Tim King, Andrew Reynolds, Dejan Jovanovic
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2017 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 Theory::Theory(TheoryId id,
  55                context::Context* satContext,
  56                context::UserContext* userContext,
  57                OutputChannel& out,
  58                Valuation valuation,
  59                const LogicInfo& logicInfo,
  60                std::string name)
  61     : d_id(id),
  62       d_instanceName(name),
  63       d_satContext(satContext),
  64       d_userContext(userContext),
  65       d_logicInfo(logicInfo),
  66       d_facts(satContext),
  67       d_factsHead(satContext, 0),
  68       d_sharedTermsIndex(satContext, 0),
  69       d_careGraph(NULL),
  70       d_quantEngine(NULL),
  71       d_extTheory(NULL),
  72       d_checkTime(getStatsPrefix(id) + name + "::checkTime"),
  73       d_computeCareGraphTime(getStatsPrefix(id) + name
  74                              + "::computeCareGraphTime"),
  75       d_sharedTerms(satContext),
  76       d_out(&out),
  77       d_valuation(valuation),
  78       d_proofsEnabled(false)
  79 {
  80   smtStatisticsRegistry()->registerStat(&d_checkTime);
  81   smtStatisticsRegistry()->registerStat(&d_computeCareGraphTime);
  82 }
  83
  84 Theory::~Theory() {
  85   smtStatisticsRegistry()->unregisterStat(&d_checkTime);
  86   smtStatisticsRegistry()->unregisterStat(&d_computeCareGraphTime);
  87
  88   delete d_extTheory;
  89 }
  90
  91 TheoryId Theory::theoryOf(TheoryOfMode mode, TNode node) {
  92   TheoryId tid = THEORY_BUILTIN;
  93   switch(mode) {
  94   case THEORY_OF_TYPE_BASED:
  95     // Constants, variables, 0-ary constructors
  96     if (node.isVar()) {
  97       if( node.getKind() == kind::BOOLEAN_TERM_VARIABLE ){
  98         tid = THEORY_UF;
  99       }else{
 100         tid = Theory::theoryOf(node.getType());
 101       }
 102     }else if (node.isConst()) {
 103       tid = Theory::theoryOf(node.getType());
 104     } else if (node.getKind() == kind::EQUAL) {
 105       // Equality is owned by the theory that owns the domain
 106       tid = Theory::theoryOf(node[0].getType());
 107     } else {
 108       // Regular nodes are owned by the kind
 109       tid = kindToTheoryId(node.getKind());
 110     }
 111     break;
 112   case THEORY_OF_TERM_BASED:
 113     // Variables
 114     if (node.isVar()) {
 115       if (Theory::theoryOf(node.getType()) != theory::THEORY_BOOL) {
 116         // We treat the variables as uninterpreted
 117         tid = s_uninterpretedSortOwner;
 118       } else {
 119         if( node.getKind() == kind::BOOLEAN_TERM_VARIABLE ){
 120           //Boolean vars go to UF
 121           tid = THEORY_UF;
 122         }else{
 123           // Except for the Boolean ones
 124           tid = THEORY_BOOL;
 125         }
 126       }
 127     } else if (node.isConst()) {
 128       // Constants go to the theory of the type
 129       tid = Theory::theoryOf(node.getType());
 130     } else if (node.getKind() == kind::EQUAL) { // Equality
 131       // If one of them is an ITE, it's irelevant, since they will get replaced out anyhow
 132       if (node[0].getKind() == kind::ITE) {
 133         tid = Theory::theoryOf(node[0].getType());
 134       } else if (node[1].getKind() == kind::ITE) {
 135         tid = Theory::theoryOf(node[1].getType());
 136       } else {
 137         TNode l = node[0];
 138         TNode r = node[1];
 139         TypeNode ltype = l.getType();
 140         TypeNode rtype = r.getType();
 141         if( ltype != rtype ){
 142           tid = Theory::theoryOf(l.getType());
 143         }else {
 144           // If both sides belong to the same theory the choice is easy
 145           TheoryId T1 = Theory::theoryOf(l);
 146           TheoryId T2 = Theory::theoryOf(r);
 147           if (T1 == T2) {
 148             tid = T1;
 149           } else {
 150             TheoryId T3 = Theory::theoryOf(ltype);
 151             // This is a case of
 152             // * x*y = f(z) -> UF
 153             // * x = c      -> UF
 154             // * f(x) = read(a, y) -> either UF or ARRAY
 155             // at least one of the theories has to be parametric, i.e. theory of the type is different
 156             // from the theory of the term
 157             if (T1 == T3) {
 158               tid = T2;
 159             } else if (T2 == T3) {
 160               tid = T1;
 161             } else {
 162               // If both are parametric, we take the smaller one (arbitrary)
 163               tid = T1 < T2 ? T1 : T2;
 164             }
 165           }
 166         }
 167       }
 168     } else {
 169       // Regular nodes are owned by the kind
 170       tid = kindToTheoryId(node.getKind());
 171     }
 172     break;
 173   default:
 174     Unreachable();
 175   }
 176   Trace("theory::internal") << "theoryOf(" << mode << ", " << node << ") -> " << tid << std::endl;
 177   return tid;
 178 }
 179
 180 void Theory::addSharedTermInternal(TNode n) {
 181   Debug("sharing") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << endl;
 182   Debug("theory::assertions") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << endl;
 183   d_sharedTerms.push_back(n);
 184   addSharedTerm(n);
 185 }
 186
 187 void Theory::computeCareGraph() {
 188   Debug("sharing") << "Theory::computeCareGraph<" << getId() << ">()" << endl;
 189   for (unsigned i = 0; i < d_sharedTerms.size(); ++ i) {
 190     TNode a = d_sharedTerms[i];
 191     TypeNode aType = a.getType();
 192     for (unsigned j = i + 1; j < d_sharedTerms.size(); ++ j) {
 193       TNode b = d_sharedTerms[j];
 194       if (b.getType() != aType) {
 195         // We don't care about the terms of different types
 196         continue;
 197       }
 198       switch (d_valuation.getEqualityStatus(a, b)) {
 199       case EQUALITY_TRUE_AND_PROPAGATED:
 200       case EQUALITY_FALSE_AND_PROPAGATED:
 201         // If we know about it, we should have propagated it, so we can skip
 202         break;
 203       default:
 204         // Let's split on it
 205         addCarePair(a, b);
 206         break;
 207       }
 208     }
 209   }
 210 }
 211
 212 void Theory::printFacts(std::ostream& os) const {
 213   unsigned i, n = d_facts.size();
 214   for(i = 0; i < n; i++){
 215     const Assertion& a_i = d_facts[i];
 216     Node assertion  = a_i;
 217     os << d_id << '[' << i << ']' << " " << assertion << endl;
 218   }
 219 }
 220
 221 void Theory::debugPrintFacts() const{
 222   DebugChannel.getStream() << "Theory::debugPrintFacts()" << endl;
 223   printFacts(DebugChannel.getStream());
 224 }
 225
 226 std::unordered_set<TNode, TNodeHashFunction> Theory::currentlySharedTerms() const{
 227   std::unordered_set<TNode, TNodeHashFunction> currentlyShared;
 228   for (shared_terms_iterator i = shared_terms_begin(),
 229            i_end = shared_terms_end(); i != i_end; ++i) {
 230     currentlyShared.insert (*i);
 231   }
 232   return currentlyShared;
 233 }
 234
 235
 236 void Theory::collectTerms(TNode n, set<Node>& termSet) const
 237 {
 238   if (termSet.find(n) != termSet.end()) {
 239     return;
 240   }
 241   Trace("theory::collectTerms") << "Theory::collectTerms: adding " << n << endl;
 242   termSet.insert(n);
 243   if (n.getKind() == kind::NOT || n.getKind() == kind::EQUAL || !isLeaf(n)) {
 244     for(TNode::iterator child_it = n.begin(); child_it != n.end(); ++child_it) {
 245       collectTerms(*child_it, termSet);
 246     }
 247   }
 248 }
 249
 250
 251 void Theory::computeRelevantTerms(set<Node>& termSet, bool includeShared) const
 252 {
 253   // Collect all terms appearing in assertions
 254   context::CDList<Assertion>::const_iterator assert_it = facts_begin(), assert_it_end = facts_end();
 255   for (; assert_it != assert_it_end; ++assert_it) {
 256     collectTerms(*assert_it, termSet);
 257   }
 258
 259   if (!includeShared) return;
 260
 261   // Add terms that are shared terms
 262   context::CDList<TNode>::const_iterator shared_it = shared_terms_begin(), shared_it_end = shared_terms_end();
 263   for (; shared_it != shared_it_end; ++shared_it) {
 264     collectTerms(*shared_it, termSet);
 265   }
 266 }
 267
 268
 269 Theory::PPAssertStatus Theory::ppAssert(TNode in,
 270                                         SubstitutionMap& outSubstitutions)
 271 {
 272   if (in.getKind() == kind::EQUAL) {
 273     // (and (= x t) phi) can be replaced by phi[x/t] if
 274     // 1) x is a variable
 275     // 2) x is not in the term t
 276     // 3) x : T and t : S, then S <: T
 277     if (in[0].isVar() && !in[1].hasSubterm(in[0]) &&
 278         (in[1].getType()).isSubtypeOf(in[0].getType()) ){
 279       outSubstitutions.addSubstitution(in[0], in[1]);
 280       return PP_ASSERT_STATUS_SOLVED;
 281     }
 282     if (in[1].isVar() && !in[0].hasSubterm(in[1]) &&
 283         (in[0].getType()).isSubtypeOf(in[1].getType())){
 284       outSubstitutions.addSubstitution(in[1], in[0]);
 285       return PP_ASSERT_STATUS_SOLVED;
 286     }
 287     if (in[0].isConst() && in[1].isConst()) {
 288       if (in[0] != in[1]) {
 289         return PP_ASSERT_STATUS_CONFLICT;
 290       }
 291     }
 292   }
 293
 294   return PP_ASSERT_STATUS_UNSOLVED;
 295 }
 296
 297 std::pair<bool, Node> Theory::entailmentCheck(
 298     TNode lit,
 299     const EntailmentCheckParameters* params,
 300     EntailmentCheckSideEffects* out) {
 301   return make_pair(false, Node::null());
 302 }
 303
 304 ExtTheory* Theory::getExtTheory() {
 305   Assert(d_extTheory != NULL);
 306   return d_extTheory;
 307 }
 308
 309 void Theory::addCarePair(TNode t1, TNode t2) {
 310   if (d_careGraph) {
 311     d_careGraph->insert(CarePair(t1, t2, d_id));
 312   }
 313 }
 314
 315 void Theory::getCareGraph(CareGraph* careGraph) {
 316   Assert(careGraph != NULL);
 317
 318   Trace("sharing") << "Theory<" << getId() << ">::getCareGraph()" << std::endl;
 319   TimerStat::CodeTimer computeCareGraphTime(d_computeCareGraphTime);
 320   d_careGraph = careGraph;
 321   computeCareGraph();
 322   d_careGraph = NULL;
 323 }
 324
 325 void Theory::setQuantifiersEngine(QuantifiersEngine* qe) {
 326   Assert(d_quantEngine == NULL);
 327   Assert(qe != NULL);
 328   d_quantEngine = qe;
 329 }
 330
 331 void Theory::setupExtTheory() {
 332   Assert(d_extTheory == NULL);
 333   d_extTheory = new ExtTheory(this);
 334 }
 335
 336
 337 EntailmentCheckParameters::EntailmentCheckParameters(TheoryId tid)
 338   : d_tid(tid) {
 339 }
 340
 341 EntailmentCheckParameters::~EntailmentCheckParameters(){}
 342
 343 TheoryId EntailmentCheckParameters::getTheoryId() const {
 344   return d_tid;
 345 }
 346
 347 EntailmentCheckSideEffects::EntailmentCheckSideEffects(TheoryId tid)
 348   : d_tid(tid)
 349 {}
 350
 351 TheoryId EntailmentCheckSideEffects::getTheoryId() const {
 352   return d_tid;
 353 }
 354
 355 EntailmentCheckSideEffects::~EntailmentCheckSideEffects() {
 356 }
 357
 358
 359
 360 ExtTheory::ExtTheory( Theory * p, bool cacheEnabled ) : d_parent( p ),
 361 d_ext_func_terms( p->getSatContext() ), d_ci_inactive( p->getUserContext() ), d_has_extf( p->getSatContext() ),
 362 d_lemmas( p->getUserContext() ), d_pp_lemmas( p->getUserContext() ), d_cacheEnabled( cacheEnabled ){
 363   d_true = NodeManager::currentNM()->mkConst( true );
 364 }
 365
 366 // Gets all leaf terms in n.
 367 std::vector<Node> ExtTheory::collectVars(Node n) {
 368   std::vector<Node> vars;
 369   std::set<Node> visited;
 370   std::vector<Node> worklist;
 371   worklist.push_back(n);
 372   while (!worklist.empty()) {
 373     Node current = worklist.back();
 374     worklist.pop_back();
 375     if (current.isConst() || visited.count(current) > 0) {
 376       continue;
 377     }
 378     visited.insert(current);
 379     // Treat terms not belonging to this theory as leaf
 380     // AJR TODO : should include terms not belonging to this theory
 381     // (commented below)
 382     if (current.getNumChildren() > 0) {
 383       //&& Theory::theoryOf(n)==d_parent->getId() ){
 384       worklist.insert(worklist.end(), current.begin(), current.end());
 385     } else {
 386       vars.push_back(current);
 387     }
 388   }
 389   return vars;
 390 }
 391
 392 Node ExtTheory::getSubstitutedTerm( int effort, Node term, std::vector< Node >& exp, bool useCache ) {
 393   if( useCache ){
 394     Assert( d_gst_cache[effort].find( term )!=d_gst_cache[effort].end() );
 395     exp.insert( exp.end(), d_gst_cache[effort][term].d_exp.begin(), d_gst_cache[effort][term].d_exp.end() );
 396     return d_gst_cache[effort][term].d_sterm;
 397   }else{
 398     std::vector< Node > terms;
 399     terms.push_back( term );
 400     std::vector< Node > sterms;
 401     std::vector< std::vector< Node > > exps;
 402     getSubstitutedTerms( effort, terms, sterms, exps, useCache );
 403     Assert( sterms.size()==1 );
 404     Assert( exps.size()==1 );
 405     exp.insert( exp.end(), exps[0].begin(), exps[0].end() );
 406     return sterms[0];
 407   }
 408 }
 409
 410 //do inferences
 411 void ExtTheory::getSubstitutedTerms(int effort, const std::vector<Node>& terms,
 412                                     std::vector<Node>& sterms,
 413                                     std::vector<std::vector<Node> >& exp,
 414                                     bool useCache) {
 415   if (useCache) {
 416     for( unsigned i=0; i<terms.size(); i++ ){
 417       Node n = terms[i];
 418       Assert( d_gst_cache[effort].find( n )!=d_gst_cache[effort].end() );
 419       sterms.push_back( d_gst_cache[effort][n].d_sterm );
 420       exp.push_back( std::vector< Node >() );
 421       exp[0].insert( exp[0].end(), d_gst_cache[effort][n].d_exp.begin(), d_gst_cache[effort][n].d_exp.end() );
 422     }
 423   }else{
 424     Trace("extt-debug") << "getSubstitutedTerms for " << terms.size() << " / " << d_ext_func_terms.size() << " extended functions." << std::endl;
 425     if( !terms.empty() ){
 426       //all variables we need to find a substitution for
 427       std::vector< Node > vars;
 428       std::vector< Node > sub;
 429       std::map< Node, std::vector< Node > > expc;
 430       for( unsigned i=0; i<terms.size(); i++ ){
 431         //do substitution, rewrite
 432         Node n = terms[i];
 433         std::map< Node, ExtfInfo >::iterator iti = d_extf_info.find( n );
 434         Assert( iti!=d_extf_info.end() );
 435         for( unsigned i=0; i<iti->second.d_vars.size(); i++ ){
 436           if( std::find( vars.begin(), vars.end(), iti->second.d_vars[i] )==vars.end() ){
 437             vars.push_back( iti->second.d_vars[i] );
 438           }
 439         }
 440       }
 441       bool useSubs = d_parent->getCurrentSubstitution( effort, vars, sub, expc );
 442       //get the current substitution for all variables
 443       Assert( !useSubs || vars.size()==sub.size() );
 444       for( unsigned i=0; i<terms.size(); i++ ){
 445         Node n = terms[i];
 446         Node ns = n;
 447         std::vector< Node > expn;
 448         if( useSubs ){
 449           //do substitution
 450           ns = n.substitute( vars.begin(), vars.end(), sub.begin(), sub.end() );
 451           if( ns!=n ){
 452             //build explanation: explanation vars = sub for each vars in FV( n )
 453             std::map< Node, ExtfInfo >::iterator iti = d_extf_info.find( n );
 454             Assert( iti!=d_extf_info.end() );
 455             for( unsigned j=0; j<iti->second.d_vars.size(); j++ ){
 456               Node v = iti->second.d_vars[j];
 457               std::map< Node, std::vector< Node > >::iterator itx = expc.find( v );
 458               if( itx!=expc.end() ){
 459                 for( unsigned k=0; k<itx->second.size(); k++ ){
 460                   if( std::find( expn.begin(), expn.end(), itx->second[k] )==expn.end() ){
 461                     expn.push_back( itx->second[k] );
 462                   }
 463                 }
 464               }
 465             }
 466           }
 467           Trace("extt-debug") << "  have " << n << " == " << ns << ", exp size=" << expn.size() << "." << std::endl;
 468         }
 469         //add to vector
 470         sterms.push_back( ns );
 471         exp.push_back( expn );
 472         //add to cache
 473         if( d_cacheEnabled ){
 474           d_gst_cache[effort][n].d_sterm = ns;
 475           d_gst_cache[effort][n].d_exp.clear();
 476           d_gst_cache[effort][n].d_exp.insert( d_gst_cache[effort][n].d_exp.end(), expn.begin(), expn.end() );
 477         }
 478       }
 479     }
 480   }
 481 }
 482
 483 bool ExtTheory::doInferencesInternal(int effort, const std::vector<Node>& terms,
 484                                      std::vector<Node>& nred, bool batch,
 485                                      bool isRed) {
 486   if (batch) {
 487     bool addedLemma = false;
 488     if( isRed ){
 489       for( unsigned i=0; i<terms.size(); i++ ){
 490         Node n = terms[i];
 491         Node nr;
 492         //TODO: reduction with substitution?
 493         int ret = d_parent->getReduction( effort, n, nr );
 494         if( ret==0 ){
 495           nred.push_back( n );
 496         }else{
 497           if( !nr.isNull() && n!=nr ){
 498             Node lem = NodeManager::currentNM()->mkNode( kind::EQUAL, n, nr );
 499             if( sendLemma( lem, true ) ){
 500               Trace("extt-lemma") << "ExtTheory : reduction lemma : " << lem << std::endl;
 501               addedLemma = true;
 502             }
 503           }
 504           markReduced( terms[i], ret<0 );
 505         }
 506       }
 507     }else{
 508       std::vector< Node > sterms;
 509       std::vector< std::vector< Node > > exp;
 510       getSubstitutedTerms( effort, terms, sterms, exp );
 511       std::map< Node, unsigned > sterm_index;
 512       for( unsigned i=0; i<terms.size(); i++ ){
 513         bool processed = false;
 514         if( sterms[i]!=terms[i] ){
 515           Node sr = Rewriter::rewrite( sterms[i] );
 516           //ask the theory if this term is reduced, e.g. is it constant or it is a non-extf term.
 517           if( d_parent->isExtfReduced( effort, sr, terms[i], exp[i] ) ){
 518             processed = true;
 519             markReduced( terms[i] );
 520             Node eq = terms[i].eqNode( sr );
 521             Node expn = exp[i].size()>1 ? NodeManager::currentNM()->mkNode( kind::AND, exp[i] ) : ( exp[i].size()==1 ? exp[i][0] : d_true );
 522             Trace("extt-debug") << "ExtTheory::doInferences : infer : " << eq << " by " << expn << std::endl;
 523             Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, expn, eq );
 524             Trace("extt-debug") << "...send lemma " << lem << std::endl;
 525             if( sendLemma( lem ) ){
 526               Trace("extt-lemma") << "ExtTheory : substitution + rewrite lemma : " << lem << std::endl;
 527               addedLemma = true;
 528             }
 529           }else{
 530             //check if we have already reduced this
 531             std::map< Node, unsigned >::iterator itsi = sterm_index.find( sr );
 532             if( itsi!=sterm_index.end() ){
 533               //unsigned j = itsi->second;
 534               //can add (non-reducing) lemma : exp[j] ^ exp[i] => sterms[i] = sterms[j]
 535               //TODO
 536             }else{
 537               sterm_index[sr] = i;
 538             }
 539             //check if we reduce to another active term?
 540
 541             Trace("extt-nred") << "Non-reduced term : " << sr << std::endl;
 542           }
 543         }else{
 544           Trace("extt-nred") << "Non-reduced term : " << sterms[i] << std::endl;
 545         }
 546         if( !processed ){
 547           nred.push_back( terms[i] );
 548         }
 549       }
 550     }
 551     return addedLemma;
 552   }else{
 553     std::vector< Node > nnred;
 554     if( terms.empty() ){
 555       for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){
 556         if( (*it).second && !isContextIndependentInactive( (*it).first ) ){
 557           std::vector< Node > nterms;
 558           nterms.push_back( (*it).first );
 559           if( doInferencesInternal( effort, nterms, nnred, true, isRed ) ){
 560             return true;
 561           }
 562         }
 563       }
 564     }else{
 565       for( unsigned i=0; i<terms.size(); i++ ){
 566         std::vector< Node > nterms;
 567         nterms.push_back( terms[i] );
 568         if( doInferencesInternal( effort, nterms, nnred, true, isRed ) ){
 569           return true;
 570         }
 571       }
 572     }
 573     return false;
 574   }
 575 }
 576
 577 bool ExtTheory::sendLemma( Node lem, bool preprocess ) {
 578   if( preprocess ){
 579     if( d_pp_lemmas.find( lem )==d_pp_lemmas.end() ){
 580       d_pp_lemmas.insert( lem );
 581       d_parent->getOutputChannel().lemma( lem, false, true );
 582       return true;
 583     }
 584   }else{
 585     if( d_lemmas.find( lem )==d_lemmas.end() ){
 586       d_lemmas.insert( lem );
 587       d_parent->getOutputChannel().lemma( lem );
 588       return true;
 589     }
 590   }
 591   return false;
 592 }
 593
 594 bool ExtTheory::doInferences(int effort, const std::vector<Node>& terms,
 595                              std::vector<Node>& nred, bool batch) {
 596   if (!terms.empty()) {
 597     return doInferencesInternal( effort, terms, nred, batch, false );
 598   }else{
 599     return false;
 600   }
 601 }
 602
 603 bool ExtTheory::doInferences( int effort, std::vector< Node >& nred, bool batch ) {
 604   std::vector< Node > terms = getActive();
 605   return doInferencesInternal( effort, terms, nred, batch, false );
 606 }
 607
 608 bool ExtTheory::doReductions(int effort, const std::vector<Node>& terms,
 609                              std::vector<Node>& nred, bool batch) {
 610   if (!terms.empty()) {
 611     return doInferencesInternal( effort, terms, nred, batch, true );
 612   }else{
 613     return false;
 614   }
 615 }
 616
 617 bool ExtTheory::doReductions(int effort, std::vector<Node>& nred, bool batch) {
 618   const std::vector<Node> terms = getActive();
 619   return doInferencesInternal(effort, terms, nred, batch, true);
 620 }
 621
 622 // Register term.
 623 void ExtTheory::registerTerm(Node n) {
 624   if (d_extf_kind.find(n.getKind()) != d_extf_kind.end()) {
 625     if (d_ext_func_terms.find(n) == d_ext_func_terms.end()) {
 626       Trace("extt-debug") << "Found extended function : " << n << " in "
 627                           << d_parent->getId() << std::endl;
 628       d_ext_func_terms[n] = true;
 629       d_has_extf = n;
 630       d_extf_info[n].d_vars = collectVars(n);
 631     }
 632   }
 633 }
 634
 635 void ExtTheory::registerTermRec(Node n) {
 636   std::set<Node> visited;
 637   registerTermRec(n, &visited);
 638 }
 639
 640 void ExtTheory::registerTermRec(Node n, std::set<Node>* visited) {
 641   if (visited->find(n) == visited->end()) {
 642     visited->insert(n);
 643     registerTerm(n);
 644     for (unsigned i = 0; i < n.getNumChildren(); i++) {
 645       registerTermRec(n[i], visited);
 646     }
 647   }
 648 }
 649
 650 //mark reduced
 651 void ExtTheory::markReduced( Node n, bool contextDepend ) {
 652   registerTerm( n );
 653   Assert( d_ext_func_terms.find( n )!=d_ext_func_terms.end() );
 654   d_ext_func_terms[n] = false;
 655   if( !contextDepend ){
 656     d_ci_inactive.insert( n );
 657   }
 658
 659   //update has_extf
 660   if( d_has_extf.get()==n ){
 661     for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){
 662       //if not already reduced
 663       if( (*it).second && !isContextIndependentInactive( (*it).first ) ){
 664          d_has_extf = (*it).first;
 665       }
 666     }
 667
 668   }
 669 }
 670
 671 //mark congruent
 672 void ExtTheory::markCongruent( Node a, Node b ) {
 673   Trace("extt-debug") << "Mark congruent : " << a << " " << b << std::endl;
 674   registerTerm( a );
 675   registerTerm( b );
 676   NodeBoolMap::const_iterator it = d_ext_func_terms.find( b );
 677   if( it!=d_ext_func_terms.end() ){
 678     if( d_ext_func_terms.find( a )!=d_ext_func_terms.end() ){
 679       d_ext_func_terms[a] = d_ext_func_terms[a] && (*it).second;
 680     }else{
 681       Assert( false );
 682     }
 683     d_ext_func_terms[b] = false;
 684   }else{
 685     Assert( false );
 686   }
 687 }
 688
 689 bool ExtTheory::isContextIndependentInactive(Node n) const {
 690   return d_ci_inactive.find(n) != d_ci_inactive.end();
 691 }
 692
 693
 694 void ExtTheory::getTerms( std::vector< Node >& terms ) {
 695   for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){
 696     terms.push_back( (*it).first );
 697   }
 698 }
 699
 700 bool ExtTheory::hasActiveTerm() {
 701   return !d_has_extf.get().isNull();
 702 }
 703
 704 //is active
 705 bool ExtTheory::isActive( Node n ) {
 706   NodeBoolMap::const_iterator it = d_ext_func_terms.find( n );
 707   if( it!=d_ext_func_terms.end() ){
 708     return (*it).second && !isContextIndependentInactive( n );
 709   }else{
 710     return false;
 711   }
 712 }
 713
 714 // get active
 715 std::vector<Node> ExtTheory::getActive() const {
 716   std::vector<Node> active;
 717   for (NodeBoolMap::iterator it = d_ext_func_terms.begin();
 718        it != d_ext_func_terms.end(); ++it) {
 719     // if not already reduced
 720     if ((*it).second && !isContextIndependentInactive((*it).first)) {
 721       active.push_back((*it).first);
 722     }
 723   }
 724   return active;
 725 }
 726
 727 std::vector<Node> ExtTheory::getActive(Kind k) const {
 728   std::vector<Node> active;
 729   for (NodeBoolMap::iterator it = d_ext_func_terms.begin();
 730        it != d_ext_func_terms.end(); ++it) {
 731     // if not already reduced
 732     if ((*it).first.getKind() == k && (*it).second &&
 733         !isContextIndependentInactive((*it).first)) {
 734       active.push_back((*it).first);
 735     }
 736   }
 737   return active;
 738 }
 739
 740 void ExtTheory::clearCache() {
 741   d_gst_cache.clear();
 742 }
 743
 744 }/* CVC4::theory namespace */
 745 }/* CVC4 namespace */