ipasir2 vs ipasir up

[barrettcw]

How does the proposed ipasir2 relate to the recent extension to ipasir up? For embedding SAT solvers in tools like SMT solvers, we need the additional flexibility of the ipasir up extension.

[m-fleury]

Maybe a first question would be whether there is any solver besides CaDiCaL that is implementing (or planning to) implement the UP interface… If the answer is none, then it is not clear if a standardization is useful.

(And there are some ugly parts in CaDiCaL to handle the UP now…)

[barrettcw]

We have transitioned to making IPASIR-UP the standard interface for the cvc5 SMT solver. We plan to use CaDiCaL as the default SAT solver in cvc5 for now, but we will definitely be encouraging other SAT solvers to implement the interface.

[Udopia]

Thank you for getting in touch. IPASIR-2 aims to cover a wide range of use cases, of which IPASIR-UP is only one. That is, we are in contact and discussing what is useful for IPASIR-UP, and we are making a coordinated move to have synergies, but we are not mixing them. IPASIR-UP will remain a stand-alone extension. But it will be easier to extend an IPASIR-2 solver to support IPASIR-UP as well, simply because we included specifications of some useful subsets of its functionality (cf. clause import, configuration of variable polarities, etc.).

[barrettcw]

Glad to hear that you are considering the impact on IAPSIR-UP. It will be great if these extensions remain compatible.