biotomas / ipasir

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

ipasir_failed documentation: clarify what is a "used assumption" #14

Closed ykazakov closed 4 years ago

ykazakov commented 4 years ago

The current documentation of the method ipasir_failed() in ipasir.h says that the value 1 is returned if the given assumption literal was used to prove the unsatisfiability of the formula. This is a bit vague and maybe easily misunderstood (e.g., that the assumption is essential for unsatisfiability of the formula; if it is removed, the formula becomes satisfiable). I suggest to add a clarification, e.g., the formula remains unsatisfiable even just under assumption literals for which ipasir_failed() returns 1