diff options
Diffstat (limited to 'subprojects/store-query/src/main')
-rw-r--r-- | subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/ClausePostProcessor.java | 57 |
1 files changed, 54 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; |