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