projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: daf1d6b) | patch
Floating point symfpu support (#1093)
authorMartin <martin.brain@diffblue.com>
Thu, 14 Sep 2017 03:51:50 +0000 (04:51 +0100)
committerAina Niemetz <aina.niemetz@gmail.com>
Thu, 14 Sep 2017 03:51:50 +0000 (20:51 -0700)
commit4a014a12d7f72c4f73dfbee8c9f62868e920bc15
treed6bcf71456c10122cb0e90bebebba095f0f75900tree
parentdaf1d6bf1176834fa697dd57c6fe28142e715585commit | diff
Floating point symfpu support (#1093)

Changes needed for the bit-blasting floating-point solver which are outside of it's area and / or applicable independently.
src/expr/node.h diff | blob | history
src/expr/node_builder.h diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/theory/fp/theory_fp_type_rules.h diff | blob | history
src/theory/theory_engine.cpp diff | blob | history
src/theory/theory_engine.h diff | blob | history