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