diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2020-11-20 14:30:57 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-11-20 14:30:57 -0800 |
| commit | fedb3256b37511943c4a843327d36da31480be69 (patch) | |
| tree | 3d452051781913fca7d1db9a94c610c5657a9e30 /src/theory/fp/fp_converter.h | |
| parent | 13a107e13f52c6418328eb798da315ca2fa1a1ca (diff) | |
FloatingPoint: Separate out symFPU glue code. (#5492)
This works towards having the symFPU headers only included where it's
absolutely needed (only in the .cpp files, not in any other headers).
Note: src/util/floatingpoint.h.in will be converted to a regular .h file
in the next step to simplify reviewing.
Diffstat (limited to 'src/theory/fp/fp_converter.h')
| -rw-r--r-- | src/theory/fp/fp_converter.h | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/fp/fp_converter.h b/src/theory/fp/fp_converter.h index fd4434832..59e65c9e1 100644 --- a/src/theory/fp/fp_converter.h +++ b/src/theory/fp/fp_converter.h @@ -29,7 +29,7 @@ #include "expr/type.h" #include "theory/valuation.h" #include "util/bitvector.h" -#include "util/floatingpoint.h" +#include "util/floatingpoint_size.h" #include "util/hash.h" #ifdef CVC4_USE_SYMFPU |