From f161a9448c5140adddfd81f53ae9be6662fcd09d Mon Sep 17 00:00:00 2001 From: Hannes Weichelt Date: Tue, 11 Jun 2024 15:18:33 +0200 Subject: [PATCH] split get_assumptions into symbols and literals --- src/clingexplaid/cli/clingo_app.py | 2 +- .../transformers/transformer_assumption.py | 17 +++++++++++++---- 2 files changed, 14 insertions(+), 5 deletions(-) diff --git a/src/clingexplaid/cli/clingo_app.py b/src/clingexplaid/cli/clingo_app.py index faa48d0..63e94fd 100644 --- a/src/clingexplaid/cli/clingo_app.py +++ b/src/clingexplaid/cli/clingo_app.py @@ -173,7 +173,7 @@ def _method_mus( control.add("base", [], program_transformed) control.ground([("base", [])]) - assumptions = at.get_assumptions(control, constants=self.argument_constants) + assumptions = at.get_assumption_literals(control, constants=self.argument_constants) cc = CoreComputer(control, assumptions) max_models = int(control.configuration.solve.models) # type: ignore diff --git a/src/clingexplaid/transformers/transformer_assumption.py b/src/clingexplaid/transformers/transformer_assumption.py index 738364b..ab5790c 100644 --- a/src/clingexplaid/transformers/transformer_assumption.py +++ b/src/clingexplaid/transformers/transformer_assumption.py @@ -79,9 +79,11 @@ def parse_files(self, paths: Sequence[Union[str, Path]]) -> str: self.transformed = True return "\n".join(out) - def get_assumptions(self, control: clingo.Control, constants: Optional[Dict[str, str]] = None) -> Set[int]: + def get_assumption_symbols( + self, control: clingo.Control, constants: Optional[Dict[str, str]] = None + ) -> Set[clingo.Symbol]: """ - Returns the assumptions which were gathered during the transformation of the program. Has to be called after + Returns the assumption symbols which were gathered during the transformation of the program. Has to be called after a program has already been transformed. """ # Just taking the fact symbolic atoms of the control given doesn't work here since we anticipate that @@ -106,7 +108,14 @@ def get_assumptions(self, control: clingo.Control, constants: Optional[Dict[str, fact_control = clingo.Control(constant_strings) fact_control.add("base", [], "\n".join(self.fact_rules)) fact_control.ground([("base", [])]) - fact_symbols = [sym.symbol for sym in fact_control.symbolic_atoms if sym.is_fact] + fact_symbols = {sym.symbol for sym in fact_control.symbolic_atoms if sym.is_fact} + return fact_symbols + def get_assumption_literals(self, control: clingo.Control, constants: Optional[Dict[str, str]] = None) -> Set[int]: + """ + Returns the assumption literals which were gathered during the transformation of the program. Has to be called + after a program has already been transformed. + """ + assumption_symbols = self.get_assumption_symbols(control, constants) symbol_to_literal_lookup = {sym.symbol: sym.literal for sym in control.symbolic_atoms} - return {symbol_to_literal_lookup[sym] for sym in fact_symbols if sym in symbol_to_literal_lookup} + return {symbol_to_literal_lookup[sym] for sym in assumption_symbols if sym in symbol_to_literal_lookup}