biotomas / ipasir

The Standard Interface for Incremental Satisfiability Solving
Other
47 stars 14 forks source link

Behaviour of repeated calls to ipasir_set_learn #22

Closed clausecker closed 3 years ago

clausecker commented 3 years ago

Right now it is unspecified what happens if you call ipasir_set_learn multiple times. There also doesn't seem to be any way to unregister a/the callback. Please amend the specification to clarify either case.

For example, you could specify that subsequent calls to ipasir_set_learn override the previously established callback. Passing NULL as a callback would deregister the callback.

biotomas commented 3 years ago

Hi Robert,

thank you for your comment, it is a valid point. Would you like to create a pull request with the described change?

all the best Tomas

clausecker commented 3 years ago

Doing that right now. Please also let me know:

In case of parallel solvers, what guarantees are made about the call to the callback? Can the assumption be made that the callback is always called from within the same thread as the call to ipasir_solve?