Termination

[Skarrabor]

Hello,

basicly what im trying to do is to terminate boolector after a function returns a certain value.

For example a function that returns true after a certain while.

My current understanding of the termination and termination_callback functions is that i enter the desired function and the state it triggers the termination into the termination_callback.

Example:

int32 myTimer(int32 x) {

  //wait for x amount of time

  return 1;

}

set_term(btor, myTimer, 1)

But when do i call boolector_terminate? 

And does it check if its supposed to terminate even if its currently solving something?

Thank you for your help and have a nice day,

Daniel

[Aina Niemetz]

Hi Daniel,

by setting the callback function with boolector_set_term, Boolector will
then terminate when the termination condition is met. Boolector checks
the callback function at certain check points in the code.

The function boolector_terminate returns true if the termination
condition is met. You typically don't need to call this function.
You will only need this if you build something on top of Boolector and
want to terminate when Boolector terminates.

Note that this termination mechanism is only propagated to the
underlying SAT solver if it also supports such a mechanism (currently,
of the supported SAT solvers only Lingeling does).

If the SAT solver does not support such a termination mechanism, we have
no way to terminate the SAT solver even when the termination condition
is true -- we have to wait until the call to the SAT solver is done.

In case you want to configure a time limit with this, we have an open PR
that implements this (and we hope to be able to merge it soon):
https://github.com/Boolector/boolector/pull/62

HTH,
Aina

> --
> You received this message because you are subscribed to the Google
> Groups "Boolector" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to boolector+...@googlegroups.com
> <mailto:boolector+...@googlegroups.com>.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/boolector/f0ad10b3-4490-4f4b-a73e-2aeea7158df2%40googlegroups.com
> <https://groups.google.com/d/msgid/boolector/f0ad10b3-4490-4f4b-a73e-2aeea7158df2%40googlegroups.com?utm_medium=email&utm_source=footer>.