Implementation of the translation into SMT of a Maximum function in DSML
DSML provides the function Maximum as a binder, but its translation into
SMT is currently not supported.
This is apparently not directly available in Z3, so it is necessary to
manually define it, in particular as a further case in the class
ConstraintToNonQuantifiedSMT.
Such a translation can be useful, e.g., for a more direct definition of the minimization of latency constraint in scheduling synthesis.
(from redmine: issue id 3546, created on 2018-10-05, closed on 2020-08-10)