src/theory/bv/theory_bv.cpp

   1 /*********************                                                        */
   2 /*! \file theory_bv.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Liana Hadarean, Aina Niemetz, Andrew Reynolds
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2018 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(),
  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(getStatsPrefix(THEORY_BV))),
  68     d_isCoreTheory(false),
  69     d_calledPreregister(false),
  70     d_needsLastCallCheck(false),
  71     d_extf_range_infer(u),
  72     d_extf_collapse_infer(u)
  73 {
  74   setupExtTheory();
  75   getExtTheory()->addFunctionKind(kind::BITVECTOR_TO_NAT);
  76   getExtTheory()->addFunctionKind(kind::INT_TO_BITVECTOR);
  77   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
  78     d_eagerSolver = new EagerBitblastSolver(this);
  79     return;
  80   }
  81
  82   if (options::bitvectorEqualitySolver() && !options::proof())
  83   {
  84     SubtheorySolver* core_solver = new CoreSolver(c, this);
  85     d_subtheories.push_back(core_solver);
  86     d_subtheoryMap[SUB_CORE] = core_solver;
  87   }
  88
  89   if (options::bitvectorInequalitySolver() && !options::proof())
  90   {
  91     SubtheorySolver* ineq_solver = new InequalitySolver(c, u, this);
  92     d_subtheories.push_back(ineq_solver);
  93     d_subtheoryMap[SUB_INEQUALITY] = ineq_solver;
  94   }
  95
  96   if (options::bitvectorAlgebraicSolver() && !options::proof())
  97   {
  98     SubtheorySolver* alg_solver = new AlgebraicSolver(c, this);
  99     d_subtheories.push_back(alg_solver);
 100     d_subtheoryMap[SUB_ALGEBRAIC] = alg_solver;
 101   }
 102
 103   BitblastSolver* bb_solver = new BitblastSolver(c, this);
 104   if (options::bvAbstraction()) {
 105     bb_solver->setAbstraction(d_abstractionModule);
 106   }
 107   d_subtheories.push_back(bb_solver);
 108   d_subtheoryMap[SUB_BITBLAST] = bb_solver;
 109 }
 110
 111 TheoryBV::~TheoryBV() {
 112   if (d_eagerSolver) {
 113     delete d_eagerSolver;
 114   }
 115   for (unsigned i = 0; i < d_subtheories.size(); ++i) {
 116     delete d_subtheories[i];
 117   }
 118   delete d_abstractionModule;
 119 }
 120
 121 void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) {
 122   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
 123     return;
 124   }
 125   if (options::bitvectorEqualitySolver()) {
 126     dynamic_cast<CoreSolver*>(d_subtheoryMap[SUB_CORE])->setMasterEqualityEngine(eq);
 127   }
 128 }
 129
 130 void TheoryBV::spendResource(unsigned amount)
 131 {
 132   getOutputChannel().spendResource(amount);
 133 }
 134
 135 TheoryBV::Statistics::Statistics():
 136   d_avgConflictSize("theory::bv::AvgBVConflictSize"),
 137   d_solveSubstitutions("theory::bv::NumSolveSubstitutions", 0),
 138   d_solveTimer("theory::bv::solveTimer"),
 139   d_numCallsToCheckFullEffort("theory::bv::NumFullCheckCalls", 0),
 140   d_numCallsToCheckStandardEffort("theory::bv::NumStandardCheckCalls", 0),
 141   d_weightComputationTimer("theory::bv::weightComputationTimer"),
 142   d_numMultSlice("theory::bv::NumMultSliceApplied", 0)
 143 {
 144   smtStatisticsRegistry()->registerStat(&d_avgConflictSize);
 145   smtStatisticsRegistry()->registerStat(&d_solveSubstitutions);
 146   smtStatisticsRegistry()->registerStat(&d_solveTimer);
 147   smtStatisticsRegistry()->registerStat(&d_numCallsToCheckFullEffort);
 148   smtStatisticsRegistry()->registerStat(&d_numCallsToCheckStandardEffort);
 149   smtStatisticsRegistry()->registerStat(&d_weightComputationTimer);
 150   smtStatisticsRegistry()->registerStat(&d_numMultSlice);
 151 }
 152
 153 TheoryBV::Statistics::~Statistics() {
 154   smtStatisticsRegistry()->unregisterStat(&d_avgConflictSize);
 155   smtStatisticsRegistry()->unregisterStat(&d_solveSubstitutions);
 156   smtStatisticsRegistry()->unregisterStat(&d_solveTimer);
 157   smtStatisticsRegistry()->unregisterStat(&d_numCallsToCheckFullEffort);
 158   smtStatisticsRegistry()->unregisterStat(&d_numCallsToCheckStandardEffort);
 159   smtStatisticsRegistry()->unregisterStat(&d_weightComputationTimer);
 160   smtStatisticsRegistry()->unregisterStat(&d_numMultSlice);
 161 }
 162
 163 Node TheoryBV::getBVDivByZero(Kind k, unsigned width) {
 164   NodeManager* nm = NodeManager::currentNM();
 165   if (k == kind::BITVECTOR_UDIV) {
 166     if (d_BVDivByZero.find(width) == d_BVDivByZero.end()) {
 167       // lazily create the function symbols
 168       ostringstream os;
 169       os << "BVUDivByZero_" << width;
 170       Node divByZero = nm->mkSkolem(os.str(),
 171                                     nm->mkFunctionType(nm->mkBitVectorType(width), nm->mkBitVectorType(width)),
 172                                     "partial bvudiv", NodeManager::SKOLEM_EXACT_NAME);
 173       d_BVDivByZero[width] = divByZero;
 174     }
 175     return d_BVDivByZero[width];
 176   }
 177   else if (k == kind::BITVECTOR_UREM) {
 178     if (d_BVRemByZero.find(width) == d_BVRemByZero.end()) {
 179       ostringstream os;
 180       os << "BVURemByZero_" << width;
 181       Node divByZero = nm->mkSkolem(os.str(),
 182                                     nm->mkFunctionType(nm->mkBitVectorType(width), nm->mkBitVectorType(width)),
 183                                     "partial bvurem", NodeManager::SKOLEM_EXACT_NAME);
 184       d_BVRemByZero[width] = divByZero;
 185     }
 186     return d_BVRemByZero[width];
 187   }
 188
 189   Unreachable();
 190 }
 191
 192
 193 void TheoryBV::collectFunctionSymbols(TNode term, TNodeSet& seen) {
 194   if (seen.find(term) != seen.end())
 195     return;
 196   if (term.getKind() == kind::APPLY_UF) {
 197     TNode func = term.getOperator();
 198     storeFunction(func, term);
 199   } else if (term.getKind() == kind::SELECT) {
 200     TNode func = term[0];
 201     storeFunction(func, term);
 202   } else if (term.getKind() == kind::STORE) {
 203     AlwaysAssert(false, "Cannot use eager bitblasting on QF_ABV formula with stores");
 204   }
 205   for (unsigned i = 0; i < term.getNumChildren(); ++i) {
 206     collectFunctionSymbols(term[i], seen);
 207   }
 208   seen.insert(term);
 209 }
 210
 211 void TheoryBV::storeFunction(TNode func, TNode term) {
 212   if (d_funcToArgs.find(func) == d_funcToArgs.end()) {
 213     d_funcToArgs.insert(make_pair(func, NodeSet()));
 214   }
 215   NodeSet& set = d_funcToArgs[func];
 216   if (set.find(term) == set.end()) {
 217     set.insert(term);
 218     Node skolem = utils::mkVar(utils::getSize(term));
 219     d_funcToSkolem.addSubstitution(term, skolem);
 220   }
 221 }
 222
 223 void TheoryBV::mkAckermanizationAssertions(std::vector<Node>& assertions) {
 224   Debug("bv-ackermanize") << "TheoryBV::mkAckermanizationAssertions\n";
 225
 226   Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER);
 227   AlwaysAssert(!options::incrementalSolving());
 228   TNodeSet seen;
 229   for (unsigned i = 0; i < assertions.size(); ++i) {
 230     collectFunctionSymbols(assertions[i], seen);
 231   }
 232
 233   FunctionToArgs::const_iterator it = d_funcToArgs.begin();
 234   NodeManager* nm = NodeManager::currentNM();
 235   for (; it!= d_funcToArgs.end(); ++it) {
 236     TNode func = it->first;
 237     const NodeSet& args = it->second;
 238     NodeSet::const_iterator it1 = args.begin();
 239     for ( ; it1 != args.end(); ++it1) {
 240       for(NodeSet::const_iterator it2 = it1; it2 != args.end(); ++it2) {
 241         TNode args1 = *it1;
 242         TNode args2 = *it2;
 243         Node args_eq;
 244
 245         if (args1.getKind() == kind::APPLY_UF) {
 246           AlwaysAssert (args1.getKind() == kind::APPLY_UF &&
 247                         args1.getOperator() == func);
 248           AlwaysAssert (args2.getKind() == kind::APPLY_UF &&
 249                         args2.getOperator() == func);
 250           AlwaysAssert (args1.getNumChildren() == args2.getNumChildren());
 251
 252           std::vector<Node> eqs(args1.getNumChildren());
 253
 254           for (unsigned i = 0; i < args1.getNumChildren(); ++i) {
 255             eqs[i] = nm->mkNode(kind::EQUAL, args1[i], args2[i]);
 256           }
 257           args_eq = utils::mkAnd(eqs);
 258         } else {
 259           AlwaysAssert (args1.getKind() == kind::SELECT &&
 260                         args1[0] == func);
 261           AlwaysAssert (args2.getKind() == kind::SELECT &&
 262                         args2[0] == func);
 263           AlwaysAssert (args1.getNumChildren() == 2);
 264           AlwaysAssert (args2.getNumChildren() == 2);
 265           args_eq = nm->mkNode(kind::EQUAL, args1[1], args2[1]);
 266         }
 267         Node func_eq = nm->mkNode(kind::EQUAL, args1, args2);
 268         Node lemma = nm->mkNode(kind::IMPLIES, args_eq, func_eq);
 269         assertions.push_back(lemma);
 270       }
 271     }
 272   }
 273
 274   // replace applications of UF by skolems (FIXME for model building)
 275   for(unsigned i = 0; i < assertions.size(); ++i) {
 276     assertions[i] = d_funcToSkolem.apply(assertions[i]);
 277   }
 278 }
 279
 280 Node TheoryBV::expandDefinition(LogicRequest &logicRequest, Node node) {
 281   Debug("bitvector-expandDefinition") << "TheoryBV::expandDefinition(" << node << ")" << std::endl;
 282
 283   switch (node.getKind()) {
 284   case kind::BITVECTOR_SDIV:
 285   case kind::BITVECTOR_SREM:
 286   case kind::BITVECTOR_SMOD:
 287     return TheoryBVRewriter::eliminateBVSDiv(node);
 288     break;
 289
 290   case kind::BITVECTOR_UDIV:
 291   case kind::BITVECTOR_UREM: {
 292     NodeManager* nm = NodeManager::currentNM();
 293     unsigned width = node.getType().getBitVectorSize();
 294
 295     if (options::bitvectorDivByZeroConst()) {
 296       Kind kind = node.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_UDIV_TOTAL : kind::BITVECTOR_UREM_TOTAL;
 297       return nm->mkNode(kind, node[0], node[1]);
 298     }
 299
 300     TNode num = node[0], den = node[1];
 301     Node den_eq_0 = nm->mkNode(kind::EQUAL, den, utils::mkZero(width));
 302     Node divTotalNumDen = nm->mkNode(node.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_UDIV_TOTAL :
 303                                      kind::BITVECTOR_UREM_TOTAL, num, den);
 304
 305     // if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
 306     //   // Ackermanize UF if using eager bit-blasting
 307     //   Node ackerman_var = nm->mkNode(node.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_ACKERMANIZE_UDIV : kind::BITVECTOR_ACKERMANIZE_UREM, num);
 308     //   node = nm->mkNode(kind::ITE, den_eq_0, ackerman_var, divTotalNumDen);
 309     //   return node;
 310     // } else {
 311       Node divByZero = getBVDivByZero(node.getKind(), width);
 312       Node divByZeroNum = nm->mkNode(kind::APPLY_UF, divByZero, num);
 313       node = nm->mkNode(kind::ITE, den_eq_0, divByZeroNum, divTotalNumDen);
 314       logicRequest.widenLogic(THEORY_UF);
 315       return node;
 316       //}
 317   }
 318     break;
 319
 320   default:
 321     return node;
 322     break;
 323   }
 324
 325   Unreachable();
 326 }
 327
 328
 329 void TheoryBV::preRegisterTerm(TNode node) {
 330   d_calledPreregister = true;
 331   Debug("bitvector-preregister") << "TheoryBV::preRegister(" << node << ")" << std::endl;
 332
 333   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
 334     // the aig bit-blaster option is set heuristically
 335     // if bv abstraction is not used
 336     if (!d_eagerSolver->isInitialized()) {
 337       d_eagerSolver->initialize();
 338     }
 339
 340     if (node.getKind() == kind::BITVECTOR_EAGER_ATOM) {
 341       Node formula = node[0];
 342       d_eagerSolver->assertFormula(formula);
 343     }
 344     // nothing to do for the other terms
 345     return;
 346   }
 347
 348   for (unsigned i = 0; i < d_subtheories.size(); ++i) {
 349     d_subtheories[i]->preRegister(node);
 350   }
 351
 352   // AJR : equality solver currently registers all terms to ExtTheory, if we want a lazy reduction without the bv equality solver, need to call this
 353   //getExtTheory()->registerTermRec( node );
 354 }
 355
 356 void TheoryBV::sendConflict() {
 357   Assert(d_conflict);
 358   if (d_conflictNode.isNull()) {
 359     return;
 360   } else {
 361     Debug("bitvector") << indent() << "TheoryBV::check(): conflict " << d_conflictNode << std::endl;
 362     d_out->conflict(d_conflictNode);
 363     d_statistics.d_avgConflictSize.addEntry(d_conflictNode.getNumChildren());
 364     d_conflictNode = Node::null();
 365   }
 366 }
 367
 368 void TheoryBV::checkForLemma(TNode fact)
 369 {
 370   if (fact.getKind() == kind::EQUAL)
 371   {
 372     NodeManager* nm = NodeManager::currentNM();
 373     if (fact[0].getKind() == kind::BITVECTOR_UREM_TOTAL)
 374     {
 375       TNode urem = fact[0];
 376       TNode result = fact[1];
 377       TNode divisor = urem[1];
 378       Node result_ult_div = nm->mkNode(kind::BITVECTOR_ULT, result, divisor);
 379       Node divisor_eq_0 =
 380           nm->mkNode(kind::EQUAL, divisor, mkZero(getSize(divisor)));
 381       Node split = nm->mkNode(
 382           kind::OR, divisor_eq_0, nm->mkNode(kind::NOT, fact), result_ult_div);
 383       lemma(split);
 384     }
 385     if (fact[1].getKind() == kind::BITVECTOR_UREM_TOTAL)
 386     {
 387       TNode urem = fact[1];
 388       TNode result = fact[0];
 389       TNode divisor = urem[1];
 390       Node result_ult_div = nm->mkNode(kind::BITVECTOR_ULT, result, divisor);
 391       Node divisor_eq_0 =
 392           nm->mkNode(kind::EQUAL, divisor, mkZero(getSize(divisor)));
 393       Node split = nm->mkNode(
 394           kind::OR, divisor_eq_0, nm->mkNode(kind::NOT, fact), result_ult_div);
 395       lemma(split);
 396     }
 397   }
 398 }
 399
 400 void TheoryBV::check(Effort e)
 401 {
 402   if (done() && e<Theory::EFFORT_FULL) {
 403     return;
 404   }
 405
 406   //last call : do reductions on extended bitvector functions
 407   if (e == Theory::EFFORT_LAST_CALL) {
 408     std::vector<Node> nred = getExtTheory()->getActive();
 409     doExtfReductions(nred);
 410     return;
 411   }
 412
 413   TimerStat::CodeTimer checkTimer(d_checkTime);
 414   Debug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl;
 415   TimerStat::CodeTimer codeTimer(d_statistics.d_solveTimer);
 416   // we may be getting new assertions so the model cache may not be sound
 417   d_invalidateModelCache.set(true);
 418   // if we are using the eager solver
 419   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
 420     // this can only happen on an empty benchmark
 421     if (!d_eagerSolver->isInitialized()) {
 422       d_eagerSolver->initialize();
 423     }
 424     if (!Theory::fullEffort(e))
 425       return;
 426
 427     std::vector<TNode> assertions;
 428     while (!done()) {
 429       TNode fact = get().assertion;
 430       Assert (fact.getKind() == kind::BITVECTOR_EAGER_ATOM);
 431       assertions.push_back(fact);
 432     }
 433     Assert (d_eagerSolver->hasAssertions(assertions));
 434
 435     bool ok = d_eagerSolver->checkSat();
 436     if (!ok) {
 437       if (assertions.size() == 1) {
 438         d_out->conflict(assertions[0]);
 439         return;
 440       }
 441       Node conflict = utils::mkAnd(assertions);
 442       d_out->conflict(conflict);
 443       return;
 444     }
 445     return;
 446   }
 447
 448
 449   if (Theory::fullEffort(e)) {
 450     ++(d_statistics.d_numCallsToCheckFullEffort);
 451   } else {
 452     ++(d_statistics.d_numCallsToCheckStandardEffort);
 453   }
 454   // if we are already in conflict just return the conflict
 455   if (inConflict()) {
 456     sendConflict();
 457     return;
 458   }
 459
 460   while (!done()) {
 461     TNode fact = get().assertion;
 462
 463     checkForLemma(fact);
 464
 465     for (unsigned i = 0; i < d_subtheories.size(); ++i) {
 466       d_subtheories[i]->assertFact(fact);
 467     }
 468   }
 469
 470   bool ok = true;
 471   bool complete = false;
 472   for (unsigned i = 0; i < d_subtheories.size(); ++i) {
 473     Assert (!inConflict());
 474     ok = d_subtheories[i]->check(e);
 475     complete = d_subtheories[i]->isComplete();
 476
 477     if (!ok) {
 478       // if we are in a conflict no need to check with other theories
 479       Assert (inConflict());
 480       sendConflict();
 481       return;
 482     }
 483     if (complete) {
 484       // if the last subtheory was complete we stop
 485       break;
 486     }
 487   }
 488
 489   //check extended functions
 490   if (Theory::fullEffort(e)) {
 491     //do inferences (adds external lemmas)  TODO: this can be improved to add internal inferences
 492     std::vector< Node > nred;
 493     if( getExtTheory()->doInferences( 0, nred ) ){
 494       return;
 495     }
 496     d_needsLastCallCheck = false;
 497     if( !nred.empty() ){
 498       //other inferences involving bv2nat, int2bv
 499       if( options::bvAlgExtf() ){
 500         if( doExtfInferences( nred ) ){
 501           return;
 502         }
 503       }
 504       if( !options::bvLazyReduceExtf() ){
 505         if( doExtfReductions( nred ) ){
 506           return;
 507         }
 508       }else{
 509         d_needsLastCallCheck = true;
 510       }
 511     }
 512   }
 513 }
 514
 515 bool TheoryBV::doExtfInferences(std::vector<Node>& terms)
 516 {
 517   NodeManager* nm = NodeManager::currentNM();
 518   bool sentLemma = false;
 519   eq::EqualityEngine* ee = getEqualityEngine();
 520   std::map<Node, Node> op_map;
 521   for (unsigned j = 0; j < terms.size(); j++)
 522   {
 523     TNode n = terms[j];
 524     Assert(n.getKind() == kind::BITVECTOR_TO_NAT
 525            || n.getKind() == kind::INT_TO_BITVECTOR);
 526     if (n.getKind() == kind::BITVECTOR_TO_NAT)
 527     {
 528       // range lemmas
 529       if (d_extf_range_infer.find(n) == d_extf_range_infer.end())
 530       {
 531         d_extf_range_infer.insert(n);
 532         unsigned bvs = n[0].getType().getBitVectorSize();
 533         Node min = nm->mkConst(Rational(0));
 534         Node max = nm->mkConst(Rational(Integer(1).multiplyByPow2(bvs)));
 535         Node lem = nm->mkNode(kind::AND,
 536                               nm->mkNode(kind::GEQ, n, min),
 537                               nm->mkNode(kind::LT, n, max));
 538         Trace("bv-extf-lemma")
 539             << "BV extf lemma (range) : " << lem << std::endl;
 540         d_out->lemma(lem);
 541         sentLemma = true;
 542       }
 543     }
 544     Node r = (ee && ee->hasTerm(n[0])) ? ee->getRepresentative(n[0]) : n[0];
 545     op_map[r] = n;
 546   }
 547   for (unsigned j = 0; j < terms.size(); j++)
 548   {
 549     TNode n = terms[j];
 550     Node r = (ee && ee->hasTerm(n[0])) ? ee->getRepresentative(n) : n;
 551     std::map<Node, Node>::iterator it = op_map.find(r);
 552     if (it != op_map.end())
 553     {
 554       Node parent = it->second;
 555       // Node cterm = parent[0]==n ? parent : nm->mkNode( parent.getOperator(),
 556       // n );
 557       Node cterm = parent[0].eqNode(n);
 558       Trace("bv-extf-lemma-debug")
 559           << "BV extf collapse based on : " << cterm << std::endl;
 560       if (d_extf_collapse_infer.find(cterm) == d_extf_collapse_infer.end())
 561       {
 562         d_extf_collapse_infer.insert(cterm);
 563
 564         Node t = n[0];
 565         if (n.getKind() == kind::INT_TO_BITVECTOR)
 566         {
 567           Assert(t.getType().isInteger());
 568           // congruent modulo 2^( bv width )
 569           unsigned bvs = n.getType().getBitVectorSize();
 570           Node coeff = nm->mkConst(Rational(Integer(1).multiplyByPow2(bvs)));
 571           Node k = nm->mkSkolem(
 572               "int_bv_cong", t.getType(), "for int2bv/bv2nat congruence");
 573           t = nm->mkNode(kind::PLUS, t, nm->mkNode(kind::MULT, coeff, k));
 574         }
 575         Node lem = parent.eqNode(t);
 576
 577         if (parent[0] != n)
 578         {
 579           Assert(ee->areEqual(parent[0], n));
 580           lem = nm->mkNode(kind::IMPLIES, parent[0].eqNode(n), lem);
 581         }
 582         Trace("bv-extf-lemma")
 583             << "BV extf lemma (collapse) : " << lem << std::endl;
 584         d_out->lemma(lem);
 585         sentLemma = true;
 586       }
 587     }
 588   }
 589   return sentLemma;
 590 }
 591
 592 bool TheoryBV::doExtfReductions( std::vector< Node >& terms ) {
 593   std::vector< Node > nredr;
 594   if( getExtTheory()->doReductions( 0, terms, nredr ) ){
 595     return true;
 596   }
 597   Assert( nredr.empty() );
 598   return false;
 599 }
 600
 601 bool TheoryBV::needsCheckLastEffort() {
 602   return d_needsLastCallCheck;
 603 }
 604 bool TheoryBV::collectModelInfo(TheoryModel* m)
 605 {
 606   Assert(!inConflict());
 607   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
 608     if (!d_eagerSolver->collectModelInfo(m, true))
 609     {
 610       return false;
 611     }
 612   }
 613   for (unsigned i = 0; i < d_subtheories.size(); ++i) {
 614     if (d_subtheories[i]->isComplete()) {
 615       return d_subtheories[i]->collectModelInfo(m, true);
 616     }
 617   }
 618   return true;
 619 }
 620
 621 Node TheoryBV::getModelValue(TNode var) {
 622   Assert(!inConflict());
 623   for (unsigned i = 0; i < d_subtheories.size(); ++i) {
 624     if (d_subtheories[i]->isComplete()) {
 625       return d_subtheories[i]->getModelValue(var);
 626     }
 627   }
 628   Unreachable();
 629 }
 630
 631 void TheoryBV::propagate(Effort e) {
 632   Debug("bitvector") << indent() << "TheoryBV::propagate()" << std::endl;
 633   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
 634     return;
 635   }
 636
 637   if (inConflict()) {
 638     return;
 639   }
 640
 641   // go through stored propagations
 642   bool ok = true;
 643   for (; d_literalsToPropagateIndex < d_literalsToPropagate.size() && ok; d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) {
 644     TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex];
 645     // temporary fix for incremental bit-blasting
 646     if (d_valuation.isSatLiteral(literal)) {
 647       Debug("bitvector::propagate") << "TheoryBV:: propagating " << literal <<"\n";
 648       ok = d_out->propagate(literal);
 649     }
 650   }
 651
 652   if (!ok) {
 653     Debug("bitvector::propagate") << indent() << "TheoryBV::propagate(): conflict from theory engine" << std::endl;
 654     setConflict();
 655   }
 656 }
 657
 658
 659 eq::EqualityEngine * TheoryBV::getEqualityEngine() {
 660   CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
 661   if( core ){
 662     return core->getEqualityEngine();
 663   }else{
 664     return NULL;
 665   }
 666 }
 667
 668 bool TheoryBV::getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp ) {
 669   eq::EqualityEngine * ee = getEqualityEngine();
 670   if( ee ){
 671     //get the constant equivalence classes
 672     bool retVal = false;
 673     for( unsigned i=0; i<vars.size(); i++ ){
 674       Node n = vars[i];
 675       if( ee->hasTerm( n ) ){
 676         Node nr = ee->getRepresentative( n );
 677         if( nr.isConst() ){
 678           subs.push_back( nr );
 679           exp[n].push_back( n.eqNode( nr ) );
 680           retVal = true;
 681         }else{
 682           subs.push_back( n );
 683         }
 684       }else{
 685         subs.push_back( n );
 686       }
 687     }
 688     //return true if the substitution is non-trivial
 689     return retVal;
 690   }
 691   return false;
 692 }
 693
 694 int TheoryBV::getReduction(int effort, Node n, Node& nr)
 695 {
 696   Trace("bv-ext") << "TheoryBV::checkExt : non-reduced : " << n << std::endl;
 697   NodeManager* const nm = NodeManager::currentNM();
 698   if (n.getKind() == kind::BITVECTOR_TO_NAT)
 699   {
 700     // taken from rewrite code
 701     const unsigned size = utils::getSize(n[0]);
 702     const Node z = nm->mkConst(Rational(0));
 703     const Node bvone = utils::mkOne(1);
 704     NodeBuilder<> result(kind::PLUS);
 705     Integer i = 1;
 706     for (unsigned bit = 0; bit < size; ++bit, i *= 2)
 707     {
 708       Node cond =
 709           nm->mkNode(kind::EQUAL,
 710                      nm->mkNode(nm->mkConst(BitVectorExtract(bit, bit)), n[0]),
 711                      bvone);
 712       result << nm->mkNode(kind::ITE, cond, nm->mkConst(Rational(i)), z);
 713     }
 714     nr = Node(result);
 715     return -1;
 716   }
 717   else if (n.getKind() == kind::INT_TO_BITVECTOR)
 718   {
 719     // taken from rewrite code
 720     const unsigned size = n.getOperator().getConst<IntToBitVector>().size;
 721     const Node bvzero = utils::mkZero(1);
 722     const Node bvone = utils::mkOne(1);
 723     std::vector<Node> v;
 724     Integer i = 2;
 725     while (v.size() < size)
 726     {
 727       Node cond = nm->mkNode(
 728           kind::GEQ,
 729           nm->mkNode(kind::INTS_MODULUS_TOTAL, n[0], nm->mkConst(Rational(i))),
 730           nm->mkConst(Rational(i, 2)));
 731       cond = Rewriter::rewrite(cond);
 732       v.push_back(nm->mkNode(kind::ITE, cond, bvone, bvzero));
 733       i *= 2;
 734     }
 735     NodeBuilder<> result(kind::BITVECTOR_CONCAT);
 736     result.append(v.rbegin(), v.rend());
 737     nr = Node(result);
 738     return -1;
 739   }
 740   return 0;
 741 }
 742
 743 Theory::PPAssertStatus TheoryBV::ppAssert(TNode in,
 744                                           SubstitutionMap& outSubstitutions)
 745 {
 746   switch (in.getKind())
 747   {
 748     case kind::EQUAL:
 749     {
 750       if (in[0].isVar() && !in[1].hasSubterm(in[0]))
 751       {
 752         ++(d_statistics.d_solveSubstitutions);
 753         outSubstitutions.addSubstitution(in[0], in[1]);
 754         return PP_ASSERT_STATUS_SOLVED;
 755       }
 756       if (in[1].isVar() && !in[0].hasSubterm(in[1]))
 757       {
 758         ++(d_statistics.d_solveSubstitutions);
 759         outSubstitutions.addSubstitution(in[1], in[0]);
 760         return PP_ASSERT_STATUS_SOLVED;
 761       }
 762       Node node = Rewriter::rewrite(in);
 763       if ((node[0].getKind() == kind::BITVECTOR_EXTRACT && node[1].isConst())
 764           || (node[1].getKind() == kind::BITVECTOR_EXTRACT
 765               && node[0].isConst()))
 766       {
 767         Node extract = node[0].isConst() ? node[1] : node[0];
 768         if (extract[0].getKind() == kind::VARIABLE)
 769         {
 770           Node c = node[0].isConst() ? node[0] : node[1];
 771
 772           unsigned high = utils::getExtractHigh(extract);
 773           unsigned low = utils::getExtractLow(extract);
 774           unsigned var_bitwidth = utils::getSize(extract[0]);
 775           std::vector<Node> children;
 776
 777           if (low == 0)
 778           {
 779             Assert(high != var_bitwidth - 1);
 780             unsigned skolem_size = var_bitwidth - high - 1;
 781             Node skolem = utils::mkVar(skolem_size);
 782             children.push_back(skolem);
 783             children.push_back(c);
 784           }
 785           else if (high == var_bitwidth - 1)
 786           {
 787             unsigned skolem_size = low;
 788             Node skolem = utils::mkVar(skolem_size);
 789             children.push_back(c);
 790             children.push_back(skolem);
 791           }
 792           else
 793           {
 794             unsigned skolem1_size = low;
 795             unsigned skolem2_size = var_bitwidth - high - 1;
 796             Node skolem1 = utils::mkVar(skolem1_size);
 797             Node skolem2 = utils::mkVar(skolem2_size);
 798             children.push_back(skolem2);
 799             children.push_back(c);
 800             children.push_back(skolem1);
 801           }
 802           Node concat = utils::mkConcat(children);
 803           Assert(utils::getSize(concat) == utils::getSize(extract[0]));
 804           outSubstitutions.addSubstitution(extract[0], concat);
 805           return PP_ASSERT_STATUS_SOLVED;
 806         }
 807       }
 808     }
 809     break;
 810     case kind::BITVECTOR_ULT:
 811     case kind::BITVECTOR_SLT:
 812     case kind::BITVECTOR_ULE:
 813     case kind::BITVECTOR_SLE:
 814
 815     default:
 816       // TODO other predicates
 817       break;
 818   }
 819   return PP_ASSERT_STATUS_UNSOLVED;
 820 }
 821
 822 Node TheoryBV::ppRewrite(TNode t)
 823 {
 824   Debug("bv-pp-rewrite") << "TheoryBV::ppRewrite " << t << "\n";
 825   Node res = t;
 826   if (RewriteRule<BitwiseEq>::applies(t)) {
 827     Node result = RewriteRule<BitwiseEq>::run<false>(t);
 828     res = Rewriter::rewrite(result);
 829   } else if (d_isCoreTheory && t.getKind() == kind::EQUAL) {
 830     std::vector<Node> equalities;
 831     Slicer::splitEqualities(t, equalities);
 832     res = utils::mkAnd(equalities);
 833   } else if (RewriteRule<UltPlusOne>::applies(t)) {
 834     Node result = RewriteRule<UltPlusOne>::run<false>(t);
 835     res = Rewriter::rewrite(result);
 836   } else if( res.getKind() == kind::EQUAL &&
 837       ((res[0].getKind() == kind::BITVECTOR_PLUS &&
 838         RewriteRule<ConcatToMult>::applies(res[1])) ||
 839        (res[1].getKind() == kind::BITVECTOR_PLUS &&
 840         RewriteRule<ConcatToMult>::applies(res[0])))) {
 841     Node mult = RewriteRule<ConcatToMult>::applies(res[0])?
 842       RewriteRule<ConcatToMult>::run<false>(res[0]) :
 843       RewriteRule<ConcatToMult>::run<true>(res[1]);
 844     Node factor = mult[0];
 845     Node sum =  RewriteRule<ConcatToMult>::applies(res[0])? res[1] : res[0];
 846     Node new_eq = NodeManager::currentNM()->mkNode(kind::EQUAL, sum, mult);
 847     Node rewr_eq = RewriteRule<SolveEq>::run<true>(new_eq);
 848     if (rewr_eq[0].isVar() || rewr_eq[1].isVar()){
 849       res = Rewriter::rewrite(rewr_eq);
 850     } else {
 851       res = t;
 852     }
 853   } else if (RewriteRule<SignExtendEqConst>::applies(t)) {
 854     res = RewriteRule<SignExtendEqConst>::run<false>(t);
 855   } else if (RewriteRule<ZeroExtendEqConst>::applies(t)) {
 856     res = RewriteRule<ZeroExtendEqConst>::run<false>(t);
 857   }
 858
 859   // if(t.getKind() == kind::EQUAL &&
 860   //    ((t[0].getKind() == kind::BITVECTOR_MULT && t[1].getKind() ==
 861   //    kind::BITVECTOR_PLUS) ||
 862   //     (t[1].getKind() == kind::BITVECTOR_MULT && t[0].getKind() ==
 863   //     kind::BITVECTOR_PLUS))) {
 864   //   // if we have an equality between a multiplication and addition
 865   //   // try to express multiplication in terms of addition
 866   //   Node mult = t[0].getKind() == kind::BITVECTOR_MULT? t[0] : t[1];
 867   //   Node add = t[0].getKind() == kind::BITVECTOR_PLUS? t[0] : t[1];
 868   //   if (RewriteRule<MultSlice>::applies(mult)) {
 869   //     Node new_mult = RewriteRule<MultSlice>::run<false>(mult);
 870   //     Node new_eq =
 871   //     Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::EQUAL,
 872   //     new_mult, add));
 873
 874   //     // the simplification can cause the formula to blow up
 875   //     // only apply if formula reduced
 876   //     if (d_subtheoryMap.find(SUB_BITBLAST) != d_subtheoryMap.end()) {
 877   //       BitblastSolver* bv = (BitblastSolver*)d_subtheoryMap[SUB_BITBLAST];
 878   //       uint64_t old_size = bv->computeAtomWeight(t);
 879   //       Assert (old_size);
 880   //       uint64_t new_size = bv->computeAtomWeight(new_eq);
 881   //       double ratio = ((double)new_size)/old_size;
 882   //       if (ratio <= 0.4) {
 883   //         ++(d_statistics.d_numMultSlice);
 884   //         return new_eq;
 885   //       }
 886   //     }
 887
 888   //     if (new_eq.getKind() == kind::CONST_BOOLEAN) {
 889   //       ++(d_statistics.d_numMultSlice);
 890   //       return new_eq;
 891   //     }
 892   //   }
 893   // }
 894
 895   if (options::bvAbstraction() && t.getType().isBoolean()) {
 896     d_abstractionModule->addInputAtom(res);
 897   }
 898   Debug("bv-pp-rewrite") << "to   " << res << "\n";
 899   return res;
 900 }
 901
 902 void TheoryBV::presolve() {
 903   Debug("bitvector") << "TheoryBV::presolve" << endl;
 904 }
 905
 906 static int prop_count = 0;
 907
 908 bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory)
 909 {
 910   Debug("bitvector::propagate") << indent() << getSatContext()->getLevel() << " " << "TheoryBV::storePropagation(" << literal << ", " << subtheory << ")" << std::endl;
 911   prop_count++;
 912
 913   // If already in conflict, no more propagation
 914   if (d_conflict) {
 915     Debug("bitvector::propagate") << indent() << "TheoryBV::storePropagation(" << literal << ", " << subtheory << "): already in conflict" << std::endl;
 916     return false;
 917   }
 918
 919   // If propagated already, just skip
 920   PropagatedMap::const_iterator find = d_propagatedBy.find(literal);
 921   if (find != d_propagatedBy.end()) {
 922     return true;
 923   } else {
 924     bool polarity = literal.getKind() != kind::NOT;
 925     Node negatedLiteral = polarity ? literal.notNode() : (Node) literal[0];
 926     find = d_propagatedBy.find(negatedLiteral);
 927     if (find != d_propagatedBy.end() && (*find).second != subtheory) {
 928       // Safe to ignore this one, subtheory should produce a conflict
 929       return true;
 930     }
 931
 932     d_propagatedBy[literal] = subtheory;
 933   }
 934
 935   // Propagate differs depending on the subtheory
 936   // * bitblaster needs to be left alone until it's done, otherwise it doesn't know how to explain
 937   // * equality engine can propagate eagerly
 938   bool ok = true;
 939   if (subtheory == SUB_CORE) {
 940     d_out->propagate(literal);
 941     if (!ok) {
 942       setConflict();
 943     }
 944   } else {
 945     d_literalsToPropagate.push_back(literal);
 946   }
 947   return ok;
 948
 949 }/* TheoryBV::propagate(TNode) */
 950
 951
 952 void TheoryBV::explain(TNode literal, std::vector<TNode>& assumptions) {
 953   Assert (wasPropagatedBySubtheory(literal));
 954   SubTheory sub = getPropagatingSubtheory(literal);
 955   d_subtheoryMap[sub]->explain(literal, assumptions);
 956 }
 957
 958
 959 Node TheoryBV::explain(TNode node) {
 960   Debug("bitvector::explain") << "TheoryBV::explain(" << node << ")" << std::endl;
 961   std::vector<TNode> assumptions;
 962
 963   // Ask for the explanation
 964   explain(node, assumptions);
 965   // this means that it is something true at level 0
 966   if (assumptions.size() == 0) {
 967     return utils::mkTrue();
 968   }
 969   // return the explanation
 970   Node explanation = utils::mkAnd(assumptions);
 971   Debug("bitvector::explain") << "TheoryBV::explain(" << node << ") => " << explanation << std::endl;
 972   Debug("bitvector::explain") << "TheoryBV::explain done. \n";
 973   return explanation;
 974 }
 975
 976
 977 void TheoryBV::addSharedTerm(TNode t) {
 978   Debug("bitvector::sharing") << indent() << "TheoryBV::addSharedTerm(" << t << ")" << std::endl;
 979   d_sharedTermsSet.insert(t);
 980   if (options::bitvectorEqualitySolver()) {
 981     for (unsigned i = 0; i < d_subtheories.size(); ++i) {
 982       d_subtheories[i]->addSharedTerm(t);
 983     }
 984   }
 985 }
 986
 987
 988 EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b)
 989 {
 990   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER)
 991     return EQUALITY_UNKNOWN;
 992   Assert (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY);
 993   for (unsigned i = 0; i < d_subtheories.size(); ++i) {
 994     EqualityStatus status = d_subtheories[i]->getEqualityStatus(a, b);
 995     if (status != EQUALITY_UNKNOWN) {
 996       return status;
 997     }
 998   }
 999   return EQUALITY_UNKNOWN; ;
1000 }
1001
1002
1003 void TheoryBV::enableCoreTheorySlicer() {
1004   Assert (!d_calledPreregister);
1005   d_isCoreTheory = true;
1006   if (d_subtheoryMap.find(SUB_CORE) != d_subtheoryMap.end()) {
1007     CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
1008     core->enableSlicer();
1009   }
1010 }
1011
1012
1013 void TheoryBV::ppStaticLearn(TNode in, NodeBuilder<>& learned) {
1014   if(d_staticLearnCache.find(in) != d_staticLearnCache.end()){
1015     return;
1016   }
1017   d_staticLearnCache.insert(in);
1018
1019   if (in.getKind() == kind::EQUAL) {
1020     if((in[0].getKind() == kind::BITVECTOR_PLUS && in[1].getKind() == kind::BITVECTOR_SHL) ||
1021        (in[1].getKind() == kind::BITVECTOR_PLUS && in[0].getKind() == kind::BITVECTOR_SHL)) {
1022       TNode p = in[0].getKind() == kind::BITVECTOR_PLUS ? in[0] : in[1];
1023       TNode s = in[0].getKind() == kind::BITVECTOR_PLUS ? in[1] : in[0];
1024
1025       if(p.getNumChildren() == 2
1026          && p[0].getKind()  == kind::BITVECTOR_SHL
1027          && p[1].getKind()  == kind::BITVECTOR_SHL ){
1028         unsigned size = utils::getSize(s);
1029         Node one = utils::mkConst(size, 1u);
1030         if(s[0] == one && p[0][0] == one && p[1][0] == one){
1031           Node zero = utils::mkConst(size, 0u);
1032           TNode b = p[0];
1033           TNode c = p[1];
1034           // (s : 1 << S) = (b : 1 << B) + (c : 1 << C)
1035           Node b_eq_0 = b.eqNode(zero);
1036           Node c_eq_0 = c.eqNode(zero);
1037           Node b_eq_c = b.eqNode(c);
1038
1039           Node dis = NodeManager::currentNM()->mkNode(
1040               kind::OR, b_eq_0, c_eq_0, b_eq_c);
1041           Node imp = in.impNode(dis);
1042           learned << imp;
1043         }
1044       }
1045     }
1046   }else if(in.getKind() == kind::AND){
1047     for(size_t i = 0, N = in.getNumChildren(); i < N; ++i){
1048       ppStaticLearn(in[i], learned);
1049     }
1050   }
1051 }
1052
1053 bool TheoryBV::applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions) {
1054   bool changed = d_abstractionModule->applyAbstraction(assertions, new_assertions);
1055   if (changed &&
1056       options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER &&
1057       options::bitvectorAig()) {
1058     // disable AIG mode
1059     AlwaysAssert (!d_eagerSolver->isInitialized());
1060     d_eagerSolver->turnOffAig();
1061     d_eagerSolver->initialize();
1062   }
1063   return changed;
1064 }
1065
1066 void TheoryBV::setProofLog( BitVectorProof * bvp ) {
1067   if( options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER ){
1068     d_eagerSolver->setProofLog( bvp );
1069   }else{
1070     for( unsigned i=0; i< d_subtheories.size(); i++ ){
1071       d_subtheories[i]->setProofLog( bvp );
1072     }
1073   }
1074 }
1075
1076 void TheoryBV::setConflict(Node conflict)
1077 {
1078   if (options::bvAbstraction())
1079   {
1080     NodeManager* const nm = NodeManager::currentNM();
1081     Node new_conflict = d_abstractionModule->simplifyConflict(conflict);
1082
1083     std::vector<Node> lemmas;
1084     lemmas.push_back(new_conflict);
1085     d_abstractionModule->generalizeConflict(new_conflict, lemmas);
1086     for (unsigned i = 0; i < lemmas.size(); ++i)
1087     {
1088       lemma(nm->mkNode(kind::NOT, lemmas[i]));
1089     }
1090   }
1091   d_conflict = true;
1092   d_conflictNode = conflict;
1093 }
1094
1095 } /* namespace CVC4::theory::bv */
1096 } /* namespace CVC4::theory */
1097 } /* namespace CVC4 */