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