diff options
author | 2023-07-10 18:38:11 +0200 | |
---|---|---|
committer | 2023-07-10 20:21:01 +0200 | |
commit | 9666818c58bb4c30ef6b0c88cc680bc559b123c6 (patch) | |
tree | e49a67fd85fcf8a8ac679553e47aeeec9b729f0b /subprojects/store-query/src/test/java | |
parent | refactor: enable data variable unification (diff) | |
download | refinery-9666818c58bb4c30ef6b0c88cc680bc559b123c6.tar.gz refinery-9666818c58bb4c30ef6b0c88cc680bc559b123c6.tar.zst refinery-9666818c58bb4c30ef6b0c88cc680bc559b123c6.zip |
feat: DNF rewriting
* DuplicateDnfRewriter replaces DNF with their canonical
representatives
* ClauseInputParameterResolver removes input parameters by demand set
transformation
* CompositeRewriter for rewriter stacks
Diffstat (limited to 'subprojects/store-query/src/test/java')
2 files changed, 372 insertions, 0 deletions
diff --git a/subprojects/store-query/src/test/java/tools/refinery/store/query/rewriter/DuplicateDnfRemoverTest.java b/subprojects/store-query/src/test/java/tools/refinery/store/query/rewriter/DuplicateDnfRemoverTest.java new file mode 100644 index 00000000..ebb24ab5 --- /dev/null +++ b/subprojects/store-query/src/test/java/tools/refinery/store/query/rewriter/DuplicateDnfRemoverTest.java | |||
@@ -0,0 +1,164 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.query.rewriter; | ||
7 | |||
8 | import org.junit.jupiter.api.BeforeEach; | ||
9 | import org.junit.jupiter.api.Test; | ||
10 | import tools.refinery.store.query.dnf.Query; | ||
11 | import tools.refinery.store.query.literal.AbstractCallLiteral; | ||
12 | import tools.refinery.store.query.literal.Reduction; | ||
13 | import tools.refinery.store.query.term.Variable; | ||
14 | import tools.refinery.store.query.view.AnySymbolView; | ||
15 | import tools.refinery.store.query.view.KeyOnlyView; | ||
16 | import tools.refinery.store.representation.Symbol; | ||
17 | |||
18 | import java.util.List; | ||
19 | |||
20 | import static org.hamcrest.MatcherAssert.assertThat; | ||
21 | import static org.hamcrest.Matchers.is; | ||
22 | import static org.hamcrest.Matchers.not; | ||
23 | import static tools.refinery.store.query.literal.Literals.not; | ||
24 | |||
25 | class DuplicateDnfRemoverTest { | ||
26 | private final static Symbol<Boolean> friend = Symbol.of("friend", 2); | ||
27 | private final static AnySymbolView friendView = new KeyOnlyView<>(friend); | ||
28 | |||
29 | private DuplicateDnfRemover sut; | ||
30 | |||
31 | @BeforeEach | ||
32 | void beforeEach() { | ||
33 | sut = new DuplicateDnfRemover(); | ||
34 | } | ||
35 | |||
36 | @Test | ||
37 | void removeDuplicateSimpleTest() { | ||
38 | var one = Query.of("One", (builder, x, y) -> builder.clause( | ||
39 | friendView.call(x, y), | ||
40 | friendView.call(y, x) | ||
41 | )); | ||
42 | var two = Query.of("Two", (builder, x, y) -> builder.clause( | ||
43 | friendView.call(x, y), | ||
44 | friendView.call(y, x) | ||
45 | )); | ||
46 | |||
47 | var oneResult = sut.rewrite(one); | ||
48 | var twoResult = sut.rewrite(two); | ||
49 | |||
50 | assertThat(oneResult, is(twoResult)); | ||
51 | assertThat(one, is(oneResult)); | ||
52 | } | ||
53 | |||
54 | @Test | ||
55 | void notDuplicateSimpleTest() { | ||
56 | var one = Query.of("One", (builder, x, y) -> builder.clause( | ||
57 | friendView.call(x, y), | ||
58 | friendView.call(y, x) | ||
59 | )); | ||
60 | var two = Query.of("Two", (builder, x, y) -> builder.clause((z) -> List.of( | ||
61 | friendView.call(x, y), | ||
62 | friendView.call(y, z) | ||
63 | ))); | ||
64 | |||
65 | var oneResult = sut.rewrite(one); | ||
66 | var twoResult = sut.rewrite(two); | ||
67 | |||
68 | assertThat(one, is(oneResult)); | ||
69 | assertThat(two, is(twoResult)); | ||
70 | } | ||
71 | |||
72 | @Test | ||
73 | void removeDuplicateRecursiveTest() { | ||
74 | var oneSubQuery = Query.of("OneSubQuery", (builder, x, y) -> builder.clause( | ||
75 | friendView.call(x, y), | ||
76 | friendView.call(y, x) | ||
77 | )); | ||
78 | var one = Query.of("One", (builder, x) -> builder.clause( | ||
79 | oneSubQuery.call(x, Variable.of()) | ||
80 | )); | ||
81 | var twoSubQuery = Query.of("TwoSubQuery", (builder, x, y) -> builder.clause( | ||
82 | friendView.call(x, y), | ||
83 | friendView.call(y, x) | ||
84 | )); | ||
85 | var two = Query.of("Two", (builder, x) -> builder.clause( | ||
86 | twoSubQuery.call(x, Variable.of()) | ||
87 | )); | ||
88 | |||
89 | var oneResult = sut.rewrite(one); | ||
90 | var twoResult = sut.rewrite(two); | ||
91 | |||
92 | assertThat(oneResult, is(twoResult)); | ||
93 | assertThat(one, is(oneResult)); | ||
94 | } | ||
95 | |||
96 | @Test | ||
97 | void notDuplicateRecursiveTest() { | ||
98 | var oneSubQuery = Query.of("OneSubQuery", (builder, x, y) -> builder.clause( | ||
99 | friendView.call(x, y), | ||
100 | friendView.call(y, x) | ||
101 | )); | ||
102 | var one = Query.of("One", (builder, x) -> builder.clause( | ||
103 | oneSubQuery.call(x, Variable.of()) | ||
104 | )); | ||
105 | var twoSubQuery = Query.of("TwoSubQuery", (builder, x, y) -> builder.clause( | ||
106 | friendView.call(x, y), | ||
107 | friendView.call(y, x) | ||
108 | )); | ||
109 | var two = Query.of("Two", (builder, x) -> builder.clause( | ||
110 | twoSubQuery.call(Variable.of(), x) | ||
111 | )); | ||
112 | |||
113 | var oneResult = sut.rewrite(one); | ||
114 | var twoResult = sut.rewrite(two); | ||
115 | |||
116 | assertThat(one, is(oneResult)); | ||
117 | assertThat(oneResult, is(not(twoResult))); | ||
118 | |||
119 | var oneCall = (AbstractCallLiteral) oneResult.getDnf().getClauses().get(0).literals().get(0); | ||
120 | var twoCall = (AbstractCallLiteral) twoResult.getDnf().getClauses().get(0).literals().get(0); | ||
121 | |||
122 | assertThat(oneCall.getTarget(), is(twoCall.getTarget())); | ||
123 | } | ||
124 | |||
125 | @Test | ||
126 | void removeContradictionTest() { | ||
127 | var oneSubQuery = Query.of("OneSubQuery", (builder, x, y) -> builder.clause( | ||
128 | friendView.call(x, y), | ||
129 | friendView.call(y, x) | ||
130 | )); | ||
131 | var twoSubQuery = Query.of("TwoSubQuery", (builder, x, y) -> builder.clause( | ||
132 | friendView.call(x, y), | ||
133 | friendView.call(y, x) | ||
134 | )); | ||
135 | var query = Query.of("Contradiction", (builder, x, y) -> builder.clause( | ||
136 | oneSubQuery.call(x, y), | ||
137 | not(twoSubQuery.call(x, y)) | ||
138 | )); | ||
139 | |||
140 | var result = sut.rewrite(query); | ||
141 | |||
142 | assertThat(result.getDnf().getReduction(), is(Reduction.ALWAYS_FALSE)); | ||
143 | } | ||
144 | |||
145 | @Test | ||
146 | void removeQuantifiedContradictionTest() { | ||
147 | var oneSubQuery = Query.of("OneSubQuery", (builder, x, y) -> builder.clause( | ||
148 | friendView.call(x, y), | ||
149 | friendView.call(y, x) | ||
150 | )); | ||
151 | var twoSubQuery = Query.of("TwoSubQuery", (builder, x, y) -> builder.clause( | ||
152 | friendView.call(x, y), | ||
153 | friendView.call(y, x) | ||
154 | )); | ||
155 | var query = Query.of("Contradiction", (builder, x) -> builder.clause( | ||
156 | oneSubQuery.call(x, Variable.of()), | ||
157 | not(twoSubQuery.call(x, Variable.of())) | ||
158 | )); | ||
159 | |||
160 | var result = sut.rewrite(query); | ||
161 | |||
162 | assertThat(result.getDnf().getReduction(), is(Reduction.ALWAYS_FALSE)); | ||
163 | } | ||
164 | } | ||
diff --git a/subprojects/store-query/src/test/java/tools/refinery/store/query/rewriter/InputParameterResolverTest.java b/subprojects/store-query/src/test/java/tools/refinery/store/query/rewriter/InputParameterResolverTest.java new file mode 100644 index 00000000..ddb2a069 --- /dev/null +++ b/subprojects/store-query/src/test/java/tools/refinery/store/query/rewriter/InputParameterResolverTest.java | |||
@@ -0,0 +1,208 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.query.rewriter; | ||
7 | |||
8 | import org.junit.jupiter.api.BeforeEach; | ||
9 | import org.junit.jupiter.api.Test; | ||
10 | import tools.refinery.store.query.dnf.Dnf; | ||
11 | import tools.refinery.store.query.dnf.Query; | ||
12 | import tools.refinery.store.query.term.ParameterDirection; | ||
13 | import tools.refinery.store.query.term.Variable; | ||
14 | import tools.refinery.store.query.view.AnySymbolView; | ||
15 | import tools.refinery.store.query.view.KeyOnlyView; | ||
16 | import tools.refinery.store.representation.Symbol; | ||
17 | |||
18 | import java.util.List; | ||
19 | |||
20 | import static org.hamcrest.MatcherAssert.assertThat; | ||
21 | import static tools.refinery.store.query.literal.Literals.not; | ||
22 | import static tools.refinery.store.query.tests.QueryMatchers.structurallyEqualTo; | ||
23 | |||
24 | class InputParameterResolverTest { | ||
25 | private final static Symbol<Boolean> person = Symbol.of("Person", 1); | ||
26 | private final static Symbol<Boolean> friend = Symbol.of("friend", 2); | ||
27 | private final static AnySymbolView personView = new KeyOnlyView<>(person); | ||
28 | private final static AnySymbolView friendView = new KeyOnlyView<>(friend); | ||
29 | |||
30 | private InputParameterResolver sut; | ||
31 | |||
32 | @BeforeEach | ||
33 | void beforeEach() { | ||
34 | sut = new InputParameterResolver(); | ||
35 | } | ||
36 | |||
37 | @Test | ||
38 | void inlineSingleClauseTest() { | ||
39 | var dnf = Dnf.of("SubQuery", builder -> { | ||
40 | var x = builder.parameter("x", ParameterDirection.OUT); | ||
41 | builder.clause(friendView.call(x, Variable.of())); | ||
42 | }); | ||
43 | var query = Query.of("Actual", (builder, x) -> builder.clause( | ||
44 | dnf.call(x), | ||
45 | personView.call(x) | ||
46 | )); | ||
47 | |||
48 | var actual = sut.rewrite(query); | ||
49 | |||
50 | var expected = Query.of("Expected", (builder, x) -> builder.clause( | ||
51 | friendView.call(x, Variable.of()), | ||
52 | personView.call(x) | ||
53 | )); | ||
54 | |||
55 | assertThat(actual.getDnf(), structurallyEqualTo(expected.getDnf())); | ||
56 | } | ||
57 | |||
58 | @Test | ||
59 | void inlineSingleClauseWIthInputTest() { | ||
60 | var dnf = Dnf.of("SubQuery", builder -> { | ||
61 | var x = builder.parameter("x", ParameterDirection.IN); | ||
62 | builder.clause(not(friendView.call(x, Variable.of()))); | ||
63 | }); | ||
64 | var query = Query.of("Actual", (builder, x) -> builder.clause( | ||
65 | dnf.call(x), | ||
66 | personView.call(x) | ||
67 | )); | ||
68 | |||
69 | var actual = sut.rewrite(query); | ||
70 | |||
71 | var expected = Query.of("Expected", (builder, x) -> builder.clause( | ||
72 | personView.call(x), | ||
73 | not(friendView.call(x, Variable.of())) | ||
74 | )); | ||
75 | |||
76 | assertThat(actual.getDnf(), structurallyEqualTo(expected.getDnf())); | ||
77 | } | ||
78 | |||
79 | @Test | ||
80 | void singleLiteralDemandSetTest() { | ||
81 | var dnf = Dnf.of("SubQuery", builder -> { | ||
82 | var x = builder.parameter("x", ParameterDirection.IN); | ||
83 | builder.clause(not(friendView.call(x, Variable.of()))); | ||
84 | builder.clause(not(friendView.call(Variable.of(), x))); | ||
85 | }); | ||
86 | var query = Query.of("Actual", (builder, x) -> builder.clause( | ||
87 | dnf.call(x), | ||
88 | personView.call(x) | ||
89 | )); | ||
90 | |||
91 | var actual = sut.rewrite(query); | ||
92 | |||
93 | var expectedSubQuery = Dnf.of("ExpectedSubQuery", builder -> { | ||
94 | var x = builder.parameter("x", ParameterDirection.OUT); | ||
95 | builder.clause( | ||
96 | personView.call(x), | ||
97 | not(friendView.call(x, Variable.of())) | ||
98 | ); | ||
99 | builder.clause( | ||
100 | personView.call(x), | ||
101 | not(friendView.call(Variable.of(), x)) | ||
102 | ); | ||
103 | }); | ||
104 | var expected = Query.of("Expected", (builder, x) -> builder.clause( | ||
105 | personView.call(x), | ||
106 | expectedSubQuery.call(x) | ||
107 | )); | ||
108 | |||
109 | assertThat(actual.getDnf(), structurallyEqualTo(expected.getDnf())); | ||
110 | } | ||
111 | |||
112 | @Test | ||
113 | void multipleLiteralDemandSetTest() { | ||
114 | var dnf = Dnf.of("SubQuery", builder -> { | ||
115 | var x = builder.parameter("x", ParameterDirection.IN); | ||
116 | var y = builder.parameter("y", ParameterDirection.IN); | ||
117 | builder.clause(not(friendView.call(x, y))); | ||
118 | builder.clause(not(friendView.call(y, x))); | ||
119 | }); | ||
120 | var query = Query.of("Actual", (builder, p1) -> builder.clause(p2 -> List.of( | ||
121 | not(dnf.call(p1, p2)), | ||
122 | personView.call(p1), | ||
123 | personView.call(p2) | ||
124 | ))); | ||
125 | |||
126 | var actual = sut.rewrite(query); | ||
127 | |||
128 | var context = Dnf.of("Context", builder -> { | ||
129 | var x = builder.parameter("x", ParameterDirection.OUT); | ||
130 | var y = builder.parameter("y", ParameterDirection.OUT); | ||
131 | builder.clause( | ||
132 | personView.call(x), | ||
133 | personView.call(y) | ||
134 | ); | ||
135 | }); | ||
136 | var expectedSubQuery = Dnf.of("ExpectedSubQuery", builder -> { | ||
137 | var x = builder.parameter("x", ParameterDirection.OUT); | ||
138 | var y = builder.parameter("x", ParameterDirection.OUT); | ||
139 | builder.clause( | ||
140 | context.call(x, y), | ||
141 | not(friendView.call(x, y)) | ||
142 | ); | ||
143 | builder.clause( | ||
144 | context.call(x, y), | ||
145 | not(friendView.call(y, x)) | ||
146 | ); | ||
147 | }); | ||
148 | var expected = Query.of("Expected", (builder, p1) -> builder.clause(p2 -> List.of( | ||
149 | context.call(p1, p2), | ||
150 | not(expectedSubQuery.call(p1, p2)) | ||
151 | ))); | ||
152 | |||
153 | assertThat(actual.getDnf(), structurallyEqualTo(expected.getDnf())); | ||
154 | } | ||
155 | |||
156 | @Test | ||
157 | void multipleParameterDemandSetTest() { | ||
158 | var dnf = Dnf.of("SubQuery", builder -> { | ||
159 | var x = builder.parameter("x", ParameterDirection.IN); | ||
160 | var y = builder.parameter("y", ParameterDirection.IN); | ||
161 | builder.clause(not(friendView.call(x, y))); | ||
162 | builder.clause(not(friendView.call(y, x))); | ||
163 | }); | ||
164 | var query = Query.of("Actual", (builder, p1) -> builder.clause( | ||
165 | not(dnf.call(p1, p1)), | ||
166 | personView.call(p1) | ||
167 | )); | ||
168 | |||
169 | var actual = sut.rewrite(query); | ||
170 | |||
171 | var expectedSubQuery = Dnf.of("ExpectedSubQuery", builder -> { | ||
172 | var x = builder.parameter("x", ParameterDirection.OUT); | ||
173 | var y = builder.parameter("y", ParameterDirection.OUT); | ||
174 | builder.clause( | ||
175 | y.isEquivalent(x), | ||
176 | personView.call(x), | ||
177 | not(friendView.call(x, x)) | ||
178 | ); | ||
179 | }); | ||
180 | var expected = Query.of("Expected", (builder, p1) -> builder.clause( | ||
181 | personView.call(p1), | ||
182 | not(expectedSubQuery.call(p1, p1)) | ||
183 | )); | ||
184 | |||
185 | assertThat(actual.getDnf(), structurallyEqualTo(expected.getDnf())); | ||
186 | } | ||
187 | |||
188 | @Test | ||
189 | void eliminateDoubleNegationTest() { | ||
190 | var dnf = Dnf.of("SubQuery", builder -> { | ||
191 | var x = builder.parameter("x", ParameterDirection.IN); | ||
192 | builder.clause(not(friendView.call(x, Variable.of()))); | ||
193 | }); | ||
194 | var query = Query.of("Actual", (builder, p1) -> builder.clause( | ||
195 | personView.call(p1), | ||
196 | not(dnf.call(p1)) | ||
197 | )); | ||
198 | |||
199 | var actual = sut.rewrite(query); | ||
200 | |||
201 | var expected = Query.of("Actual", (builder, p1) -> builder.clause( | ||
202 | personView.call(p1), | ||
203 | friendView.call(p1, Variable.of()) | ||
204 | )); | ||
205 | |||
206 | assertThat(actual.getDnf(), structurallyEqualTo(expected.getDnf())); | ||
207 | } | ||
208 | } | ||