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

Fix isFinite for all kinds of sets #286

Open
konnov opened this issue Oct 18, 2022 · 1 comment
Open

Fix isFinite for all kinds of sets #286

konnov opened this issue Oct 18, 2022 · 1 comment
Assignees
Labels
effort-easy Can be completed within about 1 day impact-low Low impact input needed Further information is requested simulator Quint simulator

Comments

@konnov
Copy link
Contributor

konnov commented Oct 18, 2022

We now have different kinds of sets, including Int and Nat, and sets containing them. We should update isFinite to work correctly.

@konnov konnov added W1 simulator Quint simulator labels Oct 18, 2022
@konnov konnov self-assigned this Oct 18, 2022
@konnov konnov added impact-low Low impact effort-easy Can be completed within about 1 day labels Nov 29, 2022
@shonfeder shonfeder removed this from the T4.3 Simulator beyond Q1 milestone Jan 9, 2024
@shonfeder shonfeder removed the W1 label Jan 9, 2024
@shonfeder
Copy link
Contributor

The current simulator definition of isFinite:

case 'isFinite':
// at the moment, we support only finite sets, so just return true
this.applyFun(app.id, 1, _set => just(rv.mkBool(true)))
break

It's not clear to me what fixing means in this context.

@shonfeder shonfeder added the input needed Further information is requested label Jan 9, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
effort-easy Can be completed within about 1 day impact-low Low impact input needed Further information is requested simulator Quint simulator
Projects
None yet
Development

No branches or pull requests

2 participants