mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-30 04:18:53 +00:00
Code Activity
22797 commits 77 branches 58 tags 269 MiB
Commit graph

132 commits

Author SHA1 Message Date
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
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
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
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
CEisenhofer
598e4ede4e Removed debug code 2026-04-09 11:03:18 +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
74cf21b852 Bug in model extraction 
Added debug check
 2026-04-08 16:37:21 +02:00
CEisenhofer
26d36ba6ee Missing justification added 
Added check for correctness of conflict core
 2026-04-08 10:15:27 +02:00
CEisenhofer
8298ba6011 Quick fix for some unsound cases 2026-04-04 18:36:25 +02:00
CEisenhofer
a58a9114d2 Fix str.< Skolem length generation overhead 2026-04-04 18:32:02 +02: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
CEisenhofer
a81ce477f5 Added classical regex factorization 2026-04-02 20:08:00 +02:00
Nikolaj Bjorner
3ca960d679 test that there is a model 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-02 10:49:09 -07:00
CEisenhofer
a8db876765 Fix problem with divisibility predicate 2026-04-02 16:25:49 +02:00
CEisenhofer
5ec28d3bc8 Eliminate length gradients from regexes 2026-04-02 15:58:15 +02:00
CEisenhofer
1282e4de11 Prevent unsoudness because of missing length propagation 2026-04-02 14:34:46 +02:00
Nikolaj Bjorner
2245451e96 remove aux function 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-01 19:07:37 -07:00
Nikolaj Bjorner
b1dc2f2be2 It is possible that a non-internalized expression gets assigned to false immediately by internalization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-01 11:49:25 -07:00
CEisenhofer
36b01a51f1 Properly extract justifications from subsolver 2026-04-01 16:58:26 +02:00
CEisenhofer
e25e93503b First try to do better dependency tracking 2026-04-01 15:23:38 +02:00
CEisenhofer
60913f0068 Output both Nielsen graph size and conflict size 2026-04-01 10:23:55 +02:00
CEisenhofer
5d95f44a03 Conflict logging 2026-04-01 10:08:03 +02:00
Nikolaj Bjorner
9aceaf3cac reviewing seq_nielsen, detect repeated final-check to avoid rebuilding nielsen graph 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-30 00:01:24 -07:00
Nikolaj Bjorner
684cb23b40 turn on constraint integrity checking 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-29 19:30:13 -07:00
Nikolaj Bjorner
d7ee475bc3 ensure equalities are propagated 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-29 16:47:05 -07:00
Copilot
09cde1f80c
Port propagate_eq from theory_seq for sk().is_eq in theory_nseq (#9165) 
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/7c0a330f-3f9f-4c5d-99f2-47fad013538f

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-29 15:44:18 -07:00
Nikolaj Bjorner
3db734d249 add note about propagate-eq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-29 15:19:36 -07:00
CEisenhofer
3b5b53126e Bug fixing with unit replacement 2026-03-26 15:56:58 +01:00
Nikolaj Bjorner
fa4cd37c07 add the false literal callback 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-25 13:35:25 -07:00
Nikolaj Bjorner
77d86343d0 add the false literal callback 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-25 13:35:18 -07:00
CEisenhofer
910c68cd42 Missing internalization 2026-03-25 20:21:54 +01:00
Nikolaj Bjorner
af4677950b add code for adding assumptions after sat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-25 11:45:43 -07:00
Nikolaj Bjorner
9d2244798d fix insertions into subst. 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-25 09:00:37 -07:00
Copilot
46c76d89e0
Make dep_mgr private in seq_nielsen; expose conflict sources vector (#9129) 
* make dep_mgr private in seq_nielsen, expose conflict_sources vector

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/998d8021-4808-4feb-afc5-b2447c6a64e5

* move deps_to_lits to seq namespace in seq_nielsen

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/8d736478-8f9b-4451-8d1f-539ce72525c7

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-25 08:05:00 -07:00
CEisenhofer
178d7439f2 Fixed to_dot for integer constraints 2026-03-25 11:25:07 +01:00
CEisenhofer
538fbc1b8d Added unit (not char) case in apply_const_nielsen 2026-03-24 13:34:39 +01:00
CEisenhofer
b74f0bbb00 Signature splits 
Fixed dot printing errorfor Skolems
 2026-03-24 13:20:30 +01:00
Nikolaj Bjorner
dbdccbff97 use recursive function for not-contains 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-23 13:18:34 -07:00
Copilot
2ab53072e9
Implement ensure_digit_axiom in theory_nseq (#9075) 
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/9b679ca3-dba7-469c-907a-9abd5edf1e1d

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-20 19:46:22 -07:00
CEisenhofer
2bd5283f6a Assertions 2026-03-20 15:11:51 +01:00
Nikolaj Bjorner
0f4126f665 add filter for avoiding creating redundant disequality axioms 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-19 23:15:23 -07:00
Nikolaj Bjorner
7a93e2296d coding nit 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-19 16:39:40 -07:00