blob: 87d07187921b4b1b8f1c8f29484c98804eac51fb (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
|
/*
* SPDX-FileCopyrightText: 2023-2024 The Refinery Authors <https://refinery.tools/>
*
* SPDX-License-Identifier: EPL-2.0
*/
package tools.refinery.logic.dnf;
import tools.refinery.logic.InvalidQueryException;
import tools.refinery.logic.equality.DnfEqualityChecker;
import tools.refinery.logic.equality.SubstitutingLiteralEqualityHelper;
import tools.refinery.logic.equality.SubstitutingLiteralHashCodeHelper;
import tools.refinery.logic.literal.Literal;
import tools.refinery.logic.term.ParameterDirection;
import tools.refinery.logic.term.Variable;
import java.util.*;
class DnfPostProcessor {
private final List<SymbolicParameter> parameters;
private final List<List<Literal>> clauses;
public DnfPostProcessor(List<SymbolicParameter> parameters, List<List<Literal>> clauses) {
this.parameters = parameters;
this.clauses = clauses;
}
public List<DnfClause> postProcessClauses() {
var parameterInfoMap = getParameterInfoMap();
var postProcessedClauses = LinkedHashSet.<CanonicalClause>newLinkedHashSet(clauses.size());
int index = 0;
for (var literals : clauses) {
var postProcessor = new ClausePostProcessor(parameterInfoMap, literals);
ClausePostProcessor.Result result;
try {
result = postProcessor.postProcessClause();
} catch (InvalidQueryException e) {
throw new InvalidClauseException(index, e);
}
if (result instanceof ClausePostProcessor.ClauseResult clauseResult) {
postProcessedClauses.add(new CanonicalClause(clauseResult.clause()));
} else if (result instanceof ClausePostProcessor.ConstantResult constantResult) {
switch (constantResult) {
case ALWAYS_TRUE -> {
var inputVariables = getInputVariables();
return List.of(new DnfClause(inputVariables, List.of()));
}
case ALWAYS_FALSE -> {
// Skip this clause because it can never match.
}
default -> throw new IllegalStateException("Unexpected ClausePostProcessor.ConstantResult: " +
constantResult);
}
} else {
throw new IllegalStateException("Unexpected ClausePostProcessor.Result: " + result);
}
index++;
}
return postProcessedClauses.stream().map(CanonicalClause::getDnfClause).toList();
}
private Map<Variable, ClausePostProcessor.ParameterInfo> getParameterInfoMap() {
var mutableParameterInfoMap = new LinkedHashMap<Variable, ClausePostProcessor.ParameterInfo>();
int arity = parameters.size();
for (int i = 0; i < arity; i++) {
var parameter = parameters.get(i);
mutableParameterInfoMap.put(parameter.getVariable(),
new ClausePostProcessor.ParameterInfo(parameter.getDirection(), i));
}
return Collections.unmodifiableMap(mutableParameterInfoMap);
}
private Set<Variable> getInputVariables() {
var inputParameters = new LinkedHashSet<Variable>();
for (var parameter : parameters) {
if (parameter.getDirection() == ParameterDirection.IN) {
inputParameters.add(parameter.getVariable());
}
}
return Collections.unmodifiableSet(inputParameters);
}
private class CanonicalClause {
private final DnfClause dnfClause;
public CanonicalClause(DnfClause dnfClause) {
this.dnfClause = dnfClause;
}
public DnfClause getDnfClause() {
return dnfClause;
}
@Override
public boolean equals(Object obj) {
if (this == obj) {
return true;
}
if (obj == null || getClass() != obj.getClass()) {
return false;
}
var otherCanonicalClause = (CanonicalClause) obj;
var helper = new SubstitutingLiteralEqualityHelper(DnfEqualityChecker.DEFAULT, parameters, parameters);
return dnfClause.equalsWithSubstitution(helper, otherCanonicalClause.dnfClause);
}
@Override
public int hashCode() {
var helper = new SubstitutingLiteralHashCodeHelper(parameters);
return dnfClause.hashCodeWithSubstitution(helper);
}
}
}
|
