GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bv/bv_solver_lazy.cpp Lines: 343 389 88.2 %
Date: 2021-03-23 Branches: 756 1658 45.6 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file bv_solver_lazy.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Mathias Preiner, Liana Hadarean, Andrew Reynolds
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
 ** [[ Add lengthier description here ]]
13
 ** \todo document this file
14
 **/
15
16
#include "theory/bv/bv_solver_lazy.h"
17
18
#include "expr/node_algorithm.h"
19
#include "options/bv_options.h"
20
#include "options/smt_options.h"
21
#include "smt/smt_statistics_registry.h"
22
#include "theory/bv/abstraction.h"
23
#include "theory/bv/bv_eager_solver.h"
24
#include "theory/bv/bv_subtheory_algebraic.h"
25
#include "theory/bv/bv_subtheory_bitblast.h"
26
#include "theory/bv/bv_subtheory_core.h"
27
#include "theory/bv/bv_subtheory_inequality.h"
28
#include "theory/bv/theory_bv_rewrite_rules_normalization.h"
29
#include "theory/bv/theory_bv_rewrite_rules_simplification.h"
30
#include "theory/bv/theory_bv_rewriter.h"
31
#include "theory/bv/theory_bv_utils.h"
32
#include "theory/theory_model.h"
33
#include "theory/trust_substitutions.h"
34
35
using namespace CVC4::theory::bv::utils;
36
37
namespace CVC4 {
38
namespace theory {
39
namespace bv {
40
41
8987
BVSolverLazy::BVSolverLazy(TheoryBV& bv,
42
                           context::Context* c,
43
                           context::UserContext* u,
44
                           ProofNodeManager* pnm,
45
8987
                           std::string name)
46
    : BVSolver(bv.d_state, bv.d_im),
47
      d_bv(bv),
48
      d_context(c),
49
      d_alreadyPropagatedSet(c),
50
      d_sharedTermsSet(c),
51
      d_subtheories(),
52
      d_subtheoryMap(),
53
      d_statistics(),
54
      d_staticLearnCache(),
55
      d_lemmasAdded(c, false),
56
      d_conflict(c, false),
57
      d_invalidateModelCache(c, true),
58
      d_literalsToPropagate(c),
59
      d_literalsToPropagateIndex(c, 0),
60
      d_propagatedBy(c),
61
      d_eagerSolver(),
62
26961
      d_abstractionModule(new AbstractionModule(getStatsPrefix(THEORY_BV))),
63
35948
      d_calledPreregister(false)
64
{
65
8987
  if (options::bitblastMode() == options::BitblastMode::EAGER)
66
  {
67
31
    d_eagerSolver.reset(new EagerBitblastSolver(c, this));
68
31
    return;
69
  }
70
71
8956
  if (options::bitvectorEqualitySolver())
72
  {
73
8954
    d_subtheories.emplace_back(new CoreSolver(c, this));
74
8954
    d_subtheoryMap[SUB_CORE] = d_subtheories.back().get();
75
  }
76
77
17912
  if (options::bitvectorInequalitySolver())
78
  {
79
8956
    d_subtheories.emplace_back(new InequalitySolver(c, u, this));
80
8956
    d_subtheoryMap[SUB_INEQUALITY] = d_subtheories.back().get();
81
  }
82
83
8956
  if (options::bitvectorAlgebraicSolver())
84
  {
85
    d_subtheories.emplace_back(new AlgebraicSolver(c, this));
86
    d_subtheoryMap[SUB_ALGEBRAIC] = d_subtheories.back().get();
87
  }
88
89
8956
  BitblastSolver* bb_solver = new BitblastSolver(c, this);
90
8956
  if (options::bvAbstraction())
91
  {
92
2
    bb_solver->setAbstraction(d_abstractionModule.get());
93
  }
94
8956
  d_subtheories.emplace_back(bb_solver);
95
8956
  d_subtheoryMap[SUB_BITBLAST] = bb_solver;
96
}
97
98
17968
BVSolverLazy::~BVSolverLazy() {}
99
100
8987
bool BVSolverLazy::needsEqualityEngine(EeSetupInfo& esi)
101
{
102
8987
  CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
103
8987
  if (core)
104
  {
105
8954
    return core->needsEqualityEngine(esi);
106
  }
107
  // otherwise we don't use an equality engine
108
33
  return false;
109
}
110
111
8987
void BVSolverLazy::finishInit()
112
{
113
8987
  CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
114
8987
  if (core)
115
  {
116
    // must finish initialization in the core solver
117
8954
    core->finishInit();
118
  }
119
8987
}
120
121
446449
void BVSolverLazy::spendResource(ResourceManager::Resource r)
122
{
123
446449
  d_im.spendResource(r);
124
446449
}
125
126
8987
BVSolverLazy::Statistics::Statistics()
127
    : d_avgConflictSize("theory::bv::lazy::AvgBVConflictSize"),
128
      d_solveSubstitutions("theory::bv::lazy::NumSolveSubstitutions", 0),
129
      d_solveTimer("theory::bv::lazy::solveTimer"),
130
      d_numCallsToCheckFullEffort("theory::bv::lazy::NumFullCheckCalls", 0),
131
      d_numCallsToCheckStandardEffort("theory::bv::lazy::NumStandardCheckCalls",
132
                                      0),
133
      d_weightComputationTimer("theory::bv::lazy::weightComputationTimer"),
134
8987
      d_numMultSlice("theory::bv::lazy::NumMultSliceApplied", 0)
135
{
136
8987
  smtStatisticsRegistry()->registerStat(&d_avgConflictSize);
137
8987
  smtStatisticsRegistry()->registerStat(&d_solveSubstitutions);
138
8987
  smtStatisticsRegistry()->registerStat(&d_solveTimer);
139
8987
  smtStatisticsRegistry()->registerStat(&d_numCallsToCheckFullEffort);
140
8987
  smtStatisticsRegistry()->registerStat(&d_numCallsToCheckStandardEffort);
141
8987
  smtStatisticsRegistry()->registerStat(&d_weightComputationTimer);
142
8987
  smtStatisticsRegistry()->registerStat(&d_numMultSlice);
143
8987
}
144
145
17968
BVSolverLazy::Statistics::~Statistics()
146
{
147
8984
  smtStatisticsRegistry()->unregisterStat(&d_avgConflictSize);
148
8984
  smtStatisticsRegistry()->unregisterStat(&d_solveSubstitutions);
149
8984
  smtStatisticsRegistry()->unregisterStat(&d_solveTimer);
150
8984
  smtStatisticsRegistry()->unregisterStat(&d_numCallsToCheckFullEffort);
151
8984
  smtStatisticsRegistry()->unregisterStat(&d_numCallsToCheckStandardEffort);
152
8984
  smtStatisticsRegistry()->unregisterStat(&d_weightComputationTimer);
153
8984
  smtStatisticsRegistry()->unregisterStat(&d_numMultSlice);
154
8984
}
155
156
211751
void BVSolverLazy::preRegisterTerm(TNode node)
157
{
158
211751
  d_calledPreregister = true;
159
423502
  Debug("bitvector-preregister")
160
211751
      << "BVSolverLazy::preRegister(" << node << ")" << std::endl;
161
162
211751
  if (options::bitblastMode() == options::BitblastMode::EAGER)
163
  {
164
    // the aig bit-blaster option is set heuristically
165
    // if bv abstraction is used
166
1878
    if (!d_eagerSolver->isInitialized())
167
    {
168
29
      d_eagerSolver->initialize();
169
    }
170
171
1878
    if (node.getKind() == kind::BITVECTOR_EAGER_ATOM)
172
    {
173
588
      Node formula = node[0];
174
294
      d_eagerSolver->assertFormula(formula);
175
    }
176
1878
    return;
177
  }
178
179
839478
  for (unsigned i = 0; i < d_subtheories.size(); ++i)
180
  {
181
629605
    d_subtheories[i]->preRegister(node);
182
  }
183
184
  // AJR : equality solver currently registers all terms to ExtTheory, if we
185
  // want a lazy reduction without the bv equality solver, need to call this
186
  // d_bv.d_extTheory->registerTermRec( node );
187
}
188
189
12827
void BVSolverLazy::sendConflict()
190
{
191
12827
  Assert(d_conflict);
192
12827
  if (d_conflictNode.isNull())
193
  {
194
    return;
195
  }
196
  else
197
  {
198
25654
    Debug("bitvector") << indent() << "BVSolverLazy::check(): conflict "
199
12827
                       << d_conflictNode << std::endl;
200
12827
    d_im.conflict(d_conflictNode, InferenceId::BV_LAZY_CONFLICT);
201
12827
    d_statistics.d_avgConflictSize << d_conflictNode.getNumChildren();
202
12827
    d_conflictNode = Node::null();
203
  }
204
}
205
206
1137863
void BVSolverLazy::checkForLemma(TNode fact)
207
{
208
1137863
  if (fact.getKind() == kind::EQUAL)
209
  {
210
371093
    NodeManager* nm = NodeManager::currentNM();
211
371093
    if (fact[0].getKind() == kind::BITVECTOR_UREM)
212
    {
213
1614
      TNode urem = fact[0];
214
1614
      TNode result = fact[1];
215
1614
      TNode divisor = urem[1];
216
1614
      Node result_ult_div = nm->mkNode(kind::BITVECTOR_ULT, result, divisor);
217
      Node divisor_eq_0 =
218
1614
          nm->mkNode(kind::EQUAL, divisor, mkZero(getSize(divisor)));
219
      Node split = nm->mkNode(
220
1614
          kind::OR, divisor_eq_0, nm->mkNode(kind::NOT, fact), result_ult_div);
221
807
      lemma(split);
222
    }
223
371093
    if (fact[1].getKind() == kind::BITVECTOR_UREM)
224
    {
225
140
      TNode urem = fact[1];
226
140
      TNode result = fact[0];
227
140
      TNode divisor = urem[1];
228
140
      Node result_ult_div = nm->mkNode(kind::BITVECTOR_ULT, result, divisor);
229
      Node divisor_eq_0 =
230
140
          nm->mkNode(kind::EQUAL, divisor, mkZero(getSize(divisor)));
231
      Node split = nm->mkNode(
232
140
          kind::OR, divisor_eq_0, nm->mkNode(kind::NOT, fact), result_ult_div);
233
70
      lemma(split);
234
    }
235
  }
236
1137863
}
237
238
214029
bool BVSolverLazy::preCheck(Theory::Effort e)
239
{
240
214029
  check(e);
241
214029
  return true;
242
}
243
244
214029
void BVSolverLazy::check(Theory::Effort e)
245
{
246
214029
  if (done() && e < Theory::EFFORT_FULL)
247
  {
248
12915
    return;
249
  }
250
251
  // last call : do reductions on extended bitvector functions
252
214029
  if (e == Theory::EFFORT_LAST_CALL)
253
  {
254
    CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
255
    if (core)
256
    {
257
      // check extended functions at last call effort
258
      core->checkExtf(e);
259
    }
260
    return;
261
  }
262
263
214029
  Debug("bitvector") << "BVSolverLazy::check(" << e << ")" << std::endl;
264
415143
  TimerStat::CodeTimer codeTimer(d_statistics.d_solveTimer);
265
  // we may be getting new assertions so the model cache may not be sound
266
214029
  d_invalidateModelCache.set(true);
267
  // if we are using the eager solver
268
214029
  if (options::bitblastMode() == options::BitblastMode::EAGER)
269
  {
270
    // this can only happen on an empty benchmark
271
88
    if (!d_eagerSolver->isInitialized())
272
    {
273
      d_eagerSolver->initialize();
274
    }
275
88
    if (!Theory::fullEffort(e)) return;
276
277
94
    std::vector<TNode> assertions;
278
635
    while (!done())
279
    {
280
588
      TNode fact = get().d_assertion;
281
294
      Assert(fact.getKind() == kind::BITVECTOR_EAGER_ATOM);
282
294
      assertions.push_back(fact);
283
294
      d_eagerSolver->assertFormula(fact[0]);
284
    }
285
286
47
    bool ok = d_eagerSolver->checkSat();
287
47
    if (!ok)
288
    {
289
18
      if (assertions.size() == 1)
290
      {
291
14
        d_im.conflict(assertions[0], InferenceId::BV_LAZY_CONFLICT);
292
14
        return;
293
      }
294
8
      Node conflict = utils::mkAnd(assertions);
295
4
      d_im.conflict(conflict, InferenceId::BV_LAZY_CONFLICT);
296
4
      return;
297
    }
298
29
    return;
299
  }
300
301
213941
  if (Theory::fullEffort(e))
302
  {
303
28943
    ++(d_statistics.d_numCallsToCheckFullEffort);
304
  }
305
  else
306
  {
307
184998
    ++(d_statistics.d_numCallsToCheckStandardEffort);
308
  }
309
  // if we are already in conflict just return the conflict
310
213941
  if (inConflict())
311
  {
312
    sendConflict();
313
    return;
314
  }
315
316
2489667
  while (!done())
317
  {
318
2275726
    TNode fact = get().d_assertion;
319
320
1137863
    checkForLemma(fact);
321
322
4551444
    for (unsigned i = 0; i < d_subtheories.size(); ++i)
323
    {
324
3413581
      d_subtheories[i]->assertFact(fact);
325
    }
326
  }
327
328
213941
  bool ok = true;
329
213941
  bool complete = false;
330
573862
  for (unsigned i = 0; i < d_subtheories.size(); ++i)
331
  {
332
573862
    Assert(!inConflict());
333
573862
    ok = d_subtheories[i]->check(e);
334
573862
    complete = d_subtheories[i]->isComplete();
335
336
573862
    if (!ok)
337
    {
338
      // if we are in a conflict no need to check with other theories
339
12827
      Assert(inConflict());
340
12827
      sendConflict();
341
12827
      return;
342
    }
343
561035
    if (complete)
344
    {
345
      // if the last subtheory was complete we stop
346
201114
      break;
347
    }
348
  }
349
350
  // check extended functions
351
201114
  if (Theory::fullEffort(e))
352
  {
353
24388
    CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
354
24388
    if (core)
355
    {
356
      // check extended functions at full effort
357
24386
      core->checkExtf(e);
358
    }
359
  }
360
}
361
362
8475
bool BVSolverLazy::needsCheckLastEffort()
363
{
364
8475
  CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
365
8475
  if (core)
366
  {
367
8444
    return core->needsCheckLastEffort();
368
  }
369
31
  return false;
370
}
371
372
7372
bool BVSolverLazy::collectModelValues(TheoryModel* m,
373
                                      const std::set<Node>& termSet)
374
{
375
7372
  Assert(!inConflict());
376
7372
  if (options::bitblastMode() == options::BitblastMode::EAGER)
377
  {
378
9
    if (!d_eagerSolver->collectModelInfo(m, true))
379
    {
380
      return false;
381
    }
382
  }
383
13495
  for (unsigned i = 0; i < d_subtheories.size(); ++i)
384
  {
385
13486
    if (d_subtheories[i]->isComplete())
386
    {
387
7363
      return d_subtheories[i]->collectModelValues(m, termSet);
388
    }
389
  }
390
9
  return true;
391
}
392
393
Node BVSolverLazy::getModelValue(TNode var)
394
{
395
  Assert(!inConflict());
396
  for (unsigned i = 0; i < d_subtheories.size(); ++i)
397
  {
398
    if (d_subtheories[i]->isComplete())
399
    {
400
      return d_subtheories[i]->getModelValue(var);
401
    }
402
  }
403
  Unreachable();
404
}
405
406
836351
void BVSolverLazy::propagate(Theory::Effort e)
407
{
408
836351
  Debug("bitvector") << indent() << "BVSolverLazy::propagate()" << std::endl;
409
836351
  if (options::bitblastMode() == options::BitblastMode::EAGER)
410
  {
411
70
    return;
412
  }
413
414
836281
  if (inConflict())
415
  {
416
    return;
417
  }
418
419
  // go through stored propagations
420
836281
  bool ok = true;
421
2206753
  for (; d_literalsToPropagateIndex < d_literalsToPropagate.size() && ok;
422
913648
       d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1)
423
  {
424
913648
    TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex];
425
    // temporary fix for incremental bit-blasting
426
456824
    if (d_state.isSatLiteral(literal))
427
    {
428
864904
      Debug("bitvector::propagate")
429
432452
          << "BVSolverLazy:: propagating " << literal << "\n";
430
432452
      ok = d_im.propagateLit(literal);
431
    }
432
  }
433
434
836281
  if (!ok)
435
  {
436
    Debug("bitvector::propagate")
437
        << indent() << "BVSolverLazy::propagate(): conflict from theory engine"
438
        << std::endl;
439
    setConflict();
440
  }
441
}
442
443
3358
Theory::PPAssertStatus BVSolverLazy::ppAssert(
444
    TrustNode tin, TrustSubstitutionMap& outSubstitutions)
445
{
446
6716
  TNode in = tin.getNode();
447
3358
  switch (in.getKind())
448
  {
449
1168
    case kind::EQUAL:
450
    {
451
1168
      if (in[0].isVar() && d_bv.isLegalElimination(in[0], in[1]))
452
      {
453
234
        ++(d_statistics.d_solveSubstitutions);
454
234
        outSubstitutions.addSubstitutionSolved(in[0], in[1], tin);
455
234
        return Theory::PP_ASSERT_STATUS_SOLVED;
456
      }
457
934
      if (in[1].isVar() && d_bv.isLegalElimination(in[1], in[0]))
458
      {
459
455
        ++(d_statistics.d_solveSubstitutions);
460
455
        outSubstitutions.addSubstitutionSolved(in[1], in[0], tin);
461
455
        return Theory::PP_ASSERT_STATUS_SOLVED;
462
      }
463
932
      Node node = Rewriter::rewrite(in);
464
1490
      if ((node[0].getKind() == kind::BITVECTOR_EXTRACT && node[1].isConst())
465
2417
          || (node[1].getKind() == kind::BITVECTOR_EXTRACT
466
545
              && node[0].isConst()))
467
      {
468
62
        Node extract = node[0].isConst() ? node[1] : node[0];
469
44
        if (extract[0].isVar())
470
        {
471
26
          Node c = node[0].isConst() ? node[0] : node[1];
472
473
26
          unsigned high = utils::getExtractHigh(extract);
474
26
          unsigned low = utils::getExtractLow(extract);
475
26
          unsigned var_bitwidth = utils::getSize(extract[0]);
476
26
          std::vector<Node> children;
477
478
26
          if (low == 0)
479
          {
480
22
            Assert(high != var_bitwidth - 1);
481
22
            unsigned skolem_size = var_bitwidth - high - 1;
482
44
            Node skolem = utils::mkVar(skolem_size);
483
22
            children.push_back(skolem);
484
22
            children.push_back(c);
485
          }
486
4
          else if (high == var_bitwidth - 1)
487
          {
488
4
            unsigned skolem_size = low;
489
8
            Node skolem = utils::mkVar(skolem_size);
490
4
            children.push_back(c);
491
4
            children.push_back(skolem);
492
          }
493
          else
494
          {
495
            unsigned skolem1_size = low;
496
            unsigned skolem2_size = var_bitwidth - high - 1;
497
            Node skolem1 = utils::mkVar(skolem1_size);
498
            Node skolem2 = utils::mkVar(skolem2_size);
499
            children.push_back(skolem2);
500
            children.push_back(c);
501
            children.push_back(skolem1);
502
          }
503
26
          Node concat = utils::mkConcat(children);
504
26
          Assert(utils::getSize(concat) == utils::getSize(extract[0]));
505
26
          if (d_bv.isLegalElimination(extract[0], concat))
506
          {
507
26
            outSubstitutions.addSubstitutionSolved(extract[0], concat, tin);
508
26
            return Theory::PP_ASSERT_STATUS_SOLVED;
509
          }
510
        }
511
453
      }
512
    }
513
453
    break;
514
2190
    case kind::BITVECTOR_ULT:
515
    case kind::BITVECTOR_SLT:
516
    case kind::BITVECTOR_ULE:
517
    case kind::BITVECTOR_SLE:
518
519
    default:
520
      // TODO other predicates
521
2190
      break;
522
  }
523
2643
  return Theory::PP_ASSERT_STATUS_UNSOLVED;
524
}
525
526
302310
TrustNode BVSolverLazy::ppRewrite(TNode t)
527
{
528
302310
  Debug("bv-pp-rewrite") << "BVSolverLazy::ppRewrite " << t << "\n";
529
604620
  Node res = t;
530
604620
  if (options::bitwiseEq() && RewriteRule<BitwiseEq>::applies(t))
531
  {
532
834
    Node result = RewriteRule<BitwiseEq>::run<false>(t);
533
417
    res = Rewriter::rewrite(result);
534
  }
535
301893
  else if (RewriteRule<UltPlusOne>::applies(t))
536
  {
537
108
    Node result = RewriteRule<UltPlusOne>::run<false>(t);
538
54
    res = Rewriter::rewrite(result);
539
  }
540
603678
  else if (res.getKind() == kind::EQUAL
541
905523
           && ((res[0].getKind() == kind::BITVECTOR_PLUS
542
302514
                && RewriteRule<ConcatToMult>::applies(res[1]))
543
318311
               || (res[1].getKind() == kind::BITVECTOR_PLUS
544
302318
                   && RewriteRule<ConcatToMult>::applies(res[0]))))
545
  {
546
12
    Node mult = RewriteRule<ConcatToMult>::applies(res[0])
547
                    ? RewriteRule<ConcatToMult>::run<false>(res[0])
548
12
                    : RewriteRule<ConcatToMult>::run<true>(res[1]);
549
12
    Node factor = mult[0];
550
12
    Node sum = RewriteRule<ConcatToMult>::applies(res[0]) ? res[1] : res[0];
551
12
    Node new_eq = NodeManager::currentNM()->mkNode(kind::EQUAL, sum, mult);
552
12
    Node rewr_eq = RewriteRule<SolveEq>::run<true>(new_eq);
553
6
    if (rewr_eq[0].isVar() || rewr_eq[1].isVar())
554
    {
555
6
      res = Rewriter::rewrite(rewr_eq);
556
    }
557
    else
558
    {
559
      res = t;
560
    }
561
  }
562
301833
  else if (RewriteRule<SignExtendEqConst>::applies(t))
563
  {
564
345
    res = RewriteRule<SignExtendEqConst>::run<false>(t);
565
  }
566
301488
  else if (RewriteRule<ZeroExtendEqConst>::applies(t))
567
  {
568
    res = RewriteRule<ZeroExtendEqConst>::run<false>(t);
569
  }
570
301488
  else if (RewriteRule<NormalizeEqPlusNeg>::applies(t))
571
  {
572
1142
    res = RewriteRule<NormalizeEqPlusNeg>::run<false>(t);
573
  }
574
575
  // if(t.getKind() == kind::EQUAL &&
576
  //    ((t[0].getKind() == kind::BITVECTOR_MULT && t[1].getKind() ==
577
  //    kind::BITVECTOR_PLUS) ||
578
  //     (t[1].getKind() == kind::BITVECTOR_MULT && t[0].getKind() ==
579
  //     kind::BITVECTOR_PLUS))) {
580
  //   // if we have an equality between a multiplication and addition
581
  //   // try to express multiplication in terms of addition
582
  //   Node mult = t[0].getKind() == kind::BITVECTOR_MULT? t[0] : t[1];
583
  //   Node add = t[0].getKind() == kind::BITVECTOR_PLUS? t[0] : t[1];
584
  //   if (RewriteRule<MultSlice>::applies(mult)) {
585
  //     Node new_mult = RewriteRule<MultSlice>::run<false>(mult);
586
  //     Node new_eq =
587
  //     Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::EQUAL,
588
  //     new_mult, add));
589
590
  //     // the simplification can cause the formula to blow up
591
  //     // only apply if formula reduced
592
  //     if (d_subtheoryMap.find(SUB_BITBLAST) != d_subtheoryMap.end()) {
593
  //       BitblastSolver* bv = (BitblastSolver*)d_subtheoryMap[SUB_BITBLAST];
594
  //       uint64_t old_size = bv->computeAtomWeight(t);
595
  //       Assert (old_size);
596
  //       uint64_t new_size = bv->computeAtomWeight(new_eq);
597
  //       double ratio = ((double)new_size)/old_size;
598
  //       if (ratio <= 0.4) {
599
  //         ++(d_statistics.d_numMultSlice);
600
  //         return new_eq;
601
  //       }
602
  //     }
603
604
  //     if (new_eq.getKind() == kind::CONST_BOOLEAN) {
605
  //       ++(d_statistics.d_numMultSlice);
606
  //       return new_eq;
607
  //     }
608
  //   }
609
  // }
610
611
302310
  if (options::bvAbstraction() && t.getType().isBoolean())
612
  {
613
12
    d_abstractionModule->addInputAtom(res);
614
  }
615
302310
  Debug("bv-pp-rewrite") << "to   " << res << "\n";
616
302310
  if (res != t)
617
  {
618
1126
    return TrustNode::mkTrustRewrite(t, res, nullptr);
619
  }
620
301184
  return TrustNode::null();
621
}
622
623
12404
void BVSolverLazy::presolve()
624
{
625
12404
  Debug("bitvector") << "BVSolverLazy::presolve" << std::endl;
626
12404
}
627
628
static int prop_count = 0;
629
630
1971103
bool BVSolverLazy::storePropagation(TNode literal, SubTheory subtheory)
631
{
632
3942206
  Debug("bitvector::propagate") << indent() << d_context->getLevel() << " "
633
1971103
                                << "BVSolverLazy::storePropagation(" << literal
634
1971103
                                << ", " << subtheory << ")" << std::endl;
635
1971103
  prop_count++;
636
637
  // If already in conflict, no more propagation
638
1971103
  if (d_conflict)
639
  {
640
    Debug("bitvector::propagate")
641
        << indent() << "BVSolverLazy::storePropagation(" << literal << ", "
642
        << subtheory << "): already in conflict" << std::endl;
643
    return false;
644
  }
645
646
  // If propagated already, just skip
647
1971103
  PropagatedMap::const_iterator find = d_propagatedBy.find(literal);
648
1971103
  if (find != d_propagatedBy.end())
649
  {
650
719854
    return true;
651
  }
652
  else
653
  {
654
1251249
    bool polarity = literal.getKind() != kind::NOT;
655
2501384
    Node negatedLiteral = polarity ? literal.notNode() : (Node)literal[0];
656
1251249
    find = d_propagatedBy.find(negatedLiteral);
657
1251249
    if (find != d_propagatedBy.end() && (*find).second != subtheory)
658
    {
659
      // Safe to ignore this one, subtheory should produce a conflict
660
1114
      return true;
661
    }
662
663
1250135
    d_propagatedBy[literal] = subtheory;
664
  }
665
666
  // Propagate differs depending on the subtheory
667
  // * bitblaster needs to be left alone until it's done, otherwise it doesn't
668
  //   know how to explain
669
  // * equality engine can propagate eagerly
670
  // TODO(2348): Determine if ok should be set by propagate. If not, remove ok.
671
1250135
  constexpr bool ok = true;
672
1250135
  if (subtheory == SUB_CORE)
673
  {
674
630950
    d_im.propagateLit(literal);
675
    if (!ok)
676
    {
677
      setConflict();
678
    }
679
  }
680
  else
681
  {
682
619185
    d_literalsToPropagate.push_back(literal);
683
  }
684
1250135
  return ok;
685
686
} /* BVSolverLazy::propagate(TNode) */
687
688
18775
void BVSolverLazy::explain(TNode literal, std::vector<TNode>& assumptions)
689
{
690
18775
  Assert(wasPropagatedBySubtheory(literal));
691
18775
  SubTheory sub = getPropagatingSubtheory(literal);
692
18775
  d_subtheoryMap[sub]->explain(literal, assumptions);
693
18775
}
694
695
18775
TrustNode BVSolverLazy::explain(TNode node)
696
{
697
37550
  Debug("bitvector::explain")
698
18775
      << "BVSolverLazy::explain(" << node << ")" << std::endl;
699
37550
  std::vector<TNode> assumptions;
700
701
  // Ask for the explanation
702
18775
  explain(node, assumptions);
703
  // this means that it is something true at level 0
704
37550
  Node explanation;
705
18775
  if (assumptions.size() == 0)
706
  {
707
153
    explanation = utils::mkTrue();
708
  }
709
  else
710
  {
711
    // return the explanation
712
18622
    explanation = utils::mkAnd(assumptions);
713
  }
714
37550
  Debug("bitvector::explain") << "BVSolverLazy::explain(" << node << ") => "
715
18775
                              << explanation << std::endl;
716
18775
  Debug("bitvector::explain") << "BVSolverLazy::explain done. \n";
717
37550
  return TrustNode::mkTrustPropExp(node, explanation, nullptr);
718
}
719
720
39898
void BVSolverLazy::notifySharedTerm(TNode t)
721
{
722
79796
  Debug("bitvector::sharing")
723
39898
      << indent() << "BVSolverLazy::notifySharedTerm(" << t << ")" << std::endl;
724
39898
  d_sharedTermsSet.insert(t);
725
39898
}
726
727
57464
EqualityStatus BVSolverLazy::getEqualityStatus(TNode a, TNode b)
728
{
729
57464
  if (options::bitblastMode() == options::BitblastMode::EAGER)
730
    return EQUALITY_UNKNOWN;
731
57464
  Assert(options::bitblastMode() == options::BitblastMode::LAZY);
732
121310
  for (unsigned i = 0; i < d_subtheories.size(); ++i)
733
  {
734
121196
    EqualityStatus status = d_subtheories[i]->getEqualityStatus(a, b);
735
121196
    if (status != EQUALITY_UNKNOWN)
736
    {
737
57350
      return status;
738
    }
739
  }
740
114
  return EQUALITY_UNKNOWN;
741
  ;
742
}
743
744
498939
void BVSolverLazy::ppStaticLearn(TNode in, NodeBuilder<>& learned)
745
{
746
498939
  if (d_staticLearnCache.find(in) != d_staticLearnCache.end())
747
  {
748
57018
    return;
749
  }
750
441921
  d_staticLearnCache.insert(in);
751
752
441921
  if (in.getKind() == kind::EQUAL)
753
  {
754
65064
    if ((in[0].getKind() == kind::BITVECTOR_PLUS
755
21702
         && in[1].getKind() == kind::BITVECTOR_SHL)
756
108440
        || (in[1].getKind() == kind::BITVECTOR_PLUS
757
21689
            && in[0].getKind() == kind::BITVECTOR_SHL))
758
    {
759
4
      TNode p = in[0].getKind() == kind::BITVECTOR_PLUS ? in[0] : in[1];
760
4
      TNode s = in[0].getKind() == kind::BITVECTOR_PLUS ? in[1] : in[0];
761
762
6
      if (p.getNumChildren() == 2 && p[0].getKind() == kind::BITVECTOR_SHL
763
6
          && p[1].getKind() == kind::BITVECTOR_SHL)
764
      {
765
2
        unsigned size = utils::getSize(s);
766
4
        Node one = utils::mkConst(size, 1u);
767
2
        if (s[0] == one && p[0][0] == one && p[1][0] == one)
768
        {
769
4
          Node zero = utils::mkConst(size, 0u);
770
4
          TNode b = p[0];
771
4
          TNode c = p[1];
772
          // (s : 1 << S) = (b : 1 << B) + (c : 1 << C)
773
4
          Node b_eq_0 = b.eqNode(zero);
774
4
          Node c_eq_0 = c.eqNode(zero);
775
4
          Node b_eq_c = b.eqNode(c);
776
777
          Node dis = NodeManager::currentNM()->mkNode(
778
4
              kind::OR, b_eq_0, c_eq_0, b_eq_c);
779
4
          Node imp = in.impNode(dis);
780
2
          learned << imp;
781
        }
782
      }
783
    }
784
  }
785
420233
  else if (in.getKind() == kind::AND)
786
  {
787
411097
    for (size_t i = 0, N = in.getNumChildren(); i < N; ++i)
788
    {
789
406965
      ppStaticLearn(in[i], learned);
790
    }
791
  }
792
}
793
794
3
bool BVSolverLazy::applyAbstraction(const std::vector<Node>& assertions,
795
                                    std::vector<Node>& new_assertions)
796
{
797
  bool changed =
798
3
      d_abstractionModule->applyAbstraction(assertions, new_assertions);
799
3
  if (changed && options::bitblastMode() == options::BitblastMode::EAGER
800
3
      && options::bitvectorAig())
801
  {
802
    // disable AIG mode
803
    AlwaysAssert(!d_eagerSolver->isInitialized());
804
    d_eagerSolver->turnOffAig();
805
    d_eagerSolver->initialize();
806
  }
807
3
  return changed;
808
}
809
810
12827
void BVSolverLazy::setConflict(Node conflict)
811
{
812
12827
  if (options::bvAbstraction())
813
  {
814
    NodeManager* const nm = NodeManager::currentNM();
815
    Node new_conflict = d_abstractionModule->simplifyConflict(conflict);
816
817
    std::vector<Node> lemmas;
818
    lemmas.push_back(new_conflict);
819
    d_abstractionModule->generalizeConflict(new_conflict, lemmas);
820
    for (unsigned i = 0; i < lemmas.size(); ++i)
821
    {
822
      lemma(nm->mkNode(kind::NOT, lemmas[i]));
823
    }
824
  }
825
12827
  d_conflict = true;
826
12827
  d_conflictNode = conflict;
827
12827
}
828
829
}  // namespace bv
830
}  // namespace theory
831
35641
} /* namespace CVC4 */