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

Conversion from Application to UF does not consider QualIdentifier::Sorted #12

Open
leonardoalt opened this issue Jan 24, 2022 · 1 comment

Comments

@leonardoalt
Copy link

Hi, I noticed that the conversion from smt2parser::concrete::Term::Application to IUF (https://github.com/awslabs/rust-smt-ir/blob/main/amzn-smt-ir/src/term/convert.rs#L185 and another instance of IUF::parse) only take the function's name, since UF takes an ISymbol and vector of Term arguments (https://github.com/awslabs/rust-smt-ir/blob/main/amzn-smt-ir/src/term/uf.rs#L19).

However, the original Application uses a QualIdentifier for the function's term, which has the Sorted variant. This variant is useful for things like ((as const (Array Int Int)) 0), where the Sorted variant keeps the sort of the const application. Currently this term gets converted into an UF { func: Symbol("const"), args: [0] } where the sort is lost.

Is this intentional, or should the sort be kept?

@BrunoDutertre
Copy link
Collaborator

This looks like a bug. Thanks for reporting this. We'll look into this.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants