diff --git a/src/renopro/predicates.py b/src/renopro/predicates.py index 7ddab65..a157853 100644 --- a/src/renopro/predicates.py +++ b/src/renopro/predicates.py @@ -226,7 +226,7 @@ class Terms(AstPredicate): """ id = IntegerOrRawField - position = IntegerField + position = IntegerOrRawField term = TermField @@ -306,7 +306,7 @@ class TheoryTerms(AstPredicate): """ id = IntegerOrRawField - position = IntegerField + position = IntegerOrRawField theory_term = TheoryTermField @@ -346,7 +346,7 @@ class TheoryOperators(AstPredicate): """ id = IntegerOrRawField - position = IntegerField + position = IntegerOrRawField operator = StringField @@ -361,7 +361,7 @@ class TheoryUnparsedTermElements(AstPredicate): """ id = IntegerOrRawField - position = IntegerField + position = IntegerOrRawField operators = TheoryOperators.unary.Field term = TheoryTermField @@ -414,7 +414,7 @@ class Guards(AstPredicate): """ id = IntegerOrRawField - position = IntegerField + position = IntegerOrRawField guard = Guard.unary.Field @@ -497,7 +497,7 @@ class Literals(AstPredicate): """ id = IntegerOrRawField - position = IntegerField + position = IntegerOrRawField literal = Literal.unary.Field @@ -523,7 +523,7 @@ class AggregateElements(AstPredicate): """ id = IntegerOrRawField - position = IntegerField + position = IntegerOrRawField element = ConditionalLiteral.unary.Field @@ -558,7 +558,7 @@ class TheoryAtomElements(AstPredicate): """ id = IntegerOrRawField - position = IntegerField + position = IntegerOrRawField terms = TheoryTerms.unary.Field condition = Literals.unary.Field @@ -604,7 +604,7 @@ class BodyAggregateElements(AstPredicate): """ id = IntegerOrRawField - position = IntegerField + position = IntegerOrRawField terms = Terms.unary.Field condition = Literals.unary.Field @@ -669,7 +669,7 @@ class BodyLiterals(AstPredicate): """ id = IntegerOrRawField - position = IntegerField + position = IntegerOrRawField body_literal = BodyLiteralField @@ -685,7 +685,7 @@ class HeadAggregateElements(AstPredicate): """ id = IntegerOrRawField - position = IntegerField + position = IntegerOrRawField terms = Terms.unary.Field condition = ConditionalLiteral.unary.Field @@ -717,7 +717,7 @@ class ConditionalLiterals(AstPredicate): """ id = IntegerOrRawField - position = IntegerField + position = IntegerOrRawField conditional_literal = ConditionalLiteral.unary.Field @@ -869,7 +869,7 @@ class Statements(AstPredicate): """ id = IntegerOrRawField - position = IntegerField + position = IntegerOrRawField statement = StatementField @@ -882,7 +882,7 @@ class Constants(AstPredicate): """ id = IntegerOrRawField - position = IntegerField + position = IntegerOrRawField constant = Function.unary.Field @@ -1002,7 +1002,7 @@ class TheoryOperatorDefinitions(AstPredicate): operator type: The type of the operator.""" id = IntegerOrRawField - position = IntegerField + position = IntegerOrRawField name = StringField priority = IntegerField operator_type = TheoryOperatorTypeField @@ -1017,7 +1017,7 @@ class TheoryTermDefinitions(AstPredicate): operators: The theory operators defined over the theory term.""" id = IntegerOrRawField - position = IntegerField + position = IntegerOrRawField name = ConstantField operators = TheoryOperatorDefinitions.unary.Field @@ -1049,7 +1049,7 @@ class TheoryAtomDefinitions(AstPredicate): """ id = IntegerOrRawField - position = IntegerField + position = IntegerOrRawField atom_type = TheoryAtomTypeField name = ConstantField arity = IntegerField diff --git a/src/renopro/rast.py b/src/renopro/rast.py index 4901aba..7f471e3 100644 --- a/src/renopro/rast.py +++ b/src/renopro/rast.py @@ -629,18 +629,16 @@ def _get_children( raise ChildQueryError(base_msg + msg) # pylint: disable=consider-using-in if expected_children_num == "*" or expected_children_num == "+": - query = query.order_by(child_ast_pred.position) child_facts = list(query.all()) + child_facts.sort(key=lambda fact: fact.position) num_child_facts = len(child_facts) - # log if there are no tuple elements in the same position - # while this is allowed, in case the user doesn't care about - # the ordering, we record this in case it was not intentional + # tuple elements in the same position are not allowed. if num_child_facts != len(set(tup.position for tup in child_facts)): msg = ( "Found multiple child facts in the same position for " f"identifier '{child_id_fact}'." ) - logger.debug(msg) + raise ChildrenQueryError(base_msg + msg) if expected_children_num == "+" and num_child_facts == 0: msg = ( f"Expected 1 or more child facts for identifier " diff --git a/tests/asp/transform/meta-telingo/outputs/output-body.lp b/tests/asp/transform/meta-telingo/outputs/output-body.lp index f320910..15dd601 100644 --- a/tests/asp/transform/meta-telingo/outputs/output-body.lp +++ b/tests/asp/transform/meta-telingo/outputs/output-body.lp @@ -3,19 +3,19 @@ a :- initial. #program base. l :- not initial; m. #program base. +#false :- final; n. +#program base. e :- prev(prev(b)); until(c,prev(d)). a(X) :- until(b(X),next(c((X+Y)))): next(d(Y)); e(X). f(X) :- 3 < #sum { 1: prev(h(Y)) }; i(X). j(X) :- next(wprev(k(X))). #program base. -#false :- final; n. -#program base. -#external prev(h(Y)) : h(Y); i(X). [false] -#external next(d(Y)) : d(Y); e(X). [false] -#external until(b(X),next(c((X+Y)))) : d(Y); e(X). [false] #external initial. [false] #external initial. [false] +#external final. [false] #external prev(prev(b)). [false] #external until(c,prev(d)). [false] +#external until(b(X),next(c((X+Y)))) : d(Y); e(X). [false] +#external next(d(Y)) : d(Y); e(X). [false] +#external prev(h(Y)) : h(Y); i(X). [false] #external next(wprev(k(X))). [false] -#external final. [false] diff --git a/tests/asp/transform/meta-telingo/outputs/output-head.lp b/tests/asp/transform/meta-telingo/outputs/output-head.lp index 0bc3ba1..c02f9ee 100644 --- a/tests/asp/transform/meta-telingo/outputs/output-head.lp +++ b/tests/asp/transform/meta-telingo/outputs/output-head.lp @@ -5,12 +5,12 @@ 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 prev(h(Y)) : h(Y); i(X). [false] -#external wnext(d(Y)) : e(X). [false] #external initial. [false] -#external k(X) : j(X). [false] +#external wnext(d(Y)) : e(X). [false] +#external prev(h(Y)) : h(Y); i(X). [false] +#external c : a. [false] #external d : a. [false] +#external b(X) : e(X). [false] #external c((X+Y)) : e(X). [false] #external j(X) : h(Y); i(X). [false] -#external b(X) : e(X). [false] -#external c : a. [false] +#external k(X) : j(X). [false] diff --git a/tests/asp/transform/meta-telingo/outputs/telingo-output.lp b/tests/asp/transform/meta-telingo/outputs/telingo-output.lp index 5eba9c0..716ac6c 100644 --- a/tests/asp/transform/meta-telingo/outputs/telingo-output.lp +++ b/tests/asp/transform/meta-telingo/outputs/telingo-output.lp @@ -26,11 +26,11 @@ firearm(gun). #show show(fail(X)) : fail(X). #show show(unloaded(X)) : unloaded(X). #program base. -#external and(and(shoot(X),prev(eventually_before(shoot(X)))),always_before(unloaded(X))) : shoot(X); unloaded(X); shoot(X). [false] +#external and(and(shoot(X),prev(eventually_before(shoot(X)))),always_before(unloaded(X))) : shoot(X); shoot(X); unloaded(X). [false] #external and(initial,firearm(X)) : firearm(X). [false] +#external fail(X) : shoot(X); shoot(X); unloaded(X). [false] #external shoot(X) : firearm(X). [false] #external unloaded(X) : firearm(X). [false] #external unloaded(X) : firearm(X). [false] -#external shoot(X) : firearm(X). [false] #external unloaded(X) : firearm(X). [false] -#external fail(X) : shoot(X); unloaded(X); shoot(X). [false] +#external shoot(X) : firearm(X). [false] diff --git a/tests/asp/transform/meta-telingo/transform-add-externals.lp b/tests/asp/transform/meta-telingo/transform-add-externals.lp index 584deee..0112b69 100644 --- a/tests/asp/transform/meta-telingo/transform-add-externals.lp +++ b/tests/asp/transform/meta-telingo/transform-add-externals.lp @@ -1,16 +1,18 @@ operator_arity((initial;final),0). -operator_arity((prev;wprev;next;wnext; +operator_arity((prev;wprev;next;wnext;neg; always;always_before;eventually;eventually_before),1). operator_arity((until;since;release;trigger;and;or),2). % Naturally, default negation is unsafe. % wnext/wprev are unsafe, as they are satisfied in the final/initial time step % even if their operand is not. -unsafe_arg((wprev;wnext),0). +arg((wprev;wnext),0,unsafe). % the left operand of binary temporal operators are considered unsafe, % as they can be satisfied even if their left operand is not. -unsafe_arg((until;since;release;trigger),0). +arg((until;since;release;trigger),0,unsafe). % both operands of or are unsafe. -unsafe_arg(or,(0;1)). +arg(or,(0;1),unsafe). +arg(Opname,Arg,safe) + :- operator_arity(Opname,Arity), Arg=0..Arity-1, not arg(Opname,Arg,unsafe). func_arity(F,A) :- function(F,_,terms(TS)), A = #count{ P: terms(TS,P,_) }. num_func_args(F,N) @@ -24,36 +26,23 @@ operator(function(F)) root_operator(Func) :- operator(Func), symbolic_atom(_,Func). -%% #show. -%% #show (F,Name) : operator(funcion(F)), function(F,Name,_). - -operand(function(F),Operand) - :- operator(function(F)), function(F,_,terms(T)), terms(T,_,Operand). - -unsafe_operand(function(F),Operand) - :- operator(function(F)), function(F,Name,terms(T)), - unsafe_arg(Name,Pos), terms(T,Pos,Operand). - -safe_operand(Func,Operand) - :- operand(Func,Operand), not unsafe_operand(Func,Operand). +operand(function(F),Operand,Safety) + :- operator(function(F)), function(F,Name,terms(T)), arg(Name,P,Safety), + terms(T,P,Operand). desc_root_op(Func,Child) :- root_operator(Func), child(Func,Child). desc_root_op(Func,Child') :- desc_root_op(Func,Child), child(Child,Child'). has_var(Func) :- desc_root_op(Func,variable(V)). -desc_root_op2operand(Func,Operand) :- operand(Func,Operand), root_operator(Func). -desc_root_op2operand(Func,Operand') - :- desc_root_op2operand(Func,Operand), operand(Operand,Operand'). -desc_root_op2safe_operand(Func,Operand) - :- safe_operand(Func,Operand), root_operator(Func). -desc_root_op2safe_operand(Func,Operand') - :- desc_root_op2safe_operand(Func,Operand), safe_operand(Operand,Operand'). -root_op2leaf_operand(Func, Operand) - :- desc_root_op2operand(Func,Operand), not operator(Operand). -root_op2safe_leaf_operand(Func, Operand) - :- root_operator(Func), desc_root_op2safe_operand(Func,Operand), - not operator(Operand). +operand_from_root(Root,Operand,Safety) + :- root_operator(Root), operand(Root,Operand,Safety). +operand_from_root(Root,Operand',Safety) + :- operand_from_root(Root,Operand,Safety), operand(Operand,Operand',safe). +operand_from_root(Root,Operand',unsafe) + :- operand_from_root(Root,Operand,Safety), operand(Operand,Operand',unsafe). +leaf_operand_from_root(Root,Operand,Safety) + :- operand_from_root(Root,Operand,Safety), not operator(Operand). root_op_sign(Func,Sign) :- root_operator(Func), symbolic_atom(A,Func), @@ -62,9 +51,6 @@ root_op_sign(Func,Sign) :- root_operator(Func), symbolic_atom(A,Func), body_literal(_,Sign,symbolic_atom(A)). -%% #show. -%% #show (Name,Name') : root_op2leaf_operand(function(F),function(F')), function(F,Name,_), function(F',Name',_). - % determine which root operators occur in the head vs the body possible_head_root_op(Func) :- root_operator(Func), symbolic_atom(S,Func), literal(L,_,symbolic_atom(S)), @@ -86,6 +72,7 @@ body_root_op(Func) :- not head_root_op(Func), root_operator(Func). desc_stm((statements(STM),Pos),Child) :- statements(STM,Pos,Child). desc_stm(Statement,Child') :- desc_stm(Statement,Child), not root_operator(Child), child(Child,Child'). +% functions occurring in the body are included root_op2possible_extern_cond(Func,Sign,Func') :- desc_stm(Statement,Func), root_operator(Func), desc_stm(Statement,body_literal(BL)), body_literal(BL,Sign,symbolic_atom(S)), @@ -96,7 +83,7 @@ root_op2possible_extern_cond(Func,Sign,Func') :- root_operator(Func), symbolic_atom(S,Func), literal(L,_,symbolic_atom(S)), conditional_literal(_,literal(L),literals(LS)), literals(LS,_,literal(L')), literal(L',Sign,symbolic_atom(S')), symbolic_atom(S',Func'). -% where operator is in body of condition (this covers body aggregates +% and where operator is in body of condition (this covers body aggregates % as well thankfully) root_op2possible_extern_cond(Func,Sign,Func') :- root_operator(Func), symbolic_atom(S,Func), literal(L,_,symbolic_atom(S)), @@ -107,46 +94,40 @@ root_op2possible_extern_cond(Func,Sign,Func') % non-operator literals in the body, and the safe leaf operands of % operator literals, omitting the safe leaf operand of the operator in % question if it is not positive. + +% no conditioning on it's own operands if it is not positive -root_op2extern_cond(Func,Sign,Func') :- root_op2possible_extern_cond(Func,Sign,Func'), Func=Func', Sign=("not";"not not"). +% we condition on each body literal root_op2extern_cond(Func,Sign,Func') :- root_op2possible_extern_cond(Func,Sign,Func'), not root_operator(Func'). root_op2extern_cond(Func,Sign,Func'') :- root_op2possible_extern_cond(Func,Sign,Func'), not -root_op2extern_cond(Func,Sign,Func'), - root_op2safe_leaf_operand(Func',Func''). + leaf_operand_from_root(Func',Func'',safe). % create a base subprogram under which the external will be added. -ast( - add(program(externals,"base",constants(externals),statements(externals))) -). +ast(add(program(externals,"base",constants(externals),statements(externals)))). % head of external condition in head operator case. -ast( - add(statements(externals,0,external(Operand)); +ast(add(statements(externals,pos(Func,Operand),external(Operand)); external(Operand,symbolic_atom(Operand),body_literals(Func),false); symbolic_atom(Operand,Operand))) - :- head_root_op(Func), root_op2leaf_operand(Func,Operand). + :- head_root_op(Func), leaf_operand_from_root(Func,Operand,_). + % head of external condition in body operator case. -ast( - add(statements(externals,0,external(Func)); +ast(add(statements(externals,pos(Func),external(Func)); external(Func,symbolic_atom(Func),body_literals(Func),false); symbolic_atom(Func,Func))) :- body_root_op(Func). -% body of external condition in all cases but when we have a propositional body operator. -ast( - add(body_literals(Func,0,body_literal(Func')); + +% body of external condition +% when we have a propositional operator in the body, we leave the condition empty +ast(add(body_literals(Func,pos(Func'),body_literal(Func')); body_literal(Func',Sign,symbolic_atom(Func')); symbolic_atom(Func',Func'))) :- root_operator(Func), root_op2extern_cond(Func,Sign,Func'), #false : not has_var(Func), body_root_op(Func). -% body of external condition when we have a propositional body operator. -ast( - add(body_literals(Func,0,body_literal(Func')); - body_literal(Func',Sign,symbolic_atom(Func')); - symbolic_atom(Func',Func'))) - :- root_operator(Func), root_op2safe_leaf_operand(Func,Sign,Func'), - not has_var(Func), body_root_op(Func). diff --git a/tests/asp/transform/meta-telingo/transform-subprogram.lp b/tests/asp/transform/meta-telingo/transform-subprogram.lp index 8fa2250..5ea191f 100644 --- a/tests/asp/transform/meta-telingo/transform-subprogram.lp +++ b/tests/asp/transform/meta-telingo/transform-subprogram.lp @@ -1,17 +1,18 @@ % transform initial, dynamic, always and final subprograms +temporal_program(P) + :- program(P,X,constants(CS),_), not constants(CS,_,_), + X=("initial";"dynamic";"always";"final"). % move all the temporal subprograms into the base subprogram -ast( - delete(program(P,X,constants(CS),statements(STS))); +ast(delete(program(P,X,constants(CS),statements(STS))); add(program(P,"base",constants(CS),statements(STS)))) - :- program(P,X,constants(CS),statements(STS)), not constants(CS,_,_), - X=("initial";"dynamic";"always";"final"). + :- program(P,X,constants(CS),statements(STS)), temporal_program(P). % tag bodies to be modified with temporal subprogram they appear in body_program(BLS,X) - :- program(_,X,constants(CS),statements(STS)), not constants(CS,_,_), statements(STS,_,Statement), - child(Statement,body_literals(BLS)), X=("initial";"dynamic";"always";"final"). + :- program(_,X,constants(CS),statements(STS)), temporal_program(P), + statements(STS,_,Statement), child(Statement,body_literals(BLS)). ast( add(body_literals(BLS,-1,body_literal(BLS)); @@ -37,13 +38,4 @@ ast( ) :- body_program(BLS,"dynamic"). -% since there will be a downstream meta-encoding, construct the -% child relation for the new ast elements. -ast( - add(child(body_literals(BLS),body_literal(BLS)); - child(body_literal(BLS),symbolic_atom(BLS)); - child(symbolic_atom(BLS),function(BLS))) -) - :- body_program(BLS,_). - diff --git a/tests/asp/transform/meta-telingo/transform-theory-to-symbolic.lp b/tests/asp/transform/meta-telingo/transform-theory-to-symbolic.lp index beb0ad8..2257dd5 100644 --- a/tests/asp/transform/meta-telingo/transform-theory-to-symbolic.lp +++ b/tests/asp/transform/meta-telingo/transform-theory-to-symbolic.lp @@ -14,6 +14,11 @@ tel_theory_atom_terms(TTS,Loc) :- theory_atom(A,function(F),theory_atom_elements(E),_), tel_theory_atom(A,Loc), theory_atom_elements(E,_,theory_terms(TTS),_). +tel_root_term(Term,Loc) :- tel_theory_atom_terms(TTS,Loc), theory_terms(TTS,0,Term). +tel_root_term_id(Term,F) :- tel_root_term(Term,_), Term=(function(F);theory_function(F)). +tel_root_term_desc(Term,Term) :- tel_root_term(Term,Loc). +tel_root_term_desc(Term,Child') :- tel_root_term_desc(Term,Child), child(Child,Child'). + % each tel theory atom element should should have a single function or % theory function in it's term tuple, as we rewrite elements as % conditional literals or body literals, and these may only have one literal in their @@ -25,11 +30,6 @@ tel_theory_atom_terms(TTS,Loc) #show log("error","{}: The term tuple of tel theory atom elements must contain a single (temporal) formula.",Loc) : tel_theory_atom_terms(TTS,Loc), #count{ P: theory_terms(TTS,P,_) } != 1. -tel_root_term(Term,Loc) :- tel_theory_atom_terms(TTS,Loc), theory_terms(TTS,0,Term). -tel_root_term_id(Term,F) :- tel_root_term(Term,_), Term=(function(F);theory_function(F)). -tel_root_term_desc(Term,Term) :- tel_root_term(Term,Loc). -tel_root_term_desc(Term,Child') :- tel_root_term_desc(Term,Child), child(Child,Child'). - #show log("error", "{}: Theory sequences not allowed in tel theory atoms, found sequence type {}.",location(theory_sequence(TS),Begin,End),SequenceType) : tel_root_term_desc(Term,theory_sequence(TS)), theory_sequence(TS,SequenceType,_), location(theory_sequence(TS),Begin,End). @@ -65,27 +65,25 @@ ast(replace(theory_function(TF,Name,theory_terms(TTS)),function(TF,Const,terms(T % body case +tel_body_theory_atom(BL,Sign,A,F,LS) + :- 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). + ast(replace(body_literal(BL,Sign,theory_atom(A)), conditional_literal((A,1),literal((A,2)),literals(LS))); add(literal((A,2),Sign,symbolic_atom((A,3))); symbolic_atom((A,3),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), + :- tel_body_theory_atom(BL,Sign,A,F,LS), literals(LS,_,_). ast(replace(body_literal(BL,Sign,theory_atom(A)), body_literal((A,0),Sign,symbolic_atom((A,1)))); add(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), + :- tel_body_theory_atom(BL,Sign,A,F,LS), not literals(LS,_,_). % head case diff --git a/tests/asp/transform/theory-parsing/parse-unparsed-theory-terms.lp b/tests/asp/transform/theory-parsing/parse-unparsed-theory-terms.lp index c43d516..ab435d3 100644 --- a/tests/asp/transform/theory-parsing/parse-unparsed-theory-terms.lp +++ b/tests/asp/transform/theory-parsing/parse-unparsed-theory-terms.lp @@ -144,7 +144,6 @@ call(parse(0,T',T)) :- last(T), next(T',T). % Finally, add the output of out Pratt parser to the AST in the correct place - parsed(@decompose(theory_function(UT,Name,Args))) :- return(parse(0,T',T),(_,theory_function_(Name,Args))), last(T), next(T',T), diff --git a/tests/test_reify_reflect.py b/tests/test_reify_reflect.py index 8623f6c..b412ace 100644 --- a/tests/test_reify_reflect.py +++ b/tests/test_reify_reflect.py @@ -273,14 +273,9 @@ def test_children_query_error_multiple_in_same_position(self): rast = ReifiedAST() rast.add_reified_files([malformed_reified_files / "multiple_in_same_pos.lp"]) regex = ( - r"multiple child facts in the same position.*guards\(7\)" + r"(?s).*multiple child facts in the same position.*guards\(7\)" ) - with self.assertLogs("renopro.rast", level="DEBUG") as cm: - rast.reflect() - logs = "\n".join(cm.output) - reo = re.compile(regex) - num_log_matches = len(reo.findall(logs)) - assert num_log_matches == 1 + with self.assertRaisesRegex(ChildrenQueryError, expected_regex=regex): rast.reflect() def test_children_query_error_one_or_more_expected_zero_found(self):