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.
- Priority changed from Low to Normal
As a consequence, it will be possible to remove the deprecated function maxTime from the dsl_v2.ecore metamodel.
- Target version changed from AF3 2.15 RC1 (Feature Freeze) to AF3 2.16 RC1 (Feature Freeze)
- Target version changed from AF3 2.16 RC1 (Feature Freeze) to AF3 2.17 (Feature Freeze)
- Target version changed from AF3 2.17 (Feature Freeze) to Backlog
- Assignee changed from Marco Volpe to Johannes Eder
- Priority changed from Normal to Low
- Status changed from New to Rejected
- Assignee deleted (
Rejected. Over 2 years old.
Also available in: Atom