search

biotomas / ipasir

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

Slight ambiguity in the interface for ipasir_failed #9

Closed tuzz closed 4 years ago

tuzz commented 5 years ago

Hello,

I think it's slightly ambiguous whether ipasir_failed should always receive positive literals or whether it should receive literals that match the polarity of the assumptions.

For example, should both A and B pass in the following pseudocode or just one of them?

ipasir_init();

ipasir_add(1);
ipasir_add(0);

ipasir_assume(-1);

ipasir_solve();

assert(ipasir_failed(1) == 1);  // A
assert(ipasir_failed(-1) == 1); // B

Please could we clarify in the documentation? Thanks

Udopia commented 4 years ago

Hi tuzz,

ipasir_failed is only specified for assumption literals, i.e., you can only assert variant B. I added a comment to the documentation of ipasir_failed.

Thank you for your feedback