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, Tim King, Aina Niemetz
   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   Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY);
 257
 258   if (!Theory::fullEffort(e)) {
 259     return true;
 260   }
 261
 262   if (!useHeuristic()) {
 263     return true;
 264   }
 265
 266   ++(d_numCalls);
 267
 268   TimerStat::CodeTimer algebraicTimer(d_statistics.d_solveTime);
 269   Debug("bv-subtheory-algebraic") << "AlgebraicSolver::check (" << e << ")\n";
 270   ++(d_statistics.d_numCallstoCheck);
 271
 272   d_explanations.clear();
 273   d_ids.clear();
 274   d_inputAssertions.clear();
 275
 276   std::vector<WorklistElement> worklist;
 277
 278   uint64_t original_bb_cost = 0;
 279
 280   NodeManager* nm = NodeManager::currentNM();
 281   NodeSet seen_assertions;
 282   // Processing assertions from scratch
 283   for (AssertionQueue::const_iterator it = assertionsBegin(); it != assertionsEnd(); ++it) {
 284     Debug("bv-subtheory-algebraic") << "   " << *it << "\n";
 285     TNode assertion = *it;
 286     unsigned id = worklist.size();
 287     d_ids[assertion] = id;
 288     worklist.push_back(WorklistElement(assertion, id));
 289     d_inputAssertions.insert(assertion);
 290     storeExplanation(assertion);
 291
 292     uint64_t assertion_size = d_quickSolver->computeAtomWeight(assertion, seen_assertions);
 293     Assert (original_bb_cost <= original_bb_cost + assertion_size);
 294     original_bb_cost+= assertion_size;
 295   }
 296
 297   for (unsigned i = 0; i < worklist.size(); ++i) {
 298     d_ids[worklist[i].node] = worklist[i].id;
 299   }
 300
 301   Debug("bv-subtheory-algebraic") << "Assertions " << worklist.size() <<" : \n";
 302
 303   Assert (d_explanations.size() == worklist.size());
 304
 305   delete d_modelMap;
 306   d_modelMap = new SubstitutionMap(d_context);
 307   SubstitutionEx subst(d_modelMap);
 308
 309   // first round of substitutions
 310   processAssertions(worklist, subst);
 311
 312   if (!d_isDifficult.get()) {
 313     // skolemize all possible extracts
 314     ExtractSkolemizer skolemizer(d_modelMap);
 315     skolemizer.skolemize(worklist);
 316     // second round of substitutions
 317     processAssertions(worklist, subst);
 318   }
 319
 320   NodeSet subst_seen;
 321   uint64_t subst_bb_cost = 0;
 322
 323   unsigned r = 0;
 324   unsigned w = 0;
 325
 326   for (; r < worklist.size(); ++r) {
 327
 328     TNode fact = worklist[r].node;
 329     unsigned id = worklist[r].id;
 330
 331     if (Dump.isOn("bv-algebraic")) {
 332       Node expl = d_explanations[id];
 333       Node query = utils::mkNot(nm->mkNode(kind::IMPLIES, expl, fact));
 334       Dump("bv-algebraic") << EchoCommand("ThoeryBV::AlgebraicSolver::substitution explanation");
 335       Dump("bv-algebraic") << PushCommand();
 336       Dump("bv-algebraic") << AssertCommand(query.toExpr());
 337       Dump("bv-algebraic") << CheckSatCommand();
 338       Dump("bv-algebraic") << PopCommand();
 339     }
 340
 341     if (fact.isConst() &&
 342         fact.getConst<bool>() == true) {
 343       continue;
 344     }
 345
 346     if (fact.isConst() &&
 347         fact.getConst<bool>() == false) {
 348       // we have a conflict
 349       Node conflict = BooleanSimplification::simplify(d_explanations[id]);
 350       d_bv->setConflict(conflict);
 351       d_isComplete.set(true);
 352       Debug("bv-subtheory-algebraic") << " UNSAT: assertion simplfies to false with conflict: "<< conflict << "\n";
 353
 354       if (Dump.isOn("bv-algebraic")) {
 355         Dump("bv-algebraic") << EchoCommand("TheoryBV::AlgebraicSolver::conflict");
 356         Dump("bv-algebraic") << PushCommand();
 357         Dump("bv-algebraic") << AssertCommand(conflict.toExpr());
 358         Dump("bv-algebraic") << CheckSatCommand();
 359         Dump("bv-algebraic") << PopCommand();
 360       }
 361
 362
 363       ++(d_statistics.d_numSimplifiesToFalse);
 364       ++(d_numSolved);
 365       return false;
 366     }
 367
 368     subst_bb_cost+= d_quickSolver->computeAtomWeight(fact, subst_seen);
 369     worklist[w] = WorklistElement(fact, id);
 370     Node expl =  BooleanSimplification::simplify(d_explanations[id]);
 371     storeExplanation(id, expl);
 372     d_ids[fact] = id;
 373     ++w;
 374   }
 375
 376   worklist.resize(w);
 377
 378
 379   if(Debug.isOn("bv-subtheory-algebraic")) {
 380     Debug("bv-subtheory-algebraic") << "Assertions post-substitutions " << worklist.size() << ":\n";
 381     for (unsigned i = 0; i < worklist.size(); ++i) {
 382       Debug("bv-subtheory-algebraic") << "   " << worklist[i].node << "\n";
 383     }
 384   }
 385
 386
 387   // all facts solved to true
 388   if (worklist.empty()) {
 389     Debug("bv-subtheory-algebraic") << " SAT: everything simplifies to true.\n";
 390     ++(d_statistics.d_numSimplifiesToTrue);
 391     ++(d_numSolved);
 392     return true;
 393   }
 394
 395   double ratio = ((double)subst_bb_cost)/original_bb_cost;
 396   if (ratio > 0.5 ||
 397       !d_isDifficult.get()) {
 398     // give up if problem not reduced enough
 399     d_isComplete.set(false);
 400     return true;
 401   }
 402
 403   d_quickSolver->clearSolver();
 404
 405   d_quickSolver->push();
 406   std::vector<Node> facts;
 407   for (unsigned i = 0; i < worklist.size(); ++i) {
 408     facts.push_back(worklist[i].node);
 409   }
 410   bool ok = quickCheck(facts);
 411
 412   Debug("bv-subtheory-algebraic") << "AlgebraicSolver::check done " << ok << ".\n";
 413   return ok;
 414 }
 415
 416 bool AlgebraicSolver::quickCheck(std::vector<Node>& facts) {
 417   SatValue res = d_quickSolver->checkSat(facts, d_budget);
 418
 419   if (res == SAT_VALUE_UNKNOWN) {
 420     d_isComplete.set(false);
 421     Debug("bv-subtheory-algebraic") << " Unknown.\n";
 422     ++(d_statistics.d_numUnknown);
 423     return true;
 424   }
 425
 426   if (res == SAT_VALUE_TRUE) {
 427     Debug("bv-subtheory-algebraic") << " Sat.\n";
 428     ++(d_statistics.d_numSat);
 429     ++(d_numSolved);
 430     d_isComplete.set(true);
 431     return true;
 432   }
 433
 434   Assert (res == SAT_VALUE_FALSE);
 435   Assert (d_quickSolver->inConflict());
 436   d_isComplete.set(true);
 437   Debug("bv-subtheory-algebraic") << " Unsat.\n";
 438   ++(d_numSolved);
 439   ++(d_statistics.d_numUnsat);
 440
 441
 442   Node conflict = d_quickSolver->getConflict();
 443   Debug("bv-subtheory-algebraic") << " Conflict: " << conflict << "\n";
 444
 445   // singleton conflict
 446   if (conflict.getKind() != kind::AND) {
 447     Assert (d_ids.find(conflict) != d_ids.end());
 448     unsigned id = d_ids[conflict];
 449     Assert (id < d_explanations.size());
 450     Node theory_confl = d_explanations[id];
 451     d_bv->setConflict(theory_confl);
 452     return false;
 453   }
 454
 455   Assert (conflict.getKind() == kind::AND);
 456   if (options::bitvectorQuickXplain()) {
 457     d_quickSolver->popToZero();
 458     Debug("bv-quick-xplain") << "AlgebraicSolver::quickCheck original conflict size " << conflict.getNumChildren() << "\n";
 459     conflict = d_quickXplain->minimizeConflict(conflict);
 460     Debug("bv-quick-xplain") << "AlgebraicSolver::quickCheck minimized conflict size " << conflict.getNumChildren() << "\n";
 461   }
 462
 463   vector<TNode> theory_confl;
 464   for (unsigned i = 0; i < conflict.getNumChildren(); ++i) {
 465     TNode c = conflict[i];
 466
 467     Assert (d_ids.find(c) != d_ids.end());
 468     unsigned c_id = d_ids[c];
 469     Assert (c_id < d_explanations.size());
 470     TNode c_expl = d_explanations[c_id];
 471     theory_confl.push_back(c_expl);
 472   }
 473
 474   Node confl = BooleanSimplification::simplify(utils::mkAnd(theory_confl));
 475
 476   Debug("bv-subtheory-algebraic") << " Out Conflict: " << confl << "\n";
 477   setConflict(confl);
 478   return false;
 479 }
 480
 481 void AlgebraicSolver::setConflict(TNode conflict) {
 482   Node final_conflict = conflict;
 483   if (options::bitvectorQuickXplain() &&
 484       conflict.getKind() == kind::AND &&
 485       conflict.getNumChildren() > 4) {
 486     final_conflict = d_quickXplain->minimizeConflict(conflict);
 487   }
 488   d_bv->setConflict(final_conflict);
 489 }
 490
 491 bool AlgebraicSolver::solve(TNode fact, TNode reason, SubstitutionEx& subst) {
 492   if (fact.getKind() != kind::EQUAL) return false;
 493
 494   NodeManager* nm = NodeManager::currentNM();
 495   TNode left = fact[0];
 496   TNode right = fact[1];
 497
 498   if (left.isVar() && !right.hasSubterm(left)) {
 499     bool changed  = subst.addSubstitution(left, right, reason);
 500     return changed;
 501   }
 502   if (right.isVar() && !left.hasSubterm(right)) {
 503     bool changed = subst.addSubstitution(right, left, reason);
 504     return changed;
 505   }
 506
 507   // xor simplification
 508   if (right.getKind() == kind::BITVECTOR_XOR &&
 509       left.getKind() == kind::BITVECTOR_XOR) {
 510     TNode var = left[0];
 511     if (var.getMetaKind() != kind::metakind::VARIABLE)
 512       return false;
 513
 514     // simplify xor with same variable on both sides
 515     if (right.hasSubterm(var)) {
 516       std::vector<Node> right_children;
 517       for (unsigned i = 0; i < right.getNumChildren(); ++i) {
 518         if (right[i] != var)
 519           right_children.push_back(right[i]);
 520       }
 521       Assert (right_children.size());
 522       Node new_right = utils::mkNaryNode(kind::BITVECTOR_XOR, right_children);
 523       std::vector<Node> left_children;
 524       for (unsigned i = 1; i < left.getNumChildren(); ++i) {
 525         left_children.push_back(left[i]);
 526       }
 527       Node new_left = utils::mkNaryNode(kind::BITVECTOR_XOR, left_children);
 528       Node new_fact = nm->mkNode(kind::EQUAL, new_left, new_right);
 529       bool changed = subst.addSubstitution(fact, new_fact, reason);
 530       return changed;
 531     }
 532
 533     NodeBuilder<> nb(kind::BITVECTOR_XOR);
 534     for (unsigned i = 1; i < left.getNumChildren(); ++i) {
 535       nb << left[i];
 536     }
 537     Node inverse = left.getNumChildren() == 2? (Node)left[1] : (Node)nb;
 538     Node new_right = nm->mkNode(kind::BITVECTOR_XOR, right, inverse);
 539     bool changed = subst.addSubstitution(var, new_right, reason);
 540
 541     if (Dump.isOn("bv-algebraic")) {
 542       Node query = utils::mkNot(nm->mkNode(
 543           kind::EQUAL, fact, nm->mkNode(kind::EQUAL, var, new_right)));
 544       Dump("bv-algebraic") << EchoCommand("ThoeryBV::AlgebraicSolver::substitution explanation");
 545       Dump("bv-algebraic") << PushCommand();
 546       Dump("bv-algebraic") << AssertCommand(query.toExpr());
 547       Dump("bv-algebraic") << CheckSatCommand();
 548       Dump("bv-algebraic") << PopCommand();
 549     }
 550
 551
 552     return changed;
 553   }
 554
 555   // (a xor t = a) <=> (t = 0)
 556   if (left.getKind() == kind::BITVECTOR_XOR &&
 557       right.getMetaKind() == kind::metakind::VARIABLE &&
 558       left.hasSubterm(right)) {
 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       right.hasSubterm(left)) {
 570     TNode var = left;
 571     Node new_right = nm->mkNode(kind::BITVECTOR_XOR, var, right);
 572     Node zero = utils::mkConst(utils::getSize(var), 0u);
 573     Node new_fact = nm->mkNode(kind::EQUAL, zero, new_right);
 574     bool changed = subst.addSubstitution(fact, new_fact, reason);
 575     return changed;
 576   }
 577
 578   // (a xor b = 0) <=> (a = b)
 579   if (left.getKind() == kind::BITVECTOR_XOR &&
 580       left.getNumChildren() == 2 &&
 581       right.getKind() == kind::CONST_BITVECTOR &&
 582       right.getConst<BitVector>() == BitVector(utils::getSize(left), 0u)) {
 583     Node new_fact = nm->mkNode(kind::EQUAL, left[0], left[1]);
 584     bool changed = subst.addSubstitution(fact, new_fact, reason);
 585     return changed;
 586   }
 587
 588
 589   return false;
 590 }
 591
 592 bool AlgebraicSolver::isSubstitutableIn(TNode node, TNode in) {
 593   if (node.getMetaKind() == kind::metakind::VARIABLE &&
 594       !in.hasSubterm(node))
 595     return true;
 596   return false;
 597 }
 598
 599 void AlgebraicSolver::processAssertions(std::vector<WorklistElement>& worklist, SubstitutionEx& subst) {
 600   NodeManager* nm = NodeManager::currentNM();
 601   bool changed = true;
 602   while(changed) {
 603     // d_bv->spendResource();
 604     changed = false;
 605     for (unsigned i = 0; i < worklist.size(); ++i) {
 606       // apply current substitutions
 607       Node current = subst.apply(worklist[i].node);
 608       unsigned current_id = worklist[i].id;
 609       Node subst_expl = subst.explain(worklist[i].node);
 610       worklist[i] = WorklistElement(Rewriter::rewrite(current), current_id);
 611       // explanation for this assertion
 612       Node old_expl = d_explanations[current_id];
 613       Node new_expl = mergeExplanations(subst_expl, old_expl);
 614       storeExplanation(current_id, new_expl);
 615
 616       // use the new substitution to solve
 617       if(solve(worklist[i].node, new_expl, subst)) {
 618         changed = true;
 619       }
 620     }
 621
 622     // check for concat slicings
 623     for (unsigned i = 0; i < worklist.size(); ++i) {
 624       TNode fact = worklist[i].node;
 625       unsigned current_id = worklist[i].id;
 626
 627       if (fact.getKind() != kind::EQUAL) {
 628         continue;
 629       }
 630
 631       TNode left = fact[0];
 632       TNode right = fact[1];
 633       if (left.getKind() != kind::BITVECTOR_CONCAT ||
 634           right.getKind() != kind::BITVECTOR_CONCAT ||
 635           left.getNumChildren() != right.getNumChildren()) {
 636         continue;
 637       }
 638
 639       bool can_slice = true;
 640       for (unsigned j = 0; j < left.getNumChildren(); ++j) {
 641         if (utils::getSize(left[j]) != utils::getSize(right[j]))
 642           can_slice = false;
 643       }
 644
 645       if (!can_slice) {
 646         continue;
 647       }
 648
 649       for (unsigned j = 0; j < left.getNumChildren(); ++j) {
 650         Node eq_j = nm->mkNode(kind::EQUAL, left[j], right[j]);
 651         unsigned id = d_explanations.size();
 652         TNode expl = d_explanations[current_id];
 653         storeExplanation(expl);
 654         worklist.push_back(WorklistElement(eq_j, id));
 655         d_ids[eq_j] = id;
 656       }
 657       worklist[i] = WorklistElement(utils::mkTrue(), worklist[i].id);
 658       changed = true;
 659     }
 660     Assert (d_explanations.size() == worklist.size());
 661   }
 662 }
 663
 664 void AlgebraicSolver::storeExplanation(unsigned id, TNode explanation) {
 665   Assert (checkExplanation(explanation));
 666   d_explanations[id] = explanation;
 667 }
 668
 669 void AlgebraicSolver::storeExplanation(TNode explanation) {
 670   Assert (checkExplanation(explanation));
 671   d_explanations.push_back(explanation);
 672 }
 673
 674 bool AlgebraicSolver::checkExplanation(TNode explanation) {
 675   Node simplified_explanation = explanation; //BooleanSimplification::simplify(explanation);
 676   if (simplified_explanation.getKind() != kind::AND) {
 677     return d_inputAssertions.find(simplified_explanation) != d_inputAssertions.end();
 678   }
 679   for (unsigned i = 0; i < simplified_explanation.getNumChildren(); ++i) {
 680     if (d_inputAssertions.find(simplified_explanation[i]) == d_inputAssertions.end()) {
 681       return false;
 682     }
 683   }
 684   return true;
 685 }
 686
 687
 688 bool AlgebraicSolver::isComplete() {
 689   return d_isComplete.get();
 690 }
 691
 692 bool AlgebraicSolver::useHeuristic() {
 693   if (d_numCalls == 0)
 694     return true;
 695
 696   double success_rate = double(d_numSolved)/double(d_numCalls);
 697   d_statistics.d_useHeuristic.setData(success_rate);
 698   return success_rate > 0.8;
 699 }
 700
 701
 702 void AlgebraicSolver::assertFact(TNode fact) {
 703   d_assertionQueue.push_back(fact);
 704   d_isComplete.set(false);
 705   if (!d_isDifficult.get()) {
 706     d_isDifficult.set(hasExpensiveBVOperators(fact));
 707   }
 708 }
 709
 710 EqualityStatus AlgebraicSolver::getEqualityStatus(TNode a, TNode b) {
 711   return EQUALITY_UNKNOWN;
 712 }
 713
 714 bool AlgebraicSolver::collectModelInfo(TheoryModel* model, bool fullModel)
 715 {
 716   Debug("bitvector-model") << "AlgebraicSolver::collectModelInfo\n";
 717   AlwaysAssert (!d_quickSolver->inConflict());
 718   set<Node> termSet;
 719   d_bv->computeRelevantTerms(termSet);
 720
 721   // collect relevant terms that the bv theory abstracts to variables
 722   // (variables and parametric terms such as select apply_uf)
 723   std::vector<TNode> variables;
 724   std::vector<Node> values;
 725   for (set<Node>::const_iterator it = termSet.begin(); it != termSet.end(); ++it) {
 726     TNode term = *it;
 727     if (term.getType().isBitVector() &&
 728         (term.getMetaKind() == kind::metakind::VARIABLE ||
 729          Theory::theoryOf(term) != THEORY_BV)) {
 730       variables.push_back(term);
 731       values.push_back(term);
 732     }
 733   }
 734
 735   NodeSet leaf_vars;
 736   Debug("bitvector-model") << "Substitutions:\n";
 737   for (unsigned i = 0; i < variables.size(); ++i) {
 738     TNode current = variables[i];
 739     TNode subst = Rewriter::rewrite(d_modelMap->apply(current));
 740     Debug("bitvector-model") << "   " << current << " => " << subst << "\n";
 741     values[i] = subst;
 742     collectVariables(subst, leaf_vars);
 743   }
 744
 745   Debug("bitvector-model") << "Model:\n";
 746
 747   for (NodeSet::const_iterator it = leaf_vars.begin(); it != leaf_vars.end(); ++it) {
 748     TNode var = *it;
 749     Node value = d_quickSolver->getVarValue(var, true);
 750     Assert (!value.isNull() || !fullModel);
 751
 752     // may be a shared term that did not appear in the current assertions
 753     // AJR: need to check whether already in map for cases where collectModelInfo is called multiple times in the same context
 754     if (!value.isNull() && !d_modelMap->hasSubstitution(var)) {
 755       Debug("bitvector-model") << "   " << var << " => " << value << "\n";
 756       Assert (value.getKind() == kind::CONST_BITVECTOR);
 757       d_modelMap->addSubstitution(var, value);
 758     }
 759   }
 760
 761   Debug("bitvector-model") << "Final Model:\n";
 762   for (unsigned i = 0; i < variables.size(); ++i) {
 763     TNode current = values[i];
 764     TNode subst = Rewriter::rewrite(d_modelMap->apply(current));
 765     Debug("bitvector-model") << "AlgebraicSolver:   " << variables[i] << " => " << subst << "\n";
 766     // Doesn't have to be constant as it may be irrelevant
 767     Assert (subst.getKind() == kind::CONST_BITVECTOR);
 768     if (!model->assertEquality(variables[i], subst, true))
 769     {
 770       return false;
 771     }
 772   }
 773   return true;
 774  }
 775
 776 Node AlgebraicSolver::getModelValue(TNode node) {
 777   return Node::null();
 778 }
 779
 780 AlgebraicSolver::Statistics::Statistics()
 781   : d_numCallstoCheck("theory::bv::algebraic::NumCallsToCheck", 0)
 782   , d_numSimplifiesToTrue("theory::bv::algebraic::NumSimplifiesToTrue", 0)
 783   , d_numSimplifiesToFalse("theory::bv::algebraic::NumSimplifiesToFalse", 0)
 784   , d_numUnsat("theory::bv::algebraic::NumUnsat", 0)
 785   , d_numSat("theory::bv::algebraic::NumSat", 0)
 786   , d_numUnknown("theory::bv::algebraic::NumUnknown", 0)
 787   , d_solveTime("theory::bv::algebraic::SolveTime")
 788   , d_useHeuristic("theory::bv::algebraic::UseHeuristic", 0.2)
 789 {
 790   smtStatisticsRegistry()->registerStat(&d_numCallstoCheck);
 791   smtStatisticsRegistry()->registerStat(&d_numSimplifiesToTrue);
 792   smtStatisticsRegistry()->registerStat(&d_numSimplifiesToFalse);
 793   smtStatisticsRegistry()->registerStat(&d_numUnsat);
 794   smtStatisticsRegistry()->registerStat(&d_numSat);
 795   smtStatisticsRegistry()->registerStat(&d_numUnknown);
 796   smtStatisticsRegistry()->registerStat(&d_solveTime);
 797   smtStatisticsRegistry()->registerStat(&d_useHeuristic);
 798 }
 799
 800 AlgebraicSolver::Statistics::~Statistics() {
 801   smtStatisticsRegistry()->unregisterStat(&d_numCallstoCheck);
 802   smtStatisticsRegistry()->unregisterStat(&d_numSimplifiesToTrue);
 803   smtStatisticsRegistry()->unregisterStat(&d_numSimplifiesToFalse);
 804   smtStatisticsRegistry()->unregisterStat(&d_numUnsat);
 805   smtStatisticsRegistry()->unregisterStat(&d_numSat);
 806   smtStatisticsRegistry()->unregisterStat(&d_numUnknown);
 807   smtStatisticsRegistry()->unregisterStat(&d_solveTime);
 808   smtStatisticsRegistry()->unregisterStat(&d_useHeuristic);
 809 }
 810
 811 bool hasExpensiveBVOperatorsRec(TNode fact, TNodeSet& seen) {
 812   if (fact.getKind() == kind::BITVECTOR_MULT ||
 813       fact.getKind() == kind::BITVECTOR_UDIV_TOTAL ||
 814       fact.getKind() == kind::BITVECTOR_UREM_TOTAL) {
 815     return true;
 816   }
 817
 818   if (seen.find(fact) != seen.end()) {
 819     return false;
 820   }
 821
 822   if (fact.getNumChildren() == 0) {
 823     return false;
 824   }
 825   for (unsigned i = 0; i < fact.getNumChildren(); ++i) {
 826     bool difficult = hasExpensiveBVOperatorsRec(fact[i], seen);
 827     if (difficult)
 828       return true;
 829   }
 830   seen.insert(fact);
 831   return false;
 832 }
 833
 834 bool hasExpensiveBVOperators(TNode fact) {
 835   TNodeSet seen;
 836   return hasExpensiveBVOperatorsRec(fact, seen);
 837 }
 838
 839 void ExtractSkolemizer::skolemize(std::vector<WorklistElement>& facts) {
 840   TNodeSet seen;
 841   for (unsigned i = 0; i < facts.size(); ++i) {
 842     TNode current = facts[i].node;
 843     collectExtracts(current, seen);
 844   }
 845
 846   for (VarExtractMap::iterator it = d_varToExtract.begin(); it != d_varToExtract.end(); ++it) {
 847     ExtractList& el = it->second;
 848     TNode var = it->first;
 849     Base& base = el.base;
 850
 851     unsigned bw = utils::getSize(var);
 852     // compute decomposition
 853     std::vector<unsigned> cuts;
 854     for (unsigned i = 1; i <= bw; ++i) {
 855       if (base.isCutPoint(i)) {
 856         cuts.push_back(i);
 857       }
 858     }
 859     unsigned previous = 0;
 860     unsigned current = 0;
 861     std::vector<Node> skolems;
 862     for (unsigned i = 0; i < cuts.size(); ++i) {
 863       current = cuts[i];
 864       Assert (current > 0);
 865       int size = current - previous;
 866       Assert (size > 0);
 867       Node sk = utils::mkVar(size);
 868       skolems.push_back(sk);
 869       previous = current;
 870     }
 871     if (current < bw -1) {
 872       int size = bw - current;
 873       Assert (size > 0);
 874       Node sk = utils::mkVar(size);
 875       skolems.push_back(sk);
 876     }
 877     NodeBuilder<> skolem_nb(kind::BITVECTOR_CONCAT);
 878
 879     for (int i = skolems.size() - 1; i >= 0; --i) {
 880       skolem_nb << skolems[i];
 881     }
 882
 883     Node skolem_concat = skolems.size() == 1 ? (Node)skolems[0] : (Node) skolem_nb;
 884     Assert (utils::getSize(skolem_concat) == utils::getSize(var));
 885     storeSkolem(var, skolem_concat);
 886
 887     for (unsigned i = 0; i < el.extracts.size(); ++i) {
 888       unsigned h = el.extracts[i].high;
 889       unsigned l = el.extracts[i].low;
 890       Node extract = utils::mkExtract(var, h, l);
 891       Node skolem_extract = Rewriter::rewrite(utils::mkExtract(skolem_concat, h, l));
 892       Assert (skolem_extract.getMetaKind() == kind::metakind::VARIABLE ||
 893               skolem_extract.getKind() == kind::BITVECTOR_CONCAT);
 894       storeSkolem(extract, skolem_extract);
 895     }
 896   }
 897
 898   for (unsigned i = 0; i < facts.size(); ++i) {
 899     facts[i] = WorklistElement(skolemize(facts[i].node), facts[i].id);
 900   }
 901 }
 902
 903 Node ExtractSkolemizer::mkSkolem(Node node) {
 904   Assert (node.getKind() == kind::BITVECTOR_EXTRACT &&
 905           node[0].getMetaKind() == kind::metakind::VARIABLE);
 906   Assert (!d_skolemSubst.hasSubstitution(node));
 907   return utils::mkVar(utils::getSize(node));
 908 }
 909
 910 void ExtractSkolemizer::unSkolemize(std::vector<WorklistElement>& facts) {
 911   for (unsigned i = 0; i < facts.size(); ++i) {
 912     facts[i] = WorklistElement(unSkolemize(facts[i].node), facts[i].id);
 913   }
 914 }
 915
 916 void ExtractSkolemizer::storeSkolem(TNode node, TNode skolem) {
 917   d_skolemSubst.addSubstitution(node, skolem);
 918   d_modelMap->addSubstitution(node, skolem);
 919   d_skolemSubstRev.addSubstitution(skolem, node);
 920 }
 921
 922 Node ExtractSkolemizer::unSkolemize(TNode node) {
 923   return d_skolemSubstRev.apply(node);
 924 }
 925
 926 Node ExtractSkolemizer::skolemize(TNode node) {
 927   return d_skolemSubst.apply(node);
 928 }
 929
 930 void ExtractSkolemizer::ExtractList::addExtract(Extract& e) {
 931   extracts.push_back(e);
 932   base.sliceAt(e.low);
 933   base.sliceAt(e.high+1);
 934 }
 935
 936 void ExtractSkolemizer::storeExtract(TNode var, unsigned high, unsigned low) {
 937   Assert (var.getMetaKind() == kind::metakind::VARIABLE);
 938   if (d_varToExtract.find(var) == d_varToExtract.end()) {
 939     d_varToExtract[var] = ExtractList(utils::getSize(var));
 940   }
 941   VarExtractMap::iterator it = d_varToExtract.find(var);
 942   ExtractList& el = it->second;
 943   Extract e(high, low);
 944   el.addExtract(e);
 945 }
 946
 947 void ExtractSkolemizer::collectExtracts(TNode node, TNodeSet& seen) {
 948   if (seen.find(node) != seen.end()) {
 949     return;
 950   }
 951
 952   if (node.getKind() == kind::BITVECTOR_EXTRACT &&
 953       node[0].getMetaKind() == kind::metakind::VARIABLE) {
 954     unsigned high = utils::getExtractHigh(node);
 955     unsigned low = utils::getExtractLow(node);
 956     TNode var = node[0];
 957     storeExtract(var, high, low);
 958     seen.insert(node);
 959     return;
 960   }
 961
 962   if (node.getNumChildren() == 0)
 963     return;
 964
 965   for (unsigned i = 0; i < node.getNumChildren(); ++i) {
 966     collectExtracts(node[i], seen);
 967   }
 968   seen.insert(node);
 969 }
 970
 971 ExtractSkolemizer::ExtractSkolemizer(theory::SubstitutionMap* modelMap)
 972   : d_emptyContext()
 973   , d_varToExtract()
 974   , d_modelMap(modelMap)
 975   , d_skolemSubst(&d_emptyContext)
 976   , d_skolemSubstRev(&d_emptyContext)
 977 {}
 978
 979 ExtractSkolemizer::~ExtractSkolemizer() {
 980 }
 981
 982 Node mergeExplanations(const std::vector<Node>& expls) {
 983   TNodeSet literals;
 984   for (unsigned i = 0; i < expls.size(); ++i) {
 985     TNode expl = expls[i];
 986     Assert (expl.getType().isBoolean());
 987     if (expl.getKind() == kind::AND) {
 988       for (unsigned i = 0; i < expl.getNumChildren(); ++i) {
 989         TNode child = expl[i];
 990         if (child == utils::mkTrue())
 991           continue;
 992         literals.insert(child);
 993       }
 994     } else if (expl != utils::mkTrue()) {
 995       literals.insert(expl);
 996     }
 997   }
 998
 999   if (literals.size() == 0) {
1000     return utils::mkTrue();
1001   }else if (literals.size() == 1) {
1002     return *literals.begin();
1003   }
1004
1005   NodeBuilder<> nb(kind::AND);
1006
1007   for (TNodeSet::const_iterator it = literals.begin(); it!= literals.end(); ++it) {
1008     nb << *it;
1009   }
1010   return nb;
1011 }
1012
1013 Node mergeExplanations(TNode expl1, TNode expl2) {
1014   std::vector<Node> expls;
1015   expls.push_back(expl1);
1016   expls.push_back(expl2);
1017   return mergeExplanations(expls);
1018 }
1019
1020 } /* namespace CVC4::theory::bv */
1021 } /* namespace CVc4::theory */
1022 } /* namespace CVC4 */