src/theory/bv/bv_solver_layered.cpp

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Mathias Preiner, Liana Hadarean, Andrew Reynolds
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 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.
  11  * ****************************************************************************
  12  *
  13  * Layered bit-vector solver.
  14  */
  15
  16 #include "theory/bv/bv_solver_layered.h"
  17
  18 #include "expr/node_algorithm.h"
  19 #include "options/bv_options.h"
  20 #include "options/smt_options.h"
  21 #include "smt/smt_statistics_registry.h"
  22 #include "theory/bv/abstraction.h"
  23 #include "theory/bv/bv_eager_solver.h"
  24 #include "theory/bv/bv_subtheory_algebraic.h"
  25 #include "theory/bv/bv_subtheory_bitblast.h"
  26 #include "theory/bv/bv_subtheory_core.h"
  27 #include "theory/bv/bv_subtheory_inequality.h"
  28 #include "theory/bv/theory_bv_rewrite_rules_normalization.h"
  29 #include "theory/bv/theory_bv_rewrite_rules_simplification.h"
  30 #include "theory/bv/theory_bv_rewriter.h"
  31 #include "theory/bv/theory_bv_utils.h"
  32 #include "theory/theory_model.h"
  33
  34 using namespace cvc5::theory::bv::utils;
  35
  36 namespace cvc5 {
  37 namespace theory {
  38 namespace bv {
  39
  40 BVSolverLayered::BVSolverLayered(TheoryBV& bv,
  41                                  Env& env,
  42                                  context::Context* c,
  43                                  context::UserContext* u,
  44                                  ProofNodeManager* pnm,
  45                                  std::string name)
  46     : BVSolver(env, bv.d_state, bv.d_im),
  47       d_bv(bv),
  48       d_context(c),
  49       d_alreadyPropagatedSet(c),
  50       d_sharedTermsSet(c),
  51       d_subtheories(),
  52       d_subtheoryMap(),
  53       d_statistics(),
  54       d_staticLearnCache(),
  55       d_lemmasAdded(c, false),
  56       d_conflict(c, false),
  57       d_invalidateModelCache(c, true),
  58       d_literalsToPropagate(c),
  59       d_literalsToPropagateIndex(c, 0),
  60       d_propagatedBy(c),
  61       d_eagerSolver(),
  62       d_abstractionModule(new AbstractionModule(getStatsPrefix(THEORY_BV))),
  63       d_calledPreregister(false)
  64 {
  65   if (options().bv.bitblastMode == options::BitblastMode::EAGER)
  66   {
  67     d_eagerSolver.reset(new EagerBitblastSolver(c, this));
  68     return;
  69   }
  70
  71   if (options().bv.bitvectorEqualitySolver)
  72   {
  73     d_subtheories.emplace_back(new CoreSolver(c, this));
  74     d_subtheoryMap[SUB_CORE] = d_subtheories.back().get();
  75   }
  76
  77   if (options().bv.bitvectorInequalitySolver)
  78   {
  79     d_subtheories.emplace_back(new InequalitySolver(c, u, this));
  80     d_subtheoryMap[SUB_INEQUALITY] = d_subtheories.back().get();
  81   }
  82
  83   if (options().bv.bitvectorAlgebraicSolver)
  84   {
  85     d_subtheories.emplace_back(new AlgebraicSolver(c, this));
  86     d_subtheoryMap[SUB_ALGEBRAIC] = d_subtheories.back().get();
  87   }
  88
  89   BitblastSolver* bb_solver = new BitblastSolver(c, this);
  90   if (options().bv.bvAbstraction)
  91   {
  92     bb_solver->setAbstraction(d_abstractionModule.get());
  93   }
  94   d_subtheories.emplace_back(bb_solver);
  95   d_subtheoryMap[SUB_BITBLAST] = bb_solver;
  96 }
  97
  98 BVSolverLayered::~BVSolverLayered() {}
  99
 100 bool BVSolverLayered::needsEqualityEngine(EeSetupInfo& esi)
 101 {
 102   CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
 103   if (core)
 104   {
 105     return core->needsEqualityEngine(esi);
 106   }
 107   // otherwise we don't use an equality engine
 108   return false;
 109 }
 110
 111 void BVSolverLayered::finishInit()
 112 {
 113   CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
 114   if (core)
 115   {
 116     // must finish initialization in the core solver
 117     core->finishInit();
 118   }
 119 }
 120
 121 void BVSolverLayered::spendResource(Resource r) { d_im.spendResource(r); }
 122
 123 BVSolverLayered::Statistics::Statistics()
 124     : d_avgConflictSize(smtStatisticsRegistry().registerAverage(
 125         "theory::bv::lazy::AvgBVConflictSize")),
 126       d_solveTimer(smtStatisticsRegistry().registerTimer(
 127           "theory::bv::lazy::solveTimer")),
 128       d_numCallsToCheckFullEffort(smtStatisticsRegistry().registerInt(
 129           "theory::bv::lazy::NumFullCheckCalls")),
 130       d_numCallsToCheckStandardEffort(smtStatisticsRegistry().registerInt(
 131           "theory::bv::lazy::NumStandardCheckCalls")),
 132       d_weightComputationTimer(smtStatisticsRegistry().registerTimer(
 133           "theory::bv::lazy::weightComputationTimer")),
 134       d_numMultSlice(smtStatisticsRegistry().registerInt(
 135           "theory::bv::lazy::NumMultSliceApplied"))
 136 {
 137 }
 138
 139 void BVSolverLayered::preRegisterTerm(TNode node)
 140 {
 141   d_calledPreregister = true;
 142   Debug("bitvector-preregister")
 143       << "BVSolverLayered::preRegister(" << node << ")" << std::endl;
 144
 145   if (options().bv.bitblastMode == options::BitblastMode::EAGER)
 146   {
 147     // the aig bit-blaster option is set heuristically
 148     // if bv abstraction is used
 149     if (!d_eagerSolver->isInitialized())
 150     {
 151       d_eagerSolver->initialize();
 152     }
 153
 154     if (node.getKind() == kind::BITVECTOR_EAGER_ATOM)
 155     {
 156       Node formula = node[0];
 157       d_eagerSolver->assertFormula(formula);
 158     }
 159     return;
 160   }
 161
 162   for (unsigned i = 0; i < d_subtheories.size(); ++i)
 163   {
 164     d_subtheories[i]->preRegister(node);
 165   }
 166
 167   // AJR : equality solver currently registers all terms to ExtTheory, if we
 168   // want a lazy reduction without the bv equality solver, need to call this
 169   // d_bv.d_extTheory->registerTermRec( node );
 170 }
 171
 172 void BVSolverLayered::sendConflict()
 173 {
 174   Assert(d_conflict);
 175   if (d_conflictNode.isNull())
 176   {
 177     return;
 178   }
 179   else
 180   {
 181     Debug("bitvector") << indent() << "BVSolverLayered::check(): conflict "
 182                        << d_conflictNode << std::endl;
 183     d_im.conflict(d_conflictNode, InferenceId::BV_LAYERED_CONFLICT);
 184     d_statistics.d_avgConflictSize << d_conflictNode.getNumChildren();
 185     d_conflictNode = Node::null();
 186   }
 187 }
 188
 189 void BVSolverLayered::checkForLemma(TNode fact)
 190 {
 191   if (fact.getKind() == kind::EQUAL)
 192   {
 193     NodeManager* nm = NodeManager::currentNM();
 194     if (fact[0].getKind() == kind::BITVECTOR_UREM)
 195     {
 196       TNode urem = fact[0];
 197       TNode result = fact[1];
 198       TNode divisor = urem[1];
 199       Node result_ult_div = nm->mkNode(kind::BITVECTOR_ULT, result, divisor);
 200       Node divisor_eq_0 =
 201           nm->mkNode(kind::EQUAL, divisor, mkZero(getSize(divisor)));
 202       Node split = nm->mkNode(
 203           kind::OR, divisor_eq_0, nm->mkNode(kind::NOT, fact), result_ult_div);
 204       lemma(split);
 205     }
 206     if (fact[1].getKind() == kind::BITVECTOR_UREM)
 207     {
 208       TNode urem = fact[1];
 209       TNode result = fact[0];
 210       TNode divisor = urem[1];
 211       Node result_ult_div = nm->mkNode(kind::BITVECTOR_ULT, result, divisor);
 212       Node divisor_eq_0 =
 213           nm->mkNode(kind::EQUAL, divisor, mkZero(getSize(divisor)));
 214       Node split = nm->mkNode(
 215           kind::OR, divisor_eq_0, nm->mkNode(kind::NOT, fact), result_ult_div);
 216       lemma(split);
 217     }
 218   }
 219 }
 220
 221 bool BVSolverLayered::preCheck(Theory::Effort e)
 222 {
 223   check(e);
 224   return true;
 225 }
 226
 227 void BVSolverLayered::check(Theory::Effort e)
 228 {
 229   if (done() && e < Theory::EFFORT_FULL)
 230   {
 231     return;
 232   }
 233
 234   Debug("bitvector") << "BVSolverLayered::check(" << e << ")" << std::endl;
 235   TimerStat::CodeTimer codeTimer(d_statistics.d_solveTimer);
 236   // we may be getting new assertions so the model cache may not be sound
 237   d_invalidateModelCache.set(true);
 238   // if we are using the eager solver
 239   if (options().bv.bitblastMode == options::BitblastMode::EAGER)
 240   {
 241     // this can only happen on an empty benchmark
 242     if (!d_eagerSolver->isInitialized())
 243     {
 244       d_eagerSolver->initialize();
 245     }
 246     if (!Theory::fullEffort(e)) return;
 247
 248     std::vector<TNode> assertions;
 249     while (!done())
 250     {
 251       TNode fact = get().d_assertion;
 252       Assert(fact.getKind() == kind::BITVECTOR_EAGER_ATOM);
 253       assertions.push_back(fact);
 254       d_eagerSolver->assertFormula(fact[0]);
 255     }
 256
 257     bool ok = d_eagerSolver->checkSat();
 258     if (!ok)
 259     {
 260       if (assertions.size() == 1)
 261       {
 262         d_im.conflict(assertions[0], InferenceId::BV_LAYERED_CONFLICT);
 263         return;
 264       }
 265       Node conflict = utils::mkAnd(assertions);
 266       d_im.conflict(conflict, InferenceId::BV_LAYERED_CONFLICT);
 267       return;
 268     }
 269     return;
 270   }
 271
 272   if (Theory::fullEffort(e))
 273   {
 274     ++(d_statistics.d_numCallsToCheckFullEffort);
 275   }
 276   else
 277   {
 278     ++(d_statistics.d_numCallsToCheckStandardEffort);
 279   }
 280   // if we are already in conflict just return the conflict
 281   if (inConflict())
 282   {
 283     sendConflict();
 284     return;
 285   }
 286
 287   while (!done())
 288   {
 289     TNode fact = get().d_assertion;
 290
 291     checkForLemma(fact);
 292
 293     for (unsigned i = 0; i < d_subtheories.size(); ++i)
 294     {
 295       d_subtheories[i]->assertFact(fact);
 296     }
 297   }
 298
 299   bool ok = true;
 300   bool complete = false;
 301   for (unsigned i = 0; i < d_subtheories.size(); ++i)
 302   {
 303     Assert(!inConflict());
 304     ok = d_subtheories[i]->check(e);
 305     complete = d_subtheories[i]->isComplete();
 306
 307     if (!ok)
 308     {
 309       // if we are in a conflict no need to check with other theories
 310       Assert(inConflict());
 311       sendConflict();
 312       return;
 313     }
 314     if (complete)
 315     {
 316       // if the last subtheory was complete we stop
 317       break;
 318     }
 319   }
 320 }
 321
 322 bool BVSolverLayered::collectModelValues(TheoryModel* m,
 323                                          const std::set<Node>& termSet)
 324 {
 325   Assert(!inConflict());
 326   if (options().bv.bitblastMode == options::BitblastMode::EAGER)
 327   {
 328     if (!d_eagerSolver->collectModelInfo(m, true))
 329     {
 330       return false;
 331     }
 332   }
 333   for (unsigned i = 0; i < d_subtheories.size(); ++i)
 334   {
 335     if (d_subtheories[i]->isComplete())
 336     {
 337       return d_subtheories[i]->collectModelValues(m, termSet);
 338     }
 339   }
 340   return true;
 341 }
 342
 343 Node BVSolverLayered::getModelValue(TNode var)
 344 {
 345   Assert(!inConflict());
 346   for (unsigned i = 0; i < d_subtheories.size(); ++i)
 347   {
 348     if (d_subtheories[i]->isComplete())
 349     {
 350       return d_subtheories[i]->getModelValue(var);
 351     }
 352   }
 353   Unreachable();
 354 }
 355
 356 void BVSolverLayered::propagate(Theory::Effort e)
 357 {
 358   Debug("bitvector") << indent() << "BVSolverLayered::propagate()" << std::endl;
 359   if (options().bv.bitblastMode == options::BitblastMode::EAGER)
 360   {
 361     return;
 362   }
 363
 364   if (inConflict())
 365   {
 366     return;
 367   }
 368
 369   // go through stored propagations
 370   bool ok = true;
 371   for (; d_literalsToPropagateIndex < d_literalsToPropagate.size() && ok;
 372        d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1)
 373   {
 374     TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex];
 375     // temporary fix for incremental bit-blasting
 376     if (d_state.isSatLiteral(literal))
 377     {
 378       Debug("bitvector::propagate")
 379           << "BVSolverLayered:: propagating " << literal << "\n";
 380       ok = d_im.propagateLit(literal);
 381     }
 382   }
 383
 384   if (!ok)
 385   {
 386     Debug("bitvector::propagate")
 387         << indent()
 388         << "BVSolverLayered::propagate(): conflict from theory engine"
 389         << std::endl;
 390     setConflict();
 391   }
 392 }
 393
 394 TrustNode BVSolverLayered::ppRewrite(TNode t)
 395 {
 396   Debug("bv-pp-rewrite") << "BVSolverLayered::ppRewrite " << t << "\n";
 397   Node res = t;
 398   if (options().bv.bitwiseEq && RewriteRule<BitwiseEq>::applies(t))
 399   {
 400     Node result = RewriteRule<BitwiseEq>::run<false>(t);
 401     res = rewrite(result);
 402   }
 403   else if (RewriteRule<UltAddOne>::applies(t))
 404   {
 405     Node result = RewriteRule<UltAddOne>::run<false>(t);
 406     res = rewrite(result);
 407   }
 408   else if (res.getKind() == kind::EQUAL
 409            && ((res[0].getKind() == kind::BITVECTOR_ADD
 410                 && RewriteRule<ConcatToMult>::applies(res[1]))
 411                || (res[1].getKind() == kind::BITVECTOR_ADD
 412                    && RewriteRule<ConcatToMult>::applies(res[0]))))
 413   {
 414     Node mult = RewriteRule<ConcatToMult>::applies(res[0])
 415                     ? RewriteRule<ConcatToMult>::run<false>(res[0])
 416                     : RewriteRule<ConcatToMult>::run<true>(res[1]);
 417     Node factor = mult[0];
 418     Node sum = RewriteRule<ConcatToMult>::applies(res[0]) ? res[1] : res[0];
 419     Node new_eq = NodeManager::currentNM()->mkNode(kind::EQUAL, sum, mult);
 420     Node rewr_eq = RewriteRule<SolveEq>::run<true>(new_eq);
 421     if (rewr_eq[0].isVar() || rewr_eq[1].isVar())
 422     {
 423       res = rewrite(rewr_eq);
 424     }
 425     else
 426     {
 427       res = t;
 428     }
 429   }
 430   else if (RewriteRule<SignExtendEqConst>::applies(t))
 431   {
 432     res = RewriteRule<SignExtendEqConst>::run<false>(t);
 433   }
 434   else if (RewriteRule<ZeroExtendEqConst>::applies(t))
 435   {
 436     res = RewriteRule<ZeroExtendEqConst>::run<false>(t);
 437   }
 438   else if (RewriteRule<NormalizeEqAddNeg>::applies(t))
 439   {
 440     res = RewriteRule<NormalizeEqAddNeg>::run<false>(t);
 441   }
 442
 443   // if(t.getKind() == kind::EQUAL &&
 444   //    ((t[0].getKind() == kind::BITVECTOR_MULT && t[1].getKind() ==
 445   //    kind::BITVECTOR_ADD) ||
 446   //     (t[1].getKind() == kind::BITVECTOR_MULT && t[0].getKind() ==
 447   //     kind::BITVECTOR_ADD))) {
 448   //   // if we have an equality between a multiplication and addition
 449   //   // try to express multiplication in terms of addition
 450   //   Node mult = t[0].getKind() == kind::BITVECTOR_MULT? t[0] : t[1];
 451   //   Node add = t[0].getKind() == kind::BITVECTOR_ADD? t[0] : t[1];
 452   //   if (RewriteRule<MultSlice>::applies(mult)) {
 453   //     Node new_mult = RewriteRule<MultSlice>::run<false>(mult);
 454   //     Node new_eq =
 455   //     rewrite(NodeManager::currentNM()->mkNode(kind::EQUAL,
 456   //     new_mult, add));
 457
 458   //     // the simplification can cause the formula to blow up
 459   //     // only apply if formula reduced
 460   //     if (d_subtheoryMap.find(SUB_BITBLAST) != d_subtheoryMap.end()) {
 461   //       BitblastSolver* bv = (BitblastSolver*)d_subtheoryMap[SUB_BITBLAST];
 462   //       uint64_t old_size = bv->computeAtomWeight(t);
 463   //       Assert (old_size);
 464   //       uint64_t new_size = bv->computeAtomWeight(new_eq);
 465   //       double ratio = ((double)new_size)/old_size;
 466   //       if (ratio <= 0.4) {
 467   //         ++(d_statistics.d_numMultSlice);
 468   //         return new_eq;
 469   //       }
 470   //     }
 471
 472   //     if (new_eq.getKind() == kind::CONST_BOOLEAN) {
 473   //       ++(d_statistics.d_numMultSlice);
 474   //       return new_eq;
 475   //     }
 476   //   }
 477   // }
 478
 479   if (options().bv.bvAbstraction && t.getType().isBoolean())
 480   {
 481     d_abstractionModule->addInputAtom(res);
 482   }
 483   Debug("bv-pp-rewrite") << "to   " << res << "\n";
 484   if (res != t)
 485   {
 486     return TrustNode::mkTrustRewrite(t, res, nullptr);
 487   }
 488   return TrustNode::null();
 489 }
 490
 491 void BVSolverLayered::presolve()
 492 {
 493   Debug("bitvector") << "BVSolverLayered::presolve" << std::endl;
 494 }
 495
 496 static int prop_count = 0;
 497
 498 bool BVSolverLayered::storePropagation(TNode literal, SubTheory subtheory)
 499 {
 500   Debug("bitvector::propagate")
 501       << indent() << d_context->getLevel() << " "
 502       << "BVSolverLayered::storePropagation(" << literal << ", " << subtheory
 503       << ")" << std::endl;
 504   prop_count++;
 505
 506   // If already in conflict, no more propagation
 507   if (d_conflict)
 508   {
 509     Debug("bitvector::propagate")
 510         << indent() << "BVSolverLayered::storePropagation(" << literal << ", "
 511         << subtheory << "): already in conflict" << std::endl;
 512     return false;
 513   }
 514
 515   // If propagated already, just skip
 516   PropagatedMap::const_iterator find = d_propagatedBy.find(literal);
 517   if (find != d_propagatedBy.end())
 518   {
 519     return true;
 520   }
 521   else
 522   {
 523     bool polarity = literal.getKind() != kind::NOT;
 524     Node negatedLiteral = polarity ? literal.notNode() : (Node)literal[0];
 525     find = d_propagatedBy.find(negatedLiteral);
 526     if (find != d_propagatedBy.end() && (*find).second != subtheory)
 527     {
 528       // Safe to ignore this one, subtheory should produce a conflict
 529       return true;
 530     }
 531
 532     d_propagatedBy[literal] = subtheory;
 533   }
 534
 535   // Propagate differs depending on the subtheory
 536   // * bitblaster needs to be left alone until it's done, otherwise it doesn't
 537   //   know how to explain
 538   // * equality engine can propagate eagerly
 539   // TODO(2348): Determine if ok should be set by propagate. If not, remove ok.
 540   constexpr bool ok = true;
 541   if (subtheory == SUB_CORE)
 542   {
 543     d_im.propagateLit(literal);
 544     if (!ok)
 545     {
 546       setConflict();
 547     }
 548   }
 549   else
 550   {
 551     d_literalsToPropagate.push_back(literal);
 552   }
 553   return ok;
 554
 555 } /* BVSolverLayered::propagate(TNode) */
 556
 557 void BVSolverLayered::explain(TNode literal, std::vector<TNode>& assumptions)
 558 {
 559   Assert(wasPropagatedBySubtheory(literal));
 560   SubTheory sub = getPropagatingSubtheory(literal);
 561   d_subtheoryMap[sub]->explain(literal, assumptions);
 562 }
 563
 564 TrustNode BVSolverLayered::explain(TNode node)
 565 {
 566   Debug("bitvector::explain")
 567       << "BVSolverLayered::explain(" << node << ")" << std::endl;
 568   std::vector<TNode> assumptions;
 569
 570   // Ask for the explanation
 571   explain(node, assumptions);
 572   // this means that it is something true at level 0
 573   Node explanation;
 574   if (assumptions.size() == 0)
 575   {
 576     explanation = utils::mkTrue();
 577   }
 578   else
 579   {
 580     // return the explanation
 581     explanation = utils::mkAnd(assumptions);
 582   }
 583   Debug("bitvector::explain") << "BVSolverLayered::explain(" << node << ") => "
 584                               << explanation << std::endl;
 585   Debug("bitvector::explain") << "BVSolverLayered::explain done. \n";
 586   return TrustNode::mkTrustPropExp(node, explanation, nullptr);
 587 }
 588
 589 void BVSolverLayered::notifySharedTerm(TNode t)
 590 {
 591   Debug("bitvector::sharing")
 592       << indent() << "BVSolverLayered::notifySharedTerm(" << t << ")"
 593       << std::endl;
 594   d_sharedTermsSet.insert(t);
 595 }
 596
 597 EqualityStatus BVSolverLayered::getEqualityStatus(TNode a, TNode b)
 598 {
 599   if (options().bv.bitblastMode == options::BitblastMode::EAGER)
 600     return EQUALITY_UNKNOWN;
 601   Assert(options().bv.bitblastMode == options::BitblastMode::LAZY);
 602   for (unsigned i = 0; i < d_subtheories.size(); ++i)
 603   {
 604     EqualityStatus status = d_subtheories[i]->getEqualityStatus(a, b);
 605     if (status != EQUALITY_UNKNOWN)
 606     {
 607       return status;
 608     }
 609   }
 610   return EQUALITY_UNKNOWN;
 611   ;
 612 }
 613
 614 void BVSolverLayered::ppStaticLearn(TNode in, NodeBuilder& learned)
 615 {
 616   if (d_staticLearnCache.find(in) != d_staticLearnCache.end())
 617   {
 618     return;
 619   }
 620   d_staticLearnCache.insert(in);
 621
 622   if (in.getKind() == kind::EQUAL)
 623   {
 624     if ((in[0].getKind() == kind::BITVECTOR_ADD
 625          && in[1].getKind() == kind::BITVECTOR_SHL)
 626         || (in[1].getKind() == kind::BITVECTOR_ADD
 627             && in[0].getKind() == kind::BITVECTOR_SHL))
 628     {
 629       TNode p = in[0].getKind() == kind::BITVECTOR_ADD ? in[0] : in[1];
 630       TNode s = in[0].getKind() == kind::BITVECTOR_ADD ? in[1] : in[0];
 631
 632       if (p.getNumChildren() == 2 && p[0].getKind() == kind::BITVECTOR_SHL
 633           && p[1].getKind() == kind::BITVECTOR_SHL)
 634       {
 635         unsigned size = utils::getSize(s);
 636         Node one = utils::mkConst(size, 1u);
 637         if (s[0] == one && p[0][0] == one && p[1][0] == one)
 638         {
 639           Node zero = utils::mkConst(size, 0u);
 640           TNode b = p[0];
 641           TNode c = p[1];
 642           // (s : 1 << S) = (b : 1 << B) + (c : 1 << C)
 643           Node b_eq_0 = b.eqNode(zero);
 644           Node c_eq_0 = c.eqNode(zero);
 645           Node b_eq_c = b.eqNode(c);
 646
 647           Node dis = NodeManager::currentNM()->mkNode(
 648               kind::OR, b_eq_0, c_eq_0, b_eq_c);
 649           Node imp = in.impNode(dis);
 650           learned << imp;
 651         }
 652       }
 653     }
 654   }
 655   else if (in.getKind() == kind::AND)
 656   {
 657     for (size_t i = 0, N = in.getNumChildren(); i < N; ++i)
 658     {
 659       ppStaticLearn(in[i], learned);
 660     }
 661   }
 662 }
 663
 664 bool BVSolverLayered::applyAbstraction(const std::vector<Node>& assertions,
 665                                        std::vector<Node>& new_assertions)
 666 {
 667   bool changed =
 668       d_abstractionModule->applyAbstraction(assertions, new_assertions);
 669   if (changed && options().bv.bitblastMode == options::BitblastMode::EAGER
 670       && options().bv.bitvectorAig)
 671   {
 672     // disable AIG mode
 673     AlwaysAssert(!d_eagerSolver->isInitialized());
 674     d_eagerSolver->turnOffAig();
 675     d_eagerSolver->initialize();
 676   }
 677   return changed;
 678 }
 679
 680 void BVSolverLayered::setConflict(Node conflict)
 681 {
 682   if (options().bv.bvAbstraction)
 683   {
 684     NodeManager* const nm = NodeManager::currentNM();
 685     Node new_conflict = d_abstractionModule->simplifyConflict(conflict);
 686
 687     std::vector<Node> lemmas;
 688     lemmas.push_back(new_conflict);
 689     d_abstractionModule->generalizeConflict(new_conflict, lemmas);
 690     for (unsigned i = 0; i < lemmas.size(); ++i)
 691     {
 692       lemma(nm->mkNode(kind::NOT, lemmas[i]));
 693     }
 694   }
 695   d_conflict = true;
 696   d_conflictNode = conflict;
 697 }
 698
 699 }  // namespace bv
 700 }  // namespace theory
 701 }  // namespace cvc5