We should remove the "batch" solving mode, which writes all the proofs obligations on disk, runs solvers on them, and parse the results back.
Indeed, PR #935 introduced the incremental mode, which gave 15% speed up on all benchmarks by not writing into SMT files but passing the SMT directly into interactive reusable I/O solvers.
The incremental mode is moreover based on an abstract solver interface that can be now implemented with any possible solver, including cloud solvers, FFI solvers like CVC5, perhaps lean automated solvers.
This abstract interface no longer assumes that the solver is SMT-based (although the current implementation of that abstract solver does use the SMT dialect and encoding).
It assumes incrementality, which we will be able to leverage to solve multiple proof obligations that share the same context, get the unsat core, get possible proofs, get specific models and possibly add more assumptions when models are disproved, and perform more fine-grained dichotomy of proof obligations to figure out better diagnostics, all of this independent of any solver.
Therefore, it makes little sense to keep the batch mode the default and even maintain it as well. At worst, we should at least deprecate it.
We should remove the "batch" solving mode, which writes all the proofs obligations on disk, runs solvers on them, and parse the results back.
Indeed, PR #935 introduced the incremental mode, which gave 15% speed up on all benchmarks by not writing into SMT files but passing the SMT directly into interactive reusable I/O solvers.
The incremental mode is moreover based on an abstract solver interface that can be now implemented with any possible solver, including cloud solvers, FFI solvers like CVC5, perhaps lean automated solvers.
This abstract interface no longer assumes that the solver is SMT-based (although the current implementation of that abstract solver does use the SMT dialect and encoding).
It assumes incrementality, which we will be able to leverage to solve multiple proof obligations that share the same context, get the unsat core, get possible proofs, get specific models and possibly add more assumptions when models are disproved, and perform more fine-grained dichotomy of proof obligations to figure out better diagnostics, all of this independent of any solver.
Therefore, it makes little sense to keep the batch mode the default and even maintain it as well. At worst, we should at least deprecate it.