diff --git a/src/renopro/asp/tests/transform/not_bad/output.lp b/src/renopro/asp/tests/transform/not_bad/output.lp index 2480851..e92957c 100644 --- a/src/renopro/asp/tests/transform/not_bad/output.lp +++ b/src/renopro/asp/tests/transform/not_bad/output.lp @@ -1,3 +1,2 @@ -#program base. good(X) :- person(X); not bad(X). good(dog(X,"spotty")) :- cute(dog(X,"spotty")); not bad(dog(X,"spotty")). diff --git a/src/renopro/asp/tests/transform/not_bad/transform.lp b/src/renopro/asp/tests/transform/not_bad/transform.lp index 5c4450d..cd38e4a 100644 --- a/src/renopro/asp/tests/transform/not_bad/transform.lp +++ b/src/renopro/asp/tests/transform/not_bad/transform.lp @@ -18,19 +18,10 @@ max_index(I,N) :- N = #max{ P : literal_tuple(I,P,_); -1 }, literal_tuple(I,_,_) % the transformation itself -add_not_bad(LitTuple,N+1,Fargs) -:- rule(_,literal(Lit),literal_tuple(LitTuple)), - literal(Lit,"pos",function(Func)), - function(Func,good,Fargs), - max_index(LitTuple,N). - - -% effect of add_not_bad -add(literal_tuple(LitTuple,Pos,literal(new_id(LitTuple,0)))) -:- add_not_bad(LitTuple,Pos,Fargs). - -add(literal(new_id(LitTuple,0),"not",function(new_id(LitTuple,1)))) -:- add_not_bad(LitTuple,Pos,Fargs). - -add(function(new_id(LitTuple,1),bad,Fargs)) -:- add_not_bad(LitTuple,Pos,Fargs). +add((literal_tuple(LT,N+1,literal(new_id(LT,0)))); + literal(new_id(LT,0),"not",function(new_id(LT,1))); + function(new_id(LT,1),bad,Fargs)) +:- rule(_,literal(L),literal_tuple(LT)), + literal(L,"pos",function(F)), + function(F,good,Fargs), + max_index(LT,N). diff --git a/src/renopro/asp/tests/transform/prev_to_timepoints/constant_input.lp b/src/renopro/asp/tests/transform/prev_to_timepoints/constant_input.lp new file mode 100644 index 0000000..363e5b7 --- /dev/null +++ b/src/renopro/asp/tests/transform/prev_to_timepoints/constant_input.lp @@ -0,0 +1 @@ +a :- prev(b), prev(prev(prev(a))). diff --git a/src/renopro/asp/tests/transform/prev_to_timepoints/constant_output.lp b/src/renopro/asp/tests/transform/prev_to_timepoints/constant_output.lp new file mode 100644 index 0000000..e844a78 --- /dev/null +++ b/src/renopro/asp/tests/transform/prev_to_timepoints/constant_output.lp @@ -0,0 +1 @@ +a(t) :- b((t-1)); a((t-3)). diff --git a/src/renopro/asp/tests/transform/robot_transform.lp b/src/renopro/asp/tests/transform/prev_to_timepoints/robot_transform_old.lp similarity index 100% rename from src/renopro/asp/tests/transform/robot_transform.lp rename to src/renopro/asp/tests/transform/prev_to_timepoints/robot_transform_old.lp diff --git a/src/renopro/asp/tests/transform/robot_input.lp b/src/renopro/asp/tests/transform/prev_to_timepoints/sad_input.lp similarity index 100% rename from src/renopro/asp/tests/transform/robot_input.lp rename to src/renopro/asp/tests/transform/prev_to_timepoints/sad_input.lp diff --git a/src/renopro/asp/tests/transform/prev_to_timepoints/sad_output.lp b/src/renopro/asp/tests/transform/prev_to_timepoints/sad_output.lp new file mode 100644 index 0000000..b429c57 --- /dev/null +++ b/src/renopro/asp/tests/transform/prev_to_timepoints/sad_output.lp @@ -0,0 +1,3 @@ +sad(robot(X),t) :- sad(robot(X),(t-1)); not cheer_up(robot(X),t). + + diff --git a/src/renopro/asp/tests/transform/prev_to_timepoints/transform.lp b/src/renopro/asp/tests/transform/prev_to_timepoints/transform.lp new file mode 100644 index 0000000..b546b13 --- /dev/null +++ b/src/renopro/asp/tests/transform/prev_to_timepoints/transform.lp @@ -0,0 +1,61 @@ +% auxiliary atoms +max_index(T,Index) :- Index = #max{ Pos : term_tuple(T,Pos,_); -1 }, term_tuple(T,_,_). +arity(F,N+1) :- function(F,_,term_tuple(T)), max_index(T,N). + + +% when a literal is not prev + +% when atom of a literal is a predicate +add((term_tuple(T,N+1,constant(new_id(T))); + constant(new_id(T),t))) +:- literal(L,_,function(F)), function(F,Name,term_tuple(T)), + Name!=prev, max_index(T,N). + +% when atom of a literal is a propositional constant +delete(literal(L,S,constant(F))) :- literal(L,S,constant(F)). +add((literal(L,S,function(F)); + function(F,Name,term_tuple(new_id(F))); + term_tuple(new_id(F),0,constant(new_id(F))); + constant(new_id(F),t))) +:- literal(L,S,constant(F)), constant(F,Name). + + +prev_chain(L,function(F),O) +:- literal(L,_,function(F)), function(F,prev,term_tuple(T)), arity(F,1), + term_tuple(T,0,O). + +prev_chain(L,function(F),O) +:- prev_chain(L,_,function(F)), function(F,prev,term_tuple(T)), arity(F,1), + term_tuple(T,0,O). + +final_operand(L,O) +:- prev_chain(L,F,O), not prev_chain(L,O,_), O=(constant(_);function(_)). + +first_prev(L,F) +:- prev_chain(L,F,O), not prev_chain(L,_,F). + +num_prevs(L,N) +:- N = #count{ F : prev_chain(L,F,_) }, prev_chain(L,_,_). + +% when final operand is a function +replace(function(F,N,A),function(F,Name,term_tuple(T))) +:- first_prev(L,function(F)), function(F,N,A), final_operand(L,function(O)), + function(O,Name,term_tuple(T)). + +add(term_tuple(T,I+1,binary_operation(new_id(O))); + binary_operation(new_id(O),"-",constant(new_id(O)),number(new_id(O))); + constant(new_id(O),t); + number(new_id(O),N)) +:- final_operand(L,function(O)), function(O,_,term_tuple(T)), max_index(T,I), + num_prevs(L,N). + +% when final operand is a constant +replace(function(F,N,A),function(F,Name,term_tuple(new_id(O)))) +:- first_prev(L,function(F)), function(F,N,A), final_operand(L,constant(O)), + constant(O,Name). + +add(term_tuple(new_id(O),0,binary_operation(new_id(O))); + binary_operation(new_id(O),"-",constant(new_id(O)),number(new_id(O))); + constant(new_id(O),t); + number(new_id(O),N)) +:- final_operand(L,constant(O)), num_prevs(L,N). diff --git a/src/renopro/asp/tests/transform/prev_to_timepoints/very_sad_input.lp b/src/renopro/asp/tests/transform/prev_to_timepoints/very_sad_input.lp new file mode 100644 index 0000000..17c803f --- /dev/null +++ b/src/renopro/asp/tests/transform/prev_to_timepoints/very_sad_input.lp @@ -0,0 +1 @@ +very_sad(robot(X)) :- prev(sad(robot(X))), prev(prev(sad(robot(X)))). \ No newline at end of file diff --git a/src/renopro/asp/tests/transform/prev_to_timepoints/very_sad_output.lp b/src/renopro/asp/tests/transform/prev_to_timepoints/very_sad_output.lp new file mode 100644 index 0000000..6546cd8 --- /dev/null +++ b/src/renopro/asp/tests/transform/prev_to_timepoints/very_sad_output.lp @@ -0,0 +1 @@ +very_sad(robot(X),t) :- sad(robot(X),(t-1)); sad(robot(X),(t-2)). diff --git a/src/renopro/asp/tests/transform/robot_output.lp b/src/renopro/asp/tests/transform/robot_output.lp deleted file mode 100644 index 5d1a523..0000000 --- a/src/renopro/asp/tests/transform/robot_output.lp +++ /dev/null @@ -1,3 +0,0 @@ -sad(robot(X),T) :- sad(robot(X),(T-1)); not cheer_up(robot(X),T). - - diff --git a/src/renopro/asp/tests/transform/robot_reified.lp b/src/renopro/asp/tests/transform/robot_reified.lp deleted file mode 100644 index c245a14..0000000 --- a/src/renopro/asp/tests/transform/robot_reified.lp +++ /dev/null @@ -1,30 +0,0 @@ -rule(literal(0),literal_tuple(6)). - -literal(0,0,function(1)). -function(1,"sad",term_tuple(2)). -term_tuple(2,0,function(3)). -function(3,"robot",term_tuple(4)). -term_tuple(4,0,variable(5)). -variable(5,"X"). - -literal_tuple(6,0,literal(7)). -literal_tuple(6,1,literal(8)). - - -function(1). - -literal(9,0,function(10)). -function(11,"prev",term_tuple(12)). -term_tuple(13,0,function(14)). -function(15,"sad",term_tuple(16)). -term_tuple(17,0,function(18)). -function(19,"robot",term_tuple(20)). -term_tuple(21,0,variable(22)). -variable(23,"X"). - -literal(8,1,function(24)). -function(24,"cheer_up",term_tuple(25)). -turm_tuple(25,0,function(26)). -function(26,"robot",term_tuple(27)). -term_tuple(27,0,variable(28)). -variable(28,"X"). diff --git a/src/renopro/asp/tests/transform/robot_reified_flat.lp b/src/renopro/asp/tests/transform/robot_reified_flat.lp deleted file mode 100644 index 059cf40..0000000 --- a/src/renopro/asp/tests/transform/robot_reified_flat.lp +++ /dev/null @@ -1,27 +0,0 @@ -rule(literal(0),literal_tuple(6)). - -literal(0,0,function(1)). -function(1,"sad",term_tuple(2)). -term_tuple(2,0,function(3)). -function(3,"robot",term_tuple(4)). -term_tuple(4,0,variable(5)). -variable(5,"X"). - -literal_tuple(6,0,literal(7)). -literal_tuple(6,0,literal(8)). - -literal(9,0,function(10)). -function(11,"prev",term_tuple(12)). -term_tuple(13,0,function(14)). -function(15,"sad",term_tuple(16)). -term_tuple(17,0,function(18)). -function(19,"robot",term_tuple(20)). -term_tuple(21,0,variable(22)). -variable(23,"X"). - -literal(8,1,function(24)). -function(24,"cheer_up",term_tuple(25)). -turm_tuple(25,0,function(26)). -function(26,"robot",term_tuple(27)). -term_tuple(27,0,variable(28)). -variable(28,"X"). diff --git a/src/renopro/asp/tests/transform/robot_transform_flat.lp b/src/renopro/asp/tests/transform/robot_transform_flat.lp deleted file mode 100644 index db3bbe2..0000000 --- a/src/renopro/asp/tests/transform/robot_transform_flat.lp +++ /dev/null @@ -1,21 +0,0 @@ -% auxiliary atoms -max_index(T,M) :- M = #max{ P : term_tuple(T,P,_); -1 }, term_tuple(T,_,_). - - -% when outermost function is not prev -add_var(T,"T") :- literal(L,_,A), function(A,N,T), N!="prev". - -% definition of add_var -new(term_tuple(T,M+1,variable(id(T)))) :- add_var(T,Var). -new(variable(id(T),Var)) :- add_var(T,Var). - - -% when outermost function is prev -remove_prev(A,T,F) :- literal(L,_,A), function(A,"prev",T), - term_tuple(T,0,function(F)), not term_tuple(T,1,_). - -replace(function(A,"prev",T),function(A,N,T')) :- remove_prev(A,T,F), function(F,N,T'). - -% add binary operator... -new() :- remove_prev(A,T,F). - diff --git a/tests/test_transform.py b/tests/test_transform.py index 61f45c1..3a360b4 100644 --- a/tests/test_transform.py +++ b/tests/test_transform.py @@ -11,6 +11,8 @@ class TestTransform(TestCase): """Tests for ast transformations defined via a meta-encodings.""" + base_str = "#program base.\n" + def test_transform_add_literal(self): """Test adding an additional literal to the body of rules. @@ -22,18 +24,22 @@ def test_transform_add_literal(self): rast.reify_files([files_dir / "input.lp"]) rast.transform(meta_files=[files_dir / "transform.lp"]) rast.reflect() - transformed_str = rast.program_string - with (files_dir / "output.lp").open("r") as good_output: - good_output_str = good_output.read().strip() - self.assertEqual(transformed_str.strip(), good_output_str) + transformed_str = rast.program_string.strip() + with (files_dir / "output.lp").open("r") as output: + expected_str = self.base_str + output.read().strip() + self.assertEqual(transformed_str, expected_str) def test_transform_add_time(self): """Test transforming a temporal logic program with the previous operator into a program with explicit time points.""" - rast = ReifiedAST() - rast.reify_files([test_transform_files / "robot_input.lp"]) - rast.transform(meta_files=[test_transform_files / "robot_transform.lp"]) - transformed_str = rast.reflect() - with (test_transform_files / "robot_output.lp").open("r") as robot_output: - robot_output_str = robot_output.read().strip() - self.assertEqual(transformed_str.strip(), robot_output_str) + for testname in ["sad", "very_sad", "constant"]: + with self.subTest(testname=testname): + rast = ReifiedAST() + files_dir = test_transform_dir / "prev_to_timepoints" + rast.reify_files([files_dir / (testname + "_input.lp")]) + rast.transform(meta_files=[files_dir / "transform.lp"]) + rast.reflect() + transformed_str = rast.program_string.strip() + with (files_dir / (testname + "_output.lp")).open("r") as output: + expected_str = self.base_str + output.read().strip() + self.assertEqual(transformed_str, expected_str)