mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-26 22:03:34 +00:00
Code Activity
22326 commits 72 branches 58 tags 227 MiB
Commit graph

22326 commits

This branch
This branch
All branches
Author SHA1 Message Date
CEisenhofer
149a087f65 Strengthened diseq axiom 2026-03-19 11:14:07 +01:00
Copilot
f837651434
seq_nielsen: replace mk_fresh_var() with mk_fresh_var(sort* s) (#9037) 
* replace mk_fresh_var() with mk_fresh_var(sort* s) in seq_nielsen; fix snode_label_html linkage

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

* remove mk_var(symbol const&) from sgraph; update all callers to pass sort explicitly

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-18 20:41:41 -07:00
Nikolaj Bjorner
4b40969da6 added diseq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-18 13:32:18 -07:00
Nikolaj Bjorner
a2352529f8 add diseq axiom 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-18 12:58:27 -07:00
CEisenhofer
777bda01a5 Subsolver was not reset properly 2026-03-18 20:22:08 +01:00
Nikolaj Bjorner
c43df60182 fix build of unit tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-18 10:29:41 -07:00
Nikolaj Bjorner
23b7e109bd partial updates to test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-18 10:04:07 -07:00
Nikolaj Bjorner
8ac8eb4ae7 create sub-class for tracked eq and mem relations to separate from seq_nielsen 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-18 10:04:01 -07:00
CEisenhofer
e7431400b4 Regex bug fixes (still not there) 2026-03-18 18:01:44 +01:00
CEisenhofer
983379f5e2 Missing semicolon 2026-03-18 16:16:59 +01:00
CEisenhofer
0a32337f0a Removed some brackets 2026-03-18 16:15:37 +01:00
CEisenhofer
d8a6ea1321 Fixed crasb if regex is reported SAT by pre-check 2026-03-18 16:08:02 +01:00
CEisenhofer
579ac6bfc4 Updated script 2026-03-18 15:45:56 +01:00
CEisenhofer
43950569eb More fixes 2026-03-18 15:41:27 +01:00
CEisenhofer
b288c2e7dc Some more bug fixes 2026-03-18 14:54:12 +01:00
CEisenhofer
ab53889c10 Fixed couple of regex problems [there are still others] 2026-03-18 14:29:18 +01:00
Lev Nachmanson
b5bf4be87e fix: move m_fixed insertion after check_long_strings guard 
m_fixed.insert(e) was placed before the check_long_strings guard,
causing check_fixed_length(false, false) to mark variables with
len > 20 as processed without actually decomposing them. The
subsequent check_fixed_length(false, true) then skipped them.

Move the insertion after the guard so variables are only marked
as fixed once they are actually decomposed.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
 2026-03-17 20:19:12 -10:00
copilot-swe-agent[bot]
960ab8e67a perf: move check_fixed_length(false,true) before check_contains in final_check_eh 
Co-authored-by: levnach <5377127+levnach@users.noreply.github.com>
 2026-03-17 20:19:12 -10:00
Lev Nachmanson
09c13a75e3 fix #8023: don't skip axiom clauses with non-base-level satisfying literals 
The add_axiom optimization that skips adding clauses when a literal is
already true was unsound: the satisfying literal could be retracted by
backtracking, leaving the axiom clause missing. This caused the solver
to miss propagations, e.g., not propagating indexof(a,s) = -1 when
contains(a,s) becomes false after backtracking.

Fix: only skip the clause if the satisfying literal is assigned at
base level (scope 0), where it can never be retracted.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
 2026-03-17 15:05:41 -10:00
Nikolaj Bjorner
b1bae695e6 comment 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-17 16:32:01 -07:00
Nikolaj Bjorner
2847dd8bb3 small simplification 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-17 16:30:53 -07:00
Nikolaj Bjorner
3719b449e8 re-organize dependencies 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-17 16:18:27 -07:00
copilot-swe-agent[bot]
3745bdd43b fix: reduce verbose lock contention in theory_diff_logic (issue #8019) 
In multi-threaded solving, IF_VERBOSE(0, ...) in found_non_diff_logic_expr
was always acquiring the global g_verbose_mux mutex (since verbosity >= 0 is
always true) while holding it for potentially expensive mk_pp() calls. This
caused catastrophic lock contention when multiple threads internalized atoms.

Change IF_VERBOSE(0, ...) to IF_VERBOSE(2, ...) in both theory_diff_logic_def.h
and theory_dense_diff_logic_def.h. The diagnostic message is still available at
verbosity level 2 (-v:2), but is no longer printed (or locked) at the default
verbosity level, eliminating the contention.

Co-authored-by: levnach <5377127+levnach@users.noreply.github.com>
 2026-03-17 13:07:20 -10:00
Lev Nachmanson
0461e010bb assign every new issue to copilot by default 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-03-17 12:09:01 -10:00
dependabot[bot]
a252121945
Bump actions/download-artifact from 8.0.0 to 8.0.1 (#9016) 
Bumps [actions/download-artifact](https://github.com/actions/download-artifact) from 8.0.0 to 8.0.1.
- [Release notes](https://github.com/actions/download-artifact/releases)
- [Commits](https://github.com/actions/download-artifact/compare/v8...v8.0.1)

---
updated-dependencies:
- dependency-name: actions/download-artifact
  dependency-version: 8.0.1
  dependency-type: direct:production
  update-type: version-update:semver-patch
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
 2026-03-16 16:11:55 -07:00
dependabot[bot]
103bf6dc35
Bump github/gh-aw from 0.53.4 to 0.59.0 (#9015) 
Bumps [github/gh-aw](https://github.com/github/gh-aw) from 0.53.4 to 0.59.0.
- [Release notes](https://github.com/github/gh-aw/releases)
- [Commits](https://github.com/github/gh-aw/compare/v0.53.4...v0.59.0)

---
updated-dependencies:
- dependency-name: github/gh-aw
  dependency-version: 0.59.0
  dependency-type: direct:production
  update-type: version-update:semver-minor
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
 2026-03-16 16:07:29 -07:00
dependabot[bot]
9d033f304a
Bump actions/setup-python from 5 to 6 (#9017) 
Bumps [actions/setup-python](https://github.com/actions/setup-python) from 5 to 6.
- [Release notes](https://github.com/actions/setup-python/releases)
- [Commits](https://github.com/actions/setup-python/compare/v5...v6)

---
updated-dependencies:
- dependency-name: actions/setup-python
  dependency-version: '6'
  dependency-type: direct:production
  update-type: version-update:semver-major
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
 2026-03-16 15:52:45 -07:00
dependabot[bot]
0564dfe32b
Bump actions/checkout from 5.0.1 to 6.0.2 (#9018) 
Bumps [actions/checkout](https://github.com/actions/checkout) from 5.0.1 to 6.0.2.
- [Release notes](https://github.com/actions/checkout/releases)
- [Commits](https://github.com/actions/checkout/compare/v5.0.1...v6.0.2)

---
updated-dependencies:
- dependency-name: actions/checkout
  dependency-version: 6.0.2
  dependency-type: direct:production
  update-type: version-update:semver-major
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
 2026-03-16 15:52:35 -07:00
Copilot
ef22ae8871
Replace dep_tracker uint_set with scoped_dependency_manager<dep_source> in seq_nielsen (#9014) 
* Initial plan

* replace dep_tracker uint_set with scoped_dependency_manager<dep_source>

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

* fix test build: update dep_tracker usages in test files and seq_state.h

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-16 15:52:18 -07:00
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
Lev Nachmanson
f4adcde585 add regression test for #9012: box mode mod optimization 
Test tst_box_mod_opt verifies that maximize (mod (- (* 232 a)) 256)
returns 248 when using box priority with multiple objectives.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
 2026-03-16 09:47:09 -10:00
CEisenhofer
84d371f2e9 Bugfix in regex overapproximation 2026-03-16 19:54:12 +01:00
Lev Nachmanson
f03cac6e51 fix #9012: incorrect optimization of mod in box mode 
Push/pop isolation in maximize_objectives1 (added for #7677) can corrupt
LP column values between objectives. For non-linear objectives like mod,
the LP maximize call may return stale values after a preceding
objective's push/pop cycle.

Fix: save the baseline model before the push/pop loop and use it as a
floor for each objective's value. Extract two helpers:
- maximize_objective_isolated: push/pop + save/restore per objective
- update_from_baseline_model: adopt baseline model value when it is better

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
 2026-03-16 07:28:34 -10: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
Copilot
fe6efef808
Add monthly Academic Citation & Research Trend Tracker workflow (#9007) 
* Initial plan

* Add academic-citation-tracker workflow and compiled lock file

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 15:39:37 -07:00
Lev Nachmanson
99099255b6 Fix inconsistent optimization with scaled objectives (#8998) 
When the LP optimizer returns the same blocker expression in successive
iterations of geometric_lex (e.g., due to nonlinear constraints like
mod/to_int preventing the LP from exploring the full feasible region),
the loop now falls back to using the model-based lower bound to push
harder instead of breaking immediately.

This fixes the case where minimize(3*a) incorrectly returned -162
while minimize(a) correctly returned -infinity with the same constraints.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
 2026-03-15 11:12:21 -10:00
Lev Nachmanson
5df80705aa Fix inconsistent optimization with scaled objectives (#8998) 
When the LP optimizer returns the same blocker expression in successive
iterations of geometric_lex (e.g., due to nonlinear constraints like
mod/to_int preventing the LP from exploring the full feasible region),
the loop now falls back to using the model-based lower bound to push
harder instead of breaking immediately.

This fixes the case where minimize(3*a) incorrectly returned -162
while minimize(a) correctly returned -infinity with the same constraints.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
 2026-03-15 11:12:21 -10:00
Copilot
fbeb4b22eb
Add missing Go Goal/FuncEntry/Model APIs and TypeScript Seq higher-order operations (#9006) 
* Initial plan

* fix: add missing API bindings from discussion #8992 for Go and TypeScript

- Go tactic.go: add Goal.Depth(), Goal.Precision(), Goal.Translate(), Goal.ConvertModel()
- Go solver.go: add FuncEntry struct, FuncInterp.GetEntry/SetElse/AddEntry, Model.HasInterp
- TypeScript types.ts + high-level.ts: add Seq.map/mapi/foldl/foldli

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 12:57:44 -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
6893674392
fix: correct misleading API comments in fp.go and JavaExample.java (#9003) 
* Initial plan

* fix: correct misleading API comments in fp.go and JavaExample.java

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 12:08:59 -07:00
Angelica Moreira
bebad7da50
Add numeral extraction helpers to Java API (#8978) 
New methods:
- Expr.getNumeralDouble(): retrieve any numeral as a double
- IntNum.getUint(): extract numeral as unsigned 32-bit value
- IntNum.getUint64(): extract numeral as unsigned 64-bit value
- RatNum.getSmall(): numerator/denominator as int64 pair
- RatNum.getRationalInt64(): numerator/denominator (returns null on overflow)

Each is a thin wrapper around the existing Native binding.
Added examples to JavaExample.java covering all new methods.
 2026-03-15 10:36: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
9256dd66e6
Switch memory-safety workflow from push to weekly Monday schedule (#9001) 
* Initial plan

* Replace push trigger with weekly Monday schedule in memory-safety.yml

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:26:10 -07:00