meta-telingo refactor. Strict position ordering, allowing Rawfield.

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

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 "

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]

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]

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]

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).