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`, }, }, }; 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/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-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..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 @@ -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,14 @@ 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.lowerBound() == 0 ? CardinalityIntervals.NONE : + count.meet(CardinalityIntervals.LONE); + }; + return getTuplesJson(cursor, transform); } } 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-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; } 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..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 @@ -77,12 +77,8 @@ 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. + // 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) 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;