GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bv/bv_subtheory_algebraic.cpp Lines: 2 604 0.3 %
Date: 2021-03-22 Branches: 3 2457 0.1 %

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