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