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

22123 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
bc5818e12d fix bogus decompose_ite 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-24 14:43:56 -07:00
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