From 6a25ba145844c79d3507f8eabdbed854be2b8097 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Tue, 25 Jul 2023 16:06:36 +0200 Subject: feat: concrete count in partial models --- .../store/query/literal/AbstractCountLiteral.java | 106 +++++++ .../refinery/store/query/literal/CountLiteral.java | 77 +---- .../UpperCardinalitySumAggregator.java | 2 +- .../reasoning/internal/PartialClauseRewriter.java | 93 +++++- .../store/reasoning/lifting/ClauseLifter.java | 4 +- .../reasoning/literal/ConcreteCountLiteral.java | 47 +++ .../reasoning/literal/CountLowerBoundLiteral.java | 48 +++ .../reasoning/literal/CountUpperBoundLiteral.java | 50 ++++ .../refinery/store/reasoning/seed/ModelSeed.java | 4 + .../multiobject/EqualsRelationRewriter.java | 3 +- .../multiobject/MultiObjectInitializer.java | 33 ++- .../multiobject/MultiObjectTranslator.java | 27 +- .../store/reasoning/ConcreteCountTest.java | 324 +++++++++++++++++++++ .../cardinality/CardinalityDomain.java | 68 +++++ .../cardinality/CardinalityIntervals.java | 6 +- .../cardinality/FiniteUpperCardinality.java | 2 +- .../cardinality/UpperCardinalities.java | 2 +- .../cardinality/UpperCardinality.java | 2 +- .../cardinality/UpperCardinalitiesTest.java | 7 +- 19 files changed, 807 insertions(+), 98 deletions(-) create mode 100644 subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AbstractCountLiteral.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ConcreteCountLiteral.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountLowerBoundLiteral.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountUpperBoundLiteral.java create mode 100644 subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/ConcreteCountTest.java create mode 100644 subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/CardinalityDomain.java (limited to 'subprojects') 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 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.query.literal; + +import tools.refinery.store.query.Constraint; +import tools.refinery.store.query.equality.LiteralEqualityHelper; +import tools.refinery.store.query.equality.LiteralHashCodeHelper; +import tools.refinery.store.query.term.ConstantTerm; +import tools.refinery.store.query.term.DataVariable; +import tools.refinery.store.query.term.Variable; + +import java.util.List; +import java.util.Objects; +import java.util.Set; + +// {@link Object#equals(Object)} is implemented by {@link AbstractLiteral}. +@SuppressWarnings("squid:S2160") +public abstract class AbstractCountLiteral extends AbstractCallLiteral { + private final Class resultType; + private final DataVariable resultVariable; + + protected AbstractCountLiteral(Class resultType, DataVariable resultVariable, Constraint target, + List arguments) { + super(target, arguments); + if (!resultVariable.getType().equals(resultType)) { + throw new IllegalArgumentException("Count result variable %s must be of type %s, got %s instead".formatted( + resultVariable, resultType, resultVariable.getType().getName())); + } + if (arguments.contains(resultVariable)) { + throw new IllegalArgumentException("Count result variable %s must not appear in the argument list" + .formatted(resultVariable)); + } + this.resultType = resultType; + this.resultVariable = resultVariable; + } + + public Class getResultType() { + return resultType; + } + + public DataVariable getResultVariable() { + return resultVariable; + } + + @Override + public Set getOutputVariables() { + return Set.of(resultVariable); + } + + protected abstract T zero(); + + protected abstract T one(); + + @Override + public Literal reduce() { + var reduction = getTarget().getReduction(); + return switch (reduction) { + case ALWAYS_FALSE -> getResultVariable().assign(new ConstantTerm<>(resultType, zero())); + // The only way a constant {@code true} predicate can be called in a negative position is to have all of + // its arguments bound as input variables. Thus, there will only be a single match. + case ALWAYS_TRUE -> getResultVariable().assign(new ConstantTerm<>(resultType, one())); + case NOT_REDUCIBLE -> this; + }; + } + + @Override + public boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other) { + if (!super.equalsWithSubstitution(helper, other)) { + return false; + } + var otherCountLiteral = (AbstractCountLiteral) other; + return Objects.equals(resultType, otherCountLiteral.resultType) && + helper.variableEqual(resultVariable, otherCountLiteral.resultVariable); + } + + @Override + public int hashCodeWithSubstitution(LiteralHashCodeHelper helper) { + return Objects.hash(super.hashCodeWithSubstitution(helper), resultType, + helper.getVariableHashCode(resultVariable)); + } + + protected abstract String operatorName(); + + @Override + public String toString() { + var builder = new StringBuilder(); + builder.append(resultVariable); + builder.append(" is "); + builder.append(operatorName()); + builder.append(' '); + builder.append(getTarget().toReferenceString()); + builder.append('('); + var argumentIterator = getArguments().iterator(); + if (argumentIterator.hasNext()) { + builder.append(argumentIterator.next()); + while (argumentIterator.hasNext()) { + builder.append(", ").append(argumentIterator.next()); + } + } + builder.append(')'); + return builder.toString(); + } +} 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 @@ package tools.refinery.store.query.literal; import tools.refinery.store.query.Constraint; -import tools.refinery.store.query.equality.LiteralEqualityHelper; -import tools.refinery.store.query.equality.LiteralHashCodeHelper; import tools.refinery.store.query.substitution.Substitution; import tools.refinery.store.query.term.DataVariable; import tools.refinery.store.query.term.Variable; -import tools.refinery.store.query.term.int_.IntTerms; import java.util.List; -import java.util.Objects; -import java.util.Set; - -// {@link Object#equals(Object)} is implemented by {@link AbstractLiteral}. -@SuppressWarnings("squid:S2160") -public class CountLiteral extends AbstractCallLiteral { - private final DataVariable resultVariable; +public class CountLiteral extends AbstractCountLiteral { public CountLiteral(DataVariable resultVariable, Constraint target, List arguments) { - super(target, arguments); - if (!resultVariable.getType().equals(Integer.class)) { - throw new IllegalArgumentException("Count result variable %s must be of type %s, got %s instead".formatted( - resultVariable, Integer.class.getName(), resultVariable.getType().getName())); - } - if (arguments.contains(resultVariable)) { - throw new IllegalArgumentException("Count result variable %s must not appear in the argument list" - .formatted(resultVariable)); - } - this.resultVariable = resultVariable; - } - - public DataVariable getResultVariable() { - return resultVariable; + super(Integer.class, resultVariable, target, arguments); } @Override - public Set getOutputVariables() { - return Set.of(resultVariable); + protected Integer zero() { + return 0; } @Override - public Literal reduce() { - var reduction = getTarget().getReduction(); - return switch (reduction) { - case ALWAYS_FALSE -> getResultVariable().assign(IntTerms.constant(0)); - // The only way a constant {@code true} predicate can be called in a negative position is to have all of - // its arguments bound as input variables. Thus, there will only be a single match. - case ALWAYS_TRUE -> getResultVariable().assign(IntTerms.constant(1)); - case NOT_REDUCIBLE -> this; - }; + protected Integer one() { + return 1; } @Override protected Literal doSubstitute(Substitution substitution, List substitutedArguments) { - return new CountLiteral(substitution.getTypeSafeSubstitute(resultVariable), getTarget(), substitutedArguments); + return new CountLiteral(substitution.getTypeSafeSubstitute(getResultVariable()), getTarget(), + substitutedArguments); } @Override protected AbstractCallLiteral internalWithTarget(Constraint newTarget) { - return new CountLiteral(resultVariable, newTarget, getArguments()); - } - - @Override - public boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other) { - if (!super.equalsWithSubstitution(helper, other)) { - return false; - } - var otherCountLiteral = (CountLiteral) other; - return helper.variableEqual(resultVariable, otherCountLiteral.resultVariable); - } - - @Override - public int hashCodeWithSubstitution(LiteralHashCodeHelper helper) { - return Objects.hash(super.hashCodeWithSubstitution(helper), helper.getVariableHashCode(resultVariable)); + return new CountLiteral(getResultVariable(), newTarget, getArguments()); } @Override - public String toString() { - var builder = new StringBuilder(); - builder.append(resultVariable); - builder.append(" is count "); - builder.append(getTarget().toReferenceString()); - builder.append("("); - var argumentIterator = getArguments().iterator(); - if (argumentIterator.hasNext()) { - builder.append(argumentIterator.next()); - while (argumentIterator.hasNext()) { - builder.append(", ").append(argumentIterator.next()); - } - } - builder.append(")"); - return builder.toString(); + protected String operatorName() { + return "count"; } } 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 0 ? UpperCardinalities.UNBOUNDED : UpperCardinalities.valueOf(sumFiniteUpperBounds); + return countUnbounded > 0 ? UpperCardinalities.UNBOUNDED : UpperCardinalities.atMost(sumFiniteUpperBounds); } @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 @@ */ package tools.refinery.store.reasoning.internal; +import tools.refinery.store.query.Constraint; import tools.refinery.store.query.dnf.Dnf; import tools.refinery.store.query.dnf.DnfClause; import tools.refinery.store.query.literal.AbstractCallLiteral; +import tools.refinery.store.query.literal.CallPolarity; import tools.refinery.store.query.literal.Literal; +import tools.refinery.store.query.term.Aggregator; +import tools.refinery.store.query.term.ConstantTerm; +import tools.refinery.store.query.term.Term; import tools.refinery.store.query.term.Variable; -import tools.refinery.store.reasoning.literal.Concreteness; -import tools.refinery.store.reasoning.literal.ModalConstraint; -import tools.refinery.store.reasoning.literal.Modality; +import tools.refinery.store.query.term.int_.IntTerms; +import tools.refinery.store.query.term.uppercardinality.UpperCardinalityTerms; +import tools.refinery.store.reasoning.literal.*; import tools.refinery.store.reasoning.representation.PartialRelation; +import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator; +import tools.refinery.store.representation.cardinality.UpperCardinalities; import java.util.*; +import java.util.function.BinaryOperator; class PartialClauseRewriter { private final PartialQueryRewriter rewriter; @@ -42,6 +50,14 @@ class PartialClauseRewriter { markAsDone(literal); return; } + if (callLiteral instanceof CountLowerBoundLiteral countLowerBoundLiteral) { + rewriteCountLowerBound(countLowerBoundLiteral); + return; + } + if (callLiteral instanceof CountUpperBoundLiteral countUpperBoundLiteral) { + rewriteCountUpperBound(countUpperBoundLiteral); + return; + } var target = callLiteral.getTarget(); if (target instanceof Dnf dnf) { rewriteRecursively(callLiteral, dnf); @@ -61,6 +77,75 @@ class PartialClauseRewriter { } } + private void rewriteCountLowerBound(CountLowerBoundLiteral literal) { + rewriteCount(literal, "lower", Modality.MUST, MultiObjectTranslator.LOWER_CARDINALITY_VIEW, 1, IntTerms::mul, + IntTerms.INT_SUM); + } + + private void rewriteCountUpperBound(CountUpperBoundLiteral literal) { + rewriteCount(literal, "upper", Modality.MAY, MultiObjectTranslator.UPPER_CARDINALITY_VIEW, + UpperCardinalities.ONE, UpperCardinalityTerms::mul, UpperCardinalityTerms.UPPER_CARDINALITY_SUM); + } + + private void rewriteCount(ConcreteCountLiteral literal, String name, Modality modality, Constraint view, + T one, BinaryOperator> mul, Aggregator sum) { + var type = literal.getResultType(); + var target = literal.getTarget(); + var concreteness = literal.getConcreteness(); + int arity = target.arity(); + var parameters = target.getParameters(); + var literalArguments = literal.getArguments(); + var privateVariables = literal.getPrivateVariables(positiveVariables); + + var builder = Dnf.builder("%s#%s#%s".formatted(target.name(), concreteness, name)); + var rewrittenArguments = new ArrayList(parameters.size()); + var variablesToCount = new ArrayList(); + var helperArguments = new ArrayList(); + var literalToRewrittenArgumentMap = new HashMap(); + for (int i = 0; i < arity; i++) { + var literalArgument = literalArguments.get(i); + var parameter = parameters.get(i); + var rewrittenArgument = literalToRewrittenArgumentMap.computeIfAbsent(literalArgument, key -> { + helperArguments.add(key); + var newArgument = builder.parameter(parameter); + if (privateVariables.contains(key)) { + variablesToCount.add(newArgument); + } + return newArgument; + }); + rewrittenArguments.add(rewrittenArgument); + } + var outputVariable = builder.parameter(type); + + var literals = new ArrayList(); + literals.add(new ModalConstraint(modality, literal.getConcreteness(), target) + .call(CallPolarity.POSITIVE, rewrittenArguments)); + switch (variablesToCount.size()) { + case 0 -> literals.add(outputVariable.assign(new ConstantTerm<>(type, one))); + case 1 -> literals.add(view.call(variablesToCount.get(0), + outputVariable)); + default -> { + var firstCount = Variable.of(type); + literals.add(view.call(variablesToCount.get(0), firstCount)); + int length = variablesToCount.size(); + Term accumulator = firstCount; + for (int i = 1; i < length; i++) { + var countVariable = Variable.of(type); + literals.add(view.call(variablesToCount.get(i), countVariable)); + accumulator = mul.apply(accumulator, countVariable); + } + literals.add(outputVariable.assign(accumulator)); + } + } + builder.clause(literals); + + var helperQuery = builder.build(); + var aggregationVariable = Variable.of(type); + helperArguments.add(aggregationVariable); + workList.addFirst(literal.getResultVariable().assign(helperQuery.aggregateBy(aggregationVariable, sum, + helperArguments))); + } + private void markAsDone(Literal literal) { completedLiterals.add(literal); positiveVariables.addAll(literal.getOutputVariables()); @@ -75,7 +160,7 @@ class PartialClauseRewriter { private void rewriteRecursively(AbstractCallLiteral callLiteral, Dnf dnf) { var rewrittenDnf = rewriter.rewrite(dnf); var rewrittenLiteral = callLiteral.withTarget(rewrittenDnf); - completedLiterals.add(rewrittenLiteral); + markAsDone(rewrittenLiteral); } 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 { literal instanceof AssignLiteral || literal instanceof CheckLiteral) { return literal; - } else if (literal instanceof CountLiteral) { + } else if (literal instanceof AbstractCountLiteral) { throw new IllegalArgumentException("Count literal %s cannot be lifted".formatted(literal)); - } else if (literal instanceof AggregationLiteral) { + } else if (literal instanceof AggregationLiteral) { throw new IllegalArgumentException("Aggregation literal %s cannot be lifted".formatted(literal)); } else if (literal instanceof RepresentativeElectionLiteral) { 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 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.literal; + +import tools.refinery.store.query.Constraint; +import tools.refinery.store.query.equality.LiteralEqualityHelper; +import tools.refinery.store.query.equality.LiteralHashCodeHelper; +import tools.refinery.store.query.literal.AbstractCountLiteral; +import tools.refinery.store.query.literal.Literal; +import tools.refinery.store.query.term.DataVariable; +import tools.refinery.store.query.term.Variable; + +import java.util.List; +import java.util.Objects; + +// {@link Object#equals(Object)} is implemented by {@link AbstractLiteral}. +@SuppressWarnings("squid:S2160") +public abstract class ConcreteCountLiteral extends AbstractCountLiteral { + private final Concreteness concreteness; + + protected ConcreteCountLiteral(Class resultType, DataVariable resultVariable, Concreteness concreteness, + Constraint target, List arguments) { + super(resultType, resultVariable, target, arguments); + this.concreteness = concreteness; + } + + public Concreteness getConcreteness() { + return concreteness; + } + + @Override + public boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other) { + if (!super.equalsWithSubstitution(helper, other)) { + return false; + } + var otherCountLiteral = (ConcreteCountLiteral) other; + return Objects.equals(concreteness, otherCountLiteral.concreteness); + } + + @Override + public int hashCodeWithSubstitution(LiteralHashCodeHelper helper) { + return Objects.hash(super.hashCodeWithSubstitution(helper), concreteness); + } +} 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 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.literal; + +import tools.refinery.store.query.Constraint; +import tools.refinery.store.query.literal.AbstractCallLiteral; +import tools.refinery.store.query.literal.Literal; +import tools.refinery.store.query.substitution.Substitution; +import tools.refinery.store.query.term.DataVariable; +import tools.refinery.store.query.term.Variable; + +import java.util.List; + +public class CountLowerBoundLiteral extends ConcreteCountLiteral { + public CountLowerBoundLiteral(DataVariable resultVariable, Concreteness concreteness, Constraint target, + List arguments) { + super(Integer.class, resultVariable, concreteness, target, arguments); + } + + @Override + protected Integer zero() { + return 0; + } + + @Override + protected Integer one() { + return 1; + } + + @Override + protected Literal doSubstitute(Substitution substitution, List substitutedArguments) { + return new CountLowerBoundLiteral(substitution.getTypeSafeSubstitute(getResultVariable()), getConcreteness(), + getTarget(), substitutedArguments); + } + + @Override + protected AbstractCallLiteral internalWithTarget(Constraint newTarget) { + return new CountLowerBoundLiteral(getResultVariable(), getConcreteness(), newTarget, getArguments()); + } + + @Override + protected String operatorName() { + return "@LowerBound(\"%s\") count".formatted(getConcreteness()); + } +} 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 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.literal; + +import tools.refinery.store.query.Constraint; +import tools.refinery.store.query.literal.AbstractCallLiteral; +import tools.refinery.store.query.literal.Literal; +import tools.refinery.store.query.substitution.Substitution; +import tools.refinery.store.query.term.DataVariable; +import tools.refinery.store.query.term.Variable; +import tools.refinery.store.representation.cardinality.UpperCardinalities; +import tools.refinery.store.representation.cardinality.UpperCardinality; + +import java.util.List; + +public class CountUpperBoundLiteral extends ConcreteCountLiteral { + public CountUpperBoundLiteral(DataVariable resultVariable, Concreteness concreteness, + Constraint target, List arguments) { + super(UpperCardinality.class, resultVariable, concreteness, target, arguments); + } + + @Override + protected UpperCardinality zero() { + return UpperCardinalities.ZERO; + } + + @Override + protected UpperCardinality one() { + return UpperCardinalities.UNBOUNDED; + } + + @Override + protected Literal doSubstitute(Substitution substitution, List substitutedArguments) { + return new CountUpperBoundLiteral(substitution.getTypeSafeSubstitute(getResultVariable()), getConcreteness(), + getTarget(), substitutedArguments); + } + + @Override + protected AbstractCallLiteral internalWithTarget(Constraint newTarget) { + return new CountUpperBoundLiteral(getResultVariable(), getConcreteness(), newTarget, getArguments()); + } + + @Override + protected String operatorName() { + return "@UpperBound(\"%s\") count".formatted(getConcreteness()); + } +} 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 { return typedSeed; } + public boolean containsSeed(AnyPartialSymbol symbol) { + return seeds.containsKey(symbol); + } + public Cursor getCursor(PartialSymbol partialSymbol, A defaultValue) { return getSeed(partialSymbol).getCursor(defaultValue, nodeCount); } 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; import tools.refinery.store.query.literal.CallLiteral; import tools.refinery.store.query.literal.Literal; import tools.refinery.store.query.term.Variable; +import tools.refinery.store.query.view.AnySymbolView; import tools.refinery.store.reasoning.interpretation.QueryBasedRelationRewriter; import tools.refinery.store.reasoning.literal.Concreteness; import tools.refinery.store.reasoning.literal.Modality; @@ -67,7 +68,7 @@ class EqualsRelationRewriter extends QueryBasedRelationRewriter { }; } - public static EqualsRelationRewriter of(UpperCardinalityView upperCardinalityView) { + public static EqualsRelationRewriter of(AnySymbolView upperCardinalityView) { var may = Query.of("MAY_EQUALS", (builder, p1, p2) -> builder .clause( 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 @@ */ package tools.refinery.store.reasoning.translator.multiobject; +import org.jetbrains.annotations.NotNull; import tools.refinery.store.model.Model; import tools.refinery.store.reasoning.ReasoningAdapter; import tools.refinery.store.reasoning.refinement.PartialModelInitializer; @@ -26,8 +27,7 @@ class MultiObjectInitializer implements PartialModelInitializer { @Override public void initialize(Model model, ModelSeed modelSeed) { - var intervals = new CardinalityInterval[modelSeed.getNodeCount()]; - Arrays.fill(intervals, CardinalityIntervals.SET); + var intervals = initializeIntervals(modelSeed); initializeExists(intervals, modelSeed); initializeEquals(intervals, modelSeed); var countInterpretation = model.getInterpretation(countSymbol); @@ -40,7 +40,33 @@ class MultiObjectInitializer implements PartialModelInitializer { } } + @NotNull + private CardinalityInterval[] initializeIntervals(ModelSeed modelSeed) { + var intervals = new CardinalityInterval[modelSeed.getNodeCount()]; + if (modelSeed.containsSeed(MultiObjectTranslator.COUNT_SYMBOL)) { + Arrays.fill(intervals, CardinalityIntervals.ONE); + var cursor = modelSeed.getCursor(MultiObjectTranslator.COUNT_SYMBOL, CardinalityIntervals.ONE); + while (cursor.move()) { + int i = cursor.getKey().get(0); + checkNodeId(intervals, i); + intervals[i] = cursor.getValue(); + } + } else { + Arrays.fill(intervals, CardinalityIntervals.SET); + if (!modelSeed.containsSeed(ReasoningAdapter.EXISTS_SYMBOL) || + !modelSeed.containsSeed(ReasoningAdapter.EQUALS_SYMBOL)) { + throw new IllegalArgumentException("Seed for %s and %s is required if there is no seed for %s" + .formatted(ReasoningAdapter.EXISTS_SYMBOL, ReasoningAdapter.EQUALS_SYMBOL, + MultiObjectTranslator.COUNT_SYMBOL)); + } + } + return intervals; + } + private void initializeExists(CardinalityInterval[] intervals, ModelSeed modelSeed) { + if (!modelSeed.containsSeed(ReasoningAdapter.EXISTS_SYMBOL)) { + return; + } var cursor = modelSeed.getCursor(ReasoningAdapter.EXISTS_SYMBOL, TruthValue.UNKNOWN); while (cursor.move()) { int i = cursor.getKey().get(0); @@ -56,6 +82,9 @@ class MultiObjectInitializer implements PartialModelInitializer { } private void initializeEquals(CardinalityInterval[] intervals, ModelSeed modelSeed) { + if (!modelSeed.containsSeed(ReasoningAdapter.EQUALS_SYMBOL)) { + return; + } var seed = modelSeed.getSeed(ReasoningAdapter.EQUALS_SYMBOL); var cursor = seed.getCursor(TruthValue.FALSE, modelSeed.getNodeCount()); 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; import tools.refinery.store.model.ModelStoreBuilder; import tools.refinery.store.model.ModelStoreConfiguration; import tools.refinery.store.query.dnf.Query; +import tools.refinery.store.query.view.AnySymbolView; import tools.refinery.store.reasoning.ReasoningAdapter; import tools.refinery.store.reasoning.ReasoningBuilder; +import tools.refinery.store.reasoning.representation.PartialFunction; import tools.refinery.store.reasoning.translator.PartialRelationTranslator; import tools.refinery.store.reasoning.translator.RoundingMode; import tools.refinery.store.representation.Symbol; +import tools.refinery.store.representation.cardinality.CardinalityDomain; import tools.refinery.store.representation.cardinality.CardinalityInterval; import tools.refinery.store.representation.cardinality.UpperCardinalities; import tools.refinery.store.representation.cardinality.UpperCardinality; @@ -26,35 +29,37 @@ import static tools.refinery.store.query.term.uppercardinality.UpperCardinalityT import static tools.refinery.store.query.term.uppercardinality.UpperCardinalityTerms.greaterEq; public class MultiObjectTranslator implements ModelStoreConfiguration { - private final Symbol countSymbol = Symbol.of("COUNT", 1, CardinalityInterval.class, + private static final Symbol COUNT_STORAGE = Symbol.of("COUNT", 1, CardinalityInterval.class, null); - private final LowerCardinalityView lowerCardinalityView = new LowerCardinalityView(countSymbol); - private final UpperCardinalityView upperCardinalityView = new UpperCardinalityView(countSymbol); + public static final AnySymbolView LOWER_CARDINALITY_VIEW = new LowerCardinalityView(COUNT_STORAGE); + public static final AnySymbolView UPPER_CARDINALITY_VIEW = new UpperCardinalityView(COUNT_STORAGE); + public static final PartialFunction COUNT_SYMBOL = new PartialFunction<>("COUNT", 1, + CardinalityDomain.INSTANCE); @Override public void apply(ModelStoreBuilder storeBuilder) { - storeBuilder.symbol(countSymbol); + storeBuilder.symbol(COUNT_STORAGE); storeBuilder.with(PartialRelationTranslator.of(ReasoningAdapter.EXISTS_SYMBOL) .may(Query.of("MAY_EXISTS", (builder, p1) -> builder .clause(UpperCardinality.class, upper -> List.of( - upperCardinalityView.call(p1, upper), + UPPER_CARDINALITY_VIEW.call(p1, upper), check(greaterEq(upper, constant(UpperCardinalities.ONE))) )))) .must(Query.of("MUST_EXISTS", (builder, p1) -> builder .clause(Integer.class, lower -> List.of( - lowerCardinalityView.call(p1, lower), + LOWER_CARDINALITY_VIEW.call(p1, lower), check(greaterEq(lower, constant(1))) )))) .roundingMode(RoundingMode.PREFER_FALSE) - .refiner(ExistsRefiner.of(countSymbol))); + .refiner(ExistsRefiner.of(COUNT_STORAGE))); storeBuilder.with(PartialRelationTranslator.of(ReasoningAdapter.EQUALS_SYMBOL) - .rewriter(EqualsRelationRewriter.of(upperCardinalityView)) - .refiner(EqualsRefiner.of(countSymbol))); + .rewriter(EqualsRelationRewriter.of(UPPER_CARDINALITY_VIEW)) + .refiner(EqualsRefiner.of(COUNT_STORAGE))); var reasoningBuilder = storeBuilder.getAdapter(ReasoningBuilder.class); - reasoningBuilder.initializer(new MultiObjectInitializer(countSymbol)); - reasoningBuilder.storageRefiner(countSymbol, MultiObjectStorageRefiner::new); + reasoningBuilder.initializer(new MultiObjectInitializer(COUNT_STORAGE)); + reasoningBuilder.storageRefiner(COUNT_STORAGE, MultiObjectStorageRefiner::new); } } 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 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning; + +import org.junit.jupiter.api.Test; +import tools.refinery.store.model.ModelStore; +import tools.refinery.store.query.ModelQueryAdapter; +import tools.refinery.store.query.dnf.Query; +import tools.refinery.store.query.resultset.ResultSet; +import tools.refinery.store.query.term.Variable; +import tools.refinery.store.query.viatra.ViatraModelQueryAdapter; +import tools.refinery.store.reasoning.literal.Concreteness; +import tools.refinery.store.reasoning.literal.CountLowerBoundLiteral; +import tools.refinery.store.reasoning.literal.CountUpperBoundLiteral; +import tools.refinery.store.reasoning.representation.PartialRelation; +import tools.refinery.store.reasoning.seed.ModelSeed; +import tools.refinery.store.reasoning.translator.PartialRelationTranslator; +import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator; +import tools.refinery.store.representation.Symbol; +import tools.refinery.store.representation.TruthValue; +import tools.refinery.store.representation.cardinality.CardinalityIntervals; +import tools.refinery.store.representation.cardinality.UpperCardinalities; +import tools.refinery.store.representation.cardinality.UpperCardinality; +import tools.refinery.store.tuple.Tuple; + +import java.util.List; + +import static org.hamcrest.MatcherAssert.assertThat; +import static org.hamcrest.Matchers.is; +import static tools.refinery.store.query.literal.Literals.not; +import static tools.refinery.store.reasoning.literal.PartialLiterals.must; + +class ConcreteCountTest { + private static final PartialRelation person = new PartialRelation("Person", 1); + private static final PartialRelation friend = new PartialRelation("friend", 2); + + @Test + void lowerBoundZeroTest() { + var query = Query.of("LowerBound", Integer.class, (builder, p1, p2, output) -> builder.clause( + must(person.call(p1)), + must(person.call(p2)), + new CountLowerBoundLiteral(output, Concreteness.PARTIAL, friend, List.of(p1, p2)) + )); + + var modelSeed = ModelSeed.builder(2) + .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder + .put(Tuple.of(0), CardinalityIntervals.atLeast(3)) + .put(Tuple.of(1), CardinalityIntervals.atMost(7))) + .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) + .seed(friend, builder -> builder + .put(Tuple.of(0, 1), TruthValue.TRUE) + .put(Tuple.of(1, 0), TruthValue.UNKNOWN) + .put(Tuple.of(1, 1), TruthValue.ERROR)) + .build(); + + var resultSet = getResultSet(query, modelSeed); + assertThat(resultSet.get(Tuple.of(0, 0)), is(0)); + assertThat(resultSet.get(Tuple.of(0, 1)), is(1)); + assertThat(resultSet.get(Tuple.of(1, 0)), is(0)); + assertThat(resultSet.get(Tuple.of(1, 1)), is(1)); + } + + @Test + void upperBoundZeroTest() { + var query = Query.of("UpperBound", UpperCardinality.class, (builder, p1, p2, output) -> builder.clause( + must(person.call(p1)), + must(person.call(p2)), + new CountUpperBoundLiteral(output, Concreteness.PARTIAL, friend, List.of(p1, p2)) + )); + + var modelSeed = ModelSeed.builder(2) + .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder + .put(Tuple.of(0), CardinalityIntervals.atLeast(3)) + .put(Tuple.of(1), CardinalityIntervals.atMost(7))) + .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) + .seed(friend, builder -> builder + .put(Tuple.of(0, 1), TruthValue.TRUE) + .put(Tuple.of(1, 0), TruthValue.UNKNOWN) + .put(Tuple.of(1, 1), TruthValue.ERROR)) + .build(); + + var resultSet = getResultSet(query, modelSeed); + assertThat(resultSet.get(Tuple.of(0, 0)), is(UpperCardinalities.ZERO)); + assertThat(resultSet.get(Tuple.of(0, 1)), is(UpperCardinalities.ONE)); + assertThat(resultSet.get(Tuple.of(1, 0)), is(UpperCardinalities.ONE)); + assertThat(resultSet.get(Tuple.of(1, 1)), is(UpperCardinalities.ZERO)); + } + + @Test + void lowerBoundOneTest() { + var query = Query.of("LowerBound", Integer.class, (builder, p1, output) -> builder.clause( + must(person.call(p1)), + new CountLowerBoundLiteral(output, Concreteness.PARTIAL, friend, List.of(p1, Variable.of())) + )); + + var modelSeed = ModelSeed.builder(4) + .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder + .reducedValue(CardinalityIntervals.ONE) + .put(Tuple.of(1), CardinalityIntervals.atLeast(3)) + .put(Tuple.of(2), CardinalityIntervals.atMost(7))) + .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) + .seed(friend, builder -> builder + .put(Tuple.of(0, 1), TruthValue.TRUE) + .put(Tuple.of(0, 2), TruthValue.TRUE) + .put(Tuple.of(0, 3), TruthValue.TRUE) + .put(Tuple.of(1, 0), TruthValue.TRUE) + .put(Tuple.of(1, 2), TruthValue.UNKNOWN) + .put(Tuple.of(1, 3), TruthValue.UNKNOWN) + .put(Tuple.of(2, 0), TruthValue.TRUE) + .put(Tuple.of(2, 1), TruthValue.ERROR)) + .build(); + + var resultSet = getResultSet(query, modelSeed); + assertThat(resultSet.get(Tuple.of(0)), is(4)); + assertThat(resultSet.get(Tuple.of(1)), is(1)); + assertThat(resultSet.get(Tuple.of(2)), is(4)); + assertThat(resultSet.get(Tuple.of(3)), is(0)); + } + + @Test + void upperBoundOneTest() { + var query = Query.of("UpperBound", UpperCardinality.class, (builder, p1, output) -> builder.clause( + must(person.call(p1)), + new CountUpperBoundLiteral(output, Concreteness.PARTIAL, friend, List.of(p1, Variable.of())) + )); + + var modelSeed = ModelSeed.builder(4) + .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder + .reducedValue(CardinalityIntervals.ONE) + .put(Tuple.of(1), CardinalityIntervals.atLeast(3)) + .put(Tuple.of(2), CardinalityIntervals.atMost(7))) + .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) + .seed(friend, builder -> builder + .put(Tuple.of(0, 1), TruthValue.TRUE) + .put(Tuple.of(0, 2), TruthValue.TRUE) + .put(Tuple.of(0, 3), TruthValue.TRUE) + .put(Tuple.of(1, 0), TruthValue.TRUE) + .put(Tuple.of(1, 2), TruthValue.UNKNOWN) + .put(Tuple.of(1, 3), TruthValue.UNKNOWN) + .put(Tuple.of(2, 0), TruthValue.TRUE) + .put(Tuple.of(2, 1), TruthValue.ERROR)) + .build(); + + var resultSet = getResultSet(query, modelSeed); + assertThat(resultSet.get(Tuple.of(0)), is(UpperCardinalities.UNBOUNDED)); + assertThat(resultSet.get(Tuple.of(1)), is(UpperCardinalities.atMost(9))); + assertThat(resultSet.get(Tuple.of(2)), is(UpperCardinalities.ONE)); + assertThat(resultSet.get(Tuple.of(3)), is(UpperCardinalities.ZERO)); + } + + @Test + void lowerBoundTwoTest() { + var subQuery = Query.of("SubQuery", (builder, p1, p2, p3) -> builder.clause( + friend.call(p1, p2), + friend.call(p1, p3), + friend.call(p2, p3) + )); + var query = Query.of("LowerBound", Integer.class, (builder, p1, output) -> builder.clause( + must(person.call(p1)), + new CountLowerBoundLiteral(output, Concreteness.PARTIAL, subQuery.getDnf(), + List.of(p1, Variable.of(), Variable.of())) + )); + + var modelSeed = ModelSeed.builder(4) + .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder + .reducedValue(CardinalityIntervals.ONE) + .put(Tuple.of(0), CardinalityIntervals.between(5, 9)) + .put(Tuple.of(1), CardinalityIntervals.atLeast(3)) + .put(Tuple.of(2), CardinalityIntervals.atMost(7))) + .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) + .seed(friend, builder -> builder + .put(Tuple.of(0, 1), TruthValue.TRUE) + .put(Tuple.of(0, 2), TruthValue.TRUE) + .put(Tuple.of(0, 3), TruthValue.TRUE) + .put(Tuple.of(1, 0), TruthValue.TRUE) + .put(Tuple.of(1, 2), TruthValue.TRUE) + .put(Tuple.of(1, 3), TruthValue.TRUE) + .put(Tuple.of(2, 0), TruthValue.TRUE) + .put(Tuple.of(2, 1), TruthValue.ERROR)) + .build(); + + var resultSet = getResultSet(query, modelSeed); + assertThat(resultSet.get(Tuple.of(0)), is(3)); + assertThat(resultSet.get(Tuple.of(1)), is(5)); + assertThat(resultSet.get(Tuple.of(2)), is(30)); + assertThat(resultSet.get(Tuple.of(3)), is(0)); + } + + @Test + void upperBoundTwoTest() { + var subQuery = Query.of("SubQuery", (builder, p1, p2, p3) -> builder.clause( + friend.call(p1, p2), + friend.call(p1, p3), + friend.call(p2, p3) + )); + var query = Query.of("UpperBound", UpperCardinality.class, (builder, p1, output) -> builder.clause( + must(person.call(p1)), + new CountUpperBoundLiteral(output, Concreteness.PARTIAL, subQuery.getDnf(), + List.of(p1, Variable.of(), Variable.of())) + )); + + var modelSeed = ModelSeed.builder(4) + .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder + .reducedValue(CardinalityIntervals.ONE) + .put(Tuple.of(0), CardinalityIntervals.between(5, 9)) + .put(Tuple.of(1), CardinalityIntervals.atLeast(3)) + .put(Tuple.of(2), CardinalityIntervals.atMost(7))) + .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) + .seed(friend, builder -> builder + .put(Tuple.of(0, 1), TruthValue.TRUE) + .put(Tuple.of(0, 2), TruthValue.TRUE) + .put(Tuple.of(0, 3), TruthValue.TRUE) + .put(Tuple.of(1, 0), TruthValue.TRUE) + .put(Tuple.of(1, 2), TruthValue.UNKNOWN) + .put(Tuple.of(1, 3), TruthValue.UNKNOWN) + .put(Tuple.of(2, 0), TruthValue.TRUE) + .put(Tuple.of(2, 1), TruthValue.ERROR)) + .build(); + + var resultSet = getResultSet(query, modelSeed); + assertThat(resultSet.get(Tuple.of(0)), is(UpperCardinalities.UNBOUNDED)); + assertThat(resultSet.get(Tuple.of(1)), is(UpperCardinalities.atMost(135))); + assertThat(resultSet.get(Tuple.of(2)), is(UpperCardinalities.ZERO)); + assertThat(resultSet.get(Tuple.of(3)), is(UpperCardinalities.ZERO)); + } + + @Test + void lowerBoundDiagonalTest() { + var subQuery = Query.of("SubQuery", (builder, p1, p2, p3) -> builder.clause( + friend.call(p1, p2), + friend.call(p1, p3), + not(friend.call(p2, p3)) + )); + var query = Query.of("LowerBound", Integer.class, (builder, p1, output) -> builder.clause(v1 -> List.of( + must(person.call(p1)), + new CountLowerBoundLiteral(output, Concreteness.PARTIAL, subQuery.getDnf(), List.of(p1, v1, v1)) + ))); + + var modelSeed = ModelSeed.builder(4) + .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder + .reducedValue(CardinalityIntervals.ONE) + .put(Tuple.of(0), CardinalityIntervals.between(5, 9)) + .put(Tuple.of(1), CardinalityIntervals.atLeast(3)) + .put(Tuple.of(2), CardinalityIntervals.atMost(7))) + .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) + .seed(friend, builder -> builder + .put(Tuple.of(0, 1), TruthValue.TRUE) + .put(Tuple.of(0, 2), TruthValue.TRUE) + .put(Tuple.of(0, 3), TruthValue.TRUE) + .put(Tuple.of(1, 0), TruthValue.TRUE) + .put(Tuple.of(1, 2), TruthValue.UNKNOWN) + .put(Tuple.of(1, 3), TruthValue.UNKNOWN) + .put(Tuple.of(2, 0), TruthValue.TRUE) + .put(Tuple.of(2, 1), TruthValue.ERROR)) + .build(); + + var resultSet = getResultSet(query, modelSeed); + assertThat(resultSet.get(Tuple.of(0)), is(4)); + assertThat(resultSet.get(Tuple.of(1)), is(5)); + assertThat(resultSet.get(Tuple.of(2)), is(8)); + assertThat(resultSet.get(Tuple.of(3)), is(0)); + } + + @Test + void upperBoundDiagonalTest() { + var subQuery = Query.of("SubQuery", (builder, p1, p2, p3) -> builder.clause( + friend.call(p1, p2), + friend.call(p1, p3), + not(friend.call(p2, p3)) + )); + var query = Query.of("UpperBound", UpperCardinality.class, (builder, p1, output) -> builder + .clause(v1 -> List.of( + must(person.call(p1)), + new CountUpperBoundLiteral(output, Concreteness.PARTIAL, subQuery.getDnf(), + List.of(p1, v1, v1)) + ))); + + var modelSeed = ModelSeed.builder(4) + .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder + .reducedValue(CardinalityIntervals.ONE) + .put(Tuple.of(0), CardinalityIntervals.between(5, 9)) + .put(Tuple.of(1), CardinalityIntervals.atLeast(3)) + .put(Tuple.of(2), CardinalityIntervals.atMost(7))) + .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) + .seed(friend, builder -> builder + .put(Tuple.of(0, 1), TruthValue.TRUE) + .put(Tuple.of(0, 2), TruthValue.TRUE) + .put(Tuple.of(0, 3), TruthValue.TRUE) + .put(Tuple.of(1, 0), TruthValue.TRUE) + .put(Tuple.of(1, 2), TruthValue.UNKNOWN) + .put(Tuple.of(1, 3), TruthValue.UNKNOWN) + .put(Tuple.of(2, 0), TruthValue.TRUE) + .put(Tuple.of(2, 1), TruthValue.ERROR)) + .build(); + + var resultSet = getResultSet(query, modelSeed); + assertThat(resultSet.get(Tuple.of(0)), is(UpperCardinalities.UNBOUNDED)); + assertThat(resultSet.get(Tuple.of(1)), is(UpperCardinalities.atMost(17))); + assertThat(resultSet.get(Tuple.of(2)), is(UpperCardinalities.atMost(9))); + assertThat(resultSet.get(Tuple.of(3)), is(UpperCardinalities.ZERO)); + } + + private static ResultSet getResultSet(Query query, ModelSeed modelSeed) { + var personStorage = Symbol.of("Person", 1, TruthValue.class, TruthValue.FALSE); + var friendStorage = Symbol.of("friend", 2, TruthValue.class, TruthValue.FALSE); + + var store = ModelStore.builder() + .with(ViatraModelQueryAdapter.builder() + .query(query)) + .with(ReasoningAdapter.builder()) + .with(new MultiObjectTranslator()) + .with(PartialRelationTranslator.of(person) + .symbol(personStorage)) + .with(PartialRelationTranslator.of(friend) + .symbol(friendStorage)) + .build(); + + var model = store.getAdapter(ReasoningStoreAdapter.class).createInitialModel(modelSeed); + return model.getAdapter(ModelQueryAdapter.class).getResultSet(query); + } +} 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 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.representation.cardinality; + +import tools.refinery.store.representation.AbstractDomain; + +import java.util.Optional; + +// Singleton pattern, because there is only one domain for truth values. +@SuppressWarnings("squid:S6548") +public class CardinalityDomain implements AbstractDomain { + public static final CardinalityDomain INSTANCE = new CardinalityDomain(); + + private CardinalityDomain() { + } + + @Override + public Class abstractType() { + return CardinalityInterval.class; + } + + @Override + public Class concreteType() { + return Integer.class; + } + + @Override + public CardinalityInterval toAbstract(Integer concreteValue) { + return CardinalityIntervals.exactly(concreteValue); + } + + @Override + public Optional toConcrete(CardinalityInterval abstractValue) { + return isConcrete(abstractValue) ? Optional.of(abstractValue.lowerBound()) : Optional.empty(); + } + + @Override + public boolean isConcrete(CardinalityInterval abstractValue) { + if (!(abstractValue instanceof NonEmptyCardinalityInterval nonEmptyValue) || + !((nonEmptyValue.upperBound()) instanceof FiniteUpperCardinality finiteUpperCardinality)) { + return false; + } + return nonEmptyValue.lowerBound() == finiteUpperCardinality.finiteUpperBound(); + } + + @Override + public CardinalityInterval commonRefinement(CardinalityInterval leftValue, CardinalityInterval rightValue) { + return leftValue.meet(rightValue); + } + + @Override + public CardinalityInterval commonAncestor(CardinalityInterval leftValue, CardinalityInterval rightValue) { + return leftValue.join(rightValue); + } + + @Override + public CardinalityInterval unknown() { + return CardinalityIntervals.SET; + } + + @Override + public boolean isError(CardinalityInterval abstractValue) { + return abstractValue.isEmpty(); + } +} 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 { } public static CardinalityInterval between(int lowerBound, int upperBound) { - return between(lowerBound, UpperCardinalities.valueOf(upperBound)); + return between(lowerBound, UpperCardinalities.atMost(upperBound)); } public static CardinalityInterval atMost(UpperCardinality upperBound) { @@ -38,7 +38,7 @@ public final class CardinalityIntervals { } public static CardinalityInterval atMost(int upperBound) { - return atMost(UpperCardinalities.valueOf(upperBound)); + return atMost(UpperCardinalities.atMost(upperBound)); } public static CardinalityInterval atLeast(int lowerBound) { @@ -46,6 +46,6 @@ public final class CardinalityIntervals { } public static CardinalityInterval exactly(int lowerBound) { - return new NonEmptyCardinalityInterval(lowerBound, UpperCardinalities.valueOf(lowerBound)); + return new NonEmptyCardinalityInterval(lowerBound, UpperCardinalities.atMost(lowerBound)); } } 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 private UpperCardinality lift(@NotNull UpperCardinality other, IntBinaryOperator operator) { if (other instanceof FiniteUpperCardinality finiteUpperCardinality) { - return UpperCardinalities.valueOf(operator.applyAsInt(finiteUpperBound, + return UpperCardinalities.atMost(operator.applyAsInt(finiteUpperBound, finiteUpperCardinality.finiteUpperBound)); } 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 { throw new IllegalStateException("This is a static utility class and should not be instantiated directly"); } - public static UpperCardinality valueOf(int upperBound) { + public static UpperCardinality atMost(int upperBound) { if (upperBound < 0) { return UNBOUNDED; } 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 pe int compareToInt(int value); static UpperCardinality of(int upperBound) { - return UpperCardinalities.valueOf(upperBound); + return UpperCardinalities.atMost(upperBound); } } 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; import org.junit.jupiter.api.Test; import org.junit.jupiter.params.ParameterizedTest; import org.junit.jupiter.params.provider.ValueSource; -import tools.refinery.store.representation.cardinality.FiniteUpperCardinality; -import tools.refinery.store.representation.cardinality.UnboundedUpperCardinality; -import tools.refinery.store.representation.cardinality.UpperCardinalities; import static org.hamcrest.MatcherAssert.assertThat; import static org.hamcrest.Matchers.equalTo; @@ -20,14 +17,14 @@ class UpperCardinalitiesTest { @ParameterizedTest @ValueSource(ints = {0, 1, 255, 256, 1000, Integer.MAX_VALUE}) void valueOfBoundedTest(int value) { - var upperCardinality = UpperCardinalities.valueOf(value); + var upperCardinality = UpperCardinalities.atMost(value); assertThat(upperCardinality, instanceOf(FiniteUpperCardinality.class)); assertThat(((FiniteUpperCardinality) upperCardinality).finiteUpperBound(), equalTo(value)); } @Test void valueOfUnboundedTest() { - var upperCardinality = UpperCardinalities.valueOf(-1); + var upperCardinality = UpperCardinalities.atMost(-1); assertThat(upperCardinality, instanceOf(UnboundedUpperCardinality.class)); } } -- cgit v1.2.3-70-g09d2