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

Handling of named terms #187

Closed
Stevendeo opened this issue Sep 29, 2023 · 2 comments
Closed

Handling of named terms #187

Stevendeo opened this issue Sep 29, 2023 · 2 comments
Assignees
Labels

Comments

@Stevendeo
Copy link

I am searching how to access the custom names of assertions (and sub expressions). For example, on the following file:

(set-logic ALL)
(declare-const x Int)
(assert (! (= x (! (+ x x) :named foo)) :named bar))

I would like to have the term + x x associated to the identifier foo and the whole assertion associated to the identifier bar.

@Stevendeo Stevendeo changed the title Handling of named formula Handling of named terms Sep 29, 2023
@Gbury Gbury self-assigned this Sep 29, 2023
@Gbury Gbury added the bug label Sep 29, 2023
@Stevendeo
Copy link
Author

After navigating through the code, I found a way to get them:
Expr.Term.get_tag term Expr.Tags.named

It still is cumbersome to visit the terms, would it be interesting to add a term visitor/iterator in Dolmen unfolding the different subterms of a given term?

@Gbury
Copy link
Owner

Gbury commented Nov 20, 2023

Closing since #199 has been merged.

@Gbury Gbury closed this as completed Nov 20, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

2 participants