5 files changed, 293 insertions, 27 deletions

diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/MapBasedSeed.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/MapBasedSeed.java
new file mode 100644
index 00000000..8b1c3bb3
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/MapBasedSeed.java
@@ -0,0 +1,111 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.seed;
+
+import tools.refinery.store.map.Cursor;
+import tools.refinery.store.map.Cursors;
+import tools.refinery.store.tuple.Tuple;
+
+import java.util.Map;
+import java.util.Objects;
+
+record MapBasedSeed<T>(int arity, Class<T> valueType, T reducedValue, Map<Tuple, T> map) implements Seed<T> {
+        @Override
+        public T get(Tuple key) {
+                var value = map.get(key);
+                return value == null ? reducedValue : value;
+        }
+
+        @Override
+        public Cursor<Tuple, T> getCursor(T defaultValue, int nodeCount) {
+                if (Objects.equals(defaultValue, reducedValue)) {
+                        return Cursors.of(map);
+                }
+                return new CartesianProductCursor<>(arity, nodeCount, reducedValue, defaultValue, map);
+        }
+
+        private static class CartesianProductCursor<T> implements Cursor<Tuple, T> {
+                private final int nodeCount;
+                private final T reducedValue;
+                private final T defaultValue;
+                private final Map<Tuple, T> map;
+                private final int[] counter;
+                private State state = State.INITIAL;
+                private Tuple key;
+                private T value;
+
+                private CartesianProductCursor(int arity, int nodeCount, T reducedValue, T defaultValue, Map<Tuple, T> map) {
+                        this.nodeCount = nodeCount;
+                        this.reducedValue = reducedValue;
+                        this.defaultValue = defaultValue;
+                        this.map = map;
+                        counter = new int[arity];
+                }
+
+                @Override
+                public Tuple getKey() {
+                        return key;
+                }
+
+                @Override
+                public T getValue() {
+                        return value;
+                }
+
+                @Override
+                public boolean isTerminated() {
+                        return state == State.TERMINATED;
+                }
+
+                @Override
+                public boolean move() {
+                        return switch (state) {
+                                case INITIAL -> {
+                                        state = State.STARTED;
+                                        yield checkValue() || moveToNext();
+                                }
+                                case STARTED -> moveToNext();
+                                case TERMINATED -> false;
+                        };
+                }
+
+                private boolean moveToNext() {
+                        do {
+                                increment();
+                        } while (state != State.TERMINATED && !checkValue());
+                        return state != State.TERMINATED;
+                }
+
+                private void increment() {
+                        int i = counter.length - 1;
+                        while (i >= 0) {
+                                counter[i]++;
+                                if (counter[i] < nodeCount) {
+                                        return;
+                                }
+                                counter[i] = 0;
+                                i--;
+                        }
+                        state = State.TERMINATED;
+                }
+
+                private boolean checkValue() {
+                        key = Tuple.of(counter);
+                        var valueInMap = map.get(key);
+                        if (Objects.equals(valueInMap, defaultValue)) {
+                                return false;
+                        }
+                        value = valueInMap == null ? reducedValue : valueInMap;
+                        return true;
+                }
+
+                private enum State {
+                        INITIAL,
+                        STARTED,
+                        TERMINATED
+                }
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/ModelSeed.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/ModelSeed.java
new file mode 100644
index 00000000..e6b3eaf9
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/ModelSeed.java
@@ -0,0 +1,95 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.seed;
+
+import tools.refinery.store.map.Cursor;
+import tools.refinery.store.reasoning.representation.AnyPartialSymbol;
+import tools.refinery.store.reasoning.representation.PartialSymbol;
+import tools.refinery.store.tuple.Tuple;
+
+import java.util.Collections;
+import java.util.LinkedHashMap;
+import java.util.Map;
+import java.util.Set;
+import java.util.function.Consumer;
+
+public class ModelSeed {
+        private final int nodeCount;
+        private final Map<AnyPartialSymbol, Seed<?>> seeds;
+
+        private ModelSeed(int nodeCount, Map<AnyPartialSymbol, Seed<?>> seeds) {
+                this.nodeCount = nodeCount;
+                this.seeds = seeds;
+        }
+
+        public int getNodeCount() {
+                return nodeCount;
+        }
+
+        public <A> Seed<A> getSeed(PartialSymbol<A, ?> partialSymbol) {
+                var seed = seeds.get(partialSymbol);
+                if (seed == null) {
+                        throw new IllegalArgumentException("No seed for partial symbol " + partialSymbol);
+                }
+                // The builder makes sure only well-typed seeds can be added.
+                @SuppressWarnings("unchecked")
+                var typedSeed = (Seed<A>) seed;
+                return typedSeed;
+        }
+
+        public boolean containsSeed(AnyPartialSymbol symbol) {
+                return seeds.containsKey(symbol);
+        }
+
+        public Set<AnyPartialSymbol> getSeededSymbols() {
+                return Collections.unmodifiableSet(seeds.keySet());
+        }
+
+        public <A> Cursor<Tuple, A> getCursor(PartialSymbol<A, ?> partialSymbol, A defaultValue) {
+                return getSeed(partialSymbol).getCursor(defaultValue, nodeCount);
+        }
+
+        public static Builder builder(int nodeCount) {
+                return new Builder(nodeCount);
+        }
+
+        public static class Builder {
+                private final int nodeCount;
+                private final Map<AnyPartialSymbol, Seed<?>> seeds = new LinkedHashMap<>();
+
+                private Builder(int nodeCount) {
+                        if (nodeCount < 0) {
+                                throw new IllegalArgumentException("Node count must not be negative");
+                        }
+                        this.nodeCount = nodeCount;
+                }
+
+                public <A> Builder seed(PartialSymbol<A, ?> partialSymbol, Seed<A> seed) {
+                        if (seed.arity() != partialSymbol.arity()) {
+                                throw new IllegalStateException("Expected seed of arity %d for partial symbol %s, but got %d instead"
+                                                .formatted(partialSymbol.arity(), partialSymbol, seed.arity()));
+                        }
+                        if (!seed.valueType().equals(partialSymbol.abstractDomain().abstractType())) {
+                                throw new IllegalStateException("Expected seed of type %s for partial symbol %s, but got %s instead"
+                                                .formatted(partialSymbol.abstractDomain().abstractType(), partialSymbol, seed.valueType()));
+                        }
+                        if (seeds.put(partialSymbol, seed) != null) {
+                                throw new IllegalArgumentException("Duplicate seed for partial symbol " + partialSymbol);
+                        }
+                        return this;
+                }
+
+                public <A> Builder seed(PartialSymbol<A, ?> partialSymbol, Consumer<Seed.Builder<A>> callback) {
+                        var builder = Seed.builder(partialSymbol);
+                        callback.accept(builder);
+                        return seed(partialSymbol, builder.build());
+                }
+
+                public ModelSeed build() {
+                        return new ModelSeed(nodeCount, Collections.unmodifiableMap(seeds));
+                }
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/Seed.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/Seed.java
index 08079f12..732efbcc 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/Seed.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/Seed.java
@@ -6,14 +6,73 @@
 package tools.refinery.store.reasoning.seed;
 
 import tools.refinery.store.map.Cursor;
+import tools.refinery.store.reasoning.representation.PartialSymbol;
+import tools.refinery.store.representation.Symbol;
 import tools.refinery.store.tuple.Tuple;
 
+import java.util.Collections;
+import java.util.LinkedHashMap;
+import java.util.Map;
+
 public interface Seed<T> {
         int arity();
 
+        Class<T> valueType();
+
         T reducedValue();
 
         T get(Tuple key);
 
         Cursor<Tuple, T> getCursor(T defaultValue, int nodeCount);
+
+        static <T> Builder<T> builder(int arity, Class<T> valueType, T reducedValue) {
+                return new Builder<>(arity, valueType, reducedValue);
+        }
+
+        static <T> Builder<T> builder(Symbol<T> symbol) {
+                return builder(symbol.arity(), symbol.valueType(), symbol.defaultValue());
+        }
+
+        static <T> Builder<T> builder(PartialSymbol<T, ?> partialSymbol) {
+                return builder(partialSymbol.arity(), partialSymbol.abstractDomain().abstractType(),
+                                partialSymbol.defaultValue());
+        }
+
+        @SuppressWarnings("UnusedReturnValue")
+        class Builder<T> {
+                private final int arity;
+                private final Class<T> valueType;
+                private T reducedValue;
+                private final Map<Tuple, T> map = new LinkedHashMap<>();
+
+                private Builder(int arity, Class<T> valueType, T reducedValue) {
+                        this.arity = arity;
+                        this.valueType = valueType;
+                        this.reducedValue = reducedValue;
+                }
+
+                public Builder<T> reducedValue(T reducedValue) {
+                        this.reducedValue = reducedValue;
+                        return this;
+                }
+
+                public Builder<T> put(Tuple key, T value) {
+                        if (key.getSize() != arity) {
+                                throw new IllegalArgumentException("Expected %s to have %d elements".formatted(key, arity));
+                        }
+                        map.put(key, value);
+                        return this;
+                }
+
+                public Builder<T> putAll(Map<Tuple, T> map) {
+                        for (var entry : map.entrySet()) {
+                                put(entry.getKey(), entry.getValue());
+                        }
+                        return this;
+                }
+
+                public Seed<T> build() {
+                        return new MapBasedSeed<>(arity, valueType, reducedValue, Collections.unmodifiableMap(map));
+                }
+        }
 }
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/SeedInitializer.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/SeedInitializer.java
new file mode 100644
index 00000000..9af457d8
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/SeedInitializer.java
@@ -0,0 +1,28 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.seed;
+
+import tools.refinery.store.model.Model;
+import tools.refinery.store.reasoning.refinement.PartialModelInitializer;
+import tools.refinery.store.reasoning.representation.PartialSymbol;
+import tools.refinery.store.representation.Symbol;
+
+public class SeedInitializer<T> implements PartialModelInitializer {
+        private final Symbol<T> symbol;
+        private final PartialSymbol<T, ?> partialSymbol;
+
+        public SeedInitializer(Symbol<T> symbol, PartialSymbol<T, ?> partialSymbol) {
+                this.symbol = symbol;
+                this.partialSymbol = partialSymbol;
+        }
+
+        @Override
+        public void initialize(Model model, ModelSeed modelSeed) {
+                var interpretation = model.getInterpretation(symbol);
+                var cursor = modelSeed.getCursor(partialSymbol, symbol.defaultValue());
+                interpretation.putAll(cursor);
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/UniformSeed.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/UniformSeed.java
deleted file mode 100644
index 451d1513..00000000
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/UniformSeed.java
+++ /dev/null
@@ -1,27 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-package tools.refinery.store.reasoning.seed;
-
-import tools.refinery.store.map.Cursor;
-import tools.refinery.store.tuple.Tuple;
-
-public record UniformSeed<T>(int arity, T reducedValue) implements Seed<T> {
-        public UniformSeed {
-                if (arity < 0) {
-                        throw new IllegalArgumentException("Arity must not be negative");
-                }
-        }
-
-        @Override
-        public T get(Tuple key) {
-                return reducedValue;
-        }
-
-        @Override
-        public Cursor<Tuple, T> getCursor(T defaultValue, int nodeCount) {
-                return null;
-        }
-}