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.

Sign up for GitHub

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

Jump to bottom

Implement functions (e.g. `abs()`) #230

Open

4 of 6 tasks

hauff opened this issue Oct 6, 2022 · 1 comment

Assignees

Labels

enhancement help wanted

Contributor

hauff commented Oct 6, 2022 •

edited

Loading

We want to support the following functions:

abs (PySMT: not implemented)
mod (PySMT: not implemented, use The Euclidean definition of the functions div and mod)
min (PySMT: https://pysmt.readthedocs.io/en/latest/api_ref.html#pysmt.shortcuts.Min)
max (PySMT: https://pysmt.readthedocs.io/en/latest/api_ref.html#pysmt.shortcuts.Max)
implement abs() for reals in Ultimate
implement min(), max() in Ultimate

hauff added enhancement help wanted labels

hauff self-assigned this

Contributor Author

hauff commented Dec 6, 2022

Maybe here is a good place to implement it.
https://github.com/ultimate-pa/ultimate/blob/dev/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/translator/Req2BoogieTranslator.java#L170

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment