Skip to content

Conversation

@aquacash5
Copy link
Contributor

Allow users to use generator expressions as arguments to z3 objects.

I think it makes the syntax a little cleaner. Removes a lot of those square brackets.

Examples:

s = Solver()

X = [[Int(f"{row} {col}") for col in range(9)] for row in range(9)]

s.add(Distinct(row) for row in X)
# vs
s.add([Distinct(row) for row in X])

@NikolajBjorner NikolajBjorner merged commit 5ad79f2 into Z3Prover:master Apr 12, 2025
1 check passed
@aquacash5 aquacash5 deleted the generator-args branch April 12, 2025 19:11
arbipher pushed a commit to arbipher/z3 that referenced this pull request Apr 17, 2025
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