Project

General

Profile

Feature #3546

Implementation of the translation into SMT of a Maximum function in DSML

Added by Marco Volpe almost 2 years ago. Updated about 2 months ago.

Status:
Rejected
Priority:
Low
Assignee:
-
Category:
-
Target version:
Start date:
10/05/2018
Due date:
% Done:

0%

Estimated time:

Description

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.

History

#1 Updated by Marco Volpe almost 2 years ago

  • 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.

#2 Updated by Marco Volpe almost 2 years ago

Related to DSE #3554.

#3 Updated by Johannes Eder over 1 year ago

  • Target version changed from AF3 2.15 RC1 (Feature Freeze) to AF3 2.16 RC1 (Feature Freeze)

#4 Updated by Marco Volpe about 1 year ago

  • Target version changed from AF3 2.16 RC1 (Feature Freeze) to AF3 2.17 (Feature Freeze)

#5 Updated by Marco Volpe 7 months ago

  • Target version changed from AF3 2.17 (Feature Freeze) to Backlog

#6 Updated by Marco Volpe about 2 months ago

  • Assignee changed from Marco Volpe to Johannes Eder
  • Priority changed from Normal to Low

#7 Updated by Johannes Eder about 2 months ago

  • Status changed from New to Rejected
  • Assignee deleted (Johannes Eder)

Rejected. Over 2 years old.

Also available in: Atom PDF