diff options
author | Kristóf Marussy <kristof@marussy.com> | 2023-06-25 22:15:32 +0200 |
---|---|---|
committer | Kristóf Marussy <kristof@marussy.com> | 2023-06-29 02:23:01 +0200 |
commit | f4408d1ec923fdf76e5755f1a7b0881ede3a4c12 (patch) | |
tree | 181a7775f405a3526cba308ccf965c8a12810b6c /subprojects/store-query/src | |
parent | refactor: query equality and hash code (diff) | |
download | refinery-f4408d1ec923fdf76e5755f1a7b0881ede3a4c12.tar.gz refinery-f4408d1ec923fdf76e5755f1a7b0881ede3a4c12.tar.zst refinery-f4408d1ec923fdf76e5755f1a7b0881ede3a4c12.zip |
feat: remove contradictory calls in Dnf builder
Diffstat (limited to 'subprojects/store-query/src')
2 files changed, 103 insertions, 3 deletions
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/ClausePostProcessor.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/ClausePostProcessor.java index 1a45c20a..f2749094 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/ClausePostProcessor.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/ClausePostProcessor.java | |||
@@ -6,9 +6,8 @@ | |||
6 | package tools.refinery.store.query.dnf; | 6 | package tools.refinery.store.query.dnf; |
7 | 7 | ||
8 | import org.jetbrains.annotations.NotNull; | 8 | import org.jetbrains.annotations.NotNull; |
9 | import tools.refinery.store.query.literal.BooleanLiteral; | 9 | import tools.refinery.store.query.Constraint; |
10 | import tools.refinery.store.query.literal.EquivalenceLiteral; | 10 | import tools.refinery.store.query.literal.*; |
11 | import tools.refinery.store.query.literal.Literal; | ||
12 | import tools.refinery.store.query.substitution.MapBasedSubstitution; | 11 | import tools.refinery.store.query.substitution.MapBasedSubstitution; |
13 | import tools.refinery.store.query.substitution.StatelessSubstitution; | 12 | import tools.refinery.store.query.substitution.StatelessSubstitution; |
14 | import tools.refinery.store.query.substitution.Substitution; | 13 | import tools.refinery.store.query.substitution.Substitution; |
@@ -58,6 +57,9 @@ class ClausePostProcessor { | |||
58 | if (filteredLiterals.isEmpty()) { | 57 | if (filteredLiterals.isEmpty()) { |
59 | return ConstantResult.ALWAYS_TRUE; | 58 | return ConstantResult.ALWAYS_TRUE; |
60 | } | 59 | } |
60 | if (hasContradictoryCall(filteredLiterals)) { | ||
61 | return ConstantResult.ALWAYS_FALSE; | ||
62 | } | ||
61 | var clause = new DnfClause(Collections.unmodifiableSet(positiveVariables), | 63 | var clause = new DnfClause(Collections.unmodifiableSet(positiveVariables), |
62 | Collections.unmodifiableList(filteredLiterals)); | 64 | Collections.unmodifiableList(filteredLiterals)); |
63 | return new ClauseResult(clause); | 65 | return new ClauseResult(clause); |
@@ -223,6 +225,55 @@ class ClausePostProcessor { | |||
223 | } | 225 | } |
224 | } | 226 | } |
225 | 227 | ||
228 | private boolean hasContradictoryCall(Collection<Literal> filteredLiterals) { | ||
229 | var positiveCalls = new HashMap<Constraint, Set<CallLiteral>>(); | ||
230 | for (var literal : filteredLiterals) { | ||
231 | if (literal instanceof CallLiteral callLiteral && callLiteral.getPolarity() == CallPolarity.POSITIVE) { | ||
232 | var callsOfTarget = positiveCalls.computeIfAbsent(callLiteral.getTarget(), key -> new HashSet<>()); | ||
233 | callsOfTarget.add(callLiteral); | ||
234 | } | ||
235 | } | ||
236 | for (var literal : filteredLiterals) { | ||
237 | if (literal instanceof CallLiteral callLiteral && callLiteral.getPolarity() == CallPolarity.NEGATIVE) { | ||
238 | var callsOfTarget = positiveCalls.get(callLiteral.getTarget()); | ||
239 | if (contradicts(callLiteral, callsOfTarget)) { | ||
240 | return true; | ||
241 | } | ||
242 | } | ||
243 | } | ||
244 | return false; | ||
245 | } | ||
246 | |||
247 | private boolean contradicts(CallLiteral negativeCall, Collection<CallLiteral> positiveCalls) { | ||
248 | if (positiveCalls == null) { | ||
249 | return false; | ||
250 | } | ||
251 | for (var positiveCall : positiveCalls) { | ||
252 | if (contradicts(negativeCall, positiveCall)) { | ||
253 | return true; | ||
254 | } | ||
255 | } | ||
256 | return false; | ||
257 | } | ||
258 | |||
259 | private boolean contradicts(CallLiteral negativeCall, CallLiteral positiveCall) { | ||
260 | var privateVariables = negativeCall.getPrivateVariables(positiveVariables); | ||
261 | var negativeArguments = negativeCall.getArguments(); | ||
262 | var positiveArguments = positiveCall.getArguments(); | ||
263 | int arity = negativeArguments.size(); | ||
264 | for (int i = 0; i < arity; i++) { | ||
265 | var negativeArgument = negativeArguments.get(i); | ||
266 | if (privateVariables.contains(negativeArgument)) { | ||
267 | continue; | ||
268 | } | ||
269 | var positiveArgument = positiveArguments.get(i); | ||
270 | if (!negativeArgument.equals(positiveArgument)) { | ||
271 | return false; | ||
272 | } | ||
273 | } | ||
274 | return true; | ||
275 | } | ||
276 | |||
226 | private class SortableLiteral implements Comparable<SortableLiteral> { | 277 | private class SortableLiteral implements Comparable<SortableLiteral> { |
227 | private final int index; | 278 | private final int index; |
228 | private final Literal literal; | 279 | private final Literal literal; |
diff --git a/subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/DnfBuilderLiteralEliminationTest.java b/subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/DnfBuilderLiteralEliminationTest.java index 9d9bf3c0..6a2dc0c7 100644 --- a/subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/DnfBuilderLiteralEliminationTest.java +++ b/subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/DnfBuilderLiteralEliminationTest.java | |||
@@ -207,4 +207,53 @@ class DnfBuilderLiteralEliminationTest { | |||
207 | 207 | ||
208 | assertThat(actual, structurallyEqualTo(expected)); | 208 | assertThat(actual, structurallyEqualTo(expected)); |
209 | } | 209 | } |
210 | |||
211 | @Test | ||
212 | void removeContradictoryTest() { | ||
213 | var actual = Dnf.of(builder -> builder.clause((p, q) -> List.of( | ||
214 | friendView.call(p, q), | ||
215 | not(friendView.call(p, q)) | ||
216 | ))); | ||
217 | var expected = Dnf.builder().build(); | ||
218 | |||
219 | assertThat(actual, structurallyEqualTo(expected)); | ||
220 | } | ||
221 | |||
222 | @Test | ||
223 | void removeContradictoryUniversalTest() { | ||
224 | var actual = Dnf.of(builder -> builder.clause((p, q) -> List.of( | ||
225 | friendView.call(q, q), | ||
226 | friendView.call(p, q), | ||
227 | not(friendView.call(p, Variable.of())) | ||
228 | ))); | ||
229 | var expected = Dnf.builder().build(); | ||
230 | |||
231 | assertThat(actual, structurallyEqualTo(expected)); | ||
232 | } | ||
233 | |||
234 | @Test | ||
235 | void removeContradictoryExistentialUniversalTest() { | ||
236 | var actual = Dnf.of(builder -> builder.clause((p) -> List.of( | ||
237 | friendView.call(p, Variable.of()), | ||
238 | not(friendView.call(p, Variable.of())) | ||
239 | ))); | ||
240 | var expected = Dnf.builder().build(); | ||
241 | |||
242 | assertThat(actual, structurallyEqualTo(expected)); | ||
243 | } | ||
244 | |||
245 | @Test | ||
246 | void removeContradictoryUniversalParameterTest() { | ||
247 | var actual = Dnf.of(builder -> { | ||
248 | var p = builder.parameter("p"); | ||
249 | builder.clause((q) -> List.of( | ||
250 | friendView.call(q, q), | ||
251 | friendView.call(p, q), | ||
252 | not(friendView.call(p, Variable.of())) | ||
253 | )); | ||
254 | }); | ||
255 | var expected = Dnf.builder().parameter(p).build(); | ||
256 | |||
257 | assertThat(actual, structurallyEqualTo(expected)); | ||
258 | } | ||
210 | } | 259 | } |