Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Proper support for quoted identifiers in models #806

Closed
bclement-ocp opened this issue Sep 11, 2023 · 2 comments
Closed

Proper support for quoted identifiers in models #806

bclement-ocp opened this issue Sep 11, 2023 · 2 comments
Assignees
Labels
bug frontend models This issue is related to model generation.

Comments

@bclement-ocp
Copy link
Collaborator

          By the way we probably have a problem with quoted identifiers as well… This is unrelated to this PR however.

Originally posted by @bclement-ocp in #804 (comment)

We do.

$ cat quoted.smt2
(set-logic ALL)
(declare-const |fail))| Int)
(assert (= |fail))| 0))
(check-sat)
(get-model)
$ alt-ergo --frontend dolmen --produce-models quoted.smt2
                                       
; File "quoted.smt2", line 4, characters 1-12: I don't know (0.4269) (1 steps) (goal g_1)

unknown
(
  (define-fun fail)) () Int 0)
)
@bclement-ocp bclement-ocp changed the title By the way we probably have a problem with quoted identifiers as well… This is unrelated to this PR however. Proper support for quoted identifiers in models Sep 11, 2023
@bclement-ocp bclement-ocp added bug frontend models This issue is related to model generation. labels Sep 11, 2023
@bclement-ocp
Copy link
Collaborator Author

Assigning @Halbaroth who said he was interested in tackling this

@Stevendeo
Copy link
Collaborator

There are few ways to tackle this issue. If Dolmen does not provide the information that the identifier was defined quoted (which would be IMO the best way to do to precisely match the user input), we can :

  • quote all the names in the output (easy, no cost, 100% sound)
  • check all names when they are built or printed that they do not contain special characters (not as easy, negligible-but-existent cost, error prone)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug frontend models This issue is related to model generation.
Projects
None yet
Development

No branches or pull requests

3 participants