Open cdisselkoen opened 4 years ago
When we initially implemented termination support, we didn't think about incremental usage. As soon as the termination function returns true, we internally set a termination flag to true. We don't reset the flag. Having the termination callback per check-sat makes sense. There are three options to add support for this:
reset
flag to boolector_set_term to indicate whether the termination flag should be reset after check-sat@mpreiner @andrewvaughanj do we plan to include this in #62? Is this already supported by #62?
It seems that the result from the termination callback is "sticky"/"permanent" even across push/pop. Meaning that if the termination callback ever returns nonzero (indicating to terminate), then all future calls to
boolector_sat()
will terminate without even bothering to call the termination callback - even ifboolector_pop()
is used to revert to a previous state. I'm not sure if this is an intended feature or not. For my use case, I would prefer ifboolector_pop()
would reset the termination state, so that the termination callback would be checked again for future operations after the pop.Here's a code example of the behavior I'm observing:
In this example, we have a termination callback which terminates the first query, but (theoretically) lets all future queries continue indefinitely. In
main()
, we make two calls toboolector_sat()
, expecting the first to be terminated. After the first call is terminated, we useboolector_pop()
to return to an earlier state and check for satisfiability there.The output I get from running this code is
which indicates that both queries were terminated. Furthermore, the termination callback only prints once, indicating that the second call to
boolector_sat()
never even checked the termination callback. This is the behavior I'm wondering whether it's intended or a bug.My intended use case is to implement per-
sat()
-call query timeouts. So, even if one query times out and is terminated by the callback, I'd like the ability toboolector_pop()
and continue working with a different set of constraints. It's possible that the termination callback mechanism is not the correct tool for this purpose - if there's a different tool that would work better, I'd love to hear about it.