diff options
author | 2023-07-25 16:06:36 +0200 | |
---|---|---|
committer | 2023-07-25 16:06:36 +0200 | |
commit | 6a25ba145844c79d3507f8eabdbed854be2b8097 (patch) | |
tree | 0ea9d4c7a9b5b94a0d4341eaa25eeb7e4d3f4f56 | |
parent | feat: custom connected component RETE node (diff) | |
download | refinery-6a25ba145844c79d3507f8eabdbed854be2b8097.tar.gz refinery-6a25ba145844c79d3507f8eabdbed854be2b8097.tar.zst refinery-6a25ba145844c79d3507f8eabdbed854be2b8097.zip |
feat: concrete count in partial models
19 files changed, 807 insertions, 98 deletions
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AbstractCountLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AbstractCountLiteral.java new file mode 100644 index 00000000..75f4bd49 --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AbstractCountLiteral.java | |||
@@ -0,0 +1,106 @@ | |||
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.query.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.term.ConstantTerm; | ||
12 | import tools.refinery.store.query.term.DataVariable; | ||
13 | import tools.refinery.store.query.term.Variable; | ||
14 | |||
15 | import java.util.List; | ||
16 | import java.util.Objects; | ||
17 | import java.util.Set; | ||
18 | |||
19 | // {@link Object#equals(Object)} is implemented by {@link AbstractLiteral}. | ||
20 | @SuppressWarnings("squid:S2160") | ||
21 | public abstract class AbstractCountLiteral<T> extends AbstractCallLiteral { | ||
22 | private final Class<T> resultType; | ||
23 | private final DataVariable<T> resultVariable; | ||
24 | |||
25 | protected AbstractCountLiteral(Class<T> resultType, DataVariable<T> resultVariable, Constraint target, | ||
26 | List<Variable> arguments) { | ||
27 | super(target, arguments); | ||
28 | if (!resultVariable.getType().equals(resultType)) { | ||
29 | throw new IllegalArgumentException("Count result variable %s must be of type %s, got %s instead".formatted( | ||
30 | resultVariable, resultType, resultVariable.getType().getName())); | ||
31 | } | ||
32 | if (arguments.contains(resultVariable)) { | ||
33 | throw new IllegalArgumentException("Count result variable %s must not appear in the argument list" | ||
34 | .formatted(resultVariable)); | ||
35 | } | ||
36 | this.resultType = resultType; | ||
37 | this.resultVariable = resultVariable; | ||
38 | } | ||
39 | |||
40 | public Class<T> getResultType() { | ||
41 | return resultType; | ||
42 | } | ||
43 | |||
44 | public DataVariable<T> getResultVariable() { | ||
45 | return resultVariable; | ||
46 | } | ||
47 | |||
48 | @Override | ||
49 | public Set<Variable> getOutputVariables() { | ||
50 | return Set.of(resultVariable); | ||
51 | } | ||
52 | |||
53 | protected abstract T zero(); | ||
54 | |||
55 | protected abstract T one(); | ||
56 | |||
57 | @Override | ||
58 | public Literal reduce() { | ||
59 | var reduction = getTarget().getReduction(); | ||
60 | return switch (reduction) { | ||
61 | case ALWAYS_FALSE -> getResultVariable().assign(new ConstantTerm<>(resultType, zero())); | ||
62 | // The only way a constant {@code true} predicate can be called in a negative position is to have all of | ||
63 | // its arguments bound as input variables. Thus, there will only be a single match. | ||
64 | case ALWAYS_TRUE -> getResultVariable().assign(new ConstantTerm<>(resultType, one())); | ||
65 | case NOT_REDUCIBLE -> this; | ||
66 | }; | ||
67 | } | ||
68 | |||
69 | @Override | ||
70 | public boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other) { | ||
71 | if (!super.equalsWithSubstitution(helper, other)) { | ||
72 | return false; | ||
73 | } | ||
74 | var otherCountLiteral = (AbstractCountLiteral<?>) other; | ||
75 | return Objects.equals(resultType, otherCountLiteral.resultType) && | ||
76 | helper.variableEqual(resultVariable, otherCountLiteral.resultVariable); | ||
77 | } | ||
78 | |||
79 | @Override | ||
80 | public int hashCodeWithSubstitution(LiteralHashCodeHelper helper) { | ||
81 | return Objects.hash(super.hashCodeWithSubstitution(helper), resultType, | ||
82 | helper.getVariableHashCode(resultVariable)); | ||
83 | } | ||
84 | |||
85 | protected abstract String operatorName(); | ||
86 | |||
87 | @Override | ||
88 | public String toString() { | ||
89 | var builder = new StringBuilder(); | ||
90 | builder.append(resultVariable); | ||
91 | builder.append(" is "); | ||
92 | builder.append(operatorName()); | ||
93 | builder.append(' '); | ||
94 | builder.append(getTarget().toReferenceString()); | ||
95 | builder.append('('); | ||
96 | var argumentIterator = getArguments().iterator(); | ||
97 | if (argumentIterator.hasNext()) { | ||
98 | builder.append(argumentIterator.next()); | ||
99 | while (argumentIterator.hasNext()) { | ||
100 | builder.append(", ").append(argumentIterator.next()); | ||
101 | } | ||
102 | } | ||
103 | builder.append(')'); | ||
104 | return builder.toString(); | ||
105 | } | ||
106 | } | ||
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 77b77389..e5f6ac0c 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 | |||
@@ -6,95 +6,40 @@ | |||
6 | package tools.refinery.store.query.literal; | 6 | package tools.refinery.store.query.literal; |
7 | 7 | ||
8 | import tools.refinery.store.query.Constraint; | 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.substitution.Substitution; | 9 | import tools.refinery.store.query.substitution.Substitution; |
12 | import tools.refinery.store.query.term.DataVariable; | 10 | import tools.refinery.store.query.term.DataVariable; |
13 | import tools.refinery.store.query.term.Variable; | 11 | import tools.refinery.store.query.term.Variable; |
14 | import tools.refinery.store.query.term.int_.IntTerms; | ||
15 | 12 | ||
16 | import java.util.List; | 13 | import java.util.List; |
17 | import java.util.Objects; | ||
18 | import java.util.Set; | ||
19 | |||
20 | // {@link Object#equals(Object)} is implemented by {@link AbstractLiteral}. | ||
21 | @SuppressWarnings("squid:S2160") | ||
22 | public class CountLiteral extends AbstractCallLiteral { | ||
23 | private final DataVariable<Integer> resultVariable; | ||
24 | 14 | ||
15 | public class CountLiteral extends AbstractCountLiteral<Integer> { | ||
25 | public CountLiteral(DataVariable<Integer> resultVariable, Constraint target, List<Variable> arguments) { | 16 | public CountLiteral(DataVariable<Integer> resultVariable, Constraint target, List<Variable> arguments) { |
26 | super(target, arguments); | 17 | super(Integer.class, resultVariable, target, arguments); |
27 | if (!resultVariable.getType().equals(Integer.class)) { | ||
28 | throw new IllegalArgumentException("Count result variable %s must be of type %s, got %s instead".formatted( | ||
29 | resultVariable, Integer.class.getName(), resultVariable.getType().getName())); | ||
30 | } | ||
31 | if (arguments.contains(resultVariable)) { | ||
32 | throw new IllegalArgumentException("Count result variable %s must not appear in the argument list" | ||
33 | .formatted(resultVariable)); | ||
34 | } | ||
35 | this.resultVariable = resultVariable; | ||
36 | } | ||
37 | |||
38 | public DataVariable<Integer> getResultVariable() { | ||
39 | return resultVariable; | ||
40 | } | 18 | } |
41 | 19 | ||
42 | @Override | 20 | @Override |
43 | public Set<Variable> getOutputVariables() { | 21 | protected Integer zero() { |
44 | return Set.of(resultVariable); | 22 | return 0; |
45 | } | 23 | } |
46 | 24 | ||
47 | @Override | 25 | @Override |
48 | public Literal reduce() { | 26 | protected Integer one() { |
49 | var reduction = getTarget().getReduction(); | 27 | return 1; |
50 | return switch (reduction) { | ||
51 | case ALWAYS_FALSE -> getResultVariable().assign(IntTerms.constant(0)); | ||
52 | // The only way a constant {@code true} predicate can be called in a negative position is to have all of | ||
53 | // its arguments bound as input variables. Thus, there will only be a single match. | ||
54 | case ALWAYS_TRUE -> getResultVariable().assign(IntTerms.constant(1)); | ||
55 | case NOT_REDUCIBLE -> this; | ||
56 | }; | ||
57 | } | 28 | } |
58 | 29 | ||
59 | @Override | 30 | @Override |
60 | protected Literal doSubstitute(Substitution substitution, List<Variable> substitutedArguments) { | 31 | protected Literal doSubstitute(Substitution substitution, List<Variable> substitutedArguments) { |
61 | return new CountLiteral(substitution.getTypeSafeSubstitute(resultVariable), getTarget(), substitutedArguments); | 32 | return new CountLiteral(substitution.getTypeSafeSubstitute(getResultVariable()), getTarget(), |
33 | substitutedArguments); | ||
62 | } | 34 | } |
63 | 35 | ||
64 | @Override | 36 | @Override |
65 | protected AbstractCallLiteral internalWithTarget(Constraint newTarget) { | 37 | protected AbstractCallLiteral internalWithTarget(Constraint newTarget) { |
66 | return new CountLiteral(resultVariable, newTarget, getArguments()); | 38 | return new CountLiteral(getResultVariable(), newTarget, getArguments()); |
67 | } | ||
68 | |||
69 | @Override | ||
70 | public boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other) { | ||
71 | if (!super.equalsWithSubstitution(helper, other)) { | ||
72 | return false; | ||
73 | } | ||
74 | var otherCountLiteral = (CountLiteral) other; | ||
75 | return helper.variableEqual(resultVariable, otherCountLiteral.resultVariable); | ||
76 | } | ||
77 | |||
78 | @Override | ||
79 | public int hashCodeWithSubstitution(LiteralHashCodeHelper helper) { | ||
80 | return Objects.hash(super.hashCodeWithSubstitution(helper), helper.getVariableHashCode(resultVariable)); | ||
81 | } | 39 | } |
82 | 40 | ||
83 | @Override | 41 | @Override |
84 | public String toString() { | 42 | protected String operatorName() { |
85 | var builder = new StringBuilder(); | 43 | return "count"; |
86 | builder.append(resultVariable); | ||
87 | builder.append(" is count "); | ||
88 | builder.append(getTarget().toReferenceString()); | ||
89 | builder.append("("); | ||
90 | var argumentIterator = getArguments().iterator(); | ||
91 | if (argumentIterator.hasNext()) { | ||
92 | builder.append(argumentIterator.next()); | ||
93 | while (argumentIterator.hasNext()) { | ||
94 | builder.append(", ").append(argumentIterator.next()); | ||
95 | } | ||
96 | } | ||
97 | builder.append(")"); | ||
98 | return builder.toString(); | ||
99 | } | 44 | } |
100 | } | 45 | } |
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/uppercardinality/UpperCardinalitySumAggregator.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/uppercardinality/UpperCardinalitySumAggregator.java index 5bbd3081..d31f00a2 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/uppercardinality/UpperCardinalitySumAggregator.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/uppercardinality/UpperCardinalitySumAggregator.java | |||
@@ -70,7 +70,7 @@ public class UpperCardinalitySumAggregator implements StatefulAggregator<UpperCa | |||
70 | 70 | ||
71 | @Override | 71 | @Override |
72 | public UpperCardinality getResult() { | 72 | public UpperCardinality getResult() { |
73 | return countUnbounded > 0 ? UpperCardinalities.UNBOUNDED : UpperCardinalities.valueOf(sumFiniteUpperBounds); | 73 | return countUnbounded > 0 ? UpperCardinalities.UNBOUNDED : UpperCardinalities.atMost(sumFiniteUpperBounds); |
74 | } | 74 | } |
75 | 75 | ||
76 | @Override | 76 | @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 bc379c64..c560162e 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 | |||
@@ -5,17 +5,25 @@ | |||
5 | */ | 5 | */ |
6 | package tools.refinery.store.reasoning.internal; | 6 | package tools.refinery.store.reasoning.internal; |
7 | 7 | ||
8 | import tools.refinery.store.query.Constraint; | ||
8 | import tools.refinery.store.query.dnf.Dnf; | 9 | import tools.refinery.store.query.dnf.Dnf; |
9 | import tools.refinery.store.query.dnf.DnfClause; | 10 | import tools.refinery.store.query.dnf.DnfClause; |
10 | import tools.refinery.store.query.literal.AbstractCallLiteral; | 11 | import tools.refinery.store.query.literal.AbstractCallLiteral; |
12 | import tools.refinery.store.query.literal.CallPolarity; | ||
11 | import tools.refinery.store.query.literal.Literal; | 13 | import tools.refinery.store.query.literal.Literal; |
14 | import tools.refinery.store.query.term.Aggregator; | ||
15 | import tools.refinery.store.query.term.ConstantTerm; | ||
16 | import tools.refinery.store.query.term.Term; | ||
12 | import tools.refinery.store.query.term.Variable; | 17 | import tools.refinery.store.query.term.Variable; |
13 | import tools.refinery.store.reasoning.literal.Concreteness; | 18 | import tools.refinery.store.query.term.int_.IntTerms; |
14 | import tools.refinery.store.reasoning.literal.ModalConstraint; | 19 | import tools.refinery.store.query.term.uppercardinality.UpperCardinalityTerms; |
15 | import tools.refinery.store.reasoning.literal.Modality; | 20 | import tools.refinery.store.reasoning.literal.*; |
16 | import tools.refinery.store.reasoning.representation.PartialRelation; | 21 | import tools.refinery.store.reasoning.representation.PartialRelation; |
22 | import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator; | ||
23 | import tools.refinery.store.representation.cardinality.UpperCardinalities; | ||
17 | 24 | ||
18 | import java.util.*; | 25 | import java.util.*; |
26 | import java.util.function.BinaryOperator; | ||
19 | 27 | ||
20 | class PartialClauseRewriter { | 28 | class PartialClauseRewriter { |
21 | private final PartialQueryRewriter rewriter; | 29 | private final PartialQueryRewriter rewriter; |
@@ -42,6 +50,14 @@ class PartialClauseRewriter { | |||
42 | markAsDone(literal); | 50 | markAsDone(literal); |
43 | return; | 51 | return; |
44 | } | 52 | } |
53 | if (callLiteral instanceof CountLowerBoundLiteral countLowerBoundLiteral) { | ||
54 | rewriteCountLowerBound(countLowerBoundLiteral); | ||
55 | return; | ||
56 | } | ||
57 | if (callLiteral instanceof CountUpperBoundLiteral countUpperBoundLiteral) { | ||
58 | rewriteCountUpperBound(countUpperBoundLiteral); | ||
59 | return; | ||
60 | } | ||
45 | var target = callLiteral.getTarget(); | 61 | var target = callLiteral.getTarget(); |
46 | if (target instanceof Dnf dnf) { | 62 | if (target instanceof Dnf dnf) { |
47 | rewriteRecursively(callLiteral, dnf); | 63 | rewriteRecursively(callLiteral, dnf); |
@@ -61,6 +77,75 @@ class PartialClauseRewriter { | |||
61 | } | 77 | } |
62 | } | 78 | } |
63 | 79 | ||
80 | private void rewriteCountLowerBound(CountLowerBoundLiteral literal) { | ||
81 | rewriteCount(literal, "lower", Modality.MUST, MultiObjectTranslator.LOWER_CARDINALITY_VIEW, 1, IntTerms::mul, | ||
82 | IntTerms.INT_SUM); | ||
83 | } | ||
84 | |||
85 | private void rewriteCountUpperBound(CountUpperBoundLiteral literal) { | ||
86 | rewriteCount(literal, "upper", Modality.MAY, MultiObjectTranslator.UPPER_CARDINALITY_VIEW, | ||
87 | UpperCardinalities.ONE, UpperCardinalityTerms::mul, UpperCardinalityTerms.UPPER_CARDINALITY_SUM); | ||
88 | } | ||
89 | |||
90 | private <T> void rewriteCount(ConcreteCountLiteral<T> literal, String name, Modality modality, Constraint view, | ||
91 | T one, BinaryOperator<Term<T>> mul, Aggregator<T, T> sum) { | ||
92 | var type = literal.getResultType(); | ||
93 | var target = literal.getTarget(); | ||
94 | var concreteness = literal.getConcreteness(); | ||
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); | ||
119 | |||
120 | var literals = new ArrayList<Literal>(); | ||
121 | literals.add(new ModalConstraint(modality, literal.getConcreteness(), target) | ||
122 | .call(CallPolarity.POSITIVE, rewrittenArguments)); | ||
123 | switch (variablesToCount.size()) { | ||
124 | case 0 -> literals.add(outputVariable.assign(new ConstantTerm<>(type, one))); | ||
125 | case 1 -> literals.add(view.call(variablesToCount.get(0), | ||
126 | outputVariable)); | ||
127 | default -> { | ||
128 | var firstCount = Variable.of(type); | ||
129 | literals.add(view.call(variablesToCount.get(0), firstCount)); | ||
130 | int length = variablesToCount.size(); | ||
131 | Term<T> accumulator = firstCount; | ||
132 | for (int i = 1; i < length; i++) { | ||
133 | var countVariable = Variable.of(type); | ||
134 | literals.add(view.call(variablesToCount.get(i), countVariable)); | ||
135 | accumulator = mul.apply(accumulator, countVariable); | ||
136 | } | ||
137 | literals.add(outputVariable.assign(accumulator)); | ||
138 | } | ||
139 | } | ||
140 | builder.clause(literals); | ||
141 | |||
142 | var helperQuery = builder.build(); | ||
143 | var aggregationVariable = Variable.of(type); | ||
144 | helperArguments.add(aggregationVariable); | ||
145 | workList.addFirst(literal.getResultVariable().assign(helperQuery.aggregateBy(aggregationVariable, sum, | ||
146 | helperArguments))); | ||
147 | } | ||
148 | |||
64 | private void markAsDone(Literal literal) { | 149 | private void markAsDone(Literal literal) { |
65 | completedLiterals.add(literal); | 150 | completedLiterals.add(literal); |
66 | positiveVariables.addAll(literal.getOutputVariables()); | 151 | positiveVariables.addAll(literal.getOutputVariables()); |
@@ -75,7 +160,7 @@ class PartialClauseRewriter { | |||
75 | private void rewriteRecursively(AbstractCallLiteral callLiteral, Dnf dnf) { | 160 | private void rewriteRecursively(AbstractCallLiteral callLiteral, Dnf dnf) { |
76 | var rewrittenDnf = rewriter.rewrite(dnf); | 161 | var rewrittenDnf = rewriter.rewrite(dnf); |
77 | var rewrittenLiteral = callLiteral.withTarget(rewrittenDnf); | 162 | var rewrittenLiteral = callLiteral.withTarget(rewrittenDnf); |
78 | completedLiterals.add(rewrittenLiteral); | 163 | markAsDone(rewrittenLiteral); |
79 | } | 164 | } |
80 | 165 | ||
81 | private void rewrite(AbstractCallLiteral callLiteral, Modality modality, Concreteness concreteness, | 166 | private void rewrite(AbstractCallLiteral callLiteral, Modality modality, Concreteness concreteness, |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/ClauseLifter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/ClauseLifter.java index 89e948dc..17916c02 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/ClauseLifter.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/ClauseLifter.java | |||
@@ -70,9 +70,9 @@ class ClauseLifter { | |||
70 | literal instanceof AssignLiteral<?> || | 70 | literal instanceof AssignLiteral<?> || |
71 | literal instanceof CheckLiteral) { | 71 | literal instanceof CheckLiteral) { |
72 | return literal; | 72 | return literal; |
73 | } else if (literal instanceof CountLiteral) { | 73 | } else if (literal instanceof AbstractCountLiteral<?>) { |
74 | throw new IllegalArgumentException("Count literal %s cannot be lifted".formatted(literal)); | 74 | throw new IllegalArgumentException("Count literal %s cannot be lifted".formatted(literal)); |
75 | } else if (literal instanceof AggregationLiteral<?,?>) { | 75 | } else if (literal instanceof AggregationLiteral<?, ?>) { |
76 | throw new IllegalArgumentException("Aggregation literal %s cannot be lifted".formatted(literal)); | 76 | throw new IllegalArgumentException("Aggregation literal %s cannot be lifted".formatted(literal)); |
77 | } else if (literal instanceof RepresentativeElectionLiteral) { | 77 | } else if (literal instanceof RepresentativeElectionLiteral) { |
78 | throw new IllegalArgumentException("SCC literal %s cannot be lifted".formatted(literal)); | 78 | throw new IllegalArgumentException("SCC literal %s cannot be lifted".formatted(literal)); |
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 new file mode 100644 index 00000000..91b30964 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ConcreteCountLiteral.java | |||
@@ -0,0 +1,47 @@ | |||
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/CountLowerBoundLiteral.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountLowerBoundLiteral.java new file mode 100644 index 00000000..261088fc --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountLowerBoundLiteral.java | |||
@@ -0,0 +1,48 @@ | |||
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.Literal; | ||
11 | import tools.refinery.store.query.substitution.Substitution; | ||
12 | import tools.refinery.store.query.term.DataVariable; | ||
13 | import tools.refinery.store.query.term.Variable; | ||
14 | |||
15 | import java.util.List; | ||
16 | |||
17 | public class CountLowerBoundLiteral extends ConcreteCountLiteral<Integer> { | ||
18 | public CountLowerBoundLiteral(DataVariable<Integer> resultVariable, Concreteness concreteness, Constraint target, | ||
19 | List<Variable> arguments) { | ||
20 | super(Integer.class, resultVariable, concreteness, target, arguments); | ||
21 | } | ||
22 | |||
23 | @Override | ||
24 | protected Integer zero() { | ||
25 | return 0; | ||
26 | } | ||
27 | |||
28 | @Override | ||
29 | protected Integer one() { | ||
30 | return 1; | ||
31 | } | ||
32 | |||
33 | @Override | ||
34 | protected Literal doSubstitute(Substitution substitution, List<Variable> substitutedArguments) { | ||
35 | return new CountLowerBoundLiteral(substitution.getTypeSafeSubstitute(getResultVariable()), getConcreteness(), | ||
36 | getTarget(), substitutedArguments); | ||
37 | } | ||
38 | |||
39 | @Override | ||
40 | protected AbstractCallLiteral internalWithTarget(Constraint newTarget) { | ||
41 | return new CountLowerBoundLiteral(getResultVariable(), getConcreteness(), newTarget, getArguments()); | ||
42 | } | ||
43 | |||
44 | @Override | ||
45 | protected String operatorName() { | ||
46 | return "@LowerBound(\"%s\") count".formatted(getConcreteness()); | ||
47 | } | ||
48 | } | ||
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 new file mode 100644 index 00000000..960ded69 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountUpperBoundLiteral.java | |||
@@ -0,0 +1,50 @@ | |||
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.Literal; | ||
11 | import tools.refinery.store.query.substitution.Substitution; | ||
12 | import tools.refinery.store.query.term.DataVariable; | ||
13 | import tools.refinery.store.query.term.Variable; | ||
14 | import tools.refinery.store.representation.cardinality.UpperCardinalities; | ||
15 | import tools.refinery.store.representation.cardinality.UpperCardinality; | ||
16 | |||
17 | import java.util.List; | ||
18 | |||
19 | public class CountUpperBoundLiteral extends ConcreteCountLiteral<UpperCardinality> { | ||
20 | public CountUpperBoundLiteral(DataVariable<UpperCardinality> resultVariable, Concreteness concreteness, | ||
21 | Constraint target, List<Variable> arguments) { | ||
22 | super(UpperCardinality.class, resultVariable, concreteness, target, arguments); | ||
23 | } | ||
24 | |||
25 | @Override | ||
26 | protected UpperCardinality zero() { | ||
27 | return UpperCardinalities.ZERO; | ||
28 | } | ||
29 | |||
30 | @Override | ||
31 | protected UpperCardinality one() { | ||
32 | return UpperCardinalities.UNBOUNDED; | ||
33 | } | ||
34 | |||
35 | @Override | ||
36 | protected Literal doSubstitute(Substitution substitution, List<Variable> substitutedArguments) { | ||
37 | return new CountUpperBoundLiteral(substitution.getTypeSafeSubstitute(getResultVariable()), getConcreteness(), | ||
38 | getTarget(), substitutedArguments); | ||
39 | } | ||
40 | |||
41 | @Override | ||
42 | protected AbstractCallLiteral internalWithTarget(Constraint newTarget) { | ||
43 | return new CountUpperBoundLiteral(getResultVariable(), getConcreteness(), newTarget, getArguments()); | ||
44 | } | ||
45 | |||
46 | @Override | ||
47 | protected String operatorName() { | ||
48 | return "@UpperBound(\"%s\") count".formatted(getConcreteness()); | ||
49 | } | ||
50 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/ModelSeed.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/ModelSeed.java index 3641730d..28e6258e 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/ModelSeed.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/ModelSeed.java | |||
@@ -39,6 +39,10 @@ public class ModelSeed { | |||
39 | return typedSeed; | 39 | return typedSeed; |
40 | } | 40 | } |
41 | 41 | ||
42 | public boolean containsSeed(AnyPartialSymbol symbol) { | ||
43 | return seeds.containsKey(symbol); | ||
44 | } | ||
45 | |||
42 | public <A> Cursor<Tuple, A> getCursor(PartialSymbol<A, ?> partialSymbol, A defaultValue) { | 46 | public <A> Cursor<Tuple, A> getCursor(PartialSymbol<A, ?> partialSymbol, A defaultValue) { |
43 | return getSeed(partialSymbol).getCursor(defaultValue, nodeCount); | 47 | return getSeed(partialSymbol).getCursor(defaultValue, nodeCount); |
44 | } | 48 | } |
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 c7bc9fff..393a8769 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 | |||
@@ -11,6 +11,7 @@ import tools.refinery.store.query.literal.AbstractCallLiteral; | |||
11 | import tools.refinery.store.query.literal.CallLiteral; | 11 | import tools.refinery.store.query.literal.CallLiteral; |
12 | import tools.refinery.store.query.literal.Literal; | 12 | import tools.refinery.store.query.literal.Literal; |
13 | import tools.refinery.store.query.term.Variable; | 13 | import tools.refinery.store.query.term.Variable; |
14 | import tools.refinery.store.query.view.AnySymbolView; | ||
14 | import tools.refinery.store.reasoning.interpretation.QueryBasedRelationRewriter; | 15 | import tools.refinery.store.reasoning.interpretation.QueryBasedRelationRewriter; |
15 | import tools.refinery.store.reasoning.literal.Concreteness; | 16 | import tools.refinery.store.reasoning.literal.Concreteness; |
16 | import tools.refinery.store.reasoning.literal.Modality; | 17 | import tools.refinery.store.reasoning.literal.Modality; |
@@ -67,7 +68,7 @@ class EqualsRelationRewriter extends QueryBasedRelationRewriter { | |||
67 | }; | 68 | }; |
68 | } | 69 | } |
69 | 70 | ||
70 | public static EqualsRelationRewriter of(UpperCardinalityView upperCardinalityView) { | 71 | public static EqualsRelationRewriter of(AnySymbolView upperCardinalityView) { |
71 | var may = Query.of("MAY_EQUALS", (builder, p1, p2) -> builder | 72 | var may = Query.of("MAY_EQUALS", (builder, p1, p2) -> builder |
72 | .clause( | 73 | .clause( |
73 | p1.isEquivalent(p2), | 74 | p1.isEquivalent(p2), |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectInitializer.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectInitializer.java index 6917b8ed..084bf6f9 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectInitializer.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectInitializer.java | |||
@@ -5,6 +5,7 @@ | |||
5 | */ | 5 | */ |
6 | package tools.refinery.store.reasoning.translator.multiobject; | 6 | package tools.refinery.store.reasoning.translator.multiobject; |
7 | 7 | ||
8 | import org.jetbrains.annotations.NotNull; | ||
8 | import tools.refinery.store.model.Model; | 9 | import tools.refinery.store.model.Model; |
9 | import tools.refinery.store.reasoning.ReasoningAdapter; | 10 | import tools.refinery.store.reasoning.ReasoningAdapter; |
10 | import tools.refinery.store.reasoning.refinement.PartialModelInitializer; | 11 | import tools.refinery.store.reasoning.refinement.PartialModelInitializer; |
@@ -26,8 +27,7 @@ class MultiObjectInitializer implements PartialModelInitializer { | |||
26 | 27 | ||
27 | @Override | 28 | @Override |
28 | public void initialize(Model model, ModelSeed modelSeed) { | 29 | public void initialize(Model model, ModelSeed modelSeed) { |
29 | var intervals = new CardinalityInterval[modelSeed.getNodeCount()]; | 30 | var intervals = initializeIntervals(modelSeed); |
30 | Arrays.fill(intervals, CardinalityIntervals.SET); | ||
31 | initializeExists(intervals, modelSeed); | 31 | initializeExists(intervals, modelSeed); |
32 | initializeEquals(intervals, modelSeed); | 32 | initializeEquals(intervals, modelSeed); |
33 | var countInterpretation = model.getInterpretation(countSymbol); | 33 | var countInterpretation = model.getInterpretation(countSymbol); |
@@ -40,7 +40,33 @@ class MultiObjectInitializer implements PartialModelInitializer { | |||
40 | } | 40 | } |
41 | } | 41 | } |
42 | 42 | ||
43 | @NotNull | ||
44 | private CardinalityInterval[] initializeIntervals(ModelSeed modelSeed) { | ||
45 | var intervals = new CardinalityInterval[modelSeed.getNodeCount()]; | ||
46 | if (modelSeed.containsSeed(MultiObjectTranslator.COUNT_SYMBOL)) { | ||
47 | Arrays.fill(intervals, CardinalityIntervals.ONE); | ||
48 | var cursor = modelSeed.getCursor(MultiObjectTranslator.COUNT_SYMBOL, CardinalityIntervals.ONE); | ||
49 | while (cursor.move()) { | ||
50 | int i = cursor.getKey().get(0); | ||
51 | checkNodeId(intervals, i); | ||
52 | intervals[i] = cursor.getValue(); | ||
53 | } | ||
54 | } else { | ||
55 | Arrays.fill(intervals, CardinalityIntervals.SET); | ||
56 | if (!modelSeed.containsSeed(ReasoningAdapter.EXISTS_SYMBOL) || | ||
57 | !modelSeed.containsSeed(ReasoningAdapter.EQUALS_SYMBOL)) { | ||
58 | throw new IllegalArgumentException("Seed for %s and %s is required if there is no seed for %s" | ||
59 | .formatted(ReasoningAdapter.EXISTS_SYMBOL, ReasoningAdapter.EQUALS_SYMBOL, | ||
60 | MultiObjectTranslator.COUNT_SYMBOL)); | ||
61 | } | ||
62 | } | ||
63 | return intervals; | ||
64 | } | ||
65 | |||
43 | private void initializeExists(CardinalityInterval[] intervals, ModelSeed modelSeed) { | 66 | private void initializeExists(CardinalityInterval[] intervals, ModelSeed modelSeed) { |
67 | if (!modelSeed.containsSeed(ReasoningAdapter.EXISTS_SYMBOL)) { | ||
68 | return; | ||
69 | } | ||
44 | var cursor = modelSeed.getCursor(ReasoningAdapter.EXISTS_SYMBOL, TruthValue.UNKNOWN); | 70 | var cursor = modelSeed.getCursor(ReasoningAdapter.EXISTS_SYMBOL, TruthValue.UNKNOWN); |
45 | while (cursor.move()) { | 71 | while (cursor.move()) { |
46 | int i = cursor.getKey().get(0); | 72 | int i = cursor.getKey().get(0); |
@@ -56,6 +82,9 @@ class MultiObjectInitializer implements PartialModelInitializer { | |||
56 | } | 82 | } |
57 | 83 | ||
58 | private void initializeEquals(CardinalityInterval[] intervals, ModelSeed modelSeed) { | 84 | private void initializeEquals(CardinalityInterval[] intervals, ModelSeed modelSeed) { |
85 | if (!modelSeed.containsSeed(ReasoningAdapter.EQUALS_SYMBOL)) { | ||
86 | return; | ||
87 | } | ||
59 | var seed = modelSeed.getSeed(ReasoningAdapter.EQUALS_SYMBOL); | 88 | var seed = modelSeed.getSeed(ReasoningAdapter.EQUALS_SYMBOL); |
60 | var cursor = seed.getCursor(TruthValue.FALSE, modelSeed.getNodeCount()); | 89 | var cursor = seed.getCursor(TruthValue.FALSE, modelSeed.getNodeCount()); |
61 | while (cursor.move()) { | 90 | while (cursor.move()) { |
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 0367214b..09993c80 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 | |||
@@ -8,11 +8,14 @@ package tools.refinery.store.reasoning.translator.multiobject; | |||
8 | import tools.refinery.store.model.ModelStoreBuilder; | 8 | import tools.refinery.store.model.ModelStoreBuilder; |
9 | import tools.refinery.store.model.ModelStoreConfiguration; | 9 | import tools.refinery.store.model.ModelStoreConfiguration; |
10 | import tools.refinery.store.query.dnf.Query; | 10 | import tools.refinery.store.query.dnf.Query; |
11 | import tools.refinery.store.query.view.AnySymbolView; | ||
11 | import tools.refinery.store.reasoning.ReasoningAdapter; | 12 | import tools.refinery.store.reasoning.ReasoningAdapter; |
12 | import tools.refinery.store.reasoning.ReasoningBuilder; | 13 | import tools.refinery.store.reasoning.ReasoningBuilder; |
14 | import tools.refinery.store.reasoning.representation.PartialFunction; | ||
13 | import tools.refinery.store.reasoning.translator.PartialRelationTranslator; | 15 | import tools.refinery.store.reasoning.translator.PartialRelationTranslator; |
14 | import tools.refinery.store.reasoning.translator.RoundingMode; | 16 | import tools.refinery.store.reasoning.translator.RoundingMode; |
15 | import tools.refinery.store.representation.Symbol; | 17 | import tools.refinery.store.representation.Symbol; |
18 | import tools.refinery.store.representation.cardinality.CardinalityDomain; | ||
16 | import tools.refinery.store.representation.cardinality.CardinalityInterval; | 19 | import tools.refinery.store.representation.cardinality.CardinalityInterval; |
17 | import tools.refinery.store.representation.cardinality.UpperCardinalities; | 20 | import tools.refinery.store.representation.cardinality.UpperCardinalities; |
18 | import tools.refinery.store.representation.cardinality.UpperCardinality; | 21 | import tools.refinery.store.representation.cardinality.UpperCardinality; |
@@ -26,35 +29,37 @@ import static tools.refinery.store.query.term.uppercardinality.UpperCardinalityT | |||
26 | import static tools.refinery.store.query.term.uppercardinality.UpperCardinalityTerms.greaterEq; | 29 | import static tools.refinery.store.query.term.uppercardinality.UpperCardinalityTerms.greaterEq; |
27 | 30 | ||
28 | public class MultiObjectTranslator implements ModelStoreConfiguration { | 31 | public class MultiObjectTranslator implements ModelStoreConfiguration { |
29 | private final Symbol<CardinalityInterval> countSymbol = Symbol.of("COUNT", 1, CardinalityInterval.class, | 32 | private static final Symbol<CardinalityInterval> COUNT_STORAGE = Symbol.of("COUNT", 1, CardinalityInterval.class, |
30 | null); | 33 | null); |
31 | private final LowerCardinalityView lowerCardinalityView = new LowerCardinalityView(countSymbol); | 34 | public static final AnySymbolView LOWER_CARDINALITY_VIEW = new LowerCardinalityView(COUNT_STORAGE); |
32 | private final UpperCardinalityView upperCardinalityView = new UpperCardinalityView(countSymbol); | 35 | public static final AnySymbolView UPPER_CARDINALITY_VIEW = new UpperCardinalityView(COUNT_STORAGE); |
36 | public static final PartialFunction<CardinalityInterval, Integer> COUNT_SYMBOL = new PartialFunction<>("COUNT", 1, | ||
37 | CardinalityDomain.INSTANCE); | ||
33 | 38 | ||
34 | @Override | 39 | @Override |
35 | public void apply(ModelStoreBuilder storeBuilder) { | 40 | public void apply(ModelStoreBuilder storeBuilder) { |
36 | storeBuilder.symbol(countSymbol); | 41 | storeBuilder.symbol(COUNT_STORAGE); |
37 | 42 | ||
38 | storeBuilder.with(PartialRelationTranslator.of(ReasoningAdapter.EXISTS_SYMBOL) | 43 | storeBuilder.with(PartialRelationTranslator.of(ReasoningAdapter.EXISTS_SYMBOL) |
39 | .may(Query.of("MAY_EXISTS", (builder, p1) -> builder | 44 | .may(Query.of("MAY_EXISTS", (builder, p1) -> builder |
40 | .clause(UpperCardinality.class, upper -> List.of( | 45 | .clause(UpperCardinality.class, upper -> List.of( |
41 | upperCardinalityView.call(p1, upper), | 46 | UPPER_CARDINALITY_VIEW.call(p1, upper), |
42 | check(greaterEq(upper, constant(UpperCardinalities.ONE))) | 47 | check(greaterEq(upper, constant(UpperCardinalities.ONE))) |
43 | )))) | 48 | )))) |
44 | .must(Query.of("MUST_EXISTS", (builder, p1) -> builder | 49 | .must(Query.of("MUST_EXISTS", (builder, p1) -> builder |
45 | .clause(Integer.class, lower -> List.of( | 50 | .clause(Integer.class, lower -> List.of( |
46 | lowerCardinalityView.call(p1, lower), | 51 | LOWER_CARDINALITY_VIEW.call(p1, lower), |
47 | check(greaterEq(lower, constant(1))) | 52 | check(greaterEq(lower, constant(1))) |
48 | )))) | 53 | )))) |
49 | .roundingMode(RoundingMode.PREFER_FALSE) | 54 | .roundingMode(RoundingMode.PREFER_FALSE) |
50 | .refiner(ExistsRefiner.of(countSymbol))); | 55 | .refiner(ExistsRefiner.of(COUNT_STORAGE))); |
51 | 56 | ||
52 | storeBuilder.with(PartialRelationTranslator.of(ReasoningAdapter.EQUALS_SYMBOL) | 57 | storeBuilder.with(PartialRelationTranslator.of(ReasoningAdapter.EQUALS_SYMBOL) |
53 | .rewriter(EqualsRelationRewriter.of(upperCardinalityView)) | 58 | .rewriter(EqualsRelationRewriter.of(UPPER_CARDINALITY_VIEW)) |
54 | .refiner(EqualsRefiner.of(countSymbol))); | 59 | .refiner(EqualsRefiner.of(COUNT_STORAGE))); |
55 | 60 | ||
56 | var reasoningBuilder = storeBuilder.getAdapter(ReasoningBuilder.class); | 61 | var reasoningBuilder = storeBuilder.getAdapter(ReasoningBuilder.class); |
57 | reasoningBuilder.initializer(new MultiObjectInitializer(countSymbol)); | 62 | reasoningBuilder.initializer(new MultiObjectInitializer(COUNT_STORAGE)); |
58 | reasoningBuilder.storageRefiner(countSymbol, MultiObjectStorageRefiner::new); | 63 | reasoningBuilder.storageRefiner(COUNT_STORAGE, MultiObjectStorageRefiner::new); |
59 | } | 64 | } |
60 | } | 65 | } |
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/ConcreteCountTest.java new file mode 100644 index 00000000..21111d7c --- /dev/null +++ b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/ConcreteCountTest.java | |||
@@ -0,0 +1,324 @@ | |||
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; | ||
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.literal.Concreteness; | ||
16 | import tools.refinery.store.reasoning.literal.CountLowerBoundLiteral; | ||
17 | import tools.refinery.store.reasoning.literal.CountUpperBoundLiteral; | ||
18 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
19 | import tools.refinery.store.reasoning.seed.ModelSeed; | ||
20 | import tools.refinery.store.reasoning.translator.PartialRelationTranslator; | ||
21 | import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator; | ||
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.representation.cardinality.UpperCardinalities; | ||
26 | import tools.refinery.store.representation.cardinality.UpperCardinality; | ||
27 | import tools.refinery.store.tuple.Tuple; | ||
28 | |||
29 | import java.util.List; | ||
30 | |||
31 | import static org.hamcrest.MatcherAssert.assertThat; | ||
32 | import static org.hamcrest.Matchers.is; | ||
33 | import static tools.refinery.store.query.literal.Literals.not; | ||
34 | import static tools.refinery.store.reasoning.literal.PartialLiterals.must; | ||
35 | |||
36 | class ConcreteCountTest { | ||
37 | private static final PartialRelation person = new PartialRelation("Person", 1); | ||
38 | private static final PartialRelation friend = new PartialRelation("friend", 2); | ||
39 | |||
40 | @Test | ||
41 | void lowerBoundZeroTest() { | ||
42 | var query = Query.of("LowerBound", Integer.class, (builder, p1, p2, output) -> builder.clause( | ||
43 | must(person.call(p1)), | ||
44 | must(person.call(p2)), | ||
45 | new CountLowerBoundLiteral(output, Concreteness.PARTIAL, friend, List.of(p1, p2)) | ||
46 | )); | ||
47 | |||
48 | var modelSeed = ModelSeed.builder(2) | ||
49 | .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder | ||
50 | .put(Tuple.of(0), CardinalityIntervals.atLeast(3)) | ||
51 | .put(Tuple.of(1), CardinalityIntervals.atMost(7))) | ||
52 | .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) | ||
53 | .seed(friend, builder -> builder | ||
54 | .put(Tuple.of(0, 1), TruthValue.TRUE) | ||
55 | .put(Tuple.of(1, 0), TruthValue.UNKNOWN) | ||
56 | .put(Tuple.of(1, 1), TruthValue.ERROR)) | ||
57 | .build(); | ||
58 | |||
59 | var resultSet = getResultSet(query, modelSeed); | ||
60 | assertThat(resultSet.get(Tuple.of(0, 0)), is(0)); | ||
61 | assertThat(resultSet.get(Tuple.of(0, 1)), is(1)); | ||
62 | assertThat(resultSet.get(Tuple.of(1, 0)), is(0)); | ||
63 | assertThat(resultSet.get(Tuple.of(1, 1)), is(1)); | ||
64 | } | ||
65 | |||
66 | @Test | ||
67 | void upperBoundZeroTest() { | ||
68 | var query = Query.of("UpperBound", UpperCardinality.class, (builder, p1, p2, output) -> builder.clause( | ||
69 | must(person.call(p1)), | ||
70 | must(person.call(p2)), | ||
71 | new CountUpperBoundLiteral(output, Concreteness.PARTIAL, friend, List.of(p1, p2)) | ||
72 | )); | ||
73 | |||
74 | var modelSeed = ModelSeed.builder(2) | ||
75 | .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder | ||
76 | .put(Tuple.of(0), CardinalityIntervals.atLeast(3)) | ||
77 | .put(Tuple.of(1), CardinalityIntervals.atMost(7))) | ||
78 | .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) | ||
79 | .seed(friend, builder -> builder | ||
80 | .put(Tuple.of(0, 1), TruthValue.TRUE) | ||
81 | .put(Tuple.of(1, 0), TruthValue.UNKNOWN) | ||
82 | .put(Tuple.of(1, 1), TruthValue.ERROR)) | ||
83 | .build(); | ||
84 | |||
85 | var resultSet = getResultSet(query, modelSeed); | ||
86 | assertThat(resultSet.get(Tuple.of(0, 0)), is(UpperCardinalities.ZERO)); | ||
87 | assertThat(resultSet.get(Tuple.of(0, 1)), is(UpperCardinalities.ONE)); | ||
88 | assertThat(resultSet.get(Tuple.of(1, 0)), is(UpperCardinalities.ONE)); | ||
89 | assertThat(resultSet.get(Tuple.of(1, 1)), is(UpperCardinalities.ZERO)); | ||
90 | } | ||
91 | |||
92 | @Test | ||
93 | void lowerBoundOneTest() { | ||
94 | var query = Query.of("LowerBound", Integer.class, (builder, p1, output) -> builder.clause( | ||
95 | must(person.call(p1)), | ||
96 | new CountLowerBoundLiteral(output, Concreteness.PARTIAL, friend, List.of(p1, Variable.of())) | ||
97 | )); | ||
98 | |||
99 | var modelSeed = ModelSeed.builder(4) | ||
100 | .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder | ||
101 | .reducedValue(CardinalityIntervals.ONE) | ||
102 | .put(Tuple.of(1), CardinalityIntervals.atLeast(3)) | ||
103 | .put(Tuple.of(2), CardinalityIntervals.atMost(7))) | ||
104 | .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) | ||
105 | .seed(friend, builder -> builder | ||
106 | .put(Tuple.of(0, 1), TruthValue.TRUE) | ||
107 | .put(Tuple.of(0, 2), TruthValue.TRUE) | ||
108 | .put(Tuple.of(0, 3), TruthValue.TRUE) | ||
109 | .put(Tuple.of(1, 0), TruthValue.TRUE) | ||
110 | .put(Tuple.of(1, 2), TruthValue.UNKNOWN) | ||
111 | .put(Tuple.of(1, 3), TruthValue.UNKNOWN) | ||
112 | .put(Tuple.of(2, 0), TruthValue.TRUE) | ||
113 | .put(Tuple.of(2, 1), TruthValue.ERROR)) | ||
114 | .build(); | ||
115 | |||
116 | var resultSet = getResultSet(query, modelSeed); | ||
117 | assertThat(resultSet.get(Tuple.of(0)), is(4)); | ||
118 | assertThat(resultSet.get(Tuple.of(1)), is(1)); | ||
119 | assertThat(resultSet.get(Tuple.of(2)), is(4)); | ||
120 | assertThat(resultSet.get(Tuple.of(3)), is(0)); | ||
121 | } | ||
122 | |||
123 | @Test | ||
124 | void upperBoundOneTest() { | ||
125 | var query = Query.of("UpperBound", UpperCardinality.class, (builder, p1, output) -> builder.clause( | ||
126 | must(person.call(p1)), | ||
127 | new CountUpperBoundLiteral(output, Concreteness.PARTIAL, friend, List.of(p1, Variable.of())) | ||
128 | )); | ||
129 | |||
130 | var modelSeed = ModelSeed.builder(4) | ||
131 | .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder | ||
132 | .reducedValue(CardinalityIntervals.ONE) | ||
133 | .put(Tuple.of(1), CardinalityIntervals.atLeast(3)) | ||
134 | .put(Tuple.of(2), CardinalityIntervals.atMost(7))) | ||
135 | .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) | ||
136 | .seed(friend, builder -> builder | ||
137 | .put(Tuple.of(0, 1), TruthValue.TRUE) | ||
138 | .put(Tuple.of(0, 2), TruthValue.TRUE) | ||
139 | .put(Tuple.of(0, 3), TruthValue.TRUE) | ||
140 | .put(Tuple.of(1, 0), TruthValue.TRUE) | ||
141 | .put(Tuple.of(1, 2), TruthValue.UNKNOWN) | ||
142 | .put(Tuple.of(1, 3), TruthValue.UNKNOWN) | ||
143 | .put(Tuple.of(2, 0), TruthValue.TRUE) | ||
144 | .put(Tuple.of(2, 1), TruthValue.ERROR)) | ||
145 | .build(); | ||
146 | |||
147 | var resultSet = getResultSet(query, modelSeed); | ||
148 | assertThat(resultSet.get(Tuple.of(0)), is(UpperCardinalities.UNBOUNDED)); | ||
149 | assertThat(resultSet.get(Tuple.of(1)), is(UpperCardinalities.atMost(9))); | ||
150 | assertThat(resultSet.get(Tuple.of(2)), is(UpperCardinalities.ONE)); | ||
151 | assertThat(resultSet.get(Tuple.of(3)), is(UpperCardinalities.ZERO)); | ||
152 | } | ||
153 | |||
154 | @Test | ||
155 | void lowerBoundTwoTest() { | ||
156 | var subQuery = Query.of("SubQuery", (builder, p1, p2, p3) -> builder.clause( | ||
157 | friend.call(p1, p2), | ||
158 | friend.call(p1, p3), | ||
159 | friend.call(p2, p3) | ||
160 | )); | ||
161 | var query = Query.of("LowerBound", Integer.class, (builder, p1, output) -> builder.clause( | ||
162 | must(person.call(p1)), | ||
163 | new CountLowerBoundLiteral(output, Concreteness.PARTIAL, subQuery.getDnf(), | ||
164 | List.of(p1, Variable.of(), Variable.of())) | ||
165 | )); | ||
166 | |||
167 | var modelSeed = ModelSeed.builder(4) | ||
168 | .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder | ||
169 | .reducedValue(CardinalityIntervals.ONE) | ||
170 | .put(Tuple.of(0), CardinalityIntervals.between(5, 9)) | ||
171 | .put(Tuple.of(1), CardinalityIntervals.atLeast(3)) | ||
172 | .put(Tuple.of(2), CardinalityIntervals.atMost(7))) | ||
173 | .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) | ||
174 | .seed(friend, builder -> builder | ||
175 | .put(Tuple.of(0, 1), TruthValue.TRUE) | ||
176 | .put(Tuple.of(0, 2), TruthValue.TRUE) | ||
177 | .put(Tuple.of(0, 3), TruthValue.TRUE) | ||
178 | .put(Tuple.of(1, 0), TruthValue.TRUE) | ||
179 | .put(Tuple.of(1, 2), TruthValue.TRUE) | ||
180 | .put(Tuple.of(1, 3), TruthValue.TRUE) | ||
181 | .put(Tuple.of(2, 0), TruthValue.TRUE) | ||
182 | .put(Tuple.of(2, 1), TruthValue.ERROR)) | ||
183 | .build(); | ||
184 | |||
185 | var resultSet = getResultSet(query, modelSeed); | ||
186 | assertThat(resultSet.get(Tuple.of(0)), is(3)); | ||
187 | assertThat(resultSet.get(Tuple.of(1)), is(5)); | ||
188 | assertThat(resultSet.get(Tuple.of(2)), is(30)); | ||
189 | assertThat(resultSet.get(Tuple.of(3)), is(0)); | ||
190 | } | ||
191 | |||
192 | @Test | ||
193 | void upperBoundTwoTest() { | ||
194 | var subQuery = Query.of("SubQuery", (builder, p1, p2, p3) -> builder.clause( | ||
195 | friend.call(p1, p2), | ||
196 | friend.call(p1, p3), | ||
197 | friend.call(p2, p3) | ||
198 | )); | ||
199 | var query = Query.of("UpperBound", UpperCardinality.class, (builder, p1, output) -> builder.clause( | ||
200 | must(person.call(p1)), | ||
201 | new CountUpperBoundLiteral(output, Concreteness.PARTIAL, subQuery.getDnf(), | ||
202 | List.of(p1, Variable.of(), Variable.of())) | ||
203 | )); | ||
204 | |||
205 | var modelSeed = ModelSeed.builder(4) | ||
206 | .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder | ||
207 | .reducedValue(CardinalityIntervals.ONE) | ||
208 | .put(Tuple.of(0), CardinalityIntervals.between(5, 9)) | ||
209 | .put(Tuple.of(1), CardinalityIntervals.atLeast(3)) | ||
210 | .put(Tuple.of(2), CardinalityIntervals.atMost(7))) | ||
211 | .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) | ||
212 | .seed(friend, builder -> builder | ||
213 | .put(Tuple.of(0, 1), TruthValue.TRUE) | ||
214 | .put(Tuple.of(0, 2), TruthValue.TRUE) | ||
215 | .put(Tuple.of(0, 3), TruthValue.TRUE) | ||
216 | .put(Tuple.of(1, 0), TruthValue.TRUE) | ||
217 | .put(Tuple.of(1, 2), TruthValue.UNKNOWN) | ||
218 | .put(Tuple.of(1, 3), TruthValue.UNKNOWN) | ||
219 | .put(Tuple.of(2, 0), TruthValue.TRUE) | ||
220 | .put(Tuple.of(2, 1), TruthValue.ERROR)) | ||
221 | .build(); | ||
222 | |||
223 | var resultSet = getResultSet(query, modelSeed); | ||
224 | assertThat(resultSet.get(Tuple.of(0)), is(UpperCardinalities.UNBOUNDED)); | ||
225 | assertThat(resultSet.get(Tuple.of(1)), is(UpperCardinalities.atMost(135))); | ||
226 | assertThat(resultSet.get(Tuple.of(2)), is(UpperCardinalities.ZERO)); | ||
227 | assertThat(resultSet.get(Tuple.of(3)), is(UpperCardinalities.ZERO)); | ||
228 | } | ||
229 | |||
230 | @Test | ||
231 | void lowerBoundDiagonalTest() { | ||
232 | var subQuery = Query.of("SubQuery", (builder, p1, p2, p3) -> builder.clause( | ||
233 | friend.call(p1, p2), | ||
234 | friend.call(p1, p3), | ||
235 | not(friend.call(p2, p3)) | ||
236 | )); | ||
237 | var query = Query.of("LowerBound", Integer.class, (builder, p1, output) -> builder.clause(v1 -> List.of( | ||
238 | must(person.call(p1)), | ||
239 | new CountLowerBoundLiteral(output, Concreteness.PARTIAL, subQuery.getDnf(), List.of(p1, v1, v1)) | ||
240 | ))); | ||
241 | |||
242 | var modelSeed = ModelSeed.builder(4) | ||
243 | .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder | ||
244 | .reducedValue(CardinalityIntervals.ONE) | ||
245 | .put(Tuple.of(0), CardinalityIntervals.between(5, 9)) | ||
246 | .put(Tuple.of(1), CardinalityIntervals.atLeast(3)) | ||
247 | .put(Tuple.of(2), CardinalityIntervals.atMost(7))) | ||
248 | .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) | ||
249 | .seed(friend, builder -> builder | ||
250 | .put(Tuple.of(0, 1), TruthValue.TRUE) | ||
251 | .put(Tuple.of(0, 2), TruthValue.TRUE) | ||
252 | .put(Tuple.of(0, 3), TruthValue.TRUE) | ||
253 | .put(Tuple.of(1, 0), TruthValue.TRUE) | ||
254 | .put(Tuple.of(1, 2), TruthValue.UNKNOWN) | ||
255 | .put(Tuple.of(1, 3), TruthValue.UNKNOWN) | ||
256 | .put(Tuple.of(2, 0), TruthValue.TRUE) | ||
257 | .put(Tuple.of(2, 1), TruthValue.ERROR)) | ||
258 | .build(); | ||
259 | |||
260 | var resultSet = getResultSet(query, modelSeed); | ||
261 | assertThat(resultSet.get(Tuple.of(0)), is(4)); | ||
262 | assertThat(resultSet.get(Tuple.of(1)), is(5)); | ||
263 | assertThat(resultSet.get(Tuple.of(2)), is(8)); | ||
264 | assertThat(resultSet.get(Tuple.of(3)), is(0)); | ||
265 | } | ||
266 | |||
267 | @Test | ||
268 | void upperBoundDiagonalTest() { | ||
269 | var subQuery = Query.of("SubQuery", (builder, p1, p2, p3) -> builder.clause( | ||
270 | friend.call(p1, p2), | ||
271 | friend.call(p1, p3), | ||
272 | not(friend.call(p2, p3)) | ||
273 | )); | ||
274 | var query = Query.of("UpperBound", UpperCardinality.class, (builder, p1, output) -> builder | ||
275 | .clause(v1 -> List.of( | ||
276 | must(person.call(p1)), | ||
277 | new CountUpperBoundLiteral(output, Concreteness.PARTIAL, subQuery.getDnf(), | ||
278 | List.of(p1, v1, v1)) | ||
279 | ))); | ||
280 | |||
281 | var modelSeed = ModelSeed.builder(4) | ||
282 | .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder | ||
283 | .reducedValue(CardinalityIntervals.ONE) | ||
284 | .put(Tuple.of(0), CardinalityIntervals.between(5, 9)) | ||
285 | .put(Tuple.of(1), CardinalityIntervals.atLeast(3)) | ||
286 | .put(Tuple.of(2), CardinalityIntervals.atMost(7))) | ||
287 | .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) | ||
288 | .seed(friend, builder -> builder | ||
289 | .put(Tuple.of(0, 1), TruthValue.TRUE) | ||
290 | .put(Tuple.of(0, 2), TruthValue.TRUE) | ||
291 | .put(Tuple.of(0, 3), TruthValue.TRUE) | ||
292 | .put(Tuple.of(1, 0), TruthValue.TRUE) | ||
293 | .put(Tuple.of(1, 2), TruthValue.UNKNOWN) | ||
294 | .put(Tuple.of(1, 3), TruthValue.UNKNOWN) | ||
295 | .put(Tuple.of(2, 0), TruthValue.TRUE) | ||
296 | .put(Tuple.of(2, 1), TruthValue.ERROR)) | ||
297 | .build(); | ||
298 | |||
299 | var resultSet = getResultSet(query, modelSeed); | ||
300 | assertThat(resultSet.get(Tuple.of(0)), is(UpperCardinalities.UNBOUNDED)); | ||
301 | assertThat(resultSet.get(Tuple.of(1)), is(UpperCardinalities.atMost(17))); | ||
302 | assertThat(resultSet.get(Tuple.of(2)), is(UpperCardinalities.atMost(9))); | ||
303 | assertThat(resultSet.get(Tuple.of(3)), is(UpperCardinalities.ZERO)); | ||
304 | } | ||
305 | |||
306 | private static <T> ResultSet<T> getResultSet(Query<T> query, ModelSeed modelSeed) { | ||
307 | var personStorage = Symbol.of("Person", 1, TruthValue.class, TruthValue.FALSE); | ||
308 | var friendStorage = Symbol.of("friend", 2, TruthValue.class, TruthValue.FALSE); | ||
309 | |||
310 | var store = ModelStore.builder() | ||
311 | .with(ViatraModelQueryAdapter.builder() | ||
312 | .query(query)) | ||
313 | .with(ReasoningAdapter.builder()) | ||
314 | .with(new MultiObjectTranslator()) | ||
315 | .with(PartialRelationTranslator.of(person) | ||
316 | .symbol(personStorage)) | ||
317 | .with(PartialRelationTranslator.of(friend) | ||
318 | .symbol(friendStorage)) | ||
319 | .build(); | ||
320 | |||
321 | var model = store.getAdapter(ReasoningStoreAdapter.class).createInitialModel(modelSeed); | ||
322 | return model.getAdapter(ModelQueryAdapter.class).getResultSet(query); | ||
323 | } | ||
324 | } | ||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/CardinalityDomain.java b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/CardinalityDomain.java new file mode 100644 index 00000000..7ae2d935 --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/CardinalityDomain.java | |||
@@ -0,0 +1,68 @@ | |||
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.representation.cardinality; | ||
7 | |||
8 | import tools.refinery.store.representation.AbstractDomain; | ||
9 | |||
10 | import java.util.Optional; | ||
11 | |||
12 | // Singleton pattern, because there is only one domain for truth values. | ||
13 | @SuppressWarnings("squid:S6548") | ||
14 | public class CardinalityDomain implements AbstractDomain<CardinalityInterval, Integer> { | ||
15 | public static final CardinalityDomain INSTANCE = new CardinalityDomain(); | ||
16 | |||
17 | private CardinalityDomain() { | ||
18 | } | ||
19 | |||
20 | @Override | ||
21 | public Class<CardinalityInterval> abstractType() { | ||
22 | return CardinalityInterval.class; | ||
23 | } | ||
24 | |||
25 | @Override | ||
26 | public Class<Integer> concreteType() { | ||
27 | return Integer.class; | ||
28 | } | ||
29 | |||
30 | @Override | ||
31 | public CardinalityInterval toAbstract(Integer concreteValue) { | ||
32 | return CardinalityIntervals.exactly(concreteValue); | ||
33 | } | ||
34 | |||
35 | @Override | ||
36 | public Optional<Integer> toConcrete(CardinalityInterval abstractValue) { | ||
37 | return isConcrete(abstractValue) ? Optional.of(abstractValue.lowerBound()) : Optional.empty(); | ||
38 | } | ||
39 | |||
40 | @Override | ||
41 | public boolean isConcrete(CardinalityInterval abstractValue) { | ||
42 | if (!(abstractValue instanceof NonEmptyCardinalityInterval nonEmptyValue) || | ||
43 | !((nonEmptyValue.upperBound()) instanceof FiniteUpperCardinality finiteUpperCardinality)) { | ||
44 | return false; | ||
45 | } | ||
46 | return nonEmptyValue.lowerBound() == finiteUpperCardinality.finiteUpperBound(); | ||
47 | } | ||
48 | |||
49 | @Override | ||
50 | public CardinalityInterval commonRefinement(CardinalityInterval leftValue, CardinalityInterval rightValue) { | ||
51 | return leftValue.meet(rightValue); | ||
52 | } | ||
53 | |||
54 | @Override | ||
55 | public CardinalityInterval commonAncestor(CardinalityInterval leftValue, CardinalityInterval rightValue) { | ||
56 | return leftValue.join(rightValue); | ||
57 | } | ||
58 | |||
59 | @Override | ||
60 | public CardinalityInterval unknown() { | ||
61 | return CardinalityIntervals.SET; | ||
62 | } | ||
63 | |||
64 | @Override | ||
65 | public boolean isError(CardinalityInterval abstractValue) { | ||
66 | return abstractValue.isEmpty(); | ||
67 | } | ||
68 | } | ||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/CardinalityIntervals.java b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/CardinalityIntervals.java index ad16a3e8..855fd248 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/CardinalityIntervals.java +++ b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/CardinalityIntervals.java | |||
@@ -30,7 +30,7 @@ public final class CardinalityIntervals { | |||
30 | } | 30 | } |
31 | 31 | ||
32 | public static CardinalityInterval between(int lowerBound, int upperBound) { | 32 | public static CardinalityInterval between(int lowerBound, int upperBound) { |
33 | return between(lowerBound, UpperCardinalities.valueOf(upperBound)); | 33 | return between(lowerBound, UpperCardinalities.atMost(upperBound)); |
34 | } | 34 | } |
35 | 35 | ||
36 | public static CardinalityInterval atMost(UpperCardinality upperBound) { | 36 | public static CardinalityInterval atMost(UpperCardinality upperBound) { |
@@ -38,7 +38,7 @@ public final class CardinalityIntervals { | |||
38 | } | 38 | } |
39 | 39 | ||
40 | public static CardinalityInterval atMost(int upperBound) { | 40 | public static CardinalityInterval atMost(int upperBound) { |
41 | return atMost(UpperCardinalities.valueOf(upperBound)); | 41 | return atMost(UpperCardinalities.atMost(upperBound)); |
42 | } | 42 | } |
43 | 43 | ||
44 | public static CardinalityInterval atLeast(int lowerBound) { | 44 | public static CardinalityInterval atLeast(int lowerBound) { |
@@ -46,6 +46,6 @@ public final class CardinalityIntervals { | |||
46 | } | 46 | } |
47 | 47 | ||
48 | public static CardinalityInterval exactly(int lowerBound) { | 48 | public static CardinalityInterval exactly(int lowerBound) { |
49 | return new NonEmptyCardinalityInterval(lowerBound, UpperCardinalities.valueOf(lowerBound)); | 49 | return new NonEmptyCardinalityInterval(lowerBound, UpperCardinalities.atMost(lowerBound)); |
50 | } | 50 | } |
51 | } | 51 | } |
diff --git a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/FiniteUpperCardinality.java b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/FiniteUpperCardinality.java index acd82beb..088e3925 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/FiniteUpperCardinality.java +++ b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/FiniteUpperCardinality.java | |||
@@ -59,7 +59,7 @@ public record FiniteUpperCardinality(int finiteUpperBound) implements UpperCardi | |||
59 | 59 | ||
60 | private UpperCardinality lift(@NotNull UpperCardinality other, IntBinaryOperator operator) { | 60 | private UpperCardinality lift(@NotNull UpperCardinality other, IntBinaryOperator operator) { |
61 | if (other instanceof FiniteUpperCardinality finiteUpperCardinality) { | 61 | if (other instanceof FiniteUpperCardinality finiteUpperCardinality) { |
62 | return UpperCardinalities.valueOf(operator.applyAsInt(finiteUpperBound, | 62 | return UpperCardinalities.atMost(operator.applyAsInt(finiteUpperBound, |
63 | finiteUpperCardinality.finiteUpperBound)); | 63 | finiteUpperCardinality.finiteUpperBound)); |
64 | } | 64 | } |
65 | if (other instanceof UnboundedUpperCardinality) { | 65 | if (other instanceof UnboundedUpperCardinality) { |
diff --git a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/UpperCardinalities.java b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/UpperCardinalities.java index 1e18dde0..17d1b292 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/UpperCardinalities.java +++ b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/UpperCardinalities.java | |||
@@ -26,7 +26,7 @@ public final class UpperCardinalities { | |||
26 | throw new IllegalStateException("This is a static utility class and should not be instantiated directly"); | 26 | throw new IllegalStateException("This is a static utility class and should not be instantiated directly"); |
27 | } | 27 | } |
28 | 28 | ||
29 | public static UpperCardinality valueOf(int upperBound) { | 29 | public static UpperCardinality atMost(int upperBound) { |
30 | if (upperBound < 0) { | 30 | if (upperBound < 0) { |
31 | return UNBOUNDED; | 31 | return UNBOUNDED; |
32 | } | 32 | } |
diff --git a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/UpperCardinality.java b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/UpperCardinality.java index 5600ab4c..3f0db028 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/UpperCardinality.java +++ b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/UpperCardinality.java | |||
@@ -27,6 +27,6 @@ public sealed interface UpperCardinality extends Comparable<UpperCardinality> pe | |||
27 | int compareToInt(int value); | 27 | int compareToInt(int value); |
28 | 28 | ||
29 | static UpperCardinality of(int upperBound) { | 29 | static UpperCardinality of(int upperBound) { |
30 | return UpperCardinalities.valueOf(upperBound); | 30 | return UpperCardinalities.atMost(upperBound); |
31 | } | 31 | } |
32 | } | 32 | } |
diff --git a/subprojects/store/src/test/java/tools/refinery/store/representation/cardinality/UpperCardinalitiesTest.java b/subprojects/store/src/test/java/tools/refinery/store/representation/cardinality/UpperCardinalitiesTest.java index e61f7b36..e403eec2 100644 --- a/subprojects/store/src/test/java/tools/refinery/store/representation/cardinality/UpperCardinalitiesTest.java +++ b/subprojects/store/src/test/java/tools/refinery/store/representation/cardinality/UpperCardinalitiesTest.java | |||
@@ -8,9 +8,6 @@ package tools.refinery.store.representation.cardinality; | |||
8 | import org.junit.jupiter.api.Test; | 8 | import org.junit.jupiter.api.Test; |
9 | import org.junit.jupiter.params.ParameterizedTest; | 9 | import org.junit.jupiter.params.ParameterizedTest; |
10 | import org.junit.jupiter.params.provider.ValueSource; | 10 | import org.junit.jupiter.params.provider.ValueSource; |
11 | import tools.refinery.store.representation.cardinality.FiniteUpperCardinality; | ||
12 | import tools.refinery.store.representation.cardinality.UnboundedUpperCardinality; | ||
13 | import tools.refinery.store.representation.cardinality.UpperCardinalities; | ||
14 | 11 | ||
15 | import static org.hamcrest.MatcherAssert.assertThat; | 12 | import static org.hamcrest.MatcherAssert.assertThat; |
16 | import static org.hamcrest.Matchers.equalTo; | 13 | import static org.hamcrest.Matchers.equalTo; |
@@ -20,14 +17,14 @@ class UpperCardinalitiesTest { | |||
20 | @ParameterizedTest | 17 | @ParameterizedTest |
21 | @ValueSource(ints = {0, 1, 255, 256, 1000, Integer.MAX_VALUE}) | 18 | @ValueSource(ints = {0, 1, 255, 256, 1000, Integer.MAX_VALUE}) |
22 | void valueOfBoundedTest(int value) { | 19 | void valueOfBoundedTest(int value) { |
23 | var upperCardinality = UpperCardinalities.valueOf(value); | 20 | var upperCardinality = UpperCardinalities.atMost(value); |
24 | assertThat(upperCardinality, instanceOf(FiniteUpperCardinality.class)); | 21 | assertThat(upperCardinality, instanceOf(FiniteUpperCardinality.class)); |
25 | assertThat(((FiniteUpperCardinality) upperCardinality).finiteUpperBound(), equalTo(value)); | 22 | assertThat(((FiniteUpperCardinality) upperCardinality).finiteUpperBound(), equalTo(value)); |
26 | } | 23 | } |
27 | 24 | ||
28 | @Test | 25 | @Test |
29 | void valueOfUnboundedTest() { | 26 | void valueOfUnboundedTest() { |
30 | var upperCardinality = UpperCardinalities.valueOf(-1); | 27 | var upperCardinality = UpperCardinalities.atMost(-1); |
31 | assertThat(upperCardinality, instanceOf(UnboundedUpperCardinality.class)); | 28 | assertThat(upperCardinality, instanceOf(UnboundedUpperCardinality.class)); |
32 | } | 29 | } |
33 | } | 30 | } |