feat: state-based store for cross references

Efficiently store cross references even if default ref(*, *): false.

Uses propagation rules instead of view queries to reason about type constraints
and multiplicity.

7 files changed, 77 insertions, 19 deletions

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 ecaa7e0d..38bf5a61 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
@@ -27,9 +27,7 @@ import tools.refinery.store.reasoning.seed.ModelSeed;
 import tools.refinery.store.reasoning.seed.Seed;
 import tools.refinery.store.reasoning.translator.TranslationException;
 import tools.refinery.store.reasoning.translator.containment.ContainmentHierarchyTranslator;
-import tools.refinery.store.reasoning.translator.metamodel.Metamodel;
-import tools.refinery.store.reasoning.translator.metamodel.MetamodelBuilder;
-import tools.refinery.store.reasoning.translator.metamodel.MetamodelTranslator;
+import tools.refinery.store.reasoning.translator.metamodel.*;
 import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator;
 import tools.refinery.store.reasoning.translator.multiplicity.ConstrainedMultiplicity;
 import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity;
@@ -73,6 +71,10 @@ public class ModelInitializer {
 
         private ScopePropagator scopePropagator;
 
+        private int nodeCount;
+
+        private ModelSeed.Builder modelSeedBuilder;
+
         private ModelSeed modelSeed;
 
         public void readProblem(Problem problem) {
@@ -101,13 +103,17 @@ public class ModelInitializer {
                                                         TruthValue.FALSE));
                         collectNodes();
                         collectPartialSymbols();
+                        nodeCount = problemTrace.getNodeTrace().size();
+                        modelSeedBuilder = ModelSeed.builder(nodeCount);
+                        collectAssertions();
                         collectMetamodel();
                         metamodel = metamodelBuilder.build();
                         problemTrace.setMetamodel(metamodel);
-                        collectAssertions();
-                        int nodeCount = problemTrace.getNodeTrace().size();
-                        var modelSeedBuilder = ModelSeed.builder(nodeCount);
+                        fixClassDeclarationAssertions();
                         for (var entry : relationInfoMap.entrySet()) {
+                                if (entry.getKey() instanceof ReferenceDeclaration) {
+                                        continue;
+                                }
                                 var info = entry.getValue();
                                 var partialRelation = info.partialRelation();
                                 modelSeedBuilder.seed(partialRelation, info.toSeed(nodeCount));
@@ -296,7 +302,20 @@ public class ModelInitializer {
                 }
                 var multiplicity = getMultiplicityConstraint(referenceDeclaration);
                 try {
-                        metamodelBuilder.reference(relation, source, containment, multiplicity, target, oppositeRelation);
+                        var seed = relationInfoMap.get(referenceDeclaration).toSeed(nodeCount);
+                        var defaultValue = seed.majorityValue();
+                        if (defaultValue.must()) {
+                                defaultValue = TruthValue.FALSE;
+                        }
+                        modelSeedBuilder.seed(relation, seed);
+                        metamodelBuilder.reference(relation, ReferenceInfo.builder()
+                                        .containment(containment)
+                                        .source(source)
+                                        .multiplicity(multiplicity)
+                                        .target(target)
+                                        .opposite(oppositeRelation)
+                                        .defaultValue(defaultValue)
+                                        .build());
                 } catch (RuntimeException e) {
                         throw TracedException.addTrace(classDeclaration, e);
                 }
@@ -355,10 +374,6 @@ public class ModelInitializer {
                 collectCardinalityAssertions(newNodeId, TruthValue.UNKNOWN);
                 var tuple = Tuple.of(newNodeId);
                 mergeValue(classDeclaration, tuple, TruthValue.TRUE);
-                var typeInfo = metamodel.typeHierarchy().getAnalysisResult(getPartialRelation(classDeclaration));
-                for (var subType : typeInfo.getDirectSubtypes()) {
-                        partialRelationInfoMap.get(subType).assertions().mergeValue(tuple, TruthValue.FALSE);
-                }
         }
 
         private void collectEnumAssertions(EnumDeclaration enumDeclaration) {
@@ -399,6 +414,27 @@ public class ModelInitializer {
                 }
         }
 
+        private void fixClassDeclarationAssertions() {
+                for (var statement : problem.getStatements()) {
+                        if (statement instanceof ClassDeclaration classDeclaration) {
+                                fixClassDeclarationAssertions(classDeclaration);
+                        }
+                }
+        }
+
+        private void fixClassDeclarationAssertions(ClassDeclaration classDeclaration) {
+                var newNode = classDeclaration.getNewNode();
+                if (newNode == null) {
+                        return;
+                }
+                var newNodeId = getNodeId(newNode);
+                var tuple = Tuple.of(newNodeId);
+                var typeInfo = metamodel.typeHierarchy().getAnalysisResult(getPartialRelation(classDeclaration));
+                for (var subType : typeInfo.getDirectSubtypes()) {
+                        partialRelationInfoMap.get(subType).assertions().mergeValue(tuple, TruthValue.FALSE);
+                }
+        }
+
         private void mergeValue(Relation relation, Tuple key, TruthValue value) {
                 getRelationInfo(relation).assertions().mergeValue(key, value);
         }
@@ -482,7 +518,7 @@ public class ModelInitializer {
                         defaultValue = TruthValue.FALSE;
                 } else {
                         var seed = modelSeed.getSeed(partialRelation);
-                        defaultValue = seed.reducedValue() == TruthValue.FALSE ? TruthValue.FALSE : TruthValue.UNKNOWN;
+                        defaultValue = seed.majorityValue() == TruthValue.FALSE ? TruthValue.FALSE : TruthValue.UNKNOWN;
                         var cursor = seed.getCursor(defaultValue, problemTrace.getNodeTrace().size());
                         // The symbol should be mutable if there is at least one non-default entry in the seed.
                         mutable = mutable || cursor.move();
@@ -495,7 +531,7 @@ public class ModelInitializer {
                 var problemParameters = predicateDefinition.getParameters();
                 int arity = problemParameters.size();
                 var parameters = new NodeVariable[arity];
-                var parameterMap = new HashMap<tools.refinery.language.model.problem.Variable, Variable>(arity);
+                var parameterMap = HashMap.<tools.refinery.language.model.problem.Variable, Variable>newHashMap(arity);
                 var commonLiterals = new ArrayList<Literal>();
                 for (int i = 0; i < arity; i++) {
                         var problemParameter = problemParameters.get(i);
@@ -532,7 +568,7 @@ public class ModelInitializer {
                         return existing;
                 }
                 int localScopeSize = existing.size() + newVariables.size();
-                var localScope = new HashMap<tools.refinery.language.model.problem.Variable, Variable>(localScopeSize);
+                var localScope = HashMap.<tools.refinery.language.model.problem.Variable, Variable>newHashMap(localScopeSize);
                 localScope.putAll(existing);
                 for (var newVariable : newVariables) {
                         localScope.put(newVariable, Variable.of(newVariable.getName()));
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTree.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTree.java
index c732f784..5d25f148 100644
--- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTree.java
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTree.java
@@ -40,8 +40,8 @@ class DecisionTree implements MutableSeed<TruthValue> {
         }
 
         @Override
-        public TruthValue reducedValue() {
-                return root.getOtherwiseReducedValue().getTruthValue();
+        public TruthValue majorityValue() {
+                return root.getMajorityValue().getTruthValueOrElse(TruthValue.FALSE);
         }
 
         @Override
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTreeNode.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTreeNode.java
index ebca2634..31d6fc78 100644
--- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTreeNode.java
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTreeNode.java
@@ -100,6 +100,8 @@ abstract class DecisionTreeNode {
 
         protected abstract LazyIntIterable getChildKeys();
 
+        public abstract DecisionTreeValue getMajorityValue();
+
         protected abstract boolean moveNextSparse(int level, DecisionTreeCursor cursor, int startIndex,
                                                                                           int[] sortedChildren);
 
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/IntermediateNode.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/IntermediateNode.java
index 0e2f5d18..2ad216ce 100644
--- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/IntermediateNode.java
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/IntermediateNode.java
@@ -130,6 +130,11 @@ final class IntermediateNode extends DecisionTreeNode {
                 return children.keysView();
         }
 
+        @Override
+        public DecisionTreeValue getMajorityValue() {
+                return otherwise.getMajorityValue();
+        }
+
         protected boolean moveNextSparse(int level, DecisionTreeCursor cursor, int startIndex, int[] sortedChildren) {
                 for (int i = startIndex; i < sortedChildren.length; i++) {
                         var key = sortedChildren[i];
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/NullaryMutableSeed.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/NullaryMutableSeed.java
index 7a72c656..f100c5a6 100644
--- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/NullaryMutableSeed.java
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/NullaryMutableSeed.java
@@ -29,14 +29,14 @@ class NullaryMutableSeed implements MutableSeed<TruthValue> {
         }
 
         @Override
-        public TruthValue reducedValue() {
+        public TruthValue majorityValue() {
                 return value.getTruthValue();
         }
 
         @Override
         public TruthValue get(Tuple key) {
                 validateKey(key);
-                return reducedValue();
+                return majorityValue();
         }
 
         private static void validateKey(Tuple key) {
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/TerminalNode.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/TerminalNode.java
index d3dd757c..dc501479 100644
--- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/TerminalNode.java
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/TerminalNode.java
@@ -115,7 +115,7 @@ class TerminalNode extends DecisionTreeNode {
 
         @Override
         protected DecisionTreeValue getOtherwiseReducedValue() {
-                return otherwise;
+                return getMajorityValue();
         }
 
         @Override
@@ -124,6 +124,11 @@ class TerminalNode extends DecisionTreeNode {
         }
 
         @Override
+        public DecisionTreeValue getMajorityValue() {
+                return otherwise;
+        }
+
+        @Override
         protected boolean moveNextSparse(int level, DecisionTreeCursor cursor, int startIndex, int[] sortedChildren) {
                 if (startIndex >= sortedChildren.length) {
                         return false;
diff --git a/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/internal/DecisionTreeTests.java b/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/internal/DecisionTreeTests.java
index 2320de2c..61ce850f 100644
--- a/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/internal/DecisionTreeTests.java
+++ b/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/internal/DecisionTreeTests.java
@@ -276,6 +276,16 @@ class DecisionTreeTests {
                 assertThat(sut.getReducedValue(), is(TruthValue.TRUE));
         }
 
+        @Test
+        void overwriteWildcardAllTest() {
+                var first = new DecisionTree(2, TruthValue.UNKNOWN);
+                first.mergeValue(Tuple.of(-1, -1), TruthValue.FALSE);
+                var second = new DecisionTree(2, null);
+                second.mergeValue(Tuple.of(1, -1), TruthValue.TRUE);
+                first.overwriteValues(second);
+                assertThat(first.majorityValue(), is(TruthValue.FALSE));
+        }
+
         private Map<Tuple, TruthValue> iterateAll(DecisionTree sut, TruthValue defaultValue, int nodeCount) {
                 var cursor = sut.getCursor(defaultValue, nodeCount);
                 var map = new LinkedHashMap<Tuple, TruthValue>();