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

Renovations for SMT solvers #3575

Open
wadoon opened this issue Feb 28, 2025 · 0 comments
Open

Renovations for SMT solvers #3575

wadoon opened this issue Feb 28, 2025 · 0 comments
Labels
External Solvers Additional Solvers such as (SMT, Isabelle, ... SMT
Milestone
v2.13.0

Comments

@wadoon
Copy link
Member

wadoon commented Feb 28, 2025

For future dives into SMT, the following requirements are for SMT support:

  1. SMT queries should be stored for reproducibility.
  2. RunAllProves should not trigger the SMT solvers but should check SMT queries for regressions with the stored previous runs.
  3. The solver definitions (currently given as properties files) should be rewritten into KeY configuration files (json-like). This allows type-safety and more structured configuration.
  4. When structured concurrency is released from the Preview area, the SMT solver should use it for portfolio solving.
  5. CVC5 should receive test cases.
  6. setup-smt should install Princess
  7. setup-smt should install CVC4
@wadoon wadoon added the External Solvers Additional Solvers such as (SMT, Isabelle, ... label Feb 28, 2025
@wadoon wadoon added this to the v2.13.0 milestone Feb 28, 2025
@wadoon wadoon mentioned this issue Feb 28, 2025
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
External Solvers Additional Solvers such as (SMT, Isabelle, ... SMT
Projects
None yet
Milestone
v2.13.0
Development

No branches or pull requests
2 participants
@wadoon @FliegendeWurst