blob: ca47e979b4267b05e457083e425633386e8bf289 (
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
113
114
115
|
package tools.refinery.store.query;
import tools.refinery.store.query.literal.Literal;
import java.util.*;
@SuppressWarnings("UnusedReturnValue")
public class DnfBuilder {
private final String name;
private final List<Variable> parameters = new ArrayList<>();
private final List<FunctionalDependency<Variable>> functionalDependencies = new ArrayList<>();
private final List<List<Literal>> clauses = new ArrayList<>();
DnfBuilder(String name) {
this.name = name;
}
public DnfBuilder parameter(Variable variable) {
parameters.add(variable);
return this;
}
public DnfBuilder parameters(Variable... variables) {
return parameters(List.of(variables));
}
public DnfBuilder parameters(Collection<Variable> variables) {
parameters.addAll(variables);
return this;
}
public DnfBuilder functionalDependencies(Collection<FunctionalDependency<Variable>> functionalDependencies) {
this.functionalDependencies.addAll(functionalDependencies);
return this;
}
public DnfBuilder functionalDependency(FunctionalDependency<Variable> functionalDependency) {
functionalDependencies.add(functionalDependency);
return this;
}
public DnfBuilder functionalDependency(Set<Variable> forEach, Set<Variable> unique) {
return functionalDependency(new FunctionalDependency<>(forEach, unique));
}
public DnfBuilder clause(Literal... literals) {
clause(List.of(literals));
return this;
}
public DnfBuilder clause(Collection<Literal> literals) {
// Remove duplicates by using a hashed data structure.
var filteredLiterals = new LinkedHashSet<Literal>(literals.size());
for (var literal : literals) {
var reduction = literal.getReduction();
switch (reduction) {
case NOT_REDUCIBLE -> filteredLiterals.add(literal);
case ALWAYS_TRUE -> {
// Literals reducible to {@code true} can be omitted, because the model is always assumed to have at
// least on object.
}
case ALWAYS_FALSE -> {
// Clauses with {@code false} literals can be omitted entirely.
return this;
}
default -> throw new IllegalArgumentException("Invalid reduction: " + reduction);
}
}
clauses.add(List.copyOf(filteredLiterals));
return this;
}
public DnfBuilder clause(DnfClause clause) {
return clause(clause.literals());
}
public DnfBuilder clauses(DnfClause... clauses) {
return clauses(List.of(clauses));
}
public DnfBuilder clauses(Collection<DnfClause> clauses) {
for (var clause : clauses) {
this.clause(clause);
}
return this;
}
public Dnf build() {
var postProcessedClauses = postProcessClauses();
return new Dnf(name, Collections.unmodifiableList(parameters),
Collections.unmodifiableList(functionalDependencies),
Collections.unmodifiableList(postProcessedClauses));
}
private List<DnfClause> postProcessClauses() {
var postProcessedClauses = new ArrayList<DnfClause>(clauses.size());
for (var literals : clauses) {
if (literals.isEmpty()) {
// Predicate will always match, the other clauses are irrelevant.
return List.of(new DnfClause(Set.of(), List.of()));
}
var variables = new HashSet<Variable>();
for (var constraint : literals) {
constraint.collectAllVariables(variables);
}
parameters.forEach(variables::remove);
postProcessedClauses.add(new DnfClause(Collections.unmodifiableSet(variables),
Collections.unmodifiableList(literals)));
}
return postProcessedClauses;
}
}
|