Skip to content

Commit

Permalink
split get_assumptions into symbols and literals
Browse files Browse the repository at this point in the history
  • Loading branch information
hweichelt committed Jun 11, 2024
1 parent 2ede4df commit f161a94
Show file tree
Hide file tree
Showing 2 changed files with 14 additions and 5 deletions.
2 changes: 1 addition & 1 deletion src/clingexplaid/cli/clingo_app.py
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
17 changes: 13 additions & 4 deletions src/clingexplaid/transformers/transformer_assumption.py
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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}

0 comments on commit f161a94

Please sign in to comment.