10 files changed, 174 insertions, 39 deletions

diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/CleanupActionLiteral.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/CleanupActionLiteral.java
new file mode 100644
index 00000000..62c35cee
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/CleanupActionLiteral.java
@@ -0,0 +1,43 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.actions;
+
+import tools.refinery.store.dse.transition.actions.AbstractActionLiteral;
+import tools.refinery.store.dse.transition.actions.BoundActionLiteral;
+import tools.refinery.store.model.Model;
+import tools.refinery.store.query.term.NodeVariable;
+import tools.refinery.store.reasoning.ReasoningAdapter;
+import tools.refinery.store.tuple.Tuple;
+
+import java.util.List;
+
+public class CleanupActionLiteral extends AbstractActionLiteral {
+        private final NodeVariable node;
+
+        public CleanupActionLiteral(NodeVariable node) {
+                this.node = node;
+        }
+
+        public NodeVariable getNode() {
+                return node;
+        }
+
+        @Override
+        public List<NodeVariable> getInputVariables() {
+                return List.of(node);
+        }
+
+        @Override
+        public List<NodeVariable> getOutputVariables() {
+                return List.of();
+        }
+
+        @Override
+        public BoundActionLiteral bindToModel(Model model) {
+                var reasoningAdapter = model.getAdapter(ReasoningAdapter.class);
+                return tuple -> reasoningAdapter.cleanup(tuple.get(0)) ? Tuple.of() : null;
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/PartialActionLiterals.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/PartialActionLiterals.java
index 990d11e5..f36fde44 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/PartialActionLiterals.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/PartialActionLiterals.java
@@ -35,4 +35,8 @@ public final class PartialActionLiterals {
         public static FocusActionLiteral focus(NodeVariable parent, NodeVariable child) {
                 return new FocusActionLiteral(parent, child);
         }
+
+        public static CleanupActionLiteral cleanup(NodeVariable node) {
+                return new CleanupActionLiteral(node);
+        }
 }
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningBuilderImpl.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningBuilderImpl.java
index d2cd2eb0..722458c8 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningBuilderImpl.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningBuilderImpl.java
@@ -18,18 +18,19 @@ import tools.refinery.store.query.dnf.Query;
 import tools.refinery.store.query.dnf.RelationalQuery;
 import tools.refinery.store.reasoning.ReasoningBuilder;
 import tools.refinery.store.reasoning.interpretation.PartialInterpretation;
-import tools.refinery.store.reasoning.refinement.DefaultStorageRefiner;
-import tools.refinery.store.reasoning.translator.AnyPartialSymbolTranslator;
-import tools.refinery.store.reasoning.translator.PartialRelationTranslator;
 import tools.refinery.store.reasoning.lifting.DnfLifter;
 import tools.refinery.store.reasoning.literal.Concreteness;
 import tools.refinery.store.reasoning.literal.Modality;
+import tools.refinery.store.reasoning.refinement.DefaultStorageRefiner;
 import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner;
 import tools.refinery.store.reasoning.refinement.PartialModelInitializer;
 import tools.refinery.store.reasoning.refinement.StorageRefiner;
 import tools.refinery.store.reasoning.representation.AnyPartialSymbol;
+import tools.refinery.store.reasoning.translator.AnyPartialSymbolTranslator;
+import tools.refinery.store.reasoning.translator.PartialRelationTranslator;
 import tools.refinery.store.representation.AnySymbol;
 import tools.refinery.store.representation.Symbol;
+import tools.refinery.store.statecoding.StateCoderBuilder;
 
 import java.util.*;
 
@@ -109,6 +110,8 @@ public class ReasoningBuilderImpl extends AbstractModelAdapterBuilder<ReasoningS
         @Override
         protected void doConfigure(ModelStoreBuilder storeBuilder) {
                 storeBuilder.symbols(ReasoningAdapterImpl.NODE_COUNT_SYMBOL);
+                storeBuilder.tryGetAdapter(StateCoderBuilder.class)
+                                .ifPresent(stateCoderBuilder -> stateCoderBuilder.exclude(ReasoningAdapterImpl.NODE_COUNT_SYMBOL));
                 for (var translator : translators.values()) {
                         translator.configure(storeBuilder);
                         if (translator instanceof PartialRelationTranslator relationConfiguration) {
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningStoreAdapterImpl.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningStoreAdapterImpl.java
index 8eb5a034..9ef6fb16 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningStoreAdapterImpl.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningStoreAdapterImpl.java
@@ -5,6 +5,7 @@
  */
 package tools.refinery.store.reasoning.internal;
 
+import tools.refinery.store.dse.propagation.PropagationAdapter;
 import tools.refinery.store.model.Model;
 import tools.refinery.store.model.ModelStore;
 import tools.refinery.store.query.ModelQueryAdapter;
@@ -103,6 +104,11 @@ class ReasoningStoreAdapterImpl implements ReasoningStoreAdapter {
                 for (var initializer : initializers) {
                         initializer.initialize(model, modelSeed);
                 }
+                model.tryGetAdapter(PropagationAdapter.class).ifPresent(propagationAdapter -> {
+                        if (propagationAdapter.propagate().isRejected()) {
+                                throw new IllegalArgumentException("Inconsistent initial mode: propagation failed");
+                        }
+                });
                 model.getAdapter(ModelQueryAdapter.class).flushChanges();
                 return model;
         }
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/RefinementResult.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/RefinementResult.java
deleted file mode 100644
index 1bc537d1..00000000
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/RefinementResult.java
+++ /dev/null
@@ -1,24 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-package tools.refinery.store.reasoning.refinement;
-
-public enum RefinementResult {
-        UNCHANGED,
-        REFINED,
-        REJECTED;
-
-        public RefinementResult andThen(RefinementResult next) {
-                return switch (this) {
-                        case UNCHANGED -> next;
-                        case REFINED -> next == REJECTED ? REJECTED : REFINED;
-                        case REJECTED -> REJECTED;
-                };
-        }
-
-        public boolean isRejected() {
-                return this == REJECTED;
-        }
-}
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 5c3298ac..61037be3 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
@@ -243,7 +243,7 @@ public class ContainmentHierarchyTranslator implements ModelStoreConfiguration {
                                                 MultiObjectTranslator.MULTI_VIEW.call(multi),
                                                 not(may(CONTAINED_SYMBOL.call(multi)))
                                 )
-                                .clause((container) -> List.of(
+                                .clause(container -> List.of(
                                                 MultiObjectTranslator.MULTI_VIEW.call(multi),
                                                 must(CONTAINS_SYMBOL.call(container, multi)),
                                                 not(MultiObjectTranslator.MULTI_VIEW.call(container))
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/InferredContainment.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/InferredContainment.java
index 90802864..8df23d9a 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/InferredContainment.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/InferredContainment.java
@@ -8,18 +8,23 @@ package tools.refinery.store.reasoning.translator.containment;
 import tools.refinery.store.reasoning.representation.PartialRelation;
 import tools.refinery.store.representation.TruthValue;
 
+import java.util.Objects;
 import java.util.Set;
 
-record InferredContainment(TruthValue contains, Set<PartialRelation> mustLinks,
-                                                   Set<PartialRelation> forbiddenLinks) {
+final class InferredContainment {
         public static final InferredContainment UNKNOWN = new InferredContainment(
                         TruthValue.UNKNOWN, Set.of(), Set.of());
+        private final TruthValue contains;
+        private final Set<PartialRelation> mustLinks;
+        private final Set<PartialRelation> forbiddenLinks;
+        private final int hashCode;
 
         public InferredContainment(TruthValue contains, Set<PartialRelation> mustLinks,
                                                            Set<PartialRelation> forbiddenLinks) {
                 this.contains = adjustContains(contains, mustLinks, forbiddenLinks);
                 this.mustLinks = mustLinks;
                 this.forbiddenLinks = forbiddenLinks;
+                hashCode = Objects.hash(contains, mustLinks, forbiddenLinks);
         }
 
         private static TruthValue adjustContains(TruthValue contains, Set<PartialRelation> mustLinks,
@@ -34,4 +39,39 @@ record InferredContainment(TruthValue contains, Set<PartialRelation> mustLinks,
                 }
                 return result;
         }
+
+        public TruthValue contains() {
+                return contains;
+        }
+
+        public Set<PartialRelation> mustLinks() {
+                return mustLinks;
+        }
+
+        public Set<PartialRelation> forbiddenLinks() {
+                return forbiddenLinks;
+        }
+
+        @Override
+        public boolean equals(Object obj) {
+                if (obj == this) return true;
+                if (obj == null || obj.getClass() != this.getClass()) return false;
+                var that = (InferredContainment) obj;
+                return Objects.equals(this.contains, that.contains) &&
+                                Objects.equals(this.mustLinks, that.mustLinks) &&
+                                Objects.equals(this.forbiddenLinks, that.forbiddenLinks);
+        }
+
+        @Override
+        public int hashCode() {
+                return hashCode;
+        }
+
+        @Override
+        public String toString() {
+                return "InferredContainment[" +
+                                "contains=" + contains + ", " +
+                                "mustLinks=" + mustLinks + ", " +
+                                "forbiddenLinks=" + forbiddenLinks + ']';
+        }
 }
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 05704096..bad96a66 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
@@ -5,17 +5,21 @@
  */
 package tools.refinery.store.reasoning.translator.multiobject;
 
+import tools.refinery.store.dse.propagation.PropagationBuilder;
+import tools.refinery.store.dse.transition.Rule;
 import tools.refinery.store.dse.transition.objectives.Criteria;
 import tools.refinery.store.dse.transition.objectives.Objectives;
 import tools.refinery.store.model.ModelStoreBuilder;
 import tools.refinery.store.model.ModelStoreConfiguration;
 import tools.refinery.store.query.dnf.Query;
+import tools.refinery.store.query.literal.Literals;
 import tools.refinery.store.query.term.Variable;
 import tools.refinery.store.query.term.int_.IntTerms;
 import tools.refinery.store.query.term.uppercardinality.UpperCardinalityTerms;
 import tools.refinery.store.query.view.AnySymbolView;
 import tools.refinery.store.reasoning.ReasoningAdapter;
 import tools.refinery.store.reasoning.ReasoningBuilder;
+import tools.refinery.store.reasoning.actions.PartialActionLiterals;
 import tools.refinery.store.reasoning.representation.PartialFunction;
 import tools.refinery.store.reasoning.translator.PartialRelationTranslator;
 import tools.refinery.store.reasoning.translator.RoundingMode;
@@ -66,6 +70,11 @@ public class MultiObjectTranslator implements ModelStoreConfiguration {
                                                                 LOWER_CARDINALITY_VIEW.call(p1, lower),
                                                                 check(greaterEq(lower, constant(1)))
                                                 ))))
+                                .candidate(Query.of("exists#candidate", (builder, p1) -> builder
+                                                .clause(
+                                                                LOWER_CARDINALITY_VIEW.call(p1, Variable.of(Integer.class)),
+                                                                Literals.not(MULTI_VIEW.call(p1))
+                                                )))
                                 .roundingMode(RoundingMode.PREFER_FALSE)
                                 .refiner(ExistsRefiner.of(COUNT_STORAGE))
                                 .exclude(null)
@@ -82,5 +91,17 @@ public class MultiObjectTranslator implements ModelStoreConfiguration {
                 var reasoningBuilder = storeBuilder.getAdapter(ReasoningBuilder.class);
                 reasoningBuilder.initializer(new MultiObjectInitializer(COUNT_STORAGE));
                 reasoningBuilder.storageRefiner(COUNT_STORAGE, MultiObjectStorageRefiner::new);
+
+                storeBuilder.tryGetAdapter(PropagationBuilder.class)
+                                .ifPresent(propagationBuilder -> propagationBuilder.rule(
+                                                Rule.of("exists#cleanup", (builder, node) -> builder
+                                                                .clause(UpperCardinality.class, upper -> List.of(
+                                                                                UPPER_CARDINALITY_VIEW.call(node, upper),
+                                                                                check(UpperCardinalityTerms.less(upper,
+                                                                                                UpperCardinalityTerms.constant(UpperCardinalities.ONE)))
+                                                                ))
+                                                                .action(
+                                                                                PartialActionLiterals.cleanup(node)
+                                                                ))));
         }
 }
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredType.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredType.java
index 1ae94ae1..9a0c2b0f 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredType.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredType.java
@@ -8,17 +8,22 @@ package tools.refinery.store.reasoning.translator.typehierarchy;
 import tools.refinery.store.reasoning.representation.PartialRelation;
 
 import java.util.Collections;
+import java.util.Objects;
 import java.util.Set;
 
-record InferredType(Set<PartialRelation> mustTypes, Set<PartialRelation> mayConcreteTypes,
-                                        PartialRelation candidateType) {
+public final class InferredType {
         public static final InferredType UNTYPED = new InferredType(Set.of(), Set.of(), null);
+        private final Set<PartialRelation> mustTypes;
+        private final Set<PartialRelation> mayConcreteTypes;
+        private final PartialRelation candidateType;
+        private final int hashCode;
 
         public InferredType(Set<PartialRelation> mustTypes, Set<PartialRelation> mayConcreteTypes,
                                                 PartialRelation candidateType) {
                 this.mustTypes = Collections.unmodifiableSet(mustTypes);
                 this.mayConcreteTypes = Collections.unmodifiableSet(mayConcreteTypes);
                 this.candidateType = candidateType;
+                hashCode = Objects.hash(mustTypes, mayConcreteTypes, candidateType);
         }
 
         public boolean isConsistent() {
@@ -32,4 +37,40 @@ record InferredType(Set<PartialRelation> mustTypes, Set<PartialRelation> mayConc
         public boolean isMayConcrete(PartialRelation partialRelation) {
                 return mayConcreteTypes.contains(partialRelation);
         }
+
+
+        public Set<PartialRelation> mustTypes() {
+                return mustTypes;
+        }
+
+        public Set<PartialRelation> mayConcreteTypes() {
+                return mayConcreteTypes;
+        }
+
+        public PartialRelation candidateType() {
+                return candidateType;
+        }
+
+        @Override
+        public boolean equals(Object o) {
+                if (this == o) return true;
+                if (o == null || getClass() != o.getClass()) return false;
+                InferredType that = (InferredType) o;
+                return Objects.equals(mustTypes, that.mustTypes) &&
+                                Objects.equals(mayConcreteTypes, that.mayConcreteTypes) &&
+                                Objects.equals(candidateType, that.candidateType);
+        }
+
+        @Override
+        public int hashCode() {
+                return hashCode;
+        }
+
+        @Override
+        public String toString() {
+                return "InferredType[" +
+                                "mustTypes=" + mustTypes + ", " +
+                                "mayConcreteTypes=" + mayConcreteTypes + ", " +
+                                "candidateType=" + candidateType + ']';
+        }
 }
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslator.java
index dc8a1d36..37ea1448 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslator.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslator.java
@@ -26,7 +26,8 @@ import static tools.refinery.store.reasoning.literal.PartialLiterals.candidateMu
 import static tools.refinery.store.reasoning.literal.PartialLiterals.may;
 
 public class TypeHierarchyTranslator implements ModelStoreConfiguration {
-        private final Symbol<InferredType> typeSymbol = Symbol.of("TYPE", 1, InferredType.class, InferredType.UNTYPED);
+        public static final Symbol<InferredType> TYPE_SYMBOL = Symbol.of("TYPE", 1, InferredType.class,
+                        InferredType.UNTYPED);
         private final TypeHierarchy typeHierarchy;
 
         public TypeHierarchyTranslator(TypeHierarchy typeHierarchy) {
@@ -39,7 +40,7 @@ public class TypeHierarchyTranslator implements ModelStoreConfiguration {
                         return;
                 }
 
-                storeBuilder.symbol(typeSymbol);
+                storeBuilder.symbol(TYPE_SYMBOL);
 
                 for (var entry : typeHierarchy.getPreservedTypes().entrySet()) {
                         storeBuilder.with(createPreservedTypeTranslator(entry.getKey(), entry.getValue()));
@@ -50,13 +51,13 @@ public class TypeHierarchyTranslator implements ModelStoreConfiguration {
                 }
 
                 var reasoningBuilder = storeBuilder.getAdapter(ReasoningBuilder.class);
-                reasoningBuilder.initializer(new TypeHierarchyInitializer(typeHierarchy, typeSymbol));
+                reasoningBuilder.initializer(new TypeHierarchyInitializer(typeHierarchy, TYPE_SYMBOL));
         }
 
         private ModelStoreConfiguration createPreservedTypeTranslator(PartialRelation type, TypeAnalysisResult result) {
                 var may = Query.of(type.name() + "#partial#may", (builder, p1) -> {
                         if (!result.isAbstractType()) {
-                                builder.clause(new MayTypeView(typeSymbol, type).call(p1));
+                                builder.clause(new MayTypeView(TYPE_SYMBOL, type).call(p1));
                         }
                         for (var subtype : result.getDirectSubtypes()) {
                                 builder.clause(may(subtype.call(p1)));
@@ -64,12 +65,12 @@ public class TypeHierarchyTranslator implements ModelStoreConfiguration {
                 });
 
                 var must = Query.of(type.name() + "#partial#must", (builder, p1) -> builder.clause(
-                                new MustTypeView(typeSymbol, type).call(p1)
+                                new MustTypeView(TYPE_SYMBOL, type).call(p1)
                 ));
 
                 var candidate = Query.of(type.name() + "#candidate", (builder, p1) -> {
                         if (!result.isAbstractType()) {
-                                builder.clause(new CandidateTypeView(typeSymbol, type).call(p1));
+                                builder.clause(new CandidateTypeView(TYPE_SYMBOL, type).call(p1));
                         }
                         for (var subtype : result.getDirectSubtypes()) {
                                 builder.clause(PartialLiterals.candidateMust(subtype.call(p1)));
@@ -80,7 +81,7 @@ public class TypeHierarchyTranslator implements ModelStoreConfiguration {
                                 .may(may)
                                 .must(must)
                                 .candidate(candidate)
-                                .refiner(InferredTypeRefiner.of(typeSymbol, result));
+                                .refiner(InferredTypeRefiner.of(TYPE_SYMBOL, result));
 
                 if (!result.isAbstractType()) {
                         var decision = Rule.of(type.name(), (builder, instance) -> builder