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