mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-07 05:44:51 +00:00
Code Activity
21872 commits 48 branches 58 tags 222 MiB
Commit graph

21872 commits

This branch
This branch
All branches
Author SHA1 Message Date
copilot-swe-agent[bot]
28d1c4a27f Add ZIPT code reviewer agentic workflow (runs 4x daily) 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-03 00:00:36 +00:00
copilot-swe-agent[bot]
67f4d30577 Initial plan 2026-03-02 23:55:15 +00:00
Nikolaj Bjorner
5ca200ba2c
Update ZIPT link in euf_sgraph.h documentation 2026-03-02 12:32:32 -08:00
Nikolaj Bjorner
8d05ab56a1
Merge pull request #8827 from Z3Prover/copilot/finish-pending-tasks-8820 
Address review feedback from PR #8820 and implement snode/sgraph operations
 2026-03-02 12:27:19 -08:00
copilot-swe-agent[bot]
1274a1e3c0 Add safety cap on minterm computation and assertion for invariant 
Co-authored-by: NikolajBjorner <56730610+NikolajBjorner@users.noreply.github.com>
 2026-03-02 19:29:41 +00:00
copilot-swe-agent[bot]
150f1fe2ea Revert is_concat changes, add ZIPT URL, implement snode/sgraph operations and tests 
- Revert is_str_concat/is_re_concat to original form (PR #8820 review)
- Add ZIPT URL (https://github.com/CEisenhofer/ZIPT) to euf_sgraph.h
- Add snode::at() for token indexing and collect_tokens() for enumeration
- Add sgraph factory methods: mk_var, mk_char, mk_empty, mk_concat
- Add sgraph drop operations: drop_first, drop_last, drop_left, drop_right
- Add sgraph substitution: subst(snode*, snode*, snode*)
- Add Brzozowski derivative via seq_rewriter::mk_derivative
- Add minterm computation from regex predicates
- Add 7 new unit tests covering all new operations with complex concats

Co-authored-by: NikolajBjorner <56730610+NikolajBjorner@users.noreply.github.com>
 2026-03-02 19:28:32 +00:00
copilot-swe-agent[bot]
40b99311e3 Fix enode_concat_eq leaf comparison, simplify is_str/re_concat, update sgraph summary 
Address remaining review feedback from PR #8820:
- Use pointer comparison instead of ID comparison in enode_concat_eq
- Remove redundant num_args() == 2 check from is_str_concat/is_re_concat
- Update euf_sgraph.h abstract to detail seq_plugin features

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-02 18:58:21 +00:00
copilot-swe-agent[bot]
5bbeedaff0 Initial plan 2026-03-02 18:32:56 +00:00
Nikolaj Bjorner
5e39ee8911
Merge pull request #8820 from Z3Prover/copilot/encapsulate-strings-in-euf-sgraph 
Add string graph encapsulation (euf_sgraph/snode), OP_SEQ_POWER, and euf_seq_plugin
 2026-03-02 10:32:26 -08:00
copilot-swe-agent[bot]
8c0be6e614 Changes before error encountered 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-02 17:50:49 +00:00
copilot-swe-agent[bot]
a3baae5942 Changes before error encountered 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-02 17:01:49 +00:00
copilot-swe-agent[bot]
037d2da801 Distinguish is_re_concat/is_str_concat and mk_re_concat/mk_str_concat in euf_seq_plugin 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-02 16:34:29 +00:00
copilot-swe-agent[bot]
921260ae82 Fix propagate_assoc find/else logic for hash table 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-02 00:38:04 +00:00
copilot-swe-agent[bot]
82051ac4d8 Reuse seq_rewriter::is_nullable, add assoc hash table to seq_plugin propagate_assoc 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-02 00:36:52 +00:00
copilot-swe-agent[bot]
3150b41724 Add self-contained unit tests for sgraph (13 tests covering classification, metadata, push/pop, assoc hash, navigation) 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-02 00:12:43 +00:00
copilot-swe-agent[bot]
6ef3be4e5e Remove sgraph dependency from seq_plugin, let sgraph register nodes via on_make callback 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-01 23:50:48 +00:00
copilot-swe-agent[bot]
b8656d4fbe Address code review: add comments for collect_leaves, find_assoc_equal, and display 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-01 23:24:59 +00:00
copilot-swe-agent[bot]
5c14edf030 Change ownership: sgraph owns egraph with seq_plugin, add assoc hash table, add unit tests 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-01 23:23:12 +00:00
copilot-swe-agent[bot]
12b7a4dae3 Remove unused old_qhead variable in seq_plugin::propagate 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-01 21:51:00 +00:00
copilot-swe-agent[bot]
78a4e3001b Add euf_seq_plugin: string plugin for egraph with concat associativity and ZIPT simplifications 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-01 21:50:06 +00:00
copilot-swe-agent[bot]
51f4f918ea Update file header years from 2025 to 2026 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-01 21:17:08 +00:00
copilot-swe-agent[bot]
17099300f2 Add co-author Clemens Eisenhofer to headers, document ZIPT features not yet ported 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-01 21:14:52 +00:00
copilot-swe-agent[bot]
e4f9a517e4 Address code review: fix const-correctness, improve child registration, add comments 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-01 20:25:18 +00:00
copilot-swe-agent[bot]
2e17bb8767 Add OP_SEQ_POWER to seq_decl_plugin and create euf_snode/euf_sgraph for string graph encapsulation 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-01 20:19:37 +00:00
copilot-swe-agent[bot]
debe81ee74 Initial plan 2026-03-01 19:51:18 +00:00
Nikolaj Bjorner
844731d99a
Merge pull request #8814 from Z3Prover/copilot/simplify-def-ref-smart-pointer 
Simplify def_ref smart pointer in model_based_opt.h
 2026-03-01 04:47:37 -08:00
copilot-swe-agent[bot]
23d194502a Simplify def_ref smart pointer: default ctor, init list, clearer bool, remove extra semicolon 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-01 02:10:19 +00:00
copilot-swe-agent[bot]
137fd735f5 Initial plan 2026-03-01 01:49:00 +00:00
Lev Nachmanson
38ab05e50a
Merge pull request #8805 from Z3Prover/qmbi_crash 
Fix assertion violation in q_mbi diagnostic output
 2026-02-28 11:28:51 -10:00
Lev Nachmanson
93ac330864 Fix assertion violation in q_mbi diagnostic output 
The IF_VERBOSE(0,...) block at line 498 in q_mbi.cpp used operator[]
on values2root map which asserts the key exists. When the model
evaluation of the inverted term produces a value not present in the
EUF values2root map, this crashes.

Use find() instead to handle the missing key gracefully, since this
is diagnostic output and the missing key is expected when the model
inversion produces inconsistent results.

Fixes assertion violation from #7027 (obj_hashtable.h line 168/174)
with forall/array/eq2ineq combination.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
 2026-02-28 11:15:28 -10:00
Lev Nachmanson
7968669cf2
Merge pull request #8803 from Z3Prover/mbo_leak 2026-02-27 19:02:56 -10:00
Lev Nachmanson
835da14afa
Update src/math/simplex/model_based_opt.h 
Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>
 2026-02-27 17:29:37 -10:00
Lev Nachmanson
9a1a407298
Merge pull request #8801 from Z3Prover/bvo 
Handle overflow predicates in new core bit-vector internalization
 2026-02-27 17:21:24 -10:00
Lev Nachmanson
fc6696c5e4 Fix memory leaks in model_based_opt def ref-counting 
Three bugs in the def ref-counting infrastructure:

1. dec_ref() incremented (++) instead of decrementing (--) the ref count,
   so objects were never freed.

2. def_ref lacked copy and move constructors, so the compiler-generated
   default copy just copied the raw pointer without inc_ref. This caused
   use-after-free when def_ref values were copied into vectors.

3. Compound def types (add_def, mul_def, div_def) lacked destructors to
   dec_ref their children. Added virtual destructor to base def class
   and child-releasing destructors to compound types.

Fixes the memory leak from #7027 (model_based_opt.cpp:81).

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
 2026-02-27 17:15:20 -10:00
Copilot
f4abd88ff5
Add arity and bit-width SASSERTs to internalize_overflow (#8802) 
* Initial plan

* Add SASSERTs for arity and bit-width in internalize_overflow

Co-authored-by: levnach <5377127+levnach@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: levnach <5377127+levnach@users.noreply.github.com>
 2026-02-27 14:30:50 -10:00
Lev Nachmanson
2dac76d19a Handle overflow predicates in new core bit-vector internalization 
Add internalize_overflow() to handle OP_BUMUL_OVFL, OP_BSMUL_OVFL,
OP_BUADD_OVFL, OP_BSADD_OVFL, OP_BUSUB_OVFL, OP_BSSUB_OVFL,
OP_BSDIV_OVFL, and OP_BNEG_OVFL in the sat.euf=true solver path.

Previously these overflow predicates hit UNREACHABLE() in
internalize_circuit(). Now they are reduced to equivalent expressions
using existing BV operations and internalized via add_def().

Fixes the assertion violation from #7027 for bvuaddo and related
overflow predicates with tactic.default_tactic=smt sat.euf=true.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
 2026-02-27 13:07:39 -10:00
Lev Nachmanson
6ec40153cc fix #7677: treat FC_CONTINUE from check_nla as FEASIBLE in maximize 
When check_nla returns FC_CONTINUE it means NLA found constraint
violations and added lemmas. The current LP value is a valid lower
bound, so the status should be FEASIBLE, not UNBOUNDED.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
 2026-02-27 12:29:14 -10:00
Lev Nachmanson
ffe29b1433 Fix #7951: add cancellation checks to polynomial gcd_prs and HNF computation 
Add checkpoint() call in gcd_prs() main loop so polynomial GCD
computation respects rlimit/timeout. Add cancellation callback to
HNF calculation so it can be interrupted when the solver is cancelled.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
 2026-02-27 10:26:28 -10:00
Nikolaj Bjorner
d906a0cc2d fix bug reported by Maria Novoszel 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-27 12:02:55 -08:00
Lev Nachmanson
5ff5b075b2
Merge pull request #8789 from Z3Prover/succ_int_mult 
Fix #7507: simplify (>= product_of_consecutive_ints 0) to true
 2026-02-27 09:45:26 -10:00
Lev Nachmanson
21c23e78db Fix #7507: simplify (>= product_of_consecutive_ints 0) to true 
The arith rewriter now recognizes that x * (x + 1) >= 0 for all
integers, since no integer lies strictly between -1 and 0.

Two changes:
1. is_non_negative: detect products where unpaired factors are
   consecutive integer expressions (differ by exactly 1), handling
   both +1 and -1 offsets and n-ary additions
2. is_separated: return true for (>= non_negative_mul 0), restricted
   to multiplication expressions to avoid disrupting other theories

Also adds regression tests for the new simplification.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
 2026-02-27 06:37:07 -10:00
Nikolaj Bjorner
fda8b4175f
Merge pull request #8793 from Z3Prover/copilot/fix-missing-api-functions 
Add missing array and FP API functions to Go, OCaml, and TypeScript bindings
 2026-02-27 03:14:18 -08:00
copilot-swe-agent[bot]
282db840de Add missing API functions to Go, OCaml, and TypeScript bindings 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-27 02:55:37 +00:00
copilot-swe-agent[bot]
3f6acc45ed Initial plan 2026-02-27 02:48:36 +00:00
Nikolaj Bjorner
ea873672c3
Merge pull request #8788 from Z3Prover/copilot/simplify-fpa-test-code 
refactor(test): extract run_fp_test helper in fpa.cpp
 2026-02-26 16:29:42 -08:00
copilot-swe-agent[bot]
cf0ffa2673 refactor: extract run_fp_test helper in fpa.cpp 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-26 23:54:17 +00:00
copilot-swe-agent[bot]
f2e00b3589 Initial plan 2026-02-26 23:52:54 +00:00
Nikolaj Bjorner
aeded4d721
Merge pull request #8787 from Z3Prover/dependabot/npm_and_yarn/src/api/js/multi-770cfcd984 
Bump minimatch in /src/api/js
 2026-02-26 15:52:39 -08:00
Nikolaj Bjorner
828e4a7ef7
Merge pull request #8779 from Z3Prover/copilot/convert-bv1-blast-to-simplifier 
Convert bv1-blast tactic to a dependent_expr_simplifier
 2026-02-26 15:52:18 -08:00
dependabot[bot]
e097a98019
Bump minimatch in /src/api/js 
Bumps  and [minimatch](https://github.com/isaacs/minimatch). These dependencies needed to be updated together.

Updates `minimatch` from 3.1.2 to 3.1.5
- [Changelog](https://github.com/isaacs/minimatch/blob/main/changelog.md)
- [Commits](https://github.com/isaacs/minimatch/compare/v3.1.2...v3.1.5)

Updates `minimatch` from 9.0.5 to 9.0.9
- [Changelog](https://github.com/isaacs/minimatch/blob/main/changelog.md)
- [Commits](https://github.com/isaacs/minimatch/compare/v3.1.2...v3.1.5)

---
updated-dependencies:
- dependency-name: minimatch
  dependency-version: 3.1.5
  dependency-type: indirect
- dependency-name: minimatch
  dependency-version: 9.0.9
  dependency-type: indirect
...

Signed-off-by: dependabot[bot] <support@github.com>
 2026-02-26 23:51:30 +00:00