diff options
author | Kristóf Marussy <kristof@marussy.com> | 2023-02-24 20:21:15 +0100 |
---|---|---|
committer | Kristóf Marussy <kristof@marussy.com> | 2023-02-24 23:29:49 +0100 |
commit | f8a3c575e400259a4985233c07b7a50e5d4d82c5 (patch) | |
tree | f5975a19fcce28eba17b5af8adde5a37ddba83c6 /subprojects/store-query | |
parent | refactor: split query and partial from store (diff) | |
download | refinery-f8a3c575e400259a4985233c07b7a50e5d4d82c5.tar.gz refinery-f8a3c575e400259a4985233c07b7a50e5d4d82c5.tar.zst refinery-f8a3c575e400259a4985233c07b7a50e5d4d82c5.zip |
feat: Dnf reduction and structural equality
Diffstat (limited to 'subprojects/store-query')
30 files changed, 1068 insertions, 58 deletions
diff --git a/subprojects/store-query/build.gradle b/subprojects/store-query/build.gradle index 2b76e608..97761936 100644 --- a/subprojects/store-query/build.gradle +++ b/subprojects/store-query/build.gradle | |||
@@ -1,7 +1,9 @@ | |||
1 | plugins { | 1 | plugins { |
2 | id 'refinery-java-library' | 2 | id 'refinery-java-library' |
3 | id 'refinery-java-test-fixtures' | ||
3 | } | 4 | } |
4 | 5 | ||
5 | dependencies { | 6 | dependencies { |
6 | api project(':refinery-store') | 7 | api project(':refinery-store') |
8 | testFixturesApi libs.hamcrest | ||
7 | } | 9 | } |
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/Dnf.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/Dnf.java index 760b264b..b6744b50 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/Dnf.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/Dnf.java | |||
@@ -1,5 +1,7 @@ | |||
1 | package tools.refinery.store.query; | 1 | package tools.refinery.store.query; |
2 | 2 | ||
3 | import tools.refinery.store.query.equality.DnfEqualityChecker; | ||
4 | import tools.refinery.store.query.equality.LiteralEqualityHelper; | ||
3 | import tools.refinery.store.query.literal.CallPolarity; | 5 | import tools.refinery.store.query.literal.CallPolarity; |
4 | import tools.refinery.store.query.literal.DnfCallLiteral; | 6 | import tools.refinery.store.query.literal.DnfCallLiteral; |
5 | import tools.refinery.store.query.literal.LiteralReduction; | 7 | import tools.refinery.store.query.literal.LiteralReduction; |
@@ -7,6 +9,8 @@ import tools.refinery.store.query.literal.LiteralReduction; | |||
7 | import java.util.*; | 9 | import java.util.*; |
8 | 10 | ||
9 | public final class Dnf implements RelationLike { | 11 | public final class Dnf implements RelationLike { |
12 | private static final String INDENTATION = " "; | ||
13 | |||
10 | private final String name; | 14 | private final String name; |
11 | 15 | ||
12 | private final String uniqueName; | 16 | private final String uniqueName; |
@@ -50,7 +54,11 @@ public final class Dnf implements RelationLike { | |||
50 | 54 | ||
51 | @Override | 55 | @Override |
52 | public String name() { | 56 | public String name() { |
53 | return name; | 57 | return name == null ? uniqueName : name; |
58 | } | ||
59 | |||
60 | public boolean isExplicitlyNamed() { | ||
61 | return name == null; | ||
54 | } | 62 | } |
55 | 63 | ||
56 | public String getUniqueName() { | 64 | public String getUniqueName() { |
@@ -102,6 +110,61 @@ public final class Dnf implements RelationLike { | |||
102 | return call(CallPolarity.TRANSITIVE, List.of(left, right)); | 110 | return call(CallPolarity.TRANSITIVE, List.of(left, right)); |
103 | } | 111 | } |
104 | 112 | ||
113 | public boolean equalsWithSubstitution(DnfEqualityChecker callEqualityChecker, Dnf other) { | ||
114 | if (arity() != other.arity()) { | ||
115 | return false; | ||
116 | } | ||
117 | int numClauses = clauses.size(); | ||
118 | if (numClauses != other.clauses.size()) { | ||
119 | return false; | ||
120 | } | ||
121 | for (int i = 0; i < numClauses; i++) { | ||
122 | var literalEqualityHelper = new LiteralEqualityHelper(callEqualityChecker, parameters, other.parameters); | ||
123 | if (!clauses.get(i).equalsWithSubstitution(literalEqualityHelper, other.clauses.get(i))) { | ||
124 | return false; | ||
125 | } | ||
126 | } | ||
127 | return true; | ||
128 | } | ||
129 | |||
130 | @Override | ||
131 | public String toString() { | ||
132 | var builder = new StringBuilder(); | ||
133 | builder.append("pred ").append(name()).append("("); | ||
134 | var parameterIterator = parameters.iterator(); | ||
135 | if (parameterIterator.hasNext()) { | ||
136 | builder.append(parameterIterator.next()); | ||
137 | while (parameterIterator.hasNext()) { | ||
138 | builder.append(", ").append(parameterIterator.next()); | ||
139 | } | ||
140 | } | ||
141 | builder.append(") <->"); | ||
142 | var clauseIterator = clauses.iterator(); | ||
143 | if (clauseIterator.hasNext()) { | ||
144 | appendClause(clauseIterator.next(), builder); | ||
145 | while (clauseIterator.hasNext()) { | ||
146 | builder.append("\n;"); | ||
147 | appendClause(clauseIterator.next(), builder); | ||
148 | } | ||
149 | } else { | ||
150 | builder.append("\n").append(INDENTATION).append("<no clauses>"); | ||
151 | } | ||
152 | builder.append(".\n"); | ||
153 | return builder.toString(); | ||
154 | } | ||
155 | |||
156 | private static void appendClause(DnfClause clause, StringBuilder builder) { | ||
157 | var iterator = clause.literals().iterator(); | ||
158 | if (!iterator.hasNext()) { | ||
159 | builder.append("\n").append(INDENTATION).append("<empty>"); | ||
160 | return; | ||
161 | } | ||
162 | builder.append("\n").append(INDENTATION).append(iterator.next()); | ||
163 | while (iterator.hasNext()) { | ||
164 | builder.append(",\n").append(INDENTATION).append(iterator.next()); | ||
165 | } | ||
166 | } | ||
167 | |||
105 | public static DnfBuilder builder() { | 168 | public static DnfBuilder builder() { |
106 | return builder(null); | 169 | return builder(null); |
107 | } | 170 | } |
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfBuilder.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfBuilder.java index b18b5177..ca47e979 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfBuilder.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfBuilder.java | |||
@@ -52,7 +52,8 @@ public class DnfBuilder { | |||
52 | } | 52 | } |
53 | 53 | ||
54 | public DnfBuilder clause(Collection<Literal> literals) { | 54 | public DnfBuilder clause(Collection<Literal> literals) { |
55 | var filteredLiterals = new ArrayList<Literal>(literals.size()); | 55 | // Remove duplicates by using a hashed data structure. |
56 | var filteredLiterals = new LinkedHashSet<Literal>(literals.size()); | ||
56 | for (var literal : literals) { | 57 | for (var literal : literals) { |
57 | var reduction = literal.getReduction(); | 58 | var reduction = literal.getReduction(); |
58 | switch (reduction) { | 59 | switch (reduction) { |
@@ -65,10 +66,10 @@ public class DnfBuilder { | |||
65 | // Clauses with {@code false} literals can be omitted entirely. | 66 | // Clauses with {@code false} literals can be omitted entirely. |
66 | return this; | 67 | return this; |
67 | } | 68 | } |
68 | default -> throw new IllegalStateException("Invalid reduction %s".formatted(reduction)); | 69 | default -> throw new IllegalArgumentException("Invalid reduction: " + reduction); |
69 | } | 70 | } |
70 | } | 71 | } |
71 | clauses.add(Collections.unmodifiableList(filteredLiterals)); | 72 | clauses.add(List.copyOf(filteredLiterals)); |
72 | return this; | 73 | return this; |
73 | } | 74 | } |
74 | 75 | ||
@@ -77,10 +78,7 @@ public class DnfBuilder { | |||
77 | } | 78 | } |
78 | 79 | ||
79 | public DnfBuilder clauses(DnfClause... clauses) { | 80 | public DnfBuilder clauses(DnfClause... clauses) { |
80 | for (var clause : clauses) { | 81 | return clauses(List.of(clauses)); |
81 | this.clause(clause); | ||
82 | } | ||
83 | return this; | ||
84 | } | 82 | } |
85 | 83 | ||
86 | public DnfBuilder clauses(Collection<DnfClause> clauses) { | 84 | public DnfBuilder clauses(Collection<DnfClause> clauses) { |
@@ -91,18 +89,27 @@ public class DnfBuilder { | |||
91 | } | 89 | } |
92 | 90 | ||
93 | public Dnf build() { | 91 | public Dnf build() { |
92 | var postProcessedClauses = postProcessClauses(); | ||
93 | return new Dnf(name, Collections.unmodifiableList(parameters), | ||
94 | Collections.unmodifiableList(functionalDependencies), | ||
95 | Collections.unmodifiableList(postProcessedClauses)); | ||
96 | } | ||
97 | |||
98 | private List<DnfClause> postProcessClauses() { | ||
94 | var postProcessedClauses = new ArrayList<DnfClause>(clauses.size()); | 99 | var postProcessedClauses = new ArrayList<DnfClause>(clauses.size()); |
95 | for (var constraints : clauses) { | 100 | for (var literals : clauses) { |
101 | if (literals.isEmpty()) { | ||
102 | // Predicate will always match, the other clauses are irrelevant. | ||
103 | return List.of(new DnfClause(Set.of(), List.of())); | ||
104 | } | ||
96 | var variables = new HashSet<Variable>(); | 105 | var variables = new HashSet<Variable>(); |
97 | for (var constraint : constraints) { | 106 | for (var constraint : literals) { |
98 | constraint.collectAllVariables(variables); | 107 | constraint.collectAllVariables(variables); |
99 | } | 108 | } |
100 | parameters.forEach(variables::remove); | 109 | parameters.forEach(variables::remove); |
101 | postProcessedClauses.add(new DnfClause(Collections.unmodifiableSet(variables), | 110 | postProcessedClauses.add(new DnfClause(Collections.unmodifiableSet(variables), |
102 | Collections.unmodifiableList(constraints))); | 111 | Collections.unmodifiableList(literals))); |
103 | } | 112 | } |
104 | return new Dnf(name, Collections.unmodifiableList(parameters), | 113 | return postProcessedClauses; |
105 | Collections.unmodifiableList(functionalDependencies), | ||
106 | Collections.unmodifiableList(postProcessedClauses)); | ||
107 | } | 114 | } |
108 | } | 115 | } |
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfClause.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfClause.java index 2ba6becc..c6e8b8c9 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfClause.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfClause.java | |||
@@ -1,9 +1,22 @@ | |||
1 | package tools.refinery.store.query; | 1 | package tools.refinery.store.query; |
2 | 2 | ||
3 | import tools.refinery.store.query.equality.LiteralEqualityHelper; | ||
3 | import tools.refinery.store.query.literal.Literal; | 4 | import tools.refinery.store.query.literal.Literal; |
4 | 5 | ||
5 | import java.util.List; | 6 | import java.util.List; |
6 | import java.util.Set; | 7 | import java.util.Set; |
7 | 8 | ||
8 | public record DnfClause(Set<Variable> quantifiedVariables, List<Literal> literals) { | 9 | public record DnfClause(Set<Variable> quantifiedVariables, List<Literal> literals) { |
10 | public boolean equalsWithSubstitution(LiteralEqualityHelper helper, DnfClause other) { | ||
11 | int size = literals.size(); | ||
12 | if (size != other.literals.size()) { | ||
13 | return false; | ||
14 | } | ||
15 | for (int i = 0; i < size; i++) { | ||
16 | if (!literals.get(i).equalsWithSubstitution(helper, other.literals.get(i))) { | ||
17 | return false; | ||
18 | } | ||
19 | } | ||
20 | return true; | ||
21 | } | ||
9 | } | 22 | } |
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfUtils.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfUtils.java index 17564d43..c7a2849c 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfUtils.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfUtils.java | |||
@@ -1,6 +1,5 @@ | |||
1 | package tools.refinery.store.query; | 1 | package tools.refinery.store.query; |
2 | 2 | ||
3 | import java.util.Map; | ||
4 | import java.util.UUID; | 3 | import java.util.UUID; |
5 | 4 | ||
6 | public final class DnfUtils { | 5 | public final class DnfUtils { |
@@ -17,8 +16,4 @@ public final class DnfUtils { | |||
17 | return originalName + uniqueString; | 16 | return originalName + uniqueString; |
18 | } | 17 | } |
19 | } | 18 | } |
20 | |||
21 | public static Variable maybeSubstitute(Variable variable, Map<Variable, Variable> substitution) { | ||
22 | return substitution.getOrDefault(variable, variable); | ||
23 | } | ||
24 | } | 19 | } |
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/EmptyResultSet.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/EmptyResultSet.java new file mode 100644 index 00000000..a01a5a2f --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/EmptyResultSet.java | |||
@@ -0,0 +1,49 @@ | |||
1 | package tools.refinery.store.query; | ||
2 | |||
3 | import tools.refinery.store.tuple.Tuple; | ||
4 | import tools.refinery.store.tuple.TupleLike; | ||
5 | |||
6 | import java.util.Optional; | ||
7 | import java.util.stream.Stream; | ||
8 | |||
9 | public class EmptyResultSet implements ResultSet { | ||
10 | @Override | ||
11 | public boolean hasResult() { | ||
12 | return false; | ||
13 | } | ||
14 | |||
15 | @Override | ||
16 | public boolean hasResult(Tuple parameters) { | ||
17 | return false; | ||
18 | } | ||
19 | |||
20 | @Override | ||
21 | public Optional<TupleLike> oneResult() { | ||
22 | return Optional.empty(); | ||
23 | } | ||
24 | |||
25 | @Override | ||
26 | public Optional<TupleLike> oneResult(Tuple parameters) { | ||
27 | return Optional.empty(); | ||
28 | } | ||
29 | |||
30 | @Override | ||
31 | public Stream<TupleLike> allResults() { | ||
32 | return Stream.of(); | ||
33 | } | ||
34 | |||
35 | @Override | ||
36 | public Stream<TupleLike> allResults(Tuple parameters) { | ||
37 | return Stream.of(); | ||
38 | } | ||
39 | |||
40 | @Override | ||
41 | public int countResults() { | ||
42 | return 0; | ||
43 | } | ||
44 | |||
45 | @Override | ||
46 | public int countResults(Tuple parameters) { | ||
47 | return 0; | ||
48 | } | ||
49 | } | ||
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/Variable.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/Variable.java index 2eb87649..d0e0dead 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/Variable.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/Variable.java | |||
@@ -20,15 +20,15 @@ public class Variable { | |||
20 | 20 | ||
21 | } | 21 | } |
22 | public String getName() { | 22 | public String getName() { |
23 | return name; | 23 | return name == null ? uniqueName : name; |
24 | } | 24 | } |
25 | 25 | ||
26 | public String getUniqueName() { | 26 | public boolean isExplicitlyNamed() { |
27 | return uniqueName; | 27 | return name != null; |
28 | } | 28 | } |
29 | 29 | ||
30 | public boolean isNamed() { | 30 | public String getUniqueName() { |
31 | return name != null; | 31 | return uniqueName; |
32 | } | 32 | } |
33 | 33 | ||
34 | public ConstantLiteral isConstant(int value) { | 34 | public ConstantLiteral isConstant(int value) { |
@@ -44,6 +44,11 @@ public class Variable { | |||
44 | } | 44 | } |
45 | 45 | ||
46 | @Override | 46 | @Override |
47 | public String toString() { | ||
48 | return getName(); | ||
49 | } | ||
50 | |||
51 | @Override | ||
47 | public boolean equals(Object o) { | 52 | public boolean equals(Object o) { |
48 | if (this == o) return true; | 53 | if (this == o) return true; |
49 | if (o == null || getClass() != o.getClass()) return false; | 54 | if (o == null || getClass() != o.getClass()) return false; |
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/DeepDnfEqualityChecker.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/DeepDnfEqualityChecker.java new file mode 100644 index 00000000..ebd7f5b0 --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/DeepDnfEqualityChecker.java | |||
@@ -0,0 +1,31 @@ | |||
1 | package tools.refinery.store.query.equality; | ||
2 | |||
3 | import tools.refinery.store.query.Dnf; | ||
4 | import tools.refinery.store.util.CycleDetectingMapper; | ||
5 | |||
6 | import java.util.List; | ||
7 | |||
8 | public class DeepDnfEqualityChecker implements DnfEqualityChecker { | ||
9 | private final CycleDetectingMapper<Pair, Boolean> mapper = new CycleDetectingMapper<>(Pair::toString, | ||
10 | this::doCheckEqual); | ||
11 | |||
12 | @Override | ||
13 | public boolean dnfEqual(Dnf left, Dnf right) { | ||
14 | return mapper.map(new Pair(left, right)); | ||
15 | } | ||
16 | |||
17 | protected boolean doCheckEqual(Pair pair) { | ||
18 | return pair.left.equalsWithSubstitution(this, pair.right); | ||
19 | } | ||
20 | |||
21 | protected List<Pair> getInProgress() { | ||
22 | return mapper.getInProgress(); | ||
23 | } | ||
24 | |||
25 | protected record Pair(Dnf left, Dnf right) { | ||
26 | @Override | ||
27 | public String toString() { | ||
28 | return "(%s, %s)".formatted(left.name(), right.name()); | ||
29 | } | ||
30 | } | ||
31 | } | ||
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/DnfEqualityChecker.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/DnfEqualityChecker.java new file mode 100644 index 00000000..eb77de17 --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/DnfEqualityChecker.java | |||
@@ -0,0 +1,8 @@ | |||
1 | package tools.refinery.store.query.equality; | ||
2 | |||
3 | import tools.refinery.store.query.Dnf; | ||
4 | |||
5 | @FunctionalInterface | ||
6 | public interface DnfEqualityChecker { | ||
7 | boolean dnfEqual(Dnf left, Dnf right); | ||
8 | } | ||
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/LiteralEqualityHelper.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/LiteralEqualityHelper.java new file mode 100644 index 00000000..23f1acc7 --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/LiteralEqualityHelper.java | |||
@@ -0,0 +1,48 @@ | |||
1 | package tools.refinery.store.query.equality; | ||
2 | |||
3 | import tools.refinery.store.query.Dnf; | ||
4 | import tools.refinery.store.query.Variable; | ||
5 | |||
6 | import java.util.HashMap; | ||
7 | import java.util.List; | ||
8 | import java.util.Map; | ||
9 | |||
10 | public class LiteralEqualityHelper { | ||
11 | private final DnfEqualityChecker dnfEqualityChecker; | ||
12 | private final Map<Variable, Variable> leftToRight; | ||
13 | private final Map<Variable, Variable> rightToLeft; | ||
14 | |||
15 | public LiteralEqualityHelper(DnfEqualityChecker dnfEqualityChecker, List<Variable> leftParameters, | ||
16 | List<Variable> rightParameters) { | ||
17 | this.dnfEqualityChecker = dnfEqualityChecker; | ||
18 | var arity = leftParameters.size(); | ||
19 | if (arity != rightParameters.size()) { | ||
20 | throw new IllegalArgumentException("Parameter lists have unequal length"); | ||
21 | } | ||
22 | leftToRight = new HashMap<>(arity); | ||
23 | rightToLeft = new HashMap<>(arity); | ||
24 | for (int i = 0; i < arity; i++) { | ||
25 | if (!variableEqual(leftParameters.get(i), rightParameters.get(i))) { | ||
26 | throw new IllegalArgumentException("Parameter lists cannot be unified: duplicate parameter " + i); | ||
27 | } | ||
28 | } | ||
29 | } | ||
30 | |||
31 | public boolean dnfEqual(Dnf left, Dnf right) { | ||
32 | return dnfEqualityChecker.dnfEqual(left, right); | ||
33 | } | ||
34 | |||
35 | public boolean variableEqual(Variable left, Variable right) { | ||
36 | if (checkMapping(leftToRight, left, right) && checkMapping(rightToLeft, right, left)) { | ||
37 | leftToRight.put(left, right); | ||
38 | rightToLeft.put(right, left); | ||
39 | return true; | ||
40 | } | ||
41 | return false; | ||
42 | } | ||
43 | |||
44 | private static boolean checkMapping(Map<Variable, Variable> map, Variable key, Variable expectedValue) { | ||
45 | var currentValue = map.get(key); | ||
46 | return currentValue == null || currentValue.equals(expectedValue); | ||
47 | } | ||
48 | } | ||
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/BooleanLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/BooleanLiteral.java index fd2f1eec..6d751be8 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/BooleanLiteral.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/BooleanLiteral.java | |||
@@ -1,18 +1,19 @@ | |||
1 | package tools.refinery.store.query.literal; | 1 | package tools.refinery.store.query.literal; |
2 | 2 | ||
3 | import tools.refinery.store.query.Variable; | 3 | import tools.refinery.store.query.Variable; |
4 | import tools.refinery.store.query.equality.LiteralEqualityHelper; | ||
5 | import tools.refinery.store.query.substitution.Substitution; | ||
4 | 6 | ||
5 | import java.util.Map; | ||
6 | import java.util.Set; | 7 | import java.util.Set; |
7 | 8 | ||
8 | public class BooleanLiteral implements Literal { | 9 | public enum BooleanLiteral implements PolarLiteral<BooleanLiteral> { |
9 | public static final BooleanLiteral TRUE = new BooleanLiteral(LiteralReduction.ALWAYS_TRUE); | 10 | TRUE(true), |
10 | public static final BooleanLiteral FALSE = new BooleanLiteral(LiteralReduction.ALWAYS_FALSE); | 11 | FALSE(false); |
11 | 12 | ||
12 | private final LiteralReduction reduction; | 13 | private final boolean value; |
13 | 14 | ||
14 | private BooleanLiteral(LiteralReduction reduction) { | 15 | BooleanLiteral(boolean value) { |
15 | this.reduction = reduction; | 16 | this.value = value; |
16 | } | 17 | } |
17 | 18 | ||
18 | @Override | 19 | @Override |
@@ -21,14 +22,29 @@ public class BooleanLiteral implements Literal { | |||
21 | } | 22 | } |
22 | 23 | ||
23 | @Override | 24 | @Override |
24 | public Literal substitute(Map<Variable, Variable> substitution) { | 25 | public Literal substitute(Substitution substitution) { |
25 | // No variables to substitute. | 26 | // No variables to substitute. |
26 | return this; | 27 | return this; |
27 | } | 28 | } |
28 | 29 | ||
29 | @Override | 30 | @Override |
30 | public LiteralReduction getReduction() { | 31 | public LiteralReduction getReduction() { |
31 | return reduction; | 32 | return value ? LiteralReduction.ALWAYS_TRUE : LiteralReduction.ALWAYS_FALSE; |
33 | } | ||
34 | |||
35 | @Override | ||
36 | public BooleanLiteral negate() { | ||
37 | return fromBoolean(!value); | ||
38 | } | ||
39 | |||
40 | @Override | ||
41 | public boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other) { | ||
42 | return equals(other); | ||
43 | } | ||
44 | |||
45 | @Override | ||
46 | public String toString() { | ||
47 | return Boolean.toString(value); | ||
32 | } | 48 | } |
33 | 49 | ||
34 | public static BooleanLiteral fromBoolean(boolean value) { | 50 | public static BooleanLiteral fromBoolean(boolean value) { |
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CallLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CallLiteral.java index 5e1ae94d..091b4e04 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CallLiteral.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CallLiteral.java | |||
@@ -1,11 +1,11 @@ | |||
1 | package tools.refinery.store.query.literal; | 1 | package tools.refinery.store.query.literal; |
2 | 2 | ||
3 | import tools.refinery.store.query.DnfUtils; | ||
4 | import tools.refinery.store.query.RelationLike; | 3 | import tools.refinery.store.query.RelationLike; |
5 | import tools.refinery.store.query.Variable; | 4 | import tools.refinery.store.query.Variable; |
5 | import tools.refinery.store.query.equality.LiteralEqualityHelper; | ||
6 | import tools.refinery.store.query.substitution.Substitution; | ||
6 | 7 | ||
7 | import java.util.List; | 8 | import java.util.List; |
8 | import java.util.Map; | ||
9 | import java.util.Objects; | 9 | import java.util.Objects; |
10 | import java.util.Set; | 10 | import java.util.Set; |
11 | 11 | ||
@@ -31,6 +31,8 @@ public abstract class CallLiteral<T extends RelationLike> implements Literal { | |||
31 | return polarity; | 31 | return polarity; |
32 | } | 32 | } |
33 | 33 | ||
34 | public abstract Class<T> getTargetType(); | ||
35 | |||
34 | public T getTarget() { | 36 | public T getTarget() { |
35 | return target; | 37 | return target; |
36 | } | 38 | } |
@@ -46,8 +48,44 @@ public abstract class CallLiteral<T extends RelationLike> implements Literal { | |||
46 | } | 48 | } |
47 | } | 49 | } |
48 | 50 | ||
49 | protected List<Variable> substituteArguments(Map<Variable, Variable> substitution) { | 51 | protected List<Variable> substituteArguments(Substitution substitution) { |
50 | return arguments.stream().map(variable -> DnfUtils.maybeSubstitute(variable, substitution)).toList(); | 52 | return arguments.stream().map(substitution::getSubstitute).toList(); |
53 | } | ||
54 | |||
55 | /** | ||
56 | * Compares the target of this call literal with another object. | ||
57 | * | ||
58 | * @param helper Equality helper for comparing {@link Variable} and {@link tools.refinery.store.query.Dnf} | ||
59 | * instances. | ||
60 | * @param otherTarget The object to compare the target to. | ||
61 | * @return {@code true} if {@code otherTarget} is equal to the return value of {@link #getTarget()} according to | ||
62 | * {@code helper}, {@code false} otherwise. | ||
63 | */ | ||
64 | protected boolean targetEquals(LiteralEqualityHelper helper, T otherTarget) { | ||
65 | return target.equals(otherTarget); | ||
66 | } | ||
67 | |||
68 | @Override | ||
69 | public boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other) { | ||
70 | if (other.getClass() != getClass()) { | ||
71 | return false; | ||
72 | } | ||
73 | var otherCallLiteral = (CallLiteral<?>) other; | ||
74 | if (getTargetType() != otherCallLiteral.getTargetType() || polarity != otherCallLiteral.polarity) { | ||
75 | return false; | ||
76 | } | ||
77 | var arity = arguments.size(); | ||
78 | if (arity != otherCallLiteral.arguments.size()) { | ||
79 | return false; | ||
80 | } | ||
81 | for (int i = 0; i < arity; i++) { | ||
82 | if (!helper.variableEqual(arguments.get(i), otherCallLiteral.arguments.get(i))) { | ||
83 | return false; | ||
84 | } | ||
85 | } | ||
86 | @SuppressWarnings("unchecked") | ||
87 | var otherTarget = (T) otherCallLiteral.target; | ||
88 | return targetEquals(helper, otherTarget); | ||
51 | } | 89 | } |
52 | 90 | ||
53 | @Override | 91 | @Override |
@@ -63,4 +101,33 @@ public abstract class CallLiteral<T extends RelationLike> implements Literal { | |||
63 | public int hashCode() { | 101 | public int hashCode() { |
64 | return Objects.hash(polarity, target, arguments); | 102 | return Objects.hash(polarity, target, arguments); |
65 | } | 103 | } |
104 | |||
105 | protected String targetToString() { | ||
106 | return "@%s %s".formatted(getTargetType().getSimpleName(), target.name()); | ||
107 | } | ||
108 | |||
109 | @Override | ||
110 | public String toString() { | ||
111 | var builder = new StringBuilder(); | ||
112 | if (!polarity.isPositive()) { | ||
113 | builder.append("!("); | ||
114 | } | ||
115 | builder.append(targetToString()); | ||
116 | if (polarity.isTransitive()) { | ||
117 | builder.append("+"); | ||
118 | } | ||
119 | builder.append("("); | ||
120 | var argumentIterator = arguments.iterator(); | ||
121 | if (argumentIterator.hasNext()) { | ||
122 | builder.append(argumentIterator.next()); | ||
123 | while (argumentIterator.hasNext()) { | ||
124 | builder.append(", ").append(argumentIterator.next()); | ||
125 | } | ||
126 | } | ||
127 | builder.append(")"); | ||
128 | if (!polarity.isPositive()) { | ||
129 | builder.append(")"); | ||
130 | } | ||
131 | return builder.toString(); | ||
132 | } | ||
66 | } | 133 | } |
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java index 746d23af..d01c7d20 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java | |||
@@ -1,9 +1,9 @@ | |||
1 | package tools.refinery.store.query.literal; | 1 | package tools.refinery.store.query.literal; |
2 | 2 | ||
3 | import tools.refinery.store.query.DnfUtils; | ||
4 | import tools.refinery.store.query.Variable; | 3 | import tools.refinery.store.query.Variable; |
4 | import tools.refinery.store.query.equality.LiteralEqualityHelper; | ||
5 | import tools.refinery.store.query.substitution.Substitution; | ||
5 | 6 | ||
6 | import java.util.Map; | ||
7 | import java.util.Set; | 7 | import java.util.Set; |
8 | 8 | ||
9 | public record ConstantLiteral(Variable variable, int nodeId) implements Literal { | 9 | public record ConstantLiteral(Variable variable, int nodeId) implements Literal { |
@@ -13,7 +13,21 @@ public record ConstantLiteral(Variable variable, int nodeId) implements Literal | |||
13 | } | 13 | } |
14 | 14 | ||
15 | @Override | 15 | @Override |
16 | public ConstantLiteral substitute(Map<Variable, Variable> substitution) { | 16 | public ConstantLiteral substitute(Substitution substitution) { |
17 | return new ConstantLiteral(DnfUtils.maybeSubstitute(variable, substitution), nodeId); | 17 | return new ConstantLiteral(substitution.getSubstitute(variable), nodeId); |
18 | } | ||
19 | |||
20 | @Override | ||
21 | public boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other) { | ||
22 | if (other.getClass() != getClass()) { | ||
23 | return false; | ||
24 | } | ||
25 | var otherConstantLiteral = (ConstantLiteral) other; | ||
26 | return helper.variableEqual(variable, otherConstantLiteral.variable) && nodeId == otherConstantLiteral.nodeId; | ||
27 | } | ||
28 | |||
29 | @Override | ||
30 | public String toString() { | ||
31 | return "%s === @Constant %d".formatted(variable, nodeId); | ||
18 | } | 32 | } |
19 | } | 33 | } |
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/DnfCallLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/DnfCallLiteral.java index de6c6005..27917265 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/DnfCallLiteral.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/DnfCallLiteral.java | |||
@@ -2,9 +2,10 @@ package tools.refinery.store.query.literal; | |||
2 | 2 | ||
3 | import tools.refinery.store.query.Dnf; | 3 | import tools.refinery.store.query.Dnf; |
4 | import tools.refinery.store.query.Variable; | 4 | import tools.refinery.store.query.Variable; |
5 | import tools.refinery.store.query.equality.LiteralEqualityHelper; | ||
6 | import tools.refinery.store.query.substitution.Substitution; | ||
5 | 7 | ||
6 | import java.util.List; | 8 | import java.util.List; |
7 | import java.util.Map; | ||
8 | 9 | ||
9 | public final class DnfCallLiteral extends CallLiteral<Dnf> implements PolarLiteral<DnfCallLiteral> { | 10 | public final class DnfCallLiteral extends CallLiteral<Dnf> implements PolarLiteral<DnfCallLiteral> { |
10 | public DnfCallLiteral(CallPolarity polarity, Dnf target, List<Variable> arguments) { | 11 | public DnfCallLiteral(CallPolarity polarity, Dnf target, List<Variable> arguments) { |
@@ -12,7 +13,12 @@ public final class DnfCallLiteral extends CallLiteral<Dnf> implements PolarLiter | |||
12 | } | 13 | } |
13 | 14 | ||
14 | @Override | 15 | @Override |
15 | public DnfCallLiteral substitute(Map<Variable, Variable> substitution) { | 16 | public Class<Dnf> getTargetType() { |
17 | return Dnf.class; | ||
18 | } | ||
19 | |||
20 | @Override | ||
21 | public DnfCallLiteral substitute(Substitution substitution) { | ||
16 | return new DnfCallLiteral(getPolarity(), getTarget(), substituteArguments(substitution)); | 22 | return new DnfCallLiteral(getPolarity(), getTarget(), substituteArguments(substitution)); |
17 | } | 23 | } |
18 | 24 | ||
@@ -26,4 +32,9 @@ public final class DnfCallLiteral extends CallLiteral<Dnf> implements PolarLiter | |||
26 | var dnfReduction = getTarget().getReduction(); | 32 | var dnfReduction = getTarget().getReduction(); |
27 | return getPolarity().isPositive() ? dnfReduction : dnfReduction.negate(); | 33 | return getPolarity().isPositive() ? dnfReduction : dnfReduction.negate(); |
28 | } | 34 | } |
35 | |||
36 | @Override | ||
37 | protected boolean targetEquals(LiteralEqualityHelper helper, Dnf otherTarget) { | ||
38 | return helper.dnfEqual(getTarget(), otherTarget); | ||
39 | } | ||
29 | } | 40 | } |
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java index f30179b2..61c753c3 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java | |||
@@ -1,9 +1,9 @@ | |||
1 | package tools.refinery.store.query.literal; | 1 | package tools.refinery.store.query.literal; |
2 | 2 | ||
3 | import tools.refinery.store.query.DnfUtils; | ||
4 | import tools.refinery.store.query.Variable; | 3 | import tools.refinery.store.query.Variable; |
4 | import tools.refinery.store.query.equality.LiteralEqualityHelper; | ||
5 | import tools.refinery.store.query.substitution.Substitution; | ||
5 | 6 | ||
6 | import java.util.Map; | ||
7 | import java.util.Set; | 7 | import java.util.Set; |
8 | 8 | ||
9 | public record EquivalenceLiteral(boolean positive, Variable left, Variable right) | 9 | public record EquivalenceLiteral(boolean positive, Variable left, Variable right) |
@@ -20,9 +20,8 @@ public record EquivalenceLiteral(boolean positive, Variable left, Variable right | |||
20 | } | 20 | } |
21 | 21 | ||
22 | @Override | 22 | @Override |
23 | public EquivalenceLiteral substitute(Map<Variable, Variable> substitution) { | 23 | public EquivalenceLiteral substitute(Substitution substitution) { |
24 | return new EquivalenceLiteral(positive, DnfUtils.maybeSubstitute(left, substitution), | 24 | return new EquivalenceLiteral(positive, substitution.getSubstitute(left), substitution.getSubstitute(right)); |
25 | DnfUtils.maybeSubstitute(right, substitution)); | ||
26 | } | 25 | } |
27 | 26 | ||
28 | @Override | 27 | @Override |
@@ -32,4 +31,19 @@ public record EquivalenceLiteral(boolean positive, Variable left, Variable right | |||
32 | } | 31 | } |
33 | return LiteralReduction.NOT_REDUCIBLE; | 32 | return LiteralReduction.NOT_REDUCIBLE; |
34 | } | 33 | } |
34 | |||
35 | @Override | ||
36 | public boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other) { | ||
37 | if (other.getClass() != getClass()) { | ||
38 | return false; | ||
39 | } | ||
40 | var otherEquivalenceLiteral = (EquivalenceLiteral) other; | ||
41 | return helper.variableEqual(left, otherEquivalenceLiteral.left) && helper.variableEqual(right, | ||
42 | otherEquivalenceLiteral.right); | ||
43 | } | ||
44 | |||
45 | @Override | ||
46 | public String toString() { | ||
47 | return "%s %s %s".formatted(left, positive ? "===" : "!==", right); | ||
48 | } | ||
35 | } | 49 | } |
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/Literal.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/Literal.java index a6893acf..ddd91775 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/Literal.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/Literal.java | |||
@@ -1,16 +1,20 @@ | |||
1 | package tools.refinery.store.query.literal; | 1 | package tools.refinery.store.query.literal; |
2 | 2 | ||
3 | import tools.refinery.store.query.Variable; | 3 | import tools.refinery.store.query.Variable; |
4 | import tools.refinery.store.query.equality.LiteralEqualityHelper; | ||
5 | import tools.refinery.store.query.substitution.Substitution; | ||
4 | 6 | ||
5 | import java.util.Map; | ||
6 | import java.util.Set; | 7 | import java.util.Set; |
7 | 8 | ||
8 | public interface Literal { | 9 | public interface Literal { |
9 | void collectAllVariables(Set<Variable> variables); | 10 | void collectAllVariables(Set<Variable> variables); |
10 | 11 | ||
11 | Literal substitute(Map<Variable, Variable> substitution); | 12 | Literal substitute(Substitution substitution); |
12 | 13 | ||
13 | default LiteralReduction getReduction() { | 14 | default LiteralReduction getReduction() { |
14 | return LiteralReduction.NOT_REDUCIBLE; | 15 | return LiteralReduction.NOT_REDUCIBLE; |
15 | } | 16 | } |
17 | |||
18 | @SuppressWarnings("BooleanMethodIsAlwaysInverted") | ||
19 | boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other); | ||
16 | } | 20 | } |
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/RelationViewLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/RelationViewLiteral.java index 4718b550..fb8b3332 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/RelationViewLiteral.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/RelationViewLiteral.java | |||
@@ -1,10 +1,10 @@ | |||
1 | package tools.refinery.store.query.literal; | 1 | package tools.refinery.store.query.literal; |
2 | 2 | ||
3 | import tools.refinery.store.query.Variable; | 3 | import tools.refinery.store.query.Variable; |
4 | import tools.refinery.store.query.substitution.Substitution; | ||
4 | import tools.refinery.store.query.view.AnyRelationView; | 5 | import tools.refinery.store.query.view.AnyRelationView; |
5 | 6 | ||
6 | import java.util.List; | 7 | import java.util.List; |
7 | import java.util.Map; | ||
8 | 8 | ||
9 | public final class RelationViewLiteral extends CallLiteral<AnyRelationView> | 9 | public final class RelationViewLiteral extends CallLiteral<AnyRelationView> |
10 | implements PolarLiteral<RelationViewLiteral> { | 10 | implements PolarLiteral<RelationViewLiteral> { |
@@ -13,7 +13,18 @@ public final class RelationViewLiteral extends CallLiteral<AnyRelationView> | |||
13 | } | 13 | } |
14 | 14 | ||
15 | @Override | 15 | @Override |
16 | public RelationViewLiteral substitute(Map<Variable, Variable> substitution) { | 16 | public Class<AnyRelationView> getTargetType() { |
17 | return AnyRelationView.class; | ||
18 | } | ||
19 | |||
20 | @Override | ||
21 | protected String targetToString() { | ||
22 | var target = getTarget(); | ||
23 | return "@RelationView(\"%s\") %s".formatted(target.getViewName(), target.getSymbol().name()); | ||
24 | } | ||
25 | |||
26 | @Override | ||
27 | public RelationViewLiteral substitute(Substitution substitution) { | ||
17 | return new RelationViewLiteral(getPolarity(), getTarget(), substituteArguments(substitution)); | 28 | return new RelationViewLiteral(getPolarity(), getTarget(), substituteArguments(substitution)); |
18 | } | 29 | } |
19 | 30 | ||
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/MapBasedSubstitution.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/MapBasedSubstitution.java new file mode 100644 index 00000000..ffc65047 --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/MapBasedSubstitution.java | |||
@@ -0,0 +1,13 @@ | |||
1 | package tools.refinery.store.query.substitution; | ||
2 | |||
3 | import tools.refinery.store.query.Variable; | ||
4 | |||
5 | import java.util.Map; | ||
6 | |||
7 | public record MapBasedSubstitution(Map<Variable, Variable> map, Substitution fallback) implements Substitution { | ||
8 | @Override | ||
9 | public Variable getSubstitute(Variable variable) { | ||
10 | var value = map.get(variable); | ||
11 | return value == null ? fallback.getSubstitute(variable) : value; | ||
12 | } | ||
13 | } | ||
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/RenewingSubstitution.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/RenewingSubstitution.java new file mode 100644 index 00000000..54d18a3f --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/RenewingSubstitution.java | |||
@@ -0,0 +1,19 @@ | |||
1 | package tools.refinery.store.query.substitution; | ||
2 | |||
3 | import tools.refinery.store.query.Variable; | ||
4 | |||
5 | import java.util.HashMap; | ||
6 | import java.util.Map; | ||
7 | |||
8 | public class RenewingSubstitution implements Substitution { | ||
9 | private final Map<Variable, Variable> alreadyRenewed = new HashMap<>(); | ||
10 | |||
11 | @Override | ||
12 | public Variable getSubstitute(Variable variable) { | ||
13 | return alreadyRenewed.computeIfAbsent(variable, RenewingSubstitution::renew); | ||
14 | } | ||
15 | |||
16 | private static Variable renew(Variable variable) { | ||
17 | return variable.isExplicitlyNamed() ? new Variable(variable.getName()) : new Variable(); | ||
18 | } | ||
19 | } | ||
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/StatelessSubstitution.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/StatelessSubstitution.java new file mode 100644 index 00000000..d33ad6fb --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/StatelessSubstitution.java | |||
@@ -0,0 +1,18 @@ | |||
1 | package tools.refinery.store.query.substitution; | ||
2 | |||
3 | import tools.refinery.store.query.Variable; | ||
4 | |||
5 | public enum StatelessSubstitution implements Substitution { | ||
6 | FAILING { | ||
7 | @Override | ||
8 | public Variable getSubstitute(Variable variable) { | ||
9 | throw new IllegalArgumentException("No substitute for " + variable); | ||
10 | } | ||
11 | }, | ||
12 | IDENTITY { | ||
13 | @Override | ||
14 | public Variable getSubstitute(Variable variable) { | ||
15 | return variable; | ||
16 | } | ||
17 | } | ||
18 | } | ||
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/Substitution.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/Substitution.java new file mode 100644 index 00000000..9d086bf5 --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/Substitution.java | |||
@@ -0,0 +1,8 @@ | |||
1 | package tools.refinery.store.query.substitution; | ||
2 | |||
3 | import tools.refinery.store.query.Variable; | ||
4 | |||
5 | @FunctionalInterface | ||
6 | public interface Substitution { | ||
7 | Variable getSubstitute(Variable variable); | ||
8 | } | ||
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/Substitutions.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/Substitutions.java new file mode 100644 index 00000000..26cf1a20 --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/Substitutions.java | |||
@@ -0,0 +1,27 @@ | |||
1 | package tools.refinery.store.query.substitution; | ||
2 | |||
3 | import tools.refinery.store.query.Variable; | ||
4 | |||
5 | import java.util.Map; | ||
6 | |||
7 | public final class Substitutions { | ||
8 | private Substitutions() { | ||
9 | throw new IllegalStateException("This is a static utility class and should not be instantiate directly"); | ||
10 | } | ||
11 | |||
12 | public static Substitution total(Map<Variable, Variable> map) { | ||
13 | return new MapBasedSubstitution(map, StatelessSubstitution.FAILING); | ||
14 | } | ||
15 | |||
16 | public static Substitution partial(Map<Variable, Variable> map) { | ||
17 | return new MapBasedSubstitution(map, StatelessSubstitution.IDENTITY); | ||
18 | } | ||
19 | |||
20 | public static Substitution renewing(Map<Variable, Variable> map) { | ||
21 | return new MapBasedSubstitution(map, renewing()); | ||
22 | } | ||
23 | |||
24 | public static Substitution renewing() { | ||
25 | return new RenewingSubstitution(); | ||
26 | } | ||
27 | } | ||
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/view/AnyRelationView.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/AnyRelationView.java index 328cde3a..bc3ac1ea 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/view/AnyRelationView.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/AnyRelationView.java | |||
@@ -10,6 +10,8 @@ import java.util.Set; | |||
10 | public sealed interface AnyRelationView extends RelationLike permits RelationView { | 10 | public sealed interface AnyRelationView extends RelationLike permits RelationView { |
11 | AnySymbol getSymbol(); | 11 | AnySymbol getSymbol(); |
12 | 12 | ||
13 | String getViewName(); | ||
14 | |||
13 | default Set<FunctionalDependency<Integer>> getFunctionalDependencies() { | 15 | default Set<FunctionalDependency<Integer>> getFunctionalDependencies() { |
14 | return Set.of(); | 16 | return Set.of(); |
15 | } | 17 | } |
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/view/RelationView.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/RelationView.java index 2714a8c5..ea9fd5e2 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/view/RelationView.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/RelationView.java | |||
@@ -21,11 +21,11 @@ import java.util.UUID; | |||
21 | public abstract non-sealed class RelationView<T> implements AnyRelationView { | 21 | public abstract non-sealed class RelationView<T> implements AnyRelationView { |
22 | private final Symbol<T> symbol; | 22 | private final Symbol<T> symbol; |
23 | 23 | ||
24 | private final String name; | 24 | private final String viewName; |
25 | 25 | ||
26 | protected RelationView(Symbol<T> symbol, String name) { | 26 | protected RelationView(Symbol<T> symbol, String viewName) { |
27 | this.symbol = symbol; | 27 | this.symbol = symbol; |
28 | this.name = name; | 28 | this.viewName = viewName; |
29 | } | 29 | } |
30 | 30 | ||
31 | protected RelationView(Symbol<T> representation) { | 31 | protected RelationView(Symbol<T> representation) { |
@@ -38,8 +38,13 @@ public abstract non-sealed class RelationView<T> implements AnyRelationView { | |||
38 | } | 38 | } |
39 | 39 | ||
40 | @Override | 40 | @Override |
41 | public String getViewName() { | ||
42 | return viewName; | ||
43 | } | ||
44 | |||
45 | @Override | ||
41 | public String name() { | 46 | public String name() { |
42 | return symbol.name() + "#" + name; | 47 | return symbol.name() + "#" + viewName; |
43 | } | 48 | } |
44 | 49 | ||
45 | public abstract boolean filter(Tuple key, T value); | 50 | public abstract boolean filter(Tuple key, T value); |
@@ -72,11 +77,11 @@ public abstract non-sealed class RelationView<T> implements AnyRelationView { | |||
72 | if (this == o) return true; | 77 | if (this == o) return true; |
73 | if (o == null || getClass() != o.getClass()) return false; | 78 | if (o == null || getClass() != o.getClass()) return false; |
74 | RelationView<?> that = (RelationView<?>) o; | 79 | RelationView<?> that = (RelationView<?>) o; |
75 | return Objects.equals(symbol, that.symbol) && Objects.equals(name, that.name); | 80 | return Objects.equals(symbol, that.symbol) && Objects.equals(viewName, that.viewName); |
76 | } | 81 | } |
77 | 82 | ||
78 | @Override | 83 | @Override |
79 | public int hashCode() { | 84 | public int hashCode() { |
80 | return Objects.hash(symbol, name); | 85 | return Objects.hash(symbol, viewName); |
81 | } | 86 | } |
82 | } | 87 | } |
diff --git a/subprojects/store-query/src/test/java/tools/refinery/store/query/DnfBuilderTest.java b/subprojects/store-query/src/test/java/tools/refinery/store/query/DnfBuilderTest.java new file mode 100644 index 00000000..e6701fe3 --- /dev/null +++ b/subprojects/store-query/src/test/java/tools/refinery/store/query/DnfBuilderTest.java | |||
@@ -0,0 +1,218 @@ | |||
1 | package tools.refinery.store.query; | ||
2 | |||
3 | import org.junit.jupiter.api.Test; | ||
4 | import tools.refinery.store.query.literal.BooleanLiteral; | ||
5 | import tools.refinery.store.query.view.KeyOnlyRelationView; | ||
6 | import tools.refinery.store.representation.Symbol; | ||
7 | |||
8 | import static org.hamcrest.MatcherAssert.assertThat; | ||
9 | import static tools.refinery.store.query.literal.Literals.not; | ||
10 | import static tools.refinery.store.query.tests.QueryMatchers.structurallyEqualTo; | ||
11 | |||
12 | class DnfBuilderTest { | ||
13 | @Test | ||
14 | void eliminateTrueTest() { | ||
15 | var p = new Variable("p"); | ||
16 | var q = new Variable("q"); | ||
17 | var friend = new Symbol<>("friend", 2, Boolean.class, false); | ||
18 | var friendView = new KeyOnlyRelationView<>(friend); | ||
19 | |||
20 | var actual = Dnf.builder() | ||
21 | .parameters(p, q) | ||
22 | .clause(BooleanLiteral.TRUE, friendView.call(p, q)) | ||
23 | .build(); | ||
24 | var expected = Dnf.builder().parameters(p, q).clause(friendView.call(p, q)).build(); | ||
25 | |||
26 | assertThat(actual, structurallyEqualTo(expected)); | ||
27 | } | ||
28 | |||
29 | @Test | ||
30 | void eliminateFalseTest() { | ||
31 | var p = new Variable("p"); | ||
32 | var q = new Variable("q"); | ||
33 | var friend = new Symbol<>("friend", 2, Boolean.class, false); | ||
34 | var friendView = new KeyOnlyRelationView<>(friend); | ||
35 | |||
36 | var actual = Dnf.builder() | ||
37 | .parameters(p, q) | ||
38 | .clause(friendView.call(p, q)) | ||
39 | .clause(friendView.call(q, p), BooleanLiteral.FALSE) | ||
40 | .build(); | ||
41 | var expected = Dnf.builder().parameters(p, q).clause(friendView.call(p, q)).build(); | ||
42 | |||
43 | assertThat(actual, structurallyEqualTo(expected)); | ||
44 | } | ||
45 | |||
46 | @Test | ||
47 | void alwaysTrueTest() { | ||
48 | var p = new Variable("p"); | ||
49 | var q = new Variable("q"); | ||
50 | var friend = new Symbol<>("friend", 2, Boolean.class, false); | ||
51 | var friendView = new KeyOnlyRelationView<>(friend); | ||
52 | |||
53 | var actual = Dnf.builder() | ||
54 | .parameters(p, q) | ||
55 | .clause(friendView.call(p, q)) | ||
56 | .clause(BooleanLiteral.TRUE) | ||
57 | .build(); | ||
58 | var expected = Dnf.builder().parameters(p, q).clause().build(); | ||
59 | |||
60 | assertThat(actual, structurallyEqualTo(expected)); | ||
61 | } | ||
62 | |||
63 | @Test | ||
64 | void alwaysFalseTest() { | ||
65 | var p = new Variable("p"); | ||
66 | var q = new Variable("q"); | ||
67 | var friend = new Symbol<>("friend", 2, Boolean.class, false); | ||
68 | var friendView = new KeyOnlyRelationView<>(friend); | ||
69 | |||
70 | var actual = Dnf.builder() | ||
71 | .parameters(p, q) | ||
72 | .clause(friendView.call(p, q), BooleanLiteral.FALSE) | ||
73 | .build(); | ||
74 | var expected = Dnf.builder().parameters(p, q).build(); | ||
75 | |||
76 | assertThat(actual, structurallyEqualTo(expected)); | ||
77 | } | ||
78 | |||
79 | @Test | ||
80 | void eliminateTrueDnfTest() { | ||
81 | var p = new Variable("p"); | ||
82 | var q = new Variable("q"); | ||
83 | var friend = new Symbol<>("friend", 2, Boolean.class, false); | ||
84 | var friendView = new KeyOnlyRelationView<>(friend); | ||
85 | var trueDnf = Dnf.builder().parameter(p).clause().build(); | ||
86 | |||
87 | var actual = Dnf.builder() | ||
88 | .parameters(p, q) | ||
89 | .clause(trueDnf.call(q), friendView.call(p, q)) | ||
90 | .build(); | ||
91 | var expected = Dnf.builder().parameters(p, q).clause(friendView.call(p, q)).build(); | ||
92 | |||
93 | assertThat(actual, structurallyEqualTo(expected)); | ||
94 | } | ||
95 | |||
96 | @Test | ||
97 | void eliminateFalseDnfTest() { | ||
98 | var p = new Variable("p"); | ||
99 | var q = new Variable("q"); | ||
100 | var friend = new Symbol<>("friend", 2, Boolean.class, false); | ||
101 | var friendView = new KeyOnlyRelationView<>(friend); | ||
102 | var falseDnf = Dnf.builder().parameter(p).build(); | ||
103 | |||
104 | var actual = Dnf.builder() | ||
105 | .parameters(p, q) | ||
106 | .clause(friendView.call(p, q)) | ||
107 | .clause(friendView.call(q, p), falseDnf.call(q)) | ||
108 | .build(); | ||
109 | var expected = Dnf.builder().parameters(p, q).clause(friendView.call(p, q)).build(); | ||
110 | |||
111 | assertThat(actual, structurallyEqualTo(expected)); | ||
112 | } | ||
113 | |||
114 | @Test | ||
115 | void alwaysTrueDnfTest() { | ||
116 | var p = new Variable("p"); | ||
117 | var q = new Variable("q"); | ||
118 | var friend = new Symbol<>("friend", 2, Boolean.class, false); | ||
119 | var friendView = new KeyOnlyRelationView<>(friend); | ||
120 | var trueDnf = Dnf.builder().parameter(p).clause().build(); | ||
121 | |||
122 | var actual = Dnf.builder() | ||
123 | .parameters(p, q) | ||
124 | .clause(friendView.call(p, q)) | ||
125 | .clause(trueDnf.call(q)) | ||
126 | .build(); | ||
127 | var expected = Dnf.builder().parameters(p, q).clause().build(); | ||
128 | |||
129 | assertThat(actual, structurallyEqualTo(expected)); | ||
130 | } | ||
131 | |||
132 | @Test | ||
133 | void alwaysFalseDnfTest() { | ||
134 | var p = new Variable("p"); | ||
135 | var q = new Variable("q"); | ||
136 | var friend = new Symbol<>("friend", 2, Boolean.class, false); | ||
137 | var friendView = new KeyOnlyRelationView<>(friend); | ||
138 | var falseDnf = Dnf.builder().parameter(p).build(); | ||
139 | |||
140 | var actual = Dnf.builder() | ||
141 | .parameters(p, q) | ||
142 | .clause(friendView.call(p, q), falseDnf.call(q)) | ||
143 | .build(); | ||
144 | var expected = Dnf.builder().parameters(p, q).build(); | ||
145 | |||
146 | assertThat(actual, structurallyEqualTo(expected)); | ||
147 | } | ||
148 | |||
149 | @Test | ||
150 | void eliminateNotFalseDnfTest() { | ||
151 | var p = new Variable("p"); | ||
152 | var q = new Variable("q"); | ||
153 | var friend = new Symbol<>("friend", 2, Boolean.class, false); | ||
154 | var friendView = new KeyOnlyRelationView<>(friend); | ||
155 | var falseDnf = Dnf.builder().parameter(p).build(); | ||
156 | |||
157 | var actual = Dnf.builder() | ||
158 | .parameters(p, q) | ||
159 | .clause(not(falseDnf.call(q)), friendView.call(p, q)) | ||
160 | .build(); | ||
161 | var expected = Dnf.builder().parameters(p, q).clause(friendView.call(p, q)).build(); | ||
162 | |||
163 | assertThat(actual, structurallyEqualTo(expected)); | ||
164 | } | ||
165 | |||
166 | @Test | ||
167 | void eliminateNotTrueDnfTest() { | ||
168 | var p = new Variable("p"); | ||
169 | var q = new Variable("q"); | ||
170 | var friend = new Symbol<>("friend", 2, Boolean.class, false); | ||
171 | var friendView = new KeyOnlyRelationView<>(friend); | ||
172 | var trueDnf = Dnf.builder().parameter(p).clause().build(); | ||
173 | |||
174 | var actual = Dnf.builder() | ||
175 | .parameters(p, q) | ||
176 | .clause(friendView.call(p, q)) | ||
177 | .clause(friendView.call(q, p), not(trueDnf.call(q))) | ||
178 | .build(); | ||
179 | var expected = Dnf.builder().parameters(p, q).clause(friendView.call(p, q)).build(); | ||
180 | |||
181 | assertThat(actual, structurallyEqualTo(expected)); | ||
182 | } | ||
183 | |||
184 | @Test | ||
185 | void alwaysNotFalseDnfTest() { | ||
186 | var p = new Variable("p"); | ||
187 | var q = new Variable("q"); | ||
188 | var friend = new Symbol<>("friend", 2, Boolean.class, false); | ||
189 | var friendView = new KeyOnlyRelationView<>(friend); | ||
190 | var falseDnf = Dnf.builder().parameter(p).build(); | ||
191 | |||
192 | var actual = Dnf.builder() | ||
193 | .parameters(p, q) | ||
194 | .clause(friendView.call(p, q)) | ||
195 | .clause(not(falseDnf.call(q))) | ||
196 | .build(); | ||
197 | var expected = Dnf.builder().parameters(p, q).clause().build(); | ||
198 | |||
199 | assertThat(actual, structurallyEqualTo(expected)); | ||
200 | } | ||
201 | |||
202 | @Test | ||
203 | void alwaysNotTrueDnfTest() { | ||
204 | var p = new Variable("p"); | ||
205 | var q = new Variable("q"); | ||
206 | var friend = new Symbol<>("friend", 2, Boolean.class, false); | ||
207 | var friendView = new KeyOnlyRelationView<>(friend); | ||
208 | var trueDnf = Dnf.builder().parameter(p).clause().build(); | ||
209 | |||
210 | var actual = Dnf.builder() | ||
211 | .parameters(p, q) | ||
212 | .clause(friendView.call(p, q), not(trueDnf.call(q))) | ||
213 | .build(); | ||
214 | var expected = Dnf.builder().parameters(p, q).build(); | ||
215 | |||
216 | assertThat(actual, structurallyEqualTo(expected)); | ||
217 | } | ||
218 | } | ||
diff --git a/subprojects/store-query/src/test/java/tools/refinery/store/query/DnfToStringTest.java b/subprojects/store-query/src/test/java/tools/refinery/store/query/DnfToStringTest.java new file mode 100644 index 00000000..e6e4bef3 --- /dev/null +++ b/subprojects/store-query/src/test/java/tools/refinery/store/query/DnfToStringTest.java | |||
@@ -0,0 +1,172 @@ | |||
1 | package tools.refinery.store.query; | ||
2 | |||
3 | import org.junit.jupiter.api.Test; | ||
4 | import tools.refinery.store.query.view.KeyOnlyRelationView; | ||
5 | import tools.refinery.store.representation.Symbol; | ||
6 | |||
7 | import static org.hamcrest.MatcherAssert.assertThat; | ||
8 | import static org.hamcrest.Matchers.is; | ||
9 | import static tools.refinery.store.query.literal.Literals.not; | ||
10 | |||
11 | class DnfToStringTest { | ||
12 | @Test | ||
13 | void noClausesTest() { | ||
14 | var p = new Variable("p"); | ||
15 | var dnf = Dnf.builder("Example").parameter(p).build(); | ||
16 | |||
17 | assertThat(dnf.toString(), is(""" | ||
18 | pred Example(p) <-> | ||
19 | <no clauses>. | ||
20 | """)); | ||
21 | } | ||
22 | |||
23 | @Test | ||
24 | void noParametersTest() { | ||
25 | var dnf = Dnf.builder("Example").build(); | ||
26 | |||
27 | assertThat(dnf.toString(), is(""" | ||
28 | pred Example() <-> | ||
29 | <no clauses>. | ||
30 | """)); | ||
31 | } | ||
32 | |||
33 | @Test | ||
34 | void emptyClauseTest() { | ||
35 | var p = new Variable("p"); | ||
36 | var dnf = Dnf.builder("Example").parameter(p).clause().build(); | ||
37 | |||
38 | assertThat(dnf.toString(), is(""" | ||
39 | pred Example(p) <-> | ||
40 | <empty>. | ||
41 | """)); | ||
42 | } | ||
43 | |||
44 | @Test | ||
45 | void relationViewPositiveTest() { | ||
46 | var p = new Variable("p"); | ||
47 | var q = new Variable("q"); | ||
48 | var friend = new Symbol<>("friend", 2, Boolean.class, false); | ||
49 | var friendView = new KeyOnlyRelationView<>(friend); | ||
50 | var dnf = Dnf.builder("Example").parameter(p).clause(friendView.call(p, q)).build(); | ||
51 | |||
52 | assertThat(dnf.toString(), is(""" | ||
53 | pred Example(p) <-> | ||
54 | @RelationView("key") friend(p, q). | ||
55 | """)); | ||
56 | } | ||
57 | |||
58 | @Test | ||
59 | void relationViewNegativeTest() { | ||
60 | var p = new Variable("p"); | ||
61 | var q = new Variable("q"); | ||
62 | var friend = new Symbol<>("friend", 2, Boolean.class, false); | ||
63 | var friendView = new KeyOnlyRelationView<>(friend); | ||
64 | var dnf = Dnf.builder("Example").parameter(p).clause(not(friendView.call(p, q))).build(); | ||
65 | |||
66 | assertThat(dnf.toString(), is(""" | ||
67 | pred Example(p) <-> | ||
68 | !(@RelationView("key") friend(p, q)). | ||
69 | """)); | ||
70 | } | ||
71 | |||
72 | @Test | ||
73 | void relationViewTransitiveTest() { | ||
74 | var p = new Variable("p"); | ||
75 | var q = new Variable("q"); | ||
76 | var friend = new Symbol<>("friend", 2, Boolean.class, false); | ||
77 | var friendView = new KeyOnlyRelationView<>(friend); | ||
78 | var dnf = Dnf.builder("Example").parameter(p).clause(friendView.callTransitive(p, q)).build(); | ||
79 | |||
80 | assertThat(dnf.toString(), is(""" | ||
81 | pred Example(p) <-> | ||
82 | @RelationView("key") friend+(p, q). | ||
83 | """)); | ||
84 | } | ||
85 | |||
86 | @Test | ||
87 | void multipleParametersTest() { | ||
88 | var p = new Variable("p"); | ||
89 | var q = new Variable("q"); | ||
90 | var friend = new Symbol<>("friend", 2, Boolean.class, false); | ||
91 | var friendView = new KeyOnlyRelationView<>(friend); | ||
92 | var dnf = Dnf.builder("Example").parameters(p, q).clause(friendView.call(p, q)).build(); | ||
93 | |||
94 | assertThat(dnf.toString(), is(""" | ||
95 | pred Example(p, q) <-> | ||
96 | @RelationView("key") friend(p, q). | ||
97 | """)); | ||
98 | } | ||
99 | |||
100 | @Test | ||
101 | void multipleLiteralsTest() { | ||
102 | var p = new Variable("p"); | ||
103 | var q = new Variable("q"); | ||
104 | var person = new Symbol<>("person", 1, Boolean.class, false); | ||
105 | var personView = new KeyOnlyRelationView<>(person); | ||
106 | var friend = new Symbol<>("friend", 2, Boolean.class, false); | ||
107 | var friendView = new KeyOnlyRelationView<>(friend); | ||
108 | var dnf = Dnf.builder("Example") | ||
109 | .parameter(p) | ||
110 | .clause( | ||
111 | personView.call(p), | ||
112 | personView.call(q), | ||
113 | friendView.call(p, q) | ||
114 | ) | ||
115 | .build(); | ||
116 | |||
117 | assertThat(dnf.toString(), is(""" | ||
118 | pred Example(p) <-> | ||
119 | @RelationView("key") person(p), | ||
120 | @RelationView("key") person(q), | ||
121 | @RelationView("key") friend(p, q). | ||
122 | """)); | ||
123 | } | ||
124 | |||
125 | @Test | ||
126 | void multipleClausesTest() { | ||
127 | var p = new Variable("p"); | ||
128 | var q = new Variable("q"); | ||
129 | var friend = new Symbol<>("friend", 2, Boolean.class, false); | ||
130 | var friendView = new KeyOnlyRelationView<>(friend); | ||
131 | var dnf = Dnf.builder("Example") | ||
132 | .parameter(p) | ||
133 | .clause(friendView.call(p, q)) | ||
134 | .clause(friendView.call(q, p)) | ||
135 | .build(); | ||
136 | |||
137 | assertThat(dnf.toString(), is(""" | ||
138 | pred Example(p) <-> | ||
139 | @RelationView("key") friend(p, q) | ||
140 | ; | ||
141 | @RelationView("key") friend(q, p). | ||
142 | """)); | ||
143 | } | ||
144 | |||
145 | @Test | ||
146 | void dnfTest() { | ||
147 | var p = new Variable("p"); | ||
148 | var q = new Variable("q"); | ||
149 | var r = new Variable("r"); | ||
150 | var s = new Variable("s"); | ||
151 | var person = new Symbol<>("person", 1, Boolean.class, false); | ||
152 | var personView = new KeyOnlyRelationView<>(person); | ||
153 | var friend = new Symbol<>("friend", 2, Boolean.class, false); | ||
154 | var friendView = new KeyOnlyRelationView<>(friend); | ||
155 | var called = Dnf.builder("Called").parameters(r, s).clause(friendView.call(r, s)).build(); | ||
156 | var dnf = Dnf.builder("Example") | ||
157 | .parameter(p) | ||
158 | .clause( | ||
159 | personView.call(p), | ||
160 | personView.call(q), | ||
161 | not(called.call(p, q)) | ||
162 | ) | ||
163 | .build(); | ||
164 | |||
165 | assertThat(dnf.toString(), is(""" | ||
166 | pred Example(p) <-> | ||
167 | @RelationView("key") person(p), | ||
168 | @RelationView("key") person(q), | ||
169 | !(@Dnf Called(p, q)). | ||
170 | """)); | ||
171 | } | ||
172 | } | ||
diff --git a/subprojects/store-query/src/test/java/tools/refinery/store/query/tests/StructurallyEqualToTest.java b/subprojects/store-query/src/test/java/tools/refinery/store/query/tests/StructurallyEqualToTest.java new file mode 100644 index 00000000..0cda22df --- /dev/null +++ b/subprojects/store-query/src/test/java/tools/refinery/store/query/tests/StructurallyEqualToTest.java | |||
@@ -0,0 +1,77 @@ | |||
1 | package tools.refinery.store.query.tests; | ||
2 | |||
3 | import org.junit.jupiter.api.Test; | ||
4 | import tools.refinery.store.query.Dnf; | ||
5 | import tools.refinery.store.query.Variable; | ||
6 | import tools.refinery.store.query.view.KeyOnlyRelationView; | ||
7 | import tools.refinery.store.representation.Symbol; | ||
8 | |||
9 | import static org.hamcrest.CoreMatchers.containsString; | ||
10 | import static org.hamcrest.MatcherAssert.assertThat; | ||
11 | import static org.junit.jupiter.api.Assertions.assertThrows; | ||
12 | import static tools.refinery.store.query.tests.QueryMatchers.structurallyEqualTo; | ||
13 | |||
14 | class StructurallyEqualToTest { | ||
15 | @Test | ||
16 | void flatEqualsTest() { | ||
17 | var p = new Variable("p"); | ||
18 | var q = new Variable("q"); | ||
19 | var person = new Symbol<>("Person", 1, Boolean.class, false); | ||
20 | var personView = new KeyOnlyRelationView<>(person); | ||
21 | |||
22 | var expected = Dnf.builder("Expected").parameters(q).clause(personView.call(q)).build(); | ||
23 | var actual = Dnf.builder("Actual").parameters(p).clause(personView.call(p)).build(); | ||
24 | |||
25 | assertThat(actual, structurallyEqualTo(expected)); | ||
26 | } | ||
27 | |||
28 | @Test | ||
29 | void flatNotEqualsTest() { | ||
30 | var p = new Variable("p"); | ||
31 | var q = new Variable("q"); | ||
32 | var person = new Symbol<>("Person", 1, Boolean.class, false); | ||
33 | var personView = new KeyOnlyRelationView<>(person); | ||
34 | |||
35 | var expected = Dnf.builder("Expected").parameters(q).clause(personView.call(q)).build(); | ||
36 | var actual = Dnf.builder("Actual").parameters(p).clause(personView.call(q)).build(); | ||
37 | |||
38 | var assertion = structurallyEqualTo(expected); | ||
39 | assertThrows(AssertionError.class, () -> assertThat(actual, assertion)); | ||
40 | } | ||
41 | |||
42 | @Test | ||
43 | void deepEqualsTest() { | ||
44 | var p = new Variable("p"); | ||
45 | var q = new Variable("q"); | ||
46 | var person = new Symbol<>("Person", 1, Boolean.class, false); | ||
47 | var personView = new KeyOnlyRelationView<>(person); | ||
48 | |||
49 | var expected = Dnf.builder("Expected").parameters(q).clause( | ||
50 | Dnf.builder("Expected2").parameters(p).clause(personView.call(p)).build().call(q) | ||
51 | ).build(); | ||
52 | var actual = Dnf.builder("Actual").parameters(q).clause( | ||
53 | Dnf.builder("Actual2").parameters(p).clause(personView.call(p)).build().call(q) | ||
54 | ).build(); | ||
55 | |||
56 | assertThat(actual, structurallyEqualTo(expected)); | ||
57 | } | ||
58 | |||
59 | @Test | ||
60 | void deepNotEqualsTest() { | ||
61 | var p = new Variable("p"); | ||
62 | var q = new Variable("q"); | ||
63 | var person = new Symbol<>("Person", 1, Boolean.class, false); | ||
64 | var personView = new KeyOnlyRelationView<>(person); | ||
65 | |||
66 | var expected = Dnf.builder("Expected").parameters(q).clause( | ||
67 | Dnf.builder("Expected2").parameters(p).clause(personView.call(p)).build().call(q) | ||
68 | ).build(); | ||
69 | var actual = Dnf.builder("Actual").parameters(q).clause( | ||
70 | Dnf.builder("Actual2").parameters(p).clause(personView.call(q)).build().call(q) | ||
71 | ).build(); | ||
72 | |||
73 | var assertion = structurallyEqualTo(expected); | ||
74 | var error = assertThrows(AssertionError.class, () -> assertThat(actual, assertion)); | ||
75 | assertThat(error.getMessage(), containsString(" called from Expected ")); | ||
76 | } | ||
77 | } | ||
diff --git a/subprojects/store-query/src/testFixtures/java/tools/refinery/store/query/tests/MismatchDescribingDnfEqualityChecker.java b/subprojects/store-query/src/testFixtures/java/tools/refinery/store/query/tests/MismatchDescribingDnfEqualityChecker.java new file mode 100644 index 00000000..aaab2e7e --- /dev/null +++ b/subprojects/store-query/src/testFixtures/java/tools/refinery/store/query/tests/MismatchDescribingDnfEqualityChecker.java | |||
@@ -0,0 +1,43 @@ | |||
1 | package tools.refinery.store.query.tests; | ||
2 | |||
3 | import org.hamcrest.Description; | ||
4 | import tools.refinery.store.query.equality.DeepDnfEqualityChecker; | ||
5 | |||
6 | class MismatchDescribingDnfEqualityChecker extends DeepDnfEqualityChecker { | ||
7 | private final Description description; | ||
8 | private boolean described; | ||
9 | |||
10 | MismatchDescribingDnfEqualityChecker(Description description) { | ||
11 | this.description = description; | ||
12 | } | ||
13 | |||
14 | public boolean isDescribed() { | ||
15 | return described; | ||
16 | } | ||
17 | |||
18 | @Override | ||
19 | protected boolean doCheckEqual(Pair pair) { | ||
20 | boolean result = super.doCheckEqual(pair); | ||
21 | if (!result && !described) { | ||
22 | describeMismatch(pair); | ||
23 | // Only describe the first found (innermost) mismatch. | ||
24 | described = true; | ||
25 | } | ||
26 | return result; | ||
27 | } | ||
28 | |||
29 | private void describeMismatch(Pair pair) { | ||
30 | var inProgress = getInProgress(); | ||
31 | int size = inProgress.size(); | ||
32 | if (size <= 1) { | ||
33 | description.appendText("was ").appendValue(pair.left()); | ||
34 | return; | ||
35 | } | ||
36 | var last = inProgress.get(size - 1); | ||
37 | description.appendText("expected ").appendValue(last.right()); | ||
38 | for (int i = size - 2; i >= 0; i--) { | ||
39 | description.appendText(" called from ").appendText(inProgress.get(i).left().name()); | ||
40 | } | ||
41 | description.appendText(" was not structurally equal to ").appendValue(last.right()); | ||
42 | } | ||
43 | } | ||
diff --git a/subprojects/store-query/src/testFixtures/java/tools/refinery/store/query/tests/QueryMatchers.java b/subprojects/store-query/src/testFixtures/java/tools/refinery/store/query/tests/QueryMatchers.java new file mode 100644 index 00000000..83614278 --- /dev/null +++ b/subprojects/store-query/src/testFixtures/java/tools/refinery/store/query/tests/QueryMatchers.java | |||
@@ -0,0 +1,14 @@ | |||
1 | package tools.refinery.store.query.tests; | ||
2 | |||
3 | import org.hamcrest.Matcher; | ||
4 | import tools.refinery.store.query.Dnf; | ||
5 | |||
6 | public final class QueryMatchers { | ||
7 | private QueryMatchers() { | ||
8 | throw new IllegalStateException("This is a static utility class and should not be instantiated directly"); | ||
9 | } | ||
10 | |||
11 | public static Matcher<Dnf> structurallyEqualTo(Dnf expected) { | ||
12 | return new StructurallyEqualTo(expected); | ||
13 | } | ||
14 | } | ||
diff --git a/subprojects/store-query/src/testFixtures/java/tools/refinery/store/query/tests/StructurallyEqualTo.java b/subprojects/store-query/src/testFixtures/java/tools/refinery/store/query/tests/StructurallyEqualTo.java new file mode 100644 index 00000000..a42396dd --- /dev/null +++ b/subprojects/store-query/src/testFixtures/java/tools/refinery/store/query/tests/StructurallyEqualTo.java | |||
@@ -0,0 +1,36 @@ | |||
1 | package tools.refinery.store.query.tests; | ||
2 | |||
3 | import org.hamcrest.Description; | ||
4 | import org.hamcrest.TypeSafeMatcher; | ||
5 | import tools.refinery.store.query.Dnf; | ||
6 | import tools.refinery.store.query.equality.DeepDnfEqualityChecker; | ||
7 | |||
8 | public class StructurallyEqualTo extends TypeSafeMatcher<Dnf> { | ||
9 | private final Dnf expected; | ||
10 | |||
11 | public StructurallyEqualTo(Dnf expected) { | ||
12 | this.expected = expected; | ||
13 | } | ||
14 | |||
15 | @Override | ||
16 | protected boolean matchesSafely(Dnf item) { | ||
17 | var checker = new DeepDnfEqualityChecker(); | ||
18 | return checker.dnfEqual(expected, item); | ||
19 | } | ||
20 | |||
21 | @Override | ||
22 | protected void describeMismatchSafely(Dnf item, Description mismatchDescription) { | ||
23 | var describingChecker = new MismatchDescribingDnfEqualityChecker(mismatchDescription); | ||
24 | if (describingChecker.dnfEqual(expected, item)) { | ||
25 | throw new IllegalStateException("Mismatched Dnf was matching on repeated comparison"); | ||
26 | } | ||
27 | if (!describingChecker.isDescribed()) { | ||
28 | super.describeMismatchSafely(item, mismatchDescription); | ||
29 | } | ||
30 | } | ||
31 | |||
32 | @Override | ||
33 | public void describeTo(Description description) { | ||
34 | description.appendText("structurally equal to ").appendValue(expected); | ||
35 | } | ||
36 | } | ||