Merge pull request #68 from kris7t/paraconsistent-count

Paraconsistent object cardinalities

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`,
       },
     },
   };

subprojects/generator/src/main/java/tools/refinery/generator/impl/FilteredInterpretation.java

@@ -57,7 +57,7 @@ public Cursor<Tuple, A> 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;
 			}
 		}

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(

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<Tuple, ?> cursor) {
+		return getTuplesJson(cursor, Function.identity());
+	}
+
+	private static <T, R> JsonArray getTuplesJson(Cursor<Tuple, T> cursor, Function<T, R> transform) {
 		var map = new TreeMap<Tuple, Object>();
 		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<CardinalityInterval> transform = switch (concreteness) {
+			case PARTIAL -> UnaryOperator.identity();
+			case CANDIDATE -> count -> count.lowerBound() == 0 ? CardinalityIntervals.NONE :
+					count.meet(CardinalityIntervals.LONE);
+		};
+		return getTuplesJson(cursor, transform);
 	}
 }

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;

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).",

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<CardinalityInterval, Integer>
-		permits NonEmptyCardinalityInterval, EmptyCardinalityInterval {
-	int lowerBound();
+public record CardinalityInterval(int lowerBound, UpperCardinality upperBound)
+		implements AbstractValue<CardinalityInterval, Integer> {
+	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);
+	}
 }

subprojects/logic/src/main/java/tools/refinery/logic/term/cardinalityinterval/CardinalityIntervals.java

@@ -19,36 +19,33 @@ 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) {
 		return between(lowerBound, UpperCardinalities.atMost(upperBound));
 	}
 
 	public static CardinalityInterval atMost(UpperCardinality upperBound) {
-		return new NonEmptyCardinalityInterval(0, upperBound);
+		return new CardinalityInterval(0, upperBound);
 	}
 
 	public static CardinalityInterval atMost(int upperBound) {
 		return atMost(UpperCardinalities.atMost(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));
 	}
 }