src/theory/bv/bv_subtheory_algebraic.cpp

   1 /*********************                                                        */
   2 /*! \file bv_subtheory_algebraic.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Liana Hadarean, Aina Niemetz, Tim King
   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  ** \brief Algebraic solver.
  13  **
  14  ** Algebraic solver.
  15  **/
  16 #include "theory/bv/bv_subtheory_algebraic.h"
  17
  18 #include <unordered_set>
  19
  20 #include "expr/node_algorithm.h"
  21 #include "options/bv_options.h"
  22 #include "smt/smt_statistics_registry.h"
  23 #include "smt_util/boolean_simplification.h"
  24 #include "theory/bv/bv_quick_check.h"
  25 #include "theory/bv/theory_bv.h"
  26 #include "theory/bv/theory_bv_utils.h"
  27 #include "theory/theory_model.h"
  28
  29 using namespace CVC4::context;
  30 using namespace CVC4::prop;
  31 using namespace CVC4::theory::bv::utils;
  32 using namespace std;
  33
  34 namespace CVC4 {
  35 namespace theory {
  36 namespace bv {
  37
  38 /* ------------------------------------------------------------------------- */
  39
  40 namespace {
  41
  42 /* Collect all variables under a given a node.  */
  43 void collectVariables(TNode node, utils::NodeSet& vars)
  44 {
  45   std::vector<TNode> stack;
  46   std::unordered_set<TNode, TNodeHashFunction> visited;
  47
  48   stack.push_back(node);
  49   while (!stack.empty())
  50   {
  51     Node n = stack.back();
  52     stack.pop_back();
  53
  54     if (vars.find(n) != vars.end()) continue;
  55     if (visited.find(n) != visited.end()) continue;
  56     visited.insert(n);
  57
  58     if (Theory::isLeafOf(n, THEORY_BV) && n.getKind() != kind::CONST_BITVECTOR)
  59     {
  60       vars.insert(n);
  61       continue;
  62     }
  63     stack.insert(stack.end(), n.begin(), n.end());
  64   }
  65 }
  66
  67 };
  68
  69 /* ------------------------------------------------------------------------- */
  70
  71 bool hasExpensiveBVOperators(TNode fact);
  72 Node mergeExplanations(const std::vector<Node>& expls);
  73 Node mergeExplanations(TNode expl1, TNode expl2);
  74
  75
  76 SubstitutionEx::SubstitutionEx(theory::SubstitutionMap* modelMap)
  77   : d_substitutions()
  78   , d_cache()
  79   , d_cacheInvalid(true)
  80   , d_modelMap(modelMap)
  81 {}
  82
  83 bool SubstitutionEx::addSubstitution(TNode from, TNode to, TNode reason) {
  84   Debug("bv-substitution") << "SubstitutionEx::addSubstitution: "<< from
  85                            <<" => "<< to << "\n" << " reason "<<reason << "\n";
  86   Assert (from != to);
  87   if (d_substitutions.find(from) != d_substitutions.end()) {
  88     return false;
  89   }
  90
  91   d_modelMap->addSubstitution(from, to);
  92
  93   d_cacheInvalid = true;
  94   d_substitutions[from] = SubstitutionElement(to, reason);
  95   return true;
  96 }
  97
  98 Node SubstitutionEx::apply(TNode node) {
  99   Debug("bv-substitution") << "SubstitutionEx::apply("<< node <<")\n";
 100   if (d_cacheInvalid) {
 101     d_cache.clear();
 102     d_cacheInvalid = false;
 103   }
 104
 105   SubstitutionsCache::iterator it = d_cache.find(node);
 106
 107   if (it != d_cache.end()) {
 108     Node res = it->second.to;
 109     Debug("bv-substitution") << "   =>"<< res <<"\n";
 110     return res;
 111   }
 112
 113   Node result = internalApply(node);
 114   Debug("bv-substitution") << "   =>"<< result <<"\n";
 115   return result;
 116 }
 117
 118 Node SubstitutionEx::internalApply(TNode node) {
 119   if (d_substitutions.empty())
 120     return node;
 121
 122   vector<SubstitutionStackElement> stack;
 123   stack.push_back(SubstitutionStackElement(node));
 124
 125   while (!stack.empty()) {
 126     SubstitutionStackElement head = stack.back();
 127     stack.pop_back();
 128
 129     TNode current = head.node;
 130
 131     if (hasCache(current)) {
 132       continue;
 133     }
 134
 135     // check if it has substitution
 136     Substitutions::const_iterator it = d_substitutions.find(current);
 137     if (it != d_substitutions.end()) {
 138       vector<Node> reasons;
 139       TNode to = it->second.to;
 140       reasons.push_back(it->second.reason);
 141       // check if the thing we subsituted to has substitutions
 142       TNode res = internalApply(to);
 143       // update reasons
 144       reasons.push_back(getReason(to));
 145       Node reason = mergeExplanations(reasons);
 146       storeCache(current, res, reason);
 147       continue;
 148     }
 149
 150     // if no children then just continue
 151     if(current.getNumChildren() == 0) {
 152       storeCache(current, current, utils::mkTrue());
 153       continue;
 154     }
 155
 156     // children already processed
 157     if (head.childrenAdded) {
 158       NodeBuilder<> nb(current.getKind());
 159       std::vector<Node> reasons;
 160
 161       if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
 162         TNode op = current.getOperator();
 163         Assert (hasCache(op));
 164         nb << getCache(op);
 165         reasons.push_back(getReason(op));
 166       }
 167       for (unsigned i = 0; i < current.getNumChildren(); ++i) {
 168         Assert (hasCache(current[i]));
 169         nb << getCache(current[i]);
 170         reasons.push_back(getReason(current[i]));
 171       }
 172       Node result = nb;
 173       // if the node is new apply substitutions to it
 174       Node subst_result = result;
 175       if (result != current) {
 176         subst_result = result!= current? internalApply(result) : result;
 177         reasons.push_back(getReason(result));
 178       }
 179       Node reason = mergeExplanations(reasons);
 180       storeCache(current, subst_result, reason);
 181       continue;
 182     } else {
 183       // add children to stack
 184       stack.push_back(SubstitutionStackElement(current, true));
 185       if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
 186         stack.push_back(SubstitutionStackElement(current.getOperator()));
 187       }
 188       for (unsigned i = 0; i < current.getNumChildren(); ++i) {
 189         stack.push_back(SubstitutionStackElement(current[i]));
 190       }
 191     }
 192   }
 193
 194   Assert(hasCache(node));
 195   return getCache(node);
 196 }
 197
 198 Node SubstitutionEx::explain(TNode node) const {
 199   if(!hasCache(node)) {
 200     return utils::mkTrue();
 201   }
 202
 203   Debug("bv-substitution") << "SubstitutionEx::explain("<< node <<")\n";
 204   Node res = getReason(node);
 205   Debug("bv-substitution") << "  with "<< res <<"\n";
 206   return res;
 207 }
 208
 209 Node SubstitutionEx::getReason(TNode node) const {
 210   Assert(hasCache(node));
 211   SubstitutionsCache::const_iterator it = d_cache.find(node);
 212   return it->second.reason;
 213 }
 214
 215 bool SubstitutionEx::hasCache(TNode node) const {
 216   return d_cache.find(node) != d_cache.end();
 217 }
 218
 219 Node SubstitutionEx::getCache(TNode node) const {
 220   Assert (hasCache(node));
 221   return d_cache.find(node)->second.to;
 222 }
 223
 224 void SubstitutionEx::storeCache(TNode from, TNode to, Node reason) {
 225   //  Debug("bv-substitution") << "SubstitutionEx::storeCache(" << from <<", " << to <<", "<< reason<<")\n";
 226   Assert (!hasCache(from));
 227   d_cache[from] = SubstitutionElement(to, reason);
 228 }
 229
 230 AlgebraicSolver::AlgebraicSolver(context::Context* c, TheoryBV* bv)
 231   : SubtheorySolver(c, bv)
 232   , d_modelMap(NULL)
 233   , d_quickSolver(new BVQuickCheck("theory::bv::algebraic", bv))
 234   , d_isComplete(c, false)
 235   , d_isDifficult(c, false)
 236   , d_budget(options::bitvectorAlgebraicBudget())
 237   , d_explanations()
 238   , d_inputAssertions()
 239   , d_ids()
 240   , d_numSolved(0)
 241   , d_numCalls(0)
 242   , d_ctx(new context::Context())
 243   , d_quickXplain(options::bitvectorQuickXplain() ? new QuickXPlain("theory::bv::algebraic", d_quickSolver) : NULL)
 244   , d_statistics()
 245 {}
 246
 247 AlgebraicSolver::~AlgebraicSolver() {
 248   if(d_modelMap != NULL) { delete d_modelMap; }
 249   delete d_quickXplain;
 250   delete d_quickSolver;
 251   delete d_ctx;
 252 }
 253
 254
 255
 256 bool AlgebraicSolver::check(Theory::Effort e)
 257 {
 258   Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY);
 259
 260   if (!Theory::fullEffort(e)) { return true; }
 261   if (!useHeuristic()) { return true; }
 262
 263   TimerStat::CodeTimer algebraicTimer(d_statistics.d_solveTime);
 264   Debug("bv-subtheory-algebraic") << "AlgebraicSolver::check (" << e << ")\n";
 265   ++(d_numCalls);
 266   ++(d_statistics.d_numCallstoCheck);
 267
 268   d_explanations.clear();
 269   d_ids.clear();
 270   d_inputAssertions.clear();
 271
 272   std::vector<WorklistElement> worklist;
 273
 274   uint64_t original_bb_cost = 0;
 275
 276   NodeManager* nm = NodeManager::currentNM();
 277   NodeSet seen_assertions;
 278   // Processing assertions from scratch
 279   for (AssertionQueue::const_iterator it = assertionsBegin(); it != assertionsEnd(); ++it) {
 280     Debug("bv-subtheory-algebraic") << "   " << *it << "\n";
 281     TNode assertion = *it;
 282     unsigned id = worklist.size();
 283     d_ids[assertion] = id;
 284     worklist.push_back(WorklistElement(assertion, id));
 285     d_inputAssertions.insert(assertion);
 286     storeExplanation(assertion);
 287
 288     uint64_t assertion_size = d_quickSolver->computeAtomWeight(assertion, seen_assertions);
 289     Assert (original_bb_cost <= original_bb_cost + assertion_size);
 290     original_bb_cost+= assertion_size;
 291   }
 292
 293   for (unsigned i = 0; i < worklist.size(); ++i) {
 294     d_ids[worklist[i].node] = worklist[i].id;
 295   }
 296
 297   Debug("bv-subtheory-algebraic") << "Assertions " << worklist.size() <<" : \n";
 298
 299   Assert (d_explanations.size() == worklist.size());
 300
 301   delete d_modelMap;
 302   d_modelMap = new SubstitutionMap(d_context);
 303   SubstitutionEx subst(d_modelMap);
 304
 305   // first round of substitutions
 306   processAssertions(worklist, subst);
 307
 308   if (!d_isDifficult.get()) {
 309     // skolemize all possible extracts
 310     ExtractSkolemizer skolemizer(d_modelMap);
 311     skolemizer.skolemize(worklist);
 312     // second round of substitutions
 313     processAssertions(worklist, subst);
 314   }
 315
 316   NodeSet subst_seen;
 317   uint64_t subst_bb_cost = 0;
 318
 319   unsigned r = 0;
 320   unsigned w = 0;
 321
 322   for (; r < worklist.size(); ++r) {
 323
 324     TNode fact = worklist[r].node;
 325     unsigned id = worklist[r].id;
 326
 327     if (Dump.isOn("bv-algebraic")) {
 328       Node expl = d_explanations[id];
 329       Node query = utils::mkNot(nm->mkNode(kind::IMPLIES, expl, fact));
 330       Dump("bv-algebraic") << EchoCommand("ThoeryBV::AlgebraicSolver::substitution explanation");
 331       Dump("bv-algebraic") << PushCommand();
 332       Dump("bv-algebraic") << AssertCommand(query.toExpr());
 333       Dump("bv-algebraic") << CheckSatCommand();
 334       Dump("bv-algebraic") << PopCommand();
 335     }
 336
 337     if (fact.isConst() &&
 338         fact.getConst<bool>() == true) {
 339       continue;
 340     }
 341
 342     if (fact.isConst() &&
 343         fact.getConst<bool>() == false) {
 344       // we have a conflict
 345       Node conflict = BooleanSimplification::simplify(d_explanations[id]);
 346       d_bv->setConflict(conflict);
 347       d_isComplete.set(true);
 348       Debug("bv-subtheory-algebraic") << " UNSAT: assertion simplfies to false with conflict: "<< conflict << "\n";
 349
 350       if (Dump.isOn("bv-algebraic")) {
 351         Dump("bv-algebraic") << EchoCommand("TheoryBV::AlgebraicSolver::conflict");
 352         Dump("bv-algebraic") << PushCommand();
 353         Dump("bv-algebraic") << AssertCommand(conflict.toExpr());
 354         Dump("bv-algebraic") << CheckSatCommand();
 355         Dump("bv-algebraic") << PopCommand();
 356       }
 357
 358
 359       ++(d_statistics.d_numSimplifiesToFalse);
 360       ++(d_numSolved);
 361       return false;
 362     }
 363
 364     subst_bb_cost+= d_quickSolver->computeAtomWeight(fact, subst_seen);
 365     worklist[w] = WorklistElement(fact, id);
 366     Node expl =  BooleanSimplification::simplify(d_explanations[id]);
 367     storeExplanation(id, expl);
 368     d_ids[fact] = id;
 369     ++w;
 370   }
 371
 372   worklist.resize(w);
 373
 374
 375   if(Debug.isOn("bv-subtheory-algebraic")) {
 376     Debug("bv-subtheory-algebraic") << "Assertions post-substitutions " << worklist.size() << ":\n";
 377     for (unsigned i = 0; i < worklist.size(); ++i) {
 378       Debug("bv-subtheory-algebraic") << "   " << worklist[i].node << "\n";
 379     }
 380   }
 381
 382
 383   // all facts solved to true
 384   if (worklist.empty()) {
 385     Debug("bv-subtheory-algebraic") << " SAT: everything simplifies to true.\n";
 386     ++(d_statistics.d_numSimplifiesToTrue);
 387     ++(d_numSolved);
 388     return true;
 389   }
 390
 391   double ratio = ((double)subst_bb_cost)/original_bb_cost;
 392   if (ratio > 0.5 ||
 393       !d_isDifficult.get()) {
 394     // give up if problem not reduced enough
 395     d_isComplete.set(false);
 396     return true;
 397   }
 398
 399   d_quickSolver->clearSolver();
 400
 401   d_quickSolver->push();
 402   std::vector<Node> facts;
 403   for (unsigned i = 0; i < worklist.size(); ++i) {
 404     facts.push_back(worklist[i].node);
 405   }
 406   bool ok = quickCheck(facts);
 407
 408   Debug("bv-subtheory-algebraic") << "AlgebraicSolver::check done " << ok << ".\n";
 409   return ok;
 410 }
 411
 412 bool AlgebraicSolver::quickCheck(std::vector<Node>& facts) {
 413   SatValue res = d_quickSolver->checkSat(facts, d_budget);
 414
 415   if (res == SAT_VALUE_UNKNOWN) {
 416     d_isComplete.set(false);
 417     Debug("bv-subtheory-algebraic") << " Unknown.\n";
 418     ++(d_statistics.d_numUnknown);
 419     return true;
 420   }
 421
 422   if (res == SAT_VALUE_TRUE) {
 423     Debug("bv-subtheory-algebraic") << " Sat.\n";
 424     ++(d_statistics.d_numSat);
 425     ++(d_numSolved);
 426     d_isComplete.set(true);
 427     return true;
 428   }
 429
 430   Assert (res == SAT_VALUE_FALSE);
 431   Assert (d_quickSolver->inConflict());
 432   d_isComplete.set(true);
 433   Debug("bv-subtheory-algebraic") << " Unsat.\n";
 434   ++(d_numSolved);
 435   ++(d_statistics.d_numUnsat);
 436
 437
 438   Node conflict = d_quickSolver->getConflict();
 439   Debug("bv-subtheory-algebraic") << " Conflict: " << conflict << "\n";
 440
 441   // singleton conflict
 442   if (conflict.getKind() != kind::AND) {
 443     Assert (d_ids.find(conflict) != d_ids.end());
 444     unsigned id = d_ids[conflict];
 445     Assert (id < d_explanations.size());
 446     Node theory_confl = d_explanations[id];
 447     d_bv->setConflict(theory_confl);
 448     return false;
 449   }
 450
 451   Assert (conflict.getKind() == kind::AND);
 452   if (options::bitvectorQuickXplain()) {
 453     d_quickSolver->popToZero();
 454     Debug("bv-quick-xplain") << "AlgebraicSolver::quickCheck original conflict size " << conflict.getNumChildren() << "\n";
 455     conflict = d_quickXplain->minimizeConflict(conflict);
 456     Debug("bv-quick-xplain") << "AlgebraicSolver::quickCheck minimized conflict size " << conflict.getNumChildren() << "\n";
 457   }
 458
 459   vector<TNode> theory_confl;
 460   for (unsigned i = 0; i < conflict.getNumChildren(); ++i) {
 461     TNode c = conflict[i];
 462
 463     Assert (d_ids.find(c) != d_ids.end());
 464     unsigned c_id = d_ids[c];
 465     Assert (c_id < d_explanations.size());
 466     TNode c_expl = d_explanations[c_id];
 467     theory_confl.push_back(c_expl);
 468   }
 469
 470   Node confl = BooleanSimplification::simplify(utils::mkAnd(theory_confl));
 471
 472   Debug("bv-subtheory-algebraic") << " Out Conflict: " << confl << "\n";
 473   setConflict(confl);
 474   return false;
 475 }
 476
 477 void AlgebraicSolver::setConflict(TNode conflict) {
 478   Node final_conflict = conflict;
 479   if (options::bitvectorQuickXplain() &&
 480       conflict.getKind() == kind::AND &&
 481       conflict.getNumChildren() > 4) {
 482     final_conflict = d_quickXplain->minimizeConflict(conflict);
 483   }
 484   d_bv->setConflict(final_conflict);
 485 }
 486
 487 bool AlgebraicSolver::solve(TNode fact, TNode reason, SubstitutionEx& subst) {
 488   if (fact.getKind() != kind::EQUAL) return false;
 489
 490   NodeManager* nm = NodeManager::currentNM();
 491   TNode left = fact[0];
 492   TNode right = fact[1];
 493
 494   if (left.isVar() && !expr::hasSubterm(right, left))
 495   {
 496     bool changed = subst.addSubstitution(left, right, reason);
 497     return changed;
 498   }
 499   if (right.isVar() && !expr::hasSubterm(left, right))
 500   {
 501     bool changed = subst.addSubstitution(right, left, reason);
 502     return changed;
 503   }
 504
 505   // xor simplification
 506   if (right.getKind() == kind::BITVECTOR_XOR &&
 507       left.getKind() == kind::BITVECTOR_XOR) {
 508     TNode var = left[0];
 509     if (var.getMetaKind() != kind::metakind::VARIABLE)
 510       return false;
 511
 512     // simplify xor with same variable on both sides
 513     if (expr::hasSubterm(right, var))
 514     {
 515       std::vector<Node> right_children;
 516       for (unsigned i = 0; i < right.getNumChildren(); ++i) {
 517         if (right[i] != var)
 518           right_children.push_back(right[i]);
 519       }
 520       Assert (right_children.size());
 521       Node new_right = utils::mkNaryNode(kind::BITVECTOR_XOR, right_children);
 522       std::vector<Node> left_children;
 523       for (unsigned i = 1; i < left.getNumChildren(); ++i) {
 524         left_children.push_back(left[i]);
 525       }
 526       Node new_left = utils::mkNaryNode(kind::BITVECTOR_XOR, left_children);
 527       Node new_fact = nm->mkNode(kind::EQUAL, new_left, new_right);
 528       bool changed = subst.addSubstitution(fact, new_fact, reason);
 529       return changed;
 530     }
 531
 532     NodeBuilder<> nb(kind::BITVECTOR_XOR);
 533     for (unsigned i = 1; i < left.getNumChildren(); ++i) {
 534       nb << left[i];
 535     }
 536     Node inverse = left.getNumChildren() == 2? (Node)left[1] : (Node)nb;
 537     Node new_right = nm->mkNode(kind::BITVECTOR_XOR, right, inverse);
 538     bool changed = subst.addSubstitution(var, new_right, reason);
 539
 540     if (Dump.isOn("bv-algebraic")) {
 541       Node query = utils::mkNot(nm->mkNode(
 542           kind::EQUAL, fact, nm->mkNode(kind::EQUAL, var, new_right)));
 543       Dump("bv-algebraic") << EchoCommand("ThoeryBV::AlgebraicSolver::substitution explanation");
 544       Dump("bv-algebraic") << PushCommand();
 545       Dump("bv-algebraic") << AssertCommand(query.toExpr());
 546       Dump("bv-algebraic") << CheckSatCommand();
 547       Dump("bv-algebraic") << PopCommand();
 548     }
 549
 550
 551     return changed;
 552   }
 553
 554   // (a xor t = a) <=> (t = 0)
 555   if (left.getKind() == kind::BITVECTOR_XOR
 556       && right.getMetaKind() == kind::metakind::VARIABLE
 557       && expr::hasSubterm(left, right))
 558   {
 559     TNode var = right;
 560     Node new_left = nm->mkNode(kind::BITVECTOR_XOR, var, left);
 561     Node zero = utils::mkConst(utils::getSize(var), 0u);
 562     Node new_fact = nm->mkNode(kind::EQUAL, zero, new_left);
 563     bool changed = subst.addSubstitution(fact, new_fact, reason);
 564     return changed;
 565   }
 566
 567   if (right.getKind() == kind::BITVECTOR_XOR
 568       && left.getMetaKind() == kind::metakind::VARIABLE
 569       && expr::hasSubterm(right, left))
 570   {
 571     TNode var = left;
 572     Node new_right = nm->mkNode(kind::BITVECTOR_XOR, var, right);
 573     Node zero = utils::mkConst(utils::getSize(var), 0u);
 574     Node new_fact = nm->mkNode(kind::EQUAL, zero, new_right);
 575     bool changed = subst.addSubstitution(fact, new_fact, reason);
 576     return changed;
 577   }
 578
 579   // (a xor b = 0) <=> (a = b)
 580   if (left.getKind() == kind::BITVECTOR_XOR &&
 581       left.getNumChildren() == 2 &&
 582       right.getKind() == kind::CONST_BITVECTOR &&
 583       right.getConst<BitVector>() == BitVector(utils::getSize(left), 0u)) {
 584     Node new_fact = nm->mkNode(kind::EQUAL, left[0], left[1]);
 585     bool changed = subst.addSubstitution(fact, new_fact, reason);
 586     return changed;
 587   }
 588
 589
 590   return false;
 591 }
 592
 593 bool AlgebraicSolver::isSubstitutableIn(TNode node, TNode in)
 594 {
 595   if (node.getMetaKind() == kind::metakind::VARIABLE
 596       && !expr::hasSubterm(in, node))
 597     return true;
 598   return false;
 599 }
 600
 601 void AlgebraicSolver::processAssertions(std::vector<WorklistElement>& worklist, SubstitutionEx& subst) {
 602   NodeManager* nm = NodeManager::currentNM();
 603   bool changed = true;
 604   while(changed) {
 605     // d_bv->spendResource();
 606     changed = false;
 607     for (unsigned i = 0; i < worklist.size(); ++i) {
 608       // apply current substitutions
 609       Node current = subst.apply(worklist[i].node);
 610       unsigned current_id = worklist[i].id;
 611       Node subst_expl = subst.explain(worklist[i].node);
 612       worklist[i] = WorklistElement(Rewriter::rewrite(current), current_id);
 613       // explanation for this assertion
 614       Node old_expl = d_explanations[current_id];
 615       Node new_expl = mergeExplanations(subst_expl, old_expl);
 616       storeExplanation(current_id, new_expl);
 617
 618       // use the new substitution to solve
 619       if(solve(worklist[i].node, new_expl, subst)) {
 620         changed = true;
 621       }
 622     }
 623
 624     // check for concat slicings
 625     for (unsigned i = 0; i < worklist.size(); ++i) {
 626       TNode fact = worklist[i].node;
 627       unsigned current_id = worklist[i].id;
 628
 629       if (fact.getKind() != kind::EQUAL) {
 630         continue;
 631       }
 632
 633       TNode left = fact[0];
 634       TNode right = fact[1];
 635       if (left.getKind() != kind::BITVECTOR_CONCAT ||
 636           right.getKind() != kind::BITVECTOR_CONCAT ||
 637           left.getNumChildren() != right.getNumChildren()) {
 638         continue;
 639       }
 640
 641       bool can_slice = true;
 642       for (unsigned j = 0; j < left.getNumChildren(); ++j) {
 643         if (utils::getSize(left[j]) != utils::getSize(right[j]))
 644           can_slice = false;
 645       }
 646
 647       if (!can_slice) {
 648         continue;
 649       }
 650
 651       for (unsigned j = 0; j < left.getNumChildren(); ++j) {
 652         Node eq_j = nm->mkNode(kind::EQUAL, left[j], right[j]);
 653         unsigned id = d_explanations.size();
 654         TNode expl = d_explanations[current_id];
 655         storeExplanation(expl);
 656         worklist.push_back(WorklistElement(eq_j, id));
 657         d_ids[eq_j] = id;
 658       }
 659       worklist[i] = WorklistElement(utils::mkTrue(), worklist[i].id);
 660       changed = true;
 661     }
 662     Assert (d_explanations.size() == worklist.size());
 663   }
 664 }
 665
 666 void AlgebraicSolver::storeExplanation(unsigned id, TNode explanation) {
 667   Assert (checkExplanation(explanation));
 668   d_explanations[id] = explanation;
 669 }
 670
 671 void AlgebraicSolver::storeExplanation(TNode explanation) {
 672   Assert (checkExplanation(explanation));
 673   d_explanations.push_back(explanation);
 674 }
 675
 676 bool AlgebraicSolver::checkExplanation(TNode explanation) {
 677   Node simplified_explanation = explanation; //BooleanSimplification::simplify(explanation);
 678   if (simplified_explanation.getKind() != kind::AND) {
 679     return d_inputAssertions.find(simplified_explanation) != d_inputAssertions.end();
 680   }
 681   for (unsigned i = 0; i < simplified_explanation.getNumChildren(); ++i) {
 682     if (d_inputAssertions.find(simplified_explanation[i]) == d_inputAssertions.end()) {
 683       return false;
 684     }
 685   }
 686   return true;
 687 }
 688
 689
 690 bool AlgebraicSolver::isComplete() {
 691   return d_isComplete.get();
 692 }
 693
 694 bool AlgebraicSolver::useHeuristic() {
 695   if (d_numCalls == 0)
 696     return true;
 697
 698   double success_rate = double(d_numSolved)/double(d_numCalls);
 699   d_statistics.d_useHeuristic.setData(success_rate);
 700   return success_rate > 0.8;
 701 }
 702
 703
 704 void AlgebraicSolver::assertFact(TNode fact) {
 705   d_assertionQueue.push_back(fact);
 706   d_isComplete.set(false);
 707   if (!d_isDifficult.get()) {
 708     d_isDifficult.set(hasExpensiveBVOperators(fact));
 709   }
 710 }
 711
 712 EqualityStatus AlgebraicSolver::getEqualityStatus(TNode a, TNode b) {
 713   return EQUALITY_UNKNOWN;
 714 }
 715
 716 bool AlgebraicSolver::collectModelInfo(TheoryModel* model, bool fullModel)
 717 {
 718   Debug("bitvector-model") << "AlgebraicSolver::collectModelInfo\n";
 719   AlwaysAssert (!d_quickSolver->inConflict());
 720   set<Node> termSet;
 721   d_bv->computeRelevantTerms(termSet);
 722
 723   // collect relevant terms that the bv theory abstracts to variables
 724   // (variables and parametric terms such as select apply_uf)
 725   std::vector<TNode> variables;
 726   std::vector<Node> values;
 727   for (set<Node>::const_iterator it = termSet.begin(); it != termSet.end(); ++it) {
 728     TNode term = *it;
 729     if (term.getType().isBitVector() &&
 730         (term.getMetaKind() == kind::metakind::VARIABLE ||
 731          Theory::theoryOf(term) != THEORY_BV)) {
 732       variables.push_back(term);
 733       values.push_back(term);
 734     }
 735   }
 736
 737   NodeSet leaf_vars;
 738   Debug("bitvector-model") << "Substitutions:\n";
 739   for (unsigned i = 0; i < variables.size(); ++i) {
 740     TNode current = variables[i];
 741     TNode subst = Rewriter::rewrite(d_modelMap->apply(current));
 742     Debug("bitvector-model") << "   " << current << " => " << subst << "\n";
 743     values[i] = subst;
 744     collectVariables(subst, leaf_vars);
 745   }
 746
 747   Debug("bitvector-model") << "Model:\n";
 748
 749   for (NodeSet::const_iterator it = leaf_vars.begin(); it != leaf_vars.end(); ++it) {
 750     TNode var = *it;
 751     Node value = d_quickSolver->getVarValue(var, true);
 752     Assert (!value.isNull() || !fullModel);
 753
 754     // may be a shared term that did not appear in the current assertions
 755     // AJR: need to check whether already in map for cases where collectModelInfo is called multiple times in the same context
 756     if (!value.isNull() && !d_modelMap->hasSubstitution(var)) {
 757       Debug("bitvector-model") << "   " << var << " => " << value << "\n";
 758       Assert (value.getKind() == kind::CONST_BITVECTOR);
 759       d_modelMap->addSubstitution(var, value);
 760     }
 761   }
 762
 763   Debug("bitvector-model") << "Final Model:\n";
 764   for (unsigned i = 0; i < variables.size(); ++i) {
 765     TNode current = values[i];
 766     TNode subst = Rewriter::rewrite(d_modelMap->apply(current));
 767     Debug("bitvector-model") << "AlgebraicSolver:   " << variables[i] << " => " << subst << "\n";
 768     // Doesn't have to be constant as it may be irrelevant
 769     Assert (subst.getKind() == kind::CONST_BITVECTOR);
 770     if (!model->assertEquality(variables[i], subst, true))
 771     {
 772       return false;
 773     }
 774   }
 775   return true;
 776  }
 777
 778 Node AlgebraicSolver::getModelValue(TNode node) {
 779   return Node::null();
 780 }
 781
 782 AlgebraicSolver::Statistics::Statistics()
 783   : d_numCallstoCheck("theory::bv::algebraic::NumCallsToCheck", 0)
 784   , d_numSimplifiesToTrue("theory::bv::algebraic::NumSimplifiesToTrue", 0)
 785   , d_numSimplifiesToFalse("theory::bv::algebraic::NumSimplifiesToFalse", 0)
 786   , d_numUnsat("theory::bv::algebraic::NumUnsat", 0)
 787   , d_numSat("theory::bv::algebraic::NumSat", 0)
 788   , d_numUnknown("theory::bv::algebraic::NumUnknown", 0)
 789   , d_solveTime("theory::bv::algebraic::SolveTime")
 790   , d_useHeuristic("theory::bv::algebraic::UseHeuristic", 0.2)
 791 {
 792   smtStatisticsRegistry()->registerStat(&d_numCallstoCheck);
 793   smtStatisticsRegistry()->registerStat(&d_numSimplifiesToTrue);
 794   smtStatisticsRegistry()->registerStat(&d_numSimplifiesToFalse);
 795   smtStatisticsRegistry()->registerStat(&d_numUnsat);
 796   smtStatisticsRegistry()->registerStat(&d_numSat);
 797   smtStatisticsRegistry()->registerStat(&d_numUnknown);
 798   smtStatisticsRegistry()->registerStat(&d_solveTime);
 799   smtStatisticsRegistry()->registerStat(&d_useHeuristic);
 800 }
 801
 802 AlgebraicSolver::Statistics::~Statistics() {
 803   smtStatisticsRegistry()->unregisterStat(&d_numCallstoCheck);
 804   smtStatisticsRegistry()->unregisterStat(&d_numSimplifiesToTrue);
 805   smtStatisticsRegistry()->unregisterStat(&d_numSimplifiesToFalse);
 806   smtStatisticsRegistry()->unregisterStat(&d_numUnsat);
 807   smtStatisticsRegistry()->unregisterStat(&d_numSat);
 808   smtStatisticsRegistry()->unregisterStat(&d_numUnknown);
 809   smtStatisticsRegistry()->unregisterStat(&d_solveTime);
 810   smtStatisticsRegistry()->unregisterStat(&d_useHeuristic);
 811 }
 812
 813 bool hasExpensiveBVOperatorsRec(TNode fact, TNodeSet& seen) {
 814   if (fact.getKind() == kind::BITVECTOR_MULT ||
 815       fact.getKind() == kind::BITVECTOR_UDIV_TOTAL ||
 816       fact.getKind() == kind::BITVECTOR_UREM_TOTAL) {
 817     return true;
 818   }
 819
 820   if (seen.find(fact) != seen.end()) {
 821     return false;
 822   }
 823
 824   if (fact.getNumChildren() == 0) {
 825     return false;
 826   }
 827   for (unsigned i = 0; i < fact.getNumChildren(); ++i) {
 828     bool difficult = hasExpensiveBVOperatorsRec(fact[i], seen);
 829     if (difficult)
 830       return true;
 831   }
 832   seen.insert(fact);
 833   return false;
 834 }
 835
 836 bool hasExpensiveBVOperators(TNode fact) {
 837   TNodeSet seen;
 838   return hasExpensiveBVOperatorsRec(fact, seen);
 839 }
 840
 841 void ExtractSkolemizer::skolemize(std::vector<WorklistElement>& facts) {
 842   TNodeSet seen;
 843   for (unsigned i = 0; i < facts.size(); ++i) {
 844     TNode current = facts[i].node;
 845     collectExtracts(current, seen);
 846   }
 847
 848   for (VarExtractMap::iterator it = d_varToExtract.begin(); it != d_varToExtract.end(); ++it) {
 849     ExtractList& el = it->second;
 850     TNode var = it->first;
 851     Base& base = el.base;
 852
 853     unsigned bw = utils::getSize(var);
 854     // compute decomposition
 855     std::vector<unsigned> cuts;
 856     for (unsigned i = 1; i <= bw; ++i) {
 857       if (base.isCutPoint(i)) {
 858         cuts.push_back(i);
 859       }
 860     }
 861     unsigned previous = 0;
 862     unsigned current = 0;
 863     std::vector<Node> skolems;
 864     for (unsigned i = 0; i < cuts.size(); ++i) {
 865       current = cuts[i];
 866       Assert (current > 0);
 867       int size = current - previous;
 868       Assert (size > 0);
 869       Node sk = utils::mkVar(size);
 870       skolems.push_back(sk);
 871       previous = current;
 872     }
 873     if (current < bw -1) {
 874       int size = bw - current;
 875       Assert (size > 0);
 876       Node sk = utils::mkVar(size);
 877       skolems.push_back(sk);
 878     }
 879     NodeBuilder<> skolem_nb(kind::BITVECTOR_CONCAT);
 880
 881     for (int i = skolems.size() - 1; i >= 0; --i) {
 882       skolem_nb << skolems[i];
 883     }
 884
 885     Node skolem_concat = skolems.size() == 1 ? (Node)skolems[0] : (Node) skolem_nb;
 886     Assert (utils::getSize(skolem_concat) == utils::getSize(var));
 887     storeSkolem(var, skolem_concat);
 888
 889     for (unsigned i = 0; i < el.extracts.size(); ++i) {
 890       unsigned h = el.extracts[i].high;
 891       unsigned l = el.extracts[i].low;
 892       Node extract = utils::mkExtract(var, h, l);
 893       Node skolem_extract = Rewriter::rewrite(utils::mkExtract(skolem_concat, h, l));
 894       Assert (skolem_extract.getMetaKind() == kind::metakind::VARIABLE ||
 895               skolem_extract.getKind() == kind::BITVECTOR_CONCAT);
 896       storeSkolem(extract, skolem_extract);
 897     }
 898   }
 899
 900   for (unsigned i = 0; i < facts.size(); ++i) {
 901     facts[i] = WorklistElement(skolemize(facts[i].node), facts[i].id);
 902   }
 903 }
 904
 905 Node ExtractSkolemizer::mkSkolem(Node node) {
 906   Assert (node.getKind() == kind::BITVECTOR_EXTRACT &&
 907           node[0].getMetaKind() == kind::metakind::VARIABLE);
 908   Assert (!d_skolemSubst.hasSubstitution(node));
 909   return utils::mkVar(utils::getSize(node));
 910 }
 911
 912 void ExtractSkolemizer::unSkolemize(std::vector<WorklistElement>& facts) {
 913   for (unsigned i = 0; i < facts.size(); ++i) {
 914     facts[i] = WorklistElement(unSkolemize(facts[i].node), facts[i].id);
 915   }
 916 }
 917
 918 void ExtractSkolemizer::storeSkolem(TNode node, TNode skolem) {
 919   d_skolemSubst.addSubstitution(node, skolem);
 920   d_modelMap->addSubstitution(node, skolem);
 921   d_skolemSubstRev.addSubstitution(skolem, node);
 922 }
 923
 924 Node ExtractSkolemizer::unSkolemize(TNode node) {
 925   return d_skolemSubstRev.apply(node);
 926 }
 927
 928 Node ExtractSkolemizer::skolemize(TNode node) {
 929   return d_skolemSubst.apply(node);
 930 }
 931
 932 void ExtractSkolemizer::ExtractList::addExtract(Extract& e) {
 933   extracts.push_back(e);
 934   base.sliceAt(e.low);
 935   base.sliceAt(e.high+1);
 936 }
 937
 938 void ExtractSkolemizer::storeExtract(TNode var, unsigned high, unsigned low) {
 939   Assert (var.getMetaKind() == kind::metakind::VARIABLE);
 940   if (d_varToExtract.find(var) == d_varToExtract.end()) {
 941     d_varToExtract[var] = ExtractList(utils::getSize(var));
 942   }
 943   VarExtractMap::iterator it = d_varToExtract.find(var);
 944   ExtractList& el = it->second;
 945   Extract e(high, low);
 946   el.addExtract(e);
 947 }
 948
 949 void ExtractSkolemizer::collectExtracts(TNode node, TNodeSet& seen) {
 950   if (seen.find(node) != seen.end()) {
 951     return;
 952   }
 953
 954   if (node.getKind() == kind::BITVECTOR_EXTRACT &&
 955       node[0].getMetaKind() == kind::metakind::VARIABLE) {
 956     unsigned high = utils::getExtractHigh(node);
 957     unsigned low = utils::getExtractLow(node);
 958     TNode var = node[0];
 959     storeExtract(var, high, low);
 960     seen.insert(node);
 961     return;
 962   }
 963
 964   if (node.getNumChildren() == 0)
 965     return;
 966
 967   for (unsigned i = 0; i < node.getNumChildren(); ++i) {
 968     collectExtracts(node[i], seen);
 969   }
 970   seen.insert(node);
 971 }
 972
 973 ExtractSkolemizer::ExtractSkolemizer(theory::SubstitutionMap* modelMap)
 974   : d_emptyContext()
 975   , d_varToExtract()
 976   , d_modelMap(modelMap)
 977   , d_skolemSubst(&d_emptyContext)
 978   , d_skolemSubstRev(&d_emptyContext)
 979 {}
 980
 981 ExtractSkolemizer::~ExtractSkolemizer() {
 982 }
 983
 984 Node mergeExplanations(const std::vector<Node>& expls) {
 985   TNodeSet literals;
 986   for (unsigned i = 0; i < expls.size(); ++i) {
 987     TNode expl = expls[i];
 988     Assert (expl.getType().isBoolean());
 989     if (expl.getKind() == kind::AND) {
 990       for (unsigned i = 0; i < expl.getNumChildren(); ++i) {
 991         TNode child = expl[i];
 992         if (child == utils::mkTrue())
 993           continue;
 994         literals.insert(child);
 995       }
 996     } else if (expl != utils::mkTrue()) {
 997       literals.insert(expl);
 998     }
 999   }
1000
1001   if (literals.size() == 0) {
1002     return utils::mkTrue();
1003   }else if (literals.size() == 1) {
1004     return *literals.begin();
1005   }
1006
1007   NodeBuilder<> nb(kind::AND);
1008
1009   for (TNodeSet::const_iterator it = literals.begin(); it!= literals.end(); ++it) {
1010     nb << *it;
1011   }
1012   return nb;
1013 }
1014
1015 Node mergeExplanations(TNode expl1, TNode expl2) {
1016   std::vector<Node> expls;
1017   expls.push_back(expl1);
1018   expls.push_back(expl2);
1019   return mergeExplanations(expls);
1020 }
1021
1022 } /* namespace CVC4::theory::bv */
1023 } /* namespace CVc4::theory */
1024 } /* namespace CVC4 */