GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bv/bitblast/eager_bitblaster.cpp Lines: 118 131 90.1 %
Date: 2021-03-22 Branches: 199 569 35.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file eager_bitblaster.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Liana Hadarean, Mathias Preiner, Andres Noetzli
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
13
 **
14
 ** Bitblaster for the eager bv solver.
15
 **/
16
17
#include "theory/bv/bitblast/eager_bitblaster.h"
18
19
#include "cvc4_private.h"
20
#include "options/bv_options.h"
21
#include "options/smt_options.h"
22
#include "prop/cnf_stream.h"
23
#include "prop/sat_solver_factory.h"
24
#include "smt/smt_engine.h"
25
#include "smt/smt_statistics_registry.h"
26
#include "theory/bv/bv_solver_lazy.h"
27
#include "theory/bv/theory_bv.h"
28
#include "theory/theory_model.h"
29
30
namespace CVC4 {
31
namespace theory {
32
namespace bv {
33
34
31
EagerBitblaster::EagerBitblaster(BVSolverLazy* theory_bv, context::Context* c)
35
    : TBitblaster<Node>(),
36
      d_context(c),
37
      d_satSolver(),
38
31
      d_bitblastingRegistrar(new BitblastingRegistrar(this)),
39
      d_bv(theory_bv),
40
      d_bbAtoms(),
41
      d_variables(),
42
62
      d_notify()
43
{
44
31
  prop::SatSolver *solver = nullptr;
45
90
  switch (options::bvSatSolver())
46
  {
47
21
    case options::SatSolverMode::MINISAT:
48
    {
49
      prop::BVSatSolverInterface* minisat =
50
42
          prop::SatSolverFactory::createMinisat(
51
21
              d_nullContext.get(), smtStatisticsRegistry(), "EagerBitblaster");
52
21
      d_notify.reset(new MinisatEmptyNotify());
53
21
      minisat->setNotify(d_notify.get());
54
21
      solver = minisat;
55
21
      break;
56
    }
57
3
    case options::SatSolverMode::CADICAL:
58
3
      solver = prop::SatSolverFactory::createCadical(smtStatisticsRegistry(),
59
                                                     "EagerBitblaster");
60
3
      break;
61
7
    case options::SatSolverMode::CRYPTOMINISAT:
62
7
      solver = prop::SatSolverFactory::createCryptoMinisat(
63
          smtStatisticsRegistry(), "EagerBitblaster");
64
7
      break;
65
    case options::SatSolverMode::KISSAT:
66
      solver = prop::SatSolverFactory::createKissat(smtStatisticsRegistry(),
67
                                                    "EagerBitblaster");
68
      break;
69
    default: Unreachable() << "Unknown SAT solver type";
70
  }
71
31
  d_satSolver.reset(solver);
72
31
  ResourceManager* rm = smt::currentResourceManager();
73
93
  d_cnfStream.reset(new prop::CnfStream(d_satSolver.get(),
74
31
                                        d_bitblastingRegistrar.get(),
75
31
                                        d_nullContext.get(),
76
                                        nullptr,
77
                                        rm,
78
                                        prop::FormulaLitPolicy::INTERNAL,
79
31
                                        "EagerBitblaster"));
80
31
}
81
82
62
EagerBitblaster::~EagerBitblaster() {}
83
84
592
void EagerBitblaster::bbFormula(TNode node)
85
{
86
  /* For incremental eager solving we assume formulas at context levels > 1. */
87
592
  if (options::incrementalSolving() && d_context->getLevel() > 1)
88
  {
89
24
    d_cnfStream->ensureLiteral(node);
90
  }
91
  else
92
  {
93
568
    d_cnfStream->convertAndAssert(node, false, false);
94
  }
95
592
}
96
97
/**
98
 * Bitblasts the atom, assigns it a marker literal, adding it to the SAT solver
99
 * NOTE: duplicate clauses are not detected because of marker literal
100
 * @param node the atom to be bitblasted
101
 *
102
 */
103
2598
void EagerBitblaster::bbAtom(TNode node)
104
{
105
2598
  node = node.getKind() == kind::NOT ? node[0] : node;
106
5196
  if (node.getKind() == kind::BITVECTOR_BITOF
107
5196
      || node.getKind() == kind::CONST_BOOLEAN || hasBBAtom(node))
108
  {
109
1935
    return;
110
  }
111
112
663
  Debug("bitvector-bitblast") << "Bitblasting node " << node << "\n";
113
114
  // the bitblasted definition of the atom
115
1326
  Node normalized = Rewriter::rewrite(node);
116
  Node atom_bb =
117
663
      normalized.getKind() != kind::CONST_BOOLEAN
118
663
          ? d_atomBBStrategies[normalized.getKind()](normalized, this)
119
1989
          : normalized;
120
121
663
  atom_bb = Rewriter::rewrite(atom_bb);
122
123
  // asserting that the atom is true iff the definition holds
124
  Node atom_definition =
125
1326
      NodeManager::currentNM()->mkNode(kind::EQUAL, node, atom_bb);
126
127
663
  AlwaysAssert(options::bitblastMode() == options::BitblastMode::EAGER);
128
663
  storeBBAtom(node, atom_bb);
129
663
  d_cnfStream->convertAndAssert(atom_definition, false, false);
130
}
131
132
663
void EagerBitblaster::storeBBAtom(TNode atom, Node atom_bb) {
133
663
  d_bbAtoms.insert(atom);
134
663
}
135
136
669
void EagerBitblaster::storeBBTerm(TNode node, const Bits& bits) {
137
669
  d_termCache.insert(std::make_pair(node, bits));
138
669
}
139
140
663
bool EagerBitblaster::hasBBAtom(TNode atom) const {
141
663
  return d_bbAtoms.find(atom) != d_bbAtoms.end();
142
}
143
144
1989
void EagerBitblaster::bbTerm(TNode node, Bits& bits) {
145
1989
  Assert(node.getType().isBitVector());
146
147
1989
  if (hasBBTerm(node)) {
148
1320
    getBBTerm(node, bits);
149
1320
    return;
150
  }
151
152
669
  d_bv->spendResource(ResourceManager::Resource::BitblastStep);
153
669
  Debug("bitvector-bitblast") << "Bitblasting node " << node << "\n";
154
155
669
  d_termBBStrategies[node.getKind()](node, bits, this);
156
157
669
  Assert(bits.size() == utils::getSize(node));
158
159
669
  storeBBTerm(node, bits);
160
}
161
162
271
void EagerBitblaster::makeVariable(TNode var, Bits& bits) {
163
271
  Assert(bits.size() == 0);
164
2183
  for (unsigned i = 0; i < utils::getSize(var); ++i) {
165
1912
    bits.push_back(utils::mkBitOf(var, i));
166
  }
167
271
  d_variables.insert(var);
168
271
}
169
170
Node EagerBitblaster::getBBAtom(TNode node) const { return node; }
171
172
/**
173
 * Calls the solve method for the Sat Solver.
174
 *
175
 * @return true for sat, and false for unsat
176
 */
177
178
25
bool EagerBitblaster::solve() {
179
25
  if (Trace.isOn("bitvector")) {
180
    Trace("bitvector") << "EagerBitblaster::solve(). \n";
181
  }
182
25
  Debug("bitvector") << "EagerBitblaster::solve(). \n";
183
  // TODO: clear some memory
184
  // if (something) {
185
  //   NodeManager* nm= NodeManager::currentNM();
186
  //   Rewriter::garbageCollect();
187
  //   nm->reclaimZombiesUntil(options::zombieHuntThreshold());
188
  // }
189
25
  return prop::SAT_VALUE_TRUE == d_satSolver->solve();
190
}
191
192
24
bool EagerBitblaster::solve(const std::vector<Node>& assumptions)
193
{
194
48
  std::vector<prop::SatLiteral> assumpts;
195
42
  for (const Node& assumption : assumptions)
196
  {
197
18
    Assert(d_cnfStream->hasLiteral(assumption));
198
18
    assumpts.push_back(d_cnfStream->getLiteral(assumption));
199
  }
200
48
  return prop::SAT_VALUE_TRUE == d_satSolver->solve(assumpts);
201
}
202
203
/**
204
 * Returns the value a is currently assigned to in the SAT solver
205
 * or null if the value is completely unassigned.
206
 *
207
 * @param a
208
 * @param fullModel whether to create a "full model," i.e., add
209
 * constants to equivalence classes that don't already have them
210
 *
211
 * @return
212
 */
213
21
Node EagerBitblaster::getModelFromSatSolver(TNode a, bool fullModel) {
214
21
  if (!hasBBTerm(a)) {
215
    return fullModel ? utils::mkConst(utils::getSize(a), 0u) : Node();
216
  }
217
218
42
  Bits bits;
219
21
  getBBTerm(a, bits);
220
42
  Integer value(0);
221
357
  for (int i = bits.size() - 1; i >= 0; --i) {
222
    prop::SatValue bit_value;
223
336
    if (d_cnfStream->hasLiteral(bits[i])) {
224
336
      prop::SatLiteral bit = d_cnfStream->getLiteral(bits[i]);
225
336
      bit_value = d_satSolver->value(bit);
226
336
      Assert(bit_value != prop::SAT_VALUE_UNKNOWN);
227
    } else {
228
      if (!fullModel) return Node();
229
      // unconstrained bits default to false
230
      bit_value = prop::SAT_VALUE_FALSE;
231
    }
232
    Integer bit_int =
233
672
        bit_value == prop::SAT_VALUE_TRUE ? Integer(1) : Integer(0);
234
336
    value = value * 2 + bit_int;
235
  }
236
21
  return utils::mkConst(bits.size(), value);
237
}
238
239
9
bool EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel)
240
{
241
9
  NodeManager* nm = NodeManager::currentNM();
242
243
  // Collect the values for the bit-vector variables
244
9
  TNodeSet::iterator it = d_variables.begin();
245
51
  for (; it != d_variables.end(); ++it) {
246
42
    TNode var = *it;
247
63
    if (d_bv->isLeaf(var) || isSharedTerm(var) ||
248
21
        (var.isVar() && var.getType().isBoolean())) {
249
      // only shared terms could not have been bit-blasted
250
21
      Assert(hasBBTerm(var) || isSharedTerm(var));
251
252
42
      Node const_value = getModelFromSatSolver(var, true);
253
254
21
      if (const_value != Node()) {
255
42
        Debug("bitvector-model")
256
21
            << "EagerBitblaster::collectModelInfo (assert (= " << var << " "
257
21
            << const_value << "))\n";
258
21
        if (!m->assertEquality(var, const_value, true))
259
        {
260
          return false;
261
        }
262
      }
263
    }
264
  }
265
266
  // Collect the values for the Boolean variables
267
18
  std::vector<TNode> vars;
268
9
  d_cnfStream->getBooleanVariables(vars);
269
13
  for (TNode var : vars)
270
  {
271
4
    Assert(d_cnfStream->hasLiteral(var));
272
4
    prop::SatLiteral bit = d_cnfStream->getLiteral(var);
273
4
    prop::SatValue value = d_satSolver->value(bit);
274
4
    Assert(value != prop::SAT_VALUE_UNKNOWN);
275
8
    if (!m->assertEquality(
276
8
            var, nm->mkConst(value == prop::SAT_VALUE_TRUE), true))
277
    {
278
      return false;
279
    }
280
  }
281
9
  return true;
282
}
283
284
bool EagerBitblaster::isSharedTerm(TNode node) {
285
  return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end();
286
}
287
288
289
}  // namespace bv
290
}  // namespace theory
291
26735
}  // namespace CVC4