Improve API for non-satisfiable problems

clyngor/answers.py

@@ -42,7 +42,7 @@ class Answers:
 
     """
 
-    def __init__(self, answers:iter, command:str='', statistics:dict={},
+    def __init__(self, answers:iter, command:str='', statistics:dict={}, specific_statuses:dict={},
                  *, decoders:iter=(), with_optimization:bool=False, on_end:callable=None, **kwargs):
         """Answer sets must be iterable of (predicate, args).
 
@@ -77,6 +77,7 @@ def __init__(self, answers:iter, command:str='', statistics:dict={},
         self._with_optimality = False
         self._with_answer_number = False
         self.__on_end = on_end or (lambda: None)
+        self.__specific_statuses = specific_statuses
 
         for k, v in kwargs.items():
             if isinstance(getattr(self, '_' + k, None), bool):
@@ -323,6 +324,14 @@ def _atoms_as_string(self) -> bool:
     def statistics(self) -> dict:
         return dict(self._statistics)
 
+    @property
+    def is_unsatisfiable(self) -> bool:
+        return self.__specific_statuses.get("unsat", False)
+
+    @property
+    def is_unknown(self) -> bool:
+        return self.__specific_statuses.get("unknown", False)
+
 
 class ClingoAnswers(Answers):
     """Proxy to the solver as called through the python clingo module.

clyngor/parsing.py

@@ -195,13 +195,13 @@ def parse_clasp_output(output:iter or str, *, yield_stats:bool=False,
 
     """
     ASW_FLAG, OPT_FLAG, OPT_FOUND, PROGRESS = 'Answer: ', 'Optimization: ', 'OPTIMUM FOUND', 'Progression :'
-    UNSAT = 'UNSATISFIABLE'
+    UNSAT, UNKNOWN = 'UNSATISFIABLE', 'UNKNOWN'
     output = iter(output.splitlines() if isinstance(output, str) else output)
 
     # get the first lines
     line = next(output)
     infos = []
-    while not line.startswith(ASW_FLAG) and not line.startswith(UNSAT):
+    while not line.startswith(ASW_FLAG) and not line.startswith(UNSAT) and not line.startswith(UNKNOWN):
         infos.append(line)
         try:
             line = next(output)
@@ -221,6 +221,8 @@ def parse_clasp_output(output:iter or str, *, yield_stats:bool=False,
             yield 'progression', line[len(PROGRESS):].strip()
         elif line.startswith(UNSAT):
             yield 'unsat', True
+        elif line.startswith(UNKNOWN):
+            yield 'unknown', True
         elif not line.strip():  # empty line: statistics are beginning
             if not yield_stats: break  # stats are the last part of the output
             stats = {}

clyngor/solving.py

@@ -115,15 +115,21 @@ def solve(files:iter=(), options:iter=[], inline:str=None,
         stderr = (line.decode() for line in clingo.stderr)
         if return_raw_output:  return ''.join(stdout), ''.join(stderr)
         statistics = {}
+        specific_statuses = {
+            'unsat': False,
+            'unknown': False,
+        }
 
         # remove the tempfile after the work.
         on_end = lambda: (clingo.stderr.close(), clingo.stdout.close())
         if inline and tempfile_to_del and delete_tempfile:
             on_end = lambda: (os.remove(tempfile_to_del), clingo.stderr.close(), clingo.stdout.close())
 
-        return Answers(_gen_answers(stdout, stderr, statistics, error_on_warning),
+        answers = _gen_answers(stdout, stderr, statistics, specific_statuses, error_on_warning)
+        return Answers(answers,
                        command=' '.join(run_command), on_end=on_end,
                        decoders=decoders, statistics=statistics,
+                       specific_statuses=specific_statuses,
                        with_optimization=True)
 
 
@@ -202,7 +208,7 @@ def clingo_version(clingo_bin_path:str=None) -> dict:
 
 
 
-def _gen_answers(stdout:iter, stderr:iter, statistics:dict,
+def _gen_answers(stdout:iter, stderr:iter, statistics:dict, specific_statuses:dict,
                  error_on_warning:bool) -> (str, int or None, bool, int):
     """Yield 4-uplet (answer set, optimization, optimum found, answer number),
     and update given statistics dict with statistics payloads
@@ -226,7 +232,9 @@ def _gen_answers(stdout:iter, stderr:iter, statistics:dict,
         elif ptype == 'statistics':
             statistics.update(payload)
         elif ptype == 'unsat':
-            pass  # don't care
+            specific_statuses['unsat'] = True
+        elif ptype == 'unknown':
+            specific_statuses['unknown'] = True
         elif ptype == 'info':
             pass  # don't care
         else:

clyngor/test/test_api.py

@@ -5,6 +5,7 @@
 from clyngor import ASP, solve, command
 from clyngor import utils, CLINGO_BIN_PATH
 from .definitions import run_with_clingo_binary_only
+from .test_time_limit import QUEENS
 
 
 @pytest.fixture
@@ -230,7 +231,11 @@ def test_unsatisfiable():
     :- p(X), q(X).
     """
     models = clyngor.solve(inline=CODE, stats=False)
+
     model = next(models, None)
+    assert models.is_unsatisfiable
+    assert not models.is_unknown
+
     assert model is None
     assert len(models.statistics) == 4
 
@@ -244,6 +249,36 @@ def test_unsatisfiable_statistics():
     :- p(X), q(X).
     """
     models = clyngor.solve(inline=CODE, stats=True)
+
     model = next(models, None)
+    assert models.is_unsatisfiable
+    assert not models.is_unknown
+
     assert model is None
     assert len(models.statistics) > 4
+
+
+def test_unknown():
+    "Should return an empty answers set"
+    models = clyngor.solve(inline=QUEENS, stats=False, time_limit=1)
+
+    model = next(models, None)
+    assert not models.is_unsatisfiable
+    assert models.is_unknown
+
+    assert model is None
+    assert len(models.statistics) == 5
+
+
+def test_unknown_statistics():
+    "Should return an empty answers set but provide the statistics"
+    models = clyngor.solve(inline=QUEENS, stats=True, time_limit=1)
+
+    model = next(models, None)
+    assert not models.is_unsatisfiable
+    assert models.is_unknown
+
+    assert model is None
+    # NOTE: This test may sometimes fail if grounding does not take place within 1 second
+    # If this happens, just re-run again.
+    assert len(models.statistics) > 5

clyngor/test/test_parsing.py

@@ -275,6 +275,32 @@ def test_unsat_stats():
             assert model == stats
 
 
+def test_unknown():
+    parsed = Parser().parse_clasp_output(OUTCLASP_UNKNOWN.splitlines())
+    current = next(parsed, None)
+    assert current is not None
+    l_type, model = current
+    assert l_type == 'unknown' and model is True
+    assert next(parsed, None) is None
+
+
+def test_unknown_stats():
+    parsed = Parser().parse_clasp_output(OUTCLASP_UNKNOWN.splitlines(), yield_stats=True)
+    stats = {
+        'Models': '0',
+        'Calls': '1',
+        'Time': '0.001s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)',
+        'CPU Time': '0.000s'
+    }
+
+    for type, model in parsed:
+        assert type in ('unknown', 'statistics')
+        if type == 'unknown':
+            assert model is True
+        elif type == 'statistics':
+            assert model == stats
+
+
 def test_multithread_with_progression():
     parsed = Parser().parse_clasp_output(CLINGO_OUTPUT_MULTITHREADING_WITH_PROGRESS.splitlines(),
                                          yield_prgs=True)
@@ -412,6 +438,17 @@ def test_multithread_with_progression():
 CPU Time     : 0.000s
 """
 
+OUTCLASP_UNKNOWN = """clasp version 3.2.0
+Reading from l.lp
+Solving...
+UNKNOWN
+
+Models       : 0
+Calls        : 1
+Time         : 0.001s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
+CPU Time     : 0.000s
+"""
+
 
 CLINGO_OUTPUT_MULTIPLE_OPT = """
 clingo version 5.2.2