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.

Sign up for GitHub

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

Jump to bottom

[SMT] Add basic array operations #6827

Merged
merged 1 commit into from
Mar 14, 2024
Merged

[SMT] Add basic array operations #6827

merged 1 commit into from
Mar 14, 2024

Conversation

maerhart
Copy link
Member

No description provided.

TaoBi22
TaoBi22 approved these changes Mar 14, 2024
View reviewed changes
Copy link
Contributor

@TaoBi22 TaoBi22 left a comment •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM! Would it maybe be worth having verifiers to make sure operands match the Array domain/range types where appropriate (e.g. index is of domain type in a store/select op)?

fabianschuiki
fabianschuiki approved these changes Mar 14, 2024
View reviewed changes
Copy link
Contributor

@fabianschuiki fabianschuiki left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM! Whoop whoop array theory!

@maerhart
Copy link
Member Author

Would it maybe be worth having verifiers to make sure operands match the Array domain/range types where appropriate (e.g. index is of domain type in a store/select op)?

That's already done by the TypesMatchWith traits added in the ODS file.

@maerhart maerhart merged commit 6914bc6 into main Mar 14, 2024
4 checks passed
@maerhart maerhart deleted the maerhart-smt-array-ops branch March 14, 2024 23:29
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@fabianschuiki fabianschuiki fabianschuiki approved these changes

@TaoBi22 TaoBi22 TaoBi22 approved these changes

@math-fehr math-fehr Awaiting requested review from math-fehr

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@maerhart @fabianschuiki @TaoBi22