GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bv/bv_solver_bitblast.cpp Lines: 1 138 0.7 %
Date: 2021-03-22 Branches: 2 584 0.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file bv_solver_bitblast.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Mathias Preiner, Gereon Kremer
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 Bit-blasting solver
13
 **
14
 ** Bit-blasting solver that supports multiple SAT backends.
15
 **/
16
17
#include "theory/bv/bv_solver_bitblast.h"
18
19
#include "options/bv_options.h"
20
#include "prop/sat_solver_factory.h"
21
#include "smt/smt_statistics_registry.h"
22
#include "theory/bv/theory_bv.h"
23
#include "theory/bv/theory_bv_utils.h"
24
#include "theory/theory_model.h"
25
26
namespace CVC4 {
27
namespace theory {
28
namespace bv {
29
30
BVSolverBitblast::BVSolverBitblast(TheoryState* s,
31
                                   TheoryInferenceManager& inferMgr,
32
                                   ProofNodeManager* pnm)
33
    : BVSolver(*s, inferMgr),
34
      d_bitblaster(new BBSimple(s)),
35
      d_nullRegistrar(new prop::NullRegistrar()),
36
      d_nullContext(new context::Context()),
37
      d_bbFacts(s->getSatContext()),
38
      d_assumptions(s->getSatContext()),
39
      d_invalidateModelCache(s->getSatContext(), true),
40
      d_inSatMode(s->getSatContext(), false),
41
      d_epg(pnm ? new EagerProofGenerator(pnm, s->getUserContext(), "")
42
                : nullptr),
43
      d_factLiteralCache(s->getSatContext()),
44
      d_literalFactCache(s->getSatContext()),
45
      d_propagate(options::bitvectorPropagate())
46
{
47
  if (pnm != nullptr)
48
  {
49
    d_bvProofChecker.registerTo(pnm->getChecker());
50
  }
51
52
  switch (options::bvSatSolver())
53
  {
54
    case options::SatSolverMode::CRYPTOMINISAT:
55
      d_satSolver.reset(prop::SatSolverFactory::createCryptoMinisat(
56
          smtStatisticsRegistry(), "BVSolverBitblast"));
57
      break;
58
    default:
59
      d_satSolver.reset(prop::SatSolverFactory::createCadical(
60
          smtStatisticsRegistry(), "BVSolverBitblast"));
61
  }
62
  d_cnfStream.reset(new prop::CnfStream(d_satSolver.get(),
63
                                        d_nullRegistrar.get(),
64
                                        d_nullContext.get(),
65
                                        nullptr,
66
                                        smt::currentResourceManager()));
67
}
68
69
void BVSolverBitblast::postCheck(Theory::Effort level)
70
{
71
  if (level != Theory::Effort::EFFORT_FULL)
72
  {
73
    /* Do bit-level propagation only if the SAT solver supports it. */
74
    if (!d_propagate || !d_satSolver->setPropagateOnly())
75
    {
76
      return;
77
    }
78
  }
79
80
  /* Process bit-blast queue and store SAT literals. */
81
  while (!d_bbFacts.empty())
82
  {
83
    Node fact = d_bbFacts.front();
84
    d_bbFacts.pop();
85
    /* Bit-blast fact and cache literal. */
86
    if (d_factLiteralCache.find(fact) == d_factLiteralCache.end())
87
    {
88
      d_bitblaster->bbAtom(fact);
89
      Node bb_fact = d_bitblaster->getStoredBBAtom(fact);
90
      d_cnfStream->ensureLiteral(bb_fact);
91
92
      prop::SatLiteral lit = d_cnfStream->getLiteral(bb_fact);
93
      d_factLiteralCache[fact] = lit;
94
      d_literalFactCache[lit] = fact;
95
    }
96
    d_assumptions.push_back(d_factLiteralCache[fact]);
97
  }
98
99
  d_invalidateModelCache.set(true);
100
  std::vector<prop::SatLiteral> assumptions(d_assumptions.begin(),
101
                                            d_assumptions.end());
102
  prop::SatValue val = d_satSolver->solve(assumptions);
103
  d_inSatMode = val == prop::SatValue::SAT_VALUE_TRUE;
104
  Debug("bv-bitblast") << "d_inSatMode: " << d_inSatMode << std::endl;
105
106
  if (val == prop::SatValue::SAT_VALUE_FALSE)
107
  {
108
    std::vector<prop::SatLiteral> unsat_assumptions;
109
    d_satSolver->getUnsatAssumptions(unsat_assumptions);
110
    Assert(unsat_assumptions.size() > 0);
111
112
    std::vector<Node> conflict;
113
    for (const prop::SatLiteral& lit : unsat_assumptions)
114
    {
115
      conflict.push_back(d_literalFactCache[lit]);
116
      Debug("bv-bitblast") << "unsat assumption (" << lit
117
                           << "): " << conflict.back() << std::endl;
118
    }
119
120
    NodeManager* nm = NodeManager::currentNM();
121
    d_im.conflict(nm->mkAnd(conflict), InferenceId::BV_BITBLAST_CONFLICT);
122
  }
123
}
124
125
bool BVSolverBitblast::preNotifyFact(
126
    TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
127
{
128
  d_bbFacts.push_back(fact);
129
  return false;  // Return false to enable equality engine reasoning in Theory.
130
}
131
132
TrustNode BVSolverBitblast::explain(TNode n)
133
{
134
  Debug("bv-bitblast") << "explain called on " << n << std::endl;
135
  return d_im.explainLit(n);
136
}
137
138
bool BVSolverBitblast::collectModelValues(TheoryModel* m,
139
                                          const std::set<Node>& termSet)
140
{
141
  for (const auto& term : termSet)
142
  {
143
    if (!d_bitblaster->isVariable(term))
144
    {
145
      continue;
146
    }
147
148
    Node value = getValueFromSatSolver(term, true);
149
    Assert(value.isConst());
150
    if (!m->assertEquality(term, value, true))
151
    {
152
      return false;
153
    }
154
  }
155
  return true;
156
}
157
158
EqualityStatus BVSolverBitblast::getEqualityStatus(TNode a, TNode b)
159
{
160
  Debug("bv-bitblast") << "getEqualityStatus on " << a << " and " << b
161
                       << std::endl;
162
  if (!d_inSatMode)
163
  {
164
    Debug("bv-bitblast") << EQUALITY_UNKNOWN << std::endl;
165
    return EQUALITY_UNKNOWN;
166
  }
167
  Node value_a = getValue(a);
168
  Node value_b = getValue(b);
169
170
  if (value_a == value_b)
171
  {
172
    Debug("bv-bitblast") << EQUALITY_TRUE_IN_MODEL << std::endl;
173
    return EQUALITY_TRUE_IN_MODEL;
174
  }
175
  Debug("bv-bitblast") << EQUALITY_FALSE_IN_MODEL << std::endl;
176
  return EQUALITY_FALSE_IN_MODEL;
177
}
178
179
Node BVSolverBitblast::getValueFromSatSolver(TNode node, bool initialize)
180
{
181
  if (node.isConst())
182
  {
183
    return node;
184
  }
185
186
  if (!d_bitblaster->hasBBTerm(node))
187
  {
188
    return initialize ? utils::mkConst(utils::getSize(node), 0u) : Node();
189
  }
190
191
  std::vector<Node> bits;
192
  d_bitblaster->getBBTerm(node, bits);
193
  Integer value(0), one(1), zero(0), bit;
194
  for (size_t i = 0, size = bits.size(), j = size - 1; i < size; ++i, --j)
195
  {
196
    if (d_cnfStream->hasLiteral(bits[j]))
197
    {
198
      prop::SatLiteral lit = d_cnfStream->getLiteral(bits[j]);
199
      prop::SatValue val = d_satSolver->modelValue(lit);
200
      bit = val == prop::SatValue::SAT_VALUE_TRUE ? one : zero;
201
    }
202
    else
203
    {
204
      if (!initialize) return Node();
205
      bit = zero;
206
    }
207
    value = value * 2 + bit;
208
  }
209
  return utils::mkConst(bits.size(), value);
210
}
211
212
Node BVSolverBitblast::getValue(TNode node)
213
{
214
  if (d_invalidateModelCache.get())
215
  {
216
    d_modelCache.clear();
217
  }
218
  d_invalidateModelCache.set(false);
219
220
  std::vector<TNode> visit;
221
222
  TNode cur;
223
  visit.push_back(node);
224
  do
225
  {
226
    cur = visit.back();
227
    visit.pop_back();
228
229
    auto it = d_modelCache.find(cur);
230
    if (it != d_modelCache.end() && !it->second.isNull())
231
    {
232
      continue;
233
    }
234
235
    if (d_bitblaster->hasBBTerm(cur))
236
    {
237
      Node value = getValueFromSatSolver(cur, false);
238
      if (value.isConst())
239
      {
240
        d_modelCache[cur] = value;
241
        continue;
242
      }
243
    }
244
    if (Theory::isLeafOf(cur, theory::THEORY_BV))
245
    {
246
      Node value = getValueFromSatSolver(cur, true);
247
      d_modelCache[cur] = value;
248
      continue;
249
    }
250
251
    if (it == d_modelCache.end())
252
    {
253
      visit.push_back(cur);
254
      d_modelCache.emplace(cur, Node());
255
      visit.insert(visit.end(), cur.begin(), cur.end());
256
    }
257
    else if (it->second.isNull())
258
    {
259
      NodeBuilder<> nb(cur.getKind());
260
      if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
261
      {
262
        nb << cur.getOperator();
263
      }
264
265
      std::unordered_map<Node, Node, NodeHashFunction>::iterator iit;
266
      for (const TNode& child : cur)
267
      {
268
        iit = d_modelCache.find(child);
269
        Assert(iit != d_modelCache.end());
270
        Assert(iit->second.isConst());
271
        nb << iit->second;
272
      }
273
      it->second = Rewriter::rewrite(nb.constructNode());
274
    }
275
  } while (!visit.empty());
276
277
  auto it = d_modelCache.find(node);
278
  Assert(it != d_modelCache.end());
279
  return it->second;
280
}
281
282
}  // namespace bv
283
}  // namespace theory
284
26676
}  // namespace CVC4