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

196 commits

Author SHA1 Message Date
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
64e7f29533 remove spurious include 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-16 04:57:27 +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
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
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
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
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
8eb0ac29d9 We have to check for local conflicts before clearing the flag 2026-04-09 11:42:30 +02:00
CEisenhofer
598e4ede4e Removed debug code 2026-04-09 11:03:18 +02:00
CEisenhofer
803018b7c3 We forgot relevant equations with one side being empty 2026-04-09 10:40:33 +02:00
CEisenhofer
684f93bed4 We should not stop eagerly on local conflicts 2026-04-08 20:13:54 +02:00
CEisenhofer
857e93fdb2 Substitutions are extensions 2026-04-08 19:13:10 +02:00
CEisenhofer
513f49f39c Debugging 2026-04-08 18:48:47 +02:00
CEisenhofer
86dc9d3268 We need to reset local conflicts 2026-04-08 18:24:11 +02:00
CEisenhofer
26ededa891 More debug info 2026-04-08 18:00:52 +02:00
CEisenhofer
26d36ba6ee Missing justification added 
Added check for correctness of conflict core
 2026-04-08 10:15:27 +02:00
CEisenhofer
c7e7b40d40 Fix 2026-04-08 09:27:46 +02:00
CEisenhofer
f895548154 Check for range conflicts for characters 2026-04-07 10:49:23 +02:00
CEisenhofer
1a1961be2f Removed tracking disequality 2026-04-07 10:33:44 +02:00
CEisenhofer
3e24cb7c10 Bug 2026-04-07 09:33:14 +02:00
CEisenhofer
2a32aa0204 fix(nseq): assert sub-sequence equalities to the SAT core 2026-04-04 19:11:36 +02:00
Nikolaj Bjorner
b60a44c66b classical 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-03 10:33:28 -07:00
Nikolaj Bjorner
95dc44b409 bugfix, better debug display of failure 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-03 09:08:22 -07:00
Copilot
fa89910452
Add SASSERT invariants and pre/postconditions to Nielsen seq solver (#9216) 
* Initial plan

* Add SASSERT invariants and pre/postconditions to Nielsen seq solver

Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/24442582-8437-45ae-a58f-957ac2bdf698

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Add clarifying comment to m_str_eq.empty() postcondition

Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/24442582-8437-45ae-a58f-957ac2bdf698

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-04-02 21:09:23 -07:00
Copilot
ddd8bf84d7
Replace apply_regex_unit_split with apply_regex_if_split (#9210) 
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/7df36402-f2c7-4de5-b626-3df14d4eee64

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-04-02 14:27:06 -07:00
Nikolaj Bjorner
e59ee306e9 allow literals to be false in model validation - we can't enforce lack of propagation after internalizing literals, especially if literals are repeated (modulo permutation of equality) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-02 12:51:47 -07:00
Nikolaj Bjorner
3629cd9447 regression fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-02 11:42:50 -07:00
CEisenhofer
9b3826ed86 Missing case in concatenation 2026-04-02 20:08:00 +02:00
CEisenhofer
a81ce477f5 Added classical regex factorization 2026-04-02 20:08:00 +02:00
Nikolaj Bjorner
b0a4a15c98 updated tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-02 10:04:02 -07:00
CEisenhofer
34cb0a17fc str.at wants a special treatment... 2026-04-02 18:33:44 +02:00
CEisenhofer
1e567a4a26 Bug fixes 2026-04-02 10:26:36 +02:00
CEisenhofer
42f421ee09 Detect that adding side constraint caused a conflict 2026-04-01 20:38:15 +02:00
Nikolaj Bjorner
4524ebe614 fix type error 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-01 10:35:10 -07:00