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