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

[A*] Improve Array type support by moving sort parsing logic from sort2type into AstVisitor #46

Merged
merged 13 commits into from
Sep 20, 2021

Conversation

maurobringolf
Copy link

@maurobringolf maurobringolf commented Sep 9, 2021

I did some major changes on the handling of compound types, e.g. (Array (Array X Y) Y). As far as I understand, in the current code:

  1. The raw parser produces a structured representation of them, e.g. the grammar has all the necessary rules.
  2. The AstVisitor converts this structure into textual representation
  3. The sort2type function converts sort strings back to type objects ( ARRAY_TYPE, BITVECTOR_TYPE, etc.).

I propose to eliminate sort2type entirely and produce structured type representations in the AstVisitor directly, as done in this PR. This is only halfway done though, as BitVector and FloatingPoint is still parsed in sort2type.

Apart from that it looks like Opfuzz uses sort2type for constructing rules, so if that is needed then we could move sort2type into the opfuzz module.

@maurobringolf maurobringolf marked this pull request as ready for review September 11, 2021 10:11
@maurobringolf maurobringolf changed the title WIP: [A*] improve Array type support by implementing sort2type for it. [A*] Improve Array type support by moving sort parsing logic from sort2type into AstVisitor Sep 11, 2021
@wintered wintered changed the base branch from master to dev September 20, 2021 21:02
@wintered wintered merged commit 7076bc6 into testsmt:dev Sep 20, 2021
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

Successfully merging this pull request may close these issues.

2 participants