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