Skip to content

Add concretize() fallback for ReduceSymbolicExpr#317

Merged
mark14wu merged 3 commits intosupport-tl-max-1-argmax-argmin-z3from
support-tl-max-2-concretize
Mar 13, 2026
Merged

Add concretize() fallback for ReduceSymbolicExpr#317
mark14wu merged 3 commits intosupport-tl-max-1-argmax-argmin-z3from
support-tl-max-2-concretize

Conversation

@mark14wu
Copy link
Copy Markdown
Collaborator

@mark14wu mark14wu commented Mar 6, 2026

Summary

  • Add _NUMPY_REDUCE_OPS mapping for concrete NumPy evaluation
  • Add ReduceSymbolicExpr.concretize() method as fallback when Z3 path is not needed
  • argmax/argmin results are cast to int32 to match the declared dtype

Test plan

  • pytest tests/unit/test_sanitizer.py::test_reduce_argmax_argmin_concretize_dtype -xvs

[FEAT] Add concretize() fallback for ReduceSymbolicExpr

Add _NUMPY_REDUCE_OPS mapping and concretize() method so that reduce
expressions can fall back to concrete NumPy evaluation when the Z3
path is not needed (e.g. for simple constant inputs). argmax/argmin
results are cast to int32 to match the declared dtype.

PR chain

  1. Add argmax/argmin as symbolic reduce ops with Z3 reasoning #316
  2. 👉 Add concretize() fallback for ReduceSymbolicExpr #317 👈 YOU ARE HERE
  3. Support tl.max/tl.min with return_indices=True #318

⚠️⚠️ Please do not click the green "merge" button unless you know what
you're doing. This PR is part of a chain of PRs, and clicking the merge
button will not merge it into master. ⚠️⚠️

Add _NUMPY_REDUCE_OPS mapping and concretize() method so that reduce
expressions can fall back to concrete NumPy evaluation when the Z3
path is not needed (e.g. for simple constant inputs). argmax/argmin
results are cast to int32 to match the declared dtype.

GPC: support-tl-max-2-concretize
@mark14wu mark14wu merged commit 5b1341e into support-tl-max-1-argmax-argmin-z3 Mar 13, 2026
@mark14wu mark14wu deleted the support-tl-max-2-concretize branch March 13, 2026 16:06
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants