Improve API for non-satisfiable problems #33
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
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:
Note that it is impossible for both
is_unknown
andis_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.