feat: PartialInterpretation representations

25 files changed, 525 insertions, 55 deletions

diff --git a/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/pquery/Dnf2PQuery.java b/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/pquery/Dnf2PQuery.java
index 02e26bde..201e0ed0 100644
--- a/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/pquery/Dnf2PQuery.java
+++ b/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/pquery/Dnf2PQuery.java
@@ -23,17 +23,16 @@ import tools.refinery.store.query.DnfUtils;
 import tools.refinery.store.query.Variable;
 import tools.refinery.store.query.literal.*;
 import tools.refinery.store.query.view.AnyRelationView;
+import tools.refinery.store.util.CycleDetectingMapper;
 
 import java.util.*;
 import java.util.function.Function;
-import java.util.stream.Collectors;
 
 public class Dnf2PQuery {
         private static final Object P_CONSTRAINT_LOCK = new Object();
 
-        private final Set<Dnf> translating = new LinkedHashSet<>();
-
-        private final Map<Dnf, RawPQuery> dnf2PQueryMap = new HashMap<>();
+        private final CycleDetectingMapper<Dnf, RawPQuery> mapper = new CycleDetectingMapper<>(Dnf::name,
+                        this::doTranslate);
 
         private final Map<AnyRelationView, RelationViewWrapper> view2WrapperMap = new LinkedHashMap<>();
 
@@ -47,24 +46,7 @@ public class Dnf2PQuery {
         }
 
         public RawPQuery translate(Dnf dnfQuery) {
-                if (translating.contains(dnfQuery)) {
-                        var path = translating.stream().map(Dnf::name).collect(Collectors.joining(" -> "));
-                        throw new IllegalStateException("Circular reference %s -> %s detected".formatted(path,
-                                        dnfQuery.name()));
-                }
-                // We can't use computeIfAbsent here, because translating referenced queries calls this method in a reentrant
-                // way, which would cause a ConcurrentModificationException with computeIfAbsent.
-                var pQuery = dnf2PQueryMap.get(dnfQuery);
-                if (pQuery == null) {
-                        translating.add(dnfQuery);
-                        try {
-                                pQuery = doTranslate(dnfQuery);
-                                dnf2PQueryMap.put(dnfQuery, pQuery);
-                        } finally {
-                                translating.remove(dnfQuery);
-                        }
-                }
-                return pQuery;
+                return mapper.map(dnfQuery);
         }
 
         public Map<AnyRelationView, IInputKey> getRelationViews() {
@@ -72,7 +54,7 @@ public class Dnf2PQuery {
         }
 
         public RawPQuery getAlreadyTranslated(Dnf dnfQuery) {
-                return dnf2PQueryMap.get(dnfQuery);
+                return mapper.getAlreadyMapped(dnfQuery);
         }
 
         private RawPQuery doTranslate(Dnf dnfQuery) {
@@ -148,7 +130,7 @@ public class Dnf2PQuery {
         }
 
         private void translateRelationViewLiteral(RelationViewLiteral relationViewLiteral, PBody body) {
-                var substitution = translateSubstitution(relationViewLiteral.getSubstitution(), body);
+                var substitution = translateSubstitution(relationViewLiteral.getArguments(), body);
                 var polarity = relationViewLiteral.getPolarity();
                 var relationView = relationViewLiteral.getTarget();
                 if (polarity == CallPolarity.POSITIVE) {
@@ -205,7 +187,7 @@ public class Dnf2PQuery {
         }
 
         private void translateDnfCallLiteral(DnfCallLiteral dnfCallLiteral, PBody body) {
-                var variablesTuple = translateSubstitution(dnfCallLiteral.getSubstitution(), body);
+                var variablesTuple = translateSubstitution(dnfCallLiteral.getArguments(), body);
                 var translatedReferred = translate(dnfCallLiteral.getTarget());
                 var polarity = dnfCallLiteral.getPolarity();
                 switch (polarity) {
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalDnfCallLiteral.java b/subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalDnfCallLiteral.java
new file mode 100644
index 00000000..8070726a
--- /dev/null
+++ b/subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalDnfCallLiteral.java
@@ -0,0 +1,30 @@
+package tools.refinery.store.partial.literal;
+
+import tools.refinery.store.query.Dnf;
+import tools.refinery.store.query.Variable;
+import tools.refinery.store.query.literal.CallPolarity;
+import tools.refinery.store.query.literal.DnfCallLiteral;
+import tools.refinery.store.query.literal.PolarLiteral;
+
+import java.util.List;
+import java.util.Map;
+
+public class ModalDnfCallLiteral extends ModalLiteral<Dnf> implements PolarLiteral<ModalDnfCallLiteral> {
+        public ModalDnfCallLiteral(CallPolarity polarity, Modality modality, Dnf target, List<Variable> arguments) {
+                super(polarity, modality, target, arguments);
+        }
+
+        public ModalDnfCallLiteral(Modality modality, DnfCallLiteral baseLiteral) {
+                super(modality.commute(baseLiteral.getPolarity()), baseLiteral);
+        }
+
+        @Override
+        public ModalDnfCallLiteral substitute(Map<Variable, Variable> substitution) {
+                return new ModalDnfCallLiteral(getPolarity(), getModality(), getTarget(), substituteArguments(substitution));
+        }
+
+        @Override
+        public ModalDnfCallLiteral negate() {
+                return new ModalDnfCallLiteral(getPolarity().negate(), getModality(), getTarget(), getArguments());
+        }
+}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalLiteral.java b/subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalLiteral.java
new file mode 100644
index 00000000..a1b6c83e
--- /dev/null
+++ b/subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalLiteral.java
@@ -0,0 +1,45 @@
+package tools.refinery.store.partial.literal;
+
+import tools.refinery.store.query.RelationLike;
+import tools.refinery.store.query.Variable;
+import tools.refinery.store.query.literal.CallLiteral;
+import tools.refinery.store.query.literal.CallPolarity;
+
+import java.util.List;
+import java.util.Objects;
+
+public abstract class ModalLiteral<T extends RelationLike> extends CallLiteral<T> {
+        private final Modality modality;
+
+        protected ModalLiteral(CallPolarity polarity, Modality modality, T target, List<Variable> arguments) {
+                super(polarity, target, arguments);
+                this.modality = modality;
+        }
+
+        protected ModalLiteral(Modality modality, CallLiteral<? extends T> baseLiteral) {
+                this(baseLiteral.getPolarity(), commute(modality, baseLiteral.getPolarity()), baseLiteral.getTarget(),
+                                baseLiteral.getArguments());
+        }
+
+        public Modality getModality() {
+                return modality;
+        }
+
+        @Override
+        public boolean equals(Object o) {
+                if (this == o) return true;
+                if (o == null || getClass() != o.getClass()) return false;
+                if (!super.equals(o)) return false;
+                ModalLiteral<?> that = (ModalLiteral<?>) o;
+                return modality == that.modality;
+        }
+
+        @Override
+        public int hashCode() {
+                return Objects.hash(super.hashCode(), modality);
+        }
+
+        private static Modality commute(Modality modality, CallPolarity polarity) {
+                return polarity.isPositive() ? modality : modality.negate();
+        }
+}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalRelationLiteral.java b/subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalRelationLiteral.java
new file mode 100644
index 00000000..dbaa524f
--- /dev/null
+++ b/subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalRelationLiteral.java
@@ -0,0 +1,31 @@
+package tools.refinery.store.partial.literal;
+
+import tools.refinery.store.partial.representation.PartialRelation;
+import tools.refinery.store.query.Variable;
+import tools.refinery.store.query.literal.CallPolarity;
+import tools.refinery.store.query.literal.PolarLiteral;
+
+import java.util.List;
+import java.util.Map;
+
+public final class ModalRelationLiteral extends ModalLiteral<PartialRelation>
+                implements PolarLiteral<ModalRelationLiteral> {
+        public ModalRelationLiteral(CallPolarity polarity, Modality modality, PartialRelation target,
+                                                 List<Variable> arguments) {
+                super(polarity, modality, target, arguments);
+        }
+
+        public ModalRelationLiteral(Modality modality, PartialRelationLiteral baseLiteral) {
+                super(modality, baseLiteral);
+        }
+
+        @Override
+        public ModalRelationLiteral substitute(Map<Variable, Variable> substitution) {
+                return new ModalRelationLiteral(getPolarity(), getModality(), getTarget(), substituteArguments(substitution));
+        }
+
+        @Override
+        public ModalRelationLiteral negate() {
+                return new ModalRelationLiteral(getPolarity().negate(), getModality(), getTarget(), getArguments());
+        }
+}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/Modality.java b/subprojects/store/src/main/java/tools/refinery/store/partial/literal/Modality.java
index 93826161..d647ef0a 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/query/literal/Modality.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/partial/literal/Modality.java
@@ -1,4 +1,6 @@
-package tools.refinery.store.query.literal;
+package tools.refinery.store.partial.literal;
+
+import tools.refinery.store.query.literal.CallPolarity;
 
 import java.util.Locale;
 
@@ -15,6 +17,13 @@ public enum Modality {
                 };
         }
 
+        public Modality commute(CallPolarity polarity) {
+                if (polarity.isPositive()) {
+                        return this;
+                }
+                return this.negate();
+        }
+
         @Override
         public String toString() {
                 return name().toLowerCase(Locale.ROOT);
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/literal/PartialLiterals.java b/subprojects/store/src/main/java/tools/refinery/store/partial/literal/PartialLiterals.java
new file mode 100644
index 00000000..51d388d3
--- /dev/null
+++ b/subprojects/store/src/main/java/tools/refinery/store/partial/literal/PartialLiterals.java
@@ -0,0 +1,33 @@
+package tools.refinery.store.partial.literal;
+
+import tools.refinery.store.query.literal.DnfCallLiteral;
+
+public final class PartialLiterals {
+        private PartialLiterals() {
+                throw new IllegalStateException("This is a static utility class and should not be instantiated directly");
+        }
+
+        public ModalRelationLiteral may(PartialRelationLiteral literal) {
+                return new ModalRelationLiteral(Modality.MAY, literal);
+        }
+
+        public ModalRelationLiteral must(PartialRelationLiteral literal) {
+                return new ModalRelationLiteral(Modality.MUST, literal);
+        }
+
+        public ModalRelationLiteral current(PartialRelationLiteral literal) {
+                return new ModalRelationLiteral(Modality.CURRENT, literal);
+        }
+
+        public ModalDnfCallLiteral may(DnfCallLiteral literal) {
+                return new ModalDnfCallLiteral(Modality.MAY, literal);
+        }
+
+        public ModalDnfCallLiteral must(DnfCallLiteral literal) {
+                return new ModalDnfCallLiteral(Modality.MUST, literal);
+        }
+
+        public ModalDnfCallLiteral current(DnfCallLiteral literal) {
+                return new ModalDnfCallLiteral(Modality.CURRENT, literal);
+        }
+}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/literal/PartialRelationLiteral.java b/subprojects/store/src/main/java/tools/refinery/store/partial/literal/PartialRelationLiteral.java
new file mode 100644
index 00000000..dc1a1da3
--- /dev/null
+++ b/subprojects/store/src/main/java/tools/refinery/store/partial/literal/PartialRelationLiteral.java
@@ -0,0 +1,27 @@
+package tools.refinery.store.partial.literal;
+
+import tools.refinery.store.partial.representation.PartialRelation;
+import tools.refinery.store.query.Variable;
+import tools.refinery.store.query.literal.CallLiteral;
+import tools.refinery.store.query.literal.CallPolarity;
+import tools.refinery.store.query.literal.PolarLiteral;
+
+import java.util.List;
+import java.util.Map;
+
+public final class PartialRelationLiteral extends CallLiteral<PartialRelation>
+                implements PolarLiteral<PartialRelationLiteral> {
+        public PartialRelationLiteral(CallPolarity polarity, PartialRelation target, List<Variable> substitution) {
+                super(polarity, target, substitution);
+        }
+
+        @Override
+        public PartialRelationLiteral substitute(Map<Variable, Variable> substitution) {
+                return new PartialRelationLiteral(getPolarity(), getTarget(), substituteArguments(substitution));
+        }
+
+        @Override
+        public PartialRelationLiteral negate() {
+                return new PartialRelationLiteral(getPolarity().negate(), getTarget(), getArguments());
+        }
+}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/representation/AnyPartialFunction.java b/subprojects/store/src/main/java/tools/refinery/store/partial/representation/AnyPartialFunction.java
new file mode 100644
index 00000000..1113245e
--- /dev/null
+++ b/subprojects/store/src/main/java/tools/refinery/store/partial/representation/AnyPartialFunction.java
@@ -0,0 +1,4 @@
+package tools.refinery.store.partial.representation;
+
+public sealed interface AnyPartialFunction extends AnyPartialSymbol permits PartialFunction {
+}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/representation/AnyPartialSymbol.java b/subprojects/store/src/main/java/tools/refinery/store/partial/representation/AnyPartialSymbol.java
new file mode 100644
index 00000000..25096e74
--- /dev/null
+++ b/subprojects/store/src/main/java/tools/refinery/store/partial/representation/AnyPartialSymbol.java
@@ -0,0 +1,11 @@
+package tools.refinery.store.partial.representation;
+
+import tools.refinery.store.representation.AnyAbstractDomain;
+
+public sealed interface AnyPartialSymbol permits AnyPartialFunction, PartialSymbol {
+        String name();
+
+        int arity();
+
+        AnyAbstractDomain abstractDomain();
+}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialFunction.java b/subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialFunction.java
new file mode 100644
index 00000000..3c186f6f
--- /dev/null
+++ b/subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialFunction.java
@@ -0,0 +1,32 @@
+package tools.refinery.store.partial.representation;
+
+import tools.refinery.store.representation.AbstractDomain;
+
+public record PartialFunction<A, C>(String name, int arity, AbstractDomain<A, C> abstractDomain)
+                implements AnyPartialFunction, PartialSymbol<A, C> {
+        @Override
+        public A defaultValue() {
+                return null;
+        }
+
+        @Override
+        public C defaultConcreteValue() {
+                return null;
+        }
+
+        @Override
+        public boolean equals(Object o) {
+                return this == o;
+        }
+
+        @Override
+        public int hashCode() {
+                // Compare by identity to make hash table lookups more efficient.
+                return System.identityHashCode(this);
+        }
+
+        @Override
+        public String toString() {
+                return "%s/%d".formatted(name, arity);
+        }
+}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialRelation.java b/subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialRelation.java
new file mode 100644
index 00000000..127355ca
--- /dev/null
+++ b/subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialRelation.java
@@ -0,0 +1,66 @@
+package tools.refinery.store.partial.representation;
+
+import tools.refinery.store.partial.literal.ModalRelationLiteral;
+import tools.refinery.store.partial.literal.PartialRelationLiteral;
+import tools.refinery.store.query.RelationLike;
+import tools.refinery.store.query.Variable;
+import tools.refinery.store.query.literal.CallPolarity;
+import tools.refinery.store.partial.literal.Modality;
+import tools.refinery.store.representation.AbstractDomain;
+import tools.refinery.store.representation.TruthValue;
+import tools.refinery.store.representation.TruthValueDomain;
+
+import java.util.List;
+
+public record PartialRelation(String name, int arity) implements PartialSymbol<TruthValue, Boolean>, RelationLike {
+        @Override
+        public AbstractDomain<TruthValue, Boolean> abstractDomain() {
+                return TruthValueDomain.INSTANCE;
+        }
+
+        @Override
+        public TruthValue defaultValue() {
+                return TruthValue.FALSE;
+        }
+
+        @Override
+        public Boolean defaultConcreteValue() {
+                return false;
+        }
+
+        public ModalRelationLiteral call(CallPolarity polarity, Modality modality, List<Variable> arguments) {
+                return new ModalRelationLiteral(polarity, modality, this, arguments);
+        }
+
+        public PartialRelationLiteral call(CallPolarity polarity, List<Variable> arguments) {
+                return new PartialRelationLiteral(polarity, this, arguments);
+        }
+
+        public PartialRelationLiteral call(CallPolarity polarity, Variable... arguments) {
+                return call(polarity, List.of(arguments));
+        }
+
+        public PartialRelationLiteral call(Variable... arguments) {
+                return call(CallPolarity.POSITIVE, arguments);
+        }
+
+        public PartialRelationLiteral callTransitive(Variable left, Variable right) {
+                return call(CallPolarity.TRANSITIVE, List.of(left, right));
+        }
+
+        @Override
+        public boolean equals(Object o) {
+                return this == o;
+        }
+
+        @Override
+        public int hashCode() {
+                // Compare by identity to make hash table lookups more efficient.
+                return System.identityHashCode(this);
+        }
+
+        @Override
+        public String toString() {
+                return "%s/%d".formatted(name, arity);
+        }
+}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialSymbol.java b/subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialSymbol.java
new file mode 100644
index 00000000..38533fa9
--- /dev/null
+++ b/subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialSymbol.java
@@ -0,0 +1,12 @@
+package tools.refinery.store.partial.representation;
+
+import tools.refinery.store.representation.AbstractDomain;
+
+public sealed interface PartialSymbol<A, C> extends AnyPartialSymbol permits PartialFunction, PartialRelation {
+        @Override
+        AbstractDomain<A, C> abstractDomain();
+
+        A defaultValue();
+
+        C defaultConcreteValue();
+}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/Dnf.java b/subprojects/store/src/main/java/tools/refinery/store/query/Dnf.java
index 1eb9ac76..b080094f 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/query/Dnf.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/query/Dnf.java
@@ -74,16 +74,16 @@ public final class Dnf implements RelationLike {
                 return clauses;
         }
 
-        public DnfCallLiteral call(CallPolarity polarity, List<Variable> substitution) {
-                return new DnfCallLiteral(polarity, this, substitution);
+        public DnfCallLiteral call(CallPolarity polarity, List<Variable> arguments) {
+                return new DnfCallLiteral(polarity, this, arguments);
         }
 
-        public DnfCallLiteral call(CallPolarity polarity, Variable... substitution) {
-                return call(polarity, List.of(substitution));
+        public DnfCallLiteral call(CallPolarity polarity, Variable... arguments) {
+                return call(polarity, List.of(arguments));
         }
 
-        public DnfCallLiteral call(Variable... substitution) {
-                return call(CallPolarity.POSITIVE, substitution);
+        public DnfCallLiteral call(Variable... arguments) {
+                return call(CallPolarity.POSITIVE, arguments);
         }
 
         public DnfCallLiteral callTransitive(Variable left, Variable right) {
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/DnfUtils.java b/subprojects/store/src/main/java/tools/refinery/store/query/DnfUtils.java
index c7a2849c..17564d43 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/query/DnfUtils.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/query/DnfUtils.java
@@ -1,5 +1,6 @@
 package tools.refinery.store.query;
 
+import java.util.Map;
 import java.util.UUID;
 
 public final class DnfUtils {
@@ -16,4 +17,8 @@ public final class DnfUtils {
                         return originalName + uniqueString;
                 }
         }
+
+        public static Variable maybeSubstitute(Variable variable, Map<Variable, Variable> substitution) {
+                return substitution.getOrDefault(variable, variable);
+        }
 }
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/CallLiteral.java b/subprojects/store/src/main/java/tools/refinery/store/query/literal/CallLiteral.java
index 59120434..5e1ae94d 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/query/literal/CallLiteral.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/query/literal/CallLiteral.java
@@ -1,28 +1,30 @@
 package tools.refinery.store.query.literal;
 
-import tools.refinery.store.query.Variable;
+import tools.refinery.store.query.DnfUtils;
 import tools.refinery.store.query.RelationLike;
+import tools.refinery.store.query.Variable;
 
 import java.util.List;
+import java.util.Map;
 import java.util.Objects;
 import java.util.Set;
 
 public abstract class CallLiteral<T extends RelationLike> implements Literal {
         private final CallPolarity polarity;
         private final T target;
-        private final List<Variable> substitution;
+        private final List<Variable> arguments;
 
-        protected CallLiteral(CallPolarity polarity, T target, List<Variable> substitution) {
-                if (substitution.size() != target.arity()) {
+        protected CallLiteral(CallPolarity polarity, T target, List<Variable> arguments) {
+                if (arguments.size() != target.arity()) {
                         throw new IllegalArgumentException("%s needs %d arguments, but got %s".formatted(target.name(),
-                                        target.arity(), substitution.size()));
+                                        target.arity(), arguments.size()));
                 }
                 if (polarity.isTransitive() && target.arity() != 2) {
                         throw new IllegalArgumentException("Transitive closures can only take binary relations");
                 }
                 this.polarity = polarity;
                 this.target = target;
-                this.substitution = substitution;
+                this.arguments = arguments;
         }
 
         public CallPolarity getPolarity() {
@@ -33,28 +35,32 @@ public abstract class CallLiteral<T extends RelationLike> implements Literal {
                 return target;
         }
 
-        public List<Variable> getSubstitution() {
-                return substitution;
+        public List<Variable> getArguments() {
+                return arguments;
         }
 
         @Override
         public void collectAllVariables(Set<Variable> variables) {
                 if (polarity.isPositive()) {
-                        variables.addAll(substitution);
+                        variables.addAll(arguments);
                 }
         }
 
+        protected List<Variable> substituteArguments(Map<Variable, Variable> substitution) {
+                return arguments.stream().map(variable -> DnfUtils.maybeSubstitute(variable, substitution)).toList();
+        }
+
         @Override
         public boolean equals(Object o) {
                 if (this == o) return true;
                 if (o == null || getClass() != o.getClass()) return false;
                 CallLiteral<?> callAtom = (CallLiteral<?>) o;
                 return polarity == callAtom.polarity && Objects.equals(target, callAtom.target) &&
-                                Objects.equals(substitution, callAtom.substitution);
+                                Objects.equals(arguments, callAtom.arguments);
         }
 
         @Override
         public int hashCode() {
-                return Objects.hash(polarity, target, substitution);
+                return Objects.hash(polarity, target, arguments);
         }
 }
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java b/subprojects/store/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java
index 41426fdd..746d23af 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java
@@ -1,7 +1,9 @@
 package tools.refinery.store.query.literal;
 
+import tools.refinery.store.query.DnfUtils;
 import tools.refinery.store.query.Variable;
 
+import java.util.Map;
 import java.util.Set;
 
 public record ConstantLiteral(Variable variable, int nodeId) implements Literal {
@@ -9,4 +11,9 @@ public record ConstantLiteral(Variable variable, int nodeId) implements Literal
         public void collectAllVariables(Set<Variable> variables) {
                 variables.add(variable);
         }
+
+        @Override
+        public ConstantLiteral substitute(Map<Variable, Variable> substitution) {
+                return new ConstantLiteral(DnfUtils.maybeSubstitute(variable, substitution), nodeId);
+        }
 }
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/DnfCallLiteral.java b/subprojects/store/src/main/java/tools/refinery/store/query/literal/DnfCallLiteral.java
index 86149b33..40499222 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/query/literal/DnfCallLiteral.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/query/literal/DnfCallLiteral.java
@@ -4,14 +4,20 @@ import tools.refinery.store.query.Dnf;
 import tools.refinery.store.query.Variable;
 
 import java.util.List;
+import java.util.Map;
 
 public final class DnfCallLiteral extends CallLiteral<Dnf> implements PolarLiteral<DnfCallLiteral> {
-        public DnfCallLiteral(CallPolarity polarity, Dnf target, List<Variable> substitution) {
-                super(polarity, target, substitution);
+        public DnfCallLiteral(CallPolarity polarity, Dnf target, List<Variable> arguments) {
+                super(polarity, target, arguments);
+        }
+
+        @Override
+        public DnfCallLiteral substitute(Map<Variable, Variable> substitution) {
+                return new DnfCallLiteral(getPolarity(), getTarget(), substituteArguments(substitution));
         }
 
         @Override
         public DnfCallLiteral negate() {
-                return new DnfCallLiteral(getPolarity().negate(), getTarget(), getSubstitution());
+                return new DnfCallLiteral(getPolarity().negate(), getTarget(), getArguments());
         }
 }
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java b/subprojects/store/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java
index 75afd50b..5fee54b1 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java
@@ -1,7 +1,9 @@
 package tools.refinery.store.query.literal;
 
+import tools.refinery.store.query.DnfUtils;
 import tools.refinery.store.query.Variable;
 
+import java.util.Map;
 import java.util.Set;
 
 public record EquivalenceLiteral(boolean positive, Variable left, Variable right)
@@ -16,4 +18,10 @@ public record EquivalenceLiteral(boolean positive, Variable left, Variable right
         public EquivalenceLiteral negate() {
                 return new EquivalenceLiteral(!positive, left, right);
         }
+
+        @Override
+        public EquivalenceLiteral substitute(Map<Variable, Variable> substitution) {
+                return new EquivalenceLiteral(positive, DnfUtils.maybeSubstitute(left, substitution),
+                                DnfUtils.maybeSubstitute(right, substitution));
+        }
 }
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/Literal.java b/subprojects/store/src/main/java/tools/refinery/store/query/literal/Literal.java
index 676ac7fd..e0f5f605 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/query/literal/Literal.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/query/literal/Literal.java
@@ -2,8 +2,11 @@ package tools.refinery.store.query.literal;
 
 import tools.refinery.store.query.Variable;
 
+import java.util.Map;
 import java.util.Set;
 
 public interface Literal {
         void collectAllVariables(Set<Variable> variables);
+
+        Literal substitute(Map<Variable, Variable> substitution);
 }
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/RelationViewLiteral.java b/subprojects/store/src/main/java/tools/refinery/store/query/literal/RelationViewLiteral.java
index 7fa99abb..4718b550 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/query/literal/RelationViewLiteral.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/query/literal/RelationViewLiteral.java
@@ -4,15 +4,21 @@ import tools.refinery.store.query.Variable;
 import tools.refinery.store.query.view.AnyRelationView;
 
 import java.util.List;
+import java.util.Map;
 
 public final class RelationViewLiteral extends CallLiteral<AnyRelationView>
                 implements PolarLiteral<RelationViewLiteral> {
-        public RelationViewLiteral(CallPolarity polarity, AnyRelationView target, List<Variable> substitution) {
-                super(polarity, target, substitution);
+        public RelationViewLiteral(CallPolarity polarity, AnyRelationView target, List<Variable> arguments) {
+                super(polarity, target, arguments);
+        }
+
+        @Override
+        public RelationViewLiteral substitute(Map<Variable, Variable> substitution) {
+                return new RelationViewLiteral(getPolarity(), getTarget(), substituteArguments(substitution));
         }
 
         @Override
         public RelationViewLiteral negate() {
-                return new RelationViewLiteral(getPolarity().negate(), getTarget(), getSubstitution());
+                return new RelationViewLiteral(getPolarity().negate(), getTarget(), getArguments());
         }
 }
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/view/RelationView.java b/subprojects/store/src/main/java/tools/refinery/store/query/view/RelationView.java
index 0bea962d..6accd27a 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/query/view/RelationView.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/query/view/RelationView.java
@@ -51,16 +51,16 @@ public abstract non-sealed class RelationView<T> implements AnyRelationView {
                 return (() -> new CursorAsIterator<>(model.getInterpretation(symbol).getAll(), this::forwardMap, this::filter));
         }
 
-        public RelationViewLiteral call(CallPolarity polarity, List<Variable> substitution) {
-                return new RelationViewLiteral(polarity, this, substitution);
+        public RelationViewLiteral call(CallPolarity polarity, List<Variable> arguments) {
+                return new RelationViewLiteral(polarity, this, arguments);
         }
 
-        public RelationViewLiteral call(CallPolarity polarity, Variable... substitution) {
-                return call(polarity, List.of(substitution));
+        public RelationViewLiteral call(CallPolarity polarity, Variable... arguments) {
+                return call(polarity, List.of(arguments));
         }
 
-        public RelationViewLiteral call(Variable... substitution) {
-                return call(CallPolarity.POSITIVE, substitution);
+        public RelationViewLiteral call(Variable... arguments) {
+                return call(CallPolarity.POSITIVE, arguments);
         }
 
         public RelationViewLiteral callTransitive(Variable left, Variable right) {
diff --git a/subprojects/store/src/main/java/tools/refinery/store/representation/AbstractDomain.java b/subprojects/store/src/main/java/tools/refinery/store/representation/AbstractDomain.java
new file mode 100644
index 00000000..18903ead
--- /dev/null
+++ b/subprojects/store/src/main/java/tools/refinery/store/representation/AbstractDomain.java
@@ -0,0 +1,29 @@
+package tools.refinery.store.representation;
+
+import java.util.Optional;
+
+public non-sealed interface AbstractDomain<A, C> extends AnyAbstractDomain {
+        @Override
+        Class<A> abstractType();
+
+        @Override
+        Class<C> concreteType();
+
+        A toAbstract(C concreteValue);
+
+        Optional<C> toConcrete(A abstractValue);
+
+        default boolean isConcrete(A abstractValue) {
+                return toConcrete(abstractValue).isPresent();
+        }
+
+        boolean isRefinement(A originalValue, A refinedValue);
+
+        A commonRefinement(A leftValue, A rightValue);
+
+        A commonAncestor(A leftValue, A rightValue);
+
+        A unknown();
+
+        boolean isError(A abstractValue);
+}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/representation/AnyAbstractDomain.java b/subprojects/store/src/main/java/tools/refinery/store/representation/AnyAbstractDomain.java
new file mode 100644
index 00000000..4c428a1e
--- /dev/null
+++ b/subprojects/store/src/main/java/tools/refinery/store/representation/AnyAbstractDomain.java
@@ -0,0 +1,7 @@
+package tools.refinery.store.representation;
+
+public sealed interface AnyAbstractDomain permits AbstractDomain {
+        Class<?> abstractType();
+
+        Class<?> concreteType();
+}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/representation/TruthValueDomain.java b/subprojects/store/src/main/java/tools/refinery/store/representation/TruthValueDomain.java
new file mode 100644
index 00000000..29858bce
--- /dev/null
+++ b/subprojects/store/src/main/java/tools/refinery/store/representation/TruthValueDomain.java
@@ -0,0 +1,60 @@
+package tools.refinery.store.representation;
+
+import java.util.Optional;
+
+public final class TruthValueDomain implements AbstractDomain<TruthValue, Boolean> {
+        public static final TruthValueDomain INSTANCE = new TruthValueDomain();
+
+        private TruthValueDomain() {
+        }
+
+        @Override
+        public Class<TruthValue> abstractType() {
+                return null;
+        }
+
+        @Override
+        public Class<Boolean> concreteType() {
+                return null;
+        }
+
+        @Override
+        public TruthValue toAbstract(Boolean concreteValue) {
+                return null;
+        }
+
+        @Override
+        public Optional<Boolean> toConcrete(TruthValue abstractValue) {
+                return Optional.empty();
+        }
+
+        @Override
+        public boolean isConcrete(TruthValue abstractValue) {
+                return AbstractDomain.super.isConcrete(abstractValue);
+        }
+
+        @Override
+        public boolean isRefinement(TruthValue originalValue, TruthValue refinedValue) {
+                return false;
+        }
+
+        @Override
+        public TruthValue commonRefinement(TruthValue leftValue, TruthValue rightValue) {
+                return null;
+        }
+
+        @Override
+        public TruthValue commonAncestor(TruthValue leftValue, TruthValue rightValue) {
+                return null;
+        }
+
+        @Override
+        public TruthValue unknown() {
+                return null;
+        }
+
+        @Override
+        public boolean isError(TruthValue abstractValue) {
+                return false;
+        }
+}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/util/CycleDetectingMapper.java b/subprojects/store/src/main/java/tools/refinery/store/util/CycleDetectingMapper.java
new file mode 100644
index 00000000..e4b462f0
--- /dev/null
+++ b/subprojects/store/src/main/java/tools/refinery/store/util/CycleDetectingMapper.java
@@ -0,0 +1,51 @@
+package tools.refinery.store.util;
+
+import java.util.HashMap;
+import java.util.LinkedHashSet;
+import java.util.Map;
+import java.util.Set;
+import java.util.function.Function;
+import java.util.stream.Collectors;
+
+public class CycleDetectingMapper<T, R> {
+        private static final String SEPARATOR = " -> ";
+
+        private final Function<T, String> getName;
+
+        private final Function<T, R> doMap;
+
+        private final Set<T> inProgress = new LinkedHashSet<>();
+
+        private final Map<T, R> results = new HashMap<>();
+
+        public CycleDetectingMapper(Function<T, String> getName, Function<T, R> doMap) {
+                this.getName = getName;
+                this.doMap = doMap;
+        }
+
+        public R map(T input) {
+                if (inProgress.contains(input)) {
+                        var path = inProgress.stream().map(getName).collect(Collectors.joining(SEPARATOR));
+                        throw new IllegalArgumentException("Circular reference %s%s%s detected".formatted(path, SEPARATOR,
+                                        getName.apply(input)));
+                }
+                // We can't use computeIfAbsent here, because translating referenced queries calls this method in a reentrant
+                // way, which would cause a ConcurrentModificationException with computeIfAbsent.
+                @SuppressWarnings("squid:S3824")
+                var result = results.get(input);
+                if (result == null) {
+                        inProgress.add(input);
+                        try {
+                                result = doMap.apply(input);
+                                results.put(input, result);
+                        } finally {
+                                inProgress.remove(input);
+                        }
+                }
+                return result;
+        }
+
+        public R getAlreadyMapped(T input) {
+                return results.get(input);
+        }
+}