Incremental support (IPASIR)

[tuzz]

Hello,

Many solvers support incremental solving and build a static library for interfacing with the solver. For example, Cadical emits an ipasir.o object file as per the makefile here:

• https://github.com/arminbiere/cadical/blob/c622a490ec3d9a1a1e998b08120c9b8d0b67a123/makefile.in#L72

Given you've done a tremendous job compiling all these solvers, would it be possible to make it so an application can call these IPASIR static libraries easily?

The only way I can think to do this is to compile/link the incremental application inside the container alongside the solver. Therefore, I think a sensible approach might be to introduce a convention where the ipasir static library is placed in a specific location on the filesystem in the docker container. Then there could be some command-line flags to simplify this process of compiling and linking an application. For example:

$ satex list --supports-incremental

This ^ command could filter the list of solvers so that only those supporting incrementality are listed.

$ satex run cadical:2019 --application my_app

This ^ command could copy the my_app/ directory into the docker container and run make && make run - or something along those lines.

Obviously, there's a lot to be figured out, but I think this could be a useful feature that's broadly inline with the aims of the SAT Heritage project, to make a vast number of solvers easily available.

Thanks

[pauleve]

Hi,
Cool feature indeed :-) I have the feeling it could be more suited for the satex build command: the idea would be to build your own docker image. Something like this for instance:

$ satex build cadical:2019 --ipasir my_app

which would build an image cadical:2019-my_app, and could be use with satex run cadical:2019-my_app or even directly with docker.

Do you have an example of my_app I can test with?

[tuzz]

Sure, here's a barebones app:

my_app.zip

You can compile and run the app with make && make run.

I've included a version of libipasir I compiled on my Mac but that would need to be replaced with the one from the Docker image. You can set the -L switch in the makefile to search a filesystem path for it.

Thanks