projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8a3876f) | patch
FP: Refactor FloatingPointLiteral in preparation for MPFR. (#6206)
authorAina Niemetz <aina.niemetz@gmail.com>
Thu, 25 Mar 2021 19:18:51 +0000 (12:18 -0700)
committerGitHub <noreply@github.com>
Thu, 25 Mar 2021 19:18:51 +0000 (19:18 +0000)
commit99a74de90a064133a8e3d03ee9334d59be34ba1d
tree3d18d56a020b1dbd2b7dfed0b763524324285c24tree
parent8a3876f74f377817345af405aebfceebc7896059commit | diff
FP: Refactor FloatingPointLiteral in preparation for MPFR. (#6206)

This pushes all symfpu specific parts from FloatingPoint into
FloatingPointLiteral. FloatingPoint is now generic. An additional
FloatingPointLiteral implementation using MPFR will be made configurable
similiarly to how we handle Integers with either GMP or CLN backend.
src/api/cvc4cpp.cpp diff | blob | history
src/printer/smt2/smt2_printer.cpp 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 diff | blob | history
src/util/floatingpoint_literal_symfpu.cpp diff | blob | history
src/util/floatingpoint_literal_symfpu.h.in diff | blob | history