feat: data structure for assertion merging

7 files changed, 528 insertions, 0 deletions

diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/ModelInitializer.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/ModelInitializer.java
new file mode 100644
index 00000000..830d4a2c
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/ModelInitializer.java
@@ -0,0 +1,9 @@
+package tools.refinery.language.semantics.model;
+
+import tools.refinery.language.utils.CollectedSymbols;
+
+public class ModelInitializer {
+        public void createModel(CollectedSymbols symbols) {
+
+        }
+}
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/DecisionTree.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/DecisionTree.java
new file mode 100644
index 00000000..8c185509
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/DecisionTree.java
@@ -0,0 +1,41 @@
+package tools.refinery.language.semantics.model.internal;
+
+import org.eclipse.collections.api.factory.primitive.IntObjectMaps;
+import tools.refinery.store.map.Cursor;
+import tools.refinery.store.model.Tuple;
+import tools.refinery.store.model.representation.TruthValue;
+
+public class DecisionTree {
+        private final int levels;
+
+        private final DecisionTreeNode root;
+
+        public DecisionTree(int levels, TruthValue initialValue) {
+                this.levels = levels;
+                DecisionTreeNode node = new TerminalNode(IntObjectMaps.mutable.empty(),
+                                DecisionTreeValue.fromTruthValue(initialValue));
+                for (int level = 1; level < levels; level++) {
+                        node = new IntermediateNode(IntObjectMaps.mutable.empty(), node);
+                }
+                root = node;
+        }
+
+        public TruthValue get(Tuple tuple) {
+                return root.getValue(levels - 1, tuple).getTruthValue();
+        }
+
+        public void mergeValue(Tuple tuple, TruthValue truthValue) {
+                if (truthValue == null) {
+                        return;
+                }
+                root.mergeValue(levels - 1, tuple, truthValue);
+        }
+
+        public void overwriteValues(DecisionTree values) {
+                root.overwriteValues(values.root);
+        }
+
+        public Cursor<Tuple, TruthValue> getCursor(TruthValue defaultValue, int nodeCount) {
+                return new DecisionTreeCursor(levels, defaultValue, nodeCount, root);
+        }
+}
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/DecisionTreeCursor.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/DecisionTreeCursor.java
new file mode 100644
index 00000000..8b02ba39
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/DecisionTreeCursor.java
@@ -0,0 +1,94 @@
+package tools.refinery.language.semantics.model.internal;
+
+import tools.refinery.store.map.Cursor;
+import tools.refinery.store.map.VersionedMap;
+import tools.refinery.store.model.Tuple;
+import tools.refinery.store.model.representation.TruthValue;
+
+import java.util.ArrayDeque;
+import java.util.Deque;
+import java.util.List;
+
+class DecisionTreeCursor implements Cursor<Tuple, TruthValue> {
+        static final int STATE_FINISH = Integer.MAX_VALUE;
+
+        private final int levels;
+
+        final DecisionTreeValue defaultValue;
+
+        final int nodeCount;
+
+        private final DecisionTreeNode root;
+
+        final int[][] sortedChildren;
+
+        final int[] iterationState;
+
+        final int[] rawTuple;
+
+        final Deque<DecisionTreeNode> path = new ArrayDeque<>();
+
+        private Tuple key;
+
+        DecisionTreeValue value = DecisionTreeValue.UNSET;
+
+        private boolean terminated;
+
+        public DecisionTreeCursor(int levels, TruthValue defaultValue, int nodeCount, DecisionTreeNode root) {
+                this.levels = levels;
+                this.defaultValue = DecisionTreeValue.fromTruthValue(defaultValue);
+                this.nodeCount = nodeCount;
+                this.root = root;
+                sortedChildren = new int[levels][];
+                iterationState = new int[levels];
+                for (int i = 0; i < levels; i++) {
+                        iterationState[i] = STATE_FINISH;
+                }
+                rawTuple = new int[levels];
+        }
+
+        @Override
+        public Tuple getKey() {
+                return key;
+        }
+
+        @Override
+        public TruthValue getValue() {
+                return value.getTruthValue();
+        }
+
+        @Override
+        public boolean isTerminated() {
+                return terminated;
+        }
+
+        @Override
+        public boolean move() {
+                boolean found = false;
+                if (path.isEmpty() && !terminated) {
+                        found = root.moveNext(levels - 1, this);
+                }
+                while (!found && !path.isEmpty()) {
+                        int level = levels - path.size();
+                        found = path.peek().moveNext(level, this);
+                }
+                if (!found) {
+                        key = null;
+                        value = DecisionTreeValue.UNSET;
+                        terminated = true;
+                        return false;
+                }
+                key = Tuple.of(rawTuple);
+                return true;
+        }
+
+        @Override
+        public boolean isDirty() {
+                return false;
+        }
+
+        @Override
+        public List<VersionedMap<?, ?>> getDependingMaps() {
+                return List.of();
+        }
+}
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/DecisionTreeNode.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/DecisionTreeNode.java
new file mode 100644
index 00000000..53954d62
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/DecisionTreeNode.java
@@ -0,0 +1,84 @@
+package tools.refinery.language.semantics.model.internal;
+
+import org.eclipse.collections.api.LazyIntIterable;
+import tools.refinery.store.model.Tuple;
+import tools.refinery.store.model.representation.TruthValue;
+
+abstract class DecisionTreeNode {
+        public DecisionTreeValue getReducedValue() {
+                return getChildKeys().isEmpty() ? getOtherwiseReducedValue() : null;
+        }
+
+        public abstract DecisionTreeValue getValue(int level, Tuple tuple);
+
+        public abstract DecisionTreeNode deepCopy();
+
+        public void mergeValue(int level, Tuple tuple, TruthValue value) {
+                int nextLevel = level - 1;
+                var key = tuple.get(level);
+                if (key < 0) {
+                        mergeAllValues(nextLevel, tuple, value);
+                } else {
+                        mergeSingleValue(key, nextLevel, tuple, value);
+                }
+        }
+
+        protected abstract void mergeAllValues(int nextLevel, Tuple tuple, TruthValue value);
+
+        protected abstract void mergeSingleValue(int key, int nextLevel, Tuple tuple, TruthValue value);
+
+        public DecisionTreeNode withMergedValue(int level, Tuple tuple, TruthValue value) {
+                var copy = deepCopy();
+                copy.mergeValue(level, tuple, value);
+                return copy;
+        }
+
+        public abstract void overwriteValues(DecisionTreeNode values);
+
+        public DecisionTreeNode withOverwrittenValues(DecisionTreeNode values) {
+                var copy = deepCopy();
+                copy.overwriteValues(values);
+                return copy;
+        }
+
+        public boolean moveNext(int level, DecisionTreeCursor cursor) {
+                var currentState = cursor.iterationState[level];
+                boolean found;
+                if (currentState == DecisionTreeCursor.STATE_FINISH) {
+                        // Entering this node for the first time.
+                        cursor.path.push(this);
+                        if (cursor.defaultValue == getOtherwiseReducedValue()) {
+                                var sortedChildren = getChildKeys().toSortedArray();
+                                cursor.sortedChildren[level] = sortedChildren;
+                                found = moveNextSparse(level, cursor, 0, sortedChildren);
+                        } else {
+                                found = moveNextDense(level, cursor, 0);
+                        }
+                } else {
+                        var sortedChildren = cursor.sortedChildren[level];
+                        if (sortedChildren == null) {
+                                found = moveNextDense(level, cursor, currentState + 1);
+                        } else {
+                                found = moveNextSparse(level, cursor, currentState + 1, sortedChildren);
+                        }
+                }
+                if (!found) {
+                        cursor.sortedChildren[level] = null;
+                        cursor.iterationState[level] = DecisionTreeCursor.STATE_FINISH;
+                        var popped = cursor.path.pop();
+                        if (popped != this) {
+                                throw new IllegalStateException("Invalid decision diagram cursor");
+                        }
+                }
+                return found;
+        }
+
+        protected abstract DecisionTreeValue getOtherwiseReducedValue();
+
+        protected abstract LazyIntIterable getChildKeys();
+
+        protected abstract boolean moveNextSparse(int level, DecisionTreeCursor cursor, int startIndex,
+                                                                                          int[] sortedChildren);
+
+        protected abstract boolean moveNextDense(int level, DecisionTreeCursor cursor, int startIndex);
+}
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/DecisionTreeValue.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/DecisionTreeValue.java
new file mode 100644
index 00000000..1bf3c8b8
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/DecisionTreeValue.java
@@ -0,0 +1,41 @@
+package tools.refinery.language.semantics.model.internal;
+
+import tools.refinery.store.model.representation.TruthValue;
+
+public enum DecisionTreeValue {
+        UNSET(null),
+        TRUE(TruthValue.TRUE),
+        FALSE(TruthValue.FALSE),
+        UNKNOWN(TruthValue.UNKNOWN),
+        ERROR(TruthValue.ERROR);
+
+        final TruthValue truthValue;
+
+        DecisionTreeValue(TruthValue truthValue) {
+                this.truthValue = truthValue;
+        }
+
+        public TruthValue getTruthValue() {
+                return truthValue;
+        }
+
+        public DecisionTreeValue merge(TruthValue other) {
+                return truthValue == null ? fromTruthValue(other) : fromTruthValue(truthValue.merge(other));
+        }
+
+        public DecisionTreeValue overwrite(DecisionTreeValue other) {
+                return other == UNSET ? this : other;
+        }
+
+        public static DecisionTreeValue fromTruthValue(TruthValue truthValue) {
+                if (truthValue == null) {
+                        return DecisionTreeValue.UNSET;
+                }
+                return switch (truthValue) {
+                        case TRUE -> TRUE;
+                        case FALSE -> FALSE;
+                        case UNKNOWN -> UNKNOWN;
+                        case ERROR -> ERROR;
+                };
+        }
+}
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/IntermediateNode.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/IntermediateNode.java
new file mode 100644
index 00000000..acc53e73
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/IntermediateNode.java
@@ -0,0 +1,130 @@
+package tools.refinery.language.semantics.model.internal;
+
+import org.eclipse.collections.api.LazyIntIterable;
+import org.eclipse.collections.api.factory.primitive.IntObjectMaps;
+import org.eclipse.collections.api.map.primitive.MutableIntObjectMap;
+import org.eclipse.collections.api.tuple.primitive.IntObjectPair;
+import tools.refinery.store.model.Tuple;
+import tools.refinery.store.model.representation.TruthValue;
+
+final class IntermediateNode extends DecisionTreeNode {
+        private final MutableIntObjectMap<DecisionTreeNode> children;
+
+        private final DecisionTreeNode otherwise;
+
+        IntermediateNode(MutableIntObjectMap<DecisionTreeNode> children, DecisionTreeNode otherwise) {
+                this.children = children;
+                this.otherwise = otherwise;
+        }
+
+        private DecisionTreeNode getChild(int index) {
+                var child = children.get(index);
+                return child == null ? otherwise : child;
+        }
+
+        @Override
+        public DecisionTreeValue getValue(int level, Tuple tuple) {
+                return getChild(tuple.get(level)).getValue(level - 1, tuple);
+        }
+
+        @Override
+        public DecisionTreeNode deepCopy() {
+                var newChildren = IntObjectMaps.mutable.from(children.keyValuesView(), IntObjectPair::getOne,
+                                pair -> pair.getTwo().deepCopy());
+                var newOtherwise = otherwise.deepCopy();
+                return new IntermediateNode(newChildren, newOtherwise);
+        }
+
+        @Override
+        protected void mergeAllValues(int nextLevel, Tuple tuple, TruthValue value) {
+                otherwise.mergeValue(nextLevel, tuple, value);
+                for (var child : children) {
+                        child.mergeValue(nextLevel, tuple, value);
+                }
+                reduceChildren();
+        }
+
+        @Override
+        protected void mergeSingleValue(int key, int nextLevel, Tuple tuple, TruthValue value) {
+                var otherwiseReduced = getOtherwiseReducedValue();
+                var child = children.get(key);
+                if (child == null) {
+                        var newChild = otherwise.withMergedValue(nextLevel, tuple, value);
+                        if (otherwiseReduced == null || newChild.getReducedValue() != otherwiseReduced) {
+                                children.put(key, newChild);
+                        }
+                        return;
+                }
+                child.mergeValue(nextLevel, tuple, value);
+                if (otherwiseReduced != null && child.getReducedValue() == otherwiseReduced) {
+                        children.remove(key);
+                }
+        }
+
+        @Override
+        public void overwriteValues(DecisionTreeNode values) {
+                if (values instanceof IntermediateNode intermediateValues) {
+                        otherwise.overwriteValues(intermediateValues.otherwise);
+                        for (var pair : children.keyValuesView()) {
+                                pair.getTwo().overwriteValues(intermediateValues.getChild(pair.getOne()));
+                        }
+                        for (var pair : intermediateValues.children.keyValuesView()) {
+                                children.getIfAbsentPut(pair.getOne(), () -> otherwise.withOverwrittenValues(pair.getTwo()));
+                        }
+                        reduceChildren();
+                } else {
+                        throw new IllegalArgumentException("Level mismatch");
+                }
+        }
+
+        private void reduceChildren() {
+                var otherwiseReduced = getOtherwiseReducedValue();
+                if (otherwiseReduced == null) {
+                        return;
+                }
+                var iterator = children.iterator();
+                while (iterator.hasNext()) {
+                        var child = iterator.next();
+                        if (child.getReducedValue() == otherwiseReduced) {
+                                iterator.remove();
+                        }
+                }
+        }
+
+        @Override
+        protected DecisionTreeValue getOtherwiseReducedValue() {
+                return otherwise.getReducedValue();
+        }
+
+        @Override
+        protected LazyIntIterable getChildKeys() {
+                return children.keysView();
+        }
+
+        protected boolean moveNextSparse(int level, DecisionTreeCursor cursor, int startIndex, int[] sortedChildren) {
+                for (int i = startIndex; i < sortedChildren.length; i++) {
+                        var key = sortedChildren[i];
+                        var child = getChild(key);
+                        var found = child.moveNext(level - 1, cursor);
+                        if (found) {
+                                cursor.iterationState[level] = i;
+                                cursor.rawTuple[level] = key;
+                                return true;
+                        }
+                }
+                return false;
+        }
+
+        protected boolean moveNextDense(int level, DecisionTreeCursor cursor, int startIndex) {
+                for (int i = startIndex; i < cursor.nodeCount; i++) {
+                        var child = getChild(i);
+                        var found = child.moveNext(level - 1, cursor);
+                        if (found) {
+                                cursor.iterationState[level] = i;
+                                cursor.rawTuple[level] = i;
+                                return true;
+                        }
+                }
+                return false;
+        }
+}
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/TerminalNode.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/TerminalNode.java
new file mode 100644
index 00000000..20dd6b20
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/TerminalNode.java
@@ -0,0 +1,129 @@
+package tools.refinery.language.semantics.model.internal;
+
+import org.eclipse.collections.api.LazyIntIterable;
+import org.eclipse.collections.api.factory.primitive.IntObjectMaps;
+import org.eclipse.collections.api.map.primitive.MutableIntObjectMap;
+import org.eclipse.collections.api.tuple.primitive.IntObjectPair;
+import tools.refinery.store.model.Tuple;
+import tools.refinery.store.model.representation.TruthValue;
+
+class TerminalNode extends DecisionTreeNode {
+        private MutableIntObjectMap<DecisionTreeValue> children;
+
+        private DecisionTreeValue otherwise;
+
+        TerminalNode(MutableIntObjectMap<DecisionTreeValue> children, DecisionTreeValue otherwise) {
+                this.children = children;
+                this.otherwise = otherwise;
+        }
+
+        private DecisionTreeValue getChild(int index) {
+                var child = children.get(index);
+                return child == null ? otherwise : child;
+        }
+
+        @Override
+        public DecisionTreeValue getValue(int level, Tuple tuple) {
+                assertLevel(level);
+                return getChild(tuple.get(level));
+        }
+
+        @Override
+        public DecisionTreeNode deepCopy() {
+                return new TerminalNode(IntObjectMaps.mutable.ofAll(children), otherwise);
+        }
+
+        @Override
+        public void mergeValue(int level, Tuple tuple, TruthValue value) {
+                assertLevel(level);
+                super.mergeValue(level, tuple, value);
+        }
+
+        @Override
+        protected void mergeAllValues(int nextLevel, Tuple tuple, TruthValue value) {
+                otherwise = otherwise.merge(value);
+                children = IntObjectMaps.mutable.from(children.keyValuesView(), IntObjectPair::getOne,
+                                pair -> pair.getTwo().merge(value));
+                reduceChildren();
+        }
+
+        @Override
+        protected void mergeSingleValue(int key, int nextLevel, Tuple tuple, TruthValue value) {
+                var newChild = getChild(key).merge(value);
+                if (newChild == otherwise) {
+                        children.remove(key);
+                } else {
+                        children.put(key, newChild);
+                }
+        }
+
+        @Override
+        public void overwriteValues(DecisionTreeNode values) {
+                if (values instanceof TerminalNode terminalValues) {
+                        otherwise = otherwise.overwrite(terminalValues.otherwise);
+                        children = IntObjectMaps.mutable.from(children.keyValuesView(), IntObjectPair::getOne,
+                                        pair -> pair.getTwo().overwrite(terminalValues.getChild(pair.getOne())));
+                        for (var pair : terminalValues.children.keyValuesView()) {
+                                children.getIfAbsentPut(pair.getOne(), otherwise.overwrite(pair.getTwo()));
+                        }
+                        reduceChildren();
+                } else {
+                        throw new IllegalArgumentException("Level mismatch");
+                }
+        }
+
+        private void reduceChildren() {
+                var iterator = children.iterator();
+                while (iterator.hasNext()) {
+                        var child = iterator.next();
+                        if (child == otherwise) {
+                                iterator.remove();
+                        }
+                }
+        }
+
+        @Override
+        public boolean moveNext(int level, DecisionTreeCursor cursor) {
+                assertLevel(level);
+                return super.moveNext(level, cursor);
+        }
+
+        @Override
+        protected DecisionTreeValue getOtherwiseReducedValue() {
+                return otherwise;
+        }
+
+        @Override
+        protected LazyIntIterable getChildKeys() {
+                return children.keysView();
+        }
+
+        @Override
+        protected boolean moveNextSparse(int level, DecisionTreeCursor cursor, int startIndex, int[] sortedChildren) {
+                if (startIndex >= sortedChildren.length) {
+                        return false;
+                }
+                var key = sortedChildren[startIndex];
+                cursor.iterationState[level] = startIndex;
+                cursor.rawTuple[level] = key;
+                cursor.value = getChild(key);
+                return true;
+        }
+
+        @Override
+        protected boolean moveNextDense(int level, DecisionTreeCursor cursor, int startIndex) {
+                if (startIndex >= cursor.nodeCount) {
+                        return false;
+                }
+                cursor.iterationState[level] = startIndex;
+                cursor.rawTuple[level] = startIndex;
+                cursor.value = getChild(startIndex);
+                return true;
+        }
+
+        private static void assertLevel(int level) {
+                if (level != 0) {
+                        throw new IllegalArgumentException("Invalid decision tree level: " + level);
+                }
+        }
+}