src/theory/bv/theory_bv.cpp

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