SMT Refactoring

[BookWood7th]

Intended Change

This PR aims to refactor the SMT parts of KeY. Among other things this PR will replace the current homemade solutions for solver scheduling with methods of ThreadPool classes. This should cut down on thread creation overhead.

Plan

• Implement ThreadPool scheduling
• Overhaul SMTResult to avoid requests to SMTSolver pertaining to its result
• Overhaul Sockets
• Overhaul SimplePipe
• Overhaul SolverCommunication
• Overhaul SMTProblem
• Overhaul SolverListener
• Document Class Responsibilities
• Testing
• Code Formatting

Type of pull request

• Refactoring (behaviour should not change or only minimally change)
• There are changes to the (Java) code

Ensuring quality

• I made sure that introduced/changed code is well documented (javadoc and inline comments).
• I have tested the feature as follows: ...
• I have checked that runtime performance has not deteriorated.

Additional information and contact(s)

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.

[wadoon]

I am not sure if this is the right time to do this. In Java, the jep for structured concurrency is on the way and truly the thing we want.

https://openjdk.org/jeps/505

[codecov]

Codecov Report

Attention: Patch coverage is 36.36364% with 35 lines in your changes missing coverage. Please review.

Project coverage is 39.05%. Comparing base (460cb53) to head (1a55ff3).
Report is 335 commits behind head on main.

Files with missing lines	Patch %	Lines
...a/de/uka/ilkd/key/smt/SMTSolverImplementation.java	32.25%	18 Missing and 3 partials ⚠️
.../main/java/de/uka/ilkd/key/smt/SolverLauncher.java	36.84%	9 Missing and 3 partials ⚠️
.../key/smt/solvertypes/SolverTypeImplementation.java	33.33%	1 Missing and 1 partial ⚠️

Additional details and impacted files

@@             Coverage Diff              @@
##               main    #3611      +/-   ##
============================================
+ Coverage     39.00%   39.05%   +0.05%     
- Complexity    17118    17157      +39     
============================================
  Files          2016     2015       -1     
  Lines        126328   126336       +8     
  Branches      21330    21322       -8     
============================================
+ Hits          49270    49339      +69     
+ Misses        70974    70914      -60     
+ Partials       6084     6083       -1     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.

[BookWood7th]

I am not sure if this is the right time to do this. In Java, the jep for structured concurrency is on the way and truly the thing we want.

Thanks for bringing this to my attention!
As far as I'm aware, the SMT Translation subtasks are fairly independent and should be treated as such. While they do spawn additional threads in the main branch version, this behavior is no longer present in this PR.
Each SMTSolver instance implements Runnable/Callable and is handled in a purely sequential manner (with the exception of the creation of an external process, which falls outside the scope of Java concurrency to my knowledge)

StructuredConcurrency would offer advantages in the case of unexpected failures due to bugs in the code of KeY, such as null pointer exceptions when not adding a listener to instances of SMTSolverImplementation, where this PR checks if any Future completed with an exception after it reports that it is "done". How KeY should behave in cases like these is unclear to me. Current main branch behavior is not suitable, as it fails without any notice in either log or UI (only as uncaught exceptions in the console).
Another point where this could be added is the SMTInvokeAction, which creates a new Thread to perform its task.

Both of these changes would still benefit from a refactoring and would be easier to implement afterwards in my opinion.