Skip to content

Commit

Permalink
Wip. reachability check.
Browse files Browse the repository at this point in the history
  • Loading branch information
namcsi committed Jan 28, 2024
1 parent 21db1d7 commit f2fb30c
Show file tree
Hide file tree
Showing 17 changed files with 617 additions and 126 deletions.
236 changes: 236 additions & 0 deletions src/renopro/asp/add-children.lp
Original file line number Diff line number Diff line change
@@ -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))).

35 changes: 35 additions & 0 deletions src/renopro/asp/decompose.lp
Original file line number Diff line number Diff line change
@@ -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.
1 change: 1 addition & 0 deletions src/renopro/asp/new_replace.lp
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
ast_operation(delete(A);add(A)) :- replace(A,B).
13 changes: 13 additions & 0 deletions src/renopro/asp/reachable.lp
Original file line number Diff line number Diff line change
@@ -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).
48 changes: 7 additions & 41 deletions src/renopro/asp/transform.lp
Original file line number Diff line number Diff line change
@@ -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.

Expand Down
Loading

0 comments on commit f2fb30c

Please sign in to comment.