aboutsummaryrefslogtreecommitdiffstats
path: root/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/lifting/DnfLifterTest.java
diff options
context:
space:
mode:
Diffstat (limited to 'subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/lifting/DnfLifterTest.java')
-rw-r--r--subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/lifting/DnfLifterTest.java395
1 files changed, 395 insertions, 0 deletions
diff --git a/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/lifting/DnfLifterTest.java b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/lifting/DnfLifterTest.java
new file mode 100644
index 00000000..793d1cec
--- /dev/null
+++ b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/lifting/DnfLifterTest.java
@@ -0,0 +1,395 @@
1/*
2 * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
3 *
4 * SPDX-License-Identifier: EPL-2.0
5 */
6package tools.refinery.store.reasoning.lifting;
7
8import org.junit.jupiter.api.BeforeEach;
9import org.junit.jupiter.api.Test;
10import tools.refinery.store.query.dnf.Dnf;
11import tools.refinery.store.query.dnf.Query;
12import tools.refinery.store.query.term.ParameterDirection;
13import tools.refinery.store.query.view.AnySymbolView;
14import tools.refinery.store.query.view.FunctionView;
15import tools.refinery.store.query.view.MustView;
16import tools.refinery.store.reasoning.ReasoningAdapter;
17import tools.refinery.store.reasoning.literal.Concreteness;
18import tools.refinery.store.reasoning.literal.ModalConstraint;
19import tools.refinery.store.reasoning.literal.Modality;
20import tools.refinery.store.reasoning.representation.PartialRelation;
21import tools.refinery.store.reasoning.representation.PartialSymbol;
22import tools.refinery.store.representation.Symbol;
23import tools.refinery.store.representation.TruthValue;
24
25import java.util.List;
26
27import static org.hamcrest.MatcherAssert.assertThat;
28import static tools.refinery.store.query.literal.Literals.check;
29import static tools.refinery.store.query.literal.Literals.not;
30import static tools.refinery.store.query.term.int_.IntTerms.*;
31import static tools.refinery.store.query.tests.QueryMatchers.structurallyEqualTo;
32
33class DnfLifterTest {
34 private static final Symbol<TruthValue> friendSymbol = Symbol.of("friend", 2, TruthValue.class,
35 TruthValue.UNKNOWN);
36 private static final AnySymbolView friendMustView = new MustView(friendSymbol);
37 private static final Symbol<Integer> age = Symbol.of("age", 1, Integer.class);
38 private static final FunctionView<Integer> ageView = new FunctionView<>(age);
39 private static final PartialRelation person = PartialSymbol.of("Person", 1);
40 private static final PartialRelation friend = PartialSymbol.of("friend", 2);
41
42 private DnfLifter sut;
43
44 @BeforeEach
45 void beforeEach() {
46 sut = new DnfLifter();
47 }
48
49 @Test
50 void liftPartialRelationCallTest() {
51 var input = Query.of("Actual", (builder, p1) -> builder.clause((v1) -> List.of(
52 friend.call(p1, v1)
53 ))).getDnf();
54 var actual = sut.lift(Modality.MUST, Concreteness.PARTIAL, input);
55
56 var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of(
57 ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, friend).call(p1, v1),
58 ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS_SYMBOL).call(v1)
59 ))).getDnf();
60
61 assertThat(actual, structurallyEqualTo(expected));
62 }
63
64 @Test
65 void liftPartialDnfCallTest() {
66 var called = Query.of("Called", (builder, p1, p2) -> builder.clause(
67 friend.call(p1, p2),
68 friend.call(p2, p1)
69 ));
70 var input = Query.of("Actual", (builder, p1) -> builder.clause((v1) -> List.of(
71 called.call(p1, v1)
72 ))).getDnf();
73 var actual = sut.lift(Modality.MUST, Concreteness.PARTIAL, input);
74
75 var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of(
76 ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, called.getDnf()).call(p1, v1),
77 ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS_SYMBOL).call(v1)
78 ))).getDnf();
79
80 assertThat(actual, structurallyEqualTo(expected));
81 }
82
83 @Test
84 void liftSymbolViewCallTest() {
85 var input = Query.of("Actual", (builder, p1) -> builder.clause((v1) -> List.of(
86 friendMustView.call(p1, v1)
87 ))).getDnf();
88 var actual = sut.lift(Modality.MUST, Concreteness.PARTIAL, input);
89
90 var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of(
91 friendMustView.call(p1, v1),
92 ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS_SYMBOL).call(v1)
93 ))).getDnf();
94
95 assertThat(actual, structurallyEqualTo(expected));
96 }
97
98 @Test
99 void liftPartialRelationNegativeCallTest() {
100 var input = Query.of("Actual", (builder, p1) -> builder.clause((v1) -> List.of(
101 not(friend.call(p1, v1)),
102 friend.call(v1, p1)
103 ))).getDnf();
104 var actual = sut.lift(Modality.MUST, Concreteness.PARTIAL, input);
105
106 var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of(
107 not(ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, friend).call(p1, v1)),
108 ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, friend).call(v1, p1),
109 ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS_SYMBOL).call(v1)
110 ))).getDnf();
111
112 assertThat(actual, structurallyEqualTo(expected));
113 }
114
115 @Test
116 void liftPartialRelationQuantifiedNegativeCallTest() {
117 var input = Query.of("Actual", (builder, p1) -> builder.clause((v1) -> List.of(
118 person.call(p1),
119 not(friend.call(p1, v1))
120 ))).getDnf();
121 var actual = sut.lift(Modality.MAY, Concreteness.PARTIAL, input);
122
123 var helper = Query.of("Helper", (builder, p1, p2) -> builder.clause(
124 ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, friend).call(p1, p2),
125 ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS_SYMBOL).call(p2)
126 ));
127 var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of(
128 ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, person).call(p1),
129 not(helper.call(p1, v1))
130 ))).getDnf();
131
132 assertThat(actual, structurallyEqualTo(expected));
133 }
134
135 @Test
136 void liftSymbolViewQuantifiedNegativeCallTest() {
137 var input = Query.of("Actual", (builder, p1) -> builder.clause((v1) -> List.of(
138 person.call(p1),
139 not(friendMustView.call(p1, v1))
140 ))).getDnf();
141 var actual = sut.lift(Modality.MAY, Concreteness.PARTIAL, input);
142
143 var helper = Query.of("Helper", (builder, p1, p2) -> builder.clause(
144 friendMustView.call(p1, p2),
145 ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS_SYMBOL).call(p2)
146 ));
147 var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of(
148 ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, person).call(p1),
149 not(helper.call(p1, v1))
150 ))).getDnf();
151
152 assertThat(actual, structurallyEqualTo(expected));
153 }
154
155 @Test
156 void liftPartialRelationQuantifiedNegativeDiagonalCallTest() {
157 var input = Query.of("Actual", (builder) -> builder.clause((v1) -> List.of(
158 not(friend.call(v1, v1))
159 ))).getDnf();
160 var actual = sut.lift(Modality.MAY, Concreteness.PARTIAL, input);
161
162 var helper = Query.of("Helper", (builder, p1) -> builder.clause(
163 ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, friend).call(p1, p1),
164 ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS_SYMBOL).call(p1)
165 ));
166 var expected = Query.of("Expected", (builder) -> builder.clause((v1) -> List.of(
167 not(helper.call(v1))
168 ))).getDnf();
169
170 assertThat(actual, structurallyEqualTo(expected));
171 }
172
173 @Test
174 void liftPartialDnfQuantifiedNegativeInputCallTest() {
175 var called = Dnf.of("Called", builder -> {
176 var p1 = builder.parameter("p1", ParameterDirection.IN);
177 var p2 = builder.parameter("p2", ParameterDirection.OUT);
178 builder.clause(
179 friend.call(p1, p2),
180 friend.call(p2, p1)
181 );
182 });
183 var input = Query.of("Actual", (builder, p1) -> builder.clause((v1) -> List.of(
184 person.call(p1),
185 not(called.call(p1, v1))
186 ))).getDnf();
187 var actual = sut.lift(Modality.MAY, Concreteness.PARTIAL, input);
188
189 var helper = Dnf.of("Helper", builder -> {
190 var p1 = builder.parameter("p1", ParameterDirection.IN);
191 var p2 = builder.parameter("p2", ParameterDirection.OUT);
192 builder.clause(
193 ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, called).call(p1, p2),
194 ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS_SYMBOL).call(p2)
195 );
196 });
197 var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of(
198 ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, person).call(p1),
199 not(helper.call(p1, v1))
200 ))).getDnf();
201
202 assertThat(actual, structurallyEqualTo(expected));
203 }
204
205 @Test
206 void liftPartialRelationTransitiveCallTest() {
207 var input = Query.of("Actual", (builder, p1, p2)-> builder.clause(
208 friend.callTransitive(p1, p2),
209 not(person.call(p2))
210 )).getDnf();
211 var actual = sut.lift(Modality.MAY, Concreteness.PARTIAL, input);
212
213 var helper = Query.of("Helper", (builder, p1, p2) -> builder.clause(
214 ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, friend).call(p1, p2),
215 ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EXISTS_SYMBOL).call(p2)
216 ));
217 var helper2 = Query.of("Helper2", (builder, p1, p2) -> {
218 builder.clause(
219 ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, friend).call(p1, p2)
220 );
221 builder.clause((v1) -> List.of(
222 helper.callTransitive(p1, v1),
223 ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, friend).call(v1, p2)
224 ));
225 });
226 var expected = Query.of("Expected", (builder, p1, p2) -> builder.clause(
227 helper2.call(p1, p2),
228 not(ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, person).call(p2))
229 )).getDnf();
230
231 assertThat(actual, structurallyEqualTo(expected));
232 }
233
234 @Test
235 void liftPartialSymbolTransitiveCallTest() {
236 var input = Query.of("Actual", (builder, p1, p2)-> builder.clause(
237 friendMustView.callTransitive(p1, p2),
238 not(person.call(p2))
239 )).getDnf();
240 var actual = sut.lift(Modality.MAY, Concreteness.PARTIAL, input);
241
242 var endExistsHelper = Query.of("EndExistsHelper", (builder, p1, p2) -> builder.clause(
243 friendMustView.call(p1, p2),
244 ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EXISTS_SYMBOL).call(p2)
245 ));
246 var transitiveHelper = Query.of("TransitiveHelper", (builder, p1, p2) -> {
247 builder.clause(
248 friendMustView.call(p1, p2)
249 );
250 builder.clause((v1) -> List.of(
251 endExistsHelper.callTransitive(p1, v1),
252 friendMustView.call(v1, p2)
253 ));
254 });
255 var expected = Query.of("Expected", (builder, p1, p2) -> builder.clause(
256 transitiveHelper.call(p1, p2),
257 not(ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, person).call(p2))
258 )).getDnf();
259
260 assertThat(actual, structurallyEqualTo(expected));
261 }
262
263 @Test
264 void liftPartialRelationTransitiveCallExistsTest() {
265 var input = Query.of("Actual", (builder, p1) -> builder.clause((v1) -> List.of(
266 friend.callTransitive(p1, v1),
267 not(person.call(v1))
268 ))).getDnf();
269 var actual = sut.lift(Modality.MAY, Concreteness.PARTIAL, input);
270
271 var helper = Query.of("Helper", (builder, p1, p2) -> builder.clause(
272 ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, friend).call(p1, p2),
273 ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EXISTS_SYMBOL).call(p2)
274 ));
275 var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of(
276 helper.callTransitive(p1, v1),
277 not(ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, person).call(v1))
278 ))).getDnf();
279
280 assertThat(actual, structurallyEqualTo(expected));
281 }
282
283 @Test
284 void liftMultipleTransitiveCallExistsTest() {
285 var input = Query.of("Actual", (builder, p1) -> builder.clause((v1) -> List.of(
286 friend.callTransitive(p1, v1),
287 friendMustView.callTransitive(p1, v1),
288 not(person.call(v1))
289 ))).getDnf();
290 var actual = sut.lift(Modality.MAY, Concreteness.PARTIAL, input);
291
292 var helper = Query.of("Helper", (builder, p1, p2) -> builder.clause(
293 ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, friend).call(p1, p2),
294 ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EXISTS_SYMBOL).call(p2)
295 ));
296 var helper2 = Query.of("Helper2", (builder, p1, p2) -> builder.clause(
297 friendMustView.call(p1, p2),
298 ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EXISTS_SYMBOL).call(p2)
299 ));
300 var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of(
301 helper.callTransitive(p1, v1),
302 helper2.callTransitive(p1, v1),
303 not(ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, person).call(v1))
304 ))).getDnf();
305
306 assertThat(actual, structurallyEqualTo(expected));
307 }
308
309 @Test
310 void liftEquivalentTest() {
311 var input = Query.of("Actual", (builder, p1, p2) -> builder.clause(
312 p1.isEquivalent(p2),
313 person.call(p1)
314 )).getDnf();
315 var actual = sut.lift(Modality.MAY, Concreteness.PARTIAL, input);
316
317 var expected = Query.of("Expected", (builder, p1, p2) -> builder.clause(
318 ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, person).call(p1),
319 ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EQUALS_SYMBOL).call(p2, p1)
320 )).getDnf();
321
322 assertThat(actual, structurallyEqualTo(expected));
323 }
324
325 @Test
326 void liftNotEquivalentTest() {
327 var input = Query.of("Actual", (builder, p1, p2) -> builder.clause(
328 not(p1.isEquivalent(p2)),
329 friend.call(p1, p2)
330 )).getDnf();
331 var actual = sut.lift(Modality.MAY, Concreteness.PARTIAL, input);
332
333 var expected = Query.of("Expected", (builder, p1, p2) -> builder.clause(
334 ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, friend).call(p1, p2),
335 not(ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EQUALS_SYMBOL).call(p1, p2))
336 )).getDnf();
337
338 assertThat(actual, structurallyEqualTo(expected));
339 }
340
341 @Test
342 void liftConstantTest() {
343 var input = Query.of("Actual", (builder, p1) -> builder.clause((v1) -> List.of(
344 v1.isConstant(0),
345 friend.call(v1, p1)
346 ))).getDnf();
347 var actual = sut.lift(Modality.MAY, Concreteness.PARTIAL, input);
348
349 var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of(
350 v1.isConstant(0),
351 ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, friend).call(v1, p1),
352 ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EXISTS_SYMBOL).call(v1)
353 ))).getDnf();
354
355 assertThat(actual, structurallyEqualTo(expected));
356 }
357
358 @Test
359 void liftAssignTest() {
360 var input = Query.of("Actual", Integer.class, (builder, p1, output) -> builder
361 .clause(Integer.class, (d1) -> List.of(
362 person.call(p1),
363 ageView.call(p1, d1),
364 output.assign(mul(constant(2), d1))
365 ))).getDnf();
366 var actual = sut.lift(Modality.MAY, Concreteness.PARTIAL, input);
367
368 var expected = Query.of("Expected", Integer.class, (builder, p1, output) -> builder
369 .clause(Integer.class, (d1) -> List.of(
370 ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, person).call(p1),
371 ageView.call(p1, d1),
372 output.assign(mul(constant(2), d1))
373 ))).getDnf();
374
375 assertThat(actual, structurallyEqualTo(expected));
376 }
377
378 @Test
379 void liftCheckTest() {
380 var input = Query.of("Actual", (builder, p1) -> builder.clause(Integer.class, (d1) -> List.of(
381 person.call(p1),
382 ageView.call(p1, d1),
383 check(greaterEq(d1, constant(21)))
384 ))).getDnf();
385 var actual = sut.lift(Modality.MAY, Concreteness.CANDIDATE, input);
386
387 var expected = Query.of("Expected", (builder, p1) -> builder.clause(Integer.class, (d1) -> List.of(
388 ModalConstraint.of(Modality.MAY, Concreteness.CANDIDATE, person).call(p1),
389 ageView.call(p1, d1),
390 check(greaterEq(d1, constant(21)))
391 ))).getDnf();
392
393 assertThat(actual, structurallyEqualTo(expected));
394 }
395}
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-07-20 18:56:22 +0000