GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bv/bv_subtheory_bitblast.cpp Lines: 102 145 70.3 %
Date: 2021-03-23 Branches: 186 484 38.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file bv_subtheory_bitblast.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Liana Hadarean, Aina Niemetz, Dejan Jovanovic
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
17
#include "theory/bv/bv_subtheory_bitblast.h"
18
19
#include "decision/decision_attributes.h"
20
#include "options/bv_options.h"
21
#include "options/decision_options.h"
22
#include "smt/smt_statistics_registry.h"
23
#include "theory/bv/abstraction.h"
24
#include "theory/bv/bitblast/lazy_bitblaster.h"
25
#include "theory/bv/bv_quick_check.h"
26
#include "theory/bv/bv_solver_lazy.h"
27
#include "theory/bv/theory_bv_utils.h"
28
29
using namespace std;
30
using namespace CVC4::context;
31
32
namespace CVC4 {
33
namespace theory {
34
namespace bv {
35
36
8956
BitblastSolver::BitblastSolver(context::Context* c, BVSolverLazy* bv)
37
    : SubtheorySolver(c, bv),
38
8956
      d_bitblaster(new TLazyBitblaster(c, bv, "theory::bv::lazy")),
39
      d_bitblastQueue(c),
40
      d_statistics(),
41
      d_validModelCache(c, true),
42
      d_lemmaAtomsQueue(c),
43
8956
      d_useSatPropagation(options::bitvectorPropagate()),
44
      d_abstractionModule(NULL),
45
      d_quickCheck(),
46
26868
      d_quickXplain()
47
{
48
8956
  if (options::bitvectorQuickXplain())
49
  {
50
    d_quickCheck.reset(new BVQuickCheck("bb", bv));
51
    d_quickXplain.reset(new QuickXPlain("bb", d_quickCheck.get()));
52
  }
53
8956
}
54
55
17906
BitblastSolver::~BitblastSolver() {}
56
57
8956
BitblastSolver::Statistics::Statistics()
58
  : d_numCallstoCheck("theory::bv::BitblastSolver::NumCallsToCheck", 0)
59
8956
  , d_numBBLemmas("theory::bv::BitblastSolver::NumTimesLemmasBB", 0)
60
{
61
8956
  smtStatisticsRegistry()->registerStat(&d_numCallstoCheck);
62
8956
  smtStatisticsRegistry()->registerStat(&d_numBBLemmas);
63
8956
}
64
17906
BitblastSolver::Statistics::~Statistics() {
65
8953
  smtStatisticsRegistry()->unregisterStat(&d_numCallstoCheck);
66
8953
  smtStatisticsRegistry()->unregisterStat(&d_numBBLemmas);
67
8953
}
68
69
2
void BitblastSolver::setAbstraction(AbstractionModule* abs) {
70
2
  d_abstractionModule = abs;
71
2
  d_bitblaster->setAbstraction(abs);
72
2
}
73
74
209873
void BitblastSolver::preRegister(TNode node) {
75
577856
  if ((node.getKind() == kind::EQUAL ||
76
302711
       node.getKind() == kind::BITVECTOR_ULT ||
77
289202
       node.getKind() == kind::BITVECTOR_ULE ||
78
274414
       node.getKind() == kind::BITVECTOR_SLT ||
79
709679
       node.getKind() == kind::BITVECTOR_SLE) &&
80
369993
      !d_bitblaster->hasBBAtom(node)) {
81
144210
    CodeTimer weightComputationTime(d_bv->d_statistics.d_weightComputationTimer);
82
72105
    d_bitblastQueue.push_back(node);
83
144210
    if ((options::decisionUseWeight() || options::decisionThreshold() != 0) &&
84
72105
        !node.hasAttribute(decision::DecisionWeightAttr())) {
85
      node.setAttribute(decision::DecisionWeightAttr(),computeAtomWeight(node));
86
    }
87
  }
88
209873
}
89
90
uint64_t BitblastSolver::computeAtomWeight(TNode node) {
91
  NodeSet seen;
92
  return d_bitblaster->computeAtomWeight(node, seen);
93
}
94
95
15034
void BitblastSolver::explain(TNode literal, std::vector<TNode>& assumptions) {
96
15034
  d_bitblaster->explain(literal, assumptions);
97
15034
}
98
99
259876
void BitblastSolver::bitblastQueue() {
100
340556
  while (!d_bitblastQueue.empty()) {
101
161360
    TNode atom = d_bitblastQueue.front();
102
80680
    d_bitblastQueue.pop();
103
80680
    Debug("bv-bitblast-queue") << "BitblastSolver::bitblastQueue (" << atom << ")\n";
104
161384
    if (options::bvAbstraction() &&
105
80704
        d_abstractionModule->isLemmaAtom(atom)) {
106
      // don't bit-blast lemma atoms
107
      continue;
108
    }
109
80680
    if( !utils::isBitblastAtom(atom) ){
110
      continue;
111
    }
112
80680
    Debug("bitblast-queue") << "Bitblasting atom " << atom <<"\n";
113
    {
114
161360
      TimerStat::CodeTimer codeTimer(d_bitblaster->d_statistics.d_bitblastTimer);
115
80680
      d_bitblaster->bbAtom(atom);
116
    }
117
  }
118
179196
}
119
120
179196
bool BitblastSolver::check(Theory::Effort e)
121
{
122
179196
  Debug("bv-bitblast") << "BitblastSolver::check (" << e << ")\n";
123
179196
  Assert(options::bitblastMode() == options::BitblastMode::LAZY);
124
125
179196
  ++(d_statistics.d_numCallstoCheck);
126
127
179196
  Debug("bv-bitblast-debug") << "...process queue" << std::endl;
128
  //// Lazy bit-blasting
129
  // bit-blast enqueued nodes
130
179196
  bitblastQueue();
131
132
  // Processing assertions
133
2222304
  while (!done())
134
  {
135
2050511
    TNode fact = get();
136
1029111
    d_validModelCache = false;
137
1029111
    Debug("bv-bitblast") << "  fact " << fact << ")\n";
138
139
1029111
    if (options::bvAbstraction())
140
    {
141
      // skip atoms that are the result of abstraction lemmas
142
4
      if (d_abstractionModule->isLemmaAtom(fact))
143
      {
144
        d_lemmaAtomsQueue.push_back(fact);
145
        continue;
146
      }
147
    }
148
    // skip facts involving integer equalities (from bv2nat)
149
1029111
    if (!utils::isBitblastAtom(fact))
150
    {
151
154
      continue;
152
    }
153
154
2057914
    if (!d_bv->inConflict()
155
3706416
        && (!d_bv->wasPropagatedBySubtheory(fact)
156
1945083
            || d_bv->getPropagatingSubtheory(fact) != SUB_BITBLAST))
157
    {
158
      // Some atoms have not been bit-blasted yet
159
619545
      d_bitblaster->bbAtom(fact);
160
      // Assert to sat
161
619545
      bool ok = d_bitblaster->assertToSat(fact, d_useSatPropagation);
162
619545
      if (!ok)
163
      {
164
15114
        std::vector<TNode> conflictAtoms;
165
7557
        d_bitblaster->getConflict(conflictAtoms);
166
7557
        setConflict(utils::mkAnd(conflictAtoms));
167
7557
        return false;
168
      }
169
    }
170
  }
171
172
171639
  Debug("bv-bitblast-debug") << "...do propagation" << std::endl;
173
  // We need to ensure we are fully propagated, so propagate now
174
171639
  if (d_useSatPropagation)
175
  {
176
171639
    d_bv->spendResource(ResourceManager::Resource::BvPropagationStep);
177
171639
    bool ok = d_bitblaster->propagate();
178
171639
    if (!ok)
179
    {
180
      std::vector<TNode> conflictAtoms;
181
      d_bitblaster->getConflict(conflictAtoms);
182
      setConflict(utils::mkAnd(conflictAtoms));
183
      return false;
184
    }
185
  }
186
187
  // Solving
188
171639
  Debug("bv-bitblast-debug") << "...do solving" << std::endl;
189
171639
  if (e == Theory::EFFORT_FULL)
190
  {
191
9151
    Assert(!d_bv->inConflict());
192
18302
    Debug("bitvector::bitblaster")
193
9151
        << "BitblastSolver::addAssertions solving. \n";
194
9151
    bool ok = d_bitblaster->solve();
195
9151
    if (!ok)
196
    {
197
9110
      std::vector<TNode> conflictAtoms;
198
4555
      d_bitblaster->getConflict(conflictAtoms);
199
9110
      Node conflict = utils::mkAnd(conflictAtoms);
200
4555
      setConflict(conflict);
201
4555
      return false;
202
    }
203
  }
204
205
167084
  Debug("bv-bitblast-debug") << "...do abs bb" << std::endl;
206
334174
  if (options::bvAbstraction() && e == Theory::EFFORT_FULL
207
167086
      && d_lemmaAtomsQueue.size())
208
  {
209
    // bit-blast lemma atoms
210
    while (!d_lemmaAtomsQueue.empty())
211
    {
212
      TNode lemma_atom = d_lemmaAtomsQueue.front();
213
      d_lemmaAtomsQueue.pop();
214
      if (!utils::isBitblastAtom(lemma_atom))
215
      {
216
        continue;
217
      }
218
      d_bitblaster->bbAtom(lemma_atom);
219
      // Assert to sat and check for conflicts
220
      bool ok = d_bitblaster->assertToSat(lemma_atom, d_useSatPropagation);
221
      if (!ok)
222
      {
223
        std::vector<TNode> conflictAtoms;
224
        d_bitblaster->getConflict(conflictAtoms);
225
        setConflict(utils::mkAnd(conflictAtoms));
226
        return false;
227
      }
228
    }
229
230
    Assert(!d_bv->inConflict());
231
    bool ok = d_bitblaster->solve();
232
    if (!ok)
233
    {
234
      std::vector<TNode> conflictAtoms;
235
      d_bitblaster->getConflict(conflictAtoms);
236
      Node conflict = utils::mkAnd(conflictAtoms);
237
      setConflict(conflict);
238
      ++(d_statistics.d_numBBLemmas);
239
      return false;
240
    }
241
  }
242
243
244
167084
  return true;
245
}
246
247
31866
EqualityStatus BitblastSolver::getEqualityStatus(TNode a, TNode b) {
248
31866
  return d_bitblaster->getEqualityStatus(a, b);
249
}
250
251
3047
bool BitblastSolver::collectModelValues(TheoryModel* m,
252
                                        const std::set<Node>& termSet)
253
{
254
3047
  return d_bitblaster->collectModelValues(m, termSet);
255
}
256
257
Node BitblastSolver::getModelValue(TNode node)
258
{
259
  if (d_bv->d_invalidateModelCache.get()) {
260
    d_bitblaster->invalidateModelCache();
261
  }
262
  d_bv->d_invalidateModelCache.set(false);
263
  Node val = d_bitblaster->getTermModel(node, true);
264
  return val;
265
}
266
267
12112
void BitblastSolver::setConflict(TNode conflict)
268
{
269
24224
  Node final_conflict = conflict;
270
12112
  if (options::bitvectorQuickXplain() &&
271
      conflict.getKind() == kind::AND) {
272
    // std::cout << "Original conflict " << conflict.getNumChildren() << "\n";
273
    final_conflict = d_quickXplain->minimizeConflict(conflict);
274
    //std::cout << "Minimized conflict " << final_conflict.getNumChildren() << "\n";
275
  }
276
12112
  d_bv->setConflict(final_conflict);
277
12112
}
278
279
}/* namespace CVC4::theory::bv */
280
}/* namespace CVC4::theory */
281
26685
}/* namespace CVC4 */