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