mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-20 11:55:49 +00:00
Code Activity
22037 commits 67 branches 58 tags 205 MiB
Commit graph

22037 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
9c36e9ce62
Revise comments for clarity on sort usage 
Updated comments to reflect review suggestions regarding the use of the sort of 'n'.
 2026-03-14 10:30:12 -07:00
Nikolaj Bjorner
aa5267cb9c
Add comments for large exponent handling 
Add comments for handling large exponents in seq_model.cpp
 2026-03-14 10:28:21 -07:00
Nikolaj Bjorner
ba7b0392fe
Add comments for regex enhancements in seq_model 
Added comments regarding future improvements for regex handling.
 2026-03-14 10:26:50 -07:00
copilot-swe-agent[bot]
1437ec25ce seq_model: remove theory_nseq dependency; get family_id from seq_util 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-14 17:20:47 +00:00
copilot-swe-agent[bot]
e01872dc70 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>
 2026-03-14 16:54:32 +00:00
copilot-swe-agent[bot]
974386d793 build verified: nseq_regex moved to smt/seq 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-14 16:49:28 +00:00
copilot-swe-agent[bot]
323d2f7fec Initial plan 2026-03-14 16:26:46 +00: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
copilot-swe-agent[bot]
d364604875 Initial plan 2026-03-11 16:35:24 +00:00
copilot-swe-agent[bot]
45a574d7fa Remove nseq_parith.h and nseq_parikh.cpp backwards-compat shims 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-11 15:48:05 +00:00
CEisenhofer
d23f376b39 Fixed a lot regarding powers, but there seems to be a model reconstruction bug left 2026-03-11 16:44:14 +01:00
CEisenhofer
6d0468861d Fixed git merge problems 2026-03-11 13:05:27 +01:00
CEisenhofer
2f46c8893e Another attempt to fix powers 2026-03-11 11:29:25 +01:00
copilot-swe-agent[bot]
213ddd36ba Rename nseq_parikh→seq_parikh; add m/seq/a member attributes to seq_parikh 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-11 05:41:16 +00:00
copilot-swe-agent[bot]
4ac5315846 Fix review: min>=max guard, ceiling-div overflow, SASSERT, accessor methods, comments 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-11 05:15:20 +00:00
copilot-swe-agent[bot]
eca5fcc7bb Integrate nseq_parith into nielsen_graph; add k upper bound and check_parikh_conflict 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-11 05:10:30 +00:00
copilot-swe-agent[bot]
35ee8f917d Remove redundant zero-guards before u_gcd calls in concat/intersection cases 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-11 04:26:26 +00:00
copilot-swe-agent[bot]
4cdfceabc5 Use u_gcd from util/mpz.h instead of local gcd definition 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-11 04:24:16 +00:00
copilot-swe-agent[bot]
d267e452a2 Add Clemens Eisenhofer as co-author to nseq_parith.h and nseq_parikh.cpp 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-11 04:21:30 +00:00
copilot-swe-agent[bot]
334df71b11 Add nseq_parith.h and nseq_parikh.cpp: Parikh filter for ZIPT string solver 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-11 00:05:26 +00:00
copilot-swe-agent[bot]
3054f0cb41 Initial plan 2026-03-10 23:43:18 +00:00
Nikolaj Bjorner
51e245a245
Merge pull request #8935 from Z3Prover/copilot/implement-int-bounds-var-bound-watcher 
Implement IntBounds/VarBoundWatcher + Constraint.Shared for Nielsen graph arithmetic pruning
 2026-03-10 16:36:52 -07:00