Add solver and interrupted exceptions to all prover methods - #676

Draft

baierd wants to merge 27 commits into

masterfrom

add_solver_and_interruptedExceptions_to_all_prover_methods

Commits on Jun 9, 2026

Add common API in AbstractProver to check inheritors for closed status
baierd
committed
c794274
Add new OptimizationProverDelegate that handled common checks of OptimizationProvers
baierd
committed
4a2e807
Remove common checks from Optimization Provers of Z3 and Mathsat
baierd
committed
d3c7a74
Add implementations for getModel() and getEvaluator() in AbstractProver with new abstract methods that implement their behavior, so that the common checks are in a central class and guaranteed to b…
baierd
committed
0886c38
Add default implementation of getUnsatCore() in AbstractProver that performs common checks before delegating to a new implementation method getUnsatCoreImpl() (that is implemented by all solvers th…
baierd
committed
8232a8d
Add default implementation of unsatCoreOverAssumptions() in AbstractProver that performs common checks before delegating to a new implementation method unsatCoreOverAssumptionsImpl() (that is imple…
baierd
committed
811e75b
Reduce visibility of getModelImpl() and getEvaluatorImpl() as they should not be public
baierd
committed
bfb7f23
Remove another redundant usage of checkGenerateModels() from MathSAT
baierd
committed
1075a97
Reduce visibility of getModelImpl() and getEvaluatorImpl() as they should not be public
baierd
committed
58f602a
Remove another redundant usage of checkGenerateModels() from MathSAT
baierd
committed
837cbd0
Add AllSat default impl in AbstractProver that calls the new method AllSatImpl after all common checks. AllSatImpl now handles all AllSat implementations and redundant checks are removed
baierd
committed
a11a593

Navigation Menu

Uh oh!

Add solver and interrupted exceptions to all prover methods - #676

Add solver and interrupted exceptions to all prover methods#676
baierd wants to merge 27 commits into
masterfrom
add_solver_and_interruptedExceptions_to_all_prover_methods

Commits on Jun 9, 2026

Add common API in AbstractProver to check inheritors for closed status

Add new OptimizationProverDelegate that handled common checks of OptimizationProvers

Remove common checks from Optimization Provers of Z3 and Mathsat

Add implementations for getModel() and getEvaluator() in AbstractProver with new abstract methods that implement their behavior, so that the common checks are in a central class and guaranteed to b…

Add default implementation of getUnsatCore() in AbstractProver that performs common checks before delegating to a new implementation method getUnsatCoreImpl() (that is implemented by all solvers th…

Add default implementation of unsatCoreOverAssumptions() in AbstractProver that performs common checks before delegating to a new implementation method unsatCoreOverAssumptionsImpl() (that is imple…

Reduce visibility of getModelImpl() and getEvaluatorImpl() as they should not be public

Remove another redundant usage of checkGenerateModels() from MathSAT

Reduce visibility of getModelImpl() and getEvaluatorImpl() as they should not be public

Remove another redundant usage of checkGenerateModels() from MathSAT

Add AllSat default impl in AbstractProver that calls the new method AllSatImpl after all common checks. AllSatImpl now handles all AllSat implementations and redundant checks are removed

Commits on Jun 10, 2026

Add JavaDoc for allsat impls

Improve impl spec JavaDoc for AbstractProver#allSatImpl

Add default impl for AbstractProver#getStatistics to perform common checks and a delegate method that can be implemented by the solvers

Move ShutdownNotifier from AbstractProverWithAllSat to AbstractProver, check for interrupts in all solver touching API and throw InterruptedException in all methods that may be interrupted (includi…

Extend optimization API with InterruptedExceptions and checks for solver shutdown + add common API shutdownIfNecessary() in AbstractProver that handles this

Add shutdownIfNecessary() check to all common checks that did not yet have it in AbstractProver

Add comment to size() in AbstractProver

Add API for shouldShutdown() in AbstractProver, handling whether a ShutdownManager should shut down without needing to use the manager

Rename most ShutdownNotifier to reflect that they are context bound

Switch Boolector and Bitwuzla to using common shouldShutdown API from AbstractProver instead of using the notifier directly

Commits on Jun 12, 2026

Add type check for delegate in OptimizationProverDelegate

Add type check for delegate in InterpolatingProverDelegate

Merge branch 'master' into add_common_optimizationProver_delegate2

Merge branch 'add_common_optimizationProver_delegate2' into handle_model_generation_api_through_impl_delegates

Merge branch 'handle_model_generation_api_through_impl_delegates' into add_common_impl_for_unsatCore_allSat

Merge branch 'add_common_impl_for_unsatCore_allSat' into add_solver_and_interruptedExceptions_to_all_prover_methods