feat: count and aggregation literal reduction

18 files changed, 281 insertions, 233 deletions

diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/Constraint.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/Constraint.java
index 207c627c..e841da9e 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/Constraint.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/Constraint.java
@@ -24,8 +24,8 @@ public interface Constraint {
                 return i < 0 || i >= arity();
         }
 
-        default LiteralReduction getReduction() {
-                return LiteralReduction.NOT_REDUCIBLE;
+        default Reduction getReduction() {
+                return Reduction.NOT_REDUCIBLE;
         }
 
         default boolean equals(LiteralEqualityHelper helper, Constraint other) {
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/LiteralReduction.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/Reduction.java
index 9d8352ea..82c52b04 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/LiteralReduction.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/Reduction.java
@@ -3,9 +3,9 @@
  *
  * SPDX-License-Identifier: EPL-2.0
  */
-package tools.refinery.store.query.literal;
+package tools.refinery.store.query;
 
-public enum LiteralReduction {
+public enum Reduction {
         /**
          * Signifies that a literal should be preserved in the clause.
          */
@@ -21,7 +21,7 @@ public enum LiteralReduction {
          */
         ALWAYS_FALSE;
 
-        public LiteralReduction negate() {
+        public Reduction negate() {
                 return switch (this) {
                         case NOT_REDUCIBLE -> NOT_REDUCIBLE;
                         case ALWAYS_TRUE -> ALWAYS_FALSE;
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/ClausePostProcessor.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/ClausePostProcessor.java
index 72bc06a1..467b8d52 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/ClausePostProcessor.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/ClausePostProcessor.java
@@ -6,6 +6,7 @@
 package tools.refinery.store.query.dnf;
 
 import org.jetbrains.annotations.NotNull;
+import tools.refinery.store.query.literal.BooleanLiteral;
 import tools.refinery.store.query.literal.EquivalenceLiteral;
 import tools.refinery.store.query.literal.Literal;
 import tools.refinery.store.query.literal.VariableDirection;
@@ -51,18 +52,11 @@ class ClausePostProcessor {
                 topologicallySortLiterals();
                 var filteredLiterals = new ArrayList<Literal>(topologicallySortedLiterals.size());
                 for (var literal : topologicallySortedLiterals) {
-                        var reduction = literal.getReduction();
-                        switch (reduction) {
-                        case NOT_REDUCIBLE -> filteredLiterals.add(literal);
-                        case ALWAYS_TRUE -> {
-                                // Literals reducible to {@code true} can be omitted, because the model is always assumed to have at
-                                // least on object.
-                        }
-                        case ALWAYS_FALSE -> {
-                                // Clauses with {@code false} literals can be omitted entirely.
+                        var reducedLiteral = literal.reduce();
+                        if (BooleanLiteral.FALSE.equals(reducedLiteral)) {
                                 return ConstantResult.ALWAYS_FALSE;
-                        }
-                        default -> throw new IllegalArgumentException("Invalid reduction: " + reduction);
+                        } else if (!BooleanLiteral.TRUE.equals(reducedLiteral)) {
+                                filteredLiterals.add(reducedLiteral);
                         }
                 }
                 if (filteredLiterals.isEmpty()) {
@@ -156,7 +150,7 @@ class ClausePostProcessor {
 
         private void computePositiveVariables() {
                 for (var literal : substitutedLiterals) {
-                        var variableBinder = literal.getVariableBinder();
+                        var variableBinder = literal.getVariableBindingSite();
                         variableBinder.getVariablesWithDirection(VariableDirection.IN_OUT)
                                         .forEach(existentiallyQuantifiedVariables::add);
                         variableBinder.getVariablesWithDirection(VariableDirection.OUT).forEach(variable -> {
@@ -192,7 +186,7 @@ class ClausePostProcessor {
         private void validateClosureVariables() {
                 var negativeVariablesMap = new HashMap<Variable, Literal>();
                 for (var literal : substitutedLiterals) {
-                        var variableBinder = literal.getVariableBinder();
+                        var variableBinder = literal.getVariableBindingSite();
                         variableBinder.getVariablesWithDirection(VariableDirection.CLOSURE, positiveVariables)
                                         .forEach(variable -> {
                                                 var oldLiteral = negativeVariablesMap.put(variable, literal);
@@ -243,7 +237,7 @@ class ClausePostProcessor {
                 private SortableLiteral(int index, Literal literal) {
                         this.index = index;
                         this.literal = literal;
-                        remainingInputs = literal.getVariableBinder()
+                        remainingInputs = literal.getVariableBindingSite()
                                         .getVariablesWithDirection(VariableDirection.IN, positiveVariables)
                                         .collect(Collectors.toCollection(HashSet::new));
                         remainingInputs.removeAll(inputParameters);
@@ -288,7 +282,7 @@ class ClausePostProcessor {
                         }
                         // Add literal if we haven't yet added a duplicate of this literal.
                         topologicallySortedLiterals.add(literal);
-                        var variableBinder = literal.getVariableBinder();
+                        var variableBinder = literal.getVariableBindingSite();
                         variableBinder.getVariablesWithDirection(VariableDirection.IN_OUT)
                                         .forEach(ClausePostProcessor.this::topologicallySortVariable);
                         variableBinder.getVariablesWithDirection(VariableDirection.OUT)
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/Dnf.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/Dnf.java
index 7e68d4a0..64790f42 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/Dnf.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/Dnf.java
@@ -6,9 +6,9 @@
 package tools.refinery.store.query.dnf;
 
 import tools.refinery.store.query.Constraint;
+import tools.refinery.store.query.Reduction;
 import tools.refinery.store.query.equality.DnfEqualityChecker;
 import tools.refinery.store.query.equality.LiteralEqualityHelper;
-import tools.refinery.store.query.literal.LiteralReduction;
 import tools.refinery.store.query.term.Parameter;
 import tools.refinery.store.query.term.Variable;
 
@@ -103,16 +103,16 @@ public final class Dnf implements Constraint {
         }
 
         @Override
-        public LiteralReduction getReduction() {
+        public Reduction getReduction() {
                 if (clauses.isEmpty()) {
-                        return LiteralReduction.ALWAYS_FALSE;
+                        return Reduction.ALWAYS_FALSE;
                 }
                 for (var clause : clauses) {
                         if (clause.literals().isEmpty()) {
-                                return LiteralReduction.ALWAYS_TRUE;
+                                return Reduction.ALWAYS_TRUE;
                         }
                 }
-                return LiteralReduction.NOT_REDUCIBLE;
+                return Reduction.NOT_REDUCIBLE;
         }
 
         public boolean equalsWithSubstitution(DnfEqualityChecker callEqualityChecker, Dnf other) {
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AggregationLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AggregationLiteral.java
index 2aa0a0d5..51a33c1f 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AggregationLiteral.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AggregationLiteral.java
@@ -9,6 +9,7 @@ import tools.refinery.store.query.Constraint;
 import tools.refinery.store.query.equality.LiteralEqualityHelper;
 import tools.refinery.store.query.substitution.Substitution;
 import tools.refinery.store.query.term.Aggregator;
+import tools.refinery.store.query.term.ConstantTerm;
 import tools.refinery.store.query.term.DataVariable;
 import tools.refinery.store.query.term.Variable;
 
@@ -19,7 +20,7 @@ public class AggregationLiteral<R, T> extends AbstractCallLiteral {
         private final DataVariable<R> resultVariable;
         private final DataVariable<T> inputVariable;
         private final Aggregator<R, T> aggregator;
-        private final VariableBinder variableBinder;
+        private final VariableBindingSite variableBindingSite;
 
         public AggregationLiteral(DataVariable<R> resultVariable, Aggregator<R, T> aggregator,
                                                           DataVariable<T> inputVariable, Constraint target, List<Variable> arguments) {
@@ -39,13 +40,13 @@ public class AggregationLiteral<R, T> extends AbstractCallLiteral {
                 this.resultVariable = resultVariable;
                 this.inputVariable = inputVariable;
                 this.aggregator = aggregator;
-                variableBinder = VariableBinder.builder()
+                variableBindingSite = VariableBindingSite.builder()
                                 .variable(resultVariable, VariableDirection.OUT)
                                 .parameterList(false, target.getParameters(), arguments)
                                 .build();
-                if (variableBinder.getDirection(inputVariable) != VariableDirection.CLOSURE) {
-                        throw new IllegalArgumentException("Input variable %s must appear in the argument list".formatted(
-                                        inputVariable));
+                if (variableBindingSite.getDirection(inputVariable) != VariableDirection.CLOSURE) {
+                        throw new IllegalArgumentException(("Input variable %s must appear in the argument list as an output " +
+                                        "variable and should not be bound anywhere else").formatted(inputVariable));
                 }
         }
 
@@ -62,8 +63,22 @@ public class AggregationLiteral<R, T> extends AbstractCallLiteral {
         }
 
         @Override
-        public VariableBinder getVariableBinder() {
-                return variableBinder;
+        public VariableBindingSite getVariableBindingSite() {
+                return variableBindingSite;
+        }
+
+        @Override
+        public Literal reduce() {
+                var reduction = getTarget().getReduction();
+                return switch (reduction) {
+                        case ALWAYS_FALSE -> {
+                                var emptyValue = aggregator.getEmptyResult();
+                                yield emptyValue == null ? BooleanLiteral.FALSE :
+                                                resultVariable.assign(new ConstantTerm<>(resultVariable.getType(), emptyValue));
+                        }
+                        case ALWAYS_TRUE -> throw new IllegalArgumentException("Trying to aggregate over an infinite set");
+                        case NOT_REDUCIBLE -> this;
+                };
         }
 
         @Override
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AssignLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AssignLiteral.java
index 4da92b90..079ba6bb 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AssignLiteral.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AssignLiteral.java
@@ -15,7 +15,7 @@ import java.util.Objects;
 public final class AssignLiteral<T> implements Literal {
         private final DataVariable<T> variable;
         private final Term<T> term;
-        private final VariableBinder variableBinder;
+        private final VariableBindingSite variableBindingSite;
 
         public AssignLiteral(DataVariable<T> variable, Term<T> term) {
                 if (!term.getType().equals(variable.getType())) {
@@ -29,7 +29,7 @@ public final class AssignLiteral<T> implements Literal {
                         throw new IllegalArgumentException("Result variable %s must not appear in the term %s".formatted(
                                         variable, term));
                 }
-                variableBinder = VariableBinder.builder()
+                variableBindingSite = VariableBindingSite.builder()
                                 .variable(variable, VariableDirection.OUT)
                                 .variables(inputVariables, VariableDirection.IN)
                                 .build();
@@ -44,8 +44,8 @@ public final class AssignLiteral<T> implements Literal {
         }
 
         @Override
-        public VariableBinder getVariableBinder() {
-                return variableBinder;
+        public VariableBindingSite getVariableBindingSite() {
+                return variableBindingSite;
         }
 
         @Override
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AssumeLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AssumeLiteral.java
index 61486e4c..3dfb8902 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AssumeLiteral.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AssumeLiteral.java
@@ -14,7 +14,7 @@ import java.util.Objects;
 
 public final class AssumeLiteral implements Literal {
         private final Term<Boolean> term;
-        private final VariableBinder variableBinder;
+        private final VariableBindingSite variableBindingSite;
 
         public AssumeLiteral(Term<Boolean> term) {
                 if (!term.getType().equals(Boolean.class)) {
@@ -22,7 +22,7 @@ public final class AssumeLiteral implements Literal {
                                         term, Boolean.class.getName(), term.getType().getName()));
                 }
                 this.term = term;
-                variableBinder = VariableBinder.builder()
+                variableBindingSite = VariableBindingSite.builder()
                                 .variables(term.getInputVariables(), VariableDirection.IN)
                                 .build();
         }
@@ -32,8 +32,8 @@ public final class AssumeLiteral implements Literal {
         }
 
         @Override
-        public VariableBinder getVariableBinder() {
-                return variableBinder;
+        public VariableBindingSite getVariableBindingSite() {
+                return variableBindingSite;
         }
 
         @Override
@@ -51,13 +51,13 @@ public final class AssumeLiteral implements Literal {
         }
 
         @Override
-        public LiteralReduction getReduction() {
+        public Literal reduce() {
                 if (term instanceof ConstantTerm<Boolean> constantTerm) {
-                        // Return {@code ALWAYS_FALSE} for {@code false} or {@code null} literals.
-                        return Boolean.TRUE.equals(constantTerm.getValue()) ? LiteralReduction.ALWAYS_TRUE :
-                                        LiteralReduction.ALWAYS_FALSE;
+                        // Return {@link BooleanLiteral#FALSE} for {@code false} or {@code null} literals.
+                        return Boolean.TRUE.equals(constantTerm.getValue()) ? BooleanLiteral.TRUE :
+                                        BooleanLiteral.FALSE;
                 }
-                return LiteralReduction.NOT_REDUCIBLE;
+                return this;
         }
 
         @Override
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/BooleanLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/BooleanLiteral.java
index e61f0535..736b3537 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/BooleanLiteral.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/BooleanLiteral.java
@@ -19,8 +19,8 @@ public enum BooleanLiteral implements CanNegate<BooleanLiteral> {
         }
 
         @Override
-        public VariableBinder getVariableBinder() {
-                return VariableBinder.EMPTY;
+        public VariableBindingSite getVariableBindingSite() {
+                return VariableBindingSite.EMPTY;
         }
 
         @Override
@@ -30,11 +30,6 @@ public enum BooleanLiteral implements CanNegate<BooleanLiteral> {
         }
 
         @Override
-        public LiteralReduction getReduction() {
-                return value ? LiteralReduction.ALWAYS_TRUE : LiteralReduction.ALWAYS_FALSE;
-        }
-
-        @Override
         public BooleanLiteral negate() {
                 return fromBoolean(!value);
         }
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CallLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CallLiteral.java
index dc6098a8..4f755e95 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CallLiteral.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CallLiteral.java
@@ -15,7 +15,7 @@ import java.util.Objects;
 
 public final class CallLiteral extends AbstractCallLiteral implements CanNegate<CallLiteral> {
         private final CallPolarity polarity;
-        private final VariableBinder variableBinder;
+        private final VariableBindingSite variableBindingSite;
 
         public CallLiteral(CallPolarity polarity, Constraint target, List<Variable> arguments) {
                 super(target, arguments);
@@ -30,7 +30,7 @@ public final class CallLiteral extends AbstractCallLiteral implements CanNegate<
                         }
                 }
                 this.polarity = polarity;
-                variableBinder = VariableBinder.builder()
+                variableBindingSite = VariableBindingSite.builder()
                                 .parameterList(polarity.isPositive(), parameters, arguments)
                                 .build();
         }
@@ -40,8 +40,8 @@ public final class CallLiteral extends AbstractCallLiteral implements CanNegate<
         }
 
         @Override
-        public VariableBinder getVariableBinder() {
-                return variableBinder;
+        public VariableBindingSite getVariableBindingSite() {
+                return variableBindingSite;
         }
 
         @Override
@@ -50,9 +50,14 @@ public final class CallLiteral extends AbstractCallLiteral implements CanNegate<
         }
 
         @Override
-        public LiteralReduction getReduction() {
+        public Literal reduce() {
                 var reduction = getTarget().getReduction();
-                return polarity.isPositive() ? reduction : reduction.negate();
+                var negatedReduction = polarity.isPositive() ? reduction : reduction.negate();
+                return switch (negatedReduction) {
+                        case ALWAYS_TRUE -> BooleanLiteral.TRUE;
+                        case ALWAYS_FALSE -> BooleanLiteral.FALSE;
+                        default -> this;
+                };
         }
 
         @Override
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java
index 7466cb1d..1bc14bab 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java
@@ -14,12 +14,12 @@ import java.util.Objects;
 public final class ConstantLiteral implements Literal {
         private final NodeVariable variable;
         private final int nodeId;
-        private final VariableBinder variableBinder;
+        private final VariableBindingSite variableBindingSite;
 
         public ConstantLiteral(NodeVariable variable, int nodeId) {
                 this.variable = variable;
                 this.nodeId = nodeId;
-                variableBinder = VariableBinder.builder().variable(variable, VariableDirection.IN_OUT).build();
+                variableBindingSite = VariableBindingSite.builder().variable(variable, VariableDirection.IN_OUT).build();
         }
 
         public NodeVariable getVariable() {
@@ -31,8 +31,8 @@ public final class ConstantLiteral implements Literal {
         }
 
         @Override
-        public VariableBinder getVariableBinder() {
-                return variableBinder;
+        public VariableBindingSite getVariableBindingSite() {
+                return variableBindingSite;
         }
 
         @Override
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CountLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CountLiteral.java
index a602d982..0a47aa66 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CountLiteral.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CountLiteral.java
@@ -10,13 +10,14 @@ import tools.refinery.store.query.equality.LiteralEqualityHelper;
 import tools.refinery.store.query.substitution.Substitution;
 import tools.refinery.store.query.term.DataVariable;
 import tools.refinery.store.query.term.Variable;
+import tools.refinery.store.query.term.int_.IntTerms;
 
 import java.util.List;
 import java.util.Objects;
 
 public class CountLiteral extends AbstractCallLiteral {
         private final DataVariable<Integer> resultVariable;
-        private final VariableBinder variableBinder;
+        private final VariableBindingSite variableBindingSite;
 
         public CountLiteral(DataVariable<Integer> resultVariable, Constraint target, List<Variable> arguments) {
                 super(target, arguments);
@@ -29,7 +30,7 @@ public class CountLiteral extends AbstractCallLiteral {
                                         .formatted(resultVariable));
                 }
                 this.resultVariable = resultVariable;
-                variableBinder = VariableBinder.builder()
+                variableBindingSite = VariableBindingSite.builder()
                                 .variable(resultVariable, VariableDirection.OUT)
                                 .parameterList(false, target.getParameters(), arguments)
                                 .build();
@@ -40,8 +41,20 @@ public class CountLiteral extends AbstractCallLiteral {
         }
 
         @Override
-        public VariableBinder getVariableBinder() {
-                return variableBinder;
+        public VariableBindingSite getVariableBindingSite() {
+                return variableBindingSite;
+        }
+
+        @Override
+        public Literal reduce() {
+                var reduction = getTarget().getReduction();
+                return switch (reduction) {
+                        case ALWAYS_FALSE -> getResultVariable().assign(IntTerms.constant(0));
+                        // The only way a constant {@code true} predicate can be called in a negative position is to have all of
+                        // its arguments bound as input variables. Thus, there will only be a single match.
+                        case ALWAYS_TRUE -> getResultVariable().assign(IntTerms.constant(1));
+                        case NOT_REDUCIBLE -> this;
+                };
         }
 
         @Override
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java
index 794cee0d..b36c0e40 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java
@@ -16,13 +16,13 @@ public final class EquivalenceLiteral
         private final boolean positive;
         private final NodeVariable left;
         private final NodeVariable right;
-        private final VariableBinder variableBinder;
+        private final VariableBindingSite variableBindingSite;
 
         public EquivalenceLiteral(boolean positive, NodeVariable left, NodeVariable right) {
                 this.positive = positive;
                 this.left = left;
                 this.right = right;
-                variableBinder = VariableBinder.builder()
+                variableBindingSite = VariableBindingSite.builder()
                                 .variable(left, positive ? VariableDirection.IN_OUT : VariableDirection.IN)
                                 .variable(right, VariableDirection.IN)
                                 .build();
@@ -41,8 +41,8 @@ public final class EquivalenceLiteral
         }
 
         @Override
-        public VariableBinder getVariableBinder() {
-                return variableBinder;
+        public VariableBindingSite getVariableBindingSite() {
+                return variableBindingSite;
         }
 
         @Override
@@ -57,11 +57,11 @@ public final class EquivalenceLiteral
         }
 
         @Override
-        public LiteralReduction getReduction() {
+        public Literal reduce() {
                 if (left.equals(right)) {
-                        return positive ? LiteralReduction.ALWAYS_TRUE : LiteralReduction.ALWAYS_FALSE;
+                        return positive ? BooleanLiteral.TRUE : BooleanLiteral.FALSE;
                 }
-                return LiteralReduction.NOT_REDUCIBLE;
+                return this;
         }
 
         @Override
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/Literal.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/Literal.java
index c3c111a4..10e4cffd 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/Literal.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/Literal.java
@@ -9,12 +9,12 @@ import tools.refinery.store.query.equality.LiteralEqualityHelper;
 import tools.refinery.store.query.substitution.Substitution;
 
 public interface Literal {
-        VariableBinder getVariableBinder();
+        VariableBindingSite getVariableBindingSite();
 
         Literal substitute(Substitution substitution);
 
-        default LiteralReduction getReduction() {
-                return LiteralReduction.NOT_REDUCIBLE;
+        default Literal reduce() {
+                return this;
         }
 
         @SuppressWarnings("BooleanMethodIsAlwaysInverted")
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableBinderBuilder.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableBinderBuilder.java
deleted file mode 100644
index b0d47240..00000000
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableBinderBuilder.java
+++ /dev/null
@@ -1,96 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-package tools.refinery.store.query.literal;
-
-import tools.refinery.store.query.exceptions.IncompatibleParameterDirectionException;
-import tools.refinery.store.query.term.*;
-
-import java.util.*;
-
-public final class VariableBinderBuilder {
-        private final Map<Variable, VariableDirection> directionMap = new LinkedHashMap<>();
-        private final Set<Variable> uniqueVariables = new HashSet<>();
-
-        VariableBinderBuilder() {
-        }
-
-        public VariableBinderBuilder variable(Variable variable, VariableDirection direction) {
-                return variable(variable, direction, direction == VariableDirection.OUT);
-        }
-
-        private VariableBinderBuilder variable(Variable variable, VariableDirection direction, boolean markAsUnique) {
-                validateDirection(variable, direction);
-                boolean unique = shouldBeUnique(variable, markAsUnique);
-                directionMap.compute(variable, (ignored, oldValue) -> {
-                        if (oldValue == null) {
-                                return direction;
-                        }
-                        if (unique) {
-                                throw new IllegalArgumentException("Duplicate binding for variable " + variable);
-                        }
-                        try {
-                                return oldValue.merge(direction);
-                        } catch (IncompatibleParameterDirectionException e) {
-                                var message = "%s for variable %s".formatted(e.getMessage(), variable);
-                                throw new IncompatibleParameterDirectionException(message, e);
-                        }
-                });
-                return this;
-        }
-
-        private static void validateDirection(Variable variable, VariableDirection direction) {
-                if (variable instanceof AnyDataVariable) {
-                        if (direction == VariableDirection.IN_OUT) {
-                                throw new IllegalArgumentException("%s direction is not supported for data variable %s"
-                                                .formatted(direction, variable));
-                        }
-                } else if (variable instanceof NodeVariable) {
-                        if (direction == VariableDirection.OUT) {
-                                throw new IllegalArgumentException("%s direction is not supported for node variable %s"
-                                                .formatted(direction, variable));
-                        }
-                } else {
-                        throw new IllegalArgumentException("Unknown variable " + variable);
-                }
-        }
-
-        private boolean shouldBeUnique(Variable variable, boolean markAsUnique) {
-                if (markAsUnique) {
-                        uniqueVariables.add(variable);
-                        return true;
-                } else {
-                        return uniqueVariables.contains(variable);
-                }
-        }
-
-        public VariableBinderBuilder variables(Collection<? extends Variable> variables, VariableDirection direction) {
-                for (var variable : variables) {
-                        variable(variable, direction);
-                }
-                return this;
-        }
-
-        public VariableBinderBuilder parameterList(boolean positive, List<Parameter> parameters,
-                                                                                           List<Variable> arguments) {
-                int arity = parameters.size();
-                if (arity != arguments.size()) {
-                        throw new IllegalArgumentException("Got %d arguments for %d parameters"
-                                        .formatted(arguments.size(), arity));
-                }
-                for (int i = 0; i < arity; i++) {
-                        var argument = arguments.get(i);
-                        var parameter = parameters.get(i);
-                        var parameterDirection = parameter.getDirection();
-                        var direction = VariableDirection.from(positive, parameterDirection);
-                        variable(argument, direction, parameterDirection == ParameterDirection.OUT);
-                }
-                return this;
-        }
-
-        public VariableBinder build() {
-                return new VariableBinder(directionMap);
-        }
-}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableBinder.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableBindingSite.java
index 5f43d07d..624af045 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableBinder.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableBindingSite.java
@@ -11,12 +11,12 @@ import java.util.Map;
 import java.util.Set;
 import java.util.stream.Stream;
 
-public final class VariableBinder {
-        public static final VariableBinder EMPTY = new VariableBinder(Map.of());
+public final class VariableBindingSite {
+        public static final VariableBindingSite EMPTY = new VariableBindingSite(Map.of());
 
         private final Map<Variable, VariableDirection> directionMap;
 
-        VariableBinder(Map<Variable, VariableDirection> directionMap) {
+        VariableBindingSite(Map<Variable, VariableDirection> directionMap) {
                 this.directionMap = directionMap;
         }
 
@@ -41,9 +41,9 @@ public final class VariableBinder {
 
         public Stream<Variable> getVariablesWithDirection(VariableDirection direction,
                                                                                                           Set<? extends Variable> positiveVariables) {
-                if (direction == VariableDirection.NEGATIVE) {
+                if (direction == VariableDirection.NEUTRAL) {
                         throw new IllegalArgumentException("Use #getVariablesWithDirection(VariableDirection) if disambiguation " +
-                                        "of VariableDirection#NEGATIVE variables according to the containing DnfClose is not desired");
+                                        "of VariableDirection#NEUTRAL variables according to the containing DnfClose is not desired");
                 }
                 return directionMap.entrySet().stream()
                                 .filter(pair -> disambiguateDirection(pair.getValue(), pair.getKey(), positiveVariables) == direction)
@@ -52,13 +52,13 @@ public final class VariableBinder {
 
         private VariableDirection disambiguateDirection(VariableDirection direction, Variable variable,
                                                                                                         Set<? extends Variable> positiveVariables) {
-                if (direction != VariableDirection.NEGATIVE) {
+                if (direction != VariableDirection.NEUTRAL) {
                         return direction;
                 }
                 return positiveVariables.contains(variable) ? VariableDirection.IN : VariableDirection.CLOSURE;
         }
 
-        public static VariableBinderBuilder builder() {
-                return new VariableBinderBuilder();
+        public static VariableBindingSiteBuilder builder() {
+                return new VariableBindingSiteBuilder();
         }
 }
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableBindingSiteBuilder.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableBindingSiteBuilder.java
new file mode 100644
index 00000000..873db1ec
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableBindingSiteBuilder.java
@@ -0,0 +1,137 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.literal;
+
+import tools.refinery.store.query.exceptions.IncompatibleParameterDirectionException;
+import tools.refinery.store.query.term.*;
+
+import java.util.*;
+
+public final class VariableBindingSiteBuilder {
+        private final Map<Variable, VariableDirection> directionMap = new LinkedHashMap<>();
+        private final Set<Variable> nonUnifiableVariables = new HashSet<>();
+
+        VariableBindingSiteBuilder() {
+        }
+
+        public VariableBindingSiteBuilder variable(Variable variable, VariableDirection direction) {
+                return variable(variable, direction, direction == VariableDirection.OUT);
+        }
+
+        public VariableBindingSiteBuilder variable(Variable variable, VariableDirection direction, boolean markAsUnique) {
+                validateUnique(direction, markAsUnique);
+                validateDirection(variable, direction);
+                boolean unique;
+                if (markAsUnique) {
+                        nonUnifiableVariables.add(variable);
+                        unique = true;
+                } else {
+                        unique = nonUnifiableVariables.contains(variable);
+                }
+                directionMap.compute(variable, (ignored, oldValue) -> {
+                        if (oldValue == null) {
+                                return direction;
+                        }
+                        if (unique) {
+                                throw new IllegalArgumentException("Duplicate binding for variable " + variable);
+                        }
+                        try {
+                                return merge(oldValue, direction);
+                        } catch (IncompatibleParameterDirectionException e) {
+                                var message = "%s for variable %s".formatted(e.getMessage(), variable);
+                                throw new IncompatibleParameterDirectionException(message, e);
+                        }
+                });
+                return this;
+        }
+
+        private static void validateUnique(VariableDirection direction, boolean markAsUnique) {
+                if (direction == VariableDirection.OUT && !markAsUnique) {
+                        throw new IllegalArgumentException("OUT binding must be marked as non-unifiable");
+                }
+                if (markAsUnique && (direction != VariableDirection.OUT && direction != VariableDirection.CLOSURE)) {
+                        throw new IllegalArgumentException("Only OUT or CLOSURE binding may be marked as non-unifiable");
+                }
+        }
+
+        private static void validateDirection(Variable variable, VariableDirection direction) {
+                if (variable instanceof AnyDataVariable) {
+                        if (direction == VariableDirection.IN_OUT) {
+                                throw new IllegalArgumentException("%s direction is not supported for data variable %s"
+                                                .formatted(direction, variable));
+                        }
+                } else if (variable instanceof NodeVariable) {
+                        if (direction == VariableDirection.OUT) {
+                                throw new IllegalArgumentException("%s direction is not supported for node variable %s"
+                                                .formatted(direction, variable));
+                        }
+                } else {
+                        throw new IllegalArgumentException("Unknown variable " + variable);
+                }
+        }
+
+        private static VariableDirection merge(VariableDirection left, VariableDirection right) {
+                return switch (left) {
+                        case IN_OUT -> switch (right) {
+                                case IN_OUT -> VariableDirection.IN_OUT;
+                                case OUT -> VariableDirection.OUT;
+                                case IN, NEUTRAL -> VariableDirection.IN;
+                                case CLOSURE -> throw incompatibleDirections(left, right);
+                        };
+                        case OUT -> switch (right) {
+                                case IN_OUT, OUT -> VariableDirection.OUT;
+                                case IN, NEUTRAL, CLOSURE -> throw incompatibleDirections(left, right);
+                        };
+                        case IN -> switch (right) {
+                                case IN_OUT, NEUTRAL, IN -> VariableDirection.IN;
+                                case OUT, CLOSURE -> throw incompatibleDirections(left, right);
+                        };
+                        case NEUTRAL -> switch (right) {
+                                case IN_OUT, IN -> VariableDirection.IN;
+                                case NEUTRAL -> VariableDirection.NEUTRAL;
+                                case CLOSURE -> VariableDirection.CLOSURE;
+                                case OUT -> throw incompatibleDirections(left, right);
+                        };
+                        case CLOSURE -> switch (right) {
+                                case NEUTRAL, CLOSURE -> VariableDirection.CLOSURE;
+                                case IN_OUT, IN, OUT -> throw incompatibleDirections(left, right);
+                        };
+                };
+        }
+
+        private static RuntimeException incompatibleDirections(VariableDirection left, VariableDirection right) {
+                return new IncompatibleParameterDirectionException("Incompatible variable directions %s and %s"
+                                .formatted(left, right));
+        }
+
+        public VariableBindingSiteBuilder variables(Collection<? extends Variable> variables, VariableDirection direction) {
+                for (var variable : variables) {
+                        variable(variable, direction);
+                }
+                return this;
+        }
+
+        public VariableBindingSiteBuilder parameterList(boolean positive, List<Parameter> parameters,
+                                                                                                        List<Variable> arguments) {
+                int arity = parameters.size();
+                if (arity != arguments.size()) {
+                        throw new IllegalArgumentException("Got %d arguments for %d parameters"
+                                        .formatted(arguments.size(), arity));
+                }
+                for (int i = 0; i < arity; i++) {
+                        var argument = arguments.get(i);
+                        var parameter = parameters.get(i);
+                        var parameterDirection = parameter.getDirection();
+                        var direction = VariableDirection.from(positive, parameterDirection);
+                        variable(argument, direction, parameterDirection == ParameterDirection.OUT);
+                }
+                return this;
+        }
+
+        public VariableBindingSite build() {
+                return new VariableBindingSite(directionMap);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableDirection.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableDirection.java
index 444dcbbf..0b7a2960 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableDirection.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableDirection.java
@@ -5,44 +5,63 @@
  */
 package tools.refinery.store.query.literal;
 
-import tools.refinery.store.query.exceptions.IncompatibleParameterDirectionException;
 import tools.refinery.store.query.term.ParameterDirection;
 
+/**
+ * Directions of the flow of a variable to ro from a clause.
+ * <p>
+ * During the evaluation of a clause
+ * <ol>
+ *     <li>reads already bound {@code IN} variables,</li>
+ *     <li>enumerates over all possible bindings of {@code CLOSURE} variables, and</li>
+ *     <li>
+ *         produces bindings for
+ *         <ul>
+ *             <li>{@code IN_OUT} variables that may already be bound in clause (if they already have a binding,
+ *             the existing values are compared to the new binding by {@link Object#equals(Object)}), and</li>
+ *             <li>{@code OUT} variables that must not be already bound in the clause (because comparison by
+ *             equality wouldn't produce an appropriate join).</li>
+ *         </ul>
+ *     </li>
+ * </ol>
+ * Variables marked as {@code NEUTRAL} may act as {@code IN} or {@code CLOSURE} depending on whether they have an
+ * existing binding that can be read.
+ */
 public enum VariableDirection {
         /**
          * Binds a node variable or check equality with a node variable.
          * <p>
-         * This is the usual direction for positive constraints on nodes. A data variable may have multiple {@code InOut}
+         * This is the usual direction for positive constraints on nodes. A data variable may have multiple {@code IN_OUT}
          * bindings, even on the same parameter list.
          * <p>
          * Cannot be used for data variables.
          */
-        IN_OUT("@InOut"),
+        IN_OUT,
 
         /**
          * Binds a data variable.
          * <p>
-         * A single variable must have at most one {@code @Out} binding. A variable with a {@code @Out} binding cannot
+         * A single variable must have at most one {@code OUT} binding. A variable with a {@code OUT} binding cannot
          * appear in any other place in a parameter list.
          * <p>
          * Cannot be used for node variables.
          */
-        OUT("@Out"),
+        OUT,
 
         /**
-         * Either takes a bound data variable or enumerates all possible data variable bindings.
+         * Takes an already bound variable.
          * <p>
-         * Cannot be used for data variables.
+         * May be used with node or data variables. An {@code IN_OUT} or {@code OUT} binding on the same parameter list
+         * cannot satisfy the {@code IN} binding, because it might introduce a (non-monotonic) circular dependency.
          */
-        NEGATIVE("@Negative"),
+        IN,
 
         /**
-         * Takes an already bound variable.
+         * Either takes a bound data variable or enumerates all possible data variable bindings.
          * <p>
-         * May be used with node or data variables. An {@code @InOut} or {@code @Out} binding on the same parameter list
-         * cannot satisfy the {@code @In} binding, because it might introduce a (non-monotonic) circular dependency.
+         * Cannot be used for data variables.
          */
-        IN("@In"),
+        NEUTRAL,
 
         /**
          * Enumerates over all possible data variable bindings.
@@ -51,49 +70,11 @@ public enum VariableDirection {
          * variable may only appear once in the parameter list, but node variables can appear multiple times to form
          * diagonal constraints.
          */
-        CLOSURE("@Closure");
-
-        private final String name;
-
-        VariableDirection(String name) {
-                this.name = name;
-        }
-
-        public VariableDirection merge(VariableDirection other) {
-                switch (this) {
-                case IN_OUT -> {
-                        if (other == IN_OUT) {
-                                return this;
-                        }
-                }
-                case OUT -> {
-                        if (other == OUT) {
-                                throw new IncompatibleParameterDirectionException("Multiple %s bindings".formatted(this));
-                        }
-                }
-                case NEGATIVE -> {
-                        if (other == NEGATIVE || other == IN || other == CLOSURE) {
-                                return other;
-                        }
-                }
-                case IN, CLOSURE -> {
-                        if (other == NEGATIVE || other == this) {
-                                return this;
-                        }
-                }
-                }
-                throw new IncompatibleParameterDirectionException("Incompatible variable directions %s and %s"
-                                .formatted(this, other));
-        }
-
-        @Override
-        public String toString() {
-                return name;
-        }
+        CLOSURE;
 
         public static VariableDirection from(boolean positive, ParameterDirection parameterDirection) {
                 return switch (parameterDirection) {
-                        case IN_OUT -> positive ? IN_OUT : NEGATIVE;
+                        case IN_OUT -> positive ? IN_OUT : NEUTRAL;
                         case OUT -> positive ? OUT : CLOSURE;
                         case IN -> IN;
                 };
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Parameter.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Parameter.java
index 29aedbef..351a353d 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Parameter.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Parameter.java
@@ -26,8 +26,12 @@ public class Parameter {
                 }
         }
 
+        public boolean isNodeVariable() {
+                return dataType == null;
+        }
+
         public boolean isDataVariable() {
-                return dataType != null;
+                return !isNodeVariable();
         }
 
         public Optional<Class<?>> tryGetType() {