projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 71699a5) | patch
FP: Factor out symfpu traits. (#6246)
authorAina Niemetz <aina.niemetz@gmail.com>
Thu, 1 Apr 2021 21:25:03 +0000 (14:25 -0700)
committerGitHub <noreply@github.com>
Thu, 1 Apr 2021 21:25:03 +0000 (21:25 +0000)
commit7fa534c85cbb6eb2863f10840b39501a21acc0b9
treef47b7c3a23a52330d292193241a8b74528c8fe82tree
parent71699a551d207ab373c733d8ea83a5b071ed99eecommit | diff
FP: Factor out symfpu traits. (#6246)

This is in preparation for a MPFR floating-point literal implementation.
We will need to have both literal kinds return a symFPU unpacked float
via `getSymUF()` in order to be able to plug it into the fp_converter.
For this, it makes sense to have the traits implemented and to be
included separately, so that they can also be included in the MPFR
implementation.
src/api/checks.h diff | blob | history
src/util/CMakeLists.txt diff | blob | history
src/util/floatingpoint_literal_symfpu.cpp diff | blob | history
src/util/floatingpoint_literal_symfpu.h.in diff | blob | history
src/util/floatingpoint_literal_symfpu_traits.cpp [new file with mode: 0644] blob
src/util/floatingpoint_literal_symfpu_traits.h.in [new file with mode: 0644] blob