Implement functions (e.g. `abs()`)
Opened this issue · 1 comments
hauff commented
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 commented
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