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