diff --git a/src/renopro/asp/add-children.lp b/src/renopro/asp/add-children.lp new file mode 100644 index 0000000..e731337 --- /dev/null +++ b/src/renopro/asp/add-children.lp @@ -0,0 +1,236 @@ +% Add child relations for facts added via ast_operation add. + +ast_operation(add(child(unary_operation(X0),Child))) + :- ast_operation(add(unary_operation(X0,X1,Child))). + +ast_operation(add(child(binary_operation(X0),Child))) + :- ast_operation(add(binary_operation(X0,X1,Child,X3))). + +ast_operation(add(child(binary_operation(X0),Child))) + :- ast_operation(add(binary_operation(X0,X1,X2,Child))). + +ast_operation(add(child(interval(X0),Child))) + :- ast_operation(add(interval(X0,Child,X2))). + +ast_operation(add(child(interval(X0),Child))) + :- ast_operation(add(interval(X0,X1,Child))). + +ast_operation(add(child(terms(X0),Child))) + :- ast_operation(add(terms(X0,X1,Child))). + +ast_operation(add(child(function(X0),Child))) + :- ast_operation(add(function(X0,X1,Child))). + +ast_operation(add(child(external_function(X0),Child))) + :- ast_operation(add(external_function(X0,X1,Child))). + +ast_operation(add(child(pool(X0),Child))) + :- ast_operation(add(pool(X0,Child))). + +ast_operation(add(child(theory_terms(X0),Child))) + :- ast_operation(add(theory_terms(X0,X1,Child))). + +ast_operation(add(child(theory_sequence(X0),Child))) + :- ast_operation(add(theory_sequence(X0,X1,Child))). + +ast_operation(add(child(theory_function(X0),Child))) + :- ast_operation(add(theory_function(X0,X1,Child))). + +ast_operation(add(child(theory_unparsed_term_elements(X0),Child))) + :- ast_operation(add(theory_unparsed_term_elements(X0,X1,Child,X3))). + +ast_operation(add(child(theory_unparsed_term_elements(X0),Child))) + :- ast_operation(add(theory_unparsed_term_elements(X0,X1,X2,Child))). + +ast_operation(add(child(theory_unparsed_term(X0),Child))) + :- ast_operation(add(theory_unparsed_term(X0,Child))). + +ast_operation(add(child(guard(X0),Child))) + :- ast_operation(add(guard(X0,X1,Child))). + +ast_operation(add(child(guards(X0),Child))) + :- ast_operation(add(guards(X0,X1,Child))). + +ast_operation(add(child(comparison(X0),Child))) + :- ast_operation(add(comparison(X0,Child,X2))). + +ast_operation(add(child(comparison(X0),Child))) + :- ast_operation(add(comparison(X0,X1,Child))). + +ast_operation(add(child(symbolic_atom(X0),Child))) + :- ast_operation(add(symbolic_atom(X0,Child))). + +ast_operation(add(child(literal(X0),Child))) + :- ast_operation(add(literal(X0,X1,Child))). + +ast_operation(add(child(literals(X0),Child))) + :- ast_operation(add(literals(X0,X1,Child))). + +ast_operation(add(child(conditional_literal(X0),Child))) + :- ast_operation(add(conditional_literal(X0,Child,X2))). + +ast_operation(add(child(conditional_literal(X0),Child))) + :- ast_operation(add(conditional_literal(X0,X1,Child))). + +ast_operation(add(child(aggregate_elements(X0),Child))) + :- ast_operation(add(aggregate_elements(X0,X1,Child))). + +ast_operation(add(child(aggregate(X0),Child))) + :- ast_operation(add(aggregate(X0,Child,X2,X3))). + +ast_operation(add(child(aggregate(X0),Child))) + :- ast_operation(add(aggregate(X0,X1,Child,X3))). + +ast_operation(add(child(aggregate(X0),Child))) + :- ast_operation(add(aggregate(X0,X1,X2,Child))). + +ast_operation(add(child(theory_atom_elements(X0),Child))) + :- ast_operation(add(theory_atom_elements(X0,X1,Child,X3))). + +ast_operation(add(child(theory_atom_elements(X0),Child))) + :- ast_operation(add(theory_atom_elements(X0,X1,X2,Child))). + +ast_operation(add(child(theory_guard(X0),Child))) + :- ast_operation(add(theory_guard(X0,X1,Child))). + +ast_operation(add(child(theory_atom(X0),Child))) + :- ast_operation(add(theory_atom(X0,Child,X2,X3))). + +ast_operation(add(child(theory_atom(X0),Child))) + :- ast_operation(add(theory_atom(X0,X1,Child,X3))). + +ast_operation(add(child(theory_atom(X0),Child))) + :- ast_operation(add(theory_atom(X0,X1,X2,Child))). + +ast_operation(add(child(body_aggregate_elements(X0),Child))) + :- ast_operation(add(body_aggregate_elements(X0,X1,Child,X3))). + +ast_operation(add(child(body_aggregate_elements(X0),Child))) + :- ast_operation(add(body_aggregate_elements(X0,X1,X2,Child))). + +ast_operation(add(child(body_aggregate(X0),Child))) + :- ast_operation(add(body_aggregate(X0,Child,X2,X3,X4))). + +ast_operation(add(child(body_aggregate(X0),Child))) + :- ast_operation(add(body_aggregate(X0,X1,X2,Child,X4))). + +ast_operation(add(child(body_aggregate(X0),Child))) + :- ast_operation(add(body_aggregate(X0,X1,X2,X3,Child))). + +ast_operation(add(child(body_literal(X0),Child))) + :- ast_operation(add(body_literal(X0,X1,Child))). + +ast_operation(add(child(body_literals(X0),Child))) + :- ast_operation(add(body_literals(X0,X1,Child))). + +ast_operation(add(child(head_aggregate_elements(X0),Child))) + :- ast_operation(add(head_aggregate_elements(X0,X1,Child,X3))). + +ast_operation(add(child(head_aggregate_elements(X0),Child))) + :- ast_operation(add(head_aggregate_elements(X0,X1,X2,Child))). + +ast_operation(add(child(head_aggregate(X0),Child))) + :- ast_operation(add(head_aggregate(X0,Child,X2,X3,X4))). + +ast_operation(add(child(head_aggregate(X0),Child))) + :- ast_operation(add(head_aggregate(X0,X1,X2,Child,X4))). + +ast_operation(add(child(head_aggregate(X0),Child))) + :- ast_operation(add(head_aggregate(X0,X1,X2,X3,Child))). + +ast_operation(add(child(conditional_literals(X0),Child))) + :- ast_operation(add(conditional_literals(X0,X1,Child))). + +ast_operation(add(child(disjunction(X0),Child))) + :- ast_operation(add(disjunction(X0,Child))). + +ast_operation(add(child(rule(X0),Child))) + :- ast_operation(add(rule(X0,Child,X2))). + +ast_operation(add(child(rule(X0),Child))) + :- ast_operation(add(rule(X0,X1,Child))). + +ast_operation(add(child(definition(X0),Child))) + :- ast_operation(add(definition(X0,X1,Child,X3))). + +ast_operation(add(child(show_term(X0),Child))) + :- ast_operation(add(show_term(X0,Child,X2))). + +ast_operation(add(child(show_term(X0),Child))) + :- ast_operation(add(show_term(X0,X1,Child))). + +ast_operation(add(child(minimize(X0),Child))) + :- ast_operation(add(minimize(X0,Child,X2,X3,X4))). + +ast_operation(add(child(minimize(X0),Child))) + :- ast_operation(add(minimize(X0,X1,Child,X3,X4))). + +ast_operation(add(child(minimize(X0),Child))) + :- ast_operation(add(minimize(X0,X1,X2,Child,X4))). + +ast_operation(add(child(minimize(X0),Child))) + :- ast_operation(add(minimize(X0,X1,X2,X3,Child))). + +ast_operation(add(child(statements(X0),Child))) + :- ast_operation(add(statements(X0,X1,Child))). + +ast_operation(add(child(constants(X0),Child))) + :- ast_operation(add(constants(X0,X1,Child))). + +ast_operation(add(child(program(X0),Child))) + :- ast_operation(add(program(X0,X1,Child,X3))). + +ast_operation(add(child(program(X0),Child))) + :- ast_operation(add(program(X0,X1,X2,Child))). + +ast_operation(add(child(external(X0),Child))) + :- ast_operation(add(external(X0,Child,X2,X3))). + +ast_operation(add(child(external(X0),Child))) + :- ast_operation(add(external(X0,X1,Child,X3))). + +ast_operation(add(child(edge(X0),Child))) + :- ast_operation(add(edge(X0,Child,X2,X3))). + +ast_operation(add(child(edge(X0),Child))) + :- ast_operation(add(edge(X0,X1,Child,X3))). + +ast_operation(add(child(edge(X0),Child))) + :- ast_operation(add(edge(X0,X1,X2,Child))). + +ast_operation(add(child(heuristic(X0),Child))) + :- ast_operation(add(heuristic(X0,Child,X2,X3,X4,X5))). + +ast_operation(add(child(heuristic(X0),Child))) + :- ast_operation(add(heuristic(X0,X1,Child,X3,X4,X5))). + +ast_operation(add(child(heuristic(X0),Child))) + :- ast_operation(add(heuristic(X0,X1,X2,Child,X4,X5))). + +ast_operation(add(child(heuristic(X0),Child))) + :- ast_operation(add(heuristic(X0,X1,X2,X3,Child,X5))). + +ast_operation(add(child(heuristic(X0),Child))) + :- ast_operation(add(heuristic(X0,X1,X2,X3,X4,Child))). + +ast_operation(add(child(project_atom(X0),Child))) + :- ast_operation(add(project_atom(X0,Child,X2))). + +ast_operation(add(child(project_atom(X0),Child))) + :- ast_operation(add(project_atom(X0,X1,Child))). + +ast_operation(add(child(theory_term_definitions(X0),Child))) + :- ast_operation(add(theory_term_definitions(X0,X1,X2,Child))). + +ast_operation(add(child(theory_guard_definition(X0),Child))) + :- ast_operation(add(theory_guard_definition(X0,Child,X2))). + +ast_operation(add(child(theory_atom_definitions(X0),Child))) + :- ast_operation(add(theory_atom_definitions(X0,X1,X2,X3,X4,X5,Child))). + +ast_operation(add(child(theory_definition(X0),Child))) + :- ast_operation(add(theory_definition(X0,X1,Child,X3))). + +ast_operation(add(child(theory_definition(X0),Child))) + :- ast_operation(add(theory_definition(X0,X1,X2,Child))). + diff --git a/src/renopro/asp/decompose.lp b/src/renopro/asp/decompose.lp new file mode 100644 index 0000000..64d84c8 --- /dev/null +++ b/src/renopro/asp/decompose.lp @@ -0,0 +1,35 @@ +#script (python) + +from clingo.symbol import Function, Number, SymbolType, Symbol, List + +from renopro.predicates import pred_names, composed_pred_names + + +def _decompose(f: Symbol, top_id: Symbol, asts: List[Symbol], i: int, top_level=False, override_id=None): + current_id = override_id if override_id is not None else i + fresh_id = Function("_fresh", [top_id, Number(current_id)]) if not top_level else top_id.arguments[0] + i = i + 1 + current_id = i + ast_args = [fresh_id] if not top_level else [] + for arg in f.arguments: + if arg.type is SymbolType.Function and arg.name in composed_pred_names: + id_term, i = _decompose(arg, top_id, asts, i) + ast_args.append(id_term) + elif arg.type is SymbolType.Function and arg.name == "": + j = i + for element in arg.arguments: + id_term, i = _decompose(element, top_id, asts, i, override_id=j) + ast_args.append(id_term) + elif arg.type is SymbolType.Function and arg.name in pred_names and len(arg.arguments) == 1: + ast_args.append(arg) + else: + ast_args.append(arg) + asts.append(Function(f.name.rstrip("_"), ast_args)) + return Function(f.name.rstrip("_"), [fresh_id]), i + +def decompose(f: Symbol): + asts = [] + _decompose(f, Function(f.name, f.arguments[:1]), asts, 0, top_level=True) + return asts + +#end. diff --git a/src/renopro/asp/new_replace.lp b/src/renopro/asp/new_replace.lp new file mode 100644 index 0000000..f6ed13d --- /dev/null +++ b/src/renopro/asp/new_replace.lp @@ -0,0 +1 @@ +ast_operation(delete(A);add(A)) :- replace(A,B). diff --git a/src/renopro/asp/reachable.lp b/src/renopro/asp/reachable.lp new file mode 100644 index 0000000..748aebb --- /dev/null +++ b/src/renopro/asp/reachable.lp @@ -0,0 +1,13 @@ +reach(program(P,Name,Params,Stms)) :- transformed(program(P,Name,Params,Stms)). + +reach(child(ParentId,ChildId);ChildFact) + :- reach(ParentFact), transformed_ast_fact2id(ParentFact,ParentId), + transformed(child(ParentId,ChildId)), transformed_ast_fact2id(ChildFact,ChildId). + +final(R) :- reach(R). + +%% #show log("warning", "{}",reach(F)) : reach(F). +%% #show log("warning", "{}",transformed(F)) : transformed(F), transformed_ast_fact2id(F,Id). +%% #show log("warning", "{}",final(F)) : final(F). +%% #show log("warning", "{}",ast(F)) : ast(F). +%% #show log("warning", "{}",ast_operation(F)) : ast_operation(F). diff --git a/src/renopro/asp/transform.lp b/src/renopro/asp/transform.lp index 75abfb8..a8818af 100644 --- a/src/renopro/asp/transform.lp +++ b/src/renopro/asp/transform.lp @@ -1,50 +1,16 @@ #include "ast.lp". #include "defined.lp". #include "replace.lp". - -#script (python) - -from clingo.symbol import Function, Number, SymbolType, Symbol, List - -from renopro.predicates import pred_names, composed_pred_names - - -def _decompose(f: Symbol, top_id: Symbol, asts: List[Symbol], i: int, top_level=False, override_id=None): - current_id = override_id if override_id is not None else i - fresh_id = Function("_fresh", [top_id, Number(current_id)]) if not top_level else top_id.arguments[0] - i = i + 1 - current_id = i - ast_args = [fresh_id] if not top_level else [] - for arg in f.arguments: - if arg.type is SymbolType.Function and arg.name in composed_pred_names: - id_term, i = _decompose(arg, top_id, asts, i) - asts.append(Function("child", [Function(f.name.rstrip("_"), [fresh_id]), id_term])) - ast_args.append(id_term) - elif arg.type is SymbolType.Function and arg.name == "": - j = i - for element in arg.arguments: - id_term, i = _decompose(element, top_id, asts, i, override_id=j) - asts.append(Function("child", [Function(f.name.rstrip("_"), [fresh_id]), id_term])) - ast_args.append(id_term) - elif arg.type is SymbolType.Function and arg.name in pred_names and len(arg.arguments) == 1: - asts.append(Function("child", [Function(f.name.rstrip("_"), [fresh_id]), arg])) - ast_args.append(arg) - else: - ast_args.append(arg) - asts.append(Function(f.name.rstrip("_"), ast_args)) - return Function(f.name.rstrip("_"), [fresh_id]), i - -def decompose(f: Symbol): - asts = [] - _decompose(f, Function(f.name, f.arguments[:1]), asts, 0, top_level=True) - return asts - - #end. +#include "decompose.lp". +#include "add-children.lp". % delete stops inertia from old ast -final(A) :- ast(A), not ast_operation(delete(A)). +transformed(A) :- ast(A), not ast_operation(delete(A)). % and even overrides adding of new ast -final(A) :- ast_operation(add(A)), not ast_operation(delete(A)). +transformed(A) :- ast_operation(add(A)), not ast_operation(delete(A)). + +#include "transformed_ast_fact2id.lp". +#include "reachable.lp". #defined ast_operation/1. diff --git a/src/renopro/asp/transformed_ast_fact2id.lp b/src/renopro/asp/transformed_ast_fact2id.lp new file mode 100644 index 0000000..4cba998 --- /dev/null +++ b/src/renopro/asp/transformed_ast_fact2id.lp @@ -0,0 +1,60 @@ +% map ast facts to their identifiers. + +transformed_ast_fact2id(string(X0,X1),string(X0)) :- transformed(string(X0,X1)). +transformed_ast_fact2id(number(X0,X1),number(X0)) :- transformed(number(X0,X1)). +transformed_ast_fact2id(variable(X0,X1),variable(X0)) :- transformed(variable(X0,X1)). +transformed_ast_fact2id(unary_operation(X0,X1,X2),unary_operation(X0)) :- transformed(unary_operation(X0,X1,X2)). +transformed_ast_fact2id(binary_operation(X0,X1,X2,X3),binary_operation(X0)) :- transformed(binary_operation(X0,X1,X2,X3)). +transformed_ast_fact2id(interval(X0,X1,X2),interval(X0)) :- transformed(interval(X0,X1,X2)). +transformed_ast_fact2id(terms(X0,X1,X2),terms(X0)) :- transformed(terms(X0,X1,X2)). +transformed_ast_fact2id(function(X0,X1,X2),function(X0)) :- transformed(function(X0,X1,X2)). +transformed_ast_fact2id(external_function(X0,X1,X2),external_function(X0)) :- transformed(external_function(X0,X1,X2)). +transformed_ast_fact2id(pool(X0,X1),pool(X0)) :- transformed(pool(X0,X1)). +transformed_ast_fact2id(theory_terms(X0,X1,X2),theory_terms(X0)) :- transformed(theory_terms(X0,X1,X2)). +transformed_ast_fact2id(theory_sequence(X0,X1,X2),theory_sequence(X0)) :- transformed(theory_sequence(X0,X1,X2)). +transformed_ast_fact2id(theory_function(X0,X1,X2),theory_function(X0)) :- transformed(theory_function(X0,X1,X2)). +transformed_ast_fact2id(theory_operators(X0,X1,X2),theory_operators(X0)) :- transformed(theory_operators(X0,X1,X2)). +transformed_ast_fact2id(theory_unparsed_term_elements(X0,X1,X2,X3),theory_unparsed_term_elements(X0)) :- transformed(theory_unparsed_term_elements(X0,X1,X2,X3)). +transformed_ast_fact2id(theory_unparsed_term(X0,X1),theory_unparsed_term(X0)) :- transformed(theory_unparsed_term(X0,X1)). +transformed_ast_fact2id(guard(X0,X1,X2),guard(X0)) :- transformed(guard(X0,X1,X2)). +transformed_ast_fact2id(guards(X0,X1,X2),guards(X0)) :- transformed(guards(X0,X1,X2)). +transformed_ast_fact2id(comparison(X0,X1,X2),comparison(X0)) :- transformed(comparison(X0,X1,X2)). +transformed_ast_fact2id(boolean_constant(X0,X1),boolean_constant(X0)) :- transformed(boolean_constant(X0,X1)). +transformed_ast_fact2id(symbolic_atom(X0,X1),symbolic_atom(X0)) :- transformed(symbolic_atom(X0,X1)). +transformed_ast_fact2id(literal(X0,X1,X2),literal(X0)) :- transformed(literal(X0,X1,X2)). +transformed_ast_fact2id(literals(X0,X1,X2),literals(X0)) :- transformed(literals(X0,X1,X2)). +transformed_ast_fact2id(conditional_literal(X0,X1,X2),conditional_literal(X0)) :- transformed(conditional_literal(X0,X1,X2)). +transformed_ast_fact2id(aggregate_elements(X0,X1,X2),aggregate_elements(X0)) :- transformed(aggregate_elements(X0,X1,X2)). +transformed_ast_fact2id(aggregate(X0,X1,X2,X3),aggregate(X0)) :- transformed(aggregate(X0,X1,X2,X3)). +transformed_ast_fact2id(theory_atom_elements(X0,X1,X2,X3),theory_atom_elements(X0)) :- transformed(theory_atom_elements(X0,X1,X2,X3)). +transformed_ast_fact2id(theory_guard(X0,X1,X2),theory_guard(X0)) :- transformed(theory_guard(X0,X1,X2)). +transformed_ast_fact2id(theory_atom(X0,X1,X2,X3),theory_atom(X0)) :- transformed(theory_atom(X0,X1,X2,X3)). +transformed_ast_fact2id(body_aggregate_elements(X0,X1,X2,X3),body_aggregate_elements(X0)) :- transformed(body_aggregate_elements(X0,X1,X2,X3)). +transformed_ast_fact2id(body_aggregate(X0,X1,X2,X3,X4),body_aggregate(X0)) :- transformed(body_aggregate(X0,X1,X2,X3,X4)). +transformed_ast_fact2id(body_literal(X0,X1,X2),body_literal(X0)) :- transformed(body_literal(X0,X1,X2)). +transformed_ast_fact2id(body_literals(X0,X1,X2),body_literals(X0)) :- transformed(body_literals(X0,X1,X2)). +transformed_ast_fact2id(head_aggregate_elements(X0,X1,X2,X3),head_aggregate_elements(X0)) :- transformed(head_aggregate_elements(X0,X1,X2,X3)). +transformed_ast_fact2id(head_aggregate(X0,X1,X2,X3,X4),head_aggregate(X0)) :- transformed(head_aggregate(X0,X1,X2,X3,X4)). +transformed_ast_fact2id(conditional_literals(X0,X1,X2),conditional_literals(X0)) :- transformed(conditional_literals(X0,X1,X2)). +transformed_ast_fact2id(disjunction(X0,X1),disjunction(X0)) :- transformed(disjunction(X0,X1)). +transformed_ast_fact2id(rule(X0,X1,X2),rule(X0)) :- transformed(rule(X0,X1,X2)). +transformed_ast_fact2id(definition(X0,X1,X2,X3),definition(X0)) :- transformed(definition(X0,X1,X2,X3)). +transformed_ast_fact2id(show_signature(X0,X1,X2,X3),show_signature(X0)) :- transformed(show_signature(X0,X1,X2,X3)). +transformed_ast_fact2id(defined(X0,X1,X2,X3),defined(X0)) :- transformed(defined(X0,X1,X2,X3)). +transformed_ast_fact2id(show_term(X0,X1,X2),show_term(X0)) :- transformed(show_term(X0,X1,X2)). +transformed_ast_fact2id(minimize(X0,X1,X2,X3,X4),minimize(X0)) :- transformed(minimize(X0,X1,X2,X3,X4)). +transformed_ast_fact2id(script(X0,X1,X2),script(X0)) :- transformed(script(X0,X1,X2)). +transformed_ast_fact2id(statements(X0,X1,X2),statements(X0)) :- transformed(statements(X0,X1,X2)). +transformed_ast_fact2id(constants(X0,X1,X2),constants(X0)) :- transformed(constants(X0,X1,X2)). +transformed_ast_fact2id(program(X0,X1,X2,X3),program(X0)) :- transformed(program(X0,X1,X2,X3)). +transformed_ast_fact2id(external(X0,X1,X2,X3),external(X0)) :- transformed(external(X0,X1,X2,X3)). +transformed_ast_fact2id(edge(X0,X1,X2,X3),edge(X0)) :- transformed(edge(X0,X1,X2,X3)). +transformed_ast_fact2id(heuristic(X0,X1,X2,X3,X4,X5),heuristic(X0)) :- transformed(heuristic(X0,X1,X2,X3,X4,X5)). +transformed_ast_fact2id(project_atom(X0,X1,X2),project_atom(X0)) :- transformed(project_atom(X0,X1,X2)). +transformed_ast_fact2id(project_signature(X0,X1,X2,X3),project_signature(X0)) :- transformed(project_signature(X0,X1,X2,X3)). +transformed_ast_fact2id(theory_operator_definitions(X0,X1,X2,X3,X4),theory_operator_definitions(X0)) :- transformed(theory_operator_definitions(X0,X1,X2,X3,X4)). +transformed_ast_fact2id(theory_term_definitions(X0,X1,X2,X3),theory_term_definitions(X0)) :- transformed(theory_term_definitions(X0,X1,X2,X3)). +transformed_ast_fact2id(theory_guard_definition(X0,X1,X2),theory_guard_definition(X0)) :- transformed(theory_guard_definition(X0,X1,X2)). +transformed_ast_fact2id(theory_atom_definitions(X0,X1,X2,X3,X4,X5,X6),theory_atom_definitions(X0)) :- transformed(theory_atom_definitions(X0,X1,X2,X3,X4,X5,X6)). +transformed_ast_fact2id(theory_definition(X0,X1,X2,X3),theory_definition(X0)) :- transformed(theory_definition(X0,X1,X2,X3)). +transformed_ast_fact2id(location(Id,Begin,End),Id) :- transformed(location(Id,Begin,End)). diff --git a/src/renopro/utils/codegen.py b/src/renopro/utils/codegen.py index 3241b1c..8c8c0e4 100644 --- a/src/renopro/utils/codegen.py +++ b/src/renopro/utils/codegen.py @@ -44,6 +44,55 @@ def generate_replace(): Path("src", "renopro", "asp", "replace.lp").write_text(program) +def generate_add_child(): + """Generate rules to create child relations for all facts added + via ast_operation add, and rules to replace identifiers via + ast_operation replace.""" + add_child_program = "% Add child relations for facts added via ast_operation add.\n\n" + for predicate in preds.AstPreds: + if predicate is preds.Location or predicate is preds.Child: + continue + child_arg_indices = [] + name = predicate.meta.name + arity = predicate.meta.arity + for idx, key in enumerate(predicate.meta.keys()): + if key == "id": + continue + field = getattr(predicate, key).meta.field + # we only care about complex adn combined fields - these + # are the terms that identify a child predicate + if field.complex is not None or hasattr(field, "fields"): + child_arg_indices.append(idx) + for idx in child_arg_indices: + add_child_args = ",".join( + ["X" + str(i) if i != idx else "Child" for i in range(arity)] + ) + add_child_program += ( + f"ast_operation(add(child({name}(X0),Child)))\n :- " + f"ast_operation(add({name}({add_child_args}))).\n\n" + ) + Path("src", "renopro", "asp", "add-children.lp").write_text(add_child_program) + + +def generate_ast_fact2id(): + "Generate rules mapping AST facts to their identifiers" + program = "% map ast facts to their identifiers.\n\n" + for predicate in preds.AstPreds: + if predicate is preds.Location: + location = "location(Id,Begin,End)" + program += f"transformed_ast_fact2id({location},Id) :- transformed({location}).\n" + continue + if predicate is preds.Child: + continue + name = predicate.meta.name + arity = predicate.meta.arity + args = ",".join(["X" + str(i) for i in range(arity)]) + fact = f"{name}({args})" + identifier = f"{name}(X0)" + program += f"transformed_ast_fact2id({fact},{identifier}) :- transformed({fact}).\n" + Path("src", "renopro", "asp", "transformed_ast_fact2id.lp").write_text(program) + + def generate_ast(): "Generate rules to tag AST facts." program = "% Rules to tag AST facts.\n\n" @@ -70,5 +119,7 @@ def generate_defined(): if __name__ == "__main__": generate_replace() + generate_add_child() generate_ast() generate_defined() + generate_ast_fact2id() diff --git a/tests/asp/transform/meta-telingo/inputs/telingo-input-bad-term.lp b/tests/asp/transform/meta-telingo/inputs/telingo-input-bad-term.lp index f1f9676..77232f9 100644 --- a/tests/asp/transform/meta-telingo/inputs/telingo-input-bad-term.lp +++ b/tests/asp/transform/meta-telingo/inputs/telingo-input-bad-term.lp @@ -1,3 +1,4 @@ &tel{ 1 }. &tel{ > a, b }. -&tel{ a : b }. +&tel{ >? (a, b) }. +:- &tel{ < a: b, c; < d: e }. diff --git a/tests/asp/transform/meta-telingo/outputs/output-body.lp b/tests/asp/transform/meta-telingo/outputs/output-body.lp index 3f40a23..1b77956 100644 --- a/tests/asp/transform/meta-telingo/outputs/output-body.lp +++ b/tests/asp/transform/meta-telingo/outputs/output-body.lp @@ -1,12 +1,3 @@ -#external initial. [false] -#external final. [false] -#external initial. [false] -#external prev(prev(b)). [false] -#external until(c,prev(d)). [false] -#external until(b(X),next(c((X+Y)))) : e(X); d(Y). [false] -#external next(d(Y)) : e(X); d(Y). [false] -#external prev(h(Y)) : i(X); h(Y). [false] -#external next(wprev(k(X))). [false] #program base. a :- initial. #program base. @@ -19,3 +10,12 @@ j(X) :- next(wprev(k(X))). #program base. #false :- final; n. #program base. +#external final. [false] +#external next(wprev(k(X))). [false] +#external until(c,prev(d)). [false] +#external prev(prev(b)). [false] +#external initial. [false] +#external initial. [false] +#external until(b(X),next(c((X+Y)))) : e(X); d(Y). [false] +#external next(d(Y)) : e(X); d(Y). [false] +#external prev(h(Y)) : i(X); h(Y). [false] diff --git a/tests/asp/transform/meta-telingo/outputs/output-head.lp b/tests/asp/transform/meta-telingo/outputs/output-head.lp index 81336d3..1fa92bc 100644 --- a/tests/asp/transform/meta-telingo/outputs/output-head.lp +++ b/tests/asp/transform/meta-telingo/outputs/output-head.lp @@ -1,16 +1,16 @@ +#program base. +a :- initial; b. +until(c,prev(d)) :- a. +release(b(X),next(c((X+Y)))): wnext(d(Y)) :- e(X). +3 < #max { 1: next(j(X)): prev(h(Y)) } :- i(X). +prev(wprev(k(X))) :- j(X). +#program base. #external c : a. [false] #external b(X) : e(X). [false] #external j(X) : i(X); h(Y). [false] -#external k(X) : j(X). [false] #external c((X+Y)) : e(X). [false] #external d : a. [false] +#external k(X) : j(X). [false] #external initial. [false] #external wnext(d(Y)) : e(X). [false] #external prev(h(Y)) : i(X); h(Y). [false] -#program base. -a :- initial; b. -until(c,prev(d)) :- a. -release(b(X),next(c((X+Y)))): wnext(d(Y)) :- e(X). -3 < #max { 1: next(j(X)): prev(h(Y)) } :- i(X). -prev(wprev(k(X))) :- j(X). -#program base. diff --git a/tests/asp/transform/meta-telingo/outputs/telingo-output.lp b/tests/asp/transform/meta-telingo/outputs/telingo-output.lp new file mode 100644 index 0000000..158af31 --- /dev/null +++ b/tests/asp/transform/meta-telingo/outputs/telingo-output.lp @@ -0,0 +1,36 @@ +#theory tel { + formula { + < : 5, unary; + <: : 5, unary; + : 5, unary; + >: : 5, unary; + >? : 5, unary; + >* : 5, unary; + >* : 4, binary, left; + >? : 4, binary, left; + <* : 4, binary, left; + 1. + #count{ P: theory_atom_elements(E,P,_,_) } > 1. ast_operation( replace(body_literal(BL),conditional_literal((A,1))); @@ -83,7 +81,20 @@ ast_operation( body_literal(BL,Sign,theory_atom(A)), tel_theory_atom(A,_), theory_atom(A,_,theory_atom_elements(E),_), theory_atom_elements(E,_,theory_terms(TS),literals(LS)), - theory_terms(TS,0,RootTerm), tel_root_term_id(RootTerm,F). + theory_terms(TS,0,RootTerm), tel_root_term_id(RootTerm,F), + literals(LS,_,_). + +ast_operation( + delete(body_literal(BL,Sign,theory_atom(A))); + add(body_literal(BL,Sign,symbolic_atom((A,1))); + symbolic_atom((A,1),function(F))) +) + :- body_literals(BLS,P,body_literal(BL)), + body_literal(BL,Sign,theory_atom(A)), tel_theory_atom(A,_), + theory_atom(A,_,theory_atom_elements(E),_), + theory_atom_elements(E,_,theory_terms(TS),literals(LS)), + theory_terms(TS,0,RootTerm), tel_root_term_id(RootTerm,F), + not literals(LS,_,_). ast_operation( replace(theory_atom(A),disjunction((A,1))); diff --git a/tests/asp/transform/not_bad/transform.lp b/tests/asp/transform/not_bad/transform.lp index 97601c7..a2bc85e 100644 --- a/tests/asp/transform/not_bad/transform.lp +++ b/tests/asp/transform/not_bad/transform.lp @@ -20,10 +20,10 @@ max_lit_index(LT,Idx) %% the transformation itself ast_operation( -add((body_literals(LT,N+1,body_literal(new_id(LT,0))); - body_literal(new_id(LT,0),"not",symbolic_atom(new_id(LT,1))); - symbolic_atom(new_id(LT,1),function(new_id(LT,2))); - function(new_id(LT,2),bad,Fargs)))) + add((body_literals(LT,N+1,body_literal(new_id(LT,0))); + body_literal(new_id(LT,0),"not",symbolic_atom(new_id(LT,1))); + symbolic_atom(new_id(LT,1),function(new_id(LT,2))); + function(new_id(LT,2),bad,Fargs)))) :- rule(_,literal(L),body_literals(LT)), literal(L,"pos",symbolic_atom(A)), symbolic_atom(A,function(F)), diff --git a/tests/asp/transform/theory-parsing/inputs/clingo-theory-term-reified.lp b/tests/asp/transform/theory-parsing/inputs/clingo-theory-term-reified.lp index 2ab90aa..42446de 100644 --- a/tests/asp/transform/theory-parsing/inputs/clingo-theory-term-reified.lp +++ b/tests/asp/transform/theory-parsing/inputs/clingo-theory-term-reified.lp @@ -1,14 +1,52 @@ +location(program(0),position("-",1,1),position("-",1,1)). +location(program(3),position("-",1,1),position("-",1,15)). +location(rule(6),position("-",2,1),position("-",2,21)). +location(theory_atom(7),position("-",2,2),position("-",2,6)). +location(function(8),position("-",2,2),position("-",2,6)). +location(theory_unparsed_term(12),position("-",2,9),position("-",2,18)). +location(theory_sequence(15),position("-",2,10),position("-",2,18)). +location(theory_unparsed_term(17),position("-",2,11),position("-",2,15)). +location(number(20),position("-",2,13),position("-",2,14)). +location(number(21),position("-",2,16),position("-",2,17)). +child(program(0),constants(1)). +child(program(0),statements(2)). +child(statements(2),program(3)). +child(program(3),constants(4)). +child(program(3),statements(5)). +child(statements(5),rule(6)). +child(rule(6),theory_atom(7)). +child(theory_atom(7),function(8)). +child(function(8),terms(9)). +child(theory_atom(7),theory_atom_elements(10)). +child(theory_atom_elements(10),theory_terms(11)). +child(theory_terms(11),theory_unparsed_term(12)). +child(theory_unparsed_term(12),theory_unparsed_term_elements(13)). +child(theory_unparsed_term_elements(13),theory_operators(14)). +child(theory_unparsed_term_elements(13),theory_sequence(15)). +child(theory_sequence(15),theory_terms(16)). +child(theory_terms(16),theory_unparsed_term(17)). +child(theory_unparsed_term(17),theory_unparsed_term_elements(18)). +child(theory_unparsed_term_elements(18),theory_operators(19)). +child(theory_unparsed_term_elements(18),number(20)). +child(theory_terms(16),number(21)). +child(theory_atom_elements(10),literals(22)). +child(rule(6),body_literals(24)). program(0,"base",constants(1),statements(2)). -function(5,eval,terms(6)). -number(13,1). -number(14,2). -theory_terms(12,0,number(13)). -theory_terms(10,0,theory_function(11)). -theory_terms(10,1,number(14)). -theory_terms(8,0,theory_function(9)). -theory_function(11,"-",theory_terms(12)). -theory_function(9,"+",theory_terms(10)). -theory_atom_elements(7,0,theory_terms(8),literals(15)). -theory_atom(4,function(5),theory_atom_elements(7),theory_guard(16)). -rule(3,theory_atom(4),body_literals(17)). -statements(2,0,rule(3)). +program(3,"base",constants(4),statements(5)). +function(8,eval,terms(9)). +theory_operators(14,0,"+"). +theory_operators(19,0,"-"). +number(20,1). +number(21,2). +theory_unparsed_term_elements(18,0,theory_operators(19),number(20)). +theory_unparsed_term_elements(13,0,theory_operators(14),theory_sequence(15)). +theory_unparsed_term(17,theory_unparsed_term_elements(18)). +theory_unparsed_term(12,theory_unparsed_term_elements(13)). +theory_terms(16,0,theory_unparsed_term(17)). +theory_terms(16,1,number(21)). +theory_terms(11,0,theory_unparsed_term(12)). +theory_sequence(15,"()",theory_terms(16)). +theory_atom_elements(10,0,theory_terms(11),literals(22)). +theory_atom(7,function(8),theory_atom_elements(10),theory_guard(23)). +rule(6,theory_atom(7),body_literals(24)). +statements(5,0,rule(6)). diff --git a/tests/asp/transform/theory-parsing/inputs/clingo-theory-term.lp b/tests/asp/transform/theory-parsing/inputs/clingo-theory-term.lp new file mode 100644 index 0000000..de618d3 --- /dev/null +++ b/tests/asp/transform/theory-parsing/inputs/clingo-theory-term.lp @@ -0,0 +1,2 @@ +#program base. +&eval { (+ ((- 1),2)) }. diff --git a/tests/test_transform.py b/tests/test_transform.py index b20efd2..1f2abd6 100644 --- a/tests/test_transform.py +++ b/tests/test_transform.py @@ -3,6 +3,7 @@ from itertools import count from pathlib import Path from typing import Dict, List, Literal, Optional +import unittest from unittest import TestCase import renopro.predicates as preds @@ -20,7 +21,7 @@ def setUp(self): # auto-generates the expected integers preds.id_count = count() - def assertTrasformEqual( + def assertTransformEqual( self, input_files: List[Path], meta: List[List[Path]], @@ -144,7 +145,7 @@ def test_transform_not_bad(self): that it's not bad. """ files_dir = test_transform_dir / "not_bad" - self.assertTrasformEqual( + self.assertTransformEqual( [files_dir / "input.lp"], [[files_dir / "transform.lp"]], files_dir / "output.lp", @@ -156,7 +157,7 @@ def test_transform_add_time(self): files_dir = test_transform_dir / "prev_to_timepoints" for testname in ["sad", "very_sad", "constant"]: with self.subTest(testname=testname): - self.assertTrasformEqual( + self.assertTransformEqual( [files_dir / (testname + "_input.lp")], [[files_dir / "transform.lp"]], files_dir / (testname + "_output.lp"), @@ -191,7 +192,7 @@ def test_parse_unparsed_theory_terms_clingo(self): (using provided operator table) are parsed correctly. """ - self.assertTrasformEqual( + self.assertTransformEqual( [self.files_dir / "inputs" / "clingo-unparsed-theory-term.lp"], [[ self.files_dir / "parse-unparsed-theory-terms.lp", @@ -201,25 +202,9 @@ def test_parse_unparsed_theory_terms_clingo(self): ) def test_parse_theory_terms_clingo(self): - """Test that theory terms with clingo operators - (using provided operator table) are parsed correctly. + """Test that undefined operators are detected correctly. """ - rast1 = ReifiedAST() - rast1.add_reified_files( - [self.files_dir / "inputs" / "clingo-theory-term-reified.lp"] - ) - rast1.transform( - meta_files=[ - self.files_dir / "parse-theory-terms.lp", - self.files_dir / "inputs" / "clingo-operator-table.lp", - ] - ) - rast2 = ReifiedAST() - rast2.add_reified_files( - [self.files_dir / "inputs" / "clingo-theory-term-reified.lp"] - ) - self.assertSetEqual(rast1.reified_facts, rast2.reified_facts) rast3 = ReifiedAST() rast3.add_reified_files( [self.files_dir / "inputs" / "clingo-theory-term-unknown-reified.lp"] @@ -240,9 +225,10 @@ def test_parse_theory_terms_clingo(self): self.files_dir / "inputs" / "clingo-operator-table.lp", ] ) + def test_parse_telingo(self): """Test that parsing of telingo theory terms works correctly.""" - self.assertTrasformEqual( + self.assertTransformEqual( [self.files_dir / "inputs" / "telingo-unparsed-term.lp", self.files_dir / "inputs" / "telingo-theory-def.lp"], [[ @@ -277,7 +263,7 @@ class TestTransformMetaTelingo(TestTransform): def test_transform_meta_telingo_externals_body(self): """Test emission of external statements to protect temporal operators in the body.""" - self.assertTrasformEqual( + self.assertTransformEqual( [self.files_dir / "inputs" / "input-body.lp"], [[self.files_dir / "transform-subprogram.lp"], [self.files_dir / "transform-add-externals.lp"]], @@ -287,22 +273,39 @@ def test_transform_meta_telingo_externals_body(self): def test_transform_meta_telingo_externals_head(self): """Test emission of external statements to protect temporal operators in the head.""" - self.assertTrasformEqual( + self.assertTransformEqual( [self.files_dir / "inputs" / "input-head.lp"], [[self.files_dir / "transform-subprogram.lp"], [self.files_dir / "transform-add-externals.lp"]], self.files_dir / "outputs" / "output-head.lp" ) - # def test_transform_meta_telingo_theory_validation(self): - # """Test validation of theory terms in telingo theory atom elements.""" - # self.assertTransformLogs( - # [self.files_dir / "inputs" / "telingo-input-bad-term.lp", - # test_transform_dir / "theory-parsing" / "inputs" / "telingo-theory-def.lp"], - # [[test_transform_dir / "theory-parsing" / "parse-theory-terms.lp"], - # [self.files_dir / "transform-theory-to-symbolic.lp"]], - # "ERROR", - # [{}, - # {r":1:2-5: The term tuple of tel theory atom elements must contain a single temporal formula.": 1, - # r":2:2-5: The term tuple of tel theory atom elements must contain a single temporal formula.": 1, - # r":3:2-5: The term tuple of tel theory atom elements must contain a single temporal formula.": 1}]) + def test_transform_meta_telingo_theory_validation(self): + """Test validation of theory terms in telingo theory atom elements.""" + self.assertTransformLogs( + [self.files_dir / "inputs" / "telingo-input-bad-term.lp", + test_transform_dir / "theory-parsing" / "inputs" / "telingo-theory-def.lp"], + [[test_transform_dir / "theory-parsing" / "parse-theory-terms.lp"], + [self.files_dir / "transform-theory-to-symbolic.lp"]], + "ERROR", + [{}, + {r":1:2-5: The term tuple of tel theory atom elements must contain a single \(temporal\) formula.": 1, + r":2:2-5: The term tuple of tel theory atom elements must contain a single \(temporal\) formula.": 1, + r":3:10-16: Theory sequences not allowed in tel theory atoms, found sequence type \(\).": 1, + r":4:5-8: tel theory atoms occurring in the body may only have one element.": 1}]) + + def test_transform_meta_telingo_theory_to_symbol(self): + """Test transformation of temporal formulas in theory format to symbolic.""" + self.assertTransformEqual( + [self.files_dir / "inputs" / "telingo-input.lp", + test_transform_dir / "theory-parsing" / "inputs" / "telingo-theory-def.lp"], + [[test_transform_dir / "theory-parsing" / "parse-theory-terms.lp"], + [self.files_dir / "transform-theory-to-symbolic.lp"], + [self.files_dir / "transform-subprogram.lp"], + [self.files_dir / "transform-add-externals.lp"]], + self.files_dir / "outputs" / "telingo-output.lp" + ) + + +if __name__ == "__main__": + unittest.main() diff --git a/tmp.lp b/tmp.lp new file mode 100644 index 0000000..2c752d2 --- /dev/null +++ b/tmp.lp @@ -0,0 +1,38 @@ +#program base. +#program base. +#theory tel { + formula { + < : 5, unary; + <: : 5, unary; + : 5, unary; + >: : 5, unary; + >? : 5, unary; + >* : 5, unary; + >* : 4, binary, left; + >? : 4, binary, left; + <* : 4, binary, left; +