From ce561c96973a83bd1b6549e877fef1892ffb16d6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Krist=C3=B3f=20Marussy?= Date: Tue, 12 Nov 2024 00:58:46 +0100 Subject: [PATCH 1/5] refactor(reasoning): support error values for exists Allow paraconsistent reasoning with unsatisfiable scope bounds. --- .../impl/FilteredInterpretation.java | 2 +- .../semantics/multiObjectExistence.problem | 4 +- .../language/semantics/ModelInitializer.java | 2 +- .../language/validation/ProblemValidator.java | 5 - .../validation/AssertionValidationTest.java | 1 - .../CardinalityInterval.java | 83 +++++++++-- .../CardinalityIntervals.java | 13 +- .../EmptyCardinalityInterval.java | 87 ----------- .../NonEmptyCardinalityInterval.java | 136 ------------------ .../CardinalityIntervalTest.java | 50 +++---- .../EmptyCardinalityIntervalTest.java | 19 --- .../FiniteCardinalityIntervalTest.java | 27 ---- .../ContainmentHierarchyTranslator.java | 2 +- .../metamodel/ReferenceInfoBuilder.java | 2 +- .../multiobject/CleanupPropagator.java | 8 +- .../translator/multiobject/ExistsRefiner.java | 8 +- .../multiobject/MultiObjectInitializer.java | 10 +- .../MultiObjectStorageRefiner.java | 2 +- .../multiobject/MultiObjectTranslator.java | 14 +- .../multiplicity/ConstrainedMultiplicity.java | 17 +-- 20 files changed, 134 insertions(+), 358 deletions(-) delete mode 100644 subprojects/logic/src/main/java/tools/refinery/logic/term/cardinalityinterval/EmptyCardinalityInterval.java delete mode 100644 subprojects/logic/src/main/java/tools/refinery/logic/term/cardinalityinterval/NonEmptyCardinalityInterval.java delete mode 100644 subprojects/logic/src/test/java/tools/refinery/logic/term/cardinalityinterval/EmptyCardinalityIntervalTest.java delete mode 100644 subprojects/logic/src/test/java/tools/refinery/logic/term/cardinalityinterval/FiniteCardinalityIntervalTest.java diff --git a/subprojects/generator/src/main/java/tools/refinery/generator/impl/FilteredInterpretation.java b/subprojects/generator/src/main/java/tools/refinery/generator/impl/FilteredInterpretation.java index 1dff02a2c..53cdba5f3 100644 --- a/subprojects/generator/src/main/java/tools/refinery/generator/impl/FilteredInterpretation.java +++ b/subprojects/generator/src/main/java/tools/refinery/generator/impl/FilteredInterpretation.java @@ -57,7 +57,7 @@ public Cursor getAll() { private boolean tupleExists(Tuple key) { int arity = key.getSize(); for (int i = 0; i < arity; i++) { - if (!existsInterpretation.get(Tuple.of(key.get(i))).may()) { + if (existsInterpretation.get(Tuple.of(key.get(i))) == TruthValue.FALSE) { return false; } } diff --git a/subprojects/generator/src/test/resources/tools/refinery/generator/semantics/multiObjectExistence.problem b/subprojects/generator/src/test/resources/tools/refinery/generator/semantics/multiObjectExistence.problem index 398e7b79f..5cb36ea91 100644 --- a/subprojects/generator/src/test/resources/tools/refinery/generator/semantics/multiObjectExistence.problem +++ b/subprojects/generator/src/test/resources/tools/refinery/generator/semantics/multiObjectExistence.problem @@ -23,10 +23,10 @@ exists(D::new). ?equals(D::new, D::new). % EXPECT CANDIDATE EXACTLY: -exists(A::new). +exists(A::new): error. equals(A::new, A::new). !exists(B::new). exists(C::new). equals(C::new, C::new). -exists(D::new). +exists(D::new): error. equals(D::new, D::new). diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java index 4732ed591..ad4273ab4 100644 --- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java +++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java @@ -418,7 +418,7 @@ private Multiplicity getMultiplicityConstraint(ReferenceDeclaration referenceDec interval = getCardinalityInterval(problemMultiplicity); } var constraint = getRelationInfo(referenceDeclaration.getInvalidMultiplicity()).partialRelation(); - return ConstrainedMultiplicity.of(interval, constraint); + return new ConstrainedMultiplicity(interval, constraint); } private static CardinalityInterval getCardinalityInterval( diff --git a/subprojects/language/src/main/java/tools/refinery/language/validation/ProblemValidator.java b/subprojects/language/src/main/java/tools/refinery/language/validation/ProblemValidator.java index c3e962071..8bb55dde4 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/validation/ProblemValidator.java +++ b/subprojects/language/src/main/java/tools/refinery/language/validation/ProblemValidator.java @@ -727,11 +727,6 @@ public void checkMultiObjectAssertion(Assertion assertion) { ProblemPackage.Literals.ASSERTION__DEFAULT, 0, UNSUPPORTED_ASSERTION_ISSUE); return; } - if (value == LogicValue.ERROR) { - acceptError("Error assertions for 'exists' and 'equals' are not supported.", assertion, - ProblemPackage.Literals.ASSERTION__DEFAULT, 0, UNSUPPORTED_ASSERTION_ISSUE); - return; - } if (isExists) { checkExistsAssertion(assertion, value); return; diff --git a/subprojects/language/src/test/java/tools/refinery/language/tests/validation/AssertionValidationTest.java b/subprojects/language/src/test/java/tools/refinery/language/tests/validation/AssertionValidationTest.java index 67bea5d61..47528128c 100644 --- a/subprojects/language/src/test/java/tools/refinery/language/tests/validation/AssertionValidationTest.java +++ b/subprojects/language/src/test/java/tools/refinery/language/tests/validation/AssertionValidationTest.java @@ -38,7 +38,6 @@ class Foo. "default exists(n).", "!exists(A).", "exists(A): error.", - "exists(n): error.", "!exists(*).", "exists(*): error.", "default equals(n, n).", diff --git a/subprojects/logic/src/main/java/tools/refinery/logic/term/cardinalityinterval/CardinalityInterval.java b/subprojects/logic/src/main/java/tools/refinery/logic/term/cardinalityinterval/CardinalityInterval.java index 996ebde51..998cc8ea7 100644 --- a/subprojects/logic/src/main/java/tools/refinery/logic/term/cardinalityinterval/CardinalityInterval.java +++ b/subprojects/logic/src/main/java/tools/refinery/logic/term/cardinalityinterval/CardinalityInterval.java @@ -5,22 +5,87 @@ */ package tools.refinery.logic.term.cardinalityinterval; +import org.jetbrains.annotations.Nullable; import tools.refinery.logic.AbstractValue; +import tools.refinery.logic.term.uppercardinality.FiniteUpperCardinality; import tools.refinery.logic.term.uppercardinality.UpperCardinality; -public sealed interface CardinalityInterval extends AbstractValue - permits NonEmptyCardinalityInterval, EmptyCardinalityInterval { - int lowerBound(); +public record CardinalityInterval(int lowerBound, UpperCardinality upperBound) + implements AbstractValue { + public CardinalityInterval { + if (lowerBound < 0) { + throw new IllegalArgumentException("lowerBound must not be negative"); + } + } - UpperCardinality upperBound(); + @Nullable + @Override + public Integer getConcrete() { + return isConcrete() ? lowerBound : null; + } - CardinalityInterval min(CardinalityInterval other); + @Override + public boolean isConcrete() { + return upperBound.compareToInt(lowerBound) == 0; + } - CardinalityInterval max(CardinalityInterval other); + @Nullable + @Override + public Integer getArbitrary() { + return isError() ? null : lowerBound; + } - CardinalityInterval add(CardinalityInterval other); + @Override + public boolean isError() { + return upperBound.compareToInt(lowerBound) < 0; + } - CardinalityInterval take(int count); + @Override + public boolean isRefinementOf(CardinalityInterval other) { + return lowerBound >= other.lowerBound && upperBound.compareTo(other.upperBound) <= 0; + } - CardinalityInterval multiply(CardinalityInterval other); + public CardinalityInterval min(CardinalityInterval other) { + return new CardinalityInterval(Math.min(lowerBound, other.lowerBound), upperBound.min(other.upperBound)); + } + + public CardinalityInterval max(CardinalityInterval other) { + return new CardinalityInterval(Math.max(lowerBound, other.lowerBound), upperBound.max(other.upperBound)); + } + + public CardinalityInterval add(CardinalityInterval other) { + return new CardinalityInterval(lowerBound + other.lowerBound, upperBound.add(other.upperBound)); + } + + public CardinalityInterval multiply(CardinalityInterval other) { + return new CardinalityInterval(lowerBound * other.lowerBound, upperBound.multiply(other.upperBound)); + } + + @Override + public CardinalityInterval meet(CardinalityInterval other) { + return new CardinalityInterval(Math.max(lowerBound, other.lowerBound), upperBound.min(other.upperBound)); + } + + @Override + public CardinalityInterval join(CardinalityInterval other) { + return new CardinalityInterval(Math.min(lowerBound, other.lowerBound), upperBound.max(other.upperBound)); + } + + @Nullable + public CardinalityInterval take(int count) { + int newLowerBound = Math.max(lowerBound - count, 0); + var newUpperBound = upperBound.take(count); + if (newUpperBound == null) { + return null; + } + return new CardinalityInterval(newLowerBound, newUpperBound); + } + + @Override + public String toString() { + if (upperBound instanceof FiniteUpperCardinality(var finiteUpperBound) && finiteUpperBound == lowerBound) { + return "[%d]".formatted(lowerBound); + } + return "[%d..%s]".formatted(lowerBound, upperBound); + } } diff --git a/subprojects/logic/src/main/java/tools/refinery/logic/term/cardinalityinterval/CardinalityIntervals.java b/subprojects/logic/src/main/java/tools/refinery/logic/term/cardinalityinterval/CardinalityIntervals.java index cb64cc0d3..a2be264e1 100644 --- a/subprojects/logic/src/main/java/tools/refinery/logic/term/cardinalityinterval/CardinalityIntervals.java +++ b/subprojects/logic/src/main/java/tools/refinery/logic/term/cardinalityinterval/CardinalityIntervals.java @@ -19,17 +19,14 @@ public final class CardinalityIntervals { public static final CardinalityInterval SOME = atLeast(1); - public static final CardinalityInterval ERROR = EmptyCardinalityInterval.INSTANCE; + public static final CardinalityInterval ERROR = between(1, UpperCardinalities.ZERO); private CardinalityIntervals() { throw new IllegalStateException("This is a static utility class and should not be instantiated directly"); } public static CardinalityInterval between(int lowerBound, UpperCardinality upperBound) { - if (upperBound.compareToInt(lowerBound) < 0) { - return ERROR; - } - return new NonEmptyCardinalityInterval(lowerBound, upperBound); + return new CardinalityInterval(lowerBound, upperBound); } public static CardinalityInterval between(int lowerBound, int upperBound) { @@ -37,7 +34,7 @@ public static CardinalityInterval between(int lowerBound, int upperBound) { } public static CardinalityInterval atMost(UpperCardinality upperBound) { - return new NonEmptyCardinalityInterval(0, upperBound); + return new CardinalityInterval(0, upperBound); } public static CardinalityInterval atMost(int upperBound) { @@ -45,10 +42,10 @@ public static CardinalityInterval atMost(int upperBound) { } public static CardinalityInterval atLeast(int lowerBound) { - return new NonEmptyCardinalityInterval(lowerBound, UpperCardinalities.UNBOUNDED); + return new CardinalityInterval(lowerBound, UpperCardinalities.UNBOUNDED); } public static CardinalityInterval exactly(int lowerBound) { - return new NonEmptyCardinalityInterval(lowerBound, UpperCardinalities.atMost(lowerBound)); + return new CardinalityInterval(lowerBound, UpperCardinalities.atMost(lowerBound)); } } diff --git a/subprojects/logic/src/main/java/tools/refinery/logic/term/cardinalityinterval/EmptyCardinalityInterval.java b/subprojects/logic/src/main/java/tools/refinery/logic/term/cardinalityinterval/EmptyCardinalityInterval.java deleted file mode 100644 index 8892b278e..000000000 --- a/subprojects/logic/src/main/java/tools/refinery/logic/term/cardinalityinterval/EmptyCardinalityInterval.java +++ /dev/null @@ -1,87 +0,0 @@ -/* - * SPDX-FileCopyrightText: 2021-2024 The Refinery Authors - * - * SPDX-License-Identifier: EPL-2.0 - */ -package tools.refinery.logic.term.cardinalityinterval; - -import org.jetbrains.annotations.Nullable; -import tools.refinery.logic.term.uppercardinality.UpperCardinalities; -import tools.refinery.logic.term.uppercardinality.UpperCardinality; - -// Singleton implementation, because there is only a single empty interval. -@SuppressWarnings("squid:S6548") -public final class EmptyCardinalityInterval implements CardinalityInterval { - static final EmptyCardinalityInterval INSTANCE = new EmptyCardinalityInterval(); - - private EmptyCardinalityInterval() { - // Singleton constructor. - } - - @Override - @Nullable - public Integer getConcrete() { - return null; - } - - @Override - @Nullable - public Integer getArbitrary() { - return null; - } - - @Override - public boolean isRefinementOf(CardinalityInterval other) { - return true; - } - - @Override - public int lowerBound() { - return 1; - } - - @Override - public UpperCardinality upperBound() { - return UpperCardinalities.ZERO; - } - - @Override - public CardinalityInterval min(CardinalityInterval other) { - return this; - } - - @Override - public CardinalityInterval max(CardinalityInterval other) { - return this; - } - - @Override - public CardinalityInterval add(CardinalityInterval other) { - return this; - } - - @Override - public CardinalityInterval take(int count) { - return this; - } - - @Override - public CardinalityInterval multiply(CardinalityInterval other) { - return this; - } - - @Override - public CardinalityInterval meet(CardinalityInterval other) { - return this; - } - - @Override - public CardinalityInterval join(CardinalityInterval other) { - return other; - } - - @Override - public String toString() { - return "error"; - } -} diff --git a/subprojects/logic/src/main/java/tools/refinery/logic/term/cardinalityinterval/NonEmptyCardinalityInterval.java b/subprojects/logic/src/main/java/tools/refinery/logic/term/cardinalityinterval/NonEmptyCardinalityInterval.java deleted file mode 100644 index d564ff66f..000000000 --- a/subprojects/logic/src/main/java/tools/refinery/logic/term/cardinalityinterval/NonEmptyCardinalityInterval.java +++ /dev/null @@ -1,136 +0,0 @@ -/* - * SPDX-FileCopyrightText: 2021-2024 The Refinery Authors - * - * SPDX-License-Identifier: EPL-2.0 - */ -package tools.refinery.logic.term.cardinalityinterval; - -import org.jetbrains.annotations.NotNull; -import org.jetbrains.annotations.Nullable; -import tools.refinery.logic.term.uppercardinality.FiniteUpperCardinality; -import tools.refinery.logic.term.uppercardinality.UpperCardinality; - -import java.util.Objects; -import java.util.function.BinaryOperator; -import java.util.function.IntBinaryOperator; - -public record NonEmptyCardinalityInterval(int lowerBound, UpperCardinality upperBound) implements CardinalityInterval { - public NonEmptyCardinalityInterval { - if (lowerBound < 0) { - throw new IllegalArgumentException("lowerBound must not be negative"); - } - if (upperBound.compareToInt(lowerBound) < 0) { - throw new IllegalArgumentException("lowerBound must not be larger than upperBound"); - } - } - - @Override - @Nullable - public Integer getConcrete() { - return isConcrete() ? lowerBound : null; - } - - @Override - public boolean isConcrete() { - return upperBound instanceof FiniteUpperCardinality(var finiteUpperBound) && finiteUpperBound == lowerBound; - } - - @Override - @NotNull - public Integer getArbitrary() { - return lowerBound; - } - - @Override - public boolean isError() { - return false; - } - - @Override - public boolean isRefinementOf(CardinalityInterval other) { - if (!(other instanceof NonEmptyCardinalityInterval(var otherLowerBound, var otherUpperBound))) { - return false; - } - return lowerBound >= otherLowerBound && upperBound.compareTo(otherUpperBound) <= 0; - } - - @Override - public CardinalityInterval min(CardinalityInterval other) { - return lift(other, Math::min, UpperCardinality::min); - } - - @Override - public CardinalityInterval max(CardinalityInterval other) { - return lift(other, Math::max, UpperCardinality::max); - } - - @Override - public CardinalityInterval add(CardinalityInterval other) { - return lift(other, Integer::sum, UpperCardinality::add); - } - - @Override - public CardinalityInterval multiply(CardinalityInterval other) { - return lift(other, (a, b) -> a * b, UpperCardinality::multiply); - } - - @Override - public CardinalityInterval meet(CardinalityInterval other) { - return lift(other, Math::max, UpperCardinality::min); - } - - @Override - public CardinalityInterval join(CardinalityInterval other) { - return lift(other, Math::min, UpperCardinality::max, this); - } - - @Override - public CardinalityInterval take(int count) { - int newLowerBound = Math.max(lowerBound - count, 0); - var newUpperBound = upperBound.take(count); - if (newUpperBound == null) { - return CardinalityIntervals.ERROR; - } - return CardinalityIntervals.between(newLowerBound, newUpperBound); - } - - private CardinalityInterval lift(CardinalityInterval other, IntBinaryOperator lowerOperator, - BinaryOperator upperOperator, - CardinalityInterval whenEmpty) { - if (other instanceof NonEmptyCardinalityInterval(var otherLowerBound, var otherUpperBound)) { - return CardinalityIntervals.between(lowerOperator.applyAsInt(lowerBound, otherLowerBound), - upperOperator.apply(upperBound, otherUpperBound)); - } - if (other instanceof EmptyCardinalityInterval) { - return whenEmpty; - } - throw new IllegalArgumentException("Unknown CardinalityInterval: " + other); - } - - private CardinalityInterval lift(CardinalityInterval other, IntBinaryOperator lowerOperator, - BinaryOperator upperOperator) { - return lift(other, lowerOperator, upperOperator, CardinalityIntervals.ERROR); - } - - @Override - public String toString() { - if (upperBound instanceof FiniteUpperCardinality(var finiteUpperBound) && - finiteUpperBound == lowerBound) { - return "[%d]".formatted(lowerBound); - } - return "[%d..%s]".formatted(lowerBound, upperBound); - } - - @Override - public boolean equals(Object o) { - if (this == o) return true; - if (o == null || getClass() != o.getClass()) return false; - NonEmptyCardinalityInterval that = (NonEmptyCardinalityInterval) o; - return lowerBound == that.lowerBound && Objects.equals(upperBound, that.upperBound); - } - - @Override - public int hashCode() { - return lowerBound * 31 + upperBound.hashCode(); - } -} diff --git a/subprojects/logic/src/test/java/tools/refinery/logic/term/cardinalityinterval/CardinalityIntervalTest.java b/subprojects/logic/src/test/java/tools/refinery/logic/term/cardinalityinterval/CardinalityIntervalTest.java index ee2dd61c3..81b3aaf67 100644 --- a/subprojects/logic/src/test/java/tools/refinery/logic/term/cardinalityinterval/CardinalityIntervalTest.java +++ b/subprojects/logic/src/test/java/tools/refinery/logic/term/cardinalityinterval/CardinalityIntervalTest.java @@ -5,17 +5,33 @@ */ package tools.refinery.logic.term.cardinalityinterval; +import org.junit.jupiter.api.Test; import org.junit.jupiter.params.ParameterizedTest; import org.junit.jupiter.params.provider.Arguments; import org.junit.jupiter.params.provider.MethodSource; +import tools.refinery.logic.term.uppercardinality.UpperCardinalities; import java.util.stream.Stream; import static org.hamcrest.MatcherAssert.assertThat; import static org.hamcrest.Matchers.equalTo; +import static org.hamcrest.Matchers.lessThan; +import static org.junit.jupiter.api.Assertions.assertThrows; import static tools.refinery.logic.term.cardinalityinterval.CardinalityIntervals.*; class CardinalityIntervalTest { + @Test + void inconsistentBoundsTest() { + assertThat(CardinalityIntervals.ERROR.upperBound().compareToInt(CardinalityIntervals.ERROR.lowerBound()), + lessThan(0)); + } + + @Test + void invalidLowerBoundConstructorTest() { + assertThrows(IllegalArgumentException.class, () -> new CardinalityInterval(-1, + UpperCardinalities.UNBOUNDED)); + } + @ParameterizedTest(name = "min({0}, {1}) == {2}") @MethodSource void minTest(CardinalityInterval a, CardinalityInterval b, CardinalityInterval expected) { @@ -27,11 +43,7 @@ static Stream minTest() { Arguments.of(atMost(1), atMost(1), atMost(1)), Arguments.of(atMost(1), between(2, 3), atMost(1)), Arguments.of(atMost(1), atLeast(2), atMost(1)), - Arguments.of(atMost(1), ERROR, ERROR), - Arguments.of(atLeast(1), atLeast(2), atLeast(1)), - Arguments.of(atLeast(1), ERROR, ERROR), - Arguments.of(ERROR, atLeast(2), ERROR), - Arguments.of(ERROR, ERROR, ERROR) + Arguments.of(atLeast(1), atLeast(2), atLeast(1)) ); } @@ -46,11 +58,7 @@ static Stream maxTest() { Arguments.of(atMost(1), atMost(1), atMost(1)), Arguments.of(atMost(1), between(2, 3), between(2, 3)), Arguments.of(atMost(1), atLeast(2), atLeast(2)), - Arguments.of(atMost(1), ERROR, ERROR), - Arguments.of(atLeast(1), atLeast(2), atLeast(2)), - Arguments.of(atLeast(1), ERROR, ERROR), - Arguments.of(ERROR, atLeast(2), ERROR), - Arguments.of(ERROR, ERROR, ERROR) + Arguments.of(atLeast(1), atLeast(2), atLeast(2)) ); } @@ -65,11 +73,7 @@ static Stream addTest() { Arguments.of(atMost(1), atMost(1), atMost(2)), Arguments.of(atMost(1), between(2, 3), between(2, 4)), Arguments.of(atMost(1), atLeast(2), atLeast(2)), - Arguments.of(atMost(1), ERROR, ERROR), - Arguments.of(atLeast(1), atLeast(2), atLeast(3)), - Arguments.of(atLeast(1), ERROR, ERROR), - Arguments.of(ERROR, atLeast(2), ERROR), - Arguments.of(ERROR, ERROR, ERROR) + Arguments.of(atLeast(1), atLeast(2), atLeast(3)) ); } @@ -83,10 +87,7 @@ static Stream multiplyTest() { return Stream.of( Arguments.of(between(2, 3), between(4, 5), between(8, 15)), Arguments.of(atLeast(2), between(4, 5), atLeast(8)), - Arguments.of(between(2, 3), atLeast(4), atLeast(8)), - Arguments.of(between(2, 3), ERROR, ERROR), - Arguments.of(ERROR, between(4, 5), ERROR), - Arguments.of(ERROR, ERROR, ERROR) + Arguments.of(between(2, 3), atLeast(4), atLeast(8)) ); } @@ -100,11 +101,7 @@ static Stream meetTest() { return Stream.of( Arguments.of(atMost(1), atMost(2), atMost(1)), Arguments.of(atMost(2), between(1, 3), between(1, 2)), - Arguments.of(atMost(1), between(1, 3), exactly(1)), - Arguments.of(atMost(1), between(2, 3), ERROR), - Arguments.of(atMost(1), ERROR, ERROR), - Arguments.of(ERROR, atMost(1), ERROR), - Arguments.of(ERROR, ERROR, ERROR) + Arguments.of(atMost(1), between(1, 3), exactly(1)) ); } @@ -118,10 +115,7 @@ static Stream joinTest() { return Stream.of( Arguments.of(atMost(1), atMost(2), atMost(2)), Arguments.of(atMost(2), between(1, 3), atMost(3)), - Arguments.of(atMost(1), between(2, 3), atMost(3)), - Arguments.of(atMost(1), ERROR, atMost(1)), - Arguments.of(ERROR, atMost(1), atMost(1)), - Arguments.of(ERROR, ERROR, ERROR) + Arguments.of(atMost(1), between(2, 3), atMost(3)) ); } } diff --git a/subprojects/logic/src/test/java/tools/refinery/logic/term/cardinalityinterval/EmptyCardinalityIntervalTest.java b/subprojects/logic/src/test/java/tools/refinery/logic/term/cardinalityinterval/EmptyCardinalityIntervalTest.java deleted file mode 100644 index 0dbc7f61d..000000000 --- a/subprojects/logic/src/test/java/tools/refinery/logic/term/cardinalityinterval/EmptyCardinalityIntervalTest.java +++ /dev/null @@ -1,19 +0,0 @@ -/* - * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors - * - * SPDX-License-Identifier: EPL-2.0 - */ -package tools.refinery.logic.term.cardinalityinterval; - -import org.junit.jupiter.api.Test; - -import static org.hamcrest.MatcherAssert.assertThat; -import static org.hamcrest.Matchers.lessThan; - -class EmptyCardinalityIntervalTest { - @Test - void inconsistentBoundsTest() { - assertThat(CardinalityIntervals.ERROR.upperBound().compareToInt(CardinalityIntervals.ERROR.lowerBound()), - lessThan(0)); - } -} diff --git a/subprojects/logic/src/test/java/tools/refinery/logic/term/cardinalityinterval/FiniteCardinalityIntervalTest.java b/subprojects/logic/src/test/java/tools/refinery/logic/term/cardinalityinterval/FiniteCardinalityIntervalTest.java deleted file mode 100644 index 588b25ab0..000000000 --- a/subprojects/logic/src/test/java/tools/refinery/logic/term/cardinalityinterval/FiniteCardinalityIntervalTest.java +++ /dev/null @@ -1,27 +0,0 @@ -/* - * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors - * - * SPDX-License-Identifier: EPL-2.0 - */ -package tools.refinery.logic.term.cardinalityinterval; - -import org.junit.jupiter.api.Test; -import tools.refinery.logic.term.uppercardinality.UpperCardinality; -import tools.refinery.logic.term.uppercardinality.UpperCardinalities; - -import static org.junit.jupiter.api.Assertions.assertThrows; - -class FiniteCardinalityIntervalTest { - @Test - void invalidLowerBoundConstructorTest() { - assertThrows(IllegalArgumentException.class, () -> new NonEmptyCardinalityInterval(-1, - UpperCardinalities.UNBOUNDED)); - } - - @Test - void invalidUpperBoundConstructorTest() { - var upperCardinality = UpperCardinality.of(1); - assertThrows(IllegalArgumentException.class, () -> new NonEmptyCardinalityInterval(2, - upperCardinality)); - } -} 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 index af3b78d89..718fbf6cf 100644 --- 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 @@ -247,7 +247,7 @@ private void translateContains(ModelStoreBuilder storeBuilder) { private void translateInvalidContainer(ModelStoreBuilder storeBuilder) { storeBuilder.with(new InvalidMultiplicityErrorTranslator(CONTAINED_SYMBOL, CONTAINS_SYMBOL, true, - ConstrainedMultiplicity.of(CardinalityIntervals.ONE, INVALID_CONTAINER))); + new ConstrainedMultiplicity(CardinalityIntervals.ONE, INVALID_CONTAINER))); } private void translateFocusNotContained(ModelStoreBuilder storeBuilder) { diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/ReferenceInfoBuilder.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/ReferenceInfoBuilder.java index 969a42a58..094b30300 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/ReferenceInfoBuilder.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/ReferenceInfoBuilder.java @@ -57,7 +57,7 @@ public ReferenceInfoBuilder multiplicity(@NotNull Multiplicity multiplicity) { public ReferenceInfoBuilder multiplicity(@NotNull CardinalityInterval multiplicityInterval, @NotNull PartialRelation errorSymbol) { - return multiplicity(ConstrainedMultiplicity.of(multiplicityInterval, errorSymbol)); + return multiplicity(new ConstrainedMultiplicity(multiplicityInterval, errorSymbol)); } public ReferenceInfoBuilder opposite(@Nullable PartialRelation opposite) { diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/CleanupPropagator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/CleanupPropagator.java index ecb36c44d..20fa9a9fa 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/CleanupPropagator.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/CleanupPropagator.java @@ -8,6 +8,7 @@ import tools.refinery.logic.dnf.Query; import tools.refinery.logic.dnf.RelationalQuery; import tools.refinery.logic.term.cardinalityinterval.CardinalityInterval; +import tools.refinery.logic.term.int_.IntTerms; import tools.refinery.logic.term.uppercardinality.UpperCardinalities; import tools.refinery.logic.term.uppercardinality.UpperCardinality; import tools.refinery.logic.term.uppercardinality.UpperCardinalityTerms; @@ -26,6 +27,7 @@ import java.util.List; import static tools.refinery.logic.literal.Literals.check; +import static tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator.LOWER_CARDINALITY_VIEW; import static tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator.UPPER_CARDINALITY_VIEW; /** @@ -34,10 +36,12 @@ */ public class CleanupPropagator implements Propagator { private static final RelationalQuery CLEANUP_QUERY = Query.of("exists#cleanup", (builder, node) -> builder - .clause(UpperCardinality.class, upper -> List.of( + .clause(Integer.class, UpperCardinality.class, (lower, upper) -> List.of( UPPER_CARDINALITY_VIEW.call(node, upper), check(UpperCardinalityTerms.less(upper, - UpperCardinalityTerms.constant(UpperCardinalities.ONE))) + UpperCardinalityTerms.constant(UpperCardinalities.ONE))), + LOWER_CARDINALITY_VIEW.call(node, lower), + check(IntTerms.eq(lower, IntTerms.constant(0))) )) ); diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/ExistsRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/ExistsRefiner.java index 8664f46de..45e6d5633 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/ExistsRefiner.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/ExistsRefiner.java @@ -43,13 +43,13 @@ public boolean merge(Tuple key, TruthValue value) { newCount = currentCount.meet(CardinalityIntervals.NONE); } case ERROR -> { - return false; + if (concretizationInProgress()) { + return false; + } + newCount = currentCount.meet(CardinalityIntervals.ERROR); } default -> throw new IllegalArgumentException("Unknown TruthValue: " + value); } - if (newCount.isError()) { - return false; - } countInterpretation.put(key, newCount); return true; } diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectInitializer.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectInitializer.java index eb13174cf..955dc1f47 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectInitializer.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectInitializer.java @@ -36,11 +36,6 @@ public void initialize(Model model, ModelSeed modelSeed) { var countInterpretation = model.getInterpretation(countSymbol); var uniqueTable = new HashMap(); for (int i = 0; i < intervals.length; i++) { - var interval = intervals[i]; - if (interval.isError()) { - throw new TranslationException(ReasoningAdapter.EXISTS_SYMBOL, - "Inconsistent existence or equality for node " + i); - } var uniqueInterval = uniqueTable.computeIfAbsent(intervals[i], Function.identity()); countInterpretation.put(Tuple.of(i), uniqueInterval); } @@ -63,7 +58,7 @@ private CardinalityInterval[] initializeIntervals(Model model, ModelSeed modelSe if (!modelSeed.containsSeed(ReasoningAdapter.EXISTS_SYMBOL) || !modelSeed.containsSeed(ReasoningAdapter.EQUALS_SYMBOL)) { throw new TranslationException(MultiObjectTranslator.COUNT_SYMBOL, - "Seed for %s and %s is required if there is no seed for %s".formatted( + "Seeds for %s and %s are required if there is no seed for %s".formatted( ReasoningAdapter.EXISTS_SYMBOL, ReasoningAdapter.EQUALS_SYMBOL, MultiObjectTranslator.COUNT_SYMBOL)); } @@ -83,8 +78,7 @@ private void initializeExists(CardinalityInterval[] intervals, Model model, Mode switch (cursor.getValue()) { case TRUE -> intervals[i] = intervals[i].meet(CardinalityIntervals.SOME); case FALSE -> intervals[i] = intervals[i].meet(CardinalityIntervals.NONE); - case ERROR -> throw new TranslationException(ReasoningAdapter.EXISTS_SYMBOL, - "Inconsistent existence for node " + i); + case ERROR -> intervals[i] = intervals[i].meet(CardinalityIntervals.ERROR); default -> throw new TranslationException(ReasoningAdapter.EXISTS_SYMBOL, "Invalid existence truth value %s for node %d".formatted(cursor.getValue(), i)); } diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectStorageRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectStorageRefiner.java index ab401f9ee..0474f1835 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectStorageRefiner.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectStorageRefiner.java @@ -28,7 +28,7 @@ public boolean split(int parentNode, int childNode) { return false; } var newParentCount = parentCount.take(1); - if (newParentCount.isError()) { + if (newParentCount == null || newParentCount.isError()) { return false; } var childKey = Tuple.of(childNode); 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 5811b05ff..54de75da3 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 @@ -6,6 +6,7 @@ package tools.refinery.store.reasoning.translator.multiobject; import tools.refinery.logic.dnf.Query; +import tools.refinery.logic.literal.Literals; import tools.refinery.logic.term.Variable; import tools.refinery.logic.term.cardinalityinterval.CardinalityDomain; import tools.refinery.logic.term.cardinalityinterval.CardinalityInterval; @@ -77,12 +78,13 @@ public void apply(ModelStoreBuilder storeBuilder) { LOWER_CARDINALITY_VIEW.call(p1, lower), check(greaterEq(lower, constant(1))) )))) - // It is impossible to obey the refinement from the partial to the candidate view, since - // multi-objects will be turned into single objects by the candidate rewriter of EQUALS_SYMBOL. - // Nevertheless, by making sure that surely existing multi-objects are preserved in the candidate - // view, we are at least able to display predicates that hold with an error value on the surely - // existing multi-objects in the partial view (or have conflicting values in the partial and - // candidate views) in the candidate view. + // Force multi-objects that surely exist in the partial view to exist with an {@code ERROR} logic + // value in the candidate view. + .candidateMay(Query.of("exists#candidate", (builder, p1) -> builder + .clause( + LOWER_CARDINALITY_VIEW.call(p1, Variable.of(Integer.class)), + Literals.not(MULTI_VIEW.call(p1)) + ))) .roundingMode(RoundingMode.PREFER_FALSE) .refiner(ExistsRefiner.of(COUNT_STORAGE)) .exclude(null) 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 index c327aac83..d6db8b9d3 100644 --- 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 @@ -5,15 +5,17 @@ */ package tools.refinery.store.reasoning.translator.multiplicity; -import tools.refinery.store.reasoning.representation.PartialRelation; -import tools.refinery.store.reasoning.translator.TranslationException; import tools.refinery.logic.term.cardinalityinterval.CardinalityInterval; import tools.refinery.logic.term.cardinalityinterval.CardinalityIntervals; -import tools.refinery.logic.term.cardinalityinterval.NonEmptyCardinalityInterval; +import tools.refinery.store.reasoning.representation.PartialRelation; +import tools.refinery.store.reasoning.translator.TranslationException; -public record ConstrainedMultiplicity(NonEmptyCardinalityInterval multiplicity, PartialRelation errorSymbol) +public record ConstrainedMultiplicity(CardinalityInterval multiplicity, PartialRelation errorSymbol) implements Multiplicity { public ConstrainedMultiplicity { + if (multiplicity.isError()) { + throw new TranslationException(errorSymbol, "Inconsistent multiplicity"); + } if (multiplicity.equals(CardinalityIntervals.SET)) { throw new TranslationException(errorSymbol, "Expected a constrained cardinality interval"); } @@ -23,13 +25,6 @@ public record ConstrainedMultiplicity(NonEmptyCardinalityInterval multiplicity, } } - public static ConstrainedMultiplicity of(CardinalityInterval multiplicity, PartialRelation errorSymbol) { - if (!(multiplicity instanceof NonEmptyCardinalityInterval nonEmptyCardinalityInterval)) { - throw new TranslationException(errorSymbol, "Inconsistent multiplicity"); - } - return new ConstrainedMultiplicity(nonEmptyCardinalityInterval, errorSymbol); - } - @Override public boolean isConstrained() { return true; From 375a21fa356bf1960cb2973094076bb25622dc93 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Krist=C3=B3f=20Marussy?= Date: Tue, 12 Nov 2024 00:59:24 +0100 Subject: [PATCH 2/5] refactor(reasoning-scope): improve scope propagator robustness * Make the scope propagator more robust by handling OR-TOOLS failures. This can happen with paraconsistent scope bounds. * Detect inconsistent variable bounds, as this can cause an ABNORMAL OR-TOOLS failure. * Cache scope propagator error messages for better performance. --- .../reasoning/scope/BoundScopePropagator.java | 15 ++++++++++----- .../reasoning/scope/TypeScopePropagator.java | 12 ++++++++++++ 2 files changed, 22 insertions(+), 5 deletions(-) diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/BoundScopePropagator.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/BoundScopePropagator.java index fd46b0da7..40c6e90d8 100644 --- a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/BoundScopePropagator.java +++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/BoundScopePropagator.java @@ -160,7 +160,12 @@ public PropagationResult propagateOne() { model.checkCancelled(); if (!propagator.updateBounds()) { // Avoid logging GLOP error to console by checking for inconsistent constraints in advance. - return createRejectedResult("Unsatisfiable %s.".formatted(propagator.getName())); + return createRejectedResult(propagator.getUnsatisfiableMessage()); + } + } + for (var variable : variables) { + if (variable.lb() > variable.ub()) { + return createRejectedResult("Object with inconsistent existence detected."); } } var result = PropagationResult.UNCHANGED; @@ -187,7 +192,7 @@ private PropagationResult checkEmptiness() { var emptinessCheckingResult = solver.solve(); return switch (emptinessCheckingResult) { case OPTIMAL, UNBOUNDED -> PropagationResult.UNCHANGED; - case INFEASIBLE -> createRejectedResult(); + case ABNORMAL, INFEASIBLE -> createRejectedResult(); default -> throw new IllegalStateException("Failed to check for consistency: " + emptinessCheckingResult); }; } @@ -202,7 +207,7 @@ private PropagationResult propagateNode(int nodeId, MPVariable variable) { switch (minimizationResult) { case OPTIMAL -> lowerBound = RoundingUtil.roundUp(objective.value()); case UNBOUNDED -> lowerBound = 0; - case INFEASIBLE -> { + case ABNORMAL, INFEASIBLE -> { return createRejectedResult(); } default -> throw new IllegalStateException("Failed to solve for minimum of %s: %s" @@ -217,7 +222,7 @@ private PropagationResult propagateNode(int nodeId, MPVariable variable) { case OPTIMAL -> upperBound = UpperCardinalities.atMost(RoundingUtil.roundDown(objective.value())); // Problem was feasible when minimizing, the only possible source of {@code UNBOUNDED_OR_INFEASIBLE} is // an unbounded maximization problem. See https://github.com/google/or-tools/issues/3319 - case UNBOUNDED, INFEASIBLE -> upperBound = UpperCardinalities.UNBOUNDED; + case ABNORMAL, UNBOUNDED, INFEASIBLE -> upperBound = UpperCardinalities.UNBOUNDED; default -> throw new IllegalStateException("Failed to solve for maximum of %s: %s" .formatted(variable, minimizationResult)); } @@ -240,7 +245,7 @@ public PropagationResult checkConcretization() { for (var propagator : propagators) { model.checkCancelled(); if (!propagator.checkConcretization()) { - return createRejectedResult("The %s was not satisfied.".formatted(propagator.getName())); + return createRejectedResult(propagator.getNotSatisfiedMessage()); } } return PropagationResult.UNCHANGED; diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/TypeScopePropagator.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/TypeScopePropagator.java index 8b9f698ff..50690d64c 100644 --- a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/TypeScopePropagator.java +++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/TypeScopePropagator.java @@ -25,6 +25,8 @@ abstract class TypeScopePropagator { private final CriterionCalculator acceptCalculator; private final PartialRelation type; protected final MPConstraint constraint; + private final String unsatisfiableMessage; + private final String notSatisfiedMessage; protected TypeScopePropagator(BoundScopePropagator adapter, RelationalQuery allQuery, RelationalQuery multiQuery, Criterion acceptCriterion, PartialRelation type) { @@ -43,6 +45,8 @@ protected TypeScopePropagator(BoundScopePropagator adapter, RelationalQuery allQ } allNodes.addListener(this::allChanged); multiNodes.addListener(this::multiChanged); + unsatisfiableMessage = "Unsatisfiable %s.".formatted(getName()); + notSatisfiedMessage = "The %s was not satisfied.".formatted(getName()); } protected abstract void doUpdateBounds(); @@ -54,6 +58,14 @@ public boolean updateBounds() { public abstract String getName(); + public String getUnsatisfiableMessage() { + return unsatisfiableMessage; + } + + public String getNotSatisfiedMessage() { + return notSatisfiedMessage; + } + public PartialRelation getType() { return type; } From fbfd3b23bb7078747d0b293ceebc23bd3e1a7b34 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Krist=C3=B3f=20Marussy?= Date: Tue, 12 Nov 2024 01:03:14 +0100 Subject: [PATCH 3/5] fix(frontend): dimmed header of non-existent nodes --- subprojects/frontend/src/graph/GraphTheme.tsx | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/subprojects/frontend/src/graph/GraphTheme.tsx b/subprojects/frontend/src/graph/GraphTheme.tsx index 8b7311e08..b65876387 100644 --- a/subprojects/frontend/src/graph/GraphTheme.tsx +++ b/subprojects/frontend/src/graph/GraphTheme.tsx @@ -177,7 +177,7 @@ export function createGraphTheme({ strokeDasharray: '2 4', }, '.node-header': { - fill: theme.palette.background.default, + fill: `${theme.palette.background.default} !important`, }, '.icon-TRUE': { fill: theme.palette.text.secondary, @@ -188,7 +188,7 @@ export function createGraphTheme({ stroke: errorColor.main, }, '.node-header': { - fill: theme.palette.background.default, + fill: `${theme.palette.background.default} !important`, }, }, }; From 51b726e8494655a5878d4a0889e50ea17a707858 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Krist=C3=B3f=20Marussy?= Date: Tue, 12 Nov 2024 01:10:30 +0100 Subject: [PATCH 4/5] refactor(langauge-web): show inconsistent candidate cardinality Since we can't access the COUNT symbol directly yet, we post-process the COUNT_STORAGE values before JSON generation. --- .../semantics/PartialInterpretation2Json.java | 22 +++++++++++++++---- 1 file changed, 18 insertions(+), 4 deletions(-) diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/PartialInterpretation2Json.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/PartialInterpretation2Json.java index ff8110335..675f92e8a 100644 --- a/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/PartialInterpretation2Json.java +++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/PartialInterpretation2Json.java @@ -11,14 +11,19 @@ import com.google.inject.Singleton; import tools.refinery.generator.ModelFacade; import tools.refinery.language.semantics.SemanticsUtils; +import tools.refinery.logic.term.cardinalityinterval.CardinalityInterval; +import tools.refinery.logic.term.cardinalityinterval.CardinalityIntervals; import tools.refinery.store.map.Cursor; import tools.refinery.store.model.Model; +import tools.refinery.store.reasoning.literal.Concreteness; import tools.refinery.store.reasoning.representation.PartialRelation; import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator; import tools.refinery.store.tuple.Tuple; import tools.refinery.store.util.CancellationToken; import java.util.TreeMap; +import java.util.function.Function; +import java.util.function.UnaryOperator; @Singleton public class PartialInterpretation2Json { @@ -36,7 +41,7 @@ public JsonObject getPartialInterpretation(ModelFacade facade, CancellationToken json.add(name, tuples); cancellationToken.checkCancelled(); } - json.add("builtin::count", getCountJson(model)); + json.add("builtin::count", getCountJson(model, facade.getConcreteness())); return json; } @@ -47,9 +52,13 @@ private static JsonArray getTuplesJson(ModelFacade facade, PartialRelation parti } private static JsonArray getTuplesJson(Cursor cursor) { + return getTuplesJson(cursor, Function.identity()); + } + + private static JsonArray getTuplesJson(Cursor cursor, Function transform) { var map = new TreeMap(); while (cursor.move()) { - map.put(cursor.getKey(), cursor.getValue()); + map.put(cursor.getKey(), transform.apply(cursor.getValue())); } var tuples = new JsonArray(); for (var entry : map.entrySet()) { @@ -68,10 +77,15 @@ private static JsonArray toArray(Tuple tuple, Object value) { return json; } - private static JsonArray getCountJson(Model model) { + private static JsonArray getCountJson(Model model, Concreteness concreteness) { var interpretation = model.getInterpretation(MultiObjectTranslator.COUNT_STORAGE); var cursor = interpretation.getAll(); - return getTuplesJson(cursor); + UnaryOperator transform = switch (concreteness) { + case PARTIAL -> UnaryOperator.identity(); + case CANDIDATE -> count -> count.equals(CardinalityIntervals.ONE) ? count : + count.meet(CardinalityIntervals.NONE); + }; + return getTuplesJson(cursor, transform); } } From 9f360fbcfee45e4078602d62c84b14adf70eb064 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Krist=C3=B3f=20Marussy?= Date: Tue, 12 Nov 2024 01:15:49 +0100 Subject: [PATCH 5/5] refactor(reasoning): multi-objects may exist in the candidate view Let multi-objects exist in the candidate view to reduce the size of candidate view deltas during model refinement, but ensure that they have an inconsistent COUNT if their lower scope bound is vioalted by concretization. --- .../generator/semantics/multiObjectExistence.problem | 4 ++-- .../web/semantics/PartialInterpretation2Json.java | 5 ++--- .../translator/multiobject/MultiObjectTranslator.java | 10 ++-------- 3 files changed, 6 insertions(+), 13 deletions(-) diff --git a/subprojects/generator/src/test/resources/tools/refinery/generator/semantics/multiObjectExistence.problem b/subprojects/generator/src/test/resources/tools/refinery/generator/semantics/multiObjectExistence.problem index 5cb36ea91..398e7b79f 100644 --- a/subprojects/generator/src/test/resources/tools/refinery/generator/semantics/multiObjectExistence.problem +++ b/subprojects/generator/src/test/resources/tools/refinery/generator/semantics/multiObjectExistence.problem @@ -23,10 +23,10 @@ exists(D::new). ?equals(D::new, D::new). % EXPECT CANDIDATE EXACTLY: -exists(A::new): error. +exists(A::new). equals(A::new, A::new). !exists(B::new). exists(C::new). equals(C::new, C::new). -exists(D::new): error. +exists(D::new). equals(D::new, D::new). diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/PartialInterpretation2Json.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/PartialInterpretation2Json.java index 675f92e8a..93ac22dec 100644 --- a/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/PartialInterpretation2Json.java +++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/PartialInterpretation2Json.java @@ -82,10 +82,9 @@ private static JsonArray getCountJson(Model model, Concreteness concreteness) { var cursor = interpretation.getAll(); UnaryOperator transform = switch (concreteness) { case PARTIAL -> UnaryOperator.identity(); - case CANDIDATE -> count -> count.equals(CardinalityIntervals.ONE) ? count : - count.meet(CardinalityIntervals.NONE); + case CANDIDATE -> count -> count.lowerBound() == 0 ? CardinalityIntervals.NONE : + count.meet(CardinalityIntervals.LONE); }; return getTuplesJson(cursor, transform); - } } 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 54de75da3..1e3120de4 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 @@ -6,7 +6,6 @@ package tools.refinery.store.reasoning.translator.multiobject; import tools.refinery.logic.dnf.Query; -import tools.refinery.logic.literal.Literals; import tools.refinery.logic.term.Variable; import tools.refinery.logic.term.cardinalityinterval.CardinalityDomain; import tools.refinery.logic.term.cardinalityinterval.CardinalityInterval; @@ -78,13 +77,8 @@ public void apply(ModelStoreBuilder storeBuilder) { LOWER_CARDINALITY_VIEW.call(p1, lower), check(greaterEq(lower, constant(1))) )))) - // Force multi-objects that surely exist in the partial view to exist with an {@code ERROR} logic - // value in the candidate view. - .candidateMay(Query.of("exists#candidate", (builder, p1) -> builder - .clause( - LOWER_CARDINALITY_VIEW.call(p1, Variable.of(Integer.class)), - Literals.not(MULTI_VIEW.call(p1)) - ))) + // Multi-objects which surely exist in the partial view will also exist in the candidate view, + // but they may have inconsistent {@code COUNT} that refines their {@code COUNT} from the partial view. .roundingMode(RoundingMode.PREFER_FALSE) .refiner(ExistsRefiner.of(COUNT_STORAGE)) .exclude(null)