Skip to content

scan for cvc5 before cvc4 + generate the error msg for missing smt#2513

Merged
facundominguez merged 5 commits into
ucsd-progsys:developfrom
clayrat:cvc5-opt
May 28, 2025
Merged

scan for cvc5 before cvc4 + generate the error msg for missing smt#2513
facundominguez merged 5 commits into
ucsd-progsys:developfrom
clayrat:cvc5-opt

Conversation

@clayrat

@clayrat clayrat commented Apr 8, 2025

Copy link
Copy Markdown
Contributor

This is potentially related to the problem that @ulysses4ever described in #1391, although I couldn't reproduce it.

ulysses4ever
ulysses4ever reviewed Apr 8, 2025
View reviewed changes

@ulysses4ever ulysses4ever left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Thanks for looking into it!

Looking at this PR and related code, I realized that CVC5 support was added just few months ago. My project currently uses a stable release of liquidhaskell (0.9.10.1), so I haven't had a chance to test this feature, and my attempts were doomed to fail... Maybe this is also why you couldn't reproduce it.

Comment thread liquidhaskell-boot/src/Language/Haskell/Liquid/UX/CmdLine.hs Outdated
Comment thread liquidhaskell-boot/src/Language/Haskell/Liquid/UX/Config.hs Outdated
@facundominguez

facundominguez commented May 26, 2025

Copy link
Copy Markdown
Collaborator

Hello @clayrat, should this be merged? Would you like to address any of the review comments in advance?

@clayrat

clayrat commented May 28, 2025

Copy link
Copy Markdown
Contributor Author

I tried the Ord+Bounded idea, but the fact that we have two different values for Z3 (Z3 and Z3mem) will probably be confusing for the user, and I couldn't think of a quick solution for this.

@clayrat

clayrat commented May 28, 2025

Copy link
Copy Markdown
Contributor Author

I think I'll change the error to be generated from the lookup order list; that way, we'll have a single source of truth.

@clayrat

clayrat commented May 28, 2025

Copy link
Copy Markdown
Contributor Author

@facundominguez Should be ready.

@clayrat clayrat changed the title scan for cvc5 before cvc4 scan for cvc5 before cvc4 + generate the error msg for missing smt May 28, 2025
@ulysses4ever

ulysses4ever commented May 28, 2025

Copy link
Copy Markdown
Contributor

I tried the Ord+Bounded idea, but the fact that we have two different values for Z3 (Z3 and Z3mem) will probably be confusing for the user, and I couldn't think of a quick solution for this.

Arguably, Filtering one specific value out of a list would still be a more robust solution than the status quo, even if not very elegant.

facundominguez
facundominguez approved these changes May 28, 2025
View reviewed changes

@facundominguez facundominguez left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

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

LGTM!

@facundominguez

facundominguez commented May 28, 2025

Copy link
Copy Markdown
Collaborator

Arguably, Filtering one specific value out of a list would still be a more robust solution than the status quo, even if not very elegant.

If you want to pursue this in another PR, I think it would be a nice improvement.

@facundominguez facundominguez merged commit 1f2a22b into ucsd-progsys:develop May 28, 2025
4 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@facundominguez facundominguez facundominguez approved these changes
+1 more reviewer
@ulysses4ever ulysses4ever ulysses4ever left review comments
Reviewers whose approvals may not affect merge requirements

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

@clayrat @facundominguez @ulysses4ever