Christoph M. Wintersteiger
|
a2503af585
|
Bugfixes for UFs and conversion functions in theory_fpa
|
2015-10-08 11:54:35 +01:00 |
|
Christoph M. Wintersteiger
|
de39173f6f
|
Corrected unspecified behavior of fp.min/fp.max corner cases in fpa2bv_converter and in theory_fpa.
Fixes #68
|
2015-10-07 20:44:08 +01:00 |
|
Christoph M. Wintersteiger
|
076e680433
|
Improved UF suppport in fpa2bv_converter.
|
2015-09-25 17:28:31 +01:00 |
|
Christoph M. Wintersteiger
|
336fa6ae83
|
Bugfix for FP to BV conversion of UFs
|
2015-09-01 17:52:19 +01:00 |
|
Christoph M. Wintersteiger
|
081ba9093a
|
Bugfix for FP theory; handling of UFs and interpreted functions from other theories.
|
2015-08-27 18:17:26 +01:00 |
|
Nikolaj Bjorner
|
4bc044c982
|
update header guards to be C++ style. Fixes issue #9
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-07-08 23:18:40 -07:00 |
|
Christoph M. Wintersteiger
|
6980fb3035
|
Bugfix for distinct of floats.
|
2015-06-12 12:58:19 +01:00 |
|
Christoph M. Wintersteiger
|
5344d6f3c0
|
various bugfixes and extensions for FPA
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2015-01-15 19:25:49 +00:00 |
|
Christoph M. Wintersteiger
|
33dc6340e1
|
More renaming mk_value -> mk_numeral
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2015-01-08 14:23:13 +00:00 |
|
Christoph M. Wintersteiger
|
c0a027fc80
|
FPA: Elminated nzero/pzero AST kinds
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2015-01-08 14:07:47 +00:00 |
|
Christoph M. Wintersteiger
|
dd17f3c7d6
|
Renaming floats, float, Floats, Float -> FPA, fpa
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2015-01-08 13:18:56 +00:00 |
|
Christoph M. Wintersteiger
|
3fe11e4c38
|
improved handling of unspecified values in FP
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2014-12-31 17:31:11 +00:00 |
|
Christoph M. Wintersteiger
|
01d78b7274
|
added internal functions to fpa2bv converter
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2014-12-31 14:49:52 +00:00 |
|
Christoph M. Wintersteiger
|
4d1f71775d
|
FPA: added to_fp_unsigned
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2014-12-28 15:26:52 +00:00 |
|
Christoph M. Wintersteiger
|
a1b4ef9e1b
|
fpa2bv refactoring
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2014-12-21 18:44:12 +00:00 |
|
Christoph M. Wintersteiger
|
47325c5fd3
|
FPA: bugfixes, naming convention, core theory additions
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2014-12-16 23:59:27 +00:00 |
|
Christoph M. Wintersteiger
|
b30e61e528
|
FPA: bugfixes, leakfixes, added fp.to_real
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2014-12-13 19:34:55 +00:00 |
|
Christoph M. Wintersteiger
|
657595818e
|
FPA API: Renaming for consistency with final SMT standard.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2014-12-10 18:45:44 +00:00 |
|
Christoph M. Wintersteiger
|
31a017e99e
|
FPA: standard function names consistency, improved error messages, bugfixes.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2014-10-22 19:47:50 +01:00 |
|
Ken McMillan
|
c007a5e5bd
|
merged with unstable
|
2014-08-06 11:16:06 -07:00 |
|
Christoph M. Wintersteiger
|
fb4c07a2ea
|
FPA refactoring in preparation for FPA support in the kernel.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2014-04-23 18:36:38 +01:00 |
|