mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity
18803 commits 49 branches 53 tags 182 MiB
Commit graph

18803 commits

This branch
This branch
All branches
Author SHA1 Message Date
Jakob Rath
01d0df0a4f remove debug output 2023-03-05 13:09:51 +01:00
Jakob Rath
1ef01c5042 Add vector::erase_if 
(ended up unused but I didn't want to throw it away)
 2023-03-05 13:02:51 +01:00
Jakob Rath
e0db58c998 viable: detect eval/bool conflicts with side conditions 2023-03-05 13:02:51 +01:00
Jakob Rath
5067707a9c fix eval_invariant 2023-03-05 12:42:02 +01:00
Jakob Rath
0433f81f78 Update eval_invariant 2023-03-05 07:55:06 +01:00
Jakob Rath
2285ed90fb move comment 2023-03-05 07:45:56 +01:00
Jakob Rath
3116b2c8d5 Clean up replay 2023-03-05 07:44:18 +01:00
Jakob Rath
1b17fe79f8 Replay is needed for evaluated literals 2023-03-05 07:41:33 +01:00
Jakob Rath
235c465ae2 extract_bilinear_form: handle case where top variable is different on LHS and RHS 2023-03-04 17:19:58 +01:00
Nikolaj Bjorner
d5271df888 fix assert 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-03-02 09:01:55 -08:00
Nikolaj Bjorner
de6fea95f6 use symbolic coefficients for y 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-03-02 08:34:13 -08:00
Nikolaj Bjorner
b823d486e8 Merge branch 'polysat' of https://github.com/z3prover/z3 into polysat 2023-03-02 08:22:06 -08:00
Nikolaj Bjorner
287a536d40 make work for variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-03-02 08:22:02 -08:00
Jakob Rath
60de8f165e debug output 2023-03-02 16:06:26 +01:00
Jakob Rath
5a901e31fd verify 2023-03-02 16:03:55 +01:00
Jakob Rath
d8c6ab3488 split repropagate_units 2023-03-02 16:01:57 +01:00
Jakob Rath
8249a075e1 repropagate outside pop_levels 2023-03-02 15:52:58 +01:00
Jakob Rath
f6b8c8da21 disable replay 2023-03-02 12:24:26 +01:00
Nikolaj Bjorner
6450ad82f4 fixup proof logging 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-27 14:46:26 -08:00
Clemens Eisenhofer
4cf24fb5fc Weaken precondition for overflow narrow 2023-02-25 14:51:26 +01:00
Nikolaj Bjorner
8be6dcce31 finish adding eqs to bv_solver justifications 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-24 10:21:56 -08:00
Jakob Rath
5e95a226c5 easy AND for size 1 2023-02-24 13:52:52 +01:00
Jakob Rath
133661d81b guard pdd-AND against wrong semantics 2023-02-24 13:51:37 +01:00
Jakob Rath
ae8075e22d check and fix pdd manager confusion 2023-02-24 13:29:59 +01:00
Nikolaj Bjorner
706d542eeb add propagation justification to bv antecedents 2023-02-23 17:52:34 -08:00
Jakob Rath
9b274f349b potential generalization 2023-02-23 11:24:32 +01:00
Jakob Rath
645f4620de catch default case 2023-02-23 10:56:12 +01:00
Jakob Rath
5ffd00073a Enable more general ule simplification ule; flip order 2023-02-22 16:47:14 +01:00
Jakob Rath
6eb0d91504 Tweak ule simplifications 2023-02-22 16:36:10 +01:00
Jakob Rath
14b2c38e7f Add lemma try_umul_ovfl_noovfl for bench23 2023-02-22 16:32:51 +01:00
Jakob Rath
a8bfd01190 minor 2023-02-22 16:30:57 +01:00
Jakob Rath
c76379c0cf assign_eh: check always-false before bool-false 2023-02-22 08:58:11 +01:00
Jakob Rath
e3b3cd58ea fix comparison of pdds with different bit-widths 2023-02-21 13:01:15 +01:00
Jakob Rath
8347c043e1 Merge remote-tracking branch 'origin/polysat' into polysat 2023-02-20 17:37:44 +01:00
Jakob Rath
33a38ba96f simplify 2023-02-20 16:28:31 +01:00
Jakob Rath
1dea87a07a fix add_overflow 2023-02-20 16:25:41 +01:00
Jakob Rath
455abb1db3 update 2023-02-20 16:19:56 +01:00
Jakob Rath
4cca164bb4 fix 2023-02-20 16:13:55 +01:00
Jakob Rath
d5ce9b3d5e Try possible ule rewrite 2023-02-20 15:23:41 +01:00
Jakob Rath
b6480e789f Repropagate may need to update watchlist 2023-02-20 15:06:31 +01:00
Jakob Rath
61ec3b9e87 log_lemma 2023-02-20 12:32:21 +01:00
Jakob Rath
1d04d08a0c Update has_max_forbidden 2023-02-20 12:19:06 +01:00
Jakob Rath
af683ea5f9 avoid fallback to circuit 2023-02-20 12:09:11 +01:00
Jakob Rath
7f41761616 xnor 2023-02-20 11:56:23 +01:00
Jakob Rath
4501a372b1 fix boolean propagation 2023-02-20 09:39:44 +01:00
Jakob Rath
2c44018a8a get_watch_level 2023-02-20 09:37:28 +01:00
Clemens Eisenhofer
790229a5d9 Bug fix for inverse of lsb-mask 2023-02-18 17:29:33 +01:00
Clemens Eisenhofer
578f2ec4e8 Assertions 2023-02-18 14:26:45 +01:00
Clemens Eisenhofer
e8b4875a17 Multiply by inverse to detect more parity constraints 2023-02-18 14:15:51 +01:00
Clemens Eisenhofer
ae70a8e9f0 Blast only one bit per conflict 2023-02-17 17:26:19 +01:00