From a15b818006313bcf832d3ebf135a6c2cfc1af92e Mon Sep 17 00:00:00 2001 From: Diego Barreiro Date: Thu, 18 May 2023 13:50:35 +0200 Subject: [PATCH 1/2] Allow yielding stats when problem resolution times out When a problem cannot return any solution because of a given time limit, allow to still yield stats without providing any valid model. --- clyngor/parsing.py | 6 ++++-- clyngor/solving.py | 2 ++ clyngor/test/test_api.py | 17 +++++++++++++++++ clyngor/test/test_parsing.py | 37 ++++++++++++++++++++++++++++++++++++ 4 files changed, 60 insertions(+), 2 deletions(-) diff --git a/clyngor/parsing.py b/clyngor/parsing.py index 3a35cbb..65b81a2 100644 --- a/clyngor/parsing.py +++ b/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 = {} diff --git a/clyngor/solving.py b/clyngor/solving.py index fb97ea5..4c61fa2 100644 --- a/clyngor/solving.py +++ b/clyngor/solving.py @@ -227,6 +227,8 @@ def _gen_answers(stdout:iter, stderr:iter, statistics:dict, statistics.update(payload) elif ptype == 'unsat': pass # don't care + elif ptype == 'unknown': + pass # don't care elif ptype == 'info': pass # don't care else: diff --git a/clyngor/test/test_api.py b/clyngor/test/test_api.py index 845ca12..10d9bbe 100644 --- a/clyngor/test/test_api.py +++ b/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 @@ -247,3 +248,19 @@ def test_unsatisfiable_statistics(): model = next(models, None) 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 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 model is None + assert len(models.statistics) > 5 diff --git a/clyngor/test/test_parsing.py b/clyngor/test/test_parsing.py index 7798213..e5c093f 100644 --- a/clyngor/test/test_parsing.py +++ b/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 From 8ffd7e3a96a7aa33b23b222a7701f24bf60ddc41 Mon Sep 17 00:00:00 2001 From: Diego Barreiro Date: Thu, 18 May 2023 15:43:51 +0200 Subject: [PATCH 2/2] Provide the result status when no answers can be found Allows developers to gather information on why a valid solution could not be provided. It allows to differentiate a timeout (UNKNOWN) from an actual irresoluble problem (UNSATISFIABLE). --- clyngor/answers.py | 11 ++++++++++- clyngor/solving.py | 14 ++++++++++---- clyngor/test/test_api.py | 18 ++++++++++++++++++ 3 files changed, 38 insertions(+), 5 deletions(-) diff --git a/clyngor/answers.py b/clyngor/answers.py index 9b71881..d860d04 100644 --- a/clyngor/answers.py +++ b/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. diff --git a/clyngor/solving.py b/clyngor/solving.py index 4c61fa2..b05983f 100644 --- a/clyngor/solving.py +++ b/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,9 +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': - pass # don't care + specific_statuses['unknown'] = True elif ptype == 'info': pass # don't care else: diff --git a/clyngor/test/test_api.py b/clyngor/test/test_api.py index 10d9bbe..5dcc49e 100644 --- a/clyngor/test/test_api.py +++ b/clyngor/test/test_api.py @@ -231,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 @@ -245,7 +249,11 @@ 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 @@ -253,7 +261,11 @@ def test_unsatisfiable_statistics(): 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 @@ -261,6 +273,12 @@ def test_unknown(): 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