mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-02 18:08:57 +00:00
Code Activity
22122 commits 83 branches 58 tags 214 MiB
Commit graph

22122 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
a5c0ecafda fixes to model generation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-24 13:27:28 -07:00
Nikolaj Bjorner
5803c6f202 fix bug in non-emptiness witness extraction 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-24 13:27:28 -07:00
CEisenhofer
da9d8c8694 Asserting character constraints 2026-03-24 16:51:01 +01:00
CEisenhofer
48273ca0ed Fixed unit substitution 2026-03-24 16:24:28 +01:00
CEisenhofer
aab96dbd29 Rule for unwinding powers in membership constraints 2026-03-24 14:58:10 +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
Copilot
1c24c835c9
Fix three assertion violations in nseq string solver (#9106) 
- seq_model.cpp: skip trivial memberships in collect_var_regex_constraints;
  SAT leaf nodes can have "" in nullable_regex (trivial) in addition to
  primitive (single-variable) memberships after Brzozowski derivative
  consumption reduces a concrete string membership to empty.

- seq_nielsen.cpp: fix SASSERT(!var) typo in var_ub(); should be SASSERT(var)
  matching the pattern in var_lb().

- seq_regex.cpp: replace VERIFY(re_expr) with null guard in
  minterm_to_char_set(); nullptr means no regex constraint and should
  return the full alphabet, as the test test_minterm_nullptr_is_full expects.


Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/31db5346-9b60-4a20-a101-beca9fc9e4f8

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-23 13:20:06 -07: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
ced7952a7b
Implement not_contains_axiom in seq_axioms.cpp (#9098) 
* Implement not_contains_axiom in seq_axioms.cpp

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/2df315a7-6f41-4d22-9e77-1e778d97fdb8

* Rewrite not_contains_axiom using recfun recursive function instead of skolem predicate

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/28c9f40f-e66f-41b6-bec0-efff6bc9f902

* Use structural decomposition a = unit(nth(a,0)) ++ tail(a) in not_contains_axiom else-branch

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/e35f6eaa-4c4a-4629-bce2-c6a2a96e2ace

* Refactor tail_s initialization in seq_axioms.cpp

---------

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-22 21:34:45 -07:00
Copilot
8db175447b
Handle unit-unit prefix/suffix splits in simplify_and_init (#9097) 
When both leading (or trailing) tokens of a string equality are
is_char_or_unit(), split the equality:
  unit(a) ++ rest1 == unit(b) ++ rest2  ->  unit(a)==unit(b), rest1==rest2
  unit(a) ++ rest1 == unit(b)           ->  unit(a)==unit(b), rest1==empty
  unit(a) == unit(b) ++ rest2           ->  unit(a)==unit(b), empty==rest2
(symmetric suffix case handled too)

Add three unit tests covering prefix split, prefix split with empty
rest, and suffix split.


Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/565287e9-a121-4bae-8aa4-6c2ec93e660f

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-22 19:39:33 -07:00
Copilot
ad94dd1b7a
implement replace_all_axiom using recursive predicate ra(s,p,t,r) (#9095) 
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/c550da78-28c6-4ab4-9bfb-7403ecc3320b

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-22 18:44:29 -07:00
Nikolaj Bjorner
d1d050f69f not-contains placeholder 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-22 18:40:08 -07:00
Nikolaj Bjorner
7b27866310 simplify solution conditions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-22 18:30:52 -07:00
Copilot
e0ca916e23
refactor: move nielsen graph display/to_dot routines into seq_nielsen_pp.cpp (#9090) 
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/c2457bcf-85f0-4ad7-9ff1-d394f4315698

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-22 17:44:22 -07:00
Nikolaj Bjorner
00aac9a6a4 replace NYI by exceptions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-22 16:07:48 -07:00
Nikolaj Bjorner
1863290b71 add deterministic solving for unit equations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-22 15:34:16 -07:00
Copilot
6b5401ef68
Remove s_other from snode_kind; unify under s_var and is_var() (#9087) 
* remove s_other, use s_var and is_var() instead

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/d56594ed-7f7e-436a-a4b2-e6dc986b18a8

* fix build: add reset() override to test dummy solver stubs

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/d437376d-55d8-4087-baf1-e89451d2d597

---------

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-22 12:05:24 -07:00
CEisenhofer
63830085b6 Delete unsupported testcases 2026-03-22 13:11:08 +01:00
Nikolaj Bjorner
aa210882c5 add review 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-21 10:14:34 -07:00
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