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