mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-11 07:40:31 +00:00
Code Activity
21983 commits 56 branches 58 tags 224 MiB
Commit graph

21983 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
c3eb0056db
Merge pull request #8933 from Z3Prover/copilot/fix-build-error-nseq-zipt 
Fix build: nseq_zipt fixture missing simple_solver arg to nielsen_graph
 2026-03-10 15:49:46 -07:00
Nikolaj Bjorner
3a71f28c6c
Rename dummy_simple_solver to zipt_dummy_simple_solver 2026-03-10 15:49:24 -07:00
copilot-swe-agent[bot]
0efb7402e8 Fix build: add dummy_simple_solver to nseq_zipt.cpp fixture, fix assert_expr in seq_nielsen.cpp 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-10 22:47:49 +00:00
copilot-swe-agent[bot]
09f5d637b0 Initial plan 2026-03-10 22:44:11 +00:00
Nikolaj Bjorner
d2739d9816 use reference to solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-10 15:22:50 -07:00
Nikolaj Bjorner
c98ea6dc21 make simple solver a reference 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-10 15:10:51 -07:00
Nikolaj Bjorner
3e3c3f106d
Merge pull request #8931 from Z3Prover/copilot/replace-lp-simple-solver 
Replace lp_simple_solver in Nielsen graph with smt::kernel-based context_solver
 2026-03-10 15:04:40 -07:00
copilot-swe-agent[bot]
5744958e46 Replace lp_simple_solver in nielsen with context_solver using smt::kernel (seq_len) 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-10 21:39:29 +00:00
copilot-swe-agent[bot]
a4f2c4a217 Initial plan 2026-03-10 21:09:43 +00:00
Nikolaj Bjorner
a8269c7d98
Merge pull request #8930 from Z3Prover/copilot/introduce-constraints-on-s 
Use mod-based constraints for semi-linear regex length sets
 2026-03-10 13:33:43 -07:00
copilot-swe-agent[bot]
334e6da60d Guard mod constraint: skip for period <= 1 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-10 20:14:53 +00:00
Nikolaj Bjorner
2ec8a1231c
Merge pull request #8929 from Z3Prover/copilot/fix-build-warnings 
Fix -Wunused-variable warnings in theory_finite_set, theory_finite_set_size, theory_nseq
 2026-03-10 12:53:53 -07:00
copilot-swe-agent[bot]
2bae0f02c4 Replace fresh-variable semi-linear constraint with mod-based approach 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-10 19:48:18 +00:00
copilot-swe-agent[bot]
3a34517162 Initial plan 2026-03-10 19:29:33 +00:00
copilot-swe-agent[bot]
472d9bde6c Fix unused variable build warnings in theory_finite_set, theory_finite_set_size, theory_nseq 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-10 18:52:40 +00:00
copilot-swe-agent[bot]
9c1d9af6d7 Initial plan 2026-03-10 18:49:44 +00:00
Nikolaj Bjorner
83c8743ea7
Merge pull request #8925 from Z3Prover/copilot/add-theory-seq-len-solver 
Add theory_seq_len: partial sequence length axiomatization via semi-linear constraints
 2026-03-10 11:36:33 -07:00
Nikolaj Bjorner
46e796114b
Merge pull request #8927 from Z3Prover/copilot/fix-build-error 
Fix build error: remove stale dep_tracker method definitions
 2026-03-10 11:34:58 -07:00
copilot-swe-agent[bot]
d4b99730b9 Fix build error: remove stale dep_tracker method definitions from seq_nielsen.cpp 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-10 18:30:33 +00:00
copilot-swe-agent[bot]
2e784a6ba3 Initial plan 2026-03-10 18:10:16 +00:00
copilot-swe-agent[bot]
56e9e9df57 Add theory_seq_len: partial axiom instantiation for sequence length constraints 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-10 18:02:04 +00:00
copilot-swe-agent[bot]
3ee78e242b Initial plan 2026-03-10 17:39:57 +00:00
Nikolaj Bjorner
4ea4533f3b
Merge pull request #8924 from Z3Prover/copilot/replace-lp-solver-with-abstract-solver 
Replace hardcoded lp_solver in seq_nielsen with abstract simple_solver interface
 2026-03-10 10:35:57 -07:00
Nikolaj Bjorner
2e636ec25d
Merge branch 'c3' into copilot/replace-lp-solver-with-abstract-solver 2026-03-10 10:35:44 -07:00
Nikolaj Bjorner
3f0e821207
Merge pull request #8923 from Z3Prover/copilot/host-char-range-and-set 
Move char_range and char_set from seq_nielsen to zstring
 2026-03-10 10:18:58 -07:00
Nikolaj Bjorner
c710e1fa14
Merge pull request #8922 from Z3Prover/copilot/replace-dep-tracker-with-uint-set 
Replace dep_tracker with uint_set in seq_nielsen
 2026-03-10 10:18:37 -07:00
copilot-swe-agent[bot]
40b33ab353 Address code review: simplify constructor, add UNREACHABLE() 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-10 17:10:36 +00:00
copilot-swe-agent[bot]
35addda546 Replace lp_solver in seq_nielsen with abstract simple_solver class 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-10 17:08:57 +00:00
copilot-swe-agent[bot]
5330bd20bc Replace dep_tracker class in seq_nielsen with uint_set 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-10 16:58:50 +00:00
copilot-swe-agent[bot]
430a43045a Move char_range and char_set from seq_nielsen to zstring 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-10 16:57:43 +00:00
Nikolaj Bjorner
08f4596cb7
Merge pull request #8921 from Z3Prover/copilot/update-file-headers-order 
Swap author order in file headers: Clemens Eisenhofer before Nikolaj Bjorner
 2026-03-10 09:50:07 -07:00
copilot-swe-agent[bot]
bf82bb0899 Initial plan 2026-03-10 16:46:03 +00:00
copilot-swe-agent[bot]
e3922f9f2b Initial plan 2026-03-10 16:33:45 +00:00
copilot-swe-agent[bot]
f3018a563e Initial plan 2026-03-10 16:32:10 +00:00
copilot-swe-agent[bot]
2f8cc1536c Swap author order: Clemens Eisenhofer before Nikolaj Bjorner in file headers 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-10 16:27:26 +00:00
Nikolaj Bjorner
4208d5d98e
Merge pull request #8919 from Z3Prover/copilot/fix-build-error-python 
fix: add `lp` dependency to `smt_seq` component in Python build
 2026-03-10 09:24:52 -07:00
copilot-swe-agent[bot]
dfebdb5f72 Initial plan 2026-03-10 16:24:16 +00:00
copilot-swe-agent[bot]
860cc023d6 fix: add lp dependency for smt_seq in mk_project.py 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-10 16:19:10 +00:00
copilot-swe-agent[bot]
b0414ec07b Initial plan 2026-03-10 16:17:59 +00:00
CEisenhofer
587eec4226 More bug fixing in the gpower introduction 2026-03-09 15:20:58 +01:00
CEisenhofer
32a09859e3 Fixing power introduction 2026-03-09 15:03:26 +01:00
CEisenhofer
e1cf20f9bd Added timeout 
Some bugfixes
 2026-03-09 14:21:06 +01:00
CEisenhofer
756673f104 Trying to port integer constraints 2026-03-06 14:01:21 +01:00
CEisenhofer
009c6de235 Ported symbolic characters 2026-03-06 11:28:06 +01:00
Nikolaj Bjorner
474cec8ccc
Merge pull request #8875 from Z3Prover/copilot/create-agentic-workflow 
[WIP] Create agentic workflow for z3 benchmarks
 2026-03-05 15:57:28 -08:00
copilot-swe-agent[bot]
a1320d031e Add QF_S string solver benchmark agentic workflow 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-05 23:13:32 +00:00
copilot-swe-agent[bot]
282485814f Initial plan 2026-03-05 22:42:13 +00:00
Nikolaj Bjorner
520ee1debc adding files to test 2026-03-05 13:38:06 -08:00
CEisenhofer
f404bef4ba Fixed CoPilot comment 2026-03-05 19:08:31 +01:00
Nikolaj Bjorner
7db00dad9d
Merge pull request #8872 from Z3Prover/copilot/simplify-dep-tracker-constructors 
refactor(seq_nielsen): eliminate duplicate dep_tracker initialization via constructor delegation
 2026-03-05 10:00:09 -08:00