Skip to content
GitLab
Projects Groups Topics Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • A AF3
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributor statistics
    • Graph
    • Compare revisions
  • Issues 170
    • Issues 170
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 15
    • Merge requests 15
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Environments
    • Releases
  • Packages and registries
    • Packages and registries
    • Package Registry
    • Container Registry
    • Infrastructure Registry
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • af3af3
  • AF3
  • Issues
  • #3364
Closed
Open
Issue created Apr 03, 2018 by Alexander Diewald@diewaldGuest

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:

  1. 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.
  2. 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)

Assignee
Assign to
Time tracking