Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

High-level bindings to create quantifiers with additional attributes #325

Open
ole-thoeb opened this issue Nov 28, 2024 · 0 comments
Open

Comments

@ole-thoeb
Copy link
Contributor

ole-thoeb commented Nov 28, 2024

As far as I know, there are currently no high-level bindings for creating quantifiers with additional attributes other than patterns.
For me, quantifier id and weight are of particular interest. The relevant function in the z3 API seems to be Z3_mk_quantifier_const_ex.

I created a PR (#326) that provides a function that wraps Z3_mk_quantifier_const_ex directly. Similar to what the z3 Java API does.
This approach results in a function with many arguments (even clippy complaints), not all of which are always of interest. Perhaps a builder would be more appropriate here. It also allows us to provide defaults and potentially add additional attributes in the future.

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

No branches or pull requests

1 participant