Skip to content

Commit

Permalink
Merge pull request #39 from jorgefandinno/lute/reificationStep4_testi…
Browse files Browse the repository at this point in the history
…ngAST

Lute/reification step4 testing ast
  • Loading branch information
lute47lillo authored Oct 3, 2022
2 parents cf79c0a + 9bd917a commit 0775e59
Show file tree
Hide file tree
Showing 4 changed files with 129 additions and 55 deletions.
2 changes: 1 addition & 1 deletion requirements.txt
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
clingo==5.5.2
clingo==5.6.2
clingox==1.2.0.post4
--extra-index-url https://test.pypi.org/simple/
64 changes: 64 additions & 0 deletions src/eclingo/parsing/transformers/function_transformer.py
Original file line number Diff line number Diff line change
@@ -0,0 +1,64 @@
"""Module providing an AST function Trasnformer"""
import clingo
from clingo import ast
from clingo.ast import ASTType, Transformer


def _rule_to_symbolic_term_adapter(rules):
"""Helper function"""
rule_trans = SymbolicTermToFunctionTransformer()
rule = rule_trans.visit_sequence(rules)
return rule


class SymbolicTermToFunctionTransformer(Transformer):
"""Transforms a SymbolicTerm AST into a Function AST"""

def visit_Interval(self, term): # pylint: disable=invalid-name
"""Visit AST to ensure right Interval element is SymbolicTerm"""

assert term.right.ast_type == ASTType.SymbolicTerm

return term

def visit_Heuristic(self, term): # pylint: disable=invalid-name
"""Visit AST to ensure modifier Heuristic element is SymbolicTerm"""

new_args = []
for x in term.atom.symbol.arguments:
if x.ast_type == ASTType.SymbolicTerm:

location = x.location
symbol = x.symbol
name = symbol.name
arguments = symbol.arguments

function = ast.Function(location, name, arguments, False)
new_args.append(function)
term.atom.symbol.arguments = new_args

final_atom = ast.SymbolicAtom(term.atom.symbol)
fin_heur = ast.Heuristic(
term.location,
final_atom,
term.body,
term.bias,
term.priority,
term.modifier,
)

return fin_heur

def visit_SymbolicTerm(self, term): # pylint: disable=invalid-name
"""Visit AST to find SymbolicTerm"""

if term.symbol.type != clingo.SymbolType.Function:
return term

location = term.location
symbol = term.symbol
name = symbol.name
arguments = symbol.arguments

function = ast.Function(location, name, arguments, False)
return function
6 changes: 5 additions & 1 deletion src/eclingo/parsing/transformers/parser_negations.py
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@
from clingo import ast
from clingo.ast import Location, Position, Transformer
from clingox.ast import reify_symbolic_atoms
from clingox.pprint import pprint

from eclingo import prefixes

Expand Down Expand Up @@ -44,12 +45,15 @@ def visit_UnaryOperation(self, x):
external = x.argument.external

if self.reification:
aux_name = "-" + name
aux_name = name
else:
aux_name = self.strong_negation_prefix + "_" + name
self.replacement.add((name, len(arguments), aux_name))

atom = ast.Function(location, aux_name, arguments, external)
if self.reification:
return ast.UnaryOperation(location, 0, atom)

return atom


Expand Down
112 changes: 59 additions & 53 deletions tests/test_reification.py
Original file line number Diff line number Diff line change
@@ -1,27 +1,25 @@
import unittest

from typing import cast
from clingo import ast
from clingox.pprint import pprint
from clingox.testing.ast import ASTTestCase, parse_statement

from eclingo.config import AppConfig
from eclingo.parsing import parser
from eclingo.parsing.transformers import ast_reify
from eclingo.parsing.transformers import ast_reify, function_transformer
from tests.test_reification2 import parse_literal

from clingox.testing.ast import ASTTestCase, parse_statement
from clingox.pprint import pprint

def flatten(lst):
result = []
for lst2 in lst:
if isinstance(lst2, list):
for e in lst2:
result.append(str(e))
result.append(e)
else:
result.append(str(lst2))
result.append(lst2)

return result


def parse_program(stm, parameters=[], name="base"):
ret = []
parser.parse_program(
Expand All @@ -33,31 +31,45 @@ def parse_program(stm, parameters=[], name="base"):
)
return flatten(ret)


def clingo_parse_program(stm):
ret = []
ast.parse_string(stm, ret.append)
ret = [str(rule) for rule in ret]
ret = [rule for rule in ret]
return ret


class TestCase(unittest.TestCase):

class TestCase(ASTTestCase):
def setUp(self):
self.print = False

def assert_equal_program(self, program, expected):
expected_program = clingo_parse_program(expected)
self.assertListEqual(sorted(program), sorted(expected_program))

expected_program = function_transformer._rule_to_symbolic_term_adapter(expected_program)

sorted_program = sorted(program)
expected_program.sort()

if len(sorted_program) != len(expected_program):
self.fail(
f"Lists differ (different lenghts {len(sorted_program)} and {len(expected_program)}"
)
for e1, e2 in zip(sorted_program, expected_program):
self.assertEqual(e1, e2)
self.assertListEqual(sorted_program, expected_program)



class Test(TestCase):

def test_non_epistemic_rules(self):
self.assert_equal_program(
parse_program("a :- b, c, not d, not not e."),
"u(a) :- u(b), u(c), not u(d), not not u(e).",
)

self.assert_equal_program(
parse_program("a :- b."),
"u(a) :- u(b).",
)

self.assert_equal_program(
parse_program("-a :- b, -c, not -d, not not -e."),
"u(-a) :- u(b), u(-c), not u(-d), not not u(-e).",
Expand All @@ -67,12 +79,15 @@ def test_epistemic_atom(self):
self.assert_equal_program(
parse_program(":- &k{a}."), ":- k(u(a)). {k(u(a))} :- u(a)."
)


def test_epistemic_atom_with_strong_negation(self):
self.assert_equal_program(
parse_program(":- &k{-a}."),
":- k(u(-a)). {k(u(-a))} :- u(-a).",
)


self.assert_equal_program(
parse_program(":- &k{- -a}."), ":- k(u(a)). {k(u(a))} :- u(a)."
)
Expand All @@ -82,69 +97,58 @@ def test_epistemic_atom_with_default_negation(self):
parse_program(":- &k{ not a}."),
":- k(not1(u(a))). not1(u(a)) :- not u(a). {k(not1(u(a)))} :- not1(u(a)).",
)

self.assert_equal_program(
parse_program("b :- &k{ not a}."),
"u(b) :- k(not1(u(a))). not1(u(a)) :- not u(a). {k(not1(u(a)))} :- not1(u(a)).",
)

self.assert_equal_program(
parse_program(":- &k{ not not a}."),
":- k(not2(u(a))). not2(u(a)) :- not not u(a). {k(not2(u(a)))} :- not2(u(a)).",
)

def test_epistemic_atom_with_both_negations(self):
'''
stat = parse_statement(":- k(not1(u(-a))).")
print()
pprint(stat)
print()
print()
print(type(parse_program(":- &k{ not -a}.")[1]))
pprint(parse_program(":- &k{ not -a}.")[1])
print()
'''


self.assert_equal_program(
parse_program(":- &k{ not -a}."),
parse_program(":- &k{ not -a}."),
":- k(not1(u(-a))). not1(u(-a)) :- not u(-a). {k(not1(u(-a)))} :- not1(u(-a))."
)

self.assert_equal_program(
parse_program(":- &k{ not not -a}."),
":- k(not2(u(-a))). not2(u(-a)) :- not not u(-a). {k(not2(u(-a)))} :- not2(u(-a))."
)

def test_epistemic_with_variables(self):
self.assert_equal_program(
parse_program(":- &k{a(V0)}."), ":- k(u(a(V0))). {k(u(a(V0)))} :- u(a(V0))."
)
self.assert_equal_program(
parse_program(":- &k{- -a(V0)}."),
parse_program(":- &k{- -a(V0)}."),
":- k(u(a(V0))). {k(u(a(V0)))} :- u(a(V0)).")

self.assert_equal_program(
parse_program(":- &k{ not a(V0)}."),
parse_program(":- &k{ not a(V0)}."),
":- k(not1(u(a(V0)))). not1(u(a(V0))) :- not u(a(V0)). {k(not1(u(a(V0))))} :- not1(u(a(V0))).")

self.assert_equal_program(
parse_program(":- &k{ not not a(V0)}."),
parse_program(":- &k{ not not a(V0)}."),
":- k(not2(u(a(V0)))). not2(u(a(V0))) :- not not u(a(V0)). {k(not2(u(a(V0))))} :- not2(u(a(V0))).")

self.assert_equal_program(
parse_program(":- &k{-a(V0)}."),
":- k(u(-a(V0))). {k(u(-a(V0)))} :- u(-a(V0)).",
)

self.assert_equal_program(
parse_program(":- &k{ not -a(V0)}."),
":- k(not1(u(-a(V0)))). not1(u(-a(V0))) :- not u(-a(V0)). {k(not1(u(-a(V0))))} :- not1(u(-a(V0))).")

self.assert_equal_program(
parse_program(":- &k{ not not -a(V0)}."),
":- k(not2(u(-a(V0)))). not2(u(-a(V0))) :- not not u(-a(V0)). {k(not2(u(-a(V0))))} :- not2(u(-a(V0))).")
":- k(not2(u(-a(V0)))). not2(u(-a(V0))) :- not not u(-a(V0)). {k(not2(u(-a(V0))))} :- not2(u(-a(V0))).")

def test_epistemic_with_variables_safety01(self):
self.assert_equal_program(
parse_program(":- &k{a(V0)}, not b(V0)."),
Expand All @@ -163,8 +167,7 @@ def test_epistemic_with_variables_safety02(self):
{ k(not1(u(b(V0)))) : } :- not1(u(b(V0))).
""",
)



def test_epistemic_with_variables_safety03(self):
self.assert_equal_program(
parse_program(":- &k{a(V0)}, &k{not b(V0)}."),
Expand All @@ -176,11 +179,11 @@ def test_epistemic_with_variables_safety03(self):
{ k(u(a(V0))) : } :- u(a(V0)).
""",
)

# Note that the last two rules appear repeated. The second copy apears when processing the rules
# not_u_b(V0) :- &k{u_a(V0)}, not u_b(V0).
# An improvement would removing those unecessary rules

'''
# # Note that the last two rules appear repeated. The second copy apears when processing the rules
# # not_u_b(V0) :- &k{u_a(V0)}, not u_b(V0).
# # An improvement would removing those unecessary rules
'''
def test_epistemic_with_variables_safety04(self):
self.assert_equal_program(
parse_program("b :- not not &k{a(X)}."),
Expand Down Expand Up @@ -209,8 +212,11 @@ def test_negated_epistemic_literals(self):
)

def test_weighted_rules(self):
self.assert_equal_program(parse_program(":-{a} = 0."), ":-{u(a)} = 0.")

self.assert_equal_program(
parse_program(":-{a} = 0."),
":-{u(a)} = 0."
)

def test_parameters01(self):
self.assert_equal_program(
parse_program("a(1..n).", ["n"], "parametrized"),
Expand Down

0 comments on commit 0775e59

Please sign in to comment.