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