src/theory/bv/theory_bv.cpp

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