search

biotomas / ipasir

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

ipasir_solve and the state of the solver #16

Closed ykazakov closed 4 years ago

ykazakov commented 4 years ago

A few questions/clarifications about the documentation of ipasir_solve:

  1. When the call of ipasir_solve is interrupted (using ipasir_set_terminate) the documentation says that the state of the solver remains INPUT. What if it was SAT or UNAST before the call of ipasir_solve? Should it change to INPUT or remain the same as before?

  2. What is the state of the solver during the run of ipasir_solve, e.g., when callback functions of ipasir_set_terminate or ipasir_set_learn are triggered? Is it allowed to call other functions, e.g., ipasir_val or ipasir_add in callbacks? Probably not a good idea. Should it be documented?

biotomas commented 4 years ago

Hi Yevgeny, thanks for your questions and remarks (in other issues). Let me asnwer: 1, the state after an interrupted ipasir_solve must change to INPUT 2, the state of the solver during ipasir_solve is undefined and therefore none of the other methods should be used.

As for your remarks, I agree with all of them, why don't you create a pull request with the changes you propose so we could integrate them in ipasir?