projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 439ab12) | patch
FP: Rewrite to_fp conversion from signed bit-vector. (#6472)
authorAina Niemetz <aina.niemetz@gmail.com>
Mon, 3 May 2021 20:27:02 +0000 (13:27 -0700)
committerGitHub <noreply@github.com>
Mon, 3 May 2021 20:27:02 +0000 (20:27 +0000)
commitc8c7a075428e6193dee86e57a9ecb8af11af270c
treeac12ea111a8228c594495573bc5407a05d3b3131tree
parent439ab123cccdbf4f046b4e084ce996a1dc2aa758commit | diff
FP: Rewrite to_fp conversion from signed bit-vector. (#6472)

SymFPU does not allow to_fp conversion from signed bv of size 1. This
adds rewrites for this case.

Rewrites for the constant and the non-constant cases were tested in
isolation.
src/theory/fp/theory_fp_rewriter.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/fp/from_sbv.smt2 [new file with mode: 0644] blob