GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bv/bitblast/bitblaster.h Lines: 102 107 95.3 %
Date: 2021-03-22 Branches: 107 262 40.8 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file bitblaster.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Liana Hadarean, Mathias Preiner, Alex Ozdemir
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 Wrapper around the SAT solver used for bitblasting
13
 **
14
 ** Wrapper around the SAT solver used for bitblasting.
15
 **/
16
17
#include "cvc4_private.h"
18
19
#ifndef CVC4__THEORY__BV__BITBLAST__BITBLASTER_H
20
#define CVC4__THEORY__BV__BITBLAST__BITBLASTER_H
21
22
#include <unordered_map>
23
#include <unordered_set>
24
#include <vector>
25
26
#include "expr/node.h"
27
#include "prop/bv_sat_solver_notify.h"
28
#include "prop/cnf_stream.h"
29
#include "prop/registrar.h"
30
#include "prop/sat_solver.h"
31
#include "prop/sat_solver_types.h"
32
#include "smt/smt_engine_scope.h"
33
#include "theory/bv/bitblast/bitblast_strategies_template.h"
34
#include "theory/theory.h"
35
#include "theory/valuation.h"
36
#include "util/resource_manager.h"
37
38
namespace CVC4 {
39
namespace theory {
40
namespace bv {
41
42
typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
43
typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
44
45
/**
46
 * The Bitblaster that manages the mapping between Nodes
47
 * and their bitwise definition
48
 *
49
 */
50
51
template <class T>
52
class TBitblaster
53
{
54
 protected:
55
  typedef std::vector<T> Bits;
56
  typedef std::unordered_map<Node, Bits, NodeHashFunction> TermDefMap;
57
  typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
58
  typedef std::unordered_map<Node, Node, NodeHashFunction> ModelCache;
59
60
  typedef void (*TermBBStrategy)(TNode, Bits&, TBitblaster<T>*);
61
  typedef T (*AtomBBStrategy)(TNode, TBitblaster<T>*);
62
63
  // caches and mappings
64
  TermDefMap d_termCache;
65
  ModelCache d_modelCache;
66
  // sat solver used for bitblasting and associated CnfStream
67
  std::unique_ptr<context::Context> d_nullContext;
68
  std::unique_ptr<prop::CnfStream> d_cnfStream;
69
70
  void initAtomBBStrategies();
71
  void initTermBBStrategies();
72
73
 protected:
74
  /// function tables for the various bitblasting strategies indexed by node
75
  /// kind
76
  TermBBStrategy d_termBBStrategies[kind::LAST_KIND];
77
  AtomBBStrategy d_atomBBStrategies[kind::LAST_KIND];
78
  virtual Node getModelFromSatSolver(TNode node, bool fullModel) = 0;
79
  virtual prop::SatSolver* getSatSolver() = 0;
80
81
82
 public:
83
  TBitblaster();
84
8992
  virtual ~TBitblaster() {}
85
  virtual void bbAtom(TNode node) = 0;
86
  virtual void bbTerm(TNode node, Bits& bits) = 0;
87
  virtual void makeVariable(TNode node, Bits& bits) = 0;
88
  virtual T getBBAtom(TNode atom) const = 0;
89
  virtual bool hasBBAtom(TNode atom) const = 0;
90
  virtual void storeBBAtom(TNode atom, T atom_bb) = 0;
91
92
  bool hasBBTerm(TNode node) const;
93
  void getBBTerm(TNode node, Bits& bits) const;
94
  virtual void storeBBTerm(TNode term, const Bits& bits);
95
96
  /**
97
   * Return a constant representing the value of a in the  model.
98
   * If fullModel is true set unconstrained bits to 0. If not return
99
   * NullNode() for a fully or partially unconstrained.
100
   *
101
   */
102
  Node getTermModel(TNode node, bool fullModel);
103
  void invalidateModelCache();
104
};
105
106
42
class MinisatEmptyNotify : public prop::BVSatSolverNotify
107
{
108
 public:
109
21
  MinisatEmptyNotify() {}
110
  bool notify(prop::SatLiteral lit) override { return true; }
111
  void notify(prop::SatClause& clause) override {}
112
19
  void spendResource(ResourceManager::Resource r) override
113
  {
114
19
    smt::currentResourceManager()->spendResource(r);
115
19
  }
116
117
3326
  void safePoint(ResourceManager::Resource r) override {}
118
};
119
120
// Bitblaster implementation
121
122
template <class T>
123
8995
void TBitblaster<T>::initAtomBBStrategies()
124
{
125
2914380
  for (int i = 0; i < kind::LAST_KIND; ++i)
126
  {
127
2905385
    d_atomBBStrategies[i] = UndefinedAtomBBStrategy<T>;
128
  }
129
  /// setting default bb strategies for atoms
130
8995
  d_atomBBStrategies[kind::EQUAL] = DefaultEqBB<T>;
131
8995
  d_atomBBStrategies[kind::BITVECTOR_ULT] = DefaultUltBB<T>;
132
8995
  d_atomBBStrategies[kind::BITVECTOR_ULE] = DefaultUleBB<T>;
133
8995
  d_atomBBStrategies[kind::BITVECTOR_UGT] = DefaultUgtBB<T>;
134
8995
  d_atomBBStrategies[kind::BITVECTOR_UGE] = DefaultUgeBB<T>;
135
8995
  d_atomBBStrategies[kind::BITVECTOR_SLT] = DefaultSltBB<T>;
136
8995
  d_atomBBStrategies[kind::BITVECTOR_SLE] = DefaultSleBB<T>;
137
8995
  d_atomBBStrategies[kind::BITVECTOR_SGT] = DefaultSgtBB<T>;
138
8995
  d_atomBBStrategies[kind::BITVECTOR_SGE] = DefaultSgeBB<T>;
139
8995
}
140
141
template <class T>
142
8995
void TBitblaster<T>::initTermBBStrategies()
143
{
144
2914380
  for (int i = 0; i < kind::LAST_KIND; ++i)
145
  {
146
2905385
    d_termBBStrategies[i] = DefaultVarBB<T>;
147
  }
148
  /// setting default bb strategies for terms:
149
8995
  d_termBBStrategies[kind::CONST_BITVECTOR] = DefaultConstBB<T>;
150
8995
  d_termBBStrategies[kind::BITVECTOR_NOT] = DefaultNotBB<T>;
151
8995
  d_termBBStrategies[kind::BITVECTOR_CONCAT] = DefaultConcatBB<T>;
152
8995
  d_termBBStrategies[kind::BITVECTOR_AND] = DefaultAndBB<T>;
153
8995
  d_termBBStrategies[kind::BITVECTOR_OR] = DefaultOrBB<T>;
154
8995
  d_termBBStrategies[kind::BITVECTOR_XOR] = DefaultXorBB<T>;
155
8995
  d_termBBStrategies[kind::BITVECTOR_XNOR] = DefaultXnorBB<T>;
156
8995
  d_termBBStrategies[kind::BITVECTOR_NAND] = DefaultNandBB<T>;
157
8995
  d_termBBStrategies[kind::BITVECTOR_NOR] = DefaultNorBB<T>;
158
8995
  d_termBBStrategies[kind::BITVECTOR_COMP] = DefaultCompBB<T>;
159
8995
  d_termBBStrategies[kind::BITVECTOR_MULT] = DefaultMultBB<T>;
160
8995
  d_termBBStrategies[kind::BITVECTOR_PLUS] = DefaultPlusBB<T>;
161
8995
  d_termBBStrategies[kind::BITVECTOR_SUB] = DefaultSubBB<T>;
162
8995
  d_termBBStrategies[kind::BITVECTOR_NEG] = DefaultNegBB<T>;
163
8995
  d_termBBStrategies[kind::BITVECTOR_UDIV] = DefaultUdivBB<T>;
164
8995
  d_termBBStrategies[kind::BITVECTOR_UREM] = DefaultUremBB<T>;
165
8995
  d_termBBStrategies[kind::BITVECTOR_SDIV] = UndefinedTermBBStrategy<T>;
166
8995
  d_termBBStrategies[kind::BITVECTOR_SREM] = UndefinedTermBBStrategy<T>;
167
8995
  d_termBBStrategies[kind::BITVECTOR_SMOD] = UndefinedTermBBStrategy<T>;
168
8995
  d_termBBStrategies[kind::BITVECTOR_SHL] = DefaultShlBB<T>;
169
8995
  d_termBBStrategies[kind::BITVECTOR_LSHR] = DefaultLshrBB<T>;
170
8995
  d_termBBStrategies[kind::BITVECTOR_ASHR] = DefaultAshrBB<T>;
171
8995
  d_termBBStrategies[kind::BITVECTOR_ULTBV] = DefaultUltbvBB<T>;
172
8995
  d_termBBStrategies[kind::BITVECTOR_SLTBV] = DefaultSltbvBB<T>;
173
8995
  d_termBBStrategies[kind::BITVECTOR_ITE] = DefaultIteBB<T>;
174
8995
  d_termBBStrategies[kind::BITVECTOR_EXTRACT] = DefaultExtractBB<T>;
175
8995
  d_termBBStrategies[kind::BITVECTOR_REPEAT] = DefaultRepeatBB<T>;
176
8995
  d_termBBStrategies[kind::BITVECTOR_ZERO_EXTEND] = DefaultZeroExtendBB<T>;
177
8995
  d_termBBStrategies[kind::BITVECTOR_SIGN_EXTEND] = DefaultSignExtendBB<T>;
178
8995
  d_termBBStrategies[kind::BITVECTOR_ROTATE_RIGHT] = DefaultRotateRightBB<T>;
179
8995
  d_termBBStrategies[kind::BITVECTOR_ROTATE_LEFT] = DefaultRotateLeftBB<T>;
180
8995
}
181
182
template <class T>
183
8995
TBitblaster<T>::TBitblaster()
184
    : d_termCache(),
185
      d_modelCache(),
186
8995
      d_nullContext(new context::Context()),
187
17990
      d_cnfStream()
188
{
189
8995
  initAtomBBStrategies();
190
8995
  initTermBBStrategies();
191
8995
}
192
193
template <class T>
194
567002
bool TBitblaster<T>::hasBBTerm(TNode node) const
195
{
196
567002
  return d_termCache.find(node) != d_termCache.end();
197
}
198
template <class T>
199
226264
void TBitblaster<T>::getBBTerm(TNode node, Bits& bits) const
200
{
201
226264
  Assert(hasBBTerm(node));
202
226264
  bits = d_termCache.find(node)->second;
203
226264
}
204
205
template <class T>
206
void TBitblaster<T>::storeBBTerm(TNode node, const Bits& bits)
207
{
208
  d_termCache.insert(std::make_pair(node, bits));
209
}
210
211
template <class T>
212
100
void TBitblaster<T>::invalidateModelCache()
213
{
214
100
  d_modelCache.clear();
215
100
}
216
217
template <class T>
218
58346
Node TBitblaster<T>::getTermModel(TNode node, bool fullModel)
219
{
220
58346
  if (d_modelCache.find(node) != d_modelCache.end()) return d_modelCache[node];
221
222
9870
  if (node.isConst()) return node;
223
224
1216
  Node value = getModelFromSatSolver(node, false);
225
608
  if (!value.isNull())
226
  {
227
562
    Debug("bv-equality-status")
228
281
        << "TLazyBitblaster::getTermModel from SatSolver" << node << " => "
229
281
        << value << "\n";
230
281
    d_modelCache[node] = value;
231
281
    Assert(value.isConst());
232
281
    return value;
233
  }
234
235
327
  if (Theory::isLeafOf(node, theory::THEORY_BV))
236
  {
237
    // if it is a leaf may ask for fullModel
238
135
    value = getModelFromSatSolver(node, true);
239
270
    Debug("bv-equality-status") << "TLazyBitblaster::getTermModel from VarValue"
240
135
                                << node << " => " << value << "\n";
241
135
    Assert((fullModel && !value.isNull() && value.isConst()) || !fullModel);
242
135
    if (!value.isNull())
243
    {
244
135
      d_modelCache[node] = value;
245
    }
246
135
    return value;
247
  }
248
192
  Assert(node.getType().isBitVector());
249
250
384
  NodeBuilder<> nb(node.getKind());
251
192
  if (node.getMetaKind() == kind::metakind::PARAMETERIZED)
252
  {
253
48
    nb << node.getOperator();
254
  }
255
256
470
  for (unsigned i = 0; i < node.getNumChildren(); ++i)
257
  {
258
278
    nb << getTermModel(node[i], fullModel);
259
  }
260
192
  value = nb;
261
192
  value = Rewriter::rewrite(value);
262
192
  Assert(value.isConst());
263
192
  d_modelCache[node] = value;
264
384
  Debug("bv-term-model") << "TLazyBitblaster::getTermModel Building Value"
265
192
                         << node << " => " << value << "\n";
266
192
  return value;
267
}
268
269
}  // namespace bv
270
}  // namespace theory
271
}  // namespace CVC4
272
273
#endif /* CVC4__THEORY__BV__BITBLAST__BITBLASTER_H */