diff --git a/src/renopro/asp/ast.lp b/src/renopro/asp/ast.lp index 64efe25..ae5c2fc 100644 --- a/src/renopro/asp/ast.lp +++ b/src/renopro/asp/ast.lp @@ -8,6 +8,12 @@ ast(interval(Id,Left,Right)) :- interval(Id,Left,Right). ast(terms(Id,Pos,Element)) :- terms(Id,Pos,Element). ast(function(Id,Name,Args)) :- function(Id,Name,Args). ast(pool(Id,Args)) :- pool(Id,Args). +ast(theory_terms(Id,Pos,Element)) :- theory_terms(Id,Pos,Element). +ast(theory_sequence(Id,SeqType,Terms)) :- theory_sequence(Id,SeqType,Terms). +ast(theory_function(Id,Name,Args)) :- theory_function(Id,Name,Args). +ast(theory_operators(Id,Pos,Operator)) :- theory_operators(Id,Pos,Operator). +ast(theory_unparsed_term_elements(Id,Pos,Operators,Term)) :- theory_unparsed_term_elements(Id,Pos,Operators,Term). +ast(theory_unparsed_term(Id,Elements)) :- theory_unparsed_term(Id,Elements). ast(guard(Id,Op,Term)) :- guard(Id,Op,Term). ast(guards(Id,Pos,Element)) :- guards(Id,Pos,Element). ast(comparison(Id,Guards)) :- comparison(Id,Guards). @@ -18,6 +24,9 @@ ast(literals(Id,Pos,Element)) :- literals(Id,Pos,Element). ast(conditional_literal(Id,Literal,Condition)) :- conditional_literal(Id,Literal,Condition). ast(agg_elements(Id,Pos,Element)) :- agg_elements(Id,Pos,Element). ast(aggregate(Id,LGuard,Elements,RGuard)) :- aggregate(Id,LGuard,Elements,RGuard). +ast(theory_atom_elements(Id,Pos,TheoryTerms,Condition)) :- theory_atom_elements(Id,Pos,TheoryTerms,Condition). +ast(theory_guard(Id,OpName,Term)) :- theory_guard(Id,OpName,Term). +ast(theory_atom(Id,Atom,Elements,TheoryGuard)) :- theory_atom(Id,Atom,Elements,TheoryGuard). ast(body_agg_elements(Id,Pos,Terms,Condition)) :- body_agg_elements(Id,Pos,Terms,Condition). ast(body_aggregate(Id,LGuard,Elements,RGuard)) :- body_aggregate(Id,LGuard,Elements,RGuard). ast(body_literal(Id,Sign,Atom)) :- body_literal(Id,Sign,Atom). diff --git a/src/renopro/asp/defined.lp b/src/renopro/asp/defined.lp index 62762f1..8381210 100644 --- a/src/renopro/asp/defined.lp +++ b/src/renopro/asp/defined.lp @@ -7,6 +7,12 @@ #defined terms/3. #defined function/3. #defined pool/2. +#defined theory_terms/3. +#defined theory_sequence/3. +#defined theory_function/3. +#defined theory_operators/3. +#defined theory_unparsed_term_elements/4. +#defined theory_unparsed_term/2. #defined guard/3. #defined guards/3. #defined comparison/2. @@ -17,6 +23,9 @@ #defined conditional_literal/3. #defined agg_elements/3. #defined aggregate/4. +#defined theory_atom_elements/4. +#defined theory_guard/3. +#defined theory_atom/4. #defined body_agg_elements/4. #defined body_aggregate/4. #defined body_literal/3. diff --git a/src/renopro/predicates.py b/src/renopro/predicates.py index 21f1213..eec8b97 100644 --- a/src/renopro/predicates.py +++ b/src/renopro/predicates.py @@ -140,6 +140,30 @@ class ComparisonOperator(str, enum.Enum): ) +class TheorySequenceType(str, enum.Enum): + """String enum of theory sequence types.""" + + List = "[]" + """ + For sequences enclosed in brackets. + """ + Set = "{}" + """ + For sequences enclosed in braces. + """ + Tuple = "()" + """ + For sequences enclosed in parenthesis. + """ + + +TheorySequenceTypeField = define_enum_field( + parent_field=StringField, + enum_class=TheorySequenceType, + name="TheorySequenceTypeField", +) + + class Sign(str, enum.Enum): """String enum of possible sign of a literal.""" @@ -380,13 +404,119 @@ class Pool1(ComplexTerm, name="pool"): ) +TheoryTermField = combine_fields_lazily( + [String1.Field, Number1.Field, Function1.Field, Variable1.Field], name="TheoryTermField" +) + + +class Theory_Terms(Predicate): + """Predicate representing an element of a tuple of theory terms. + + id: Identifier of the tuple of theory terms. + position: Integer representing position of the element the tuple, ordered by <. + element: Term identifying the element. + """ + + id = Identifier_Field(default=lambda: next(id_count)) + position = IntegerField + element = TheoryTermField + + +class Theory_Terms1(ComplexTerm, name="theory_terms"): + "Term identifying a child tuple of theory terms." + id = Identifier_Field(default=lambda: next(id_count)) + + +class Theory_Sequence(Predicate): + """Predicate representing a sequence of theory terms. + + id: The identifier of the theory sequence. + sequence_type: The type of the theory sequence. + terms: The tuple of terms forming the sequence. + """ + + id = Identifier_Field(default=lambda: next(id_count)) + sequence_type = TheorySequenceTypeField + terms = Theory_Terms1.Field + + +class Theory_Sequence1(ComplexTerm, name="theory_sequence"): + "Term identifying a child theory sequence fact." + id = Identifier_Field(default=lambda: next(id_count)) + + +class Theory_Function(Predicate): + """Predicate representing a theory function term. + + id: The identifier of the theory function. + name: The name of the theory function. + terms: The tuple of theory terms forming the arguments of + the theory function. + """ + + id = Identifier_Field(default=lambda: next(id_count)) + name = ConstantField + arguments = Theory_Terms1.Field + + +class Theory_Function1(ComplexTerm, name="theory_function"): + "Term identifying a child theory function fact." + id = Identifier_Field(default=lambda: next(id_count)) + + +class Theory_Operators(Predicate): + """Predicate representing an element of tuple of theory operators. + + id: The identifier of the tuple of theory operators. + position: Integer representing position of the element the tuple, ordered by <. + operator: A theory operator, represented as a string. + """ + + id = Identifier_Field(default=lambda: next(id_count)) + position = IntegerField + operator = StringField + + +class Theory_Operators1(ComplexTerm, name="theory_operators"): + "Term identifying a child tuple of theory operators" + id = Identifier_Field(default=lambda: next(id_count)) + + +class Theory_Unparsed_Term(Predicate): + """An unparsed theory term is a tuple, each element of which + consists of a tuple of theory operators and a theory term. This + predicate represents an element of an unparsed theory term. + + id: The identifier of the unparsed theory term. + position: Integer representing position of the element + of the theory tuple, ordered by <. + operators: A tuple of theory operators. + term: The theory term. + """ + + id = Identifier_Field(default=lambda: next(id_count)) + position = IntegerField + operators = Theory_Operators1.Field + term = TheoryTermField + + +class Theory_Unparsed_Term1(ComplexTerm, name="theory_unparsed_term"): + "Term identifying a child unparsed theory term fact." + id = Identifier_Field(default=lambda: next(id_count)) + + +TheoryTermField.fields.extend( + [Theory_Sequence1.Field, Theory_Function1.Field, Theory_Unparsed_Term1.Field] +) + + # Literals class Guard(Predicate): """Predicate representing a guard for a comparison or aggregate atom. - id: identifier of the + id: identifier of the guard. """ @@ -551,7 +681,7 @@ class Agg_Elements1(ComplexTerm, name="agg_elements"): class Aggregate(Predicate): - """Predicate representing an (implicit) count aggregate atom with + """Predicate representing an simple (count) aggregate atom with conditional literal elements. id: Identifier of the count aggregate. @@ -574,13 +704,78 @@ class Aggregate1(ComplexTerm, name="aggregate"): id = Identifier_Field(default=lambda: next(id_count)) +class Theory_Atom_Elements(Predicate): + """Predicate representing an element of a tuple forming a theory atom's + aggregate-like part. + + id: Identifier of the tuple of theory atom elements. + position: Integer representing position of the element in the tuple, + ordered by <. + terms: The tuple of theory terms which form an element to be conditionally + aggregated in the theory atom. + condition: The tuple of literals forming a conjunction on which the + tuple of theory terms is conditioned. + """ + + id = Identifier_Field(default=lambda: next(id_count)) + position = IntegerField + terms = Theory_Terms1.Field + condition = Literals1.Field + + +class Theory_Atom_Elements1(ComplexTerm, name="theory_atom_elements"): + "Term identifying a child tuple of of theory atom element facts." + id = Identifier_Field(default=lambda: next(id_count)) + + +class Theory_Guard(Predicate): + """Predicate representing a theory guard. + + id: The identifier of the theory guard. + operator_name: The name of the binary theory operator applied to + the aggregated elements of the theory atom and the theory term. + term: The theory term to which the theory operator is applied. + """ + + id = Identifier_Field(default=lambda: next(id_count)) + operator_name = StringField + term = TheoryTermField + + +class Theory_Guard1(ComplexTerm, name="theory_guard"): + "Term identifying a child theory guard fact." + id = Identifier_Field(default=lambda: next(id_count)) + + +class Theory_Atom(Predicate): + """Predicate representing a theory atom. + + id: Identifier of the theory atom. + atom: The atom forming the symbolic part of the theory atom. + elements: The tuple of elements aggregated in the theory atom. + guard: The (optional) theory guard applied the aggregated elements + of the theory atom. + """ + + id = Identifier_Field(default=lambda: next(id_count)) + atom = Symbolic_Atom1.Field + elements = Theory_Atom_Elements1.Field + guard = Theory_Guard1.Field + + +class Theory_Atom1(ComplexTerm, name="theory_atom"): + "Term identifying a child theory atom fact." + id = Identifier_Field(default=lambda: next(id_count)) + + class Body_Agg_Elements(Predicate, name="body_agg_elements"): """Predicate representing an element of a body aggregate. id: Identifier of the tuple of body aggregate elements. - position: Integer representing position of the element the tuple, ordered by <. + position: Integer representing position of the element in the tuple, ordered by <. terms: The tuple of terms to which the aggregate function will be applied. - condition: The tuple of literals on which the tuple of terms is conditioned. + condition: The tuple of literals forming a conjunction on which the + tuple of terms is conditioned. """ id = Identifier_Field(default=lambda: next(id_count)) @@ -620,7 +815,8 @@ class Body_Aggregate1(Predicate, name="body_aggregate"): BodyAtomField = combine_fields_lazily( - AtomField.fields + [Aggregate1.Field, Body_Aggregate1.Field], name="BodyAtomField" + AtomField.fields + [Aggregate1.Field, Body_Aggregate1.Field, Theory_Atom1.Field], + name="BodyAtomField", ) @@ -720,9 +916,11 @@ class Disjunction(Predicate): """Predicate representing a disjunction of (conditional) literals. id: Identifier of the disjunction. - elements: The conditional literals constituting the disjunction. - Literals occurring in the disjunction are represented - as a conditional literal with an empty condition. + position: Integer representing position of the element the disjunction, + ordered by <. + element: The element of the disjunction, a conditional literal. + A literal in a disjunction is represented as a conditional literal + with an empty condition. """ id = Identifier_Field(default=lambda: next(id_count)) @@ -736,7 +934,13 @@ class Disjunction1(ComplexTerm, name="disjunction"): HeadField = combine_fields( - [Literal1.Field, Aggregate1.Field, Head_Aggregate1.Field, Disjunction1.Field], + [ + Literal1.Field, + Aggregate1.Field, + Head_Aggregate1.Field, + Disjunction1.Field, + Theory_Atom1.Field, + ], name="HeadField", ) @@ -848,6 +1052,11 @@ class Program(Predicate): Terms, Function, Pool, + Theory_Terms, + Theory_Sequence, + Theory_Function, + Theory_Operators, + Theory_Unparsed_Term, Guard, Guards, Comparison, @@ -858,6 +1067,9 @@ class Program(Predicate): Conditional_Literal, Agg_Elements, Aggregate, + Theory_Atom_Elements, + Theory_Guard, + Theory_Atom, Body_Agg_Elements, Body_Aggregate, Body_Literal, @@ -882,6 +1094,11 @@ class Program(Predicate): Terms, Function, Pool, + Theory_Terms, + Theory_Sequence, + Theory_Function, + Theory_Operators, + Theory_Unparsed_Term, Guard, Guards, Comparison, @@ -892,6 +1109,9 @@ class Program(Predicate): Conditional_Literal, Agg_Elements, Aggregate, + Theory_Atom_Elements, + Theory_Guard, + Theory_Atom, Body_Agg_Elements, Body_Aggregate, Body_Literal, diff --git a/src/renopro/rast.py b/src/renopro/rast.py index 745f79c..c15c8fd 100644 --- a/src/renopro/rast.py +++ b/src/renopro/rast.py @@ -376,6 +376,59 @@ def _reify_pool(self, node): self._reify_ast_seqence(node.arguments, pool.arguments.id, preds.Terms) return pool1 + @reify_node.register(ASTType.TheorySequence) + def _reify_theory_sequence(self, node): + theory_seq1 = preds.Theory_Sequence1() + clorm_theory_seq_type = preds.convert_enum( + ast.TheorySequenceType(node.sequence_type), preds.TheorySequenceType + ) + theory_seq = preds.Theory_Sequence( + id=theory_seq1.id, + sequence_type=clorm_theory_seq_type, + terms=preds.Theory_Terms1(), + ) + self._reified.add(theory_seq) + self._reify_ast_seqence(node.terms, theory_seq.terms.id, preds.Theory_Terms) + return theory_seq1 + + @reify_node.register(ASTType.TheoryFunction) + def _reify_theory_function(self, node): + theory_func1 = preds.Theory_Function1() + theory_func = preds.Theory_Function( + id=theory_func1.id, name=node.name, arguments=preds.Theory_Terms1() + ) + self._reified.add(theory_func) + self._reify_ast_seqence( + seq=node.arguments, + tup_id=theory_func.arguments.id, + tup_pred=preds.Theory_Terms, + ) + return theory_func1 + + @reify_node.register(ASTType.TheoryUnparsedTerm) + def _reify_unparsed_theory_term(self, node): + reified_unparsed_theory_term1 = preds.Theory_Unparsed_Term1() + # reified_unparsed_theory_term = preds.Theory_Unparsed_Term( + # id=reified_unparsed_theory_term1.id, + # elements=preds.Theory_Unparsed_Term_Elements1(), + # ) + for pos, element in enumerate(node.elements): + operators = preds.Theory_Operators1() + reified_operators = [ + preds.Theory_Operators(id=operators.id, position=p, operator=op) + for p, op in enumerate(element.operators) + ] + self._reified.add(reified_operators) + reified_theory_term1 = self.reify_node(element.term) + reified_unparsed_theory_term = preds.Theory_Unparsed_Term( + id=reified_unparsed_theory_term1.id, + position=pos, + operators=operators, + term=reified_theory_term1, + ) + self._reified.add(reified_unparsed_theory_term) + return reified_unparsed_theory_term1 + @reify_node.register(ASTType.Guard) def _reify_guard(self, node): guard1 = preds.Guard1() @@ -449,11 +502,9 @@ def _reify_aggregate(self, node) -> preds.Aggregate1: ) elements1 = preds.Agg_Elements1() self._reify_ast_seqence(node.elements, elements1.id, preds.Agg_Elements) - right_guard = ( - preds.Guard1() - if node.right_guard is None - else self.reify_node(node.right_guard) - ) + right_guard = preds.Guard1() + if node.right_guard is not None: + self.reify_node(node.right_guard) count_agg = preds.Aggregate( id=count_agg1.id, left_guard=left_guard, @@ -463,6 +514,44 @@ def _reify_aggregate(self, node) -> preds.Aggregate1: self._reified.add(count_agg) return count_agg1 + @reify_node.register(ASTType.TheoryAtom) + def _reify_theory_atom(self, node) -> preds.Theory_Atom1: + theory_atom1 = preds.Theory_Atom1() + # we make a slight modification in the reified representation + # vs the AST, wrapping the function into a symbolic atom, as + # that's what it really is IMO. + theory_symbolic_atom1 = self.reify_node(ast.SymbolicAtom(node.term)) + theory_atom_elements1 = preds.Theory_Atom_Elements1() + reified_elements = [] + for pos, element in enumerate(node.elements): + theory_terms1 = preds.Theory_Terms1() + self._reify_ast_seqence(element.terms, theory_terms1.id, preds.Theory_Terms) + literals1 = preds.Literals1() + self._reify_ast_seqence(element.condition, literals1.id, preds.Literals) + reified_element = preds.Theory_Atom_Elements( + id=theory_atom_elements1.id, + position=pos, + terms=theory_terms1, + condition=literals1, + ) + reified_elements.append(reified_element) + self._reified.add(reified_elements) + theory_guard1 = preds.Theory_Guard1() + if node.guard is not None: + guard_theory_term = self.reify_node(node.guard.term) + theory_guard = preds.Theory_Guard( + id=theory_guard1.id, operator_name=node.guard.operator_name, term=guard_theory_term + ) + self._reified.add(theory_guard) + theory_atom = preds.Theory_Atom( + id=theory_atom1.id, + atom=theory_symbolic_atom1, + elements=theory_atom_elements1, + guard=theory_guard1, + ) + self._reified.add(theory_atom) + return theory_atom1 + @reify_node.register(ASTType.BodyAggregate) def _reify_body_aggregate(self, node) -> preds.Body_Aggregate1: agg1 = preds.Body_Aggregate1() @@ -647,7 +736,7 @@ def _reflect_child_pred(self, parent_fact, child_id_fact, optional=False): raise ChildQueryError(msg) raise RuntimeError("Code should be unreachable.") # nocoverage - def get_child_facts(self, parent_fact, children_id_fact): + def _get_child_facts(self, parent_fact, children_id_fact): """Query factbase to retrieve all tuple facts identified by children_id_fact.""" identifier = children_id_fact.id child_ast_pred = getattr(preds, type(children_id_fact).__name__.rstrip("1")) @@ -674,7 +763,7 @@ def _reflect_child_preds(self, parent_fact, children_id_fact): child facts. """ - child_facts = self.get_child_facts(parent_fact, children_id_fact) + child_facts = self._get_child_facts(parent_fact, children_id_fact) child_nodes = [] for fact in child_facts: child_nodes.append(self._reflect_child_pred(fact, fact.element)) @@ -766,6 +855,51 @@ def _reflect_pool(self, pool: preds.Pool) -> AST: arg_nodes = self._reflect_child_preds(pool, pool.arguments) return ast.Pool(location=DUMMY_LOC, arguments=arg_nodes) + @reflect_predicate.register + def _reflect_theory_sequence(self, theory_seq: preds.Theory_Sequence) -> AST: + clingo_theory_sequence_type = preds.convert_enum( + preds.TheorySequenceType(theory_seq.sequence_type), ast.TheorySequenceType + ) + theory_term_nodes = self._reflect_child_preds(theory_seq, theory_seq.terms) + return ast.TheorySequence( + location=DUMMY_LOC, + sequence_type=clingo_theory_sequence_type, + terms=theory_term_nodes, + ) + + @reflect_predicate.register + def _reflect_theory_function(self, theory_func: preds.Theory_Function) -> AST: + arguments = self._reflect_child_preds(theory_func, theory_func.arguments) + return ast.TheoryFunction( + location=DUMMY_LOC, name=theory_func.name, arguments=arguments + ) + + @reflect_predicate.register + def _reflect_theory_unparsed_term( + self, theory_unparsed_term: preds.Theory_Unparsed_Term + ) -> AST: + # child_elements = self._get_child_facts( + # theory_unparsed_term, theory_unparsed_term.elements + # ) + # if len(child_elements) == 0: + # msg = ( + # f"Error finding child facts of predicate '{theory_unparsed_term}'.\n" + # "Found no child 'theory_unparsed_term_elements' facts with identifier " + # f"matching {theory_unparsed_term.elements}, expected at least one." + # ) + # raise ChildQueryError(msg) + # reflected_elements = [] + # for element in child_elements: + # child_operators = self._get_child_facts(element, element.ope) + # reflected_operators = [operator.operator for operator in child_operators] + # reflected_term = self._reflect_child_pred(element, element.term) + # reflected_element = ast.TheoryUnparsedTermElement( + # operators=reflected_operators, term=reflected_term + # ) + # reflected_elements.append(reflected_element) + # return ast.TheoryUnparsedTerm(location=DUMMY_LOC, elements=reflected_elements) + pass + @reflect_predicate.register def _reflect_guard(self, guard: preds.Guard) -> AST: clingo_operator = preds.convert_enum( @@ -833,6 +967,38 @@ def _reflect_aggregate(self, aggregate: preds.Aggregate) -> AST: ), ) + @reflect_predicate.register + def _reflect_theory_guard(self, theory_guard: preds.Theory_Guard) -> AST: + reflected_operator_name = theory_guard.operator_name + reflected_theory_term = self._reflect_child_pred( + theory_guard, theory_guard.term + ) + return ast.TheoryGuard( + operator_name=reflected_operator_name, term=reflected_theory_term + ) + + @reflect_predicate.register + def _reflect_theory_atom(self, theory_atom: preds.Theory_Atom) -> AST: + reflected_syb_atom = self._reflect_child_pred(theory_atom, theory_atom.atom) + reflected_elements = [] + elements = self._get_child_facts(theory_atom, theory_atom.elements) + for e in elements: + reflected_terms = self._reflect_child_preds(e, e.terms) + reflected_condition = self._reflect_child_preds(e, e.condition) + reflected_element = ast.TheoryAtomElement( + terms=reflected_terms, condition=reflected_condition + ) + reflected_elements.append(reflected_element) + reflected_guard = self._reflect_child_pred( + theory_atom, theory_atom.guard, optional=True + ) + return ast.TheoryAtom( + location=DUMMY_LOC, + term=reflected_syb_atom.symbol, + elements=reflected_elements, + guard=reflected_guard, + ) + @reflect_predicate.register def _reflect_body_aggregate(self, aggregate: preds.Body_Aggregate) -> AST: reflected_left_guard = self._reflect_child_pred( @@ -841,7 +1007,7 @@ def _reflect_body_aggregate(self, aggregate: preds.Body_Aggregate) -> AST: reflected_agg_function = preds.convert_enum( preds.AggregateFunction(aggregate.function), ast.AggregateFunction ) - elements = self.get_child_facts(aggregate, aggregate.elements) + elements = self._get_child_facts(aggregate, aggregate.elements) reflected_elements = [] for e in elements: reflected_terms = self._reflect_child_preds(e, e.terms) @@ -874,7 +1040,7 @@ def _reflect_head_aggregate(self, aggregate: preds.Head_Aggregate) -> AST: reflected_agg_function = preds.convert_enum( preds.AggregateFunction(aggregate.function), ast.AggregateFunction ) - elements = self.get_child_facts(aggregate, aggregate.elements) + elements = self._get_child_facts(aggregate, aggregate.elements) reflected_elements = [] for e in elements: reflected_terms = self._reflect_child_preds(e, e.terms) @@ -979,13 +1145,15 @@ def transform( for meta_file in meta_files: with meta_file.open() as f: meta_prog += f.read() - logger.debug("Applying transformation defined in following meta-encoding:\n%s", meta_prog) + logger.debug( + "Applying transformation defined in following meta-encoding:\n%s", meta_prog + ) clingo_logger = get_clingo_logger_callback(logger) clingo_options = [] if clingo_options is None else clingo_options ctl = Control(clingo_options, logger=clingo_logger) logger.debug( "Reified facts before applying transformation:\n%s", self.reified_string - ) + ) control_add_facts(ctl, self._reified) ctl.add(meta_prog) ctl.load("./src/renopro/asp/transform.lp") diff --git a/tests/asp/reify_reflect/well_formed_ast/theory_atom_simple.lp b/tests/asp/reify_reflect/well_formed_ast/theory_atom_simple.lp new file mode 100644 index 0000000..43a1b32 --- /dev/null +++ b/tests/asp/reify_reflect/well_formed_ast/theory_atom_simple.lp @@ -0,0 +1,10 @@ +% reified fact representation of program: +% #program base. +% &a. + +program("base",constants(0),statements(1)). +statements(1,0,rule(2)). +rule(2,theory_atom(3),body_literals(9)). +theory_atom(3,symbolic_atom(4),theory_atom_elements(7),theory_guard(8)). +symbolic_atom(4,function(5)). +function(5,a,terms(6)). diff --git a/tests/asp/reify_reflect/well_formed_ast/theory_atom_simple_arg.lp b/tests/asp/reify_reflect/well_formed_ast/theory_atom_simple_arg.lp new file mode 100644 index 0000000..5a8ed37 --- /dev/null +++ b/tests/asp/reify_reflect/well_formed_ast/theory_atom_simple_arg.lp @@ -0,0 +1,12 @@ +% reified fact representation of program: +% #program base. +% &a("b"). + +program("base",constants(0),statements(1)). +statements(1,0,rule(2)). +rule(2,theory_atom(3),body_literals(10)). +theory_atom(3,symbolic_atom(4),theory_atom_elements(8),theory_guard(9)). +symbolic_atom(4,function(5)). +function(5,a,terms(6)). +terms(6,0,string(7)). +string(7,"b"). diff --git a/tests/asp/reify_reflect/well_formed_ast/theory_atom_simple_guard.lp b/tests/asp/reify_reflect/well_formed_ast/theory_atom_simple_guard.lp new file mode 100644 index 0000000..9c68bcc --- /dev/null +++ b/tests/asp/reify_reflect/well_formed_ast/theory_atom_simple_guard.lp @@ -0,0 +1,12 @@ +% reified fact representation of program: +% #program base. +% &a{} | b. + +program("base",constants(0),statements(1)). +statements(1,0,rule(2)). +rule(2,theory_atom(3),body_literals(11)). +theory_atom(3,symbolic_atom(4),theory_atom_elements(7),theory_guard(8)). +symbolic_atom(4,function(5)). +function(5,a,terms(6)). +theory_guard(8,"|",function(9)). +function(9,b,terms(10)). diff --git a/tests/asp/reify_reflect/well_formed_ast/theory_function.lp b/tests/asp/reify_reflect/well_formed_ast/theory_function.lp new file mode 100644 index 0000000..2748535 --- /dev/null +++ b/tests/asp/reify_reflect/well_formed_ast/theory_function.lp @@ -0,0 +1,15 @@ +% reified fact representation of program: +% #program base. +% &a { f(1) }. + +program("base",constants(0),statements(1)). +statements(1,0,rule(2)). +rule(2,theory_atom(3),body_literals(14)). +theory_atom(3,symbolic_atom(4),theory_atom_elements(7),theory_guard(13)). +symbolic_atom(4,function(5)). +function(5,a,terms(6)). +theory_atom_elements(7,0,theory_terms(8),literals(12)). +theory_terms(8,0,theory_function(9)). +theory_function(9,f,theory_terms(10)). +theory_terms(10,0,number(11)). +number(11,1). diff --git a/tests/asp/reify_reflect/well_formed_ast/theory_sequence.lp b/tests/asp/reify_reflect/well_formed_ast/theory_sequence.lp new file mode 100644 index 0000000..a3a031e --- /dev/null +++ b/tests/asp/reify_reflect/well_formed_ast/theory_sequence.lp @@ -0,0 +1,17 @@ +% reified fact representation of program: +% #program base. +% &a{[1,b]}. + +program("base",constants(0),statements(1)). +statements(1,0,rule(2)). +rule(2,theory_atom(3),body_literals(16)). +theory_atom(3,symbolic_atom(4),theory_atom_elements(7),theory_guard(15)). +symbolic_atom(4,function(5)). +function(5,a,terms(6)). +theory_atom_elements(7,0,theory_terms(8),literals(14)). +theory_terms(8,0,theory_sequence(9)). +theory_sequence(9,"[]",theory_terms(10)). +theory_terms(10,0,number(11)). +number(11,1). +theory_terms(10,1,function(12)). +function(12,b,terms(13)). diff --git a/tests/asp/reify_reflect/well_formed_ast/theory_unparsed_term.lp b/tests/asp/reify_reflect/well_formed_ast/theory_unparsed_term.lp new file mode 100644 index 0000000..7f18322 --- /dev/null +++ b/tests/asp/reify_reflect/well_formed_ast/theory_unparsed_term.lp @@ -0,0 +1,20 @@ +% reified fact representation of program: +% #program base. +% &a { +1!-"b" }. + +program("base",constants(0),statements(1)). +statements(1,0,rule(2)). +rule(2,theory_atom(3),body_literals(15)). +theory_atom(3,symbolic_atom(4),theory_atom_elements(7),theory_guard(14)). +symbolic_atom(4,function(5)). +function(5,a,terms(6)). +theory_atom_elements(7,0,theory_terms(8),literals(13)). +theory_terms(8,0,theory_unparsed_term(9)). +theory_unparsed_term(9,theory_unparsed_term_elements(10)). +theory_unparsed_term_elements(10,0,theory_operators(11),number(12)). +theory_operators(11,0,"+"). +number(12,1). +theory_unparsed_term_elements(10,1,theory_operators(12),string(13)). +theory_operators(12,0,"!"). +theory_operators(12,1,"-"). +string(13,"b"). diff --git a/tests/test_reify_reflect.py b/tests/test_reify_reflect.py index dd0c559..2299ea1 100644 --- a/tests/test_reify_reflect.py +++ b/tests/test_reify_reflect.py @@ -271,6 +271,38 @@ def test_rast_aggregate(self): with self.subTest(operation="reflect"): self.assertReflectEqual("1 <= { a: b; c }.", ["aggregate.lp"]) + def test_rast_simple_theory_atom(self): + """Test reification and reflection of simple theory atoms + consisting only of symbolic part.""" + with self.subTest(operation="reify"): + self.assertReifyEqual("&a.", ["theory_atom_simple.lp"]) + with self.subTest(operation="reflect"): + self.assertReflectEqual("&a { }.", ["theory_atom_simple.lp"]) + self.setUp() + self.assertReifyReflectEqual('&a("b") { }.', ["theory_atom_simple_arg.lp"]) + self.setUp() + self.assertReifyReflectEqual('&a { } | b.', ["theory_atom_simple_guard.lp"]) + + def test_rast_theory_sequence(self): + "Test reification and reflection of a theory sequence." + self.assertReifyReflectEqual("&a { [1,b] }.", ["theory_sequence.lp"]) + + def test_rast_theory_sequence_type(self): + "Test that all theory sequence types are accepted in reified representation." + pass + + def test_rast_theory_function(self): + "Test reification and reflection of a theory function." + self.assertReifyReflectEqual("&a { f(1) }.", ["theory_function.lp"]) + + def test_rast_theory_term(self): + "Test that all theory terms are accepted in reified representation." + pass + + def test_rast_theory_unparsed_term(self): + "Test reification and reflection of an unparsed theory term." + self.assertReifyReflectEqual('&a { +1!-"b" }.', ["theory_unparsed_term.lp"]) + def test_rast_head_aggregate(self): "Test reification and reflection of a head aggregate." with self.subTest(operation="reify"):