src/theory/bv/theory_bv.cpp

   1 /*********************                                                        */
   2 /*! \file theory_bv.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Liana Hadarean, Andrew Reynolds, Aina Niemetz
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2019 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  ** [[ Add lengthier description here ]]
  13  ** \todo document this file
  14  **/
  15
  16 #include "theory/bv/theory_bv.h"
  17
  18 #include "expr/node_algorithm.h"
  19 #include "options/bv_options.h"
  20 #include "options/smt_options.h"
  21 #include "proof/proof_manager.h"
  22 #include "proof/theory_proof.h"
  23 #include "smt/smt_statistics_registry.h"
  24 #include "theory/bv/abstraction.h"
  25 #include "theory/bv/bv_eager_solver.h"
  26 #include "theory/bv/bv_subtheory_algebraic.h"
  27 #include "theory/bv/bv_subtheory_bitblast.h"
  28 #include "theory/bv/bv_subtheory_core.h"
  29 #include "theory/bv/bv_subtheory_inequality.h"
  30 #include "theory/bv/slicer.h"
  31 #include "theory/bv/theory_bv_rewrite_rules_normalization.h"
  32 #include "theory/bv/theory_bv_rewrite_rules_simplification.h"
  33 #include "theory/bv/theory_bv_rewriter.h"
  34 #include "theory/bv/theory_bv_utils.h"
  35 #include "theory/ext_theory.h"
  36 #include "theory/theory_model.h"
  37 #include "theory/valuation.h"
  38
  39 using namespace CVC4::context;
  40 using namespace CVC4::theory::bv::utils;
  41 using namespace std;
  42
  43 namespace CVC4 {
  44 namespace theory {
  45 namespace bv {
  46
  47 TheoryBV::TheoryBV(context::Context* c,
  48                    context::UserContext* u,
  49                    OutputChannel& out,
  50                    Valuation valuation,
  51                    const LogicInfo& logicInfo,
  52                    std::string name)
  53     : Theory(THEORY_BV, c, u, out, valuation, logicInfo, name),
  54       d_context(c),
  55       d_alreadyPropagatedSet(c),
  56       d_sharedTermsSet(c),
  57       d_subtheories(),
  58       d_subtheoryMap(),
  59       d_statistics(),
  60       d_staticLearnCache(),
  61       d_BVDivByZero(),
  62       d_BVRemByZero(),
  63       d_lemmasAdded(c, false),
  64       d_conflict(c, false),
  65       d_invalidateModelCache(c, true),
  66       d_literalsToPropagate(c),
  67       d_literalsToPropagateIndex(c, 0),
  68       d_propagatedBy(c),
  69       d_eagerSolver(),
  70       d_abstractionModule(new AbstractionModule(getStatsPrefix(THEORY_BV))),
  71       d_isCoreTheory(false),
  72       d_calledPreregister(false),
  73       d_needsLastCallCheck(false),
  74       d_extf_range_infer(u),
  75       d_extf_collapse_infer(u)
  76 {
  77   setupExtTheory();
  78   getExtTheory()->addFunctionKind(kind::BITVECTOR_TO_NAT);
  79   getExtTheory()->addFunctionKind(kind::INT_TO_BITVECTOR);
  80   if (options::bitblastMode() == options::BitblastMode::EAGER)
  81   {
  82     d_eagerSolver.reset(new EagerBitblastSolver(c, this));
  83     return;
  84   }
  85
  86   if (options::bitvectorEqualitySolver() && !options::proof())
  87   {
  88     d_subtheories.emplace_back(new CoreSolver(c, this));
  89     d_subtheoryMap[SUB_CORE] = d_subtheories.back().get();
  90   }
  91
  92   if (options::bitvectorInequalitySolver() && !options::proof())
  93   {
  94     d_subtheories.emplace_back(new InequalitySolver(c, u, this));
  95     d_subtheoryMap[SUB_INEQUALITY] = d_subtheories.back().get();
  96   }
  97
  98   if (options::bitvectorAlgebraicSolver() && !options::proof())
  99   {
 100     d_subtheories.emplace_back(new AlgebraicSolver(c, this));
 101     d_subtheoryMap[SUB_ALGEBRAIC] = d_subtheories.back().get();
 102   }
 103
 104   BitblastSolver* bb_solver = new BitblastSolver(c, this);
 105   if (options::bvAbstraction())
 106   {
 107     bb_solver->setAbstraction(d_abstractionModule.get());
 108   }
 109   d_subtheories.emplace_back(bb_solver);
 110   d_subtheoryMap[SUB_BITBLAST] = bb_solver;
 111 }
 112
 113 TheoryBV::~TheoryBV() {}
 114
 115 void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) {
 116   if (options::bitblastMode() == options::BitblastMode::EAGER)
 117   {
 118     return;
 119   }
 120   if (options::bitvectorEqualitySolver()) {
 121     dynamic_cast<CoreSolver*>(d_subtheoryMap[SUB_CORE])->setMasterEqualityEngine(eq);
 122   }
 123 }
 124
 125 void TheoryBV::spendResource(ResourceManager::Resource r)
 126 {
 127   getOutputChannel().spendResource(r);
 128 }
 129
 130 TheoryBV::Statistics::Statistics():
 131   d_avgConflictSize("theory::bv::AvgBVConflictSize"),
 132   d_solveSubstitutions("theory::bv::NumSolveSubstitutions", 0),
 133   d_solveTimer("theory::bv::solveTimer"),
 134   d_numCallsToCheckFullEffort("theory::bv::NumFullCheckCalls", 0),
 135   d_numCallsToCheckStandardEffort("theory::bv::NumStandardCheckCalls", 0),
 136   d_weightComputationTimer("theory::bv::weightComputationTimer"),
 137   d_numMultSlice("theory::bv::NumMultSliceApplied", 0)
 138 {
 139   smtStatisticsRegistry()->registerStat(&d_avgConflictSize);
 140   smtStatisticsRegistry()->registerStat(&d_solveSubstitutions);
 141   smtStatisticsRegistry()->registerStat(&d_solveTimer);
 142   smtStatisticsRegistry()->registerStat(&d_numCallsToCheckFullEffort);
 143   smtStatisticsRegistry()->registerStat(&d_numCallsToCheckStandardEffort);
 144   smtStatisticsRegistry()->registerStat(&d_weightComputationTimer);
 145   smtStatisticsRegistry()->registerStat(&d_numMultSlice);
 146 }
 147
 148 TheoryBV::Statistics::~Statistics() {
 149   smtStatisticsRegistry()->unregisterStat(&d_avgConflictSize);
 150   smtStatisticsRegistry()->unregisterStat(&d_solveSubstitutions);
 151   smtStatisticsRegistry()->unregisterStat(&d_solveTimer);
 152   smtStatisticsRegistry()->unregisterStat(&d_numCallsToCheckFullEffort);
 153   smtStatisticsRegistry()->unregisterStat(&d_numCallsToCheckStandardEffort);
 154   smtStatisticsRegistry()->unregisterStat(&d_weightComputationTimer);
 155   smtStatisticsRegistry()->unregisterStat(&d_numMultSlice);
 156 }
 157
 158 Node TheoryBV::getBVDivByZero(Kind k, unsigned width) {
 159   NodeManager* nm = NodeManager::currentNM();
 160   if (k == kind::BITVECTOR_UDIV) {
 161     if (d_BVDivByZero.find(width) == d_BVDivByZero.end()) {
 162       // lazily create the function symbols
 163       ostringstream os;
 164       os << "BVUDivByZero_" << width;
 165       Node divByZero = nm->mkSkolem(os.str(),
 166                                     nm->mkFunctionType(nm->mkBitVectorType(width), nm->mkBitVectorType(width)),
 167                                     "partial bvudiv", NodeManager::SKOLEM_EXACT_NAME);
 168       d_BVDivByZero[width] = divByZero;
 169     }
 170     return d_BVDivByZero[width];
 171   }
 172   else if (k == kind::BITVECTOR_UREM) {
 173     if (d_BVRemByZero.find(width) == d_BVRemByZero.end()) {
 174       ostringstream os;
 175       os << "BVURemByZero_" << width;
 176       Node divByZero = nm->mkSkolem(os.str(),
 177                                     nm->mkFunctionType(nm->mkBitVectorType(width), nm->mkBitVectorType(width)),
 178                                     "partial bvurem", NodeManager::SKOLEM_EXACT_NAME);
 179       d_BVRemByZero[width] = divByZero;
 180     }
 181     return d_BVRemByZero[width];
 182   }
 183
 184   Unreachable();
 185 }
 186
 187 void TheoryBV::finishInit()
 188 {
 189   // these kinds are semi-evaluated in getModelValue (applications of this
 190   // kind are treated as variables)
 191   TheoryModel* tm = d_valuation.getModel();
 192   Assert(tm != nullptr);
 193   tm->setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UDIV);
 194   tm->setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UREM);
 195 }
 196
 197 Node TheoryBV::expandDefinition(Node node)
 198 {
 199   Debug("bitvector-expandDefinition") << "TheoryBV::expandDefinition(" << node << ")" << std::endl;
 200
 201   switch (node.getKind()) {
 202   case kind::BITVECTOR_SDIV:
 203   case kind::BITVECTOR_SREM:
 204   case kind::BITVECTOR_SMOD:
 205     return TheoryBVRewriter::eliminateBVSDiv(node);
 206     break;
 207
 208   case kind::BITVECTOR_UDIV:
 209   case kind::BITVECTOR_UREM: {
 210     NodeManager* nm = NodeManager::currentNM();
 211     unsigned width = node.getType().getBitVectorSize();
 212
 213     if (options::bitvectorDivByZeroConst()) {
 214       Kind kind = node.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_UDIV_TOTAL : kind::BITVECTOR_UREM_TOTAL;
 215       return nm->mkNode(kind, node[0], node[1]);
 216     }
 217
 218     TNode num = node[0], den = node[1];
 219     Node den_eq_0 = nm->mkNode(kind::EQUAL, den, utils::mkZero(width));
 220     Node divTotalNumDen = nm->mkNode(node.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_UDIV_TOTAL :
 221                                      kind::BITVECTOR_UREM_TOTAL, num, den);
 222     Node divByZero = getBVDivByZero(node.getKind(), width);
 223     Node divByZeroNum = nm->mkNode(kind::APPLY_UF, divByZero, num);
 224     node = nm->mkNode(kind::ITE, den_eq_0, divByZeroNum, divTotalNumDen);
 225     return node;
 226   }
 227     break;
 228
 229   default:
 230     return node;
 231     break;
 232   }
 233
 234   Unreachable();
 235 }
 236
 237 void TheoryBV::preRegisterTerm(TNode node) {
 238   d_calledPreregister = true;
 239   Debug("bitvector-preregister") << "TheoryBV::preRegister(" << node << ")" << std::endl;
 240
 241   if (options::bitblastMode() == options::BitblastMode::EAGER)
 242   {
 243     // the aig bit-blaster option is set heuristically
 244     // if bv abstraction is used
 245     if (!d_eagerSolver->isInitialized())
 246     {
 247       d_eagerSolver->initialize();
 248     }
 249
 250     if (node.getKind() == kind::BITVECTOR_EAGER_ATOM)
 251     {
 252       Node formula = node[0];
 253       d_eagerSolver->assertFormula(formula);
 254     }
 255     return;
 256   }
 257
 258   for (unsigned i = 0; i < d_subtheories.size(); ++i) {
 259     d_subtheories[i]->preRegister(node);
 260   }
 261
 262   // AJR : equality solver currently registers all terms to ExtTheory, if we want a lazy reduction without the bv equality solver, need to call this
 263   //getExtTheory()->registerTermRec( node );
 264 }
 265
 266 void TheoryBV::sendConflict() {
 267   Assert(d_conflict);
 268   if (d_conflictNode.isNull()) {
 269     return;
 270   } else {
 271     Debug("bitvector") << indent() << "TheoryBV::check(): conflict " << d_conflictNode << std::endl;
 272     d_out->conflict(d_conflictNode);
 273     d_statistics.d_avgConflictSize.addEntry(d_conflictNode.getNumChildren());
 274     d_conflictNode = Node::null();
 275   }
 276 }
 277
 278 void TheoryBV::checkForLemma(TNode fact)
 279 {
 280   if (fact.getKind() == kind::EQUAL)
 281   {
 282     NodeManager* nm = NodeManager::currentNM();
 283     if (fact[0].getKind() == kind::BITVECTOR_UREM_TOTAL)
 284     {
 285       TNode urem = fact[0];
 286       TNode result = fact[1];
 287       TNode divisor = urem[1];
 288       Node result_ult_div = nm->mkNode(kind::BITVECTOR_ULT, result, divisor);
 289       Node divisor_eq_0 =
 290           nm->mkNode(kind::EQUAL, divisor, mkZero(getSize(divisor)));
 291       Node split = nm->mkNode(
 292           kind::OR, divisor_eq_0, nm->mkNode(kind::NOT, fact), result_ult_div);
 293       lemma(split);
 294     }
 295     if (fact[1].getKind() == kind::BITVECTOR_UREM_TOTAL)
 296     {
 297       TNode urem = fact[1];
 298       TNode result = fact[0];
 299       TNode divisor = urem[1];
 300       Node result_ult_div = nm->mkNode(kind::BITVECTOR_ULT, result, divisor);
 301       Node divisor_eq_0 =
 302           nm->mkNode(kind::EQUAL, divisor, mkZero(getSize(divisor)));
 303       Node split = nm->mkNode(
 304           kind::OR, divisor_eq_0, nm->mkNode(kind::NOT, fact), result_ult_div);
 305       lemma(split);
 306     }
 307   }
 308 }
 309
 310 void TheoryBV::check(Effort e)
 311 {
 312   if (done() && e<Theory::EFFORT_FULL) {
 313     return;
 314   }
 315
 316   //last call : do reductions on extended bitvector functions
 317   if (e == Theory::EFFORT_LAST_CALL) {
 318     std::vector<Node> nred = getExtTheory()->getActive();
 319     doExtfReductions(nred);
 320     return;
 321   }
 322
 323   TimerStat::CodeTimer checkTimer(d_checkTime);
 324   Debug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl;
 325   TimerStat::CodeTimer codeTimer(d_statistics.d_solveTimer);
 326   // we may be getting new assertions so the model cache may not be sound
 327   d_invalidateModelCache.set(true);
 328   // if we are using the eager solver
 329   if (options::bitblastMode() == options::BitblastMode::EAGER)
 330   {
 331     // this can only happen on an empty benchmark
 332     if (!d_eagerSolver->isInitialized()) {
 333       d_eagerSolver->initialize();
 334     }
 335     if (!Theory::fullEffort(e))
 336       return;
 337
 338     std::vector<TNode> assertions;
 339     while (!done()) {
 340       TNode fact = get().d_assertion;
 341       Assert(fact.getKind() == kind::BITVECTOR_EAGER_ATOM);
 342       assertions.push_back(fact);
 343       d_eagerSolver->assertFormula(fact[0]);
 344     }
 345
 346     bool ok = d_eagerSolver->checkSat();
 347     if (!ok) {
 348       if (assertions.size() == 1) {
 349         d_out->conflict(assertions[0]);
 350         return;
 351       }
 352       Node conflict = utils::mkAnd(assertions);
 353       d_out->conflict(conflict);
 354       return;
 355     }
 356     return;
 357   }
 358
 359   if (Theory::fullEffort(e)) {
 360     ++(d_statistics.d_numCallsToCheckFullEffort);
 361   } else {
 362     ++(d_statistics.d_numCallsToCheckStandardEffort);
 363   }
 364   // if we are already in conflict just return the conflict
 365   if (inConflict()) {
 366     sendConflict();
 367     return;
 368   }
 369
 370   while (!done()) {
 371     TNode fact = get().d_assertion;
 372
 373     checkForLemma(fact);
 374
 375     for (unsigned i = 0; i < d_subtheories.size(); ++i) {
 376       d_subtheories[i]->assertFact(fact);
 377     }
 378   }
 379
 380   bool ok = true;
 381   bool complete = false;
 382   for (unsigned i = 0; i < d_subtheories.size(); ++i) {
 383     Assert(!inConflict());
 384     ok = d_subtheories[i]->check(e);
 385     complete = d_subtheories[i]->isComplete();
 386
 387     if (!ok) {
 388       // if we are in a conflict no need to check with other theories
 389       Assert(inConflict());
 390       sendConflict();
 391       return;
 392     }
 393     if (complete) {
 394       // if the last subtheory was complete we stop
 395       break;
 396     }
 397   }
 398
 399   //check extended functions
 400   if (Theory::fullEffort(e)) {
 401     //do inferences (adds external lemmas)  TODO: this can be improved to add internal inferences
 402     std::vector< Node > nred;
 403     if( getExtTheory()->doInferences( 0, nred ) ){
 404       return;
 405     }
 406     d_needsLastCallCheck = false;
 407     if( !nred.empty() ){
 408       //other inferences involving bv2nat, int2bv
 409       if( options::bvAlgExtf() ){
 410         if( doExtfInferences( nred ) ){
 411           return;
 412         }
 413       }
 414       if( !options::bvLazyReduceExtf() ){
 415         if( doExtfReductions( nred ) ){
 416           return;
 417         }
 418       }else{
 419         d_needsLastCallCheck = true;
 420       }
 421     }
 422   }
 423 }
 424
 425 bool TheoryBV::doExtfInferences(std::vector<Node>& terms)
 426 {
 427   NodeManager* nm = NodeManager::currentNM();
 428   bool sentLemma = false;
 429   eq::EqualityEngine* ee = getEqualityEngine();
 430   std::map<Node, Node> op_map;
 431   for (unsigned j = 0; j < terms.size(); j++)
 432   {
 433     TNode n = terms[j];
 434     Assert(n.getKind() == kind::BITVECTOR_TO_NAT
 435            || n.getKind() == kind::INT_TO_BITVECTOR);
 436     if (n.getKind() == kind::BITVECTOR_TO_NAT)
 437     {
 438       // range lemmas
 439       if (d_extf_range_infer.find(n) == d_extf_range_infer.end())
 440       {
 441         d_extf_range_infer.insert(n);
 442         unsigned bvs = n[0].getType().getBitVectorSize();
 443         Node min = nm->mkConst(Rational(0));
 444         Node max = nm->mkConst(Rational(Integer(1).multiplyByPow2(bvs)));
 445         Node lem = nm->mkNode(kind::AND,
 446                               nm->mkNode(kind::GEQ, n, min),
 447                               nm->mkNode(kind::LT, n, max));
 448         Trace("bv-extf-lemma")
 449             << "BV extf lemma (range) : " << lem << std::endl;
 450         d_out->lemma(lem);
 451         sentLemma = true;
 452       }
 453     }
 454     Node r = (ee && ee->hasTerm(n[0])) ? ee->getRepresentative(n[0]) : n[0];
 455     op_map[r] = n;
 456   }
 457   for (unsigned j = 0; j < terms.size(); j++)
 458   {
 459     TNode n = terms[j];
 460     Node r = (ee && ee->hasTerm(n[0])) ? ee->getRepresentative(n) : n;
 461     std::map<Node, Node>::iterator it = op_map.find(r);
 462     if (it != op_map.end())
 463     {
 464       Node parent = it->second;
 465       // Node cterm = parent[0]==n ? parent : nm->mkNode( parent.getOperator(),
 466       // n );
 467       Node cterm = parent[0].eqNode(n);
 468       Trace("bv-extf-lemma-debug")
 469           << "BV extf collapse based on : " << cterm << std::endl;
 470       if (d_extf_collapse_infer.find(cterm) == d_extf_collapse_infer.end())
 471       {
 472         d_extf_collapse_infer.insert(cterm);
 473
 474         Node t = n[0];
 475         if (t.getType() == parent.getType())
 476         {
 477           if (n.getKind() == kind::INT_TO_BITVECTOR)
 478           {
 479             Assert(t.getType().isInteger());
 480             // congruent modulo 2^( bv width )
 481             unsigned bvs = n.getType().getBitVectorSize();
 482             Node coeff = nm->mkConst(Rational(Integer(1).multiplyByPow2(bvs)));
 483             Node k = nm->mkSkolem(
 484                 "int_bv_cong", t.getType(), "for int2bv/bv2nat congruence");
 485             t = nm->mkNode(kind::PLUS, t, nm->mkNode(kind::MULT, coeff, k));
 486           }
 487           Node lem = parent.eqNode(t);
 488
 489           if (parent[0] != n)
 490           {
 491             Assert(ee->areEqual(parent[0], n));
 492             lem = nm->mkNode(kind::IMPLIES, parent[0].eqNode(n), lem);
 493           }
 494           // this handles inferences of the form, e.g.:
 495           //   ((_ int2bv w) (bv2nat x)) == x (if x is bit-width w)
 496           //   (bv2nat ((_ int2bv w) x)) == x + k*2^w for some k
 497           Trace("bv-extf-lemma")
 498               << "BV extf lemma (collapse) : " << lem << std::endl;
 499           d_out->lemma(lem);
 500           sentLemma = true;
 501         }
 502       }
 503       Trace("bv-extf-lemma-debug")
 504           << "BV extf f collapse based on : " << cterm << std::endl;
 505     }
 506   }
 507   return sentLemma;
 508 }
 509
 510 bool TheoryBV::doExtfReductions( std::vector< Node >& terms ) {
 511   std::vector< Node > nredr;
 512   if( getExtTheory()->doReductions( 0, terms, nredr ) ){
 513     return true;
 514   }
 515   Assert(nredr.empty());
 516   return false;
 517 }
 518
 519 bool TheoryBV::needsCheckLastEffort() {
 520   return d_needsLastCallCheck;
 521 }
 522 bool TheoryBV::collectModelInfo(TheoryModel* m)
 523 {
 524   Assert(!inConflict());
 525   if (options::bitblastMode() == options::BitblastMode::EAGER)
 526   {
 527     if (!d_eagerSolver->collectModelInfo(m, true))
 528     {
 529       return false;
 530     }
 531   }
 532   for (unsigned i = 0; i < d_subtheories.size(); ++i) {
 533     if (d_subtheories[i]->isComplete()) {
 534       return d_subtheories[i]->collectModelInfo(m, true);
 535     }
 536   }
 537   return true;
 538 }
 539
 540 Node TheoryBV::getModelValue(TNode var) {
 541   Assert(!inConflict());
 542   for (unsigned i = 0; i < d_subtheories.size(); ++i) {
 543     if (d_subtheories[i]->isComplete()) {
 544       return d_subtheories[i]->getModelValue(var);
 545     }
 546   }
 547   Unreachable();
 548 }
 549
 550 void TheoryBV::propagate(Effort e) {
 551   Debug("bitvector") << indent() << "TheoryBV::propagate()" << std::endl;
 552   if (options::bitblastMode() == options::BitblastMode::EAGER)
 553   {
 554     return;
 555   }
 556
 557   if (inConflict()) {
 558     return;
 559   }
 560
 561   // go through stored propagations
 562   bool ok = true;
 563   for (; d_literalsToPropagateIndex < d_literalsToPropagate.size() && ok; d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) {
 564     TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex];
 565     // temporary fix for incremental bit-blasting
 566     if (d_valuation.isSatLiteral(literal)) {
 567       Debug("bitvector::propagate") << "TheoryBV:: propagating " << literal <<"\n";
 568       ok = d_out->propagate(literal);
 569     }
 570   }
 571
 572   if (!ok) {
 573     Debug("bitvector::propagate") << indent() << "TheoryBV::propagate(): conflict from theory engine" << std::endl;
 574     setConflict();
 575   }
 576 }
 577
 578
 579 eq::EqualityEngine * TheoryBV::getEqualityEngine() {
 580   CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
 581   if( core ){
 582     return core->getEqualityEngine();
 583   }else{
 584     return NULL;
 585   }
 586 }
 587
 588 bool TheoryBV::getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp ) {
 589   eq::EqualityEngine * ee = getEqualityEngine();
 590   if( ee ){
 591     //get the constant equivalence classes
 592     bool retVal = false;
 593     for( unsigned i=0; i<vars.size(); i++ ){
 594       Node n = vars[i];
 595       if( ee->hasTerm( n ) ){
 596         Node nr = ee->getRepresentative( n );
 597         if( nr.isConst() ){
 598           subs.push_back( nr );
 599           exp[n].push_back( n.eqNode( nr ) );
 600           retVal = true;
 601         }else{
 602           subs.push_back( n );
 603         }
 604       }else{
 605         subs.push_back( n );
 606       }
 607     }
 608     //return true if the substitution is non-trivial
 609     return retVal;
 610   }
 611   return false;
 612 }
 613
 614 int TheoryBV::getReduction(int effort, Node n, Node& nr)
 615 {
 616   Trace("bv-ext") << "TheoryBV::checkExt : non-reduced : " << n << std::endl;
 617   if (n.getKind() == kind::BITVECTOR_TO_NAT)
 618   {
 619     nr = utils::eliminateBv2Nat(n);
 620     return -1;
 621   }
 622   else if (n.getKind() == kind::INT_TO_BITVECTOR)
 623   {
 624     nr = utils::eliminateInt2Bv(n);
 625     return -1;
 626   }
 627   return 0;
 628 }
 629
 630 Theory::PPAssertStatus TheoryBV::ppAssert(TNode in,
 631                                           SubstitutionMap& outSubstitutions)
 632 {
 633   switch (in.getKind())
 634   {
 635     case kind::EQUAL:
 636     {
 637       if (in[0].isVar() && isLegalElimination(in[0], in[1]))
 638       {
 639         ++(d_statistics.d_solveSubstitutions);
 640         outSubstitutions.addSubstitution(in[0], in[1]);
 641         return PP_ASSERT_STATUS_SOLVED;
 642       }
 643       if (in[1].isVar() && isLegalElimination(in[1], in[0]))
 644       {
 645         ++(d_statistics.d_solveSubstitutions);
 646         outSubstitutions.addSubstitution(in[1], in[0]);
 647         return PP_ASSERT_STATUS_SOLVED;
 648       }
 649       Node node = Rewriter::rewrite(in);
 650       if ((node[0].getKind() == kind::BITVECTOR_EXTRACT && node[1].isConst())
 651           || (node[1].getKind() == kind::BITVECTOR_EXTRACT
 652               && node[0].isConst()))
 653       {
 654         Node extract = node[0].isConst() ? node[1] : node[0];
 655         if (extract[0].isVar())
 656         {
 657           Node c = node[0].isConst() ? node[0] : node[1];
 658
 659           unsigned high = utils::getExtractHigh(extract);
 660           unsigned low = utils::getExtractLow(extract);
 661           unsigned var_bitwidth = utils::getSize(extract[0]);
 662           std::vector<Node> children;
 663
 664           if (low == 0)
 665           {
 666             Assert(high != var_bitwidth - 1);
 667             unsigned skolem_size = var_bitwidth - high - 1;
 668             Node skolem = utils::mkVar(skolem_size);
 669             children.push_back(skolem);
 670             children.push_back(c);
 671           }
 672           else if (high == var_bitwidth - 1)
 673           {
 674             unsigned skolem_size = low;
 675             Node skolem = utils::mkVar(skolem_size);
 676             children.push_back(c);
 677             children.push_back(skolem);
 678           }
 679           else
 680           {
 681             unsigned skolem1_size = low;
 682             unsigned skolem2_size = var_bitwidth - high - 1;
 683             Node skolem1 = utils::mkVar(skolem1_size);
 684             Node skolem2 = utils::mkVar(skolem2_size);
 685             children.push_back(skolem2);
 686             children.push_back(c);
 687             children.push_back(skolem1);
 688           }
 689           Node concat = utils::mkConcat(children);
 690           Assert(utils::getSize(concat) == utils::getSize(extract[0]));
 691           if (isLegalElimination(extract[0], concat))
 692           {
 693             outSubstitutions.addSubstitution(extract[0], concat);
 694             return PP_ASSERT_STATUS_SOLVED;
 695           }
 696         }
 697       }
 698     }
 699     break;
 700     case kind::BITVECTOR_ULT:
 701     case kind::BITVECTOR_SLT:
 702     case kind::BITVECTOR_ULE:
 703     case kind::BITVECTOR_SLE:
 704
 705     default:
 706       // TODO other predicates
 707       break;
 708   }
 709   return PP_ASSERT_STATUS_UNSOLVED;
 710 }
 711
 712 Node TheoryBV::ppRewrite(TNode t)
 713 {
 714   Debug("bv-pp-rewrite") << "TheoryBV::ppRewrite " << t << "\n";
 715   Node res = t;
 716   if (options::bitwiseEq() && RewriteRule<BitwiseEq>::applies(t)) {
 717     Node result = RewriteRule<BitwiseEq>::run<false>(t);
 718     res = Rewriter::rewrite(result);
 719   } else if (d_isCoreTheory && t.getKind() == kind::EQUAL) {
 720     std::vector<Node> equalities;
 721     Slicer::splitEqualities(t, equalities);
 722     res = utils::mkAnd(equalities);
 723   } else if (RewriteRule<UltPlusOne>::applies(t)) {
 724     Node result = RewriteRule<UltPlusOne>::run<false>(t);
 725     res = Rewriter::rewrite(result);
 726   } else if( res.getKind() == kind::EQUAL &&
 727       ((res[0].getKind() == kind::BITVECTOR_PLUS &&
 728         RewriteRule<ConcatToMult>::applies(res[1])) ||
 729        (res[1].getKind() == kind::BITVECTOR_PLUS &&
 730         RewriteRule<ConcatToMult>::applies(res[0])))) {
 731     Node mult = RewriteRule<ConcatToMult>::applies(res[0])?
 732       RewriteRule<ConcatToMult>::run<false>(res[0]) :
 733       RewriteRule<ConcatToMult>::run<true>(res[1]);
 734     Node factor = mult[0];
 735     Node sum =  RewriteRule<ConcatToMult>::applies(res[0])? res[1] : res[0];
 736     Node new_eq = NodeManager::currentNM()->mkNode(kind::EQUAL, sum, mult);
 737     Node rewr_eq = RewriteRule<SolveEq>::run<true>(new_eq);
 738     if (rewr_eq[0].isVar() || rewr_eq[1].isVar()){
 739       res = Rewriter::rewrite(rewr_eq);
 740     } else {
 741       res = t;
 742     }
 743   } else if (RewriteRule<SignExtendEqConst>::applies(t)) {
 744     res = RewriteRule<SignExtendEqConst>::run<false>(t);
 745   } else if (RewriteRule<ZeroExtendEqConst>::applies(t)) {
 746     res = RewriteRule<ZeroExtendEqConst>::run<false>(t);
 747   }
 748   else if (RewriteRule<NormalizeEqPlusNeg>::applies(t))
 749   {
 750     res = RewriteRule<NormalizeEqPlusNeg>::run<false>(t);
 751   }
 752
 753   // if(t.getKind() == kind::EQUAL &&
 754   //    ((t[0].getKind() == kind::BITVECTOR_MULT && t[1].getKind() ==
 755   //    kind::BITVECTOR_PLUS) ||
 756   //     (t[1].getKind() == kind::BITVECTOR_MULT && t[0].getKind() ==
 757   //     kind::BITVECTOR_PLUS))) {
 758   //   // if we have an equality between a multiplication and addition
 759   //   // try to express multiplication in terms of addition
 760   //   Node mult = t[0].getKind() == kind::BITVECTOR_MULT? t[0] : t[1];
 761   //   Node add = t[0].getKind() == kind::BITVECTOR_PLUS? t[0] : t[1];
 762   //   if (RewriteRule<MultSlice>::applies(mult)) {
 763   //     Node new_mult = RewriteRule<MultSlice>::run<false>(mult);
 764   //     Node new_eq =
 765   //     Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::EQUAL,
 766   //     new_mult, add));
 767
 768   //     // the simplification can cause the formula to blow up
 769   //     // only apply if formula reduced
 770   //     if (d_subtheoryMap.find(SUB_BITBLAST) != d_subtheoryMap.end()) {
 771   //       BitblastSolver* bv = (BitblastSolver*)d_subtheoryMap[SUB_BITBLAST];
 772   //       uint64_t old_size = bv->computeAtomWeight(t);
 773   //       Assert (old_size);
 774   //       uint64_t new_size = bv->computeAtomWeight(new_eq);
 775   //       double ratio = ((double)new_size)/old_size;
 776   //       if (ratio <= 0.4) {
 777   //         ++(d_statistics.d_numMultSlice);
 778   //         return new_eq;
 779   //       }
 780   //     }
 781
 782   //     if (new_eq.getKind() == kind::CONST_BOOLEAN) {
 783   //       ++(d_statistics.d_numMultSlice);
 784   //       return new_eq;
 785   //     }
 786   //   }
 787   // }
 788
 789   if (options::bvAbstraction() && t.getType().isBoolean()) {
 790     d_abstractionModule->addInputAtom(res);
 791   }
 792   Debug("bv-pp-rewrite") << "to   " << res << "\n";
 793   return res;
 794 }
 795
 796 void TheoryBV::presolve() {
 797   Debug("bitvector") << "TheoryBV::presolve" << endl;
 798 }
 799
 800 static int prop_count = 0;
 801
 802 bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory)
 803 {
 804   Debug("bitvector::propagate") << indent() << getSatContext()->getLevel() << " " << "TheoryBV::storePropagation(" << literal << ", " << subtheory << ")" << std::endl;
 805   prop_count++;
 806
 807   // If already in conflict, no more propagation
 808   if (d_conflict) {
 809     Debug("bitvector::propagate") << indent() << "TheoryBV::storePropagation(" << literal << ", " << subtheory << "): already in conflict" << std::endl;
 810     return false;
 811   }
 812
 813   // If propagated already, just skip
 814   PropagatedMap::const_iterator find = d_propagatedBy.find(literal);
 815   if (find != d_propagatedBy.end()) {
 816     return true;
 817   } else {
 818     bool polarity = literal.getKind() != kind::NOT;
 819     Node negatedLiteral = polarity ? literal.notNode() : (Node) literal[0];
 820     find = d_propagatedBy.find(negatedLiteral);
 821     if (find != d_propagatedBy.end() && (*find).second != subtheory) {
 822       // Safe to ignore this one, subtheory should produce a conflict
 823       return true;
 824     }
 825
 826     d_propagatedBy[literal] = subtheory;
 827   }
 828
 829   // Propagate differs depending on the subtheory
 830   // * bitblaster needs to be left alone until it's done, otherwise it doesn't
 831   //   know how to explain
 832   // * equality engine can propagate eagerly
 833   // TODO(2348): Determine if ok should be set by propagate. If not, remove ok.
 834   constexpr bool ok = true;
 835   if (subtheory == SUB_CORE) {
 836     d_out->propagate(literal);
 837     if (!ok) {
 838       setConflict();
 839     }
 840   } else {
 841     d_literalsToPropagate.push_back(literal);
 842   }
 843   return ok;
 844
 845 }/* TheoryBV::propagate(TNode) */
 846
 847
 848 void TheoryBV::explain(TNode literal, std::vector<TNode>& assumptions) {
 849   Assert(wasPropagatedBySubtheory(literal));
 850   SubTheory sub = getPropagatingSubtheory(literal);
 851   d_subtheoryMap[sub]->explain(literal, assumptions);
 852 }
 853
 854
 855 Node TheoryBV::explain(TNode node) {
 856   Debug("bitvector::explain") << "TheoryBV::explain(" << node << ")" << std::endl;
 857   std::vector<TNode> assumptions;
 858
 859   // Ask for the explanation
 860   explain(node, assumptions);
 861   // this means that it is something true at level 0
 862   if (assumptions.size() == 0) {
 863     return utils::mkTrue();
 864   }
 865   // return the explanation
 866   Node explanation = utils::mkAnd(assumptions);
 867   Debug("bitvector::explain") << "TheoryBV::explain(" << node << ") => " << explanation << std::endl;
 868   Debug("bitvector::explain") << "TheoryBV::explain done. \n";
 869   return explanation;
 870 }
 871
 872
 873 void TheoryBV::addSharedTerm(TNode t) {
 874   Debug("bitvector::sharing") << indent() << "TheoryBV::addSharedTerm(" << t << ")" << std::endl;
 875   d_sharedTermsSet.insert(t);
 876   if (options::bitvectorEqualitySolver()) {
 877     for (unsigned i = 0; i < d_subtheories.size(); ++i) {
 878       d_subtheories[i]->addSharedTerm(t);
 879     }
 880   }
 881 }
 882
 883
 884 EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b)
 885 {
 886   if (options::bitblastMode() == options::BitblastMode::EAGER)
 887     return EQUALITY_UNKNOWN;
 888   Assert(options::bitblastMode() == options::BitblastMode::LAZY);
 889   for (unsigned i = 0; i < d_subtheories.size(); ++i) {
 890     EqualityStatus status = d_subtheories[i]->getEqualityStatus(a, b);
 891     if (status != EQUALITY_UNKNOWN) {
 892       return status;
 893     }
 894   }
 895   return EQUALITY_UNKNOWN; ;
 896 }
 897
 898
 899 void TheoryBV::enableCoreTheorySlicer() {
 900   Assert(!d_calledPreregister);
 901   d_isCoreTheory = true;
 902   if (d_subtheoryMap.find(SUB_CORE) != d_subtheoryMap.end()) {
 903     CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
 904     core->enableSlicer();
 905   }
 906 }
 907
 908
 909 void TheoryBV::ppStaticLearn(TNode in, NodeBuilder<>& learned) {
 910   if(d_staticLearnCache.find(in) != d_staticLearnCache.end()){
 911     return;
 912   }
 913   d_staticLearnCache.insert(in);
 914
 915   if (in.getKind() == kind::EQUAL) {
 916     if((in[0].getKind() == kind::BITVECTOR_PLUS && in[1].getKind() == kind::BITVECTOR_SHL) ||
 917        (in[1].getKind() == kind::BITVECTOR_PLUS && in[0].getKind() == kind::BITVECTOR_SHL)) {
 918       TNode p = in[0].getKind() == kind::BITVECTOR_PLUS ? in[0] : in[1];
 919       TNode s = in[0].getKind() == kind::BITVECTOR_PLUS ? in[1] : in[0];
 920
 921       if(p.getNumChildren() == 2
 922          && p[0].getKind()  == kind::BITVECTOR_SHL
 923          && p[1].getKind()  == kind::BITVECTOR_SHL ){
 924         unsigned size = utils::getSize(s);
 925         Node one = utils::mkConst(size, 1u);
 926         if(s[0] == one && p[0][0] == one && p[1][0] == one){
 927           Node zero = utils::mkConst(size, 0u);
 928           TNode b = p[0];
 929           TNode c = p[1];
 930           // (s : 1 << S) = (b : 1 << B) + (c : 1 << C)
 931           Node b_eq_0 = b.eqNode(zero);
 932           Node c_eq_0 = c.eqNode(zero);
 933           Node b_eq_c = b.eqNode(c);
 934
 935           Node dis = NodeManager::currentNM()->mkNode(
 936               kind::OR, b_eq_0, c_eq_0, b_eq_c);
 937           Node imp = in.impNode(dis);
 938           learned << imp;
 939         }
 940       }
 941     }
 942   }else if(in.getKind() == kind::AND){
 943     for(size_t i = 0, N = in.getNumChildren(); i < N; ++i){
 944       ppStaticLearn(in[i], learned);
 945     }
 946   }
 947 }
 948
 949 bool TheoryBV::applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions) {
 950   bool changed = d_abstractionModule->applyAbstraction(assertions, new_assertions);
 951   if (changed && options::bitblastMode() == options::BitblastMode::EAGER
 952       && options::bitvectorAig())
 953   {
 954     // disable AIG mode
 955     AlwaysAssert(!d_eagerSolver->isInitialized());
 956     d_eagerSolver->turnOffAig();
 957     d_eagerSolver->initialize();
 958   }
 959   return changed;
 960 }
 961
 962 void TheoryBV::setProofLog(proof::BitVectorProof* bvp)
 963 {
 964   if (options::bitblastMode() == options::BitblastMode::EAGER)
 965   {
 966     d_eagerSolver->setProofLog(bvp);
 967   }
 968   else
 969   {
 970     for( unsigned i=0; i< d_subtheories.size(); i++ ){
 971       d_subtheories[i]->setProofLog( bvp );
 972     }
 973   }
 974 }
 975
 976 void TheoryBV::setConflict(Node conflict)
 977 {
 978   if (options::bvAbstraction())
 979   {
 980     NodeManager* const nm = NodeManager::currentNM();
 981     Node new_conflict = d_abstractionModule->simplifyConflict(conflict);
 982
 983     std::vector<Node> lemmas;
 984     lemmas.push_back(new_conflict);
 985     d_abstractionModule->generalizeConflict(new_conflict, lemmas);
 986     for (unsigned i = 0; i < lemmas.size(); ++i)
 987     {
 988       lemma(nm->mkNode(kind::NOT, lemmas[i]));
 989     }
 990   }
 991   d_conflict = true;
 992   d_conflictNode = conflict;
 993 }
 994
 995 } /* namespace CVC4::theory::bv */
 996 } /* namespace CVC4::theory */
 997 } /* namespace CVC4 */