src/theory/bv/bv_subtheory_core.cpp

   1 /*********************                                                        */
   2 /*! \file bv_subtheory_core.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Liana Hadarean, Aina Niemetz
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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 Algebraic solver.
  13  **
  14  ** Algebraic solver.
  15  **/
  16
  17 #include "theory/bv/bv_subtheory_core.h"
  18
  19 #include "options/bv_options.h"
  20 #include "options/smt_options.h"
  21 #include "smt/smt_statistics_registry.h"
  22 #include "theory/bv/bv_solver_lazy.h"
  23 #include "theory/bv/theory_bv_utils.h"
  24 #include "theory/ext_theory.h"
  25 #include "theory/theory_model.h"
  26
  27 using namespace std;
  28 using namespace CVC4;
  29 using namespace CVC4::context;
  30 using namespace CVC4::theory;
  31 using namespace CVC4::theory::bv;
  32 using namespace CVC4::theory::bv::utils;
  33
  34 bool CoreSolverExtTheoryCallback::getCurrentSubstitution(
  35     int effort,
  36     const std::vector<Node>& vars,
  37     std::vector<Node>& subs,
  38     std::map<Node, std::vector<Node> >& exp)
  39 {
  40   if (d_equalityEngine == nullptr)
  41   {
  42     return false;
  43   }
  44   // get the constant equivalence classes
  45   bool retVal = false;
  46   for (const Node& n : vars)
  47   {
  48     if (d_equalityEngine->hasTerm(n))
  49     {
  50       Node nr = d_equalityEngine->getRepresentative(n);
  51       if (nr.isConst())
  52       {
  53         subs.push_back(nr);
  54         exp[n].push_back(n.eqNode(nr));
  55         retVal = true;
  56       }
  57       else
  58       {
  59         subs.push_back(n);
  60       }
  61     }
  62     else
  63     {
  64       subs.push_back(n);
  65     }
  66   }
  67   // return true if the substitution is non-trivial
  68   return retVal;
  69 }
  70
  71 bool CoreSolverExtTheoryCallback::getReduction(int effort,
  72                                                Node n,
  73                                                Node& nr,
  74                                                bool& satDep)
  75 {
  76   Trace("bv-ext") << "TheoryBV::checkExt : non-reduced : " << n << std::endl;
  77   if (n.getKind() == kind::BITVECTOR_TO_NAT)
  78   {
  79     nr = utils::eliminateBv2Nat(n);
  80     satDep = false;
  81     return true;
  82   }
  83   else if (n.getKind() == kind::INT_TO_BITVECTOR)
  84   {
  85     nr = utils::eliminateInt2Bv(n);
  86     satDep = false;
  87     return true;
  88   }
  89   return false;
  90 }
  91
  92 CoreSolver::CoreSolver(context::Context* c, BVSolverLazy* bv)
  93     : SubtheorySolver(c, bv),
  94       d_notify(*this),
  95       d_isComplete(c, true),
  96       d_lemmaThreshold(16),
  97       d_preregisterCalled(false),
  98       d_checkCalled(false),
  99       d_bv(bv),
 100       d_extTheoryCb(),
 101       d_extTheory(new ExtTheory(d_extTheoryCb,
 102                                 bv->d_bv.getSatContext(),
 103                                 bv->d_bv.getUserContext(),
 104                                 bv->d_bv.getOutputChannel())),
 105       d_reasons(c),
 106       d_needsLastCallCheck(false),
 107       d_extf_range_infer(bv->d_bv.getUserContext()),
 108       d_extf_collapse_infer(bv->d_bv.getUserContext())
 109 {
 110   d_extTheory->addFunctionKind(kind::BITVECTOR_TO_NAT);
 111   d_extTheory->addFunctionKind(kind::INT_TO_BITVECTOR);
 112 }
 113
 114 CoreSolver::~CoreSolver() {}
 115
 116 bool CoreSolver::needsEqualityEngine(EeSetupInfo& esi)
 117 {
 118   esi.d_notify = &d_notify;
 119   esi.d_name = "theory::bv::ee";
 120   return true;
 121 }
 122
 123 void CoreSolver::finishInit()
 124 {
 125   // use the parent's equality engine, which may be the one we allocated above
 126   d_equalityEngine = d_bv->d_bv.getEqualityEngine();
 127
 128   // The kinds we are treating as function application in congruence
 129   d_equalityEngine->addFunctionKind(kind::BITVECTOR_CONCAT, true);
 130   //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_AND);
 131   //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_OR);
 132   //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_XOR);
 133   //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_NOT);
 134   //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_NAND);
 135   //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_NOR);
 136   //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_XNOR);
 137   //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_COMP);
 138   d_equalityEngine->addFunctionKind(kind::BITVECTOR_MULT, true);
 139   d_equalityEngine->addFunctionKind(kind::BITVECTOR_PLUS, true);
 140   d_equalityEngine->addFunctionKind(kind::BITVECTOR_EXTRACT, true);
 141   //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_SUB);
 142   //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_NEG);
 143   //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_UDIV);
 144   //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_UREM);
 145   //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_SDIV);
 146   //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_SREM);
 147   //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_SMOD);
 148   //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_SHL);
 149   //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_LSHR);
 150   //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_ASHR);
 151   //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_ULT);
 152   //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_ULE);
 153   //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_UGT);
 154   //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_UGE);
 155   //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_SLT);
 156   //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_SLE);
 157   //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_SGT);
 158   //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_SGE);
 159   d_equalityEngine->addFunctionKind(kind::BITVECTOR_TO_NAT);
 160   d_equalityEngine->addFunctionKind(kind::INT_TO_BITVECTOR);
 161 }
 162
 163 void CoreSolver::preRegister(TNode node) {
 164   d_preregisterCalled = true;
 165   if (node.getKind() == kind::EQUAL) {
 166     d_equalityEngine->addTriggerPredicate(node);
 167   } else {
 168     d_equalityEngine->addTerm(node);
 169     // Register with the extended theory, for context-dependent simplification.
 170     // Notice we do this for registered terms but not internally generated
 171     // equivalence classes. The two should roughly cooincide. Since ExtTheory is
 172     // being used as a heuristic, it is good enough to be registered here.
 173     d_extTheory->registerTerm(node);
 174   }
 175 }
 176
 177
 178 void CoreSolver::explain(TNode literal, std::vector<TNode>& assumptions) {
 179   bool polarity = literal.getKind() != kind::NOT;
 180   TNode atom = polarity ? literal : literal[0];
 181   if (atom.getKind() == kind::EQUAL) {
 182     d_equalityEngine->explainEquality(atom[0], atom[1], polarity, assumptions);
 183   } else {
 184     d_equalityEngine->explainPredicate(atom, polarity, assumptions);
 185   }
 186 }
 187
 188 bool CoreSolver::check(Theory::Effort e) {
 189   Trace("bitvector::core") << "CoreSolver::check \n";
 190
 191   d_bv->d_inferManager.spendResource(
 192       ResourceManager::Resource::TheoryCheckStep);
 193
 194   d_checkCalled = true;
 195   Assert(!d_bv->inConflict());
 196   ++(d_statistics.d_numCallstoCheck);
 197   bool ok = true;
 198   std::vector<Node> core_eqs;
 199   TNodeBoolMap seen;
 200   while (! done()) {
 201     TNode fact = get();
 202     if (d_isComplete && !isCompleteForTerm(fact, seen)) {
 203       d_isComplete = false;
 204     }
 205
 206     // only reason about equalities
 207     if (fact.getKind() == kind::EQUAL || (fact.getKind() == kind::NOT && fact[0].getKind() == kind::EQUAL)) {
 208       ok = assertFactToEqualityEngine(fact, fact);
 209     } else {
 210       ok = assertFactToEqualityEngine(fact, fact);
 211     }
 212     if (!ok)
 213       return false;
 214   }
 215
 216   if (Theory::fullEffort(e) && isComplete()) {
 217     buildModel();
 218   }
 219
 220   return true;
 221 }
 222
 223 void CoreSolver::buildModel()
 224 {
 225   Debug("bv-core") << "CoreSolver::buildModel() \n";
 226   NodeManager* nm = NodeManager::currentNM();
 227   d_modelValues.clear();
 228   TNodeSet constants;
 229   TNodeSet constants_in_eq_engine;
 230   // collect constants in equality engine
 231   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(d_equalityEngine);
 232   while (!eqcs_i.isFinished())
 233   {
 234     TNode repr = *eqcs_i;
 235     if (repr.getKind() == kind::CONST_BITVECTOR)
 236     {
 237       // must check if it's just the constant
 238       eq::EqClassIterator it(repr, d_equalityEngine);
 239       if (!(++it).isFinished() || true)
 240       {
 241         constants.insert(repr);
 242         constants_in_eq_engine.insert(repr);
 243       }
 244     }
 245     ++eqcs_i;
 246   }
 247
 248   // build repr to value map
 249
 250   eqcs_i = eq::EqClassesIterator(d_equalityEngine);
 251   while (!eqcs_i.isFinished())
 252   {
 253     TNode repr = *eqcs_i;
 254     ++eqcs_i;
 255
 256     if (!repr.isVar() && repr.getKind() != kind::CONST_BITVECTOR
 257         && !d_bv->isSharedTerm(repr))
 258     {
 259       continue;
 260     }
 261
 262     TypeNode type = repr.getType();
 263     if (type.isBitVector() && repr.getKind() != kind::CONST_BITVECTOR)
 264     {
 265       Debug("bv-core-model") << "   processing " << repr << "\n";
 266       // we need to assign a value for it
 267       TypeEnumerator te(type);
 268       Node val;
 269       do
 270       {
 271         val = *te;
 272         ++te;
 273         // Debug("bv-core-model") << "  trying value " << val << "\n";
 274         // Debug("bv-core-model") << "  is in set? " << constants.count(val) <<
 275         // "\n"; Debug("bv-core-model") << "  enumerator done? " <<
 276         // te.isFinished() << "\n";
 277       } while (constants.count(val) != 0 && !(te.isFinished()));
 278
 279       if (te.isFinished() && constants.count(val) != 0)
 280       {
 281         // if we cannot enumerate anymore values we just return the lemma
 282         // stating that at least two of the representatives are equal.
 283         std::vector<TNode> representatives;
 284         representatives.push_back(repr);
 285
 286         for (TNodeSet::const_iterator it = constants_in_eq_engine.begin();
 287              it != constants_in_eq_engine.end();
 288              ++it)
 289         {
 290           TNode constant = *it;
 291           if (utils::getSize(constant) == utils::getSize(repr))
 292           {
 293             representatives.push_back(constant);
 294           }
 295         }
 296         for (ModelValue::const_iterator it = d_modelValues.begin();
 297              it != d_modelValues.end();
 298              ++it)
 299         {
 300           representatives.push_back(it->first);
 301         }
 302         std::vector<Node> equalities;
 303         for (unsigned i = 0; i < representatives.size(); ++i)
 304         {
 305           for (unsigned j = i + 1; j < representatives.size(); ++j)
 306           {
 307             TNode a = representatives[i];
 308             TNode b = representatives[j];
 309             if (a.getKind() == kind::CONST_BITVECTOR
 310                 && b.getKind() == kind::CONST_BITVECTOR)
 311             {
 312               Assert(a != b);
 313               continue;
 314             }
 315             if (utils::getSize(a) == utils::getSize(b))
 316             {
 317               equalities.push_back(nm->mkNode(kind::EQUAL, a, b));
 318             }
 319           }
 320         }
 321         // better off letting the SAT solver split on values
 322         if (equalities.size() > d_lemmaThreshold)
 323         {
 324           d_isComplete = false;
 325           return;
 326         }
 327
 328         if (equalities.size() == 0)
 329         {
 330           Debug("bv-core") << "  lemma: true (no equalities)" << std::endl;
 331         }
 332         else
 333         {
 334           Node lemma = utils::mkOr(equalities);
 335           d_bv->lemma(lemma);
 336           Debug("bv-core") << "  lemma: " << lemma << std::endl;
 337         }
 338         return;
 339       }
 340
 341       Debug("bv-core-model") << "   " << repr << " => " << val << "\n";
 342       constants.insert(val);
 343       d_modelValues[repr] = val;
 344     }
 345   }
 346 }
 347
 348 bool CoreSolver::assertFactToEqualityEngine(TNode fact, TNode reason) {
 349   // Notify the equality engine
 350   if (!d_bv->inConflict()
 351       && (!d_bv->wasPropagatedBySubtheory(fact)
 352           || d_bv->getPropagatingSubtheory(fact) != SUB_CORE))
 353   {
 354     Debug("bv-slicer-eq") << "CoreSolver::assertFactToEqualityEngine fact=" << fact << endl;
 355     // Debug("bv-slicer-eq") << "                     reason=" << reason << endl;
 356     bool negated = fact.getKind() == kind::NOT;
 357     TNode predicate = negated ? fact[0] : fact;
 358     if (predicate.getKind() == kind::EQUAL) {
 359       if (negated) {
 360         // dis-equality
 361         d_equalityEngine->assertEquality(predicate, false, reason);
 362       } else {
 363         // equality
 364         d_equalityEngine->assertEquality(predicate, true, reason);
 365       }
 366     } else {
 367       // Adding predicate if the congruence over it is turned on
 368       if (d_equalityEngine->isFunctionKind(predicate.getKind()))
 369       {
 370         d_equalityEngine->assertPredicate(predicate, !negated, reason);
 371       }
 372     }
 373   }
 374
 375   // checking for a conflict
 376   if (d_bv->inConflict())
 377   {
 378     return false;
 379   }
 380   return true;
 381 }
 382
 383 bool CoreSolver::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool value) {
 384   Debug("bitvector::core") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false" ) << ")" << std::endl;
 385   if (value) {
 386     return d_solver.storePropagation(predicate);
 387   }
 388   return d_solver.storePropagation(predicate.notNode());
 389 }
 390
 391 bool CoreSolver::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
 392   Debug("bitvector::core") << "NotifyClass::eqNotifyTriggerTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
 393   if (value) {
 394     return d_solver.storePropagation(t1.eqNode(t2));
 395   } else {
 396     return d_solver.storePropagation(t1.eqNode(t2).notNode());
 397   }
 398 }
 399
 400 void CoreSolver::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2) {
 401   d_solver.conflict(t1, t2);
 402 }
 403
 404 bool CoreSolver::storePropagation(TNode literal) {
 405   return d_bv->storePropagation(literal, SUB_CORE);
 406 }
 407
 408 void CoreSolver::conflict(TNode a, TNode b) {
 409   std::vector<TNode> assumptions;
 410   d_equalityEngine->explainEquality(a, b, true, assumptions);
 411   Node conflict = flattenAnd(assumptions);
 412   d_bv->setConflict(conflict);
 413 }
 414
 415 bool CoreSolver::isCompleteForTerm(TNode term, TNodeBoolMap& seen) {
 416   return utils::isEqualityTerm(term, seen);
 417 }
 418
 419 bool CoreSolver::collectModelValues(TheoryModel* m,
 420                                     const std::set<Node>& termSet)
 421 {
 422   if (Debug.isOn("bitvector-model")) {
 423     context::CDQueue<Node>::const_iterator it = d_assertionQueue.begin();
 424     for (; it!= d_assertionQueue.end(); ++it) {
 425       Debug("bitvector-model")
 426           << "CoreSolver::collectModelValues (assert " << *it << ")\n";
 427     }
 428   }
 429   if (isComplete()) {
 430     Debug("bitvector-model") << "CoreSolver::collectModelValues complete.";
 431     for (ModelValue::const_iterator it = d_modelValues.begin(); it != d_modelValues.end(); ++it) {
 432       Node a = it->first;
 433       Node b = it->second;
 434       Debug("bitvector-model") << "CoreSolver::collectModelValues modelValues "
 435                                << a << " => " << b << ")\n";
 436       if (!m->assertEquality(a, b, true))
 437       {
 438         return false;
 439       }
 440     }
 441   }
 442   return true;
 443 }
 444
 445 Node CoreSolver::getModelValue(TNode var) {
 446   Debug("bitvector-model") << "CoreSolver::getModelValue (" << var <<")";
 447   Assert(isComplete());
 448   TNode repr = d_equalityEngine->getRepresentative(var);
 449   Node result = Node();
 450   if (repr.getKind() == kind::CONST_BITVECTOR) {
 451     result = repr;
 452   } else if (d_modelValues.find(repr) == d_modelValues.end()) {
 453     // it may be a shared term that never gets asserted
 454     // result is just Null
 455     Assert(d_bv->isSharedTerm(var));
 456   } else {
 457     result = d_modelValues[repr];
 458   }
 459   Debug("bitvector-model") << " => " << result <<"\n";
 460   return result;
 461 }
 462
 463 EqualityStatus CoreSolver::getEqualityStatus(TNode a, TNode b)
 464 {
 465   if (d_equalityEngine->areEqual(a, b))
 466   {
 467     // The terms are implied to be equal
 468     return EQUALITY_TRUE;
 469   }
 470   if (d_equalityEngine->areDisequal(a, b, false))
 471   {
 472     // The terms are implied to be dis-equal
 473     return EQUALITY_FALSE;
 474   }
 475   return EQUALITY_UNKNOWN;
 476 }
 477
 478 bool CoreSolver::hasTerm(TNode node) const
 479 {
 480   return d_equalityEngine->hasTerm(node);
 481 }
 482 void CoreSolver::addTermToEqualityEngine(TNode node)
 483 {
 484   d_equalityEngine->addTerm(node);
 485 }
 486
 487 CoreSolver::Statistics::Statistics()
 488   : d_numCallstoCheck("theory::bv::CoreSolver::NumCallsToCheck", 0)
 489 {
 490   smtStatisticsRegistry()->registerStat(&d_numCallstoCheck);
 491 }
 492 CoreSolver::Statistics::~Statistics() {
 493   smtStatisticsRegistry()->unregisterStat(&d_numCallstoCheck);
 494 }
 495
 496 void CoreSolver::checkExtf(Theory::Effort e)
 497 {
 498   if (e == Theory::EFFORT_LAST_CALL)
 499   {
 500     std::vector<Node> nred = d_extTheory->getActive();
 501     doExtfReductions(nred);
 502   }
 503   Assert(e == Theory::EFFORT_FULL);
 504   // do inferences (adds external lemmas)  TODO: this can be improved to add
 505   // internal inferences
 506   std::vector<Node> nred;
 507   if (d_extTheory->doInferences(0, nred))
 508   {
 509     return;
 510   }
 511   d_needsLastCallCheck = false;
 512   if (!nred.empty())
 513   {
 514     // other inferences involving bv2nat, int2bv
 515     if (options::bvAlgExtf())
 516     {
 517       if (doExtfInferences(nred))
 518       {
 519         return;
 520       }
 521     }
 522     if (!options::bvLazyReduceExtf())
 523     {
 524       if (doExtfReductions(nred))
 525       {
 526         return;
 527       }
 528     }
 529     else
 530     {
 531       d_needsLastCallCheck = true;
 532     }
 533   }
 534 }
 535
 536 bool CoreSolver::needsCheckLastEffort() const { return d_needsLastCallCheck; }
 537
 538 bool CoreSolver::doExtfInferences(std::vector<Node>& terms)
 539 {
 540   NodeManager* nm = NodeManager::currentNM();
 541   bool sentLemma = false;
 542   eq::EqualityEngine* ee = d_equalityEngine;
 543   std::map<Node, Node> op_map;
 544   for (unsigned j = 0; j < terms.size(); j++)
 545   {
 546     TNode n = terms[j];
 547     Assert(n.getKind() == kind::BITVECTOR_TO_NAT
 548            || n.getKind() == kind::INT_TO_BITVECTOR);
 549     if (n.getKind() == kind::BITVECTOR_TO_NAT)
 550     {
 551       // range lemmas
 552       if (d_extf_range_infer.find(n) == d_extf_range_infer.end())
 553       {
 554         d_extf_range_infer.insert(n);
 555         unsigned bvs = n[0].getType().getBitVectorSize();
 556         Node min = nm->mkConst(Rational(0));
 557         Node max = nm->mkConst(Rational(Integer(1).multiplyByPow2(bvs)));
 558         Node lem = nm->mkNode(kind::AND,
 559                               nm->mkNode(kind::GEQ, n, min),
 560                               nm->mkNode(kind::LT, n, max));
 561         Trace("bv-extf-lemma")
 562             << "BV extf lemma (range) : " << lem << std::endl;
 563         d_bv->d_inferManager.lemma(lem);
 564         sentLemma = true;
 565       }
 566     }
 567     Node r = (ee && ee->hasTerm(n[0])) ? ee->getRepresentative(n[0]) : n[0];
 568     op_map[r] = n;
 569   }
 570   for (unsigned j = 0; j < terms.size(); j++)
 571   {
 572     TNode n = terms[j];
 573     Node r = (ee && ee->hasTerm(n[0])) ? ee->getRepresentative(n) : n;
 574     std::map<Node, Node>::iterator it = op_map.find(r);
 575     if (it != op_map.end())
 576     {
 577       Node parent = it->second;
 578       // Node cterm = parent[0]==n ? parent : nm->mkNode( parent.getOperator(),
 579       // n );
 580       Node cterm = parent[0].eqNode(n);
 581       Trace("bv-extf-lemma-debug")
 582           << "BV extf collapse based on : " << cterm << std::endl;
 583       if (d_extf_collapse_infer.find(cterm) == d_extf_collapse_infer.end())
 584       {
 585         d_extf_collapse_infer.insert(cterm);
 586
 587         Node t = n[0];
 588         if (t.getType() == parent.getType())
 589         {
 590           if (n.getKind() == kind::INT_TO_BITVECTOR)
 591           {
 592             Assert(t.getType().isInteger());
 593             // congruent modulo 2^( bv width )
 594             unsigned bvs = n.getType().getBitVectorSize();
 595             Node coeff = nm->mkConst(Rational(Integer(1).multiplyByPow2(bvs)));
 596             Node k = nm->mkSkolem(
 597                 "int_bv_cong", t.getType(), "for int2bv/bv2nat congruence");
 598             t = nm->mkNode(kind::PLUS, t, nm->mkNode(kind::MULT, coeff, k));
 599           }
 600           Node lem = parent.eqNode(t);
 601
 602           if (parent[0] != n)
 603           {
 604             Assert(ee->areEqual(parent[0], n));
 605             lem = nm->mkNode(kind::IMPLIES, parent[0].eqNode(n), lem);
 606           }
 607           // this handles inferences of the form, e.g.:
 608           //   ((_ int2bv w) (bv2nat x)) == x (if x is bit-width w)
 609           //   (bv2nat ((_ int2bv w) x)) == x + k*2^w for some k
 610           Trace("bv-extf-lemma")
 611               << "BV extf lemma (collapse) : " << lem << std::endl;
 612           d_bv->d_inferManager.lemma(lem);
 613           sentLemma = true;
 614         }
 615       }
 616       Trace("bv-extf-lemma-debug")
 617           << "BV extf f collapse based on : " << cterm << std::endl;
 618     }
 619   }
 620   return sentLemma;
 621 }
 622
 623 bool CoreSolver::doExtfReductions(std::vector<Node>& terms)
 624 {
 625   std::vector<Node> nredr;
 626   if (d_extTheory->doReductions(0, terms, nredr))
 627   {
 628     return true;
 629   }
 630   Assert(nredr.empty());
 631   return false;
 632 }