1 /********************* */
2 /*! \file fp_converter.h
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-2020 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
12 ** \brief Converts floating-point nodes to bit-vector expressions.
14 ** Uses the symfpu library to convert from floating-point operations to
15 ** bit-vectors and propositions allowing the theory to be solved by
18 ** !!! This header is not to be included in any other headers !!!
21 #include "cvc4_private.h"
23 #ifndef CVC4__THEORY__FP__FP_CONVERTER_H
24 #define CVC4__THEORY__FP__FP_CONVERTER_H
26 #include "base/check.h"
27 #include "context/cdhashmap.h"
28 #include "context/cdlist.h"
29 #include "expr/node.h"
30 #include "expr/node_builder.h"
31 #include "expr/type_node.h"
32 #include "theory/valuation.h"
33 #include "util/bitvector.h"
34 #include "util/floatingpoint_size.h"
35 #include "util/hash.h"
37 #ifdef CVC4_USE_SYMFPU
38 #include "symfpu/core/unpackedFloat.h"
41 #ifdef CVC4_SYM_SYMBOLIC_EVAL
42 // This allows debugging of the CVC4 symbolic back-end.
43 // By enabling this and disabling constant folding in the rewriter,
44 // SMT files that have operations on constants will be evaluated
45 // during the encoding step, which means that the expressions
46 // generated by the symbolic back-end can be debugged with gdb.
47 #include "theory/rewriter.h"
55 * This is a symfpu symbolic "back-end". It allows the library to be used to
56 * construct bit-vector expressions that compute floating-point operations.
57 * This is effectively the glue between symfpu's notion of "signed bit-vector"
60 namespace symfpuSymbolic
{
62 // Forward declarations of the wrapped types so that traits can be defined early
63 // and used in the implementations
64 class symbolicRoundingMode
;
65 class floatingPointTypeInfo
;
66 class symbolicProposition
;
68 class symbolicBitVector
;
70 // This is the template parameter for symfpu's templates.
74 // The six key types that symfpu uses.
76 typedef symbolicRoundingMode rm
;
77 typedef floatingPointTypeInfo fpt
;
78 typedef symbolicProposition prop
;
79 typedef symbolicBitVector
<true> sbv
;
80 typedef symbolicBitVector
<false> ubv
;
82 // Give concrete instances (wrapped nodes) for each rounding mode.
83 static symbolicRoundingMode
RNE(void);
84 static symbolicRoundingMode
RNA(void);
85 static symbolicRoundingMode
RTP(void);
86 static symbolicRoundingMode
RTN(void);
87 static symbolicRoundingMode
RTZ(void);
89 // Properties used by symfpu
90 static void precondition(const bool b
);
91 static void postcondition(const bool b
);
92 static void invariant(const bool b
);
93 static void precondition(const prop
&p
);
94 static void postcondition(const prop
&p
);
95 static void invariant(const prop
&p
);
98 // Use the same type names as symfpu.
99 typedef traits::bwt bwt
;
102 * Wrap the CVC4::Node types so that we can debug issues with this back-end
104 class nodeWrapper
: public Node
107 /* CVC4_SYM_SYMBOLIC_EVAL is for debugging CVC4 symbolic back-end issues.
108 * Enable this and disabling constant folding will mean that operations
109 * that are input with constant args are 'folded' using the symbolic encoding
110 * allowing them to be traced via GDB.
112 #ifdef CVC4_SYM_SYMBOLIC_EVAL
113 nodeWrapper(const Node
&n
) : Node(theory::Rewriter::rewrite(n
)) {}
115 nodeWrapper(const Node
&n
) : Node(n
) {}
119 class symbolicProposition
: public nodeWrapper
122 bool checkNodeType(const TNode node
);
124 #ifdef CVC4_USE_SYMFPU
125 friend ::symfpu::ite
<symbolicProposition
, symbolicProposition
>; // For ITE
129 symbolicProposition(const Node n
);
130 symbolicProposition(bool v
);
131 symbolicProposition(const symbolicProposition
&old
);
133 symbolicProposition
operator!(void)const;
134 symbolicProposition
operator&&(const symbolicProposition
&op
) const;
135 symbolicProposition
operator||(const symbolicProposition
&op
) const;
136 symbolicProposition
operator==(const symbolicProposition
&op
) const;
137 symbolicProposition
operator^(const symbolicProposition
&op
) const;
140 class symbolicRoundingMode
: public nodeWrapper
143 bool checkNodeType(const TNode n
);
145 #ifdef CVC4_USE_SYMFPU
146 friend ::symfpu::ite
<symbolicProposition
, symbolicRoundingMode
>; // For ITE
150 symbolicRoundingMode(const Node n
);
151 symbolicRoundingMode(const unsigned v
);
152 symbolicRoundingMode(const symbolicRoundingMode
&old
);
154 symbolicProposition
valid(void) const;
155 symbolicProposition
operator==(const symbolicRoundingMode
&op
) const;
158 // Type function for mapping between types
160 struct signedToLiteralType
;
163 struct signedToLiteralType
<true>
165 typedef int literalType
;
168 struct signedToLiteralType
<false>
170 typedef unsigned int literalType
;
173 template <bool isSigned
>
174 class symbolicBitVector
: public nodeWrapper
177 typedef typename signedToLiteralType
<isSigned
>::literalType literalType
;
179 Node
boolNodeToBV(Node node
) const;
180 Node
BVToBoolNode(Node node
) const;
182 Node
fromProposition(Node node
) const;
183 Node
toProposition(Node node
) const;
184 bool checkNodeType(const TNode n
);
185 friend symbolicBitVector
<!isSigned
>; // To allow conversion between the types
187 #ifdef CVC4_USE_SYMFPU
188 friend ::symfpu::ite
<symbolicProposition
,
189 symbolicBitVector
<isSigned
> >; // For ITE
193 symbolicBitVector(const Node n
);
194 symbolicBitVector(const bwt w
, const unsigned v
);
195 symbolicBitVector(const symbolicProposition
&p
);
196 symbolicBitVector(const symbolicBitVector
<isSigned
> &old
);
197 symbolicBitVector(const BitVector
&old
);
199 bwt
getWidth(void) const;
201 /*** Constant creation and test ***/
202 static symbolicBitVector
<isSigned
> one(const bwt
&w
);
203 static symbolicBitVector
<isSigned
> zero(const bwt
&w
);
204 static symbolicBitVector
<isSigned
> allOnes(const bwt
&w
);
206 symbolicProposition
isAllOnes() const;
207 symbolicProposition
isAllZeros() const;
209 static symbolicBitVector
<isSigned
> maxValue(const bwt
&w
);
210 static symbolicBitVector
<isSigned
> minValue(const bwt
&w
);
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%(
230 const symbolicBitVector
<isSigned
> &op
) const;
231 symbolicBitVector
<isSigned
> operator-(void) const;
232 symbolicBitVector
<isSigned
> operator~(void)const;
233 symbolicBitVector
<isSigned
> increment() const;
234 symbolicBitVector
<isSigned
> decrement() const;
235 symbolicBitVector
<isSigned
> signExtendRightShift(
236 const symbolicBitVector
<isSigned
> &op
) const;
238 /*** Modular operations ***/
239 // This back-end doesn't do any overflow checking so these are the same as
241 symbolicBitVector
<isSigned
> modularLeftShift(
242 const symbolicBitVector
<isSigned
> &op
) const;
243 symbolicBitVector
<isSigned
> modularRightShift(
244 const symbolicBitVector
<isSigned
> &op
) const;
245 symbolicBitVector
<isSigned
> modularIncrement() const;
246 symbolicBitVector
<isSigned
> modularDecrement() const;
247 symbolicBitVector
<isSigned
> modularAdd(
248 const symbolicBitVector
<isSigned
> &op
) const;
249 symbolicBitVector
<isSigned
> modularNegate() const;
251 /*** Comparisons ***/
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 symbolicProposition
operator<(const symbolicBitVector
<isSigned
> &op
) const;
256 symbolicProposition
operator>(const symbolicBitVector
<isSigned
> &op
) const;
258 /*** Type conversion ***/
259 // CVC4 nodes make no distinction between signed and unsigned, thus these are
261 symbolicBitVector
<true> toSigned(void) const;
262 symbolicBitVector
<false> toUnsigned(void) const;
265 symbolicBitVector
<isSigned
> extend(bwt extension
) const;
266 symbolicBitVector
<isSigned
> contract(bwt reduction
) const;
267 symbolicBitVector
<isSigned
> resize(bwt newSize
) const;
268 symbolicBitVector
<isSigned
> matchWidth(
269 const symbolicBitVector
<isSigned
> &op
) const;
270 symbolicBitVector
<isSigned
> append(
271 const symbolicBitVector
<isSigned
> &op
) const;
273 // Inclusive of end points, thus if the same, extracts just one bit
274 symbolicBitVector
<isSigned
> extract(bwt upper
, bwt lower
) const;
277 // Use the same type information as the literal back-end but add an interface to
278 // TypeNodes for convenience.
279 class floatingPointTypeInfo
: public FloatingPointSize
282 floatingPointTypeInfo(const TypeNode t
);
283 floatingPointTypeInfo(unsigned exp
, unsigned sig
);
284 floatingPointTypeInfo(const floatingPointTypeInfo
&old
);
286 TypeNode
getTypeNode(void) const;
291 * This class uses SymFPU to convert an expression containing floating-point
292 * kinds and operations into a logically equivalent form with bit-vector
293 * operations replacing the floating-point ones. It also has a getValue method
294 * to produce an expression which will reconstruct the value of the
295 * floating-point terms from a valuation.
297 * Internally it caches all of the unpacked floats so that unnecessary packing
298 * and unpacking operations are avoided and to make best use of structural
305 FpConverter(context::UserContext
*);
309 /** Adds a node to the conversion, returns the converted node */
312 /** Gives the node representing the value of a given variable */
313 Node
getValue(Valuation
&, TNode
);
315 context::CDList
<Node
> d_additionalAssertions
;
318 #ifdef CVC4_USE_SYMFPU
319 typedef symfpuSymbolic::traits traits
;
320 typedef ::symfpu::unpackedFloat
<symfpuSymbolic::traits
> uf
;
321 typedef symfpuSymbolic::traits::rm rm
;
322 typedef symfpuSymbolic::traits::fpt fpt
;
323 typedef symfpuSymbolic::traits::prop prop
;
324 typedef symfpuSymbolic::traits::ubv ubv
;
325 typedef symfpuSymbolic::traits::sbv sbv
;
327 typedef context::CDHashMap
<Node
, uf
, NodeHashFunction
> fpMap
;
328 typedef context::CDHashMap
<Node
, rm
, NodeHashFunction
> rmMap
;
329 typedef context::CDHashMap
<Node
, prop
, NodeHashFunction
> boolMap
;
330 typedef context::CDHashMap
<Node
, ubv
, NodeHashFunction
> ubvMap
;
331 typedef context::CDHashMap
<Node
, sbv
, NodeHashFunction
> sbvMap
;
339 /* These functions take a symfpu object and convert it to a node.
340 * These should ensure that constant folding it will give a
341 * constant of the right type.
344 Node
ufToNode(const fpt
&, const uf
&) const;
345 Node
rmToNode(const rm
&) const;
346 Node
propToNode(const prop
&) const;
347 Node
ubvToNode(const ubv
&) const;
348 Node
sbvToNode(const sbv
&) const;
350 /* Creates the relevant components for a variable */
351 uf
buildComponents(TNode current
);
356 } // namespace theory
359 #endif /* CVC4__THEORY__FP__THEORY_FP_H */