mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-30 19:22:28 +00:00
Code Activity
14290 commits 49 branches 53 tags 182 MiB
Commit graph

14290 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
6b380811b8 fix #4524 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-09 15:05:55 -07:00
Nikolaj Bjorner
65e6b73873 fix #4538 - regression when renaming family from special_relations to specrels 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-08 14:46:40 -07:00
Nikolaj Bjorner
80cc45c5c1 display justifications compactly for tracing #4575 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-08 13:32:41 -07:00
Nikolaj Bjorner
ab7b8b6ec5 fix #4572 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-08 11:58:44 -07:00
Nikolaj Bjorner
061abd153c fixing #4515 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-08 11:43:32 -07:00
Nikolaj Bjorner
ec3066c28a #4532 - arithmetic using SAT for interpreted atoms such as (< 0 0) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-08 11:43:32 -07:00
Nikolaj Bjorner
e1a0a2e536 give up on addition subterms in monomial decomposition caused by disabling rewriter.flat seems to be corner case exercised in #4532. 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-08 11:43:32 -07:00
Nikolaj Bjorner
69afd9f6bd formatting 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-08 11:43:31 -07:00
Nikolaj Bjorner
9bcda408ba towards closing small domain equality enforcement gap #4515 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-08 11:43:31 -07: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
688d38d868 typo 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-07 19:07:26 -07:00
Nikolaj Bjorner
4e77984c57 enable binary string access to unsigned numerals over API #4568 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-07 18:59:20 -07:00
Nikolaj Bjorner
4b346ef693 enable binary string access to unsigned numerals over API #4568 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-07 18:58:42 -07:00
Nikolaj Bjorner
4a8533e41f enable binary string access to unsigned numerals over API #4568 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-07 18:17:54 -07:00
Nikolaj Bjorner
2d358a9a50 fix #4565 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-06 17:07:37 -07:00
Nuno Lopes
ca97bfb4b8 fix build 2020-07-05 11:44:12 +01:00
Nikolaj Bjorner
006418e027 build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-04 23:34:21 -07:00
Nikolaj Bjorner
f380d4cf83 mpfx 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-04 18:25:32 -07:00
Nikolaj Bjorner
74eb401c3b addrecdef 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-04 18:18:25 -07:00
Nikolaj Bjorner
51d43c04ea st 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-04 17:13:04 -07:00
Nikolaj Bjorner
2bb712c9da ml 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-04 17:09:08 -07:00
Nikolaj Bjorner
5ea145ce26 ml 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-04 17:08:22 -07:00
Nikolaj Bjorner
bf14444f7d st 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-04 17:07:07 -07:00
Nikolaj Bjorner
f3b51db891 ml build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-04 16:22:01 -07:00
Nikolaj Bjorner
d0e20e44ff booyah 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-04 15:56:30 -07:00
Nikolaj Bjorner
10d0404175 add rec decl/def to ML #4563 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-04 15:38:32 -07:00
Lev Nachmanson
62b9630c4b remove unicode from hnf_cutter.h 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-07-04 09:33:45 -07:00
Lev Nachmanson
7a4eed0216 add comments to hnf_cutter 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-07-04 09:33:45 -07:00
Lev Nachmanson
49e49d6bb6 add comments to hnf_cutter 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-07-04 09:33:45 -07:00
Lev Nachmanson
80a4da9b1d add comments to hnf_cutter 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-07-04 09:33:45 -07:00
Lev Nachmanson
fff6a94de4 cheap_eqs - fix the build 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-07-04 09:33:45 -07:00
Lev Nachmanson
61da368ee3 cheap_eqs - work on fixed_phase 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-07-04 09:33:45 -07:00
Lev Nachmanson
f4502ff952 cheap_eqs - work on fixed_phase 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-07-04 09:33:45 -07:00
Lev Nachmanson
1695379dc9 cheap_eqs - work on fixed_phase 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-07-04 09:33:45 -07:00
Lev Nachmanson
a1c5cff541 cheap_eqs - work on fixed_phase 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-07-04 09:33:45 -07:00
Lev Nachmanson
29b3f438bc cheap_eqs - work on fixed_phase 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-07-04 09:33:45 -07:00
Lev Nachmanson
cb3ebac3dd cleanup lp_bound_propagator.h 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-07-04 09:33:45 -07:00
Lev Nachmanson
b996bc1f02 remove cheap equalities with the table 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-07-04 09:33:45 -07:00
Murphy Berzish
e8690d28f8
z3str3: continue instead of incorrectly giving up in solve_regex_automata (#4556) 2020-07-03 17:13:27 -05:00
Nikolaj Bjorner
8d3caa00fe do as Lev does 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-03 13:21:43 -07:00
Nikolaj Bjorner
7802e33f37 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-03 12:22:13 -07:00
Nikolaj Bjorner
5e768c9697 move unused literals under if0 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-03 12:21:20 -07:00
Nikolaj Bjorner
5987d9ae20 cache computing strings and regexes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-02 11:14:29 -07:00
Nikolaj Bjorner
655166b867 randomize generation of 'some value' for user sorts. #4557 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-01 16:34:09 -07:00
Nikolaj Bjorner
d91ca423ab enforce reference count ownership in context of mk_derivative calls. 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-01 13:13:17 -07:00
Nikolaj Bjorner
d75ce38016 fix #4552 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-30 19:14:55 -07:00
Murphy Berzish
fce1252145
Z3str3: Add consistency checks for string-integer conversion terms in model construction (#4551) 
* z3str3: check consistency of str.to_int in fixed length solver

* z3str3: add similar check for int.to_str as well

* z3str3: refactor string-integer conversion check and add post checks for model construction
 2020-06-30 11:20:44 -05:00
Nuno Lopes
8fda4f904d API: dont deref already free'd memory on error 2020-06-30 15:04:40 +01:00
Nuno Lopes
64f1a759a7 inline api_context::reset_error_code() 2020-06-29 19:14:17 +01:00