mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-15 00:46:38 +00:00
Code Activity
14923 commits 42 branches 51 tags 169 MiB
Commit graph

249 commits

Author SHA1 Message Date
Nikolaj Bjorner
8f577d3943 remove ast_manager get_sort method entirely 2021-02-02 13:57:01 -08:00
Nikolaj Bjorner
937b61fc88 fix build, refactor 2021-02-02 05:26:57 -08:00
Nikolaj Bjorner
3ae4c6e9de refactor get_sort 2021-02-02 04:45:54 -08:00
Nuno Lopes
4db41c02cc remove some dead code from fpa2bv converter 2021-01-04 17:06:35 +00:00
Christoph M. Wintersteiger
eadf755628
Fix bonus subtraction in fp.rem. Fixes #4564. Fixes most of #2381. 2020-11-06 20:54:10 +00:00
Nikolaj Bjorner
fa58a36b9f
model refactor (#4723) 
* refactor model fixing

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* missing cond macro

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* file

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* file

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* add macros dependency

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* deps and debug

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* add dependency to normal forms

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* build issues

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* compile

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix leal regression

* complete model fixer

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fold back private functionality to model_finder

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* avoid duplicate fixed callbacks

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-10-05 14:13:05 -07:00
Nikolaj Bjorner
08a87b102c more fpa 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-10-01 17:47:50 -07:00
Nikolaj Bjorner
2087c01cac first cut of fpa solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-10-01 07:18:36 -07:00
Nikolaj Bjorner
4cb07a539b more fpa 2020-09-30 19:06:07 -07:00
Nikolaj Bjorner
6708a764f5 move generic functionality for fpa 
move generic functionality for fpa to converter/rewriter so it can be used outside of theory_fpa @wintersteiger
 2020-09-30 18:50:07 -07:00
Nikolaj Bjorner
35e3d8425c move fpa 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-29 11:16:21 -07:00
Nikolaj Bjorner
72d140334f fixes for #4634 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-13 08:45:22 -07:00
Christoph M. Wintersteiger
a298091322
Fix for fp.roundToIntegral of tiny, denormal floats. Fixes #4190. 2020-07-17 15:58:01 +00:00
Christoph M. Wintersteiger
2ef57d7f8d
Fix FP rounding of huge exponents. Fixes #3776. 2020-07-17 13:42:12 +00:00
Christoph M. Wintersteiger
ccdae7af24
Fix for corner-case in fp.roundToIntegral. Fixes #2894. 2020-07-16 11:58:18 +00:00
Christoph M. Wintersteiger
3776588375
Clarify bit-blasting of fp.neg. Fixes #4466. 2020-07-08 18:24:08 +00:00
Christoph M. Wintersteiger
c59519bf9c
Add missing FP conversion. Fixes #4470. 2020-07-08 17:56:25 +00:00
Nikolaj Bjorner
d0e20e44ff booyah 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-04 15:56:30 -07:00
Nikolaj Bjorner
6ca039c855 fix #3919 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-11 12:31:38 -07:00
Nikolaj Bjorner
399cf75ad4 fpa warning 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-05 00:55:13 -07:00
Nikolaj Bjorner
eacde16b3e fix #3199 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-04 23:55:44 -07:00
Nikolaj Bjorner
7477e96e59 fix #3519 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-04 23:18:15 -07:00
Nikolaj Bjorner
28bdda326b fix #3499 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-23 13:37:08 -07:00
Nikolaj Bjorner
bb451c39c9 fix #3495 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-23 10:32:19 -07:00
Christoph M. Wintersteiger
963f8240c2
Throw proper warning instead of assertion violation in fp.rem. Fixes #2934. 2020-02-25 17:17:41 +00:00
Nikolaj Bjorner
541658fe02 move to abstract symbols 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-10 12:14:13 -08:00
Christoph M. Wintersteiger
4faaff5b76
Fix memory leak in bv2fpa_converter 2019-10-28 14:15:30 +00:00
Christoph M. Wintersteiger
2308d8af09
Fix for partially interpreted floating-point functions. Relates to #2596, #2631. 2019-10-28 14:15:29 +00:00
Nikolaj Bjorner
f4fd94747c fix #2652 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-23 09:39:40 -07:00
Nikolaj Bjorner
f18b4430c3 fix to_app crash 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-12 18:26:11 -07:00
Nikolaj Bjorner
cc26d49060 preparations for dealing with #2596 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-12 17:44:52 -07:00
Nikolaj Bjorner
5bdcc737ec remove function name 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-12 11:58:30 -07:00
Nikolaj Bjorner
ce06cd0d7a replace iterators by for, looking at @2596 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-12 10:08:30 -07:00
Nuno Lopes
bc50b6bea2 fix a few warnings 2019-10-09 14:09:33 +01:00
Christoph M. Wintersteiger
423fb73d34
Fix for fp.rem. Pertains to #2381. 2019-08-19 13:13:01 +01:00
Christoph M. Wintersteiger
892aa12660
Fix for fp.rem. Fixes #2381. 2019-08-15 16:44:55 +01:00
Christoph M. Wintersteiger
1517ca907e
Another fix for fp.rem. 2019-07-03 16:09:07 +01:00
Christoph M. Wintersteiger
e0dc05c97e
Fixed final alignment step of fp.rem. Fixes #2369 and does not break #2289. 2019-07-03 12:22:35 +01:00
Nikolaj Bjorner
e0d8cefde4 remove cooperate 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-12 20:15:46 -07:00
Christoph M. Wintersteiger
998b0ff7f4
Fixed corner-case in fp.rem encoding. Fixes #2289. 2019-06-07 18:03:51 +01:00
Christoph M. Wintersteiger
d1d49ef3a9
Fix BV-conversion of fp.roundToIntegral. Fixes #2191. 2019-03-27 17:13:00 +00:00
Christoph M. Wintersteiger
64d085c188
Fix bug in fpa2bv_converter, fixes #2136. 2019-02-12 14:02:30 +00:00
Florian Pigorsch
326bf401b9 Fix some spelling errors (mostly in comments). 2018-10-20 17:07:41 +02:00
Christoph M. Wintersteiger
48ec7c1175
Follow-up fix for fpa2bv_converter. 2018-10-01 17:25:02 +01:00
Christoph M. Wintersteiger
2a92de0aee
Fixed side conditions for UFs translated from FP to BV. Fixes #1825. 2018-10-01 15:20:00 +01:00
Nuno Lopes
5de6628a5d remove spurious copies and inc_refs around ref_vector 2018-06-28 10:31:38 +01:00
Nikolaj Bjorner
520ce9a5ee integrate lambda expressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-26 07:23:04 -07:00
Christoph M. Wintersteiger
dab8e49e22 Fixed corner-case in fp.to_ubv. 2018-04-16 18:28:13 +01:00
Christoph M. Wintersteiger
2abc759d0e Merge branch 'master' of https://github.com/Z3Prover/z3 2018-04-08 21:58:39 +01:00
Christoph M. Wintersteiger
b373bf4252 Bugfixes for fpa2bv_converter. Fixes #1564. 2018-04-08 21:51:27 +01:00