Improve string identifier generation for Z3 backend
Current state.
In order to interact with Z3, string identifiers have to be created such that objects can be passed to and received from Z3. Since some characters have a special meaning, they are forbidden by Z3 and converted to different characters, thus complicating the back translation into the AF3 representation of the calculated solutions.
Proposed change.
There are two possible approaches for the above mentioned problem:
- Translate the string descriptor before passing it to Z3 such that it contains only ASCII characters and forbidden characters are replaced. This could be encapsulated in a single translator class.
- Use only Class names and IDs to create the string descriptors. This approach avoids the above mentioned problems since we operate only on EMF classes (here: DSML expressions) that do not contain problematic characters. If more expressive descriptors are required for debugging, the names of elements passed to Z3 could be added depending on the presence of the DSE_DEBUG_VERBOSE env flag. However, this comes at the risk of introducing invalid characters when debugging.
Due to the reduced effort, change #2 is favored currently.
(from redmine: issue id 3364, created on 2018-04-03, closed on 2018-09-25)