User-defined decisions in SMT-LIB

[Tomáš Kolárik]

Dear SMT-LIB community,

I am forming a working group for the proposal of handling user-defined
decisions of SMT solvers to the standard.
I drafted a proposal of several commands on the topic in the following
thread on the official SMT-LIB GitHub:

https://github.com/SMT-LIB/SMT-LIB-2/discussions/35

I invite you to join the group of interested people and to collect
feedback, benchmarks and compliant solvers.
For example, the functionality should not be difficult to implement in
SMT solvers with an underlying SAT solver that follows the IPASIR interface.
Join the discussion or write me an e-mail. Let me know if you have a
student or an interested fellow from your group so I can reach them.

The goal is to write down a proposal as a submission to an SMT-related
venue, supported by a series of benchmarks.

For example, there is a family of satisfiable incremental benchmarks in
the SMT-LIB that remains unsolved:

https://smt-comp.github.io/2024/results/qf_bvlra-incremental/
https://smt-comp.github.io/2025/results/qf_bvlra-incremental/

because the original benchmarks rely on guiding the decisions.
The proposal would allow to encode them.

Best,
Tomáš Kolárik
Maintainer of OpenSMT