GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/fp/fp_converter.h Lines: 5 5 100.0 %
Date: 2021-03-23 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file fp_converter.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Martin Brain, Mathias Preiner, Aina Niemetz
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 Converts floating-point nodes to bit-vector expressions.
13
 **
14
 ** Uses the symfpu library to convert from floating-point operations to
15
 ** bit-vectors and propositions allowing the theory to be solved by
16
 ** 'bit-blasting'.
17
 **
18
 ** !!! This header is not to be included in any other headers !!!
19
 **/
20
21
#include "cvc4_private.h"
22
23
#ifndef CVC4__THEORY__FP__FP_CONVERTER_H
24
#define CVC4__THEORY__FP__FP_CONVERTER_H
25
26
#include "context/cdhashmap.h"
27
#include "context/cdlist.h"
28
#include "expr/node.h"
29
#include "expr/type_node.h"
30
#include "theory/valuation.h"
31
#include "util/bitvector.h"
32
#include "util/floatingpoint_size.h"
33
#include "util/hash.h"
34
35
#ifdef CVC4_USE_SYMFPU
36
#include "symfpu/core/unpackedFloat.h"
37
#endif
38
39
#ifdef CVC4_SYM_SYMBOLIC_EVAL
40
// This allows debugging of the CVC4 symbolic back-end.
41
// By enabling this and disabling constant folding in the rewriter,
42
// SMT files that have operations on constants will be evaluated
43
// during the encoding step, which means that the expressions
44
// generated by the symbolic back-end can be debugged with gdb.
45
#include "theory/rewriter.h"
46
#endif
47
48
namespace CVC4 {
49
namespace theory {
50
namespace fp {
51
52
/**
53
 * This is a symfpu symbolic "back-end".  It allows the library to be used to
54
 * construct bit-vector expressions that compute floating-point operations.
55
 * This is effectively the glue between symfpu's notion of "signed bit-vector"
56
 * and CVC4's node.
57
 */
58
namespace symfpuSymbolic {
59
60
// Forward declarations of the wrapped types so that traits can be defined early
61
// and used in the implementations
62
class symbolicRoundingMode;
63
class floatingPointTypeInfo;
64
class symbolicProposition;
65
template <bool T>
66
class symbolicBitVector;
67
68
// This is the template parameter for symfpu's templates.
69
class traits
70
{
71
 public:
72
  // The six key types that symfpu uses.
73
  typedef unsigned bwt;
74
  typedef symbolicRoundingMode rm;
75
  typedef floatingPointTypeInfo fpt;
76
  typedef symbolicProposition prop;
77
  typedef symbolicBitVector<true> sbv;
78
  typedef symbolicBitVector<false> ubv;
79
80
  // Give concrete instances (wrapped nodes) for each rounding mode.
81
  static symbolicRoundingMode RNE(void);
82
  static symbolicRoundingMode RNA(void);
83
  static symbolicRoundingMode RTP(void);
84
  static symbolicRoundingMode RTN(void);
85
  static symbolicRoundingMode RTZ(void);
86
87
  // Properties used by symfpu
88
  static void precondition(const bool b);
89
  static void postcondition(const bool b);
90
  static void invariant(const bool b);
91
  static void precondition(const prop &p);
92
  static void postcondition(const prop &p);
93
  static void invariant(const prop &p);
94
};
95
96
// Use the same type names as symfpu.
97
typedef traits::bwt bwt;
98
99
/**
100
 * Wrap the CVC4::Node types so that we can debug issues with this back-end
101
 */
102
1471087
class nodeWrapper : public Node
103
{
104
 protected:
105
/* CVC4_SYM_SYMBOLIC_EVAL is for debugging CVC4 symbolic back-end issues.
106
 * Enable this and disabling constant folding will mean that operations
107
 * that are input with constant args are 'folded' using the symbolic encoding
108
 * allowing them to be traced via GDB.
109
 */
110
#ifdef CVC4_SYM_SYMBOLIC_EVAL
111
  nodeWrapper(const Node &n) : Node(theory::Rewriter::rewrite(n)) {}
112
#else
113
1415831
  nodeWrapper(const Node &n) : Node(n) {}
114
#endif
115
};
116
117
541529
class symbolicProposition : public nodeWrapper
118
{
119
 protected:
120
  bool checkNodeType(const TNode node);
121
122
#ifdef CVC4_USE_SYMFPU
123
  friend ::symfpu::ite<symbolicProposition, symbolicProposition>;  // For ITE
124
#endif
125
126
 public:
127
  symbolicProposition(const Node n);
128
  symbolicProposition(bool v);
129
  symbolicProposition(const symbolicProposition &old);
130
131
  symbolicProposition operator!(void)const;
132
  symbolicProposition operator&&(const symbolicProposition &op) const;
133
  symbolicProposition operator||(const symbolicProposition &op) const;
134
  symbolicProposition operator==(const symbolicProposition &op) const;
135
  symbolicProposition operator^(const symbolicProposition &op) const;
136
};
137
138
1673
class symbolicRoundingMode : public nodeWrapper
139
{
140
 protected:
141
  bool checkNodeType(const TNode n);
142
143
#ifdef CVC4_USE_SYMFPU
144
  friend ::symfpu::ite<symbolicProposition, symbolicRoundingMode>;  // For ITE
145
#endif
146
147
 public:
148
  symbolicRoundingMode(const Node n);
149
  symbolicRoundingMode(const unsigned v);
150
  symbolicRoundingMode(const symbolicRoundingMode &old);
151
152
  symbolicProposition valid(void) const;
153
  symbolicProposition operator==(const symbolicRoundingMode &op) const;
154
};
155
156
// Type function for mapping between types
157
template <bool T>
158
struct signedToLiteralType;
159
160
template <>
161
struct signedToLiteralType<true>
162
{
163
  typedef int literalType;
164
};
165
template <>
166
struct signedToLiteralType<false>
167
{
168
  typedef unsigned int literalType;
169
};
170
171
template <bool isSigned>
172
902021
class symbolicBitVector : public nodeWrapper
173
{
174
 protected:
175
  typedef typename signedToLiteralType<isSigned>::literalType literalType;
176
177
  Node boolNodeToBV(Node node) const;
178
  Node BVToBoolNode(Node node) const;
179
180
  Node fromProposition(Node node) const;
181
  Node toProposition(Node node) const;
182
  bool checkNodeType(const TNode n);
183
  friend symbolicBitVector<!isSigned>;  // To allow conversion between the types
184
185
#ifdef CVC4_USE_SYMFPU
186
  friend ::symfpu::ite<symbolicProposition,
187
                       symbolicBitVector<isSigned> >;  // For ITE
188
#endif
189
190
 public:
191
  symbolicBitVector(const Node n);
192
  symbolicBitVector(const bwt w, const unsigned v);
193
  symbolicBitVector(const symbolicProposition &p);
194
  symbolicBitVector(const symbolicBitVector<isSigned> &old);
195
  symbolicBitVector(const BitVector &old);
196
197
  bwt getWidth(void) const;
198
199
  /*** Constant creation and test ***/
200
  static symbolicBitVector<isSigned> one(const bwt &w);
201
  static symbolicBitVector<isSigned> zero(const bwt &w);
202
  static symbolicBitVector<isSigned> allOnes(const bwt &w);
203
204
  symbolicProposition isAllOnes() const;
205
  symbolicProposition isAllZeros() const;
206
207
  static symbolicBitVector<isSigned> maxValue(const bwt &w);
208
  static symbolicBitVector<isSigned> minValue(const bwt &w);
209
210
  /*** Operators ***/
211
  symbolicBitVector<isSigned> operator<<(
212
      const symbolicBitVector<isSigned> &op) const;
213
  symbolicBitVector<isSigned> operator>>(
214
      const symbolicBitVector<isSigned> &op) const;
215
  symbolicBitVector<isSigned> operator|(
216
      const symbolicBitVector<isSigned> &op) const;
217
  symbolicBitVector<isSigned> operator&(
218
      const symbolicBitVector<isSigned> &op) const;
219
  symbolicBitVector<isSigned> operator+(
220
      const symbolicBitVector<isSigned> &op) const;
221
  symbolicBitVector<isSigned> operator-(
222
      const symbolicBitVector<isSigned> &op) const;
223
  symbolicBitVector<isSigned> operator*(
224
      const symbolicBitVector<isSigned> &op) const;
225
  symbolicBitVector<isSigned> operator/(
226
      const symbolicBitVector<isSigned> &op) const;
227
  symbolicBitVector<isSigned> operator%(
228
      const symbolicBitVector<isSigned> &op) const;
229
  symbolicBitVector<isSigned> operator-(void) const;
230
  symbolicBitVector<isSigned> operator~(void)const;
231
  symbolicBitVector<isSigned> increment() const;
232
  symbolicBitVector<isSigned> decrement() const;
233
  symbolicBitVector<isSigned> signExtendRightShift(
234
      const symbolicBitVector<isSigned> &op) const;
235
236
  /*** Modular operations ***/
237
  // This back-end doesn't do any overflow checking so these are the same as
238
  // other operations
239
  symbolicBitVector<isSigned> modularLeftShift(
240
      const symbolicBitVector<isSigned> &op) const;
241
  symbolicBitVector<isSigned> modularRightShift(
242
      const symbolicBitVector<isSigned> &op) const;
243
  symbolicBitVector<isSigned> modularIncrement() const;
244
  symbolicBitVector<isSigned> modularDecrement() const;
245
  symbolicBitVector<isSigned> modularAdd(
246
      const symbolicBitVector<isSigned> &op) const;
247
  symbolicBitVector<isSigned> modularNegate() const;
248
249
  /*** Comparisons ***/
250
  symbolicProposition operator==(const symbolicBitVector<isSigned> &op) const;
251
  symbolicProposition operator<=(const symbolicBitVector<isSigned> &op) const;
252
  symbolicProposition operator>=(const symbolicBitVector<isSigned> &op) const;
253
  symbolicProposition operator<(const symbolicBitVector<isSigned> &op) const;
254
  symbolicProposition operator>(const symbolicBitVector<isSigned> &op) const;
255
256
  /*** Type conversion ***/
257
  // CVC4 nodes make no distinction between signed and unsigned, thus these are
258
  // trivial
259
  symbolicBitVector<true> toSigned(void) const;
260
  symbolicBitVector<false> toUnsigned(void) const;
261
262
  /*** Bit hacks ***/
263
  symbolicBitVector<isSigned> extend(bwt extension) const;
264
  symbolicBitVector<isSigned> contract(bwt reduction) const;
265
  symbolicBitVector<isSigned> resize(bwt newSize) const;
266
  symbolicBitVector<isSigned> matchWidth(
267
      const symbolicBitVector<isSigned> &op) const;
268
  symbolicBitVector<isSigned> append(
269
      const symbolicBitVector<isSigned> &op) const;
270
271
  // Inclusive of end points, thus if the same, extracts just one bit
272
  symbolicBitVector<isSigned> extract(bwt upper, bwt lower) const;
273
};
274
275
// Use the same type information as the literal back-end but add an interface to
276
// TypeNodes for convenience.
277
class floatingPointTypeInfo : public FloatingPointSize
278
{
279
 public:
280
  floatingPointTypeInfo(const TypeNode t);
281
  floatingPointTypeInfo(unsigned exp, unsigned sig);
282
  floatingPointTypeInfo(const floatingPointTypeInfo &old);
283
284
  TypeNode getTypeNode(void) const;
285
};
286
}
287
288
/**
289
 * This class uses SymFPU to convert an expression containing floating-point
290
 * kinds and operations into a logically equivalent form with bit-vector
291
 * operations replacing the floating-point ones.  It also has a getValue method
292
 * to produce an expression which will reconstruct the value of the
293
 * floating-point terms from a valuation.
294
 *
295
 * Internally it caches all of the unpacked floats so that unnecessary packing
296
 * and unpacking operations are avoided and to make best use of structural
297
 * sharing.
298
 */
299
class FpConverter
300
{
301
 public:
302
  /** Constructor. */
303
  FpConverter(context::UserContext*);
304
  /** Destructor. */
305
  ~FpConverter();
306
307
  /** Adds a node to the conversion, returns the converted node */
308
  Node convert(TNode);
309
310
  /** Gives the node representing the value of a given variable */
311
  Node getValue(Valuation&, TNode);
312
313
  context::CDList<Node> d_additionalAssertions;
314
315
 protected:
316
#ifdef CVC4_USE_SYMFPU
317
  typedef symfpuSymbolic::traits traits;
318
  typedef ::symfpu::unpackedFloat<symfpuSymbolic::traits> uf;
319
  typedef symfpuSymbolic::traits::rm rm;
320
  typedef symfpuSymbolic::traits::fpt fpt;
321
  typedef symfpuSymbolic::traits::prop prop;
322
  typedef symfpuSymbolic::traits::ubv ubv;
323
  typedef symfpuSymbolic::traits::sbv sbv;
324
325
  typedef context::CDHashMap<Node, uf, NodeHashFunction> fpMap;
326
  typedef context::CDHashMap<Node, rm, NodeHashFunction> rmMap;
327
  typedef context::CDHashMap<Node, prop, NodeHashFunction> boolMap;
328
  typedef context::CDHashMap<Node, ubv, NodeHashFunction> ubvMap;
329
  typedef context::CDHashMap<Node, sbv, NodeHashFunction> sbvMap;
330
331
  fpMap d_fpMap;
332
  rmMap d_rmMap;
333
  boolMap d_boolMap;
334
  ubvMap d_ubvMap;
335
  sbvMap d_sbvMap;
336
337
  /* These functions take a symfpu object and convert it to a node.
338
   * These should ensure that constant folding it will give a
339
   * constant of the right type.
340
   */
341
342
  Node ufToNode(const fpt &, const uf &) const;
343
  Node rmToNode(const rm &) const;
344
  Node propToNode(const prop &) const;
345
  Node ubvToNode(const ubv &) const;
346
  Node sbvToNode(const sbv &) const;
347
348
  /* Creates the relevant components for a variable */
349
  uf buildComponents(TNode current);
350
#endif
351
};
352
353
}  // namespace fp
354
}  // namespace theory
355
}  // namespace CVC4
356
357
#endif /* CVC4__THEORY__FP__THEORY_FP_H */