diff options
55 files changed, 2385 insertions, 146 deletions
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AbstractCallLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AbstractCallLiteral.java index b309f24b..3722f7f9 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AbstractCallLiteral.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AbstractCallLiteral.java | |||
@@ -100,10 +100,10 @@ public abstract class AbstractCallLiteral extends AbstractLiteral { | |||
100 | if (Objects.equals(target, newTarget)) { | 100 | if (Objects.equals(target, newTarget)) { |
101 | return this; | 101 | return this; |
102 | } | 102 | } |
103 | return internalWithTarget(newTarget); | 103 | return withArguments(newTarget, arguments); |
104 | } | 104 | } |
105 | 105 | ||
106 | protected abstract AbstractCallLiteral internalWithTarget(Constraint newTarget); | 106 | public abstract AbstractCallLiteral withArguments(Constraint newTarget, List<Variable> newArguments); |
107 | 107 | ||
108 | @Override | 108 | @Override |
109 | public boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other) { | 109 | public boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other) { |
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AggregationLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AggregationLiteral.java index dac34332..a2f8e009 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AggregationLiteral.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AggregationLiteral.java | |||
@@ -92,8 +92,8 @@ public class AggregationLiteral<R, T> extends AbstractCallLiteral { | |||
92 | } | 92 | } |
93 | 93 | ||
94 | @Override | 94 | @Override |
95 | protected AbstractCallLiteral internalWithTarget(Constraint newTarget) { | 95 | public AbstractCallLiteral withArguments(Constraint newTarget, List<Variable> newArguments) { |
96 | return new AggregationLiteral<>(resultVariable, aggregator, inputVariable, newTarget, getArguments()); | 96 | return new AggregationLiteral<>(resultVariable, aggregator, inputVariable, newTarget, newArguments); |
97 | } | 97 | } |
98 | 98 | ||
99 | @Override | 99 | @Override |
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 3a80cefd..1b05943d 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 | |||
@@ -102,8 +102,8 @@ public final class CallLiteral extends AbstractCallLiteral implements CanNegate< | |||
102 | } | 102 | } |
103 | 103 | ||
104 | @Override | 104 | @Override |
105 | protected AbstractCallLiteral internalWithTarget(Constraint newTarget) { | 105 | public AbstractCallLiteral withArguments(Constraint newTarget, List<Variable> newArguments) { |
106 | return new CallLiteral(polarity, newTarget, getArguments()); | 106 | return new CallLiteral(polarity, newTarget, newArguments); |
107 | } | 107 | } |
108 | 108 | ||
109 | @Override | 109 | @Override |
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CountLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CountLiteral.java index e5f6ac0c..3d078d89 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CountLiteral.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CountLiteral.java | |||
@@ -34,8 +34,8 @@ public class CountLiteral extends AbstractCountLiteral<Integer> { | |||
34 | } | 34 | } |
35 | 35 | ||
36 | @Override | 36 | @Override |
37 | protected AbstractCallLiteral internalWithTarget(Constraint newTarget) { | 37 | public AbstractCallLiteral withArguments(Constraint newTarget, List<Variable> newArguments) { |
38 | return new CountLiteral(getResultVariable(), newTarget, getArguments()); | 38 | return new CountLiteral(getResultVariable(), newTarget, newArguments); |
39 | } | 39 | } |
40 | 40 | ||
41 | @Override | 41 | @Override |
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/RepresentativeElectionLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/RepresentativeElectionLiteral.java index 876ae253..5d57c06c 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/RepresentativeElectionLiteral.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/RepresentativeElectionLiteral.java | |||
@@ -77,8 +77,8 @@ public class RepresentativeElectionLiteral extends AbstractCallLiteral { | |||
77 | } | 77 | } |
78 | 78 | ||
79 | @Override | 79 | @Override |
80 | protected AbstractCallLiteral internalWithTarget(Constraint newTarget) { | 80 | public AbstractCallLiteral withArguments(Constraint newTarget, List<Variable> newArguments) { |
81 | return new RepresentativeElectionLiteral(connectivity, newTarget, getArguments()); | 81 | return new RepresentativeElectionLiteral(connectivity, newTarget, newArguments); |
82 | } | 82 | } |
83 | 83 | ||
84 | @Override | 84 | @Override |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialClauseRewriter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialClauseRewriter.java index c560162e..40993235 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialClauseRewriter.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialClauseRewriter.java | |||
@@ -7,8 +7,10 @@ package tools.refinery.store.reasoning.internal; | |||
7 | 7 | ||
8 | import tools.refinery.store.query.Constraint; | 8 | import tools.refinery.store.query.Constraint; |
9 | import tools.refinery.store.query.dnf.Dnf; | 9 | import tools.refinery.store.query.dnf.Dnf; |
10 | import tools.refinery.store.query.dnf.DnfBuilder; | ||
10 | import tools.refinery.store.query.dnf.DnfClause; | 11 | import tools.refinery.store.query.dnf.DnfClause; |
11 | import tools.refinery.store.query.literal.AbstractCallLiteral; | 12 | import tools.refinery.store.query.literal.AbstractCallLiteral; |
13 | import tools.refinery.store.query.literal.AbstractCountLiteral; | ||
12 | import tools.refinery.store.query.literal.CallPolarity; | 14 | import tools.refinery.store.query.literal.CallPolarity; |
13 | import tools.refinery.store.query.literal.Literal; | 15 | import tools.refinery.store.query.literal.Literal; |
14 | import tools.refinery.store.query.term.Aggregator; | 16 | import tools.refinery.store.query.term.Aggregator; |
@@ -17,6 +19,7 @@ import tools.refinery.store.query.term.Term; | |||
17 | import tools.refinery.store.query.term.Variable; | 19 | import tools.refinery.store.query.term.Variable; |
18 | import tools.refinery.store.query.term.int_.IntTerms; | 20 | import tools.refinery.store.query.term.int_.IntTerms; |
19 | import tools.refinery.store.query.term.uppercardinality.UpperCardinalityTerms; | 21 | import tools.refinery.store.query.term.uppercardinality.UpperCardinalityTerms; |
22 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
20 | import tools.refinery.store.reasoning.literal.*; | 23 | import tools.refinery.store.reasoning.literal.*; |
21 | import tools.refinery.store.reasoning.representation.PartialRelation; | 24 | import tools.refinery.store.reasoning.representation.PartialRelation; |
22 | import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator; | 25 | import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator; |
@@ -58,6 +61,14 @@ class PartialClauseRewriter { | |||
58 | rewriteCountUpperBound(countUpperBoundLiteral); | 61 | rewriteCountUpperBound(countUpperBoundLiteral); |
59 | return; | 62 | return; |
60 | } | 63 | } |
64 | if (callLiteral instanceof CountCandidateLowerBoundLiteral countCandidateLowerBoundLiteral) { | ||
65 | rewriteCountCandidateLowerBound(countCandidateLowerBoundLiteral); | ||
66 | return; | ||
67 | } | ||
68 | if (callLiteral instanceof CountCandidateUpperBoundLiteral countCandidateUpperBoundLiteral) { | ||
69 | rewriteCountCandidateUpperBound(countCandidateUpperBoundLiteral); | ||
70 | return; | ||
71 | } | ||
61 | var target = callLiteral.getTarget(); | 72 | var target = callLiteral.getTarget(); |
62 | if (target instanceof Dnf dnf) { | 73 | if (target instanceof Dnf dnf) { |
63 | rewriteRecursively(callLiteral, dnf); | 74 | rewriteRecursively(callLiteral, dnf); |
@@ -78,48 +89,26 @@ class PartialClauseRewriter { | |||
78 | } | 89 | } |
79 | 90 | ||
80 | private void rewriteCountLowerBound(CountLowerBoundLiteral literal) { | 91 | private void rewriteCountLowerBound(CountLowerBoundLiteral literal) { |
81 | rewriteCount(literal, "lower", Modality.MUST, MultiObjectTranslator.LOWER_CARDINALITY_VIEW, 1, IntTerms::mul, | 92 | rewritePartialCount(literal, "lower", Modality.MUST, MultiObjectTranslator.LOWER_CARDINALITY_VIEW, 1, |
82 | IntTerms.INT_SUM); | 93 | IntTerms::mul, IntTerms.INT_SUM); |
83 | } | 94 | } |
84 | 95 | ||
85 | private void rewriteCountUpperBound(CountUpperBoundLiteral literal) { | 96 | private void rewriteCountUpperBound(CountUpperBoundLiteral literal) { |
86 | rewriteCount(literal, "upper", Modality.MAY, MultiObjectTranslator.UPPER_CARDINALITY_VIEW, | 97 | rewritePartialCount(literal, "upper", Modality.MAY, MultiObjectTranslator.UPPER_CARDINALITY_VIEW, |
87 | UpperCardinalities.ONE, UpperCardinalityTerms::mul, UpperCardinalityTerms.UPPER_CARDINALITY_SUM); | 98 | UpperCardinalities.ONE, UpperCardinalityTerms::mul, UpperCardinalityTerms.UPPER_CARDINALITY_SUM); |
88 | } | 99 | } |
89 | 100 | ||
90 | private <T> void rewriteCount(ConcreteCountLiteral<T> literal, String name, Modality modality, Constraint view, | 101 | private <T> void rewritePartialCount(AbstractCountLiteral<T> literal, String name, Modality modality, |
91 | T one, BinaryOperator<Term<T>> mul, Aggregator<T, T> sum) { | 102 | Constraint view, T one, BinaryOperator<Term<T>> mul, Aggregator<T, T> sum) { |
92 | var type = literal.getResultType(); | 103 | var type = literal.getResultType(); |
93 | var target = literal.getTarget(); | 104 | var countResult = computeCountVariables(literal, Concreteness.PARTIAL, name); |
94 | var concreteness = literal.getConcreteness(); | 105 | var builder = countResult.builder(); |
95 | int arity = target.arity(); | ||
96 | var parameters = target.getParameters(); | ||
97 | var literalArguments = literal.getArguments(); | ||
98 | var privateVariables = literal.getPrivateVariables(positiveVariables); | ||
99 | |||
100 | var builder = Dnf.builder("%s#%s#%s".formatted(target.name(), concreteness, name)); | ||
101 | var rewrittenArguments = new ArrayList<Variable>(parameters.size()); | ||
102 | var variablesToCount = new ArrayList<Variable>(); | ||
103 | var helperArguments = new ArrayList<Variable>(); | ||
104 | var literalToRewrittenArgumentMap = new HashMap<Variable, Variable>(); | ||
105 | for (int i = 0; i < arity; i++) { | ||
106 | var literalArgument = literalArguments.get(i); | ||
107 | var parameter = parameters.get(i); | ||
108 | var rewrittenArgument = literalToRewrittenArgumentMap.computeIfAbsent(literalArgument, key -> { | ||
109 | helperArguments.add(key); | ||
110 | var newArgument = builder.parameter(parameter); | ||
111 | if (privateVariables.contains(key)) { | ||
112 | variablesToCount.add(newArgument); | ||
113 | } | ||
114 | return newArgument; | ||
115 | }); | ||
116 | rewrittenArguments.add(rewrittenArgument); | ||
117 | } | ||
118 | var outputVariable = builder.parameter(type); | 106 | var outputVariable = builder.parameter(type); |
107 | var variablesToCount = countResult.variablesToCount(); | ||
119 | 108 | ||
120 | var literals = new ArrayList<Literal>(); | 109 | var literals = new ArrayList<Literal>(); |
121 | literals.add(new ModalConstraint(modality, literal.getConcreteness(), target) | 110 | literals.add(new ModalConstraint(modality, Concreteness.PARTIAL, literal.getTarget()) |
122 | .call(CallPolarity.POSITIVE, rewrittenArguments)); | 111 | .call(CallPolarity.POSITIVE, countResult.rewrittenArguments())); |
123 | switch (variablesToCount.size()) { | 112 | switch (variablesToCount.size()) { |
124 | case 0 -> literals.add(outputVariable.assign(new ConstantTerm<>(type, one))); | 113 | case 0 -> literals.add(outputVariable.assign(new ConstantTerm<>(type, one))); |
125 | case 1 -> literals.add(view.call(variablesToCount.get(0), | 114 | case 1 -> literals.add(view.call(variablesToCount.get(0), |
@@ -141,11 +130,65 @@ class PartialClauseRewriter { | |||
141 | 130 | ||
142 | var helperQuery = builder.build(); | 131 | var helperQuery = builder.build(); |
143 | var aggregationVariable = Variable.of(type); | 132 | var aggregationVariable = Variable.of(type); |
133 | var helperArguments = countResult.helperArguments(); | ||
144 | helperArguments.add(aggregationVariable); | 134 | helperArguments.add(aggregationVariable); |
145 | workList.addFirst(literal.getResultVariable().assign(helperQuery.aggregateBy(aggregationVariable, sum, | 135 | workList.addFirst(literal.getResultVariable().assign(helperQuery.aggregateBy(aggregationVariable, sum, |
146 | helperArguments))); | 136 | helperArguments))); |
147 | } | 137 | } |
148 | 138 | ||
139 | private void rewriteCountCandidateLowerBound(CountCandidateLowerBoundLiteral literal) { | ||
140 | rewriteCandidateCount(literal, "lower", Modality.MAY); | ||
141 | } | ||
142 | |||
143 | private void rewriteCountCandidateUpperBound(CountCandidateUpperBoundLiteral literal) { | ||
144 | rewriteCandidateCount(literal, "upper", Modality.MUST); | ||
145 | } | ||
146 | |||
147 | private void rewriteCandidateCount(AbstractCountLiteral<Integer> literal, String name, Modality modality) { | ||
148 | var countResult = computeCountVariables(literal, Concreteness.CANDIDATE, name); | ||
149 | var builder = countResult.builder(); | ||
150 | |||
151 | var literals = new ArrayList<Literal>(); | ||
152 | literals.add(new ModalConstraint(modality, Concreteness.CANDIDATE, literal.getTarget()) | ||
153 | .call(CallPolarity.POSITIVE, countResult.rewrittenArguments())); | ||
154 | for (var variable : countResult.variablesToCount()) { | ||
155 | literals.add(new ModalConstraint(modality, Concreteness.CANDIDATE, ReasoningAdapter.EXISTS_SYMBOL) | ||
156 | .call(variable)); | ||
157 | } | ||
158 | builder.clause(literals); | ||
159 | |||
160 | var helperQuery = builder.build(); | ||
161 | workList.addFirst(literal.getResultVariable().assign(helperQuery.count(countResult.helperArguments()))); | ||
162 | } | ||
163 | |||
164 | private CountResult computeCountVariables(AbstractCountLiteral<?> literal, Concreteness concreteness, | ||
165 | String name) { | ||
166 | var target = literal.getTarget(); | ||
167 | int arity = target.arity(); | ||
168 | var parameters = target.getParameters(); | ||
169 | var literalArguments = literal.getArguments(); | ||
170 | var privateVariables = literal.getPrivateVariables(positiveVariables); | ||
171 | var builder = Dnf.builder("%s#%s#%s".formatted(target.name(), concreteness, name)); | ||
172 | var rewrittenArguments = new ArrayList<Variable>(parameters.size()); | ||
173 | var variablesToCount = new ArrayList<Variable>(); | ||
174 | var helperArguments = new ArrayList<Variable>(); | ||
175 | var literalToRewrittenArgumentMap = new HashMap<Variable, Variable>(); | ||
176 | for (int i = 0; i < arity; i++) { | ||
177 | var literalArgument = literalArguments.get(i); | ||
178 | var parameter = parameters.get(i); | ||
179 | var rewrittenArgument = literalToRewrittenArgumentMap.computeIfAbsent(literalArgument, key -> { | ||
180 | helperArguments.add(key); | ||
181 | var newArgument = builder.parameter(parameter); | ||
182 | if (privateVariables.contains(key)) { | ||
183 | variablesToCount.add(newArgument); | ||
184 | } | ||
185 | return newArgument; | ||
186 | }); | ||
187 | rewrittenArguments.add(rewrittenArgument); | ||
188 | } | ||
189 | return new CountResult(builder, rewrittenArguments, helperArguments, variablesToCount); | ||
190 | } | ||
191 | |||
149 | private void markAsDone(Literal literal) { | 192 | private void markAsDone(Literal literal) { |
150 | completedLiterals.add(literal); | 193 | completedLiterals.add(literal); |
151 | positiveVariables.addAll(literal.getOutputVariables()); | 194 | positiveVariables.addAll(literal.getOutputVariables()); |
@@ -173,4 +216,8 @@ class PartialClauseRewriter { | |||
173 | workList.addFirst(literals.get(i)); | 216 | workList.addFirst(literals.get(i)); |
174 | } | 217 | } |
175 | } | 218 | } |
219 | |||
220 | private record CountResult(DnfBuilder builder, List<Variable> rewrittenArguments, List<Variable> helperArguments, | ||
221 | List<Variable> variablesToCount) { | ||
222 | } | ||
176 | } | 223 | } |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/DnfLifter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/DnfLifter.java index f878b674..889f595f 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/DnfLifter.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/DnfLifter.java | |||
@@ -41,7 +41,7 @@ public class DnfLifter { | |||
41 | var modality = modalDnf.modality(); | 41 | var modality = modalDnf.modality(); |
42 | var concreteness = modalDnf.concreteness(); | 42 | var concreteness = modalDnf.concreteness(); |
43 | var dnf = modalDnf.dnf(); | 43 | var dnf = modalDnf.dnf(); |
44 | var builder = Dnf.builder("%s#%s#%s".formatted(dnf.name(), modality, concreteness)); | 44 | var builder = Dnf.builder(decorateName(dnf.name(), modality, concreteness)); |
45 | builder.symbolicParameters(dnf.getSymbolicParameters()); | 45 | builder.symbolicParameters(dnf.getSymbolicParameters()); |
46 | builder.functionalDependencies(dnf.getFunctionalDependencies()); | 46 | builder.functionalDependencies(dnf.getFunctionalDependencies()); |
47 | for (var clause : dnf.getClauses()) { | 47 | for (var clause : dnf.getClauses()) { |
@@ -65,4 +65,8 @@ public class DnfLifter { | |||
65 | return "%s %s %s".formatted(modality, concreteness, dnf.name()); | 65 | return "%s %s %s".formatted(modality, concreteness, dnf.name()); |
66 | } | 66 | } |
67 | } | 67 | } |
68 | |||
69 | public static String decorateName(String name, Modality modality, Concreteness concreteness) { | ||
70 | return "%s#%s#%s".formatted(name, modality, concreteness); | ||
71 | } | ||
68 | } | 72 | } |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ConcreteCountLiteral.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ConcreteCountLiteral.java deleted file mode 100644 index 91b30964..00000000 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ConcreteCountLiteral.java +++ /dev/null | |||
@@ -1,47 +0,0 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.literal; | ||
7 | |||
8 | import tools.refinery.store.query.Constraint; | ||
9 | import tools.refinery.store.query.equality.LiteralEqualityHelper; | ||
10 | import tools.refinery.store.query.equality.LiteralHashCodeHelper; | ||
11 | import tools.refinery.store.query.literal.AbstractCountLiteral; | ||
12 | import tools.refinery.store.query.literal.Literal; | ||
13 | import tools.refinery.store.query.term.DataVariable; | ||
14 | import tools.refinery.store.query.term.Variable; | ||
15 | |||
16 | import java.util.List; | ||
17 | import java.util.Objects; | ||
18 | |||
19 | // {@link Object#equals(Object)} is implemented by {@link AbstractLiteral}. | ||
20 | @SuppressWarnings("squid:S2160") | ||
21 | public abstract class ConcreteCountLiteral<T> extends AbstractCountLiteral<T> { | ||
22 | private final Concreteness concreteness; | ||
23 | |||
24 | protected ConcreteCountLiteral(Class<T> resultType, DataVariable<T> resultVariable, Concreteness concreteness, | ||
25 | Constraint target, List<Variable> arguments) { | ||
26 | super(resultType, resultVariable, target, arguments); | ||
27 | this.concreteness = concreteness; | ||
28 | } | ||
29 | |||
30 | public Concreteness getConcreteness() { | ||
31 | return concreteness; | ||
32 | } | ||
33 | |||
34 | @Override | ||
35 | public boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other) { | ||
36 | if (!super.equalsWithSubstitution(helper, other)) { | ||
37 | return false; | ||
38 | } | ||
39 | var otherCountLiteral = (ConcreteCountLiteral<?>) other; | ||
40 | return Objects.equals(concreteness, otherCountLiteral.concreteness); | ||
41 | } | ||
42 | |||
43 | @Override | ||
44 | public int hashCodeWithSubstitution(LiteralHashCodeHelper helper) { | ||
45 | return Objects.hash(super.hashCodeWithSubstitution(helper), concreteness); | ||
46 | } | ||
47 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountCandidateLowerBoundLiteral.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountCandidateLowerBoundLiteral.java new file mode 100644 index 00000000..91dd2b72 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountCandidateLowerBoundLiteral.java | |||
@@ -0,0 +1,49 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.literal; | ||
7 | |||
8 | import tools.refinery.store.query.Constraint; | ||
9 | import tools.refinery.store.query.literal.AbstractCallLiteral; | ||
10 | import tools.refinery.store.query.literal.AbstractCountLiteral; | ||
11 | import tools.refinery.store.query.literal.Literal; | ||
12 | import tools.refinery.store.query.substitution.Substitution; | ||
13 | import tools.refinery.store.query.term.DataVariable; | ||
14 | import tools.refinery.store.query.term.Variable; | ||
15 | |||
16 | import java.util.List; | ||
17 | |||
18 | public class CountCandidateLowerBoundLiteral extends AbstractCountLiteral<Integer> { | ||
19 | public CountCandidateLowerBoundLiteral(DataVariable<Integer> resultVariable, Constraint target, | ||
20 | List<Variable> arguments) { | ||
21 | super(Integer.class, resultVariable, target, arguments); | ||
22 | } | ||
23 | |||
24 | @Override | ||
25 | protected Integer zero() { | ||
26 | return 0; | ||
27 | } | ||
28 | |||
29 | @Override | ||
30 | protected Integer one() { | ||
31 | return 1; | ||
32 | } | ||
33 | |||
34 | @Override | ||
35 | protected Literal doSubstitute(Substitution substitution, List<Variable> substitutedArguments) { | ||
36 | return new CountCandidateLowerBoundLiteral(substitution.getTypeSafeSubstitute(getResultVariable()), getTarget(), | ||
37 | substitutedArguments); | ||
38 | } | ||
39 | |||
40 | @Override | ||
41 | public AbstractCallLiteral withArguments(Constraint newTarget, List<Variable> newArguments) { | ||
42 | return new CountCandidateLowerBoundLiteral(getResultVariable(), newTarget, newArguments); | ||
43 | } | ||
44 | |||
45 | @Override | ||
46 | protected String operatorName() { | ||
47 | return "@LowerBound(\"candidate\") count"; | ||
48 | } | ||
49 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountCandidateUpperBoundLiteral.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountCandidateUpperBoundLiteral.java new file mode 100644 index 00000000..94c9399d --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountCandidateUpperBoundLiteral.java | |||
@@ -0,0 +1,49 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.literal; | ||
7 | |||
8 | import tools.refinery.store.query.Constraint; | ||
9 | import tools.refinery.store.query.literal.AbstractCallLiteral; | ||
10 | import tools.refinery.store.query.literal.AbstractCountLiteral; | ||
11 | import tools.refinery.store.query.literal.Literal; | ||
12 | import tools.refinery.store.query.substitution.Substitution; | ||
13 | import tools.refinery.store.query.term.DataVariable; | ||
14 | import tools.refinery.store.query.term.Variable; | ||
15 | |||
16 | import java.util.List; | ||
17 | |||
18 | public class CountCandidateUpperBoundLiteral extends AbstractCountLiteral<Integer> { | ||
19 | public CountCandidateUpperBoundLiteral(DataVariable<Integer> resultVariable, Constraint target, | ||
20 | List<Variable> arguments) { | ||
21 | super(Integer.class, resultVariable, target, arguments); | ||
22 | } | ||
23 | |||
24 | @Override | ||
25 | protected Integer zero() { | ||
26 | return 0; | ||
27 | } | ||
28 | |||
29 | @Override | ||
30 | protected Integer one() { | ||
31 | return 1; | ||
32 | } | ||
33 | |||
34 | @Override | ||
35 | protected Literal doSubstitute(Substitution substitution, List<Variable> substitutedArguments) { | ||
36 | return new CountCandidateUpperBoundLiteral(substitution.getTypeSafeSubstitute(getResultVariable()), getTarget(), | ||
37 | substitutedArguments); | ||
38 | } | ||
39 | |||
40 | @Override | ||
41 | public AbstractCallLiteral withArguments(Constraint newTarget, List<Variable> newArguments) { | ||
42 | return new CountCandidateUpperBoundLiteral(getResultVariable(), newTarget, newArguments); | ||
43 | } | ||
44 | |||
45 | @Override | ||
46 | protected String operatorName() { | ||
47 | return "@UpperBound(\"candidate\") count"; | ||
48 | } | ||
49 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountLowerBoundLiteral.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountLowerBoundLiteral.java index 261088fc..b75b0cab 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountLowerBoundLiteral.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountLowerBoundLiteral.java | |||
@@ -7,6 +7,7 @@ package tools.refinery.store.reasoning.literal; | |||
7 | 7 | ||
8 | import tools.refinery.store.query.Constraint; | 8 | import tools.refinery.store.query.Constraint; |
9 | import tools.refinery.store.query.literal.AbstractCallLiteral; | 9 | import tools.refinery.store.query.literal.AbstractCallLiteral; |
10 | import tools.refinery.store.query.literal.AbstractCountLiteral; | ||
10 | import tools.refinery.store.query.literal.Literal; | 11 | import tools.refinery.store.query.literal.Literal; |
11 | import tools.refinery.store.query.substitution.Substitution; | 12 | import tools.refinery.store.query.substitution.Substitution; |
12 | import tools.refinery.store.query.term.DataVariable; | 13 | import tools.refinery.store.query.term.DataVariable; |
@@ -14,10 +15,10 @@ import tools.refinery.store.query.term.Variable; | |||
14 | 15 | ||
15 | import java.util.List; | 16 | import java.util.List; |
16 | 17 | ||
17 | public class CountLowerBoundLiteral extends ConcreteCountLiteral<Integer> { | 18 | public class CountLowerBoundLiteral extends AbstractCountLiteral<Integer> { |
18 | public CountLowerBoundLiteral(DataVariable<Integer> resultVariable, Concreteness concreteness, Constraint target, | 19 | public CountLowerBoundLiteral(DataVariable<Integer> resultVariable, Constraint target, |
19 | List<Variable> arguments) { | 20 | List<Variable> arguments) { |
20 | super(Integer.class, resultVariable, concreteness, target, arguments); | 21 | super(Integer.class, resultVariable, target, arguments); |
21 | } | 22 | } |
22 | 23 | ||
23 | @Override | 24 | @Override |
@@ -32,17 +33,17 @@ public class CountLowerBoundLiteral extends ConcreteCountLiteral<Integer> { | |||
32 | 33 | ||
33 | @Override | 34 | @Override |
34 | protected Literal doSubstitute(Substitution substitution, List<Variable> substitutedArguments) { | 35 | protected Literal doSubstitute(Substitution substitution, List<Variable> substitutedArguments) { |
35 | return new CountLowerBoundLiteral(substitution.getTypeSafeSubstitute(getResultVariable()), getConcreteness(), | 36 | return new CountLowerBoundLiteral(substitution.getTypeSafeSubstitute(getResultVariable()), getTarget(), |
36 | getTarget(), substitutedArguments); | 37 | substitutedArguments); |
37 | } | 38 | } |
38 | 39 | ||
39 | @Override | 40 | @Override |
40 | protected AbstractCallLiteral internalWithTarget(Constraint newTarget) { | 41 | public AbstractCallLiteral withArguments(Constraint newTarget, List<Variable> newArguments) { |
41 | return new CountLowerBoundLiteral(getResultVariable(), getConcreteness(), newTarget, getArguments()); | 42 | return new CountLowerBoundLiteral(getResultVariable(), newTarget, newArguments); |
42 | } | 43 | } |
43 | 44 | ||
44 | @Override | 45 | @Override |
45 | protected String operatorName() { | 46 | protected String operatorName() { |
46 | return "@LowerBound(\"%s\") count".formatted(getConcreteness()); | 47 | return "@LowerBound(\"partial\") count"; |
47 | } | 48 | } |
48 | } | 49 | } |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountUpperBoundLiteral.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountUpperBoundLiteral.java index 960ded69..03842143 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountUpperBoundLiteral.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountUpperBoundLiteral.java | |||
@@ -7,6 +7,7 @@ package tools.refinery.store.reasoning.literal; | |||
7 | 7 | ||
8 | import tools.refinery.store.query.Constraint; | 8 | import tools.refinery.store.query.Constraint; |
9 | import tools.refinery.store.query.literal.AbstractCallLiteral; | 9 | import tools.refinery.store.query.literal.AbstractCallLiteral; |
10 | import tools.refinery.store.query.literal.AbstractCountLiteral; | ||
10 | import tools.refinery.store.query.literal.Literal; | 11 | import tools.refinery.store.query.literal.Literal; |
11 | import tools.refinery.store.query.substitution.Substitution; | 12 | import tools.refinery.store.query.substitution.Substitution; |
12 | import tools.refinery.store.query.term.DataVariable; | 13 | import tools.refinery.store.query.term.DataVariable; |
@@ -16,10 +17,10 @@ import tools.refinery.store.representation.cardinality.UpperCardinality; | |||
16 | 17 | ||
17 | import java.util.List; | 18 | import java.util.List; |
18 | 19 | ||
19 | public class CountUpperBoundLiteral extends ConcreteCountLiteral<UpperCardinality> { | 20 | public class CountUpperBoundLiteral extends AbstractCountLiteral<UpperCardinality> { |
20 | public CountUpperBoundLiteral(DataVariable<UpperCardinality> resultVariable, Concreteness concreteness, | 21 | public CountUpperBoundLiteral(DataVariable<UpperCardinality> resultVariable, Constraint target, |
21 | Constraint target, List<Variable> arguments) { | 22 | List<Variable> arguments) { |
22 | super(UpperCardinality.class, resultVariable, concreteness, target, arguments); | 23 | super(UpperCardinality.class, resultVariable, target, arguments); |
23 | } | 24 | } |
24 | 25 | ||
25 | @Override | 26 | @Override |
@@ -34,17 +35,17 @@ public class CountUpperBoundLiteral extends ConcreteCountLiteral<UpperCardinalit | |||
34 | 35 | ||
35 | @Override | 36 | @Override |
36 | protected Literal doSubstitute(Substitution substitution, List<Variable> substitutedArguments) { | 37 | protected Literal doSubstitute(Substitution substitution, List<Variable> substitutedArguments) { |
37 | return new CountUpperBoundLiteral(substitution.getTypeSafeSubstitute(getResultVariable()), getConcreteness(), | 38 | return new CountUpperBoundLiteral(substitution.getTypeSafeSubstitute(getResultVariable()), getTarget(), |
38 | getTarget(), substitutedArguments); | 39 | substitutedArguments); |
39 | } | 40 | } |
40 | 41 | ||
41 | @Override | 42 | @Override |
42 | protected AbstractCallLiteral internalWithTarget(Constraint newTarget) { | 43 | public AbstractCallLiteral withArguments(Constraint newTarget, List<Variable> newArguments) { |
43 | return new CountUpperBoundLiteral(getResultVariable(), getConcreteness(), newTarget, getArguments()); | 44 | return new CountUpperBoundLiteral(getResultVariable(), newTarget, newArguments); |
44 | } | 45 | } |
45 | 46 | ||
46 | @Override | 47 | @Override |
47 | protected String operatorName() { | 48 | protected String operatorName() { |
48 | return "@UpperBound(\"%s\") count".formatted(getConcreteness()); | 49 | return "@UpperBound(\"partial\") count"; |
49 | } | 50 | } |
50 | } | 51 | } |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/RefinementBasedInitializer.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/RefinementBasedInitializer.java new file mode 100644 index 00000000..b6bccb01 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/RefinementBasedInitializer.java | |||
@@ -0,0 +1,34 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.refinement; | ||
7 | |||
8 | import tools.refinery.store.model.Model; | ||
9 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
10 | import tools.refinery.store.reasoning.representation.PartialSymbol; | ||
11 | import tools.refinery.store.reasoning.seed.ModelSeed; | ||
12 | |||
13 | public class RefinementBasedInitializer<A, C> implements PartialModelInitializer { | ||
14 | private final PartialSymbol<A, C> partialSymbol; | ||
15 | |||
16 | public RefinementBasedInitializer(PartialSymbol<A, C> partialSymbol) { | ||
17 | this.partialSymbol = partialSymbol; | ||
18 | } | ||
19 | |||
20 | @Override | ||
21 | public void initialize(Model model, ModelSeed modelSeed) { | ||
22 | var refiner = model.getAdapter(ReasoningAdapter.class).getRefiner(partialSymbol); | ||
23 | var defaultValue = partialSymbol.abstractDomain().unknown(); | ||
24 | var cursor = modelSeed.getCursor(partialSymbol, defaultValue); | ||
25 | while (cursor.move()) { | ||
26 | var key = cursor.getKey(); | ||
27 | var value = cursor.getValue(); | ||
28 | if (!refiner.merge(key, value)) { | ||
29 | throw new IllegalArgumentException("Failed to merge value %s for key %s into %s" | ||
30 | .formatted(value, key, partialSymbol)); | ||
31 | } | ||
32 | } | ||
33 | } | ||
34 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialRelationTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialRelationTranslator.java index aee74eb3..6f9492a3 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialRelationTranslator.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialRelationTranslator.java | |||
@@ -9,6 +9,7 @@ import tools.refinery.store.model.ModelStoreBuilder; | |||
9 | import tools.refinery.store.query.Constraint; | 9 | import tools.refinery.store.query.Constraint; |
10 | import tools.refinery.store.query.ModelQueryBuilder; | 10 | import tools.refinery.store.query.ModelQueryBuilder; |
11 | import tools.refinery.store.query.dnf.Query; | 11 | import tools.refinery.store.query.dnf.Query; |
12 | import tools.refinery.store.query.dnf.QueryBuilder; | ||
12 | import tools.refinery.store.query.dnf.RelationalQuery; | 13 | import tools.refinery.store.query.dnf.RelationalQuery; |
13 | import tools.refinery.store.query.term.Variable; | 14 | import tools.refinery.store.query.term.Variable; |
14 | import tools.refinery.store.query.view.MayView; | 15 | import tools.refinery.store.query.view.MayView; |
@@ -18,16 +19,20 @@ import tools.refinery.store.reasoning.interpretation.PartialInterpretation; | |||
18 | import tools.refinery.store.reasoning.interpretation.PartialRelationRewriter; | 19 | import tools.refinery.store.reasoning.interpretation.PartialRelationRewriter; |
19 | import tools.refinery.store.reasoning.interpretation.QueryBasedRelationInterpretationFactory; | 20 | import tools.refinery.store.reasoning.interpretation.QueryBasedRelationInterpretationFactory; |
20 | import tools.refinery.store.reasoning.interpretation.QueryBasedRelationRewriter; | 21 | import tools.refinery.store.reasoning.interpretation.QueryBasedRelationRewriter; |
22 | import tools.refinery.store.reasoning.lifting.DnfLifter; | ||
21 | import tools.refinery.store.reasoning.literal.Concreteness; | 23 | import tools.refinery.store.reasoning.literal.Concreteness; |
22 | import tools.refinery.store.reasoning.literal.Modality; | 24 | import tools.refinery.store.reasoning.literal.Modality; |
23 | import tools.refinery.store.reasoning.refinement.ConcreteSymbolRefiner; | 25 | import tools.refinery.store.reasoning.refinement.ConcreteSymbolRefiner; |
24 | import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner; | 26 | import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner; |
27 | import tools.refinery.store.reasoning.refinement.PartialModelInitializer; | ||
25 | import tools.refinery.store.reasoning.refinement.StorageRefiner; | 28 | import tools.refinery.store.reasoning.refinement.StorageRefiner; |
26 | import tools.refinery.store.reasoning.representation.PartialRelation; | 29 | import tools.refinery.store.reasoning.representation.PartialRelation; |
27 | import tools.refinery.store.representation.AnySymbol; | 30 | import tools.refinery.store.representation.AnySymbol; |
28 | import tools.refinery.store.representation.Symbol; | 31 | import tools.refinery.store.representation.Symbol; |
29 | import tools.refinery.store.representation.TruthValue; | 32 | import tools.refinery.store.representation.TruthValue; |
30 | 33 | ||
34 | import java.util.function.BiConsumer; | ||
35 | |||
31 | @SuppressWarnings("UnusedReturnValue") | 36 | @SuppressWarnings("UnusedReturnValue") |
32 | public final class PartialRelationTranslator extends PartialSymbolTranslator<TruthValue, Boolean> { | 37 | public final class PartialRelationTranslator extends PartialSymbolTranslator<TruthValue, Boolean> { |
33 | private final PartialRelation partialRelation; | 38 | private final PartialRelation partialRelation; |
@@ -84,6 +89,12 @@ public final class PartialRelationTranslator extends PartialSymbolTranslator<Tru | |||
84 | return this; | 89 | return this; |
85 | } | 90 | } |
86 | 91 | ||
92 | @Override | ||
93 | public PartialRelationTranslator initializer(PartialModelInitializer initializer) { | ||
94 | super.initializer(initializer); | ||
95 | return this; | ||
96 | } | ||
97 | |||
87 | public PartialRelationTranslator query(RelationalQuery query) { | 98 | public PartialRelationTranslator query(RelationalQuery query) { |
88 | checkNotConfigured(); | 99 | checkNotConfigured(); |
89 | if (this.query != null) { | 100 | if (this.query != null) { |
@@ -102,6 +113,12 @@ public final class PartialRelationTranslator extends PartialSymbolTranslator<Tru | |||
102 | return this; | 113 | return this; |
103 | } | 114 | } |
104 | 115 | ||
116 | public PartialRelationTranslator mayNever() { | ||
117 | var never = createQuery(partialRelation.name() + "#never", (builder, parameters) -> {}); | ||
118 | may(never); | ||
119 | return this; | ||
120 | } | ||
121 | |||
105 | public PartialRelationTranslator must(RelationalQuery must) { | 122 | public PartialRelationTranslator must(RelationalQuery must) { |
106 | checkNotConfigured(); | 123 | checkNotConfigured(); |
107 | if (this.must != null) { | 124 | if (this.must != null) { |
@@ -163,20 +180,24 @@ public final class PartialRelationTranslator extends PartialSymbolTranslator<Tru | |||
163 | } | 180 | } |
164 | } | 181 | } |
165 | 182 | ||
166 | private RelationalQuery createQuery(Constraint constraint) { | 183 | private RelationalQuery createQuery(String name, BiConsumer<QueryBuilder, Variable[]> callback) { |
167 | int arity = partialRelation.arity(); | 184 | int arity = partialRelation.arity(); |
168 | var queryBuilder = Query.builder(partialRelation.name()); | 185 | var queryBuilder = Query.builder(name); |
169 | var parameters = new Variable[arity]; | 186 | var parameters = new Variable[arity]; |
170 | for (int i = 0; i < arity; i++) { | 187 | for (int i = 0; i < arity; i++) { |
171 | parameters[i] = queryBuilder.parameter("p" + 1); | 188 | parameters[i] = queryBuilder.parameter("p" + 1); |
172 | } | 189 | } |
173 | queryBuilder.clause(constraint.call(parameters)); | 190 | callback.accept(queryBuilder, parameters); |
174 | return queryBuilder.build(); | 191 | return queryBuilder.build(); |
175 | } | 192 | } |
176 | 193 | ||
194 | private RelationalQuery createQuery(String name, Constraint constraint) { | ||
195 | return createQuery(name, (builder, parameters) -> builder.clause(constraint.call(parameters))); | ||
196 | } | ||
197 | |||
177 | private void createFallbackQueryFromRewriter() { | 198 | private void createFallbackQueryFromRewriter() { |
178 | if (rewriter != null && query == null) { | 199 | if (rewriter != null && query == null) { |
179 | query = createQuery(partialRelation); | 200 | query = createQuery(partialRelation.name(), partialRelation); |
180 | } | 201 | } |
181 | } | 202 | } |
182 | 203 | ||
@@ -189,10 +210,12 @@ public final class PartialRelationTranslator extends PartialSymbolTranslator<Tru | |||
189 | var typedStorageSymbol = (Symbol<TruthValue>) storageSymbol; | 210 | var typedStorageSymbol = (Symbol<TruthValue>) storageSymbol; |
190 | var defaultValue = typedStorageSymbol.defaultValue(); | 211 | var defaultValue = typedStorageSymbol.defaultValue(); |
191 | if (may == null && !defaultValue.may()) { | 212 | if (may == null && !defaultValue.may()) { |
192 | may = createQuery(new MayView(typedStorageSymbol)); | 213 | may = createQuery(DnfLifter.decorateName(partialRelation.name(), Modality.MAY, Concreteness.PARTIAL), |
214 | new MayView(typedStorageSymbol)); | ||
193 | } | 215 | } |
194 | if (must == null && !defaultValue.must()) { | 216 | if (must == null && !defaultValue.must()) { |
195 | must = createQuery(new MustView(typedStorageSymbol)); | 217 | must = createQuery(DnfLifter.decorateName(partialRelation.name(), Modality.MUST, Concreteness.PARTIAL), |
218 | new MustView(typedStorageSymbol)); | ||
196 | } | 219 | } |
197 | } | 220 | } |
198 | 221 | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentHierarchyTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentHierarchyTranslator.java new file mode 100644 index 00000000..9d1b8cf4 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentHierarchyTranslator.java | |||
@@ -0,0 +1,221 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.containment; | ||
7 | |||
8 | import tools.refinery.store.model.ModelStoreBuilder; | ||
9 | import tools.refinery.store.model.ModelStoreConfiguration; | ||
10 | import tools.refinery.store.query.dnf.Query; | ||
11 | import tools.refinery.store.query.dnf.RelationalQuery; | ||
12 | import tools.refinery.store.query.literal.Connectivity; | ||
13 | import tools.refinery.store.query.literal.Literal; | ||
14 | import tools.refinery.store.query.literal.RepresentativeElectionLiteral; | ||
15 | import tools.refinery.store.query.term.Variable; | ||
16 | import tools.refinery.store.query.view.AnySymbolView; | ||
17 | import tools.refinery.store.reasoning.lifting.DnfLifter; | ||
18 | import tools.refinery.store.reasoning.literal.Concreteness; | ||
19 | import tools.refinery.store.reasoning.literal.CountLowerBoundLiteral; | ||
20 | import tools.refinery.store.reasoning.literal.Modality; | ||
21 | import tools.refinery.store.reasoning.refinement.RefinementBasedInitializer; | ||
22 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
23 | import tools.refinery.store.reasoning.translator.PartialRelationTranslator; | ||
24 | import tools.refinery.store.reasoning.translator.RoundingMode; | ||
25 | import tools.refinery.store.reasoning.translator.multiplicity.ConstrainedMultiplicity; | ||
26 | import tools.refinery.store.reasoning.translator.multiplicity.InvalidMultiplicityErrorTranslator; | ||
27 | import tools.refinery.store.representation.Symbol; | ||
28 | import tools.refinery.store.representation.cardinality.CardinalityIntervals; | ||
29 | import tools.refinery.store.representation.cardinality.FiniteUpperCardinality; | ||
30 | |||
31 | import java.util.ArrayList; | ||
32 | import java.util.List; | ||
33 | import java.util.Map; | ||
34 | |||
35 | import static tools.refinery.store.query.literal.Literals.check; | ||
36 | import static tools.refinery.store.query.literal.Literals.not; | ||
37 | import static tools.refinery.store.query.term.int_.IntTerms.constant; | ||
38 | import static tools.refinery.store.query.term.int_.IntTerms.less; | ||
39 | import static tools.refinery.store.reasoning.ReasoningAdapter.EXISTS_SYMBOL; | ||
40 | import static tools.refinery.store.reasoning.literal.PartialLiterals.may; | ||
41 | import static tools.refinery.store.reasoning.literal.PartialLiterals.must; | ||
42 | |||
43 | public class ContainmentHierarchyTranslator implements ModelStoreConfiguration { | ||
44 | public static final PartialRelation CONTAINED_SYMBOL = new PartialRelation("contained", 1); | ||
45 | public static final PartialRelation INVALID_NUMBER_OF_CONTAINERS = new PartialRelation("invalidNumberOfContainers", | ||
46 | 1); | ||
47 | public static final PartialRelation CONTAINS_SYMBOL = new PartialRelation("contains", 2); | ||
48 | |||
49 | private final Symbol<InferredContainment> containsStorage = Symbol.of("CONTAINS", 2, InferredContainment.class, | ||
50 | InferredContainment.UNKNOWN); | ||
51 | private final AnySymbolView forbiddenContainsView = new ForbiddenContainsView(containsStorage); | ||
52 | private final RelationalQuery containsMayNewTargetHelper; | ||
53 | private final RelationalQuery containsMayExistingHelper; | ||
54 | private final RelationalQuery weakComponents; | ||
55 | private final RelationalQuery strongComponents; | ||
56 | private final Map<PartialRelation, ContainmentInfo> containmentInfoMap; | ||
57 | |||
58 | public ContainmentHierarchyTranslator(Map<PartialRelation, ContainmentInfo> containmentInfoMap) { | ||
59 | this.containmentInfoMap = containmentInfoMap; | ||
60 | |||
61 | var name = CONTAINS_SYMBOL.name(); | ||
62 | |||
63 | containsMayNewTargetHelper = Query.of(name + "#mayNewTargetHelper", (builder, child) -> builder | ||
64 | .clause(Integer.class, existingContainers -> List.of( | ||
65 | may(CONTAINED_SYMBOL.call(child)), | ||
66 | new CountLowerBoundLiteral(existingContainers, CONTAINS_SYMBOL, List.of(Variable.of(), child)), | ||
67 | check(less(existingContainers, constant(1))) | ||
68 | ))); | ||
69 | |||
70 | containsMayExistingHelper = Query.of(name + "#mayExistingHelper", (builder, parent, child) -> builder | ||
71 | .clause(Integer.class, existingContainers -> List.of( | ||
72 | must(CONTAINS_SYMBOL.call(parent, child)), | ||
73 | not(forbiddenContainsView.call(parent, child)) | ||
74 | // Violation of monotonicity: | ||
75 | // Containment edges violating upper multiplicity will not be marked as {@code ERROR}, but the | ||
76 | // {@code invalidNumberOfContainers} error pattern will already mark the node as invalid. | ||
77 | ))); | ||
78 | |||
79 | var mustExistBothContains = Query.of(name + "#mustExistBoth", (builder, parent, child) -> builder.clause( | ||
80 | must(CONTAINS_SYMBOL.call(parent, child)), | ||
81 | must(EXISTS_SYMBOL.call(parent)), | ||
82 | must(EXISTS_SYMBOL.call(child)) | ||
83 | )); | ||
84 | |||
85 | weakComponents = Query.of(name + "#weakComponents", (builder, node, representative) -> builder.clause( | ||
86 | new RepresentativeElectionLiteral(Connectivity.WEAK, mustExistBothContains.getDnf(), node, | ||
87 | representative) | ||
88 | )); | ||
89 | |||
90 | strongComponents = Query.of(name + "#strongComponents", (builder, node, representative) -> builder.clause( | ||
91 | new RepresentativeElectionLiteral(Connectivity.STRONG, mustExistBothContains.getDnf(), node, | ||
92 | representative) | ||
93 | )); | ||
94 | } | ||
95 | |||
96 | @Override | ||
97 | public void apply(ModelStoreBuilder storeBuilder) { | ||
98 | storeBuilder.symbol(containsStorage); | ||
99 | translateContains(storeBuilder); | ||
100 | translateInvalidNumberOfContainers(storeBuilder); | ||
101 | for (var entry : containmentInfoMap.entrySet()) { | ||
102 | var linkType = entry.getKey(); | ||
103 | var info = entry.getValue(); | ||
104 | translateContainmentLinkType(storeBuilder, linkType, info); | ||
105 | translateInvalidMultiplicity(storeBuilder, linkType, info); | ||
106 | } | ||
107 | } | ||
108 | |||
109 | private void translateContainmentLinkType(ModelStoreBuilder storeBuilder, PartialRelation linkType, | ||
110 | ContainmentInfo info) { | ||
111 | var name = linkType.name(); | ||
112 | var sourceType = info.sourceType(); | ||
113 | var targetType = info.targetType(); | ||
114 | var upperCardinality = info.multiplicity().multiplicity().upperBound(); | ||
115 | |||
116 | var mayNewSourceHelper = Query.of(name + "#mayNewSourceHelper", (builder, parent) -> { | ||
117 | var literals = new ArrayList<Literal>(); | ||
118 | literals.add(may(sourceType.call(parent))); | ||
119 | if (upperCardinality instanceof FiniteUpperCardinality finiteUpperCardinality) { | ||
120 | var existingCount = Variable.of("existingCount", Integer.class); | ||
121 | literals.add(new CountLowerBoundLiteral(existingCount, linkType, List.of(parent, Variable.of()))); | ||
122 | literals.add(check(less(existingCount, constant(finiteUpperCardinality.finiteUpperBound())))); | ||
123 | } | ||
124 | builder.clause(literals); | ||
125 | }); | ||
126 | |||
127 | var mayNewTargetHelper = Query.of(name + "#mayNewTargetHelper", (builder, child) -> builder.clause( | ||
128 | containsMayNewTargetHelper.call(child), | ||
129 | may(targetType.call(child)) | ||
130 | )); | ||
131 | |||
132 | var forbiddenLinkView = new ForbiddenContainmentLinkView(containsStorage, linkType); | ||
133 | |||
134 | var mayNewHelper = Query.of(name + "#mayNewHelper", (builder, parent, child) -> builder.clause( | ||
135 | mayNewSourceHelper.call(parent), | ||
136 | mayNewTargetHelper.call(child), | ||
137 | not(must(CONTAINS_SYMBOL.call(parent, child))), | ||
138 | not(forbiddenLinkView.call(parent, child)) | ||
139 | )); | ||
140 | |||
141 | var mayExistingHelper = Query.of(name + "#mayExistingHelper", (builder, parent, child) -> builder.clause( | ||
142 | must(linkType.call(parent, child)), | ||
143 | containsMayExistingHelper.call(parent, child), | ||
144 | may(sourceType.call(parent)), | ||
145 | may(targetType.call(child)), | ||
146 | not(forbiddenLinkView.call(parent, child)) | ||
147 | // Violation of monotonicity: | ||
148 | // Containment edges violating upper multiplicity will not be marked as {@code ERROR}, but the | ||
149 | // {@code invalidNumberOfContainers} error pattern will already mark the node as invalid. | ||
150 | )); | ||
151 | |||
152 | var may = Query.of(name + "#may", (builder, parent, child) -> builder | ||
153 | .clause( | ||
154 | mayNewHelper.call(parent, child), | ||
155 | not(weakComponents.call(parent, Variable.of())) | ||
156 | ) | ||
157 | .clause(representative -> List.of( | ||
158 | mayNewHelper.call(parent, child), | ||
159 | weakComponents.call(child, representative), | ||
160 | // Violation of para-consistency: | ||
161 | // If there is a surely existing node with at least two containers, its (transitive) containers | ||
162 | // will end up in the same weakly connected component, and we will spuriously mark the | ||
163 | // containment edge between the (transitive) containers as {@code FALSE}. However, such | ||
164 | // models can never be finished. | ||
165 | // | ||
166 | // Violation of monotonicity: | ||
167 | // if the a {@code TRUE} value is added to the representation in the previous situation, | ||
168 | // we'll check strongly connected components instead of weakly connected ones. Therefore, the | ||
169 | // view for the partial symbol will change from {@code FALSE} to {@code TRUE}. This doesn't | ||
170 | // affect the overall inconsistency of the partial model (due to the surely existing node | ||
171 | // with multiple containers). | ||
172 | not(weakComponents.call(child, representative)) | ||
173 | )) | ||
174 | .clause( | ||
175 | mayExistingHelper.call(parent, child), | ||
176 | not(strongComponents.call(parent, Variable.of())) | ||
177 | ) | ||
178 | .clause(representative -> List.of( | ||
179 | mayExistingHelper.call(parent, child), | ||
180 | strongComponents.call(parent, representative), | ||
181 | not(strongComponents.call(parent, representative)) | ||
182 | ))); | ||
183 | |||
184 | storeBuilder.with(PartialRelationTranslator.of(linkType) | ||
185 | .may(may) | ||
186 | .must(Query.of(name + "#must", (builder, parent, child) -> builder.clause( | ||
187 | new MustContainmentLinkView(containsStorage, linkType).call(parent, child) | ||
188 | ))) | ||
189 | .roundingMode(RoundingMode.PREFER_FALSE) | ||
190 | .refiner(ContainmentLinkRefiner.of(linkType, containsStorage, info.sourceType(), info.targetType())) | ||
191 | .initializer(new RefinementBasedInitializer<>(linkType))); | ||
192 | } | ||
193 | |||
194 | private void translateInvalidMultiplicity(ModelStoreBuilder storeBuilder, PartialRelation linkType, | ||
195 | ContainmentInfo info) { | ||
196 | storeBuilder.with(new InvalidMultiplicityErrorTranslator(info.sourceType(), linkType, false, | ||
197 | info.multiplicity())); | ||
198 | } | ||
199 | |||
200 | private void translateContains(ModelStoreBuilder storeBuilder) { | ||
201 | var name = CONTAINS_SYMBOL.name(); | ||
202 | var mustName = DnfLifter.decorateName(name, Modality.MUST, Concreteness.PARTIAL); | ||
203 | |||
204 | storeBuilder.with(PartialRelationTranslator.of(CONTAINS_SYMBOL) | ||
205 | .query(Query.of(name, (builder, parent, child) -> { | ||
206 | for (var linkType : containmentInfoMap.keySet()) { | ||
207 | builder.clause(linkType.call(parent, child)); | ||
208 | } | ||
209 | })) | ||
210 | .must(Query.of(mustName, (builder, parent, child) -> builder.clause( | ||
211 | new MustContainsView(containsStorage).call(parent, child) | ||
212 | ))) | ||
213 | .refiner(ContainsRefiner.of(containsStorage)) | ||
214 | .initializer(new RefinementBasedInitializer<>(CONTAINS_SYMBOL))); | ||
215 | } | ||
216 | |||
217 | private void translateInvalidNumberOfContainers(ModelStoreBuilder storeBuilder) { | ||
218 | storeBuilder.with(new InvalidMultiplicityErrorTranslator(CONTAINED_SYMBOL, CONTAINS_SYMBOL, true, | ||
219 | ConstrainedMultiplicity.of(CardinalityIntervals.ONE, INVALID_NUMBER_OF_CONTAINERS))); | ||
220 | } | ||
221 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentInfo.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentInfo.java new file mode 100644 index 00000000..1087e54d --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentInfo.java | |||
@@ -0,0 +1,23 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.containment; | ||
7 | |||
8 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
9 | import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity; | ||
10 | |||
11 | public record ContainmentInfo(PartialRelation sourceType, Multiplicity multiplicity, | ||
12 | PartialRelation targetType) { | ||
13 | public ContainmentInfo { | ||
14 | if (sourceType.arity() != 1) { | ||
15 | throw new IllegalArgumentException("Expected source type %s to be of arity 1, got %d instead" | ||
16 | .formatted(sourceType, sourceType.arity())); | ||
17 | } | ||
18 | if (targetType.arity() != 1) { | ||
19 | throw new IllegalArgumentException("Expected target type %s to be of arity 1, got %d instead" | ||
20 | .formatted(targetType, targetType.arity())); | ||
21 | } | ||
22 | } | ||
23 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentLinkRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentLinkRefiner.java new file mode 100644 index 00000000..497ed98f --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentLinkRefiner.java | |||
@@ -0,0 +1,128 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.containment; | ||
7 | |||
8 | import tools.refinery.store.model.Interpretation; | ||
9 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
10 | import tools.refinery.store.reasoning.refinement.AbstractPartialInterpretationRefiner; | ||
11 | import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner; | ||
12 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
13 | import tools.refinery.store.reasoning.representation.PartialSymbol; | ||
14 | import tools.refinery.store.representation.Symbol; | ||
15 | import tools.refinery.store.representation.TruthValue; | ||
16 | import tools.refinery.store.tuple.Tuple; | ||
17 | |||
18 | import java.util.ArrayList; | ||
19 | import java.util.Set; | ||
20 | |||
21 | class ContainmentLinkRefiner extends AbstractPartialInterpretationRefiner<TruthValue, Boolean> { | ||
22 | private final Factory factory; | ||
23 | private final Interpretation<InferredContainment> interpretation; | ||
24 | private final PartialInterpretationRefiner<TruthValue, Boolean> sourceRefiner; | ||
25 | private final PartialInterpretationRefiner<TruthValue, Boolean> targetRefiner; | ||
26 | |||
27 | public ContainmentLinkRefiner(ReasoningAdapter adapter, PartialSymbol<TruthValue, Boolean> partialSymbol, | ||
28 | Factory factory) { | ||
29 | super(adapter, partialSymbol); | ||
30 | this.factory = factory; | ||
31 | interpretation = adapter.getModel().getInterpretation(factory.symbol); | ||
32 | sourceRefiner = adapter.getRefiner(factory.sourceType); | ||
33 | targetRefiner = adapter.getRefiner(factory.targetType); | ||
34 | } | ||
35 | |||
36 | @Override | ||
37 | public boolean merge(Tuple key, TruthValue value) { | ||
38 | var oldValue = interpretation.get(key); | ||
39 | var newValue = mergeLink(oldValue, value); | ||
40 | if (oldValue != newValue) { | ||
41 | interpretation.put(key, newValue); | ||
42 | } | ||
43 | if (value.must()) { | ||
44 | return sourceRefiner.merge(Tuple.of(key.get(0)), TruthValue.TRUE) && | ||
45 | targetRefiner.merge(Tuple.of(key.get(1)), TruthValue.TRUE); | ||
46 | } | ||
47 | return true; | ||
48 | } | ||
49 | |||
50 | public InferredContainment mergeLink(InferredContainment oldValue, TruthValue toMerge) { | ||
51 | return switch (toMerge) { | ||
52 | case UNKNOWN -> oldValue; | ||
53 | case TRUE -> mustLink(oldValue); | ||
54 | case FALSE -> forbidLink(oldValue); | ||
55 | case ERROR -> errorLink(oldValue); | ||
56 | }; | ||
57 | } | ||
58 | |||
59 | public InferredContainment mustLink(InferredContainment oldValue) { | ||
60 | var mustLinks = oldValue.mustLinks(); | ||
61 | if (oldValue.contains().may() && mustLinks.isEmpty() && oldValue.forbiddenLinks().isEmpty()) { | ||
62 | return factory.trueLink; | ||
63 | } | ||
64 | if (mustLinks.contains(factory.linkType)) { | ||
65 | return oldValue; | ||
66 | } | ||
67 | return new InferredContainment(oldValue.contains().merge(TruthValue.TRUE), | ||
68 | addToSet(mustLinks, factory.linkType), oldValue.forbiddenLinks()); | ||
69 | } | ||
70 | |||
71 | public InferredContainment forbidLink(InferredContainment oldValue) { | ||
72 | var forbiddenLinks = oldValue.forbiddenLinks(); | ||
73 | if (oldValue.contains() == TruthValue.UNKNOWN && oldValue.mustLinks().isEmpty() && forbiddenLinks.isEmpty()) { | ||
74 | return factory.falseLinkUnknownContains; | ||
75 | } | ||
76 | if (forbiddenLinks.contains(factory.linkType)) { | ||
77 | return oldValue; | ||
78 | } | ||
79 | return new InferredContainment(oldValue.contains(), oldValue.mustLinks(), | ||
80 | addToSet(forbiddenLinks, factory.linkType)); | ||
81 | } | ||
82 | |||
83 | public InferredContainment errorLink(InferredContainment oldValue) { | ||
84 | return new InferredContainment(TruthValue.ERROR, addToSet(oldValue.mustLinks(), factory.linkType), | ||
85 | addToSet(oldValue.forbiddenLinks(), factory.linkType)); | ||
86 | } | ||
87 | |||
88 | private static Set<PartialRelation> addToSet(Set<PartialRelation> oldSet, PartialRelation linkType) { | ||
89 | if (oldSet.isEmpty()) { | ||
90 | return Set.of(linkType); | ||
91 | } | ||
92 | var newElements = new ArrayList<PartialRelation>(oldSet.size() + 1); | ||
93 | newElements.addAll(oldSet); | ||
94 | newElements.add(linkType); | ||
95 | return Set.copyOf(newElements); | ||
96 | } | ||
97 | |||
98 | public static PartialInterpretationRefiner.Factory<TruthValue, Boolean> of( | ||
99 | PartialRelation linkType, Symbol<InferredContainment> symbol, PartialRelation sourceType, | ||
100 | PartialRelation targetType) { | ||
101 | return new Factory(linkType, symbol, sourceType, targetType); | ||
102 | } | ||
103 | |||
104 | private static class Factory implements PartialInterpretationRefiner.Factory<TruthValue, Boolean> { | ||
105 | public final PartialRelation linkType; | ||
106 | public final Symbol<InferredContainment> symbol; | ||
107 | public final PartialRelation targetType; | ||
108 | public final PartialRelation sourceType; | ||
109 | public final InferredContainment trueLink; | ||
110 | public final InferredContainment falseLinkUnknownContains; | ||
111 | |||
112 | public Factory(PartialRelation linkType, Symbol<InferredContainment> symbol, PartialRelation sourceType, | ||
113 | PartialRelation targetType) { | ||
114 | this.linkType = linkType; | ||
115 | this.symbol = symbol; | ||
116 | this.sourceType = sourceType; | ||
117 | this.targetType = targetType; | ||
118 | trueLink = new InferredContainment(TruthValue.TRUE, Set.of(linkType), Set.of()); | ||
119 | falseLinkUnknownContains = new InferredContainment(TruthValue.FALSE, Set.of(), Set.of(linkType)); | ||
120 | } | ||
121 | |||
122 | @Override | ||
123 | public PartialInterpretationRefiner<TruthValue, Boolean> create( | ||
124 | ReasoningAdapter adapter, PartialSymbol<TruthValue, Boolean> partialSymbol) { | ||
125 | return new ContainmentLinkRefiner(adapter, partialSymbol, this); | ||
126 | } | ||
127 | } | ||
128 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainsRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainsRefiner.java new file mode 100644 index 00000000..b57ca095 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainsRefiner.java | |||
@@ -0,0 +1,70 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.containment; | ||
7 | |||
8 | import tools.refinery.store.model.Interpretation; | ||
9 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
10 | import tools.refinery.store.reasoning.refinement.AbstractPartialInterpretationRefiner; | ||
11 | import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner; | ||
12 | import tools.refinery.store.reasoning.representation.PartialSymbol; | ||
13 | import tools.refinery.store.representation.Symbol; | ||
14 | import tools.refinery.store.representation.TruthValue; | ||
15 | import tools.refinery.store.tuple.Tuple; | ||
16 | |||
17 | import java.util.Set; | ||
18 | |||
19 | class ContainsRefiner extends AbstractPartialInterpretationRefiner<TruthValue, Boolean> { | ||
20 | private static final InferredContainment CONTAINS_TRUE = new InferredContainment(TruthValue.TRUE, Set.of(), | ||
21 | Set.of()); | ||
22 | private static final InferredContainment CONTAINS_FALSE = new InferredContainment(TruthValue.FALSE, Set.of(), | ||
23 | Set.of()); | ||
24 | private static final InferredContainment CONTAINS_ERROR = new InferredContainment(TruthValue.ERROR, Set.of(), | ||
25 | Set.of()); | ||
26 | |||
27 | private final PartialInterpretationRefiner<TruthValue, Boolean> containedRefiner; | ||
28 | private final Interpretation<InferredContainment> interpretation; | ||
29 | |||
30 | public ContainsRefiner(ReasoningAdapter adapter, PartialSymbol<TruthValue, Boolean> partialSymbol, | ||
31 | Symbol<InferredContainment> symbol) { | ||
32 | super(adapter, partialSymbol); | ||
33 | containedRefiner = adapter.getRefiner(ContainmentHierarchyTranslator.CONTAINED_SYMBOL); | ||
34 | interpretation = adapter.getModel().getInterpretation(symbol); | ||
35 | } | ||
36 | |||
37 | @Override | ||
38 | public boolean merge(Tuple key, TruthValue value) { | ||
39 | var oldValue = interpretation.get(key); | ||
40 | var newValue = mergeContains(oldValue, value); | ||
41 | if (oldValue != newValue) { | ||
42 | interpretation.put(key, newValue); | ||
43 | } | ||
44 | if (value.must()) { | ||
45 | return containedRefiner.merge(Tuple.of(key.get(1)), TruthValue.TRUE); | ||
46 | } | ||
47 | return true; | ||
48 | } | ||
49 | |||
50 | public InferredContainment mergeContains(InferredContainment oldValue, TruthValue toMerge) { | ||
51 | var oldContains = oldValue.contains(); | ||
52 | var newContains = oldContains.merge(toMerge); | ||
53 | if (newContains == oldContains) { | ||
54 | return oldValue; | ||
55 | } | ||
56 | if (oldValue.mustLinks().isEmpty() && oldValue.forbiddenLinks().isEmpty()) { | ||
57 | return switch (toMerge) { | ||
58 | case UNKNOWN -> oldValue; | ||
59 | case TRUE -> oldContains.may() ? CONTAINS_TRUE : CONTAINS_ERROR; | ||
60 | case FALSE -> oldContains.must() ? CONTAINS_ERROR : CONTAINS_FALSE; | ||
61 | case ERROR -> CONTAINS_ERROR; | ||
62 | }; | ||
63 | } | ||
64 | return new InferredContainment(newContains, oldValue.mustLinks(), oldValue.forbiddenLinks()); | ||
65 | } | ||
66 | |||
67 | public static Factory<TruthValue, Boolean> of(Symbol<InferredContainment> symbol) { | ||
68 | return (adapter, partialSymbol) -> new ContainsRefiner(adapter, partialSymbol, symbol); | ||
69 | } | ||
70 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ForbiddenContainmentLinkView.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ForbiddenContainmentLinkView.java new file mode 100644 index 00000000..cf0e2971 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ForbiddenContainmentLinkView.java | |||
@@ -0,0 +1,21 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.containment; | ||
7 | |||
8 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
9 | import tools.refinery.store.representation.Symbol; | ||
10 | import tools.refinery.store.tuple.Tuple; | ||
11 | |||
12 | class ForbiddenContainmentLinkView extends InferredContainmentLinkView { | ||
13 | public ForbiddenContainmentLinkView(Symbol<InferredContainment> symbol, PartialRelation link) { | ||
14 | super(symbol, "must", link); | ||
15 | } | ||
16 | |||
17 | @Override | ||
18 | protected boolean doFilter(Tuple key, InferredContainment value) { | ||
19 | return value.forbiddenLinks().contains(link); | ||
20 | } | ||
21 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ForbiddenContainsView.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ForbiddenContainsView.java new file mode 100644 index 00000000..efe674f1 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ForbiddenContainsView.java | |||
@@ -0,0 +1,21 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.containment; | ||
7 | |||
8 | import tools.refinery.store.query.view.TuplePreservingView; | ||
9 | import tools.refinery.store.representation.Symbol; | ||
10 | import tools.refinery.store.tuple.Tuple; | ||
11 | |||
12 | class ForbiddenContainsView extends TuplePreservingView<InferredContainment> { | ||
13 | public ForbiddenContainsView(Symbol<InferredContainment> symbol) { | ||
14 | super(symbol, "contains#forbidden"); | ||
15 | } | ||
16 | |||
17 | @Override | ||
18 | protected boolean doFilter(Tuple key, InferredContainment value) { | ||
19 | return !value.contains().may(); | ||
20 | } | ||
21 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/InferredContainment.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/InferredContainment.java new file mode 100644 index 00000000..90802864 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/InferredContainment.java | |||
@@ -0,0 +1,37 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.containment; | ||
7 | |||
8 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
9 | import tools.refinery.store.representation.TruthValue; | ||
10 | |||
11 | import java.util.Set; | ||
12 | |||
13 | record InferredContainment(TruthValue contains, Set<PartialRelation> mustLinks, | ||
14 | Set<PartialRelation> forbiddenLinks) { | ||
15 | public static final InferredContainment UNKNOWN = new InferredContainment( | ||
16 | TruthValue.UNKNOWN, Set.of(), Set.of()); | ||
17 | |||
18 | public InferredContainment(TruthValue contains, Set<PartialRelation> mustLinks, | ||
19 | Set<PartialRelation> forbiddenLinks) { | ||
20 | this.contains = adjustContains(contains, mustLinks, forbiddenLinks); | ||
21 | this.mustLinks = mustLinks; | ||
22 | this.forbiddenLinks = forbiddenLinks; | ||
23 | } | ||
24 | |||
25 | private static TruthValue adjustContains(TruthValue contains, Set<PartialRelation> mustLinks, | ||
26 | Set<PartialRelation> forbiddenLinks) { | ||
27 | var result = contains; | ||
28 | if (!mustLinks.isEmpty()) { | ||
29 | result = result.merge(TruthValue.TRUE); | ||
30 | } | ||
31 | boolean hasErrorLink = mustLinks.stream().anyMatch(forbiddenLinks::contains); | ||
32 | if (mustLinks.size() >= 2 || hasErrorLink) { | ||
33 | result = result.merge(TruthValue.ERROR); | ||
34 | } | ||
35 | return result; | ||
36 | } | ||
37 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/InferredContainmentLinkView.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/InferredContainmentLinkView.java new file mode 100644 index 00000000..d187ad91 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/InferredContainmentLinkView.java | |||
@@ -0,0 +1,35 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.containment; | ||
7 | |||
8 | import tools.refinery.store.query.view.TuplePreservingView; | ||
9 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
10 | import tools.refinery.store.representation.Symbol; | ||
11 | |||
12 | import java.util.Objects; | ||
13 | |||
14 | abstract class InferredContainmentLinkView extends TuplePreservingView<InferredContainment> { | ||
15 | protected final PartialRelation link; | ||
16 | |||
17 | protected InferredContainmentLinkView(Symbol<InferredContainment> symbol, String name, PartialRelation link) { | ||
18 | super(symbol, link.name() + "#" + name); | ||
19 | this.link = link; | ||
20 | } | ||
21 | |||
22 | @Override | ||
23 | public boolean equals(Object o) { | ||
24 | if (this == o) return true; | ||
25 | if (o == null || getClass() != o.getClass()) return false; | ||
26 | if (!super.equals(o)) return false; | ||
27 | InferredContainmentLinkView that = (InferredContainmentLinkView) o; | ||
28 | return Objects.equals(link, that.link); | ||
29 | } | ||
30 | |||
31 | @Override | ||
32 | public int hashCode() { | ||
33 | return Objects.hash(super.hashCode(), link); | ||
34 | } | ||
35 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/MustContainmentLinkView.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/MustContainmentLinkView.java new file mode 100644 index 00000000..474942d6 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/MustContainmentLinkView.java | |||
@@ -0,0 +1,21 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.containment; | ||
7 | |||
8 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
9 | import tools.refinery.store.representation.Symbol; | ||
10 | import tools.refinery.store.tuple.Tuple; | ||
11 | |||
12 | class MustContainmentLinkView extends InferredContainmentLinkView { | ||
13 | public MustContainmentLinkView(Symbol<InferredContainment> symbol, PartialRelation link) { | ||
14 | super(symbol, "must", link); | ||
15 | } | ||
16 | |||
17 | @Override | ||
18 | protected boolean doFilter(Tuple key, InferredContainment value) { | ||
19 | return value.mustLinks().contains(link); | ||
20 | } | ||
21 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/MustContainsView.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/MustContainsView.java new file mode 100644 index 00000000..6bc62a59 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/MustContainsView.java | |||
@@ -0,0 +1,21 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.containment; | ||
7 | |||
8 | import tools.refinery.store.query.view.TuplePreservingView; | ||
9 | import tools.refinery.store.representation.Symbol; | ||
10 | import tools.refinery.store.tuple.Tuple; | ||
11 | |||
12 | class MustContainsView extends TuplePreservingView<InferredContainment> { | ||
13 | public MustContainsView(Symbol<InferredContainment> symbol) { | ||
14 | super(symbol, "contains#must"); | ||
15 | } | ||
16 | |||
17 | @Override | ||
18 | protected boolean doFilter(Tuple key, InferredContainment value) { | ||
19 | return value.contains().must(); | ||
20 | } | ||
21 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/CrossReferenceUtils.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/CrossReferenceUtils.java new file mode 100644 index 00000000..c4a2f2b3 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/CrossReferenceUtils.java | |||
@@ -0,0 +1,57 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.crossreference; | ||
7 | |||
8 | import tools.refinery.store.query.dnf.Query; | ||
9 | import tools.refinery.store.query.dnf.RelationalQuery; | ||
10 | import tools.refinery.store.query.literal.Literal; | ||
11 | import tools.refinery.store.query.term.NodeVariable; | ||
12 | import tools.refinery.store.query.term.Variable; | ||
13 | import tools.refinery.store.reasoning.literal.CountLowerBoundLiteral; | ||
14 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
15 | import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity; | ||
16 | import tools.refinery.store.representation.cardinality.FiniteUpperCardinality; | ||
17 | |||
18 | import java.util.ArrayList; | ||
19 | import java.util.List; | ||
20 | |||
21 | import static tools.refinery.store.query.literal.Literals.check; | ||
22 | import static tools.refinery.store.query.term.int_.IntTerms.constant; | ||
23 | import static tools.refinery.store.query.term.int_.IntTerms.less; | ||
24 | import static tools.refinery.store.reasoning.literal.PartialLiterals.may; | ||
25 | |||
26 | class CrossReferenceUtils { | ||
27 | private CrossReferenceUtils() { | ||
28 | throw new IllegalStateException("This is a static utility class and should not be instantiated directly"); | ||
29 | } | ||
30 | |||
31 | public static RelationalQuery createMayHelper(PartialRelation linkType, PartialRelation type, | ||
32 | Multiplicity multiplicity, boolean inverse) { | ||
33 | String name; | ||
34 | NodeVariable variable; | ||
35 | List<Variable> arguments; | ||
36 | if (inverse) { | ||
37 | name = "Target"; | ||
38 | variable = Variable.of("target"); | ||
39 | arguments = List.of(Variable.of("source"), variable); | ||
40 | } else { | ||
41 | name = "Source"; | ||
42 | variable = Variable.of("source"); | ||
43 | arguments = List.of(variable, Variable.of("target")); | ||
44 | } | ||
45 | var builder = Query.builder(linkType.name() + "#mayNew" + name); | ||
46 | builder.parameter(variable); | ||
47 | var literals = new ArrayList<Literal>(); | ||
48 | literals.add(may(type.call(variable))); | ||
49 | if (multiplicity.multiplicity().upperBound() instanceof FiniteUpperCardinality finiteUpperCardinality) { | ||
50 | var existingLinks = Variable.of("existingLinks", Integer.class); | ||
51 | literals.add(new CountLowerBoundLiteral(existingLinks, linkType, arguments)); | ||
52 | literals.add(check(less(existingLinks, constant(finiteUpperCardinality.finiteUpperBound())))); | ||
53 | } | ||
54 | builder.clause(literals); | ||
55 | return builder.build(); | ||
56 | } | ||
57 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceInfo.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceInfo.java new file mode 100644 index 00000000..d8c6a5ea --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceInfo.java | |||
@@ -0,0 +1,16 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.crossreference; | ||
7 | |||
8 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
9 | import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity; | ||
10 | |||
11 | public record DirectedCrossReferenceInfo(PartialRelation sourceType, Multiplicity sourceMultiplicity, | ||
12 | PartialRelation targetType, Multiplicity targetMultiplicity) { | ||
13 | public boolean isConstrained() { | ||
14 | return sourceMultiplicity.isConstrained() || targetMultiplicity.isConstrained(); | ||
15 | } | ||
16 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceRefiner.java new file mode 100644 index 00000000..0700f9f7 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceRefiner.java | |||
@@ -0,0 +1,46 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.crossreference; | ||
7 | |||
8 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
9 | import tools.refinery.store.reasoning.refinement.ConcreteSymbolRefiner; | ||
10 | import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner; | ||
11 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
12 | import tools.refinery.store.reasoning.representation.PartialSymbol; | ||
13 | import tools.refinery.store.representation.Symbol; | ||
14 | import tools.refinery.store.representation.TruthValue; | ||
15 | import tools.refinery.store.tuple.Tuple; | ||
16 | |||
17 | class DirectedCrossReferenceRefiner extends ConcreteSymbolRefiner<TruthValue, Boolean> { | ||
18 | private final PartialInterpretationRefiner<TruthValue, Boolean> sourceRefiner; | ||
19 | private final PartialInterpretationRefiner<TruthValue, Boolean> targetRefiner; | ||
20 | |||
21 | public DirectedCrossReferenceRefiner(ReasoningAdapter adapter, PartialSymbol<TruthValue, Boolean> partialSymbol, | ||
22 | Symbol<TruthValue> concreteSymbol, PartialRelation sourceType, | ||
23 | PartialRelation targetType) { | ||
24 | super(adapter, partialSymbol, concreteSymbol); | ||
25 | sourceRefiner = adapter.getRefiner(sourceType); | ||
26 | targetRefiner = adapter.getRefiner(targetType); | ||
27 | } | ||
28 | |||
29 | @Override | ||
30 | public boolean merge(Tuple key, TruthValue value) { | ||
31 | if (!super.merge(key, value)) { | ||
32 | return false; | ||
33 | } | ||
34 | if (value.must()) { | ||
35 | return sourceRefiner.merge(Tuple.of(key.get(0)), TruthValue.TRUE) && | ||
36 | targetRefiner.merge(Tuple.of(key.get(1)), TruthValue.TRUE); | ||
37 | } | ||
38 | return true; | ||
39 | } | ||
40 | |||
41 | public static Factory<TruthValue, Boolean> of(Symbol<TruthValue> concreteSymbol, PartialRelation sourceType, | ||
42 | PartialRelation targetType) { | ||
43 | return (adapter, partialSymbol) -> new DirectedCrossReferenceRefiner(adapter, partialSymbol, concreteSymbol, | ||
44 | sourceType, targetType); | ||
45 | } | ||
46 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceTranslator.java new file mode 100644 index 00000000..f978aad4 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceTranslator.java | |||
@@ -0,0 +1,82 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.crossreference; | ||
7 | |||
8 | import tools.refinery.store.model.ModelStoreBuilder; | ||
9 | import tools.refinery.store.model.ModelStoreConfiguration; | ||
10 | import tools.refinery.store.query.dnf.Query; | ||
11 | import tools.refinery.store.query.dnf.RelationalQuery; | ||
12 | import tools.refinery.store.query.view.ForbiddenView; | ||
13 | import tools.refinery.store.reasoning.lifting.DnfLifter; | ||
14 | import tools.refinery.store.reasoning.literal.Concreteness; | ||
15 | import tools.refinery.store.reasoning.literal.Modality; | ||
16 | import tools.refinery.store.reasoning.refinement.RefinementBasedInitializer; | ||
17 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
18 | import tools.refinery.store.reasoning.translator.PartialRelationTranslator; | ||
19 | import tools.refinery.store.reasoning.translator.multiplicity.InvalidMultiplicityErrorTranslator; | ||
20 | import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity; | ||
21 | import tools.refinery.store.representation.Symbol; | ||
22 | import tools.refinery.store.representation.TruthValue; | ||
23 | |||
24 | import static tools.refinery.store.query.literal.Literals.not; | ||
25 | import static tools.refinery.store.reasoning.literal.PartialLiterals.may; | ||
26 | import static tools.refinery.store.reasoning.literal.PartialLiterals.must; | ||
27 | |||
28 | public class DirectedCrossReferenceTranslator implements ModelStoreConfiguration { | ||
29 | private final PartialRelation linkType; | ||
30 | private final DirectedCrossReferenceInfo info; | ||
31 | private final Symbol<TruthValue> symbol; | ||
32 | |||
33 | public DirectedCrossReferenceTranslator(PartialRelation linkType, DirectedCrossReferenceInfo info) { | ||
34 | this.linkType = linkType; | ||
35 | this.info = info; | ||
36 | symbol = Symbol.of(linkType.name(), 2, TruthValue.class, TruthValue.UNKNOWN); | ||
37 | } | ||
38 | |||
39 | @Override | ||
40 | public void apply(ModelStoreBuilder storeBuilder) { | ||
41 | var name = linkType.name(); | ||
42 | var sourceType = info.sourceType(); | ||
43 | var targetType = info.targetType(); | ||
44 | var mayNewSource = createMayHelper(sourceType, info.sourceMultiplicity(), false); | ||
45 | var mayNewTarget = createMayHelper(targetType, info.targetMultiplicity(), true); | ||
46 | var forbiddenView = new ForbiddenView(symbol); | ||
47 | var mayName = DnfLifter.decorateName(name, Modality.MAY, Concreteness.PARTIAL); | ||
48 | |||
49 | storeBuilder.with(PartialRelationTranslator.of(linkType) | ||
50 | .symbol(symbol) | ||
51 | .may(Query.of(mayName, (builder, source, target) -> { | ||
52 | builder.clause( | ||
53 | mayNewSource.call(source), | ||
54 | mayNewTarget.call(target), | ||
55 | not(forbiddenView.call(source, target)) | ||
56 | ); | ||
57 | if (info.isConstrained()) { | ||
58 | // Violation of monotonicity: | ||
59 | // Edges violating upper multiplicity will not be marked as {@code ERROR}, but the | ||
60 | // corresponding error pattern will already mark the node as invalid. | ||
61 | builder.clause( | ||
62 | must(linkType.call(source, target)), | ||
63 | not(forbiddenView.call(source, target)), | ||
64 | may(sourceType.call(source)), | ||
65 | may(targetType.call(target)) | ||
66 | ); | ||
67 | } | ||
68 | })) | ||
69 | .refiner(DirectedCrossReferenceRefiner.of(symbol, sourceType, targetType)) | ||
70 | .initializer(new RefinementBasedInitializer<>(linkType))); | ||
71 | |||
72 | storeBuilder.with(new InvalidMultiplicityErrorTranslator(sourceType, linkType, false, | ||
73 | info.sourceMultiplicity())); | ||
74 | |||
75 | storeBuilder.with(new InvalidMultiplicityErrorTranslator(targetType, linkType, true, | ||
76 | info.targetMultiplicity())); | ||
77 | } | ||
78 | |||
79 | private RelationalQuery createMayHelper(PartialRelation type, Multiplicity multiplicity, boolean inverse) { | ||
80 | return CrossReferenceUtils.createMayHelper(linkType, type, multiplicity, inverse); | ||
81 | } | ||
82 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceInfo.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceInfo.java new file mode 100644 index 00000000..fe99bc54 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceInfo.java | |||
@@ -0,0 +1,15 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.crossreference; | ||
7 | |||
8 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
9 | import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity; | ||
10 | |||
11 | public record UndirectedCrossReferenceInfo(PartialRelation type, Multiplicity multiplicity) { | ||
12 | public boolean isConstrained() { | ||
13 | return multiplicity.isConstrained(); | ||
14 | } | ||
15 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceRefiner.java new file mode 100644 index 00000000..43c1462b --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceRefiner.java | |||
@@ -0,0 +1,44 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.crossreference; | ||
7 | |||
8 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
9 | import tools.refinery.store.reasoning.refinement.ConcreteSymbolRefiner; | ||
10 | import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner; | ||
11 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
12 | import tools.refinery.store.reasoning.representation.PartialSymbol; | ||
13 | import tools.refinery.store.representation.Symbol; | ||
14 | import tools.refinery.store.representation.TruthValue; | ||
15 | import tools.refinery.store.tuple.Tuple; | ||
16 | |||
17 | class UndirectedCrossReferenceRefiner extends ConcreteSymbolRefiner<TruthValue, Boolean> { | ||
18 | private final PartialInterpretationRefiner<TruthValue, Boolean> sourceRefiner; | ||
19 | |||
20 | public UndirectedCrossReferenceRefiner(ReasoningAdapter adapter, PartialSymbol<TruthValue, Boolean> partialSymbol, | ||
21 | Symbol<TruthValue> concreteSymbol, PartialRelation sourceType) { | ||
22 | super(adapter, partialSymbol, concreteSymbol); | ||
23 | sourceRefiner = adapter.getRefiner(sourceType); | ||
24 | } | ||
25 | |||
26 | @Override | ||
27 | public boolean merge(Tuple key, TruthValue value) { | ||
28 | int source = key.get(0); | ||
29 | int target = key.get(1); | ||
30 | if (!super.merge(key, value) || !super.merge(Tuple.of(target, source), value)) { | ||
31 | return false; | ||
32 | } | ||
33 | if (value.must()) { | ||
34 | return sourceRefiner.merge(Tuple.of(source), TruthValue.TRUE) && | ||
35 | sourceRefiner.merge(Tuple.of(target), TruthValue.TRUE); | ||
36 | } | ||
37 | return true; | ||
38 | } | ||
39 | |||
40 | public static Factory<TruthValue, Boolean> of(Symbol<TruthValue> concreteSymbol, PartialRelation sourceType) { | ||
41 | return (adapter, partialSymbol) -> new UndirectedCrossReferenceRefiner(adapter, partialSymbol, concreteSymbol, | ||
42 | sourceType); | ||
43 | } | ||
44 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceTranslator.java new file mode 100644 index 00000000..e599992d --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceTranslator.java | |||
@@ -0,0 +1,71 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.crossreference; | ||
7 | |||
8 | import tools.refinery.store.model.ModelStoreBuilder; | ||
9 | import tools.refinery.store.model.ModelStoreConfiguration; | ||
10 | import tools.refinery.store.query.dnf.Query; | ||
11 | import tools.refinery.store.query.view.ForbiddenView; | ||
12 | import tools.refinery.store.reasoning.lifting.DnfLifter; | ||
13 | import tools.refinery.store.reasoning.literal.Concreteness; | ||
14 | import tools.refinery.store.reasoning.literal.Modality; | ||
15 | import tools.refinery.store.reasoning.refinement.RefinementBasedInitializer; | ||
16 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
17 | import tools.refinery.store.reasoning.translator.PartialRelationTranslator; | ||
18 | import tools.refinery.store.reasoning.translator.multiplicity.InvalidMultiplicityErrorTranslator; | ||
19 | import tools.refinery.store.representation.Symbol; | ||
20 | import tools.refinery.store.representation.TruthValue; | ||
21 | |||
22 | import static tools.refinery.store.query.literal.Literals.not; | ||
23 | import static tools.refinery.store.reasoning.literal.PartialLiterals.may; | ||
24 | import static tools.refinery.store.reasoning.literal.PartialLiterals.must; | ||
25 | |||
26 | public class UndirectedCrossReferenceTranslator implements ModelStoreConfiguration { | ||
27 | private final PartialRelation linkType; | ||
28 | private final UndirectedCrossReferenceInfo info; | ||
29 | private final Symbol<TruthValue> symbol; | ||
30 | |||
31 | public UndirectedCrossReferenceTranslator(PartialRelation linkType, UndirectedCrossReferenceInfo info) { | ||
32 | this.linkType = linkType; | ||
33 | this.info = info; | ||
34 | symbol = Symbol.of(linkType.name(), 2, TruthValue.class, TruthValue.UNKNOWN); | ||
35 | } | ||
36 | |||
37 | @Override | ||
38 | public void apply(ModelStoreBuilder storeBuilder) { | ||
39 | var name = linkType.name(); | ||
40 | var type = info.type(); | ||
41 | var forbiddenView = new ForbiddenView(symbol); | ||
42 | var mayName = DnfLifter.decorateName(name, Modality.MAY, Concreteness.PARTIAL); | ||
43 | |||
44 | var mayNewSource = CrossReferenceUtils.createMayHelper(linkType, type, info.multiplicity(), false); | ||
45 | |||
46 | storeBuilder.with(PartialRelationTranslator.of(linkType) | ||
47 | .symbol(symbol) | ||
48 | .may(Query.of(mayName, (builder, source, target) -> { | ||
49 | builder.clause( | ||
50 | mayNewSource.call(source), | ||
51 | mayNewSource.call(target), | ||
52 | not(forbiddenView.call(source, target)) | ||
53 | ); | ||
54 | if (info.isConstrained()) { | ||
55 | // Violation of monotonicity: | ||
56 | // Edges violating upper multiplicity will not be marked as {@code ERROR}, but the | ||
57 | // corresponding error pattern will already mark the node as invalid. | ||
58 | builder.clause( | ||
59 | must(linkType.call(source, target)), | ||
60 | not(forbiddenView.call(source, target)), | ||
61 | may(type.call(source)), | ||
62 | may(type.call(target)) | ||
63 | ); | ||
64 | } | ||
65 | })) | ||
66 | .refiner(UndirectedCrossReferenceRefiner.of(symbol, type)) | ||
67 | .initializer(new RefinementBasedInitializer<>(linkType))); | ||
68 | |||
69 | storeBuilder.with(new InvalidMultiplicityErrorTranslator(type, linkType, false, info.multiplicity())); | ||
70 | } | ||
71 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/ContainedTypeHierarchyBuilder.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/ContainedTypeHierarchyBuilder.java new file mode 100644 index 00000000..cc43bce6 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/ContainedTypeHierarchyBuilder.java | |||
@@ -0,0 +1,32 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.metamodel; | ||
7 | |||
8 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
9 | import tools.refinery.store.reasoning.translator.containment.ContainmentHierarchyTranslator; | ||
10 | import tools.refinery.store.reasoning.translator.typehierarchy.TypeHierarchyBuilder; | ||
11 | |||
12 | import java.util.Collection; | ||
13 | |||
14 | public class ContainedTypeHierarchyBuilder extends TypeHierarchyBuilder { | ||
15 | ContainedTypeHierarchyBuilder() { | ||
16 | } | ||
17 | |||
18 | boolean isInvalidType(PartialRelation type) { | ||
19 | return !typeInfoMap.containsKey(type); | ||
20 | } | ||
21 | |||
22 | void setContainedTypes(Collection<PartialRelation> containedTypes) { | ||
23 | for (var containedType : containedTypes) { | ||
24 | var currentInfo = typeInfoMap.get(containedType); | ||
25 | if (currentInfo == null) { | ||
26 | throw new IllegalArgumentException("Invalid contained type: " + containedType); | ||
27 | } | ||
28 | var newInfo = currentInfo.addSupertype(ContainmentHierarchyTranslator.CONTAINED_SYMBOL); | ||
29 | typeInfoMap.put(containedType, newInfo); | ||
30 | } | ||
31 | } | ||
32 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/Metamodel.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/Metamodel.java new file mode 100644 index 00000000..72b836ff --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/Metamodel.java | |||
@@ -0,0 +1,23 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.metamodel; | ||
7 | |||
8 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
9 | import tools.refinery.store.reasoning.translator.containment.ContainmentInfo; | ||
10 | import tools.refinery.store.reasoning.translator.crossreference.DirectedCrossReferenceInfo; | ||
11 | import tools.refinery.store.reasoning.translator.crossreference.UndirectedCrossReferenceInfo; | ||
12 | import tools.refinery.store.reasoning.translator.typehierarchy.TypeHierarchy; | ||
13 | |||
14 | import java.util.Map; | ||
15 | |||
16 | public record Metamodel(TypeHierarchy typeHierarchy, Map<PartialRelation, ContainmentInfo> containmentHierarchy, | ||
17 | Map<PartialRelation, DirectedCrossReferenceInfo> directedCrossReferences, | ||
18 | Map<PartialRelation, UndirectedCrossReferenceInfo> undirectedCrossReferences, | ||
19 | Map<PartialRelation, PartialRelation> oppositeReferences) { | ||
20 | public static MetamodelBuilder builder() { | ||
21 | return new MetamodelBuilder(); | ||
22 | } | ||
23 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelBuilder.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelBuilder.java new file mode 100644 index 00000000..92370e25 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelBuilder.java | |||
@@ -0,0 +1,223 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.metamodel; | ||
7 | |||
8 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
9 | import tools.refinery.store.reasoning.translator.containment.ContainmentHierarchyTranslator; | ||
10 | import tools.refinery.store.reasoning.translator.containment.ContainmentInfo; | ||
11 | import tools.refinery.store.reasoning.translator.crossreference.DirectedCrossReferenceInfo; | ||
12 | import tools.refinery.store.reasoning.translator.crossreference.UndirectedCrossReferenceInfo; | ||
13 | import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity; | ||
14 | import tools.refinery.store.reasoning.translator.multiplicity.UnconstrainedMultiplicity; | ||
15 | import tools.refinery.store.reasoning.translator.typehierarchy.TypeInfo; | ||
16 | import tools.refinery.store.representation.cardinality.CardinalityIntervals; | ||
17 | |||
18 | import java.util.*; | ||
19 | |||
20 | public class MetamodelBuilder { | ||
21 | private final ContainedTypeHierarchyBuilder typeHierarchyBuilder = new ContainedTypeHierarchyBuilder(); | ||
22 | private final Map<PartialRelation, ReferenceInfo> referenceInfoMap = new LinkedHashMap<>(); | ||
23 | private final Set<PartialRelation> containedTypes = new HashSet<>(); | ||
24 | private final Map<PartialRelation, ContainmentInfo> containmentHierarchy = new LinkedHashMap<>(); | ||
25 | private final Map<PartialRelation, DirectedCrossReferenceInfo> directedCrossReferences = new LinkedHashMap<>(); | ||
26 | private final Map<PartialRelation, UndirectedCrossReferenceInfo> undirectedCrossReferences = new LinkedHashMap<>(); | ||
27 | private final Map<PartialRelation, PartialRelation> oppositeReferences = new LinkedHashMap<>(); | ||
28 | |||
29 | MetamodelBuilder() { | ||
30 | typeHierarchyBuilder.type(ContainmentHierarchyTranslator.CONTAINED_SYMBOL, true); | ||
31 | } | ||
32 | |||
33 | public MetamodelBuilder type(PartialRelation partialRelation, TypeInfo typeInfo) { | ||
34 | typeHierarchyBuilder.type(partialRelation, typeInfo); | ||
35 | return this; | ||
36 | |||
37 | } | ||
38 | |||
39 | public MetamodelBuilder type(PartialRelation partialRelation, boolean abstractType, | ||
40 | PartialRelation... supertypes) { | ||
41 | typeHierarchyBuilder.type(partialRelation, abstractType, supertypes); | ||
42 | return this; | ||
43 | } | ||
44 | |||
45 | public MetamodelBuilder type(PartialRelation partialRelation, boolean abstractType, | ||
46 | Collection<PartialRelation> supertypes) { | ||
47 | typeHierarchyBuilder.type(partialRelation, abstractType, supertypes); | ||
48 | return this; | ||
49 | } | ||
50 | |||
51 | public MetamodelBuilder type(PartialRelation partialRelation, PartialRelation... supertypes) { | ||
52 | typeHierarchyBuilder.type(partialRelation, supertypes); | ||
53 | return this; | ||
54 | } | ||
55 | |||
56 | public MetamodelBuilder type(PartialRelation partialRelation, Collection<PartialRelation> supertypes) { | ||
57 | typeHierarchyBuilder.type(partialRelation, supertypes); | ||
58 | return this; | ||
59 | } | ||
60 | |||
61 | public MetamodelBuilder types(Collection<Map.Entry<PartialRelation, TypeInfo>> entries) { | ||
62 | typeHierarchyBuilder.types(entries); | ||
63 | return this; | ||
64 | } | ||
65 | |||
66 | public MetamodelBuilder types(Map<PartialRelation, TypeInfo> map) { | ||
67 | typeHierarchyBuilder.types(map); | ||
68 | return this; | ||
69 | } | ||
70 | |||
71 | public MetamodelBuilder reference(PartialRelation linkType, ReferenceInfo info) { | ||
72 | if (linkType.arity() != 2) { | ||
73 | throw new IllegalArgumentException("Only references of arity 2 are supported, got %s with %d instead" | ||
74 | .formatted(linkType, linkType.arity())); | ||
75 | } | ||
76 | var putResult = referenceInfoMap.put(linkType, info); | ||
77 | if (putResult != null && !putResult.equals(info)) { | ||
78 | throw new IllegalArgumentException("Duplicate reference info for partial relation: " + linkType); | ||
79 | } | ||
80 | return this; | ||
81 | } | ||
82 | |||
83 | public MetamodelBuilder reference(PartialRelation linkType, PartialRelation sourceType, boolean containment, | ||
84 | Multiplicity multiplicity, PartialRelation targetType, | ||
85 | PartialRelation opposite) { | ||
86 | return reference(linkType, new ReferenceInfo(containment, sourceType, multiplicity, targetType, opposite)); | ||
87 | } | ||
88 | |||
89 | public MetamodelBuilder reference(PartialRelation linkType, PartialRelation sourceType, Multiplicity multiplicity, | ||
90 | PartialRelation targetType, PartialRelation opposite) { | ||
91 | return reference(linkType, sourceType, false, multiplicity, targetType, opposite); | ||
92 | } | ||
93 | |||
94 | public MetamodelBuilder reference(PartialRelation linkType, PartialRelation sourceType, | ||
95 | boolean containment, PartialRelation targetType, PartialRelation opposite) { | ||
96 | return reference(linkType, sourceType, containment, UnconstrainedMultiplicity.INSTANCE, targetType, opposite); | ||
97 | } | ||
98 | |||
99 | public MetamodelBuilder reference(PartialRelation linkType, PartialRelation sourceType, PartialRelation targetType, | ||
100 | PartialRelation opposite) { | ||
101 | return reference(linkType, sourceType, UnconstrainedMultiplicity.INSTANCE, targetType, opposite); | ||
102 | } | ||
103 | |||
104 | public MetamodelBuilder reference(PartialRelation linkType, PartialRelation sourceType, boolean containment, | ||
105 | Multiplicity multiplicity, PartialRelation targetType) { | ||
106 | return reference(linkType, sourceType, containment, multiplicity, targetType, null); | ||
107 | } | ||
108 | |||
109 | public MetamodelBuilder reference(PartialRelation linkType, PartialRelation sourceType, Multiplicity multiplicity, | ||
110 | PartialRelation targetType) { | ||
111 | return reference(linkType, sourceType, multiplicity, targetType, null); | ||
112 | } | ||
113 | |||
114 | public MetamodelBuilder reference(PartialRelation linkType, PartialRelation sourceType, boolean containment, | ||
115 | PartialRelation targetType) { | ||
116 | return reference(linkType, sourceType, containment, targetType, null); | ||
117 | } | ||
118 | |||
119 | public MetamodelBuilder reference(PartialRelation linkType, PartialRelation sourceType, | ||
120 | PartialRelation targetType) { | ||
121 | return reference(linkType, sourceType, targetType, null); | ||
122 | } | ||
123 | |||
124 | public MetamodelBuilder references(Collection<Map.Entry<PartialRelation, ReferenceInfo>> entries) { | ||
125 | for (var entry : entries) { | ||
126 | reference(entry.getKey(), entry.getValue()); | ||
127 | } | ||
128 | return this; | ||
129 | } | ||
130 | |||
131 | public MetamodelBuilder references(Map<PartialRelation, ReferenceInfo> map) { | ||
132 | return references(map.entrySet()); | ||
133 | } | ||
134 | |||
135 | public Metamodel build() { | ||
136 | for (var entry : referenceInfoMap.entrySet()) { | ||
137 | var linkType = entry.getKey(); | ||
138 | var info = entry.getValue(); | ||
139 | processReferenceInfo(linkType, info); | ||
140 | } | ||
141 | typeHierarchyBuilder.setContainedTypes(containedTypes); | ||
142 | var typeHierarchy = typeHierarchyBuilder.build(); | ||
143 | return new Metamodel(typeHierarchy, Collections.unmodifiableMap(containmentHierarchy), | ||
144 | Collections.unmodifiableMap(directedCrossReferences), | ||
145 | Collections.unmodifiableMap(undirectedCrossReferences), | ||
146 | Collections.unmodifiableMap(oppositeReferences)); | ||
147 | } | ||
148 | |||
149 | private void processReferenceInfo(PartialRelation linkType, ReferenceInfo info) { | ||
150 | if (oppositeReferences.containsKey(linkType) || containmentHierarchy.containsKey(linkType)) { | ||
151 | // We already processed this reference while processing its opposite. | ||
152 | return; | ||
153 | } | ||
154 | var sourceType = info.sourceType(); | ||
155 | var targetType = info.targetType(); | ||
156 | if (typeHierarchyBuilder.isInvalidType(sourceType)) { | ||
157 | throw new IllegalArgumentException("Source type %s of %s is not in type hierarchy" | ||
158 | .formatted(sourceType, linkType)); | ||
159 | } | ||
160 | if (typeHierarchyBuilder.isInvalidType(targetType)) { | ||
161 | throw new IllegalArgumentException("Target type %s of %s is not in type hierarchy" | ||
162 | .formatted(targetType, linkType)); | ||
163 | } | ||
164 | var opposite = info.opposite(); | ||
165 | Multiplicity targetMultiplicity = UnconstrainedMultiplicity.INSTANCE; | ||
166 | if (opposite != null) { | ||
167 | var oppositeInfo = referenceInfoMap.get(opposite); | ||
168 | validateOpposite(linkType, info, opposite, oppositeInfo); | ||
169 | targetMultiplicity = oppositeInfo.multiplicity(); | ||
170 | if (oppositeInfo.containment()) { | ||
171 | // Skip processing this reference and process it once we encounter its containment opposite. | ||
172 | return; | ||
173 | } | ||
174 | if (opposite.equals(linkType)) { | ||
175 | if (!sourceType.equals(targetType)) { | ||
176 | throw new IllegalArgumentException("Target %s of undirected reference %s differs from source %s" | ||
177 | .formatted(targetType, linkType, sourceType)); | ||
178 | } | ||
179 | undirectedCrossReferences.put(linkType, new UndirectedCrossReferenceInfo(sourceType, | ||
180 | info.multiplicity())); | ||
181 | return; | ||
182 | } | ||
183 | oppositeReferences.put(opposite, linkType); | ||
184 | } | ||
185 | if (info.containment()) { | ||
186 | if (targetMultiplicity.multiplicity().meet(CardinalityIntervals.ONE).isEmpty()) { | ||
187 | throw new IllegalArgumentException("Invalid opposite %s with multiplicity %s of containment %s" | ||
188 | .formatted(opposite, targetMultiplicity, linkType)); | ||
189 | } | ||
190 | containedTypes.add(targetType); | ||
191 | containmentHierarchy.put(linkType, new ContainmentInfo(sourceType, info.multiplicity(), targetType)); | ||
192 | return; | ||
193 | } | ||
194 | directedCrossReferences.put(linkType, new DirectedCrossReferenceInfo(sourceType, info.multiplicity(), | ||
195 | targetType, targetMultiplicity)); | ||
196 | } | ||
197 | |||
198 | private static void validateOpposite(PartialRelation linkType, ReferenceInfo info, PartialRelation opposite, | ||
199 | ReferenceInfo oppositeInfo) { | ||
200 | var sourceType = info.sourceType(); | ||
201 | var targetType = info.targetType(); | ||
202 | if (oppositeInfo == null) { | ||
203 | throw new IllegalArgumentException("Opposite %s of %s is not defined" | ||
204 | .formatted(opposite, linkType)); | ||
205 | } | ||
206 | if (!oppositeInfo.opposite().equals(linkType)) { | ||
207 | throw new IllegalArgumentException("Expected %s to have opposite %s, got %s instead" | ||
208 | .formatted(opposite, linkType, oppositeInfo.opposite())); | ||
209 | } | ||
210 | if (!oppositeInfo.sourceType().equals(targetType)) { | ||
211 | throw new IllegalArgumentException("Expected %s to have source type %s, got %s instead" | ||
212 | .formatted(opposite, targetType, oppositeInfo.sourceType())); | ||
213 | } | ||
214 | if (!oppositeInfo.targetType().equals(sourceType)) { | ||
215 | throw new IllegalArgumentException("Expected %s to have target type %s, got %s instead" | ||
216 | .formatted(opposite, sourceType, oppositeInfo.targetType())); | ||
217 | } | ||
218 | if (oppositeInfo.containment() && info.containment()) { | ||
219 | throw new IllegalArgumentException("Opposite %s of containment %s cannot be containment" | ||
220 | .formatted(opposite, linkType)); | ||
221 | } | ||
222 | } | ||
223 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelTranslator.java new file mode 100644 index 00000000..5afa58f2 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelTranslator.java | |||
@@ -0,0 +1,37 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.metamodel; | ||
7 | |||
8 | import tools.refinery.store.model.ModelStoreBuilder; | ||
9 | import tools.refinery.store.model.ModelStoreConfiguration; | ||
10 | import tools.refinery.store.reasoning.translator.containment.ContainmentHierarchyTranslator; | ||
11 | import tools.refinery.store.reasoning.translator.crossreference.DirectedCrossReferenceTranslator; | ||
12 | import tools.refinery.store.reasoning.translator.crossreference.UndirectedCrossReferenceTranslator; | ||
13 | import tools.refinery.store.reasoning.translator.opposite.OppositeRelationTranslator; | ||
14 | import tools.refinery.store.reasoning.translator.typehierarchy.TypeHierarchyTranslator; | ||
15 | |||
16 | public class MetamodelTranslator implements ModelStoreConfiguration { | ||
17 | private final Metamodel metamodel; | ||
18 | |||
19 | public MetamodelTranslator(Metamodel metamodel) { | ||
20 | this.metamodel = metamodel; | ||
21 | } | ||
22 | |||
23 | @Override | ||
24 | public void apply(ModelStoreBuilder storeBuilder) { | ||
25 | storeBuilder.with(new TypeHierarchyTranslator(metamodel.typeHierarchy())); | ||
26 | storeBuilder.with(new ContainmentHierarchyTranslator(metamodel.containmentHierarchy())); | ||
27 | for (var entry : metamodel.directedCrossReferences().entrySet()) { | ||
28 | storeBuilder.with(new DirectedCrossReferenceTranslator(entry.getKey(), entry.getValue())); | ||
29 | } | ||
30 | for (var entry : metamodel.undirectedCrossReferences().entrySet()) { | ||
31 | storeBuilder.with(new UndirectedCrossReferenceTranslator(entry.getKey(), entry.getValue())); | ||
32 | } | ||
33 | for (var entry : metamodel.oppositeReferences().entrySet()) { | ||
34 | storeBuilder.with(new OppositeRelationTranslator(entry.getKey(), entry.getValue())); | ||
35 | } | ||
36 | } | ||
37 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/ReferenceInfo.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/ReferenceInfo.java new file mode 100644 index 00000000..9a6b4012 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/ReferenceInfo.java | |||
@@ -0,0 +1,13 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.metamodel; | ||
7 | |||
8 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
9 | import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity; | ||
10 | |||
11 | public record ReferenceInfo(boolean containment, PartialRelation sourceType, Multiplicity multiplicity, | ||
12 | PartialRelation targetType, PartialRelation opposite) { | ||
13 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/EqualsRelationRewriter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/EqualsRelationRewriter.java index 393a8769..61b9488c 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/EqualsRelationRewriter.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/EqualsRelationRewriter.java | |||
@@ -69,12 +69,12 @@ class EqualsRelationRewriter extends QueryBasedRelationRewriter { | |||
69 | } | 69 | } |
70 | 70 | ||
71 | public static EqualsRelationRewriter of(AnySymbolView upperCardinalityView) { | 71 | public static EqualsRelationRewriter of(AnySymbolView upperCardinalityView) { |
72 | var may = Query.of("MAY_EQUALS", (builder, p1, p2) -> builder | 72 | var may = Query.of("equals#may", (builder, p1, p2) -> builder |
73 | .clause( | 73 | .clause( |
74 | p1.isEquivalent(p2), | 74 | p1.isEquivalent(p2), |
75 | upperCardinalityView.call(p1, Variable.of(UpperCardinality.class)) | 75 | upperCardinalityView.call(p1, Variable.of(UpperCardinality.class)) |
76 | )); | 76 | )); |
77 | var must = Query.of("MUST_EQUALS", (builder, p1, p2) -> builder | 77 | var must = Query.of("equals#must", (builder, p1, p2) -> builder |
78 | .clause(UpperCardinality.class, upper -> List.of( | 78 | .clause(UpperCardinality.class, upper -> List.of( |
79 | p1.isEquivalent(p2), | 79 | p1.isEquivalent(p2), |
80 | upperCardinalityView.call(p1, upper), | 80 | upperCardinalityView.call(p1, upper), |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectTranslator.java index 09993c80..c62557d7 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectTranslator.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectTranslator.java | |||
@@ -41,12 +41,12 @@ public class MultiObjectTranslator implements ModelStoreConfiguration { | |||
41 | storeBuilder.symbol(COUNT_STORAGE); | 41 | storeBuilder.symbol(COUNT_STORAGE); |
42 | 42 | ||
43 | storeBuilder.with(PartialRelationTranslator.of(ReasoningAdapter.EXISTS_SYMBOL) | 43 | storeBuilder.with(PartialRelationTranslator.of(ReasoningAdapter.EXISTS_SYMBOL) |
44 | .may(Query.of("MAY_EXISTS", (builder, p1) -> builder | 44 | .may(Query.of("exists#may", (builder, p1) -> builder |
45 | .clause(UpperCardinality.class, upper -> List.of( | 45 | .clause(UpperCardinality.class, upper -> List.of( |
46 | UPPER_CARDINALITY_VIEW.call(p1, upper), | 46 | UPPER_CARDINALITY_VIEW.call(p1, upper), |
47 | check(greaterEq(upper, constant(UpperCardinalities.ONE))) | 47 | check(greaterEq(upper, constant(UpperCardinalities.ONE))) |
48 | )))) | 48 | )))) |
49 | .must(Query.of("MUST_EXISTS", (builder, p1) -> builder | 49 | .must(Query.of("exists#must", (builder, p1) -> builder |
50 | .clause(Integer.class, lower -> List.of( | 50 | .clause(Integer.class, lower -> List.of( |
51 | LOWER_CARDINALITY_VIEW.call(p1, lower), | 51 | LOWER_CARDINALITY_VIEW.call(p1, lower), |
52 | check(greaterEq(lower, constant(1))) | 52 | check(greaterEq(lower, constant(1))) |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/ConstrainedMultiplicity.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/ConstrainedMultiplicity.java new file mode 100644 index 00000000..e441e41e --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/ConstrainedMultiplicity.java | |||
@@ -0,0 +1,36 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.multiplicity; | ||
7 | |||
8 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
9 | import tools.refinery.store.representation.cardinality.CardinalityInterval; | ||
10 | import tools.refinery.store.representation.cardinality.CardinalityIntervals; | ||
11 | import tools.refinery.store.representation.cardinality.NonEmptyCardinalityInterval; | ||
12 | |||
13 | public record ConstrainedMultiplicity(NonEmptyCardinalityInterval multiplicity, PartialRelation errorSymbol) | ||
14 | implements Multiplicity { | ||
15 | public ConstrainedMultiplicity { | ||
16 | if (multiplicity.equals(CardinalityIntervals.SET)) { | ||
17 | throw new IllegalArgumentException("Expected a constrained cardinality interval"); | ||
18 | } | ||
19 | if (errorSymbol.arity() != 1) { | ||
20 | throw new IllegalArgumentException("Expected error symbol %s to have arity 1, got %d instead" | ||
21 | .formatted(errorSymbol, errorSymbol.arity())); | ||
22 | } | ||
23 | } | ||
24 | |||
25 | public static ConstrainedMultiplicity of(CardinalityInterval multiplicity, PartialRelation errorSymbol) { | ||
26 | if (!(multiplicity instanceof NonEmptyCardinalityInterval nonEmptyCardinalityInterval)) { | ||
27 | throw new IllegalArgumentException("Inconsistent multiplicity"); | ||
28 | } | ||
29 | return new ConstrainedMultiplicity(nonEmptyCardinalityInterval, errorSymbol); | ||
30 | } | ||
31 | |||
32 | @Override | ||
33 | public boolean isConstrained() { | ||
34 | return true; | ||
35 | } | ||
36 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/InvalidMultiplicityErrorTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/InvalidMultiplicityErrorTranslator.java new file mode 100644 index 00000000..522d8455 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/InvalidMultiplicityErrorTranslator.java | |||
@@ -0,0 +1,115 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.multiplicity; | ||
7 | |||
8 | import tools.refinery.store.model.ModelStoreBuilder; | ||
9 | import tools.refinery.store.model.ModelStoreConfiguration; | ||
10 | import tools.refinery.store.query.dnf.Query; | ||
11 | import tools.refinery.store.query.term.Variable; | ||
12 | import tools.refinery.store.query.term.int_.IntTerms; | ||
13 | import tools.refinery.store.reasoning.lifting.DnfLifter; | ||
14 | import tools.refinery.store.reasoning.literal.*; | ||
15 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
16 | import tools.refinery.store.reasoning.translator.PartialRelationTranslator; | ||
17 | import tools.refinery.store.representation.cardinality.FiniteUpperCardinality; | ||
18 | import tools.refinery.store.representation.cardinality.UpperCardinalities; | ||
19 | import tools.refinery.store.representation.cardinality.UpperCardinality; | ||
20 | |||
21 | import java.util.List; | ||
22 | |||
23 | import static tools.refinery.store.query.literal.Literals.check; | ||
24 | import static tools.refinery.store.query.term.int_.IntTerms.greater; | ||
25 | import static tools.refinery.store.query.term.uppercardinality.UpperCardinalityTerms.constant; | ||
26 | import static tools.refinery.store.query.term.uppercardinality.UpperCardinalityTerms.less; | ||
27 | import static tools.refinery.store.reasoning.literal.PartialLiterals.candidateMust; | ||
28 | import static tools.refinery.store.reasoning.literal.PartialLiterals.must; | ||
29 | |||
30 | public class InvalidMultiplicityErrorTranslator implements ModelStoreConfiguration { | ||
31 | private final PartialRelation nodeType; | ||
32 | private final PartialRelation linkType; | ||
33 | private final boolean inverse; | ||
34 | private final Multiplicity multiplicity; | ||
35 | |||
36 | public InvalidMultiplicityErrorTranslator(PartialRelation nodeType, PartialRelation linkType, | ||
37 | boolean inverse, Multiplicity multiplicity) { | ||
38 | if (nodeType.arity() != 1) { | ||
39 | throw new IllegalArgumentException("Node type must be of arity 1, got %s with arity %d instead" | ||
40 | .formatted(nodeType, nodeType.arity())); | ||
41 | } | ||
42 | if (linkType.arity() != 2) { | ||
43 | throw new IllegalArgumentException("Link type must be of arity 2, got %s with arity %d instead" | ||
44 | .formatted(linkType, linkType.arity())); | ||
45 | } | ||
46 | this.nodeType = nodeType; | ||
47 | this.linkType = linkType; | ||
48 | this.inverse = inverse; | ||
49 | this.multiplicity = multiplicity; | ||
50 | } | ||
51 | |||
52 | @Override | ||
53 | public void apply(ModelStoreBuilder storeBuilder) { | ||
54 | if (!(multiplicity instanceof ConstrainedMultiplicity constrainedMultiplicity)) { | ||
55 | return; | ||
56 | } | ||
57 | |||
58 | var name = constrainedMultiplicity.errorSymbol().name(); | ||
59 | var cardinalityInterval = constrainedMultiplicity.multiplicity(); | ||
60 | var node = Variable.of("node"); | ||
61 | var other = Variable.of("other"); | ||
62 | List<Variable> arguments = inverse ? List.of(other, node) : List.of(node, other); | ||
63 | var mustBuilder = Query.builder(DnfLifter.decorateName(name, Modality.MUST, Concreteness.PARTIAL)) | ||
64 | .parameter(node); | ||
65 | var candidateMayBuilder = Query.builder(DnfLifter.decorateName(name, Modality.MAY, Concreteness.PARTIAL)) | ||
66 | .parameter(node); | ||
67 | var candidateMustBuilder = Query.builder(DnfLifter.decorateName(name, Modality.MUST, Concreteness.PARTIAL)) | ||
68 | .parameter(node); | ||
69 | |||
70 | int lowerBound = cardinalityInterval.lowerBound(); | ||
71 | if (lowerBound > 0) { | ||
72 | var lowerBoundCardinality = UpperCardinalities.atMost(lowerBound); | ||
73 | mustBuilder.clause(UpperCardinality.class, existingContents -> List.of( | ||
74 | must(nodeType.call(node)), | ||
75 | new CountUpperBoundLiteral(existingContents, linkType, arguments), | ||
76 | check(less(existingContents, constant(lowerBoundCardinality))) | ||
77 | )); | ||
78 | candidateMayBuilder.clause(Integer.class, existingContents -> List.of( | ||
79 | candidateMust(nodeType.call(node)), | ||
80 | new CountCandidateLowerBoundLiteral(existingContents, linkType, arguments), | ||
81 | check(IntTerms.less(existingContents, IntTerms.constant(lowerBound))) | ||
82 | )); | ||
83 | candidateMustBuilder.clause(Integer.class, existingContents -> List.of( | ||
84 | candidateMust(nodeType.call(node)), | ||
85 | new CountCandidateUpperBoundLiteral(existingContents, linkType, arguments), | ||
86 | check(IntTerms.less(existingContents, IntTerms.constant(lowerBound))) | ||
87 | )); | ||
88 | } | ||
89 | |||
90 | if (cardinalityInterval.upperBound() instanceof FiniteUpperCardinality finiteUpperCardinality) { | ||
91 | int upperBound = finiteUpperCardinality.finiteUpperBound(); | ||
92 | mustBuilder.clause(Integer.class, existingContents -> List.of( | ||
93 | must(nodeType.call(node)), | ||
94 | new CountLowerBoundLiteral(existingContents, linkType, arguments), | ||
95 | check(greater(existingContents, IntTerms.constant(upperBound))) | ||
96 | )); | ||
97 | candidateMayBuilder.clause(Integer.class, existingContents -> List.of( | ||
98 | candidateMust(nodeType.call(node)), | ||
99 | new CountCandidateUpperBoundLiteral(existingContents, linkType, arguments), | ||
100 | check(greater(existingContents, IntTerms.constant(upperBound))) | ||
101 | )); | ||
102 | candidateMustBuilder.clause(Integer.class, existingContents -> List.of( | ||
103 | candidateMust(nodeType.call(node)), | ||
104 | new CountCandidateLowerBoundLiteral(existingContents, linkType, arguments), | ||
105 | check(greater(existingContents, IntTerms.constant(upperBound))) | ||
106 | )); | ||
107 | } | ||
108 | |||
109 | storeBuilder.with(PartialRelationTranslator.of(constrainedMultiplicity.errorSymbol()) | ||
110 | .mayNever() | ||
111 | .must(mustBuilder.build()) | ||
112 | .candidateMay(candidateMayBuilder.build()) | ||
113 | .candidateMust(candidateMustBuilder.build())); | ||
114 | } | ||
115 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/Multiplicity.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/Multiplicity.java new file mode 100644 index 00000000..d1d6dd1e --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/Multiplicity.java | |||
@@ -0,0 +1,14 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.multiplicity; | ||
7 | |||
8 | import tools.refinery.store.representation.cardinality.CardinalityInterval; | ||
9 | |||
10 | public sealed interface Multiplicity permits ConstrainedMultiplicity, UnconstrainedMultiplicity { | ||
11 | CardinalityInterval multiplicity(); | ||
12 | |||
13 | boolean isConstrained(); | ||
14 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/UnconstrainedMultiplicity.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/UnconstrainedMultiplicity.java new file mode 100644 index 00000000..2159b88c --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/UnconstrainedMultiplicity.java | |||
@@ -0,0 +1,28 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.multiplicity; | ||
7 | |||
8 | import tools.refinery.store.representation.cardinality.CardinalityInterval; | ||
9 | import tools.refinery.store.representation.cardinality.CardinalityIntervals; | ||
10 | |||
11 | // Singleton implementation, because there is only a single complete interval. | ||
12 | @SuppressWarnings("squid:S6548") | ||
13 | public final class UnconstrainedMultiplicity implements Multiplicity { | ||
14 | public static final UnconstrainedMultiplicity INSTANCE = new UnconstrainedMultiplicity(); | ||
15 | |||
16 | private UnconstrainedMultiplicity() { | ||
17 | } | ||
18 | |||
19 | @Override | ||
20 | public CardinalityInterval multiplicity() { | ||
21 | return CardinalityIntervals.SET; | ||
22 | } | ||
23 | |||
24 | @Override | ||
25 | public boolean isConstrained() { | ||
26 | return true; | ||
27 | } | ||
28 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/opposite/OppositeInterpretation.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/opposite/OppositeInterpretation.java new file mode 100644 index 00000000..7290ab40 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/opposite/OppositeInterpretation.java | |||
@@ -0,0 +1,77 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.opposite; | ||
7 | |||
8 | |||
9 | import tools.refinery.store.map.AnyVersionedMap; | ||
10 | import tools.refinery.store.map.Cursor; | ||
11 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
12 | import tools.refinery.store.reasoning.interpretation.AbstractPartialInterpretation; | ||
13 | import tools.refinery.store.reasoning.interpretation.PartialInterpretation; | ||
14 | import tools.refinery.store.reasoning.literal.Concreteness; | ||
15 | import tools.refinery.store.reasoning.representation.PartialSymbol; | ||
16 | import tools.refinery.store.tuple.Tuple; | ||
17 | |||
18 | import java.util.Set; | ||
19 | |||
20 | class OppositeInterpretation<A, C> extends AbstractPartialInterpretation<A, C> { | ||
21 | private final PartialInterpretation<A, C> opposite; | ||
22 | |||
23 | private OppositeInterpretation(ReasoningAdapter adapter, Concreteness concreteness, | ||
24 | PartialSymbol<A, C> partialSymbol, PartialInterpretation<A, C> opposite) { | ||
25 | super(adapter, concreteness, partialSymbol); | ||
26 | this.opposite = opposite; | ||
27 | } | ||
28 | |||
29 | @Override | ||
30 | public A get(Tuple key) { | ||
31 | return opposite.get(OppositeUtils.flip(key)); | ||
32 | } | ||
33 | |||
34 | @Override | ||
35 | public Cursor<Tuple, A> getAll() { | ||
36 | return new OppositeCursor<>(opposite.getAll()); | ||
37 | } | ||
38 | |||
39 | public static <A1, C1> Factory<A1, C1> of(PartialSymbol<A1, C1> oppositeSymbol) { | ||
40 | return (adapter, concreteness, partialSymbol) -> { | ||
41 | var opposite = adapter.getPartialInterpretation(concreteness, oppositeSymbol); | ||
42 | return new OppositeInterpretation<>(adapter, concreteness, partialSymbol, opposite); | ||
43 | }; | ||
44 | } | ||
45 | |||
46 | private record OppositeCursor<T>(Cursor<Tuple, T> opposite) implements Cursor<Tuple, T> { | ||
47 | @Override | ||
48 | public Tuple getKey() { | ||
49 | return OppositeUtils.flip(opposite.getKey()); | ||
50 | } | ||
51 | |||
52 | @Override | ||
53 | public T getValue() { | ||
54 | return opposite.getValue(); | ||
55 | } | ||
56 | |||
57 | @Override | ||
58 | public boolean isTerminated() { | ||
59 | return opposite.isTerminated(); | ||
60 | } | ||
61 | |||
62 | @Override | ||
63 | public boolean move() { | ||
64 | return opposite.move(); | ||
65 | } | ||
66 | |||
67 | @Override | ||
68 | public Set<AnyVersionedMap> getDependingMaps() { | ||
69 | return opposite.getDependingMaps(); | ||
70 | } | ||
71 | |||
72 | @Override | ||
73 | public boolean isDirty() { | ||
74 | return opposite.isDirty(); | ||
75 | } | ||
76 | } | ||
77 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/opposite/OppositeRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/opposite/OppositeRefiner.java new file mode 100644 index 00000000..d09684df --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/opposite/OppositeRefiner.java | |||
@@ -0,0 +1,32 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.opposite; | ||
7 | |||
8 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
9 | import tools.refinery.store.reasoning.refinement.AbstractPartialInterpretationRefiner; | ||
10 | import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner; | ||
11 | import tools.refinery.store.reasoning.representation.PartialSymbol; | ||
12 | import tools.refinery.store.tuple.Tuple; | ||
13 | |||
14 | public class OppositeRefiner<A, C> extends AbstractPartialInterpretationRefiner<A, C> { | ||
15 | private final PartialInterpretationRefiner<A, C> opposite; | ||
16 | |||
17 | protected OppositeRefiner(ReasoningAdapter adapter, PartialSymbol<A, C> partialSymbol, | ||
18 | PartialSymbol<A, C> oppositeSymbol) { | ||
19 | super(adapter, partialSymbol); | ||
20 | opposite = adapter.getRefiner(oppositeSymbol); | ||
21 | } | ||
22 | |||
23 | @Override | ||
24 | public boolean merge(Tuple key, A value) { | ||
25 | var oppositeKey = OppositeUtils.flip(key); | ||
26 | return opposite.merge(oppositeKey, value); | ||
27 | } | ||
28 | |||
29 | public static <A1, C1> Factory<A1, C1> of(PartialSymbol<A1, C1> oppositeSymbol) { | ||
30 | return (adapter, partialSymbol) -> new OppositeRefiner<>(adapter, partialSymbol, oppositeSymbol); | ||
31 | } | ||
32 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/opposite/OppositeRelationTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/opposite/OppositeRelationTranslator.java new file mode 100644 index 00000000..b25b9d7d --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/opposite/OppositeRelationTranslator.java | |||
@@ -0,0 +1,51 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.opposite; | ||
7 | |||
8 | import tools.refinery.store.model.ModelStoreBuilder; | ||
9 | import tools.refinery.store.model.ModelStoreConfiguration; | ||
10 | import tools.refinery.store.query.literal.AbstractCallLiteral; | ||
11 | import tools.refinery.store.query.literal.Literal; | ||
12 | import tools.refinery.store.query.term.Variable; | ||
13 | import tools.refinery.store.reasoning.interpretation.PartialRelationRewriter; | ||
14 | import tools.refinery.store.reasoning.literal.Concreteness; | ||
15 | import tools.refinery.store.reasoning.literal.ModalConstraint; | ||
16 | import tools.refinery.store.reasoning.literal.Modality; | ||
17 | import tools.refinery.store.reasoning.refinement.RefinementBasedInitializer; | ||
18 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
19 | import tools.refinery.store.reasoning.translator.PartialRelationTranslator; | ||
20 | |||
21 | import java.util.List; | ||
22 | import java.util.Set; | ||
23 | |||
24 | public class OppositeRelationTranslator implements ModelStoreConfiguration, PartialRelationRewriter { | ||
25 | private final PartialRelation linkType; | ||
26 | private final PartialRelation opposite; | ||
27 | |||
28 | public OppositeRelationTranslator(PartialRelation linkType, PartialRelation opposite) { | ||
29 | this.linkType = linkType; | ||
30 | this.opposite = opposite; | ||
31 | } | ||
32 | |||
33 | @Override | ||
34 | public void apply(ModelStoreBuilder storeBuilder) { | ||
35 | storeBuilder.with(PartialRelationTranslator.of(linkType) | ||
36 | .rewriter(this) | ||
37 | .interpretation(OppositeInterpretation.of(opposite)) | ||
38 | .refiner(OppositeRefiner.of(opposite)) | ||
39 | .initializer(new RefinementBasedInitializer<>(linkType))); | ||
40 | } | ||
41 | |||
42 | @Override | ||
43 | public List<Literal> rewriteLiteral(Set<Variable> positiveVariables, AbstractCallLiteral literal, | ||
44 | Modality modality, Concreteness concreteness) { | ||
45 | var arguments = literal.getArguments(); | ||
46 | var newArguments = List.of(arguments.get(1), arguments.get(0)); | ||
47 | var modalOpposite = new ModalConstraint(modality, concreteness, opposite); | ||
48 | var oppositeLiteral = literal.withArguments(modalOpposite, newArguments); | ||
49 | return List.of(oppositeLiteral); | ||
50 | } | ||
51 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/opposite/OppositeUtils.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/opposite/OppositeUtils.java new file mode 100644 index 00000000..2a9e6b5d --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/opposite/OppositeUtils.java | |||
@@ -0,0 +1,22 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.opposite; | ||
7 | |||
8 | import tools.refinery.store.tuple.Tuple; | ||
9 | import tools.refinery.store.tuple.Tuple2; | ||
10 | |||
11 | final class OppositeUtils { | ||
12 | private OppositeUtils() { | ||
13 | throw new IllegalStateException("This is a static utility class and should not be instantiated directly"); | ||
14 | } | ||
15 | |||
16 | public static Tuple flip(Tuple tuple) { | ||
17 | if (!(tuple instanceof Tuple2 tuple2)) { | ||
18 | throw new IllegalArgumentException("Cannot flip tuple: " + tuple); | ||
19 | } | ||
20 | return Tuple.of(tuple2.value1(), tuple2.value0()); | ||
21 | } | ||
22 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalysisResult.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalysisResult.java index 39a76745..ebe0d1b9 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalysisResult.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalysisResult.java | |||
@@ -10,7 +10,7 @@ import tools.refinery.store.representation.TruthValue; | |||
10 | 10 | ||
11 | import java.util.*; | 11 | import java.util.*; |
12 | 12 | ||
13 | final class TypeAnalysisResult { | 13 | public final class TypeAnalysisResult { |
14 | private final ExtendedTypeInfo extendedTypeInfo; | 14 | private final ExtendedTypeInfo extendedTypeInfo; |
15 | private final List<PartialRelation> directSubtypes; | 15 | private final List<PartialRelation> directSubtypes; |
16 | private final List<ExtendedTypeInfo> allExternalTypeInfoList; | 16 | private final List<ExtendedTypeInfo> allExternalTypeInfoList; |
@@ -44,6 +44,10 @@ final class TypeAnalysisResult { | |||
44 | return inferredType; | 44 | return inferredType; |
45 | } | 45 | } |
46 | 46 | ||
47 | public boolean isSubtypeOf(TypeAnalysisResult other) { | ||
48 | return extendedTypeInfo.getAllSubtypes().contains(other.type()); | ||
49 | } | ||
50 | |||
47 | public InferredType merge(InferredType inferredType, TruthValue value) { | 51 | public InferredType merge(InferredType inferredType, TruthValue value) { |
48 | return switch (value) { | 52 | return switch (value) { |
49 | case UNKNOWN -> inferredType; | 53 | case UNKNOWN -> inferredType; |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchy.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchy.java index 99069ab9..c32a06cb 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchy.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchy.java | |||
@@ -79,7 +79,12 @@ public class TypeHierarchy { | |||
79 | var found = new HashSet<PartialRelation>(); | 79 | var found = new HashSet<PartialRelation>(); |
80 | var allSupertypes = extendedTypeInfo.getAllSupertypes(); | 80 | var allSupertypes = extendedTypeInfo.getAllSupertypes(); |
81 | for (var supertype : allSupertypes) { | 81 | for (var supertype : allSupertypes) { |
82 | found.addAll(extendedTypeInfoMap.get(supertype).getAllSupertypes()); | 82 | var supertypeInfo = extendedTypeInfoMap.get(supertype); |
83 | if (supertypeInfo == null) { | ||
84 | throw new IllegalArgumentException("Supertype %s of %s is missing from the type hierarchy" | ||
85 | .formatted(supertype, extendedTypeInfo.getType())); | ||
86 | } | ||
87 | found.addAll(supertypeInfo.getAllSupertypes()); | ||
83 | } | 88 | } |
84 | if (allSupertypes.addAll(found)) { | 89 | if (allSupertypes.addAll(found)) { |
85 | changed = true; | 90 | changed = true; |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyBuilder.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyBuilder.java index 0fca4810..36efb878 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyBuilder.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyBuilder.java | |||
@@ -7,18 +7,19 @@ package tools.refinery.store.reasoning.translator.typehierarchy; | |||
7 | 7 | ||
8 | import tools.refinery.store.reasoning.representation.PartialRelation; | 8 | import tools.refinery.store.reasoning.representation.PartialRelation; |
9 | 9 | ||
10 | import java.util.Collection; | 10 | import java.util.*; |
11 | import java.util.LinkedHashMap; | ||
12 | import java.util.List; | ||
13 | import java.util.Map; | ||
14 | 11 | ||
12 | @SuppressWarnings("UnusedReturnValue") | ||
15 | public class TypeHierarchyBuilder { | 13 | public class TypeHierarchyBuilder { |
16 | private final Map<PartialRelation, TypeInfo> typeInfoMap = new LinkedHashMap<>(); | 14 | protected final Map<PartialRelation, TypeInfo> typeInfoMap = new LinkedHashMap<>(); |
15 | |||
16 | protected TypeHierarchyBuilder() { | ||
17 | } | ||
17 | 18 | ||
18 | public TypeHierarchyBuilder type(PartialRelation partialRelation, TypeInfo typeInfo) { | 19 | public TypeHierarchyBuilder type(PartialRelation partialRelation, TypeInfo typeInfo) { |
19 | if (partialRelation.arity() != 1) { | 20 | if (partialRelation.arity() != 1) { |
20 | throw new IllegalArgumentException("Only types of arity 1 are supported, hot %d instead" | 21 | throw new IllegalArgumentException("Only types of arity 1 are supported, got %s with %d instead" |
21 | .formatted(partialRelation.arity())); | 22 | .formatted(partialRelation, partialRelation.arity())); |
22 | } | 23 | } |
23 | var putResult = typeInfoMap.put(partialRelation, typeInfo); | 24 | var putResult = typeInfoMap.put(partialRelation, typeInfo); |
24 | if (putResult != null && !putResult.equals(typeInfo)) { | 25 | if (putResult != null && !putResult.equals(typeInfo)) { |
@@ -29,7 +30,7 @@ public class TypeHierarchyBuilder { | |||
29 | 30 | ||
30 | public TypeHierarchyBuilder type(PartialRelation partialRelation, boolean abstractType, | 31 | public TypeHierarchyBuilder type(PartialRelation partialRelation, boolean abstractType, |
31 | PartialRelation... supertypes) { | 32 | PartialRelation... supertypes) { |
32 | return type(partialRelation, abstractType, List.of(supertypes)); | 33 | return type(partialRelation, abstractType, Set.of(supertypes)); |
33 | } | 34 | } |
34 | 35 | ||
35 | public TypeHierarchyBuilder type(PartialRelation partialRelation, boolean abstractType, | 36 | public TypeHierarchyBuilder type(PartialRelation partialRelation, boolean abstractType, |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslator.java index 6a45acd3..4bff4557 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslator.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslator.java | |||
@@ -44,7 +44,7 @@ public class TypeHierarchyTranslator implements ModelStoreConfiguration { | |||
44 | } | 44 | } |
45 | 45 | ||
46 | private ModelStoreConfiguration createPreservedTypeTranslator(PartialRelation type, TypeAnalysisResult result) { | 46 | private ModelStoreConfiguration createPreservedTypeTranslator(PartialRelation type, TypeAnalysisResult result) { |
47 | var may = Query.of(type.name() + "#may", (builder, p1) -> { | 47 | var may = Query.of(type.name() + "#partial#may", (builder, p1) -> { |
48 | if (result.isAbstractType()) { | 48 | if (result.isAbstractType()) { |
49 | for (var subtype : result.getDirectSubtypes()) { | 49 | for (var subtype : result.getDirectSubtypes()) { |
50 | builder.clause(PartialLiterals.may(subtype.call(p1))); | 50 | builder.clause(PartialLiterals.may(subtype.call(p1))); |
@@ -54,7 +54,7 @@ public class TypeHierarchyTranslator implements ModelStoreConfiguration { | |||
54 | } | 54 | } |
55 | }); | 55 | }); |
56 | 56 | ||
57 | var must = Query.of(type.name() + "#must", (builder, p1) -> builder.clause( | 57 | var must = Query.of(type.name() + "#partial#must", (builder, p1) -> builder.clause( |
58 | new MustTypeView(typeSymbol, type).call(p1) | 58 | new MustTypeView(typeSymbol, type).call(p1) |
59 | )); | 59 | )); |
60 | 60 | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeInfo.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeInfo.java index 68ed4089..e6bdaff2 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeInfo.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeInfo.java | |||
@@ -9,5 +9,15 @@ import tools.refinery.store.reasoning.representation.PartialRelation; | |||
9 | 9 | ||
10 | import java.util.*; | 10 | import java.util.*; |
11 | 11 | ||
12 | public record TypeInfo(Collection<PartialRelation> supertypes, boolean abstractType) { | 12 | public record TypeInfo(Set<PartialRelation> supertypes, boolean abstractType) { |
13 | public TypeInfo(Collection<PartialRelation> supertypes, boolean abstractType) { | ||
14 | this(Set.copyOf(supertypes), abstractType); | ||
15 | } | ||
16 | |||
17 | public TypeInfo addSupertype(PartialRelation newSupertype) { | ||
18 | var newSupertypes = new ArrayList<PartialRelation>(supertypes.size() + 1); | ||
19 | newSupertypes.addAll(supertypes); | ||
20 | newSupertypes.add(newSupertype); | ||
21 | return new TypeInfo(newSupertypes, abstractType); | ||
22 | } | ||
13 | } | 23 | } |
diff --git a/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/PartialModelTest.java b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/PartialModelTest.java index b2188f5d..77560a68 100644 --- a/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/PartialModelTest.java +++ b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/PartialModelTest.java | |||
@@ -49,7 +49,7 @@ class PartialModelTest { | |||
49 | .symbol(personStorage)) | 49 | .symbol(personStorage)) |
50 | .with(PartialRelationTranslator.of(friend) | 50 | .with(PartialRelationTranslator.of(friend) |
51 | .symbol(friendStorage) | 51 | .symbol(friendStorage) |
52 | .may(Query.of("mayPerson", (builder, p1, p2) -> builder.clause( | 52 | .may(Query.of("mayFriend", (builder, p1, p2) -> builder.clause( |
53 | may(person.call(p1)), | 53 | may(person.call(p1)), |
54 | may(person.call(p2)), | 54 | may(person.call(p2)), |
55 | not(must(EQUALS_SYMBOL.call(p1, p2))), | 55 | not(must(EQUALS_SYMBOL.call(p1, p2))), |
diff --git a/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelTest.java b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelTest.java new file mode 100644 index 00000000..9e74cf02 --- /dev/null +++ b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelTest.java | |||
@@ -0,0 +1,108 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.metamodel; | ||
7 | |||
8 | import org.junit.jupiter.api.Test; | ||
9 | import tools.refinery.store.model.ModelStore; | ||
10 | import tools.refinery.store.query.viatra.ViatraModelQueryAdapter; | ||
11 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
12 | import tools.refinery.store.reasoning.ReasoningStoreAdapter; | ||
13 | import tools.refinery.store.reasoning.literal.Concreteness; | ||
14 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
15 | import tools.refinery.store.reasoning.seed.ModelSeed; | ||
16 | import tools.refinery.store.reasoning.translator.containment.ContainmentHierarchyTranslator; | ||
17 | import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator; | ||
18 | import tools.refinery.store.reasoning.translator.multiplicity.ConstrainedMultiplicity; | ||
19 | import tools.refinery.store.representation.TruthValue; | ||
20 | import tools.refinery.store.representation.cardinality.CardinalityIntervals; | ||
21 | import tools.refinery.store.tuple.Tuple; | ||
22 | |||
23 | import static org.hamcrest.MatcherAssert.assertThat; | ||
24 | import static org.hamcrest.Matchers.is; | ||
25 | |||
26 | class MetamodelTest { | ||
27 | private final PartialRelation person = new PartialRelation("Person", 1); | ||
28 | private final PartialRelation student = new PartialRelation("Student", 1); | ||
29 | private final PartialRelation teacher = new PartialRelation("Teacher", 1); | ||
30 | private final PartialRelation university = new PartialRelation("University", 1); | ||
31 | private final PartialRelation course = new PartialRelation("Course", 1); | ||
32 | private final PartialRelation courses = new PartialRelation("courses", 2); | ||
33 | private final PartialRelation location = new PartialRelation("location", 2); | ||
34 | private final PartialRelation lecturer = new PartialRelation("lecturer", 2); | ||
35 | private final PartialRelation invalidLecturerCount = new PartialRelation("invalidLecturerCount", 1); | ||
36 | private final PartialRelation enrolledStudents = new PartialRelation("enrolledStudents", 2); | ||
37 | private final PartialRelation invalidStudentCount = new PartialRelation("invalidStudentCount", 1); | ||
38 | |||
39 | @Test | ||
40 | void metamodelTest() { | ||
41 | var metamodel = Metamodel.builder() | ||
42 | .type(person, true) | ||
43 | .type(student, person) | ||
44 | .type(teacher, person) | ||
45 | .type(university) | ||
46 | .type(course) | ||
47 | .reference(courses, university, true, course, location) | ||
48 | .reference(location, course, university, courses) | ||
49 | .reference(lecturer, course, | ||
50 | ConstrainedMultiplicity.of(CardinalityIntervals.ONE, invalidLecturerCount), teacher) | ||
51 | .reference(enrolledStudents, course, | ||
52 | ConstrainedMultiplicity.of(CardinalityIntervals.SOME, invalidStudentCount), student) | ||
53 | .build(); | ||
54 | |||
55 | var store = ModelStore.builder() | ||
56 | .with(ViatraModelQueryAdapter.builder()) | ||
57 | .with(ReasoningAdapter.builder()) | ||
58 | .with(new MultiObjectTranslator()) | ||
59 | .with(new MetamodelTranslator(metamodel)) | ||
60 | .build(); | ||
61 | |||
62 | var seed = ModelSeed.builder(5) | ||
63 | .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder | ||
64 | .reducedValue(CardinalityIntervals.ONE) | ||
65 | .put(Tuple.of(1), CardinalityIntervals.SET) | ||
66 | .put(Tuple.of(4), CardinalityIntervals.SET)) | ||
67 | .seed(ContainmentHierarchyTranslator.CONTAINED_SYMBOL, builder -> builder | ||
68 | .reducedValue(TruthValue.UNKNOWN)) | ||
69 | .seed(ContainmentHierarchyTranslator.CONTAINS_SYMBOL, builder -> builder | ||
70 | .reducedValue(TruthValue.UNKNOWN)) | ||
71 | .seed(person, builder -> builder.reducedValue(TruthValue.UNKNOWN)) | ||
72 | .seed(student, builder -> builder.reducedValue(TruthValue.UNKNOWN)) | ||
73 | .seed(teacher, builder -> builder.reducedValue(TruthValue.UNKNOWN)) | ||
74 | .seed(university, builder -> builder | ||
75 | .reducedValue(TruthValue.UNKNOWN) | ||
76 | .put(Tuple.of(0), TruthValue.TRUE)) | ||
77 | .seed(course, builder -> builder | ||
78 | .reducedValue(TruthValue.UNKNOWN) | ||
79 | .put(Tuple.of(2), TruthValue.TRUE)) | ||
80 | .seed(courses, builder -> builder.reducedValue(TruthValue.UNKNOWN)) | ||
81 | .seed(location, builder -> builder | ||
82 | .reducedValue(TruthValue.UNKNOWN) | ||
83 | .put(Tuple.of(1, 0), TruthValue.TRUE)) | ||
84 | .seed(lecturer, builder -> builder | ||
85 | .reducedValue(TruthValue.FALSE) | ||
86 | .put(Tuple.of(1, 3), TruthValue.TRUE)) | ||
87 | .seed(enrolledStudents, builder -> builder.reducedValue(TruthValue.UNKNOWN)) | ||
88 | .build(); | ||
89 | |||
90 | var model = store.getAdapter(ReasoningStoreAdapter.class).createInitialModel(seed); | ||
91 | var reasoningAdapter = model.getAdapter(ReasoningAdapter.class); | ||
92 | |||
93 | var coursesInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.PARTIAL, courses); | ||
94 | assertThat(coursesInterpretation.get(Tuple.of(0, 1)), is(TruthValue.TRUE)); | ||
95 | assertThat(coursesInterpretation.get(Tuple.of(0, 2)), is(TruthValue.UNKNOWN)); | ||
96 | assertThat(coursesInterpretation.get(Tuple.of(0, 3)), is(TruthValue.FALSE)); | ||
97 | |||
98 | var invalidLecturerCountInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.PARTIAL, | ||
99 | invalidLecturerCount); | ||
100 | assertThat(invalidLecturerCountInterpretation.get(Tuple.of(1)), is(TruthValue.FALSE)); | ||
101 | assertThat(invalidLecturerCountInterpretation.get(Tuple.of(2)), is(TruthValue.ERROR)); | ||
102 | |||
103 | var enrolledStudentsInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.PARTIAL, | ||
104 | enrolledStudents); | ||
105 | assertThat(enrolledStudentsInterpretation.get(Tuple.of(1, 3)), is(TruthValue.FALSE)); | ||
106 | assertThat(enrolledStudentsInterpretation.get(Tuple.of(1, 4)), is(TruthValue.UNKNOWN)); | ||
107 | } | ||
108 | } | ||
diff --git a/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/multiobject/CandidateCountTest.java b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/multiobject/CandidateCountTest.java new file mode 100644 index 00000000..28391ec7 --- /dev/null +++ b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/multiobject/CandidateCountTest.java | |||
@@ -0,0 +1,321 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.multiobject; | ||
7 | |||
8 | import org.junit.jupiter.api.Test; | ||
9 | import tools.refinery.store.model.ModelStore; | ||
10 | import tools.refinery.store.query.ModelQueryAdapter; | ||
11 | import tools.refinery.store.query.dnf.Query; | ||
12 | import tools.refinery.store.query.resultset.ResultSet; | ||
13 | import tools.refinery.store.query.term.Variable; | ||
14 | import tools.refinery.store.query.viatra.ViatraModelQueryAdapter; | ||
15 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
16 | import tools.refinery.store.reasoning.ReasoningStoreAdapter; | ||
17 | import tools.refinery.store.reasoning.literal.CountCandidateLowerBoundLiteral; | ||
18 | import tools.refinery.store.reasoning.literal.CountCandidateUpperBoundLiteral; | ||
19 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
20 | import tools.refinery.store.reasoning.seed.ModelSeed; | ||
21 | import tools.refinery.store.reasoning.translator.PartialRelationTranslator; | ||
22 | import tools.refinery.store.representation.Symbol; | ||
23 | import tools.refinery.store.representation.TruthValue; | ||
24 | import tools.refinery.store.representation.cardinality.CardinalityIntervals; | ||
25 | import tools.refinery.store.tuple.Tuple; | ||
26 | |||
27 | import java.util.List; | ||
28 | |||
29 | import static org.hamcrest.MatcherAssert.assertThat; | ||
30 | import static org.hamcrest.Matchers.is; | ||
31 | import static tools.refinery.store.query.literal.Literals.not; | ||
32 | import static tools.refinery.store.reasoning.literal.PartialLiterals.must; | ||
33 | |||
34 | class CandidateCountTest { | ||
35 | private static final PartialRelation person = new PartialRelation("Person", 1); | ||
36 | private static final PartialRelation friend = new PartialRelation("friend", 2); | ||
37 | |||
38 | @Test | ||
39 | void lowerBoundZeroTest() { | ||
40 | var query = Query.of("LowerBound", Integer.class, (builder, p1, p2, output) -> builder.clause( | ||
41 | must(person.call(p1)), | ||
42 | must(person.call(p2)), | ||
43 | new CountCandidateLowerBoundLiteral(output, friend, List.of(p1, p2)) | ||
44 | )); | ||
45 | |||
46 | var modelSeed = ModelSeed.builder(2) | ||
47 | .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder | ||
48 | .put(Tuple.of(0), CardinalityIntervals.atLeast(3)) | ||
49 | .put(Tuple.of(1), CardinalityIntervals.atMost(7))) | ||
50 | .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) | ||
51 | .seed(friend, builder -> builder | ||
52 | .put(Tuple.of(0, 1), TruthValue.TRUE) | ||
53 | .put(Tuple.of(1, 0), TruthValue.UNKNOWN) | ||
54 | .put(Tuple.of(1, 1), TruthValue.ERROR)) | ||
55 | .build(); | ||
56 | |||
57 | var resultSet = getResultSet(query, modelSeed); | ||
58 | assertThat(resultSet.get(Tuple.of(0, 0)), is(0)); | ||
59 | assertThat(resultSet.get(Tuple.of(0, 1)), is(1)); | ||
60 | assertThat(resultSet.get(Tuple.of(1, 0)), is(0)); | ||
61 | assertThat(resultSet.get(Tuple.of(1, 1)), is(1)); | ||
62 | } | ||
63 | |||
64 | @Test | ||
65 | void upperBoundZeroTest() { | ||
66 | var query = Query.of("UpperBound", Integer.class, (builder, p1, p2, output) -> builder.clause( | ||
67 | must(person.call(p1)), | ||
68 | must(person.call(p2)), | ||
69 | new CountCandidateUpperBoundLiteral(output, friend, List.of(p1, p2)) | ||
70 | )); | ||
71 | |||
72 | var modelSeed = ModelSeed.builder(2) | ||
73 | .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder | ||
74 | .put(Tuple.of(0), CardinalityIntervals.atLeast(3)) | ||
75 | .put(Tuple.of(1), CardinalityIntervals.atMost(7))) | ||
76 | .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) | ||
77 | .seed(friend, builder -> builder | ||
78 | .put(Tuple.of(0, 1), TruthValue.TRUE) | ||
79 | .put(Tuple.of(1, 0), TruthValue.UNKNOWN) | ||
80 | .put(Tuple.of(1, 1), TruthValue.ERROR)) | ||
81 | .build(); | ||
82 | |||
83 | var resultSet = getResultSet(query, modelSeed); | ||
84 | assertThat(resultSet.get(Tuple.of(0, 0)), is(0)); | ||
85 | assertThat(resultSet.get(Tuple.of(0, 1)), is(1)); | ||
86 | assertThat(resultSet.get(Tuple.of(1, 0)), is(0)); | ||
87 | assertThat(resultSet.get(Tuple.of(1, 1)), is(1)); | ||
88 | } | ||
89 | |||
90 | @Test | ||
91 | void lowerBoundOneTest() { | ||
92 | var query = Query.of("LowerBound", Integer.class, (builder, p1, output) -> builder.clause( | ||
93 | must(person.call(p1)), | ||
94 | new CountCandidateLowerBoundLiteral(output, friend, List.of(p1, Variable.of())) | ||
95 | )); | ||
96 | |||
97 | var modelSeed = ModelSeed.builder(4) | ||
98 | .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder | ||
99 | .reducedValue(CardinalityIntervals.ONE) | ||
100 | .put(Tuple.of(1), CardinalityIntervals.atLeast(3)) | ||
101 | .put(Tuple.of(2), CardinalityIntervals.atMost(7))) | ||
102 | .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) | ||
103 | .seed(friend, builder -> builder | ||
104 | .put(Tuple.of(0, 1), TruthValue.TRUE) | ||
105 | .put(Tuple.of(0, 2), TruthValue.TRUE) | ||
106 | .put(Tuple.of(0, 3), TruthValue.TRUE) | ||
107 | .put(Tuple.of(1, 0), TruthValue.TRUE) | ||
108 | .put(Tuple.of(1, 2), TruthValue.UNKNOWN) | ||
109 | .put(Tuple.of(1, 3), TruthValue.UNKNOWN) | ||
110 | .put(Tuple.of(2, 0), TruthValue.TRUE) | ||
111 | .put(Tuple.of(2, 1), TruthValue.ERROR)) | ||
112 | .build(); | ||
113 | |||
114 | var resultSet = getResultSet(query, modelSeed); | ||
115 | assertThat(resultSet.get(Tuple.of(0)), is(2)); | ||
116 | assertThat(resultSet.get(Tuple.of(1)), is(1)); | ||
117 | assertThat(resultSet.get(Tuple.of(2)), is(2)); | ||
118 | assertThat(resultSet.get(Tuple.of(3)), is(0)); | ||
119 | } | ||
120 | |||
121 | @Test | ||
122 | void upperBoundOneTest() { | ||
123 | var query = Query.of("UpperBound", Integer.class, (builder, p1, output) -> builder.clause( | ||
124 | must(person.call(p1)), | ||
125 | new CountCandidateUpperBoundLiteral(output, friend, List.of(p1, Variable.of())) | ||
126 | )); | ||
127 | |||
128 | var modelSeed = ModelSeed.builder(4) | ||
129 | .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder | ||
130 | .reducedValue(CardinalityIntervals.ONE) | ||
131 | .put(Tuple.of(1), CardinalityIntervals.atLeast(3)) | ||
132 | .put(Tuple.of(2), CardinalityIntervals.atMost(7))) | ||
133 | .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) | ||
134 | .seed(friend, builder -> builder | ||
135 | .put(Tuple.of(0, 1), TruthValue.TRUE) | ||
136 | .put(Tuple.of(0, 2), TruthValue.TRUE) | ||
137 | .put(Tuple.of(0, 3), TruthValue.TRUE) | ||
138 | .put(Tuple.of(1, 0), TruthValue.TRUE) | ||
139 | .put(Tuple.of(1, 2), TruthValue.UNKNOWN) | ||
140 | .put(Tuple.of(1, 3), TruthValue.UNKNOWN) | ||
141 | .put(Tuple.of(2, 0), TruthValue.TRUE) | ||
142 | .put(Tuple.of(2, 1), TruthValue.ERROR)) | ||
143 | .build(); | ||
144 | |||
145 | var resultSet = getResultSet(query, modelSeed); | ||
146 | assertThat(resultSet.get(Tuple.of(0)), is(2)); | ||
147 | assertThat(resultSet.get(Tuple.of(1)), is(1)); | ||
148 | assertThat(resultSet.get(Tuple.of(2)), is(2)); | ||
149 | assertThat(resultSet.get(Tuple.of(3)), is(0)); | ||
150 | } | ||
151 | |||
152 | @Test | ||
153 | void lowerBoundTwoTest() { | ||
154 | var subQuery = Query.of("SubQuery", (builder, p1, p2, p3) -> builder.clause( | ||
155 | friend.call(p1, p2), | ||
156 | friend.call(p1, p3), | ||
157 | friend.call(p2, p3) | ||
158 | )); | ||
159 | var query = Query.of("LowerBound", Integer.class, (builder, p1, output) -> builder.clause( | ||
160 | must(person.call(p1)), | ||
161 | new CountCandidateLowerBoundLiteral(output, subQuery.getDnf(), | ||
162 | List.of(p1, Variable.of(), Variable.of())) | ||
163 | )); | ||
164 | |||
165 | var modelSeed = ModelSeed.builder(4) | ||
166 | .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder | ||
167 | .reducedValue(CardinalityIntervals.ONE) | ||
168 | .put(Tuple.of(0), CardinalityIntervals.between(5, 9)) | ||
169 | .put(Tuple.of(1), CardinalityIntervals.atLeast(3)) | ||
170 | .put(Tuple.of(2), CardinalityIntervals.atMost(7))) | ||
171 | .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) | ||
172 | .seed(friend, builder -> builder | ||
173 | .put(Tuple.of(0, 1), TruthValue.TRUE) | ||
174 | .put(Tuple.of(0, 2), TruthValue.TRUE) | ||
175 | .put(Tuple.of(0, 3), TruthValue.TRUE) | ||
176 | .put(Tuple.of(1, 0), TruthValue.TRUE) | ||
177 | .put(Tuple.of(1, 2), TruthValue.TRUE) | ||
178 | .put(Tuple.of(1, 3), TruthValue.TRUE) | ||
179 | .put(Tuple.of(2, 0), TruthValue.TRUE) | ||
180 | .put(Tuple.of(2, 1), TruthValue.ERROR)) | ||
181 | .build(); | ||
182 | |||
183 | var resultSet = getResultSet(query, modelSeed); | ||
184 | assertThat(resultSet.get(Tuple.of(0)), is(1)); | ||
185 | assertThat(resultSet.get(Tuple.of(1)), is(1)); | ||
186 | assertThat(resultSet.get(Tuple.of(2)), is(2)); | ||
187 | assertThat(resultSet.get(Tuple.of(3)), is(0)); | ||
188 | } | ||
189 | |||
190 | @Test | ||
191 | void upperBoundTwoTest() { | ||
192 | var subQuery = Query.of("SubQuery", (builder, p1, p2, p3) -> builder.clause( | ||
193 | friend.call(p1, p2), | ||
194 | friend.call(p1, p3), | ||
195 | friend.call(p2, p3) | ||
196 | )); | ||
197 | var query = Query.of("UpperBound", Integer.class, (builder, p1, output) -> builder.clause( | ||
198 | must(person.call(p1)), | ||
199 | new CountCandidateUpperBoundLiteral(output, subQuery.getDnf(), | ||
200 | List.of(p1, Variable.of(), Variable.of())) | ||
201 | )); | ||
202 | |||
203 | var modelSeed = ModelSeed.builder(4) | ||
204 | .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder | ||
205 | .reducedValue(CardinalityIntervals.ONE) | ||
206 | .put(Tuple.of(0), CardinalityIntervals.between(5, 9)) | ||
207 | .put(Tuple.of(1), CardinalityIntervals.atLeast(3)) | ||
208 | .put(Tuple.of(2), CardinalityIntervals.atMost(7))) | ||
209 | .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) | ||
210 | .seed(friend, builder -> builder | ||
211 | .put(Tuple.of(0, 1), TruthValue.TRUE) | ||
212 | .put(Tuple.of(0, 2), TruthValue.TRUE) | ||
213 | .put(Tuple.of(0, 3), TruthValue.TRUE) | ||
214 | .put(Tuple.of(1, 0), TruthValue.TRUE) | ||
215 | .put(Tuple.of(1, 2), TruthValue.UNKNOWN) | ||
216 | .put(Tuple.of(1, 3), TruthValue.UNKNOWN) | ||
217 | .put(Tuple.of(2, 0), TruthValue.TRUE) | ||
218 | .put(Tuple.of(2, 1), TruthValue.ERROR)) | ||
219 | .build(); | ||
220 | |||
221 | var resultSet = getResultSet(query, modelSeed); | ||
222 | assertThat(resultSet.get(Tuple.of(0)), is(0)); | ||
223 | assertThat(resultSet.get(Tuple.of(1)), is(0)); | ||
224 | assertThat(resultSet.get(Tuple.of(2)), is(2)); | ||
225 | assertThat(resultSet.get(Tuple.of(3)), is(0)); | ||
226 | } | ||
227 | |||
228 | @Test | ||
229 | void lowerBoundDiagonalTest() { | ||
230 | var subQuery = Query.of("SubQuery", (builder, p1, p2, p3) -> builder.clause( | ||
231 | friend.call(p1, p2), | ||
232 | friend.call(p1, p3), | ||
233 | not(friend.call(p2, p3)) | ||
234 | )); | ||
235 | var query = Query.of("LowerBound", Integer.class, (builder, p1, output) -> builder.clause(v1 -> List.of( | ||
236 | must(person.call(p1)), | ||
237 | new CountCandidateLowerBoundLiteral(output, subQuery.getDnf(), List.of(p1, v1, v1)) | ||
238 | ))); | ||
239 | |||
240 | var modelSeed = ModelSeed.builder(4) | ||
241 | .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder | ||
242 | .reducedValue(CardinalityIntervals.ONE) | ||
243 | .put(Tuple.of(0), CardinalityIntervals.between(5, 9)) | ||
244 | .put(Tuple.of(1), CardinalityIntervals.atLeast(3)) | ||
245 | .put(Tuple.of(2), CardinalityIntervals.atMost(7))) | ||
246 | .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) | ||
247 | .seed(friend, builder -> builder | ||
248 | .put(Tuple.of(0, 1), TruthValue.TRUE) | ||
249 | .put(Tuple.of(0, 2), TruthValue.TRUE) | ||
250 | .put(Tuple.of(0, 3), TruthValue.TRUE) | ||
251 | .put(Tuple.of(1, 0), TruthValue.TRUE) | ||
252 | .put(Tuple.of(1, 2), TruthValue.UNKNOWN) | ||
253 | .put(Tuple.of(1, 3), TruthValue.UNKNOWN) | ||
254 | .put(Tuple.of(2, 0), TruthValue.TRUE) | ||
255 | .put(Tuple.of(2, 1), TruthValue.ERROR)) | ||
256 | .build(); | ||
257 | |||
258 | var resultSet = getResultSet(query, modelSeed); | ||
259 | assertThat(resultSet.get(Tuple.of(0)), is(2)); | ||
260 | assertThat(resultSet.get(Tuple.of(1)), is(1)); | ||
261 | assertThat(resultSet.get(Tuple.of(2)), is(2)); | ||
262 | assertThat(resultSet.get(Tuple.of(3)), is(0)); | ||
263 | } | ||
264 | |||
265 | @Test | ||
266 | void upperBoundDiagonalTest() { | ||
267 | var subQuery = Query.of("SubQuery", (builder, p1, p2, p3) -> builder.clause( | ||
268 | friend.call(p1, p2), | ||
269 | friend.call(p1, p3), | ||
270 | not(friend.call(p2, p3)) | ||
271 | )); | ||
272 | var query = Query.of("UpperBound", Integer.class, (builder, p1, output) -> builder | ||
273 | .clause(v1 -> List.of( | ||
274 | must(person.call(p1)), | ||
275 | new CountCandidateUpperBoundLiteral(output, subQuery.getDnf(), List.of(p1, v1, v1)) | ||
276 | ))); | ||
277 | |||
278 | var modelSeed = ModelSeed.builder(4) | ||
279 | .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder | ||
280 | .reducedValue(CardinalityIntervals.ONE) | ||
281 | .put(Tuple.of(0), CardinalityIntervals.between(5, 9)) | ||
282 | .put(Tuple.of(1), CardinalityIntervals.atLeast(3)) | ||
283 | .put(Tuple.of(2), CardinalityIntervals.atMost(7))) | ||
284 | .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) | ||
285 | .seed(friend, builder -> builder | ||
286 | .put(Tuple.of(0, 1), TruthValue.TRUE) | ||
287 | .put(Tuple.of(0, 2), TruthValue.TRUE) | ||
288 | .put(Tuple.of(0, 3), TruthValue.TRUE) | ||
289 | .put(Tuple.of(1, 0), TruthValue.TRUE) | ||
290 | .put(Tuple.of(1, 2), TruthValue.UNKNOWN) | ||
291 | .put(Tuple.of(1, 3), TruthValue.UNKNOWN) | ||
292 | .put(Tuple.of(2, 0), TruthValue.TRUE) | ||
293 | .put(Tuple.of(2, 1), TruthValue.ERROR)) | ||
294 | .build(); | ||
295 | |||
296 | var resultSet = getResultSet(query, modelSeed); | ||
297 | assertThat(resultSet.get(Tuple.of(0)), is(2)); | ||
298 | assertThat(resultSet.get(Tuple.of(1)), is(1)); | ||
299 | assertThat(resultSet.get(Tuple.of(2)), is(2)); | ||
300 | assertThat(resultSet.get(Tuple.of(3)), is(0)); | ||
301 | } | ||
302 | |||
303 | private static <T> ResultSet<T> getResultSet(Query<T> query, ModelSeed modelSeed) { | ||
304 | var personStorage = Symbol.of("Person", 1, TruthValue.class, TruthValue.FALSE); | ||
305 | var friendStorage = Symbol.of("friend", 2, TruthValue.class, TruthValue.FALSE); | ||
306 | |||
307 | var store = ModelStore.builder() | ||
308 | .with(ViatraModelQueryAdapter.builder() | ||
309 | .query(query)) | ||
310 | .with(ReasoningAdapter.builder()) | ||
311 | .with(new MultiObjectTranslator()) | ||
312 | .with(PartialRelationTranslator.of(person) | ||
313 | .symbol(personStorage)) | ||
314 | .with(PartialRelationTranslator.of(friend) | ||
315 | .symbol(friendStorage)) | ||
316 | .build(); | ||
317 | |||
318 | var model = store.getAdapter(ReasoningStoreAdapter.class).createInitialModel(modelSeed); | ||
319 | return model.getAdapter(ModelQueryAdapter.class).getResultSet(query); | ||
320 | } | ||
321 | } | ||
diff --git a/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/ConcreteCountTest.java b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/multiobject/PartialCountTest.java index 21111d7c..64230cf6 100644 --- a/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/ConcreteCountTest.java +++ b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/multiobject/PartialCountTest.java | |||
@@ -3,7 +3,7 @@ | |||
3 | * | 3 | * |
4 | * SPDX-License-Identifier: EPL-2.0 | 4 | * SPDX-License-Identifier: EPL-2.0 |
5 | */ | 5 | */ |
6 | package tools.refinery.store.reasoning; | 6 | package tools.refinery.store.reasoning.translator.multiobject; |
7 | 7 | ||
8 | import org.junit.jupiter.api.Test; | 8 | import org.junit.jupiter.api.Test; |
9 | import tools.refinery.store.model.ModelStore; | 9 | import tools.refinery.store.model.ModelStore; |
@@ -12,13 +12,13 @@ import tools.refinery.store.query.dnf.Query; | |||
12 | import tools.refinery.store.query.resultset.ResultSet; | 12 | import tools.refinery.store.query.resultset.ResultSet; |
13 | import tools.refinery.store.query.term.Variable; | 13 | import tools.refinery.store.query.term.Variable; |
14 | import tools.refinery.store.query.viatra.ViatraModelQueryAdapter; | 14 | import tools.refinery.store.query.viatra.ViatraModelQueryAdapter; |
15 | import tools.refinery.store.reasoning.literal.Concreteness; | 15 | import tools.refinery.store.reasoning.ReasoningAdapter; |
16 | import tools.refinery.store.reasoning.ReasoningStoreAdapter; | ||
16 | import tools.refinery.store.reasoning.literal.CountLowerBoundLiteral; | 17 | import tools.refinery.store.reasoning.literal.CountLowerBoundLiteral; |
17 | import tools.refinery.store.reasoning.literal.CountUpperBoundLiteral; | 18 | import tools.refinery.store.reasoning.literal.CountUpperBoundLiteral; |
18 | import tools.refinery.store.reasoning.representation.PartialRelation; | 19 | import tools.refinery.store.reasoning.representation.PartialRelation; |
19 | import tools.refinery.store.reasoning.seed.ModelSeed; | 20 | import tools.refinery.store.reasoning.seed.ModelSeed; |
20 | import tools.refinery.store.reasoning.translator.PartialRelationTranslator; | 21 | import tools.refinery.store.reasoning.translator.PartialRelationTranslator; |
21 | import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator; | ||
22 | import tools.refinery.store.representation.Symbol; | 22 | import tools.refinery.store.representation.Symbol; |
23 | import tools.refinery.store.representation.TruthValue; | 23 | import tools.refinery.store.representation.TruthValue; |
24 | import tools.refinery.store.representation.cardinality.CardinalityIntervals; | 24 | import tools.refinery.store.representation.cardinality.CardinalityIntervals; |
@@ -33,7 +33,7 @@ import static org.hamcrest.Matchers.is; | |||
33 | import static tools.refinery.store.query.literal.Literals.not; | 33 | import static tools.refinery.store.query.literal.Literals.not; |
34 | import static tools.refinery.store.reasoning.literal.PartialLiterals.must; | 34 | import static tools.refinery.store.reasoning.literal.PartialLiterals.must; |
35 | 35 | ||
36 | class ConcreteCountTest { | 36 | class PartialCountTest { |
37 | private static final PartialRelation person = new PartialRelation("Person", 1); | 37 | private static final PartialRelation person = new PartialRelation("Person", 1); |
38 | private static final PartialRelation friend = new PartialRelation("friend", 2); | 38 | private static final PartialRelation friend = new PartialRelation("friend", 2); |
39 | 39 | ||
@@ -42,7 +42,7 @@ class ConcreteCountTest { | |||
42 | var query = Query.of("LowerBound", Integer.class, (builder, p1, p2, output) -> builder.clause( | 42 | var query = Query.of("LowerBound", Integer.class, (builder, p1, p2, output) -> builder.clause( |
43 | must(person.call(p1)), | 43 | must(person.call(p1)), |
44 | must(person.call(p2)), | 44 | must(person.call(p2)), |
45 | new CountLowerBoundLiteral(output, Concreteness.PARTIAL, friend, List.of(p1, p2)) | 45 | new CountLowerBoundLiteral(output, friend, List.of(p1, p2)) |
46 | )); | 46 | )); |
47 | 47 | ||
48 | var modelSeed = ModelSeed.builder(2) | 48 | var modelSeed = ModelSeed.builder(2) |
@@ -68,7 +68,7 @@ class ConcreteCountTest { | |||
68 | var query = Query.of("UpperBound", UpperCardinality.class, (builder, p1, p2, output) -> builder.clause( | 68 | var query = Query.of("UpperBound", UpperCardinality.class, (builder, p1, p2, output) -> builder.clause( |
69 | must(person.call(p1)), | 69 | must(person.call(p1)), |
70 | must(person.call(p2)), | 70 | must(person.call(p2)), |
71 | new CountUpperBoundLiteral(output, Concreteness.PARTIAL, friend, List.of(p1, p2)) | 71 | new CountUpperBoundLiteral(output, friend, List.of(p1, p2)) |
72 | )); | 72 | )); |
73 | 73 | ||
74 | var modelSeed = ModelSeed.builder(2) | 74 | var modelSeed = ModelSeed.builder(2) |
@@ -93,7 +93,7 @@ class ConcreteCountTest { | |||
93 | void lowerBoundOneTest() { | 93 | void lowerBoundOneTest() { |
94 | var query = Query.of("LowerBound", Integer.class, (builder, p1, output) -> builder.clause( | 94 | var query = Query.of("LowerBound", Integer.class, (builder, p1, output) -> builder.clause( |
95 | must(person.call(p1)), | 95 | must(person.call(p1)), |
96 | new CountLowerBoundLiteral(output, Concreteness.PARTIAL, friend, List.of(p1, Variable.of())) | 96 | new CountLowerBoundLiteral(output, friend, List.of(p1, Variable.of())) |
97 | )); | 97 | )); |
98 | 98 | ||
99 | var modelSeed = ModelSeed.builder(4) | 99 | var modelSeed = ModelSeed.builder(4) |
@@ -124,7 +124,7 @@ class ConcreteCountTest { | |||
124 | void upperBoundOneTest() { | 124 | void upperBoundOneTest() { |
125 | var query = Query.of("UpperBound", UpperCardinality.class, (builder, p1, output) -> builder.clause( | 125 | var query = Query.of("UpperBound", UpperCardinality.class, (builder, p1, output) -> builder.clause( |
126 | must(person.call(p1)), | 126 | must(person.call(p1)), |
127 | new CountUpperBoundLiteral(output, Concreteness.PARTIAL, friend, List.of(p1, Variable.of())) | 127 | new CountUpperBoundLiteral(output, friend, List.of(p1, Variable.of())) |
128 | )); | 128 | )); |
129 | 129 | ||
130 | var modelSeed = ModelSeed.builder(4) | 130 | var modelSeed = ModelSeed.builder(4) |
@@ -160,8 +160,7 @@ class ConcreteCountTest { | |||
160 | )); | 160 | )); |
161 | var query = Query.of("LowerBound", Integer.class, (builder, p1, output) -> builder.clause( | 161 | var query = Query.of("LowerBound", Integer.class, (builder, p1, output) -> builder.clause( |
162 | must(person.call(p1)), | 162 | must(person.call(p1)), |
163 | new CountLowerBoundLiteral(output, Concreteness.PARTIAL, subQuery.getDnf(), | 163 | new CountLowerBoundLiteral(output, subQuery.getDnf(), List.of(p1, Variable.of(), Variable.of())) |
164 | List.of(p1, Variable.of(), Variable.of())) | ||
165 | )); | 164 | )); |
166 | 165 | ||
167 | var modelSeed = ModelSeed.builder(4) | 166 | var modelSeed = ModelSeed.builder(4) |
@@ -198,8 +197,7 @@ class ConcreteCountTest { | |||
198 | )); | 197 | )); |
199 | var query = Query.of("UpperBound", UpperCardinality.class, (builder, p1, output) -> builder.clause( | 198 | var query = Query.of("UpperBound", UpperCardinality.class, (builder, p1, output) -> builder.clause( |
200 | must(person.call(p1)), | 199 | must(person.call(p1)), |
201 | new CountUpperBoundLiteral(output, Concreteness.PARTIAL, subQuery.getDnf(), | 200 | new CountUpperBoundLiteral(output, subQuery.getDnf(), List.of(p1, Variable.of(), Variable.of())) |
202 | List.of(p1, Variable.of(), Variable.of())) | ||
203 | )); | 201 | )); |
204 | 202 | ||
205 | var modelSeed = ModelSeed.builder(4) | 203 | var modelSeed = ModelSeed.builder(4) |
@@ -236,7 +234,7 @@ class ConcreteCountTest { | |||
236 | )); | 234 | )); |
237 | var query = Query.of("LowerBound", Integer.class, (builder, p1, output) -> builder.clause(v1 -> List.of( | 235 | var query = Query.of("LowerBound", Integer.class, (builder, p1, output) -> builder.clause(v1 -> List.of( |
238 | must(person.call(p1)), | 236 | must(person.call(p1)), |
239 | new CountLowerBoundLiteral(output, Concreteness.PARTIAL, subQuery.getDnf(), List.of(p1, v1, v1)) | 237 | new CountLowerBoundLiteral(output, subQuery.getDnf(), List.of(p1, v1, v1)) |
240 | ))); | 238 | ))); |
241 | 239 | ||
242 | var modelSeed = ModelSeed.builder(4) | 240 | var modelSeed = ModelSeed.builder(4) |
@@ -274,8 +272,7 @@ class ConcreteCountTest { | |||
274 | var query = Query.of("UpperBound", UpperCardinality.class, (builder, p1, output) -> builder | 272 | var query = Query.of("UpperBound", UpperCardinality.class, (builder, p1, output) -> builder |
275 | .clause(v1 -> List.of( | 273 | .clause(v1 -> List.of( |
276 | must(person.call(p1)), | 274 | must(person.call(p1)), |
277 | new CountUpperBoundLiteral(output, Concreteness.PARTIAL, subQuery.getDnf(), | 275 | new CountUpperBoundLiteral(output, subQuery.getDnf(), List.of(p1, v1, v1)) |
278 | List.of(p1, v1, v1)) | ||
279 | ))); | 276 | ))); |
280 | 277 | ||
281 | var modelSeed = ModelSeed.builder(4) | 278 | var modelSeed = ModelSeed.builder(4) |