wkschwartz / pigosat

Go (golang) bindings for Picosat, the satisfiability solver
Other
15 stars 4 forks source link

Implement picosat_set_interrupt #27

Open wkschwartz opened 7 years ago

wkschwartz commented 7 years ago

Allow users to set custom interrupt functions as well as providing default time and signal-based (e.g., Ctrl+C) ones.

picosat.h doesn't say it, but the interrupt function should return non-zero when it's time for picosat_sat to give up and zero if it can keep going. The external_state should be a pointer to some Go object that the Go interrupt function can read for information about what it's supposed to do. May need some C type casting to allow this.

wkschwartz commented 7 years ago

Is there any way to use the Context type. Perhaps we pass a Context object to a new method SolveInContext (but not just to Solve, which would violate the backward compatibility promise; the context package says Context objects should always be passed to every function that uses one rather than stored in a struct).

wkschwartz commented 7 years ago

A user could not use picosat_set_interrupt more than once concurrently. We'll have to be careful to serialize access to it. Otherwise a timer going off (for example) for one Solve call would end all Solve calls. This may automatically be taken care of by way of Solve's use of a write lock.