kissat_set_terminate is not Implemented

[ghost]

Declaration is there but implementation is not.

[arminbiere]

As we discussed per EMail, the asynchronous 'kissat_terminate' function is implemented (and heavily tested actually), but the function 'kissat_set_terminate' which uses more synchronous call-backs following the IPASIR interface is not implemented yet. It should not be difficult to do so though and I will work on it while making the solver incremental and thus supporting IPASIR completely.

[arminbiere]

In the latest release it is implemented but the call back is actually not executed yet, thus the effect is zero at this point. So I will keep the issue and it will need to be addressed during further work on incremental solving.

[arminbiere]

The function now exists in the sc2022 variants (so linking works), but it does not trigger checking, i.e., calling the termination function yet. Again, I will work on this if I find time to extend IPASIR support.

[amatuag]

Hi Armin,

Is there a Kissat equivalent of Cadical's terminator which is checked periodically for termination or is kissat_set_terminate the synchronous one which is yet to be implemented ?

[arminbiere]

There is this 'set_terminate' exactly for this purpose. As Kissat testing is driven by line coverage there is even a complex testing method for all the places termination can be triggered (see testterminate.c and terminate.[ch])