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

satNum isn't working #553

Closed
LeventErkok opened this issue Oct 29, 2018 · 2 comments
Closed

satNum isn't working #553

LeventErkok opened this issue Oct 29, 2018 · 2 comments

Comments

@LeventErkok
Copy link
Contributor

   Cryptol> :set satNum=2
   Cryptol> :sat \x -> x >(3:Integer)
   .. Runs forever ..

#552 should address this.

@LeventErkok
Copy link
Contributor Author

LeventErkok commented Nov 1, 2018

@atomb You can close this ticket since you merged the PR; though one issue remains.

If you set satNum=all and if there are an infinite-number of satisfying models, then you'll wait forever; since allSat in SBV is no longer lazy. (Well, you'll probably first run out of heap I suppose.)

This is less of a problem for Cryptol than SBV proper, as most interesting Cryptol types subject to sat will only be finitely inhabited. But now that you guys added Integer to the mix, perhaps it's worth mentioning it in the docs somewhere.

@atomb
Copy link
Contributor

atomb commented Nov 1, 2018

Thanks, @LeventErkok ! I'll update the docs to reflect that.

@atomb atomb closed this as completed Nov 1, 2018
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