mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-23 12:59:12 +00:00
Code Activity
22102 commits 76 branches 58 tags 207 MiB
Commit graph

22102 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
a39ff701c7 remove include of nielsen in sgraph 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-21 09:48: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
Copilot
f518faac9b
Add nseq issue drafts from Ostrich benchmark analysis (discussion #9071) (#9073) 
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/04321ea7-2a53-4ed5-9f43-816dc6f7476b

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:07:51 -07:00
Nikolaj Bjorner
8ef491edea new instructions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-20 14:59:59 -07:00
Nikolaj Bjorner
35c400dd18 updated agentics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-20 13:03:16 -07:00
Nikolaj Bjorner
0bfab0223a add ostrich benchmark markdown for agent to read in the c3 branch 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-20 11:33:36 -07:00
Nikolaj Bjorner
ae12956545 updates based on discussion 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-20 11:20:29 -07:00
CEisenhofer
a99b93ef1f Added testcases 2026-03-20 18:40:55 +01:00
CEisenhofer
2bd5283f6a Assertions 2026-03-20 15:11:51 +01:00
CEisenhofer
88ef8c7cda Another regex witness bug 2026-03-20 14:07:12 +01:00
CEisenhofer
737c5d44ed Simplify regex splits 2026-03-20 13:33:53 +01:00
CEisenhofer
5d912bdfa5 ... 2026-03-20 12:22:38 +01:00
CEisenhofer
fdb7f33552 ... one more 2026-03-20 12:20:16 +01:00
CEisenhofer
e3ed7f214b Removed debug lines 2026-03-20 12:19:53 +01:00
CEisenhofer
9aaf103ca0 Fix union problem (might not solve all bugs) 2026-03-20 12:17:44 +01:00
CEisenhofer
4f884e7d9a Bug 2026-03-20 12:11:18 +01:00
CEisenhofer
a873d5cdda Fixed output error 2026-03-20 11:51:37 +01:00
CEisenhofer
3662b89adc Missing range cases 2026-03-20 10:41:56 +01:00
Nikolaj Bjorner
d77e9d5c95 add code review comment 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-20 00:26:57 -07: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
1d928663de add reset method 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-19 22:57:59 -07:00
Nikolaj Bjorner
a895548b99 cleanup 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-19 16:39:41 -07:00
Nikolaj Bjorner
7a93e2296d coding nit 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-19 16:39:40 -07:00
Copilot
2ec305f206
port range regular expressions to snode from ZIPT (#9048) 
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-19 15:59:20 -07:00
Copilot
59bc9b17ea
theory_nseq: remove seq_state, embed tracked entries directly in prop_queue (#9045) 
* Remove seq_state: embed tracked_str_eq/tracked_str_mem directly in prop_queue

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

* theory_nseq: use type aliases for eq_item/mem_item instead of wrapper structs

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

* seq_model: validate_regex takes single tracked_str_mem, caller loops

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-03-19 14:45:53 -07:00
Copilot
8795bf06fb
theory_nseq: dispatch assign_eh on all seq predicate cases via m_axioms, add enqueue/dequeue_axiom with variant prop_item (#9040) 
* dispatch assign_eh cases via m_axioms: add prefix/suffix/contains true axioms

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

* fix build: remove stale snode_label_html declaration from seq_nielsen.h

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

* theory_nseq: add enqueue/dequeue_axiom + std::variant prop_item + relevant_eh

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>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-19 10:42:18 -07:00
CEisenhofer
109ab7d098 Fixed regex witness 2026-03-19 17:16:29 +01:00
CEisenhofer
d31968f0ad Added problematic case as unit-test 2026-03-19 17:09:51 +01:00
CEisenhofer
51f3996464 Create dummy sat-node to avoid problems in case the preprocessor solves the problem entirely 2026-03-19 16:02:51 +01:00
CEisenhofer
9f4e823c8b ... and another one... 2026-03-19 15:44:15 +01:00
CEisenhofer
4271bdad55 Another minterm bug 2026-03-19 15:12:22 +01:00
CEisenhofer
149a087f65 Strengthened diseq axiom 2026-03-19 11:14:07 +01:00
Copilot
f837651434
seq_nielsen: replace mk_fresh_var() with mk_fresh_var(sort* s) (#9037) 
* replace mk_fresh_var() with mk_fresh_var(sort* s) in seq_nielsen; fix snode_label_html linkage

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

* remove mk_var(symbol const&) from sgraph; update all callers to pass sort explicitly

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-03-18 20:41:41 -07:00
Nikolaj Bjorner
4b40969da6 added diseq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-18 13:32:18 -07:00
Nikolaj Bjorner
a2352529f8 add diseq axiom 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-18 12:58:27 -07:00
CEisenhofer
777bda01a5 Subsolver was not reset properly 2026-03-18 20:22:08 +01:00
Nikolaj Bjorner
c43df60182 fix build of unit tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-18 10:29:41 -07:00
Nikolaj Bjorner
23b7e109bd partial updates to test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-18 10:04:07 -07:00
Nikolaj Bjorner
8ac8eb4ae7 create sub-class for tracked eq and mem relations to separate from seq_nielsen 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-18 10:04:01 -07:00
CEisenhofer
e7431400b4 Regex bug fixes (still not there) 2026-03-18 18:01:44 +01:00
CEisenhofer
983379f5e2 Missing semicolon 2026-03-18 16:16:59 +01:00
CEisenhofer
0a32337f0a Removed some brackets 2026-03-18 16:15:37 +01:00
CEisenhofer
d8a6ea1321 Fixed crasb if regex is reported SAT by pre-check 2026-03-18 16:08:02 +01:00
CEisenhofer
579ac6bfc4 Updated script 2026-03-18 15:45:56 +01:00
CEisenhofer
43950569eb More fixes 2026-03-18 15:41:27 +01:00
CEisenhofer
b288c2e7dc Some more bug fixes 2026-03-18 14:54:12 +01:00
CEisenhofer
ab53889c10 Fixed couple of regex problems [there are still others] 2026-03-18 14:29:18 +01:00
Nikolaj Bjorner
b1bae695e6 comment 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-17 16:32:01 -07:00
Nikolaj Bjorner
2847dd8bb3 small simplification 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-17 16:30:53 -07:00
Nikolaj Bjorner
3719b449e8 re-organize dependencies 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-17 16:18:27 -07:00