-
Notifications
You must be signed in to change notification settings - Fork 5
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
Support for sending custom expressions to the solver #30
Comments
This is definitely something we should support. Would you be open to whipping up a PR? |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Hi,
easy_smt
currently provides nice access to creating customatom
s and using them in custom expressions, but has no way to actually send these to the solver for the user (assolver.send
is private). This is useful for example with optimization in z3 which provides special(minimize expr)
and(maximize expr)
expressions that need to be sent to the solver.Such expressions can be made using the following
but they cannot yet be sent to the solver. This should be a relatively simple patch to include a wrapper for
solver.send
.The text was updated successfully, but these errors were encountered: