biotomas / ipasir

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

ipasir_val documentation: clarify when a literal is "not important". #15

Closed ykazakov closed 4 years ago

ykazakov commented 4 years ago

The current documentation of the method ipasir_val() in ipasir.h says that the value 0 is returned if the literal is not important. I suggest to clarify what does it mean, e.g., that each solution that agrees with all non-zero values of ipasir_val() is a model of the formula under the assumptions.