Skip to content

Commit

Permalink
add conflict free variable support to recursion
Browse files Browse the repository at this point in the history
  • Loading branch information
stephanzwicknagl committed Apr 7, 2023
1 parent 33ab300 commit 28e31e5
Show file tree
Hide file tree
Showing 3 changed files with 32 additions and 10 deletions.
15 changes: 12 additions & 3 deletions backend/src/viasp/asp/justify.py
Original file line number Diff line number Diff line change
Expand Up @@ -79,7 +79,11 @@ def collect_h_symbols_and_create_nodes(h_symbols: Collection[Symbol], relevant_i
def make_reason_path_from_facts_to_stable_model(wrapped_stable_model,
rule_mapping: Dict[int, Union[AST, str]],
fact_node: Node, h_syms,
recursive_transformations:frozenset, h="h", pad=True) \
recursive_transformations:frozenset,
h="h",
get_conflict_free_model: callable = lambda s: "model",
get_conflict_free_iterindex: callable = lambda s: "n",
pad=True) \
-> nx.DiGraph:
h_syms = collect_h_symbols_and_create_nodes(h_syms, rule_mapping.keys(), pad)
h_syms.sort(key=lambda node: node.rule_nr)
Expand All @@ -98,7 +102,12 @@ def make_reason_path_from_facts_to_stable_model(wrapped_stable_model,

for a, b in pairwise(h_syms):
if rule_mapping[b.rule_nr].rules in recursive_transformations:
b.recursive = get_recursion_subgraph(a.atoms, b.diff, rule_mapping[b.rule_nr], h)
b.recursive = get_recursion_subgraph(a.atoms,
b.diff,
rule_mapping[b.rule_nr],
h,
get_conflict_free_model,
get_conflict_free_iterindex)
g.add_edge(a, b, transformation=rule_mapping[b.rule_nr])

return g
Expand Down Expand Up @@ -144,7 +153,7 @@ def build_graph(wrapped_stable_models: Collection[str], transformed_prg: Collect
for model in wrapped_stable_models:
h_symbols = get_h_symbols_from_model(model, transformed_prg, facts, analyzer.get_constants(),
conflict_free_h)
new_path = make_reason_path_from_facts_to_stable_model(model, mapping, fact_node, h_symbols, recursion_transformations, conflict_free_h)
new_path = make_reason_path_from_facts_to_stable_model(model, mapping, fact_node, h_symbols, recursion_transformations, conflict_free_h, analyzer.get_conflict_free_model, analyzer.get_conflict_free_iterindex)
paths.append(new_path)

result_graph = identify_reasons(join_paths_with_facts(paths))
Expand Down
20 changes: 13 additions & 7 deletions backend/src/viasp/asp/recursion.py
Original file line number Diff line number Diff line change
Expand Up @@ -19,13 +19,14 @@ def __init__(self, **kwargs):
self.program = kwargs.pop("program", "")
self.register_h_symbols = kwargs.pop("callback", None)
self.conflict_free_h = kwargs.pop("conflict_free_h", "h")
self.conflict_free_n = kwargs.pop("conflict_free_n", "n")

def new(self):
return self.atoms

def main(self):
control = Control()
control.add("iter", ["n"], self.program)
control.add("iter", [f"{self.conflict_free_n}"], self.program)
self.atoms = self.init

step = 1
Expand All @@ -42,7 +43,9 @@ def main(self):


def get_recursion_subgraph(facts: frozenset, supernode_symbols: frozenset,
transformation: Union[AST, str], conflict_free_h: str):
transformation: Union[AST, str], conflict_free_h: str,
get_conflict_free_model: callable = lambda s: "model",
get_conflict_free_iterindex: callable = lambda s: "n") -> nx.DiGraph:
"""
Get a recursion explanation for the given facts and the recursive transformation.
Generate graph from explanation, sorted by the iteration step number.
Expand All @@ -55,22 +58,25 @@ def get_recursion_subgraph(facts: frozenset, supernode_symbols: frozenset,
enable_python()
init = [fact.symbol for fact in facts]
justification_program = ""
model_str:str = get_conflict_free_model()
n_str:str = get_conflict_free_iterindex()
for i,rule in enumerate(transformation.rules):
tupleified = ",".join(list(map(str,rule.body)))
justification_head = f"{conflict_free_h}({i+1}, {rule.head}, ({tupleified}), n)"
justification_body = ",".join(f"model({atom})" for atom in rule.body)
justification_body += f", not model({rule.head})"
justification_head = f"{conflict_free_h}({i+1}, {rule.head}, ({tupleified}), {n_str})"
justification_body = ",".join(f"{model_str}({atom})" for atom in rule.body)
justification_body += f", not {model_str}({rule.head})"

justification_program += f"{justification_head} :- {justification_body}.\n"

justification_program += "model(@new())."
justification_program += f"{model_str}(@new())."

h_syms = set()
try:
RecursionReasoner(init = init,
program = justification_program,
callback = h_syms.add,
conflict_free_h = conflict_free_h).main()
conflict_free_h = conflict_free_h,
conflict_free_n = n_str).main()
except RuntimeError:
return False

Expand Down
7 changes: 7 additions & 0 deletions backend/src/viasp/asp/reify.py
Original file line number Diff line number Diff line change
Expand Up @@ -222,6 +222,13 @@ def get_conflict_free_variable(self):
self.names = self.names.union({new_var})
return new_var

def get_conflict_free_iterindex(self):
"""
For use in generation of subgraphs at recursive
transformations.
"""
return self._get_conflict_free_version_of_name("n")

def get_facts(self):
return extract_symbols(self.facts, self.constants)

Expand Down

0 comments on commit 28e31e5

Please sign in to comment.