mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-17 15:39:27 +00:00
Code Activity
22513 commits 86 branches 58 tags 206 MiB
Commit graph

22513 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
a12be9670c remove print 2026-05-16 17:05:51 -07:00
Nikolaj Bjorner
1198d9aaa5 templatize vector for dependencies 2026-05-16 16:22:56 -07:00
Nikolaj Bjorner
d99f0ce230 use shrink instead of pop in a loop 2026-05-16 16:22:56 -07:00
Nikolaj Bjorner
5ca32d65bd use shrink instead of pop in a loop 2026-05-16 16:22:56 -07:00
Nikolaj Bjorner
b8052d67cb simplification to value reconstruction 
use the fact that dependencies are already present in the model-value object.
There is no need for fragile code to reconstruct the mapping from enodes to values.
 2026-05-16 16:22:51 -07:00
CEisenhofer
b77d2b3360 We need a better witness during model construction 2026-05-16 16:21:57 +02:00
CEisenhofer
501462b494 Fix for model construction (?) 2026-05-16 15:27:30 +02:00
CEisenhofer
723e19b435 Updated string benchmark script 2026-05-16 14:39:44 +02:00
Nikolaj Bjorner
1405547dc0 iterate on model construction 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-05-13 11:38:02 -07:00
Copilot
27cd086d24
Fix python build: remove circular smt_enode.h include from seq_nielsen.cpp (#9508) 
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/e0d3c96d-3caa-4c0b-a723-d0fb4a9db3c9

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-05-12 13:33:02 -04:00
CEisenhofer
71d7d70080 Missing dependency bug. Still not fixed, but better now 2026-05-12 14:00:50 +02:00
CEisenhofer
c9fb432191 The side-condition of the "if"-split belongs on the edges 2026-05-12 10:30:29 +02:00
CEisenhofer
bb639af485 Bit more pp 2026-05-12 09:29:49 +02:00
CEisenhofer
22583a7abd Typo in pp: lt != le 2026-05-12 09:08:47 +02:00
CEisenhofer
55ea1929e9 A bit more "dot" improvements 2026-05-11 19:22:45 +02:00
CEisenhofer
d20a27e1df Make dot output a bit more readable 2026-05-11 19:17:00 +02:00
CEisenhofer
fb6b05aa83 Fixed the "partial automaton" after we push regex unwinding to ITE splitting 2026-05-11 17:57:06 +02:00
Nikolaj Bjorner
7ec3bf55ff merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-05-07 10:48:03 -04:00
CEisenhofer
50f471a95b For membership constraints just unwind 2026-05-07 16:20:04 +02:00
CEisenhofer
f7f2ee8f74 Using only one solver 2026-05-07 15:49:16 +02:00
CEisenhofer
712cd68e8c Don't add duplicate equations and membership constraints to Nielsen root 2026-05-06 16:38:26 +02:00
CEisenhofer
e62ba9b60b stoi lemmas might have been forgotten so we need to reassert 2026-05-06 15:46:53 +02:00
CEisenhofer
6fa354102a A new axiomatization for "stoi" 2026-05-06 15:30:09 +02:00
Nikolaj Bjorner
57692811fa reduce set of assumptions passed into m_core_solver 2026-05-06 03:58:29 -07:00
CEisenhofer
11ff3ccae7 Power unwinding was unsound 2026-05-06 10:22:39 +02:00
Nikolaj Bjorner
8c02ec087b fix crash with D:\\bench\\inputs\\QF_S\\20240318-omark\\cyclic-xy.smt2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-05-05 10:53:12 -07:00
CEisenhofer
b65f22ef3b Bug fix 2026-05-05 14:58:42 +02:00
CEisenhofer
e7cc24d7ea Next step towards partial automata 2026-05-05 13:58:15 +02:00
CEisenhofer
bfa9d17408 We need new variables 2026-05-05 10:48:49 +02:00
Nikolaj Bjorner
e242257070 avoid disequalities from str.at axioms 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-05-04 16:33:12 -07:00
Nikolaj Bjorner
af2769dbc0 more logging for when arith_value fails 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-05-04 14:07:49 -07:00
Nikolaj Bjorner
a5c01dcddb move to new model construction instead of original 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-05-04 13:53:33 -07:00
CEisenhofer
e2e876c7a9 Removed legacy code 2026-05-04 20:16:13 +02:00
CEisenhofer
5b3d734ecb Fixed regex factorization again 2026-05-04 19:25:07 +02:00
CEisenhofer
adb9ca4305 Some steps towards partial automatons 2026-05-04 18:31:38 +02:00
Nikolaj Bjorner
b199b0782a ignore ostrich files under tests 2026-05-03 13:59:37 -07:00
Nikolaj Bjorner
266008e81f update seq_model draft 
redo seq_model to be compatible with model_generator
 2026-05-03 13:57:56 -07:00
Nikolaj Bjorner
e1d3eb1a80 flag replace_all as unhandled 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-05-02 15:53:36 -07:00
Nikolaj Bjorner
2c45740986 iterate on seq_model redo draft 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-05-02 15:47:19 -07:00
Nikolaj Bjorner
3eaa5b7ab7 iterate on seq_model redo draft 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-05-02 15:37:39 -07:00
Nikolaj Bjorner
6abb2da6a1 update draft 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-05-02 10:40:53 -07:00
Nikolaj Bjorner
466bfea604 add draft for model construction 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-05-01 11:07:27 -07:00
Nikolaj Bjorner
c7ccca0873 fix bug exposed in ostrich substr_var_sat.smt2 crash. Add notes to seq_model.cpp to prepare for further fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-30 10:25:15 -07:00
Copilot
42582c6835
euf_seq_plugin: fix identity elimination after merge, activate loop merging, integrate sgraph improvements (#9414) 
* Initial plan

* Initial plan

* Fix identity elimination after merge and activate loop merging in euf_seq_plugin

Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/053b94e4-645a-4cde-ae5d-cf6d61222f92

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

* Apply three ZIPT code review improvements to euf_seq_plugin

Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/da8647c4-ddff-47ce-9364-2eee3810c38d

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

* Address code review: improve loop-merge defensive code and test variable names

Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/053b94e4-645a-4cde-ae5d-cf6d61222f92

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

* Refactor: extract saturating_add helper, simplify hash-check condition

Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/da8647c4-ddff-47ce-9364-2eee3810c38d

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-29 11:12:00 -07:00
Nikolaj Bjorner
f461369ab8 fix tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-26 08:23:26 -07:00
Nikolaj Bjorner
014315764d re-fix the same bug pointed out to an earlier version 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-26 08:16:37 -07:00
Nikolaj Bjorner
b28f83e2e0 add initial scaffolding for using assumption literals 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-25 08:09:25 -07:00
Nikolaj Bjorner
abbe36561d cleanup service 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-24 17:22:04 -07:00
Nikolaj Bjorner
cedd896ea5 redo length re-computation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-24 15:49:19 -07:00
Nikolaj Bjorner
7fc68d20ea brain got parked somewhere? 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-23 19:16:18 -07:00