src/theory/bv/theory_bv.cpp

   1 /*********************                                                        */
   2 /*! \file theory_bv.cpp
   3  ** \verbatim
   4  ** Original author: Dejan Jovanovic
   5  ** Major contributors: Liana Hadarean
   6  ** Minor contributors (to current version): Tim King, Kshitij Bansal, Clark Barrett, Andrew Reynolds, Morgan Deters, Martin Brain <>
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2014  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** [[ Add lengthier description here ]]
  13  ** \todo document this file
  14  **/
  15
  16 #include "theory/bv/theory_bv.h"
  17
  18 #include "options/bv_options.h"
  19 #include "options/smt_options.h"
  20 #include "smt/smt_statistics_registry.h"
  21 #include "theory/bv/abstraction.h"
  22 #include "theory/bv/bv_eager_solver.h"
  23 #include "theory/bv/bv_subtheory_algebraic.h"
  24 #include "theory/bv/bv_subtheory_bitblast.h"
  25 #include "theory/bv/bv_subtheory_core.h"
  26 #include "theory/bv/bv_subtheory_inequality.h"
  27 #include "theory/bv/slicer.h"
  28 #include "theory/bv/theory_bv_rewrite_rules_normalization.h"
  29 #include "theory/bv/theory_bv_rewrite_rules_simplification.h"
  30 #include "theory/bv/theory_bv_rewriter.h"
  31 #include "theory/bv/theory_bv_utils.h"
  32 #include "theory/theory_model.h"
  33 #include "proof/theory_proof.h"
  34 #include "proof/proof_manager.h"
  35 #include "theory/valuation.h"
  36
  37 using namespace CVC4::context;
  38 using namespace CVC4::theory::bv::utils;
  39 using namespace std;
  40
  41 namespace CVC4 {
  42 namespace theory {
  43 namespace bv {
  44
  45 TheoryBV::TheoryBV(context::Context* c, context::UserContext* u,
  46                    OutputChannel& out, Valuation valuation,
  47                    const LogicInfo& logicInfo, SmtGlobals* globals)
  48     : Theory(THEORY_BV, c, u, out, valuation, logicInfo, globals),
  49       d_context(c),
  50       d_alreadyPropagatedSet(c),
  51       d_sharedTermsSet(c),
  52       d_subtheories(),
  53       d_subtheoryMap(),
  54       d_statistics(),
  55       d_staticLearnCache(),
  56       d_lemmasAdded(c, false),
  57       d_conflict(c, false),
  58       d_invalidateModelCache(c, true),
  59       d_literalsToPropagate(c),
  60       d_literalsToPropagateIndex(c, 0),
  61       d_propagatedBy(c),
  62       d_eagerSolver(NULL),
  63       d_abstractionModule(new AbstractionModule()),
  64       d_isCoreTheory(false),
  65       d_calledPreregister(false)
  66 {
  67
  68   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
  69     d_eagerSolver = new EagerBitblastSolver(this);
  70     return;
  71   }
  72
  73   if (options::bitvectorEqualitySolver()) {
  74     SubtheorySolver* core_solver = new CoreSolver(c, this);
  75     d_subtheories.push_back(core_solver);
  76     d_subtheoryMap[SUB_CORE] = core_solver;
  77   }
  78
  79   if (options::bitvectorInequalitySolver()) {
  80     SubtheorySolver* ineq_solver = new InequalitySolver(c, this);
  81     d_subtheories.push_back(ineq_solver);
  82     d_subtheoryMap[SUB_INEQUALITY] = ineq_solver;
  83   }
  84
  85   if (options::bitvectorAlgebraicSolver()) {
  86     SubtheorySolver* alg_solver = new AlgebraicSolver(c, this);
  87     d_subtheories.push_back(alg_solver);
  88     d_subtheoryMap[SUB_ALGEBRAIC] = alg_solver;
  89   }
  90
  91   BitblastSolver* bb_solver = new BitblastSolver(c, this);
  92   if (options::bvAbstraction()) {
  93     bb_solver->setAbstraction(d_abstractionModule);
  94   }
  95   d_subtheories.push_back(bb_solver);
  96   d_subtheoryMap[SUB_BITBLAST] = bb_solver;
  97 }
  98
  99
 100 TheoryBV::~TheoryBV() {
 101   for (unsigned i = 0; i < d_subtheories.size(); ++i) {
 102     delete d_subtheories[i];
 103   }
 104   delete d_abstractionModule;
 105 }
 106
 107 void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) {
 108   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
 109     return;
 110   }
 111   if (options::bitvectorEqualitySolver()) {
 112     dynamic_cast<CoreSolver*>(d_subtheoryMap[SUB_CORE])->setMasterEqualityEngine(eq);
 113   }
 114 }
 115
 116 void TheoryBV::spendResource(unsigned ammount) throw(UnsafeInterruptException) {
 117   getOutputChannel().spendResource(ammount);
 118 }
 119
 120 TheoryBV::Statistics::Statistics():
 121   d_avgConflictSize("theory::bv::AvgBVConflictSize"),
 122   d_solveSubstitutions("theory::bv::NumberOfSolveSubstitutions", 0),
 123   d_solveTimer("theory::bv::solveTimer"),
 124   d_numCallsToCheckFullEffort("theory::bv::NumberOfFullCheckCalls", 0),
 125   d_numCallsToCheckStandardEffort("theory::bv::NumberOfStandardCheckCalls", 0),
 126   d_weightComputationTimer("theory::bv::weightComputationTimer"),
 127   d_numMultSlice("theory::bv::NumMultSliceApplied", 0)
 128 {
 129   smtStatisticsRegistry()->registerStat(&d_avgConflictSize);
 130   smtStatisticsRegistry()->registerStat(&d_solveSubstitutions);
 131   smtStatisticsRegistry()->registerStat(&d_solveTimer);
 132   smtStatisticsRegistry()->registerStat(&d_numCallsToCheckFullEffort);
 133   smtStatisticsRegistry()->registerStat(&d_numCallsToCheckStandardEffort);
 134   smtStatisticsRegistry()->registerStat(&d_weightComputationTimer);
 135   smtStatisticsRegistry()->registerStat(&d_numMultSlice);
 136 }
 137
 138 TheoryBV::Statistics::~Statistics() {
 139   smtStatisticsRegistry()->unregisterStat(&d_avgConflictSize);
 140   smtStatisticsRegistry()->unregisterStat(&d_solveSubstitutions);
 141   smtStatisticsRegistry()->unregisterStat(&d_solveTimer);
 142   smtStatisticsRegistry()->unregisterStat(&d_numCallsToCheckFullEffort);
 143   smtStatisticsRegistry()->unregisterStat(&d_numCallsToCheckStandardEffort);
 144   smtStatisticsRegistry()->unregisterStat(&d_weightComputationTimer);
 145   smtStatisticsRegistry()->unregisterStat(&d_numMultSlice);
 146 }
 147
 148 Node TheoryBV::getBVDivByZero(Kind k, unsigned width) {
 149   NodeManager* nm = NodeManager::currentNM();
 150   if (k == kind::BITVECTOR_UDIV) {
 151     if (d_BVDivByZero.find(width) == d_BVDivByZero.end()) {
 152       // lazily create the function symbols
 153       ostringstream os;
 154       os << "BVUDivByZero_" << width;
 155       Node divByZero = nm->mkSkolem(os.str(),
 156                                     nm->mkFunctionType(nm->mkBitVectorType(width), nm->mkBitVectorType(width)),
 157                                     "partial bvudiv", NodeManager::SKOLEM_EXACT_NAME);
 158       d_BVDivByZero[width] = divByZero;
 159     }
 160     return d_BVDivByZero[width];
 161   }
 162   else if (k == kind::BITVECTOR_UREM) {
 163     if (d_BVRemByZero.find(width) == d_BVRemByZero.end()) {
 164       ostringstream os;
 165       os << "BVURemByZero_" << width;
 166       Node divByZero = nm->mkSkolem(os.str(),
 167                                     nm->mkFunctionType(nm->mkBitVectorType(width), nm->mkBitVectorType(width)),
 168                                     "partial bvurem", NodeManager::SKOLEM_EXACT_NAME);
 169       d_BVRemByZero[width] = divByZero;
 170     }
 171     return d_BVRemByZero[width];
 172   }
 173
 174   Unreachable();
 175 }
 176
 177
 178 void TheoryBV::collectNumerators(TNode term, TNodeSet& seen) {
 179   if (seen.find(term) != seen.end())
 180     return;
 181   if (term.getKind() == kind::BITVECTOR_ACKERMANIZE_UDIV) {
 182     unsigned size = utils::getSize(term[0]);
 183     if (d_BVDivByZeroAckerman.find(size) == d_BVDivByZeroAckerman.end()) {
 184       d_BVDivByZeroAckerman[size] = TNodeSet();
 185     }
 186     d_BVDivByZeroAckerman[size].insert(term[0]);
 187     seen.insert(term);
 188   } else if (term.getKind() == kind::BITVECTOR_ACKERMANIZE_UREM) {
 189     unsigned size = utils::getSize(term[0]);
 190     if (d_BVRemByZeroAckerman.find(size) == d_BVRemByZeroAckerman.end()) {
 191       d_BVRemByZeroAckerman[size] = TNodeSet();
 192     }
 193     d_BVRemByZeroAckerman[size].insert(term[0]);
 194     seen.insert(term);
 195   }
 196   for (unsigned i = 0; i < term.getNumChildren(); ++i) {
 197     collectNumerators(term[i], seen);
 198   }
 199   seen.insert(term);
 200 }
 201
 202 void TheoryBV::mkAckermanizationAsssertions(std::vector<Node>& assertions) {
 203   Debug("bv-ackermanize") << "TheoryBV::mkAckermanizationAsssertions\n";
 204
 205   Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER);
 206   AlwaysAssert(!options::incrementalSolving());
 207   TNodeSet seen;
 208   for (unsigned i = 0; i < assertions.size(); ++i) {
 209     collectNumerators(assertions[i], seen);
 210   }
 211
 212   // process division UF
 213   Debug("bv-ackermanize") << "Process division UF...\n";
 214   for (WidthToNumerators::const_iterator it = d_BVDivByZeroAckerman.begin(); it != d_BVDivByZeroAckerman.end(); ++it) {
 215     const TNodeSet& numerators= it->second;
 216     for (TNodeSet::const_iterator i = numerators.begin(); i != numerators.end(); ++i) {
 217       TNodeSet::const_iterator j = i;
 218       j++;
 219       for (; j != numerators.end(); ++j) {
 220         TNode arg1 = *i;
 221         TNode arg2 = *j;
 222         TNode acker1 = utils::mkNode(kind::BITVECTOR_ACKERMANIZE_UDIV, arg1);
 223         TNode acker2 = utils::mkNode(kind::BITVECTOR_ACKERMANIZE_UDIV, arg2);
 224
 225         Node arg_eq = utils::mkNode(kind::EQUAL, arg1, arg2);
 226         Node acker_eq = utils::mkNode(kind::EQUAL, acker1, acker2);
 227         Node lemma = utils::mkNode(kind::IMPLIES, arg_eq, acker_eq);
 228         Debug("bv-ackermanize") << "  " << lemma << "\n";
 229         assertions.push_back(lemma);
 230       }
 231     }
 232   }
 233   // process remainder UF
 234   Debug("bv-ackermanize") << "Process remainder UF...\n";
 235   for (WidthToNumerators::const_iterator it = d_BVRemByZeroAckerman.begin(); it != d_BVRemByZeroAckerman.end(); ++it) {
 236     const TNodeSet& numerators= it->second;
 237     for (TNodeSet::const_iterator i = numerators.begin(); i != numerators.end(); ++i) {
 238       TNodeSet::const_iterator j = i;
 239       j++;
 240       for (; j != numerators.end(); ++j) {
 241         TNode arg1 = *i;
 242         TNode arg2 = *j;
 243         TNode acker1 = utils::mkNode(kind::BITVECTOR_ACKERMANIZE_UREM, arg1);
 244         TNode acker2 = utils::mkNode(kind::BITVECTOR_ACKERMANIZE_UREM, arg2);
 245
 246         Node arg_eq = utils::mkNode(kind::EQUAL, arg1, arg2);
 247         Node acker_eq = utils::mkNode(kind::EQUAL, acker1, acker2);
 248         Node lemma = utils::mkNode(kind::IMPLIES, arg_eq, acker_eq);
 249         Debug("bv-ackermanize") << "  " << lemma << "\n";
 250         assertions.push_back(lemma);
 251       }
 252     }
 253   }
 254 }
 255
 256 Node TheoryBV::expandDefinition(LogicRequest &logicRequest, Node node) {
 257   Debug("bitvector-expandDefinition") << "TheoryBV::expandDefinition(" << node << ")" << std::endl;
 258
 259   switch (node.getKind()) {
 260   case kind::BITVECTOR_SDIV:
 261   case kind::BITVECTOR_SREM:
 262   case kind::BITVECTOR_SMOD:
 263     return TheoryBVRewriter::eliminateBVSDiv(node);
 264     break;
 265
 266   case kind::BITVECTOR_UDIV:
 267   case kind::BITVECTOR_UREM: {
 268     NodeManager* nm = NodeManager::currentNM();
 269     unsigned width = node.getType().getBitVectorSize();
 270
 271     if (options::bitvectorDivByZeroConst()) {
 272       Kind kind = node.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_UDIV_TOTAL : kind::BITVECTOR_UREM_TOTAL;
 273       return nm->mkNode(kind, node[0], node[1]);
 274     }
 275
 276     TNode num = node[0], den = node[1];
 277     Node den_eq_0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(BitVector(width, Integer(0))));
 278     Node divTotalNumDen = nm->mkNode(node.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_UDIV_TOTAL :
 279                                      kind::BITVECTOR_UREM_TOTAL, num, den);
 280
 281     if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
 282       // Ackermanize UF if using eager bit-blasting
 283       Node ackerman_var = nm->mkNode(node.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_ACKERMANIZE_UDIV : kind::BITVECTOR_ACKERMANIZE_UREM, num);
 284       node = nm->mkNode(kind::ITE, den_eq_0, ackerman_var, divTotalNumDen);
 285       return node;
 286     } else {
 287       Node divByZero = getBVDivByZero(node.getKind(), width);
 288       Node divByZeroNum = nm->mkNode(kind::APPLY_UF, divByZero, num);
 289       node = nm->mkNode(kind::ITE, den_eq_0, divByZeroNum, divTotalNumDen);
 290       logicRequest.widenLogic(THEORY_UF);
 291       return node;
 292     }
 293   }
 294     break;
 295
 296   default:
 297     return node;
 298     break;
 299   }
 300
 301   Unreachable();
 302 }
 303
 304
 305 void TheoryBV::preRegisterTerm(TNode node) {
 306   d_calledPreregister = true;
 307   Debug("bitvector-preregister") << "TheoryBV::preRegister(" << node << ")" << std::endl;
 308
 309   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
 310     // the aig bit-blaster option is set heuristically
 311     // if bv abstraction is not used
 312     if (!d_eagerSolver->isInitialized()) {
 313       d_eagerSolver->initialize();
 314     }
 315
 316     if (node.getKind() == kind::BITVECTOR_EAGER_ATOM) {
 317       Node formula = node[0];
 318       d_eagerSolver->assertFormula(formula);
 319     }
 320     // nothing to do for the other terms
 321     return;
 322   }
 323
 324   for (unsigned i = 0; i < d_subtheories.size(); ++i) {
 325     d_subtheories[i]->preRegister(node);
 326   }
 327 }
 328
 329 void TheoryBV::sendConflict() {
 330   Assert(d_conflict);
 331   if (d_conflictNode.isNull()) {
 332     return;
 333   } else {
 334     Debug("bitvector") << indent() << "TheoryBV::check(): conflict " << d_conflictNode;
 335     d_out->conflict(d_conflictNode);
 336     d_statistics.d_avgConflictSize.addEntry(d_conflictNode.getNumChildren());
 337     d_conflictNode = Node::null();
 338   }
 339 }
 340
 341 void TheoryBV::checkForLemma(TNode fact) {
 342   if (fact.getKind() == kind::EQUAL) {
 343     if (fact[0].getKind() == kind::BITVECTOR_UREM_TOTAL) {
 344       TNode urem = fact[0];
 345       TNode result = fact[1];
 346       TNode divisor = urem[1];
 347       Node result_ult_div = mkNode(kind::BITVECTOR_ULT, result, divisor);
 348       Node divisor_eq_0 = mkNode(kind::EQUAL,
 349                                  divisor,
 350                                  mkConst(BitVector(getSize(divisor), 0u)));
 351       Node split = utils::mkNode(kind::OR, divisor_eq_0, mkNode(kind::NOT, fact), result_ult_div);
 352       lemma(split);
 353     }
 354     if (fact[1].getKind() == kind::BITVECTOR_UREM_TOTAL) {
 355       TNode urem = fact[1];
 356       TNode result = fact[0];
 357       TNode divisor = urem[1];
 358       Node result_ult_div = mkNode(kind::BITVECTOR_ULT, result, divisor);
 359       Node divisor_eq_0 = mkNode(kind::EQUAL,
 360                                  divisor,
 361                                  mkConst(BitVector(getSize(divisor), 0u)));
 362       Node split = utils::mkNode(kind::OR, divisor_eq_0, mkNode(kind::NOT, fact), result_ult_div);
 363       lemma(split);
 364     }
 365   }
 366 }
 367
 368 void TheoryBV::check(Effort e)
 369 {
 370   if (done() && !fullEffort(e)) {
 371     return;
 372   }
 373   TimerStat::CodeTimer checkTimer(d_checkTime);
 374   Debug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl;
 375   TimerStat::CodeTimer codeTimer(d_statistics.d_solveTimer);
 376   // we may be getting new assertions so the model cache may not be sound
 377   d_invalidateModelCache.set(true);
 378   // if we are using the eager solver
 379   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
 380     // this can only happen on an empty benchmark
 381     if (!d_eagerSolver->isInitialized()) {
 382       d_eagerSolver->initialize();
 383     }
 384     if (!Theory::fullEffort(e))
 385       return;
 386
 387     std::vector<TNode> assertions;
 388     while (!done()) {
 389       TNode fact = get().assertion;
 390       Assert (fact.getKind() == kind::BITVECTOR_EAGER_ATOM);
 391       assertions.push_back(fact);
 392     }
 393     Assert (d_eagerSolver->hasAssertions(assertions));
 394
 395     bool ok = d_eagerSolver->checkSat();
 396     if (!ok) {
 397       if (assertions.size() == 1) {
 398         d_out->conflict(assertions[0]);
 399         return;
 400       }
 401       Node conflict = NodeManager::currentNM()->mkNode(kind::AND, assertions);
 402       d_out->conflict(conflict);
 403       return;
 404     }
 405     return;
 406   }
 407
 408
 409   if (Theory::fullEffort(e)) {
 410     ++(d_statistics.d_numCallsToCheckFullEffort);
 411   } else {
 412     ++(d_statistics.d_numCallsToCheckStandardEffort);
 413   }
 414   // if we are already in conflict just return the conflict
 415   if (inConflict()) {
 416     sendConflict();
 417     return;
 418   }
 419
 420   while (!done()) {
 421     TNode fact = get().assertion;
 422
 423     checkForLemma(fact);
 424
 425     for (unsigned i = 0; i < d_subtheories.size(); ++i) {
 426       d_subtheories[i]->assertFact(fact);
 427     }
 428   }
 429
 430   bool ok = true;
 431   bool complete = false;
 432   for (unsigned i = 0; i < d_subtheories.size(); ++i) {
 433     Assert (!inConflict());
 434     ok = d_subtheories[i]->check(e);
 435     complete = d_subtheories[i]->isComplete();
 436
 437     if (!ok) {
 438       // if we are in a conflict no need to check with other theories
 439       Assert (inConflict());
 440       sendConflict();
 441       return;
 442     }
 443     if (complete) {
 444       // if the last subtheory was complete we stop
 445       return;
 446     }
 447   }
 448 }
 449
 450 void TheoryBV::collectModelInfo( TheoryModel* m, bool fullModel ){
 451   Assert(!inConflict());
 452   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
 453     d_eagerSolver->collectModelInfo(m, fullModel);
 454   }
 455   for (unsigned i = 0; i < d_subtheories.size(); ++i) {
 456     if (d_subtheories[i]->isComplete()) {
 457       d_subtheories[i]->collectModelInfo(m, fullModel);
 458       return;
 459     }
 460   }
 461 }
 462
 463 Node TheoryBV::getModelValue(TNode var) {
 464   Assert(!inConflict());
 465   for (unsigned i = 0; i < d_subtheories.size(); ++i) {
 466     if (d_subtheories[i]->isComplete()) {
 467       return d_subtheories[i]->getModelValue(var);
 468     }
 469   }
 470   Unreachable();
 471 }
 472
 473 void TheoryBV::propagate(Effort e) {
 474   Debug("bitvector") << indent() << "TheoryBV::propagate()" << std::endl;
 475   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
 476     return;
 477   }
 478
 479   if (inConflict()) {
 480     return;
 481   }
 482
 483   // go through stored propagations
 484   bool ok = true;
 485   for (; d_literalsToPropagateIndex < d_literalsToPropagate.size() && ok; d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) {
 486     TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex];
 487     // temporary fix for incremental bit-blasting
 488     if (d_valuation.isSatLiteral(literal)) {
 489       Debug("bitvector::propagate") << "TheoryBV:: propagating " << literal <<"\n";
 490       ok = d_out->propagate(literal);
 491     }
 492   }
 493
 494   if (!ok) {
 495     Debug("bitvector::propagate") << indent() << "TheoryBV::propagate(): conflict from theory engine" << std::endl;
 496     setConflict();
 497   }
 498 }
 499
 500
 501 Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
 502   switch(in.getKind()) {
 503   case kind::EQUAL:
 504     {
 505       if (in[0].isVar() && !in[1].hasSubterm(in[0])) {
 506         ++(d_statistics.d_solveSubstitutions);
 507         outSubstitutions.addSubstitution(in[0], in[1]);
 508         return PP_ASSERT_STATUS_SOLVED;
 509       }
 510       if (in[1].isVar() && !in[0].hasSubterm(in[1])) {
 511         ++(d_statistics.d_solveSubstitutions);
 512         outSubstitutions.addSubstitution(in[1], in[0]);
 513         return PP_ASSERT_STATUS_SOLVED;
 514       }
 515       Node node = Rewriter::rewrite(in);
 516       if ((node[0].getKind() == kind::BITVECTOR_EXTRACT && node[1].isConst()) ||
 517           (node[1].getKind() == kind::BITVECTOR_EXTRACT && node[0].isConst())) {
 518         Node extract = node[0].isConst() ? node[1] : node[0];
 519         if (extract[0].getKind() == kind::VARIABLE) {
 520           Node c = node[0].isConst() ? node[0] : node[1];
 521
 522           unsigned high = utils::getExtractHigh(extract);
 523           unsigned low = utils::getExtractLow(extract);
 524           unsigned var_bitwidth = utils::getSize(extract[0]);
 525           std::vector<Node> children;
 526
 527           if (low == 0) {
 528             Assert (high != var_bitwidth - 1);
 529             unsigned skolem_size = var_bitwidth - high - 1;
 530             Node skolem = utils::mkVar(skolem_size);
 531             children.push_back(skolem);
 532             children.push_back(c);
 533           } else if (high == var_bitwidth - 1) {
 534             unsigned skolem_size = low;
 535             Node skolem = utils::mkVar(skolem_size);
 536             children.push_back(c);
 537             children.push_back(skolem);
 538           } else {
 539             unsigned skolem1_size = low;
 540             unsigned skolem2_size = var_bitwidth - high - 1;
 541             Node skolem1 = utils::mkVar(skolem1_size);
 542             Node skolem2 = utils::mkVar(skolem2_size);
 543             children.push_back(skolem2);
 544             children.push_back(c);
 545             children.push_back(skolem1);
 546           }
 547           Node concat = utils::mkNode(kind::BITVECTOR_CONCAT, children);
 548           Assert (utils::getSize(concat) == utils::getSize(extract[0]));
 549           outSubstitutions.addSubstitution(extract[0], concat);
 550           return PP_ASSERT_STATUS_SOLVED;
 551         }
 552       }
 553     }
 554     break;
 555   case kind::BITVECTOR_ULT:
 556   case kind::BITVECTOR_SLT:
 557   case kind::BITVECTOR_ULE:
 558   case kind::BITVECTOR_SLE:
 559
 560   default:
 561     // TODO other predicates
 562     break;
 563   }
 564   return PP_ASSERT_STATUS_UNSOLVED;
 565 }
 566
 567 Node TheoryBV::ppRewrite(TNode t)
 568 {
 569   Debug("bv-pp-rewrite") << "TheoryBV::ppRewrite " << t << "\n";
 570   Node res = t;
 571   if (RewriteRule<BitwiseEq>::applies(t)) {
 572     Node result = RewriteRule<BitwiseEq>::run<false>(t);
 573     res = Rewriter::rewrite(result);
 574   } else if (d_isCoreTheory && t.getKind() == kind::EQUAL) {
 575     std::vector<Node> equalities;
 576     Slicer::splitEqualities(t, equalities);
 577     res = utils::mkAnd(equalities);
 578   } else if (RewriteRule<UltPlusOne>::applies(t)) {
 579     Node result = RewriteRule<UltPlusOne>::run<false>(t);
 580     res = Rewriter::rewrite(result);
 581   } else if( res.getKind() == kind::EQUAL &&
 582       ((res[0].getKind() == kind::BITVECTOR_PLUS &&
 583         RewriteRule<ConcatToMult>::applies(res[1])) ||
 584        (res[1].getKind() == kind::BITVECTOR_PLUS &&
 585         RewriteRule<ConcatToMult>::applies(res[0])))) {
 586     Node mult = RewriteRule<ConcatToMult>::applies(res[0])?
 587       RewriteRule<ConcatToMult>::run<false>(res[0]) :
 588       RewriteRule<ConcatToMult>::run<true>(res[1]);
 589     Node factor = mult[0];
 590     Node sum =  RewriteRule<ConcatToMult>::applies(res[0])? res[1] : res[0];
 591     Node new_eq =utils::mkNode(kind::EQUAL, sum, mult);
 592     Node rewr_eq = RewriteRule<SolveEq>::run<true>(new_eq);
 593     if (rewr_eq[0].isVar() || rewr_eq[1].isVar()){
 594       res = Rewriter::rewrite(rewr_eq);
 595     } else {
 596       res = t;
 597     }
 598   }
 599
 600
 601   // if(t.getKind() == kind::EQUAL &&
 602   //    ((t[0].getKind() == kind::BITVECTOR_MULT && t[1].getKind() == kind::BITVECTOR_PLUS) ||
 603   //     (t[1].getKind() == kind::BITVECTOR_MULT && t[0].getKind() == kind::BITVECTOR_PLUS))) {
 604   //   // if we have an equality between a multiplication and addition
 605   //   // try to express multiplication in terms of addition
 606   //   Node mult = t[0].getKind() == kind::BITVECTOR_MULT? t[0] : t[1];
 607   //   Node add = t[0].getKind() == kind::BITVECTOR_PLUS? t[0] : t[1];
 608   //   if (RewriteRule<MultSlice>::applies(mult)) {
 609   //     Node new_mult = RewriteRule<MultSlice>::run<false>(mult);
 610   //     Node new_eq = Rewriter::rewrite(utils::mkNode(kind::EQUAL, new_mult, add));
 611
 612   //     // the simplification can cause the formula to blow up
 613   //     // only apply if formula reduced
 614   //     if (d_subtheoryMap.find(SUB_BITBLAST) != d_subtheoryMap.end()) {
 615   //       BitblastSolver* bv = (BitblastSolver*)d_subtheoryMap[SUB_BITBLAST];
 616   //       uint64_t old_size = bv->computeAtomWeight(t);
 617   //       Assert (old_size);
 618   //       uint64_t new_size = bv->computeAtomWeight(new_eq);
 619   //       double ratio = ((double)new_size)/old_size;
 620   //       if (ratio <= 0.4) {
 621   //         ++(d_statistics.d_numMultSlice);
 622   //         return new_eq;
 623   //       }
 624   //     }
 625
 626   //     if (new_eq.getKind() == kind::CONST_BOOLEAN) {
 627   //       ++(d_statistics.d_numMultSlice);
 628   //       return new_eq;
 629   //     }
 630   //   }
 631   // }
 632
 633   if (options::bvAbstraction() && t.getType().isBoolean()) {
 634     d_abstractionModule->addInputAtom(res);
 635   }
 636   Debug("bv-pp-rewrite") << "to   " << res << "\n";
 637   return res;
 638 }
 639
 640 void TheoryBV::presolve() {
 641   Debug("bitvector") << "TheoryBV::presolve" << endl;
 642 }
 643
 644 static int prop_count = 0;
 645
 646 bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory)
 647 {
 648   Debug("bitvector::propagate") << indent() << getSatContext()->getLevel() << " " << "TheoryBV::storePropagation(" << literal << ", " << subtheory << ")" << std::endl;
 649   prop_count++;
 650
 651   // If already in conflict, no more propagation
 652   if (d_conflict) {
 653     Debug("bitvector::propagate") << indent() << "TheoryBV::storePropagation(" << literal << ", " << subtheory << "): already in conflict" << std::endl;
 654     return false;
 655   }
 656
 657   // If propagated already, just skip
 658   PropagatedMap::const_iterator find = d_propagatedBy.find(literal);
 659   if (find != d_propagatedBy.end()) {
 660     return true;
 661   } else {
 662     bool polarity = literal.getKind() != kind::NOT;
 663     Node negatedLiteral = polarity ? literal.notNode() : (Node) literal[0];
 664     find = d_propagatedBy.find(negatedLiteral);
 665     if (find != d_propagatedBy.end() && (*find).second != subtheory) {
 666       // Safe to ignore this one, subtheory should produce a conflict
 667       return true;
 668     }
 669
 670     d_propagatedBy[literal] = subtheory;
 671   }
 672
 673   // Propagate differs depending on the subtheory
 674   // * bitblaster needs to be left alone until it's done, otherwise it doesn't know how to explain
 675   // * equality engine can propagate eagerly
 676   bool ok = true;
 677   if (subtheory == SUB_CORE) {
 678     d_out->propagate(literal);
 679     if (!ok) {
 680       setConflict();
 681     }
 682   } else {
 683     d_literalsToPropagate.push_back(literal);
 684   }
 685   return ok;
 686
 687 }/* TheoryBV::propagate(TNode) */
 688
 689
 690 void TheoryBV::explain(TNode literal, std::vector<TNode>& assumptions) {
 691   Assert (wasPropagatedBySubtheory(literal));
 692   SubTheory sub = getPropagatingSubtheory(literal);
 693   d_subtheoryMap[sub]->explain(literal, assumptions);
 694 }
 695
 696
 697 Node TheoryBV::explain(TNode node) {
 698   Debug("bitvector::explain") << "TheoryBV::explain(" << node << ")" << std::endl;
 699   std::vector<TNode> assumptions;
 700
 701   // Ask for the explanation
 702   explain(node, assumptions);
 703   // this means that it is something true at level 0
 704   if (assumptions.size() == 0) {
 705     return utils::mkTrue();
 706   }
 707   // return the explanation
 708   Node explanation = utils::mkAnd(assumptions);
 709   Debug("bitvector::explain") << "TheoryBV::explain(" << node << ") => " << explanation << std::endl;
 710   Debug("bitvector::explain") << "TheoryBV::explain done. \n";
 711   return explanation;
 712 }
 713
 714
 715 void TheoryBV::addSharedTerm(TNode t) {
 716   Debug("bitvector::sharing") << indent() << "TheoryBV::addSharedTerm(" << t << ")" << std::endl;
 717   d_sharedTermsSet.insert(t);
 718   if (options::bitvectorEqualitySolver()) {
 719     for (unsigned i = 0; i < d_subtheories.size(); ++i) {
 720       d_subtheories[i]->addSharedTerm(t);
 721     }
 722   }
 723 }
 724
 725
 726 EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b)
 727 {
 728   Assert (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY);
 729   for (unsigned i = 0; i < d_subtheories.size(); ++i) {
 730     EqualityStatus status = d_subtheories[i]->getEqualityStatus(a, b);
 731     if (status != EQUALITY_UNKNOWN) {
 732       return status;
 733     }
 734   }
 735   return EQUALITY_UNKNOWN; ;
 736 }
 737
 738
 739 void TheoryBV::enableCoreTheorySlicer() {
 740   Assert (!d_calledPreregister);
 741   d_isCoreTheory = true;
 742   if (d_subtheoryMap.find(SUB_CORE) != d_subtheoryMap.end()) {
 743     CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
 744     core->enableSlicer();
 745   }
 746 }
 747
 748
 749 void TheoryBV::ppStaticLearn(TNode in, NodeBuilder<>& learned) {
 750   if(d_staticLearnCache.find(in) != d_staticLearnCache.end()){
 751     return;
 752   }
 753   d_staticLearnCache.insert(in);
 754
 755   if (in.getKind() == kind::EQUAL) {
 756     if((in[0].getKind() == kind::BITVECTOR_PLUS && in[1].getKind() == kind::BITVECTOR_SHL) ||
 757        (in[1].getKind() == kind::BITVECTOR_PLUS && in[0].getKind() == kind::BITVECTOR_SHL)) {
 758       TNode p = in[0].getKind() == kind::BITVECTOR_PLUS ? in[0] : in[1];
 759       TNode s = in[0].getKind() == kind::BITVECTOR_PLUS ? in[1] : in[0];
 760
 761       if(p.getNumChildren() == 2
 762          && p[0].getKind()  == kind::BITVECTOR_SHL
 763          && p[1].getKind()  == kind::BITVECTOR_SHL ){
 764         unsigned size = utils::getSize(s);
 765         Node one = utils::mkConst(size, 1u);
 766         if(s[0] == one && p[0][0] == one && p[1][0] == one){
 767           Node zero = utils::mkConst(size, 0u);
 768           TNode b = p[0];
 769           TNode c = p[1];
 770           // (s : 1 << S) = (b : 1 << B) + (c : 1 << C)
 771           Node b_eq_0 = b.eqNode(zero);
 772           Node c_eq_0 = c.eqNode(zero);
 773           Node b_eq_c = b.eqNode(c);
 774
 775           Node dis = utils::mkNode(kind::OR, b_eq_0, c_eq_0, b_eq_c);
 776           Node imp = in.impNode(dis);
 777           learned << imp;
 778         }
 779       }
 780     }
 781   }else if(in.getKind() == kind::AND){
 782     for(size_t i = 0, N = in.getNumChildren(); i < N; ++i){
 783       ppStaticLearn(in[i], learned);
 784     }
 785   }
 786 }
 787
 788 bool TheoryBV::applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions) {
 789   bool changed = d_abstractionModule->applyAbstraction(assertions, new_assertions);
 790   if (changed &&
 791       options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER &&
 792       options::bitvectorAig()) {
 793     // disable AIG mode
 794     AlwaysAssert (!d_eagerSolver->isInitialized());
 795     d_eagerSolver->turnOffAig();
 796     d_eagerSolver->initialize();
 797   }
 798   return changed;
 799 }
 800
 801 void TheoryBV::setProofLog( BitVectorProof * bvp ) {
 802   if( options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER ){
 803     d_eagerSolver->setProofLog( bvp );
 804   }else{
 805     for( unsigned i=0; i< d_subtheories.size(); i++ ){
 806       d_subtheories[i]->setProofLog( bvp );
 807     }
 808   }
 809 }
 810
 811 void TheoryBV::setConflict(Node conflict) {
 812   if (options::bvAbstraction()) {
 813     Node new_conflict = d_abstractionModule->simplifyConflict(conflict);
 814
 815     std::vector<Node> lemmas;
 816     lemmas.push_back(new_conflict);
 817     d_abstractionModule->generalizeConflict(new_conflict, lemmas);
 818     for (unsigned i = 0; i < lemmas.size(); ++i) {
 819       lemma(utils::mkNode(kind::NOT, lemmas[i]));
 820     }
 821   }
 822   d_conflict = true;
 823   d_conflictNode = conflict;
 824 }
 825
 826 } /* namespace CVC4::theory::bv */
 827 } /* namespace CVC4::theory */
 828 } /* namespace CVC4 */