1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Aina Niemetz, Martin Brain, Andres Noetzli |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
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. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* SymFPU glue code for floating-point values. |
14 |
|
* |
15 |
|
* !!! This header is only to be included in floating-point literal headers !!! |
16 |
|
* |
17 |
|
* This is a symfpu literal "back-end". It allows the library to be used as |
18 |
|
* an arbitrary precision floating-point implementation. This is effectively |
19 |
|
* the glue between symfpu's notion of "signed bit-vector" and cvc5's |
20 |
|
* BitVector. |
21 |
|
*/ |
22 |
|
|
23 |
|
#include "cvc5_private.h" |
24 |
|
|
25 |
|
#ifndef CVC5__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_TRAITS_H |
26 |
|
#define CVC5__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_TRAITS_H |
27 |
|
|
28 |
|
// clang-format off |
29 |
|
#if 1 |
30 |
|
// clang-format on |
31 |
|
|
32 |
|
#include "util/bitvector.h" |
33 |
|
#include "util/floatingpoint_size.h" |
34 |
|
#include "util/roundingmode.h" |
35 |
|
|
36 |
|
#include <symfpu/core/unpackedFloat.h> |
37 |
|
|
38 |
|
/* -------------------------------------------------------------------------- */ |
39 |
|
|
40 |
|
namespace cvc5 { |
41 |
|
namespace symfpuLiteral { |
42 |
|
|
43 |
|
/** |
44 |
|
* Forward declaration of wrapper so that traits can be defined early and so |
45 |
|
* used in the implementation of wrappedBitVector. |
46 |
|
*/ |
47 |
|
template <bool T> |
48 |
|
class wrappedBitVector; |
49 |
|
|
50 |
|
using Cvc5BitWidth = uint32_t; |
51 |
|
using Cvc5Prop = bool; |
52 |
|
using Cvc5RM = ::cvc5::RoundingMode; |
53 |
|
using Cvc5FPSize = ::cvc5::FloatingPointSize; |
54 |
|
using Cvc5UnsignedBitVector = wrappedBitVector<false>; |
55 |
|
using Cvc5SignedBitVector = wrappedBitVector<true>; |
56 |
|
|
57 |
|
/** |
58 |
|
* This is the template parameter for symfpu's templates. |
59 |
|
*/ |
60 |
|
class traits |
61 |
|
{ |
62 |
|
public: |
63 |
|
/** The six key types that symfpu uses. */ |
64 |
|
using bwt = Cvc5BitWidth; // bit-width type |
65 |
|
using prop = Cvc5Prop; // boolean type |
66 |
|
using rm = Cvc5RM; // rounding-mode type |
67 |
|
using fpt = Cvc5FPSize; // floating-point format type |
68 |
|
using ubv = Cvc5UnsignedBitVector; // unsigned bit-vector type |
69 |
|
using sbv = Cvc5SignedBitVector; // signed bit-vector type |
70 |
|
|
71 |
|
/** Give concrete instances of each rounding mode, mainly for comparisons. */ |
72 |
|
static rm RNE(void); |
73 |
|
static rm RNA(void); |
74 |
|
static rm RTP(void); |
75 |
|
static rm RTN(void); |
76 |
|
static rm RTZ(void); |
77 |
|
|
78 |
|
/** The sympfu properties. */ |
79 |
|
static void precondition(const prop& p); |
80 |
|
static void postcondition(const prop& p); |
81 |
|
static void invariant(const prop& p); |
82 |
|
}; |
83 |
|
|
84 |
|
/** |
85 |
|
* Type function for mapping between types. |
86 |
|
*/ |
87 |
|
template <bool T> |
88 |
|
struct signedToLiteralType; |
89 |
|
|
90 |
|
template <> |
91 |
|
struct signedToLiteralType<true> |
92 |
|
{ |
93 |
|
using literalType = int32_t; |
94 |
|
}; |
95 |
|
template <> |
96 |
|
struct signedToLiteralType<false> |
97 |
|
{ |
98 |
|
using literalType = uint32_t; |
99 |
|
}; |
100 |
|
|
101 |
|
/** |
102 |
|
* This extends the interface for cvc5::BitVector for compatibility with symFPU. |
103 |
|
* The template parameter distinguishes signed and unsigned bit-vectors, a |
104 |
|
* distinction symfpu uses. |
105 |
|
*/ |
106 |
|
template <bool isSigned> |
107 |
1676944 |
class wrappedBitVector : public BitVector |
108 |
|
{ |
109 |
|
protected: |
110 |
|
using literalType = typename signedToLiteralType<isSigned>::literalType; |
111 |
|
friend wrappedBitVector<!isSigned>; // To allow conversion between types |
112 |
|
|
113 |
|
friend ::symfpu::ite<Cvc5Prop, wrappedBitVector<isSigned> >; // For ITE |
114 |
|
|
115 |
|
public: |
116 |
|
/** Constructors. */ |
117 |
672268 |
wrappedBitVector(const Cvc5BitWidth w, const uint32_t v) : BitVector(w, v) {} |
118 |
9630 |
wrappedBitVector(const Cvc5Prop& p) : BitVector(1, p ? 1U : 0U) {} |
119 |
175183 |
wrappedBitVector(const wrappedBitVector<isSigned>& old) : BitVector(old) {} |
120 |
819566 |
wrappedBitVector(const BitVector& old) : BitVector(old) {} |
121 |
|
|
122 |
|
/** Get the bit-width of this wrapped bit-vector. */ |
123 |
335384 |
Cvc5BitWidth getWidth(void) const { return getSize(); } |
124 |
|
|
125 |
|
/** Create a zero value of given bit-width 'w'. */ |
126 |
|
static wrappedBitVector<isSigned> one(const Cvc5BitWidth& w); |
127 |
|
/** Create a one value of given bit-width 'w'. */ |
128 |
|
static wrappedBitVector<isSigned> zero(const Cvc5BitWidth& w); |
129 |
|
/** Create a ones value (all bits 1) of given bit-width 'w'. */ |
130 |
|
static wrappedBitVector<isSigned> allOnes(const Cvc5BitWidth& w); |
131 |
|
/** Create a maximum signed/unsigned value of given bit-width 'w'. */ |
132 |
|
static wrappedBitVector<isSigned> maxValue(const Cvc5BitWidth& w); |
133 |
|
/** Create a minimum signed/unsigned value of given bit-width 'w'. */ |
134 |
|
static wrappedBitVector<isSigned> minValue(const Cvc5BitWidth& w); |
135 |
|
|
136 |
|
/** Return true if this a bit-vector representing a ones value. */ |
137 |
|
Cvc5Prop isAllOnes() const; |
138 |
|
/** Return true if this a bit-vector representing a zero value. */ |
139 |
|
Cvc5Prop isAllZeros() const; |
140 |
|
|
141 |
|
/** Left shift. */ |
142 |
|
wrappedBitVector<isSigned> operator<<( |
143 |
|
const wrappedBitVector<isSigned>& op) const; |
144 |
|
/** Logical (unsigned) and arithmetic (signed) right shift. */ |
145 |
|
wrappedBitVector<isSigned> operator>>( |
146 |
|
const wrappedBitVector<isSigned>& op) const; |
147 |
|
|
148 |
|
/** |
149 |
|
* Inherited but ... |
150 |
|
* *sigh* if we use the inherited version then it will return a |
151 |
|
* cvc5::BitVector which can be converted back to a |
152 |
|
* wrappedBitVector<isSigned> but isn't done automatically when working |
153 |
|
* out types for templates instantiation. ITE is a particular |
154 |
|
* problem as expressions and constants no longer derive the |
155 |
|
* same type. There aren't any good solutions in C++, we could |
156 |
|
* use CRTP but Liana wouldn't appreciate that, so the following |
157 |
|
* pointless wrapping functions are needed. |
158 |
|
*/ |
159 |
|
|
160 |
|
/** Bit-wise or. */ |
161 |
|
wrappedBitVector<isSigned> operator|( |
162 |
|
const wrappedBitVector<isSigned>& op) const; |
163 |
|
/** Bit-wise and. */ |
164 |
|
wrappedBitVector<isSigned> operator&( |
165 |
|
const wrappedBitVector<isSigned>& op) const; |
166 |
|
/** Bit-vector addition. */ |
167 |
|
wrappedBitVector<isSigned> operator+( |
168 |
|
const wrappedBitVector<isSigned>& op) const; |
169 |
|
/** Bit-vector subtraction. */ |
170 |
|
wrappedBitVector<isSigned> operator-( |
171 |
|
const wrappedBitVector<isSigned>& op) const; |
172 |
|
/** Bit-vector multiplication. */ |
173 |
|
wrappedBitVector<isSigned> operator*( |
174 |
|
const wrappedBitVector<isSigned>& op) const; |
175 |
|
/** Bit-vector signed/unsigned division. */ |
176 |
|
wrappedBitVector<isSigned> operator/( |
177 |
|
const wrappedBitVector<isSigned>& op) const; |
178 |
|
/** Bit-vector signed/unsigned remainder. */ |
179 |
|
wrappedBitVector<isSigned> operator%( |
180 |
|
const wrappedBitVector<isSigned>& op) const; |
181 |
|
/** Bit-vector negation. */ |
182 |
|
wrappedBitVector<isSigned> operator-(void) const; |
183 |
|
/** Bit-wise not. */ |
184 |
|
wrappedBitVector<isSigned> operator~(void) const; |
185 |
|
|
186 |
|
/** Bit-vector increment. */ |
187 |
|
wrappedBitVector<isSigned> increment() const; |
188 |
|
/** Bit-vector decrement. */ |
189 |
|
wrappedBitVector<isSigned> decrement() const; |
190 |
|
/** |
191 |
|
* Bit-vector logical/arithmetic right shift where 'op' extended to the |
192 |
|
* bit-width of this wrapped bit-vector. |
193 |
|
*/ |
194 |
|
wrappedBitVector<isSigned> signExtendRightShift( |
195 |
|
const wrappedBitVector<isSigned>& op) const; |
196 |
|
|
197 |
|
/** |
198 |
|
* Modular operations. |
199 |
|
* Note: No overflow checking so these are the same as other operations. |
200 |
|
*/ |
201 |
|
wrappedBitVector<isSigned> modularLeftShift( |
202 |
|
const wrappedBitVector<isSigned>& op) const; |
203 |
|
wrappedBitVector<isSigned> modularRightShift( |
204 |
|
const wrappedBitVector<isSigned>& op) const; |
205 |
|
wrappedBitVector<isSigned> modularIncrement() const; |
206 |
|
wrappedBitVector<isSigned> modularDecrement() const; |
207 |
|
wrappedBitVector<isSigned> modularAdd( |
208 |
|
const wrappedBitVector<isSigned>& op) const; |
209 |
|
wrappedBitVector<isSigned> modularNegate() const; |
210 |
|
|
211 |
|
/** Bit-vector equality. */ |
212 |
|
Cvc5Prop operator==(const wrappedBitVector<isSigned>& op) const; |
213 |
|
/** Bit-vector signed/unsigned less or equal than. */ |
214 |
|
Cvc5Prop operator<=(const wrappedBitVector<isSigned>& op) const; |
215 |
|
/** Bit-vector sign/unsigned greater or equal than. */ |
216 |
|
Cvc5Prop operator>=(const wrappedBitVector<isSigned>& op) const; |
217 |
|
/** Bit-vector signed/unsigned less than. */ |
218 |
|
Cvc5Prop operator<(const wrappedBitVector<isSigned>& op) const; |
219 |
|
/** Bit-vector sign/unsigned greater or equal than. */ |
220 |
|
Cvc5Prop operator>(const wrappedBitVector<isSigned>& op) const; |
221 |
|
|
222 |
|
/** Convert this bit-vector to a signed bit-vector. */ |
223 |
|
wrappedBitVector<true> toSigned(void) const; |
224 |
|
/** Convert this bit-vector to an unsigned bit-vector. */ |
225 |
|
wrappedBitVector<false> toUnsigned(void) const; |
226 |
|
|
227 |
|
/** Bit-vector signed/unsigned (zero) extension. */ |
228 |
|
wrappedBitVector<isSigned> extend(Cvc5BitWidth extension) const; |
229 |
|
|
230 |
|
/** |
231 |
|
* Create a "contracted" bit-vector by cutting off the 'reduction' number of |
232 |
|
* most significant bits, i.e., by extracting the (bit-width - reduction) |
233 |
|
* least significant bits. |
234 |
|
*/ |
235 |
|
wrappedBitVector<isSigned> contract(Cvc5BitWidth reduction) const; |
236 |
|
|
237 |
|
/** |
238 |
|
* Create a "resized" bit-vector of given size bei either extending (if new |
239 |
|
* size is larger) or contracting (if it is smaller) this wrapped bit-vector. |
240 |
|
*/ |
241 |
|
wrappedBitVector<isSigned> resize(Cvc5BitWidth newSize) const; |
242 |
|
|
243 |
|
/** |
244 |
|
* Create an extension of this bit-vector that matches the bit-width of the |
245 |
|
* given bit-vector. |
246 |
|
* |
247 |
|
* Note: The size of the given bit-vector may not be larger than the size of |
248 |
|
* this bit-vector. |
249 |
|
*/ |
250 |
|
wrappedBitVector<isSigned> matchWidth( |
251 |
|
const wrappedBitVector<isSigned>& op) const; |
252 |
|
|
253 |
|
/** Bit-vector concatenation. */ |
254 |
|
wrappedBitVector<isSigned> append(const wrappedBitVector<isSigned>& op) const; |
255 |
|
|
256 |
|
/** Inclusive of end points, thus if the same, extracts just one bit. */ |
257 |
|
wrappedBitVector<isSigned> extract(Cvc5BitWidth upper, |
258 |
|
Cvc5BitWidth lower) const; |
259 |
|
}; |
260 |
|
} // namespace symfpuLiteral |
261 |
|
} |
262 |
|
|
263 |
|
#endif |
264 |
|
#endif |