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