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

Add a flag to allow using multiple solvers at the same time #572

Open
yav opened this issue Sep 11, 2024 · 1 comment
Open

Add a flag to allow using multiple solvers at the same time #572

yav opened this issue Sep 11, 2024 · 1 comment
Labels
cn solver Related to the SMT solver backend

Comments

@yav
Copy link
Collaborator

yav commented Sep 11, 2024

Different solvers perform better on different problems. To gain the best of both worlds, we may want to issue a problem to more than one solver at the same time.

Potentials challenges:

  • We need to investigate if there is a way to interrupt a solver that is taking a long time.
  • Worst case we can just kill the process, but we need to be able to rebuild the solver's state, to get it ready for the next query.
@yav yav added cn solver Related to the SMT solver backend labels Sep 11, 2024
@cp526
Copy link
Collaborator

cp526 commented Oct 31, 2024

Setting up CN so it always runs both cvc5 and z3 in parallel would be really good, and might noticeably improve CN performance for practical purpose.

Here's a recent issue where the two solvers result in drastically different performance: #613 .

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
cn solver Related to the SMT solver backend
Projects
None yet
Development

No branches or pull requests

2 participants