mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-18 11:04:09 +00:00
Code Activity
22051 commits 66 branches 58 tags 203 MiB
Commit graph

22051 commits

This branch
This branch
All branches
Author SHA1 Message Date
CEisenhofer
39bf6af870 Missing file edits 2026-03-16 21:10:40 +01:00
CEisenhofer
e439504ec8 Delete cached substitutions completely (for now) to avoid dangling pointers after backtracking 2026-03-16 21:04:47 +01:00
CEisenhofer
84d371f2e9 Bugfix in regex overapproximation 2026-03-16 19:54:12 +01:00
CEisenhofer
16f693b09a Regex intersection bug fixe 2026-03-16 16:30:20 +01:00
Nikolaj Bjorner
256f1bdf1a remove non-compiling timeout code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-15 21:39:14 -07:00
Nikolaj Bjorner
32eedde897 disable rewrite that makes nseq solving harder 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-15 21:36:22 -07:00
Nikolaj Bjorner
db8a2f4f9e update print and cancelation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-15 20:43:49 -07:00
Nikolaj Bjorner
7dea14f732 move statistics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-15 20:09:19 -07:00
Nikolaj Bjorner
d137f25b65 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-15 19:58:21 -07:00
Nikolaj Bjorner
d15aed0d04 code organization in theory_nseq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-15 19:39:53 -07:00
Nikolaj Bjorner
a4c9a5b2b0 add review comments 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-15 12:23:17 -07:00
Copilot
1a8570ed3f
Refactor seq_nielsen: address NSB review comments (#8993) 
* Initial plan

* Refactor seq_nielsen: m_graph reference, accessor methods, seq_util.is_power, m.are_equal/are_distinct

- Add ast_manager& m_m and seq_util& m_seq members to nielsen_graph with accessors
- Change m_graph from pointer to reference in nielsen_node
- Remove redundant g parameter from simplify_and_init (use m_graph instead)
- Use seq.str.is_power() matcher in get_power_base/exp_expr and handle_empty_side
- Use m.are_equal/are_distinct for E-graph-aware token comparison
- Fix seq.is_const_char unchecked return value
- Simplify has_char/all_eliminable loop with std::any_of/all_of
- Fix rebuilt=nullptr pattern in merge_adjacent_powers and simplify_const_powers
- Add formal Spec: comments for DirectionalInconsistency and CommPower cancellation
- Remove addressed NSB review comments

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

* Fix CI: update test files for simplified simplify_and_init signature

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: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-15 10:35:45 -07:00
Copilot
d53846d501
nseq: port ZIPT regex pre-check to fix benchmark discrepancy on regex-only problems (#8994) 
* Initial plan

* Port ZIPT regex pre-check and DFS node budget to address nseq benchmark discrepancy

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-15 10:10:53 -07:00
Copilot
2212f59704
seq_model: address NSB review comments (#8995) 
* Initial plan

* Address NSB review comments in seq_model.cpp

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

* Address code review feedback: improve null-sort handling in seq_model and some_seq_in_re

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-14 21:55:32 -07:00
Nikolaj Bjorner
6947698d65 add notes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-14 16:03:04 -07:00
Nikolaj Bjorner
b5dae574ad add review notes to seq_model 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-14 15:49:00 -07:00
Nikolaj Bjorner
4c64c82cef update workflow 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-14 12:32:29 -07:00
Nikolaj Bjorner
40b9d80ae5 more review 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-14 12:20:01 -07:00
Nikolaj Bjorner
744d75e8cc more review 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-14 12:10:12 -07:00
Nikolaj Bjorner
0dc5b4eef5 add review comments 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-14 11:59:47 -07:00
Copilot
5a3dbaf9f3
Move nseq_regex/state into smt/seq and seq_model into smt/; rename to seq_* prefix (#8984) 
* Initial plan

* build verified: nseq_regex moved to smt/seq

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

* rename nseq_regex/state/model to seq_regex/state/model in smt/seq; add Clemens Eisenhofer as co-author

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

* seq_model: remove theory_nseq dependency; get family_id from seq_util

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

* Add comments for regex enhancements in seq_model

Added comments regarding future improvements for regex handling.

* Add comments for large exponent handling

Add comments for handling large exponents in seq_model.cpp

* Revise comments for clarity on sort usage

Updated comments to reflect review suggestions regarding the use of the sort of 'n'.

* seq_state: remove sgraph dep; seq_model: use snode sort for is_empty; remove NSB review comments

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

* Update seq_state.h

* Remove unnecessary include for smt_context.h

* move seq_model from smt/seq/ to smt/; fix seq_state.h add_str_mem typo

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-14 11:45:32 -07:00
Nikolaj Bjorner
27f5541b0b updates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-13 18:19:25 -07:00
Nikolaj Bjorner
8a48caf742 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-13 10:25:43 -07:00
Nikolaj Bjorner
df9df50a71 update generation of empty sequence to take sort argument, fix mk_concat substitution 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-13 10:03:52 -07:00
CEisenhofer
e384e8f3d4 Added right-to-left rules 2026-03-13 17:25:14 +01:00
CEisenhofer
ff6534b53e Updated script to optionally compare against ZIPT as well 2026-03-13 10:24:06 +01:00
Nikolaj Bjorner
e9ab936dea perf exploration 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-12 20:27:04 -07:00
Nikolaj Bjorner
e5da478f20
Merge pull request #8969 from Z3Prover/copilot/fix-build-in-c3 
Fix build: missing comma in nielsen_graph constructor initializer list
 2026-03-12 14:13:35 -07:00
copilot-swe-agent[bot]
c6cfd43ab2 Fix build: correct constructor initializer list syntax in seq_nielsen.cpp 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-12 20:16:52 +00:00
copilot-swe-agent[bot]
196ce815f3 Initial plan 2026-03-12 19:55:20 +00:00
Nikolaj Bjorner
acbf5c6e4a
Merge pull request #8938 from Z3Prover/copilot/add-parikh-filter-implementation-again 
Add seq_parikh.h and seq_parikh.cpp: Parikh image filter for ZIPT Nielsen solver
 2026-03-12 09:20:18 -07:00
Nikolaj Bjorner
5d0f5dc4e5
Merge branch 'c3' into copilot/add-parikh-filter-implementation-again 2026-03-12 09:20:03 -07:00
CEisenhofer
3ad9c290fc Use length information during Nielsen saturation 2026-03-12 17:01:44 +01:00
CEisenhofer
e8354a783a Power base compression 2026-03-12 13:24:20 +01:00
CEisenhofer
bee9fd82f0 Another power bug 2026-03-12 12:59:03 +01:00
CEisenhofer
87c5be8904 Fixed progress annotations 2026-03-12 11:22:42 +01:00
CEisenhofer
1351efe9af Unit cases 2026-03-12 11:13:18 +01:00
copilot-swe-agent[bot]
9813b2adfb Merge branch 'c3' of https://github.com/Z3Prover/z3 into copilot/add-parikh-filter-implementation-again 2026-03-12 04:22:43 +00:00
Nikolaj Bjorner
a567a7edfb
Merge pull request #8949 from Z3Prover/copilot/remove-dependency-smt-kernel 
Remove smt_kernel.h dependency from seq_nielsen.cpp
 2026-03-11 20:13:59 -07:00
copilot-swe-agent[bot]
dac52ae4e0 remove smt_kernel.h dependency from seq_nielsen.cpp 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-12 03:00:38 +00:00
copilot-swe-agent[bot]
bd9b5337af Initial plan 2026-03-12 02:53:14 +00:00
Nikolaj Bjorner
6fa3c7eabb
Merge branch 'c3' into copilot/add-parikh-filter-implementation-again 2026-03-11 19:27:03 -07:00
Nikolaj Bjorner
db7db05eff
Merge pull request #8943 from Z3Prover/copilot/update-simple-solver-incremental-mode 
nielsen: use simple_solver incrementally with push/pop scopes in DFS
 2026-03-11 19:24:34 -07:00
Nikolaj Bjorner
3d36fb95ec
Merge branch 'c3' into copilot/update-simple-solver-incremental-mode 2026-03-11 19:24:21 -07:00
copilot-swe-agent[bot]
a51ba544ea Fix typo: rename m_parith to m_parikh in seq_nielsen.h/.cpp 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-11 19:08:11 +00:00
copilot-swe-agent[bot]
4b2f5e2bb0 Add seq_parikh unit tests: 32 tests covering stride, constraints, conflict, char_set 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-11 18:36:28 +00:00
copilot-swe-agent[bot]
30c2a9ccdc Address code review: add SASSERT for lo>hi, simplify is_to_re handling 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-11 17:23:00 +00:00
copilot-swe-agent[bot]
194dfe6c61 Port ZIPT Parikh features: minterm_to_char_set, char range constraints, fix stride soundness 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-11 17:21:27 +00:00
CEisenhofer
99727faf70 Model reconstruction 2026-03-11 18:13:16 +01:00
copilot-swe-agent[bot]
255d381b72 Make simple_solver incremental: use push/pop scopes in Nielsen DFS 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-11 17:09:34 +00:00