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

22025 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
9b0a7c17a5
Merge branch 'c3' into copilot/design-linear-constraints-regex 2026-03-12 10:43:55 -07: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
copilot-swe-agent[bot]
2ec09f88c4 Make sort required in sgraph::mk_var and nielsen_graph::mk_fresh_var 
sgraph::mk_var(symbol const& name) silently hardcoded m_str_sort (always
String), which is wrong when sequences of other element sorts are in play.

Changes:
- euf_snode.h: add get_sort() convenience accessor (SASSERT that expr is
  non-null, then return expr->get_sort()) so call sites are readable and the
  precondition is checked in one place.
- euf_sgraph.h / euf_sgraph.cpp: make sort a required parameter of mk_var;
  remove the implicit use of m_str_sort.
- seq_nielsen.h / seq_nielsen.cpp: make sort a required parameter of
  mk_fresh_var; forward it to mk_var.
- All mk_fresh_var() call sites in seq_nielsen.cpp updated to derive the sort
  from the adjacent contextual snode via ->get_sort():
    lhead/rhead: sort of the variable being substituted
    lhs_toks[0]: sort of the equation's leading token (padding case)
    first: sort of the string membership variable
    base: sort of the power's base sequence

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-12 02:45:37 +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
Nikolaj Bjorner
53d5d98341
Merge branch 'c3' into copilot/implement-int-bounds-var-bound-watcher 2026-03-10 16:33:25 -07:00
copilot-swe-agent[bot]
57ede4cdcd Address code review: clarify add_lower/upper_int_bound return semantics; fix test assertion 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-10 23:29:15 +00:00
copilot-swe-agent[bot]
47f9be0270 Implement IntBounds/VarBoundWatcher + Constraint.Shared; fix pre-existing build errors 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-10 23:26:55 +00:00
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
copilot-swe-agent[bot]
07ee2f31ef Initial plan 2026-03-10 22:41:43 +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
copilot-swe-agent[bot]
918418fdb8 Generalize semi-linear length constraints for regex union and concatenation 
Replace the old single-period (base, period) schema in theory_seq_len with a
richer svector<len_arm> representation where each arm captures one arithmetic
progression via an existential linear constraint:
  ∃ k_0,...,k_{n-1} ≥ 0 :  |s| = base + ∑ periods[i] * k_i

Key improvements:
- Union R1|R2: recurse on both sides, return the concatenated arm sets.
  When asserting, fresh guard Booleans are introduced so the SAT solver
  case-splits between the two sets of length constraints.
- General concatenation R1++R2: compute the Minkowski product of arm sets.
  Combined arms carry the merged period lists so, e.g., (aa)*++(bbb)* yields
  |s| = 2*k1 + 3*k2 with k1,k2 ≥ 0, immediately ruling out length 1.
  A MAX_LEN_ARMS=16 cap prevents combinatorial explosion.
- Option (R)?: now produces two precise fixed arms {0} and {n} instead of
  the over-approximate single progression {0, n, 2n, …}.
- Each arm is encoded via fresh non-negative Int Skolem constants, letting
  the linear arithmetic solver find counting witnesses directly.

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-10 21:07:45 +00:00