aboutsummaryrefslogtreecommitdiffstats
path: root/subprojects/logic/src/test/java/tools/refinery/logic/dnf/DnfBuilderLiteralEliminationTest.java
diff options
context:
space:
mode:
authorLibravatar Kristóf Marussy <kristof@marussy.com>2024-03-07 22:10:42 +0100
committerLibravatar Kristóf Marussy <kristof@marussy.com>2024-04-07 14:55:46 +0200
commit16a9b534adec2c53b50f92a43c1623918b1c59c0 (patch)
tree690b299a2ca31e302ddad219a7aa94bcf86d5d0b /subprojects/logic/src/test/java/tools/refinery/logic/dnf/DnfBuilderLiteralEliminationTest.java
parentfix(frontend): * operator highlighting (diff)
downloadrefinery-16a9b534adec2c53b50f92a43c1623918b1c59c0.tar.gz
refinery-16a9b534adec2c53b50f92a43c1623918b1c59c0.tar.zst
refinery-16a9b534adec2c53b50f92a43c1623918b1c59c0.zip
refactor: move terms and DNF into logic subproject
Diffstat (limited to 'subprojects/logic/src/test/java/tools/refinery/logic/dnf/DnfBuilderLiteralEliminationTest.java')
-rw-r--r--subprojects/logic/src/test/java/tools/refinery/logic/dnf/DnfBuilderLiteralEliminationTest.java257
1 files changed, 257 insertions, 0 deletions
diff --git a/subprojects/logic/src/test/java/tools/refinery/logic/dnf/DnfBuilderLiteralEliminationTest.java b/subprojects/logic/src/test/java/tools/refinery/logic/dnf/DnfBuilderLiteralEliminationTest.java
new file mode 100644
index 00000000..d5a9ccad
--- /dev/null
+++ b/subprojects/logic/src/test/java/tools/refinery/logic/dnf/DnfBuilderLiteralEliminationTest.java
@@ -0,0 +1,257 @@
1/*
2 * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
3 *
4 * SPDX-License-Identifier: EPL-2.0
5 */
6package tools.refinery.logic.dnf;
7
8import org.junit.jupiter.api.Test;
9import org.junit.jupiter.params.ParameterizedTest;
10import org.junit.jupiter.params.provider.CsvSource;
11import tools.refinery.logic.Constraint;
12import tools.refinery.logic.literal.BooleanLiteral;
13import tools.refinery.logic.term.NodeVariable;
14import tools.refinery.logic.term.ParameterDirection;
15import tools.refinery.logic.term.Variable;
16import tools.refinery.logic.term.bool.BoolTerms;
17import tools.refinery.logic.tests.FakeKeyOnlyView;
18
19import java.util.List;
20
21import static org.hamcrest.MatcherAssert.assertThat;
22import static tools.refinery.logic.literal.Literals.check;
23import static tools.refinery.logic.literal.Literals.not;
24import static tools.refinery.logic.tests.QueryMatchers.structurallyEqualTo;
25
26class DnfBuilderLiteralEliminationTest {
27 private final Constraint friendView = new FakeKeyOnlyView("friend", 2);
28 private final NodeVariable p = Variable.of("p");
29 private final NodeVariable q = Variable.of("q");
30 private final Dnf trueDnf = Dnf.builder().parameter(p, ParameterDirection.IN).clause().build();
31 private final Dnf falseDnf = Dnf.builder().parameter(p).build();
32
33 @Test
34 void eliminateTrueTest() {
35 var actual = Dnf.builder()
36 .parameters(p, q)
37 .clause(BooleanLiteral.TRUE, friendView.call(p, q))
38 .build();
39 var expected = Dnf.builder().parameters(p, q).clause(friendView.call(p, q)).build();
40
41 assertThat(actual, structurallyEqualTo(expected));
42 }
43
44 @Test
45 void eliminateTrueAssumptionTest() {
46 var actual = Dnf.builder()
47 .parameters(p, q)
48 .clause(check(BoolTerms.constant(true)), friendView.call(p, q))
49 .build();
50 var expected = Dnf.builder().parameters(p, q).clause(friendView.call(p, q)).build();
51
52 assertThat(actual, structurallyEqualTo(expected));
53 }
54
55 @Test
56 void eliminateFalseTest() {
57 var actual = Dnf.builder()
58 .parameters(p, q)
59 .clause(friendView.call(p, q))
60 .clause(friendView.call(q, p), BooleanLiteral.FALSE)
61 .build();
62 var expected = Dnf.builder().parameters(p, q).clause(friendView.call(p, q)).build();
63
64 assertThat(actual, structurallyEqualTo(expected));
65 }
66
67 @ParameterizedTest
68 @CsvSource(value = {
69 "false",
70 "null"
71 }, nullValues = "null")
72 void eliminateFalseAssumptionTest(Boolean value) {
73 var actual = Dnf.builder()
74 .parameters(p, q)
75 .clause(friendView.call(p, q))
76 .clause(friendView.call(q, p), check(BoolTerms.constant(value)))
77 .build();
78 var expected = Dnf.builder().parameters(p, q).clause(friendView.call(p, q)).build();
79
80 assertThat(actual, structurallyEqualTo(expected));
81 }
82
83 @Test
84 void alwaysTrueTest() {
85 var actual = Dnf.builder()
86 .parameters(List.of(p, q), ParameterDirection.IN)
87 .clause(friendView.call(p, q))
88 .clause(BooleanLiteral.TRUE)
89 .build();
90 var expected = Dnf.builder().parameters(List.of(p, q), ParameterDirection.IN).clause().build();
91
92 assertThat(actual, structurallyEqualTo(expected));
93 }
94
95 @Test
96 void alwaysFalseTest() {
97 var actual = Dnf.builder()
98 .parameters(p, q)
99 .clause(friendView.call(p, q), BooleanLiteral.FALSE)
100 .build();
101 var expected = Dnf.builder().parameters(p, q).build();
102
103 assertThat(actual, structurallyEqualTo(expected));
104 }
105
106 @Test
107 void eliminateTrueDnfTest() {
108 var actual = Dnf.builder()
109 .parameters(p, q)
110 .clause(trueDnf.call(q), friendView.call(p, q))
111 .build();
112 var expected = Dnf.builder().parameters(p, q).clause(friendView.call(p, q)).build();
113
114 assertThat(actual, structurallyEqualTo(expected));
115 }
116
117 @Test
118 void eliminateFalseDnfTest() {
119 var actual = Dnf.builder()
120 .parameters(p, q)
121 .clause(friendView.call(p, q))
122 .clause(friendView.call(q, p), falseDnf.call(q))
123 .build();
124 var expected = Dnf.builder().parameters(p, q).clause(friendView.call(p, q)).build();
125
126 assertThat(actual, structurallyEqualTo(expected));
127 }
128
129 @Test
130 void alwaysTrueDnfTest() {
131 var actual = Dnf.builder()
132 .parameters(List.of(p, q), ParameterDirection.IN)
133 .clause(friendView.call(p, q))
134 .clause(trueDnf.call(q))
135 .build();
136 var expected = Dnf.builder().parameters(List.of(p, q), ParameterDirection.IN).clause().build();
137
138 assertThat(actual, structurallyEqualTo(expected));
139 }
140
141 @Test
142 void alwaysFalseDnfTest() {
143 var actual = Dnf.builder()
144 .parameters(p, q)
145 .clause(friendView.call(p, q), falseDnf.call(q))
146 .build();
147 var expected = Dnf.builder().parameters(p, q).build();
148
149 assertThat(actual, structurallyEqualTo(expected));
150 }
151
152 @Test
153 void eliminateNotFalseDnfTest() {
154 var actual = Dnf.builder()
155 .parameters(p, q)
156 .clause(not(falseDnf.call(q)), friendView.call(p, q))
157 .build();
158 var expected = Dnf.builder().parameters(p, q).clause(friendView.call(p, q)).build();
159
160 assertThat(actual, structurallyEqualTo(expected));
161 }
162
163 @Test
164 void eliminateNotTrueDnfTest() {
165 var actual = Dnf.builder()
166 .parameters(p, q)
167 .clause(friendView.call(p, q))
168 .clause(friendView.call(q, p), not(trueDnf.call(q)))
169 .build();
170 var expected = Dnf.builder().parameters(p, q).clause(friendView.call(p, q)).build();
171
172 assertThat(actual, structurallyEqualTo(expected));
173 }
174
175 @Test
176 void alwaysNotFalseDnfTest() {
177 var actual = Dnf.builder()
178 .parameters(List.of(p, q), ParameterDirection.IN)
179 .clause(friendView.call(p, q))
180 .clause(not(falseDnf.call(q)))
181 .build();
182 var expected = Dnf.builder().parameters(List.of(p, q), ParameterDirection.IN).clause().build();
183
184 assertThat(actual, structurallyEqualTo(expected));
185 }
186
187 @Test
188 void alwaysNotTrueDnfTest() {
189 var actual = Dnf.builder()
190 .parameters(p, q)
191 .clause(friendView.call(p, q), not(trueDnf.call(q)))
192 .build();
193 var expected = Dnf.builder().parameters(p, q).build();
194
195 assertThat(actual, structurallyEqualTo(expected));
196 }
197
198 @Test
199 void removeDuplicateTest() {
200 var actual = Dnf.of(builder -> builder.clause((p, q) -> List.of(
201 friendView.call(p, q),
202 friendView.call(p, q)
203 )));
204 var expected = Dnf.of(builder -> builder.clause((p, q) -> List.of(friendView.call(p, q))));
205
206 assertThat(actual, structurallyEqualTo(expected));
207 }
208
209 @Test
210 void removeContradictoryTest() {
211 var actual = Dnf.of(builder -> builder.clause((p, q) -> List.of(
212 friendView.call(p, q),
213 not(friendView.call(p, q))
214 )));
215 var expected = Dnf.builder().build();
216
217 assertThat(actual, structurallyEqualTo(expected));
218 }
219
220 @Test
221 void removeContradictoryUniversalTest() {
222 var actual = Dnf.of(builder -> builder.clause((p, q) -> List.of(
223 friendView.call(q, q),
224 friendView.call(p, q),
225 not(friendView.call(p, Variable.of()))
226 )));
227 var expected = Dnf.builder().build();
228
229 assertThat(actual, structurallyEqualTo(expected));
230 }
231
232 @Test
233 void removeContradictoryExistentialUniversalTest() {
234 var actual = Dnf.of(builder -> builder.clause((p) -> List.of(
235 friendView.call(p, Variable.of()),
236 not(friendView.call(p, Variable.of()))
237 )));
238 var expected = Dnf.builder().build();
239
240 assertThat(actual, structurallyEqualTo(expected));
241 }
242
243 @Test
244 void removeContradictoryUniversalParameterTest() {
245 var actual = Dnf.of(builder -> {
246 var p = builder.parameter("p");
247 builder.clause((q) -> List.of(
248 friendView.call(q, q),
249 friendView.call(p, q),
250 not(friendView.call(p, Variable.of()))
251 ));
252 });
253 var expected = Dnf.builder().parameter(p).build();
254
255 assertThat(actual, structurallyEqualTo(expected));
256 }
257}
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-06-30 05:50:19 +0000