projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 13a107e) | patch
FloatingPoint: Separate out symFPU glue code. (#5492)
authorAina Niemetz <aina.niemetz@gmail.com>
Fri, 20 Nov 2020 22:30:57 +0000 (14:30 -0800)
committerGitHub <noreply@github.com>
Fri, 20 Nov 2020 22:30:57 +0000 (14:30 -0800)
commitfedb3256b37511943c4a843327d36da31480be69
tree3d452051781913fca7d1db9a94c610c5657a9e30tree
parent13a107e13f52c6418328eb798da315ca2fa1a1cacommit | 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.
src/theory/fp/fp_converter.cpp diff | blob | history
src/theory/fp/fp_converter.h diff | blob | history
src/theory/fp/theory_fp_rewriter.cpp diff | blob | history
src/theory/fp/theory_fp_type_rules.h diff | blob | history
src/util/floatingpoint.cpp diff | blob | history
src/util/floatingpoint.h.in diff | blob | history
src/util/roundingmode.h diff | blob | history
src/util/symfpu_literal.cpp diff | blob | history
src/util/symfpu_literal.h.in diff | blob | history