mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-16 23:25:36 +00:00
Code Activity
22462 commits 86 branches 58 tags 205 MiB
Commit graph

22462 commits

This branch
This branch
All branches
Author SHA1 Message Date
CEisenhofer
e045e650da Fixed order of undoing 2026-04-23 17:18:04 +02:00
Nikolaj Bjorner
ace4105a90 fix test build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-23 08:06:15 -07:00
Nikolaj Bjorner
5f7e14315d fix tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-22 10:54:06 -07:00
CEisenhofer
3873f387be Model construction has to respect the length constraints 2026-04-22 19:51:09 +02:00
CEisenhofer
0a1eb26952 Avoid Skolem functions for length and symbolic characters introduced during Nielsen saturation (power exponents are still Skolem functions) 2026-04-22 11:06:55 +02:00
Nikolaj Bjorner
aed76af2b5 deal with code smells/duplicate 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-21 18:57:25 +02:00
CEisenhofer
46364a1502 Extract argument of unit when adding constant character to range 2026-04-21 18:54:36 +02:00
CEisenhofer
8b2643ff02 Missing unit around symbolic characters 2026-04-21 18:38:03 +02:00
Nikolaj Bjorner
b2fa00ecf4 fix vector<le, false> to vector<le> we need the copy and destructor semantics for expr_ref 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-21 18:37:23 +02:00
CEisenhofer
03c990e0e1 Push substitutions back to base solver 2026-04-21 18:29:40 +02:00
Nikolaj Bjorner
4446705eae clean up conflict generation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-21 18:28:25 +02:00
Nikolaj Bjorner
3296681a19 add code review comments 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-21 17:17:19 +02:00
Nikolaj Bjorner
40122b494c add comments, fix a bug in early return for min-term version of expansion 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-21 16:49:29 +02:00
Nikolaj Bjorner
3beeadfe51 nits 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-21 16:20:17 +02:00
CEisenhofer
ec92a532b8 Use dedicated string variables based on mod. count 2026-04-21 10:53:35 +02:00
Nikolaj Bjorner
8cc85a7d7b code simplification, fix conflict in new_diseq_eh 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-21 10:17:43 +02:00
Nikolaj Bjorner
352b14fe2b fix and optimize not-contains and regex equalities 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-21 09:16:00 +02:00
Nikolaj Bjorner
c18188cba8 avoid crashes in cases like wildcard-matching-regex-67.smt2, need regex constraint solving 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-21 05:44:53 +02:00
Nikolaj Bjorner
e172aa370d add simplification rule to concatentations of regex to avoid stack overflow in derivatives of very long expressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-20 18:20:43 +02:00
CEisenhofer
41412293fe Let's try to justify bounds 2026-04-20 15:52:35 +02:00
Nikolaj Bjorner
0bcdca787f fix crashes when using replace_all 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-16 22:37:36 +02:00
Nikolaj Bjorner
64e7f29533 remove spurious include 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-16 04:57:27 +02:00
Nikolaj Bjorner
c97aebe2b6 remove spurious ref 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-16 04:53:39 +02:00
CEisenhofer
82df1afeaf tentative solution: use existing nullability check (we might want to check in the future which guards of the ITE are actually true) 2026-04-14 18:07:03 +02:00
Nikolaj Bjorner
f09f6d5097 add internalization as fallback option 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-14 08:47:55 -07:00
Nikolaj Bjorner
725b13680e na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-14 08:39:22 -07:00
CEisenhofer
0c4e4ad702 Regex factorization missed some justifications 2026-04-14 17:19:07 +02:00
CEisenhofer
2db99473a3 Removed irrelevant information from membership constraints 2026-04-14 16:27:50 +02:00
CEisenhofer
195f2caf25 Removed strange code that caused the solver to give up when finding a model instantly 2026-04-14 16:06:03 +02:00
CEisenhofer
3fdd903373 Bug if uninternalized literal becomes internalized and immediately false 2026-04-14 15:48:13 +02:00
CEisenhofer
ed4387c70e Log to file 2026-04-14 11:47:26 +02:00
Nikolaj Bjorner
acae332b13 add spp for easier pretty printing snode 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-14 00:39:01 -07:00
Nikolaj Bjorner
53cc320efa deps 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-14 00:29:58 -07:00
Nikolaj Bjorner
68d7917653 debug printing for widening 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-13 12:16:03 -07:00
Nikolaj Bjorner
035ea95faa add pp methods 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-13 11:41:58 -07:00
CEisenhofer
9155ce85bb Removed unused function 2026-04-13 15:05:41 +02:00
CEisenhofer
d620f20c63 Simplify code 2026-04-13 14:06:16 +02:00
Nikolaj Bjorner
276b9c38af log conflict 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-13 04:41:38 -07:00
Nikolaj Bjorner
4dfb6f7a7d display node state 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-12 15:45:03 -07:00
Nikolaj Bjorner
1be70988b9 add logging for length / Parikh bug 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-12 15:34:22 -07:00
CEisenhofer
95d28ad02c Fixed the model generation fix 2026-04-12 19:34:11 +02:00
Nikolaj Bjorner
2a142cd150 recompile aw 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-11 10:12:03 -07:00
CEisenhofer
e584895c98 Make model extraction a bit more stable 2026-04-10 18:15:06 +02:00
CEisenhofer
2b7204b07c Does model construction work properly now? 2026-04-10 17:59:16 +02:00
CEisenhofer
e6ef0d29c4 We need to check local consistency over and over again 2026-04-09 15:56:00 +02:00
CEisenhofer
09572b20ed Character ranges must be passed back to the solver 2026-04-09 15:21:12 +02:00
CEisenhofer
aafb704cf8 Bug fix in model extraction 2026-04-09 14:42:48 +02:00
CEisenhofer
d127055841 fix(nseq): handle empty children in apply_regex_factorization 2026-04-09 14:24:44 +02:00
CEisenhofer
a36254f104 Some more bug fixes 2026-04-09 13:47:29 +02:00
CEisenhofer
38d725dc5a Deriving by allchar should not crash 2026-04-09 11:48:35 +02:00