mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-31 07:14:54 +00:00
Code Activity
7866 commits 65 branches 52 tags 178 MiB
Commit graph

187 commits

Author SHA1 Message Date
Christoph M. Wintersteiger
333374229d Fixed UFs for unspecified cases of FP conversion operators. Thanks for Youcheng Sun for reporting this bug. 2018-02-03 16:48:05 +00:00
Christoph M. Wintersteiger
c3ed986031 Fixed RNA FP rounding mode semantics. Fixes #1190 and bugs reported by Youcheng Sun. 2018-02-03 16:46:21 +00:00
Christoph M. Wintersteiger
8689921e9c Fixed missing bit of precision in fp.to_ubv/fp.to_sbv. Thanks to Youcheng Sun for reporting this bug. 2018-02-03 15:16:23 +00:00
Christoph M. Wintersteiger
f5ff9fae34 Fixed bug check in bv2fpa converter. Fixes #1291. 2017-11-17 21:15:30 +00:00
Christoph M. Wintersteiger
2d221155b3 Fixed bug in fp.to_ieee_bv with rewriter.hi_fp_unspecified=true. Reported in #1349. 2017-11-08 20:52:48 +00:00
Nikolaj Bjorner
637a0fa139 unused warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 08:49:25 -07:00
Nikolaj Bjorner
c9f540b066 additional array functions exposed over API, ping #1223 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-19 11:08:48 -07:00
Christoph M. Wintersteiger
50042ab638 removed unused variables 2017-10-06 13:00:09 +01:00
Christoph M. Wintersteiger
cc9f67267d Eliminated the remaining operator kinds for partially unspecified FP operators. 2017-09-20 20:16:09 +01:00
Christoph M. Wintersteiger
00651f8f21 Tabs, formatting. 2017-09-17 14:54:09 +01:00
Christoph M. Wintersteiger
8871cb120a Fixed bug in fp.to_{s,u}bv 2017-09-17 12:57:29 +01:00
Christoph M. Wintersteiger
65697eb277 Portability fixes 2017-09-15 21:13:47 +01:00
Christoph M. Wintersteiger
05447d612a Bugfixes for fp.to_* operators 2017-09-15 19:56:15 +01:00
Christoph M. Wintersteiger
15ccb34a81 Removed unused function 2017-09-15 11:48:42 +01:00
Christoph M. Wintersteiger
ff42c44f37 Debug traces 2017-09-15 11:48:25 +01:00
Christoph M. Wintersteiger
a479fa610a Refactored treatment of unspecified FPA functions. 2017-09-14 20:29:07 +01:00
Christoph M. Wintersteiger
2165c09def Improved FPA models of partial theory functions 2017-09-13 19:50:51 +01:00
Christoph M. Wintersteiger
de15932f4c Fixed BV encoding of fp.to_{s,u}bv. 2017-09-13 19:47:59 +01:00
Christoph M. Wintersteiger
31cfca0444 Eliminated unspecified operators for fp.to_*bv, fp.to_real. Also fixes #1191. 2017-09-12 19:43:45 +01:00
Christoph M. Wintersteiger
4ceef09156 Renamed FPA-internal functions now that they are exposed. 2017-09-11 15:04:53 +01:00
Nikolaj Bjorner
7dd28781ab remove simplifier dependencies from cmakelist.txt files 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-23 16:33:36 -07:00
Nikolaj Bjorner
ce04c18a7a trying to get rid of last simplifier dependency in macros 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-22 22:14:13 -07:00
Nikolaj Bjorner
2b82fd5d0c updated include directives 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-01 10:51:47 -07:00
Christoph M. Wintersteiger
e8cdc34219 Debug fix in fpa2bv converter. Relates to #872. 2017-07-31 22:34:58 +01:00
Christoph M. Wintersteiger
6a2fa91818 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-07-31 22:12:37 +01:00
Christoph M. Wintersteiger
9601761a6f Added missing float conversion in fpa2bv converter. Relates to #1178. 2017-07-31 22:12:15 +01:00
Nikolaj Bjorner
063b6e9ea5 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-07-31 13:24:57 -07:00
Nikolaj Bjorner
b19f94ae5b make include paths uniformly use path relative to src. #534 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-31 13:24:11 -07:00
Christoph M. Wintersteiger
507356c7bf Fixed bug in fpa2bv converter. Fixes #1178. 2017-07-31 20:18:39 +01:00
Christoph M. Wintersteiger
52cf80d637 Simplified bit-vector bounds in fp.rem. Relates to #872. 2017-07-31 19:53:55 +01:00
Christoph M. Wintersteiger
ecfd241e19 Injected 3 missing bits of precision into fp.rem. Relates to #872. 2017-07-31 19:53:44 +01:00
Christoph M. Wintersteiger
a59907170d Fixed renormalization in fp.mul. Relates to #872. 2017-07-31 18:34:46 +01:00
Christoph M. Wintersteiger
175f042db8 Fixed renormalization in fp.fma. Relates to #872. 2017-07-28 23:01:01 +01:00
Christoph M. Wintersteiger
0610392a05 Bugfix for fp.fma. Fixes #872. 2017-07-28 20:16:13 +01:00
Christoph M. Wintersteiger
33ebdc8adc Cleaned up mpf rounder. Rewrote mpf fma. Relates to #872. 2017-07-27 23:08:35 +01:00
Christoph M. Wintersteiger
f1c0ac72e7 Fix for fp.fma encoding. Relates to #872. 2017-07-25 20:29:10 +01:00
Christoph M. Wintersteiger
0f1583309d Bugfix for fp.fma. One piece of puzzle #872. 2017-07-21 21:12:45 +01:00
Dan Liew
4b517b96df [CMake] Move CMake files into their intended location so the 
`contrib/cmake/bootstrap.py` script no longer needs to be executed.

The previous location of the CMake files was a compromise proposed
by @agurfinkel in #461. While this has served us well (allowing progress
to be made) over time limitations of this approach have appeared.

The main problem is that doing many git operations (e.g. pull, rebase)
means the CMake files don't get updated unless the user remembers to
run the script. This can lead to broken and confusing build system
behaviour.

This commit only does the file moving and necessary changes to
`.gitignore`. Other changes will be done in subsequent commits.
 2017-06-12 11:59:00 +01:00
Christoph M. Wintersteiger
a7d5bb7b36 Tabs 2017-05-31 12:18:00 +01:00
Nikolaj Bjorner
df492e200f merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-21 10:04:02 -08:00
Nikolaj Bjorner
8d18fd075e remove sources for unused variable warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-21 09:54:45 -08:00
Christoph M. Wintersteiger
56b1a8b086 Bugfix for special-case handling in fp.fma. 
Thanks to Florian Schanda for reporting this bug.
 2016-12-09 13:43:05 +00:00
Christoph M. Wintersteiger
bea7bc5e30 Bugfix for bv2fpa_converter. Fixes #767. 2016-10-26 16:32:44 +01:00
Christoph M. Wintersteiger
5ac3bb04ee Tabs 2016-10-18 13:18:59 +01:00
Nikolaj Bjorner
edaec81aa2 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-10-17 14:53:13 -04:00
Christoph M. Wintersteiger
2f6ef0f3be Removed unnecessary variables. 2016-10-17 16:33:09 +01:00
Christoph M. Wintersteiger
707dbd4173 Bugfix for bv2fpa (model) conversion. 
Relates to #740
 2016-10-17 16:19:27 +01:00
Nikolaj Bjorner
4cae91b096 spacing, unit test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-17 08:07:23 -04:00
Christoph M. Wintersteiger
009af4455d Refactored and fixed model conversion for fpa2bv conversion of unspecified values via theory_fpa. 2016-10-15 18:35:39 +02:00
Christoph M. Wintersteiger
7e705a2d32 Bug fixes for underspecified FP operations. 2016-10-15 18:35:39 +02:00