KeY/JSON config for SMT solvers

[wadoon]

Intended Change

The SMT solvers are defined in unstructured untyped properties files. In the meantime, we have updated our KeY config to a JSON-like format, we should also update our SMT solvers definition files.

This comes with this PR.

Plan

• rewriting history

Type of pull request

• Refactoring (behaviour should not change or only minimally change)

Ensuring quality

• CI

[wadoon]

KaKeY: Go ahead.

[mattulbrich]

Agreed at meeting: Good idea, but let's have individual json files (to allow for additions)

[wadoon]

Agreed at meeting: Good idea, but let's have individual json files (to allow for additions)

After re-considering this: This suggestion makes no sense. The addition of new SMT solvers is independent of single/multiple solvers in a config file. Also, as Java has no built-in discovery of resources in a classpath destination, this is unimplementable without great effort or external libraries.

The current implementation uses an index file. The user needs to create the folder ROOT/de/uka/ilkd/key/smt/solvertypes/ with the solvers.txt and the properties file of the SMT solver. Then, KeY needs to be loaded with java -cp key-exe.jar:ROOT/ <main>.

The new resolution of SMT solvers is described in the javadoc, and allows addition and overriding SMT solver configs using files in $HOME/.key/smt-solvers.json and <cwd>/smt-solvers.json.

[wadoon]

Two errors should remain:

1. spotlessApply does not fix the formatting locally.
2. EOFException b/c Stream is closed when sending (get-unsat-core) to Z3.

[wadoon]

The page in key-docs: https://keyproject.github.io/key-docs/devel/AddingSMTSolvers/
needs to be revised.

Is done. I discovered that the preamble loading is stupid (only classpath), and made some extensions for files/URLs.

[wadoon]

@unp1 @Drodt it is ready now.