clyngor
clyngor copied to clipboard
Improve API for non-satisfiable problems
Related to #32, I was playing around with clyngor
a little bit more, and noticed that when a problem resolution times out, it actually generates some stats (if grounding took place). However, clyngor
does not support this, because there was no difference from the API perspective on when a problem fails to return an answer because of being unsatisfiable or unknown (actual timeout).
This PR implements the following functionality:
- Allows yielding stats on UNKNOWN status (basically, when resolution times out).
- Allows developers to differentiate timeouts from unsatisfiable problems in the API.
models = clyngor.solve(inline="")
next(models) # It is needed to first iterate and try to search for a valid answer
assert models.is_unknown is True # is_unknown will be True if a timeout happens
assert models.is_unsatisfiable is True # is_unsatisfiable will be True if an unsatisfiable problem is provided
Note that it is impossible for both is_unknown
and is_unsatisifiable
to be True at the same time.
Also, statistics
will be available on both statuses now.
Unit tests provided:
-
test_api::test_unsatisfiable
: Now it also checks for both attributes. -
test_api::test_unsatisfiable_statistics
: Now it also checks for both attributes. -
test_api::test_unknown
: New test case using the Queens problem and a 1-second time limit to validate the unknown stats behaviour. -
test_api::test_unknown_statistics
: Like the previous one, but checking stats as well. -
test_parsing::test_unknown
: Checks the correct parsing and yielding of theUNKNOWN
status. -
test_parsing::test_unknown_statistics
: Like the previous one, but checking that it yields stats when needed.
While working on these changes, I noticed that some room for improvement: unify how result statuses are handled.
Here is the original source on the result status report from clasp
: https://github.com/potassco/clasp/blob/17c4e466111c0b9da173f9097786a0d22b70e1c4/src/clasp_output.cpp#L638
As you can notice, it has 4 possible statuses:
-
UNKNOWN
-
UNSATISFIABLE
-
SATISFIABLE
-
OPTIMUM FOUND
The first two statuses are now available as an attribute to the Answers
class. However, to differentiate and handle the last two, the OPTIMUM FOUND
status is yielded with the answers iterator.
It would be interesting to provide an enum with those 4 statuses, then access it like models.result_status
and remove the optimum_found
yield. The problem is that removing this last variable would probably break some implementations though.