From 9639e80f72f62940baaaf465f818e9f7ce3e265f Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Sun, 13 Aug 2023 22:23:38 +0200 Subject: feat: metamodel translator --- .../reasoning/internal/PartialClauseRewriter.java | 111 +++++-- .../store/reasoning/lifting/DnfLifter.java | 6 +- .../reasoning/literal/ConcreteCountLiteral.java | 47 --- .../literal/CountCandidateLowerBoundLiteral.java | 49 ++++ .../literal/CountCandidateUpperBoundLiteral.java | 49 ++++ .../reasoning/literal/CountLowerBoundLiteral.java | 17 +- .../reasoning/literal/CountUpperBoundLiteral.java | 19 +- .../refinement/RefinementBasedInitializer.java | 34 +++ .../translator/PartialRelationTranslator.java | 35 ++- .../ContainmentHierarchyTranslator.java | 221 ++++++++++++++ .../translator/containment/ContainmentInfo.java | 23 ++ .../containment/ContainmentLinkRefiner.java | 128 ++++++++ .../translator/containment/ContainsRefiner.java | 70 +++++ .../containment/ForbiddenContainmentLinkView.java | 21 ++ .../containment/ForbiddenContainsView.java | 21 ++ .../containment/InferredContainment.java | 37 +++ .../containment/InferredContainmentLinkView.java | 35 +++ .../containment/MustContainmentLinkView.java | 21 ++ .../translator/containment/MustContainsView.java | 21 ++ .../crossreference/CrossReferenceUtils.java | 57 ++++ .../crossreference/DirectedCrossReferenceInfo.java | 16 + .../DirectedCrossReferenceRefiner.java | 46 +++ .../DirectedCrossReferenceTranslator.java | 82 ++++++ .../UndirectedCrossReferenceInfo.java | 15 + .../UndirectedCrossReferenceRefiner.java | 44 +++ .../UndirectedCrossReferenceTranslator.java | 71 +++++ .../metamodel/ContainedTypeHierarchyBuilder.java | 32 ++ .../reasoning/translator/metamodel/Metamodel.java | 23 ++ .../translator/metamodel/MetamodelBuilder.java | 223 ++++++++++++++ .../translator/metamodel/MetamodelTranslator.java | 37 +++ .../translator/metamodel/ReferenceInfo.java | 13 + .../multiobject/EqualsRelationRewriter.java | 4 +- .../multiobject/MultiObjectTranslator.java | 4 +- .../multiplicity/ConstrainedMultiplicity.java | 36 +++ .../InvalidMultiplicityErrorTranslator.java | 115 ++++++++ .../translator/multiplicity/Multiplicity.java | 14 + .../multiplicity/UnconstrainedMultiplicity.java | 28 ++ .../opposite/OppositeInterpretation.java | 77 +++++ .../translator/opposite/OppositeRefiner.java | 32 ++ .../opposite/OppositeRelationTranslator.java | 51 ++++ .../translator/opposite/OppositeUtils.java | 22 ++ .../typehierarchy/TypeAnalysisResult.java | 6 +- .../translator/typehierarchy/TypeHierarchy.java | 7 +- .../typehierarchy/TypeHierarchyBuilder.java | 17 +- .../typehierarchy/TypeHierarchyTranslator.java | 4 +- .../translator/typehierarchy/TypeInfo.java | 12 +- .../store/reasoning/ConcreteCountTest.java | 324 --------------------- .../refinery/store/reasoning/PartialModelTest.java | 2 +- .../translator/metamodel/MetamodelTest.java | 108 +++++++ .../translator/multiobject/CandidateCountTest.java | 321 ++++++++++++++++++++ .../translator/multiobject/PartialCountTest.java | 321 ++++++++++++++++++++ 51 files changed, 2684 insertions(+), 445 deletions(-) delete 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/CountCandidateLowerBoundLiteral.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountCandidateUpperBoundLiteral.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/RefinementBasedInitializer.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentHierarchyTranslator.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentInfo.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentLinkRefiner.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainsRefiner.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ForbiddenContainmentLinkView.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ForbiddenContainsView.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/InferredContainment.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/InferredContainmentLinkView.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/MustContainmentLinkView.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/MustContainsView.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/CrossReferenceUtils.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceInfo.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceRefiner.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceTranslator.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceInfo.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceRefiner.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceTranslator.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/ContainedTypeHierarchyBuilder.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/Metamodel.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelBuilder.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelTranslator.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/ReferenceInfo.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/ConstrainedMultiplicity.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/InvalidMultiplicityErrorTranslator.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/Multiplicity.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/UnconstrainedMultiplicity.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/opposite/OppositeInterpretation.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/opposite/OppositeRefiner.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/opposite/OppositeRelationTranslator.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/opposite/OppositeUtils.java delete mode 100644 subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/ConcreteCountTest.java create mode 100644 subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelTest.java create mode 100644 subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/multiobject/CandidateCountTest.java create mode 100644 subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/multiobject/PartialCountTest.java (limited to 'subprojects/store-reasoning/src') diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialClauseRewriter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialClauseRewriter.java index c560162e..40993235 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialClauseRewriter.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialClauseRewriter.java @@ -7,8 +7,10 @@ package tools.refinery.store.reasoning.internal; import tools.refinery.store.query.Constraint; import tools.refinery.store.query.dnf.Dnf; +import tools.refinery.store.query.dnf.DnfBuilder; import tools.refinery.store.query.dnf.DnfClause; import tools.refinery.store.query.literal.AbstractCallLiteral; +import tools.refinery.store.query.literal.AbstractCountLiteral; import tools.refinery.store.query.literal.CallPolarity; import tools.refinery.store.query.literal.Literal; import tools.refinery.store.query.term.Aggregator; @@ -17,6 +19,7 @@ import tools.refinery.store.query.term.Term; import tools.refinery.store.query.term.Variable; import tools.refinery.store.query.term.int_.IntTerms; import tools.refinery.store.query.term.uppercardinality.UpperCardinalityTerms; +import tools.refinery.store.reasoning.ReasoningAdapter; import tools.refinery.store.reasoning.literal.*; import tools.refinery.store.reasoning.representation.PartialRelation; import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator; @@ -58,6 +61,14 @@ class PartialClauseRewriter { rewriteCountUpperBound(countUpperBoundLiteral); return; } + if (callLiteral instanceof CountCandidateLowerBoundLiteral countCandidateLowerBoundLiteral) { + rewriteCountCandidateLowerBound(countCandidateLowerBoundLiteral); + return; + } + if (callLiteral instanceof CountCandidateUpperBoundLiteral countCandidateUpperBoundLiteral) { + rewriteCountCandidateUpperBound(countCandidateUpperBoundLiteral); + return; + } var target = callLiteral.getTarget(); if (target instanceof Dnf dnf) { rewriteRecursively(callLiteral, dnf); @@ -78,48 +89,26 @@ class PartialClauseRewriter { } private void rewriteCountLowerBound(CountLowerBoundLiteral literal) { - rewriteCount(literal, "lower", Modality.MUST, MultiObjectTranslator.LOWER_CARDINALITY_VIEW, 1, IntTerms::mul, - IntTerms.INT_SUM); + rewritePartialCount(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, + rewritePartialCount(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) { + private void rewritePartialCount(AbstractCountLiteral 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 countResult = computeCountVariables(literal, Concreteness.PARTIAL, name); + var builder = countResult.builder(); var outputVariable = builder.parameter(type); + var variablesToCount = countResult.variablesToCount(); var literals = new ArrayList(); - literals.add(new ModalConstraint(modality, literal.getConcreteness(), target) - .call(CallPolarity.POSITIVE, rewrittenArguments)); + literals.add(new ModalConstraint(modality, Concreteness.PARTIAL, literal.getTarget()) + .call(CallPolarity.POSITIVE, countResult.rewrittenArguments())); switch (variablesToCount.size()) { case 0 -> literals.add(outputVariable.assign(new ConstantTerm<>(type, one))); case 1 -> literals.add(view.call(variablesToCount.get(0), @@ -141,11 +130,65 @@ class PartialClauseRewriter { var helperQuery = builder.build(); var aggregationVariable = Variable.of(type); + var helperArguments = countResult.helperArguments(); helperArguments.add(aggregationVariable); workList.addFirst(literal.getResultVariable().assign(helperQuery.aggregateBy(aggregationVariable, sum, helperArguments))); } + private void rewriteCountCandidateLowerBound(CountCandidateLowerBoundLiteral literal) { + rewriteCandidateCount(literal, "lower", Modality.MAY); + } + + private void rewriteCountCandidateUpperBound(CountCandidateUpperBoundLiteral literal) { + rewriteCandidateCount(literal, "upper", Modality.MUST); + } + + private void rewriteCandidateCount(AbstractCountLiteral literal, String name, Modality modality) { + var countResult = computeCountVariables(literal, Concreteness.CANDIDATE, name); + var builder = countResult.builder(); + + var literals = new ArrayList(); + literals.add(new ModalConstraint(modality, Concreteness.CANDIDATE, literal.getTarget()) + .call(CallPolarity.POSITIVE, countResult.rewrittenArguments())); + for (var variable : countResult.variablesToCount()) { + literals.add(new ModalConstraint(modality, Concreteness.CANDIDATE, ReasoningAdapter.EXISTS_SYMBOL) + .call(variable)); + } + builder.clause(literals); + + var helperQuery = builder.build(); + workList.addFirst(literal.getResultVariable().assign(helperQuery.count(countResult.helperArguments()))); + } + + private CountResult computeCountVariables(AbstractCountLiteral literal, Concreteness concreteness, + String name) { + var target = literal.getTarget(); + 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); + } + return new CountResult(builder, rewrittenArguments, helperArguments, variablesToCount); + } + private void markAsDone(Literal literal) { completedLiterals.add(literal); positiveVariables.addAll(literal.getOutputVariables()); @@ -173,4 +216,8 @@ class PartialClauseRewriter { workList.addFirst(literals.get(i)); } } + + private record CountResult(DnfBuilder builder, List rewrittenArguments, List helperArguments, + List variablesToCount) { + } } diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/DnfLifter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/DnfLifter.java index f878b674..889f595f 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/DnfLifter.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/DnfLifter.java @@ -41,7 +41,7 @@ public class DnfLifter { var modality = modalDnf.modality(); var concreteness = modalDnf.concreteness(); var dnf = modalDnf.dnf(); - var builder = Dnf.builder("%s#%s#%s".formatted(dnf.name(), modality, concreteness)); + var builder = Dnf.builder(decorateName(dnf.name(), modality, concreteness)); builder.symbolicParameters(dnf.getSymbolicParameters()); builder.functionalDependencies(dnf.getFunctionalDependencies()); for (var clause : dnf.getClauses()) { @@ -65,4 +65,8 @@ public class DnfLifter { return "%s %s %s".formatted(modality, concreteness, dnf.name()); } } + + public static String decorateName(String name, Modality modality, Concreteness concreteness) { + return "%s#%s#%s".formatted(name, modality, concreteness); + } } diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ConcreteCountLiteral.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ConcreteCountLiteral.java deleted file mode 100644 index 91b30964..00000000 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ConcreteCountLiteral.java +++ /dev/null @@ -1,47 +0,0 @@ -/* - * 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/CountCandidateLowerBoundLiteral.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountCandidateLowerBoundLiteral.java new file mode 100644 index 00000000..91dd2b72 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountCandidateLowerBoundLiteral.java @@ -0,0 +1,49 @@ +/* + * 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.AbstractCountLiteral; +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 CountCandidateLowerBoundLiteral extends AbstractCountLiteral { + public CountCandidateLowerBoundLiteral(DataVariable resultVariable, Constraint target, + List arguments) { + super(Integer.class, resultVariable, target, arguments); + } + + @Override + protected Integer zero() { + return 0; + } + + @Override + protected Integer one() { + return 1; + } + + @Override + protected Literal doSubstitute(Substitution substitution, List substitutedArguments) { + return new CountCandidateLowerBoundLiteral(substitution.getTypeSafeSubstitute(getResultVariable()), getTarget(), + substitutedArguments); + } + + @Override + public AbstractCallLiteral withArguments(Constraint newTarget, List newArguments) { + return new CountCandidateLowerBoundLiteral(getResultVariable(), newTarget, newArguments); + } + + @Override + protected String operatorName() { + return "@LowerBound(\"candidate\") count"; + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountCandidateUpperBoundLiteral.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountCandidateUpperBoundLiteral.java new file mode 100644 index 00000000..94c9399d --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountCandidateUpperBoundLiteral.java @@ -0,0 +1,49 @@ +/* + * 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.AbstractCountLiteral; +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 CountCandidateUpperBoundLiteral extends AbstractCountLiteral { + public CountCandidateUpperBoundLiteral(DataVariable resultVariable, Constraint target, + List arguments) { + super(Integer.class, resultVariable, target, arguments); + } + + @Override + protected Integer zero() { + return 0; + } + + @Override + protected Integer one() { + return 1; + } + + @Override + protected Literal doSubstitute(Substitution substitution, List substitutedArguments) { + return new CountCandidateUpperBoundLiteral(substitution.getTypeSafeSubstitute(getResultVariable()), getTarget(), + substitutedArguments); + } + + @Override + public AbstractCallLiteral withArguments(Constraint newTarget, List newArguments) { + return new CountCandidateUpperBoundLiteral(getResultVariable(), newTarget, newArguments); + } + + @Override + protected String operatorName() { + return "@UpperBound(\"candidate\") count"; + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountLowerBoundLiteral.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountLowerBoundLiteral.java index 261088fc..b75b0cab 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountLowerBoundLiteral.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountLowerBoundLiteral.java @@ -7,6 +7,7 @@ package tools.refinery.store.reasoning.literal; import tools.refinery.store.query.Constraint; import tools.refinery.store.query.literal.AbstractCallLiteral; +import tools.refinery.store.query.literal.AbstractCountLiteral; import tools.refinery.store.query.literal.Literal; import tools.refinery.store.query.substitution.Substitution; import tools.refinery.store.query.term.DataVariable; @@ -14,10 +15,10 @@ import tools.refinery.store.query.term.Variable; import java.util.List; -public class CountLowerBoundLiteral extends ConcreteCountLiteral { - public CountLowerBoundLiteral(DataVariable resultVariable, Concreteness concreteness, Constraint target, +public class CountLowerBoundLiteral extends AbstractCountLiteral { + public CountLowerBoundLiteral(DataVariable resultVariable, Constraint target, List arguments) { - super(Integer.class, resultVariable, concreteness, target, arguments); + super(Integer.class, resultVariable, target, arguments); } @Override @@ -32,17 +33,17 @@ public class CountLowerBoundLiteral extends ConcreteCountLiteral { @Override protected Literal doSubstitute(Substitution substitution, List substitutedArguments) { - return new CountLowerBoundLiteral(substitution.getTypeSafeSubstitute(getResultVariable()), getConcreteness(), - getTarget(), substitutedArguments); + return new CountLowerBoundLiteral(substitution.getTypeSafeSubstitute(getResultVariable()), getTarget(), + substitutedArguments); } @Override - protected AbstractCallLiteral internalWithTarget(Constraint newTarget) { - return new CountLowerBoundLiteral(getResultVariable(), getConcreteness(), newTarget, getArguments()); + public AbstractCallLiteral withArguments(Constraint newTarget, List newArguments) { + return new CountLowerBoundLiteral(getResultVariable(), newTarget, newArguments); } @Override protected String operatorName() { - return "@LowerBound(\"%s\") count".formatted(getConcreteness()); + return "@LowerBound(\"partial\") count"; } } diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountUpperBoundLiteral.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountUpperBoundLiteral.java index 960ded69..03842143 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountUpperBoundLiteral.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountUpperBoundLiteral.java @@ -7,6 +7,7 @@ package tools.refinery.store.reasoning.literal; import tools.refinery.store.query.Constraint; import tools.refinery.store.query.literal.AbstractCallLiteral; +import tools.refinery.store.query.literal.AbstractCountLiteral; import tools.refinery.store.query.literal.Literal; import tools.refinery.store.query.substitution.Substitution; import tools.refinery.store.query.term.DataVariable; @@ -16,10 +17,10 @@ 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); +public class CountUpperBoundLiteral extends AbstractCountLiteral { + public CountUpperBoundLiteral(DataVariable resultVariable, Constraint target, + List arguments) { + super(UpperCardinality.class, resultVariable, target, arguments); } @Override @@ -34,17 +35,17 @@ public class CountUpperBoundLiteral extends ConcreteCountLiteral substitutedArguments) { - return new CountUpperBoundLiteral(substitution.getTypeSafeSubstitute(getResultVariable()), getConcreteness(), - getTarget(), substitutedArguments); + return new CountUpperBoundLiteral(substitution.getTypeSafeSubstitute(getResultVariable()), getTarget(), + substitutedArguments); } @Override - protected AbstractCallLiteral internalWithTarget(Constraint newTarget) { - return new CountUpperBoundLiteral(getResultVariable(), getConcreteness(), newTarget, getArguments()); + public AbstractCallLiteral withArguments(Constraint newTarget, List newArguments) { + return new CountUpperBoundLiteral(getResultVariable(), newTarget, newArguments); } @Override protected String operatorName() { - return "@UpperBound(\"%s\") count".formatted(getConcreteness()); + return "@UpperBound(\"partial\") count"; } } diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/RefinementBasedInitializer.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/RefinementBasedInitializer.java new file mode 100644 index 00000000..b6bccb01 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/RefinementBasedInitializer.java @@ -0,0 +1,34 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.refinement; + +import tools.refinery.store.model.Model; +import tools.refinery.store.reasoning.ReasoningAdapter; +import tools.refinery.store.reasoning.representation.PartialSymbol; +import tools.refinery.store.reasoning.seed.ModelSeed; + +public class RefinementBasedInitializer implements PartialModelInitializer { + private final PartialSymbol partialSymbol; + + public RefinementBasedInitializer(PartialSymbol partialSymbol) { + this.partialSymbol = partialSymbol; + } + + @Override + public void initialize(Model model, ModelSeed modelSeed) { + var refiner = model.getAdapter(ReasoningAdapter.class).getRefiner(partialSymbol); + var defaultValue = partialSymbol.abstractDomain().unknown(); + var cursor = modelSeed.getCursor(partialSymbol, defaultValue); + while (cursor.move()) { + var key = cursor.getKey(); + var value = cursor.getValue(); + if (!refiner.merge(key, value)) { + throw new IllegalArgumentException("Failed to merge value %s for key %s into %s" + .formatted(value, key, partialSymbol)); + } + } + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialRelationTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialRelationTranslator.java index aee74eb3..6f9492a3 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialRelationTranslator.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialRelationTranslator.java @@ -9,6 +9,7 @@ import tools.refinery.store.model.ModelStoreBuilder; import tools.refinery.store.query.Constraint; import tools.refinery.store.query.ModelQueryBuilder; import tools.refinery.store.query.dnf.Query; +import tools.refinery.store.query.dnf.QueryBuilder; import tools.refinery.store.query.dnf.RelationalQuery; import tools.refinery.store.query.term.Variable; import tools.refinery.store.query.view.MayView; @@ -18,16 +19,20 @@ import tools.refinery.store.reasoning.interpretation.PartialInterpretation; import tools.refinery.store.reasoning.interpretation.PartialRelationRewriter; import tools.refinery.store.reasoning.interpretation.QueryBasedRelationInterpretationFactory; import tools.refinery.store.reasoning.interpretation.QueryBasedRelationRewriter; +import tools.refinery.store.reasoning.lifting.DnfLifter; import tools.refinery.store.reasoning.literal.Concreteness; import tools.refinery.store.reasoning.literal.Modality; import tools.refinery.store.reasoning.refinement.ConcreteSymbolRefiner; import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner; +import tools.refinery.store.reasoning.refinement.PartialModelInitializer; import tools.refinery.store.reasoning.refinement.StorageRefiner; import tools.refinery.store.reasoning.representation.PartialRelation; import tools.refinery.store.representation.AnySymbol; import tools.refinery.store.representation.Symbol; import tools.refinery.store.representation.TruthValue; +import java.util.function.BiConsumer; + @SuppressWarnings("UnusedReturnValue") public final class PartialRelationTranslator extends PartialSymbolTranslator { private final PartialRelation partialRelation; @@ -84,6 +89,12 @@ public final class PartialRelationTranslator extends PartialSymbolTranslator {}); + may(never); + return this; + } + public PartialRelationTranslator must(RelationalQuery must) { checkNotConfigured(); if (this.must != null) { @@ -163,20 +180,24 @@ public final class PartialRelationTranslator extends PartialSymbolTranslator callback) { int arity = partialRelation.arity(); - var queryBuilder = Query.builder(partialRelation.name()); + var queryBuilder = Query.builder(name); var parameters = new Variable[arity]; for (int i = 0; i < arity; i++) { parameters[i] = queryBuilder.parameter("p" + 1); } - queryBuilder.clause(constraint.call(parameters)); + callback.accept(queryBuilder, parameters); return queryBuilder.build(); } + private RelationalQuery createQuery(String name, Constraint constraint) { + return createQuery(name, (builder, parameters) -> builder.clause(constraint.call(parameters))); + } + private void createFallbackQueryFromRewriter() { if (rewriter != null && query == null) { - query = createQuery(partialRelation); + query = createQuery(partialRelation.name(), partialRelation); } } @@ -189,10 +210,12 @@ public final class PartialRelationTranslator extends PartialSymbolTranslator) storageSymbol; var defaultValue = typedStorageSymbol.defaultValue(); if (may == null && !defaultValue.may()) { - may = createQuery(new MayView(typedStorageSymbol)); + may = createQuery(DnfLifter.decorateName(partialRelation.name(), Modality.MAY, Concreteness.PARTIAL), + new MayView(typedStorageSymbol)); } if (must == null && !defaultValue.must()) { - must = createQuery(new MustView(typedStorageSymbol)); + must = createQuery(DnfLifter.decorateName(partialRelation.name(), Modality.MUST, Concreteness.PARTIAL), + new MustView(typedStorageSymbol)); } } diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentHierarchyTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentHierarchyTranslator.java new file mode 100644 index 00000000..9d1b8cf4 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentHierarchyTranslator.java @@ -0,0 +1,221 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.translator.containment; + +import tools.refinery.store.model.ModelStoreBuilder; +import tools.refinery.store.model.ModelStoreConfiguration; +import tools.refinery.store.query.dnf.Query; +import tools.refinery.store.query.dnf.RelationalQuery; +import tools.refinery.store.query.literal.Connectivity; +import tools.refinery.store.query.literal.Literal; +import tools.refinery.store.query.literal.RepresentativeElectionLiteral; +import tools.refinery.store.query.term.Variable; +import tools.refinery.store.query.view.AnySymbolView; +import tools.refinery.store.reasoning.lifting.DnfLifter; +import tools.refinery.store.reasoning.literal.Concreteness; +import tools.refinery.store.reasoning.literal.CountLowerBoundLiteral; +import tools.refinery.store.reasoning.literal.Modality; +import tools.refinery.store.reasoning.refinement.RefinementBasedInitializer; +import tools.refinery.store.reasoning.representation.PartialRelation; +import tools.refinery.store.reasoning.translator.PartialRelationTranslator; +import tools.refinery.store.reasoning.translator.RoundingMode; +import tools.refinery.store.reasoning.translator.multiplicity.ConstrainedMultiplicity; +import tools.refinery.store.reasoning.translator.multiplicity.InvalidMultiplicityErrorTranslator; +import tools.refinery.store.representation.Symbol; +import tools.refinery.store.representation.cardinality.CardinalityIntervals; +import tools.refinery.store.representation.cardinality.FiniteUpperCardinality; + +import java.util.ArrayList; +import java.util.List; +import java.util.Map; + +import static tools.refinery.store.query.literal.Literals.check; +import static tools.refinery.store.query.literal.Literals.not; +import static tools.refinery.store.query.term.int_.IntTerms.constant; +import static tools.refinery.store.query.term.int_.IntTerms.less; +import static tools.refinery.store.reasoning.ReasoningAdapter.EXISTS_SYMBOL; +import static tools.refinery.store.reasoning.literal.PartialLiterals.may; +import static tools.refinery.store.reasoning.literal.PartialLiterals.must; + +public class ContainmentHierarchyTranslator implements ModelStoreConfiguration { + public static final PartialRelation CONTAINED_SYMBOL = new PartialRelation("contained", 1); + public static final PartialRelation INVALID_NUMBER_OF_CONTAINERS = new PartialRelation("invalidNumberOfContainers", + 1); + public static final PartialRelation CONTAINS_SYMBOL = new PartialRelation("contains", 2); + + private final Symbol containsStorage = Symbol.of("CONTAINS", 2, InferredContainment.class, + InferredContainment.UNKNOWN); + private final AnySymbolView forbiddenContainsView = new ForbiddenContainsView(containsStorage); + private final RelationalQuery containsMayNewTargetHelper; + private final RelationalQuery containsMayExistingHelper; + private final RelationalQuery weakComponents; + private final RelationalQuery strongComponents; + private final Map containmentInfoMap; + + public ContainmentHierarchyTranslator(Map containmentInfoMap) { + this.containmentInfoMap = containmentInfoMap; + + var name = CONTAINS_SYMBOL.name(); + + containsMayNewTargetHelper = Query.of(name + "#mayNewTargetHelper", (builder, child) -> builder + .clause(Integer.class, existingContainers -> List.of( + may(CONTAINED_SYMBOL.call(child)), + new CountLowerBoundLiteral(existingContainers, CONTAINS_SYMBOL, List.of(Variable.of(), child)), + check(less(existingContainers, constant(1))) + ))); + + containsMayExistingHelper = Query.of(name + "#mayExistingHelper", (builder, parent, child) -> builder + .clause(Integer.class, existingContainers -> List.of( + must(CONTAINS_SYMBOL.call(parent, child)), + not(forbiddenContainsView.call(parent, child)) + // Violation of monotonicity: + // Containment edges violating upper multiplicity will not be marked as {@code ERROR}, but the + // {@code invalidNumberOfContainers} error pattern will already mark the node as invalid. + ))); + + var mustExistBothContains = Query.of(name + "#mustExistBoth", (builder, parent, child) -> builder.clause( + must(CONTAINS_SYMBOL.call(parent, child)), + must(EXISTS_SYMBOL.call(parent)), + must(EXISTS_SYMBOL.call(child)) + )); + + weakComponents = Query.of(name + "#weakComponents", (builder, node, representative) -> builder.clause( + new RepresentativeElectionLiteral(Connectivity.WEAK, mustExistBothContains.getDnf(), node, + representative) + )); + + strongComponents = Query.of(name + "#strongComponents", (builder, node, representative) -> builder.clause( + new RepresentativeElectionLiteral(Connectivity.STRONG, mustExistBothContains.getDnf(), node, + representative) + )); + } + + @Override + public void apply(ModelStoreBuilder storeBuilder) { + storeBuilder.symbol(containsStorage); + translateContains(storeBuilder); + translateInvalidNumberOfContainers(storeBuilder); + for (var entry : containmentInfoMap.entrySet()) { + var linkType = entry.getKey(); + var info = entry.getValue(); + translateContainmentLinkType(storeBuilder, linkType, info); + translateInvalidMultiplicity(storeBuilder, linkType, info); + } + } + + private void translateContainmentLinkType(ModelStoreBuilder storeBuilder, PartialRelation linkType, + ContainmentInfo info) { + var name = linkType.name(); + var sourceType = info.sourceType(); + var targetType = info.targetType(); + var upperCardinality = info.multiplicity().multiplicity().upperBound(); + + var mayNewSourceHelper = Query.of(name + "#mayNewSourceHelper", (builder, parent) -> { + var literals = new ArrayList(); + literals.add(may(sourceType.call(parent))); + if (upperCardinality instanceof FiniteUpperCardinality finiteUpperCardinality) { + var existingCount = Variable.of("existingCount", Integer.class); + literals.add(new CountLowerBoundLiteral(existingCount, linkType, List.of(parent, Variable.of()))); + literals.add(check(less(existingCount, constant(finiteUpperCardinality.finiteUpperBound())))); + } + builder.clause(literals); + }); + + var mayNewTargetHelper = Query.of(name + "#mayNewTargetHelper", (builder, child) -> builder.clause( + containsMayNewTargetHelper.call(child), + may(targetType.call(child)) + )); + + var forbiddenLinkView = new ForbiddenContainmentLinkView(containsStorage, linkType); + + var mayNewHelper = Query.of(name + "#mayNewHelper", (builder, parent, child) -> builder.clause( + mayNewSourceHelper.call(parent), + mayNewTargetHelper.call(child), + not(must(CONTAINS_SYMBOL.call(parent, child))), + not(forbiddenLinkView.call(parent, child)) + )); + + var mayExistingHelper = Query.of(name + "#mayExistingHelper", (builder, parent, child) -> builder.clause( + must(linkType.call(parent, child)), + containsMayExistingHelper.call(parent, child), + may(sourceType.call(parent)), + may(targetType.call(child)), + not(forbiddenLinkView.call(parent, child)) + // Violation of monotonicity: + // Containment edges violating upper multiplicity will not be marked as {@code ERROR}, but the + // {@code invalidNumberOfContainers} error pattern will already mark the node as invalid. + )); + + var may = Query.of(name + "#may", (builder, parent, child) -> builder + .clause( + mayNewHelper.call(parent, child), + not(weakComponents.call(parent, Variable.of())) + ) + .clause(representative -> List.of( + mayNewHelper.call(parent, child), + weakComponents.call(child, representative), + // Violation of para-consistency: + // If there is a surely existing node with at least two containers, its (transitive) containers + // will end up in the same weakly connected component, and we will spuriously mark the + // containment edge between the (transitive) containers as {@code FALSE}. However, such + // models can never be finished. + // + // Violation of monotonicity: + // if the a {@code TRUE} value is added to the representation in the previous situation, + // we'll check strongly connected components instead of weakly connected ones. Therefore, the + // view for the partial symbol will change from {@code FALSE} to {@code TRUE}. This doesn't + // affect the overall inconsistency of the partial model (due to the surely existing node + // with multiple containers). + not(weakComponents.call(child, representative)) + )) + .clause( + mayExistingHelper.call(parent, child), + not(strongComponents.call(parent, Variable.of())) + ) + .clause(representative -> List.of( + mayExistingHelper.call(parent, child), + strongComponents.call(parent, representative), + not(strongComponents.call(parent, representative)) + ))); + + storeBuilder.with(PartialRelationTranslator.of(linkType) + .may(may) + .must(Query.of(name + "#must", (builder, parent, child) -> builder.clause( + new MustContainmentLinkView(containsStorage, linkType).call(parent, child) + ))) + .roundingMode(RoundingMode.PREFER_FALSE) + .refiner(ContainmentLinkRefiner.of(linkType, containsStorage, info.sourceType(), info.targetType())) + .initializer(new RefinementBasedInitializer<>(linkType))); + } + + private void translateInvalidMultiplicity(ModelStoreBuilder storeBuilder, PartialRelation linkType, + ContainmentInfo info) { + storeBuilder.with(new InvalidMultiplicityErrorTranslator(info.sourceType(), linkType, false, + info.multiplicity())); + } + + private void translateContains(ModelStoreBuilder storeBuilder) { + var name = CONTAINS_SYMBOL.name(); + var mustName = DnfLifter.decorateName(name, Modality.MUST, Concreteness.PARTIAL); + + storeBuilder.with(PartialRelationTranslator.of(CONTAINS_SYMBOL) + .query(Query.of(name, (builder, parent, child) -> { + for (var linkType : containmentInfoMap.keySet()) { + builder.clause(linkType.call(parent, child)); + } + })) + .must(Query.of(mustName, (builder, parent, child) -> builder.clause( + new MustContainsView(containsStorage).call(parent, child) + ))) + .refiner(ContainsRefiner.of(containsStorage)) + .initializer(new RefinementBasedInitializer<>(CONTAINS_SYMBOL))); + } + + private void translateInvalidNumberOfContainers(ModelStoreBuilder storeBuilder) { + storeBuilder.with(new InvalidMultiplicityErrorTranslator(CONTAINED_SYMBOL, CONTAINS_SYMBOL, true, + ConstrainedMultiplicity.of(CardinalityIntervals.ONE, INVALID_NUMBER_OF_CONTAINERS))); + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentInfo.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentInfo.java new file mode 100644 index 00000000..1087e54d --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentInfo.java @@ -0,0 +1,23 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.translator.containment; + +import tools.refinery.store.reasoning.representation.PartialRelation; +import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity; + +public record ContainmentInfo(PartialRelation sourceType, Multiplicity multiplicity, + PartialRelation targetType) { + public ContainmentInfo { + if (sourceType.arity() != 1) { + throw new IllegalArgumentException("Expected source type %s to be of arity 1, got %d instead" + .formatted(sourceType, sourceType.arity())); + } + if (targetType.arity() != 1) { + throw new IllegalArgumentException("Expected target type %s to be of arity 1, got %d instead" + .formatted(targetType, targetType.arity())); + } + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentLinkRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentLinkRefiner.java new file mode 100644 index 00000000..497ed98f --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentLinkRefiner.java @@ -0,0 +1,128 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.translator.containment; + +import tools.refinery.store.model.Interpretation; +import tools.refinery.store.reasoning.ReasoningAdapter; +import tools.refinery.store.reasoning.refinement.AbstractPartialInterpretationRefiner; +import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner; +import tools.refinery.store.reasoning.representation.PartialRelation; +import tools.refinery.store.reasoning.representation.PartialSymbol; +import tools.refinery.store.representation.Symbol; +import tools.refinery.store.representation.TruthValue; +import tools.refinery.store.tuple.Tuple; + +import java.util.ArrayList; +import java.util.Set; + +class ContainmentLinkRefiner extends AbstractPartialInterpretationRefiner { + private final Factory factory; + private final Interpretation interpretation; + private final PartialInterpretationRefiner sourceRefiner; + private final PartialInterpretationRefiner targetRefiner; + + public ContainmentLinkRefiner(ReasoningAdapter adapter, PartialSymbol partialSymbol, + Factory factory) { + super(adapter, partialSymbol); + this.factory = factory; + interpretation = adapter.getModel().getInterpretation(factory.symbol); + sourceRefiner = adapter.getRefiner(factory.sourceType); + targetRefiner = adapter.getRefiner(factory.targetType); + } + + @Override + public boolean merge(Tuple key, TruthValue value) { + var oldValue = interpretation.get(key); + var newValue = mergeLink(oldValue, value); + if (oldValue != newValue) { + interpretation.put(key, newValue); + } + if (value.must()) { + return sourceRefiner.merge(Tuple.of(key.get(0)), TruthValue.TRUE) && + targetRefiner.merge(Tuple.of(key.get(1)), TruthValue.TRUE); + } + return true; + } + + public InferredContainment mergeLink(InferredContainment oldValue, TruthValue toMerge) { + return switch (toMerge) { + case UNKNOWN -> oldValue; + case TRUE -> mustLink(oldValue); + case FALSE -> forbidLink(oldValue); + case ERROR -> errorLink(oldValue); + }; + } + + public InferredContainment mustLink(InferredContainment oldValue) { + var mustLinks = oldValue.mustLinks(); + if (oldValue.contains().may() && mustLinks.isEmpty() && oldValue.forbiddenLinks().isEmpty()) { + return factory.trueLink; + } + if (mustLinks.contains(factory.linkType)) { + return oldValue; + } + return new InferredContainment(oldValue.contains().merge(TruthValue.TRUE), + addToSet(mustLinks, factory.linkType), oldValue.forbiddenLinks()); + } + + public InferredContainment forbidLink(InferredContainment oldValue) { + var forbiddenLinks = oldValue.forbiddenLinks(); + if (oldValue.contains() == TruthValue.UNKNOWN && oldValue.mustLinks().isEmpty() && forbiddenLinks.isEmpty()) { + return factory.falseLinkUnknownContains; + } + if (forbiddenLinks.contains(factory.linkType)) { + return oldValue; + } + return new InferredContainment(oldValue.contains(), oldValue.mustLinks(), + addToSet(forbiddenLinks, factory.linkType)); + } + + public InferredContainment errorLink(InferredContainment oldValue) { + return new InferredContainment(TruthValue.ERROR, addToSet(oldValue.mustLinks(), factory.linkType), + addToSet(oldValue.forbiddenLinks(), factory.linkType)); + } + + private static Set addToSet(Set oldSet, PartialRelation linkType) { + if (oldSet.isEmpty()) { + return Set.of(linkType); + } + var newElements = new ArrayList(oldSet.size() + 1); + newElements.addAll(oldSet); + newElements.add(linkType); + return Set.copyOf(newElements); + } + + public static PartialInterpretationRefiner.Factory of( + PartialRelation linkType, Symbol symbol, PartialRelation sourceType, + PartialRelation targetType) { + return new Factory(linkType, symbol, sourceType, targetType); + } + + private static class Factory implements PartialInterpretationRefiner.Factory { + public final PartialRelation linkType; + public final Symbol symbol; + public final PartialRelation targetType; + public final PartialRelation sourceType; + public final InferredContainment trueLink; + public final InferredContainment falseLinkUnknownContains; + + public Factory(PartialRelation linkType, Symbol symbol, PartialRelation sourceType, + PartialRelation targetType) { + this.linkType = linkType; + this.symbol = symbol; + this.sourceType = sourceType; + this.targetType = targetType; + trueLink = new InferredContainment(TruthValue.TRUE, Set.of(linkType), Set.of()); + falseLinkUnknownContains = new InferredContainment(TruthValue.FALSE, Set.of(), Set.of(linkType)); + } + + @Override + public PartialInterpretationRefiner create( + ReasoningAdapter adapter, PartialSymbol partialSymbol) { + return new ContainmentLinkRefiner(adapter, partialSymbol, this); + } + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainsRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainsRefiner.java new file mode 100644 index 00000000..b57ca095 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainsRefiner.java @@ -0,0 +1,70 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.translator.containment; + +import tools.refinery.store.model.Interpretation; +import tools.refinery.store.reasoning.ReasoningAdapter; +import tools.refinery.store.reasoning.refinement.AbstractPartialInterpretationRefiner; +import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner; +import tools.refinery.store.reasoning.representation.PartialSymbol; +import tools.refinery.store.representation.Symbol; +import tools.refinery.store.representation.TruthValue; +import tools.refinery.store.tuple.Tuple; + +import java.util.Set; + +class ContainsRefiner extends AbstractPartialInterpretationRefiner { + private static final InferredContainment CONTAINS_TRUE = new InferredContainment(TruthValue.TRUE, Set.of(), + Set.of()); + private static final InferredContainment CONTAINS_FALSE = new InferredContainment(TruthValue.FALSE, Set.of(), + Set.of()); + private static final InferredContainment CONTAINS_ERROR = new InferredContainment(TruthValue.ERROR, Set.of(), + Set.of()); + + private final PartialInterpretationRefiner containedRefiner; + private final Interpretation interpretation; + + public ContainsRefiner(ReasoningAdapter adapter, PartialSymbol partialSymbol, + Symbol symbol) { + super(adapter, partialSymbol); + containedRefiner = adapter.getRefiner(ContainmentHierarchyTranslator.CONTAINED_SYMBOL); + interpretation = adapter.getModel().getInterpretation(symbol); + } + + @Override + public boolean merge(Tuple key, TruthValue value) { + var oldValue = interpretation.get(key); + var newValue = mergeContains(oldValue, value); + if (oldValue != newValue) { + interpretation.put(key, newValue); + } + if (value.must()) { + return containedRefiner.merge(Tuple.of(key.get(1)), TruthValue.TRUE); + } + return true; + } + + public InferredContainment mergeContains(InferredContainment oldValue, TruthValue toMerge) { + var oldContains = oldValue.contains(); + var newContains = oldContains.merge(toMerge); + if (newContains == oldContains) { + return oldValue; + } + if (oldValue.mustLinks().isEmpty() && oldValue.forbiddenLinks().isEmpty()) { + return switch (toMerge) { + case UNKNOWN -> oldValue; + case TRUE -> oldContains.may() ? CONTAINS_TRUE : CONTAINS_ERROR; + case FALSE -> oldContains.must() ? CONTAINS_ERROR : CONTAINS_FALSE; + case ERROR -> CONTAINS_ERROR; + }; + } + return new InferredContainment(newContains, oldValue.mustLinks(), oldValue.forbiddenLinks()); + } + + public static Factory of(Symbol symbol) { + return (adapter, partialSymbol) -> new ContainsRefiner(adapter, partialSymbol, symbol); + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ForbiddenContainmentLinkView.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ForbiddenContainmentLinkView.java new file mode 100644 index 00000000..cf0e2971 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ForbiddenContainmentLinkView.java @@ -0,0 +1,21 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.translator.containment; + +import tools.refinery.store.reasoning.representation.PartialRelation; +import tools.refinery.store.representation.Symbol; +import tools.refinery.store.tuple.Tuple; + +class ForbiddenContainmentLinkView extends InferredContainmentLinkView { + public ForbiddenContainmentLinkView(Symbol symbol, PartialRelation link) { + super(symbol, "must", link); + } + + @Override + protected boolean doFilter(Tuple key, InferredContainment value) { + return value.forbiddenLinks().contains(link); + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ForbiddenContainsView.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ForbiddenContainsView.java new file mode 100644 index 00000000..efe674f1 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ForbiddenContainsView.java @@ -0,0 +1,21 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.translator.containment; + +import tools.refinery.store.query.view.TuplePreservingView; +import tools.refinery.store.representation.Symbol; +import tools.refinery.store.tuple.Tuple; + +class ForbiddenContainsView extends TuplePreservingView { + public ForbiddenContainsView(Symbol symbol) { + super(symbol, "contains#forbidden"); + } + + @Override + protected boolean doFilter(Tuple key, InferredContainment value) { + return !value.contains().may(); + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/InferredContainment.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/InferredContainment.java new file mode 100644 index 00000000..90802864 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/InferredContainment.java @@ -0,0 +1,37 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.translator.containment; + +import tools.refinery.store.reasoning.representation.PartialRelation; +import tools.refinery.store.representation.TruthValue; + +import java.util.Set; + +record InferredContainment(TruthValue contains, Set mustLinks, + Set forbiddenLinks) { + public static final InferredContainment UNKNOWN = new InferredContainment( + TruthValue.UNKNOWN, Set.of(), Set.of()); + + public InferredContainment(TruthValue contains, Set mustLinks, + Set forbiddenLinks) { + this.contains = adjustContains(contains, mustLinks, forbiddenLinks); + this.mustLinks = mustLinks; + this.forbiddenLinks = forbiddenLinks; + } + + private static TruthValue adjustContains(TruthValue contains, Set mustLinks, + Set forbiddenLinks) { + var result = contains; + if (!mustLinks.isEmpty()) { + result = result.merge(TruthValue.TRUE); + } + boolean hasErrorLink = mustLinks.stream().anyMatch(forbiddenLinks::contains); + if (mustLinks.size() >= 2 || hasErrorLink) { + result = result.merge(TruthValue.ERROR); + } + return result; + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/InferredContainmentLinkView.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/InferredContainmentLinkView.java new file mode 100644 index 00000000..d187ad91 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/InferredContainmentLinkView.java @@ -0,0 +1,35 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.translator.containment; + +import tools.refinery.store.query.view.TuplePreservingView; +import tools.refinery.store.reasoning.representation.PartialRelation; +import tools.refinery.store.representation.Symbol; + +import java.util.Objects; + +abstract class InferredContainmentLinkView extends TuplePreservingView { + protected final PartialRelation link; + + protected InferredContainmentLinkView(Symbol symbol, String name, PartialRelation link) { + super(symbol, link.name() + "#" + name); + this.link = link; + } + + @Override + public boolean equals(Object o) { + if (this == o) return true; + if (o == null || getClass() != o.getClass()) return false; + if (!super.equals(o)) return false; + InferredContainmentLinkView that = (InferredContainmentLinkView) o; + return Objects.equals(link, that.link); + } + + @Override + public int hashCode() { + return Objects.hash(super.hashCode(), link); + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/MustContainmentLinkView.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/MustContainmentLinkView.java new file mode 100644 index 00000000..474942d6 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/MustContainmentLinkView.java @@ -0,0 +1,21 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.translator.containment; + +import tools.refinery.store.reasoning.representation.PartialRelation; +import tools.refinery.store.representation.Symbol; +import tools.refinery.store.tuple.Tuple; + +class MustContainmentLinkView extends InferredContainmentLinkView { + public MustContainmentLinkView(Symbol symbol, PartialRelation link) { + super(symbol, "must", link); + } + + @Override + protected boolean doFilter(Tuple key, InferredContainment value) { + return value.mustLinks().contains(link); + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/MustContainsView.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/MustContainsView.java new file mode 100644 index 00000000..6bc62a59 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/MustContainsView.java @@ -0,0 +1,21 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.translator.containment; + +import tools.refinery.store.query.view.TuplePreservingView; +import tools.refinery.store.representation.Symbol; +import tools.refinery.store.tuple.Tuple; + +class MustContainsView extends TuplePreservingView { + public MustContainsView(Symbol symbol) { + super(symbol, "contains#must"); + } + + @Override + protected boolean doFilter(Tuple key, InferredContainment value) { + return value.contains().must(); + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/CrossReferenceUtils.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/CrossReferenceUtils.java new file mode 100644 index 00000000..c4a2f2b3 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/CrossReferenceUtils.java @@ -0,0 +1,57 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.translator.crossreference; + +import tools.refinery.store.query.dnf.Query; +import tools.refinery.store.query.dnf.RelationalQuery; +import tools.refinery.store.query.literal.Literal; +import tools.refinery.store.query.term.NodeVariable; +import tools.refinery.store.query.term.Variable; +import tools.refinery.store.reasoning.literal.CountLowerBoundLiteral; +import tools.refinery.store.reasoning.representation.PartialRelation; +import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity; +import tools.refinery.store.representation.cardinality.FiniteUpperCardinality; + +import java.util.ArrayList; +import java.util.List; + +import static tools.refinery.store.query.literal.Literals.check; +import static tools.refinery.store.query.term.int_.IntTerms.constant; +import static tools.refinery.store.query.term.int_.IntTerms.less; +import static tools.refinery.store.reasoning.literal.PartialLiterals.may; + +class CrossReferenceUtils { + private CrossReferenceUtils() { + throw new IllegalStateException("This is a static utility class and should not be instantiated directly"); + } + + public static RelationalQuery createMayHelper(PartialRelation linkType, PartialRelation type, + Multiplicity multiplicity, boolean inverse) { + String name; + NodeVariable variable; + List arguments; + if (inverse) { + name = "Target"; + variable = Variable.of("target"); + arguments = List.of(Variable.of("source"), variable); + } else { + name = "Source"; + variable = Variable.of("source"); + arguments = List.of(variable, Variable.of("target")); + } + var builder = Query.builder(linkType.name() + "#mayNew" + name); + builder.parameter(variable); + var literals = new ArrayList(); + literals.add(may(type.call(variable))); + if (multiplicity.multiplicity().upperBound() instanceof FiniteUpperCardinality finiteUpperCardinality) { + var existingLinks = Variable.of("existingLinks", Integer.class); + literals.add(new CountLowerBoundLiteral(existingLinks, linkType, arguments)); + literals.add(check(less(existingLinks, constant(finiteUpperCardinality.finiteUpperBound())))); + } + builder.clause(literals); + return builder.build(); + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceInfo.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceInfo.java new file mode 100644 index 00000000..d8c6a5ea --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceInfo.java @@ -0,0 +1,16 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.translator.crossreference; + +import tools.refinery.store.reasoning.representation.PartialRelation; +import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity; + +public record DirectedCrossReferenceInfo(PartialRelation sourceType, Multiplicity sourceMultiplicity, + PartialRelation targetType, Multiplicity targetMultiplicity) { + public boolean isConstrained() { + return sourceMultiplicity.isConstrained() || targetMultiplicity.isConstrained(); + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceRefiner.java new file mode 100644 index 00000000..0700f9f7 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceRefiner.java @@ -0,0 +1,46 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.translator.crossreference; + +import tools.refinery.store.reasoning.ReasoningAdapter; +import tools.refinery.store.reasoning.refinement.ConcreteSymbolRefiner; +import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner; +import tools.refinery.store.reasoning.representation.PartialRelation; +import tools.refinery.store.reasoning.representation.PartialSymbol; +import tools.refinery.store.representation.Symbol; +import tools.refinery.store.representation.TruthValue; +import tools.refinery.store.tuple.Tuple; + +class DirectedCrossReferenceRefiner extends ConcreteSymbolRefiner { + private final PartialInterpretationRefiner sourceRefiner; + private final PartialInterpretationRefiner targetRefiner; + + public DirectedCrossReferenceRefiner(ReasoningAdapter adapter, PartialSymbol partialSymbol, + Symbol concreteSymbol, PartialRelation sourceType, + PartialRelation targetType) { + super(adapter, partialSymbol, concreteSymbol); + sourceRefiner = adapter.getRefiner(sourceType); + targetRefiner = adapter.getRefiner(targetType); + } + + @Override + public boolean merge(Tuple key, TruthValue value) { + if (!super.merge(key, value)) { + return false; + } + if (value.must()) { + return sourceRefiner.merge(Tuple.of(key.get(0)), TruthValue.TRUE) && + targetRefiner.merge(Tuple.of(key.get(1)), TruthValue.TRUE); + } + return true; + } + + public static Factory of(Symbol concreteSymbol, PartialRelation sourceType, + PartialRelation targetType) { + return (adapter, partialSymbol) -> new DirectedCrossReferenceRefiner(adapter, partialSymbol, concreteSymbol, + sourceType, targetType); + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceTranslator.java new file mode 100644 index 00000000..f978aad4 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceTranslator.java @@ -0,0 +1,82 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.translator.crossreference; + +import tools.refinery.store.model.ModelStoreBuilder; +import tools.refinery.store.model.ModelStoreConfiguration; +import tools.refinery.store.query.dnf.Query; +import tools.refinery.store.query.dnf.RelationalQuery; +import tools.refinery.store.query.view.ForbiddenView; +import tools.refinery.store.reasoning.lifting.DnfLifter; +import tools.refinery.store.reasoning.literal.Concreteness; +import tools.refinery.store.reasoning.literal.Modality; +import tools.refinery.store.reasoning.refinement.RefinementBasedInitializer; +import tools.refinery.store.reasoning.representation.PartialRelation; +import tools.refinery.store.reasoning.translator.PartialRelationTranslator; +import tools.refinery.store.reasoning.translator.multiplicity.InvalidMultiplicityErrorTranslator; +import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity; +import tools.refinery.store.representation.Symbol; +import tools.refinery.store.representation.TruthValue; + +import static tools.refinery.store.query.literal.Literals.not; +import static tools.refinery.store.reasoning.literal.PartialLiterals.may; +import static tools.refinery.store.reasoning.literal.PartialLiterals.must; + +public class DirectedCrossReferenceTranslator implements ModelStoreConfiguration { + private final PartialRelation linkType; + private final DirectedCrossReferenceInfo info; + private final Symbol symbol; + + public DirectedCrossReferenceTranslator(PartialRelation linkType, DirectedCrossReferenceInfo info) { + this.linkType = linkType; + this.info = info; + symbol = Symbol.of(linkType.name(), 2, TruthValue.class, TruthValue.UNKNOWN); + } + + @Override + public void apply(ModelStoreBuilder storeBuilder) { + var name = linkType.name(); + var sourceType = info.sourceType(); + var targetType = info.targetType(); + var mayNewSource = createMayHelper(sourceType, info.sourceMultiplicity(), false); + var mayNewTarget = createMayHelper(targetType, info.targetMultiplicity(), true); + var forbiddenView = new ForbiddenView(symbol); + var mayName = DnfLifter.decorateName(name, Modality.MAY, Concreteness.PARTIAL); + + storeBuilder.with(PartialRelationTranslator.of(linkType) + .symbol(symbol) + .may(Query.of(mayName, (builder, source, target) -> { + builder.clause( + mayNewSource.call(source), + mayNewTarget.call(target), + not(forbiddenView.call(source, target)) + ); + if (info.isConstrained()) { + // Violation of monotonicity: + // Edges violating upper multiplicity will not be marked as {@code ERROR}, but the + // corresponding error pattern will already mark the node as invalid. + builder.clause( + must(linkType.call(source, target)), + not(forbiddenView.call(source, target)), + may(sourceType.call(source)), + may(targetType.call(target)) + ); + } + })) + .refiner(DirectedCrossReferenceRefiner.of(symbol, sourceType, targetType)) + .initializer(new RefinementBasedInitializer<>(linkType))); + + storeBuilder.with(new InvalidMultiplicityErrorTranslator(sourceType, linkType, false, + info.sourceMultiplicity())); + + storeBuilder.with(new InvalidMultiplicityErrorTranslator(targetType, linkType, true, + info.targetMultiplicity())); + } + + private RelationalQuery createMayHelper(PartialRelation type, Multiplicity multiplicity, boolean inverse) { + return CrossReferenceUtils.createMayHelper(linkType, type, multiplicity, inverse); + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceInfo.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceInfo.java new file mode 100644 index 00000000..fe99bc54 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceInfo.java @@ -0,0 +1,15 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.translator.crossreference; + +import tools.refinery.store.reasoning.representation.PartialRelation; +import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity; + +public record UndirectedCrossReferenceInfo(PartialRelation type, Multiplicity multiplicity) { + public boolean isConstrained() { + return multiplicity.isConstrained(); + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceRefiner.java new file mode 100644 index 00000000..43c1462b --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceRefiner.java @@ -0,0 +1,44 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.translator.crossreference; + +import tools.refinery.store.reasoning.ReasoningAdapter; +import tools.refinery.store.reasoning.refinement.ConcreteSymbolRefiner; +import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner; +import tools.refinery.store.reasoning.representation.PartialRelation; +import tools.refinery.store.reasoning.representation.PartialSymbol; +import tools.refinery.store.representation.Symbol; +import tools.refinery.store.representation.TruthValue; +import tools.refinery.store.tuple.Tuple; + +class UndirectedCrossReferenceRefiner extends ConcreteSymbolRefiner { + private final PartialInterpretationRefiner sourceRefiner; + + public UndirectedCrossReferenceRefiner(ReasoningAdapter adapter, PartialSymbol partialSymbol, + Symbol concreteSymbol, PartialRelation sourceType) { + super(adapter, partialSymbol, concreteSymbol); + sourceRefiner = adapter.getRefiner(sourceType); + } + + @Override + public boolean merge(Tuple key, TruthValue value) { + int source = key.get(0); + int target = key.get(1); + if (!super.merge(key, value) || !super.merge(Tuple.of(target, source), value)) { + return false; + } + if (value.must()) { + return sourceRefiner.merge(Tuple.of(source), TruthValue.TRUE) && + sourceRefiner.merge(Tuple.of(target), TruthValue.TRUE); + } + return true; + } + + public static Factory of(Symbol concreteSymbol, PartialRelation sourceType) { + return (adapter, partialSymbol) -> new UndirectedCrossReferenceRefiner(adapter, partialSymbol, concreteSymbol, + sourceType); + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceTranslator.java new file mode 100644 index 00000000..e599992d --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceTranslator.java @@ -0,0 +1,71 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.translator.crossreference; + +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.ForbiddenView; +import tools.refinery.store.reasoning.lifting.DnfLifter; +import tools.refinery.store.reasoning.literal.Concreteness; +import tools.refinery.store.reasoning.literal.Modality; +import tools.refinery.store.reasoning.refinement.RefinementBasedInitializer; +import tools.refinery.store.reasoning.representation.PartialRelation; +import tools.refinery.store.reasoning.translator.PartialRelationTranslator; +import tools.refinery.store.reasoning.translator.multiplicity.InvalidMultiplicityErrorTranslator; +import tools.refinery.store.representation.Symbol; +import tools.refinery.store.representation.TruthValue; + +import static tools.refinery.store.query.literal.Literals.not; +import static tools.refinery.store.reasoning.literal.PartialLiterals.may; +import static tools.refinery.store.reasoning.literal.PartialLiterals.must; + +public class UndirectedCrossReferenceTranslator implements ModelStoreConfiguration { + private final PartialRelation linkType; + private final UndirectedCrossReferenceInfo info; + private final Symbol symbol; + + public UndirectedCrossReferenceTranslator(PartialRelation linkType, UndirectedCrossReferenceInfo info) { + this.linkType = linkType; + this.info = info; + symbol = Symbol.of(linkType.name(), 2, TruthValue.class, TruthValue.UNKNOWN); + } + + @Override + public void apply(ModelStoreBuilder storeBuilder) { + var name = linkType.name(); + var type = info.type(); + var forbiddenView = new ForbiddenView(symbol); + var mayName = DnfLifter.decorateName(name, Modality.MAY, Concreteness.PARTIAL); + + var mayNewSource = CrossReferenceUtils.createMayHelper(linkType, type, info.multiplicity(), false); + + storeBuilder.with(PartialRelationTranslator.of(linkType) + .symbol(symbol) + .may(Query.of(mayName, (builder, source, target) -> { + builder.clause( + mayNewSource.call(source), + mayNewSource.call(target), + not(forbiddenView.call(source, target)) + ); + if (info.isConstrained()) { + // Violation of monotonicity: + // Edges violating upper multiplicity will not be marked as {@code ERROR}, but the + // corresponding error pattern will already mark the node as invalid. + builder.clause( + must(linkType.call(source, target)), + not(forbiddenView.call(source, target)), + may(type.call(source)), + may(type.call(target)) + ); + } + })) + .refiner(UndirectedCrossReferenceRefiner.of(symbol, type)) + .initializer(new RefinementBasedInitializer<>(linkType))); + + storeBuilder.with(new InvalidMultiplicityErrorTranslator(type, linkType, false, info.multiplicity())); + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/ContainedTypeHierarchyBuilder.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/ContainedTypeHierarchyBuilder.java new file mode 100644 index 00000000..cc43bce6 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/ContainedTypeHierarchyBuilder.java @@ -0,0 +1,32 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.translator.metamodel; + +import tools.refinery.store.reasoning.representation.PartialRelation; +import tools.refinery.store.reasoning.translator.containment.ContainmentHierarchyTranslator; +import tools.refinery.store.reasoning.translator.typehierarchy.TypeHierarchyBuilder; + +import java.util.Collection; + +public class ContainedTypeHierarchyBuilder extends TypeHierarchyBuilder { + ContainedTypeHierarchyBuilder() { + } + + boolean isInvalidType(PartialRelation type) { + return !typeInfoMap.containsKey(type); + } + + void setContainedTypes(Collection containedTypes) { + for (var containedType : containedTypes) { + var currentInfo = typeInfoMap.get(containedType); + if (currentInfo == null) { + throw new IllegalArgumentException("Invalid contained type: " + containedType); + } + var newInfo = currentInfo.addSupertype(ContainmentHierarchyTranslator.CONTAINED_SYMBOL); + typeInfoMap.put(containedType, newInfo); + } + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/Metamodel.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/Metamodel.java new file mode 100644 index 00000000..72b836ff --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/Metamodel.java @@ -0,0 +1,23 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.translator.metamodel; + +import tools.refinery.store.reasoning.representation.PartialRelation; +import tools.refinery.store.reasoning.translator.containment.ContainmentInfo; +import tools.refinery.store.reasoning.translator.crossreference.DirectedCrossReferenceInfo; +import tools.refinery.store.reasoning.translator.crossreference.UndirectedCrossReferenceInfo; +import tools.refinery.store.reasoning.translator.typehierarchy.TypeHierarchy; + +import java.util.Map; + +public record Metamodel(TypeHierarchy typeHierarchy, Map containmentHierarchy, + Map directedCrossReferences, + Map undirectedCrossReferences, + Map oppositeReferences) { + public static MetamodelBuilder builder() { + return new MetamodelBuilder(); + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelBuilder.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelBuilder.java new file mode 100644 index 00000000..92370e25 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelBuilder.java @@ -0,0 +1,223 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.translator.metamodel; + +import tools.refinery.store.reasoning.representation.PartialRelation; +import tools.refinery.store.reasoning.translator.containment.ContainmentHierarchyTranslator; +import tools.refinery.store.reasoning.translator.containment.ContainmentInfo; +import tools.refinery.store.reasoning.translator.crossreference.DirectedCrossReferenceInfo; +import tools.refinery.store.reasoning.translator.crossreference.UndirectedCrossReferenceInfo; +import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity; +import tools.refinery.store.reasoning.translator.multiplicity.UnconstrainedMultiplicity; +import tools.refinery.store.reasoning.translator.typehierarchy.TypeInfo; +import tools.refinery.store.representation.cardinality.CardinalityIntervals; + +import java.util.*; + +public class MetamodelBuilder { + private final ContainedTypeHierarchyBuilder typeHierarchyBuilder = new ContainedTypeHierarchyBuilder(); + private final Map referenceInfoMap = new LinkedHashMap<>(); + private final Set containedTypes = new HashSet<>(); + private final Map containmentHierarchy = new LinkedHashMap<>(); + private final Map directedCrossReferences = new LinkedHashMap<>(); + private final Map undirectedCrossReferences = new LinkedHashMap<>(); + private final Map oppositeReferences = new LinkedHashMap<>(); + + MetamodelBuilder() { + typeHierarchyBuilder.type(ContainmentHierarchyTranslator.CONTAINED_SYMBOL, true); + } + + public MetamodelBuilder type(PartialRelation partialRelation, TypeInfo typeInfo) { + typeHierarchyBuilder.type(partialRelation, typeInfo); + return this; + + } + + public MetamodelBuilder type(PartialRelation partialRelation, boolean abstractType, + PartialRelation... supertypes) { + typeHierarchyBuilder.type(partialRelation, abstractType, supertypes); + return this; + } + + public MetamodelBuilder type(PartialRelation partialRelation, boolean abstractType, + Collection supertypes) { + typeHierarchyBuilder.type(partialRelation, abstractType, supertypes); + return this; + } + + public MetamodelBuilder type(PartialRelation partialRelation, PartialRelation... supertypes) { + typeHierarchyBuilder.type(partialRelation, supertypes); + return this; + } + + public MetamodelBuilder type(PartialRelation partialRelation, Collection supertypes) { + typeHierarchyBuilder.type(partialRelation, supertypes); + return this; + } + + public MetamodelBuilder types(Collection> entries) { + typeHierarchyBuilder.types(entries); + return this; + } + + public MetamodelBuilder types(Map map) { + typeHierarchyBuilder.types(map); + return this; + } + + public MetamodelBuilder reference(PartialRelation linkType, ReferenceInfo info) { + if (linkType.arity() != 2) { + throw new IllegalArgumentException("Only references of arity 2 are supported, got %s with %d instead" + .formatted(linkType, linkType.arity())); + } + var putResult = referenceInfoMap.put(linkType, info); + if (putResult != null && !putResult.equals(info)) { + throw new IllegalArgumentException("Duplicate reference info for partial relation: " + linkType); + } + return this; + } + + public MetamodelBuilder reference(PartialRelation linkType, PartialRelation sourceType, boolean containment, + Multiplicity multiplicity, PartialRelation targetType, + PartialRelation opposite) { + return reference(linkType, new ReferenceInfo(containment, sourceType, multiplicity, targetType, opposite)); + } + + public MetamodelBuilder reference(PartialRelation linkType, PartialRelation sourceType, Multiplicity multiplicity, + PartialRelation targetType, PartialRelation opposite) { + return reference(linkType, sourceType, false, multiplicity, targetType, opposite); + } + + public MetamodelBuilder reference(PartialRelation linkType, PartialRelation sourceType, + boolean containment, PartialRelation targetType, PartialRelation opposite) { + return reference(linkType, sourceType, containment, UnconstrainedMultiplicity.INSTANCE, targetType, opposite); + } + + public MetamodelBuilder reference(PartialRelation linkType, PartialRelation sourceType, PartialRelation targetType, + PartialRelation opposite) { + return reference(linkType, sourceType, UnconstrainedMultiplicity.INSTANCE, targetType, opposite); + } + + public MetamodelBuilder reference(PartialRelation linkType, PartialRelation sourceType, boolean containment, + Multiplicity multiplicity, PartialRelation targetType) { + return reference(linkType, sourceType, containment, multiplicity, targetType, null); + } + + public MetamodelBuilder reference(PartialRelation linkType, PartialRelation sourceType, Multiplicity multiplicity, + PartialRelation targetType) { + return reference(linkType, sourceType, multiplicity, targetType, null); + } + + public MetamodelBuilder reference(PartialRelation linkType, PartialRelation sourceType, boolean containment, + PartialRelation targetType) { + return reference(linkType, sourceType, containment, targetType, null); + } + + public MetamodelBuilder reference(PartialRelation linkType, PartialRelation sourceType, + PartialRelation targetType) { + return reference(linkType, sourceType, targetType, null); + } + + public MetamodelBuilder references(Collection> entries) { + for (var entry : entries) { + reference(entry.getKey(), entry.getValue()); + } + return this; + } + + public MetamodelBuilder references(Map map) { + return references(map.entrySet()); + } + + public Metamodel build() { + for (var entry : referenceInfoMap.entrySet()) { + var linkType = entry.getKey(); + var info = entry.getValue(); + processReferenceInfo(linkType, info); + } + typeHierarchyBuilder.setContainedTypes(containedTypes); + var typeHierarchy = typeHierarchyBuilder.build(); + return new Metamodel(typeHierarchy, Collections.unmodifiableMap(containmentHierarchy), + Collections.unmodifiableMap(directedCrossReferences), + Collections.unmodifiableMap(undirectedCrossReferences), + Collections.unmodifiableMap(oppositeReferences)); + } + + private void processReferenceInfo(PartialRelation linkType, ReferenceInfo info) { + if (oppositeReferences.containsKey(linkType) || containmentHierarchy.containsKey(linkType)) { + // We already processed this reference while processing its opposite. + return; + } + var sourceType = info.sourceType(); + var targetType = info.targetType(); + if (typeHierarchyBuilder.isInvalidType(sourceType)) { + throw new IllegalArgumentException("Source type %s of %s is not in type hierarchy" + .formatted(sourceType, linkType)); + } + if (typeHierarchyBuilder.isInvalidType(targetType)) { + throw new IllegalArgumentException("Target type %s of %s is not in type hierarchy" + .formatted(targetType, linkType)); + } + var opposite = info.opposite(); + Multiplicity targetMultiplicity = UnconstrainedMultiplicity.INSTANCE; + if (opposite != null) { + var oppositeInfo = referenceInfoMap.get(opposite); + validateOpposite(linkType, info, opposite, oppositeInfo); + targetMultiplicity = oppositeInfo.multiplicity(); + if (oppositeInfo.containment()) { + // Skip processing this reference and process it once we encounter its containment opposite. + return; + } + if (opposite.equals(linkType)) { + if (!sourceType.equals(targetType)) { + throw new IllegalArgumentException("Target %s of undirected reference %s differs from source %s" + .formatted(targetType, linkType, sourceType)); + } + undirectedCrossReferences.put(linkType, new UndirectedCrossReferenceInfo(sourceType, + info.multiplicity())); + return; + } + oppositeReferences.put(opposite, linkType); + } + if (info.containment()) { + if (targetMultiplicity.multiplicity().meet(CardinalityIntervals.ONE).isEmpty()) { + throw new IllegalArgumentException("Invalid opposite %s with multiplicity %s of containment %s" + .formatted(opposite, targetMultiplicity, linkType)); + } + containedTypes.add(targetType); + containmentHierarchy.put(linkType, new ContainmentInfo(sourceType, info.multiplicity(), targetType)); + return; + } + directedCrossReferences.put(linkType, new DirectedCrossReferenceInfo(sourceType, info.multiplicity(), + targetType, targetMultiplicity)); + } + + private static void validateOpposite(PartialRelation linkType, ReferenceInfo info, PartialRelation opposite, + ReferenceInfo oppositeInfo) { + var sourceType = info.sourceType(); + var targetType = info.targetType(); + if (oppositeInfo == null) { + throw new IllegalArgumentException("Opposite %s of %s is not defined" + .formatted(opposite, linkType)); + } + if (!oppositeInfo.opposite().equals(linkType)) { + throw new IllegalArgumentException("Expected %s to have opposite %s, got %s instead" + .formatted(opposite, linkType, oppositeInfo.opposite())); + } + if (!oppositeInfo.sourceType().equals(targetType)) { + throw new IllegalArgumentException("Expected %s to have source type %s, got %s instead" + .formatted(opposite, targetType, oppositeInfo.sourceType())); + } + if (!oppositeInfo.targetType().equals(sourceType)) { + throw new IllegalArgumentException("Expected %s to have target type %s, got %s instead" + .formatted(opposite, sourceType, oppositeInfo.targetType())); + } + if (oppositeInfo.containment() && info.containment()) { + throw new IllegalArgumentException("Opposite %s of containment %s cannot be containment" + .formatted(opposite, linkType)); + } + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelTranslator.java new file mode 100644 index 00000000..5afa58f2 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelTranslator.java @@ -0,0 +1,37 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.translator.metamodel; + +import tools.refinery.store.model.ModelStoreBuilder; +import tools.refinery.store.model.ModelStoreConfiguration; +import tools.refinery.store.reasoning.translator.containment.ContainmentHierarchyTranslator; +import tools.refinery.store.reasoning.translator.crossreference.DirectedCrossReferenceTranslator; +import tools.refinery.store.reasoning.translator.crossreference.UndirectedCrossReferenceTranslator; +import tools.refinery.store.reasoning.translator.opposite.OppositeRelationTranslator; +import tools.refinery.store.reasoning.translator.typehierarchy.TypeHierarchyTranslator; + +public class MetamodelTranslator implements ModelStoreConfiguration { + private final Metamodel metamodel; + + public MetamodelTranslator(Metamodel metamodel) { + this.metamodel = metamodel; + } + + @Override + public void apply(ModelStoreBuilder storeBuilder) { + storeBuilder.with(new TypeHierarchyTranslator(metamodel.typeHierarchy())); + storeBuilder.with(new ContainmentHierarchyTranslator(metamodel.containmentHierarchy())); + for (var entry : metamodel.directedCrossReferences().entrySet()) { + storeBuilder.with(new DirectedCrossReferenceTranslator(entry.getKey(), entry.getValue())); + } + for (var entry : metamodel.undirectedCrossReferences().entrySet()) { + storeBuilder.with(new UndirectedCrossReferenceTranslator(entry.getKey(), entry.getValue())); + } + for (var entry : metamodel.oppositeReferences().entrySet()) { + storeBuilder.with(new OppositeRelationTranslator(entry.getKey(), entry.getValue())); + } + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/ReferenceInfo.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/ReferenceInfo.java new file mode 100644 index 00000000..9a6b4012 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/ReferenceInfo.java @@ -0,0 +1,13 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.translator.metamodel; + +import tools.refinery.store.reasoning.representation.PartialRelation; +import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity; + +public record ReferenceInfo(boolean containment, PartialRelation sourceType, Multiplicity multiplicity, + PartialRelation targetType, PartialRelation opposite) { +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/EqualsRelationRewriter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/EqualsRelationRewriter.java index 393a8769..61b9488c 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/EqualsRelationRewriter.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/EqualsRelationRewriter.java @@ -69,12 +69,12 @@ class EqualsRelationRewriter extends QueryBasedRelationRewriter { } public static EqualsRelationRewriter of(AnySymbolView upperCardinalityView) { - var may = Query.of("MAY_EQUALS", (builder, p1, p2) -> builder + var may = Query.of("equals#may", (builder, p1, p2) -> builder .clause( p1.isEquivalent(p2), upperCardinalityView.call(p1, Variable.of(UpperCardinality.class)) )); - var must = Query.of("MUST_EQUALS", (builder, p1, p2) -> builder + var must = Query.of("equals#must", (builder, p1, p2) -> builder .clause(UpperCardinality.class, upper -> List.of( p1.isEquivalent(p2), upperCardinalityView.call(p1, upper), diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectTranslator.java index 09993c80..c62557d7 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectTranslator.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectTranslator.java @@ -41,12 +41,12 @@ public class MultiObjectTranslator implements ModelStoreConfiguration { storeBuilder.symbol(COUNT_STORAGE); storeBuilder.with(PartialRelationTranslator.of(ReasoningAdapter.EXISTS_SYMBOL) - .may(Query.of("MAY_EXISTS", (builder, p1) -> builder + .may(Query.of("exists#may", (builder, p1) -> builder .clause(UpperCardinality.class, upper -> List.of( UPPER_CARDINALITY_VIEW.call(p1, upper), check(greaterEq(upper, constant(UpperCardinalities.ONE))) )))) - .must(Query.of("MUST_EXISTS", (builder, p1) -> builder + .must(Query.of("exists#must", (builder, p1) -> builder .clause(Integer.class, lower -> List.of( LOWER_CARDINALITY_VIEW.call(p1, lower), check(greaterEq(lower, constant(1))) diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/ConstrainedMultiplicity.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/ConstrainedMultiplicity.java new file mode 100644 index 00000000..e441e41e --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/ConstrainedMultiplicity.java @@ -0,0 +1,36 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.translator.multiplicity; + +import tools.refinery.store.reasoning.representation.PartialRelation; +import tools.refinery.store.representation.cardinality.CardinalityInterval; +import tools.refinery.store.representation.cardinality.CardinalityIntervals; +import tools.refinery.store.representation.cardinality.NonEmptyCardinalityInterval; + +public record ConstrainedMultiplicity(NonEmptyCardinalityInterval multiplicity, PartialRelation errorSymbol) + implements Multiplicity { + public ConstrainedMultiplicity { + if (multiplicity.equals(CardinalityIntervals.SET)) { + throw new IllegalArgumentException("Expected a constrained cardinality interval"); + } + if (errorSymbol.arity() != 1) { + throw new IllegalArgumentException("Expected error symbol %s to have arity 1, got %d instead" + .formatted(errorSymbol, errorSymbol.arity())); + } + } + + public static ConstrainedMultiplicity of(CardinalityInterval multiplicity, PartialRelation errorSymbol) { + if (!(multiplicity instanceof NonEmptyCardinalityInterval nonEmptyCardinalityInterval)) { + throw new IllegalArgumentException("Inconsistent multiplicity"); + } + return new ConstrainedMultiplicity(nonEmptyCardinalityInterval, errorSymbol); + } + + @Override + public boolean isConstrained() { + return true; + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/InvalidMultiplicityErrorTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/InvalidMultiplicityErrorTranslator.java new file mode 100644 index 00000000..522d8455 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/InvalidMultiplicityErrorTranslator.java @@ -0,0 +1,115 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.translator.multiplicity; + +import tools.refinery.store.model.ModelStoreBuilder; +import tools.refinery.store.model.ModelStoreConfiguration; +import tools.refinery.store.query.dnf.Query; +import tools.refinery.store.query.term.Variable; +import tools.refinery.store.query.term.int_.IntTerms; +import tools.refinery.store.reasoning.lifting.DnfLifter; +import tools.refinery.store.reasoning.literal.*; +import tools.refinery.store.reasoning.representation.PartialRelation; +import tools.refinery.store.reasoning.translator.PartialRelationTranslator; +import tools.refinery.store.representation.cardinality.FiniteUpperCardinality; +import tools.refinery.store.representation.cardinality.UpperCardinalities; +import tools.refinery.store.representation.cardinality.UpperCardinality; + +import java.util.List; + +import static tools.refinery.store.query.literal.Literals.check; +import static tools.refinery.store.query.term.int_.IntTerms.greater; +import static tools.refinery.store.query.term.uppercardinality.UpperCardinalityTerms.constant; +import static tools.refinery.store.query.term.uppercardinality.UpperCardinalityTerms.less; +import static tools.refinery.store.reasoning.literal.PartialLiterals.candidateMust; +import static tools.refinery.store.reasoning.literal.PartialLiterals.must; + +public class InvalidMultiplicityErrorTranslator implements ModelStoreConfiguration { + private final PartialRelation nodeType; + private final PartialRelation linkType; + private final boolean inverse; + private final Multiplicity multiplicity; + + public InvalidMultiplicityErrorTranslator(PartialRelation nodeType, PartialRelation linkType, + boolean inverse, Multiplicity multiplicity) { + if (nodeType.arity() != 1) { + throw new IllegalArgumentException("Node type must be of arity 1, got %s with arity %d instead" + .formatted(nodeType, nodeType.arity())); + } + if (linkType.arity() != 2) { + throw new IllegalArgumentException("Link type must be of arity 2, got %s with arity %d instead" + .formatted(linkType, linkType.arity())); + } + this.nodeType = nodeType; + this.linkType = linkType; + this.inverse = inverse; + this.multiplicity = multiplicity; + } + + @Override + public void apply(ModelStoreBuilder storeBuilder) { + if (!(multiplicity instanceof ConstrainedMultiplicity constrainedMultiplicity)) { + return; + } + + var name = constrainedMultiplicity.errorSymbol().name(); + var cardinalityInterval = constrainedMultiplicity.multiplicity(); + var node = Variable.of("node"); + var other = Variable.of("other"); + List arguments = inverse ? List.of(other, node) : List.of(node, other); + var mustBuilder = Query.builder(DnfLifter.decorateName(name, Modality.MUST, Concreteness.PARTIAL)) + .parameter(node); + var candidateMayBuilder = Query.builder(DnfLifter.decorateName(name, Modality.MAY, Concreteness.PARTIAL)) + .parameter(node); + var candidateMustBuilder = Query.builder(DnfLifter.decorateName(name, Modality.MUST, Concreteness.PARTIAL)) + .parameter(node); + + int lowerBound = cardinalityInterval.lowerBound(); + if (lowerBound > 0) { + var lowerBoundCardinality = UpperCardinalities.atMost(lowerBound); + mustBuilder.clause(UpperCardinality.class, existingContents -> List.of( + must(nodeType.call(node)), + new CountUpperBoundLiteral(existingContents, linkType, arguments), + check(less(existingContents, constant(lowerBoundCardinality))) + )); + candidateMayBuilder.clause(Integer.class, existingContents -> List.of( + candidateMust(nodeType.call(node)), + new CountCandidateLowerBoundLiteral(existingContents, linkType, arguments), + check(IntTerms.less(existingContents, IntTerms.constant(lowerBound))) + )); + candidateMustBuilder.clause(Integer.class, existingContents -> List.of( + candidateMust(nodeType.call(node)), + new CountCandidateUpperBoundLiteral(existingContents, linkType, arguments), + check(IntTerms.less(existingContents, IntTerms.constant(lowerBound))) + )); + } + + if (cardinalityInterval.upperBound() instanceof FiniteUpperCardinality finiteUpperCardinality) { + int upperBound = finiteUpperCardinality.finiteUpperBound(); + mustBuilder.clause(Integer.class, existingContents -> List.of( + must(nodeType.call(node)), + new CountLowerBoundLiteral(existingContents, linkType, arguments), + check(greater(existingContents, IntTerms.constant(upperBound))) + )); + candidateMayBuilder.clause(Integer.class, existingContents -> List.of( + candidateMust(nodeType.call(node)), + new CountCandidateUpperBoundLiteral(existingContents, linkType, arguments), + check(greater(existingContents, IntTerms.constant(upperBound))) + )); + candidateMustBuilder.clause(Integer.class, existingContents -> List.of( + candidateMust(nodeType.call(node)), + new CountCandidateLowerBoundLiteral(existingContents, linkType, arguments), + check(greater(existingContents, IntTerms.constant(upperBound))) + )); + } + + storeBuilder.with(PartialRelationTranslator.of(constrainedMultiplicity.errorSymbol()) + .mayNever() + .must(mustBuilder.build()) + .candidateMay(candidateMayBuilder.build()) + .candidateMust(candidateMustBuilder.build())); + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/Multiplicity.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/Multiplicity.java new file mode 100644 index 00000000..d1d6dd1e --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/Multiplicity.java @@ -0,0 +1,14 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.translator.multiplicity; + +import tools.refinery.store.representation.cardinality.CardinalityInterval; + +public sealed interface Multiplicity permits ConstrainedMultiplicity, UnconstrainedMultiplicity { + CardinalityInterval multiplicity(); + + boolean isConstrained(); +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/UnconstrainedMultiplicity.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/UnconstrainedMultiplicity.java new file mode 100644 index 00000000..2159b88c --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/UnconstrainedMultiplicity.java @@ -0,0 +1,28 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.translator.multiplicity; + +import tools.refinery.store.representation.cardinality.CardinalityInterval; +import tools.refinery.store.representation.cardinality.CardinalityIntervals; + +// Singleton implementation, because there is only a single complete interval. +@SuppressWarnings("squid:S6548") +public final class UnconstrainedMultiplicity implements Multiplicity { + public static final UnconstrainedMultiplicity INSTANCE = new UnconstrainedMultiplicity(); + + private UnconstrainedMultiplicity() { + } + + @Override + public CardinalityInterval multiplicity() { + return CardinalityIntervals.SET; + } + + @Override + public boolean isConstrained() { + return true; + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/opposite/OppositeInterpretation.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/opposite/OppositeInterpretation.java new file mode 100644 index 00000000..7290ab40 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/opposite/OppositeInterpretation.java @@ -0,0 +1,77 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.translator.opposite; + + +import tools.refinery.store.map.AnyVersionedMap; +import tools.refinery.store.map.Cursor; +import tools.refinery.store.reasoning.ReasoningAdapter; +import tools.refinery.store.reasoning.interpretation.AbstractPartialInterpretation; +import tools.refinery.store.reasoning.interpretation.PartialInterpretation; +import tools.refinery.store.reasoning.literal.Concreteness; +import tools.refinery.store.reasoning.representation.PartialSymbol; +import tools.refinery.store.tuple.Tuple; + +import java.util.Set; + +class OppositeInterpretation extends AbstractPartialInterpretation { + private final PartialInterpretation opposite; + + private OppositeInterpretation(ReasoningAdapter adapter, Concreteness concreteness, + PartialSymbol partialSymbol, PartialInterpretation opposite) { + super(adapter, concreteness, partialSymbol); + this.opposite = opposite; + } + + @Override + public A get(Tuple key) { + return opposite.get(OppositeUtils.flip(key)); + } + + @Override + public Cursor getAll() { + return new OppositeCursor<>(opposite.getAll()); + } + + public static Factory of(PartialSymbol oppositeSymbol) { + return (adapter, concreteness, partialSymbol) -> { + var opposite = adapter.getPartialInterpretation(concreteness, oppositeSymbol); + return new OppositeInterpretation<>(adapter, concreteness, partialSymbol, opposite); + }; + } + + private record OppositeCursor(Cursor opposite) implements Cursor { + @Override + public Tuple getKey() { + return OppositeUtils.flip(opposite.getKey()); + } + + @Override + public T getValue() { + return opposite.getValue(); + } + + @Override + public boolean isTerminated() { + return opposite.isTerminated(); + } + + @Override + public boolean move() { + return opposite.move(); + } + + @Override + public Set getDependingMaps() { + return opposite.getDependingMaps(); + } + + @Override + public boolean isDirty() { + return opposite.isDirty(); + } + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/opposite/OppositeRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/opposite/OppositeRefiner.java new file mode 100644 index 00000000..d09684df --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/opposite/OppositeRefiner.java @@ -0,0 +1,32 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.translator.opposite; + +import tools.refinery.store.reasoning.ReasoningAdapter; +import tools.refinery.store.reasoning.refinement.AbstractPartialInterpretationRefiner; +import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner; +import tools.refinery.store.reasoning.representation.PartialSymbol; +import tools.refinery.store.tuple.Tuple; + +public class OppositeRefiner extends AbstractPartialInterpretationRefiner { + private final PartialInterpretationRefiner opposite; + + protected OppositeRefiner(ReasoningAdapter adapter, PartialSymbol partialSymbol, + PartialSymbol oppositeSymbol) { + super(adapter, partialSymbol); + opposite = adapter.getRefiner(oppositeSymbol); + } + + @Override + public boolean merge(Tuple key, A value) { + var oppositeKey = OppositeUtils.flip(key); + return opposite.merge(oppositeKey, value); + } + + public static Factory of(PartialSymbol oppositeSymbol) { + return (adapter, partialSymbol) -> new OppositeRefiner<>(adapter, partialSymbol, oppositeSymbol); + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/opposite/OppositeRelationTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/opposite/OppositeRelationTranslator.java new file mode 100644 index 00000000..b25b9d7d --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/opposite/OppositeRelationTranslator.java @@ -0,0 +1,51 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.translator.opposite; + +import tools.refinery.store.model.ModelStoreBuilder; +import tools.refinery.store.model.ModelStoreConfiguration; +import tools.refinery.store.query.literal.AbstractCallLiteral; +import tools.refinery.store.query.literal.Literal; +import tools.refinery.store.query.term.Variable; +import tools.refinery.store.reasoning.interpretation.PartialRelationRewriter; +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.reasoning.refinement.RefinementBasedInitializer; +import tools.refinery.store.reasoning.representation.PartialRelation; +import tools.refinery.store.reasoning.translator.PartialRelationTranslator; + +import java.util.List; +import java.util.Set; + +public class OppositeRelationTranslator implements ModelStoreConfiguration, PartialRelationRewriter { + private final PartialRelation linkType; + private final PartialRelation opposite; + + public OppositeRelationTranslator(PartialRelation linkType, PartialRelation opposite) { + this.linkType = linkType; + this.opposite = opposite; + } + + @Override + public void apply(ModelStoreBuilder storeBuilder) { + storeBuilder.with(PartialRelationTranslator.of(linkType) + .rewriter(this) + .interpretation(OppositeInterpretation.of(opposite)) + .refiner(OppositeRefiner.of(opposite)) + .initializer(new RefinementBasedInitializer<>(linkType))); + } + + @Override + public List rewriteLiteral(Set positiveVariables, AbstractCallLiteral literal, + Modality modality, Concreteness concreteness) { + var arguments = literal.getArguments(); + var newArguments = List.of(arguments.get(1), arguments.get(0)); + var modalOpposite = new ModalConstraint(modality, concreteness, opposite); + var oppositeLiteral = literal.withArguments(modalOpposite, newArguments); + return List.of(oppositeLiteral); + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/opposite/OppositeUtils.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/opposite/OppositeUtils.java new file mode 100644 index 00000000..2a9e6b5d --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/opposite/OppositeUtils.java @@ -0,0 +1,22 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.translator.opposite; + +import tools.refinery.store.tuple.Tuple; +import tools.refinery.store.tuple.Tuple2; + +final class OppositeUtils { + private OppositeUtils() { + throw new IllegalStateException("This is a static utility class and should not be instantiated directly"); + } + + public static Tuple flip(Tuple tuple) { + if (!(tuple instanceof Tuple2 tuple2)) { + throw new IllegalArgumentException("Cannot flip tuple: " + tuple); + } + return Tuple.of(tuple2.value1(), tuple2.value0()); + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalysisResult.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalysisResult.java index 39a76745..ebe0d1b9 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalysisResult.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalysisResult.java @@ -10,7 +10,7 @@ import tools.refinery.store.representation.TruthValue; import java.util.*; -final class TypeAnalysisResult { +public final class TypeAnalysisResult { private final ExtendedTypeInfo extendedTypeInfo; private final List directSubtypes; private final List allExternalTypeInfoList; @@ -44,6 +44,10 @@ final class TypeAnalysisResult { return inferredType; } + public boolean isSubtypeOf(TypeAnalysisResult other) { + return extendedTypeInfo.getAllSubtypes().contains(other.type()); + } + public InferredType merge(InferredType inferredType, TruthValue value) { return switch (value) { case UNKNOWN -> inferredType; diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchy.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchy.java index 99069ab9..c32a06cb 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchy.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchy.java @@ -79,7 +79,12 @@ public class TypeHierarchy { var found = new HashSet(); var allSupertypes = extendedTypeInfo.getAllSupertypes(); for (var supertype : allSupertypes) { - found.addAll(extendedTypeInfoMap.get(supertype).getAllSupertypes()); + var supertypeInfo = extendedTypeInfoMap.get(supertype); + if (supertypeInfo == null) { + throw new IllegalArgumentException("Supertype %s of %s is missing from the type hierarchy" + .formatted(supertype, extendedTypeInfo.getType())); + } + found.addAll(supertypeInfo.getAllSupertypes()); } if (allSupertypes.addAll(found)) { changed = true; diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyBuilder.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyBuilder.java index 0fca4810..36efb878 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyBuilder.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyBuilder.java @@ -7,18 +7,19 @@ package tools.refinery.store.reasoning.translator.typehierarchy; import tools.refinery.store.reasoning.representation.PartialRelation; -import java.util.Collection; -import java.util.LinkedHashMap; -import java.util.List; -import java.util.Map; +import java.util.*; +@SuppressWarnings("UnusedReturnValue") public class TypeHierarchyBuilder { - private final Map typeInfoMap = new LinkedHashMap<>(); + protected final Map typeInfoMap = new LinkedHashMap<>(); + + protected TypeHierarchyBuilder() { + } public TypeHierarchyBuilder type(PartialRelation partialRelation, TypeInfo typeInfo) { if (partialRelation.arity() != 1) { - throw new IllegalArgumentException("Only types of arity 1 are supported, hot %d instead" - .formatted(partialRelation.arity())); + throw new IllegalArgumentException("Only types of arity 1 are supported, got %s with %d instead" + .formatted(partialRelation, partialRelation.arity())); } var putResult = typeInfoMap.put(partialRelation, typeInfo); if (putResult != null && !putResult.equals(typeInfo)) { @@ -29,7 +30,7 @@ public class TypeHierarchyBuilder { public TypeHierarchyBuilder type(PartialRelation partialRelation, boolean abstractType, PartialRelation... supertypes) { - return type(partialRelation, abstractType, List.of(supertypes)); + return type(partialRelation, abstractType, Set.of(supertypes)); } public TypeHierarchyBuilder type(PartialRelation partialRelation, boolean abstractType, diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslator.java index 6a45acd3..4bff4557 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslator.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslator.java @@ -44,7 +44,7 @@ public class TypeHierarchyTranslator implements ModelStoreConfiguration { } private ModelStoreConfiguration createPreservedTypeTranslator(PartialRelation type, TypeAnalysisResult result) { - var may = Query.of(type.name() + "#may", (builder, p1) -> { + var may = Query.of(type.name() + "#partial#may", (builder, p1) -> { if (result.isAbstractType()) { for (var subtype : result.getDirectSubtypes()) { builder.clause(PartialLiterals.may(subtype.call(p1))); @@ -54,7 +54,7 @@ public class TypeHierarchyTranslator implements ModelStoreConfiguration { } }); - var must = Query.of(type.name() + "#must", (builder, p1) -> builder.clause( + var must = Query.of(type.name() + "#partial#must", (builder, p1) -> builder.clause( new MustTypeView(typeSymbol, type).call(p1) )); diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeInfo.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeInfo.java index 68ed4089..e6bdaff2 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeInfo.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeInfo.java @@ -9,5 +9,15 @@ import tools.refinery.store.reasoning.representation.PartialRelation; import java.util.*; -public record TypeInfo(Collection supertypes, boolean abstractType) { +public record TypeInfo(Set supertypes, boolean abstractType) { + public TypeInfo(Collection supertypes, boolean abstractType) { + this(Set.copyOf(supertypes), abstractType); + } + + public TypeInfo addSupertype(PartialRelation newSupertype) { + var newSupertypes = new ArrayList(supertypes.size() + 1); + newSupertypes.addAll(supertypes); + newSupertypes.add(newSupertype); + return new TypeInfo(newSupertypes, abstractType); + } } 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 deleted file mode 100644 index 21111d7c..00000000 --- a/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/ConcreteCountTest.java +++ /dev/null @@ -1,324 +0,0 @@ -/* - * 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-reasoning/src/test/java/tools/refinery/store/reasoning/PartialModelTest.java b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/PartialModelTest.java index b2188f5d..77560a68 100644 --- a/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/PartialModelTest.java +++ b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/PartialModelTest.java @@ -49,7 +49,7 @@ class PartialModelTest { .symbol(personStorage)) .with(PartialRelationTranslator.of(friend) .symbol(friendStorage) - .may(Query.of("mayPerson", (builder, p1, p2) -> builder.clause( + .may(Query.of("mayFriend", (builder, p1, p2) -> builder.clause( may(person.call(p1)), may(person.call(p2)), not(must(EQUALS_SYMBOL.call(p1, p2))), diff --git a/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelTest.java b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelTest.java new file mode 100644 index 00000000..9e74cf02 --- /dev/null +++ b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelTest.java @@ -0,0 +1,108 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.translator.metamodel; + +import org.junit.jupiter.api.Test; +import tools.refinery.store.model.ModelStore; +import tools.refinery.store.query.viatra.ViatraModelQueryAdapter; +import tools.refinery.store.reasoning.ReasoningAdapter; +import tools.refinery.store.reasoning.ReasoningStoreAdapter; +import tools.refinery.store.reasoning.literal.Concreteness; +import tools.refinery.store.reasoning.representation.PartialRelation; +import tools.refinery.store.reasoning.seed.ModelSeed; +import tools.refinery.store.reasoning.translator.containment.ContainmentHierarchyTranslator; +import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator; +import tools.refinery.store.reasoning.translator.multiplicity.ConstrainedMultiplicity; +import tools.refinery.store.representation.TruthValue; +import tools.refinery.store.representation.cardinality.CardinalityIntervals; +import tools.refinery.store.tuple.Tuple; + +import static org.hamcrest.MatcherAssert.assertThat; +import static org.hamcrest.Matchers.is; + +class MetamodelTest { + private final PartialRelation person = new PartialRelation("Person", 1); + private final PartialRelation student = new PartialRelation("Student", 1); + private final PartialRelation teacher = new PartialRelation("Teacher", 1); + private final PartialRelation university = new PartialRelation("University", 1); + private final PartialRelation course = new PartialRelation("Course", 1); + private final PartialRelation courses = new PartialRelation("courses", 2); + private final PartialRelation location = new PartialRelation("location", 2); + private final PartialRelation lecturer = new PartialRelation("lecturer", 2); + private final PartialRelation invalidLecturerCount = new PartialRelation("invalidLecturerCount", 1); + private final PartialRelation enrolledStudents = new PartialRelation("enrolledStudents", 2); + private final PartialRelation invalidStudentCount = new PartialRelation("invalidStudentCount", 1); + + @Test + void metamodelTest() { + var metamodel = Metamodel.builder() + .type(person, true) + .type(student, person) + .type(teacher, person) + .type(university) + .type(course) + .reference(courses, university, true, course, location) + .reference(location, course, university, courses) + .reference(lecturer, course, + ConstrainedMultiplicity.of(CardinalityIntervals.ONE, invalidLecturerCount), teacher) + .reference(enrolledStudents, course, + ConstrainedMultiplicity.of(CardinalityIntervals.SOME, invalidStudentCount), student) + .build(); + + var store = ModelStore.builder() + .with(ViatraModelQueryAdapter.builder()) + .with(ReasoningAdapter.builder()) + .with(new MultiObjectTranslator()) + .with(new MetamodelTranslator(metamodel)) + .build(); + + var seed = ModelSeed.builder(5) + .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder + .reducedValue(CardinalityIntervals.ONE) + .put(Tuple.of(1), CardinalityIntervals.SET) + .put(Tuple.of(4), CardinalityIntervals.SET)) + .seed(ContainmentHierarchyTranslator.CONTAINED_SYMBOL, builder -> builder + .reducedValue(TruthValue.UNKNOWN)) + .seed(ContainmentHierarchyTranslator.CONTAINS_SYMBOL, builder -> builder + .reducedValue(TruthValue.UNKNOWN)) + .seed(person, builder -> builder.reducedValue(TruthValue.UNKNOWN)) + .seed(student, builder -> builder.reducedValue(TruthValue.UNKNOWN)) + .seed(teacher, builder -> builder.reducedValue(TruthValue.UNKNOWN)) + .seed(university, builder -> builder + .reducedValue(TruthValue.UNKNOWN) + .put(Tuple.of(0), TruthValue.TRUE)) + .seed(course, builder -> builder + .reducedValue(TruthValue.UNKNOWN) + .put(Tuple.of(2), TruthValue.TRUE)) + .seed(courses, builder -> builder.reducedValue(TruthValue.UNKNOWN)) + .seed(location, builder -> builder + .reducedValue(TruthValue.UNKNOWN) + .put(Tuple.of(1, 0), TruthValue.TRUE)) + .seed(lecturer, builder -> builder + .reducedValue(TruthValue.FALSE) + .put(Tuple.of(1, 3), TruthValue.TRUE)) + .seed(enrolledStudents, builder -> builder.reducedValue(TruthValue.UNKNOWN)) + .build(); + + var model = store.getAdapter(ReasoningStoreAdapter.class).createInitialModel(seed); + var reasoningAdapter = model.getAdapter(ReasoningAdapter.class); + + var coursesInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.PARTIAL, courses); + assertThat(coursesInterpretation.get(Tuple.of(0, 1)), is(TruthValue.TRUE)); + assertThat(coursesInterpretation.get(Tuple.of(0, 2)), is(TruthValue.UNKNOWN)); + assertThat(coursesInterpretation.get(Tuple.of(0, 3)), is(TruthValue.FALSE)); + + var invalidLecturerCountInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.PARTIAL, + invalidLecturerCount); + assertThat(invalidLecturerCountInterpretation.get(Tuple.of(1)), is(TruthValue.FALSE)); + assertThat(invalidLecturerCountInterpretation.get(Tuple.of(2)), is(TruthValue.ERROR)); + + var enrolledStudentsInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.PARTIAL, + enrolledStudents); + assertThat(enrolledStudentsInterpretation.get(Tuple.of(1, 3)), is(TruthValue.FALSE)); + assertThat(enrolledStudentsInterpretation.get(Tuple.of(1, 4)), is(TruthValue.UNKNOWN)); + } +} diff --git a/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/multiobject/CandidateCountTest.java b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/multiobject/CandidateCountTest.java new file mode 100644 index 00000000..28391ec7 --- /dev/null +++ b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/multiobject/CandidateCountTest.java @@ -0,0 +1,321 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.translator.multiobject; + +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.ReasoningAdapter; +import tools.refinery.store.reasoning.ReasoningStoreAdapter; +import tools.refinery.store.reasoning.literal.CountCandidateLowerBoundLiteral; +import tools.refinery.store.reasoning.literal.CountCandidateUpperBoundLiteral; +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.representation.Symbol; +import tools.refinery.store.representation.TruthValue; +import tools.refinery.store.representation.cardinality.CardinalityIntervals; +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 CandidateCountTest { + 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 CountCandidateLowerBoundLiteral(output, 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", Integer.class, (builder, p1, p2, output) -> builder.clause( + must(person.call(p1)), + must(person.call(p2)), + new CountCandidateUpperBoundLiteral(output, 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 lowerBoundOneTest() { + var query = Query.of("LowerBound", Integer.class, (builder, p1, output) -> builder.clause( + must(person.call(p1)), + new CountCandidateLowerBoundLiteral(output, 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(2)); + assertThat(resultSet.get(Tuple.of(1)), is(1)); + assertThat(resultSet.get(Tuple.of(2)), is(2)); + assertThat(resultSet.get(Tuple.of(3)), is(0)); + } + + @Test + void upperBoundOneTest() { + var query = Query.of("UpperBound", Integer.class, (builder, p1, output) -> builder.clause( + must(person.call(p1)), + new CountCandidateUpperBoundLiteral(output, 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(2)); + assertThat(resultSet.get(Tuple.of(1)), is(1)); + assertThat(resultSet.get(Tuple.of(2)), is(2)); + assertThat(resultSet.get(Tuple.of(3)), is(0)); + } + + @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 CountCandidateLowerBoundLiteral(output, 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(1)); + assertThat(resultSet.get(Tuple.of(1)), is(1)); + assertThat(resultSet.get(Tuple.of(2)), is(2)); + 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", Integer.class, (builder, p1, output) -> builder.clause( + must(person.call(p1)), + new CountCandidateUpperBoundLiteral(output, 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(0)); + assertThat(resultSet.get(Tuple.of(1)), is(0)); + assertThat(resultSet.get(Tuple.of(2)), is(2)); + assertThat(resultSet.get(Tuple.of(3)), is(0)); + } + + @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 CountCandidateLowerBoundLiteral(output, 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(2)); + assertThat(resultSet.get(Tuple.of(1)), is(1)); + assertThat(resultSet.get(Tuple.of(2)), is(2)); + 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", Integer.class, (builder, p1, output) -> builder + .clause(v1 -> List.of( + must(person.call(p1)), + new CountCandidateUpperBoundLiteral(output, 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(2)); + assertThat(resultSet.get(Tuple.of(1)), is(1)); + assertThat(resultSet.get(Tuple.of(2)), is(2)); + assertThat(resultSet.get(Tuple.of(3)), is(0)); + } + + 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-reasoning/src/test/java/tools/refinery/store/reasoning/translator/multiobject/PartialCountTest.java b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/multiobject/PartialCountTest.java new file mode 100644 index 00000000..64230cf6 --- /dev/null +++ b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/multiobject/PartialCountTest.java @@ -0,0 +1,321 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.translator.multiobject; + +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.ReasoningAdapter; +import tools.refinery.store.reasoning.ReasoningStoreAdapter; +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.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 PartialCountTest { + 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, 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, 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, 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, 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, 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, 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, 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, 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); + } +} -- cgit v1.2.3-54-g00ecf